Skip to content

fix(circuit): fill the failure guarantee with the real nullifier and modulus - #1658

Open
TomerStarkware wants to merge 1 commit into
mainfrom
tomer/circuit_failure_guarantee
Open

fix(circuit): fill the failure guarantee with the real nullifier and modulus#1658
TomerStarkware wants to merge 1 commit into
mainfrom
tomer/circuit_failure_guarantee

Conversation

@TomerStarkware

@TomerStarkware TomerStarkware commented Aug 25, 2026

Copy link
Copy Markdown
Collaborator

The bug

eval_circuit's failure branch and circuit_failure_guarantee_verify returned llvm::undef for the failure guarantee. The corelib walk that destructs it (u96_limbs_less_than_guarantee_verify) extracts the guarantee's limbs and branches on their comparison — so native branched on poison, while the VM branches on the real (nullifier, modulus) values its hint computes.

The walk stops at the first limb pair (most significant first) where the nullifier and modulus differ. In contracts (compiled with optimizations, so every arm carries a redeposit_gas), the stop position determines how much gas is refunded on the failure path. Native's poison walk folds to a fixed arm, so after any failing circuit_inverse — e.g. inverting 0, reachable by any modular-arithmetic contract with attacker-controlled input — its remaining gas diverges from the VM: 380 gas for the BLS12-381 modulus, 90 for secp256k1. Around the gas-exhaustion boundary this escalates to a hard divergence: the VM completes the transaction where native reverts with out-of-gas. Branching on poison is also UB regardless of the observed symptom.

The fix

CircuitFailureGuarantee was a ZST in native (the VM's guarantee holds pointers into the builtin segments, which native doesn't have), so it couldn't carry anything. It's now a real value holding the nullifier and modulus limbs:

  • build_gate_evaluation forwards the failing inverse gate's gcd (already computed by the egcd runtime call) to the error block.
  • eval_circuit's error branch materializes nullifier = modulus / gcd(input, modulus) — exactly the value the VM's hint computes (0 < nullifier < modulus, input · nullifier ≡ 0 (mod modulus)) — and stores {nullifier, modulus} in the guarantee.
  • circuit_failure_guarantee_verify unpacks the carried limbs into its U96LimbsLtGuarantee<4> output instead of returning undef.

No verification is performed — the values exist solely because the destruct walk's branches consume them.

The test

test_data/programs/circuit_failure_guarantee.cairo destructs the guarantee manually (the corelib-private walk API is importable in single-file programs) and returns the walk length as a first-class value, compared VM-vs-native. Two moduli with different expected lengths (secp256k1 → 2, [7,0,0,0] → 4) ensure any walk not steered by the actual limb values fails at least one case. Verified to fail with a return-value mismatch when the fix is reverted.

Note the existing test_circuit_fail couldn't catch this: its [0,0,0,0] modulus panics at try_into().unwrap() before ever reaching the guarantee path, and the precompiled test programs are built with Optimizations::Disabled, which emits no redeposit_gas, making remaining gas path-independent.

🤖 Generated with Claude Code


This change is Reviewable

…modulus

`eval_circuit`'s failure branch and `circuit_failure_guarantee_verify`
returned `llvm::undef` for the failure guarantee, so the corelib walk that
destructs it (`u96_limbs_less_than_guarantee_verify`) branched on poison
instead of on the guarantee's limbs. The walk's stop position determines how
much gas is redeposited on the failure path of contracts (compiled with
optimizations, each arm carries a `redeposit_gas`), so native's remaining gas
diverged from the VM after any failing `circuit_inverse` (e.g. inverting 0):
380 gas for the BLS12-381 modulus, 90 for secp256k1, and around the
exhaustion boundary the VM succeeds where native runs out of gas.

`CircuitFailureGuarantee` is now a real value carrying the nullifier and
modulus limbs: the failing inverse gate's gcd is forwarded to the error
block, which materializes `nullifier = modulus / gcd(input, modulus)` -
exactly the value the VM's hint computes - and
`circuit_failure_guarantee_verify` unpacks it into the
`U96LimbsLtGuarantee<4>` output.

The regression test destructs the guarantee manually (the corelib-private
walk API is importable in single-file programs) and returns the walk length
as a value, comparing it against the VM; two moduli with different expected
lengths catch any walk not steered by the actual limb values.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
@github-actions

Copy link
Copy Markdown

Benchmarking results

Benchmark for program dict_insert

