Changelog

Release history for Achronyme.

All notable changes to Achronyme are documented here. Each release bumps all 10 workspace crates to the same version.

0.1.0-beta.20 — Unreleased

Circom frontend: compile .circom files through Achronyme’s pipeline with structural safety guarantees that the original compiler doesn’t provide.

New: ach circom command

End-to-end compilation of .circom files: parse → constraint analysis → lower to ProveIR → optimize → R1CS → Groth16 proof.

ach circom circuit.circom --inputs "a=3,b=7" --prove

Supports --input-file input.toml, --prove, --r1cs, --wtns, --solidity, and --prove-backend r1cs|plonkish.

New: Circom parser (full Circom 2.x syntax)

Hand-written Pratt parser covering all Circom constructs: templates, functions, signals (input/output/intermediate), component declarations, <==, <--, -->, ==>, ===, for/while/if-else, anonymous components, parallel ops, tags, pragmas, includes.

New: WitnessHint — correct <-- semantics

<-- in Circom is a witness computation hint with zero constraints. Our CircuitNode::WitnessHint models this correctly: the hint expression is evaluated off-circuit by the prover, and only === constraints verify the result. This prevents the Circom-common bug where witness hints accidentally inflate constraint counts.

A dedicated witness evaluator computes hint values using integer arithmetic on the canonical 4-limb representation, supporting all bitwise operations (>>, <<, &, |, ^, ~) natively.

New: E100 — under-constrained signal detection

Hard error when a signal assigned via <-- has no corresponding === constraint. This catches the #1 source of ZK vulnerabilities at compile time — bare <-- without verification.

New: W101 — unconstrained input/output signal warning

Warning when an input or output signal doesn’t participate in any constraint expression. A malicious prover can set unverified signals to arbitrary values. The original Circom compiler does not detect this.

warning: input signal `in` is not referenced in any constraint
  note: a input signal that doesn't participate in constraints cannot be verified
        — a malicious prover can set it to any value

New: Bitwise operations via Decompose

Six new CircuitExpr variants (BitAnd, BitOr, BitXor, BitNot, ShiftR, ShiftL) expanded during instantiation using the existing Decompose infrastructure. Each operation decomposes operands into bits, applies the operation per bit using field arithmetic (AND = multiply, OR = a+b−ab, XOR = a+b−2ab), and recomposes the result.

New: Large number literals

FieldConst::from_decimal_str and from_hex_str support constants up to 256 bits, covering the full BN254 field range. The Circom lowering falls back to these when literals exceed u64.

New: Component inlining and function inlining

Component instantiation (component c = Template(args)) inlines the template body with .-separated name mangling (collision-free by construction — . cannot appear in Circom identifiers). Function calls are inlined with parameter substitution, depth-limited to 64 levels.

New: Capture classification

Template parameters are classified as StructureOnly (loop bounds, array sizes), CircuitInput (constraint expressions), or Both, enabling ProveIR to optimize how captures are resolved during instantiation.

New: E2E Groth16 proofs for 33 circomlib templates

Full pipeline verified end-to-end for 33 real circomlib circuits: Multiplier, logic gates (AND, OR, XOR, NOT, NAND, NOR), MultiAND, Num2Bits(8), Bits2Num(8), IsZero, IsEqual, Mux1, MultiMux1/2/4, Switcher, BinSum(4), LessThan(8), LessEqThan(8), GreaterThan(8), GreaterEqThan(8), ForceEqualIfEnabled, RangeProof(8), Min(8), AbsDiff(8), Decoder(4), DoubleMultiplier, MerkleProof(2), ParallelMul(3), FuncNbits, FuncSimple, Poseidon(2). Each generates and verifies a Groth16 proof on BN254.

Poseidon(2) compiles the real circomlib implementation through include chains (poseidon.circom → poseidon_constants.circom → helper functions) using compile-time array evaluation for the 960+ round constants.

New: Dynamic loop bounds in prove {} blocks

for i in 0..n and for i in 0..n+1 now work in prove blocks when n is captured from the outer scope. The parser accepts ForIterable::ExprRange, and the ProveIR compiler emits ForRange::WithCapture (simple captures) or ForRange::WithExpr (computed expressions). The loop is unrolled at instantiation time when capture values are known.

let size = 8
prove my_proof(result: Public) {
    for i in 0..size {
        // size is auto-captured from outer scope
    }
    for i in 0..size + 1 {
        // computed bounds work too
    }
}

New: Computed template arguments in component inlining

Component instantiation with expression arguments like Num2Bits(n+1) inside templates (e.g., LessThan) now works correctly. The ForRange::WithExpr variant preserves the bound expression through inlining, and the instantiator evaluates it using eval_const_expr when capture values are resolved.

New: Compile-time function evaluation

Circom function bodies with imperative logic (var, while, for, if/else, return, ++, *=, nested calls) are now fully evaluated at compile time. Functions like nbits(a) that compute array sizes or loop bounds resolve to constants during lowering — no runtime overhead.

A pre-pass (precompute_vars) evaluates var declarations before signal layout extraction, enabling patterns like var nb = nbits(n); signal output out[nb]; where the output array size depends on a function result.

