Lysis VM (en progreso)

Tercera VM: instanciación estructural de plantillas con hash-consing. Estado: Fase 3.B entregada.

Estado

Lysis está en progreso. Las fases 0–2 + 3.A + 3.B + 3.C.6 P1 + P1.5 están entregadas (al 2026-04-24). La Fase 3.C (oracle gate, 7 fixtures × 3 fields, 38 E2E de circom vía la ruta Lysis, HARD GATE de SHA-256(64)) es el siguiente entregable.

Esta página está sujeta a cambios — los números de opcodes y la semántica de los sinks pueden evolucionar antes de que cierre la Fase 3.C. Trátala como el estado actual de la implementación, no un contrato estable.

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 legacy ir::prove_ir::instantiate (~3,025 LOC) expande plantillas de manera ávida y desenrolla loops. Lysis difiere esa expansión a runtime y deduplica sub-grafos redundantes vía hash-consing — se midió una reducción de constraints de 58.3× en el esqueleto SHA-256(64) en la Fase 2.

Dónde se ubica Lysis

ProveIR
  │
  ▼
ir-forge::lysis_lift::walker  ── BTA + extract + diff + symbolic ──▶  Lysis bytecode (.lysis)
                                                                              │
                                                                              ▼
                                                              lysis::execute (interpreter)
                                                                              │
                                                                              ▼
                                                              InterningSink (hash-cons)
                                                                              │
                                                                              ▼
                                                              Vec<Instruction<F>>  (IR-SSA)
                                                                              │
                                                                              ▼
                                                                          R1CS / Plonkish

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: crates/ir-forge/src/lysis_lift/mod.rs. Cinco fases:

Las cinco implementan el RFC §6 (Lysis Fase 3.B) con evaluación diferida — las plantillas permanecen simbólicas hasta proof-time.

Encabezado del bytecode

0..4    magic "AALSS"  (0xAA 0x4C 0x53 0x53)
4..5    version (u8)
5..6    field_family (u8)        — BnLike256 | Goldilocks64
6..…    const_pool (FieldConst entries + bytecode blobs for Artik calls)
…..     body (instruction stream)

Las secciones más allá del cuerpo están por definir — la Fase 3 puede agregar una sección de tabla de plantillas.

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.

Tabla de opcodes (29 opcodes)

Sujeto a cambios. Archivo: crates/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 (Fase 1, usado para tests de esqueleto)
• InterningSink — hash-cons vía IndexMap<NodeKey, NodeId>. Default de la Fase 2. Materializa un Vec<Instruction<F>> plano vía sink.materialize().

Futuro: la Fase 4 puede agregar un RecordingSink para el oracle gate.

Loop del despachador

Archivo: crates/lysis/src/execute/mod.rs:77-179. 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.

Salida del lift → walker

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

Oracle (andamiaje de la Fase 3.C)

Archivo: crates/zkc/src/lysis_oracle/. Compara el R1CS emitido por Lysis contra el R1CS directo de circom vía:

1. canonicalize_ssa — renombrado topológico de variables SSA
2. semantic_equivalence — comparación de constraints como multiset + solver de testigos

La Fase 3.C debe pasar: 7 fixtures × 3 fields = 21 celdas del oracle, todas en verde.

HARD GATE de SHA-256(64)

El benchmark bloqueante es Decompose(254) en Num2Bits_strict para slicing de arrays de bits de SHA.

• Fase 2 (superada el 2026-04-20): el interner logró 58.3× de reducción de constraints vs desenrollado ávido.
• Gate de la Fase 3: wallclock de SHA-256(64) < 60s, conteo de constraints dentro de ±5% de circom O2.

Snapshot del estado de fases

Archivos fuente

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