fix(aiur): preserve scope and effect order during hoisting - #628
Merged
Merged
Conversation
Freshen caller and callee bindings with a collision-free name supply, preserve strict argument evaluation order, and keep assertions, IO, and debug statements before their continuations. Port the production fix from 0ecd150 in PR #626. Reproduce 40 failing checks in the existing aiur-cross suite before applying the fix. Cover shadowing, effect order, guarded inline matches, generated names, and pattern validity there, and add one combined aiur-prove case with explicit output and IO expectations. Regenerate all three Rust modules. Validation: Aiur cross, proof, cost, hash, RBTreeMap, Multi-STARK, and recursive-verifier suites pass with --wfail. After codegen, the IxVM suite passes all 249 parity checks and all 83 kernel FFT pins plus the shard pin; no FFT pin updates are needed. Codegen --check passes for all three modules. Co-authored-by: J. C. Burnham <jcb@agathic.com>
arthurpaulino
enabled auto-merge
September 12, 2026 00:37
samuelburnham
approved these changes
Sep 12, 2026
samuelburnham
added a commit
that referenced
this pull request
Sep 15, 2026
…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.
samuelburnham
added a commit
that referenced
this pull request
Sep 16, 2026
…ging main `ix codegen` from the merged Lean sources: main's FLT kernel work (#624, #627) and hoisting fix (#628) on the IxVM side, the branch's record-cap propagation at returns and calls on all three. `ix codegen --check` reports the three files up to date; the CUDA build of the merged tree passes and the aiur, ix-kernel and ixvm-codegen release test suites pass (66, 841 and 7 tests).
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Freshen caller and callee bindings with a collision-free name supply, preserve strict argument evaluation order, and keep assertions, IO, and debug statements before their continuations. Port the production fix from 0ecd150 in PR #626.
Reproduce 40 failing checks in the existing aiur-cross suite before applying the fix. Cover shadowing, effect order, guarded inline matches, generated names, and pattern validity there, and add one combined aiur-prove case with explicit output and IO expectations. Regenerate all three Rust modules.
Validation: Aiur cross, proof, cost, hash, RBTreeMap, Multi-STARK, and recursive-verifier suites pass with --wfail. After codegen, the IxVM suite passes all 249 parity checks and all 83 kernel FFT pins plus the shard pin; no FFT pin updates are needed. Codegen --check passes for all three modules.