Rocq log: 1RB---_0LC1RF_1LE0RD_0RB1RC_1RD0LE_0RC1RA (F3, delta of kill #4)
Formalization round 1 (2026-10-10)
Result: check_kill PASS on the first run (exit 0; compile 6.5 s native, coqchk -norec 2.1 s, 0 assumptions, 9 s wall).
Kill file: 1RB---_0LC1RF_1LE0RD_0RB1RC_1RD0LE_0RC1RA.v, 510 lines, sha256 0c89b5109f87c793105cadaa9b157902254e5b8e33d1f9bc610d76b9f7a43e37.
Full check_kill output: rocq/check_kill.out.
How it was built: python3 -B rocq/make_kill.py (reads #4's .v read-only, asserts its sha256 51e3dea1...e923).
- Header: replaced whole with a house-style header (machine, "Adapted from the proof of ... (kill #4), which is adapted from
verify/SBCv7.v, Module TM4", sigma and start state, the delta, the AI line, the Checked line with "busycoq BB6"
and "Closed under the global context"). Asserts no repo-local path prefix in the output.
- Code: identical to rocq/plan_check.v (verified by diff; only the closing comment differs):
TM string; sigma = EDBCFA on every {{X}} in one re.sub (asserted counts A 37, C 6, E 35; parent uses only A, C, E);
init0 RHS ... bA^^14 <* bB^^4 <* <[0;0] {{B}}> 0inf by esx (16,590 steps); init : c0 -->* CfgF 5 0 14 4
by apply init0; nonhalt index (5,0,14,4)%nat, final unfold Inv. cbn. lia. unchanged (closes the tight facet).
- Closing comment block: sigma line added, <A 001 / 001 E> -> <E 001 / 001 F>, 00 C> -> 00 B> in P/Q, start line
updated (with #4's start for comparison).
Nothing failed. Remaining for packaging (not this round): status.json / notes.md / STATUS.md update, submission bundle.
Packaging (2026-10-10)
- Independent audit (19:23:15Z,
--json): PASS, 17/17, compile 6.9 s, coqchk 2.2 s, same sha2560c89b510…3e37. - Fresh human-readable check_kill for the submission (19:25:05Z): PASS, 17/17, compile 7.0 s (native on), coqchk pass 2.1 s, 0 assumptions. Output:
submission/check_kill.txt(stderr line + stdout, as in #4's package); raw stdoutrocq/check_kill_submission.out. rocq/make_submission_proof.pybuildssubmission/proof.mdfrom the working proof.md (single-match replacements, path scrub, refuses to write on a leftover repo-local path).submission/parent-proof.mdis a verbatim copy of #4's submission proof.md (cited as P§n).- status.json set to KILLED_NONHALT / done. Nothing posted.