Fix air soundness gaps by aszepieniec · Pull Request #438 · TritonVM/triton-vm

aszepieniec · 2026-06-15T11:59:15Z

No description provided.

Regression test for a soundness gap in the Hash Table: on a transition into a padding row (mode `Pad`, round number 0, instruction `hash`) the cascade client log-derivative update constraint vanishes identically, so a malicious prover can set the S-box lookup terminal to any value. This test fails on the unfixed constraints and passes once the gap is closed. Test authored by huuhait; gap independently confirmed during audit. Co-authored-by: huuhait <huuhadz2k@gmail.com> Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

The cascade client log-derivative update constraint guards its "remains" branches with deselectors keyed to active-execution values (`round_number == NUM_ROUNDS`, `ci == sponge_init`) while gating the "update" branch on `mode != Pad`. On a padding row — forced by the consistency constraints to `(Mode=Pad, RoundNumber=0, CI=hash)` — all three guards vanish, so the constraint becomes `0 = 0` and the prover can drive the S-box lookup terminal to any value. Add an explicit `next_row_is_padding_row * cascade_log_derivative_remains` term so the log-derivative is pinned on every padding transition. Regenerates the constraint-system fingerprint, the proof-hash snapshots, and the arithmetization overview. The proof-format version bump is left for a separate, coordinated commit at integration. Co-authored-by: huuhait <huuhadz2k@gmail.com> Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

Regression test for a soundness gap in the RAM Table: on a transition into a padding row where the prover decreases the RAM pointer across the boundary, the clock-jump-difference lookup log-derivative update constraint vanishes identically, freeing the lookup terminal. This test fails on the unfixed constraints and passes once the gap is closed. Test authored by huuhait; gap independently confirmed during audit. Co-authored-by: huuhait <huuhadz2k@gmail.com> Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

The clock-jump-difference lookup log-derivative update constraint guards its "remains" branch with `ram_pointer_difference` and gates accumulation on `next_row_is_padding_row` (= `instruction_type - PADDING`). Entering a padding row the prover may decrease the RAM pointer by two, which zeroes the constraint identically: the accumulate guard vanishes (next row is padding), and the remains guard `ram_pointer_difference + it(it-1)` becomes `-2 + 2 = 0`. The lookup terminal is then free, breaking the memory-consistency timestamp argument. Unlike the Op Stack Table, RAM pointers may jump by arbitrary amounts, so nothing else forbids the jump. Multiply the "ram pointer doesn't change" remains term by `next_row_is_padding_row` so that, on padding rows, the log-derivative is pinned unconditionally by the `next_row_is_not_padding_row` term regardless of the pointer value. Regenerates the constraint-system fingerprint, the proof-hash snapshots, and the arithmetization overview. The proof-format version bump is left for a separate, coordinated commit at integration. Co-authored-by: huuhait <huuhadz2k@gmail.com> Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

Regression test for a soundness gap in the Hash Table: after a `sponge_init` row the round number may leave its legal range `0..=NUM_ROUNDS`, because the increment constraint is disabled there and the wrap-at-`NUM_ROUNDS` constraint is vacuous (the `sponge_init` row has round number 0). At an out-of-range round number the round-number-gated hash-digest evaluation argument collapses. This test fails on the unfixed constraints and passes once the reset is enforced. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

After a `sponge_init` row the round number is unconstrained: the mode-gated increment constraint excludes `sponge_init`, and the wrap-at-`NUM_ROUNDS` constraint is vacuous because the row's round number is 0. A prover can therefore set the next round number outside the legal range `0..=NUM_ROUNDS`, at which point the round-number-gated evaluation arguments (notably `HashDigestRunningEvaluation`) collapse. Add `if_ci_is_sponge_init_then_round_number_next_is_0` to enforce the reset explicitly, pinning the round number into its legal range across `sponge_init` rows. Regenerates the constraint-system fingerprint, the proof-hash snapshots, and the arithmetization overview. The proof-format version bump is a separate commit. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