Open benchmarks
Command Mean [s] Min [s] Max [s] Relative
Cairo-vm (Rust, Cairo 1) 10.505 ± 0.042 10.422 10.552 5.68 ± 0.04
cairo-native (embedded AOT) 1.850 ± 0.011 1.837 1.871 1.00
cairo-native (embedded JIT using LLVM's ORC Engine) 1.875 ± 0.012 1.857 1.891 1.01 ± 0.01

Benchmark for program dict_snapshot

Open benchmarks
Command Mean [ms] Min [ms] Max [ms] Relative
Cairo-vm (Rust, Cairo 1) 540.8 ± 8.2 530.6 557.3 1.00
cairo-native (embedded AOT) 1687.7 ± 10.6 1671.0 1708.2 3.12 ± 0.05
cairo-native (embedded JIT using LLVM's ORC Engine) 1712.0 ± 14.2 1695.1 1740.4 3.17 ± 0.05

Benchmark for program factorial_2M

Open benchmarks
Command Mean [s] Min [s] Max [s] Relative
Cairo-vm (Rust, Cairo 1) 4.692 ± 0.015 4.671 4.708 2.69 ± 0.04
cairo-native (embedded AOT) 1.746 ± 0.026 1.715 1.795 1.00
cairo-native (embedded JIT using LLVM's ORC Engine) 1.767 ± 0.020 1.741 1.804 1.01 ± 0.02

Benchmark for program fib_2M

Open benchmarks
Command Mean [s] Min [s] Max [s] Relative
Cairo-vm (Rust, Cairo 1) 4.620 ± 0.018 4.578 4.640 2.77 ± 0.04
cairo-native (embedded AOT) 1.669 ± 0.021 1.637 1.703 1.00
cairo-native (embedded JIT using LLVM's ORC Engine) 1.742 ± 0.012 1.722 1.759 1.04 ± 0.01

Benchmark for program linear_search

Open benchmarks
Command Mean [ms] Min [ms] Max [ms] Relative
Cairo-vm (Rust, Cairo 1) 586.6 ± 6.7 576.7 598.7 1.00
cairo-native (embedded AOT) 1710.9 ± 19.6 1687.3 1750.0 2.92 ± 0.05
cairo-native (embedded JIT using LLVM's ORC Engine) 1735.2 ± 13.5 1712.0 1755.0 2.96 ± 0.04

Benchmark for program logistic_map

Open benchmarks
Command Mean [ms] Min [ms] Max [ms] Relative
Cairo-vm (Rust, Cairo 1) 498.0 ± 9.4 489.5 521.6 1.00
cairo-native (embedded AOT) 1683.4 ± 13.5 1666.5 1707.4 3.38 ± 0.07
cairo-native (embedded JIT using LLVM's ORC Engine) 1701.8 ± 7.7 1690.7 1710.9 3.42 ± 0.07

@github-actions

Copy link
Copy Markdown

Benchmark results Main vs HEAD.

Base

Command Mean [s] Min [s] Max [s] Relative
base dict_insert.cairo (JIT) 1.851 ± 0.013 1.828 1.873 1.01 ± 0.01
base dict_insert.cairo (AOT) 1.829 ± 0.010 1.814 1.843 1.00

Head

Command Mean [s] Min [s] Max [s] Relative
head dict_insert.cairo (JIT) 1.920 ± 0.026 1.882 1.968 1.00
head dict_insert.cairo (AOT) 1.933 ± 0.023 1.886 1.966 1.01 ± 0.02

Base

Command Mean [s] Min [s] Max [s] Relative
base dict_snapshot.cairo (JIT) 1.662 ± 0.011 1.649 1.683 1.02 ± 0.01
base dict_snapshot.cairo (AOT) 1.637 ± 0.016 1.610 1.666 1.00

Head

Command Mean [s] Min [s] Max [s] Relative
head dict_snapshot.cairo (JIT) 1.709 ± 0.039 1.680 1.813 1.00
head dict_snapshot.cairo (AOT) 1.715 ± 0.024 1.682 1.748 1.00 ± 0.03

Base

Command Mean [s] Min [s] Max [s] Relative
base factorial_2M.cairo (JIT) 1.728 ± 0.011 1.708 1.749 1.01 ± 0.01
base factorial_2M.cairo (AOT) 1.704 ± 0.010 1.692 1.720 1.00

Head

Command Mean [s] Min [s] Max [s] Relative
head factorial_2M.cairo (JIT) 1.802 ± 0.016 1.776 1.820 1.02 ± 0.02
head factorial_2M.cairo (AOT) 1.767 ± 0.023 1.720 1.804 1.00

Base

Command Mean [s] Min [s] Max [s] Relative
base fib_2M.cairo (JIT) 1.692 ± 0.026 1.665 1.739 1.02 ± 0.02
base fib_2M.cairo (AOT) 1.652 ± 0.025 1.612 1.687 1.00

Head

Command Mean [s] Min [s] Max [s] Relative
head fib_2M.cairo (JIT) 1.732 ± 0.013 1.710 1.751 1.01 ± 0.01
head fib_2M.cairo (AOT) 1.710 ± 0.021 1.678 1.743 1.00

Base

Command Mean [s] Min [s] Max [s] Relative
base linear_search.cairo (JIT) 1.699 ± 0.012 1.680 1.714 1.00
base linear_search.cairo (AOT) 1.701 ± 0.012 1.681 1.720 1.00 ± 0.01

Head

Command Mean [s] Min [s] Max [s] Relative
head linear_search.cairo (JIT) 1.752 ± 0.037 1.707 1.825 1.01 ± 0.03
head linear_search.cairo (AOT) 1.736 ± 0.023 1.706 1.773 1.00

Base

Command Mean [s] Min [s] Max [s] Relative
base logistic_map.cairo (JIT) 1.690 ± 0.030 1.648 1.750 1.00
base logistic_map.cairo (AOT) 1.696 ± 0.041 1.658 1.784 1.00 ± 0.03

Head

Command Mean [s] Min [s] Max [s] Relative
head logistic_map.cairo (JIT) 1.732 ± 0.022 1.702 1.772 1.02 ± 0.02
head logistic_map.cairo (AOT) 1.706 ± 0.015 1.692 1.734 1.00

@orizi orizi left a comment

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

@orizi reviewed all commit messages and made 2 comments.
Reviewable status: 0 of 4 files reviewed, 2 unresolved discussions (waiting on TomerStarkware).


src/types/circuit.rs line 69 at r1 (raw file):

            Ok(IntegerType::new(context, 64).into())
        }
        // The VM's failure guarantee holds pointers into the builtin segments. There

overdoc


tests/tests/circuit.rs line 329 at r1 (raw file):

}

/// Checks that on a failing circuit evaluation, native fills the failure

overdoc

@orizi orizi left a comment

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

@orizi made 1 comment.
Reviewable status: 0 of 4 files reviewed, 3 unresolved discussions (waiting on TomerStarkware).


src/libfuncs/circuit.rs line 427 at r1 (raw file):

        ))?;

        // The failure guarantee carries the nullifier and modulus limbs that

overdoc

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants