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. The most demanding workload it now carries end-to-end is ECDSAVerify(64,4) — the heaviest circomlib reference circuit (secp256k1 ECDSA) — which lifts, generates a witness, and proves through Groth16 with the witness verifying (optimized R1CS ~1.49M constraints, below circom’s own count for the same circuit).

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

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

Control flow

TagOpcodeOperands
0x01Jumptarget: u32
0x02JumpIfcond: Reg, target: u32
0x03Return-
0x04Trapcode: u16
0x05Callfunc_id: u32, args: Vec<Reg>, rets: Vec<Reg>

Call invokes another subprogram by func_id: argument registers are copied cell-for-cell into the callee’s parameter registers and return values land back in the caller’s rets. Array cells carry a handle into the program-global array store, so array arguments and returns cross frames with no backing copy. This is what makes Artik a multi-subprogram VM — a lifted Circom body can call sibling functions instead of forcing everything to inline.

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)
0x26FIDivdst, a, b (field-precision integer quotient, traps on b == 0)
0x27FIRemdst, a, b (field-precision integer remainder, traps on b == 0)
0x28FShrdst, src, amount: u32 (field-precision right shift)
0x29FAnddst, src, mask_const_id: u32 (field-precision bitmask)
0x2AFPow2dst, amount: Reg (computes 1 << amount at full field width)
0x2BFCmpLtdst, a, b (field-precision unsigned ordered compare, dst is U8)

FIDiv, FIRem, FShr, FAnd, and FPow2 operate at full field precision rather than demoting to a fixed integer width, so bignum-style limb arithmetic stays exact. FCmpLt is the field-level unsigned ordered comparison that the secp256k1 long-division and modular-reduction bodies depend on — an ordered < that holds across the full 256-bit field value, not a U64-truncated compare.

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
0x53ArrayIddst, arr (read an array’s store handle into a register)
0x54ArrayFromIddst, id, elem: ElemT (rebind a register-carried handle as a typed array)

Arrays live in a bump-allocated Vec managed by the executor — no GC. ArrayId / ArrayFromId pass array handles through scalar registers, which is how arrays travel across Call frames and how 2D row slices are addressed without copying the backing cells.

Native bignum intrinsics

A handful of multi-limb bignum routines (secp256k1’s Fermat-style modular inverse, modular exponentiation, schoolbook product, and long division) are too slow to interpret limb-by-limb. The lift fingerprints these function bodies and, on a match, executes them natively as ModInv, ModExp, Prod, or LongDiv instead of walking the interpreted bytecode:

IntrinsicRecognized body
ModInvFermat modular inverse (a^(p−2) mod p)
ModExpsquare-and-multiply modular exponentiation
Prodschoolbook multi-limb product
LongDivschoolbook long division (quotient + remainder)

Each recognized body still falls back to the interpreted path if its fingerprint does not match exactly, so soundness is unchanged. The native path is what dropped the ECDSAVerify(64,4) witness walk from roughly 226 s to 64 s end-to-end — the interpreted Fermat inversion was 98.6% of the walk — with constraint count and verification identical.

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.

Recently closed gaps

The three biggest historical lift gaps are all closed — they are exactly what enabled the secp256k1 ECDSA witness closure:

  • Array parameters — function bodies with array params (sha256compression(hin[256], inp[512]), secp256k1 helpers) lift via call-site dimension inference + array binding, no longer bailing to E212.
  • Multi-dimensional arrays — 2D row slices (var M[t][t], pubkey[2][k]) are addressed and passed through array handles, not just 1D.
  • Runtime loop bounds — loops with a signal-dependent or descending end are lifted using Artik’s JumpIf instead of requiring a compile-time unroll.

Remaining limits

  • Plonkish backend — returns a clean error on WitnessCall. R1CS is the sole proving path for Artik this release.

E2E coverage

CasePath
ECDSAVerify(64,4) (secp256k1)lift -> R1CS -> witness -> Groth16 (verified, ~1.49M constraints, below circom)
SHA-256 sigma0lift -> R1CS -> witness (end-to-end verified)
Pedersen_old(8)field-aware BigVal + lift -> R1CS
EdDSaMiMCVerifierlift + R1CS with enabled=0
Fuzz (10M-iter soak)clean exit on bytecode decode + execute targets

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/
IR dispatchir/src/eval/mod.rs::dispatch_witness_call
R1CS dispatchzkc/src/witness/artik.rs::dispatch_artik_call
IR variantir-core/src/types/instruction.rsInstruction::WitnessCall
Navigation