Skip to content

fix(aiur): correct lookup constraints and strengthen proof validation - #634

Merged
arthurpaulino merged 8 commits into
mainfrom
ap/fixes
Sep 15, 2026
Merged

fix(aiur): correct lookup constraints and strengthen proof validation#634
arthurpaulino merged 8 commits into
mainfrom
ap/fixes

Conversation

@arthurpaulino

@arthurpaulino arthurpaulino commented Sep 15, 2026

Copy link
Copy Markdown
Member

Aiur could accept false public results through inactive provider rows, incorrectly combined lookup messages, and ambiguous function-message boundaries. The lookup-gating bug also prevented an honest execution from verifying. This PR fixes those failures, rejects Merkle-cap configurations that fail to bind every trace matrix, and adds explicit structural validation at the Aiur boundary.

The changes distill the first and third commits of #631 into seven atomic commits. Call-rank machinery, cyclic-trace defenses, and performance improvements from that PR are excluded. Cyclic call traces remain outside this PR's scope.

The fixes distinguish soundness (rejecting proofs of false claims) from completeness (allowing honest executions to prove and verify):

Commit Change Classification and evidence
2897d6b5 Require function and memory provider multiplicities to vanish on inactive rows, including grouped function circuits. Soundness. A supplied-trace regression previously proved 3 * 5 = 16. Additional constraint tests cover inactive memory rows and every grouped member.
9d5d0fe9 Correct lookup argument gating and grouping for circuits with empty branches. Soundness and completeness. An inactive branch's store could redirect a live function call into memory and establish a false result; an honest execution also failed verification. Both regressions are reproduced and fixed.
c852ccce Validate constrained-call arities, continuation yields, and public claim channel, visibility, and arity. Soundness. Lookup zero-padding allowed an empty return to establish a public claim containing an extra zero output. The regression uses the existing claim encoding without rank fields.
15be618e Validate control counts, circuit members, and selector capacity before synthesis. Construction validation. The malformed fixture already failed downstream; this makes structural bounds explicit and rejects it earlier. No new soundness or completeness failure is demonstrated.
e6046b4e Require fixed preprocessed circuits to be active at their exact heights. Soundness hardening. Tests establish early rejection of omitted byte tables and incorrect heights. These malformed proofs already failed downstream.
58a6ce66 Bound total lookup consumers below the field characteristic, with checked arithmetic and metadata alignment. Soundness hardening. Makes the lookup-count assumption explicit. Tests cover field and machine bounds; they do not demonstrate a previously accepted false claim.
e9048e89 Reject caps that omit shorter trace matrices. Soundness. Native MMCS tests demonstrate identical commitments for different short matrices and acceptance of altered single and multi-openings. Aiur rejects the unsafe cap/trace combinations and accepts the safe boundary.

The adversarial regressions use the existing Rust Aiur test infrastructure and supplied trace rows, independently of honest witness generation. The Merkle-cap guard is also checked against direct injection geometry across 288,225 boundary cases. Honest proofs using unsafe cap configurations are intentionally rejected; the normal root-cap setting remains supported.

The lookup-gating fix has a conservative proving-cost tradeoff: only a single-selector, single-function circuit with terminal control retains raw lookup arguments and grouped accumulators. Some safe functions containing matches therefore lose that optimization. Execution counts and main trace widths are unchanged, but stage-2 width and potentially quotient degree increase. Measured FFT estimates rise by 0.22% for Nat.add_comm and 0.38% for the shard pipeline. The corresponding exact pins are updated in the gating commit. These are FFT-model changes, not measured wall-clock slowdowns; a more precise lookup-writer analysis is deferred.

Validation passed:

  • All 35 Rust Aiur tests: cargo test --locked --release -p aiur --features parallel.
  • Strict workspace Clippy with CI features: cargo clippy --locked --release --workspace --all-targets --features ix-ffi/parallel,ix-ffi/net,ix-ffi/test-ffi -- -D warnings.
  • Formatting: cargo fmt --all -- --check.
  • Codegen parity: lake exe ix codegen --check; all three generated programs are unchanged.
  • Lean suites: lake test --wfail -- aiur-cross aiur-cost aiur-prove aiur-hashes rbtree-map multi-stark recursive-verifier ix-aggr.
  • Full IxVM suite, including generated-code parity and updated FFT pins: lake test --wfail -- --ignored ixvm.