function nbits(a) {
    var n = 1;
    var r = 0;
    while (n - 1 < a) { r++; n *= 2; }
    return r;
}

template T(maxval) {
    var nb = nbits(maxval);      // evaluated at compile time → 8
    signal output out[nb];       // array dimension resolved from function result
}
component main = T(255);

New: Component arrays

component muls[n] declares an array of component instances. Loop bodies containing component array operations (muls[i] = Template(), muls[i].signal <== expr) are automatically unrolled at lowering time using known_constants, since component inlining requires concrete names like muls_0, muls_1.

New: Multi-dimensional array support

N-dimensional signal arrays like signal c[n][2] are linearized using stride-based indexing during lowering. c[i][j] compiles to c[i*2+j], generalizing to arbitrary dimensions with strides computed right-to-left.

New: Indexed array assignment in prove {} blocks

Mutable arrays in .ach prove blocks support indexed assignment: mut arr = [0, 0, 0]; arr[i] = expr emits CircuitNode::LetIndexed. Validates that the array exists and is declared with mut. Works in both prove {} blocks and .ach circuit files.

Improved: Capture resolution in shifts and array indices

Shift operations (x >> n, 1 << n) and array indexing (arr[n]) now resolve captures at instantiation time via eval_const_expr, falling back to the previous extract_const method. This enables patterns where a template parameter is used both structurally (loop bounds) and in constraint expressions.

Improved: Lazy Mux evaluation in witness hints

The witness evaluator now short-circuits ternary expressions (cond ? a : b), only evaluating the taken branch. This prevents division-by-zero errors in patterns like in != 0 ? 1/in : 0 (used by IsZero) when the condition is false.

New: Include resolution with -l flag

Multi-file compilation with include directives:

ach circom circuit.circom -l ./node_modules/circomlib/circuits/

The compile_file() API resolves include directives by searching the file’s directory first, then any -l library directories. Mutual includes are deduplicated by canonical path. Circular includes are detected and reported.

New: Array-returning functions and compile-time array variables

Functions like POSEIDON_C(t) that return arrays via if-else chains are fully evaluated at compile time. EvalValue supports three forms: Scalar(i64), Array(Vec<EvalValue>), and Expr(Box<Expr>) for constants too large for i64 (256-bit field elements).

function POSEIDON_C(t) {
    if (t == 2) { return [0x09c46e..., 0x0c19da..., ...]; }
    // ... 960+ constants per configuration
}

template Poseidon(nInputs) {
    var t = nInputs + 1;
    var C[t] = POSEIDON_C(t);   // evaluated at compile time
    var M[t][t] = POSEIDON_M(t); // 2-D arrays with stride linearization
    // C[i+r] resolves from known_array_values during lowering
}

2-D arrays are flattened with stride-based indexing: M[i][j] compiles to M[i*cols+j]. A unified precompute_all pass processes both scalar and array vars in declaration order, allowing later vars to reference earlier ones (e.g., var nRoundsP = N_ROUNDS_P[t - 2]).

New: Structured diagnostics — rustc-style error reporting

Circom errors now render with source snippets, underlined spans, error codes, and ANSI colors — identical to Achronyme’s native .ach diagnostic output:

error[E200]: undefined variable `amout` in circuit context
  --> circuit.circom:6:16
  |
6 |     result <== amout * 2;
  |                ^^^^^
  |
  = help: a similar name exists in scope: `amount`

All error types produce structured Diagnostic objects:

• E100–E102, W101–W103: Constraint analysis (existing)
• E200: Undefined variable/signal (with “did you mean?” via Levenshtein distance)
• E201: Undefined function (with suggestion)
• E202: Undefined template (with suggestion)
• E203–E204: Include errors (I/O, not found, circular)
• E205: Unsupported features (bus types, custom templates)
• E206: Arity mismatch
• E208: Loop constraint violations
• E209: Compile-time evaluation failures
• E210–E211: Missing or undefined main component

Three output formats via --error-format: human (default, rustc-style), json (JSON Lines for tooling), short (file:line:col: severity: message).

Improved: Lowering architecture

The lowering pipeline was refactored from 3 monolithic files (4,959 LOC combined) into 21 focused modules, with no file exceeding 400 lines of production code. The component wiring state machine protocol is now formally documented. All production unwrap()/panic!() calls either carry // SAFETY: justification or were replaced with proper error propagation.

New: BigVal 256-bit evaluator

Compile-time variable evaluation migrated from i64 to BigVal([u64; 4]) — a 256-bit two’s complement type with full arithmetic (add, sub, mul, div, mod, shifts, bitwise ops, comparisons). Parameter maps upgraded from u64 to FieldConst. This unblocks circuits like CompConstant whose vars compute (1 << 128) - 1, which overflowed with i64.

New: Mixed signal+var loop unrolling

Loops whose body both writes signals and mutates vars (e.g., CompConstant’s for that updates b, a, e each iteration while also constraining signals) are now detected and fully unrolled. This ensures var values are concrete constants when used as coefficients in signal expressions — required for valid R1CS.

New: 2D array literal support in lowering

Nested array literals like var BASE[10][2] = [[...], ...] (Pedersen’s 10 BabyJubjub base points, each a 254-bit (x, y) pair) are now handled correctly. The precompute pass evaluates them at compile time; the lowering skips re-processing and resolves values from known_array_values during component inlining.

