Lysis VM (in-progress)

Third VM: structural template instantiation with hash-consing. Status: Phase 3.B shipped.

Status

Lysis is in-progress. Phases 0–2 + 3.A + 3.B + 3.C.6 P1 + P1.5 are shipped (as of 2026-04-24). Phase 3.C (oracle gate, 7 fixtures × 3 fields, 38 circom E2E via Lysis path, SHA-256(64) HARD GATE) is the next deliverable.

This page is subject to change — opcode numbers and sink semantics may evolve before Phase 3.C closes. Treat it as the current state of the implementation, not a stable contract.

Why Lysis exists

Akron and Artik both execute once per proof. Lysis is different: it separates compile/instantiate from runtime emission. The walker emits a Lysis program that, when run, produces SSA IR — and the executor’s interning sink collapses structurally identical sub-trees during emission.

Concretely: the legacy ir::prove_ir::instantiate (~3,025 LOC) eagerly expands templates and unrolls loops. Lysis defers that expansion to runtime and dedupes redundant sub-graphs via hash-consing — a 58.3× constraint reduction was measured on the SHA-256(64) skeleton in Phase 2.

Where Lysis sits

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

The walker is the IR-side lifter: it consumes ExtendedInstruction<F> (from ir-forge) and produces Lysis bytecode. The executor is the VM side: it runs that bytecode and emits SSA via a sink.

Lift pipeline (ir-forge::lysis_lift)

File: crates/ir-forge/src/lysis_lift/mod.rs. Five phases:

All five implement RFC §6 (Lysis Phase 3.B) with deferred evaluation — templates remain symbolic until proof-time.

Bytecode header

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)

Sections beyond the body are TBD — Phase 3 may add a template-table section.

Register / frame model

• Registers: 256 per frame, stored as Vec<Option<FieldElement<F>>> (undefined until written).
• Frame stack: Vec<Frame> with pc, body_start_idx, body_end_idx, template_id, loop_stack: Vec<LoopState>.
• Loop state: each LoopUnroll pushes a LoopState tracking iteration bounds; the dispatcher’s advance_loops() step increments and detects completion.

Opcode table (29 opcodes)

Subject to change. File: crates/lysis/src/bytecode/opcode.rs.

Emit* opcodes don’t compute results — they push entries into the sink.

Sinks

The dispatcher writes IR-emitting opcodes into a IrSink trait object. Two implementations exist:

• StubSink — no-op (Phase 1, used for skeleton tests)
• InterningSink — hash-cons via IndexMap<NodeKey, NodeId>. Phase 2 default. Materialises a flat Vec<Instruction<F>> via sink.materialize().

Future: Phase 4 may add a RecordingSink for the oracle gate.

Dispatcher loop

File: crates/lysis/src/execute/mod.rs:77-179. Outer loop over frames + inner step:

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()?;
}

Memory model

No GC. Frame registers live in the frame struct. The interner internally uses IndexMap<NodeKey, NodeId> borrowed mutably during execution.

Lift output → walker

File: crates/ir-forge/src/lysis_lift/walker.rs. Driver that consumes Vec<ExtendedInstruction<F>>:

Oracle (Phase 3.C scaffold)

File: crates/zkc/src/lysis_oracle/. Compares Lysis-emitted R1CS against circom-direct R1CS via:

1. canonicalize_ssa — topological renaming of SSA vars
2. semantic_equivalence — multiset constraint comparison + witness solver

Phase 3.C must pass: 7 fixtures × 3 fields = 21 oracle cells, all green.

SHA-256(64) HARD GATE

The blocking benchmark is Decompose(254) in Num2Bits_strict for SHA bit-array slicing.

• Phase 2 (cleared 2026-04-20): interner achieved 58.3× constraint reduction vs eager unroll.
• Phase 3 gate: SHA-256(64) wallclock < 60s, constraint count within ±5% of circom O2.

Phase status snapshot

Source files

See ProveIR for the layer feeding Lysis. See Akron VM and Artik Witness VM for the other two VMs.