Lysis VM

Tercera VM: instanciación estructural de plantillas con hash-consing y heap de spill. El ejemplo canónico de Bytecode-Oriented Compilation en Achronyme.

Por qué existe Lysis

Akron y Artik ejecutan ambos una vez por prueba. Lysis es diferente: separa compile/instantiate de la emisión en runtime. El walker emite un programa Lysis que, al correr, produce IR SSA — y el sink interning del ejecutor colapsa sub-árboles estructuralmente idénticos durante la emisión.

Concretamente: el expansor ávido legacy desenrollaba todos los loops e inlineaba todos los sub-templates por adelantado. Lysis difiere esa expansión a runtime y deduplica sub-grafos redundantes vía hash-consing. Los comentarios y tests actuales del árbol identifican circuitos con forma SHA-256(64) como el objetivo de escala motivador; las cifras exactas de tiempo y delta de constraints son salidas de benchmark, no invariantes arquitecturales.

Bytecode-Oriented Compilation (BOC)

Lysis es el ejemplo canónico de lo que llamamos Bytecode-Oriented Compilation (BOC) dentro de Achronyme: una arquitectura de compilador en la que el paso de compilación es él mismo un programa en bytecode, y la salida de la compilación es el efecto lateral de correr ese bytecode sobre una VM.

La forma:

Fuente → Bytecode → Correr sobre la VM → Salida de compilación

Dos distinciones que conviene hacer explícitas, porque BOC vive al lado de varios patrones con nombres parecidos:

• BOC no es “un compilador que emite bytecode”. javac y CPython producen bytecode como artefacto final — ese bytecode es dato, consumido después por un runtime separado. En BOC el bytecode se consume como parte de la compilación misma: cada paso que la VM ejecuta empuja una entrada hacia la salida. En el caso de Lysis, esas entradas son nodos SSA IR que terminan convertidos en constraints R1CS. El bytecode es el motor de la compilación, no su producto.
• BOC es staged compilation heterogénea. Los vecinos más cercanos en la literatura son multi-stage programming (MetaOCaml, Template Haskell), compile-time function execution (Zig comptime, D CTFE) y metacompilación (Forth). Todos ellos son típicamente homogéneos — el stage-2 produce código con la forma del stage-1, horneado en el mismo binario destino. BOC es heterogéneo: el bytecode de Lysis es un ISA distinto del de su salida, y la salida es un sistema de constraints, no un ejecutable.

La consecuencia práctica es que las pipelines BOC fallan y escalan como programas, no como estructuras de dato. El manejo de frame overflow, el heap de spill, la regla single-static-store del validador, la profundidad de llamada por defecto de 8192 — nada de eso existiría para un IR pasivo. Existen porque el meta-programa es un programa real sometido a límites de recurso reales, y el compile-time del compilador queda reificado como el runtime de esta VM. Cuando Lysis choca contra un límite, la solución rara vez es “cambiar la forma del dato”; suele ser “darle más capacidad al ejecutor” o “enseñarle un opcode nuevo al ejecutor”. Esa es la firma de BOC.

Dónde se ubica Lysis

El walker es el lifter del lado IR: consume ExtendedInstruction<F> (de ir-forge) y produce bytecode Lysis. El ejecutor es el lado VM: corre ese bytecode y emite SSA vía un sink.

Pipeline de lift (ir-forge::lysis_lift)

Archivo: ir-forge/src/lysis_lift/mod.rs. Cinco etapas:

Las cinco implementan evaluación diferida — las plantillas permanecen simbólicas hasta proof-time.

Encabezado del bytecode

0..4    magic "LYSI"
4..6    version (u16 LE)          — actual: 2 (los streams v1 decodifican con heap_size_hint = 0)
6       field_family (u8)         — BnLike256 | Goldilocks64
7       flags (u8)                — bit 0: has_witness_calls
8..12   const_pool_len (u32 LE)
12..16  body_len (u32 LE)
16..20  heap_size_hint (u32 LE)   — tamaño del heap de spill en entradas (sólo v2)
20..…   const_pool (entradas FieldConst + bytecode blobs para llamadas a Artik)
…..     body (stream de instrucciones)