Fix: R1CS auto-materialization — prevents OOM on large circuits

Circom-lowered Poseidon has 57 partial rounds where state elements only receive linear operations (MDS with constant coefficients). Without materialization, LinearCombination terms grow exponentially — f(n) ≈ 2^n — causing >12 GB memory usage and OOM kills.

Three targeted fixes:

1. Auto-materialize Add/Sub results exceeding 8 terms in the R1CS compiler
2. Materialize source LCs before bit-decomposition loops (avoids cloning large LCs 252+ times into WitnessOps)
3. Same for Decompose instructions

This mirrors the optimization already present in the native Poseidon circuit (constraints/src/poseidon/circuit.rs) but applied generically to all IR-generated constraints.

Expanded: circomlib E2E R1CS coverage — 21 verified circuits

Full constraint system verification (compile → instantiate → R1CS → witness → verify) now covers 21 real circomlib circuits. Constraint counts below are post-optimizer (O1); circom reference is --O1 unless noted.

EdDSAPoseidon (full EdDSA signature verification over BabyJubjub with Poseidon hash) is verified end-to-end with 3,965 post-optimizer constraints — 2.04× fewer than circom’s --O1 output at 8,086. Pedersen and EscalarMulFix match circom’s --O2 output without an equivalent O2 pass.

New: R1CS linear constraint optimizer (O1 + O2)

Two-tier optimizer that reduces constraint count after compilation:

O1 — Linear elimination (single pass):

1. Frequency heuristic: selects the most-referenced wire for substitution to maximize cascading simplifications
2. Linear elimination: substitutes wires defined by k * LC = LC, removing the constraint entirely
3. Deduplication: removes identical constraints produced by variable substitution
4. Tautological removal: drops zero-product constraints (0 = 0) that arise after substitution

O2 — Algebraic deduction (optional second pass, with rollback): 5. DEDUCE: Gaussian elimination on the quadratic monomial matrix. Finds linear combinations of quadratic constraints that yield purely linear equations, introducing new wire equations without adding constraints. Applied iteratively until convergence. 6. Constant propagation: substitutes wires proven equal to field constants, collapsing entire sub-expressions. Wired constants from component inlining (e.g., Pedersen base points) propagate through Montgomery/Edwards arithmetic — the entire chain reduces to zero constraints per base operation. 7. Rollback: if DEDUCE+constant-prop does not reduce the total constraint count, the O2 pass is discarded and O1 output is used.

Results on representative circuits (pre-opt → O1 → O2):

New: Bool propagation and bit-pattern inference

Two new IR optimization passes:

• Bool propagation: detects v * (v - 1) = 0 constraints (boolean checks) and propagates bit-proven status. Enables Decompose(v, N) to skip redundant boolean constraints on bits already proven.
• Bit-pattern bound inference: recognizes Num2Bits-style patterns (bit decomposition + linear recombination) and marks decomposed bits as proven boolean — avoids double-constraining in circuits that compose Num2Bits internally.

Fix: signal output mapped to public R1CS wires

Previously, signal output declarations were discarded during ProveIR assembly — output signals had no public R1CS wires. DCE then eliminated all constraints in circuits whose only observable behavior was through outputs (Multiplier, AND, OR, NOT, Switcher, Bits2Num, etc. → 0 constraints).

The fix adds outputs to ProveIR.public_inputs and introduces instantiate_with_outputs() which allocates public wires for each output signal. Body nodes (WitnessHint, Let) that assign to output signals reuse the public wire instead of creating duplicate witness wires, ensuring exactly one wire per signal with correct R1CS semantics.

Improved: Constant folding in instantiation

• ShiftL/ShiftR with constant operands are folded at instantiation time (47× instruction reduction on EscalarMulAny)
• Decompose(Const(k), N) is expanded to N bit constants directly
• Tautological AssertEq(x, x) instructions eliminated during DCE

Fix: duplicate constraints from <== lowering

<== was incorrectly emitting both a Let node and an AssertEq node, with the RHS expression cloned into both. Every multiplication in the RHS produced two R1CS constraints — one real, one duplicate. Circuits with many <== signal assignments (essentially all of circomlib) produced approximately 2× the correct constraint count.

The fix: <== now emits only Let. The R1CS backend derives the constraint from the Let expression’s Mul instructions. The AssertEq is only needed for explicit === statements.

Improved: Constant propagation through component inlining

When a component input is wired to a compile-time constant (S.in <== BASE_POINT_X), that constant is now injected into the sub-template’s known_constants before lowering its body. Expressions that depend solely on constants are folded at lowering time using exact BN254 modular arithmetic (try_fold_const).

This enables full constant folding of:

• Montgomery operations with known base points (add, double, affine conversion)
• Edwards operations with known base points
• MUX tables where constant inputs collapse selector-independent paths

Impact on Pedersen(8): 8 Window4 selectors × base-point wiring → 2 Montgomery operations + 1 M2E conversion, all constant-folded. Constraint count: 88 → 13 (matching circom --O2).

Perf: Template body cache — 1.7× speedup on EscalarMulAny

