[afflom]

Stacked on #262 (claude/issue-91-stage4-heap-memory at c353d2536, merged in); draft. Second of the two memory PRs of the heap half (H3b).

What

RustLists (compiler/src/RustLists.lex.tex, language 1.2, on RustMemory's buffers and the calculus's values) models the runtime's List<T> (Repr::{Nil, Run{buffer: Rc<Vec>, len}, Cell(Rc<Node>)}) as a handle: the items of the cells in front (spine) and a terminal, the empty list or a run, the first more+1 slots of the buffer at an address of a store, a chain of RustMemory::Buf. A handle reads back as the calculus's list (absHandle). Reference counting is derived, not stored: holds is the sameness of the terminal's address and the buffer's, aloneOn (no other handle holds it) is the answer of Rc::get_mut, and consWorld consults it. 53 theorems, all [propext] except the reflexivities, no definition observing an axiom.

• In-place cons: one law, and its lemmas. cons_in_place: for the first buffer of a store with room after the run and any length at least the run's, with no other handle, the cons through consWorld reads as the item before the old list. It is closed by simplifying with min_keeps_run, room_before_slot and put_run_abs as rewrite rules. The pieces it is built from are stated apart: consIn truncates the buffer to the run (bufTruncate) and pushes with RustMemory.bufPush, keeping the buffer when the push is refused; the room guard is F = lessThan m (size slots), m = minNat n len; walk_cons (the read back is a pick by F), push_run_abs, full_is_capacity (a refusal is F failing; the outcome is Full), min_keeps_run and truncate_keeps_run (on bufTruncate: its length is the run when the buffer is at least as long), inplace_view and cons_view (the handle, with the in-place write chosen by aloneOn).
• Growth (the declared effect allocation). growBuf appends slots: grow_run_abs/append_run_abs (the slots read as they did), room_after_growth/grown_has_room (the grown buffer has room).
• Allocation. The first cons onto nil writes a buffer of length one and capacity sixteen (the item and fifteen blank slots behind it, as the oracle reserves; alloc_capacity, alloc_length) at storeLen and no other address (walk_alloc, cons_alloc_view, cons_alloc_store), and the buffers before it are read as they were (alloc_frame).
• Cell and shared cons write no buffer. cons_cell_view/cons_cell_store, cons_shared_view/cons_shared_store, and cons_held_store on consWorld for a holder among the other handles (store after = store before).
• Uncons. run_uncons_abs, run_last_abs, walk_uncons, walk_uncons_last, uncons_cell_*, uncons_run_*, uncons_last_*.
• Frame. cons_frame, inplace_frame (phrased with holds).
• Holders, both ways. same_with_itself, holder_on_own_buffer, holder_without_run; a handle on another address holds nothing (apart_above, apart_below, holds_apart_above, holds_apart_below); own_blocks, holder_blocks (a holder blocks the write), others_allow_above/below, holder_elsewhere_above/below.
• Release. release_ends, release_one_short, release_needs_fuel (releaseLoop n (unshared (n+1)) is spent), release_one_cell.

Dropped from the first draft: the literal step tables and their two theorems, gapOf/gapPick/same_is_no_gap (sameNat is the single address test), takeN/snoc, the free fresh and unique parameters.