El decodificador despacha sobre version y lee el encabezado v1 (16 bytes) cuando ve un stream v1, dejando heap_size_hint por defecto en 0.

Modelo de registros / frame

• Registros: 256 por frame, almacenados como Vec<Option<FieldElement<F>>> (indefinidos hasta que se escriben).
• Pila de frames: Vec<Frame> con pc, body_start_idx, body_end_idx, template_id, loop_stack: Vec<LoopState>.
• Estado de loop: cada LoopUnroll empuja un LoopState rastreando los límites de iteración; el paso advance_loops() del despachador incrementa y detecta completitud.
• Profundidad de llamada por defecto: 8192 (subida desde el original 64 para acomodar árboles de plantillas profundos como el message schedule de SHA-256).

Heap de spill

El heap del frame es un Vec<FieldElement<F>> plano alocado por ejecución del programa, dimensionado por heap_size_hint. Contiene valores que sobreviven al frame que los escribió — capturas invariantes de loop, arrays materializados de loops rolled, buffers de witness-call — que no caben en la ventana de 256 registros del frame activo.

Cada slot del heap está gobernado por un invariante de single-static-store: un slot se escribe exactamente una vez por ejecución. El validador rechaza programas que emiten dos StoreHeap al mismo slot, y el ejecutor trapea ante un LoadHeap desde un slot no escrito. Esto hace que el heap se comporte como registros SSA extendidos a un espacio de direcciones más ancho, con las mismas garantías de dataflow que el resto de la VM asume.

Tabla de opcodes (37 opcodes)

Archivo: lysis/src/bytecode/opcode.rs.

Los opcodes Emit* no computan resultados — empujan entradas al sink.

Sinks

El despachador escribe los opcodes que emiten IR en un trait object IrSink. Existen dos implementaciones:

• StubSink — no-op, usado por tests de esqueleto que ejercitan control flow sin materializar IR.
• InterningSink — hash-cons vía IndexMap<NodeKey, NodeId>. Default en producción. Materializa un Vec<Instruction<F>> plano vía sink.materialize().

Loop del despachador

Archivo: lysis/src/execute/mod.rs. Loop externo sobre frames + paso interno:

loop {
    check_instruction_budget()?;
    let instr = program.body[frame.pc];
    match dispatch(instr, ...)? {
        Step::Next => frame.pc += 1,
        Step::JumpToIndex(idx) => frame.pc = idx,
        Step::PushFrame(f) => stack.push(f),
        Step::PopFrame => stack.pop(),
        Step::Halt => break,
    }
    advance_loops()?;
}

Modelo de memoria

Sin GC. Los registros del frame viven en la struct del frame. El interner usa internamente un IndexMap<NodeKey, NodeId> prestado mutablemente durante la ejecución. El heap de spill es un único Vec<FieldElement<F>> propiedad del ejecutor durante una corrida del programa, reseteado entre ejecuciones.

Salida del lift → walker

Archivo: ir-forge/src/lysis_lift/walker/. Driver que consume Vec<ExtendedInstruction<F>>:

Cuando un body es demasiado ancho para mantener sus valores en la ventana de 256 registros — el body de la ronda de SHA-256 es el ejemplo canónico — el walker baja a unroll por iteración y rutea valores cargados por el loop a través de slots del heap, de modo que cada iteración arranca con un archivo de registros fresco.

Cobertura E2E

Preguntas abiertas

• Los números actuales de benchmark para SHA-256(64), MiMCSponge y deltas contra circom O2 deben regenerarse desde el harness de benchmarks antes de publicarse como conteos exactos o tiempos de pared.

Archivos fuente

Ver ProveIR para la capa que alimenta a Lysis. Ver Akron VM y Artik Witness VM para las otras dos VMs.