W4-3 formalization log

Machine 1RB0RF_1RC0RB_1LD0RA_1LE0LD_1RB0LC_1LA--- (740 line 341). Kill file: machines/1RB0RF_1RC0RB_1LD0RA_1LE0LD_1RB0LC_1LA---/1RB0RF_1RC0RB_1LD0RA_1LE0LD_1RB0LC_1LA---.v.

Round 1 (2026-10-12)

Architecture chosen

proof.md section 10 recommends a verified interpreter. Built a symbolic run-length simulator (ssim) instead of a defect-model interpreter: it runs the machine itself, so the soundness proof is generic (it calls tm for single steps) and only the two sweep cycles are machine-specific.

• A run is (first symbol, length); a length is a linear form LF c [v0; v1; ...] = c + sum v_i x_i over N. A side is (list run, tail), tail T0 = 0^inf or TV k = abstract side k. ev_cfg nu sg c evaluates a data config to a TM config for a valuation nu : list N of the x_i and sg : nat -> side of the abstract sides.
• sstep: if the head state and the first symbol of the next run are in a sweep cycle (right B0 C1 A0 B1, left D1 D0 E1 C0) and every coefficient of the run length is 0 mod 4, cross the whole run in one step (state index + c mod 4; the run is pushed, complemented and reversed, onto the other side, merged with its first run when the alternation continues). Otherwise one machine step (pop the head cell; needs c >= 1, or a definitely empty run, which is dropped). Returns a flag: true iff at least one machine step was made.
• sstep_spec : sstep c = Some (c', b) -> Rel b (ev_cfg nu sg c) (ev_cfg nu sg c') for ALL nu, sg (Rel true = -->+, Rel false = -->*), and runp_spec for runp p (exactly p steps, p positive).
• Reading an abstract tail makes sstep return None. So a run "until stuck" with abstract sides is a locality proof for free: the lemma holds for every content of the abstract sides.

Proved (rocq/ssim.v, 1.5 s; kill file compiles, see below)

• ssim + soundness: push_spec, pop_spec, push_run_spec, accR/accL (+ _S progress versions, induction on the run length over the 4-cycle), single_spec, sstep_spec, runp_spec.
• init28 : c0 -->* ev_cfg [] (fun _ => const S0) cfg28 by runp 18571896 and native_compute (17 s for the cast). cfg28 = record exit 28 (step 2,629,088,227,408, class r5, e = 2, u = 1, K = 7). It matches proof.md 3.4 (right region B -224493- x1 -673559- x2 -7- x3 -9841- x4 -1942040- x5 -3- hi) and the chain of 3.3 (window 8277, 24912, 74808 = 8316u-39, 24948u-36, 74844u-36). Record exit 16 is reached after 225,240 simulator steps (398,090,000 machine steps) and matches Appendix C cell by cell.

Validated by dev runs (rocq/dev_*.v, not in the kill file)

• dev_sym.v: the record-exit-28 episode with every long gap symbolic (27 + 4 x0, ...) and the left side abstract: 117 simulator steps, 8 ms, returns Lc D ([], TV 0) [27+4x0, 27+4x1, 8, 20+4x2, 53+4x3] = Appendix B r5 start (7 -> 8, 9841 -> 9836, last gap +30, hi gap absorbed).
• dev_visit.v: from cfg28 the head reaches the cut (3 cells after B-2) in state A in 1 step; the first chain visit Lc D ((S0,3) :: chain, T0) ([], TV 1) is 9 simulator steps and ends Rc A with block K's digit moved -1 (8277 -> 8278, inter gap 2737 -> 2736) = Lemma C, U0 -> U1, exit c_K+2.

Conventions for the next rounds (decided in round 1)

