Introducing Achronyme — a language for zero-knowledge proofs. Read the announcement arrow_right_alt

Artik Witness VM

Register-based witness-computation VM: bytecode, lift surface, and R1CS dispatch.

Artik is a dedicated, register-based VM for witness computation in Achronyme circuits. It closes the E212 gap — the class of Circom functions (with var, for, if/else, nested calls, and runtime signal arguments) that previously could not be inlined into a circuit.

Artik is paired with Akron, the general-purpose bytecode VM. Unlike Akron, Artik has no heap, no GC, no tagged values at runtime, and no shared state with the main VM. It is a one-shot interpreter: signals in, witness slots out.

Why Artik exists

Before Artik, any non-trivial function body with signal arguments surfaced as E212 — function body not inlineable with runtime signal arguments. Circom solves the same problem with witness calculators executed at prove time; SHA-256, Pedersen, and EdDSA-family primitives all need this.

Artik lifts those function bodies to a compact bytecode, emits an Instruction::WitnessCall in the IR, and executes the bytecode at R1CS witness-gen time against the live witness vector.

Architecture

Circom .circom
    |
    v
circom::lowering (ProveIR)
    |
    +-- pure expression? --> CircuitExpr (inline)
    |
    +-- complex body?     --> artik_lift --> Artik bytecode
                                                |
                                                v
                                      Instruction::WitnessCall { program_bytes }
                                                |
                                                v
                              R1CS backend: WitnessOp::ArtikCall
                                                |
                                                v
                              WitnessGenerator::execute_op --> artik::execute

Crate layout

artik/
  src/
    lib.rs        // re-exports, public surface
    header.rs     // 16-byte header + FieldFamily
    ir.rs         // Instr, IntW, IntBinOp, RegType, OpTag
    program.rs    // Program + FieldConstEntry
    bytecode/
      encode.rs   // Program -> bytes
      decode.rs   // bytes -> Program (runs validator)
    validate.rs   // structural invariants
    executor.rs   // execute / execute_with_budget
    builder.rs    // ProgramBuilder API (used by the lift)
    error.rs      // ArtikError

Bytecode format

Every .artik program is prefixed by a 16-byte header:

0..4   magic "ARTK"
4..6   version (u16 LE)           // current: 1
6      field_family (u8)          // 0=BnLike256, 1=Goldilocks64, 2=M31_32
7      flags (u8)
8..12  const_pool_len (u32 LE)
12..16 body_len (u32 LE)

The body begins with a 4-byte frame_size prelude, then a sequence of encoded instructions. The validator checks every decoded program before the executor touches it.

FieldFamily

FamilyPrimesMax const bytes
BnLike256BN254, BLS12-381, Grumpkin, Pallas, Vesta, Secp256r1, BLS12-37732
Goldilocks64Goldilocks (2^64 - 2^32 + 1)8
M31_32Mersenne-31 (reserved for v2)4

A single .artik blob can be executed against any prime in its declared family — the runtime picks up F from the caller.

Registers & types

Artik is SSA-style: each register is assigned at most once per function (enforced at emit time). Every register carries a type category, tracked by the validator:

enum RegType {
    Field,
    Int(IntW),          // U8 | U32 | U64 | I64
    Array(ElemT),       // Field | IntU8 | IntU32 | IntU64 | IntI64
}

Integer ops are bit-exact with wrapping semantics; width-specific mask is applied on every arithmetic output. Field and int registers cannot mix without an explicit IntFromField / FieldFromInt conversion.

Opcodes

~25 opcodes, grouped by category. Encoding is <opcode tag>(1 byte) + operands.

Control flow

TagOpcodeOperands
0x01Jumptarget: u32
0x02JumpIfcond: Reg, target: u32
0x03Return-
0x04Trapcode: u16

Constants & signals

TagOpcodeOperands
0x10PushConstdst: Reg, const_id: u32
0x11ReadSignaldst: Reg, signal_id: u32
0x12WriteWitnessslot_id: u32, src: Reg

Signals are read-only; witness slots are the sole output channel.

Field ops

TagOpcodeOperands
0x20FAdddst, a, b
0x21FSubdst, a, b
0x22FMuldst, a, b
0x23FDivdst, a, b
0x24FInvdst, src
0x25FEqdst, a, b (dst is U8: 0 or 1)

Integer ops

TagOpcodeOperands
0x30IBinop: IntBinOp, w: IntW, dst, a, b
0x31INotw: IntW, dst, src
0x32Rotl32dst, src, n
0x33Rotr32dst, src, n
0x34Rotl8dst, src, n

IntBinOp covers Add, Sub, Mul, And, Or, Xor, Shl, Shr, CmpLt, CmpEq. The SHA-family Rotl32 / Rotr32 / Rotl8 are first-class opcodes so bit-hash lowering stays compact.

Conversion

TagOpcodeOperands
0x40IntFromFieldw: IntW, dst, src
0x41FieldFromIntdst, src, w: IntW

Arrays

