[afflom]

Stacked on #259 (claude/issue-91-stage4-heap-validate at eda82e1ad, merged in); draft. First of the two memory PRs of the heap half (H3a of H3a/H3b; the list representation and its abstraction theorems are H3b).

What

RustMemory (compiler/src/RustMemory.lex.tex, a language-1.2 module of the compiler project over the calculus's values; two inductives Flag and Cells, two structures Buf and Window, and sixteen definitions) models a runtime buffer (Buf) as index-addressed slots (Cells), whose number is the capacity, and a length, and a slice (Window) as base slots, an offset, and a count (subWindow taking a window of a window, its count bounded by what the parent has left after the skip, minusNat). Seventeen theorems, each kernel-checked with [propext], no definition observing an axiom:

• size_put: a write never changes the number of slots (put beyond the slots is a no-op in the model and is not the runtime's behaviour, which refuses).
• get_put_same, get_put_below, get_put_above: a write is read back at its own index (none when no slot), and every slot below and above it is as it was.
• size_blank, get_blank: a new buffer has the capacity it was asked for, each slot the fill.
• no_room_at_capacity, room_before_slot, push_lands_in_slot, put_in_slot: the push guard lessThan len (size slots) is no at capacity and yes before a slot, and put at the length writes the slot.
• push_at_capacity, push_with_room: stated directly. A push at capacity is none and writes nothing; a push with a slot at its length is some of the buffer with the item in that slot and the length one more. Both are closed by simplifying with the prior theorems above as rewrite rules (pushResult is gone).
• below_truncated, get_truncated: a truncated length (bufTruncate) admits the indices below both lengths in bufGet.
• plus_assoc, window_of_window, window_count: a window of a window adds its offsets, and its count is minNat keep (minusNat count skip).

Every statement is total because the proof language has no hypothesis to assume (a prior theorem can be a rewrite rule, a premise cannot): facts about an index below a length are stated for a sum with a gap, or as a guard's result (guardGet, lessThan, both). The claim is the model's; that the runtime's Vec behaves as the model, and growth by reallocation (the declared effect allocation), are the differential's and rustc's evidence and are not claimed here (growth is modelled in H3b).

SP-26 (build)

Command and host: cargo test -p repo-conformance --test conformance -- conformance_sp_26, 4-core 15 GB container, pinned Lean 4.32.1: 43.9 s wall with the accepted module and five planted modules. The case lists the 17 laws itself (not read from the module) and requires each theorem to state the functions of its law; plants: a write that lands elsewhere (⊢ some head = some item), a write that drops a slot (⊢ size tail = size tail + 1), a reversed order of indices (⊢ some item = none), a truncation that keeps one too many (⊢ lessThan lower (minNat less oldLess + 1)), a push that adds two to the length (len := size front + 1 + 1, in push_with_room), a theorem renamed, a law without a theorem, a theorem about another function.

Calibration for H3b (cost)

The plan estimated 15 to 40 minutes of Lean per module family and called the first theorem the proof risk. Measured: seconds per module. What costs is the shape of the statements: a hypothesis cannot be assumed, so a fact about a valid state is stated as a guard or a gap, and unused simplify arguments are verification errors (the lists were pruned mechanically).

Identity

compiler/src is not in the embedded set the compiler-semantics ID hashes and compiler/expected covers only Main's closure, so this PR moves no ID and owes no relock or record. Register 448, SP-26 in the §31 table and the totals (xtask spec_links, repository.rs, README, SPEC).

---

Generated by Claude Code

[afflom]

Maintainer review of e7adb12 (read-only; validate-model 448 ids, validate-spec-links 448 rows, check-test-inventory 778 tests; conformance_sp_26 reproduced green in 25.3 s with Lean 4.32.1). The R3 chain, the counts, the plants, the [propext] pins audited by the verifier, the SPEC disclaimer of growth and of the runtime's behaviour, and the diff (nothing outside the expected trees, nothing of #255 or #259) all check out, and the eleven theorems are each a real property of the function they state. One round is needed, because the register statement, which is normative and byte-copied into §31, attributes two laws to theorems that do not state them:

Round

1. "the offsets of a window of a window add (plus_assoc)": the module defines no window. plus_assoc is associativity of the module's own plus, which no definition uses. The design says a slice is a (base, offset, length) view, and H4 needs it, so define the view now: a Window {base, offset, count} (or the names you prefer) with its sub-window, and state the law on it. If you would rather leave the view to H3b, drop the clause and the theorem from the statement and the laws list and say so in the PR body; the register may not claim a law of an object the module lacks.
2. "so that its push is refused and writes nothing (no_room_at_capacity)" and "the write lands in that slot (push_lands_in_slot)" claim bufPush behaviour, but no theorem mentions bufPush, bufGet or bufTruncate; the theorems are about lessThan, put and minNat, and the push consequence is by inspection of lines 157-159. Add the three Buf-level theorems (push at capacity is none; push with a slot at the length is some with the slot written and the length one more; bufGet (bufTruncate b k) at is the guarded read) and list them in LAWS. You measured a theorem in seconds, so this is cheap.
3. sameNat and pick are used by no definition or theorem (RustMemory.lex.tex:47-57, 76-85). Remove them, and from the term_cases list.

Nits (same push)

4. below_truncated's term_cases list names all twelve definitions while the goal uses three (both, lessThan, minNat); VERIFICATION says the lists were pruned. Prune it and re-verify.
5. rust_memory.rs:122-125 asserts "a theorem that states another function" by is_err() only; assert the diagnostic text. Lines 167-171 assert unsolved goals without the theorem's name; assert it per plant.
6. PR body: compiler/src is not in the embedded set the compiler-semantics ID hashes and compiler/expected covers only Main's closure, so this PR moves no ID and owes no relock or record; and Cells is a cons list, so "neither is a list" should go (the SPEC prose, which says the capacity is the number of slots, is right).
7. SPEC §17.17 prose: say that put beyond the slots is a no-op in the model (line 112) and is not the runtime's behaviour, which refuses. VERIFICATION: "three inductives … and the structure" names two inductives and one structure.
8. The base moved to eda82e1 (the #91 stage 4, H2: the runtime syntax validator is bootstrap source (BS-09) #259 round); no overlap, but merge it before the PR lands.

I will re-verify the round by reading the diff.

---

Generated by Claude Code

[afflom]

Maintainer, amending item 3 of the round: keep sameNat, which #264's RustLists uses (holds, same_is_no_gap, same_with_itself); only pick is unused and goes.

---

Generated by Claude Code

[afflom]

Maintainer: re-verification of the round at 36704c3 (read-only; cargo fmt --check, validate-model 448, validate-spec-links 448, check-test-inventory 778 green; conformance_sp_26 reproduced green in 23.7 s; the branch carries eda82e1 verbatim). Done: the Window view and subWindow with window_of_window stating the offset law on it; get_truncated exactly as asked; pick gone and sameNat kept; the term_cases pruning; the listing-plant assertion by text and the Lean plants by their goal text (the diagnostic carries position and goal, not the declaration name, so the goal is the discriminator; VERIFICATION records the theorem per plant); the PR body, SPEC and VERIFICATION corrections. One more push is needed, on one item:

1. push_at_capacity and push_with_room (RustMemory.lex.tex:497-511) state bufPush … = pushResult (lessThan …) …, where pushResult is bufPush's own body abstracted over the flag, so each is a definitional restatement and the reader still inspects pushResult's branches for the none and the some; the register and §17.17 ("refused and writes nothing", "lands in that slot with the length one more") attribute to them facts they do not state. The direct forms are provable: a prior theorem is a simplify rule in this proof language (ir/semantic.rs accepts any member of the proof rules, lowered to simp only; Gnaf.lex.tex uses orAssociative this way). State bufPush {slots := cells, len := plus (size cells) gap} item = none by simplify{definitions: [bufPush, no_room_at_capacity]} and bufPush {slots := append front (CCons old back), len := size front} item = some {slots := put … (size front) item, len := size front + 1} by simplify{definitions: [bufPush, room_before_slot]}; drop pushResult; adjust LAWS (add put to push_with_room's functions). Correct the PR body's and VERIFICATION's sentence that the language has no lemma-as-rewrite.

Two small things to carry in the same push:

2. subWindow's count is minNat keep (count win), not bounded by the parent's count minus skip, so a sub-window can reach past its parent (count 3, skip 2, keep 3 gives count 3). The register claims only the offset law, so nothing false is claimed, but H4 builds on this view: bound it (minNat keep (minus (count win) skip) with a truncated minus) and state the count law, or say in §17.17 that the sub-window's count is not bounded in this row.
3. No plant reaches the four theorems added this round. Add one Buf-level plant (for example bufTruncate's len := minNat keep len made len := keep, leaving get_truncated unsolved, or bufPush's len + 1 made len + 2, leaving push_with_room unsolved) and record it.

Whoever pushes (the author session or the owner), one push; I re-verify by reading.

---

Generated by Claude Code

[afflom]

Maintainer: re-verification of 87a4985 (read-only; cargo fmt --check, validate-model 448, validate-spec-links 448, check-test-inventory 778 green; conformance_sp_26 reproduced green in 26.8 s). push_at_capacity states none and push_with_room states some with the item in its slot and the length one more, both closed by the prior theorems as rules, with put_in_slot as the stated form of the slot write (stronger than the put … form I wrote, and right); pushResult is gone; the Buf plant is in and recorded; the sentence is corrected in all three places. One last one-line item, of the same kind as before:

• The clause "its count is bounded by what its parent has left after the skip (plus_assoc, window_of_window)" attributes the count bound to window_of_window, which states only the offset law; subWindow now computes the bound but no theorem states it. Add window_count: project (subWindow {base, offset, count} skip keep) count = minNat keep (minusNat count skip) by simplify{definitions: [subWindow]}, list it in LAWS with [subWindow, minNat, minusNat], and cite it in the clause (regenerating the §31 row, the scenario and CONFORMANCE.md). Or move the count sentence out of the theorem-attributed clause and say in §17.17 that no theorem states it. The first is one theorem and is the form the rule asks for.

After that the PR is accepted and waits for its landing after #254 and #255.

---

Generated by Claude Code

[afflom]

Maintainer: c353d25 is accepted (read-only re-verification; cargo fmt --check, validate-model 448, validate-spec-links 448, check-test-inventory 778 green; conformance_sp_26 reproduced green in 27 s). window_count states the sub-window's count on subWindow exactly as asked, sits in LAWS (17), and the clause now reads "the least of the count asked for and what its parent has left after the skip" with the three theorems cited. Seventeen theorems, every register law stated by its theorem on the named function.

Lands after #254 and #255 with its own regeneration.

---

Generated by Claude Code