The cascade, RAM clock-jump-difference, and round-number soundness fixes change the AIR, so proofs produced by the previous version no longer verify. Bump `CURRENT_VERSION` 3 -> 4 to make the incompatibility explicit, and regenerate the version-dependent proof-hash snapshots. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

jan-ferdinand

Looks perfect. 👌

`HashInputRunningEvaluation` may only be updated at its absorb point `(mode = Hash, round_number = 0)`; elsewhere it must remain unchanged. Its transition constraint guards the "remains" branch with `round_number_next + (mode_next - Hash)`, whose summands have opposite sign over the legal domain and cancel at the reachable interior rows `(ProgramHashing, rn = 2)` and `(Sponge, rn = 1)` (both satisfy `rn + mode = 3`). There the constraint vanishes regardless of the column, so a prover can shift the running evaluation by an arbitrary amount that flows to the cross-table terminal, breaking the Processor <-> Hash hash-input binding. This test asserts the column is pinned off its update point; it fails on the current constraints and passes once the guard is corrected. Discovered by huuhait. Co-authored-by: huuhait <huuhadz2k@gmail.com> Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

The "remains" branch of `running_evaluation_hash_input_is_updated_correctly` was guarded by `round_number_next + (mode_next - Hash)`. The two summands have opposite sign over the legal domain (`round_number_next` ≥ 0, zero only at rn' = 0; `mode_next - Hash` ≤ 0, zero only at mode' = Hash), so their sum cancels on the anti-diagonal `rn' + mode' = 3`, which contains the reachable interior rows (ProgramHashing, rn' = 2) and (Sponge, rn' = 1). At those rows the whole constraint vanished regardless of `HashInputRunningEvaluation`, letting a prover shift it by an arbitrary amount that propagates to the cross-table terminal and breaks the Processor <-> Hash hash-input binding. Replace the mode guard with `Hash - mode_next` so both "remains" guards are ≥ 0 and their sum is zero only at the update point (rn' = 0, mode' = Hash) — the same same-sign structure that already makes the hash digest constraint sound. The regression test added in the previous commit now passes. Proof format stays at version 4 (this completes the unreleased soundness batch); regenerates the constraint fingerprint, proof-hash snapshots, and arithmetization overview. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

A parametric regression harness that, for every accumulator aux column in every table, perturbs only that column's next-row cell across a set of adversarial 2-row windows and asserts some transition constraint rejects the change. A window is first checked for reachability (rejected if a main-column-only constraint already forbids it) so that genuine gaps are distinguished from spurious ones — e.g. the real RAM pointer-delta -2 gap versus an Op Stack delta -2 that the stack-pointer constraint forbids. Windows cover into-padding, padding-to-padding, and — crucially — the interior `(mode, round-number)` transitions within a permutation, which is what exposes additive-cancellation gaps like the hash-input one fixed in the preceding commits. Reverting any of the cascade, RAM clock-jump, or hash-input fixes makes the harness fail and name the freed column. Scope is documented in the module: it probes transition constraints on the enumerated windows, so a clean run means "no gap found on covered windows," not a proof of pinning. The Processor table (per-instruction deselector guards rather than a single padding indicator) is only smoke-covered. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

`InstructionType` has no consistency constraint confining it to its legal set {WRITE=0, READ=1, PADDING=2}; it is confined only indirectly via the permutation argument. But the perm-arg coefficient of `RunningProductPermArg_next` is `type_next^2 - 2`, which is zero at `type_next = sqrt(2)` (sqrt(2) exists in the field since the prime is 1 mod 8). A row carrying that out-of-set type at the real->padding boundary frees the perm-arg terminal, letting a prover forge the RAM <-> Processor memory permutation. This test asserts out-of-set instruction types are rejected; it fails on the current constraints and passes once the type is locally confined. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

