docs(#946): Tiers 2+3 honesty sweep — live exclusions re-grounded, selector/CLI docs un-understated, counts re-derived

CLAUDE.md

@@ -150,9 +150,11 @@ frozen and oracle-gated every step:
   #682 model↔selector drift is unrepresentable at the instruction-sequence level
   for those ops (the interim `VcrSelRulesGenCheck.v` reflexivity gate was
   retired as vacuous/subsumed). `VCR-WASM-001` WasmCert-Coq source semantics —
-  phases 1+2 landed: the i32 integer fragment (19 ops) transcribed from the
+  phases 1–3 landed: the i32 (19 ops) AND i64 (22 ops) integer fragments
+  transcribed from the
   pinned coq9.0-wasm-2.2.0 sources with line-level provenance and proven
-  refined by `exec_wasm_instr` (49 Qed, `coq/Synth/WASM/WasmCertBridge.v`);
+  refined by `exec_wasm_instr` (104 Qed, `coq/Synth/WASM/WasmCertBridge.v`;
+  all 22 i64 ops carry both op-level and executor-level refinement);
   real external dep nix-feasible, bazel-deferred (roadmap entry).
 - **Track C (validation):** the differential oracles are CI-gated jobs
   (cmp-select, RV32 shift-fold/const-addr-fold, callee-saved, spill-frame,

artifacts/gale-integration.yaml

@@ -581,7 +581,7 @@ artifacts:
     description: >
       gale #369 reported soft-float for all f32/f64; deterministic diagnosis
       against v0.11.45 showed it is WORSE — a silent wrong-value miscompile,
-      and the drop is at the DECODER, not the selector. `map_operator` in
+      and the drop is at the DECODER, not the selector. `convert_operator` in
       crates/synth-core/src/wasm_decoder.rs decodes the SIMD `F32x4*` family
       (lines 765-780) but has NO arm for any scalar `f32.*`/`f64.*` op, so
       scalar floats fall through the catch-all `_ => None`

claims.yaml

@@ -752,6 +752,9 @@ claims:
     evidence:
       # The straight-line-expansion ceiling — bumped 4→5 after auditing a 3-reg
       # 16-bit PUSH/POP in I64Popcnt (1+3=4 cyc/halfword had zero margin).
+      # #946 re-audit: the priced I64Rotl/I64Rotr fixed-ABI wrappers emit a
+      # 4-register PUSH {R0-R3} (0xB40F), so 5 holds EXACTLY (1+4), not with
+      # margin — a 5+-register 16-bit PUSH/POP in a priced arm would exceed it.
       - kind: count-eq
         pattern: 'const STRAIGHTLINE_CEIL_PER_HALFWORD: u64 = 5;'
         glob: ['crates/synth-backend/src/wcet.rs']

coq/STATUS.md

@@ -242,7 +242,7 @@ umbrella #147).
 | **Infrastructure** | Properties of integers, states, flag lemmas | 65¹ |
 
 ¹ T1/T2/Infrastructure tier classification is the 2026-06-04 semantic recount
-and predates the VcrSelRules (42), VcrSelPilot (7) and SailArmBridge (92) Qed;
+and predates the VcrSelRules (52), VcrSelPilot (7) and SailArmBridge (92) Qed;
 see the per-file breakdown below for current per-file counts. The T3 row and
 the headline total are re-derived by the claim gate.
 
@@ -511,7 +511,8 @@ All fully proved (Qed); no new axioms.
 
 ## Per-File Breakdown
 
-Recount 2026-07-10 (`grep -oE 'Qed\.'` / `'Admitted\.'` per file):
+Recount 2026-08-13, #946 doc sweep (`grep -c 'Qed\.'` / `'Admitted\.'` per
+file; the per-file rows below sum EXACTLY to the CI-gated headline 592 / 2):
 
 | File | Qed | Admitted | Tier |
 |------|-----|----------|------|
@@ -530,7 +531,7 @@ Recount 2026-07-10 (`grep -oE 'Qed\.'` / `'Admitted\.'` per file):
 | ArmFlagLemmas.v | 46 | 0 | Infra (flag correspondence + i64 carry/borrow/shift lemmas) |
 | Tactics.v | 1 | 0 | Infra |
 | ArmState.v | 14 | 0 | Infra |
-| ArmSemantics.v | 8 | 0 | Infra |
+| ArmSemantics.v | 14 | 0 | Infra |
 | SailArmBridge.v | 92 | 0 | Infra (VCR-ISA-001 Sail/ASL bridge: AddWithCarry family + ALU + shifts + moves) |
 | WasmSemantics.v | 6 | 0 | Infra |
 | Compilation.v | 5 | 0 | Infra (#166: `ex_compile_simple_add` + `ex_compile_increment_local` discharged via `vm_compute`) |
@@ -540,8 +541,13 @@ Recount 2026-07-10 (`grep -oE 'Qed\.'` / `'Admitted\.'` per file):
 | WasmCertReference.v | 0 | 0 | definitions only (VCR-WASM-001: WasmCert-Coq i32 AND i64 rules transcribed from the pinned coq9.0-wasm-2.2.0 sources with line-level provenance). PHASE 3 (v0.48, #242): the extra-coq-package bazel/nix HOOK is LANDED (blocker (1) closed) but the REAL dep stays PENDING and this file stays a hand transcription — nixpkgs pin 88d3861a ships wasmcert 2.2.0, which propagates the UNFREE compcert 3.16 (inria-compcert, meta.license.free=false); wasmcert >= 2.2.1 (drops CompCert) not yet in the pin, so the "trusted transcription" caveat is NOT yet retired |
 | WasmCertBridge.v | 104 | 0 | Infra/T1-analogue (VCR-WASM-001 phase 2: 19 i32 ops; phase 3 (#242): 22 i64 ops — add/sub/mul/and/or/xor/shl/shr_u/shr_s/rotl/rotr/eqz/eq/ne/lt/gt/le/ge, each with an op-level refinement Qed against the WasmCert reference, PLUS an executor-level Qed through the real `exec_wasm_instr` for ALL 22 ops. The v0.50 wiring batch (#242) WIRED the six arithmetic/bitwise ops (add/sub/mul/and/or/xor) into `exec_wasm_instr` (pop2_i64 / VI64), closing the former op-level-only residual — plus the i64 encoding/bit-level/rotate-boundary helper Qed) |
 | VcrSelPilot.v | 7 | 0 | T1 (register-polymorphic; VCR-SEL-001 go/abandon measurement) |
-| VcrSelRules.v | 42 | 0 | T1 (register-polymorphic; the WIRED VCR-SEL-001 increment-1+2+3+4 rule table — 40 rule theorems 1:1 with `coq/vcr_sel_rules.manifest`, coverage-gated by `//coq:vcr_sel_rules_coverage`, + 2 mod-32 helper lemmas #683. VCR-ISA-001 #667 increment 2: every `rule_X` is DEFINED as the GENERATED `Gen.rule_X` of `VcrSelRulesGenerated.v` — emitted from the shipped `sel_dsl::RULES` — so the theorems are stated directly about the shipped sequences; a table change regenerates `Gen` and breaks the matching Qed. The former `VcrSelRulesGenCheck.v` 40-lemma `reflexivity` gate is retired as vacuous/subsumed) |
-| **Total** | **585** | **3** | (+2 `admit.`; headline re-derived by the claim gate) |
+| VcrSelRules.v | 52 | 0 | T1 (register-polymorphic; the WIRED VCR-SEL-001 increment-1+2+3+4 rule table — 50 rule theorems 1:1 with `coq/vcr_sel_rules.manifest`, coverage-gated by `//coq:vcr_sel_rules_coverage`, + 2 mod-32 helper lemmas #683. VCR-ISA-001 #667 increment 2: every `rule_X` is DEFINED as the GENERATED `Gen.rule_X` of `VcrSelRulesGenerated.v` — emitted from the shipped `sel_dsl::RULES` — so the theorems are stated directly about the shipped sequences; a table change regenerates `Gen` and breaks the matching Qed. The former `VcrSelRulesGenCheck.v` 40-lemma `reflexivity` gate is retired as vacuous/subsumed) |
+| VcrSelExpansion.v | 29 | 0 | T1 expansion tier (the ten binary I64SetCond rules re-proven against the encoder's dual-precision CMP-lo/SBCS-hi/MOVcc chains — see the 2026-07 executor-upgrade section) |
+| VcrSelRulesGenerated.v | 0 | 0 | generated definitions only (`Module Gen`, emitted from the shipped `sel_dsl::RULES`) |
+| ArmInstructions.v | 0 | 0 | definitions only |
+| WasmInstructions.v | 0 | 0 | definitions only |
+| CompilerExtract.v | 0 | 0 | extraction directives only |
+| **Total** | **592** | **2** | (+2 `admit.`; headline re-derived by the claim gate — the rows above now sum to it exactly) |
 
 ## VCR-SEL-001 increments 1 (2026-07-07) + 2 + 3 + 4 (2026-07-08): VcrSelRules.v
 
@@ -583,8 +589,9 @@ tier: the encoder's CMP-lo/SBCS-hi expansion is below the flat executor,
 see `docs/design/vcr-sel-001-increment-4.md`).
 
 **50 Qed / 0 Admitted**, same T1 bound as the pilot ("the ARM sequence
-computes the named result", not WASM refinement). These 48 Qed (pilot +
-rules) are included in the recount above.
+computes the named result", not WASM refinement). These 57 rule/pilot Qed
+(50 rule theorems + 7 pilot, plus VcrSelRules.v's 2 helper lemmas) are
+included in the recount above.
 
 ## DSL coverage vs model relevance (per-op-family metric, #667)
 

coq/Synth/Synth/CorrectnessI32.v

@@ -1,7 +1,7 @@
 (** * I32 Operations Correctness
 
     This file contains correctness proofs for all i32 WebAssembly operations.
-    Total: 29 theorems — 29 Qed, 0 Admitted
+    Total: 29 theorems + 2 helper lemmas — 31 Qed, 0 Admitted
 
     Strategy:
     - Arithmetic (add, sub, mul, and, or, xor): synth_binop_proof tactic

coq/Synth/Synth/VcrSelRules.v

@@ -12,11 +12,11 @@
     [crate::sel_dsl::generate_rocq_lowering_source] from the SAME shipped
     RULES table that produces the Rust lowering [sel_dsl/generated.rs]).
     There is no hand-written copy of the instruction sequences left in this
-    file — the generated file is the single source for the 40 covered ops,
+    file — the generated file is the single source for the 50 covered ops,
     so the model cannot drift from the shipped selector (the #682
     vacuous-proof failure mode). If the shipped table changes, regeneration
     changes [Gen.rule_X], and the matching correctness theorem below stops
-    compiling: the 40 Qed themselves are the divergence gate (strictly
+    compiling: the 50 Qed themselves are the divergence gate (strictly
     stronger than the retired [VcrSelRulesGenCheck.v] reflexivity check,
     which could only compare against a hand-written mirror).
     The theorems prove the T1 bound carried over from the pilot

crates/synth-backend-aarch64/src/selector.rs

@@ -32,23 +32,22 @@
 //! `grow(0)≡size`, `grow(n>0)`→−1, the #539 rule — growth failure is
 //! §-permitted and keeps the #865 static bounds limit sound).
 //!
-//! **Deliberately still declined (loud-skip, never wrong code) — the
-//! mechanically-derived complement lives in the cross-backend op-parity oracle
+//! **Still declined (loud-skip, never wrong code):** the current decline
+//! complement is MECHANICALLY DERIVED by the cross-backend op-parity oracle
 //! (`crates/synth-backend-riscv/tests/cross_backend_op_parity.rs`, aarch64
-//! leg):**
-//! - `call_indirect`, import calls, `>8` integer args, multi-result or
-//!   float-result callees (returned in v0/d0, not x0), a caller reading its own
-//!   params across a call (param-homing is a later increment), and WRITING a
-//!   parameter (`local.set`/`tee` on a param index).
-//! - register spilling and bulk memory (`memory.copy`/`memory.fill`).
-//! - Float rounding (`ceil`/`floor`/`trunc`/`nearest`), f32/f64 linear-memory
-//!   load/store, i64→float converts, and the TRAPPING i64-target truncations
-//!   (the saturating forms do lower).
-//! - Data-segment init and the startup that establishes the `x28` linear-memory
-//!   base (the load/store lowering is correct given the base precondition;
-//!   wiring it at runtime is a follow-on). OOB accesses TRAP since #865 under
-//!   [`MemBounds::Software`] (the CLI default); `--safety-bounds none` is the
-//!   explicit unchecked opt-out.
+//! leg) — consult it, not a hand list. A hand-maintained list here went stale
+//! twice (#946: it still named `call_indirect`, float rounding, f32/f64
+//! linear-memory load/store, i64→float converts, and the trapping i64-target
+//! truncations as declined after all of them had shipped lowerings in this
+//! very file), so it was deleted rather than re-synced. Two decline facts
+//! worth stating because they are contracts, not coverage gaps:
+//! - Data-segment init: this backend ships NO data section and REFUSES a
+//!   module carrying active data segments loudly (#851, `backend.rs`); the
+//!   startup that establishes the `x28` linear-memory base at runtime is a
+//!   follow-on (the load/store lowering is correct given the base
+//!   precondition).
+//! - OOB accesses TRAP since #865 under [`MemBounds::Software`] (the CLI
+//!   default); `--safety-bounds none` is the explicit unchecked opt-out.
 //!
 //! **#851 — non-param locals:** GP locals beyond the params (index >=
 //! `num_params`) get zero-initialized 8-byte stack slots (`[sp, #(idx -
@@ -266,13 +265,14 @@ fn param_map(num_params: u32, params_f32: &[bool], params_f64: &[bool]) -> Vec<V
 /// (`(param_count, result_count)` of the k-th `Block`/`Loop`/`If` in op order),
 /// used to gate the control-flow increment.
 ///
-/// **Control-flow subset (#538 cf increment):** VOID-result `block … end` with
-/// forward `br`/`br_if` to enclosing block ends. Only `block_arity == (0,0)`
-/// blocks are accepted — a value-carrying (typed) block would need result-
-/// register reconciliation across the branch and is LOUD-DECLINED. `loop`
-/// (backward branch), `if`, and `br_table` are declined by name. This keeps the
-/// straight-line value-stack model sound: nothing crosses the branch, so at each
-/// `end` the value stack is exactly its block-entry height (asserted).
+/// **Control flow:** full since VCR-A64-CF-001 (v0.55) — `block`, `loop`,
+/// `if`/`else`, `br`/`br_if`, and `br_table` (compare-and-branch chain, up to
+/// [`BR_TABLE_MAX_TARGETS`]) are all lowered, including VALUE-CARRYING frames
+/// via the reserved reconciliation-slot construction (see the module header).
+/// The #538-era wording here ("only `(0,0)` blocks; `loop`/`if`/`br_table`
+/// declined by name") described the first cf increment and went stale (#946).
+/// Residual declines live where the lowerings themselves say so (e.g. loop
+/// PARAMETERS, over-threshold `br_table`) — each a loud skip, never wrong code.
 pub fn select_typed_cf(
     ops: &[WasmOp],
     num_params: u32,

crates/synth-backend-riscv/src/alloc_validator.rs

@@ -55,7 +55,9 @@
 //! only manufacture a false-positive (a body `s11` read/def with no save the pass
 //! was never going to add). Unlike the ARM validator, there is NO "unmodeled op →
 //! force prologue" fail-safe: on RV every `op_dest == None` op is control-flow /
-//! system / label / call (none write an `s`-register), so the fail-safe is
+//! system / label / call / store (`Sb`/`Sh`/`Sw` are `op_dest == None` too —
+//! stores write memory, not a register), so none of them can write an
+//! `s`-register and the fail-safe is
 //! unnecessary AND would disagree with the pass (which has none) → false-positive.
 //!
 //! # Documented boundaries (false-negatives, never false-positives)

crates/synth-backend-riscv/src/selector.rs

@@ -10,10 +10,13 @@
 //! Out of scope (see `select_simple` doc comments for the full list):
 //! - sign-extending sub-word i64 loads (`i64.load8_s` etc.)
 //! - F32/F64 (RV32F/D — not yet wired)
-//! - br_table (lowered in B3 alongside jump tables)
-//! - Cross-function calls (need linker-resolvable Call ops + relocations)
 //! - Component Model lifting/lowering
 //!
+//! Formerly listed out-of-scope, since shipped (#946 doc sweep): `br_table`
+//! (#882, compare-and-branch chain up to [`BR_TABLE_MAX_TARGETS`]) and
+//! cross-function calls (direct `call` with linker-resolvable relocations,
+//! #871 — some shapes still decline at their sites, loudly).
+//!
 //! i64 representation: on RV32, an i64 value is held in a *register pair*
 //! `(lo, hi)` where `lo` is bits [31:0] and `hi` is bits [63:32]. The two
 //! halves don't need to be consecutive registers (unlike ARM's LDRD/STRD
@@ -1512,7 +1515,11 @@ impl Selector {
 
     /// Registers currently pinned by a live `vstack` value — exactly the values
     /// that must survive until they are popped, and which `alloc_temp` must
-    /// never hand out.
+    /// never hand out. (One caveat: on pool exhaustion `alloc_temp_avoiding`
+    /// still RETURNS `self.temps[0]` — by construction a pinned register — but
+    /// it sets `alloc_exhausted` first and the caller turns that flag into a
+    /// loud per-function decline, so the pinned register is never silently
+    /// clobbered in emitted code.)
     ///
     /// Most entries are temps, but NOT all: `lower_local_get` aliases a
     /// #472-promoted local's callee-saved s-register directly onto the vstack

crates/synth-backend/src/wcet.rs

@@ -75,18 +75,23 @@ const BL_BLX_CALL_OVERHEAD_CYCLES: u64 = 4;
 ///  - a 16-bit (1-halfword) ALU/shift/mov/cmp/forward-branch is ≤ 3 cycles → ≤ 5;
 ///  - a 32-bit (2-halfword) op — including UMULL/MLA (M3 worst ≈ 5) — is priced at
 ///    2×5 = 10 ≥ its worst;
-///  - a 16-bit `PUSH`/`POP` of up to 4 registers is 1+4 = 5 cycles → exactly ≤ 5
-///    (the audited expansions push at most 3 registers, so this holds with margin;
-///    the i64 software div/rem, which pushes 4, is a LoopedExpansion decline and
-///    is never priced here).
+///  - a 16-bit `PUSH`/`POP` of up to 4 registers is 1+4 = 5 cycles → exactly ≤ 5.
+///    The priced arms DO contain 4-register lists: the #610 fixed-ABI wrappers
+///    around the priced `I64Rotl`/`I64Rotr` expansions emit `PUSH {R0-R3}`
+///    (`0xB40F`, `emit_i64_fixed_abi_entry`) and the matching ≤4-register
+///    restore, so the ceiling holds EXACTLY there, with no margin — the bound
+///    is still sound, but any future 16-bit `PUSH`/`POP` of 5+ registers in a
+///    priced arm would exceed it and must force a re-derivation.
 ///
 /// Hardware `SDIV`/`UDIV` (up to 12) do NOT appear in any priced expansion — the
-/// only i64 division is the looped-expansion decline — so no single instruction
+/// only i64 division is the looped-expansion decline (it also pushes 4 registers,
+/// but is never priced here) — so no single instruction
 /// exceeds the ceiling. 5 cycles/halfword is therefore a sound over-estimate of any
 /// priced straight-line block; the block executes exactly once in a loop-free
 /// function, so summing the ceiling stays sound. Audited against `arm_encoder.rs`
-/// (#778): the only 16-bit `PUSH`/`POP` in a priced arm is I64Popcnt's 3-register
-/// `0xB438`/`0xBC38`.
+/// (#778, re-audited #946): the 16-bit `PUSH`/`POP`s in priced arms are
+/// I64Popcnt's 3-register `0xB438`/`0xBC38` and the I64Rotl/I64Rotr fixed-ABI
+/// wrappers' 4-register `PUSH {R0-R3}`/restore.
 const STRAIGHTLINE_CEIL_PER_HALFWORD: u64 = 5;
 
 /// Worst-case cycles for a straight-line multi-byte expansion, sized from the

crates/synth-cli/src/main.rs

@@ -4816,11 +4816,14 @@ struct NativeGlobalsLayout {
     /// NEVER re-based.
     sp_alias_indices: Vec<u32>,
     /// #383 (VCR-MEM-001): integrator-declared shadow-stack budget in bytes. When
-    /// `Some(B)`, the caller asked to shrink the [0, sp_init) reservation to `B`
-    /// (re-basing the stack top and shifting the high zero-init static relocs
-    /// down). The retarget surgery is silicon-gated (link-fragile native-pointer
-    /// path, the #368→#359 lesson); until it lands, a `Some` here is an honest
-    /// Err, never a silent no-op.
+    /// `Some(B)`, the reservation shrinks from the full [0, sp_init) page to
+    /// `B` + the static tail (re-basing the SP global and the #707 alias set;
+    /// #739 refuses on an un-relocated baked static address the rebase cannot
+    /// see). The surgery is IMPLEMENTED and test-gated
+    /// (`shadow_stack_shrink_383.rs`: gust 1048720 → 4240 B `.bss`); shapes it
+    /// cannot handle honestly Err (budget > sp_init, no identified SP global,
+    /// multi-memory) — never a silent no-op. An earlier doc here called the
+    /// surgery "silicon-gated / not yet landed" (#946 — stale).
     shadow_stack_size: Option<u32>,
 }
 

crates/synth-core/src/static_data_addr.rs

@@ -80,9 +80,11 @@
 //!    (zeroed RAM serves every address): any nonzero runtime-image byte is
 //!    then a served/runtime mismatch (the silent initializer-drop this
 //!    validator caught on the pre-#798 RV32 path).
-//! 3. **AArch64: N/A** — the `-b aarch64` integer subset has no linear-memory
-//!    loads/stores (every memory op loud-declines at selection), so compiled
-//!    code cannot observe static data; there is nothing to validate.
+//! 3. **AArch64: N/A** — the `-b aarch64` backend HAS bounds-checked
+//!    linear-memory loads/stores (v0.52 #865), but it emits no data section
+//!    at all and REFUSES a module carrying active data segments loudly
+//!    (#851, `synth-backend-aarch64/src/backend.rs`), so there is no
+//!    served-vs-runtime image to compare; nothing to validate.
 
 use std::collections::HashMap;