[0.5.0] Discharge the overflow effect with a kernel-checked bound #116

Activity

1. humuhumu33

   added this to the LexLean v0.5 milestone on Oct 16, 2026
2. humuhumu33 commented on Oct 22, 2026

   

   humuhumu33

   on Oct 22, 2026

   Contributor

   More actions

   Taking this one. Plan: a production root may name a bound, production: {effects: E, targets: T, bound: B}, where B is a prior theorem of the root's module whose statement is exactly the obligation linking generates from the root (as for termination evidence and model entries, require_statement): under the hypothesis that each nat and int parameter lies in the target width, every operation of the root's own body whose registry row names its result representation (nat_add, nat_mul, succ, int_add, int_sub, int_mul, int_neg) stays within that width, a conjunction in evaluation order. verify kernel-checks the theorem like any other. Eligibility then discharges the overflow sources the bound covers and refuses, with a registered diagnostic naming the operation, a bound that does not cover one (an operation under a match, an if, a lambda or in a callee, or another primitive), so the effect is never silently kept or dropped and nothing is inferred by an optimizer or checked at run time. The rendering of a discharged root calls plain runtime items (a + b, no R<T>, no ?), whose declared machine meaning is the primitive with abort at the overflow the bound rules out; certificate A proves from B that __fits_0 holds on every representable argument, so A and E state the value outcome. Register rows, scenarios and failing tests first (R3): one PD row for the discharge and its diagnostic, one SP row for the certificates, one RB row for the rendering, one LLT error row; a general corpus root in examples/production-coverage (a midpoint with two additions, the textbook overflow) with its bound, written to become a member of #124's corpus. This moves the language identity (runtime text, RustSyntax), so the PR lands one at a time with its regeneration. Draft PR against release/v0.5.
3. humuhumu33 commented on Oct 23, 2026

   

   humuhumu33

   on Oct 23, 2026

   Contributor

   More actions

   Draft PR: #295 (against release/v0.5).

   What landed in the PR: the bound as a member of the production declaration, linking's obligation and LLT4017, eligibility's discharge and the bound of the report (PD-09), and certificate A's bounded and root_value, kernel-checked with the pinned Lean on the new corpus root Coverage.Bounds.maxOfThree (SP-29). The plants (bound removed, narrowed, reordered, forged) are in VERIFICATION.md with their output.

   What is registered and open: RB-20, the rendering without checks. The acceptance's second half needs a Rust construct certificate B can certify, and the declared machine has none: every unchecked operation is a new Machine or Item constructor whose correspondence rule and soundness case live in the migrated proof library (RustCorr, RustSound), and Callee.machine has no correspondence rule at all today, so it cannot carry the rendering. The shape that fits the library as it stands: an infallible runtime item per covered operation (nat_add_plain(a, b) -> u64 { a + b }, itemFallible = false, itemPrimitive = natAdd), whose machine meaning runItem already gives, the primitive's overflow as abort, which Realizes accepts and which root_value proves no argument in the width reaches; SP-07's rule that an infallible item never overflows on the boundary inputs then needs the plain items excepted for that reason, as a length is. That is a proposal, not done here; the row, scenario and failing test are in place for it.

   @afflom, one question: will you add the correspondence rule (and its soundness case) in the proof library for an unchecked operation along these lines, or do you prefer another route for RB-20?

   The PR moves the language identity (the module schema gains the member), so it lands alone with its regeneration; what was regenerated here is stated in the PR (everything but the Atlas).