TagOpcodeOperands
0x50AllocArraydst, len: u32, elem: ElemT
0x51LoadArrdst, arr, idx
0x52StoreArrarr, idx, val

Arrays live in a bump-allocated Vec managed by the executor — no GC.

Static & runtime limits

The validator rejects adversarial bytecode before it reaches the executor:

LimitValueEnforced by
MAX_FRAME_SIZE2^16 registersvalidator
MAX_ARRAY_LEN2^20 cells per AllocArrayvalidator
MAX_ARRAY_MEMORY_CELLS2^24 cumulative cells per executeexecutor
DEFAULT_BUDGET8M instructions per callexecutor (execute_with_budget overrides)

Constants larger than family.max_const_bytes() are rejected. All traps surface as typed ArtikError variants.

Lift surface

circom::lowering::artik_lift compiles function bodies to Artik bytecode. What the lift currently accepts:

Statements

  • Scalar VarDecl and 1D array VarDecl
  • Scalar Substitution and indexed (arr[i] = expr) with runtime indices
  • Compound-assigns (+=, *=, etc.), with const-fold on loop variables
  • For with compile-time bounds (unrolled, max 4096 iterations)
  • IfElse — both compile-time folded and runtime via field-arithmetic mux
  • Return — scalar or array
  • Bare ++ / -- on loop variables

Expressions

  • Ident, Number, HexNumber
  • BinOpAdd/Sub/Mul/Div + bitwise And/Or/Xor/ShiftL/ShiftR via U32 int-promotion
  • UnaryOp::Neg and ::BitNot
  • Index with compile-time-folded or runtime index
  • Call — inlined, scalar or array return
  • Ternary

Runtime if/else mux

Both arms are lifted; scalar locals merge via the standard cond * then + (1 - cond) * else pattern. cond is normalized via FEq(cond, 0) -> FieldFromInt U8 -> 1 - is_zero. Branches must be side-effect-free (no array writes, no return).

Nested calls are admissible inside mux branches — nested returns capture into nested_result without emitting WriteWitness.

Runtime dispatch

ir::eval::evaluate + evaluate_lenient dispatch to artik::execute on every Instruction::WitnessCall:

Instruction::WitnessCall {
    outputs: Vec<Variable>,        // witness slots to fill
    inputs: Vec<LinearCombination>, // signals, materialized into LC wires
    program_bytes: Vec<u8>,        // the .artik blob
}

The R1CS backend materializes each input LC into a fresh witness wire, allocates wires for each output, and emits a WitnessOp::ArtikCall into the trace. At witness-gen time, WitnessGenerator::execute_op decodes the bytecode and runs Artik against the live witness vector.

See Witness Generation for the full trace replay model.

Design decisions

  • Side-channel via Instruction::WitnessCall, not a separate side-table on IrProgram. Keeps witness programs in instruction order so the prover’s witness-gen loop naturally interleaves them between other WitnessOp replays. Cost: ~8 exhaustive match sites extended across ir + zkc.
  • Primary output = outputs[0], extras via extra_result_vars. Array-returning lifts expose secondary witness slots this way. Non-empty invariant enforced by the lift.
  • Public outputs win over fresh witness wires. Instantiate reuses output_pub_vars[name] when the binding name matches a public output signal, so Artik writes directly into the public-output wire.
  • BN-family check via F::PRIME_ID, not type_name. Cleaner and catches Goldilocks as unsupported rather than silently accepting.
  • No heap, no GC. Arrays are bump-allocated into a single Vec owned by the executor. A program is one-shot: it runs once per proof, then drops.

Current limits

  • Array parameters — biggest remaining gap. sha256compression(hin[256], inp[512]) bails to E212 because the lift maps each param to a single ReadSignal. Needs call-site dimension inference + N-signal allocation + array binding.
  • Multi-dim arrays (var M[t][t]) — current support is 1D only.
  • Runtime loop bounds — loops with signal-dependent end are not unrolled; Artik’s JumpIf is not yet used by the lift.
  • Plonkish backend — returns a clean error on WitnessCall. R1CS is the sole proving path for Artik this release.

E2E coverage

CasePath
SHA-256 sigma0lift -> R1CS -> witness (end-to-end verified)
Pedersen_old(8)field-aware BigVal + lift -> R1CS
EdDSaMiMCVerifierlift + R1CS with enabled=0
Fuzz (180s / target)62M runs / 0 crashes after Fase 6 hardening

Source files

ComponentFile
IR + opcodesartik/src/ir.rs
Header + familiesartik/src/header.rs
Programartik/src/program.rs
Encode / decodeartik/src/bytecode/
Validatorartik/src/validate.rs
Executorartik/src/executor.rs
Builder API (used by lift)artik/src/builder.rs
Circom liftcircom/src/lowering/artik_lift.rs
IR dispatchir/src/eval/mod.rs::dispatch_witness_call
R1CS dispatchzkc/src/r1cs_witness.rs::dispatch_artik_call
IR variantir/src/types.rsInstruction::WitnessCall
Navigation