WIP: Jcb/ixvm consistency - #632
Open
johnchandlerburnham wants to merge 30 commits into
Open
johnchandlerburnham wants to merge 30 commits into
johnchandlerburnham wants to merge 30 commits into
Conversation
Add certified source and claim entry points whose receipts connect authenticated Ixon source to the set model. A closed logical receipt excludes the profile's false proposition under the explicit SetTheory hypothesis. Move Ix.Tc and its callers to Ix.Kernel, internalize the named specification, and import the kernel, theory, and host scaffolding from jcb/monorepo at 7b06b75. Remove the root lean4lean dependency and its replay benchmark and test targets. Preserve source identities, licenses, exact theorem audits, and the frozen adapter corpus. Include the separate Mathlib ZFSet construction: a countable increasing chain of strongly inaccessible cardinals supplies the actual Ix SetTheory interface. The model-existence theorem's full dependency audit permits only propext, Classical.choice, and Quot.sound; the cardinal hypothesis stays explicit. Direct production refinements cover universe comparison, structural expression reading, interning, and sort inference. Full checkEnvAnon refinement remains open. New compiler, circuit, and certificate VM development is deferred; existing compiler proofs receive the necessary namespace and exact hash-axiom audit updates. Run the implementation-proof audits on ordinary PRs, add the unified lake run check-kernel --with-model gate, and document the theorem boundaries and review entry points. Replace milestone labels in docs, comments, and test diagnostics with functional descriptions while retaining frozen inputs. Validation: - lake run check-kernel --with-model - lake test --wfail -- cli - ix codegen --check - bench-measures tests and benchmark CLI help - nix-instantiate --parse flake.nix
Connect all-success production checkEnvAnon results to model extension for monomorphic standalone aliases and closed universe terms. The proof follows the actual lazy lookup, standalone routing, reset, validation, inference, and conversion calls. Its operational witnesses require uncached value inference and the initial hash-equality conversion path with explicit representation faithfulness; they do not assume a checker-soundness callback or supplied typing proof. Start the model interface with exactly the source axioms, then add fresh definitions in dependency order while retaining their actual serial work positions. Every model of the axiom interface extends without changing any axiom interpretation. Source representation includes the checked type, universe arity, and definition body. The no-False corollary preserves an initial empty interpretation, and a separate theorem excludes fresh self aliases. All result rows must succeed; the public outer ok is insufficient. The full checker and independent serialized-Ixon reader refinement remain outside this fragment. Runtime checker behavior is unchanged. Validation: - lake build --wfail IxKernelConsistency: 36 exact full-dependency audits, no proof holes or checker/certificate soundness shortcuts; four existing generated 32-byte length proofs are enumerated explicitly. - lake test --wfail -- tc-unit: 403 checks, including eight new production regressions for aliases, sorts, cache clearing, and failed result rows. - git diff --check
Replace repeated state-monad case splits with a local bind-success lemma and direct EStateM.bind unfolding. Name the components of soundness results and simplify result-preservation and entry-equality proofs. Keep model extension's explicit import in the environment layer. Public theorem statements and their assumptions are unchanged. Tighten comments and documentation around the supported production fragment, the source-axiom model hypothesis, and remaining refinement obligations. Collect provenance details together and link the Mathlib model to the fragment contract. Validation: - lake build --wfail IxKernelConsistency: 36 exact theorem audits passed. - lake test --wfail -- tc-unit: 403 checks passed. - git diff --check: passed.
Constrain inactive provider multiplicities, enforce range-checked call ranks, validate lookup message boundaries, and gate lookups in circuits whose control flow does not establish a unique writer. Check control counts, fixed-table shapes, and the global lookup budget. Align compiler layouts and witness generation with the rank constraints, retain supplied-witness regressions, and update the measured FFT baselines.
Port emission validation from b8cf284 and the EqZero allocation repair from f83498c on top of the optimized component-rank and lookup-group implementation. Retain the native regressions from monorepo 1260006 and check rejection with an acyclic component layout as well. Validation: 60 release Aiur tests passed (two existing performance tests ignored); release Clippy with all targets and parallel features passed with warnings denied; cargo fmt check passed.
Import the scoped Aiur proof and native-binding components onto the newer kernel base without the independent compiler library. Adapt generic calls to six gap columns and derived child ranks, prove component relayout preserves complete evaluation and arity, and model all three allocation modes. Generic physical extraction explicitly retains its layout premise pending the full component-mode extension. Bind compiled keys after production lookup retuning. Preserve the destination fresh-name implementation while fixing demonstrated array-update effect order and explicit-return inlining errors. Review and freeze 1,574 root statements, 988 premise sections and 197 runtime workers, with the source migration review beside the manifest. Validation: check-aiur; check-kernel --with-model; 112 parallel native release tests; all-target parallel Clippy with warnings denied; format; three generated executor checks; Lean proving/components/byte hints/recursive-verifier/aggregate suites; full ignored IxVM corpus and unchanged shard FFT cost.
Replace Lean's unbounded conversion loops with source-derived finite work bounds and reject cycles in active sharing expansions. Validate reachable sharing graphs before Rust conversion, memoizing completed expression DAGs. Prove the actual loader changes only declarations, blocks and intern tables on success and failure, then establish the driver's structural local-state invariant without an assumed loader effect. Discharge projection inference's separate state contract using its recursive inference and reduction contracts. Audit all 59 new projection/ingress roots with exact dependency allowances. Validation: full check-kernel --with-model gate; 847 Rust kernel tests passed (8 ignored); release Clippy and formatting; nine new native Lean regressions. Conversion semantics and general mutual checker soundness remain open.
Prove that public inference, reduction and conversion preserve the caller's local declarations and installed loader on success and failure, while maintaining coherent lookup and a monotone fresh-variable bound. Induction on production's finite method tables discharges all recursive frame premises. Cover the actual reduction and conversion helpers, bounded workers, binder and let scopes, speculation, cache updates and cleanup. Add checked proof composition and register exact full-dependency allowances for all 279 new theorem roots. No production or Rust implementation changes. Validation: strict IxKernelConsistency build (717 audited roots), full check-kernel --with-model gate, and git diff --check pass. General semantic checker soundness and the remaining IxVM milestones are still open.
Distinguish source recursion from a cyclic reference in an elaborated safe kernel declaration. Add structural, well-founded and mutual Lean recursion fixtures, export each complete dependency closure without partial output, and require successful checking by both host kernels with matching targets. Check that every requested definition remains present and is actually checked. Register the positive regressions in tc-unit and a focused tc-safe-recursion suite, and clarify the kernel-level scope of the guard in the documentation. Production code and theorem trust boundaries are unchanged. Validation: lake test --wfail -- tc-safe-recursion and the full lake test --wfail -- tc-unit pass. git diff --check passes.
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.
Working towards a proof that the IxVM circuit cannot admit
False