W5-7 1RB0RD_1LC1RE_1LA0LD_0RE0RF_1LC1RA_0LE---: Rocq log

The machine HALTS (proof.md), so the kill statement is Lemma halt: halts tm c0. and the oracle is tools/check_kill.sh --halt (the computed task text said nonhalt; that form is false for this machine).

Kill file: ../1RB0RD_1LC1RE_1LA0LD_0RE0RF_1LC1RA_0LE---.v (top level, no Module). Template: SOBCv6.v Module TM3, copied and adapted. Helpers: rocq/cc.sh <file> <dir> (compile a copy as W57.v under -Q . Dev, ulimit -v 8000000), rocq/chk.sh <dir> <timeout> (coqchk -norec Dev.W57). Work dirs must be unique: the scratchpad is shared with other agents (another agent's Kill.v was in c1/).

Round 1 (2026-10-13)

Done (compiles, 25 s, 0.6 GB, Print Assumptions halt: functional_extensionality_dep only)

• TM3 lemmas copied with the two notations renamed (<| = <{{D}} [0;1;0], |> = {{A}}>, hR := (A,<[0;0;1]), hL := (D,[0;1;0])): LInc_spec, LOv_spec, LIncs_spec, RIncs, Incs, Ov, LIncs_lpow, LIncs_lpow', LOv_lpow. All replayed unchanged on the renamed table, first try.
• New LOv_peel (L4): lpow_shift + LOv_d1_1 + LOv_lpow.
• LD' with W10 (l:nat), W11 (l:nat); Lmp'_W10/W11 at exponent 1+l+n.
• LInc_rec with the new case W10 (S l)::t => Some (W1'::W1'::W10 l::t); spec: cbn turns [W1;W0]^^(1+S l+n) into W1::W0::[W1;W0]^^(1+l+n), then LInc_d0.
• LOv_rec with keep (TM3) and peel cases; the peel's 1+S l0+n is convertible to 1+(1+l0+n), so LOv_peel applies directly.
• LIncs_rec with the count bound in N (upd n m := N.min 256 (2*n + N.of_nat m), upd_le by lia, then Opaque upd in the spec). Spec: n' >= N.to_nat n.
• step_rec (new block = one token W10 n0, N.to_nat n = S n0), step_rec_spec, iter, iter_spec.
• init: P x2' (x2 = 70 words, 38,573 steps) by solve_init.
• walk0, walk1 by es; doomed_w0/w1/pow; far_halt (1,368 steps, r symbolic) by solve_halt.
• doom_rec (equality with x_far' tested first, via a boolean ltok_eqb), doom_rec_spec by induction on a length bound; final_check k, final_check_ok: final_check 192 = true by vm_compute; reflexivity; halt_from k (no computation, k abstract); halt := halt_from 192 final_check_ok.

Tactics: worked / failed

• WORKED: chain timing. iter 192 x2' gives length 38,120 (= proof.md C3); doom_rec z194 = true.
• FAILED (slow): count bound in unary nat (Nat.min maxv (n*2+m), TM3's form) with maxv = 256: 192 iterations took 27 s in the VM. WORKED: the bound in N: 1.2 s.
• FAILED (memory): Definition final_check : bool := match iter 192 x2' with ... end (a closed heavy term) makes coqc with -native-compiler yes use 7.0 GB and +30 s without any Eval (the native compilation step evaluates it; with an Eval in the same file it hit Fatal error: out of memory under ulimit -v 8000000). WORKED: make it a function final_check (k:nat); the lemma final_check 192 = true then costs nothing extra.
• FAILED (hang, killed after 10 min): proving halt with destruct (iter 192 x2') eqn:E1 etc. directly on the concrete term. WORKED: a generic halt_from k : final_check k = true -> halts tm c0 (k abstract, so no tactic can start reducing), then exact (halt_from 192 final_check_ok).
• PITFALL: after inverts, hypothesis numbering differs from TM3's once LD' constructors carry arguments; use match goal with HL: Lmp' x _ |- _ => specialize (IHT _ _ _ E HL) ... end.
• PITFALL: exists [], 0 fails (0 parses in sym_scope); write exists (@nil LD), 0%nat.
• PITFALL: andb_true_iff is not in scope; Eqb redefines && as if x then y else false: use Eqb's and_true_iff.
• WORKED: coqchk. With the N bound the whole 192-cycle check is one vm_compute; reflexivity lemma (final_check_ok), and coqchk -norec re-checks it by plain conversion in 43.6 s at 0.43 GB, so no chunking was needed (a unary-nat bound would have made the lazy kernel do ~1000 reductions per digit).

Result

• tools/check_kill.sh --halt <file> 1RB0RD_1LC1RE_1LA0LD_0RE0RF_1LC1RA_0LE---: RESULT: PASS -- this is a kill, exit 0 (compile 25.7 s, -native-compiler yes; coqchk 43.6 s, finished; assumptions: functional_extensionality_dep, in the baseline). File sha256 30ba9693...6786. Full report: rocq/check_kill.out.
• Open (not Rocq): status.json / STATUS.md not updated by this round (outside this round's files); submission packaging (public write-up from proof.md) still to do.

Packaging (2026-10-13)

• Fresh tools/check_kill.sh --halt on the unchanged kill file (sha256 30ba9693...6786): RESULT: PASS, exit 0 (compile 25.6 s native, coqchk 43.3 s finished, functional_extensionality_dep only). Verbatim output in ../submission/check_kill.txt. status.json set to KILLED_HALT; submission/ packaged (not posted).