docs: Archive obsolete documentation - #31

avrabe · 2026-01-10T11:44:59Z

Summary

Moved historical and experimental documentation to docs/archive/ to keep active docs focused and current.

Changes

Archived to docs/archive/sessions/ (13 files)

All SESSION_*.md files - historical development notes from Phase 1-3

Archived to docs/archive/experimental/ (9 files)

REALITY_CHECK.md, SAIL_REALITY_CHECK.md, SAIL_HONEST_COMPARISON.md - meta/self-assessment docs
ASILD_SAIL_MIGRATION_PLAN.md - superseded planning
PHASE1/2 status docs - historical phase completion
VALIDATION_REPORT.md - superseded by COMPREHENSIVE version

Added

docs/archive/README.md - explains archive contents

Result

Active documentation is now cleaner:

docs/status/: 4 current files
docs/analysis/: 7 relevant files
docs/validation/: 3 current files

Historical docs preserved in docs/archive/ for reference.

Closes #8

Moved historical and experimental docs to docs/archive/: Archived to docs/archive/sessions/ (13 files): - All SESSION_*.md files - historical development notes Archived to docs/archive/experimental/ (9 files): - REALITY_CHECK.md, SAIL_REALITY_CHECK.md, SAIL_HONEST_COMPARISON.md - ASILD_SAIL_MIGRATION_PLAN.md - superseded planning - PHASE1/2 status docs - historical - VALIDATION_REPORT.md - superseded by COMPREHENSIVE version Added docs/archive/README.md explaining archive contents. Remaining active docs: - docs/status/: 4 current status files - docs/analysis/: 7 relevant analysis docs - docs/validation/: 3 current validation docs Closes #8