• Cuts. Every region boundary is a cut inside an alternating stretch, never at a defect:
• chain / right region: after cell B+1 (3 cells after the U0 place of s3 = B-2);
• block j / block j+1: 3 cells after block j's s3 (U0 place); block j+1 gets I-3 >= 2 cells of the inter gap I (residue 2 mod 4);
• left word / chain: between cells A-1 and A (block 1 gets 3 cells before its digit at A+2). All footprints of proof.md (Lemma B, L81, R) stay inside their region, so every regional run is an ssim run with the other sides abstract.
• States at cuts. Entering a block from the right at its phase c: Lc D reading 0. At c+2: Lc C reading 0. Leaving to the right at phase c+2: Rc A (reads 0); at phase c: Rc B (reads 0). (Block bases differ by 2 mod 4, so "c+2 of block j" = "c of block j-1".)
• Block runs, left side, nearest first (m = 3): with gap lengths a (digit gap), s, t (separator gaps), lp (left part) and state offsets (dd, d1, d2, d3) from proof.md 3.2: [(S0, 3-d3); (_, t+d3-d2); (_, s+d2-d1); (_, a+d1-dd); (_, lp+dd)], symbols by the defect rule (next run starts with the far symbol of the previous one). At rest every block starts with S0 at its right cut, in every state (the region length and the defect count are fixed).
• Global config at a visit boundary: Lc D (chain runs ++ left word runs, T0) (right runs, T0), the head on cell B+1. Invariant point for Lemma S: Rc A ... at the same cut (after the record visit).

Plan for rounds 2-4

1. Generate (script) the 18 single-block runs of proof.md 4.1 / Appendix D as ssim lemmas with symbolic a, s, t, lp and abstract sides; case-split tight gaps (a = 1 vs 5+4x, s,t = 4 vs 8+4x, lp = 2 vs 6+4x) where ssim fails. Then Lemma C / C' by induction on the block list (LSB first, like #11's LbS/RbS), with relations Visit c c' p := forall r, side c <{{D}} r -->+ side c' {{st p}}> r.
2. Left word: episodes 1-80 as one forallb over i of an ssim check (head enters at A-1, abstract right side); L81 as one ssim run with block 1 in D0.
3. Right region: Ep p R R' := forall l, l {{st p}}> R -->* l <{{D}} R'; singles of Appendix B as ssim runs in t (u = 1 + 8t); 4-cycles as one ssim run on fresh variables (composite f(h) = h + d) plus an induction on the cycle count.
4. Interleaving: Visits c c' ps -> EpSeq ps R R' -> cfg(c,R) -->* cfg(c',R'); Lemma T gives ps = 2^T 0^(N-T).
5. Record visit, regrouping (tape equality), window closing (lia in t), INV, nonhalt.

Added at the end of round 1

• reach fuel c tgt + reach_spec (in ssim.v and the kill file): every regional lemma of rounds 2-4 is apply (reach_spec N). vm_compute. reflexivity. on data configs with symbolic lengths and abstract sides. cfg_eqb compares lengths up to trailing zero coefficients (so zadd padding never matters).
• dev_reach.v: block U0 (m = 3) entered from the right at its phase c, symbolic t, s, a, lp (4+4x0, 4+4x1, 1+4x2, 2+4x3): blk_U0 : ev U0c -->+ ev U1o (U0 -> U1: digit gap +1, left part -1, leaves Rc A), closed under the global context. dev_block.v: U1 -> U2 the same way, and the tight digit gap a = 1 needs no case split for these two runs.
• Kill file: 711 lines, compiles in 35.6 s (native); check_kill --text-only: everything PASS except theorem_text (no nonhalt yet, by design: no Admitted anywhere).

Next round, first steps

1. A script rocq/gen_blocks.py that emits the 18 runs of proof.md Appendix D as reach lemmas, using the block-runs convention above (m = 3 and m = 1, the 8 / 5 states), entry states Lc D (right, phase c), Lc C (right, c+2), Rc A/Rc B (left entries); fall back to destruct on tight gaps where reach fails. Check each event count against Appendix D.
2. The chain word as a list (LSB = block K first) and Visit by induction, as in #11's LbS/RbS.
3. Left episodes: one forallb over i in 1..80 of a reach check (left word W_i, head entering at A-1).

Round 2 (2026-10-12)

Dev files (this folder): chain.v (blocks, chain visit, left word), count.v (Lemma T), right.v (right-region executor and the six interval programs), regroup.v (6.2 regrouping), step.v (Lemma S, class r5), rec2.v/rec3.v (record-exit episode experiments). All merged into the kill file, which compiles (native) in about 37 s.

Proved (all Qed, no Admitted)