arthurpaulino and others added 7 commits September 15, 2026 14:51
@arthurpaulino @johnchandlerburnham
fix(aiur): constrain inactive provider multiplicities
2897d6b 
Require function and memory provider multiplicities to vanish on inactive
rows, including each member of a grouped circuit. Preserve lookup widths
and linear multiplicities.

Port the activity repair from PR #631's first commit without its call ranks.
The supplied-trace regression accepted 3 * 5 = 16 before the fix; it now
rejects. All four acceptance tests pass in the release parallel test suite.

Co-authored-by: John C. Burnham <john@agathic.com>
@arthurpaulino @johnchandlerburnham
fix(aiur): gate lookups in circuits with empty branches
9d5d0fe 
Only omit argument gates for a single function with terminal control and
one selector. An empty branch still emits operation lookups even though
it allocates no terminal selector. Use the same condition for lookup
grouping so the gated expressions fit the quotient degree.

Port this independent repair from PR #631 without call-order columns.
Before the fix, an inactive store redirected a live call into memory and
proved a false result; honest execution also failed proof verification.
Both regressions now pass. Strict release parallel Clippy passes.

Co-authored-by: John C. Burnham <john@agathic.com>
@arthurpaulino @johnchandlerburnham
fix(aiur): validate function lookup message boundaries
c852ccc 
Validate constrained call input/output arities and continuation yields at
construction. Check the public claim channel, entry visibility, and exact
input/output shape before proof verification. Preserve the claim encoding.

Adapt PR #631's message-shape checks without its rank field. A supplied
trace for an empty return previously verified a claim returning zero due
to lookup zero-padding; the new regression rejects it. A mismatched call
with sufficient allocated columns is now rejected at construction too.
All five shape regressions and strict release parallel Clippy pass.

Co-authored-by: John C. Burnham <john@agathic.com>
@arthurpaulino @johnchandlerburnham
fix(aiur): validate circuit control counts before synthesis
15be618 
Check circuit member indices, bounded control counts, and selector capacity
before constructing constraints. Count continuation-consumed yields and
empty matches correctly. This ports PR #631's structural guard without
changing compiler layouts or adding call-order constraints.

Tests cover malformed selector counts, continuation accounting, machine
overflow and field bounds. The missing-selector fixture now fails at the
Aiur validation boundary rather than downstream column compilation.
All three count tests and strict release parallel Clippy pass.

Co-authored-by: John C. Burnham <john@agathic.com>
@arthurpaulino @johnchandlerburnham
fix(aiur): validate fixed trace activity and heights
e6046b4 
Require every fixed preprocessed circuit to be active at its exact height
before entering PCS verification. Align proof degrees by active position
and reject malformed metadata without shifting by unchecked amounts.

Port PR #631's fixed-table guard without rank lookups. The tests distinguish
early InvalidProofShape rejection from later opening failures, cover absent
byte tables and incorrect heights, and preserve honest verification.
All three fixed-table tests and strict release parallel Clippy pass.

Co-authored-by: John C. Burnham <john@agathic.com>
@arthurpaulino @johnchandlerburnham
fix(aiur): bound global lookup consumers before verification
58a6ce6 
Bound one public claim plus every lookup slot in every active trace row
below the Goldilocks characteristic. Count slots in canonical circuit
order and degrees in active order; reject metadata mismatches, shifts and
arithmetic overflow before verifying openings.

Port this supporting bound from PR #631 without call-rank machinery.
Tests cover alignment, active/inactive circuits, machine and field bounds,
serialized-key limits, and public verifier metadata rejection. All five
tests and strict release parallel Clippy pass. This guard makes the count
assumption explicit; it is not another demonstrated false-result exploit.

Co-authored-by: John C. Burnham <john@agathic.com>
@arthurpaulino @johnchandlerburnham
fix(aiur): reject Merkle caps that omit trace matrices
e9048e8 
Require the effective native MMCS cap to cover every trace matrix after
LDE blowup. Reject uncovered short matrices before verifying openings;
root caps take the constant-time path and trace layouts are unchanged.