Sub-templates instantiated multiple times with the same template parameters are now lowered once and cached. Subsequent instantiations re-use the unmangled body, applying only a fast name-mangling pass.

EscalarMulAny(254) instantiates SegmentMulAny(1) 254 times. After caching, the 254 re-instantiations cost ~10 µs each instead of full re-lowering. End-to-end lowering time for EscalarMulAny: 1,500 ms → 880 ms (1.7×).

Cache key: template_name:param₁=v₁:…. Only cacheable when const_inputs and array_args are empty (constant propagation changes the body; array args inject different compile-time arrays).

Fix: MiMCSponge soundness — loop variable contamination

In has_mixed_signal_var loops (loops whose body both constrains signals and mutates vars — e.g., MiMCFeistel’s round loop), var-only statements are evaluated at compile time via try_eval_stmt_in_place. On success, all eval_vars are written back to ctx.param_values so later signal expressions can use the updated var values.

The bug: the loop variable itself (e.g., i) was included in this write-back. For iteration i = 0, ctx.param_values["i"] = 0 was written. For i = 1, the else branch c = c_partial[i-1] failed compile-time evaluation (because c_partial is an array, not a scalar in eval_vars), so the write-back did not execute — and ctx.param_values["i"] remained 0 from the previous iteration.

all_constants() merges param_values and env.known_constants with or_insert (param_values wins). The correctly-set env.known_constants["i"] = 1 was always shadowed by the stale param_values["i"] = 0. Every ternary (i == 0) ? ... : ... evaluated to the i = 0 branch for all 220 iterations, collapsing the entire MiMC hash to a single computation.

The fix: exclude the loop variable from the param_values write-back. The loop variable is managed exclusively by env.known_constants at the top of each iteration.

Impact: MiMCSponge(2, 220, 1) — 19 constraints (unsound) → 2,581 pre-opt → 1,317 post-O1 — matching circom’s 1,320.

Breaking: :: path operator for module and circom namespace imports

Module-qualified access now uses the :: path operator instead of dot notation:

import "./math.ach" as math
import "./circomlib/poseidon.circom" as P

print(math::add(1, 2))          // was: math.add(1, 2)
let h = P::Poseidon(2)([a, b])  // was: P.Poseidon(2)([a, b])

The lookup is fully resolved at compile time — the compiler rewrites alias::name to the mangled global alias::name, reusing the same dispatch path that already handles built-in statics like Int::MAX, Field::ZERO, and BigInt::from_bits. There is no runtime alias object, no HashMap lookup per call, and the same syntax works inside VM code, circuit declarations, and prove {} blocks — closing the gap where dot-based dispatch used to break inside prove blocks.

The old alias.name / alias.func(...) forms produce a migration error that points at the correct spelling with a did-you-mean hint. Applies to both .ach module aliases and .circom library aliases.

See Modules and Importing Circom Templates for the full syntax reference.

0.1.0-beta.19 — 2026-04-02

Multi-prime field architecture: compile-time generics over any prime field.

New: FieldBackend trait and generic FieldElement<F>

The field layer is now generic over the prime. FieldElement<F: FieldBackend = Bn254Fr> wraps an associated Repr type (e.g., [u64; 4] for 254/255-bit curves, u64 for Goldilocks). One match at the session boundary selects the backend; monomorphization carries it everywhere else — no runtime overhead.

New: PrimeId enum

Identifies which prime field is in use across serialization boundaries and CLI flags. Supports 8 curves: BN254, BLS12-381, Goldilocks, Grumpkin, Pallas, Vesta, secp256r1, BLS12-377.

New: BLS12-381 scalar field backend

Bls12_381Fr — same CIOS Montgomery algorithm as BN254, different constants. 255-bit modulus, Repr = [u64; 4]. 28 unit tests including BigUint constant verification.

New: Goldilocks prime field backend

GoldilocksFr — the first non-Montgomery backend with Repr = u64. Uses the Goldilocks identity 2⁶⁴ ≡ 2³² − 1 (mod p) for fast branchless reduction without division. 36 unit tests including Fermat’s little theorem verification.

New: Multi-field Poseidon

PoseidonParams<F> is now generic over the field backend with a configurable S-box exponent (alpha). Constructors for BN254 (circomlibjs, α=5), BLS12-381 (LFSR, α=5), and Goldilocks (LFSR, α=7). The Grain LFSR generates paper-compliant constants for any field. Native hash functions (poseidon_hash, poseidon_permutation) are fully generic. R1CS sbox_circuit supports both α=5 (3 constraints) and α=7 (4 constraints).

0.1.0-beta.18 — 2026-03-30

Circom parity infrastructure, bit decomposition, integer division, array params/returns in circuit functions, inspector, proving crate, WASM LSP.

New: ach inspect command

Interactive DAG visualization for circuits and prove blocks. Compiles the source, builds a constraint graph with source span mapping, and serves an embedded HTML frontend on a local HTTP server.

ach inspect examples/inspect_membership.ach --input-file examples/inspect_membership.toml

Features:

• Constraint DAG — directed acyclic graph of IR instructions with variable flow edges.
• Source spans — each node links back to the original .ach source line.
• Witness evaluation — lenient evaluator computes concrete values for inspector tooltips, even when inputs are incomplete.
• Constraint origin tracking — the R1CS backend annotates each constraint with the IR instruction that generated it.

