/machines/1RB0RF_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---/rocq-plan.md · raw

Rocq plan for #2 (formalization prep)

Machine #2 = 1RB0RF_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---. Template: vendor/busycoq/verify/SOMDCv6.v, Module TM7, whose machine differs from #2 only in A1 (TM7 0RC, #2 0RF). Written 2026-10-10. This is preparation only. No proof of #2 has been written; the only Rocq for #2 is the segment probe in §3.2.

0. Summary

  1. The template route works. A top-level copy of TM7 compiles in 3.8 s with Closed under the global context, and tools/check_kill.sh gives RESULT: PASS on it in 5 s (coqchk passes in 0.8 s).
  2. Most of the file carries over. With only the machine string swapped to #2, everything in TM7 compiles except two cases of RIncs_spec: an eater entering an L, and a drain pass entering an L. BigStep, the start-up from blank, and all non-L cases go through unchanged.
  3. The new low-level facts are proved by the existing automation. The +1 pass is an ordinary h visit (enter as B, leave as C), and both L-entry segments emit h ++ h' ++ h^^(1+k) to the right. All 8 probe lemmas compile in 6.5 s (rocq-scratch/probe_segments_2.v).
  4. The domain lemma does NOT carry over, and it is the real work. TM7 proves nonhalting with the invariant P r := exists r', RIncs hx 0 r r' ("r is in the domain"). For #2 that set is not closed: LLLL10LL1L1 is in the domain, but its image LLLLL1LLLLLLL111 is not. - The set image(eat) ∩ dom(eat) is closed in every test so far: exhaustive over inputs of length ≤ 12, plus about 62k random inputs of length ≤ 40. - Proving that closure needs a new lemma about three consecutive sweeps. Its invariant has not been found yet (§3.5). - A simpler fix, "the same domain with a fixed safety margin", is not closed either. Margin 2 looked closed up to length 10 but failed at length 11.
  5. Size estimate. The finished file should run about 450–700 lines (TM7 has 245). Roughly 150 of those are routine. A 3-sweep domain lemma of 150–400 lines carries almost all of the risk.
  6. What this means for Checkpoint A, Q2 ("extend TM7"). Extending TM7 is still the right route for the machine-facing part. The nonhalting argument needs a genuinely new idea, so proof.md must settle the invariant before any .v work.

1. Template anatomy

1.1 Shared header (SOMDCv6.v lines 1–17)

Item Statement / body Role
imports From BusyCoq Require Import Individual62 Longitudinal DivModCases., then ZifyNat Lia ZArith String List Individual62 provides the machine and the segment machinery. Longitudinal provides segRLs_addmul_v2 and sideRLs_1. DivModCases provides mod2 and sub. All three are on check_kill's allowlist and built (.vo + native).
Ltac esc tries BoundedConfig.segRLs_c_spec (T:=10^3), then BoundedConfig.sideRLs_c_spec (T:=10^3), then sideRLs_c_spec (T:=10^6) with vm_compute Proves a concrete segRLs/sideRLs goal by computation. Used for the right-end base case and inside am.
Ltac ec econstructor Builds RIncs derivations.
Ltac am a a' k b b' applys_eq (segRLs_addmul_v2 a a' k b b'); unfold DH0; flia; esc Proves segRLs tm (h^^(k*a+b)) (h^^(k*a'+b')) w1 w2 from two concrete facts: b visits give b' out, and every further a visits give a' out. Used for the binary-counter digits (a 0-digit absorbing 1+2k or 2+2k passes). flia comes from the import chain. The header does not define it, but it resolves.

Framework pieces TM7 relies on (from Individual.v / Individual62.v / Longitudinal.v): - sideRLs tm ls r1 r2. The right half of the tape, initially r1, receives the visits in ls from the left and ends as r2. Each visit (h1,h2) enters moving right in state/prefix h1 and leaves moving left as h2. - segRLs tm ls1 ls2 w1 w2. A finite word w1 (becoming w2) turns incoming visits ls1 into outgoing visits ls2 to its right. - segRLs_sideRLs_concat glues a segment onto a side. - segRLs_trans, sideRLs_trans concatenate visit lists. - segRLs_wall''. segRLs h1 h2 w w -> segRLs (h1^^n) (h2^^n) w w. - sideRLs_1 turns a one-visit sideRLs into -->+. - esx dispatches to solve_segRLs, solve_sideRLs, solve_init or es by goal shape. - follow10.

1.2 Module TM7 (lines 1627–1870), item by item

