W5-5 halting proof: formalization log

Round 1 (2026-10-13)

Plan followed: rocq-plan.md (C2-552-style checked certificate runner, no flip, generic run-length macro simulator with concrete N counts). ES_v3 was not needed: the own simulator and its soundness proofs compiled on the first full attempt after five small proof fixes.

Files

• dev/W55.v: the whole verified development (rounds, digits, batch arithmetic, macro simulator, K-form parser, urun, checker next, run_ok/run_halt, init, literal decoder mk). 3.2 s, Print Assumptions run_ok/init: Closed under the global context.
• dev/build.sh: slot-waiting compile (pgrep -c coqc <= 1, MemAvailable > 10 GB, ulimit -s/-v, project flags).
• gen/ext.v: OCaml extraction of next etc. (scratch only; Extraction is forbidden in the kill file).
• gen/w55inst.ml(i): the extraction plus a macro-step counter (side effect only); gen/driver.ml: full run with statistics; gen/dprof.ml, gen/w55prof.ml: profile counters; gen/gen.ml: chunk generator (writes Definition k_i := mk [...] b c. / Lemma s_i: run T k_{i-1} = inl k_i. Proof. vm_check_eq. Qed. and the halting chain h_i, halt).
• test/assemble.py + test/header.txt + test/footer.txt: build the kill file from dev/W55.v and the generated part. test/Pre3.v, test/Pre30.v: prefix tests (reach k3 / k30 from c0).
• ck.sh: slot-waiting tools/check_kill.sh --halt wrapper, logs check_kill_r1.log.

Design as built (differences from the plan)

• krec = (w : sd, b : N, c : N); the counter word is kept as a run-length side (no flat word, no re-encoding). kden (w,b,c) = K (sdn w) b c; kcfg pushes the boundary 0 onto w and builds the bell as 4 runs.
• Batch: split 16 w takes up to 16 clean digits from the low end (pop3 pops a whole 3-cell block from a run; past the end of w the 0inf tail gives D0 digits, so padding is automatic), propose = min b (maxv - val D), addn adds n digit by digit (Z, small numbers), pushd pushes the new digits back with block merging; push_block drops all-zero blocks pushed onto an empty side (u^^n *> 0inf = 0inf).
• rounds needs no bound hypothesis: val ds' <= maxv |ds'| (val_le_maxv) gives it; n = 0 by val_inj.
• Eat: urun 1 (first K-form with b >= 1); oracle round: urun 0. FUEL = 65535 (max needed 12,954).
• pop skips empty blocks / zero counts (sound for any sd), push folds 3 singletons into a following equal run and 6 singletons into a run of 2 (as the Python mirror).

Results

• Extracted run (OCaml native, 72 s): HALT at iteration 4,942,482 from k0 = K 0inf 0 2; the halting iteration's state is w = 001^6 0 1 1 101 (nearest first) = 101 110 100^6 (MSD first), b = 1,211,396, c = 7,437: exactly the predicted halting round start. 611,578 eats (cycles 0..611,577), 2,234,211 batches, 2,096,694 simulated rounds, 300,612,334 macro steps (96% single steps; 852k rule tries per 14M macro steps).
• VM speed: 20,000 iterations (1,157,497 macro steps) in 2.44 s vm_compute = 2.1 us/macro step; the 30-chunk prefix (6.0M macro steps) compiles in 18.1 s with -native-compiler yes (17.7 s with no): about 2.5 us per macro step in chunked casts, so the full run is about 750 s of compile.
• coqchk on the 3-chunk prefix (200k macro steps per cast): 31 s, max RSS 305 MB.
• Kill file: 751 chunks of about 400k macro steps (gen/full400k.v, 218 KB), 2,975 lines; check_kill --text-only: TEXT_ONLY_OK. Full check_kill: see below.

Call-only variant (fallback, not in the kill file): dev/W55b.v

• For a simulated round with b >= 1: enter (E1, F0) + simulate only the counter call from (C, w, ([0],1) :: bellsd b c, DL) until state B, DR with the right side syntactically back to the start (sd_eqb), then round_sim (= enter ; call ; bellpart). Gives up (CFail) when the right side equals the bell alone (the head crossed the boundary, e.g. a counter overflow), then falls back to the full urun 0. Compiles (2.0 s, -native-compiler no).
• OCaml measurement over the whole run: simulated rounds 185.5M -> 137.3M macro steps (16,680 fail-fast fallbacks), i.e. 300.6M -> about 254M macro steps in all (-15%, less than the plan's 30%). Kept in reserve in case the full compile comes close to the 1800 s cap.
• Profile (first 200k iterations): 96% of macro steps are single TM steps (13.6M of 14.2M); 852k rule tries, 7.7M window-simulation steps. A typical round is about 35 macro steps (call ~16, bell part ~17).

Cross-check against the independent model

• gen/eats.ml prints every b = 0 state of the extracted checker (cycle index, c, word MSD first, leading zeros stripped): 611,578 lines (gen/eats_all.txt), byte-identical to columns 1, 3, 4 of work/indep/k0_model_all.txt for cycles 0..611,577 (that file has one more line, its END record). So the checker's cycle starts are exactly the model's K0 states, and its halt comes in cycle 611,577.

check_kill (round 1): PASS

• tools/check_kill.sh --halt on the kill file (sha256 851ca695...60ea92, 2,975 lines, 751 chunks): RESULT: PASS, exit 0 (log check_kill_r1.log). Compile 609.7 s with -native-compiler yes (cap 1800 s; other workflows' coqchk/coqc runs were going at the same time). Print Assumptions halt: closed (0 entries), in-file and isolated. coqchk: timeout at the 600 s cap (policy A warning; RSS about 470 MB, no error). Whole check 1,211.6 s wall.
• Fallback test/KillB.v (call-only variant, 634 chunks) also compiles: 531.8 s under the same load (plain coqc, not check_kill'd). Not needed.