Add a consistency constraint `InstructionType·(InstructionType−1)· (InstructionType−2) = 0` pinning the column to {WRITE=0, READ=1, PADDING=2} on every row. Previously the column was confined only indirectly by the permutation argument, whose coefficient of `RunningProductPermArg_next` is `type_next² − 2`. That coefficient vanishes at the out-of-set value `type_next = √2` (which exists since the prime is 1 mod 8), so a row carrying √2 at the real→padding boundary left the perm-arg terminal free, letting a prover forge the RAM <-> Processor memory permutation. Pinning the type locally makes every legal value give a nonzero coefficient (−2, −1, 2) and removes the out-of-set value entirely. The regression test from the previous commit now passes. Proof format stays at version 4 (unreleased soundness batch); regenerates the constraint fingerprint, proof-hash snapshots, and arithmetization overview. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

`IB1ShrinkStack` has no consistency constraint confining it to its legal set {0, 1, PADDING=2}; it is confined only indirectly via the permutation argument, whose coefficient of `RunningProductPermArg_next` is `ib1_next^2 - 2`. That coefficient vanishes at `ib1_next = sqrt(2)` (sqrt(2) exists since the field prime is 1 mod 8), so a row carrying that out-of-set value at the real->padding boundary frees the perm-arg terminal, letting a prover forge the OpStack <-> Processor permutation. This test asserts out-of-set values are rejected; it fails on the current constraints and passes once the column is locally confined. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

Add a consistency constraint `IB1ShrinkStack·(IB1ShrinkStack−1)· (IB1ShrinkStack−2) = 0` pinning the column to {0, 1, PADDING=2} on every row. Previously the column was confined only indirectly by the permutation argument, whose coefficient of `RunningProductPermArg_next` is `ib1_next² − 2`. That coefficient vanishes at the out-of-set value `ib1_next = √2` (which exists since the prime is 1 mod 8), so a row carrying √2 at the real→padding boundary left the perm-arg terminal free, letting a prover forge the OpStack <-> Processor permutation. Pinning the value locally makes every legal value give a nonzero coefficient and removes the out-of-set value entirely. The regression test from the previous commit now passes. Proof format stays at version 4 (unreleased soundness batch); regenerates the constraint fingerprint, proof-hash snapshots, and arithmetization overview. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

The harness previously probed selector/type columns only over their legal values, so it missed gaps exposed by out-of-domain values — notably the RAM/OpStack `RunningProductPermArg` freedom at `type_next = ±√2`, where the perm-arg coefficient `type_next² − 2` vanishes. Two changes: - Reachability now honours consistency constraints as well as transition constraints. Consistency constraints are single-row and checked against each row of the window; an out-of-domain selector value is unreachable precisely because a (main-only) consistency constraint rejects it. This lets the harness drop the √2 windows once the range constraints are present, and flag them once removed — without false positives. - Add `±√2` out-of-set windows for RAM `InstructionType` and OpStack `IB1ShrinkStack`. Sweeping the roots of a guard coefficient is the general lesson: an out-of-set value that is not such a root (e.g. 3) keeps the coefficient nonzero and would not expose the gap. Validated: green on the fixed tree; disabling either range constraint makes the harness flag that table's RunningProductPermArg at the ±√2 windows. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

jan-ferdinand

While I'm a big fan of regression tests, I'm not sure (a) the many, highly specific, rather verbose tests are what we want in this codebase, and (b) they should be included in the branch called critical_fixes.

How about we include the fixes here and do the tests properly on the main branch?

jan-ferdinand · 2026-06-16T07:40:39Z

I don't currently agree with the inclusion of accumulator_pinning.rs. Several stylistic issues aside (see below), the tests included therein feel like they help the process of identifying gaps in the AIR, but they also seem to be something of a clutch. The knowledge required to set up and test for any given suspected gap in the AIR strikes me as highly specific, preventing this approach from becoming more general. I currently think we're better of to use the results produced by these tests, but to not include the tests and write something more general instead.

