diff --git a/CLAUDE.md b/CLAUDE.md index 3b142011..c0b16ada 100644 --- a/CLAUDE.md +++ b/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, diff --git a/artifacts/gale-integration.yaml b/artifacts/gale-integration.yaml index 05d8f9a7..a5282897 100644 --- a/artifacts/gale-integration.yaml +++ b/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` diff --git a/claims.yaml b/claims.yaml index c16f2c1f..9df90286 100644 --- a/claims.yaml +++ b/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'] diff --git a/coq/STATUS.md b/coq/STATUS.md index 63af40e8..77a6d341 100644 --- a/coq/STATUS.md +++ b/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) diff --git a/coq/Synth/Synth/CorrectnessI32.v b/coq/Synth/Synth/CorrectnessI32.v index ec7ded48..93a4ba7d 100644 --- a/coq/Synth/Synth/CorrectnessI32.v +++ b/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 diff --git a/coq/Synth/Synth/VcrSelRules.v b/coq/Synth/Synth/VcrSelRules.v index 185473d4..46258654 100644 --- a/coq/Synth/Synth/VcrSelRules.v +++ b/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 diff --git a/crates/synth-backend-aarch64/src/selector.rs b/crates/synth-backend-aarch64/src/selector.rs index 55d54969..08953e8c 100644 --- a/crates/synth-backend-aarch64/src/selector.rs +++ b/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, /// #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, } diff --git a/crates/synth-core/src/static_data_addr.rs b/crates/synth-core/src/static_data_addr.rs index 8fffdd79..b50424cf 100644 --- a/crates/synth-core/src/static_data_addr.rs +++ b/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; diff --git a/crates/synth-synthesis/src/instruction_selector.rs b/crates/synth-synthesis/src/instruction_selector.rs index ebef428f..4d657a28 100644 --- a/crates/synth-synthesis/src/instruction_selector.rs +++ b/crates/synth-synthesis/src/instruction_selector.rs @@ -2282,8 +2282,13 @@ fn vfp_s_index(r: VfpReg) -> Option { } /// Allocate the lowest-numbered free single-precision S-register (S0..S15). -/// Errs (honest decline) when all 16 are live — phase 1 has no VFP spilling, so -/// an f32 expression deeper than the register file loud-skips its function. +/// Errs (honest decline) when all 16 are live. Since #881 (VCR-RA-004) this +/// Err is RECOVERABLE: the backend catches the "VFP register file exhausted" +/// substring (`arm_backend.rs`, the VFP rung) and reruns the entire selection +/// with VFP spilling enabled — the pre-op pressure guard spills the deepest +/// segment-local f32/f64 value to the frame and reloads before consumers. A +/// function that exhausts even under the spill rung stays a loud skip. (The +/// substring is the retry trigger — keep it stable.) fn alloc_vfp_temp(used: &mut [bool; 16]) -> Result { for (i, slot) in used.iter_mut().enumerate() { if !*slot { @@ -2292,8 +2297,9 @@ fn alloc_vfp_temp(used: &mut [bool; 16]) -> Result { } } Err(synth_core::Error::synthesis( - "GI-FPU-002: VFP register file exhausted (S0..S15 all live) — f32 \ - expression too deep for phase 1 (no VFP spilling yet)" + "GI-FPU-002: VFP register file exhausted (S0..S15 all live) — \ + f32/f64 register pressure exceeds the file; the backend retries \ + with VFP spilling (#881) and this surfaces only if that also fails" .to_string(), )) } @@ -2916,7 +2922,10 @@ fn vfp_d_index(r: VfpReg) -> Option { /// Allocate the lowest-numbered free caller-saved D-register (D0..D7), marking /// BOTH aliased S-slots in the shared `vfp_used` map. Errs (honest decline) -/// when no aligned pair of S-slots is free — no VFP spilling mid-expression. +/// when no aligned pair of S-slots is free. Like [`alloc_vfp_temp`]'s S-file +/// exhaustion, this Err is RECOVERABLE since #881: the backend catches the +/// "VFP D-register file exhausted" substring and retries the whole selection +/// with VFP spilling enabled (keep the substring stable — it is the trigger). fn alloc_vfp_dtemp(used: &mut [bool; 16]) -> Result { for i in 0..8usize { if !used[2 * i] && !used[2 * i + 1] { @@ -2927,8 +2936,10 @@ fn alloc_vfp_dtemp(used: &mut [bool; 16]) -> Result { } Err(synth_core::Error::synthesis( "GI-FPU-002 phase 2: caller-saved VFP D-register file exhausted \ - (D0..D7 all live) — f64 expression too deep for this increment \ - (no VFP spilling, and D8..D15 are callee-saved) — declining (#369)" + (D0..D7 all live; D8..D15 are callee-saved and never allocated \ + here) — f64 register pressure exceeds the file; the backend \ + retries with VFP spilling (#881) and this surfaces only if that \ + also fails" .to_string(), )) } @@ -5035,9 +5046,12 @@ pub struct InstructionSelector { } /// `SYNTH_SEL_DSL` (VCR-SEL-001, #242): **default ON** since the increment-1..4 -/// default-on flip — the 40 Rocq-proved rules are the SHIPPED lowering path for -/// their covered ops (i32 add/sub/mul/and/or/xor/rotl/rotr + comparisons + -/// shifts + clz/ctz/popcnt, i64 add/sub/and/or/xor/eqz + i64 comparisons). The +/// default-on flip — the 50 Rocq-proved rules are the SHIPPED lowering path for +/// their covered ops. The op list is `sel_dsl::RULES` itself (the single +/// source — it also emits the Rocq model, `VcrSelRulesGenerated.v`, and is +/// 1:1 coverage-gated against `coq/vcr_sel_rules.manifest`); a hand +/// enumeration here said "40" and omitted nine i64 ops (#946), so it was +/// replaced by this pointer. The /// flip is byte-invisible by construction: every rule was mirror-pinned /// byte-identical to the hand-written arm it replaces. /// diff --git a/crates/synth-verify/src/arm_semantics.rs b/crates/synth-verify/src/arm_semantics.rs index c1bc53bc..f5a8a282 100644 --- a/crates/synth-verify/src/arm_semantics.rs +++ b/crates/synth-verify/src/arm_semantics.rs @@ -670,21 +670,21 @@ impl ArmSemantics { // ======================================================================== // i64 Division and Remainder // ======================================================================== - // Note: Full 64-bit division on ARM32 requires library calls or - // very complex multi-instruction sequences. For verification, we model - // the results symbolically. + // Note: ARM32 has no 64-bit divide instruction — the shipped + // lowering expands these pseudo-ops INLINE to a software + // long-division sequence with an internal 64-iteration runtime + // loop (arm_encoder.rs; no `__aeabi_*` library call is emitted). + // For verification, we model the results symbolically. ArmOp::I64DivS { rdlo, rdhi, .. } => { - // Signed 64-bit division - // Real implementation would require __aeabi_ldivmod or equivalent - // For verification, return symbolic values + // Signed 64-bit division — the value the inline expansion + // must produce; modeled here as symbolic values state.set_reg(rdlo, BV::new_const("i64_divs_lo", 32)); state.set_reg(rdhi, BV::new_const("i64_divs_hi", 32)); } ArmOp::I64DivU { rdlo, rdhi, .. } => { - // Unsigned 64-bit division - // Real implementation would require __aeabi_uldivmod or equivalent - // For verification, return symbolic values + // Unsigned 64-bit division — same inline-expansion note as + // I64DivS; for verification, return symbolic values state.set_reg(rdlo, BV::new_const("i64_divu_lo", 32)); state.set_reg(rdhi, BV::new_const("i64_divu_hi", 32)); } @@ -700,9 +700,10 @@ impl ArmSemantics { } => { // Signed 64-bit remainder (modulo). Same shape as I64RemU but // the SIGNED remainder (`bvsrem`, SMT-LIB sign-of-dividend). The - // shipped lowering is an `__aeabi_ldivmod` library call; the - // value it must produce is exactly the native 64-bit signed - // remainder. The value VC (`verify_i64_rem_value_preservation`) + // shipped lowering is an inline software long-division + // expansion (arm_encoder.rs, 64-iteration loop — not a library + // call); the value it must produce is exactly the native + // 64-bit signed remainder. The value VC (`verify_i64_rem_value_preservation`) // asserts the R0:R1 pair equals it on the non-trapping path. // rem_s traps ONLY on ÷0 (`rem_s(INT64_MIN,-1) == 0`, no // overflow trap). @@ -730,9 +731,10 @@ impl ArmSemantics { } => { // Unsigned 64-bit remainder (modulo). ARM32 has no 64-bit // divide instruction — the shipped lowering expands this - // pseudo-op to an `__aeabi_uldivmod` library call — but for - // translation-validation the *value* the call must produce is - // exactly the native 64-bit unsigned remainder. Model it with + // pseudo-op INLINE to a software long-division loop + // (arm_encoder.rs, not a library call) — but for + // translation-validation the *value* the expansion must + // produce is exactly the native 64-bit unsigned remainder. Model it with // the native `BvTerm::Urem` (ordeal 0.12, plumbed via // `BV::bvurem`) instead of a HAVOC constant, so the value VC // (`verify_i64_rem_value_preservation`) proves the register diff --git a/crates/synth-verify/src/validator_pattern.rs b/crates/synth-verify/src/validator_pattern.rs index 8f41ff75..c5ee68ef 100644 --- a/crates/synth-verify/src/validator_pattern.rs +++ b/crates/synth-verify/src/validator_pattern.rs @@ -91,12 +91,17 @@ //! multiply — but *remainder* crosses the tractability line. Deferred //! until the validator can discharge the `MLS` identity with a //! multiplier-aware tactic rather than raw bit-blasting. -//! - **i64 div_s / div_u / rem_s / rem_u** — synth lowers 64-bit division to -//! a *runtime-library call* (`__aeabi_ldivmod` and friends); there is no -//! fixed 32-bit ARM instruction sequence to symbolically execute. Modeling -//! a fictitious native 64-bit divide would certify a lowering the compiler -//! never emits. These are deferred until the validator can reason about -//! helper-call summaries. +//! - **i64 div_s / div_u / rem_s / rem_u** — synth expands 64-bit division +//! *inline* to a software long-division sequence with an internal +//! 64-iteration runtime loop (`arm_encoder.rs`, the `I64DivU`/`I64DivS`/ +//! `I64RemU`/`I64RemS` arms; no `__aeabi_*` library call is ever emitted — +//! `__aeabi` appears in this tree only in comments). A looped expansion has +//! no fixed straight-line instruction sequence for this validator's +//! symbolic executor to walk, and unrolling 64 rounds of a symbolic +//! long-division bit-blasts past any practical solver budget (the same +//! tractability line the i32 `MLS` remainder identity already crosses). +//! Deferred until the validator can discharge looped expansions via loop +//! summaries/invariants rather than raw unrolling. //! - **Clz / Ctz / Popcnt** (i32 and i64) — bit-counting. The 32-bit ARM //! `CLZ` is available, but `Ctz`/`Popcnt` are lowered to multi-instruction //! bit-twiddling and `i64.clz/ctz/popcnt` combine two limbs conditionally. diff --git a/docs/status/FEATURE_MATRIX.md b/docs/status/FEATURE_MATRIX.md index 6e0e14f1..80ef3ef9 100644 --- a/docs/status/FEATURE_MATRIX.md +++ b/docs/status/FEATURE_MATRIX.md @@ -69,7 +69,7 @@ see [coq/STATUS.md](../../coq/STATUS.md) for the per-file matrix. | Sail/ASL ISA bridge (VCR-ISA-001) | 92 Qed | `coq/Synth/ARM/SailArmBridge.v` | | ISA-model basis (#867) | 50/50 rule theorems stated against the SIMPLIFIED `ArmSemantics.v` model (0 against the Sail-derived one) · 5 assumed simplified→Sail obligations (`ArmRefinement.v`) · 72 simplified-model axioms | The counted #682-class trusted base — "covered" ≠ "faithful": a Qed against a simplified model is only as good as that model; see `coq/STATUS.md` | | Model coverage (#867 phase 2) | 26 bridge-validated / 68 simplified-only / 4 UNCOVERED modelled `arm_instr` behaviours | The uncovered complement = candidate list for the next silent miscompile (`artifacts/model-coverage.json`, static heuristic labelled as one; complement is an under-approximation) | -| WasmCert-Coq source anchor (VCR-WASM-001) | 104 Qed | `coq/Synth/WASM/WasmCertBridge.v` — i32 integer fragment refined against pinned WasmCert-Coq rules | +| WasmCert-Coq source anchor (VCR-WASM-001) | 104 Qed | `coq/Synth/WASM/WasmCertBridge.v` — i32 (19 ops) + i64 (22 ops) integer fragments refined against pinned WasmCert-Coq rules | | Kani (bounded model checking) | 18 harnesses | ARM encoder properties | | Verus (SMT contracts) | 8 spec functions | `synth-synthesis/src/contracts.rs` | diff --git a/docs/status/POC_ACHIEVEMENTS.md b/docs/status/POC_ACHIEVEMENTS.md index 22be67c0..abb4ec50 100644 --- a/docs/status/POC_ACHIEVEMENTS.md +++ b/docs/status/POC_ACHIEVEMENTS.md @@ -22,7 +22,7 @@ The Synth WebAssembly-to-ARM compiler proof-of-concept has been successfully com - ✅ **Pattern Matching System** - ISLE-inspired rule-based transformation - ✅ **Instruction Selector** - Intelligent WASM → ARM mapping with cost models - ✅ **Peephole Optimizer** - Local optimization passes (redundancy elimination, NOP removal, instruction fusion) -- ✅ **Register Allocator** - Efficient management of R0-R12 registers +- ✅ **Register Allocator** - Efficient management of the R0-R8 temp pool (R9-R11 are runtime-reserved bases, R12 is encoder scratch — see the Verus spec in `crates/synth-synthesis/src/contracts.rs`) #### 2. ARM Code Generation (65+ tests) diff --git a/docs/status/PROJECT_STATUS.md b/docs/status/PROJECT_STATUS.md index b51ff227..ad2fe196 100644 --- a/docs/status/PROJECT_STATUS.md +++ b/docs/status/PROJECT_STATUS.md @@ -1,91 +1,26 @@ -# Synth Project Status - -Last updated: 2026-04-12 - -Synth is a WebAssembly-to-ARM Cortex-M compiler with mechanized correctness proofs. -**This is pre-release software. It has not been tested on physical hardware.** - -## Crates (16) - -| Crate | Purpose | Status | -|-------|---------|--------| -| synth-cli | CLI (`synth compile`, `synth verify`, `synth disasm`) | Implemented | -| synth-core | Shared types, error handling, WASM decoder | Implemented | -| synth-frontend | WASM Component Model parser and validator | Implemented | -| synth-backend | ARM Thumb-2 encoder, ELF builder, vector table, linker | Implemented | -| synth-backend-awsm | aWsm backend integration | Partial | -| synth-backend-wasker | Wasker backend integration | Partial | -| synth-synthesis | WASM to ARM instruction selection, pattern matcher | Implemented | -| synth-cfg | Control flow graph construction and analysis | Implemented | -| synth-opt | IR optimization passes (CSE, constant folding, DCE) | Implemented | -| synth-verify | Z3 SMT translation validation | Implemented | -| synth-analysis | SSA, control flow analysis, call graph | Implemented | -| synth-abi | WebAssembly Component Model ABI (lift/lower) | Implemented | -| synth-memory | Portable memory abstraction (Zephyr, Linux, bare-metal) | Partial | -| synth-qemu | QEMU integration for testing | Implemented | -| synth-test | WAST to Robot Framework test generator for Renode | Implemented | -| synth-wit | WIT parser | Implemented | - -## Tests - -895 tests passing, 0 failing (cargo test --workspace, 2026-04-12). - -## Formal Verification - -### Rocq (Coq) Proofs - -291 Qed / 9 Admitted across all `.v` files in `coq/Synth/`. - -| Tier | Meaning | Count | -|------|---------|-------| -| T1: Result correspondence | ARM output = WASM result value | 35 | -| T2: Existence-only | ARM execution succeeds (no result claim) | 142 | -| T3: Admitted | Trap guards, constants, Sail, Rocq 9 migration | 10 | -| Infrastructure | Integer properties, state lemmas, flag lemmas | 56 | - -See `coq/STATUS.md` for the per-file breakdown. - -### Kani (Bounded Model Checking) - -18 proof harnesses in `crates/synth-backend/tests/kani_arm_encoding.rs`. - -### Z3 (SMT Translation Validation) - -110 Z3-based tests in synth-verify (57 unit + 53 comprehensive). - -### Verus (Deductive Verification) - -8 spec functions in `crates/synth-synthesis/src/contracts.rs` covering register allocation, -instruction encoding, memory access, and division trap invariants. - -## What Works - -- **i32 operations**: All arithmetic, bitwise, comparison, shift/rotate, division. - Fully implemented, tested, and proven (39 T1 result-correspondence proofs in Rocq). -- **i64 operations**: Register-pair architecture for 64-bit on ARM32. - Implemented and tested. Rocq proofs at T2 level (execution succeeds) plus 4 T1 division proofs. -- **f32/f64 operations**: VFP single/double precision. Implemented and tested. - Rocq proofs at T2 level using abstract VFP axioms (not Flocq IEEE 754). -- **Control flow**: block, loop, br, br_if, br_table, call, return. -- **Memory**: i32/i64/f32/f64 load/store with bounds checking. -- **ELF output**: Produces bare-metal ELF binaries for Cortex-M4. -- **Renode emulation tests**: WAST-derived Robot Framework tests run on emulated Cortex-M4. - -## What Is Partial - -- **i64 proofs**: T2 existence proofs only (except division). No T1 result correspondence for - arithmetic, bitwise, comparison, or shift operations. -- **Float proofs**: T2 existence proofs using abstract axioms. Upgrading to T1 requires Flocq - IEEE 754 integration. -- **Component Model**: WIT parser and ABI lift/lower implemented; end-to-end integration incomplete. -- **Alternative backends**: awsm and wasker backends are stubs/partial. - -## What Is Missing - -- No testing on physical ARM hardware (Renode emulation only). -- No WASI support. -- SIMD (v128) Helium MVE encoding is experimental (Cortex-M55 only, untested on hardware). -- No reference types. -- No multi-memory. -- No bulk memory operations. -- No performance benchmarks. +# Synth Project Status — moved + +This file used to restate project status by hand and was pinned by nothing — +by the time of the #946 doc sweep it was ~16 months stale (it said 291 Qed +while the tree held 592, 16 crates while the workspace held 18, named Z3 as +the default validator three eras after ordeal replaced it, and listed +multi-memory and bulk memory as missing after both had shipped and been +claim-pinned). Restating status in a second place is how status goes stale, +so the restatement is deleted rather than re-synced. + +Current status lives in the sources of truth: + +- **[`docs/status/FEATURE_MATRIX.md`](FEATURE_MATRIX.md)** — the generated + op-surface and capability matrix (rendered from + `scripts/templates/feature_matrix.md.tmpl` by + `python3 scripts/claim_check.py claims.yaml --emit-status`; staleness-gated + in CI). +- **`artifacts/status.json`** — the machine-derived numbers (proof counts, + rule counts, harness counts; re-derived on every commit by the claim gate). +- **[`coq/STATUS.md`](../../coq/STATUS.md)** — Rocq proof coverage, per-file + breakdown, tiers, and the trusted base. +- **`artifacts/verified-codegen-roadmap.yaml`** — VCR-* roadmap statuses + (single source for roadmap claims). +- **[`README.md`](../../README.md)** — the prose overview, whose load-bearing + claims are pinned in `claims.yaml` and re-derived by + `scripts/claim_check.py` in CI. diff --git a/scripts/templates/feature_matrix.md.tmpl b/scripts/templates/feature_matrix.md.tmpl index 64e2343c..7619e358 100644 --- a/scripts/templates/feature_matrix.md.tmpl +++ b/scripts/templates/feature_matrix.md.tmpl @@ -69,7 +69,7 @@ see [coq/STATUS.md](../../coq/STATUS.md) for the per-file matrix. | Sail/ASL ISA bridge (VCR-ISA-001) | {{sail_bridge_qed}} Qed | `coq/Synth/ARM/SailArmBridge.v` | | ISA-model basis (#867) | {{sel_rules_simplified_basis}}/{{sel_dsl_rule_qed}} rule theorems stated against the SIMPLIFIED `ArmSemantics.v` model (0 against the Sail-derived one) · {{arm_refinement_assumed_connection}} assumed simplified→Sail obligations (`ArmRefinement.v`) · {{arm_semantics_axioms}} simplified-model axioms | The counted #682-class trusted base — "covered" ≠ "faithful": a Qed against a simplified model is only as good as that model; see `coq/STATUS.md` | | Model coverage (#867 phase 2) | {{isa_model_bridge_validated}} bridge-validated / {{isa_model_simplified_only}} simplified-only / {{isa_model_uncovered}} UNCOVERED modelled `arm_instr` behaviours | The uncovered complement = candidate list for the next silent miscompile (`artifacts/model-coverage.json`, static heuristic labelled as one; complement is an under-approximation) | -| WasmCert-Coq source anchor (VCR-WASM-001) | {{wasmcert_bridge_qed}} Qed | `coq/Synth/WASM/WasmCertBridge.v` — i32 integer fragment refined against pinned WasmCert-Coq rules | +| WasmCert-Coq source anchor (VCR-WASM-001) | {{wasmcert_bridge_qed}} Qed | `coq/Synth/WASM/WasmCertBridge.v` — i32 (19 ops) + i64 (22 ops) integer fragments refined against pinned WasmCert-Coq rules | | Kani (bounded model checking) | {{kani_harnesses}} harnesses | ARM encoder properties | | Verus (SMT contracts) | {{verus_spec_fns}} spec functions | `synth-synthesis/src/contracts.rs` |