/machines/1RB0RD_1LC0RA_---1RD_1RA1LE_1RC0LF_1LE0LB/rocq-plan.md · raw

C2-552 halting proof: Rocq plan

Target: Lemma halt: halts tm c0. in machines/1RB0RD_1LC0RA_---1RD_1RA1LE_1RC0LF_1LE0LB/1RB0RD_1LC0RA_---1RD_1RA1LE_1RC0LF_1LE0LB.v, passing tools/check_kill.sh --halt. Written 2026-10-12, after a design pass with small prototypes.

Verdict

Feasible, with a known architecture and no new framework. The proof is a checked certificate runner in the style of verify/Sk1Machines.v (TM91/TM94), run in the mirrored machine tmf := Eval compute in (flip tm). In the mirror the counter sits to the right of the head, which is the orientation busycoq's call-stream framework (segRLs/sideRLs in Individual.v, sideRLs_halt in LongitudinalHalt.v) is written for.

A Coq-executable next : cfg -> cfg + unit works on a unit-list configuration with N fields.
Each next either applies a binary-counter batch of d increments (Sk1 batch pattern) or runs one structural increment (TM91 call/outcome pattern), and returns inr tt when the call halts.
Soundness: next_spec (each step is -[tmf]->*, or the config halts) and check_spec via Eqb.N_iter_until_spec, copied from Sk1Auto.check_spec.
The run itself is one native_check_eq of check FUEL = true, with FUEL about 1.2e5 iterations.

The riskiest unknowns were checked and hold: 1. Every unit boundary is crossed by a uniform call protocol. 2. solve_seg/es prove the parametric window lemmas in the flipped machine. 3. The root, batch, halting and flip glue compose. 4. native_compute runs 150k checker-sized iterations in seconds.

1. Orientation and the call protocol (the key fact)

The cut of a unit is the left edge (in tm coordinates) of its boundary block 1^(3g+2). This covers plain 11 and glued 1^5, 1^8, … alike. The tail's boundary has a cut too.

