Rocq log: 1RB0RE_1LC0RE_1LD0LD_1RA0LC_1RA1RF_1RA--- (#33)
Round 1 (2026-10-10): check_kill PASS
Kill file: machines/1RB0RE_1LC0RE_1LD0LD_1RA0LC_1RA1RF_1RA---/1RB0RE_1LC0RE_1LD0LD_1RA0LC_1RA1RF_1RA---.v
(669 lines, sha256 de6bda6c8bb3503ad05411dfd417cfd70a4d047eafb6fa9f59513284c107ce22).
check_kill: exit 0, RESULT: PASS -- this is a kill; compile 11.4 s (native on), coqchk -norec pass in 2.2 s,
0 assumptions. Full record: rocq/check_kill.out.
How it was built (route (a) of proof.md section 6, the scripted mirror of kill #11):
1. rocq/plan_check.v (prepared earlier, unchanged): tm, S1-S6, T1-T14, rot01/rot10, fin, Lb/Lf/Rb/Ro,
dg/dr/app_ds/R0/K, init : c0 -->* K [d1 1 3] 4 1 (solve_init, 215 steps).
2. rocq/port_part.v (new, this round): the rest of #11's machine part, mirrored by hand with the
dictionary l {{q}}> r <-> r <{{pi q}} l, l <* x <* y <-> y *> x *> l, list literals unchanged:
- map1, map0, Oz, Oout verbatim from #11;
- rw is now a left-side accumulator rw ((u,v)::t) l = rw t (l <* [1;1] <* [1;0]^^v <* [0;1]^^(S u)),
ro_out a right-side builder ro_out ((u,v)::t) r = [0;1]^^v *> [1;0]^^(S u) *> [0;0] *> ro_out t r;
- LbS : l {{E}}> app_ds r (map1 os) -->* rw os l {{E}}> r,
RbS : rw os l <* [1;1] <{{D}} r -->* l <* [1;1] <{{D}} app_ds r (map0 os),
RoS : rw os l <{{C}} [0;0;0] *> r -->* l <{{C}} [0;0;0] *> ro_out os r (same induction scripts as #11);
- Ozeq : [1;0]^^u *> [0;0] *> ro_out t r = app_ds r (Oz t u);
- chunkA (es), chunkC (follow S5/T8/S1, fin), chunkO (#11's follow chain verbatim; the explicit S6
instance mirrored to S6 (0inf <* [1;1;0;1]) ([1] *> [0;1]^^a *> [0;0;1] *> r) (S (S (S b))));
- M_spec, Mdrop_spec, O_spec: #11's statements verbatim, #11's proof scripts with dl->dr,
L0->R0, plus unfold R0 before follow T9 in O_spec.
All of it compiled on the first try (plan_check + port_part: 1.8 s).
3. #11's abstract part (lines 268-656 of #11's .v) verbatim, with Lemma step renamed macro_step
(avoids shadowing TM.step), then #11's nonhalt with the base K [d1 1 3] 4 1 (as in abstract_check.v).
Full file: 9.7 s with -native-compiler yes in the scratch compile; check_kill PASS on the first run.
Nothing failed this round. No hand-written arithmetic or invariant work was needed: the abstract part is byte-identical to #11's apart from the rename.
Packaging (2026-10-10)
Fresh tools/check_kill.sh run for the submission, 2026-10-10T17:49:20Z, same sha256 de6bda6c…: PASS, compile 9.7 s
(native on), coqchk -norec pass 1.8 s, 0 assumptions (submission/check_kill.txt). The independent audit's run (17:46:58Z)
gave 9.9 s / 1.9 s. Diff of the abstract part (Open Scope nat_scope .. Lemma nonhalt) against #11's .v: only the
step -> macro_step line differs. No tactic work.