Distill the third commit of PR #631. Reproduce native single- and
multi-opening acceptance of altered short-matrix values and identical
commitments for different short matrices. The public-verifier regression
fails before the guard and passes afterward; valid boundary caps still
verify. Compare the guard against direct injection geometry across
288225 boundary cases.

All 35 Aiur tests and strict release parallel Clippy pass.

Co-authored-by: John C. Burnham <john@agathic.com>
@arthurpaulino

arthurpaulino commented Sep 15, 2026

Copy link
Copy Markdown
Member Author

!benchmark fresh

@argument-ci-bot

argument-ci-bot Bot commented Sep 15, 2026 •
edited
Loading

Copy link
Copy Markdown
Contributor

!benchmark — main vs e9048e8

backends: aiur=prove · envs: InitStd · baseline: fresh (benchmark products rebuilt, base-SHA run, bencher bypassed)

aiur · InitStd · prove — main from: base run @ 58eb097 (fresh — bencher bypassed)

7 constants · 5 with regressions · 2 with improvements (|Δ| > 3.0% on any metric).

IxVM on FRI (7 constants)
constant execute-time (main) execute-time (PR) Δ% prove-time (main) prove-time (PR) Δ% throughput (const/s) (main) throughput (const/s) (PR) Δ% peak-ram (main) peak-ram (PR) Δ% proof-size (main) proof-size (PR) Δ% verify-time (main) verify-time (PR) Δ% fft-cost (main) fft-cost (PR) Δ%
ByteArray.utf8DecodeChar?_utf8EncodeChar_append 8.757 s 9.000 s +2.8% 37.224 s 37.492 s +0.7% 74.550 74.020 -0.7% 72.44 GiB 72.65 GiB +0.3% 5.16 MiB 5.20 MiB +0.7% 31.8 ms 33.1 ms +4.3% ⚠️ 132.99B 133.40B +0.3%
Char.ofOrdinal_le_of_le 6.453 s 6.479 s +0.4% 31.054 s 30.812 s -0.8% 88.970 89.670 +0.8% 62.75 GiB 62.94 GiB +0.3% 5.16 MiB 5.20 MiB +0.7% 30.8 ms 30.2 ms -2.1% 95.52B 95.82B +0.3%
Array.extract_append 6.527 s 6.392 s -2.1% 28.145 s 27.851 s -1.0% 57.060 57.660 +1.1% 53.13 GiB 53.26 GiB +0.3% 5.01 MiB 5.06 MiB +1.0% 29.5 ms 32.2 ms +9.3% (1.09× slower) ⚠️ 95.20B 95.44B +0.3%
Std.HashMap 3.999 s 4.009 s +0.3% 17.980 s 17.919 s -0.3% 113.570 113.960 +0.3% 36.41 GiB 36.39 GiB -0.0% 5.08 MiB 5.13 MiB +0.9% 30.1 ms 31.0 ms +3.2% ⚠️ 61.01B 61.21B +0.3%
_private.Init.Data.Range.Polymorphic.SInt.0.Int64.instRxcHasSize_eq 3.680 s 3.655 s -0.7% 16.972 s 16.871 s -0.6% 110 110.660 +0.6% 35.03 GiB 35.26 GiB +0.7% 5.05 MiB 5.09 MiB +0.8% 29.9 ms 29.9 ms +0.1% 55.56B 55.75B +0.3%
String.append 449.8 ms 441.7 ms -1.8% 1.906 s 1.878 s -1.5% 171.600 174.120 +1.5% 5.75 GiB 4.88 GiB -15.2% (1.18× smaller) 🟢 4.80 MiB 4.84 MiB +0.9% 29.0 ms 27.9 ms -3.7% 🟢 3.45B 3.46B +0.3%
Nat.add_comm 270.8 ms 267.8 ms -1.1% 772.2 ms 779.4 ms +0.9% 59.570 59.020 -0.9% 4.90 GiB 4.02 GiB -17.9% (1.22× smaller) 🟢 4.60 MiB 4.65 MiB +1.1% 26.7 ms 27.1 ms +1.7% 320.32M 321.01M +0.2%
FRI verifier on FRI (7 constants)
constant execute-time (main) execute-time (PR) Δ% prove-time (main) prove-time (PR) Δ% throughput (const/s) (main) throughput (const/s) (PR) Δ% peak-ram (main) peak-ram (PR) Δ% proof-size (main) proof-size (PR) Δ% verify-time (main) verify-time (PR) Δ% fft-cost (main) fft-cost (PR) Δ%
ByteArray.utf8DecodeChar?_utf8EncodeChar_append 2.600 s 2.596 s -0.1% 22.893 s 22.887 s -0.0% 121.220 121.250 +0.0% 56.50 GiB 56.56 GiB +0.1% 2.20 MiB 2.21 MiB +0.5% 13.0 ms 13.4 ms +3.4% ⚠️ 110.55B 111.05B +0.5%
Char.ofOrdinal_le_of_le 2.566 s 2.624 s +2.3% 22.998 s 22.968 s -0.1% 120.140 120.300 +0.1% 56.45 GiB 56.63 GiB +0.3% 2.21 MiB 2.20 MiB -0.5% 14.1 ms 13.7 ms -3.0% 110.68B 110.96B +0.2%
Array.extract_append 2.437 s 2.513 s +3.1% ⚠️ 22.159 s 22.529 s +1.7% 72.480 71.290 -1.6% 54.42 GiB 55.13 GiB +1.3% 2.20 MiB 2.21 MiB +0.4% 12.7 ms 13.4 ms +5.9% (1.06× slower) ⚠️ 105.50B 107.38B +1.8%
Std.HashMap 2.535 s 2.604 s +2.7% 22.411 s 23.018 s +2.7% 91.120 88.710 -2.6% 54.99 GiB 55.78 GiB +1.4% 2.20 MiB 2.21 MiB +0.2% 12.9 ms 12.9 ms -0.1% 108.13B 109.21B +1.0%
_private.Init.Data.Range.Polymorphic.SInt.0.Int64.instRxcHasSize_eq 2.469 s 2.592 s +5.0% (1.05× slower) ⚠️ 22.398 s 22.505 s +0.5% 83.360 82.960 -0.5% 54.64 GiB 55.12 GiB +0.9% 2.19 MiB 2.21 MiB +0.7% 12.9 ms 13.1 ms +1.5% 107.01B 108.09B +1.0%
String.append 2.338 s 2.375 s +1.6% 21.102 s 21.013 s -0.4% 15.500 15.560 +0.4% 50.49 GiB 51.44 GiB +1.9% 2.21 MiB 2.21 MiB -0.1% 13.6 ms 13.0 ms -4.6% 🟢 96.08B 98.51B +2.5%
Nat.add_comm 2.217 s 2.264 s +2.1% 20.979 s 20.742 s -1.1% 2.190 2.220 +1.4% 50.54 GiB 50.67 GiB +0.3% 2.21 MiB 2.20 MiB -0.5% 12.9 ms 13.9 ms +8.4% (1.08× slower) ⚠️ 90.48B 93.37B +3.2% ⚠️
Aggregate flat join (7 constants)
constant execute-time (main) execute-time (PR) Δ% prove-time (main) prove-time (PR) Δ% peak-ram (main) peak-ram (PR) Δ% proof-size (main) proof-size (PR) Δ% verify-time (main) verify-time (PR) Δ% fft-cost (main) fft-cost (PR) Δ%
ByteArray.utf8DecodeChar?_utf8EncodeChar_append n/a n/a n/a n/a n/a n/a n/a n/a n/a n/a n/a n/a n/a n/a n/a n/a n/a n/a
Char.ofOrdinal_le_of_le n/a n/a n/a n/a n/a n/a n/a n/a n/a n/a n/a n/a n/a n/a n/a n/a n/a n/a
Array.extract_append n/a n/a n/a n/a n/a n/a n/a n/a n/a n/a n/a n/a n/a n/a n/a n/a n/a n/a
Std.HashMap n/a n/a n/a n/a n/a n/a n/a n/a n/a n/a n/a n/a n/a n/a n/a n/a n/a n/a
_private.Init.Data.Range.Polymorphic.SInt.0.Int64.instRxcHasSize_eq n/a n/a n/a n/a n/a n/a n/a n/a n/a n/a n/a n/a n/a n/a n/a n/a n/a n/a
String.append n/a n/a n/a n/a n/a n/a n/a n/a n/a n/a n/a n/a n/a n/a n/a n/a n/a n/a
Nat.add_comm n/a n/a n/a n/a n/a n/a n/a n/a n/a n/a n/a n/a n/a n/a n/a n/a n/a n/a
Pipeline total (7 constants)
constant total-time (main) total-time (PR) Δ% pipeline-throughput (const/s) (main) pipeline-throughput (const/s) (PR) Δ% pipeline-peak-ram (main) pipeline-peak-ram (PR) Δ%
ByteArray.utf8DecodeChar?_utf8EncodeChar_append 1m 0.1s 1m 0.4s +0.4% 46.160 45.960 -0.4% 72.44 GiB 72.65 GiB +0.3%
Char.ofOrdinal_le_of_le 54.052 s 53.780 s -0.5% 51.120 51.380 +0.5% 62.75 GiB 62.94 GiB +0.3%
Array.extract_append 50.304 s 50.380 s +0.2% 31.930 31.880 -0.2% 54.42 GiB 55.13 GiB +1.3%
Std.HashMap 40.390 s 40.936 s +1.4% 50.560 49.880 -1.3% 54.99 GiB 55.78 GiB +1.4%
_private.Init.Data.Range.Polymorphic.SInt.0.Int64.instRxcHasSize_eq 39.370 s 39.376 s +0.0% 47.420 47.410 -0.0% 54.64 GiB 55.12 GiB +0.9%
String.append 23.007 s 22.891 s -0.5% 14.210 14.290 +0.6% 50.49 GiB 51.44 GiB +1.9%
Nat.add_comm 21.751 s 21.521 s -1.1% 2.110 2.140 +1.4% 50.54 GiB 50.67 GiB +0.3%