Stylistic issues

Code & comments break with the style established in the rest of the codebase. To name a few:

Functions like generic_challenges are duplicated code. (In this specific case, use Challenges::default instead.) Other places construct challenges themselves, calling neither of the now multiple available functions.

Comments introduce new terminology without explaining it, like “guard column” or “off-domain value”.

There is dead code (even marked #[allow(dead_code)]).

cargo fmt produces a non-empty diff.

Several comments describe old behavior or talk about specific changes, for example “<-- the fix”.

jan-ferdinand · 2026-06-16T08:01:30Z

        let running_evaluation_hash_input_updates = running_evaluation_hash_input_next
            - hash_input_eval_indeterminate * running_evaluation_hash_input
            - compressed_row_from_processor;
        let running_evaluation_hash_input_is_updated_correctly =
            Self::round_number_deselector(circuit_builder, &round_number_next, 0)
                * Self::mode_deselector(circuit_builder, &mode_next, HashTableMode::Hash)
                * running_evaluation_hash_input_updates
                + round_number_next.clone() * running_evaluation_hash_input_remains.clone()
-                + Self::select_mode(circuit_builder, &mode_next, HashTableMode::Hash)
+                // The "remains" guard is the sum of this term's coefficient and
+                // the `round_number_next` coefficient above; it must vanish only
+                // at the update point (round_number_next = 0, mode_next = Hash).
+                // `round_number_next` is ≥ 0 over the legal range and zero only
+                // at rn' = 0, so the mode guard must also be ≥ 0 and zero only at
+                // mode' = Hash. Using `mode_next - Hash` (≤ 0) instead gives the
+                // two guards opposite signs, so their sum cancels at the reachable
+                // interior rows where rn' + mode' = 3 — (ProgramHashing, rn' = 2)
+                // and (Sponge, rn' = 1) — leaving the running evaluation free.
+                // Hence `Hash - mode_next`, mirroring the digest constraint's
+                // same-sign guards `(rn' - NUM_ROUNDS) + (mode' - Hash)`.
+                + (circuit_builder.b_constant(HashTableMode::Hash) - mode_next.clone())
                    * running_evaluation_hash_input_remains;


A comment in the middle of an expression (a) is odd and (b) prevents cargo fmt from doing its job.
Given that we're using both Self::round_number_deselector and Self::mode_deselector, I don't even think a comment regarding the Self::select_mode introduced in this PR is necessary.

Suggested change

* running_evaluation_hash_input_remains;

let running_evaluation_hash_input_is_updated_correctly =

Self::round_number_deselector(circuit_builder, &round_number_next, 0)

* Self::mode_deselector(circuit_builder, &mode_next, HashTableMode::Hash)

* running_evaluation_hash_input_updates

+ round_number_next.clone() * running_evaluation_hash_input_remains.clone()

+ Self::select_mode(circuit_builder, &mode_next, HashTableMode::Hash)

* running_evaluation_hash_input_remains;

jan-ferdinand · 2026-06-16T08:31:10Z

+        // Confine `IB1ShrinkStack` to its legal set {0, 1, PADDING=2} on every
+        // row. Without this, the column is constrained only indirectly through
+        // the permutation argument, whose coefficient of
+        // `RunningProductPermArg_next` is `ib1_next² − 2`; that coefficient
+        // vanishes at the out-of-set value `ib1_next = √2` (which exists since
+        // the prime is 1 mod 8), freeing the perm-arg terminal at the
+        // real→padding boundary.


Suggested change

// Confine `IB1ShrinkStack` to its legal set {0, 1, PADDING=2} on every

// row. Without this, the column is constrained only indirectly through

// the permutation argument, whose coefficient of

// `RunningProductPermArg_next` is `ib1_next² − 2`; that coefficient

// vanishes at the out-of-set value `ib1_next = √2` (which exists since

// the prime is 1 mod 8), freeing the perm-arg terminal at the

// real→padding boundary.

jan-ferdinand · 2026-06-16T08:33:02Z

+        // Confine `InstructionType` to its legal set {WRITE=0, READ=1,
+        // PADDING=2} on every row. Without this, the column is constrained only
+        // indirectly through the permutation argument, whose coefficient of
+        // `RunningProductPermArg_next` is `type_next² − 2`; that coefficient
+        // vanishes at the out-of-set value `type_next = √2` (which exists since
+        // the prime is 1 mod 8), freeing the perm-arg terminal at the
+        // real→padding boundary.


Suggested change

// Confine `InstructionType` to its legal set {WRITE=0, READ=1,

// PADDING=2} on every row. Without this, the column is constrained only

// indirectly through the permutation argument, whose coefficient of

// `RunningProductPermArg_next` is `type_next² − 2`; that coefficient

// vanishes at the out-of-set value `type_next = √2` (which exists since

// the prime is 1 mod 8), freeing the perm-arg terminal at the

// real→padding boundary.

jan-ferdinand · 2026-06-16T08:34:12Z

+        // the prime is 1 mod 8), freeing the perm-arg terminal at the
+        // real→padding boundary.
+        let instruction_type = main_row(Self::MainColumn::InstructionType);
+        let instruction_type_is_legal = instruction_type.clone()


Suggested change

let instruction_type_is_legal = instruction_type.clone()

let instruction_type_is_legal = (instruction_type.clone()

- constant(INSTRUCTION_TYPE_WRITE))

aszepieniec and others added 7 commits June 15, 2026 12:45

jan-ferdinand self-requested a review June 15, 2026 12:21

jan-ferdinand approved these changes Jun 15, 2026

View reviewed changes

aszepieniec and others added 4 commits June 15, 2026 15:00

aszepieniec marked this pull request as draft June 15, 2026 13:35

aszepieniec and others added 4 commits June 15, 2026 15:39

aszepieniec marked this pull request as ready for review June 15, 2026 14:25

aszepieniec requested a review from jan-ferdinand June 15, 2026 14:57

jan-ferdinand reviewed Jun 16, 2026

View reviewed changes

Navigation Menu

Uh oh!

Fix air soundness gaps - #438

Fix air soundness gaps#438
aszepieniec wants to merge 15 commits into
critical_fixesfrom
asz/fix-air-soundness-gaps

aszepieniec commented Jun 15, 2026

Uh oh!

jan-ferdinand left a comment

Uh oh!

jan-ferdinand left a comment

Uh oh!

jan-ferdinand Jun 16, 2026

Uh oh!

jan-ferdinand Jun 16, 2026

Uh oh!

jan-ferdinand Jun 16, 2026

Uh oh!

jan-ferdinand Jun 16, 2026

Uh oh!

jan-ferdinand Jun 16, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

	let instruction_type_is_legal = instruction_type.clone()
	let instruction_type_is_legal = (instruction_type.clone()
	- constant(INSTRUCTION_TYPE_WRITE))

Uh oh!

Conversation

aszepieniec commented Jun 15, 2026

Uh oh!

jan-ferdinand left a comment

Choose a reason for hiding this comment

Uh oh!

jan-ferdinand left a comment

Choose a reason for hiding this comment

Uh oh!

jan-ferdinand Jun 16, 2026

Choose a reason for hiding this comment

Stylistic issues

Uh oh!

jan-ferdinand Jun 16, 2026

Choose a reason for hiding this comment

Uh oh!

jan-ferdinand Jun 16, 2026

Choose a reason for hiding this comment

Uh oh!

jan-ferdinand Jun 16, 2026

Choose a reason for hiding this comment

Uh oh!

jan-ferdinand Jun 16, 2026

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants