/machines/1RB0RC_1LC1RB_0RE1LD_0LC1LA_1RF1RA_---0RB/rocq/log.md · raw

W5-4 Rocq log (1RB0RC_1LC1RB_0RE1LD_0LC1LA_1RF1RA_---0RB)

Dev file: rocq/W54.v (compiled from a scratch copy with -native-compiler yes). The kill file ../1RB0RC_..._---0RB.v is a header-wrapped copy of it.

Round 1 (2026-10-13)

Design (differs from W4-2 in the left side, same one-lemma-per-rule layout)

Tape family: RT l q Z := l {{C}}> [0;0] *> [1;0]^^q *> Z *> const 0 with Z : list sym (NOT list Sym: Sym and sym are convertible but rewrite treats them as different terms, so a zone typed list Sym breaks every rewrite against lemma statements whose numerals elaborate to sym).
Left side = a stack of frames. FR p l := [1] *> [0;1]^^p *> [0;0] *> l is the frame 00 (10)^p 1; the cycle start has no frame (l = const 0). Rounds give [1;0;1;0] *> FR p l = FR (p+2) l (FR_round, FR_rounds), PUSH k gives [1;0;0]^^k *> [1;0;1;0] *> FR p l = Nat.iter k (FR 0) (FR (p+2) l) (FR_push): the pending inner levels are frames with p = 0, and an ending bite pops the top frame. So the shift law is free: no rule lemma reads below the top frame.
Zone: zone r L v := [1]^^r ++ dg L v ++ [1;1;1], dg (S L) v = [1;1;bitc v] ++ dg L (div2 v), bitc v = 0 iff v odd. Width 3L+3+r; bit b of v on the b-th block 11c (= the lattice of proof.md, lowest cell 2/3/4 for r = 0/1/2). Lowbit decomposition v = 2^b (2o+1): dg_low ((111)^b 110 dg o) and dg_lowones ((110)^k 111 dg o for v = 2^k-1+2^(k+1) o).

Proved (all Qed, file compiles in ~4.6 s)

Low-level rules by plain es (each 1 line): BR, SW (=S), TT (=T), PS, the three round arrivals RND2/RND1/RND0 (W + PS^q + ZA composed in one es), PUSH k, BITE1, BITE0, BITE0c, BITE0c3. The halting tail Ht is not needed (non-halting never runs it).
Counter forms of all rounds for any left side: R1z (r=0), R1t (r=2), R2r, O2r, O1r, O0r.
Counter forms of all bites on a frame: PUSHr (B2 = k 0, N = k >= 1), B1z0, B1z1, B1o, B1t, B0r, B0cr, B0c3r.
Batches R1s_z / R1s_t (j rounds of R1, by induction on j).
nh_prog / nh_ev: c -->+ c' (resp. -->*) and ~halts_in c' M for all M < N (resp. <= N) give ~halts_in c N (from TM.v preceeds_halt / exceeds_halt): the transfer lemmas for the bounded route 3 of proof.md section 9.
init : c0 -->* RT (const 0) 6 (zone 2 0 0) (= (6,5,0), 327 steps) by solve_init.

Tactics that worked / failed

FAILED: stating a zone as [1]^^(3*j+2) *> [0] *> r; st rewrites 3*j with lpow_mul into [1]^^j *> [1]^^j *> [1]^^j and the T rule is never found. WORKED: write the zone as [1;1;1]^^j *> [1;1;0] *> r (es then finds BR over [1;1;1]^^j and T itself).
WORKED: list-shape identities as stream lemmas (S_ones2 : [1;1] *> [1;1;1]^^b *> s = [1;1;1]^^b *> [1;1] *> s, S_sh110 : [1;1] *> [0;1;1]^^b *> s = [1;1;0]^^b *> [1;1] *> s), applied after rewrite !Str_app_assoc; concrete regroupings by change ([1;1;1;1] *> ?X) with ([1;1] *> [1;1] *> X).
WORKED: trailing blanks: assert (E: ... *> [1;1;1] *> const 0 = ... *> [1;1;1;0] *> const 0) by f_equal. cbn. repeat f_equal. apply const_unfold. (two blanks: cbn. rewrite <-!const_unfold. reflexivity.). rewrite (const_unfold 0) fails (the type argument T is explicit).
PITFALL: repeat/app_assoc are not in scope (only ListNotations is exported): use List.repeat, List.app_assoc. Nat.odd_mul etc. need Require Import ZArith (or Arith).

Also proved in round 1 (second half; file compiles in ~6.6 s, 76 lemmas, no Admitted)

