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..87b5ef1 --- /dev/null +++ b/crates/synth-synthesis/src/contracts.rs @@ -0,0 +1,303 @@ +//! 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. +//! +//! # Dual-mode operation +//! +//! This file is written with Verus annotations inside `verus! {}` blocks. +//! Two compilation paths are supported: +//! +//! 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 +/// runtime calling convention: +/// - R9: globals base pointer +/// - R10: linear memory size (for bounds checks) +/// - R11: linear memory base pointer +pub mod regalloc { + use super::Reg; + + /// Reserved registers that must NEVER be allocated as temporaries. + pub const RESERVED_REGS: [Reg; 3] = [Reg::R9, Reg::R10, Reg::R11]; + + /// 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. + #[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. + #[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. + #[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. +pub mod encoding { + /// 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]: must be 2 bytes, got {}", + bytes.len() + ); + } + + /// 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]: must be 4 bytes, got {}", + bytes.len() + ); + } + + /// 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 {:#x} exceeds 16-bit range", + imm + ); + } + + /// 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 {} exceeds valid range (0-14)", + rd + ); + } + + /// 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 {} must be 0-7 for Thumb-16", + reg + ); + } +} + +/// Memory access safety invariants. +pub mod memory { + /// Valid access sizes for WebAssembly memory operations. + pub const VALID_ACCESS_SIZES: [u32; 4] = [1, 2, 4, 8]; + + /// 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 size {} (must be 1, 2, 4, or 8)", + access_size + ); + } + + /// 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) + .is_some_and(|end| end <= memory_size) + } +} + +/// Division trap guard invariants. +pub mod division { + /// 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]: must have >= 4 instructions, got {}", + sequence_len + ); + } +} + +#[cfg(test)] +mod tests { + use super::*; + + #[test] + fn test_regalloc_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() { + assert!(!regalloc::is_allocatable(&Reg::R9)); + assert!(!regalloc::is_allocatable(&Reg::R10)); + assert!(!regalloc::is_allocatable(&Reg::R11)); + } + + #[test] + fn test_regalloc_architectural() { + 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() { + 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() { + 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() { + assert!(memory::verify_bounds_check(0, 4, 65536)); + assert!(memory::verify_bounds_check(65532, 4, 65536)); + assert!(!memory::verify_bounds_check(65533, 4, 65536)); + assert!(!memory::verify_bounds_check(u32::MAX, 1, u32::MAX)); + } + + #[test] + fn test_division_trap_guard_length() { + 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;