/machines/1RB0LE_1RC---_0RD0RB_1RE0LA_1RF0LF_1LD1RF/rocq/plan.md · raw

W6-1 formal plan (2026-10-14)

Machine: 1RB0LE_1RC---_0RD0RB_1RE0LA_1RF0LF_1LD1RF, the SOBCv10 table mirrored and renamed, started in SOBCv10's state D.

This page says what is now in Rocq, what is only stated, and what the rest costs.

Files

All paths are under machines/1RB0LE_1RC---_0RD0RB_1RE0LA_1RF0LF_1LD1RF/rocq/.

file what it is
W61Exit.v the exit, fully proved (366 lines, no Admitted)
W61Plan.v the planning file: the open statements (4 Admitted) and the proved composition
cc.sh build script: copies a file into build/ and compiles it with coqc 8.20.1
build/ the unmodified copy of SOBCv10.v used as a library, .vo files, compile logs
gen_exit.py Python check of the step counts and output words used in the base lemmas

The library is the upstream SOBCv10.v, copied unchanged from vendor (commit 0940bb9, identical to upstream cdaf693). It compiles in 84 s using 0.8 GB.

Build commands:

rocq/cc.sh SOBCv10     # 84 s, 0.8 GB
rocq/cc.sh W61Exit     # 2 s
rocq/cc.sh W61Plan     # 2 s

What compiles: W61Exit.v (no Admitted)

Everything is in SOBCv10's frame, on SOBCv10's table.

lemma line content
raw_tail_base 49 T2 base, k = 0..5: B U^(2k+1) B t → 101, U^(2k+3) y_k (98 to 910 steps each, left side never read)
raw_tail_column 59 T2 for one column B^(e+1), by induction on e
raw_tail_columns 93 T2 for any column layout: each column B^(e+1) becomes E^e A, the last becomes E^e, and the tail becomes U^(2k+3) y_k
cycler_step 129 Lemma C: L Y B> 0^∞ → L 100 Y B> 0^∞ in 919 steps, for every L
cycler_nonhalt 135 C as a nonhalting statement, for every L
overflow_base 144 Lemma O base: B U^13 B t → 1010 Y B> 0^∞ in 1208 steps, left side never read
overflow_column, overflow_columns 152, 163 O for any all-B layout with tail U^13 B t
exit_nonhalt 182 O + C: such a configuration never halts, whatever is on its left
pre_rotate_list, nested_pre_left 198, 214 the trigger's 101 plus the finished calls is an exception pre-state whose far end holds the pending calls
launch_far, relaunch_far, relaunches_far 227-257 SOBCv10's launch and relaunch lemmas with any far end
nested_launch 272 E′ → E″ launch: from the nested pre-state, h calls through the counter, then the next call leaves
E_to_B, nested_counter 288, 319 E′'s counter word runs to all B in nested_required es e calls, with no carry into the tail
nested_exit 340 the whole exit: from exception 9's trigger configuration (c pending, f finished, tail U^11 B t), if nested_required es e <= f then the machine never halts

Print Assumptions nested_exit gives only functional_extensionality_dep, which the kill baseline already allows. exit_nonhalt is closed.

What is stated: W61Plan.v

There are four open statements (Admitted).

statement role
tail_round the tail-aware round lemma: one SOBCv10 round with the far-end tail carried along, no trigger
tail_round_trigger the same round when the decode triggers (exception 9, k = 4), ending at nested_exit's configuration with nested_required es e <= f
opening from the blank tape (state D) to the entry state: exceptions 1-5, families (a)-(d)
entry_pre the round precondition at the entry (concrete numbers)

The rest of the file is proved, given these four:

Print Assumptions nonhalt lists exactly the four open statements (plus functional_extensionality_dep). So the remaining work is exactly those four.

The round lemma, as stated:

tail_round current previous zs last k lv :
  tail_round_pre current previous zs last k lv ->
  ~ tail_triggers k last lv ->
  exists zs' last' lv',
    post_ca_tail (round_post_unary current previous)
                 (round_primary_width current previous) zs last k lv
    -[tm]->+
    post_ca_tail (round_post_unary next current) (round_primary_width next current)
                 (z_column previous :: zs') last' (S k) lv'
    /\ tail_round_pre next current (z_column previous :: zs') last' (S k) lv'
    /\ length last' = pred (length last)
    /\ eff_level last' lv' = k + 1 - eff_level last lv
  where next = tail_next_index current previous zs last lv

The parameters round_post_unary, round_primary_width and z_column are SOBCv10's own. The layout is SOBCv10's post-C/A word with the last column split off as a signed-digit word, followed by U^(2k+1) y.

The precondition tail_round_pre is a draft: SOBCv10's column safety, head parity and width dominance, a value window for the last column, k ≤ 4 and lv ≤ 5. It holds at the entry by hand, and it is consistent with the four rows of proof.md section 4. Fixing it exactly is the first task of stage R1.

Remaining work, in 2 h stages

The estimate is about 10 stages (range 9-12).

stage work SOBCv10 parts to copy and generalize
R1 Fix tail_round_pre. Counter phase post-C/A → trigger with a tail: frontier counts for a signed last column plus the tail digit (levels via hash_A, sobc1_B_blank, hash_E, hash_D). columns_frontier_count, binary_columns_to_frontier, post_ca_to_frontier (lines 1715-1860, 2300-2356)
R2 T1 as an identity (trigger hash = 5·2^W − V) and the raw pass with the tally (exception_columns_raw_to_pre with a tail, using raw_tail_columns). all_A_widths_finish, all_A_widths_to_exception, round_frontier_exception_equation (2357-2426, 3027-3070)
R3, R4 T3, the decode: n hashes into the raw-pass word give SOBCv10's output columns, the last column with one digit fewer, and the tail at level k + 1 − L (or a deficit in the last column). Arithmetic: n = n_s + (2 − L)·2^(W−1) against round_output_required. mixed_columns_spec, columns_step_required, odometer arithmetic, round_output_required (1373-1433, 2539-3020)
R5 exception_done_to_next_post with the tail in rest (its rest is already arbitrary), and keeping tail_round_pre: width dominance with the larger n, column safety for four rounds, head parity. Closes tail_round. exception_done_to_next_post, round_width_dominance_step, columns_step_exists (3159-3310)
R6 tail_round_trigger: the exception-9 decode up to the trigger hash, the closed form of nested_required, and h″ − 1 ≤ h_t − 1 (margin (5/2)·2^W). the decode from R3-R4
R7, R8 opening and entry_pre: exceptions 1-3 (small), exception 4 by family (a) for general m, cd, family (b) by induction on p, (c) = T2 with k = 0 (done), (d) by induction, then the entry's numeric facts. the pattern of sobc1_c0_to_entry_post (3867-4227); the left-emitter and C/A batches unchanged
R9 One self-contained kill file: SOBCv10's 4,234 lines inlined (no .vo of it exists in vendor), then ours. check_kill, coqchk, public write-up. all

About 3,000 of SOBCv10's 4,234 lines are reused unchanged: the rules, the exception and left-emitter machinery, the C/A batches, and the z-column and abstract schedule theory. About 800-1,200 lines are copied and generalized: the frontier counts, the raw pass, the decode and odometer arithmetic, and the round composition. New code: the opening (about 600-900 lines), and the exit, which is done (366 lines).

Induction and proof shape

Risks

risk where mitigation
The T3 decode with a deficit (D/E digits left in the last column) does not fit SOBCv10's odometer lemmas, which assume A/B digits. R3-R4 Only rounds 7 and 9 start with a deficit (1 and 2 levels). If the general lemma is costly, prove the four rounds' last-column decodes as explicit lemmas instead.
The draft precondition is too weak or too strong at one of the four rounds. R1, R5 The numbers of all four rounds are known (proof.md section 4). Check each field against them before proving.
Families (b) and (d) at p = n4 are closed forms checked only on small cases (11 and 9 pairs). R7-R8 Exceptions 1-4 are exact (hash-level run) and (a) is exact at m = 30. An off-by-one would change only constants, not the route (the robustness argument, proof.md section 6).
Kill-file size and compile time. R9 SOBCv10 alone compiles in 84 s using 0.8 GB, and our parts in seconds. The base lemmas are at most 1,208 direct steps, far below coqchk's limits.
Effort overrun. all Stop and re-ask at the end of R4 if T3 is not closed.

Not at risk: the exit. O, C, T2 (k = 0..5) and the nested launch are proved in Rocq, and nested_exit closes the run from exception 9's trigger to the cycler.