RQ-64-CFOBLIG (#1057): Block/End — WASM half landed, ARM obligation stated with its obstruction kernel-pinned (done-when branch B)

[avrabe]

RQ-64-CFOBLIG (#1057) — done-when branch B, taken deliberately

The artifact's done-when has two acceptable branches: a kernel-checked Block/End correspondence obligation reflected semantically in proof-inventory.json, OR the obstruction stated precisely enough to be VCR-ISA-001 input — with no existence-only theorem named *_correct. This PR takes branch B, and lands the half of the obligation that was never blocked.

Why B. The correspondence cannot be discharged against ArmSemantics.v as it stands, for reasons that are now kernel-checked facts rather than sentences. The fragment that IS statable today (forward, void, index-granular) would be blind to every closed control-flow miscompile (#483, #500, #509, #740, #930) — a green Qed there is exactly the overclaim the artifact forbids, so it was deliberately not written.

What the kernel checked (bazel test //coq:verify_proofs: rocq_proofs PASSED executed after each step, vcr_sel_rules_coverage PASSED; 630 -> 645 Qed / 2 Admitted, zero admit., nothing named *_correct in the new files)

1. WasmInstructions.v gains Block / Loop / Br : nat / End_, one constructor per shipped WasmOp variant in the FLAT op-stream form the compiler consumes. End_ only because End is a reserved Rocq keyword. exec_wasm_instr declines all four via its catch-all; compile_wasm_to_arm (the one exhaustive match the addition broke, per the kernel) gets LOUD-DECLINE [UDF 255] arms with the reason written down.
2. WasmBlocks.v, 11 Qed, WASM-only by design. split_block (nesting-aware scan to the matching End_), unwind_to (a taken branch restores the target block's entry stack — br is stack-polymorphic, the arity-0 half of the Direct selector miscompiles value-returning br_table — carried value dropped (affects --relocatable/shipped path) #509/thumb-2: br/br_if out of an if is not taken when its value operand is a block that branches (labels.wast) — silent wrong value, exit 0 #930 value class), the fuel-bounded structured executor exec_wasm_blocks (Block consumes WBranch 0 and resumes after End_, Loop re-enters, deeper branches propagate decremented, Br is an unconditional WBranch, a stray End_ is None). exec_wasm_blocks_structured_free proves it IS exec_wasm_seq on programs without the four constructors, so the executor every existing theorem and brif_correct are stated against is unchanged by construction. Computed non-vacuity: the SAME block, differing only in the branch constant, lands with an unwound empty stack or with a 7 on top; a counting loop reaches local 0 = 0; with fuel for one pass it declines rather than reporting a one-iteration result.
3. BlockEndObligation.v, 4 Qed, NO correctness theorem. Model-gap pins, each of which stops compiling when VCR-ISA-001 closes its gap: exec_program_pc_B_not_taken / _BL_not_taken (the index executor runs an unconditional branch / a call as a fall-through, writing only the PC register), exec_program_pc_bcond_backward_falls_through (for off < 0 the taken and not-taken targets coincide), and arm_count_loop_body_runs_once (ADD;CMP #10;BNE -3 from R0 = 0 exits with R0 = 1 under exec_program_br — where WasmBlocks.v's executor iterates).

The obstruction, as VCR-ISA-001 input (file header, coq/STATUS.md section, roadmap entry)

#	Obstruction	Evidence	Would have missed
O1	exec_program_pc intercepts only BCondOffset; B/BL write the PC REGISTER while the executor advances its INDEX — two disjoint program counters. Shipped Br = B label; gale's 31 Call rows share the shape	kernel lemma	every br, every call
O2	pc + 1 + Z.to_nat off, off < 0 -> pc + 1: a loop back-edge is a silent fall-through; fuel assumes forward-only	kernel lemma + concrete loop	every loop
O3	model pc is an instruction INDEX; arm_backend.rs resolves labels to BYTE offsets by summing the real encoder's sizes (Label = 0 B) until 16/32-bit widths converge	measured in the shipped resolver	#483 (mid-instruction landing), #740 (halved B<c>.W)
O4	state_correspondence (Compilation.v:692) is defined and used by ZERO theorem statements; every Qed is one instruction under fixed-register hypotheses	grep: 1 definition / 0 statements	anything spanning a block body
O5	the arity-1 join register is chosen lazily at the first branch edge (result_reg, edge_value_move); End emits a MOV only then — an atomic compile_wasm_to_arm End_ = [] would be the #1021 popcnt shape	measured in select_with_stack.rs	#509, #930

Supply list, in dependence order: (a) a byte-addressed executor with an encoder-derived size function admitting negative offsets, in which B/BL/BCondOffset are all executor-visible — O1, O2, O3 are ONE decision, not three; (b) step-counted fuel and the re-check of every exec_program_pc site (ArmSemantics 20, CorrectnessI32 27, CorrectnessBrIf 11, Compilation 1); (c) a simulation relation preserved across instructions; (d) blocktype arity and the join register in the model.

Reflected semantically in proof-inventory.json

Block/Loop/Br/End move from unmodeled to absent (modeled, unproven): summary modeled 138 -> 142, unmodeled 141 -> 137, absent 0 -> 4; qed 138 and result_correspondence 63 unchanged; the BrIf row byte-identical. One tier up, still uncovered for a consumer — nothing in the row can be read as coverage.

The join gained its ONE Rocq-keyword escape (End_ -> End). Red-first: the unpatched generator refused End_ with exit 1 on this tree. constructor_op strips exactly one underscore from a stem in ROCQ_RESERVED_WORDS = {End} and nothing else — Foo_ still refuses, so the escape cannot grow into the alias table the join exists to forbid. scripts/test_proof_inventory.py (7 tests) drives both branches plus the real tree's rows and is wired beside the freshness check in the claim-check job.

Ledger and docs moved together

claims.yaml: rocq_qed 630 -> 645 (with CLAUDE.md and coq/STATUS.md), "modeled": false 141 -> 137, and new SYNTH-BLOCKEND-OBSTRUCTION-1057 — exactly 4 Qed in the obstruction file, zero *_correct names and zero admits across the two new files, exactly 4 absent rows, the decision quoted from STATUS.md. Mutation-verified, each planted then restored: a planted Lemma planted_block_correct -> red; a planted extra Qed. -> red (the fields-equal cross-check caught it independently); the End row hand-flipped absent -> qed -> red (derived 3 != documented 4); restored -> 62/62 hold.

coq/STATUS.md: dated header entry, Total 645 / 2, per-file rows, the DSL-coverage control-flow row corrected (br_if is model-only via brif_correct; the pinned DSL-served total untouched), and a new "Block/End correspondence — obligation stated, obstruction pinned" section. artifacts/verified-codegen-roadmap.yaml: VCR-ISA-001 gains the dated input paragraph (no moving Qed figure cited; S-rule citations unchanged at 34). RQ-64-CFOBLIG.yaml: proposed -> implemented on branch B, verified-by written from measurements, names no PR and no live pinned value.

Gates re-derived on the merged tree (after rebasing over #1186)

claim_check.py claims.yaml 62/62 · proof_inventory.py --check 0 · test_proof_inventory.py 7/7 · status_evidence_check.py 0 failures, 7/7 window commits attributed, floor-prose restated 0 times · oracle_wiring_check.py 0 · rivet validate 40 cross-repo errors with AND without the roadmap paragraph, 0 ours under CI's filter · bazel test //coq:verify_proofs 2/2.

Not claimed

Any Block/End correspondence with ARM code; value-carrying blocks; If/Else/Return/BrTable/Call (unmodeled rows, unchanged). Deferring the ARM half a second time, now with the obstruction kernel-pinned, is the outcome the artifact named as acceptable.

Refs #1057

🤖 Generated with Claude Code

https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L

[codecov]

Codecov Report

✅ All modified and coverable lines are covered by tests.

📢 Thoughts on this report? Let us know!