Item Statement Role
tm Eval compute in (TM_from_str "1RB0RC_…") The machine. This is the only line that names A1.
notations ld:=[1;1;0] (L), d0:=[0;0;0], d1:=[1;0;0]; hR:=(B,[]), hR':=(D,[1]), hL:=(C,[]); h:=[(hR,hL)], h':=[(hR',hL)] Digits, and the two visit kinds. h is the drain-pass visit and, for #2, also the +1 pass. h' is the eater (state D with a 1 on its left).
RD, H LD \| D0 \| D1; hx \| h1 Digit names. hx is the eater; h1 is count mode, which has a stray 1 in front, so the alignment shifts by one cell.
toRC list RD -> side, digits then 0inf Converts the digit list to the tape side.
toH', toH toH' hx=[], toH' h1=[1]; toH hx=h', toH h1=[] The extra cell in front of the side, and the first visit of the mode.
RIncs 10 clauses, H -> nat -> list RD -> list RD -> Prop (mode, pass count k, input, output) The sweep as a relation. hx_ld, hx_d0: eat, k+1. hx_d1: switch to h1 with k. h1_ld: back to hx with the same k. h1_d1: absorb one pass. h1_d0_0/1: halve. h1_rh_0/1/2: write k at the right end (bijective binary followed by a terminating D1).
cat3, tr1, wal, tr2 Ltacs cat3 peels a 3-cell digit off the side. tr1 splits h^^(1+k) and proves the first visit by esx. wal handles k identical visits through a wall. tr2 handles a leading sideRLs step.
RIncs_spec RIncs tp k r r' -> sideRLs tm (toH tp++h^^k) (toH' tp*>toRC r) (toRC r') Soundness: the relation is what the machine does. Proved by induction on the derivation, one bullet per clause.
RIncs_nxt_1 exists r, RIncs h1 k [] r The right end always succeeds in count mode. Proved by well-founded induction on k with mod2.
solve_v2, solve_v1 Ltacs Automation tailored to the case list of RIncs_nxt.
RIncs_nxt RIncs tp k r r' -> cond(tp,k,tp',k') -> exists r'', RIncs tp' k' r' r'', where cond is: hx,hx: k<=k'; h1,h1: 2k+1<=k'; h1,hx: k+1<=k'; otherwise False The domain lemma: the output of a sweep is again in the domain. Proved by induction on r, with a nested lt_wf_ind on k for []. It does not mention tm.
lh, S' lh := 0inf<*<[1]; S' r := lh {{{(hR',R)}}} toH' hx *> toRC r The boundary configuration 0^inf 1 1 D> r.
BigStep RIncs hx 0 r r' -> S' r -->+ S' r' One sweep: RIncs_spec, then sideRLs_1 and follow10, then es steps back from the left wall.
nonhalt ~halts tm c0 multistep_nonhalt to S' [D1] (esx, 5 steps), then progress_nonhalt_cond with P r := exists r', RIncs hx 0 r r', closed by RIncs_nxt (hx,0)->(hx,0).

TM8 (line 1874, A1 = 0LC) reuses the same proof text.

2. Standalone TM7 copy (template validation)

3. What changes for #2

3.1 Measured: what breaks when only tm changes

I swapped the string in the TM7 copy and compiled it (scratchpad only, not kept): - The first error is RIncs_spec, bullet 1 (RIncs_hx_ld). The eater's visit over ld now emits a different visit list. - I then stubbed the two L bullets (1 and 4) in a throwaway copy that is not kept anywhere in the project. Everything else compiled: the other 8 bullets of RIncs_spec, RIncs_nxt_1, RIncs_nxt, BigStep, and the c0 -->* S' [D1] start. - So the two L-entry segments are the only places where the machine's A1 matters. - TM7 has no separate es/ind lemmas. Every low-level fact goes through the segment automation (esx/esc/am/wal), so no other low-level lemma touches A1.

3.2 New relation Inc and Inc_spec (segment facts verified)

Inductive Inc: list RD -> list RD -> Prop :=
| Inc_nil: Inc [] [D1]
| Inc_d0 r: Inc (D0::r) (D1::r)
| Inc_d1 r r': Inc r r' -> Inc (D1::r) (D0::r')
| Inc_ld r r': Inc r r' -> Inc (LD::r) (LD::r').
Lemma Inc_spec r r': Inc r r' -> sideRLs tm h (toRC r) (toRC r').

Each case is cat3 plus one segment fact. The segment facts are proved in rocq-scratch/probe_segments_2.v (compiles in 6.5 s): - segRLs tm h [] d0 d1, by esx; - segRLs tm h h d1 d0, by esx; - segRLs tm h h ld ld, by esx; - sideRLs tm h 0inf (d1 *> 0inf), by esc.

Planned helper lemmas: - Inc_total: forall r, exists r', Inc r r'. - Inc_fun: Inc is deterministic. - Inc_D1: the output always contains D1.

3.3 The two RIncs clauses that change

| RIncs_hx_ld k r r1 r':  Inc r r1 -> RIncs hx (1+k) r1 r' -> RIncs hx k (LD::r) (LD::r')
| RIncs_h1_ld k r r1 r':  Inc r r1 -> RIncs hx (1+k) r1 r' -> RIncs h1 (1+k) (LD::r) (LD::r')

The other 8 clauses are TM7's, verbatim. Simulation agrees with this relation: - rocq-scratch/py/rincs.py mirrors these exact clauses; - out(hx,0,·) equals check_rules.eat on all 29,523 words of length ≤ 9; - check_rules.py matches 208/208 real sweeps.

3.4 RIncs_spec: the two new bullets

Segment facts, verified in the probe: - Eater: segRLs tm (h' ++ h^^k) (h ++ h' ++ h^^(1+k)) ld ld. TM7's is h' ++ h^^(1+k). - Drain pass: segRLs tm (h^^1 ++ h^^k) (h ++ h' ++ h^^(1+k)) [1;1;1;0] ld.

Both proofs are: - rewrite lpow_add; - then change (h ++ h' ++ h^^1 ++ h^^k) with ((h ++ h' ++ h^^1) ++ h^^k); - then eapply segRLs_trans; [esx | wal].

Bullet shape: eapply segRLs_sideRLs_concat with the segment fact, then eapply (sideRLs_trans (ls1:=h)); [apply Inc_spec; eauto | eauto].

TM7's cat3 ends in [|eauto 1], which cannot find the sideRLs_trans split, so these bullets are written out (about 4 lines each).

3.5 The domain argument (main risk)

TM7's invariant fails for #2. Script: rocq-scratch/py/domain_facts.py. - Over all words of length ≤ 10, TM7's map keeps its domain (12,491 words, 0 escape). - #2's map does not: 8 of 26,019 domain words map outside the domain. - Over words of length ≤ 12 that end in 1, 230 domain words map outside the domain. - Worked example: LLLL10LL1L1 → LLLLL1LLLLLLL111. On the second word, the eater reaches the tail 10001 with k = 13. The 1 becomes L, and the drain of 0001 then needs 15 passes but has 12.

So RIncs_nxt has no #2 analogue with any condition on (tp, k, tp', k'). I derived this by hand and the measurements back it: the constraints forced on a bound g(k) are contradictory (g(k+2) ≤ g(k)+1 versus g(k) ≥ k−1).

What holds instead (tested, not proved): 1. Commutation lemma RIncs_Inc: RIncs tp k r r' -> Inc r' r'' -> RIncs tp (1+k) r r''. In words, a +1 applied to a sweep's output is the same as one more pass in that sweep. - It holds because the count-mode digits encode the leftover passes in bijective base 2 (D0=1, D1=2, terminated by D1), and Inc is exactly bijective +1 on that code. - Checked on 659,938 cases (all words of length ≤ 8, k < 40). - Proof: induction on the RIncs derivation, inverting Inc. Every case closes with one constructor and the IH; the D0 cases need mod2 arithmetic. Estimate 40–60 lines. 2. image(eat) ∩ dom(eat) is closed under eat. - 0 failures exhaustive: 26,011 image words from inputs of length ≤ 10, and 197,471 from inputs of length ≤ 12. - 0 failures random: about 62k image words from inputs of length ≤ 40. - The real orbit lies in this set, since every config after S(1) is an image.

Proposed proof shape: - Invariant: P r := (exists r0, RIncs hx 0 r0 r) /\ (exists r', RIncs hx 0 r r'). - Start: S' [LD;D1], reached at step 16 from blank (by simulation; esx should do it as for TM7). P [LD;D1] holds via r0 = [D1], with r' = [LD;LD;LD;D1;D1], which matches the step-91 config. - Key lemma (new): RIncs tpA a s r -> RIncs tpB b r r' -> Cond(tpA,a,tpB,b,tpC,c) -> exists r'', RIncs tpC c r' r''. It describes three sweeps A, B, C side by side, digit by digit. - A +1 fired by B on its rest becomes a+1, by RIncs_Inc together with Inc_fun and RIncs determinism. A +1 fired by C becomes b+1. - Induction: on a measure of the middle word r, e.g. length r + 2*(count of LD in r). This strictly drops every step even after B's Inc. TM7's structural induction on r fails here, because the sub-derivation runs on Inc r. - Unknown: Cond. The harness rocq-scratch/py/joint.py replays the three sweeps jointly; it agrees with direct composition on 1678/1678 samples. Its data, over all inputs of length ≤ 11 where A and B succeed (71,695 inputs, C always succeeds): - only the mode triples xxx, 1xx, 11x, 111 occur (A's mode ≥ B's ≥ C's); - b >= a and 2c >= b hold at every position; - 111 occurs only after A has finished (a = 0). - Neither 2c >= b nor a TM7-style pairwise condition is inductive on its own. Hand-checking the 111 transitions breaks both, so Cond must use a and the phase (A still reading, at the right end, or finished). Finding it is the first job of proof.md. - Shortcut tried and ruled out: a fixed safety margin. The real orbit has large slack: at count-mode entries, k exceeds the passes needed by at least 2 in the first 400 sweeps, and usually by hundreds. So I tested "the sweep still succeeds if each eater-to-count switch hands over fewer passes". Script: rocq-scratch/py/margin.py. - Each variant holds on the real orbit, but none is closed under the real eat. - Margin 1 fails on 8 words of length ≤ 10. - Margin 2 has 0 failures at length ≤ 10, which looked promising, but 38 at length ≤ 11 and 16 of 8,198 random words. - Halving the count fails on 3,240 words; taking 3/4 of it fails on 64. - The failures repeat the …1 L^a 111 pattern of the counterexample above, at larger sizes. - A TM7-style condition also fails on the margin-2 domain. The least k' that works for an hx count k is [0,9,1,10,6,11,7,12,8] for k = 0..8: not monotone, and parity-driven (margin_cond.py). - Any quantitative invariant would have to scale with n, the length of the L-run. That route is untested.

3.6 BigStep and nonhalt

3.7 Size estimate

Piece Lines Risk
TM7 text kept (notations, toRC, 8 RIncs clauses, 8 RIncs_spec bullets, RIncs_nxt_1, BigStep) ~150 none (compiles today)
Inc, Inc_spec, Inc_total, Inc_fun 40–60 low (segments verified)
2 new RIncs_spec bullets ~10 low (verified)
RIncs determinism, RIncs_Inc 60–90 low–medium
3-sweep domain lemma (replaces RIncs_nxt) 150–400 high: invariant unknown
nonhalt ~25 low
Total ~450–700 Compile should stay under 30 s: the computation is local segments only.

4. Tactics to reuse, and pitfalls

Reuse: - cat3 / tr1 / wal / tr2 / am / esc unchanged. - The rewrite lpow_add + change (… ++ h^^k) + segRLs_trans; [esx | wal] pattern for any visit list of the form "fixed prefix, then k copies". - mod2 / sub from DivModCases for parity and predecessor case splits, as in TM7's RIncs_nxt. - gen + inverts (LibTactics) for derivation inversion.

Pitfalls (each hit while probing): - Open Scope nat turns list literals into list nat. [1;1;1;0] fails as a list Sym. Declare word notations (e.g. Notation w1ld := [1;1;1;0].) before Open Scope nat, as TM7 does for ld/d0/d1. - Use 0inf, not const 0, for the blank side. const 0 is read as Stream nat. - cat3's [|eauto 1] will not combine Inc_spec with the IH. Write the sideRLs_trans split explicitly. - TM7's solve_v1/solve_v2 are tied to its case order. The new domain lemma needs its own automation. - Inducting on the derivation gives no IH for the Inc premise. That is fine for RIncs_spec. For the domain lemma, use the measure induction described in §3.5. - check_kill reads raw text, comments included. Keep the forbidden words out of the final file, even in comments (see rocq-notes, "Trust base"). The stub run in §3.1 lived only in the scratchpad. - Stack, native and timeouts are not an issue at this size. - TM7 needs no ulimit change in practice; it is set anyway. - Native compile adds about 1 s. - coqchk finishes in under 1 s, far below the 600 s cap. - esc's vm_compute fallback (T:=10^6) is never reached by the probes; BoundedConfig with T:=10^3 suffices.

5. Files

Reproduce the data: cd rocq-scratch/py, then run: - python3 -B rincs.py (about 1 min); - python3 -B domain_facts.py 10 (about 2 min); - python3 -B joint.py (about 5 min); - python3 -u -B margin.py 2 11 40000 300 (about 15 min).