Built on a new ir::inspector module (~730 lines) that constructs the graph JSON from IrProgram metadata (var_spans, constraint origins).

Refactor: proving crate

The Groth16, Halo2/PlonK, and Solidity verifier modules have been extracted from cli into a standalone proving crate. This allows ach-server (and future consumers) to depend on proving logic without pulling in the full CLI. The workspace now has 10 crates.

New: Bool methods

let flag = true
print(flag.to_string())   // "true"
print(flag.to_int())      // 1

New: List.to_string() and improved value formatting

let xs = [1, 2, 3]
print(xs.to_string())   // "[1, 2, 3]"

Nested collections and mixed-type lists are formatted recursively with proper delimiters.

New: WASM LSP functions

The achronyme-wasm crate now exposes LSP functions (diagnostics, hover, completions) via ach-lsp-core, enabling language intelligence in the browser playground without a server round-trip.

Fix: ach init templates

The scaffolded main.ach, circuit.ach, and prove.ach templates generated by ach init have been updated to current syntax with working examples that compile and run out of the box.

ProveIR source span propagation

CircuitNode::Expr now carries source spans through instantiation, enabling the inspector (and future error messages) to point back to the original source location for each constraint.

Fix: array parameters and returns in circuit functions

Functions inside circuit and prove blocks can now accept array parameters and return arrays. Previously, the array type annotation on function parameters was silently ignored, causing a “expected scalar, got array” error when passing arrays. This enables a component-like composition pattern where reusable constraint-generating functions can be composed:

fn verify_path(leaf, siblings: Field[2], dirs: Field[2]) -> Field {
    let l1 = poseidon(mux(dirs[0] == 0, leaf, siblings[0]),
                       mux(dirs[0] == 0, siblings[0], leaf))
    let l2 = poseidon(mux(dirs[1] == 0, l1, siblings[1]),
                       mux(dirs[1] == 0, siblings[1], l1))
    l2
}

circuit main(root: Public, secret: Witness) {
    let path: Field[2] = [sibling0, sibling1]
    let dirs: Field[2] = [0, 0]
    assert_eq(verify_path(poseidon(secret, 0), path, dirs), root)
}

This is foundational infrastructure for a future Circom frontend: Circom templates map to functions, component instantiation maps to function calls, and signal wiring maps to array params/returns.

New: decompose() — bit decomposition with accessible bits

New builtin that decomposes a field element into individual bit variables:

circuit main(x: Witness) {
    let bits = decompose(x, 8)    // 8 boolean-constrained bit variables
    assert_eq(bits[1], 1)          // access individual bits
    assert_eq(bits[0] + bits[1] * 2 + bits[2] * 4, x)  // use in constraints
}

Unlike range_check, which verifies a value fits in N bits but doesn’t expose them, decompose returns the bits as an array. This is the Achronyme equivalent of Circom’s Num2Bits template — the foundation for bitwise operations, binary arithmetic, and most of circomlib.

Cost: N+1 constraints (N boolean checks + 1 sum equality).

New: int_div() and int_mod() — integer arithmetic in circuits

Integer quotient and remainder on field elements:

circuit main(a: Witness, b: Witness) {
    let q = int_div(a, b, 32)     // floor(a / b), 32-bit range check
    let r = int_mod(a, b, 32)     // a - b * floor(a / b)
    assert_eq(b * q + r, a)       // always holds
}

The third argument max_bits specifies the range check bound for soundness — it prevents a malicious prover from exploiting field wraparound. The user chooses the bound based on their value range (8 bits for bytes, 32 for counters, 64 for large values, 252 for full field).

These are the Achronyme equivalents of Circom’s \ and % operators.

Docs migration

The docs/ directory and its deploy workflow have been removed from the main repository. Documentation now lives in achronyme-web.

0.1.0-beta.17 — 2026-03-28

8.6x VM speedup, bytecode optimizer, ProveIR observability, WASM crate, OuterScope unification, 42% constraint reduction.

Performance: 1315ms → 303ms (8.6x with PGO)

Six VM hot-path optimizations and a three-pass bytecode optimizer bring the 10M-iteration benchmark from 1315ms to 303ms:

Three attempted optimizations were reverted after measurement showed no improvement with PGO (branch reordering, Result removal, specialized integer opcodes), confirming that with PGO the branch predictor already handles hot-path branches optimally — future gains must reduce work, not branches.

Bytecode optimizer (compiler/src/optimizer.rs)

Three peephole passes run on every function’s bytecode after compilation:

1. Redundant Load Elimination — SetGlobal Ra, idx; GetGlobal Rb, idx → Move Rb, Ra. Jump targets act as barriers.
2. Constant Hoisting (LICM) — Loop-invariant LoadConst moved before loop. Re-runs after register promotion to catch newly hoistable constants.
3. Register Promotion — Globals in call-free innermost loops promoted to local registers. GET_GLOBAL/SET_GLOBAL become Move, with one-time load before the loop and write-back at each exit point.

26 unit tests. The optimizer correctly handles continue (collapsed back-edges), nested loops (innermost-only promotion), and read-only globals (no write-back for let bindings).

ProveIR Display