Workflow logs

@arthurpaulino
arthurpaulino added this pull request to the merge queue Sep 15, 2026
Merged via the queue into main with commit cf77c95 Sep 15, 2026
14 checks passed
@arthurpaulino
arthurpaulino deleted the ap/fixes branch September 15, 2026 19:29
samuelburnham added a commit that referenced this pull request Sep 15, 2026
@samuelburnham
Merge origin/main (#624–#634): FLT check costs, hoisting order, looku…
92fa743 
…p soundness and proof-shape validation

Conflicts and how they were resolved:

- Ix/Aiur/Stages/Source.lean: both sides fixed inlining's statement
  ordering; main's #628 (freshening plus prefix hoisting with tests in
  Tests/Aiur/Cross.lean) replaces the branch's statement-frame hoisting
  (13fada3), which nothing else referenced.
- crates/aiur/src/constraints.rs, memory.rs: both sides closed the same
  hole, a padding row pulling a return or memory message with a
  multiplicity of its own. Main's #634 form is kept (linear lookup
  multiplicity plus a `multiplicity * (1 - selector)` constraint) and the
  branch's memory-segment boundary lookups stay on top of it.
- crates/aiur/src/synthesis.rs: main's structural validation runs in
  build_on_device; main's proof-shape guards (claim shape, fixed trace
  heights, Merkle cap coverage, lookup query bound) now run on every
  shard header of a batch proof before the batch policy and verify_batch.
- Main's new synthesis tests (#634) are ported to the batch API: a
  hand-built witness is proven as a one-shard batch, shape fields live
  on the shard header, and Aiur's verify wraps multi-stark's errors.
- crates/ixvm-codegen/src/*.rs: the branch's generated kernels are kept
  provisionally; they are regenerated with `ix codegen` in the next
  commit from the merged Lean sources.
@arthurpaulino arthurpaulino mentioned this pull request Sep 16, 2026
Merged
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@gabriel-barrett gabriel-barrett gabriel-barrett approved these changes

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@arthurpaulino @gabriel-barrett @johnchandlerburnham