[david415]

this reply written by agent mycroft@luna:

The Lean member follows katzenqt's (katzenpost/katzenqt#188). Its traces and wire vectors are regenerated from that branch.

Each change is driven by vectors. katzenqt's Python member generates the traces and wire vectors; cryptlib's Lean model must replay them. Every change was first shown to make the old Lean model disagree, then made in both.

1. Numbering stays inside the roster. A member numbered past roster index 255, which a one-byte index can't carry: Lean truncated it, and Python's encoder raised. Numbering now stops at 255, an Introduction made without room assigns no number, and room tells a client whether one more member fits. katzenqt refuses an induction when it doesn't (acks.RosterFull).
2. A removed member's placeholder is not a known key. retire renamed the member's key to its placeholder (retired + its place, exactly a prefix long), so a Numbers prefix could name it, and an acknowledgement at that index was recorded for a stream that doesn't exist. The key is now dropped.
3. What a member remembers is bounded. received grew for good although only a received-content expiry policy uses it, which the app never sets. It is now kept only while such a policy is set. A scan's tried grew with every acknowledgement it ever looked for; it now keeps only boxes still heard and still ahead. A scan no longer walks to acknowledged boxes behind it, which a walk can never reach.
4. A member whose client writes writes nothing itself. A member driven by a client that writes for it could still, if handed an event, write from its own pool at an index the client also hands out: the same box written twice with different bytes. The new allocates flag is cleared by the client's first write call (compose, written, begin_induction, introduce_now); from then on the member writes and derives nothing itself.
5. One membership hash rule. The model and the simulator put the zero sentinel on control messages and Introductions, while the app overwrote it with its own view. The member now stamps its own view when it composes: itself and every member it reads, less the newcomer for an Introduction. The hash is kept with the message so that a backfill rewrite is byte-identical. The app uses the stamp, and checks that it equals its own view. A sentinel on the wire reads as no hash.
6. Every Numbers field reads back as written. Two members introduced together whose keys share an 8-byte prefix made a Numbers field that every receiver refuses whole. A control message now names each prefix once, and the other member waits for the next control message.

New edge traces (edge-*.jsonl, from katzenqt's tests/groupchat_edges.py) drive members through each case the scenario language can't reach: a nearly full roster, a retired prefix, bounded state, a client that writes, and shared prefixes.

New theorems, all resting on Lean's own axioms only:

• numbering bounds: controlOf_lt, introductionOf_lt
• every composed Numbers field reads back as written: controlOf_wf, controlOf_numbers_roundtrip, introductionOf_numbers_roundtrip
• removing a member: retire_forgets, retire_keys
• bounded memory: deliver_received, onEpoch_received, scan_tried, scan_tried_nodup, scan_tried_length
• a client that writes: flush_client, clientWrites_allocates
• the hash rule: controlOf_hash, introductionOf_hash

introduction_index and introduction_index_pending now assume the roster has room.

scripts/verify-vectors.sh now regenerates the group chat wire vectors and traces from a katzenqt checkout and compares them, not only the scenario files. Three tactics that did nothing are dropped.

Checks: replay 20 traces, 647 calls, no difference; 14 of 14 scenarios; 36 wire vectors; 51 Acks vectors; make axioms clean. katzenqt's random traces (123 traces, 20594 calls) replay with no difference.