Skip to content

Commit 582bdf6

Browse files
avrabeclaude
avrabe
and
claude
authored
feat: Verus-style contracts with runtime debug_assert! checking (#69)
* feat: Verus-style contracts with debug_assert! runtime checking 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) <noreply@anthropic.com> * 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) <noreply@anthropic.com> --------- Co-authored-by: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
1 parent 41d651b commit 582bdf6

5 files changed

Lines changed: 448 additions & 17 deletions

File tree

‎artifacts/verification-gaps.yaml‎

Lines changed: 15 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -12,9 +12,12 @@ artifacts:
1212
description: >
1313
The PulseEngine verification guide requires all projects to pass Verus
1414
verification with explicit requires/ensures specs on public functions.
15-
Synth has zero Verus annotations. The instruction selector, register
16-
allocator, and ARM encoder have no formal pre/postcondition specs.
17-
status: planned
15+
Verus-style contracts (requires/ensures doc comments + debug_assert!
16+
runtime checks) have been added to alloc_reg, index_to_reg,
17+
generate_load/store_with_bounds_check, division trap guard sequences,
18+
encode_thumb32_movw/movt, and SDIV/UDIV encoders. Full Verus macro
19+
integration pending rules_verus + verus_strip Bazel integration.
20+
status: in-progress
1821
tags: [verification-gap, verus]
1922
links:
2023
- type: derives-from
@@ -122,10 +125,15 @@ artifacts:
122125
title: "No explicit requires/ensures specs on public Rust functions"
123126
description: >
124127
The verification guide requires explicit specs (requires/ensures)
125-
on all public functions. Synth has zero Verus-style specifications.
126-
Critical functions lacking specs include: alloc_reg, select_default,
127-
select_with_stack, encode_thumb, encode_arm32, build_elf.
128-
status: planned
128+
on all public functions. Verus-style specification annotations
129+
(doc-comment contracts + debug_assert! runtime checks) have been
130+
added to critical functions: alloc_reg, index_to_reg,
131+
generate_load/store_with_bounds_check, division trap sequences,
132+
encode_thumb32_movw/movt, SDIV/UDIV encoders. Contracts module at
133+
synth-synthesis/src/contracts.rs defines formal invariants for
134+
regalloc, encoding, memory, and division subsystems. Remaining
135+
functions (select_with_stack, encode_thumb, build_elf) still need specs.
136+
status: in-progress
129137
tags: [verification-gap, verus, specs]
130138
links:
131139
- type: derives-from

‎crates/synth-backend/src/arm_encoder.rs‎

Lines changed: 47 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -4,6 +4,7 @@
44
55
use synth_core::Result;
66
use synth_core::target::FPUPrecision;
7+
use synth_synthesis::contracts::encoding as encoding_contracts;
78
use synth_synthesis::{ArmOp, MemAddr, MveSize, Operand2, QReg, Reg, VfpReg};
89

910
/// ARM instruction encoding
@@ -1538,7 +1539,9 @@ impl ArmEncoder {
15381539
// UDF (Undefined) in Thumb-2: 16-bit encoding is 0xDE00 | imm8
15391540
// This triggers UsageFault/HardFault, used for WASM traps
15401541
let instr: u16 = 0xDE00 | (*imm as u16);
1541-
Ok(instr.to_le_bytes().to_vec())
1542+
let bytes = instr.to_le_bytes().to_vec();
1543+
encoding_contracts::verify_thumb16(&bytes);
1544+
Ok(bytes)
15421545
}
15431546

