C2-552 Rocq log

Compile helper: rocq/cc.sh <file.v> [no|yes] (temp dir, bb6 flags, ulimit -s unlimited; ulimit -v 8000000, refuses when MemAvailable < 10 GB or more than one other coqc runs). Capture tool for words in the mirror convention: rocq/tools/mcap.py "<tm tokens>" L R (prints IN/OUT/BACK/RET crossings of tm cells L and R with the near-first words that segRR/segLL/segRL expect).

Round 1 (2026-10-12)

Design decision: hybrid engine instead of hand-written structural rules (changes plan section 4)

Measured on the real run (scratchpad scripts, numbers reproducible from work/fast.py): - 53,973 structural increments; 53,805 batches. - Carry paths of the structural increments contain 88.1M wall/gap tokens in total (max config 2,990 tokens). - Event unit: U0 in 25,150 increments, U1 in 26,179, others ~5k; the event unit's marker count summed over all structural increments is 19.9M (max k = 1,342).

So: - The plan's call1 needs ~15 structural lemma families (glue, unglue g=1/g>=2, absorb, edge1, U0-1111, U0-stop, resets, glue-after-unglue) plus canon re-cut lemmas. That was the plan's risk #1 and #2. - A purely generic run-length simulator (busycoq Sk1Tape.Runs + RunMachine.raw + Sk1 scans) needs no structural lemmas but would take ~1e9 macro steps (88M tokens x ~10 steps): too slow. - Chosen (B'): generic engine on RunMachine.config for tmf (Sk1Tape/Sk1Check machinery: raw steps, scans with context), plus verified macro rules that skip a whole standard unit (unit segRR/segLL/segRL) or a whole passive block (block segRR/segLL), plus auto_bulk at the root (the batch). Structural events then need no lemma at all: the event unit is simulated by raw steps + scans + block macros (cost ~ sum of k of event units ~ 20M macro steps, plus ~25 unit macros per structural increment). Opening (342 steps) and the halt itself are also done by the engine (RM.raw returns None = halted). - Untrusted proposals (parse of the Runs into unit records, batch size d) need no proofs; every use is checked by Runs.remove-style word removal (Sk1Check.remove_cells pattern) whose spec is generic.

Call protocol, block level (found with mcap.py, confirmed by solve_seg)

Mirror machine tmf, words near-first. A unit (root-first) = prefix ++ lead ++ x-gap ++ boundary, where prefix = Y block (y gap + last passive) followed by the chain of passive blocks (gap + stack), all of shape blk m j = [0] ++ [1;0]^^m ++ [1] ++ [1;1;1]^^j; k=1 digits have an empty prefix. - Y block: out B->F, back D->D. Chain blocks: out F->F, back D->D (LL cuts are shifted 2 cells root-ward; this is what lbw m j = [0;1;1]^^j ++ [0;1]^^(S m) encodes, and cmid_shift re-associates). - Lead 1111 (= blk a 1): out F->F (or B->F for k=1); back A->D. Lead 00 stop: F->D (B->D for k=1). - x gap + boundary 11 after a 1111 lead: out F->B, back D->A, word unchanged. - U0 far region (x gap + edge 1^(3f)), e = 0 mod 3: side F->D, edge f -> f+1. - Unit level: in B, out B, back D, return D (hB/hD, h = [(hB,hD)]), as in the plan.

Proved (rocq/dev/core.v, compiles in 2.5 s, -native-compiler no, all by solve_seg/es + list algebra)