ach disassemble examples/proof_of_membership.ach

  -- ProveIR block 1 (instruction 0134) --
  Captures:
    key_5                (witness)
    proof_path_0..2      (witness)
    proof_indices_0..2   (witness)
  Public inputs:
    merkle_root: Field
  Body:
    let my_commitment = poseidon($key_5, 0)
    merkle_verify(merkle_root, my_commitment, proof_path, proof_indices)

Human-readable representation of pre-compiled circuit templates. Captured variables prefixed with $ to distinguish them from circuit-local names. Shows captures with usage roles (witness/structure/both), typed inputs, and full circuit body with proper indentation.

Disassembler rewrite

The ach disassemble command now works from compiled artifacts instead of re-parsing source:

• Prove blocks — Deserialized from bytecode constant pool via ProveIR::from_bytes(). Previously failed with “expected expression, found ..”.
• Circuit declarations — circuit name(params) { body } extracted from AST with span-based source slicing. Previously failed with “circuit declarations not supported inside circuits”.

New: achronyme-wasm crate

7 of 9 core crates compile to wasm32-unknown-unknown (parser, compiler, vm, ir, memory, constraints, std). The wasm/ crate provides a browser-ready API for the planned playground (0.3.0).

New: Int and String type annotations

let count: Int = 42
let name: String = "hello"

VM-mode type annotations for documentation and future type checking. Joins the existing Field, Bool, Public, Witness annotations.

OuterScope unification

Functions defined before prove {} and inline circuit {} blocks are now accessible inside them — the same behavior that ach circuit files already had, now unified across all compilation paths.

fn double(x) { x * 2 }

prove(expected: Public) {
    assert_eq(double(val), expected)   // ✓ works now
}

New OuterScope struct replaces the ad-hoc preamble prepend hack in compile_circuit(). FnDecl ASTs are registered in the ProveIR compiler’s fn_table before block compilation, so outer functions are inlined identically to locally-defined ones.

ZK constraint optimization: 2,539 → 1,461 (-42.4%)

Three optimizations reduce the proof of membership (depth-3 Merkle) constraint count:

Conditional swap — The merkle_verify builtin now uses 2 Mux + 1 Poseidon per Merkle level (365 constraints) instead of 2 Poseidon + 1 Mux (724 constraints). This matches the standard pattern used by Tornado Cash and Semaphore.

Boolean enforcement dedup — The R1CS backend now tracks which variables have already had v * (1-v) = 0 enforced. When the same condition is used in multiple Mux/And/Or instructions, the check is emitted only once.

New: CSE (Common Sub-expression Elimination) pass

New IR optimization pass that identifies duplicate pure computations and remaps their results to the first occurrence. Covers all pure instructions: arithmetic, Poseidon, Mux, boolean ops, comparisons. Side-effecting instructions (AssertEq, Assert, RangeCheck) are never deduplicated. Handles chained substitutions.

The optimization pipeline is now: constant folding → bound inference → CSE → dead code elimination.

New: Proof of membership example

examples/proof_of_membership.ach — depth-3 Merkle tree with 8 members. Two members prove membership via Poseidon commitments and merkle_verify without revealing identity. 1,461 constraints per proof (Groth16, ~855 bytes).

Fix: BigInt.to_string() and BigInt.to_hex()

BigInt values now support string conversion:

let b = bigint256(42)
print(b.to_string())   // "42"
print(b.to_hex())      // "0x2a"

Test suite: 2,705 tests

2,543 unit/integration tests (cargo test —workspace) + 162 E2E tests (run_tests.sh). Up from 2,125 in beta.16.

PGO build script

./scripts/build-pgo.sh

Builds an optimized binary using profile-guided optimization. Collects profiles from the hot-loop benchmark and the VM test suite, then rebuilds with LLVM PGO. Integrated into CI (release.yml) for native release targets.

0.1.0-beta.16 — 2026-03-25

Hardening, circuit imports, assert messages, TOML inputs.

Hardening

• Panics → Result: Arena::alloc() returns Result, unreachable!() replaced with Err(InvalidOpcode), ~35 defensive unwrap conversions.
• Generic errors eliminated: RuntimeError::Unknown and SystemError replaced with specific variants (StaleHeapHandle, StaleUpvalue, IoError, etc.).
• Lexer robustness: from_utf8().unwrap() replaced with proper error propagation.
• Flat circuit format removed: Top-level public/witness declarations are a compile error. Use circuit name(param: Type, ...) { body }.
• Keyword argument validation: Typos in circuit calls produce “did you mean?” suggestions.

assert_eq / assert with custom messages

assert_eq(computed, expected, "commitment mismatch")
assert(is_valid, "eligibility check failed")

Optional third argument (string literal) shown when witness evaluation fails. Falls back to variable names + values when no message is provided.

Circuit imports in ProveIR

import "./hash_lib.ach" as h

circuit main(out: Public, a: Witness, b: Witness) {
    assert_eq(h.my_hash(a, b), out)
}

Circuits can now import functions from other modules. Imported functions are inlined during ProveIR compilation. Supports import ... as alias and selective imports. Circular import detection included.

--input-file for TOML circuit inputs

ach circuit merkle.ach --input-file inputs.toml