lev P l (shifted frame index P = p+1; P = 0 = cycle start over const 0, guarded by okL P l := P = 0 -> l = const 0): lev_round, lev_rounds. With it the outer cycle (P = 0) and an inner level (P = 1 = frame p = 0) are the same lemma, and a level started at P pops at RT l (P + n') ... where n' is the pop of the same run from a cycle start (F(t) for P = 0, G(t) = F(t)+1 for P = 1): the shift law SL1 holds by construction.
Rnd (inductive, the 6 round types) with Rnd_tape (on lev), Rnd_valid (v' < 2^L', r' < 3), Rnd_exists (q >= 3 always has a round), Rnd_sign (the sign-law quantity Qv P q r L v := (Mv q r L v + 2P) mod 3 is invariant; plain lia handles the mod 3 after rewrite ?Nat.pow_add_r; cbn [Nat.pow]).
EB (inductive, the 7 ending bites: B1 x4, B0, B0c, B0c on 111) with EB_tape (RT (FR p l) q zone -->+ RT l (S p + e) zone') and EB_sign ((Mv(pop) + Qv(bite)) mod 3 = 0; nia for the B0 case, products 2^b*o).
PUSH_lev (q = 2: k pending frames Nat.iter k (FR 0) over lev (P+2) l, q = 1, zone 1 L o), inner1 (the innermost level is one B1: pops at q = 3, zone 0 L o = t_2).
chain (standard levels from (Q, 0, L, 2^L-2), by lt_wf_ind on Q): reaches (P', Q', L') with Q'+2 <= 2^(L'+1), invariants P'+Q'+L' = P+Q+L and Q' + 2^(L'+1) = Q + 2^(L+1) + L' - L.
run_bite (r = 0, 2, q <= 2v+2: j rounds to qb <= 2, qb >= 1 if q >= 3), run_ovf0 / run_ovf2 (q >= 2v+3: v rounds then O0 / O2).
Definitions cap, Kst (d >= 2), Jst, Mv, Qv, Ist; init_I : Ist 6 2 0 0.
check_kill on the kill file: FAIL only at theorem_text (no nonhalt yet); forbidden, structure, Require allowlist and the tm literal PASS.

Plan for round 2+ (route 3 of proof.md 9, CPS form)

safe c N := forall M, M <= N -> ~ halts_in tm c M.
Phase lemma PH (pure -->*, no IH needed): from a config (P, q, r, L, v) with r in {0,2} to its bite, three outcomes: (A) no overflow (run_bite); (B) r = 2, O2, then q in {1,2} with the all-set zone (q = 2 here is exactly H: excluded by H* arithmetic); (C) O0/O2(+R1), then chain, then run_bite on the bite level (zone 0 L' (2^L'-2-j)). In (C) the bite zone is never all set, so H never happens there.
U(N) by strong_induction on N: forall P l n r L v, okL P l -> r < 3 -> v < 2^L -> (Jst n r \/ K' n r L v) -> (forall n' r' L' v', Props (n,r,L,v) (n',r',L',v') -> safe (RT l (P + n') (zone r' L' v')) N) -> ~ halts_in tm (RT (lev P l) n (zone r L v)) N. Props = (U1)-(U4) of proof.md 6 (+ the (6,4,0) exclusion for K' starts). Cases: r = 1 first round by hand (R2 / O1, EQ1 / EQ2 arithmetic), then PH; the bite: EB_tape (pop, continuation), B2 = PUSH_lev k = 0 then EB1o, N = PUSH_lev k >= 1 then inner1, then IH at a smaller budget (nh_prog gives M < N) for each inner level lev 1 and for the resumed phase lev (P_c+2) l (a J start), chaining the continuations.
Keep every arithmetic case in its own small lemma (W4-2 perf pitfall: lia with the invariant in context is slow); facts like 2^(S(S L)) = 4*2^L given to lia explicitly.
Final: nonhalt by strong induction on N over cycle starts in Ist, from init and U with P = 0, l = const 0, the continuation being the induction hypothesis.

Round 2 (2026-10-13): nonhalt proved

The kill file and rocq/W54.v are now the same file (1039 lines, header + base + main induction + rule-table comment). Single-file compile: 36 s native (base 8 s + main part 10 s when compiled as two files; the single-file time varies with machine load). Print Assumptions nonhalt: Closed under the global context. No Admitted.

Design change: phase invariants instead of chain arithmetic

The round-1 plan (phase lemma PH with three explicit outcomes, then Lemma K / Z' / A1 / Kp as separate arithmetic on the overflow chain, EQ1/EQ2 for w = 1 mod 3) was replaced by one generic lemma plus invariants: - phase Inv: for any Inv j q r L v (j = frame offset from the level start) that every Rnd preserves, the run from a config with Inv reaches a bite config (q <= 2) with Inv, by lt_wf_ind on q. No case analysis on overflows at all. - PI t (the phase invariant of a level from t = (n,r,L,v)) is a conjunction of - j even; Qv j .. = Mv t (sign law, from Rnd_sign); - r' = 1 -> j = 0, r' = 2 -> L' = 0 -> j <= 2 (the (6,4,0) exclusion, U5); - Saf q r L v (Lemma P: no H, every bite has a rule; parity of q when w = 2, the O1 lookahead); - t in K' -> KI j q r L v: r = 0: 2^L <= j+q /\ (2^(L+1) <= j+2v+2 \/ 2^(L+1)+1 <= j+q) /\ (q = 0 -> v <> 0) /\ (L = 0 -> 4 <= q); r = 1: 2^(L+2)+2 <= q /\ (v = 0 -> 2^(L+1)+5 <= q); r = 2: 2^(L+1)+2 <= j+q /\ 2v+5 <= q. At the bite this gives d(F t) >= 2 for every plain end and A1 (2^Lc <= j+2) for a nested bite. - t in J, d(t) <= 1 -> ZI (cap t + 1): r = 0: L <= C+1 /\ q + 2^(L+2) + C <= 2v + L + 2^(C+3) + 1 /\ (q = 0 -> v = 0 -> L <= C) (q + 2^(L+2) - 2v - L is constant along R1/O0, so at most one more overflow); r = 1, 2: the start bounds. Gives cap(G t) <= cap(t) + 1 (Lemma Z'). The w = 1 mod 3 starts need no EQ1/EQ2: K1/ZI1/Saf1 hold at the start and map to K0/K2 etc. - Post t t' = U1..U5 of proof.md 6 (+ validity); U N = CPS form: pops safe for N-1 steps -> start safe for N steps (safe c N := forall M <= N, ~halts_in tm c M). - U_all by strong_induction: N = 0 by one round (safe_prog0); else phase, then bite_shape: ending bite (EB_lev + ending), B2+B1 (ending_B2), or nested bite: PUSH_lev, inner1, STK (induction on the number of pending frames, U at fewer steps per level, carrying Budget t C := Kst t \/ cap t <= C and the alternating sign SR), then U for the rest of the level at frame P+j+2, and compose for the arithmetic (QvN: the N row of the sign law via 2^k = 3x + 1 + k mod 2). - cycles: strong induction on N over Ist (= K' with M <> 0); nonhalt from init.

Pruned

Unused round-1 lemmas removed: stk/cfg, FR_rounds, FR_push, R1s_z/t, R1s_lz/lt, lev_rounds, chain, run_bite, run_ovf0/2, nh_prog/nh_ev. Jst now uses n mod 2 = 1 (lia-friendly) instead of Nat.odd.

Tactics that worked / failed (round 2)

PITFALL: cbn [ZI] in H does NOT unfold ZI when its body is 1 <= C /\ match r with .. (cbn only unfolds when the head reduces); destruct the conjunction first, then cbn [ZI] iota-reduces the match. Bodies that are a bare match r with (Saf, KI) unfold fine.
PITFALL: cbn in H on a hypothesis with x mod 2 unfolds Nat.modulo into divmod and lia fails; use rewrite Nat.pow_0_r, Nat.mul_1_l in H.
PITFALL: lia does not know L = 0 -> 2^L = 1; add pose proof (pow0 L) to every invariant step.
PITFALL: apply IH unified Ist ?n .. with 0 + n'; change (0 + n')%nat with n' first.
PITFALL: ltac:(lia) inside a term argument okL_ge _ _ ltac:(lia) runs before the evar is instantiated; give the arguments explicitly.
PITFALL: numeral 1 as a nat argument after apply (HU B ..) parsed at sym; write 1%nat.
WORKED: lia with products of variables (x * o, x * 2^L) after substituting 2^k = 3x+1+k mod 2 and rewriting k mod 2 to a constant: the monomials are atoms.

check_kill (round 2, final file)

tools/check_kill.sh <kill file> 1RB0RC_1LC1RB_0RE1LD_0LC1LA_1RF1RA_---0RB: RESULT: PASS, exit 0 (sha256 f61649bdc6b6e97b170ccd8b89a210e50f4714d06d97a352c620e62d712574fc; compile 36.8 s native; coqchk pass 4.6 s; 0 assumptions). Full output: rocq/check_kill_round2.log.