W5-5 halting proof: Rocq plan

Target: Lemma halt: halts tm c0. in machines/1RB0RE_1RC0RA_0LD0RB_1LA0LE_1LC1LF_0LC---/1RB0RE_1RC0RA_0LD0RB_1LA0LE_1LC1LF_0LC---.v, passing tools/check_kill.sh --halt (compile cap 1800 s, ulimit -v 8000000, coqchk cap 600 s). Written 2026-10-13 after a design pass with small prototypes (section 6).

Verdict

Feasible with one machine-specific lemma family (the round) and one generic engine (a verified run-length macro simulator). The cycle model is never trusted: the checker re-derives every eat and every dirty carry by simulating the TM itself, and only the clean increments are taken from a proved closed form.

• No flip. The counter stays left of the head, the bell right of it. The busycoq call-stream machinery (segRLs/sideRLs) is not needed: a single call protocol and an induction over the digit list do the job.
• The proof is a checked certificate runner in the C2-552 shape (next, next_spec, Eqb.N_iter_until_spec, chunked run_ok/run_halt casts), but its next has three cases: 1. batch: n clean increments in closed form (proved round lemma + digit arithmetic); 2. oracle round: one round whose carry reaches a dirty digit, by the macro simulator; 3. eat: the whole eat (all sub-rounds) by the macro simulator.
• The macro simulator is generic (any TM, block rules found at run time by a window simulation), so the eat needs no parametric eat lemma: the bell lengths c ~ 1.2e6 are N counts that block rules cross in O(1).
• The opening is direct execution (solve_init, 288 steps); the endgame is not a separate phase: the halting round of cycle 611,577 is an oracle round whose simulation returns Halt.

The riskiest pieces were prototyped (section 6): the round lemma and the clean counter call compile with plain es; a Python mirror of the exact planned simulator + batch arithmetic, written from the TM table only, reproduces the model's words on all checked cycles and halts in cycle 611,577 after 7,434 complete rounds, as predicted.

1. Run facts the design rests on (all measured this stage)

Block rules the machine needs (all 3-cell, found by brute force over window contexts, shift_rule_R/L form with a fixed context d next to the head): - zigzag right over the bell: B, d = 10, 001 -> 001, 9 steps per block; - left sweep over the bell: C/D/E on the three rotations (010 -> 100, 001 -> 010, 100 -> 001), 3 steps; - counter carry left through trailing 2s: C, 100 -> 010, 5 steps; through a dirty run: C, 010 -> 100, 3 steps; - counter return right: C, d = 1, 100 -> 001, 9 steps. The simulator does not hard-code these; it tries contexts of 0..2 cells and keeps a rule when the window run exits forward in the same state with the context unchanged.

2. (a) Tape representation and the proved lemmas

The round-start form and the counter call (Prop side)

bellw b c = [1;0;1] ++ [0;0;1]^^b ++ [0;0;0;1] ++ [0;0;1]^^c
K X b c   = X <* [0] {{E}}> bellw b c *> 0inf          (X: the counter, a left stream, low cell first)
callw X X' = forall r, X <{{C}} 0 >> r -->* X' {{B}}> 0 >> r

A round starts with E1 -> 1LF, F0 -> 0LC: the head enters the counter's low cell in C. The counter call ends with the head back on the boundary cell (still 0) in B. Only then does the bell part run (zigzag, defect move, left sweep), and it ends with D0 -> 1LA, A1 -> 0RE on the boundary and the 101 cell, never reading X.

• bellpart X b c : X {{B}}> 0 >> bellw (S b) c *> 0inf -->+ K X b (S c) by es (the two bell shift rules are found automatically). Prototyped.
• round : callw X X' -> K X (S b) c -->+ K X' b (S c) (two steps, follow H, then bellpart). Prototyped.
• It holds for every b >= 0, c >= 0 (the rounds at b = 1, 2 are ordinary too: checked by direct simulation).

Clean digits and the call by induction

dg = Dm | D0 | D1 | D2        (001 = -1, 000 = 0, 101 = 1, 100 = 2; near-first cells [y;0;x])
cells ds                      (LSB first)
inc : list dg -> option (list dg)   (D2 passes the carry, the first other digit absorbs; None = overflow)

• Absorb lemmas absm, abs0, abs1: callw (dcell d *> H) (dcell (succ d) *> H), by es.
• Pass lemma pass2 : callw X X' -> callw ([0;0;1] *> X) ([1;0;0] *> X'): five steps, follow H, es. The return through a passed digit peeks one cell to the right (C0 -> 0LD, the "bounce" seen at the cuts); that cell is always the 0 of the boundary or of the next lower passed digit, which is exactly why callw is stated with 0 >> r on the right.
• callw_inc : inc ds = Some ds' -> callw (cells ds *> H) (cells ds' *> H) by list induction. Prototyped.
• H is arbitrary: the dirty high part of the word is never read when the carry is absorbed in the clean part.

Batch lemma (n rounds) and its arithmetic