4. humuhumu33

   added 2 commits that reference this issue on Oct 23, 2026

   chore(#116): regenerate SPEC.md, calculus and production export after…

   ...

   64af3e0

   chore(#116): relock spec and the performance corpus, rewrite the gene…

   ...

   335e6da
5. humuhumu33 commented on Oct 24, 2026

   

   humuhumu33

   on Oct 24, 2026

   Contributor

   More actions

   @afflom, a ping on the question above: draft PR #295 stays a draft, with RB-20 red by design, until you rule on it.

   The one question: will you add the correspondence rule (and its soundness case) in the proof library for an unchecked operation, along the lines of the infallible runtime item nat_add_plain(a, b) -> u64 { a + b } described above, or do you prefer another route for RB-20?

   What I need back: yes or no on that rule, and if no, the route you want. PD-09 and SP-29 are Lean-verified already, and nothing else in the PR waits on your answer. The PR lands after #300 and #303, and I will merge release/v0.5 into it and regenerate then.
6. afflom commented on Oct 25, 2026

   

   afflom

   on Oct 25, 2026 – with Claude

   MemberAuthor

   More actions

   Ruling on the RB-20 route (read on three trees: release/v0.5 at 80bf4bae9, #295 at 335e6da9f, and the v0.4 heap line at H6 20b23c0df, which forward-merges into release/v0.5 after the heap half lands; nothing built). Sorry for the wait.

   Yes to your shape, and no new correspondence rule is needed. A plain infallible runtime item per covered operation (itemFallible = false, itemPrimitive = natAdd, the primitive's overflow as abort) is already covered by the library as it stands: the prim rule is generic over the item (RustCorr 600-605 in the Lean source at ba52c601: premises itemPrimitive item = op, plainItem item, itemOK, itemTyped, primTyped, !itemFallible item || fl), and sem_prim (RustLemmas 1062-1130) discharges the infallible overflow case with abort through runItem_eq; Realizes takes .overflow, .abort (RustCorr 764-768), and certificate B's root statement is already RealizesFn. So a Callee.machine rule is not the route: it would be a new rule plus a new sem_* case for no gain. Callee.machine stays without a rule.

   What the route costs, and who carries it.

   1. New Item constructors invalidate the migrated library: itemOperands_eq is cases item, and the DAG names every constructor and Item.casesOn. The library is a kernel-DAG export with no Lean source in the tree, so it is re-elaborated from the sources at ba52c601:language/preservation-1.2/library/LexLeanPreservation/ with the exporter at d54dbf855:tests/preservation-library/oracle/ (precedent for a post-migration change: 1ca756cd2, which grafted RustCorr/RustSound nodes with a one-off tool), with MIGRATION.md's equivalence evidence updated. That is yours, in #116: a production root's overflow effect discharged by a kernel-checked bound (PD-09, SP-31; RB-23 red) #295; I land it.
   2. The rest is as you listed it: the constructors and their rows in RustSyntax.lex.tex (itemPrimitive, itemFallible, itemHeap, itemOperands, itemWidth, itemTakes/itemShifts, itemAccepts), Item::all() and data_b::item_constructor in the renderer, the plain items in the runtime text, the RB-20 case.
   3. SP-07's exception is structural, not by name: a renderer predicate (item.plain()), skipped the way length_ is skipped, and armed: the case asserts that each plain item does overflow on a boundary input (otherwise the exception is vacuous), and RB-20 asserts plain items are called only from roots whose bounded discharged the operation.
   4. Pin the overflow outcome. The differential builds debug crates, where a + b panics as abort models; a release build wraps. The generated Cargo.toml must set overflow-checks = true in every profile, and the RB-20 statement must say "without LexLean's checks (R<T>, ?)", not "without checks": the declared machine says abort, and the rendered program has to realize it.

   Sequence. The implementation lives in files the heap half rewrites: runtime.rs is gone after RB-21 (the std runtime is source, compiler/src/RustRuntime.lex.tex), ast.rs, data_b/syntax.rs and the bootstrap twins all move, and on that tree a plain item is a RustRuntime function whose body is a new plain Machine constructor (printed {} + {}), with printer and validator twin cases and a refines_* for SP-30. So RB-20 is written after the forward merge of release/v0.4, which I do once the heap half lands (#297, #298, #304, #305). #295 then lands after #300 and #303, as you planned. Two things to do at that merge, not before: renumber RB-20 and SP-29, which collide with the v0.4 line's RB-20 (the std runtime text) and SP-29 (refines_*), to the first free numbers above the merged line's (test names, feature tags and IdsRB/IdsSP follow); and merge preservation.rs (your hunk 1535-1723, H6's at 4809/4854, disjoint).

   PD-09 and SP-29 as they stand need nothing from me. Say here if any of the four points changes your estimate.

   ---

   Generated by Claude Code
7. humuhumu33 commented on Oct 25, 2026

   

   humuhumu33

   on Oct 25, 2026

   Contributor

   More actions

   Thank you for the ruling. All four points are accepted, with one change to the estimate.

   1. Library re-elaboration (mine, in #116: a production root's overflow effect discharged by a kernel-checked bound (PD-09, SP-31; RB-23 red) #295). I re-elaborate LexLeanPreservation from the sources at ba52c601 (13 modules, RustLemmas the largest at about 160 KB) with the exporter at d54dbf855, graft the new Item constructors in the way 1ca756cd2 did, and update MIGRATION.md's equivalence evidence. Callee.machine stays without a rule.
   2. The rest as listed. The constructors and their RustSyntax rows, Item::all() and data_b::item_constructor, the plain items in the runtime text, and the RB-20 case. On the post-merge tree that means the RustRuntime function with a plain Machine constructor, the printer and validator twin cases, and the refines_* for SP-30.
   3. SP-07's exception is structural. A renderer predicate item.plain(), skipped the way length_ is. It is armed: the case asserts each plain item overflows on a boundary input, and RB-20 asserts plain items are called only from roots whose bounded discharged the operation.
   4. Overflow outcome pinned. overflow-checks = true in every generated profile, and the RB-20 statement reads "without LexLean's checks (R<T>, ?)".

   Estimate. It goes up. Before, RB-20 was one correspondence rule plus the renderer. Now the dominant cost is the library re-elaboration and its equivalence evidence, and I cannot size it before running the exporter once on the ba52c601 sources. I will prepare that tooling in a scratch directory and report the measured cost here before writing any RB-20 code. Everything that touches the files the heap half rewrites waits for your forward merge of release/v0.4.

   At that merge I renumber RB-20 and SP-29 to the first free numbers above the merged line's and merge preservation.rs (my hunk 1535-1723 against H6's 4809/4854). #295 stays a draft and lands after #300 and #303.
8. afflom

   added 3 commits that reference this issue on Nov 1, 2026

   chore(#116): regenerate verification records after merging release/v0.5

   ...

   69c64a7

   chore(#116): rewrite the calculus fixtures after the relock

   ...

   6010432

   docs(#116): record the forward merge and the state of RB-23 in VERIFI…

   ...

   61e9b04
9. humuhumu33

   added a commit that references this issue on Nov 2, 2026

   Renumber to SP-32 and SP-33: SP-31 is claimed on release/v0.5

   ...

   4f41736