• composition: segRR_app, segLL_app, segRR_RL_LL, segRR_sideRL_LL, segRL_frame.
• blocks: blkRR_F, blkRR_B, blkLL, sweepLL, leadLL, xbRR, xbLL, leadstopS, leadstop0, stop1, edge0L, edge0L0, edge0E.
• chains: chainRR, chainLL (induction over the list), cmid_shift, bmid_S, prefRR, prefLL.
• unit touches: stopK (k>=2 stop, any m1 incl. 0), stopK1 (k=1 stop), passK (k>=2 pass, plain boundary), passK1 (k=1 pass), halt0 (k=1 lead 00, fuel 0: halts).
• U0: u0L (leadless U0 + edge overflow, any x incl. 0), u0E (empty U0 + edge).
• root: root_in/out/step/steps (from the prototype), root_halt.
• records: dg (pre = option (Y gap, Y stack, chain); bit; da; dx; dgl), dword, touch1, touch1_spec, iter, iter_spec (n touches as segRLs (h^^n) (h^^p)), u0r (U0L | U0E | U0X opaque), u0iter_spec, batchn, batchn_spec, batch_root (whole batch at nat level: root t (...) -->* root (n+t) (...)).
• closed-form basis: iter_app, iter_pairsK (k>=2: 2q touches from bit 0 = c-2q, a+q, x+q, q forwarded), iter_pairs1 (k=1: a-q, x+q, q forwarded).

Next (round 2), in order

1. N-level closed form for iter (digits: from bit 0, n = 2q + r: c -= n, a += q (k>=2) or a -= q + r (k=1), x += q - r, bit = r, forwarded q; from bit 1 do one pass first; guards as in rocq-plan) with closedN_spec : closedN n d = Some (d',p) -> iter (N.to_nat n) (toNat d) = Some (toNat d', N.to_nat p), proved by induction on q (pairs lemma) + case split. Same for u0iter (trivial closed form).
2. Pieces representation: a unit word as a list of (word, N) pieces; generic remove/push with spec (copy Sk1Check.remove_cells/push_cells); dword (toNat d) = pieces_word (dpieces d).
3. Engine: advance = (at root: proposal d -> batch) | unit/block macros | scans | RM.raw. Sk1Machines.vo does not exist in vendor/ (and vendor/ is read-only), so check_kill would reject Require Sk1Machines: copy Sk1Tape.Runs, RunMachine (raw/raw_spec), Sk1Check (orient, scan_stacks, use_scan, remove_cells/push_cells) into the kill file ("adapted from verify/Sk1Machines.v"). Eqb.vo, LongitudinalHalt.vo, Flip.vo exist (N_iter_until_spec, sideRLs_halt, flip_halts_iff). Scans needed (brute force, scratchpad tmf.py): A/L, B/L, D/L over [0;1]/[1;0]; E/R, F/R over [1;0]/[0;1]; 1-walls: E/R and F/R over [1;1;1], B/R over [1;1;1] with context, D/L over [0;1;1], A/L over [1;1;0] (verify each by shift_rule + es).
4. Untrusted parse (Runs -> unit records) and batch-size proposal (fast.py event_touch/first_inc).
5. Test on prefixes with vm_compute/native (the checker itself is the mirror), then the full run.

Open questions

• Internal empty units: a capture shows an empty unit [y] with plain boundary is NOT a single call-transparent segment (B in, B out, D back, A ret, then F in again). Check whether they occur in batches (rocq/tools/shapes.py, ~3 min; also counts batched digits with m1 = 0 and U0 shapes); if they do, they need their own lemma (or a batch guard that excludes them).

Round 2 (2026-10-12)