root = "7853200120375982..."
leaf = "1"
path = ["2", "3"]
indices = ["0", "1"]

Replaces the --inputs "path_0=2,path_1=3" convention with native TOML arrays. Supports string values, integers, hex ("0xFF"), and negative values. Mutually exclusive with --inputs.

Internal

• ModuleLoader moved from compiler to ir crate (shared between bytecode compiler and ProveIR).
• ProveIR format version bumped to v3 (assert message field in CircuitNode::AssertEq/Assert).
• WASM feasibility verified: 7/9 core crates compile to wasm32-unknown-unknown.

0.1.0-beta.15 — 2026-03-23

Syntax unification, global type metadata, Tornado Cash example.

Breaking: Unified syntax

Six inconsistent syntax patterns consolidated into one coherent design:

// Circuit definitions — params with visibility types
circuit eligibility(root: Public, secret: Witness, path: Witness Field[3]) {
    merkle_verify(root, poseidon(secret, 0), path, indices)
}

// Prove blocks — only public params, witnesses auto-captured
prove withdrawal(root: Public, nullifier_hash: Public) {
    merkle_verify(root, commitment, path, indices)
}

// Keyword arguments for all callables
eligibility(root: root_val, secret: my_secret, path: my_path)

• TypeAnnotation refactored from enum to struct with visibility, base, array_size fields.
• Public/Witness are contextual type keywords: root: Public, path: Witness Field[3].
• Call/CircuitCall unified — single Call node with Vec<CallArg> supports keyword args for all callables.
• CircuitParam, CircuitVisibility removed from AST.
• Old syntax removed — prove(public: [...]), circuit(public x, witness y) no longer parse.

circuit keyword — reusable circuit definitions

circuit eligibility(root: Public, secret: Witness, path: Witness Field[3], indices: Witness Field[3]) {
    let commitment = poseidon(secret, 0)
    merkle_verify(root, commitment, path, indices)
}

• ach circuit file.ach requires the circuit name(...) declaration format.
• import circuit "./path.ach" as name imports standalone circuit files.
• Circuit calls with keyword arguments: eligibility(root: val, secret: s).

Named prove blocks

prove vote(hash: Public) {
    assert_eq(poseidon(secret, 0), hash)
}

• prove name(...) at statement level desugars to let name = prove name(...)
• Proofs are first-class values (TAG_PROOF)

--circuit-stats — circuit constraint profiler

ach circuit merkle.ach --circuit-stats
ach run program.ach --circuit-stats

• 7 categories: Arithmetic, Assertions, Range checks, Hashes, Comparisons, Boolean ops, Selections
• ach run --circuit-stats collects stats across all prove blocks at runtime
• Static cost model matches actual R1CS constraint counts exactly

Global type metadata (GlobalEntry)

Global variables now carry type annotations through the compiler pipeline:

let path: Field[2] = [voter1, n1]   // type_ann preserved in GlobalEntry
prove(root: Public) {
    merkle_verify(root, leaf, path, idx)  // path correctly captured as array
}

• global_symbols upgraded from HashMap<String, u16> to HashMap<String, GlobalEntry> with index, type_ann, is_mutable fields.
• compile_prove reads GlobalEntry.type_ann to build enriched OuterScopeEntry for globals.
• find_array_size searches locals, upvalues, AND globals.
• Selective imports propagate type_ann from source module.

Prove block array captures

Array variables from VM scope are automatically captured by prove blocks:

let path = [voter1, n1]           // inferred as Field[2]
prove(merkle_root: Public) {
    merkle_verify(merkle_root, commitment, path, indices)
}

• Array type inference — let x = [a, b, c] infers Field[3] on immutable bindings.
• extract_array_ident capture tracking — merkle_verify and array-consuming constructs now correctly mark array element captures for instantiation.
• VM prove handler auto-expands TAG_LIST captures into scalar entries.

Type annotation warnings

let x: Bool = 0p42          // W006: type mismatch
let a: Field[3] = [1, 2]    // W007: array size mismatch

Examples

• tornado_mixer.ach — Full Tornado Cash–style private mixer: 4-user deposit tree, Merkle membership proofs, nullifier-based double-spend prevention, recipient binding. 3 Groth16 proofs generated end-to-end.
• credential_proof.ach — Updated to use real arrays instead of _N convention.
• prove_secret_vote.ach — Modernized to new prove(x: Public) syntax.

Editor

• TextMate grammar updated: Public/Witness as visibility modifiers, Field/Bool as types, circuit/prove named definitions, import circuit, ZK builtins separated.
• Grammar synced to docs site for Shiki highlighting.

Documentation

• 21 pages updated (EN + ES) to new syntax across tutorials, getting-started, circuits, and zk-concepts.

0.1.0-beta.14 — 2026-03-21

ProveIR pipeline complete (Phases A-H). Prove blocks are now compiled at compile time and serialized into bytecode, eliminating runtime re-parsing.

New syntax

• prove(public: [...]) — Prove block syntax with witness auto-inference (superseded by prove(name: Public) in beta.15).

let secret = 0p42
let hash = poseidon(secret, 0)

let p = prove(public: [hash]) {
    assert_eq(poseidon(secret, 0), hash)
}

ProveIR pipeline

