Verify HasPrimitives conservation - #32
Open
kim-em wants to merge 134 commits into
Open
Conversation
- State addDecl.WF, the intended main theorem of the Verify development, as a sorry in the new Verify/Environment.lean. - Update the 'currently false' comments in Verify/Axioms.lean: the lean4#8554 fix is long since merged, so the cached-flag axioms should now be provable from mkData_eq (but this has not been done yet). - Document that AddInduct (an empty inductive) is essentially a sorry. - divergences.md: the new level algorithm is not in fact complete (max 2 v >= imax 2 v fails, reachable from the inductive ctor universe check); plan of record is to verify the original algorithm. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
kim-em
force-pushed
the
agent/hasprimitives-conservation
branch
from
August 4, 2026 01:34
9b323af to
8bee9c5
Compare
# Conflicts: # Lean4Lean/Environment.lean # Lean4Lean/Inductive/Add.lean # Lean4Lean/Verify.lean # Lean4Lean/Verify/Axioms.lean # Lean4Lean/Verify/Environment.lean # Lean4Lean/Verify/Environment/Basic.lean # Lean4Lean/Verify/Environment/Lemmas.lean # divergences.md
kim-em
force-pushed
the
agent/hasprimitives-conservation
branch
from
August 4, 2026 02:10
041c498 to
2283ffe
Compare
Introduce a NatBinaryEvidence pack (contexts, bound-variable and value translations, and the generic recursive-call translation) together with a generic checkNatBinaryTyped.WF theorem covering the uniform part of the Nat.add/Nat.sub/Nat.mul/Nat.pow typed checker proofs. Each per-primitive WF_typed proof now supplies only its required-constant facts and the typed translations of its two equation right-hand sides. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_017b11HQL6K7r3R6La5nNadk
Remove the unused plain .WF and .WF.conservesHasPrimitives checker theorem families for all primitives, together with their now-orphaned helpers: the verified environment layer consumes only the WF_typed variants. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_017b11HQL6K7r3R6La5nNadk
Introduce checkSafePrimitiveDefinition.WF covering the checker program shared by all safe primitive definitions; each per-primitive theorem now supplies only its WF_typed lemma (plus, for the evidence-pack cases, the level-parameter projection). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_017b11HQL6K7r3R6La5nNadk
Add VEnv.LE.contains, .mono transport lemmas for the four primitive evidence packs, and a generic addDefinition.WF_safe_primitive theorem; each per-primitive WF_safe theorem now supplies only its checker theorem and the conservation argument for its own evidence. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_017b11HQL6K7r3R6La5nNadk
Restate checkPrimitiveDef.nat{Xor,Land,Lor}.WF_typed without the
value-shape hypothesis: the proofs now split on the checker's own match
on v.value. This lets the three checkSafe*Definition.WF theorems ride
the generic checker theorem and replaces the success_*_value_shape
monad-stack dissections (and their maxSteps workaround) with direct
WF_safe members.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_017b11HQL6K7r3R6La5nNadk
Introduce checkNatBinaryBoolTyped.WF covering the checker program shared by Nat.beq and Nat.ble; the two WF_typed proofs now supply only the translations of their three boolean right-hand sides. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_017b11HQL6K7r3R6La5nNadk
Introduce checkNatShiftTyped.WF for the binary Nat primitives that recurse on their first argument; Nat.shiftLeft and Nat.shiftRight now supply only their required constant and successor right-hand side over the shared NatBinaryEvidence pack. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_017b11HQL6K7r3R6La5nNadk
Add List.Forall₂.forall_left/forall_right to Std.Basic and reduce the mutual-header/body projection lemmas to one-line applications of these and Forall₂.imp; delete the unused mutualHeader_toFinal. Collapse the six inductive-name dispatcher cases and drop its maxRecDepth bump. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_017b11HQL6K7r3R6La5nNadk
The Forall₂ lemmas live under the Lean4Lean namespace prefix (core owns List.Forall₂), so dot notation cannot resolve them; apply them by name. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_017b11HQL6K7r3R6La5nNadk
Introduce of_unary_step_equations (Nat.add via Nat.succ, Nat.sub via Nat.pred) and of_binop_step_equations (Nat.mul via Nat.add, Nat.pow via Nat.mul), each carrying the shared literal-evaluation induction once; the four per-primitive of_*_equations lemmas become instantiations. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_017b11HQL6K7r3R6La5nNadk
Rewrite addNatPred/addNatAdd/addNatSub as addPrimitiveDefEq wrappers instead of hand-built HasPrimitives records, and introduce HasPrimitives.defKit carrying the shared typing/defeq scaffolding of the add*Def theorems; nine members now supply only their equation semantics. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_017b11HQL6K7r3R6La5nNadk
Introduce addConst_all (the per-safety addConst construction) and the generic addConst_ext / addConst_ext_ite scaffolding theorems covering the unthresholded and thresholded environment extensions; the nine VEnvs.WF.add* theorems become short instantiations with their per-declaration translation and primitives steps. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_017b11HQL6K7r3R6La5nNadk
Introduce FuelStep and VEnv.natLit_defeq_of_fuel_relation, the strong induction shared by every fuel-indexed primitive recursion, and re-derive the four existing inductions (of_modCore_equations, of_divCore_equations, of_gcd_fix_relation, evalNatBitwise_of_fix_relation) as instances with their statements unchanged. Include the design document for the remaining layers of the certificate interpreter. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_017b11HQL6K7r3R6La5nNadk
The executable checker must faithfully match the lean4 kernel, so the interpreter design is verification-side only; the certificate-entry unification layer is out of scope. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_017b11HQL6K7r3R6La5nNadk
Factor the checked-lambda instantiation into a single-binder step lemma (instantiate_lamU_step) with the lam3/lam4 forms as instances, move the telescope-agnostic proof-binder lemma next to lam_instU₂, and rewrite the gcd top/zero/succ semantics on canonical call/state helpers; the gcd-specific argument swap and Nat.mod renormalization stay visible. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_017b11HQL6K7r3R6La5nNadk
Introduce Verify/ConditionReflect.lean carrying the Reflection-scheme and Bool-implementation generic machinery: branch selection for ite/natDITE applications, applied-term canonicalization, literal evaluation through any ReflectsNatNatBool primitive, and closed-lambda instantiation. The natLE (mod/div) and natEq (bitwise) condition files become instantiations with their public interfaces unchanged. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_017b11HQL6K7r3R6La5nNadk
Replace the mod/div instantiation ladder and proof-binder alignment with instantiate_lamU_step and finish_bitwise_proof_equation via a generic instantiate_natGo_equation, dedupe the mod/div twin lemmas through a parameterized NatGoEquationTranslation with thin per-track instances, and factor the shared body of the two bitwise zero transition proofs; all public statements unchanged. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_017b11HQL6K7r3R6La5nNadk
…nery Generalize the bitwise weakening/instantiation helpers to the 4- and 5-binder level in BitwiseSupport (the zero transitions now consume them from there), add a canonical translation lemma for g (Nat.succ x) 2 over any reflected binary primitive, and restructure the successor proof as call-spine canonicalization plus right-hand-side semantics over the shared condition and telescope lemmas; the succ_semantics statement is unchanged. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_017b11HQL6K7r3R6La5nNadk
Brings the branch onto v4.33.0-rc2. The kernel hardening in that release (leanprover/lean4#14608) rejects mutual blocks whose members disagree on their universe parameters or repeat a name, which `preserve mutual definition parity` had deliberately started accepting. Restores both checks as `checkMutualNames`, guarded by `check` as the kernel guards them, and drops the now-false clause about duplicate names from the `addMutual` divergence entry. `Tests/Environment.lean` asserted that the kernel accepted both of those, so its two mutual-block cases are gone; `Tests/KernelHardening.lean` on master covers the same ground with the opposite expectation.
`checkMutualNames` forces every member's universe parameters to agree, so the per-member `M.run` no longer varies them; only the caches differ.
kim-em
marked this pull request as ready for review
August 6, 2026 03:00
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.
Summary
VEnv.HasPrimitivesthrough primitive definitions, mutual definitions, quotient initialization, and declaration dispatchBase
PR #28 has merged. This branch now merges current
master(1a16b72), so the PR is no longer conflict-blocked or dependent on an unmerged stack. The conservation proof continues to build on theVEnvs.WF/TrEnvverified-environment model introduced by #28.Review and simplification
An independent simplification review has been acted on in the branch. In particular, the mutual-definition implementation and conservation argument no longer impose the recovered branch’s stricter common-universe/unique-name runtime behavior.
A first economy pass factored the verified type/zero/successor equation chain shared by
Nat.add,Nat.sub,Nat.mul, andNat.pow, but saved only 14 net lines: most of the size was in constructing the typed translations. A systematic second round therefore lets shared evidence own those translations outright. On the checker side, theNatBinaryEvidencepack with the genericcheckNatBinaryTyped.WF,checkNatBinaryBoolTyped.WF, andcheckNatShiftTyped.WFtheorems covers the binaryNat,Nat → Nat → Bool, and shift primitives, and the bitwiseWF_typedlemmas now perform the value-shape split themselves. On the environment side,checkSafePrimitiveDefinition.WF,addDefinition.WF_safe_primitive, and theVEnvs.WF.addConst_extscaffolding absorb the per-primitive checker, conservation, and extension boilerplate, and the checker layer superseded byWF_typedis deleted outright. Together with generic recurrence lemmas for the add/sub/mul/pow reflection arguments and theHasPrimitives.defKitscaffolding, this removes about 3,600 net lines, with every theorem statement consumed elsewhere left unchanged. The substantive bitwise and mod/div reflection mathematics is deliberately untouched, and no specification/certificate interpreter turned out to be needed.Checks
lake build(164/164) ✅Lean4Lean.Experimental,Init.Corereplay, and cleanInit.System.IOrecheck ✅git diff --check✅sorryin the changed environment files ✅