Design change back to structured records (supersedes round 1's hybrid engine)

• rocq/tools/kinds.py (full run, ~5 min) classifies every touch of the 53,973 single increments by the lemma family it needs. Event units are mostly U0 (leadless, Pascal rows, k up to 1,342); a generic engine would pay O(k) macro steps per event (sum ~2e7). Records pay O(1) (O(k) list append for unglue).
• Key fact (found with the probe tactic, rocq/r2/probe_hdr.v): in the mirror every touch of a unit consumes the two root-most cells [0;1] of the unit word ("all passive walls move 2 cells root-ward"). So with uw bs b a x far = cw bs ++ leadw b a x ++ far (bs = passive blocks root-first, blk c j = gap 2c+1 then 1^(3j+1)) every family is consume of a block list: c>=1 -> c-1; c=0 -> glue (overhang [1;1;1]^^j into the root-side boundary, re-cut = tailw g ++ [1;1;1]^^j = tailw (g+j)); bs=[] (k=1) -> the lead's own gap a-1.
• Families (all proved, rocq/r2/A1.v A2.v, compile 7 s): t_stop, t_pass, t_ungl1 (bs ++ [(a,1)], new lead lead0 (S x) 1), t_ungl2 (bs ++ [(a,1);(x,g-1)], lead0 0 1), t_halt, z_lead (leadless U0 + edge), z_empty, z_absorb (edgew 0 (S f) -> [1;1] ++ [1;1;1]^^(S f)), z_stop (U0 digit, class-1 edge), z_1111 (U0 digit lead 1111 + edge1: bs ++ [(a,1);(x,f)], new edge 111), reset1 (root with 1^5 tail -> NT), reset1_halt, reset2 (NT -> root 0). Generic composition: gen_RL/gen_RLg, gen_fwd/gen_fwdg, gen_side/gen_sideg (prefix out B->F, core in F, prefix back D->D, glue variant via prefLL_glue); B-entry cores coincide with F-entry cores (checked per core).
• N-level: unitN/zN/tailN/cfg, consumeN (+spec), touchN (+ stop/pass/halt specs) compile (rocq/r2/B1.v).
• Call/increment layer (rocq/r2/B2.v): ztouch (+ret/abs specs), callN (+callN_ret, callN_halt), inc1 (+inc1_ok, inc1_halt) incl. reset1/reset2. Batch layer (B3.v, B4.v): pairK, pair1, clK0/clK1/cl10/cl11, closedU_spec, zLs/zEs, closedZ_spec, batchL_spec, propose (untrusted), batch_step_spec, next_spec, check_spec.
• Python mirror rocq/tools/coqmirror.py (same functions as the Coq checker): from cfg342 it matches rules3/fast at all 107,778 checkpoints (every batch and single step), then IHalt at iteration 107,781 = during increment 11,631,266,794,472,450,654,093 (the predicted one). One bug found by it before Coq: the bit-1 closed form is x + q + 2 - rb, not + 3.
• Coq run: vm_compute of check 107780 = false, check 107781 = true, 31 s each; init (342 steps) by solve_init. The kill file (header, A0..B4, init, halt_tmf with check_spec 110000 + vm_cast_no_check, halt via flip_halts_iff, rule-table comment) compiles in 38 s with -native-compiler yes, 0.5 GB.
• Sources: rocq/r2/{A0,A1,A2,B1,B2,B3,B4}.v + H0.v (header) + Z0.v (run + footer); the kill file is their concatenation (cat H0.v A0.v A1.v A2.v B1.v B2.v B3.v B4.v Z0.v).
• check_kill run 1 (single check_spec 110000 + vm_cast): every check PASS (compile 39 s, tm, theorem, isolation, assumptions = functional_extensionality_dep only) except coqchk: "Fatal error: out of memory" after 346 s under ulimit -v 8000000 (an error, not a timeout, so FAIL under policy A). Log: rocq/check_kill_r2.log.
• Measured kernel (Qed-time lazy conversion) cost of a prefix: 3,000 iterations 1.4 s/+90 MB, 20,000 iterations 20 s/+650 MB (memory grows with the length of one conversion problem). Forcing all changed fields each iteration (rocq/r2/F1.v, not used) only saved ~15% memory and cost 35% time.
• Fix: the run is split into 22 chunks of 5,000 iterations: Definition k_i := Eval vm_compute in unl (run 5000 k_{i-1}), Lemma s_i: run 5000 k_{i-1} = inl k_i by vm_cast, last s22: run 5000 k21 = inr tt; run_ok, run_halt (N_iter_until_spec) chain them. Compile 69 s, 0.58 GB. Sources rocq/r2/H0.v + A0..B4 + Z1.v.
• check_kill run 2: RESULT: PASS, exit 0 (rocq/check_kill_r2b.log; file sha256 95335b49...515c). Compile 69 s (-native-compiler yes); Print Assumptions halt = functional_extensionality_dep only (baseline); coqchk finished and passed in 508.5 s (so the vm_cast chunks are re-checked by the independent kernel; coqchk RSS stayed 0.5-1.0 GB). 508 s is close to the 600 s coqchk cap: larger chunk costs would turn it into a (policy-A-tolerated) timeout.
• Open: machines//proof.md does not exist yet (the .v header refers to "the accompanying write-up (proof.md)"); status.json/STATUS.md not updated by this round.