Prove each arith host role in its own certificate theorem - #770
Merged
Conversation
The whole-module arith host-role check was proved as a single kernel reduction that materialized all five decoded and synthesized helper bodies at once, setting a high memory floor for every certificate over a module that carries the Int runtime. Split it: a carriered module now proves each declared role in its own freed theorem in a separate generated file and recombines them with a cheap rewrite. The emitted acceptance theorem's statement is unchanged byte for byte; only its proof differs. A module without the Int carrier keeps its original single-step proof and emits no extra file.
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.
A follow-up to the per-claim proof split. After that change, the one per-module conjunct still above the import floor is
decodedHostRoles, whose proof was a singledecide +kernelthat materializes all five decoded and five synthesized host-helper bodies in one kernel reduction (~0.5 GB over the floor).What changed
Producer-side only, two files. A carriered module now emits a small
ArtifactHostRoles.leanunit holding five leaf theorems — onearithRoleCheck … = trueper host role (box,toIndex,add,sub,mul), each its own freed top-level declaration proved bydecide +kernel.Artifact.leanimports them and provesdecodedHostRolesby rewriting the manifest projections to their literals, unfoldingarithTableCheck, rewriting the five role subterms totruefrom the leaves, and closing the remaining carrier/index conjuncts with onedecide +kernel. The theorem statement is byte-identical; only its proof changed. Carrierless modules keep the original single-step proof and emit no leaf file.The wall is untouched — no
assets/wall/**,CURRENT_WALL_IDdoes not move. A wrong split fails the kernel, so there is no soundness surface.Measured (affine, capped)
Artifact.lean: 1.458 GB → 0.903 GB (1.6x), the shelf the earlier floor measurement projected.cert verifypeak: 1.445 GB → 1.335 GB (~7%). The verify peak is the max over all Lean subprocesses, and onceArtifact.leandrops, the ceiling becomes the wall's ownRecursionSoundnessbuild (~1.3 GB) — intrinsic to the unchanged wall and not movable from the producer side. This is the honest headline: the change takes the one currently-shaveable per-module cost off the table, but on a small module the practical win is modest because a wall-build cost sits just underneath. It helps most whereArtifact.lean, not the wall build, is a module's ceiling.Gates
cert_certify_spec34/34 (no snapshot drift), wall-identity tests pass unchanged, axioms[propext, Classical.choice, Quot.sound],cargo fmt --checkclean, clippy clean in all shapes.