15441547
// i64 support: ADDS, ADC, SUBS, SBC for register pair arithmetic
@@ -1631,6 +1634,9 @@ impl ArmEncoder {
16311634
let rd_bits = reg_to_bits(rd);
16321635
let rn_bits = reg_to_bits(rn);
16331636
let rm_bits = reg_to_bits(rm);
1637+
encoding_contracts::verify_reg_bits(rd_bits);
1638+
encoding_contracts::verify_reg_bits(rn_bits);
1639+
encoding_contracts::verify_reg_bits(rm_bits);
16341640

16351641
// Thumb-2 SDIV: FB90 F0F0 | Rn<<16 | Rd<<8 | Rm
16361642
// First halfword: 1111 1011 1001 Rn = 0xFB90 | Rn
@@ -1641,6 +1647,7 @@ impl ArmEncoder {
16411647
// Thumb-2 32-bit instructions: first halfword, then second halfword (little-endian each)
16421648
let mut bytes = hw1.to_le_bytes().to_vec();
16431649
bytes.extend_from_slice(&hw2.to_le_bytes());
1650+
encoding_contracts::verify_thumb32(&bytes);
16441651
Ok(bytes)
16451652
}
16461653

@@ -1649,13 +1656,17 @@ impl ArmEncoder {
16491656
let rd_bits = reg_to_bits(rd);
16501657
let rn_bits = reg_to_bits(rn);
16511658
let rm_bits = reg_to_bits(rm);
1659+
encoding_contracts::verify_reg_bits(rd_bits);
1660+
encoding_contracts::verify_reg_bits(rn_bits);
1661+
encoding_contracts::verify_reg_bits(rm_bits);
16521662

16531663
// Thumb-2 UDIV: FBB0 F0F0 | Rn<<16 | Rd<<8 | Rm
16541664
let hw1: u16 = (0xFBB0 | rn_bits) as u16;
16551665
let hw2: u16 = (0xF0F0 | (rd_bits << 8) | rm_bits) as u16;
16561666

16571667
let mut bytes = hw1.to_le_bytes().to_vec();
16581668
bytes.extend_from_slice(&hw2.to_le_bytes());
1669+
encoding_contracts::verify_thumb32(&bytes);
16591670
Ok(bytes)
16601671
}
16611672

@@ -5832,8 +5843,16 @@ impl ArmEncoder {
58325843
}
58335844

58345845
/// Encode Thumb-2 32-bit MOVW (16-bit immediate)
5846+
///
5847+
/// # Contract (Verus-style)
5848+
/// ```text
5849+
/// requires rd <= R14
5850+
/// ensures result.len() == 4
5851+
/// ensures (imm & 0xFFFF) can be reconstructed from the encoding
5852+
/// ```
58355853
fn encode_thumb32_movw(&self, rd: &Reg, imm: u32) -> Result<Vec<u8>> {
58365854
let rd_bits = reg_to_bits(rd);
5855+
encoding_contracts::verify_reg_bits(rd_bits);
58375856
let imm16 = imm & 0xFFFF;
58385857

58395858
// MOVW Rd, #imm16
@@ -5848,10 +5867,17 @@ impl ArmEncoder {
58485867

58495868
let mut bytes = hw1.to_le_bytes().to_vec();
58505869
bytes.extend_from_slice(&hw2.to_le_bytes());
5870+
encoding_contracts::verify_thumb32(&bytes);
58515871
Ok(bytes)
58525872
}
58535873

58545874
/// Encode Thumb-2 32-bit shift with immediate
5875+
///
5876+
/// # Contract (Verus-style)
5877+
/// ```text
5878+
/// requires rd <= R14, rm <= R14
5879+
/// ensures result.len() == 4
5880+
/// ```
58555881
fn encode_thumb32_shift(
58565882
&self,
58575883
rd: &Reg,
@@ -5861,6 +5887,8 @@ impl ArmEncoder {
58615887
) -> Result<Vec<u8>> {
58625888
let rd_bits = reg_to_bits(rd);
58635889
let rm_bits = reg_to_bits(rm);
5890+
encoding_contracts::verify_reg_bits(rd_bits);
5891+
encoding_contracts::verify_reg_bits(rm_bits);
58645892
let imm5 = shift & 0x1F;
58655893
let imm2 = imm5 & 0x3;
58665894
let imm3 = (imm5 >> 2) & 0x7;
@@ -6165,7 +6193,15 @@ impl ArmEncoder {
61656193
// === Raw encoding helpers for POPCNT (take register numbers directly) ===
61666194

61676195
/// Encode Thumb-2 32-bit MOVW (16-bit immediate) - raw version
6196+
///
6197+
/// # Contract (Verus-style)
6198+
/// ```text
6199+
/// requires rd <= 14, imm16 <= 0xFFFF
6200+
/// ensures result.len() == 4
6201+
/// ```
61686202
fn encode_thumb32_movw_raw(&self, rd: u32, imm16: u32) -> Result<Vec<u8>> {
6203+
encoding_contracts::verify_reg_bits(rd);
6204+
encoding_contracts::verify_imm16(imm16);
61696205
// MOVW Rd, #imm16
61706206
// 1111 0 i 10 0 1 0 0 imm4 | 0 imm3 Rd imm8
61716207
let imm16 = imm16 & 0xFFFF;
@@ -6179,11 +6215,20 @@ impl ArmEncoder {
61796215

61806216
let mut bytes = hw1.to_le_bytes().to_vec();
61816217
bytes.extend_from_slice(&hw2.to_le_bytes());
6218+
encoding_contracts::verify_thumb32(&bytes);
61826219
Ok(bytes)
61836220
}
61846221

61856222
/// Encode Thumb-2 32-bit MOVT (move top 16 bits) - raw version
6223+
///
6224+
/// # Contract (Verus-style)
6225+
/// ```text
6226+
/// requires rd <= 14, imm16 <= 0xFFFF
6227+
/// ensures result.len() == 4
6228+
/// ```
61866229
fn encode_thumb32_movt_raw(&self, rd: u32, imm16: u32) -> Result<Vec<u8>> {
6230+
encoding_contracts::verify_reg_bits(rd);
6231+
encoding_contracts::verify_imm16(imm16);
61876232
// MOVT Rd, #imm16
61886233
// 1111 0 i 10 1 1 0 0 imm4 | 0 imm3 Rd imm8
61896234
let imm16 = imm16 & 0xFFFF;
@@ -6197,6 +6242,7 @@ impl ArmEncoder {
61976242

61986243
let mut bytes = hw1.to_le_bytes().to_vec();
61996244
bytes.extend_from_slice(&hw2.to_le_bytes());
6245+
encoding_contracts::verify_thumb32(&bytes);
62006246
Ok(bytes)
62016247
}
62026248

0 commit comments

Comments
 (0)