• Phase A: ProveIR compiler — AST to pre-compiled circuit templates with SSA desugaring, function inlining, and method lowering.
• Phase B: Instantiation — unrolls loops, resolves captures, emits flat IR SSA. Includes MAX_INSTANTIATE_ITERATIONS (1M) and AssertEq consistency enforcement for captures used in both structure and constraints.
• Phase C: Serialization — bincode with ACHP magic header, version byte, 64 MB size limit, and post-deserialization validation.
• Phase D: ach circuit uses ProveIR instead of IrLowering (IrLowering fallback retained for circuits with imports).
• Phase E: compile_prove() compiles prove blocks to ProveIR at compile time and stores serialized bytes in the bytecode constant pool via TAG_BYTES.
• Phase F: VM handle_prove() reads ProveIR bytes from the constant pool, the handler deserializes and instantiates with captured scope values.
• Phase G: Parser supports prove(name: Public) syntax. Compiler synthesizes PublicDecl statements and validates no mixed syntax.
• Phase H: Documentation updated (18 pages, EN + ES).

Hardening

• ImportsNotSupported explicit error variant (replaces fragile string matching for IrLowering fallback detection).
• Capture reference validation in ProveIR::validate() — rejects ArraySize::Capture and ForRange::WithCapture referencing unknown capture names.
• Signed-range comparison contract documented on Instruction::IsLt / IsLe.
• Input validation in execute_prove_ir() — errors instead of silently skipping missing scope values.
• Upvalue scope fix — compile_prove() includes parent scope locals so prove blocks inside nested functions can reference upvalue-accessible variables.

Infrastructure

• TAG_BYTES = 14 — new value tag for binary blob constants (GC mark, sweep, recount integrated).
• BytesInterner — append-only compiler interner for serialized ProveIR.
• SER_TAG_BYTES — bytecode serializer/loader support for bytes constants in .achb files.
• Removed source: String from Expr::Prove AST and unused source parameter from Parser::new().

Examples

Three new examples in examples/:

• private_auction.ach — Sealed-bid auction with Poseidon commitments, range checks, and comparison gadgets.
• credential_proof.ach — Anonymous credential verification with Merkle membership and age threshold proofs.
• hash_chain_proof.ach — Iterated Poseidon hashing with functions inside prove blocks.

Editor

• TextMate grammar: prove-block rule for prove(name: Public) syntax highlighting.
• LSP: provep completion snippet, updated hover docs.

0.1.0-beta.13 — 2026-03-19

Method dispatch, static namespaces, namespace reorg.

Features

• Method dispatch (.method()) — 50 prototype methods across 8 types (Int, Field, String, List, Map, BigInt, Bool, Proof). Resolved at compile time via MethodCall opcode (161).
• Static namespaces (Type::MEMBER) — Int::MAX, Int::MIN, Field::ZERO, Field::ONE, Field::ORDER, BigInt::from_bits. Compiled to LoadConst or GetGlobal.
• Namespace reorg — Global function count reduced from 43 to 14 builtins + 2 std. Functions like abs, len, min, max, pow, to_string migrated to methods.

Documentation

• 83 documentation pages (EN + ES) on docs.achrony.me.
• Map methods reference, method migration guide, static namespace reference.

0.1.0-beta.12 — 2026-03-18

NativeModule trait, standard library, proc-macros.

Features

• NativeModule trait — Modular native function registration. Each stdlib group implements NativeModule.
• achronyme-std crate — 16 new native functions: type conversion, math utilities, extended strings, I/O (feature-gated).
• #[ach_native] / #[ach_module] proc-macros — Automatic NativeFn wrapper generation with arity checks and type-safe argument extraction.
• FromValue / IntoValue traits — Type-safe conversion between VM Value and Rust types.

0.1.0-beta.11 — 2026-03-16

Project manifest, ach init command.

Features

• achronyme.toml — Project configuration with walk-up directory search. Supports [project], [circuit], and [output] sections.
• ach init — Interactive project scaffolding.
• Config resolution — CLI flags > TOML > defaults.

0.1.0-beta.10 — 2026-03-16

Plonkish lookup fix, W003 warning.

Bug Fix

• Plonkish range_check and IsLtBounded now generate real KZG proofs. Migrated from meta.selector() to meta.fixed_column() + meta.lookup_any().

Features

• W003 warning — Warns when comparisons remain unbounded (~761 constraints) with range_check suggestion.

0.1.0-beta.9 — 2026-03-15

R1CS export fix, IsLtBounded optimization.

Security Fix

• R1CS export: write_lc() simplifies LinearCombinations before serialization (fixes snarkjs wtns check failures).

Features

• IsLtBounded optimization — bound_inference pass rewrites comparisons when operands have proven bitwidth. 761 constraints down to 66 for 64-bit comparisons.

Benchmark

0.1.0-beta.3 — 2026-03-04

Zero-panic hardening, architecture refactoring.

Security (16 fixes)

All .unwrap() and panic! paths replaced with Result propagation across compiler, VM, memory, and constraint backends.

Architecture (13 refactors)

Monolithic files split into focused submodules: vm.rs, field.rs, parser.rs, poseidon.rs, plonkish_backend.rs, lower.rs, eval.rs, Arena<T>.