Every increment is one call from the root (the tail and the head) into the units to its left, so the calls nest the way a binary counter carries: - In: the head crosses a cut leftward exactly once, in state B, onto a cell holding 0. - Out: it crosses back rightward exactly once, in state D, onto a cell holding 0 (the boundary's first cell, zeroed on the way in).

Evidence: - Empirical (rocq/tools/cuts.py, log rocq/tools/cuts_3e7.txt): from the blank tape to 3·10⁷ steps, about 4.5k increments and 33,739 cut observations. Every crossed cut follows exactly [(L,B,0),(R,D,0)], with 0 deviations. This covers plain and glued boundaries b2 … b41 and the resets, glue, unglue, absorb and edge events of that window. - Inside a unit the same holds at the left edge of every passive wall or stack 1^(3j+1): in F onto 0, out D onto 0 (rocq/tools/walls_cross.py). So passive chains can be cut there as well, giving per-block induction. - Proved in Coq (below): with hin := (B,[]), hout := (D,[]) and h := [(hin,hout)], the touch lemmas are plain segRL/segRLs facts. Since the protocol is a single call type, every forwarded stream is h^^p. TM91 needed two call types, h and h'; this machine needs only one.

Words are lists in root-first order (nearest the head first, i.e. tm right-to-left). A segRR output is far-first, which is busycoq's convention for l <* w.

2. Prototype results (compiled, Coq 8.20.1, all < 2 s, all `Closed under the global context` except the flip transfer)

Files are in rocq/proto/. Compile them with the standard flags from a temp dir.

file	content	result
`root_k1_batch.v`	`root t X := 0inf <{{A}} ([0;1]^^t ++ [0;1;1]) > X`; `root_in`, `root_out`, `root_step` (one call via `sideRL tmf hin hout`), `root_steps` (d calls, induction: `root t X --> root (d+t) X'`); k=1 digit words `w1 a c` (lead 1111, x=2a+1, y=2c+1) and `w0 a c` (lead 00, x=2a, y=2c); `stop1 : segRL tmf hin hout (w0 (S a) (S c)) (w1 a c)`; `pass1 : segRLs tmf h h (w1 a c) (w0 (S (S a)) c)` (via `segRLs_lrcons` of `pass1_RR`/`pass1_LL`); `halt0 : halts tmf (l {{B}}> w0 a 0 > r)`; `pair1`, `pairs1 n : segRLs tmf (h^^(n2)) (h^^n) (w0 (S a) (n+c)) (w0 (S (n+a)) c)` (the Sk1 `total_spec` pattern)	all Qed
`blocks.v`	passive block `blk m j := [0] ++ [1;0]^^m ++ stack j` (odd gap 2m+1, stack `1^(3j+1)`); `blockRR : segRR tmf (F,[]) (F,[]) (blk m j) ([0;1] ++ [0;1;1]^^j ++ [0;1]^^m)`, `blockLL : segLL tmf (D,[]) (D,[]) (mid (S m) j) ([0] ++ [1;0]^^m ++ stack j ++ [0;1])`, parametric in m and j	Qed by `solve_seg`
`halt_flip.v`	`root_halt : sideRLs_halt tmf [(hin,hout)] X -> halts tmf (root t X)` (LongitudinalHalt); a toy halting root; `flipc0 : halts tmf c0 -> halts tm c0` by `apply flip_halts_iff; exact H` (`tmf` ≡ `flip tm`, `flip_conf c0` ≡ `c0` by conversion)	Qed. Adds only `functional_extensionality_dep`, which is in the baseline
`perf.v`	synthetic checker-shaped loop: 150k `N_iter_until` iterations over 25 records with 70–75-bit `N` fields, a 1300-element list rebuilt every 2nd iteration	`native_check_eq`: 11–16 s wall for the whole file, 450 MB RSS. `vm_check_eq`: 59 s. Negative control (`fuel` too small) fails as it should

Tactic notes are logged in atlas/rocq-notes.md under "C2-552 … Rocq design".

3. (a) Tape representation and the rule lemmas

Checker data (all numbers `N`, pair counts so parity is structural)

wall := Z (00) | O j (1^(3j+1), j ≥ 1); a boundary is g : N (1^(3g+2)).
unit := { g; x; lead : option bool (None = leadless); m1; mids : list (wall*N); y }.
mids holds the interior passives P₁…P_{k−1} with their gaps, in tm order.
A batch touches only x, lead, m1 and y, so it is O(1) per unit.
Glue drops the last passive; unglue prepends at the lead.
k=1 has no m1/mids. Empty = [y].
cfg := { e : N (edge 1^e); u0; us : list unit (LSB first); tail : TailT t | TailG t (glued 1^5) | NoTail }.
Sizes on the real run (fast.py rerun, this session): up to 25 units, k up to 1,339, about 2.9k wall tokens in the whole configuration, numbers up to 73 bits.

Words (Prop side only; never computed on the big data)

Gaps by phase class, as root-first pair counts:
between two 1-walls (odd): [0] ++ [1;0]^^c;
between a 1-wall and a 00 lead on the far side: [0;1]^^c;
after a 00 lead (x, or m1 of a 00-lead unit): [1;0]^^a.
Walls:
00: [0;0];
stack: [1] ++ [1;1;1]^^j;
boundary: [1;1] ++ [1;1;1]^^g.
Unit word, root-first: y-block, chain blocks (gap ++ far wall), lead block (m1 ++ M), x-block (x ++ boundary). The blk lemmas above are exactly the chain-block case.
side us u0 e := unit words ++ U0 word ++ 1^e *> 0inf; denote cfg := root t (side …) or the reset variants.

Mapping of every rules3.py case to lemmas

pairs = Sk1-style n-touch induction. Every lemma is parametric (lpow on nat; N.to_nat at the interface).

rules3 case	lemma(s), flipped machine	status
tail `t += 2` per increment	`root_in`, `root_out`, `root_step`, `root_steps`	proved
M stop, k=1 (lead 00, any boundary: leave the boundary in `r`)	`stop1`	proved
M pass, k=1 (lead 1111, boundary 11), including y 1→0 (the fuel-out shape `[x,00,0]`)	`pass1` (c arbitrary, c=0 allowed)	proved
call into `[x,00,0]` halts (F reads 1 after 00)	`halt0` + `sideRLs_halt` + `segRLs_sideRLs_halt_concat` + `root_halt`	proved
M touches k ≥ 2	`yblockRR/LL` (y-gap + last passive, entered in B) ∘ `chainRR/LL` (induction over `mids` from `blockRR/LL`) ∘ `leadRR/LL` (pass: m1, 1111, x, 11, out in B) or `lead_stop` (00 turnaround, F→D); composition lemmas `RR∘RL∘LL = RL` and `RR∘(call)∘LL = segRLs_lrcons`	blocks proved, rest to do
leadless unit (all walls +2)	`yblock` ∘ `chain` ∘ `xblockRR/LL` (first wall passive)	to do
empty unit	`emptyRR/LL` on `[y, 11]`	to do
glue (last gap 1→−1) for digit, leadless, U0, and right after an unglue	`yglueRR/LL`: the y-block with c=0. The last stack shifts 2 cells toward the root and ends 1 cell past the cut (captured: `01111 → 11101`). Then a re-cut equality that merges it into the root-side boundary	to do
unglue g=1 and g≥2 (boundary `1^(3g+2)`, lead 1111, a pass): `[x,1111,…] → [2,00,x+1,1111,…]` / `[2,00,0,1^(3g−2),x,1111,…]`	`unglue1RR/LL`, `ungluegRR/LL` (stack shift over `[1;1;1]^^g`; g up to 6·10¹⁴, so symbolic)	to do
U0-1111 (U0 digit, lead moves like a passive, edge e≡1)	U0 side lemma + `edge1`	to do
U0-stop	the stop lemmas (the turn never reaches the edge)	reuse
edge e≡0 (overflow: e += 3, U0's first gap −2) with U0 empty / leadless	`edge0_empty`, `edge0_leadless` (`sideRL`); `edge0s` by induction for m overflows (`sideRLs (h^^m)`)	to do
edge e≡1 fossilization (old edge becomes U0's first stack, new `111` two cells out)	`edge1` (`sideRL`, uses `0inf` cells)	to do
absorb (empty U0's gap −1, so e += r−1)	`absorb` (`sideRL`) + re-cut	to do
reset first half (tail boundary `1^5`) `… 1^5 [t] → … 11 [2,00,t+2]`, call continues	`root_reset1 : sideRL tmf hin hout X X' -> rootG t X -->+ rootN (digit 2 00 (t+2)) X'`	to do
reset second half (no tail) `… [2,00,t+2] → … [1,1111,t] 11 [1]`	`root_reset2` (no side call: the last unit stops the carry)	to do

About 30 lemma families in all. - Words for each family come from the capture tools in rocq/tools/ (block.py L R, seg.py, rootcap.py). - They also come from solve_seg itself: when the stated output is wrong, the error message prints the computed word. That is how blockRR's middle word was found.

4. (b) Running about 54k structural events and the batches inside Coq

The task brief estimated about 60k structural events. Rerunning fast.py this session gives the exact counts: - 53,973 structural single increments to the fuel-out at increment 11,631,266,794,472,450,654,090. - Events among them: - glue 28,314, unglue 28,234; - overflow-edge0 48,714, leadless-U0 48,654; - reset1 81, reset2 82; - absorb, edge1, U0-stop, U0-1111 and empty: 60 each.

Batch (d increments, no structural event)

Per-unit lemma unit_batch: segRLs tmf (h^^n) (h^^p) (uword u) (uword u'), where
p = (n + bit)/2;
u' is the closed form: x += 3p − (n−p), bit' = (bit+n) mod 2, m1 += n, y −= n (k=1) or 2n (k≥2).
It is proved by induction on n from the single-touch lemmas with segRLs_trans (as pairs1), then moved to N with N2Nat plus lia (as Sk1 totalN_rule).
Guards are exactly the lemma side conditions: stop needs a ≥ 1 and c ≥ 1; fuel stays ≥ 1; glued-boundary units take at most one stop; leadless and empty units forward n.
Unit list batch n us : option (N * list unit): recursion from the LSB (Sk1 batch / TM91 batch_correct); batch_spec follows by segRLs_concat.
U0 and edge: edge0s gives sideRLs tmf (h^^m) …. Then segRLs_sideRLs_concat and root_steps finish the batch.
Proposal d: fast.py's event_touch/first_inc translated to Coq (levels, binary-counter value C, shifts).
It is untrusted: a wrong d is rejected by the batch guards and the step falls back to the single increment.
It must reproduce fast.py's d, though. A d that is systematically too small never terminates.

Structural increment `call1`

This is one call (TM91 call/outcome/resume_correct).
Walk the units from the LSB; each unit's case is stop, pass, glue, unglue, leadless, empty, U0/edge or halt.
Outcome Returned cfg' | Halted | Failed:
Returned: the call composes with segRLs_S/segRLs_lrcons/segRLs_sideRLs_concat;
Halted: sideRLs_halt (LongitudinalHalt);
Failed: the checker returns false and nothing is claimed.
During a call the cuts are fixed, so a glue (or an absorb) leaves an overhang of 1-cells at a segment's root end. canon then re-cuts: it merges the overhang into the root-side boundary (or the edge). Its soundness is a pure list equality (lpow_add, lpow_shift', Str_app_assoc), proved once per pattern.

Checker and soundness

next c := match propose c with Some d => batch … | None => call1 c end.
next_spec: either denote c -[tmf]->* denote c' or halts tmf (denote c).
check fuel := N_iter_until next (inl cfg342) fuel is inr; check_spec is Sk1Auto's proof.

Computation

About 54k single steps plus at most 54k batches, so roughly 1.1·10⁵ iterations of next. FUEL is 1.2·10⁵, confirmed by the Python mirror.
Work per iteration: O(25 units) of N arithmetic on 73-bit numbers, plus O(k ≤ 1339) list work per glue.
perf.v measures this order of work at 11 s native / 59 s VM. Allow 3–10× for the real step function:
native: well under 5 min;
VM fallback: under 15 min.
Both are inside check_kill's 1800 s compile timeout.

5. (c) Opening and endgame

Opening: init : c0 -[tmf]->* denote cfg342 by direct execution (unfold; esx/solve_init, 342 steps; c0 is flip-symmetric). cfg342 = edge 111, U0 = leadless [1, 1^10, 1], U1 = [2,00,3] with a glued boundary 1^5, NoTail. So the checker's first step is reset2 with a glued boundary, which root_reset2 must allow: the stop never touches the boundary.
Endgame: there is no separate phase. The run passes unit 21 with fuel 1, which gives [x,00,0] (pass1, c=0). The LSB then stops (stop1) and is passed with fuel 1 (pass1, c=0). The call is forwarded into unit 21, whose word starts with 00 at the cut. There halt0 fires: B writes 1 and moves, and C reads 0, which is the halt. call1 returns Halted, and root_halt lifts this to the whole configuration.
Final theorem: Theorem halt: halts tm c0. Proof. apply flipc0. apply (check_spec FUEL). native_check_eq. Qed. check_spec includes init and halts_evstep.
Option: a funext-free transfer as in #5's notes. Prove Perm (flip tmf) tm id pointwise and use flip_halts + perm_halts. Not needed, because funext is in the baseline.
Not needed: the exact step count (halts is ∃n). The steps_exact workflow can serve as an independent cross-check only.

6. (d) Compile-time and memory risks

Window lemmas: solve_seg lemmas take about 0.1–1 s each, so about 30 families plus compositions come to a minute or two.
The native cast: one native compilation plus run of the checker, under 1 GB RSS in perf.v. The 8 GB ulimit -v leaves a wide margin. Keep Eval compute out of the checker definitions; only tm/tmf use it.
coqchk will hit its 600 s cap. It re-checks the native_cast_no_check by lazy kernel conversion over about 10⁵ iterations of N arithmetic. That is a warning under policy A, and the RESULT line will say so. Window lemmas and the rest re-check quickly.
es normal forms: root_out failed under plain es, which ran past the target because of a lpow rotation mismatch. It was fixed with an explicit shift_rule_L sweep plus lpow_shift'. Expect this on about 20% of the lemmas.

7. Work order (each stage non-blocking, about 2–4 h)

proof.md (CLAUDE.md: before the .v). Include the protocol, the rule table above, and the batch closed forms. In parallel, work/coqmirror.py: a Python mirror of the Coq checker with the same records, guards, cases, proposal and canon. - Run it from cfg342 to Halted. - Assert equality with fast.py at all 82 resets (work/resets_long.jsonl) and at work/fuelout_config.json. - Output FUEL and per-case counts. This settles coverage before any Coq lemma is written: any Failed in the mirror is a missing lemma family.
Lemma catalogue: capture the words of every family from small instances (rocq/tools/block.py). Then prove them in this order: - root and resets; - k=1 (done); - chain; - k≥2 stop/pass; - leadless and empty; - glue; - unglue g=1, g≥2; - U0/edge (edge0, edge1, absorb, U0-1111). Each file is compiled separately (-native-compiler no is enough).
Batch, call1, canon, checker, soundness. Smoke-test on a prefix with a check_reach variant that proves c0 -[tmf]->* denote cfg_target, for example the reset-40 snapshot. Native-run timing comes from that test.
Full run, the kill file and check_kill --halt. Then status.json and STATUS.md.

8. Risks, most serious first

Lemma inventory and words for the structural families. These are unglue g≥2 with stacks, glue right after an unglue, the U0/edge cases and the resets. A shape no lemma covers makes the checker return Failed. Mitigation: the mirror decides coverage first, and the capture tools and solve_seg errors give the words.
Re-cut (canon) equalities after glue, absorb, unglue and the resets: tedious lpow/N.to_nat list algebra. Write one normalization tactic early.
The proposal must match fast.py. Fallback keeps the proof sound, but iteration counts can explode.
es/solve_seg normal-form mismatches (seen once). Budget for manual shift_rule proofs.
coqchk timeout (advisory, expected).
Rule trust is not a risk to soundness. The proof never assumes rules3. If a rule is wrong far out (more than 10 units, never TM-checked), its lemma or the checker fails and the halt prediction is refuted, not certified.