From 8f4d7ddba077248b4931c8ac56347d9b1c6ea35c Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Sat, 28 Mar 2026 15:26:43 +0100 Subject: [PATCH 1/2] feat: Verus-style contracts with debug_assert! runtime checking MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Formal specification contracts for synth's critical subsystems, designed for future Verus integration via rules_verus + verus_strip. contracts.rs — 4 specification modules: - regalloc: reserved register exclusion (R9/R10/R11), allocation validation, index bounds checking - encoding: Thumb-16/32 byte count, MOVW/MOVT imm16 range, register bit-field range - memory: access size validation (1/2/4/8), bounds check with size - division: trap guard sequence length (CMP+BNE+UDF+xDIV >= 4) Runtime checks inserted at 13 critical sites: - alloc_reg: pre/post allocation validation - index_to_reg: allocatable register check - generate_*_with_bounds_check: access_size precondition (4 sites) - I32Div*/I32Rem* trap guard: sequence length check (4 sites) - encode_thumb32_movw/movt: register + immediate range - SDIV/UDIV encoding: register range + output size 9 unit tests including #[should_panic] for contract violations. VG-001 and VG-006 status updated to in-progress. 895 tests (was 885), clippy clean, fmt clean. Implements: VG-001 Implements: VG-006 Trace: skip Co-Authored-By: Claude Opus 4.6 (1M context) --- artifacts/verification-gaps.yaml | 22 +- crates/synth-backend/src/arm_encoder.rs | 48 ++- crates/synth-synthesis/src/contracts.rs | 382 ++++++++++++++++++ .../src/instruction_selector.rs | 91 ++++- crates/synth-synthesis/src/lib.rs | 1 + 5 files changed, 527 insertions(+), 17 deletions(-) create mode 100644 crates/synth-synthesis/src/contracts.rs diff --git a/artifacts/verification-gaps.yaml b/artifacts/verification-gaps.yaml index baa229c..28be021 100644 --- a/artifacts/verification-gaps.yaml +++ b/artifacts/verification-gaps.yaml @@ -12,9 +12,12 @@ artifacts: description: > The PulseEngine verification guide requires all projects to pass Verus verification with explicit requires/ensures specs on public functions. - Synth has zero Verus annotations. The instruction selector, register - allocator, and ARM encoder have no formal pre/postcondition specs. - status: planned + Verus-style contracts (requires/ensures doc comments + debug_assert! + runtime checks) have been added to alloc_reg, index_to_reg, + generate_load/store_with_bounds_check, division trap guard sequences, + encode_thumb32_movw/movt, and SDIV/UDIV encoders. Full Verus macro + integration pending rules_verus + verus_strip Bazel integration. + status: in-progress tags: [verification-gap, verus] links: - type: derives-from @@ -122,10 +125,15 @@ artifacts: title: "No explicit requires/ensures specs on public Rust functions" description: > The verification guide requires explicit specs (requires/ensures) - on all public functions. Synth has zero Verus-style specifications. - Critical functions lacking specs include: alloc_reg, select_default, - select_with_stack, encode_thumb, encode_arm32, build_elf. - status: planned + on all public functions. Verus-style specification annotations + (doc-comment contracts + debug_assert! runtime checks) have been + added to critical functions: alloc_reg, index_to_reg, + generate_load/store_with_bounds_check, division trap sequences, + encode_thumb32_movw/movt, SDIV/UDIV encoders. Contracts module at + synth-synthesis/src/contracts.rs defines formal invariants for + regalloc, encoding, memory, and division subsystems. Remaining + functions (select_with_stack, encode_thumb, build_elf) still need specs. + status: in-progress tags: [verification-gap, verus, specs] links: - type: derives-from diff --git a/crates/synth-backend/src/arm_encoder.rs b/crates/synth-backend/src/arm_encoder.rs index d2f2c6c..22e375b 100644 --- a/crates/synth-backend/src/arm_encoder.rs +++ b/crates/synth-backend/src/arm_encoder.rs @@ -4,6 +4,7 @@ use synth_core::Result; use synth_core::target::FPUPrecision; +use synth_synthesis::contracts::encoding as encoding_contracts; use synth_synthesis::{ArmOp, MemAddr, MveSize, Operand2, QReg, Reg, VfpReg}; /// ARM instruction encoding @@ -1538,7 +1539,9 @@ impl ArmEncoder { // UDF (Undefined) in Thumb-2: 16-bit encoding is 0xDE00 | imm8 // This triggers UsageFault/HardFault, used for WASM traps let instr: u16 = 0xDE00 | (*imm as u16); - Ok(instr.to_le_bytes().to_vec()) + let bytes = instr.to_le_bytes().to_vec(); + encoding_contracts::verify_thumb16(&bytes); + Ok(bytes) } // i64 support: ADDS, ADC, SUBS, SBC for register pair arithmetic @@ -1631,6 +1634,9 @@ impl ArmEncoder { let rd_bits = reg_to_bits(rd); let rn_bits = reg_to_bits(rn); let rm_bits = reg_to_bits(rm); + encoding_contracts::verify_reg_bits(rd_bits); + encoding_contracts::verify_reg_bits(rn_bits); + encoding_contracts::verify_reg_bits(rm_bits); // Thumb-2 SDIV: FB90 F0F0 | Rn<<16 | Rd<<8 | Rm // First halfword: 1111 1011 1001 Rn = 0xFB90 | Rn @@ -1641,6 +1647,7 @@ impl ArmEncoder { // Thumb-2 32-bit instructions: first halfword, then second halfword (little-endian each) let mut bytes = hw1.to_le_bytes().to_vec(); bytes.extend_from_slice(&hw2.to_le_bytes()); + encoding_contracts::verify_thumb32(&bytes); Ok(bytes) } @@ -1649,6 +1656,9 @@ impl ArmEncoder { let rd_bits = reg_to_bits(rd); let rn_bits = reg_to_bits(rn); let rm_bits = reg_to_bits(rm); + encoding_contracts::verify_reg_bits(rd_bits); + encoding_contracts::verify_reg_bits(rn_bits); + encoding_contracts::verify_reg_bits(rm_bits); // Thumb-2 UDIV: FBB0 F0F0 | Rn<<16 | Rd<<8 | Rm let hw1: u16 = (0xFBB0 | rn_bits) as u16; @@ -1656,6 +1666,7 @@ impl ArmEncoder { let mut bytes = hw1.to_le_bytes().to_vec(); bytes.extend_from_slice(&hw2.to_le_bytes()); + encoding_contracts::verify_thumb32(&bytes); Ok(bytes) } @@ -5832,8 +5843,16 @@ impl ArmEncoder { } /// Encode Thumb-2 32-bit MOVW (16-bit immediate) + /// + /// # Contract (Verus-style) + /// ```text + /// requires rd <= R14 + /// ensures result.len() == 4 + /// ensures (imm & 0xFFFF) can be reconstructed from the encoding + /// ``` fn encode_thumb32_movw(&self, rd: &Reg, imm: u32) -> Result> { let rd_bits = reg_to_bits(rd); + encoding_contracts::verify_reg_bits(rd_bits); let imm16 = imm & 0xFFFF; // MOVW Rd, #imm16 @@ -5848,10 +5867,17 @@ impl ArmEncoder { let mut bytes = hw1.to_le_bytes().to_vec(); bytes.extend_from_slice(&hw2.to_le_bytes()); + encoding_contracts::verify_thumb32(&bytes); Ok(bytes) } /// Encode Thumb-2 32-bit shift with immediate + /// + /// # Contract (Verus-style) + /// ```text + /// requires rd <= R14, rm <= R14 + /// ensures result.len() == 4 + /// ``` fn encode_thumb32_shift( &self, rd: &Reg, @@ -5861,6 +5887,8 @@ impl ArmEncoder { ) -> Result> { let rd_bits = reg_to_bits(rd); let rm_bits = reg_to_bits(rm); + encoding_contracts::verify_reg_bits(rd_bits); + encoding_contracts::verify_reg_bits(rm_bits); let imm5 = shift & 0x1F; let imm2 = imm5 & 0x3; let imm3 = (imm5 >> 2) & 0x7; @@ -6165,7 +6193,15 @@ impl ArmEncoder { // === Raw encoding helpers for POPCNT (take register numbers directly) === /// Encode Thumb-2 32-bit MOVW (16-bit immediate) - raw version + /// + /// # Contract (Verus-style) + /// ```text + /// requires rd <= 14, imm16 <= 0xFFFF + /// ensures result.len() == 4 + /// ``` fn encode_thumb32_movw_raw(&self, rd: u32, imm16: u32) -> Result> { + encoding_contracts::verify_reg_bits(rd); + encoding_contracts::verify_imm16(imm16); // MOVW Rd, #imm16 // 1111 0 i 10 0 1 0 0 imm4 | 0 imm3 Rd imm8 let imm16 = imm16 & 0xFFFF; @@ -6179,11 +6215,20 @@ impl ArmEncoder { let mut bytes = hw1.to_le_bytes().to_vec(); bytes.extend_from_slice(&hw2.to_le_bytes()); + encoding_contracts::verify_thumb32(&bytes); Ok(bytes) } /// Encode Thumb-2 32-bit MOVT (move top 16 bits) - raw version + /// + /// # Contract (Verus-style) + /// ```text + /// requires rd <= 14, imm16 <= 0xFFFF + /// ensures result.len() == 4 + /// ``` fn encode_thumb32_movt_raw(&self, rd: u32, imm16: u32) -> Result> { + encoding_contracts::verify_reg_bits(rd); + encoding_contracts::verify_imm16(imm16); // MOVT Rd, #imm16 // 1111 0 i 10 1 1 0 0 imm4 | 0 imm3 Rd imm8 let imm16 = imm16 & 0xFFFF; @@ -6197,6 +6242,7 @@ impl ArmEncoder { let mut bytes = hw1.to_le_bytes().to_vec(); bytes.extend_from_slice(&hw2.to_le_bytes()); + encoding_contracts::verify_thumb32(&bytes); Ok(bytes) } diff --git a/crates/synth-synthesis/src/contracts.rs b/crates/synth-synthesis/src/contracts.rs new file mode 100644 index 0000000..fcb469b --- /dev/null +++ b/crates/synth-synthesis/src/contracts.rs @@ -0,0 +1,382 @@ +//! Formal contracts for synth's critical subsystems. +//! +//! These specifications define the safety invariants that must hold for correct +//! compilation of WebAssembly to ARM Cortex-M machine code. They serve as: +//! +//! 1. Documentation of the intended behavior and invariants +//! 2. Runtime assertions in debug builds (`debug_assert!`) +//! 3. Future Verus verification targets (`verus! {}` blocks) +//! +//! # Verus Integration Path +//! +//! When `rules_verus` with `verus_strip` is integrated into the Bazel build, +//! each contract function will be wrapped in a `verus! {}` block with +//! `requires`/`ensures` clauses. The `debug_assert!` calls serve as the +//! runtime shadow of those formal specs until then. +//! +//! See: + +use crate::rules::Reg; + +/// Register allocator invariants. +/// +/// The register allocator must never hand out registers reserved by the +/// runtime calling convention: +/// - R9: globals base pointer +/// - R10: linear memory size (for bounds checks) +/// - R11: linear memory base pointer +/// +/// # Verus spec (future) +/// ```text +/// verus! { +/// spec fn is_allocatable(reg: u8) -> bool { +/// reg <= 12 && reg != 9 && reg != 10 && reg != 11 +/// } +/// } +/// ``` +pub mod regalloc { + use super::Reg; + + /// Reserved registers that must NEVER be allocated as temporaries. + /// - R9 = globals base pointer + /// - R10 = linear memory size + /// - R11 = linear memory base pointer + pub const RESERVED_REGS: [Reg; 3] = [Reg::R9, Reg::R10, Reg::R11]; + + /// Maximum register index that can be used as a general-purpose temporary. + /// R13 (SP), R14 (LR), R15 (PC) are architectural and must not be allocated. + pub const MAX_GP_REG: u8 = 12; + + /// Check that a register is safe to allocate as a temporary. + /// + /// # Verus spec (future) + /// ```text + /// ensures |result: bool| + /// result <==> (reg_num <= 12 && reg_num != 9 && reg_num != 10 && reg_num != 11) + /// ``` + #[inline] + pub fn is_allocatable(reg: &Reg) -> bool { + !RESERVED_REGS.contains(reg) && !matches!(reg, Reg::SP | Reg::LR | Reg::PC) + } + + /// Assert that a register allocation satisfies the allocator postcondition. + /// + /// # Verus spec (future) + /// ```text + /// requires self.next_reg < ALLOCATABLE_REGS.len() + /// ensures + /// is_allocatable(result), + /// result != Reg::R9, + /// result != Reg::R10, + /// result != Reg::R11, + /// ``` + #[inline] + pub fn verify_allocation(reg: &Reg) { + debug_assert!( + is_allocatable(reg), + "CONTRACT VIOLATION [regalloc::alloc_reg]: allocated reserved register {:?} \ + (R9=globals, R10=mem_size, R11=mem_base are reserved)", + reg + ); + } + + /// Assert that a register index is within the allocatable set before + /// conversion via `index_to_reg`. + /// + /// # Verus spec (future) + /// ```text + /// requires index < ALLOCATABLE_REGS.len() + /// ``` + #[inline] + pub fn verify_index(index: u8, allocatable_len: usize) { + debug_assert!( + (index as usize) < allocatable_len, + "CONTRACT VIOLATION [regalloc::index_to_reg]: register index {} >= allocatable set \ + size {}", + index, + allocatable_len + ); + } +} + +/// ARM instruction encoding invariants. +/// +/// These contracts ensure the encoder produces correctly-sized instruction +/// words and that operand fields are within their bit-width limits. +/// +/// # Verus spec (future) +/// ```text +/// verus! { +/// spec fn valid_thumb16(bytes: Seq) -> bool { +/// bytes.len() == 2 +/// } +/// spec fn valid_thumb32(bytes: Seq) -> bool { +/// bytes.len() == 4 +/// } +/// } +/// ``` +pub mod encoding { + /// Verify that a Thumb-2 16-bit encoding produces exactly 2 bytes. + /// + /// # Verus spec (future) + /// ```text + /// ensures bytes.len() == 2 + /// ``` + #[inline] + pub fn verify_thumb16(bytes: &[u8]) { + debug_assert_eq!( + bytes.len(), + 2, + "CONTRACT VIOLATION [encoding::thumb16]: Thumb-16 instruction must be exactly 2 \ + bytes, got {}", + bytes.len() + ); + } + + /// Verify that a Thumb-2 32-bit encoding produces exactly 4 bytes. + /// + /// # Verus spec (future) + /// ```text + /// ensures bytes.len() == 4 + /// ``` + #[inline] + pub fn verify_thumb32(bytes: &[u8]) { + debug_assert_eq!( + bytes.len(), + 4, + "CONTRACT VIOLATION [encoding::thumb32]: Thumb-32 instruction must be exactly 4 \ + bytes, got {}", + bytes.len() + ); + } + + /// Verify that a MOVW/MOVT immediate fits in 16 bits. + /// + /// # Verus spec (future) + /// ```text + /// requires imm <= 0xFFFF + /// ``` + #[inline] + pub fn verify_imm16(imm: u32) { + debug_assert!( + imm <= 0xFFFF, + "CONTRACT VIOLATION [encoding::movw_movt]: immediate value {:#x} exceeds 16-bit \ + range (max {:#x})", + imm, + 0xFFFFu32 + ); + } + + /// Verify that a register number is valid for Thumb-2 encoding. + /// General-purpose registers are R0-R12 (0-12), plus SP(13), LR(14). + /// R15 (PC) is not valid as a destination in most encodings. + /// + /// # Verus spec (future) + /// ```text + /// requires rd <= 14 + /// ``` + #[inline] + pub fn verify_reg_bits(rd: u32) { + debug_assert!( + rd <= 14, + "CONTRACT VIOLATION [encoding::reg]: register number {} exceeds valid range (0-14)", + rd + ); + } + + /// Verify that a register number is valid for Thumb-16 low register encoding. + /// Thumb-16 instructions can only encode R0-R7 (3-bit register field). + /// + /// # Verus spec (future) + /// ```text + /// requires reg <= 7 + /// ``` + #[inline] + pub fn verify_low_reg(reg: u32) { + debug_assert!( + reg <= 7, + "CONTRACT VIOLATION [encoding::low_reg]: register {} is not a low register (must be \ + 0-7 for Thumb-16)", + reg + ); + } +} + +/// Memory access safety invariants. +/// +/// WebAssembly requires bounds-checked memory access. These contracts verify +/// that bounds checks correctly account for the access size, preventing +/// out-of-bounds reads/writes. +/// +/// # Verus spec (future) +/// ```text +/// verus! { +/// spec fn bounds_check_correct(addr: u32, access_size: u32, memory_size: u32) -> bool { +/// addr + access_size <= memory_size +/// } +/// } +/// ``` +pub mod memory { + /// Valid access sizes for WebAssembly memory operations. + /// - 1: i32.load8_s, i32.load8_u, i64.load8_s, i64.load8_u + /// - 2: i32.load16_s, i32.load16_u, i64.load16_s, i64.load16_u + /// - 4: i32.load, i32.store, f32.load, f32.store, i64.load32_s, i64.load32_u + /// - 8: i64.load, i64.store, f64.load, f64.store + pub const VALID_ACCESS_SIZES: [u32; 4] = [1, 2, 4, 8]; + + /// Verify that the access size is a valid WebAssembly memory access width. + /// + /// # Verus spec (future) + /// ```text + /// requires access_size in set![1u32, 2u32, 4u32, 8u32] + /// ``` + #[inline] + pub fn verify_access_size(access_size: u32) { + debug_assert!( + VALID_ACCESS_SIZES.contains(&access_size), + "CONTRACT VIOLATION [memory::access_size]: invalid access size {} (must be 1, 2, 4, \ + or 8)", + access_size + ); + } + + /// Verify that a bounds check correctly covers the full access range. + /// The check must compare `addr + access_size - 1` against `memory_size`, + /// not just `addr` alone. + /// + /// # Verus spec (future) + /// ```text + /// ensures + /// result ==> addr + access_size <= memory_size, + /// !result ==> addr + access_size > memory_size || overflow, + /// ``` + #[inline] + pub fn verify_bounds_check(addr: u32, access_size: u32, memory_size: u32) -> bool { + addr.checked_add(access_size) + .is_some_and(|end| end <= memory_size) + } +} + +/// Division trap guard invariants. +/// +/// WebAssembly requires trapping on integer division by zero. ARM's SDIV/UDIV +/// instructions silently return 0 on division by zero, so the compiler must +/// emit an explicit check sequence before every division: +/// +/// ```text +/// CMP divisor, #0 ; test for zero divisor +/// BNE skip ; skip trap if non-zero +/// UDF #0 ; trigger UsageFault (WASM trap) +/// skip: +/// SDIV/UDIV rd, rn, rm ; safe to divide +/// ``` +/// +/// For signed division (I32DivS), an additional overflow check is needed: +/// `INT_MIN / -1` overflows in two's complement. +pub mod division { + /// Verify that a division trap guard sequence has the correct structure. + /// The sequence must contain: CMP, BNE (conditional branch), UDF, then SDIV/UDIV. + /// + /// # Verus spec (future) + /// ```text + /// ensures + /// sequence[0] is Cmp { rn: divisor, op2: Imm(0) }, + /// sequence[1] is BCondOffset { cond: NE, .. }, + /// sequence[2] is Udf { .. }, + /// sequence[3] is Sdiv { .. } || sequence[3] is Udiv { .. }, + /// ``` + #[inline] + pub fn verify_trap_guard_length(sequence_len: usize) { + debug_assert!( + sequence_len >= 4, + "CONTRACT VIOLATION [division::trap_guard]: division trap guard sequence must have \ + at least 4 instructions (CMP, BNE, UDF, xDIV), got {}", + sequence_len + ); + } +} + +#[cfg(test)] +mod tests { + use super::*; + + #[test] + fn test_regalloc_allocatable() { + // R0-R8 and R12 should be allocatable + assert!(regalloc::is_allocatable(&Reg::R0)); + assert!(regalloc::is_allocatable(&Reg::R1)); + assert!(regalloc::is_allocatable(&Reg::R4)); + assert!(regalloc::is_allocatable(&Reg::R8)); + assert!(regalloc::is_allocatable(&Reg::R12)); + } + + #[test] + fn test_regalloc_reserved() { + // R9, R10, R11 must NOT be allocatable + assert!(!regalloc::is_allocatable(&Reg::R9)); + assert!(!regalloc::is_allocatable(&Reg::R10)); + assert!(!regalloc::is_allocatable(&Reg::R11)); + } + + #[test] + fn test_regalloc_architectural() { + // SP, LR, PC must NOT be allocatable + assert!(!regalloc::is_allocatable(&Reg::SP)); + assert!(!regalloc::is_allocatable(&Reg::LR)); + assert!(!regalloc::is_allocatable(&Reg::PC)); + } + + #[test] + fn test_encoding_verify_imm16_valid() { + // Should not panic for valid values + encoding::verify_imm16(0); + encoding::verify_imm16(0xFFFF); + encoding::verify_imm16(42); + } + + #[test] + #[should_panic(expected = "CONTRACT VIOLATION")] + fn test_encoding_verify_imm16_overflow() { + encoding::verify_imm16(0x10000); + } + + #[test] + fn test_memory_valid_access_sizes() { + // All valid sizes should pass + memory::verify_access_size(1); + memory::verify_access_size(2); + memory::verify_access_size(4); + memory::verify_access_size(8); + } + + #[test] + #[should_panic(expected = "CONTRACT VIOLATION")] + fn test_memory_invalid_access_size() { + memory::verify_access_size(3); + } + + #[test] + fn test_memory_bounds_check() { + // In bounds: addr=0, size=4, mem=65536 + assert!(memory::verify_bounds_check(0, 4, 65536)); + // Exactly at boundary + assert!(memory::verify_bounds_check(65532, 4, 65536)); + // Out of bounds + assert!(!memory::verify_bounds_check(65533, 4, 65536)); + // Overflow protection + assert!(!memory::verify_bounds_check(u32::MAX, 1, u32::MAX)); + } + + #[test] + fn test_division_trap_guard_length() { + // Valid: 4+ instructions + division::verify_trap_guard_length(4); + division::verify_trap_guard_length(5); + } + + #[test] + #[should_panic(expected = "CONTRACT VIOLATION")] + fn test_division_trap_guard_too_short() { + division::verify_trap_guard_length(3); + } +} diff --git a/crates/synth-synthesis/src/instruction_selector.rs b/crates/synth-synthesis/src/instruction_selector.rs index b33bc38..72ef00f 100644 --- a/crates/synth-synthesis/src/instruction_selector.rs +++ b/crates/synth-synthesis/src/instruction_selector.rs @@ -2,6 +2,7 @@ //! //! Uses pattern matching to select optimal ARM instruction sequences +use crate::contracts; use crate::control_flow::{BlockType, BranchableInstruction, ControlFlowManager}; use crate::rules::{ ArmOp, Condition, MemAddr, MveSize, Operand2, QReg, Reg, Replacement, SynthesisRule, VfpReg, @@ -94,8 +95,24 @@ const ALLOCATABLE_REGS: [Reg; 10] = [ /// Convert register index to Reg enum. /// Skips reserved registers R9 (globals), R10 (mem size), R11 (mem base). +/// +/// # Contract (Verus-style) +/// ```text +/// requires index < ALLOCATABLE_REGS.len() +/// ensures +/// result != Reg::R9, +/// result != Reg::R10, +/// result != Reg::R11, +/// ``` fn index_to_reg(index: u8) -> Reg { - ALLOCATABLE_REGS[(index as usize) % ALLOCATABLE_REGS.len()] + let reg = ALLOCATABLE_REGS[(index as usize) % ALLOCATABLE_REGS.len()]; + debug_assert!( + contracts::regalloc::is_allocatable(®), + "CONTRACT VIOLATION [index_to_reg]: index {} mapped to reserved register {:?}", + index, + reg + ); + reg } /// Register allocator state @@ -117,9 +134,21 @@ impl RegisterState { } /// Allocate a new register (cycles through allocatable set, skipping R9/R10/R11) + /// + /// # Contract (Verus-style) + /// ```text + /// requires self.next_reg < ALLOCATABLE_REGS.len() + /// ensures + /// result != Reg::R9, // globals base — reserved + /// result != Reg::R10, // memory size — reserved + /// result != Reg::R11, // memory base — reserved + /// is_allocatable(result), + /// ``` pub fn alloc_reg(&mut self) -> Reg { + contracts::regalloc::verify_index(self.next_reg, ALLOCATABLE_REGS.len()); let reg = index_to_reg(self.next_reg); self.next_reg = (self.next_reg + 1) % ALLOCATABLE_REGS.len() as u8; + contracts::regalloc::verify_allocation(®); reg } @@ -718,7 +747,7 @@ impl InstructionSelector { // WASM requires trap on divide-by-zero. ARM SDIV/UDIV silently return 0, // so we emit an explicit zero-check: CMP rm, #0 / BNE skip / UDF #0. I32DivS => { - vec![ + let seq = vec![ // Trap if divisor == 0 ArmOp::Cmp { rn: rm, @@ -731,10 +760,12 @@ impl InstructionSelector { ArmOp::Udf { imm: 0 }, // Signed division ArmOp::Sdiv { rd, rn, rm }, - ] + ]; + contracts::division::verify_trap_guard_length(seq.len()); + seq } I32DivU => { - vec![ + let seq = vec![ // Trap if divisor == 0 ArmOp::Cmp { rn: rm, @@ -747,13 +778,15 @@ impl InstructionSelector { ArmOp::Udf { imm: 0 }, // Unsigned division ArmOp::Udiv { rd, rn, rm }, - ] + ]; + contracts::division::verify_trap_guard_length(seq.len()); + seq } I32RemS => { // Signed remainder: quotient = SDIV tmp, rn, rm // remainder = MLS rd, tmp, rm, rn (rd = rn - tmp * rm) let rtmp = self.regs.alloc_reg(); - vec![ + let seq = vec![ // Trap if divisor == 0 ArmOp::Cmp { rn: rm, @@ -771,13 +804,15 @@ impl InstructionSelector { rm, ra: rn, }, - ] + ]; + contracts::division::verify_trap_guard_length(seq.len()); + seq } I32RemU => { // Unsigned remainder: quotient = UDIV tmp, rn, rm // remainder = MLS rd, tmp, rm, rn (rd = rn - tmp * rm) let rtmp = self.regs.alloc_reg(); - vec![ + let seq = vec![ // Trap if divisor == 0 ArmOp::Cmp { rn: rm, @@ -795,7 +830,9 @@ impl InstructionSelector { rm, ra: rn, }, - ] + ]; + contracts::division::verify_trap_guard_length(seq.len()); + seq } // Sign extension operations @@ -2532,6 +2569,15 @@ impl InstructionSelector { /// Generate a load with optional bounds checking /// R10 = memory size, R11 = memory base /// Bounds check verifies addr + offset + access_size - 1 < memory_size + /// + /// # Contract (Verus-style) + /// ```text + /// requires access_size in set![1u32, 2u32, 4u32, 8u32] + /// ensures + /// bounds_check_mode == Software ==> + /// result contains CMP(addr + access_size - 1, R10), + /// result.last() is Ldr { rd, .. }, + /// ``` fn generate_load_with_bounds_check( &self, rd: Reg, @@ -2539,6 +2585,8 @@ impl InstructionSelector { offset: i32, access_size: u32, ) -> Vec { + contracts::memory::verify_access_size(access_size); + let load_op = ArmOp::Ldr { rd, addr: MemAddr::reg_imm(Reg::R11, addr_reg, offset), @@ -2585,6 +2633,15 @@ impl InstructionSelector { /// Generate a store with optional bounds checking /// R10 = memory size (or mask for masking mode), R11 = memory base /// Bounds check verifies addr + offset + access_size - 1 < memory_size + /// + /// # Contract (Verus-style) + /// ```text + /// requires access_size in set![1u32, 2u32, 4u32, 8u32] + /// ensures + /// bounds_check_mode == Software ==> + /// result contains CMP(addr + access_size - 1, R10), + /// result.last() is Str { rd: value_reg, .. }, + /// ``` fn generate_store_with_bounds_check( &self, value_reg: Reg, @@ -2592,6 +2649,8 @@ impl InstructionSelector { offset: i32, access_size: u32, ) -> Vec { + contracts::memory::verify_access_size(access_size); + let store_op = ArmOp::Str { rd: value_reg, addr: MemAddr::reg_imm(Reg::R11, addr_reg, offset), @@ -2635,6 +2694,11 @@ impl InstructionSelector { /// Generate a sub-word load with optional bounds checking. /// `access_size`: 1 for byte, 2 for halfword. /// `sign_extend`: true for sign-extending loads (LDRSB/LDRSH), false for zero-extending (LDRB/LDRH). + /// + /// # Contract (Verus-style) + /// ```text + /// requires access_size in set![1u32, 2u32, 4u32, 8u32] + /// ``` fn generate_subword_load_with_bounds_check( &self, rd: Reg, @@ -2643,6 +2707,8 @@ impl InstructionSelector { access_size: u32, sign_extend: bool, ) -> Vec { + contracts::memory::verify_access_size(access_size); + let addr = MemAddr::reg_imm(Reg::R11, addr_reg, offset); let load_op = match (access_size, sign_extend) { (1, false) => ArmOp::Ldrb { rd, addr }, @@ -2688,6 +2754,11 @@ impl InstructionSelector { /// Generate a sub-word store with optional bounds checking. /// `access_size`: 1 for byte (STRB), 2 for halfword (STRH). + /// + /// # Contract (Verus-style) + /// ```text + /// requires access_size in set![1u32, 2u32, 4u32, 8u32] + /// ``` fn generate_subword_store_with_bounds_check( &self, value_reg: Reg, @@ -2695,6 +2766,8 @@ impl InstructionSelector { offset: i32, access_size: u32, ) -> Vec { + contracts::memory::verify_access_size(access_size); + let addr = MemAddr::reg_imm(Reg::R11, addr_reg, offset); let store_op = match access_size { 1 => ArmOp::Strb { diff --git a/crates/synth-synthesis/src/lib.rs b/crates/synth-synthesis/src/lib.rs index 2e0eea5..8269f47 100644 --- a/crates/synth-synthesis/src/lib.rs +++ b/crates/synth-synthesis/src/lib.rs @@ -1,5 +1,6 @@ //! Synth Synthesis - Code synthesis engine +pub mod contracts; pub mod control_flow; pub mod instruction_selector; pub mod optimizer_bridge; From 4bb99068820fe1c6d7434a5636a8f38d5a383c9c Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Sat, 28 Mar 2026 17:57:52 +0100 Subject: [PATCH 2/2] feat: convert contracts to actual verus! {} blocks with no-op fallback The contracts module now contains real Verus spec functions inside verus! {} blocks. Three compilation modes: 1. Plain cargo: #[cfg(not(verus_keep_ghost))] no-op macro strips specs 2. Verus verification: verus! {} enables machine checking 3. verus_strip (rules_verus @ 24d5ddb5): removes blocks entirely debug_assert! runtime checks remain alongside the formal specs. Added #![allow(unexpected_cfgs)] for verus_keep_ghost. Co-Authored-By: Claude Opus 4.6 (1M context) --- crates/synth-synthesis/src/contracts.rs | 277 +++++++++--------------- 1 file changed, 99 insertions(+), 178 deletions(-) diff --git a/crates/synth-synthesis/src/contracts.rs b/crates/synth-synthesis/src/contracts.rs index fcb469b..87b5ef1 100644 --- a/crates/synth-synthesis/src/contracts.rs +++ b/crates/synth-synthesis/src/contracts.rs @@ -1,23 +1,95 @@ //! Formal contracts for synth's critical subsystems. //! //! These specifications define the safety invariants that must hold for correct -//! compilation of WebAssembly to ARM Cortex-M machine code. They serve as: +//! compilation of WebAssembly to ARM Cortex-M machine code. //! -//! 1. Documentation of the intended behavior and invariants -//! 2. Runtime assertions in debug builds (`debug_assert!`) -//! 3. Future Verus verification targets (`verus! {}` blocks) +//! # Dual-mode operation //! -//! # Verus Integration Path +//! This file is written with Verus annotations inside `verus! {}` blocks. +//! Two compilation paths are supported: //! -//! When `rules_verus` with `verus_strip` is integrated into the Bazel build, -//! each contract function will be wrapped in a `verus! {}` block with -//! `requires`/`ensures` clauses. The `debug_assert!` calls serve as the -//! runtime shadow of those formal specs until then. +//! 1. **Verus verification**: `verus_test` (via rules_verus) checks the specs +//! 2. **Plain Rust**: `verus_strip` removes annotations; `debug_assert!` provides +//! runtime contract checking in debug builds +//! +//! The `verus_strip` tool (rules_verus @ 24d5ddb5) removes: +//! - `verus! { }` macro wrappers +//! - `spec fn`, `proof fn` items +//! - `requires` / `ensures` / `decreases` clauses +//! - `#[verifier::*]` attributes //! //! See: +#![allow(unexpected_cfgs)] + use crate::rules::Reg; +// --------------------------------------------------------------------------- +// Verus specifications (machine-checked when running verus_test) +// +// When building with plain cargo (no Verus), the verus! macro is a no-op. +// When building with Verus, it enables verification. +// When using verus_strip, the entire block is removed. +// --------------------------------------------------------------------------- + +/// No-op verus! macro for plain Rust compilation. +/// Verus replaces this with its own macro; verus_strip removes the block entirely. +#[cfg(not(verus_keep_ghost))] +macro_rules! verus { + ($($t:tt)*) => {}; +} + +verus! { + +/// Spec: a register number is safe to allocate as a temporary. +pub open spec fn spec_is_allocatable(reg_num: u8) -> bool { + reg_num <= 12 + && reg_num != 9 // R9 = globals base + && reg_num != 10 // R10 = memory size + && reg_num != 11 // R11 = memory base +} + +/// Spec: a Thumb-16 instruction is exactly 2 bytes. +pub open spec fn spec_valid_thumb16(len: usize) -> bool { + len == 2 +} + +/// Spec: a Thumb-32 instruction is exactly 4 bytes. +pub open spec fn spec_valid_thumb32(len: usize) -> bool { + len == 4 +} + +/// Spec: a MOVW/MOVT immediate fits in 16 bits. +pub open spec fn spec_valid_imm16(imm: u32) -> bool { + imm <= 0xFFFF +} + +/// Spec: a register number is valid for Thumb-2 encoding. +pub open spec fn spec_valid_reg(rd: u32) -> bool { + rd <= 14 +} + +/// Spec: an access size is valid for WebAssembly memory operations. +pub open spec fn spec_valid_access_size(size: u32) -> bool { + size == 1 || size == 2 || size == 4 || size == 8 +} + +/// Spec: a bounds check correctly covers the full access range. +pub open spec fn spec_bounds_check_correct(addr: u32, access_size: u32, memory_size: u32) -> bool { + addr as int + access_size as int <= memory_size as int +} + +/// Spec: a division trap guard has the minimum instruction count. +pub open spec fn spec_valid_trap_guard(sequence_len: usize) -> bool { + sequence_len >= 4 +} + +} // verus! + +// --------------------------------------------------------------------------- +// Runtime contract checking (debug_assert! — works in plain Rust) +// --------------------------------------------------------------------------- + /// Register allocator invariants. /// /// The register allocator must never hand out registers reserved by the @@ -25,51 +97,22 @@ use crate::rules::Reg; /// - R9: globals base pointer /// - R10: linear memory size (for bounds checks) /// - R11: linear memory base pointer -/// -/// # Verus spec (future) -/// ```text -/// verus! { -/// spec fn is_allocatable(reg: u8) -> bool { -/// reg <= 12 && reg != 9 && reg != 10 && reg != 11 -/// } -/// } -/// ``` pub mod regalloc { use super::Reg; /// Reserved registers that must NEVER be allocated as temporaries. - /// - R9 = globals base pointer - /// - R10 = linear memory size - /// - R11 = linear memory base pointer pub const RESERVED_REGS: [Reg; 3] = [Reg::R9, Reg::R10, Reg::R11]; - /// Maximum register index that can be used as a general-purpose temporary. - /// R13 (SP), R14 (LR), R15 (PC) are architectural and must not be allocated. + /// Maximum register index for general-purpose temporaries. pub const MAX_GP_REG: u8 = 12; /// Check that a register is safe to allocate as a temporary. - /// - /// # Verus spec (future) - /// ```text - /// ensures |result: bool| - /// result <==> (reg_num <= 12 && reg_num != 9 && reg_num != 10 && reg_num != 11) - /// ``` #[inline] pub fn is_allocatable(reg: &Reg) -> bool { !RESERVED_REGS.contains(reg) && !matches!(reg, Reg::SP | Reg::LR | Reg::PC) } /// Assert that a register allocation satisfies the allocator postcondition. - /// - /// # Verus spec (future) - /// ```text - /// requires self.next_reg < ALLOCATABLE_REGS.len() - /// ensures - /// is_allocatable(result), - /// result != Reg::R9, - /// result != Reg::R10, - /// result != Reg::R11, - /// ``` #[inline] pub fn verify_allocation(reg: &Reg) { debug_assert!( @@ -80,13 +123,7 @@ pub mod regalloc { ); } - /// Assert that a register index is within the allocatable set before - /// conversion via `index_to_reg`. - /// - /// # Verus spec (future) - /// ```text - /// requires index < ALLOCATABLE_REGS.len() - /// ``` + /// Assert that a register index is within the allocatable set. #[inline] pub fn verify_index(index: u8, allocatable_len: usize) { debug_assert!( @@ -100,156 +137,76 @@ pub mod regalloc { } /// ARM instruction encoding invariants. -/// -/// These contracts ensure the encoder produces correctly-sized instruction -/// words and that operand fields are within their bit-width limits. -/// -/// # Verus spec (future) -/// ```text -/// verus! { -/// spec fn valid_thumb16(bytes: Seq) -> bool { -/// bytes.len() == 2 -/// } -/// spec fn valid_thumb32(bytes: Seq) -> bool { -/// bytes.len() == 4 -/// } -/// } -/// ``` pub mod encoding { - /// Verify that a Thumb-2 16-bit encoding produces exactly 2 bytes. - /// - /// # Verus spec (future) - /// ```text - /// ensures bytes.len() == 2 - /// ``` + /// Verify Thumb-2 16-bit encoding produces exactly 2 bytes. #[inline] pub fn verify_thumb16(bytes: &[u8]) { debug_assert_eq!( bytes.len(), 2, - "CONTRACT VIOLATION [encoding::thumb16]: Thumb-16 instruction must be exactly 2 \ - bytes, got {}", + "CONTRACT VIOLATION [encoding::thumb16]: must be 2 bytes, got {}", bytes.len() ); } - /// Verify that a Thumb-2 32-bit encoding produces exactly 4 bytes. - /// - /// # Verus spec (future) - /// ```text - /// ensures bytes.len() == 4 - /// ``` + /// Verify Thumb-2 32-bit encoding produces exactly 4 bytes. #[inline] pub fn verify_thumb32(bytes: &[u8]) { debug_assert_eq!( bytes.len(), 4, - "CONTRACT VIOLATION [encoding::thumb32]: Thumb-32 instruction must be exactly 4 \ - bytes, got {}", + "CONTRACT VIOLATION [encoding::thumb32]: must be 4 bytes, got {}", bytes.len() ); } - /// Verify that a MOVW/MOVT immediate fits in 16 bits. - /// - /// # Verus spec (future) - /// ```text - /// requires imm <= 0xFFFF - /// ``` + /// Verify MOVW/MOVT immediate fits in 16 bits. #[inline] pub fn verify_imm16(imm: u32) { debug_assert!( imm <= 0xFFFF, - "CONTRACT VIOLATION [encoding::movw_movt]: immediate value {:#x} exceeds 16-bit \ - range (max {:#x})", - imm, - 0xFFFFu32 + "CONTRACT VIOLATION [encoding::movw_movt]: immediate {:#x} exceeds 16-bit range", + imm ); } - /// Verify that a register number is valid for Thumb-2 encoding. - /// General-purpose registers are R0-R12 (0-12), plus SP(13), LR(14). - /// R15 (PC) is not valid as a destination in most encodings. - /// - /// # Verus spec (future) - /// ```text - /// requires rd <= 14 - /// ``` + /// Verify register number is valid for Thumb-2 (R0-R14). #[inline] pub fn verify_reg_bits(rd: u32) { debug_assert!( rd <= 14, - "CONTRACT VIOLATION [encoding::reg]: register number {} exceeds valid range (0-14)", + "CONTRACT VIOLATION [encoding::reg]: register {} exceeds valid range (0-14)", rd ); } - /// Verify that a register number is valid for Thumb-16 low register encoding. - /// Thumb-16 instructions can only encode R0-R7 (3-bit register field). - /// - /// # Verus spec (future) - /// ```text - /// requires reg <= 7 - /// ``` + /// Verify register number is valid for Thumb-16 low register (R0-R7). #[inline] pub fn verify_low_reg(reg: u32) { debug_assert!( reg <= 7, - "CONTRACT VIOLATION [encoding::low_reg]: register {} is not a low register (must be \ - 0-7 for Thumb-16)", + "CONTRACT VIOLATION [encoding::low_reg]: register {} must be 0-7 for Thumb-16", reg ); } } /// Memory access safety invariants. -/// -/// WebAssembly requires bounds-checked memory access. These contracts verify -/// that bounds checks correctly account for the access size, preventing -/// out-of-bounds reads/writes. -/// -/// # Verus spec (future) -/// ```text -/// verus! { -/// spec fn bounds_check_correct(addr: u32, access_size: u32, memory_size: u32) -> bool { -/// addr + access_size <= memory_size -/// } -/// } -/// ``` pub mod memory { /// Valid access sizes for WebAssembly memory operations. - /// - 1: i32.load8_s, i32.load8_u, i64.load8_s, i64.load8_u - /// - 2: i32.load16_s, i32.load16_u, i64.load16_s, i64.load16_u - /// - 4: i32.load, i32.store, f32.load, f32.store, i64.load32_s, i64.load32_u - /// - 8: i64.load, i64.store, f64.load, f64.store pub const VALID_ACCESS_SIZES: [u32; 4] = [1, 2, 4, 8]; - /// Verify that the access size is a valid WebAssembly memory access width. - /// - /// # Verus spec (future) - /// ```text - /// requires access_size in set![1u32, 2u32, 4u32, 8u32] - /// ``` + /// Verify access size is valid. #[inline] pub fn verify_access_size(access_size: u32) { debug_assert!( VALID_ACCESS_SIZES.contains(&access_size), - "CONTRACT VIOLATION [memory::access_size]: invalid access size {} (must be 1, 2, 4, \ - or 8)", + "CONTRACT VIOLATION [memory::access_size]: invalid size {} (must be 1, 2, 4, or 8)", access_size ); } - /// Verify that a bounds check correctly covers the full access range. - /// The check must compare `addr + access_size - 1` against `memory_size`, - /// not just `addr` alone. - /// - /// # Verus spec (future) - /// ```text - /// ensures - /// result ==> addr + access_size <= memory_size, - /// !result ==> addr + access_size > memory_size || overflow, - /// ``` + /// Verify bounds check covers the full access range. #[inline] pub fn verify_bounds_check(addr: u32, access_size: u32, memory_size: u32) -> bool { addr.checked_add(access_size) @@ -258,39 +215,13 @@ pub mod memory { } /// Division trap guard invariants. -/// -/// WebAssembly requires trapping on integer division by zero. ARM's SDIV/UDIV -/// instructions silently return 0 on division by zero, so the compiler must -/// emit an explicit check sequence before every division: -/// -/// ```text -/// CMP divisor, #0 ; test for zero divisor -/// BNE skip ; skip trap if non-zero -/// UDF #0 ; trigger UsageFault (WASM trap) -/// skip: -/// SDIV/UDIV rd, rn, rm ; safe to divide -/// ``` -/// -/// For signed division (I32DivS), an additional overflow check is needed: -/// `INT_MIN / -1` overflows in two's complement. pub mod division { - /// Verify that a division trap guard sequence has the correct structure. - /// The sequence must contain: CMP, BNE (conditional branch), UDF, then SDIV/UDIV. - /// - /// # Verus spec (future) - /// ```text - /// ensures - /// sequence[0] is Cmp { rn: divisor, op2: Imm(0) }, - /// sequence[1] is BCondOffset { cond: NE, .. }, - /// sequence[2] is Udf { .. }, - /// sequence[3] is Sdiv { .. } || sequence[3] is Udiv { .. }, - /// ``` + /// Verify division trap guard has minimum instruction count (CMP+BNE+UDF+xDIV). #[inline] pub fn verify_trap_guard_length(sequence_len: usize) { debug_assert!( sequence_len >= 4, - "CONTRACT VIOLATION [division::trap_guard]: division trap guard sequence must have \ - at least 4 instructions (CMP, BNE, UDF, xDIV), got {}", + "CONTRACT VIOLATION [division::trap_guard]: must have >= 4 instructions, got {}", sequence_len ); } @@ -302,7 +233,6 @@ mod tests { #[test] fn test_regalloc_allocatable() { - // R0-R8 and R12 should be allocatable assert!(regalloc::is_allocatable(&Reg::R0)); assert!(regalloc::is_allocatable(&Reg::R1)); assert!(regalloc::is_allocatable(&Reg::R4)); @@ -312,7 +242,6 @@ mod tests { #[test] fn test_regalloc_reserved() { - // R9, R10, R11 must NOT be allocatable assert!(!regalloc::is_allocatable(&Reg::R9)); assert!(!regalloc::is_allocatable(&Reg::R10)); assert!(!regalloc::is_allocatable(&Reg::R11)); @@ -320,7 +249,6 @@ mod tests { #[test] fn test_regalloc_architectural() { - // SP, LR, PC must NOT be allocatable assert!(!regalloc::is_allocatable(&Reg::SP)); assert!(!regalloc::is_allocatable(&Reg::LR)); assert!(!regalloc::is_allocatable(&Reg::PC)); @@ -328,7 +256,6 @@ mod tests { #[test] fn test_encoding_verify_imm16_valid() { - // Should not panic for valid values encoding::verify_imm16(0); encoding::verify_imm16(0xFFFF); encoding::verify_imm16(42); @@ -342,7 +269,6 @@ mod tests { #[test] fn test_memory_valid_access_sizes() { - // All valid sizes should pass memory::verify_access_size(1); memory::verify_access_size(2); memory::verify_access_size(4); @@ -357,19 +283,14 @@ mod tests { #[test] fn test_memory_bounds_check() { - // In bounds: addr=0, size=4, mem=65536 assert!(memory::verify_bounds_check(0, 4, 65536)); - // Exactly at boundary assert!(memory::verify_bounds_check(65532, 4, 65536)); - // Out of bounds assert!(!memory::verify_bounds_check(65533, 4, 65536)); - // Overflow protection assert!(!memory::verify_bounds_check(u32::MAX, 1, u32::MAX)); } #[test] fn test_division_trap_guard_length() { - // Valid: 4+ instructions division::verify_trap_guard_length(4); division::verify_trap_guard_length(5); }