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

[avrabe]

Tiers 2 and 3 of the #946 doc-honesty sweep: every load-bearing comment/doc claim audited against the source it describes, corrected where the code moved past it, and each corrected premise re-verified against the source (per the #967 lesson — no scanner-generated claim taken at face value).

Per-item table

Item	What the doc said	What is actually true	Action
wcet.rs CEIL rationale	5 cyc/halfword ceiling holds "with margin"; only priced 16-bit PUSH/POP is I64Popcnt's 3-register	Priced I64Rotl/I64Rotr fixed-ABI wrappers emit 4-register PUSH {R0-R3} (0xB40F, arm_encoder.rs:8386) → 1+4 = 5, EXACT, zero margin	Rationale corrected; claims.yaml comment updated alongside (comment-only — no check loosened, constant unchanged)
validator_pattern.rs + 3 arm_semantics.rs echo sites	i64 div/rem excluded because they are an __aeabi_ldivmod library call	Encoder expands them INLINE as a 64-iteration shift-subtract loop (arm_encoder.rs:354); no __aeabi_ldivmod exists anywhere in the tree	Exclusion re-justified on the true ground: looped expansion, no straight-line sequence to symbolically execute
static_data_addr.rs AArch64 N/A reason	N/A because AArch64 lacks linear-memory load/store	It HAS bounds-checked load/store (#865); N/A because it ships no data section and loudly refuses active data segments (#851)	Reason rewritten (CLAUDE.md Track C paragraph already carried the correct framing)
alloc_validator.rs (RV) soundness note	"every op_dest==None op is control-flow/system/label/call"	Omits stores (Sb/Sh/Sw); conclusion survives because stores write no register	Argument now states the store case explicitly
selector.rs (RV) live_regs note	"alloc_temp must never hand out" live regs, unconditionally	The exhaustion path returns temps[0] behind the alloc_exhausted loud decline	Note names that path
aarch64 selector header	Hand list of "deliberately still declined" ops: call_indirect, float rounding, f32/f64 load/store, i64→float converts, trapping i64 truncations	All have shipped lowerings in the same file	Hand list deleted in favor of the mechanically-derived complement (cross-backend op-parity oracle) it already cited; the two true contract facts kept (#851 refusal, #865 bounds default)
aarch64 select_typed_cf	loop/if/br_table "declined by name"	All three lower since VCR-A64-CF-001 (v0.55), value-carrying frames included (selector.rs:1679/1779/1802)	Corrected
RV selector header	br_table and cross-function calls listed out-of-scope	Shipped: #882 (br_table), #871 (extern-call relocs)	Moved out of the out-of-scope list
instruction_selector.rs	"the 40 Rocq-proved rules" + hand enumeration	50 rules, single source sel_dsl::RULES, manifest-gated 1:1	Count fixed, enumeration replaced by pointer at the single source
alloc_vfp_temp/alloc_vfp_dtemp	"phase 1 has no VFP spilling"	#881: backend catches both exhaustion Errs and retries with VFP spilling	Docs + user-visible strings updated; retry-trigger substrings kept verbatim (arm_backend.rs:710-711 match sites re-verified, no cross-match)
--shadow-stack-size layout doc	Shrink surgery "silicon-gated, honest Err"	Implemented and test-gated (shadow_stack_shrink_383.rs)	Corrected
CLAUDE.md VCR-WASM-001 line	"phases 1+2, 19 ops, 49 Qed"	Phases 1–3: i32 (19) + i64 (22) ops, 104 Qed (re-derived: grep -c 'Qed\.' WasmCertBridge.v = 104)	Corrected
coq/STATUS.md per-file table	Recount of 2026-07-10: ArmSemantics 8, VcrSelRules 42, "40 rule theorems", total 585/3, "48 Qed (pilot+rules)"	ArmSemantics 14, VcrSelRules 52, 50 rule theorems, VcrSelExpansion.v (29) + four definition-only files missing, total 592/2, 57 pilot/rule Qed — every number re-derived from source this session; per-file rows now sum EXACTLY to the CI-gated 592/2 headline	Table re-derived
VcrSelRules.v header	"40 covered ops" / "40 Qed divergence gate"	50 / 50	Comment-only fix; no proof text touched
CorrectnessI32.v header	"29 Qed"	29 theorems + 2 helper lemmas = 31 Qed (re-derived)	Comment-only fix
feature_matrix.md.tmpl WasmCert row	"i32-only" while carrying the i32+i64 count	i32 (19 ops) + i64 (22 ops)	Template fixed; FEATURE_MATRIX.md regenerated via --emit-status (status.json byte-identical)
docs/status/PROJECT_STATUS.md	~16 months stale, pinned by nothing: 291 vs 592 Qed, 16 vs 18 crates, Z3-as-default, "no bulk/multi-memory"	Hand restatement unmaintainable	DELETED in favor of a pointer stub at the generated/pinned sources of truth (the v0.57 North-Star-portal rule)
POC_ACHIEVEMENTS.md	"R0-R12" allocatable	R0-R8 per the Verus spec (contracts.rs spec_is_allocatable)	Corrected
gale-integration.yaml	Cites map_operator	Symbol never existed (git log -S); the decoder function is convert_operator (wasm_decoder.rs:1904)	Phantom symbol fixed
README "op-level-only residual" (issue line 59)	—	Already resolved by the #963 North Star portal rewrite	Issue item stale — no change needed

Verification

• python3 scripts/claim_check.py claims.yaml → 43/43 claims hold (re-run after merging origin/main at eea92e11, post-fix(#944): verified machine-readable origins for compiler-introduced object branches — the 9 were never unattributed, the real 33 now are attributed #967)
• bazel test //coq:verify_proofs → RUN LOCALLY, 2/2 PASSED (//coq:rocq_proofs + //coq:vcr_sel_rules_coverage) — the .v edits are comment-only, but the suite was executed, not assumed
• cargo fmt --check clean; cargo check -p synth-synthesis -p synth-cli --features riscv clean (covers the only non-comment code change: the two VFP exhaustion message strings)
• Retry-trigger substrings "VFP register file exhausted" / "VFP D-register file exhausted" verified verbatim in the new strings, and verified not to cross-match each other
• Re-derived counts confirmed against source post-merge: WasmCertBridge 104, VcrSelRules 52, ArmSemantics 14, CorrectnessI32 31, VcrSelExpansion 29, VcrSelPilot 7; tree totals 592 Qed / 2 Admitted — the STATUS.md per-file table sums exactly to the headline

Closes the Tier 2 + Tier 3 halves of #946.

🤖 Generated with Claude Code

https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L

[temper-pulseengine]

Automated review for PR #968

pulseengine/synth:docs/946-tiers-2-3-sweep → pulseengine/synth:main

Verdict: 💬 Comment

Summary: The changes in the claims.yaml file do not introduce any new claims or evidence that need to be verified. The only change is a re-audit of the straight-line-expansion ceiling, which has been updated from 4 to 5 cycles/halfword after auditing a 3-register 16-bit PUSH/POP in I64Popcnt (1+3=4 cyc/halfword had zero margin). This does not affect the overall claim that the straight-line-expansion ceil

Findings: 0 mechanical (rivet) · 1 from local AI model.

Findings (1):

1. crates/synth-backend/src/wcet.rs:75

   const STRAIGHTLINE_CEIL_PER_HALFWORD: u64 = 5;
   

   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).

---

Generated by a local AI model and post-validated against a strict JSON contract. Each finding includes the verbatim line being criticised — verify by reading the file at the cited location.

Reviewed at fd9c15e

[codecov]

Codecov Report

❌ Patch coverage is 42.10526% with 11 lines in your changes missing coverage. Please review.

Files with missing lines	Patch %	Lines
crates/synth-synthesis/src/instruction_selector.rs	0.00%	7 Missing ⚠️
crates/synth-verify/src/arm_semantics.rs	66.66%	4 Missing ⚠️

📢 Thoughts on this report? Let us know!