WIP: Monorepo MegaPR: Integrate certified checking, compilation and Aiur soundness foundations - #629
Open
johnchandlerburnham wants to merge 31 commits into
Open
johnchandlerburnham wants to merge 31 commits into
johnchandlerburnham wants to merge 31 commits into
Conversation
Import the compiler and selected consistency model into Ix, consolidate the production kernel, and maintain the certified source and claim adapters with their exact provenance, dependency audits, differential corpora and CI gates. Repair Aiur call-cycle, inactive lookup, memory and compiler-normalization soundness defects, retain native supplied-witness regressions, and add checked extraction from balanced physical circuit lookups to finite bytecode execution. Derive witness shapes and lookup limits from the actual compiler and grouping. The Aiur component audit now checks 268 roots and freezes their exact premises and runtime inventory. Full public certified-verification soundness remains open: native/FFI reflection, the remaining compiler and certified VM bridge, release selection and the concrete cryptographic reduction are not asserted. Validation: compiler, theory, certified-adapter and Aiur component gates; 49 parallel release Aiur tests, release Clippy, 1,345 broader Aiur assertions, C2 VM integration cases, and exact generated VM source comparisons.
Decode the native memory layout and its four valued equations into valid memory rows and equivalent weighted lookup providers. Compilation supplies distinct canonical memory widths, and the checked global trace budget gives functional memory. Compose these results with backend trace execution. Add 1,800 native/Lean memory-row comparisons and include them in check-aiur. The exact audit now covers 290 roots and preserves every prior root statement, premise definition and recursion-worker body. Full C8 native extraction, compiler refinement and certified semantic/cryptographic soundness remain open. Validation: strict Lean build; exact audit and review; all eight native comparisons and complete check-aiur gate; 50 parallel release Rust tests; release Clippy with warnings denied; Rust formatting and whitespace checks.
johnchandlerburnham
changed the title
Require fixed preprocessed tables active at their committed heights before Aiur enters cryptographic verification. Prove the total guard's shape and alignment properties, and connect all thirteen physical byte lookup slots to the logical provider tables. Combine canonical function, memory and byte columns in SystemTraces for selected-call execution and functional memory. Compare 17,910 native/Lean guard cases and evaluate the existing exhaustive byte corpus through the physical column model. The exact audit covers 308 roots, preserving all previous root statements, premises and worker bodies. Add a documented inventory of the confirmed Aiur bug fixes and open issues. Validation: strict Lean build; exact audit/review; all nine native comparisons and complete check-aiur gate; 54 parallel release Rust tests; release Clippy; 1,345 broader Aiur assertions; C2 VM 12 accepted / 16 rejected / 2 exclusions with zero unexpected errors; formatting and whitespace checks. Native verifier/codec reflection, compiler refinement and full certified semantic and quantitative cryptographic soundness remain open.
Reject malformed key-graph references before degree recomputation; check leaf/root bounds, stage-two lookup-prefix reads and overflowing or incorrect degrees. The self-reference regression previously panicked and now errors. Valid keys retain their existing v5 bytes. The decoder currently has no production callers; serialization is the connected key path. Prove defined full/prefix sweeps, expression unfolding and weighted lookup projection for arbitrary working operations. Compare 88,228 native layouts and 240 assignments over ten actual compiled graphs, including 8,016 node values and the shorter prefix reconstructed after constant folding. Validation: strict 237-job build, exact 338-root audit/review, eleven native comparison corpora and complete component gate, all 59 parallel release Rust tests, release Clippy with warnings denied, formatting and whitespace. All 308 earlier root statements, 318 premise definitions and 146 worker bodies are unchanged. Add 30 roots, 58 definitions and four inspected workers. Frontend/Rust/codec refinement and full certified semantic and quantitative cryptographic soundness remain open.
Derive the four verifier challenges and continuing PCS challenger state from the selected key parameters and shape, proof commitments, heights, public claims and accumulators. Prove exact observation order, buffer invariants, finite rejection traces, fuel monotonicity and integration with checked-row arithmetic. Keep the 32-byte hash function explicit; concrete hashing, PCS authentication and quantitative security remain open. Compare 40 actual native verifier schedules and PCS continuations, four accepted proofs, 1,280 byte operations, 26 forced rejected limbs and 48 witness checks. Preserve all 1,162 prior root statements and axiom sets, 791 definitions and 174 workers in the reviewed 1,231-root audit. All 86 parallel Rust tests, strict Clippy, formatting, the 445-job build and the complete 30-corpus gate pass.
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
1 participant
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.
Import the compiler and selected consistency model into Ix, consolidate the production kernel, and maintain the certified source and claim adapters with their exact provenance, dependency audits, differential corpora and CI gates.
Repair Aiur call-cycle, inactive lookup, memory and compiler-normalization soundness defects, retain native supplied-witness regressions, and add checked extraction from balanced physical circuit lookups to finite bytecode execution. Derive witness shapes and lookup limits from the actual compiler and grouping.
The Aiur component audit now checks 268 roots and freezes their exact premises and runtime inventory. Full public certified-verification soundness remains open: native/FFI reflection, the remaining compiler and certified VM bridge, release selection and the concrete cryptographic reduction are not asserted.
Validation: compiler, theory, certified-adapter and Aiur component gates; 49 parallel release Aiur tests, release Clippy, 1,345 broader Aiur assertions, C2 VM integration cases, and exact generated VM source comparisons.