• val ds = sum e_i 4^i in Z, maxv f = 2 (4^f - 1)/3.
• Pure lemmas:
• inc_val: inc ds = Some ds' gives val ds' = val ds + 1 and the same length;
• inc_some: val ds < maxv (length ds) gives inc ds = Some _;
• val_inj: equal length and equal value give equal lists (the digits -1..2 are distinct mod 4).
• rounds n : val ds + n <= maxv (length ds) -> length ds' = length ds -> val ds' = val ds + n -> n <= b -> K (cells ds *> H) b c -->* K (cells ds' *> H) (b - n) (c + n), by induction on n (nat, symbolic only).
• Leading zeros: [0;0;0]^^k *> 0inf = 0inf (from const_unfold), so a fully clean word is padded with D0 digits until maxv covers n; the result is trimmed by the same lemma.

Checker data (computed side)

krec = { w : list code (3-cell codes, LSB first, 8 values); b : N; c : N }
denote k = K (wcells (w k) *> 0inf) (N.to_nat (b k)) (N.to_nat (c k))

• split w = (D, H): D = the longest clean prefix (as list dg), H = the rest (cells).
• The batch computes D' by balanced base-4 addition in Z and checks length, val D' = val D + n, val D + n <= maxv, n <= b; the proposal n (untrusted) is b when H = [] (whole word clean, padded) and min b (maxv f - val D) otherwise. n = 0 falls through to the oracle round.
• Never compute N.to_nat on b or c in the checker: they reach 1.2e6 (unary nat).

The macro simulator (generic, used for oracle rounds, eats and the halt)

sd  = list (list Sym * N)          runs (block, count), near-first, then 0inf
cfg = Q * sd * sd * dn             dn = DL | DR: the head is on the first cell of L or of R

• pop (with rotation: popping the first cell z of (z::u)^n leaves (u++[z])^(n-1) ++ u), push (merges equal blocks; three singletons equal to the next run's block are folded into it), take k.
• One macro step: if the run under the head has n >= 2, try a block rule: take k = 0..2 context cells d from the other side, run wsim (a fuel-64 window simulator with the moves mirrored for DL) on d ++ block; if it exits forward in the same state with d unchanged, cross the whole run (shift_rule_R/shift_rule_L with that d). Otherwise make one TM step by calling tm itself.
• Soundness lemmas: pop_spec, push_spec, take_spec (stream equalities via lpow_add, lpow_rotate_list, const_unfold), wsim_spec (induction on fuel, step_left/step_right), try_rule_spec (wsim_spec + shift_rule_R/L), mstep_spec (-->* or halts), isK_spec (a K-form parser over runs: 101, a run-aware count of 001 blocks, 0001, 001 blocks, all-zero tail), urun_spec (an early-exit recursion on positive fuel: returns Kf, Halt or Fuel).

• The window simulator is the only place tm is evaluated besides single steps; nothing in it is machine-specific, so a wrong rule simply never fires.

• Alternative engine considered: verify/ES_v3.v (the verified symbolic executor behind es': vside with named exponents, rotation, try_sr shift rules over bounded windows, vconfig_es_spec, vconfig_es_halt_spec). It would save the simulator soundness proofs, and its named exponents would even make each eat hold for all c. Not chosen as the default: it runs to a given target and compares configurations syntactically after rotation, so every eat and oracle round would need its exact normal-form target proposed from outside, and its string-named exponents and per-step window searches are untested at 2.7e8 steps. Time-box half an hour at the start of stage 2: if vconfig_er_sr can be driven to the next K-form with a proposed target that the generator reproduces exactly, use it and skip the own soundness proofs.

3. (b) Executing the 611,577 cycles inside Coq

next k := if b k = 0 then eat k                          (urun from kcfg k to the first K-form with b >= 1)
          else match batch k with Some k' => inl k'
               | None => oracle k end                     (urun from kcfg k to the next K-form)

• eat/oracle return inr tt on Halt (then halts tm (denote k) by urun_spec).
• A failed parse or fuel-out returns inl k unchanged (sound, and the fuel count exposes it).
• eat stops at the first K-form with b >= 1 (not the model's b >= 3): every K-form satisfies the round lemma, so any stopping point is sound. Only the first cycles (c below the model's bell size 40) decompose differently from fastabs2; the TM trajectory is the same.
• next_spec: denote k -->* denote k' or halts tm (denote k); check_spec and the chunk lemmas are copied from C2-552 (run T k = inl k' -> -->*, run T k = inr tt -> halts).
• About 5.4M iterations and 2.7e8 macro steps in all. Chunks of 4,000 iterations (about 2e5 macro steps): about 1,350 chunks.
• The chunk boundary states are literals written by a generator, not Eval vm_compute definitions: the kernel then runs each chunk once (at the vm_cast_no_check Qed), not twice.
• Generator and mirror: OCaml extraction of the same next (Extraction of the checker module), run natively; it prints the chunk states as Coq terms and the exact fuel. This also replaces a hand-written mirror (the Python mirror in rocq/mirror/macro.py remains the design reference).
• Optional speed-up if the VM time is too high: run oracle rounds as round + a counter-only simulation (an abstract right tail after the boundary cell), which drops the 38 bell macro steps per oracle round (about 8e7 of the 2.7e8).

4. (c) Opening and endgame

• Opening: init : c0 -->* denote (krec [] 0 2) by solve_init (288 steps; K0('', 2) is 0inf <* [0] {{E}}> bellw 0 2 *> 0inf).
• Endgame: none separate. Cycle 611,577 is eat, then batches and oracle rounds; after 7,434 complete rounds the next oracle round's simulation hits F1 = --- and urun returns Halt (the Python mirror reproduces exactly this). The last chunk is run T k_last = inr tt.
• The 108,456,557,258 direct steps of the last cycle are never executed one by one; the bell crossings are block rules with N counts.
• Final theorem: Lemma halt: halts tm c0. by halts_evstep over init and the chunk lemmas, as in C2-552. No flip, so no functional_extensionality_dep is expected (Print Assumptions should be empty).

5. (d) Compile-time and memory

• Lemma part: the round, digit and simulator lemmas are small (es runs a few hundred steps); budget under 1 minute.
• The run: measured 2.2 µs per macro step in the VM (section 6), so about 600 s for 2.7e8 macro steps. With literal chunk states the kernel evaluates the run once. Do not also Eval vm_compute the chunk states in the kill file (that would double it to about 20 minutes, too close to the 1800 s cap).
• Native casts have a per-call compilation overhead: the prototype's one native_compute took 1.1 s wall for 0.32 s of run. With about 1,350 casts that is 15-20 minutes of overhead, so use vm_cast_no_check. If the VM is too slow, use native casts in a few large chunks, but larger chunks raise the coqchk memory risk.
• coqchk will hit its 600 s cap (a warning under policy A). It re-checks casts by lazy kernel conversion, far slower than the VM, so it only gets through the first chunks.
• coqchk out-of-memory is a FAIL: kernel conversion memory grows with the length of one cast (C2-552: OOM at 110k iterations in one cast, fine at 5k; W4-3: 3.3 GB at 500k simulator steps per cast). Keep each cast at about 2e5 macro steps. Before the first full check_kill, measure coqchk RSS on a 3-chunk file.
• Memory in coqc: the VM is small for this data (states under 1 KB; words up to about 130 digits, N numbers under 2^21, Z values up to about 2^260).

6. Prototype results (this stage)

Files: rocq/proto/round.v, rocq/proto/perf.v (compiled from a temp dir with the standard flags, ulimit -v 8000000; logs rocq/proto/*_out.txt), rocq/mirror/ (Python mirror and C instrumentation).

Extrapolated run cost: 2.7e8 macro steps at 2.2 µs is about 10 minutes of vm_compute (about 4 with native_compute), plus 2.7M batches of digit arithmetic. That leaves the 1800 s compile cap a 3x margin; the counter-only oracle variant (section 3) would cut it by about 30%.

Not prototyped: the simulator soundness proofs (routine but the largest piece), the batch arithmetic lemmas, chunking, and coqchk memory per chunk.

7. Work order (stages are non-blocking, about 2 h each)

1. proof.md (CLAUDE.md: before the .v): K-form, round, clean increments, the checked-simulation argument for eats and dirty carries, the final halting round. Short, since the eat needs no closed form.
2. Simulator + soundness (rocq/dev/macro.v): pop/push/take/wsim/try_rule/mstep/isK/urun and their specs. Test on the opening and on one real eat (urun result equals the extraction's).
3. Batch (rocq/dev/batch.v): val, inc_val, inc_some, val_inj, rounds, padding/trim lemmas, batch.
4. Checker, extraction, chunk generator: next, next_spec, run_ok, run_halt; extract, run all cycles, write k_i literals; smoke-test a prefix (c0 -->* denote k_100) under check_kill-like flags.
5. Full file and check_kill --halt; then status.json, STATUS.md and the Eqv_v2 TM291 partner note.

8. Risks, most serious first

1. Total VM time: about 600 s estimated (2.7e8 macro steps from the mirror times 2.2 µs measured in Coq). The margin to the 1800 s cap is about 3x; a slower real next (soundness-friendly data structures) eats into it. Mitigations: the counter-only oracle variant (-30%), native casts in a few large chunks, or check_kill --timeout, which needs Dennis's OK because the task names the default command.
2. coqchk OOM on the first chunks: measure RSS early; shrink the chunks if needed (timeout is fine).
3. Simulator soundness proofs: rotation, merging and the run-aware K parser are the fiddly stream equalities. Keep pop/push minimal and prove each against sdn with list lemmas only.
4. Unhandled shapes make urun run long but never unsound. A fuel-out shows up in the extraction run before any Coq compile.
5. Model trust is not a risk to soundness: the cycle model only supplies the batch sizes. If the model were wrong, the extraction run would not halt and nothing would be claimed.