Skip to content

feat: rules_verus Bazel integration + verify_contracts target #70

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
avrabe merged 3 commits into from
Mar 28, 2026
+480 −17
Merged

feat: rules_verus Bazel integration + verify_contracts target #70

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
8f4d7dd
feat: Verus-style contracts with debug_assert! runtime checking
avrabe Mar 28, 2026
4bb9906
feat: convert contracts to actual verus! {} blocks with no-op fallback
avrabe Mar 28, 2026
ee8002b
feat: add rules_verus to Bazel + verify_contracts target
avrabe Mar 28, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
13 changes: 13 additions & 0 deletions MODULE.bazel
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -75,6 +75,19 @@ crate.spec(package = "object", version = "0.36", default_features = False, featu
crate.from_specs()
use_repo(crate, "crates")

# Verus formal verification (SMT/Z3 track)
# Provides verus_library, verus_test, verus_strip, verus_strip_test
bazel_dep(name = "rules_verus", version = "0.0.0")
git_override(
module_name = "rules_verus",
remote = "https://github.com/pulseengine/rules_verus.git",
commit = "a49f72ef", # fix: bundle Rust nightly sysroot with Verus toolchain
)

verus = use_extension("@rules_verus//verus:extensions.bzl", "verus")
use_repo(verus, "verus_toolchains")
register_toolchains("@verus_toolchains//:all")

# PulseEngine WebAssembly Component Model rules
bazel_dep(name = "rules_wasm_component", version = "1.0.0")
git_override(
Expand Down
22 changes: 15 additions & 7 deletions artifacts/verification-gaps.yaml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down
19 changes: 19 additions & 0 deletions crates/BUILD.bazel
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -281,3 +281,22 @@ filegroup(
":synth-memory",
],
)

# =============================================================================
# Verus formal verification targets
# =============================================================================

load("@rules_verus//verus:defs.bzl", "verus_test", "verus_strip")

# Verify contracts with Verus (SMT/Z3 track)
verus_test(
name = "verify_contracts",
srcs = ["synth-synthesis/src/contracts.rs"],
tags = ["verus", "verification"],
)

# Strip Verus annotations for plain Rust consumption
verus_strip(
name = "contracts_plain",
srcs = ["synth-synthesis/src/contracts.rs"],
)
48 changes: 47 additions & 1 deletion crates/synth-backend/src/arm_encoder.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand All @@ -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)
}

Expand All @@ -1649,13 +1656,17 @@ 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;
let hw2: u16 = (0xF0F0 | (rd_bits << 8) | rm_bits) as u16;

let mut bytes = hw1.to_le_bytes().to_vec();
bytes.extend_from_slice(&hw2.to_le_bytes());
encoding_contracts::verify_thumb32(&bytes);
Ok(bytes)
}

Expand Down Expand Up @@ -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<Vec<u8>> {
let rd_bits = reg_to_bits(rd);
encoding_contracts::verify_reg_bits(rd_bits);
let imm16 = imm & 0xFFFF;

// MOVW Rd, #imm16
Expand All @@ -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,
Expand All @@ -5861,6 +5887,8 @@ impl ArmEncoder {
) -> Result<Vec<u8>> {
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;
Expand Down Expand Up @@ -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<Vec<u8>> {
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;
Expand All @@ -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<Vec<u8>> {
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;
Expand All @@ -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)
}

Expand Down
Loading
Loading