The claim is the model's, and the register says so: that Rc/Vec/List behave as the model, that the derived count is the Rc's, and that the Drop loop is the release loop are the differential's and rustc's evidence (H4's), never these theorems.

SP-27 (build)

cargo test -p repo-conformance --test conformance -- conformance_sp_27, 4-core 15 GB container, pinned Lean 4.32.1: 83.9 s wall (module + ten planted modules). Each plant is asserted by the theorems Lean refuses and the diagnostic: wrong slot (walk_cons, cons_in_place), wrong uncons slot (walk_uncons, walk_uncons_last), shared run written in place (cons_view, cons_held_store), a write reaching the next buffer (cons_frame), a release counted one short (release_ends), growth dropping the slots (grow_run_abs, grown_has_room), a fresh buffer not at storeLen (cons_alloc_view), a fresh buffer a slot short of sixteen (alloc_capacity), an inverted refusal (full_is_capacity, cons_in_place), a holder that does not block (own_blocks); plus the listing refusals.

Identity

New module in the compiler project. compiler/src is not in the embedded set the compiler-semantics ID hashes and compiler/expected covers only Main's closure, so no ID moves, no record regenerates, and no relock is owed. Register 449, SP-27 in §31 and the totals.

---

🤖 Generated with Claude Code

https://claude.ai/code/session_018vK7Tm6xHF5etAwKM6r9HG

[afflom]

Maintainer review of b8b46a1 (read-only; validate-model 449, validate-spec-links 449, check-test-inventory 779, cargo fmt --check green; conformance_sp_27 reproduced green in 35.8 s; RustLists.lex.tex canonical after a scratch relock). The R3 chain, counts, plants, pins, diff and stack hygiene are clean, walk_cons, walk_uncons, walk_frame and the abstraction pairs are real properties, and the cons and uncons cases correspond to std.rs.txt at the slot level. One round is needed, for the same reason as #262 and larger: the register attributes laws to theorems that do not state them, and the model drops the capacity constraint the design fixes. From here on, write the theorem first and the register clause from its statement, never the other way round.

Round

1. "writes no buffer" (cons_cell_abs, cons_shared_abs) has no theorem: both state only the abstraction. Add cons_cell_store and cons_shared_store stating that the store after the cons is the store before, list them in LAWS, or drop the clause.
2. consSteps and unconsSteps (897-958) are literal tables that nothing in consWorld or unconsHandle produces, so *_steps_bounded bound a table, not the operations. Make the operations return a step count the theorems bound, or drop the clause, the tables and the two theorems from the statement and §17.17.
3. aloneOn (877-887) is used by no definition or theorem, yet the prose (5905-5906) says it is consWorld's unique argument. Pass it in (with a frame theorem for the other handles) or remove it and reword.
4. The capacity constraint is not modelled and not declared: the store holds RustMemory::Cells, not Buf; takeN and snoc change the slot count on every push with no allocation effect and no refusal, where the oracle keeps capacity and grows under allocation; fresh is any address, so a first cons can overwrite a held buffer. The design fixes a Vec as capacity plus length with growth only under allocation, and H4's differential for cons needs that split, so model it now rather than declare it away: the store holds Buf, the in-place cons goes through bufPush (refused at capacity; growth is a separate step under the effect, with its own theorem), and fresh is the store's length (the allocator's one-line definition) rather than a free parameter. If you judge this too large for this PR, say so with the cost and I will decide, but do not land a prose disclaimer in its place.
5. Stack: holds, same_is_no_gap and same_with_itself use RustMemory::sameNat, which my #91 stage 4, H3a: the memory model of a runtime buffer, kernel-checked (SP-26) #262 round asked to remove as unused. #91 stage 4, H3a: the memory model of a runtime buffer, kernel-checked (SP-26) #262 keeps sameNat (I am amending that round now); pick still goes.
6. "needs that many" (release_needs_fuel) states fuel 0 on one cell. State it for an unshared chain of n (releaseLoop n (unshared (n+1)) = spent) or weaken the clause.

Nits (same push)

7. "a cons and an uncon" in the statement, three byte-copies.
8. rust_lists.rs:144-147 and 194-198: assert the diagnostic text for the "another function" refusal and the failing theorem's name per plant; the unsolved goals || Type mismatch disjunction should say which plant yields which.
9. "exactly when": state the converse on holds itself, so the iff is about the named function.
10. PR body: compiler/src is not embedded, so no record regenerates and no relock is owed (as on #91 stage 4, H3a: the memory model of a runtime buffer, kernel-checked (SP-26) #262).
11. VERIFICATION plant 5 is in lengthOf, not the release; say "a chain counted one short".

Observations for H4, no action here: no Str/Bytes buffers, no window view yet (#262's round adds it), no operation creates a second handle so no theorem relates the derived count to clone or to uncons on a shared list, and the release loop is over flags rather than a chain in the store.

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

---

Generated by Claude Code

[afflom]

Maintainer: re-verification of the round at 6574d14 (read-only; cargo fmt --check, validate-model 449, validate-spec-links 449, check-test-inventory 779 green; conformance_sp_27 reproduced green in 59.9 s; the statement byte-equal in its three places; the net diff against #262's 87a4985 touches only SP-27's files and the count). The substantive asks are done: the store holds Buf, the in-place cons goes through bufTruncate and bufPush with Full leaving the store untouched, growBuf is a separate step with grow_run_abs and grown_has_room, fresh is storeLen with walk_alloc and alloc_frame, aloneOn is wired into consWorld with the holds-phrased frames, the steps are gone, release_needs_fuel is on unshared (n+1), and the nine plants are asserted by kind, goal and the exact refused set. One more small push, on four points of the same rule (the theorem states the law on the named operation):

1. "writes no buffer" for the shared cons: cons_shared_store is stated on the helper sharedCons, not on consWorld. Add cons_held_store on consWorld for a holder among the others (by simplify over consWorld, holder_blocks, sharedCons, storeOf) and name it in the clause.
2. truncate_keeps_run states minNat length (plus length gap) = length, about minNat and plus, while the clause says "the truncation keeps the run of a buffer at least as long". Restate it on bufTruncate (the truncated buffer's len is length) and add bufTruncate to its LAWS row.
3. "holds a buffer exactly when its run is on the buffer's address": the converse is stated only on sameNat/notAlone/aloneOn, never on holds. Add the holds … (TRun (other address) …) = no pair, or drop "exactly".
4. allocBuf makes a buffer of capacity 1 where the oracle reserves 16 (Vec::with_capacity(16)), so in the model every second cons on a fresh buffer is Full; nothing declares this. Allocate the oracle's capacity (blank slots behind the item, length 1) so H4's cons differential meets the same shape, and state the capacity in the first-cons clause.

Carry in the same push: the single valid-state theorem I asked for separately (the in-place cons for a buffer with room, encoded as slots := append front (CCons x back), reads as item :: the run, closed with walk_cons, push_run_abs and a one-induction lemma relating runWalk to absRun as simplify rules), named in the in-place clause with the chain as its lemmas; and "uncon" as a noun ("the uncon of a cell", "an uncon that reads the wrong slot") in the statement's three byte-copies and the §17.17 prose, which is "uncons". Observation, no action: uncons_run_taken and uncons_last_taken are reflexivities carrying no content beyond the definition; fine as the _taken half of the abstraction pairs.

---

Generated by Claude Code

[afflom]

Maintainer: e5383bb is accepted (read-only re-verification; cargo fmt --check, validate-model 449, validate-spec-links 449, check-test-inventory 779 green; conformance_sp_27 reproduced green in 62 s). All six items are as asked: cons_held_store on consWorld, truncate_keeps_run on bufTruncate with min_keeps_run as the arithmetic, the holds converse in both directions on holds, allocBuf of length one and capacity sixteen with its plant, cons_in_place closed by min_keeps_run, room_before_slot and put_run_abs as rules, and "uncons" throughout. The model's first cons now matches the oracle's with_capacity(16): conses two to sixteen on a fresh buffer are in place and the seventeenth is Full, growth being the separate step. Fifty-three theorems, ten plants each asserted by kind, goal and exact refused set.

Two wording corrections to ride the next push on this branch (no theorem, gate or plant changes): the in-place clause says cons_in_place is "closed from the lemmas … (push_run_abs, put_run_abs, walk_cons, inplace_view, cons_view)", but its rules are min_keeps_run, room_before_slot and put_run_abs; name those as what it is closed from and keep the other four as the separate statements of the pieces (three byte-copies and CONFORMANCE.md). VERIFICATION's first plant refuses walk_cons and cons_in_place, not walk_cons alone.

Lands after #254, #255, #259 and #262 with its own regeneration.

---

Generated by Claude Code