• Blocks. lab = U0 U1 U2 W0 W1 D0 D1 D2 (m = 3), lab1 = P0 P1 PD0 PD1 PD2 (block 1). blk s = run list from the block's right cut, lengths lens s with variables x0..x3 = (t-4)/4, (s-4)/4, (a-1)/4, (lp-2)/4 (so every tight gap is the instance x = 0). rblk = the full block after a leftward pass (right side). The 18 runs of Appendix D are blk_turn, blk_pass, blk_reset, blk1_turn, blk1_pass, blk1_back, each one reach check with both sides abstract (no case split needed, tight gaps included).
• Left word. lw i closed form (base-3 digits of i, i = 0..80) and lw 81 = output of the left record. lw_ep : i < 81 -> LWs i <{{E}} Y -->+ LWs (S i) {{B}}> Y: one forallb over 81 reach checks. Episode 80 is the left record (L81); no separate lemma is needed. Block 1 hands over to the left word in state E (not D).
• Chain visit (Lemma C, C'). Functions visit3, cb, vis on labels; visit3_spec, pass_spec, cb_spec, vis_spec by list induction; runv n iterates vis; runv_spec: n visits plus the interleaved episodes (EpSeq of the exit phases) on the machine.
• Lemma T (interval): runv (81*3^K-1) (U0^m, P0, 0) = Some ((D0^m, PD0, 80), true^T ++ false^(81*3^K-1-T)) with 2T+5 = 3^(K+1), K = m+1, for every m >= 2. Pieces CU, CW, S3 (mixed regime), allD (value counting), cyc/cycs. interval_tm and record_visit put it on the machine.
• Right region. ep_run (simulate until stuck, must end Lc D ([], TV 0) (rr', T0)), jump_run (4-cycle jump: runs the cycle once on the actual config, derives a template with one fresh variable per changing run, checks the cycle on the template, and composes; soundness jump_lemma by induction on the cycle count with shifted valuations), exec over ISingle/IJump programs, prog_check_spec. The six programs of Appendix B (prog_r5 .. prog_r4, u = 1 + 8t, jump counts as linear forms in t) are checked by vm_compute in 15-70 ms each; the phase counts come out as T = 3278+26244t / 9839+78732t and F = 173868+1390932t / 521601+4172796t, exactly Lemma T's.
• Regrouping (6.2): regroup (list induction, any chain): chain in D2 = (S0,1)(S0,2+4xt_K) ++ chain in U0 regrouped one defect later (rshift), and regroup_b1 for block 1 + left word (by reflexivity).
• Record-exit episodes: by reach, all six classes close against the next class's start vector: drop classes r5->r0, r1->r2, r3->r4 directly (target Lc D ([], TV 0) (Rs_next, T0)); take-in classes r0->r1, r2->r3, r4->r5 found by search (rec3.v): the head passes x1..x3, and the new cut is inside a merged run, so it must be split (see next steps). r4->r5 matches Rs_r5 at t' = 1 + 9t (sub9).
• S_r5: the full record interval of class r5 on the machine, for every e >= 2, every deep chain: Gc (U0^m) ([W5t t; W5s t; W5a t; f1] :: deep) (evR [t] Rs_r5) -->+ Gc (U0^m) ([W5s t; W5a t; f1; rtop deep 0] :: rshift deep 0) (evR [t] Rs_r0), given 1 + 8t = 9^(e-2) and length deep = 1 + 2e.

Tactic notes (also in atlas/rocq-notes.md)

• apply (reach_LL 100) on a goal with concrete nu = [] hung in unification; refine (reach_LL 100 D E l r [] L R _) with explicit arguments is instant.
• A proof that asserted lw_ok i = true then unfold lw_ok in H and exact hung at Qed (kernel); splitting into lw_ok_spec (exact) and lw_ok_lt (forallb_forall) is instant.
• destruct (visit3 ls) ... eqn: also rewrites the IH's premise; use IH _ _ eq_refl.
• Pos.iter-based "run until stuck" loops keep iterating after stopping (slow at fuel 1e5); urun recursion on positive returns early.
• Large nat literals (>= 5000) become Nat.of_num_uint ... and lia cannot read them: write 6561 as 81 * 81.
• ZArith (needed for Z.div/Z.modulo in mk_jump) shadows shift/top: renamed to rshift/rtop.

Next steps (round 3)

1. Take-in record steps (r0->r1, r2->r3, r4->r5): split the 4th run of Re_r (x3 -> x4) as (b,3)(sneg b, n-3) by alt_add, run part (a) with the rest of the right side abstract (TV 1): Rc B ([(S0,1);(S0,L2)], TV 0) (first3 ++ [(b4, cn 3)], TV 1) -> Rc A (comp_runs sigma (blk U0), TV 0) ([], TV 1), then part (b) ep_run true Re' = Some Rs_next. For r2, r4 the free xt_K is variable 1 (LF 2 [0;4]), sigma's 4th entry LF 0 [0;1]. New nus = q_new :: rshift nus 0.
2. Drop classes r1->r2 (block K' also dropped: left part = [(S0,1);(S0,673558+..)] ++ comp_runs sigma (blk U0)) and r3->r4: same as step_r5. Then S_r for all six (the S_r5 proof is the template; K0 = 3 or 4).
3. Invariant: Inv r e t nus with the window shapes (r5: [W5t;W5s;W5a;f] :: deep; r0: [W0t;W0s;f;f'] :: deep; r1: [all four] :: [W1t';f;f';f''] :: deep; r3: [W3t;f;f';f''] :: deep; r2, r4: any), length nus = K0 + 2e - 1, 1 + 8t = 9^(e-2). r4 -> r5: e+1, t' = 1 + 9t (sub9).
4. Base case: from cfg28 reach Gc (U0^6, P0, 0) nus28 (evR [0] Rs_r5) (concrete target; use a conc lemma ev_runs nu rs X = ev_runs [] (conc nu rs) X to compare by cfg_eqb). nus28 from cfg28's chain (block 7: [18701; 6227; 2069; 683]).
5. nonhalt via progress_nonhalt with P c := exists r e t nus, Inv /\ c = Gc ...; then check_kill.

Round 2, later the same session: the proof is complete

After the checkpoint above, the remaining steps were all done in this round:

• step2.v: record steps for all six classes. Drop classes (r5, r3: drop 1; r1: drop 5, the new block K' is part of the left list of the reach start) by drop_step. Take-in classes (r0, r2, r4) by take_step: split4 splits the 4th run of the end vector (x3 -> x4) as (b,3)(sneg b, n-3); part (a) is a reach with the rest of the right side abstract (TV 1), ending Rc A (comp_runs sig (blk U0), TV 0) ([], TV 1); part (b) is ep_run true Rp_r = Some Rs_next. For r2, r4 the free last t gap of the chain is variable 1 (xv = LF 2 [0;4]). r4 -> r5 ends at sub9 Rs_r5 (t -> 1 + 9t, ev_runs_sub9).
• S_r0 .. S_r4 (generated from the S_r5 template; K0 = 3 or 4; constants written as products, e.g. 243 * 81).
• main.v: cls, cfgI, win (window shapes), Inv, inv_step : Inv s -> exists s', cfgI s -->+ cfgI s' /\ Inv s'; nus28 (chain of record exit 28 in gap variables: block 7 = [18701; 6227; 2069; 683]), inv28, base28 (cfg28 -> 3 cells to the cut -> record-exit episode -> cfgI (C5, 2, 0, nus28); the chain equality b28_chain is plain reflexivity).
• Kill file: nonhalt : ~ halts tm c0 via multistep_nonhalt (init28 + base28) and progress_nonhalt_cond (cfgI, Inv, inv_step, inv28). 2,411 lines; compiles with native in 43 s; Print Assumptions nonhalt: Closed under the global context.

check_kill, round 2

• First run (rocq/check_kill_r2.log): every check PASS except (h) coqchk: Fatal error: out of memory after 112 s (not a timeout, so FAIL). Cause, isolated on the round-1 file (ssim + base case only): coqchk re-checks the single 18,571,896-step runp cast by VM conversion and grows to 7.1 GB (the 8 GB ulimit -v cap) in 100 s. The same cast with vm_compute in coqc needs only 433 MB (3:25), so the growth is coqchk's.
• Fix: the base case is cut into 38 pieces (ck_0 .. ck_37, 500,000 simulator steps each, the 38 intermediate configurations written out as b28_i, generated by gen28.v). coqchk on the base-case-only file then stays at about 3.3 GB and was still running after 9.5 min (the VM re-check is slow, so expect the 600 s coqchk timeout, a warning under policy A). Compile time is unchanged (47 s for the base-case file).
• Second run: rocq/check_kill_r2b.log.
• Second run (chunked base case): RESULT: PASS, exit 0. All checks PASS; coqchk SKIP after its 600 s cap (policy A warning: the native/VM computations rest on coqc's checks). Isolated Print Assumptions nonhalt: closed (0 assumptions).

State after round 2

The kill file is complete and passes check_kill. Rounds 3-4 are free for: a coqchk that finishes (it would need a cheaper base case, e.g. starting the induction at an earlier record exit), clean-up of the file (dead helper lemmas such as sum_false_true), and the public write-up.