i64 register pair support (all 38 operations): - Arithmetic: ADDS/ADC, SUBS/SBC for add/sub; UMULL+MLA for mul - Bitwise: AND/ORR/EOR on both halves - Comparisons: ORR+CMP for eqz; CMP hi then lo for relational - Shifts: funnel shift sequences for shl/shr_u/shr_s/rotl/rotr - Division: binary long division pseudo-ops - Conversions: extend (ASR #31), wrap (take low word), load/store pairs - 47 new tests (29 instruction selector + 18 encoder) GlobalGet/GlobalSet: - R9 as globals base register, LDR/STR with 4-byte stride - Both stack and non-stack instruction selection modes Select instruction: - CMP + MOV + SelectMove (IT EQ; MOV) pattern WAST test pipeline: - wast_multi_func_test Bazel macro replaces 2480 lines with 25 targets - All 22 .wast files wired into renode_test pipeline - Compiles with --all-exports, tests all functions per module Spec test suite: - Added WebAssembly/testsuite as git submodule (257 .wast files) - ~20 files runnable today (i32 + control flow + locals) 762 tests total (up from 687), clippy clean, fmt clean. Implements: FR-002 Implements: FR-005 Trace: skip Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

…te (#55) i64 register pair support (all 38 operations): - Arithmetic: ADDS/ADC, SUBS/SBC for add/sub; UMULL+MLA for mul - Bitwise: AND/ORR/EOR on both halves - Comparisons: ORR+CMP for eqz; CMP hi then lo for relational - Shifts: funnel shift sequences for shl/shr_u/shr_s/rotl/rotr - Division: binary long division pseudo-ops - Conversions: extend (ASR #31), wrap (take low word), load/store pairs - 47 new tests (29 instruction selector + 18 encoder) GlobalGet/GlobalSet: - R9 as globals base register, LDR/STR with 4-byte stride - Both stack and non-stack instruction selection modes Select instruction: - CMP + MOV + SelectMove (IT EQ; MOV) pattern WAST test pipeline: - wast_multi_func_test Bazel macro replaces 2480 lines with 25 targets - All 22 .wast files wired into renode_test pipeline - Compiles with --all-exports, tests all functions per module Spec test suite: - Added WebAssembly/testsuite as git submodule (257 .wast files) - ~20 files runnable today (i32 + control flow + locals) 762 tests total (up from 687), clippy clean, fmt clean. Implements: FR-002 Implements: FR-005 Trace: skip Co-authored-by: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

…#118) The exploration fuzz harness `i64_lowering_doesnt_clobber_params` was flagging `Movw R0, 0` writes as AAPCS param-clobber bugs when the very next ARM op was a `Mov R0, _` overwriting the same register. The two- instruction sequence appears in the function-final i32 return-value placement — the selector zeros R0 and then immediately overwrites with the actual return value. The Movw R0, 0 is a redundant dead store, not a real clobber: the param is already preserved at this point and the immediately-following Mov overrides the zero before any observer sees it. This is the "option (b) harness-side" fix per the issue's investigation comment — cheaper than the underlying peephole (option a, deferred for a future codegen-quality PR) and lets the exploration harness make forward progress toward gating-status promotion (#31). ## Carve-out shape For each ARM instruction in the param-protection window, check whether the immediately-following instruction also writes the same param reg. If so, the current write is dead and gets skipped. Indexed iteration keeps the lookup O(1). ## Soundness The carve-out is local: it only suppresses writes whose result is *provably* dead at the next instruction. A real mid-computation clobber would either: (a) have non-overwriting next-op → still flagged. (b) be part of a chain where the *final* write overwrites R{p} → still flagged on the final write (its next op is typically Pop, which doesn't write the param reg). So the carve-out does not hide real AAPCS clobbers; it only suppresses the duplicate report on the first write of a write-then-overwrite pair. ## What this enables After this lands and a couple of green fuzz-smoke cycles confirm the harness stays quiet, it can be promoted from `gating: false` to `gating: true` in `.github/workflows/fuzz-smoke.yml` — tracked as task #31. Issue: #112

…mask on both direct selectors, DSL rules, and the Rocq models (#682) (#683) ARMv7-M register-controlled shifts consume Rm[7:0] and yield 0 (LSL/LSR) or the sign (ASR) for amounts >= 32; WASM requires amount mod 32. The bare LSL.W/LSR.W/ASR.W lowering predates VCR-SEL inc-2 (the DSL faithfully mirrored a latent hand-written bug) and the model-side Qed was vacuous: ArmSemantics' LSL_reg used I32.shl's INTERNAL mod-32 (WASM-like) semantics — the exact divergence SailArmBridge.v documents as gaps 6-7, whose 'unreachable via WASM masking' judgment this issue falsifies. - Both direct selectors emit AND R12, rm, #31 before the shift (R12 = encoder scratch, never allocatable per #212 — the same pattern the optimized bridge always used, which is why the default optimized path was never affected). ROR is cyclic (Rm[7:0] mod 32 == WASM) — exempt, pinned by the differential. - DSL rules rule_i32_shl/shr_s/shr_u gain the mask + a scratch param with the rs != rn side condition (rotl pattern); table + generator + generated Rust updated; Rocq theorems re-proved for the masked sequences (correct under BOTH the current model semantics and real Rm[7:0] hardware). Compilation.v's monolithic lowering + CorrectnessI32.v proofs updated identically. The HONEST model fix (Rm[7:0] semantics per bridge gaps 6-7) remains the flat-executor follow-up. - Red -> green: scripts/repro/i32_shift_mask_682_differential.py (gale's repro table + variable amounts + the rotr exemption + in-range sanity): 8 mismatches on v0.37.0's relocatable path -> all green both paths; CI-gated as a new oracle job. - Deliberate byte change (+4B per register-controlled i32 shift; const amounts imm-fold and are unaffected — signed_div_const pin unchanged). Refreeze ritual: all 23 CI-gated differentials PASS on the new bytes BEFORE re-pinning; 13 goldens re-pinned; RV32 pins untouched. The gate gains a documented SYNTH_REFREEZE_PRINT repin aid. Closes #682. Co-authored-by: Claude Fable 5 <noreply@anthropic.com>

…ovably < 32 (#686) gale measured #682's unconditional AND R12,#31 mask at ~12% cyc/call (+14 B) on gust_mix, whose Q8 fixed-point shifts are all CONSTANTS — the mask can never fire there, yet every register-controlled i32 shift pays it. New peephole liveness::elide_shift_masks removes the mask ONLY when the amount is statically provable < 32; anything unproven keeps it — elision is an optimization, the mask stays the sound default. Two proven shapes, keyed on the #682 idiom (and r12,rK,#31 ; shift by r12 — emitted adjacently by both direct selectors, the Rocq-proved DSL rules, and the optimized bridge; the DSL rules stay MASKED, no proof changes): - Const amount: nearest preceding def of rK is a pure materialization (movw, or the bridge's mov #imm) over a fully-modeled redefinition- free window -> fold the whole triple to the immediate shift, REDUCED MOD 32 (so >= 32 amounts shrink too — the fold computes exactly the WASM semantics the mask enforces); C mod 32 == 0 lowers to MOV (imm5 == 0 encodes shift-by-32, the LSR/ASR pitfall). The movw drops when rK has no other reader (reg_dead_by_redef). This supersedes fold_immediate_shifts for the masked idiom — its movw->shift window is intercepted by the #682 and, so post-#682 it declined every const-amount register shift (the gust_mix regression's second half). - Range-carried amount: nearest def is and rK,rX,#c with c < 32 -> rK < 32 at the shift, the re-mask is a no-op; shift by rK directly. Covers the wasm-level x&31 / x&15 idioms. A #494 fact-spec value- range premise is the documented follow-up. Soundness scaffolding as the sibling folds: backward scan aborts on any reg_effect-unmodeled op (call/branch/LABEL = merge point); dropping the and r12 write is safe by the #212 R12-scratch convention; rotr is never masked (#682 exemption) so the pattern cannot match it; removal/rewrite-only before branch resolution (offset-neutral). FLAG-OFF (opt-in SYNTH_SHIFT_MASK_ELIDE=1) per the flag-then-flip protocol: the elision MOVES the frozen anchors — measured on this commit, per-function, no function grows, every const-shift function shrinks (bytes ON vs OFF, identical on both paths): control_step_decide 313 -> 293 (-20) flight_seam flight_algo 376 -> 296 (-80), controller_step 325 -> 241 (-84) flight_seam_flat flight_algo 520 -> 436 (-84), controller_step -84 gust_mix (the #686 fixture) 65 -> 55 (-10) — recovers the measured regression (the +14 B was mask + retained movw + wide shift) i32_shift_mask_682 shl32/shl33/shl300/shr300/sar300 -> 8-12 B each signed_div_const untouched Default (flag unset) is byte-identical to v0.37.1 everywhere: the frozen byte-gate passes unchanged, and shift_mask_elide_686.rs pins unset == opt-out. The default-on flip is the maintainer's separate refreeze (all differentials green on the new bytes, goldens re-pinned). Oracles on this commit: - i32_shift_mask_682_differential.py: all green DEFAULT and ELIDE-ON, both paths, including every >= 32 row; now also CI-gated with the flag ON. RED-TESTED: a temporary force-elide of const >= 32 (bare register shift, no mask) turned 10 rows red on both paths — the oracle catches unsound elision; hack removed. - Execution differentials with the flag ON over the moved fixtures: flight_seam flight_algo 0x07FDF307 MATCH, control_step 13/13, frame_slot_dce PASS, const_cse PASS. - shift_mask_elide_686.rs: per-function no-grow table over the corpus (both paths) + strict shrink on gust_mix + default==opt-out pin. - 10 new unit tests: mod-32 fold (< 32, >= 32, == 32 -> MOV), bridge mov-imm form, range-carried and-mask (#15 folds, #63 declines), unproven def declines, label-in-window declines, movw kept when the amount register has other readers, non-R12 pattern untouched. Closes #686. Refs #682 #683. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

…ovably < 32 (#686) (#692) gale measured #682's unconditional AND R12,#31 mask at ~12% cyc/call (+14 B) on gust_mix, whose Q8 fixed-point shifts are all CONSTANTS — the mask can never fire there, yet every register-controlled i32 shift pays it. New peephole liveness::elide_shift_masks removes the mask ONLY when the amount is statically provable < 32; anything unproven keeps it — elision is an optimization, the mask stays the sound default. Two proven shapes, keyed on the #682 idiom (and r12,rK,#31 ; shift by r12 — emitted adjacently by both direct selectors, the Rocq-proved DSL rules, and the optimized bridge; the DSL rules stay MASKED, no proof changes): - Const amount: nearest preceding def of rK is a pure materialization (movw, or the bridge's mov #imm) over a fully-modeled redefinition- free window -> fold the whole triple to the immediate shift, REDUCED MOD 32 (so >= 32 amounts shrink too — the fold computes exactly the WASM semantics the mask enforces); C mod 32 == 0 lowers to MOV (imm5 == 0 encodes shift-by-32, the LSR/ASR pitfall). The movw drops when rK has no other reader (reg_dead_by_redef). This supersedes fold_immediate_shifts for the masked idiom — its movw->shift window is intercepted by the #682 and, so post-#682 it declined every const-amount register shift (the gust_mix regression's second half). - Range-carried amount: nearest def is and rK,rX,#c with c < 32 -> rK < 32 at the shift, the re-mask is a no-op; shift by rK directly. Covers the wasm-level x&31 / x&15 idioms. A #494 fact-spec value- range premise is the documented follow-up. Soundness scaffolding as the sibling folds: backward scan aborts on any reg_effect-unmodeled op (call/branch/LABEL = merge point); dropping the and r12 write is safe by the #212 R12-scratch convention; rotr is never masked (#682 exemption) so the pattern cannot match it; removal/rewrite-only before branch resolution (offset-neutral). FLAG-OFF (opt-in SYNTH_SHIFT_MASK_ELIDE=1) per the flag-then-flip protocol: the elision MOVES the frozen anchors — measured on this commit, per-function, no function grows, every const-shift function shrinks (bytes ON vs OFF, identical on both paths): control_step_decide 313 -> 293 (-20) flight_seam flight_algo 376 -> 296 (-80), controller_step 325 -> 241 (-84) flight_seam_flat flight_algo 520 -> 436 (-84), controller_step -84 gust_mix (the #686 fixture) 65 -> 55 (-10) — recovers the measured regression (the +14 B was mask + retained movw + wide shift) i32_shift_mask_682 shl32/shl33/shl300/shr300/sar300 -> 8-12 B each signed_div_const untouched Default (flag unset) is byte-identical to v0.37.1 everywhere: the frozen byte-gate passes unchanged, and shift_mask_elide_686.rs pins unset == opt-out. The default-on flip is the maintainer's separate refreeze (all differentials green on the new bytes, goldens re-pinned). Oracles on this commit: - i32_shift_mask_682_differential.py: all green DEFAULT and ELIDE-ON, both paths, including every >= 32 row; now also CI-gated with the flag ON. RED-TESTED: a temporary force-elide of const >= 32 (bare register shift, no mask) turned 10 rows red on both paths — the oracle catches unsound elision; hack removed. - Execution differentials with the flag ON over the moved fixtures: flight_seam flight_algo 0x07FDF307 MATCH, control_step 13/13, frame_slot_dce PASS, const_cse PASS. - shift_mask_elide_686.rs: per-function no-grow table over the corpus (both paths) + strict shrink on gust_mix + default==opt-out pin. - 10 new unit tests: mod-32 fold (< 32, >= 32, == 32 -> MOV), bridge mov-imm form, range-carried and-mask (#15 folds, #63 declines), unproven def declines, label-in-window declines, movw kept when the amount register has other readers, non-R12 pattern untouched. Closes #686. Refs #682 #683. Co-authored-by: Claude Fable 5 <noreply@anthropic.com>

…ansmuted to CMP at FIVE sites, not two (#919) * test(#916): RED — i64 zero-fill transmutes to CMP for a high destination (5 sites, not 2) Red-first evidence on unmodified main. `MOVS Rd,#imm8` (T1) has a THREE-bit Rd field; `reg_to_bits(R8)` = 8 overflows into bit 11 and `0x2000|0x0800 = 0x2800` is `CMP r0,#0` — not a move. The half that must be zeroed is never written. The issue named two sites. Sweeping every 16-bit imm8 T1 emission in the Thumb-2 encoder found FIVE: I64Shl rd_lo large-shift arm conditional (n >= 32) I64ShrU rd_hi large-shift arm conditional (n >= 32) I64Clz rnhi high-word clear UNCONDITIONAL I64Ctz rnhi high-word clear UNCONDITIONAL I64ExtendI32U rdhi high-word clear UNCONDITIONAL The last three are worse than the two filed: they have no `n >= 32` precondition, so every i64.clz / i64.ctz / i64.extend_i32_u whose high half lands in R8 returns garbage in its upper 32 bits. `I64ExtendI32U{rdhi=R8}` emits literally [4608, 2800] — a two-instruction expansion, half of which is the wrong instruction. Failing today (7 assertions): I64Shl{rd_lo=R8} tail 0x2800 I64ShrU{rd_hi=R8} tail 0x2800 (the shape rv32_cmp_select_472.wat emits) I64Clz{rnhi=R8} tail 0x2800 I64Ctz{rnhi=R8} tail 0x2800 I64ExtendI32U{rdhi=R8} tail 0x2800 I64Shl / I64ShrU branch-displacement checks (pre-staged for the widening) NOT defective, and pinned as such so the sweep is recorded rather than asserted in prose: - A32 (cortex-r5): `MOV Rd,#0` is `0xE3A00000 | Rd<<12`, a FOUR-bit Rd field. R8 encodes correctly. Test passes on main. - I64ShrS: its large-shift arm sign-fills with the 32-bit `ASR.W rd_hi,rn_hi,#31`, no 16-bit form to transmute. - I64SetCond / I64SetCondZ / Mov / f32+f64 compare: already carry the #311 guard. Branch targets were settled by DECODING the imm fields, not by reading comments: - Shl/ShrU: `B .done` (0xE002) targets halfword 19 = END of expansion, PAST the MOV at halfword 18. Widening the MOV MOVES the target -> displacement must be recomputed to 0xE003. - Clz/Ctz: `B .done` targets byte 22 / 30, which IS THE MOV's OWN ADDRESS. An instruction cannot move its own address -> no displacement change. - I64ExtendI32U: no branches. `assert_branches_still_land` re-derives every target from the emitted bytes so a mis-recomputed displacement fails here rather than at run time. Trading a data miscompile for a control-flow one would be strictly worse. Refs #916, #311, #180, #498 Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L * fix(#916): GREEN — emit MOV.W for high-register i64 zero-fills, deriving the branch displacement Follows #311's shape (32-bit `MOV.W Rd,#imm8`, T2 `F04F 0000 | Rd<<8 | imm8`, whenever `rd >= R8`) at all FIVE affected sites, behind one shared helper (`emit_thumb_zero_fill`) so a sixth site cannot reintroduce the class silently. INSTRUCTION SIZE / DISPLACEMENTS — the reason this was not a one-liner. `MOV.W` is 4 bytes where `MOVS` was 2. Whether that moves a branch target was settled per site by DECODING the emitted imm fields, not by reading comments: I64Shl / I64ShrU `B .done` (0xE002) targets halfword 19 = the END of the expansion, PAST the zero-fill at halfword 18. The target MOVES. The displacement is now DERIVED from the zero-fill's real width (`thumb_zero_fill_halfwords`) rather than hard-coded, so the encoder cannot drift from itself: 0xE002 for a low destination, 0xE003 for a high one. `BPL .large` (0xD50A) targets halfword 16, before the zero-fill -> unaffected. I64Clz / I64Ctz `B .done` targets byte 22 / 30, which IS the zero-fill's OWN address. An instruction cannot move its own address -> no displacement change. `BEQ` targets 14 / 18, before it. I64ExtendI32U no branches at all. Reordering the large-shift arm to dodge the size change was REJECTED, not overlooked: zeroing rd_lo before the `LSL.W` would destroy rn_lo in the in-place case rd_lo == rn_lo. That reasoning is in the code so it is not "simplified" away later. ESTIMATOR MIRROR (#498). `estimate_arm_byte_size` is a hand-maintained mirror of this encoder and feeds optimized-path branch resolution; I64Shl/ShrU/Clz/Ctz are all classified OnPath. Left un-mirrored, a high-reg shift would be under-counted by 2 and every branch spanning it would land short — the #483 class, and exactly the control-flow miscompile that would have been strictly worse than the data bug. Now register-shape-sensitive (38/40, 24/26, 32/34), matching the existing house pattern for Cmn/Sxtb/Uxth/Mov. The direct selector needs no change: it resolves branches from real `code.len()`, not the estimator. I64ExtendI32U is classified NotOnPath (lowered to 32-bit op pairs upstream), so it has no estimator entry to update. GATE COVERAGE ADDED IN THE SAME COMMIT — re-running the old cases would have proved nothing, because they only ever used low registers: - estimator_encoder_agreement: +5 high-destination cases (I64Shl, I64ShrU, I64ShrS, I64Clz, I64Ctz). Without them the #498 oracle stayed green while blind to the entire high-reg half of these expansions. - i64_expansion_certification: +5 high-register variants fed to the symbolic executor. This was a THIRD validator blind spot in the same family as the two recorded in v0.53 — `covered_i64_pseudo_selections` fed these ops only at R0/R1, and the high-register variant list covered only I64SetCond/ SetCondZ/Mul/Popcnt, so no validator on the tree could see the defect. Confined to rd >= R8: low-register expansions are byte-identical (38/38/40/24/ 32/4), so frozen anchors do not move unless a fixture actually had a high-reg destination. Fixes #916. Refs #311, #180, #498, #483 Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L * test(#916): RED validator shape — prove the certifier is non-vacuous on this class The five high-register variants added to `shipped_expansions_certify_high_register_variants` are only meaningful if the validator can DISTINGUISH the fixed expansion from the broken one. Splice the pre-fix `I64ShrU{rd_hi=R8}` tail back on — the narrow `B .done` (0xE002) and the transmuted 0x2800 — and it must produce a counterexample: ✗ #916 shape rejected as required: I64ShrU: a_lo=0xffffffff, a_hi=0x0, b_lo=0x20, b_hi=0x0 b_lo = 0x20 = 32, i.e. the solver picked exactly the large-shift arm that reaches the zero-fill. Same pattern as the #632 red shape already in this file. The fixed tail is pinned in the test, so an encoder change breaks it loudly rather than silently making the splice meaningless. Refs #916 Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L * test(#916): execution differential — 48 runs vs wasmtime, RED before the fix The byte-level test pins the emitted halfword and the certifier pins the symbolic semantics, but neither can catch a MIS-RECOMPUTED BRANCH. Widening the zero-fill from 2 to 4 bytes moved `.done` in I64Shl/I64ShrU; if the displacement were wrong the branch would sail past the end of the expansion, and the tail halfword would still assert clean. Only execution sees that. `i64_high_reg_zero_fill_916.wat` removes the luck that hides the bug on main: every export KEEPS the half the broken instruction was supposed to zero (no following I32WrapI64 to discard it). Shift amounts straddle 32 — 0,1,31 take the small-shift arm and the moved branch, 32,33,40,63 take the large arm with the widened zero-fill. `pressure_shru` is the reachability witness: four i32 params pinned in r0-r3 (#193/#204) plus live i64 pairs push a zero-fill destination into R8. Verified in the emitted image — `MOV.W R8, #0` at byte 0x252 of the compiled .text. R8 and unused argument registers are seeded with 0xDEADBEEF, not left at 0. #916 leaves the destination UNWRITTEN, so a run that passed only because the stale register happened to hold 0 would be a false green. RED-FIRST EVIDENCE (encoder reverted to the pre-fix commit, CLI rebuilt): FAIL pressure_shru(0x20,0x1,0x20,0x2) = 0x22d3c110320fedcc expect 0x00000007320fedcc FAIL pressure_shru(0x28,0x7,0x21,0xb) = 0x7786944434320ff1 expect 0x5555555534320ff1 FAIL pressure_shru(0x3f,0xffffffff,..) = 0x22d3c121b3333335 expect 0x00000032b3333335 exit 1 The three failures are exactly the shift amounts >= 32 (0x20, 0x28, 0x3f); the 0x1 and 0x1f cases pass because they take the small-shift arm and never reach the zero-fill. The corrupted HIGH halves are stale register contents. With the fix restored: 48/48 OK, exit 0. CI-wired in this commit (`set -euo pipefail`, `# ci-status: wired`, and a non-zero-count assertion on executions so a silently-empty run cannot pass). `scripts/oracle_wiring_check.py` green: 159 scripts, 152 wired, 0 unwired, 0 UNDECLARED. `scripts/claim_check.py` green: 38/38. Refs #916 Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L * style(#916): cargo fmt + clippy unnecessary_cast on the zero-fill helper `((rd_bits as u16) << 8) as u16` — the outer cast is a no-op (rust-1.96 clippy::unnecessary_cast, -D warnings in CI). Gate sweep by REAL exit code, not piped output: cargo fmt --check exit 0 cargo clippy --workspace --all-targets -D warnings exit 0 cargo test --workspace exit 0 frozen_codegen_bytes (10 anchors) exit 0, BYTE-IDENTICAL estimator_encoder_agreement (#498) exit 0 scripts/oracle_wiring_check.py exit 0 scripts/claim_check.py exit 0, 38/38 NO frozen fixture moved. The fix is confined to `rd >= R8` and none of the four anchors (control_step, flight_seam, flight_seam_flat, signed_div_const) has a high-register i64 zero-fill destination, so their .text sha256 pins are unchanged — nothing to re-pin, and no re-pin to justify. Refs #916 Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L * test(#916): pin the differential's reachability witness so it cannot degrade into a no-op The execution differential's entire value rests on one unstated fact: the allocator actually places a zero-fill destination in R8 inside `pressure_shru`. That was verified by hand (`MOV.W R8,#0` at .text+0x252) but NOTHING asserted it. Any allocator change can quietly reallocate that function to R0-R7 — and VCR-DEC-001 is actively churning the allocator, with #917's interference edge specifically keeping R8 out of the candidate colours. The differential would then still print "48/48 OK" and exit 0 while testing nothing about the high-register path. That is the #890 "gate that cannot fail" shape, arrived at by drift instead of by a bug. So the witness is now an assertion: scan .text for the 32-bit `MOV.W Rd,#0` (F04F 0000 | Rd<<8) with Rd >= 8, and fail if there is none. That encoding exists ONLY because of the #916 fix — before it, the same site emitted 0x2800. Proven non-vacuous by construction, not by inspection: on the shipped module it reports `reachability witness: MOV.W R8,#0 @ 0x252` and exits 0; on a single-function low-pressure module whose shift destination lands in a low register it fires and exits 1. The assertion message says what to do — raise pressure in the .wat, do not delete the check — and names the likely cause, so if #917's decline lands and takes R8 away, this goes RED (correct: the oracle lost its witness) rather than silently green. Also closed while here: no WCET test asserts an exact cycle literal for i64.shl/shr_u/clz/ctz (the only i64 entry in wcet_bound_gate.rs is div, which declines), so the estimator's 38->40 / 24->26 / 32->34 widening touches no pinned bound. 39/39 wcet_bound_gate green. The direction is sound regardless — a longer instruction yields a HIGHER cycle bound. Refs #916, #890 Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L --------- Co-authored-by: Claude Opus 5 <noreply@anthropic.com>

…ier passed a lowering that is wrong on silicon (#975) * fix(#923): arm_semantics silently no-oped 87 of 222 ArmOps — record, decline, and model the shipped ones `ArmSemantics::encode_op`'s `_ => {}` default arm left the state UNCHANGED for any op it had no arm for. That is the false-ACCEPT direction, not the safe one: a lowering that computes the right value and then destroys it is invisible to the value VC. Measured on v0.57 main, through the public API `synth verify` itself uses (`TranslationValidator::verify_rule` → `verify_equivalence`): i32.add → ADD r0,r0,r1 ; UXTB r0,r0 => Verified That sequence returns `(x + y) & 0xFF` on silicon. The trap path had already noticed the hazard — `exec_trap_subset_op`'s doc says `encode_op`'s silent default "must never green-wash a trap derivation" — but its defence was a hand-maintained allowlist mirroring `encode_op`'s arms, and the mirror had drifted: `Rsb` (a SHIPPED sel-DSL rule's instruction), `I32TruncF32S` and `I32TruncF32U` were all allowlisted to DELEGATE to a model that does not implement them. The guard was inert for exactly those three. The same gap in the other direction made the model reject CORRECT code: the shipped `i32.shl` lowering `AND r1,#31 ; LSL r0,r0,r1` came back `Invalid`, which is the real reason the CLI rule table declines every shift rule. Fixes, in the order they matter: 1. One source of truth, not two. The default arm now RECORDS the first unmodeled op in `ArmState::unmodeled` instead of ignoring it. The modeled set stays defined solely by `encode_op`'s match arms, so it cannot rot. - the value VC turns a set field into `UnsupportedOperation`; - `exec_trap_subset_op` re-checks it after every delegation, so an allowlisted-but-unmodeled op is a loud decline (closes the `Rsb` hole generically, for future allowlist entries too). 2. Register-amount shifts modeled FAITHFULLY: ARMv7-M A7.7.68/70/12/117 give `shift_n = UInt(Rm<7:0>)` — the low EIGHT bits, not `Rm mod 32` and not all 32. This is the #682 class. WASM's mod-32 rule belongs to the LOWERING (the selector's `AND #31`), never to the ARM model. Verified live: the unmasked lowering is now rejected with counterexample `Rm = 0x40000080`, a witness only the `<7:0>` rule can produce (`Rm mod 32 = 0`, `Rm<7:0> = 128 ≥ 32`). 3. Modeled alongside, all shipped-selector ops: `Rsb`, `Sxtb`/`Sxth`/`Uxtb`/ `Uxth`, `I32TruncF32S`/`I32TruncF32U`. `Cmn`/`Movw`/`Movt` had a DUPLICATE model inside `exec_trap_subset_op`; that copy is deleted and the ops now delegate to the single model in `encode_op`. Verdicts after, same entry point: ADD;UXTB Verified -> Invalid (caught, with counterexample) ADD;POP Verified -> Err(UnsupportedOperation) (loud decline) 5 correct shift/rotate lowerings Invalid -> Verified Residual, stated not hidden: MVE vector ops, subword/symbol memory ops, branch and stack ops remain unmodeled — but they now DECLINE instead of passing. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L * test(#923): ISA-faithfulness tests for ArmSemantics — 24 tests written against the ARM ARM, not against the model A test that asserts the model agrees with itself adds coverage and zero safety. Every assertion here is written against ARMv7-M (DDI 0403E.b) behaviour, with two disciplines making that concrete: * INDEPENDENT ORACLE — expected values come from Rust (signed vs unsigned comparison, wrapping arithmetic, `count_ones`/`leading_zeros`/`reverse_bits`, IEEE-754 `<`), a second implementation rather than a mirror of the model. * DISCRIMINATING VECTORS — chosen to SEPARATE the ARM rule from the rules it gets confused with, since a vector in the easy range agrees with every plausible-but-wrong model. The shift table is the clearest case: with Rn = 1, `Rm = 0x100` gives 1 under `Rm<7:0>` and 1 under mod-32 but 0 under raw-32, while `Rm = 0x120` gives 0 under `Rm<7:0>` and 1 under mod-32. Together the two vectors pin `<7:0>` against BOTH wrong readings. Prioritised by consequence, not by line count: * register-amount shifts (#682 class, decided in this file); * `update_flags_sub`/`update_flags_add` + all ten condition codes — every i32 comparison and the cmp→select lever ride on these, and `CMN` drives the `i32.div_s` INT_MIN/-1 overflow guard, so a wrong C or V there is a wrong TRAP. `update_flags_add` had ZERO coverage. `CMP 1, -1` is the vector that separates the C-reading conditions from the N/V-reading ones; * the ordered VFP compares behind the #709/#756 trunc guards: NaN makes every ordered relation false (`Ge` included — a `!(a<b)` implementation gets this wrong), ±0.0 compare equal, negatives order by decreasing magnitude; * 64-bit pairs: carry/borrow across the pair, and the lexicographic compares' UNSIGNED low-word tiebreak; * the #923 regressions in both directions, plus a drift guard asserting every trap-subset delegate is actually modeled. DELIBERATELY NOT ASSERTED, and said so in the file header: SDIV/UDIV by zero. ARM yields 0, SMT-LIB bvsdiv/bvudiv are total and yield something else, WASM traps, and the value clause is asserted only on the non-trapping path by the trap-gated VC. Pinning either answer would turn a scoped exclusion into a false claim. The division tests stop where ARM, SMT and WASM all agree. POTENCY CHECKED, not assumed — all 24 passed on the first run, which is exactly when to ask whether they can fail. Eight mutations of the model, each confirmed present before and absent after replacement, each turning the suite RED: raw-32 shift amount (3 tests red), CMP carry polarity (2), CMN carry polarity, MOVT clobbering the low half, F32 Ge dropping its NaN exclusion, i64.lt_s using a signed low-word tiebreak, SXTB zero-extending, and removing the #923 unmodeled-op check. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L * fix(#923): state the same shift rule in both of this crate's ARM models `validator_pattern.rs` (the VCR-RA-003 whole-function validator) fed the RAW 32-bit `Rm` to its SMT shift and carried a comment saying "the selector is responsible for masking the amount mod 32" — conflating ARM's `Rm<7:0>` with WASM's mod-32. Neither is what the executor did. Consequence, graded honestly: this one can only ever false-ALARM, never false-accept. For the model to bless a lowering it must match the WASM reference for ALL `Rm`, which forces the amount into `[0,31]`, exactly where the raw value and `Rm<7:0>` coincide; and an unmasked lowering is rejected by both readings. So no verdict changes, and the full synth-verify suite confirms it (267 tests, unchanged). Fixed anyway, because the point of this lane is that a model is evidence about silicon: two models in one crate stating different rules for one instruction means at most one of them is evidence, and a reader cannot tell which. They now share a helper and a citation. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L * style(#923): clippy bool-literal assertions in the CMN flag test Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L * docs(#923): say how second the second ARM op model actually is Three places assert that `synth-verify`'s `ArmSemantics::encode_op` is "a genuinely second model of the same operations" — the VCR-VER-004 independence caveat in FEATURE_MATRIX (via its template), `abi_contract.rs`'s module doc, and the roadmap entry. The claim was load-bearing (it is what keeps "three independent validators" from being an overclaim) and it was more generous than the code: 87 of `ArmOp`'s 222 variants were modeled as doing nothing. Amended with the measured number, before and after, and with the residual split by kind (41 MVE, 32 others) rather than left as a category list. FEATURE_MATRIX is generated, so the edit lands in `scripts/templates/feature_matrix.md.tmpl` and the committed copy is regenerated; `artifacts/status.json` is unchanged (no counts moved). claim_check 43/43. Also completes the trap-subset drift guard to cover EVERY delegate on the allowlist, not 21 of the 29. A test that guards against a hand-maintained mirror must not be a hand-maintained mirror of part of it; the runtime `delegate_to_encode_op` check is the real guard, and the test now says so. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L * test(#923): pin the shipped Rocq-proved i32.rotl rule instruction-for-instruction The sharpest instance of the finding, taken verbatim from the shipped table rather than paraphrased. `sel_dsl::generated::rule_i32_rotl` is a DEFAULT-ON, Rocq-proved selector rule (`VcrSelRules.rule_i32_rotl_correct`, Qed) and it emits exactly `RSB rs, rm, #32` then `ROR rd, rn, rs` — BOTH of which were in the silently-dropped 87. The Rocq proof was never in question. The SMT model simply executed neither instruction, so its opinion of this rule was worth nothing in either direction: it could not have caught a wrong rotl, and it would have rejected the right one. The test calls the generator rather than transcribing its output, so a change to the shipped rule reaches the assertion instead of drifting away from it, and it asserts the emitted SHAPE before the verdict so a shape change fails loudly with "re-derive this test rather than loosening it" instead of silently verifying something else. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L --------- Co-authored-by: Claude Opus 5 <noreply@anthropic.com>

avrabe added this to the phase-0-cleanup milestone Jan 10, 2026

avrabe merged commit aa96db8 into main Jan 10, 2026

avrabe deleted the phase0/issue-8-archive-obsolete-docs branch January 10, 2026 11:54

avrabe mentioned this pull request Mar 2, 2026

Complex test case #36

Closed

avrabe mentioned this pull request Mar 19, 2026

feat: i64 register pairs, globals/select, WAST pipeline + spec-testsuite #55

Merged

3 tasks

avrabe mentioned this pull request May 10, 2026

feat(opt): direct hi/lo extraction for u64-packed values (#94) #98

Merged

5 tasks

avrabe mentioned this pull request May 27, 2026

feat(coq): add i64 pseudo-op result-correspondence axioms + discharge 5 v0.8.0 admits (v0.9.0 precursor) #153

Merged

Navigation Menu

Uh oh!

docs: Archive obsolete documentation - #31