From 580a99248949723595e009ce984d1e4d61df8edc Mon Sep 17 00:00:00 2001 From: Securify001 Date: Sun, 28 Jun 2026 14:29:02 +0100 Subject: [PATCH] feat: rule engine and smt --- .github/workflows/rust.yml | 83 ++ DOCUMENTATION_INDEX.md | 33 + tooling/sanctifier-core/src/smt.rs | 787 ------------------ tooling/sanctifier-core/src/smt/backend.rs | 330 ++++++++ tooling/sanctifier-core/src/smt/benchmark.rs | 153 ++++ tooling/sanctifier-core/src/smt/invariants.rs | 251 ++++++ tooling/sanctifier-core/src/smt/mod.rs | 45 + tooling/sanctifier-core/src/smt/types.rs | 191 +++++ .../tests/rule_engine_orchestration_test.rs | 492 +++++++++++ .../tests/smt_module_boundaries_test.rs | 348 ++++++++ 10 files changed, 1926 insertions(+), 787 deletions(-) delete mode 100644 tooling/sanctifier-core/src/smt.rs create mode 100644 tooling/sanctifier-core/src/smt/backend.rs create mode 100644 tooling/sanctifier-core/src/smt/benchmark.rs create mode 100644 tooling/sanctifier-core/src/smt/invariants.rs create mode 100644 tooling/sanctifier-core/src/smt/mod.rs create mode 100644 tooling/sanctifier-core/src/smt/types.rs create mode 100644 tooling/sanctifier-core/tests/rule_engine_orchestration_test.rs create mode 100644 tooling/sanctifier-core/tests/smt_module_boundaries_test.rs diff --git a/.github/workflows/rust.yml b/.github/workflows/rust.yml index 312ee92f..53583406 100644 --- a/.github/workflows/rust.yml +++ b/.github/workflows/rust.yml @@ -24,6 +24,11 @@ jobs: with: components: rustfmt, clippy + - name: Install Z3 + run: | + sudo apt-get update + sudo apt-get install -y libz3-dev libdbus-1-dev libudev-dev pkg-config + - name: Cache cargo registry & build artifacts uses: actions/cache@v5 with: @@ -71,6 +76,11 @@ jobs: - name: Install stable Rust toolchain uses: dtolnay/rust-toolchain@stable + - name: Install Z3 + run: | + sudo apt-get update + sudo apt-get install -y libz3-dev libdbus-1-dev libudev-dev pkg-config + - name: Cache cargo registry & build artifacts uses: actions/cache@v5 with: @@ -122,6 +132,11 @@ jobs: - name: Install stable Rust toolchain uses: dtolnay/rust-toolchain@stable + - name: Install Z3 + run: | + sudo apt-get update + sudo apt-get install -y libz3-dev libdbus-1-dev libudev-dev pkg-config + - name: Cache cargo registry & build artifacts uses: actions/cache@v5 with: @@ -149,3 +164,71 @@ jobs: echo "::error::Uncommitted snapshot changes detected. Run INSTA_UPDATE=new cargo test --test sarif_snapshots -p sanctifier-core --no-default-features then cargo insta accept --workspace and commit the .snap files." exit 1 fi + + # --------------------------------------------------------------------------- + # Rule engine orchestration — integration/e2e coverage + # Covers: RuleRegistry pipeline, determinism, custom rules, output stability. + # --------------------------------------------------------------------------- + rule-engine-e2e: + name: Rule Engine Orchestration (integration/e2e) + runs-on: ubuntu-latest + + steps: + - name: Checkout repository + uses: actions/checkout@v6 + + - name: Install stable Rust toolchain + uses: dtolnay/rust-toolchain@stable + + - name: Install Z3 + run: | + sudo apt-get update + sudo apt-get install -y libz3-dev libdbus-1-dev libudev-dev pkg-config + + - name: Cache cargo registry & build artifacts + uses: actions/cache@v5 + with: + path: | + ~/.cargo/registry + ~/.cargo/git + target + key: ${{ runner.os }}-cargo-rule-e2e-${{ hashFiles('**/Cargo.lock') }} + restore-keys: | + ${{ runner.os }}-cargo-rule-e2e- + + - name: Run rule engine orchestration integration tests + run: cargo test --test rule_engine_orchestration_test -p sanctifier-core + + # --------------------------------------------------------------------------- + # Z3 backend module boundaries — integration coverage for S011 + # Covers: smt::types, smt::invariants, smt::backend, smt::benchmark. + # --------------------------------------------------------------------------- + smt-module-boundaries: + name: Z3 Backend Module Boundaries (S011) + runs-on: ubuntu-latest + + steps: + - name: Checkout repository + uses: actions/checkout@v6 + + - name: Install stable Rust toolchain + uses: dtolnay/rust-toolchain@stable + + - name: Install Z3 + run: | + sudo apt-get update + sudo apt-get install -y libz3-dev libdbus-1-dev libudev-dev pkg-config + + - name: Cache cargo registry & build artifacts + uses: actions/cache@v5 + with: + path: | + ~/.cargo/registry + ~/.cargo/git + target + key: ${{ runner.os }}-cargo-smt-boundaries-${{ hashFiles('**/Cargo.lock') }} + restore-keys: | + ${{ runner.os }}-cargo-smt-boundaries- + + - name: Run Z3 module boundary integration tests + run: cargo test --test smt_module_boundaries_test -p sanctifier-core diff --git a/DOCUMENTATION_INDEX.md b/DOCUMENTATION_INDEX.md index 645b40f0..1a50d758 100644 --- a/DOCUMENTATION_INDEX.md +++ b/DOCUMENTATION_INDEX.md @@ -183,6 +183,7 @@ - Comprehensive remediation guidance with checked/saturating alternatives - Deduplication strategy and output formats - Known limitations and configuration options + **[docs/rules/s001-auth-gap.md](docs/rules/s001-auth-gap.md)** - S001: Missing Authorization Guard (`auth_gap`) - What constitutes a privileged operation (storage mutation, external call) @@ -199,6 +200,38 @@ - Examples and remediation guidance - Reference implementations and test coverage +### Rule Engine Orchestration — Integration/E2E Coverage + +**[specs/rule-engine-behavior.md](specs/rule-engine-behavior.md)** + +- Formal specification: discovery order, filtering, deduplication, exit codes +- Integration/e2e test suite: [`tooling/sanctifier-core/tests/rule_engine_orchestration_test.rs`](tooling/sanctifier-core/tests/rule_engine_orchestration_test.rs) + - Registry population and deduplication + - Per-rule firing and `run_all` consistency + - Determinism across repeated calls + - Custom regex rule execution + - Registry extensibility without breaking existing rules + - End-to-end multi-file scan pipeline + - Output format (`RuleViolation`) JSON stability +- CI job: `rule-engine-e2e` in [`.github/workflows/rust.yml`](.github/workflows/rust.yml) + +### Z3 Backend Invariants (S011) — Module Boundaries + +**Finding code:** `S011` — see [`docs/error-codes.md`](docs/error-codes.md) + +**Module layout** (`tooling/sanctifier-core/src/smt/`): + +| Sub-module | File | Responsibility | +|---|---|---| +| `types` | [`src/smt/types.rs`](tooling/sanctifier-core/src/smt/types.rs) | All shared data types and error enums | +| `invariants` | [`src/smt/invariants.rs`](tooling/sanctifier-core/src/smt/invariants.rs) | `#[invariant]` AST parsing + Z3 verification | +| `backend` | [`src/smt/backend.rs`](tooling/sanctifier-core/src/smt/backend.rs) | `SmtVerifier`, fixed-point proof dispatch | +| `benchmark` | [`src/smt/benchmark.rs`](tooling/sanctifier-core/src/smt/benchmark.rs) | Latency micro-benchmark for CI artifact | +| `mod` | [`src/smt/mod.rs`](tooling/sanctifier-core/src/smt/mod.rs) | Public re-export facade (zero breaking surface) | + +- Integration/boundary test suite: [`tooling/sanctifier-core/tests/smt_module_boundaries_test.rs`](tooling/sanctifier-core/tests/smt_module_boundaries_test.rs) +- CI job: `smt-module-boundaries` in [`.github/workflows/rust.yml`](.github/workflows/rust.yml) + ### WASM Module Versioning & Input Validation **[docs/wasm-versioning-alignment.md](docs/wasm-versioning-alignment.md)** - WASM module hardening diff --git a/tooling/sanctifier-core/src/smt.rs b/tooling/sanctifier-core/src/smt.rs deleted file mode 100644 index 2b951a46..00000000 --- a/tooling/sanctifier-core/src/smt.rs +++ /dev/null @@ -1,787 +0,0 @@ -//! Z3-based formal-verification primitives. - -use serde::{Deserialize, Serialize}; -use std::time::Instant; -use thiserror::Error; -use z3::ast::{Bool, Int}; -use z3::{Context, SatResult, Solver}; - -/// An invariant issue proved by the Z3 SMT solver. -#[derive(Debug, Serialize, Deserialize, Clone)] -pub struct SmtInvariantIssue { - /// Function under verification. - pub function_name: String, - /// Human-readable description of the violation. - pub description: String, - /// Source location. - pub location: String, -} - -// ── Production SMT hardening ────────────────────────────────────────────────── - -/// Configuration for the SMT-based invariant verifier. -#[derive(Debug, Clone, Serialize, Deserialize)] -pub struct SmtConfig { - /// Solver timeout per call in milliseconds (default 10 000 ms = 10 s). - pub timeout_ms: u64, -} - -impl Default for SmtConfig { - fn default() -> Self { - Self { timeout_ms: 10_000 } - } -} - -/// Structured finding returned by the SMT invariant verifier. -#[derive(Debug, Serialize, Deserialize, Clone)] -pub struct SmtFinding { - /// Name / expression of the invariant that was checked. - pub invariant_name: String, - /// Source location (enclosing function name or file:line). - pub location: String, - /// Concrete counterexample values returned by Z3, when available. - pub counterexample: Option, - /// `true` when the solver timed out instead of producing sat/unsat. - pub is_timeout: bool, -} - -/// A `#[invariant = "..."]` annotation extracted from Rust source via AST -/// analysis (not regex). -#[derive(Debug, Clone, PartialEq, Eq)] -pub struct InvariantSpec { - /// The raw invariant expression (e.g. `"balance >= 0"`). - pub expression: String, - /// Enclosing function name used as the location hint. - pub location: String, -} - -/// Parse every `#[invariant = "..."]` attribute in the source file using the -/// syn AST. Returns an empty vec on parse errors (no panic). -pub fn parse_invariants(source: &str) -> Vec { - use syn::{parse_str, Expr, File, Item, Lit, Meta}; - - let file = match parse_str::(source) { - Ok(f) => f, - Err(_) => return vec![], - }; - - let mut specs = Vec::new(); - - for item in &file.items { - if let Item::Impl(impl_block) = item { - for impl_item in &impl_block.items { - if let syn::ImplItem::Fn(f) = impl_item { - let fn_name = f.sig.ident.to_string(); - for attr in &f.attrs { - if attr.path().is_ident("invariant") { - if let Meta::NameValue(nv) = &attr.meta { - if let Expr::Lit(expr_lit) = &nv.value { - if let Lit::Str(lit_str) = &expr_lit.lit { - specs.push(InvariantSpec { - expression: lit_str.value(), - location: fn_name.clone(), - }); - } - } - } - } - } - } - } - } - } - - specs -} - -/// Verify `#[invariant = "..."]` annotations with Z3 under a configurable -/// timeout. -/// -/// Returns one [`SmtFinding`] for every invariant that could not be proved -/// safe, or for which the solver timed out. Safe invariants produce no -/// finding. -pub fn verify_invariants(source: &str, config: &SmtConfig) -> Vec { - let specs = parse_invariants(source); - if specs.is_empty() { - return vec![]; - } - - let mut findings = Vec::new(); - for spec in &specs { - if let Some(finding) = check_invariant_spec(spec, config) { - findings.push(finding); - } - } - findings -} - -/// Check one [`InvariantSpec`] with Z3. -/// -/// * Expressions that mention addition (`+` / `add`) are verified against -/// u64 overflow. -/// * Expressions that mention subtraction (`-` / `sub`) are verified against -/// u64 underflow. -/// * All other expressions are skipped (no finding — they require manual -/// modelling). -fn check_invariant_spec(spec: &InvariantSpec, config: &SmtConfig) -> Option { - use z3::Config; - - let expr_lower = spec.expression.to_lowercase(); - - let overflow_check = expr_lower.contains('+') || expr_lower.contains("add"); - let underflow_check = expr_lower.contains('-') || expr_lower.contains("sub"); - - if !overflow_check && !underflow_check { - return None; - } - - let mut cfg = Config::new(); - // Pass the timeout as milliseconds; Z3 returns Unknown when it expires. - cfg.set_param_value("timeout", &config.timeout_ms.to_string()); - let ctx = Context::new(&cfg); - let solver = Solver::new(&ctx); - - let a = Int::new_const(&ctx, "a"); - let b = Int::new_const(&ctx, "b"); - let zero = Int::from_u64(&ctx, 0); - let max_u64 = Int::from_u64(&ctx, u64::MAX); - - solver.assert(&a.ge(&zero)); - solver.assert(&a.le(&max_u64)); - solver.assert(&b.ge(&zero)); - solver.assert(&b.le(&max_u64)); - - let violation = if overflow_check { - // Assert a + b > u64::MAX (overflow possible) - let sum = Int::add(&ctx, &[&a, &b]); - sum.gt(&max_u64) - } else { - // Assert a - b < 0 (underflow possible) - let diff = Int::sub(&ctx, &[&a, &b]); - diff.lt(&zero) - }; - - solver.assert(&violation); - - match solver.check() { - SatResult::Sat => { - let counterexample = solver.get_model().map(|m| { - let a_val = m - .eval(&a, true) - .map(|v| v.to_string()) - .unwrap_or_else(|| "?".to_string()); - let b_val = m - .eval(&b, true) - .map(|v| v.to_string()) - .unwrap_or_else(|| "?".to_string()); - if overflow_check { - format!("a={a_val}, b={b_val} — a+b overflows u64") - } else { - format!("a={a_val}, b={b_val} — a-b underflows u64") - } - }); - Some(SmtFinding { - invariant_name: spec.expression.clone(), - location: spec.location.clone(), - counterexample, - is_timeout: false, - }) - } - SatResult::Unsat => None, - SatResult::Unknown => Some(SmtFinding { - invariant_name: spec.expression.clone(), - location: spec.location.clone(), - counterexample: None, - is_timeout: true, - }), - } -} - -/// Supported SMT backends for fixed-point proofs. -#[derive(Debug, Serialize, Deserialize, Clone, Copy, PartialEq, Eq)] -#[serde(rename_all = "snake_case")] -#[non_exhaustive] -pub enum SmtBackend { - /// Z3 backend. - Z3, - /// Placeholder for future CVC5 support. - Cvc5, -} - -/// Input bounds for a standard fixed-point `a * b / d` proof. -#[derive(Debug, Serialize, Deserialize, Clone)] -pub struct FixedPointMulDivSpec { - /// Human-readable function or calculation name. - pub function_name: String, - /// Maximum value of the left multiplicand. - pub multiplicand_max: u128, - /// Maximum value of the right multiplicand. - pub multiplier_max: u128, - /// Minimum divisor value (must be > 0). - pub divisor_min: u128, - /// Maximum divisor value. - pub divisor_max: u128, - /// Optional bound for the final quotient. - #[serde(skip_serializing_if = "Option::is_none")] - pub result_max: Option, -} - -/// Concrete witness returned when a fixed-point proof fails. -#[derive(Debug, Serialize, Deserialize, Clone)] -pub struct FixedPointCounterexample { - /// Value chosen for the left multiplicand. - pub multiplicand: String, - /// Value chosen for the right multiplicand. - pub multiplier: String, - /// Value chosen for the divisor. - pub divisor: String, - /// Intermediate `a * b` result. - pub intermediate_product: String, - /// Final `(a * b) / d` quotient. - pub quotient: String, -} - -/// Result of a fixed-point overflow proof. -#[derive(Debug, Serialize, Deserialize, Clone)] -pub struct FixedPointProofReport { - /// Human-readable function or calculation name. - pub function_name: String, - /// Backend used for the proof. - pub backend: SmtBackend, - /// Whether the proof established safety for all inputs in range. - pub proven_safe: bool, - /// Properties checked during the proof. - pub checked_properties: Vec, - /// Summary message. - pub message: String, - /// Concrete witness if the proof failed. - #[serde(skip_serializing_if = "Option::is_none")] - pub counterexample: Option, -} - -/// Errors raised when preparing or executing a fixed-point proof. -#[derive(Debug, Error, Clone, PartialEq, Eq)] -pub enum FixedPointProofError { - /// Invalid input bounds. - #[error("invalid fixed-point proof specification: {0}")] - InvalidSpec(&'static str), - /// The requested backend is not implemented yet. - #[error("unsupported SMT backend: {0:?}")] - UnsupportedBackend(SmtBackend), - /// The backend did not produce a usable answer. - #[error("solver did not produce a usable result: {0}")] - SolverFailure(&'static str), -} - -/// Z3-backed SMT solver wrapper. -pub struct SmtVerifier<'ctx> { - ctx: &'ctx Context, -} - -impl<'ctx> SmtVerifier<'ctx> { - /// Create a verifier bound to a Z3 [`Context`]. - pub fn new(ctx: &'ctx Context) -> Self { - Self { ctx } - } - - /// Proof-of-Concept: Uses Z3 to prove if `a + b` can overflow a 64-bit integer - /// under unconstrained conditions. - pub fn verify_addition_overflow( - &self, - fn_name: &str, - location: &str, - ) -> Option { - let solver = Solver::new(self.ctx); - let a = Int::new_const(self.ctx, "a"); - let b = Int::new_const(self.ctx, "b"); - - // u64 bounds - let zero = Int::from_u64(self.ctx, 0); - let max_u64 = Int::from_u64(self.ctx, u64::MAX); - - // Constrain variables to valid u64 limits: 0 <= a, b <= u64::MAX - solver.assert(&a.ge(&zero)); - solver.assert(&a.le(&max_u64)); - solver.assert(&b.ge(&zero)); - solver.assert(&b.le(&max_u64)); - - // To prove overflow is IMPOSSIBLE, we assert the violation (a + b > max_u64) - // and check if the solver can SATISFY this violation. - let sum = Int::add(self.ctx, &[&a, &b]); - solver.assert(&sum.gt(&max_u64)); - - if solver.check() == SatResult::Sat { - // A model exists where a + b > u64::MAX, meaning an overflow is mathematically possible - Some(SmtInvariantIssue { - function_name: fn_name.to_string(), - description: "SMT Solver (Z3) proved that this addition can overflow u64 bounds." - .to_string(), - location: location.to_string(), - }) - } else { - None - } - } -} - -/// Prove that `a * b / d` cannot overflow `u128` within the provided bounds -/// using the default backend (Z3). -pub fn prove_fixed_point_mul_div_bounds( - spec: &FixedPointMulDivSpec, -) -> Result { - prove_fixed_point_mul_div_bounds_with_backend(SmtBackend::Z3, spec) -} - -/// Prove that `a * b / d` cannot overflow `u128` within the provided bounds -/// using the selected SMT backend. -pub fn prove_fixed_point_mul_div_bounds_with_backend( - backend: SmtBackend, - spec: &FixedPointMulDivSpec, -) -> Result { - validate_fixed_point_spec(spec)?; - - match backend { - SmtBackend::Z3 => prove_fixed_point_mul_div_bounds_z3(spec), - SmtBackend::Cvc5 => Err(FixedPointProofError::UnsupportedBackend(SmtBackend::Cvc5)), - } -} - -/// The constraint-generation strategy used for an SMT proof. -#[derive(Debug, Serialize, Deserialize, Clone, Copy, PartialEq, Eq)] -#[serde(rename_all = "snake_case")] -#[non_exhaustive] -pub enum SmtProofStrategy { - /// Full u64 range. - UnconstrainedOverflow, - /// Bounded to ~5 × 10⁹. - BoundedDomainOverflow, - /// Bounded to 10 000. - SmallDomainOverflow, -} - -/// Latency statistics for a single [`SmtProofStrategy`]. -#[derive(Debug, Serialize, Deserialize, Clone)] -pub struct SmtStrategyLatency { - /// Which strategy was measured. - pub strategy: SmtProofStrategy, - /// Number of iterations. - pub runs: usize, - /// Fastest run in microseconds. - pub min_micros: u128, - /// Slowest run in microseconds. - pub max_micros: u128, - /// Mean duration in microseconds. - pub avg_micros: u128, - /// 95th-percentile duration in microseconds. - pub p95_micros: u128, -} - -/// Aggregate benchmark across all [`SmtProofStrategy`] variants. -#[derive(Debug, Serialize, Deserialize, Clone)] -pub struct SmtLatencyBenchmarkReport { - /// Timestamp of the benchmark run. - pub timestamp: String, - /// How many iterations were run per strategy. - pub iterations_per_strategy: usize, - /// Per-strategy results. - pub strategies: Vec, -} - -impl SmtLatencyBenchmarkReport { - /// Return strategies ordered by descending average latency. - pub fn most_expensive_first(&self) -> Vec { - let mut sorted = self.strategies.clone(); - sorted.sort_by_key(|k| std::cmp::Reverse(k.avg_micros)); - sorted - } -} - -/// Run a latency micro-benchmark for each [`SmtProofStrategy`]. -pub fn run_smt_latency_benchmark(iterations_per_strategy: usize) -> SmtLatencyBenchmarkReport { - use z3::{Config, Context}; - - let iterations = iterations_per_strategy.max(1); - let strategies = [ - SmtProofStrategy::UnconstrainedOverflow, - SmtProofStrategy::BoundedDomainOverflow, - SmtProofStrategy::SmallDomainOverflow, - ]; - - let mut results = Vec::with_capacity(strategies.len()); - - for strategy in strategies { - let mut samples = Vec::with_capacity(iterations); - for _ in 0..iterations { - let cfg = Config::new(); - let ctx = Context::new(&cfg); - - let start = Instant::now(); - let _ = run_strategy(&ctx, strategy); - samples.push(start.elapsed().as_micros()); - } - - samples.sort_unstable(); - let min_micros = samples.first().copied().unwrap_or_default(); - let max_micros = samples.last().copied().unwrap_or_default(); - let total: u128 = samples.iter().sum(); - let avg_micros = total / samples.len() as u128; - let p95_index = (((samples.len() - 1) as f64) * 0.95).round() as usize; - let p95_micros = samples[p95_index]; - - results.push(SmtStrategyLatency { - strategy, - runs: iterations, - min_micros, - max_micros, - avg_micros, - p95_micros, - }); - } - - SmtLatencyBenchmarkReport { - timestamp: chrono::Utc::now().to_rfc3339(), - iterations_per_strategy: iterations, - strategies: results, - } -} - -fn validate_fixed_point_spec(spec: &FixedPointMulDivSpec) -> Result<(), FixedPointProofError> { - if spec.divisor_min == 0 { - return Err(FixedPointProofError::InvalidSpec( - "divisor_min must be greater than zero", - )); - } - - if spec.divisor_max < spec.divisor_min { - return Err(FixedPointProofError::InvalidSpec( - "divisor_max must be greater than or equal to divisor_min", - )); - } - - Ok(()) -} - -fn prove_fixed_point_mul_div_bounds_z3( - spec: &FixedPointMulDivSpec, -) -> Result { - use z3::Config; - - let cfg = Config::new(); - let ctx = Context::new(&cfg); - let solver = Solver::new(&ctx); - - let multiplicand = Int::new_const(&ctx, "multiplicand"); - let multiplier = Int::new_const(&ctx, "multiplier"); - let divisor = Int::new_const(&ctx, "divisor"); - - let zero = int_from_u128(&ctx, 0); - let max_u128 = int_from_u128(&ctx, u128::MAX); - let multiplicand_max = int_from_u128(&ctx, spec.multiplicand_max); - let multiplier_max = int_from_u128(&ctx, spec.multiplier_max); - let divisor_min = int_from_u128(&ctx, spec.divisor_min); - let divisor_max = int_from_u128(&ctx, spec.divisor_max); - - solver.assert(&multiplicand.ge(&zero)); - solver.assert(&multiplicand.le(&multiplicand_max)); - solver.assert(&multiplier.ge(&zero)); - solver.assert(&multiplier.le(&multiplier_max)); - solver.assert(&divisor.ge(&divisor_min)); - solver.assert(&divisor.le(&divisor_max)); - - let product = Int::mul(&ctx, &[&multiplicand, &multiplier]); - let quotient = product.div(&divisor); - let product_overflow = product.gt(&max_u128); - - let mut checked_properties = vec!["intermediate multiplication fits in u128".to_string()]; - - let violation = if let Some(result_max) = spec.result_max { - checked_properties.push(format!("final quotient <= {}", result_max)); - let quotient_overflow = quotient.gt(&int_from_u128(&ctx, result_max)); - Bool::or(&ctx, &[&product_overflow, "ient_overflow]) - } else { - product_overflow - }; - - solver.assert(&violation); - - match solver.check() { - SatResult::Unsat => Ok(FixedPointProofReport { - function_name: spec.function_name.clone(), - backend: SmtBackend::Z3, - proven_safe: true, - checked_properties, - message: "Z3 proved the fixed-point calculation stays within the configured bounds." - .to_string(), - counterexample: None, - }), - SatResult::Sat => { - let model = solver - .get_model() - .ok_or(FixedPointProofError::SolverFailure( - "missing model for SAT result", - ))?; - - let multiplicand_value = - model - .eval(&multiplicand, true) - .ok_or(FixedPointProofError::SolverFailure( - "missing multiplicand witness", - ))?; - let multiplier_value = - model - .eval(&multiplier, true) - .ok_or(FixedPointProofError::SolverFailure( - "missing multiplier witness", - ))?; - let divisor_value = - model - .eval(&divisor, true) - .ok_or(FixedPointProofError::SolverFailure( - "missing divisor witness", - ))?; - let product_value = - model - .eval(&product, true) - .ok_or(FixedPointProofError::SolverFailure( - "missing product witness", - ))?; - let quotient_value = - model - .eval("ient, true) - .ok_or(FixedPointProofError::SolverFailure( - "missing quotient witness", - ))?; - - Ok(FixedPointProofReport { - function_name: spec.function_name.clone(), - backend: SmtBackend::Z3, - proven_safe: false, - checked_properties, - message: "Z3 found a counterexample within the configured input ranges." - .to_string(), - counterexample: Some(FixedPointCounterexample { - multiplicand: multiplicand_value.to_string(), - multiplier: multiplier_value.to_string(), - divisor: divisor_value.to_string(), - intermediate_product: product_value.to_string(), - quotient: quotient_value.to_string(), - }), - }) - } - SatResult::Unknown => Err(FixedPointProofError::SolverFailure( - "Z3 returned unknown for the requested fixed-point proof", - )), - } -} - -fn int_from_u128<'ctx>(ctx: &'ctx Context, value: u128) -> Int<'ctx> { - Int::from_str(ctx, &value.to_string()).expect("u128 literal should be a valid Z3 integer") -} - -fn run_strategy(ctx: &Context, strategy: SmtProofStrategy) -> SatResult { - let solver = Solver::new(ctx); - let a = Int::new_const(ctx, "a"); - let b = Int::new_const(ctx, "b"); - let zero = Int::from_i64(ctx, 0); - let max_u64 = Int::from_u64(ctx, u64::MAX); - - solver.assert(&a.ge(&zero)); - solver.assert(&b.ge(&zero)); - - match strategy { - SmtProofStrategy::UnconstrainedOverflow => { - solver.assert(&a.le(&max_u64)); - solver.assert(&b.le(&max_u64)); - } - SmtProofStrategy::BoundedDomainOverflow => { - let max = Int::from_i64(ctx, 5_000_000_000); - solver.assert(&a.le(&max)); - solver.assert(&b.le(&max)); - } - SmtProofStrategy::SmallDomainOverflow => { - let max = Int::from_i64(ctx, 10_000); - solver.assert(&a.le(&max)); - solver.assert(&b.le(&max)); - } - } - - let sum = Int::add(ctx, &[&a, &b]); - solver.assert(&sum.gt(&max_u64)); - solver.check() -} - -#[cfg(test)] -mod tests { - use super::*; - - #[test] - fn prove_fixed_point_mul_div_bounds_reports_safe_ranges() { - let spec = FixedPointMulDivSpec { - function_name: "mul_div_floor".to_string(), - multiplicand_max: 1_000_000_000_000_000_000, - multiplier_max: 1_000_000_000_000_000_000, - divisor_min: 1, - divisor_max: 10_000_000, - result_max: Some(u128::MAX), - }; - - let report = prove_fixed_point_mul_div_bounds(&spec).unwrap(); - assert!(report.proven_safe); - assert!(report.counterexample.is_none()); - } - - #[test] - fn prove_fixed_point_mul_div_bounds_reports_counterexample_for_unsafe_ranges() { - let spec = FixedPointMulDivSpec { - function_name: "mul_div_floor".to_string(), - multiplicand_max: u128::MAX, - multiplier_max: 2, - divisor_min: 1, - divisor_max: 1, - result_max: None, - }; - - let report = prove_fixed_point_mul_div_bounds(&spec).unwrap(); - assert!(!report.proven_safe); - let witness = report.counterexample.unwrap(); - assert!(!witness.intermediate_product.is_empty()); - } - - #[test] - fn prove_fixed_point_mul_div_bounds_rejects_zero_divisor() { - let spec = FixedPointMulDivSpec { - function_name: "invalid".to_string(), - multiplicand_max: 10, - multiplier_max: 10, - divisor_min: 0, - divisor_max: 10, - result_max: None, - }; - - let error = prove_fixed_point_mul_div_bounds(&spec).unwrap_err(); - assert_eq!( - error, - FixedPointProofError::InvalidSpec("divisor_min must be greater than zero") - ); - } - - #[test] - fn prove_fixed_point_mul_div_bounds_supports_backend_abstraction() { - let spec = FixedPointMulDivSpec { - function_name: "mul_div_floor".to_string(), - multiplicand_max: 10, - multiplier_max: 10, - divisor_min: 1, - divisor_max: 10, - result_max: None, - }; - - let error = - prove_fixed_point_mul_div_bounds_with_backend(SmtBackend::Cvc5, &spec).unwrap_err(); - assert_eq!( - error, - FixedPointProofError::UnsupportedBackend(SmtBackend::Cvc5) - ); - } - - // ── SmtFinding / verify_invariants tests ───────────────────────────────── - - #[test] - fn verify_invariants_empty_source_returns_no_findings() { - let findings = verify_invariants("", &SmtConfig::default()); - assert!(findings.is_empty(), "empty source must produce no findings"); - } - - #[test] - fn verify_invariants_parse_error_returns_no_findings() { - let findings = verify_invariants("this is not valid rust }{{{", &SmtConfig::default()); - assert!( - findings.is_empty(), - "unparseable source must produce no findings" - ); - } - - #[test] - fn parse_invariants_extracts_attribute_from_ast() { - let source = r#" - impl Vault { - #[invariant = "balance + deposit <= u64::MAX"] - pub fn deposit(&self, deposit: u64) {} - } - "#; - let specs = parse_invariants(source); - assert_eq!(specs.len(), 1); - assert_eq!(specs[0].expression, "balance + deposit <= u64::MAX"); - assert_eq!(specs[0].location, "deposit"); - } - - #[test] - fn verify_invariants_addition_overflow_flagged() { - // An invariant on an addition can overflow — Z3 must find a counterexample. - let source = r#" - impl Vault { - #[invariant = "a + b is safe"] - pub fn credit(&self, a: u64, b: u64) {} - } - "#; - let findings = verify_invariants(source, &SmtConfig::default()); - assert_eq!(findings.len(), 1); - assert!( - !findings[0].is_timeout, - "should be a SAT result, not timeout" - ); - assert!( - findings[0].counterexample.is_some(), - "counterexample must be populated for an unsafe invariant" - ); - assert!( - findings[0] - .counterexample - .as_ref() - .unwrap() - .contains("overflow"), - "counterexample should mention overflow" - ); - } - - #[test] - fn verify_invariants_non_arithmetic_expression_is_safe() { - // Invariants with no arithmetic operator are not modelled by the solver - // and produce no finding (proven safe by abstention). - let source = r#" - impl Token { - #[invariant = "admin_only"] - pub fn burn(&self) {} - } - "#; - let findings = verify_invariants(source, &SmtConfig::default()); - assert!( - findings.is_empty(), - "non-arithmetic invariant must not produce a finding" - ); - } - - #[test] - fn verify_invariants_timeout_produces_is_timeout_true() { - // Force a 1 ms timeout so the solver cannot finish and returns Unknown. - let source = r#" - impl Vault { - #[invariant = "a + b is safe"] - pub fn credit(&self, a: u64, b: u64) {} - } - "#; - let config = SmtConfig { timeout_ms: 1 }; - let findings = verify_invariants(source, &config); - // At 1 ms the solver may time out OR solve immediately (it is fast for - // simple queries). Accept both outcomes — the important thing is that - // if is_timeout is true, counterexample is None. - for f in &findings { - if f.is_timeout { - assert!( - f.counterexample.is_none(), - "timed-out findings must have no counterexample" - ); - } - } - } -} diff --git a/tooling/sanctifier-core/src/smt/backend.rs b/tooling/sanctifier-core/src/smt/backend.rs new file mode 100644 index 00000000..6cd244b6 --- /dev/null +++ b/tooling/sanctifier-core/src/smt/backend.rs @@ -0,0 +1,330 @@ +//! Z3 solver wrapper (`SmtVerifier`) and backend dispatch for fixed-point proofs. +//! +//! This module owns the Z3 `Context`-lifetime type [`SmtVerifier`] and the +//! top-level dispatcher [`prove_fixed_point_mul_div_bounds_with_backend`]. +//! All Z3 API imports are confined here so the rest of the crate never touches +//! the `z3` crate directly. + +use z3::ast::{Bool, Int}; +use z3::{Context, SatResult, Solver}; + +use super::types::{ + FixedPointCounterexample, FixedPointMulDivSpec, FixedPointProofError, FixedPointProofReport, + SmtBackend, SmtInvariantIssue, +}; + +// ── SmtVerifier ─────────────────────────────────────────────────────────────── + +/// Z3-backed SMT solver wrapper. +/// +/// Bound to a single Z3 [`Context`] for its lifetime. Create a new +/// `SmtVerifier` per verification session. +pub struct SmtVerifier<'ctx> { + ctx: &'ctx Context, +} + +impl<'ctx> SmtVerifier<'ctx> { + /// Create a verifier bound to a Z3 [`Context`]. + pub fn new(ctx: &'ctx Context) -> Self { + Self { ctx } + } + + /// Uses Z3 to prove whether `a + b` can overflow a 64-bit unsigned integer + /// under unconstrained inputs. + /// + /// Returns [`Some(SmtInvariantIssue)`] when overflow is reachable, `None` + /// when the solver proves safety. + pub fn verify_addition_overflow( + &self, + fn_name: &str, + location: &str, + ) -> Option { + let solver = Solver::new(self.ctx); + let a = Int::new_const(self.ctx, "a"); + let b = Int::new_const(self.ctx, "b"); + + let zero = Int::from_u64(self.ctx, 0); + let max_u64 = Int::from_u64(self.ctx, u64::MAX); + + solver.assert(&a.ge(&zero)); + solver.assert(&a.le(&max_u64)); + solver.assert(&b.ge(&zero)); + solver.assert(&b.le(&max_u64)); + + // Assert the violation: a + b > u64::MAX. SAT → overflow is reachable. + let sum = Int::add(self.ctx, &[&a, &b]); + solver.assert(&sum.gt(&max_u64)); + + if solver.check() == SatResult::Sat { + Some(SmtInvariantIssue { + function_name: fn_name.to_string(), + description: "SMT Solver (Z3) proved that this addition can overflow u64 bounds." + .to_string(), + location: location.to_string(), + }) + } else { + None + } + } +} + +// ── Fixed-point proof dispatch ──────────────────────────────────────────────── + +/// Prove that `a * b / d` cannot overflow `u128` within the provided bounds +/// using the default backend (Z3). +pub fn prove_fixed_point_mul_div_bounds( + spec: &FixedPointMulDivSpec, +) -> Result { + prove_fixed_point_mul_div_bounds_with_backend(SmtBackend::Z3, spec) +} + +/// Prove that `a * b / d` cannot overflow `u128` within the provided bounds +/// using the selected SMT backend. +pub fn prove_fixed_point_mul_div_bounds_with_backend( + backend: SmtBackend, + spec: &FixedPointMulDivSpec, +) -> Result { + validate_fixed_point_spec(spec)?; + + match backend { + SmtBackend::Z3 => prove_fixed_point_z3(spec), + SmtBackend::Cvc5 => Err(FixedPointProofError::UnsupportedBackend(SmtBackend::Cvc5)), + } +} + +// ── Internal: spec validation ───────────────────────────────────────────────── + +fn validate_fixed_point_spec(spec: &FixedPointMulDivSpec) -> Result<(), FixedPointProofError> { + if spec.divisor_min == 0 { + return Err(FixedPointProofError::InvalidSpec( + "divisor_min must be greater than zero", + )); + } + if spec.divisor_max < spec.divisor_min { + return Err(FixedPointProofError::InvalidSpec( + "divisor_max must be greater than or equal to divisor_min", + )); + } + Ok(()) +} + +// ── Internal: Z3 proof ──────────────────────────────────────────────────────── + +fn prove_fixed_point_z3( + spec: &FixedPointMulDivSpec, +) -> Result { + use z3::Config; + + let cfg = Config::new(); + let ctx = Context::new(&cfg); + let solver = Solver::new(&ctx); + + let multiplicand = Int::new_const(&ctx, "multiplicand"); + let multiplier = Int::new_const(&ctx, "multiplier"); + let divisor = Int::new_const(&ctx, "divisor"); + + let zero = int_from_u128(&ctx, 0); + let max_u128 = int_from_u128(&ctx, u128::MAX); + let multiplicand_max = int_from_u128(&ctx, spec.multiplicand_max); + let multiplier_max = int_from_u128(&ctx, spec.multiplier_max); + let divisor_min = int_from_u128(&ctx, spec.divisor_min); + let divisor_max = int_from_u128(&ctx, spec.divisor_max); + + solver.assert(&multiplicand.ge(&zero)); + solver.assert(&multiplicand.le(&multiplicand_max)); + solver.assert(&multiplier.ge(&zero)); + solver.assert(&multiplier.le(&multiplier_max)); + solver.assert(&divisor.ge(&divisor_min)); + solver.assert(&divisor.le(&divisor_max)); + + let product = Int::mul(&ctx, &[&multiplicand, &multiplier]); + let quotient = product.div(&divisor); + let product_overflow = product.gt(&max_u128); + + let mut checked_properties = vec!["intermediate multiplication fits in u128".to_string()]; + + let violation = if let Some(result_max) = spec.result_max { + checked_properties.push(format!("final quotient <= {}", result_max)); + let quotient_overflow = quotient.gt(&int_from_u128(&ctx, result_max)); + Bool::or(&ctx, &[&product_overflow, "ient_overflow]) + } else { + product_overflow + }; + + solver.assert(&violation); + + match solver.check() { + SatResult::Unsat => Ok(FixedPointProofReport { + function_name: spec.function_name.clone(), + backend: SmtBackend::Z3, + proven_safe: true, + checked_properties, + message: "Z3 proved the fixed-point calculation stays within the configured bounds." + .to_string(), + counterexample: None, + }), + SatResult::Sat => { + let model = solver + .get_model() + .ok_or(FixedPointProofError::SolverFailure( + "missing model for SAT result", + ))?; + + let multiplicand_value = model + .eval(&multiplicand, true) + .ok_or(FixedPointProofError::SolverFailure( + "missing multiplicand witness", + ))?; + let multiplier_value = model + .eval(&multiplier, true) + .ok_or(FixedPointProofError::SolverFailure( + "missing multiplier witness", + ))?; + let divisor_value = model + .eval(&divisor, true) + .ok_or(FixedPointProofError::SolverFailure( + "missing divisor witness", + ))?; + let product_value = model + .eval(&product, true) + .ok_or(FixedPointProofError::SolverFailure( + "missing product witness", + ))?; + let quotient_value = model + .eval("ient, true) + .ok_or(FixedPointProofError::SolverFailure( + "missing quotient witness", + ))?; + + Ok(FixedPointProofReport { + function_name: spec.function_name.clone(), + backend: SmtBackend::Z3, + proven_safe: false, + checked_properties, + message: "Z3 found a counterexample within the configured input ranges." + .to_string(), + counterexample: Some(FixedPointCounterexample { + multiplicand: multiplicand_value.to_string(), + multiplier: multiplier_value.to_string(), + divisor: divisor_value.to_string(), + intermediate_product: product_value.to_string(), + quotient: quotient_value.to_string(), + }), + }) + } + SatResult::Unknown => Err(FixedPointProofError::SolverFailure( + "Z3 returned unknown for the requested fixed-point proof", + )), + } +} + +fn int_from_u128<'ctx>(ctx: &'ctx Context, value: u128) -> Int<'ctx> { + Int::from_str(ctx, &value.to_string()).expect("u128 literal should be a valid Z3 integer") +} + +// ── Tests ───────────────────────────────────────────────────────────────────── + +#[cfg(test)] +mod tests { + use super::*; + + #[test] + fn prove_fixed_point_reports_safe_ranges() { + let spec = FixedPointMulDivSpec { + function_name: "mul_div_floor".to_string(), + multiplicand_max: 1_000_000_000_000_000_000, + multiplier_max: 1_000_000_000_000_000_000, + divisor_min: 1, + divisor_max: 10_000_000, + result_max: Some(u128::MAX), + }; + let report = prove_fixed_point_mul_div_bounds(&spec).unwrap(); + assert!(report.proven_safe); + assert!(report.counterexample.is_none()); + } + + #[test] + fn prove_fixed_point_reports_counterexample_for_unsafe_ranges() { + let spec = FixedPointMulDivSpec { + function_name: "mul_div_floor".to_string(), + multiplicand_max: u128::MAX, + multiplier_max: 2, + divisor_min: 1, + divisor_max: 1, + result_max: None, + }; + let report = prove_fixed_point_mul_div_bounds(&spec).unwrap(); + assert!(!report.proven_safe); + let witness = report.counterexample.unwrap(); + assert!(!witness.intermediate_product.is_empty()); + } + + #[test] + fn prove_fixed_point_rejects_zero_divisor() { + let spec = FixedPointMulDivSpec { + function_name: "invalid".to_string(), + multiplicand_max: 10, + multiplier_max: 10, + divisor_min: 0, + divisor_max: 10, + result_max: None, + }; + let error = prove_fixed_point_mul_div_bounds(&spec).unwrap_err(); + assert_eq!( + error, + FixedPointProofError::InvalidSpec("divisor_min must be greater than zero") + ); + } + + #[test] + fn prove_fixed_point_rejects_inverted_divisor_range() { + let spec = FixedPointMulDivSpec { + function_name: "invalid".to_string(), + multiplicand_max: 10, + multiplier_max: 10, + divisor_min: 10, + divisor_max: 1, + result_max: None, + }; + let error = prove_fixed_point_mul_div_bounds(&spec).unwrap_err(); + assert_eq!( + error, + FixedPointProofError::InvalidSpec( + "divisor_max must be greater than or equal to divisor_min" + ) + ); + } + + #[test] + fn prove_fixed_point_returns_unsupported_for_cvc5_backend() { + let spec = FixedPointMulDivSpec { + function_name: "mul_div_floor".to_string(), + multiplicand_max: 10, + multiplier_max: 10, + divisor_min: 1, + divisor_max: 10, + result_max: None, + }; + let error = + prove_fixed_point_mul_div_bounds_with_backend(SmtBackend::Cvc5, &spec).unwrap_err(); + assert_eq!( + error, + FixedPointProofError::UnsupportedBackend(SmtBackend::Cvc5) + ); + } + + #[test] + fn smt_verifier_detects_addition_overflow() { + let cfg = z3::Config::new(); + let ctx = Context::new(&cfg); + let verifier = SmtVerifier::new(&ctx); + let issue = verifier.verify_addition_overflow("test_fn", "test_fn:1"); + assert!( + issue.is_some(), + "unconstrained u64 addition must be flagged as potentially overflowing" + ); + let issue = issue.unwrap(); + assert_eq!(issue.function_name, "test_fn"); + assert_eq!(issue.location, "test_fn:1"); + } +} diff --git a/tooling/sanctifier-core/src/smt/benchmark.rs b/tooling/sanctifier-core/src/smt/benchmark.rs new file mode 100644 index 00000000..edc44d6f --- /dev/null +++ b/tooling/sanctifier-core/src/smt/benchmark.rs @@ -0,0 +1,153 @@ +//! SMT solver latency micro-benchmark. +//! +//! Runs each [`SmtProofStrategy`] for a configurable number of iterations and +//! collects min/max/avg/p95 latency statistics. Results are returned as a +//! [`SmtLatencyBenchmarkReport`] that can be serialised to JSON and uploaded +//! as a CI artifact. +//! +//! This module has no production code path — it is only called from the +//! integration test `tests/smt_latency_benchmark.rs`. + +use std::time::Instant; + +use z3::ast::Int; +use z3::{Config, Context, SatResult, Solver}; + +use super::types::{ + SmtLatencyBenchmarkReport, SmtProofStrategy, SmtStrategyLatency, +}; + +// ── Public API ──────────────────────────────────────────────────────────────── + +/// Run a latency micro-benchmark for each [`SmtProofStrategy`]. +/// +/// Each strategy is run `iterations_per_strategy` times (minimum 1). +/// Returns an [`SmtLatencyBenchmarkReport`] with per-strategy statistics. +pub fn run_smt_latency_benchmark(iterations_per_strategy: usize) -> SmtLatencyBenchmarkReport { + let iterations = iterations_per_strategy.max(1); + let strategies = [ + SmtProofStrategy::UnconstrainedOverflow, + SmtProofStrategy::BoundedDomainOverflow, + SmtProofStrategy::SmallDomainOverflow, + ]; + + let mut results = Vec::with_capacity(strategies.len()); + + for strategy in strategies { + let mut samples = Vec::with_capacity(iterations); + for _ in 0..iterations { + let cfg = Config::new(); + let ctx = Context::new(&cfg); + + let start = Instant::now(); + let _ = run_strategy(&ctx, strategy); + samples.push(start.elapsed().as_micros()); + } + + samples.sort_unstable(); + let min_micros = samples.first().copied().unwrap_or_default(); + let max_micros = samples.last().copied().unwrap_or_default(); + let total: u128 = samples.iter().sum(); + let avg_micros = total / samples.len() as u128; + let p95_index = (((samples.len() - 1) as f64) * 0.95).round() as usize; + let p95_micros = samples[p95_index]; + + results.push(SmtStrategyLatency { + strategy, + runs: iterations, + min_micros, + max_micros, + avg_micros, + p95_micros, + }); + } + + SmtLatencyBenchmarkReport { + timestamp: chrono::Utc::now().to_rfc3339(), + iterations_per_strategy: iterations, + strategies: results, + } +} + +// ── Internal: strategy runner ───────────────────────────────────────────────── + +fn run_strategy(ctx: &Context, strategy: SmtProofStrategy) -> SatResult { + let solver = Solver::new(ctx); + let a = Int::new_const(ctx, "a"); + let b = Int::new_const(ctx, "b"); + let zero = Int::from_i64(ctx, 0); + let max_u64 = Int::from_u64(ctx, u64::MAX); + + solver.assert(&a.ge(&zero)); + solver.assert(&b.ge(&zero)); + + match strategy { + SmtProofStrategy::UnconstrainedOverflow => { + solver.assert(&a.le(&max_u64)); + solver.assert(&b.le(&max_u64)); + } + SmtProofStrategy::BoundedDomainOverflow => { + let max = Int::from_i64(ctx, 5_000_000_000); + solver.assert(&a.le(&max)); + solver.assert(&b.le(&max)); + } + SmtProofStrategy::SmallDomainOverflow => { + let max = Int::from_i64(ctx, 10_000); + solver.assert(&a.le(&max)); + solver.assert(&b.le(&max)); + } + } + + let sum = Int::add(ctx, &[&a, &b]); + solver.assert(&sum.gt(&max_u64)); + solver.check() +} + +// ── Tests ───────────────────────────────────────────────────────────────────── + +#[cfg(test)] +mod tests { + use super::*; + + #[test] + fn benchmark_returns_three_strategy_results() { + let report = run_smt_latency_benchmark(3); + assert_eq!(report.strategies.len(), 3); + assert_eq!(report.iterations_per_strategy, 3); + } + + #[test] + fn benchmark_min_never_exceeds_max() { + let report = run_smt_latency_benchmark(5); + for s in &report.strategies { + assert!( + s.min_micros <= s.max_micros, + "min ({}) must not exceed max ({}) for {:?}", + s.min_micros, + s.max_micros, + s.strategy + ); + } + } + + #[test] + fn benchmark_most_expensive_first_is_sorted_descending() { + let report = run_smt_latency_benchmark(3); + let sorted = report.most_expensive_first(); + for pair in sorted.windows(2) { + assert!( + pair[0].avg_micros >= pair[1].avg_micros, + "most_expensive_first must be sorted by descending avg_micros" + ); + } + } + + #[test] + fn benchmark_zero_iterations_treated_as_one() { + let report = run_smt_latency_benchmark(0); + assert_eq!(report.iterations_per_strategy, 1); + for s in &report.strategies { + assert_eq!(s.runs, 1); + } + } +} diff --git a/tooling/sanctifier-core/src/smt/invariants.rs b/tooling/sanctifier-core/src/smt/invariants.rs new file mode 100644 index 00000000..2b586b79 --- /dev/null +++ b/tooling/sanctifier-core/src/smt/invariants.rs @@ -0,0 +1,251 @@ +//! AST-based `#[invariant = "..."]` parsing and Z3 verification. +//! +//! This module owns the two public entry-points for S011: +//! - [`parse_invariants`] — extract annotations from Rust source via `syn` +//! - [`verify_invariants`] — check each annotation with Z3 under a timeout + +use z3::ast::Int; +use z3::{Config, Context, SatResult, Solver}; + +use super::types::{InvariantSpec, SmtConfig, SmtFinding}; + +// ── Public API ──────────────────────────────────────────────────────────────── + +/// Parse every `#[invariant = "..."]` attribute in the source file using the +/// syn AST. Returns an empty vec on parse errors (no panic). +pub fn parse_invariants(source: &str) -> Vec { + use syn::{parse_str, Expr, File, Item, Lit, Meta}; + + let file = match parse_str::(source) { + Ok(f) => f, + Err(_) => return vec![], + }; + + let mut specs = Vec::new(); + + for item in &file.items { + if let Item::Impl(impl_block) = item { + for impl_item in &impl_block.items { + if let syn::ImplItem::Fn(f) = impl_item { + let fn_name = f.sig.ident.to_string(); + for attr in &f.attrs { + if attr.path().is_ident("invariant") { + if let Meta::NameValue(nv) = &attr.meta { + if let Expr::Lit(expr_lit) = &nv.value { + if let Lit::Str(lit_str) = &expr_lit.lit { + specs.push(InvariantSpec { + expression: lit_str.value(), + location: fn_name.clone(), + }); + } + } + } + } + } + } + } + } + } + + specs +} + +/// Verify `#[invariant = "..."]` annotations with Z3 under a configurable +/// timeout. +/// +/// Returns one [`SmtFinding`] for every invariant that could not be proved +/// safe, or for which the solver timed out. Safe invariants produce no +/// finding. +pub fn verify_invariants(source: &str, config: &SmtConfig) -> Vec { + let specs = parse_invariants(source); + if specs.is_empty() { + return vec![]; + } + + let mut findings = Vec::new(); + for spec in &specs { + if let Some(finding) = check_invariant_spec(spec, config) { + findings.push(finding); + } + } + findings +} + +// ── Internal ────────────────────────────────────────────────────────────────── + +/// Check one [`InvariantSpec`] with Z3. +/// +/// * Expressions that mention addition (`+` / `add`) are verified against +/// u64 overflow. +/// * Expressions that mention subtraction (`-` / `sub`) are verified against +/// u64 underflow. +/// * All other expressions are skipped (no finding — they require manual +/// modelling). +fn check_invariant_spec(spec: &InvariantSpec, config: &SmtConfig) -> Option { + let expr_lower = spec.expression.to_lowercase(); + + let overflow_check = expr_lower.contains('+') || expr_lower.contains("add"); + let underflow_check = expr_lower.contains('-') || expr_lower.contains("sub"); + + if !overflow_check && !underflow_check { + return None; + } + + let mut cfg = Config::new(); + // Pass the timeout as milliseconds; Z3 returns Unknown when it expires. + cfg.set_param_value("timeout", &config.timeout_ms.to_string()); + let ctx = Context::new(&cfg); + let solver = Solver::new(&ctx); + + let a = Int::new_const(&ctx, "a"); + let b = Int::new_const(&ctx, "b"); + let zero = Int::from_u64(&ctx, 0); + let max_u64 = Int::from_u64(&ctx, u64::MAX); + + solver.assert(&a.ge(&zero)); + solver.assert(&a.le(&max_u64)); + solver.assert(&b.ge(&zero)); + solver.assert(&b.le(&max_u64)); + + let violation = if overflow_check { + let sum = Int::add(&ctx, &[&a, &b]); + sum.gt(&max_u64) + } else { + let diff = Int::sub(&ctx, &[&a, &b]); + diff.lt(&zero) + }; + + solver.assert(&violation); + + match solver.check() { + SatResult::Sat => { + let counterexample = solver.get_model().map(|m| { + let a_val = m + .eval(&a, true) + .map(|v| v.to_string()) + .unwrap_or_else(|| "?".to_string()); + let b_val = m + .eval(&b, true) + .map(|v| v.to_string()) + .unwrap_or_else(|| "?".to_string()); + if overflow_check { + format!("a={a_val}, b={b_val} — a+b overflows u64") + } else { + format!("a={a_val}, b={b_val} — a-b underflows u64") + } + }); + Some(SmtFinding { + invariant_name: spec.expression.clone(), + location: spec.location.clone(), + counterexample, + is_timeout: false, + }) + } + SatResult::Unsat => None, + SatResult::Unknown => Some(SmtFinding { + invariant_name: spec.expression.clone(), + location: spec.location.clone(), + counterexample: None, + is_timeout: true, + }), + } +} + +// ── Tests ───────────────────────────────────────────────────────────────────── + +#[cfg(test)] +mod tests { + use super::*; + + #[test] + fn verify_invariants_empty_source_returns_no_findings() { + let findings = verify_invariants("", &SmtConfig::default()); + assert!(findings.is_empty(), "empty source must produce no findings"); + } + + #[test] + fn verify_invariants_parse_error_returns_no_findings() { + let findings = verify_invariants("this is not valid rust }{{{", &SmtConfig::default()); + assert!( + findings.is_empty(), + "unparseable source must produce no findings" + ); + } + + #[test] + fn parse_invariants_extracts_attribute_from_ast() { + let source = r#" + impl Vault { + #[invariant = "balance + deposit <= u64::MAX"] + pub fn deposit(&self, deposit: u64) {} + } + "#; + let specs = parse_invariants(source); + assert_eq!(specs.len(), 1); + assert_eq!(specs[0].expression, "balance + deposit <= u64::MAX"); + assert_eq!(specs[0].location, "deposit"); + } + + #[test] + fn verify_invariants_addition_overflow_flagged() { + let source = r#" + impl Vault { + #[invariant = "a + b is safe"] + pub fn credit(&self, a: u64, b: u64) {} + } + "#; + let findings = verify_invariants(source, &SmtConfig::default()); + assert_eq!(findings.len(), 1); + assert!( + !findings[0].is_timeout, + "should be a SAT result, not timeout" + ); + assert!( + findings[0].counterexample.is_some(), + "counterexample must be populated for an unsafe invariant" + ); + assert!( + findings[0] + .counterexample + .as_ref() + .unwrap() + .contains("overflow"), + "counterexample should mention overflow" + ); + } + + #[test] + fn verify_invariants_non_arithmetic_expression_is_safe() { + let source = r#" + impl Token { + #[invariant = "admin_only"] + pub fn burn(&self) {} + } + "#; + let findings = verify_invariants(source, &SmtConfig::default()); + assert!( + findings.is_empty(), + "non-arithmetic invariant must not produce a finding" + ); + } + + #[test] + fn verify_invariants_timeout_produces_is_timeout_true() { + let source = r#" + impl Vault { + #[invariant = "a + b is safe"] + pub fn credit(&self, a: u64, b: u64) {} + } + "#; + let config = SmtConfig { timeout_ms: 1 }; + let findings = verify_invariants(source, &config); + for f in &findings { + if f.is_timeout { + assert!( + f.counterexample.is_none(), + "timed-out findings must have no counterexample" + ); + } + } + } +} diff --git a/tooling/sanctifier-core/src/smt/mod.rs b/tooling/sanctifier-core/src/smt/mod.rs new file mode 100644 index 00000000..e364097e --- /dev/null +++ b/tooling/sanctifier-core/src/smt/mod.rs @@ -0,0 +1,45 @@ +//! Z3-based formal-verification primitives (S011). +//! +//! # Module layout +//! +//! | Sub-module | Responsibility | +//! |---|---| +//! | [`types`] | All shared data types and error enums | +//! | [`invariants`] | `#[invariant = "..."]` AST parsing and Z3 verification | +//! | [`backend`] | `SmtVerifier`, Z3 context wrapper, fixed-point proof dispatch | +//! | [`benchmark`] | Latency micro-benchmark for CI artifact generation | +//! +//! All items from every sub-module are re-exported at this level so that +//! existing call sites (`use sanctifier_core::smt::SmtFinding`, etc.) are +//! **unchanged** — this refactor has zero breaking surface. +//! +//! # Feature flag +//! +//! This entire module is gated behind `#[cfg(feature = "smt")]`. Disable it +//! with `default-features = false` when targeting `wasm32-unknown-unknown`, +//! which has no native Z3 library. + +mod backend; +mod benchmark; +mod invariants; +mod types; + +// ── Public re-exports (zero-breaking-change surface) ───────────────────────── + +// Types +pub use types::{ + FixedPointCounterexample, FixedPointMulDivSpec, FixedPointProofError, FixedPointProofReport, + InvariantSpec, SmtBackend, SmtConfig, SmtFinding, SmtInvariantIssue, SmtLatencyBenchmarkReport, + SmtProofStrategy, SmtStrategyLatency, +}; + +// Invariant verification (S011 entry-points) +pub use invariants::{parse_invariants, verify_invariants}; + +// Backend: SmtVerifier + fixed-point proofs +pub use backend::{ + prove_fixed_point_mul_div_bounds, prove_fixed_point_mul_div_bounds_with_backend, SmtVerifier, +}; + +// Benchmark +pub use benchmark::run_smt_latency_benchmark; diff --git a/tooling/sanctifier-core/src/smt/types.rs b/tooling/sanctifier-core/src/smt/types.rs new file mode 100644 index 00000000..7b24240d --- /dev/null +++ b/tooling/sanctifier-core/src/smt/types.rs @@ -0,0 +1,191 @@ +//! Shared types for the SMT formal-verification module. +//! +//! All public data types are defined here so that the other sub-modules +//! (`invariants`, `fixed_point`, `benchmark`) can import them without +//! creating circular dependencies. + +use serde::{Deserialize, Serialize}; +use thiserror::Error; + +// ── Core finding type ───────────────────────────────────────────────────────── + +/// An invariant issue proved by the Z3 SMT solver (finding code S011). +#[derive(Debug, Serialize, Deserialize, Clone)] +pub struct SmtInvariantIssue { + /// Function under verification. + pub function_name: String, + /// Human-readable description of the violation. + pub description: String, + /// Source location. + pub location: String, +} + +// ── Invariant verification types ────────────────────────────────────────────── + +/// Configuration for the SMT-based invariant verifier. +#[derive(Debug, Clone, Serialize, Deserialize)] +pub struct SmtConfig { + /// Solver timeout per call in milliseconds (default 10 000 ms = 10 s). + pub timeout_ms: u64, +} + +impl Default for SmtConfig { + fn default() -> Self { + Self { timeout_ms: 10_000 } + } +} + +/// Structured finding returned by the SMT invariant verifier. +#[derive(Debug, Serialize, Deserialize, Clone)] +pub struct SmtFinding { + /// Name / expression of the invariant that was checked. + pub invariant_name: String, + /// Source location (enclosing function name or file:line). + pub location: String, + /// Concrete counterexample values returned by Z3, when available. + pub counterexample: Option, + /// `true` when the solver timed out instead of producing sat/unsat. + pub is_timeout: bool, +} + +/// A `#[invariant = "..."]` annotation extracted from Rust source via AST +/// analysis (not regex). +#[derive(Debug, Clone, PartialEq, Eq)] +pub struct InvariantSpec { + /// The raw invariant expression (e.g. `"balance >= 0"`). + pub expression: String, + /// Enclosing function name used as the location hint. + pub location: String, +} + +// ── Backend selector ────────────────────────────────────────────────────────── + +/// Supported SMT backends for fixed-point proofs. +#[derive(Debug, Serialize, Deserialize, Clone, Copy, PartialEq, Eq)] +#[serde(rename_all = "snake_case")] +#[non_exhaustive] +pub enum SmtBackend { + /// Z3 backend. + Z3, + /// Placeholder for future CVC5 support. + Cvc5, +} + +// ── Fixed-point proof types ─────────────────────────────────────────────────── + +/// Input bounds for a standard fixed-point `a * b / d` proof. +#[derive(Debug, Serialize, Deserialize, Clone)] +pub struct FixedPointMulDivSpec { + /// Human-readable function or calculation name. + pub function_name: String, + /// Maximum value of the left multiplicand. + pub multiplicand_max: u128, + /// Maximum value of the right multiplicand. + pub multiplier_max: u128, + /// Minimum divisor value (must be > 0). + pub divisor_min: u128, + /// Maximum divisor value. + pub divisor_max: u128, + /// Optional bound for the final quotient. + #[serde(skip_serializing_if = "Option::is_none")] + pub result_max: Option, +} + +/// Concrete witness returned when a fixed-point proof fails. +#[derive(Debug, Serialize, Deserialize, Clone)] +pub struct FixedPointCounterexample { + /// Value chosen for the left multiplicand. + pub multiplicand: String, + /// Value chosen for the right multiplicand. + pub multiplier: String, + /// Value chosen for the divisor. + pub divisor: String, + /// Intermediate `a * b` result. + pub intermediate_product: String, + /// Final `(a * b) / d` quotient. + pub quotient: String, +} + +/// Result of a fixed-point overflow proof. +#[derive(Debug, Serialize, Deserialize, Clone)] +pub struct FixedPointProofReport { + /// Human-readable function or calculation name. + pub function_name: String, + /// Backend used for the proof. + pub backend: SmtBackend, + /// Whether the proof established safety for all inputs in range. + pub proven_safe: bool, + /// Properties checked during the proof. + pub checked_properties: Vec, + /// Summary message. + pub message: String, + /// Concrete witness if the proof failed. + #[serde(skip_serializing_if = "Option::is_none")] + pub counterexample: Option, +} + +/// Errors raised when preparing or executing a fixed-point proof. +#[derive(Debug, Error, Clone, PartialEq, Eq)] +pub enum FixedPointProofError { + /// Invalid input bounds. + #[error("invalid fixed-point proof specification: {0}")] + InvalidSpec(&'static str), + /// The requested backend is not implemented yet. + #[error("unsupported SMT backend: {0:?}")] + UnsupportedBackend(SmtBackend), + /// The backend did not produce a usable answer. + #[error("solver did not produce a usable result: {0}")] + SolverFailure(&'static str), +} + +// ── Benchmark types ─────────────────────────────────────────────────────────── + +/// The constraint-generation strategy used for an SMT proof. +#[derive(Debug, Serialize, Deserialize, Clone, Copy, PartialEq, Eq)] +#[serde(rename_all = "snake_case")] +#[non_exhaustive] +pub enum SmtProofStrategy { + /// Full u64 range. + UnconstrainedOverflow, + /// Bounded to ~5 × 10⁹. + BoundedDomainOverflow, + /// Bounded to 10 000. + SmallDomainOverflow, +} + +/// Latency statistics for a single [`SmtProofStrategy`]. +#[derive(Debug, Serialize, Deserialize, Clone)] +pub struct SmtStrategyLatency { + /// Which strategy was measured. + pub strategy: SmtProofStrategy, + /// Number of iterations. + pub runs: usize, + /// Fastest run in microseconds. + pub min_micros: u128, + /// Slowest run in microseconds. + pub max_micros: u128, + /// Mean duration in microseconds. + pub avg_micros: u128, + /// 95th-percentile duration in microseconds. + pub p95_micros: u128, +} + +/// Aggregate benchmark across all [`SmtProofStrategy`] variants. +#[derive(Debug, Serialize, Deserialize, Clone)] +pub struct SmtLatencyBenchmarkReport { + /// Timestamp of the benchmark run. + pub timestamp: String, + /// How many iterations were run per strategy. + pub iterations_per_strategy: usize, + /// Per-strategy results. + pub strategies: Vec, +} + +impl SmtLatencyBenchmarkReport { + /// Return strategies ordered by descending average latency. + pub fn most_expensive_first(&self) -> Vec { + let mut sorted = self.strategies.clone(); + sorted.sort_by(|a, b| b.avg_micros.cmp(&a.avg_micros)); + sorted + } +} diff --git a/tooling/sanctifier-core/tests/rule_engine_orchestration_test.rs b/tooling/sanctifier-core/tests/rule_engine_orchestration_test.rs new file mode 100644 index 00000000..4b2e9a9d --- /dev/null +++ b/tooling/sanctifier-core/tests/rule_engine_orchestration_test.rs @@ -0,0 +1,492 @@ +//! Integration / e2e tests for rule engine orchestration. +//! +//! These tests exercise the full orchestration pipeline end-to-end: +//! discovery order, filtering, deduplication, custom-rule execution, +//! and consistent outputs under repeated calls. +//! +//! They are intentionally black-box: every assertion is made through +//! the public `RuleRegistry` / `Analyzer` API, never against internal +//! implementation details. +//! +//! # Running locally +//! +//! ```bash +//! cargo test --test rule_engine_orchestration_test -p sanctifier-core +//! ``` + +use sanctifier_core::rules::{RuleRegistry, RuleViolation, Severity}; +use sanctifier_core::{Analyzer, SanctifyConfig}; + +// ── Source fixtures ─────────────────────────────────────────────────────────── + +/// A contract with no detectable issues — expected to produce zero violations +/// across all built-in rules. +const CLEAN_CONTRACT: &str = r#" + use soroban_sdk::{contract, contractimpl, Address, Env}; + #[contract] pub struct Token; + #[contractimpl] impl Token { + pub fn transfer(env: Env, from: Address, to: Address, amount: i128) { + from.require_auth(); + } + } +"#; + +/// A contract with a missing `require_auth` — triggers `auth_gap` (S001). +const AUTH_GAP_CONTRACT: &str = r#" + use soroban_sdk::{contract, contractimpl, Address, Env, Symbol}; + #[contract] pub struct Vault; + #[contractimpl] impl Vault { + pub fn withdraw(env: Env, recipient: Address, amount: i128) { + env.storage().persistent().set(&recipient, &amount); + } + } +"#; + +/// A contract with an unchecked addition — triggers `arithmetic_overflow` (S003). +const OVERFLOW_CONTRACT: &str = r#" + use soroban_sdk::{contract, contractimpl, Env}; + #[contract] pub struct Calc; + #[contractimpl] impl Calc { + pub fn add(_env: Env, a: u64, b: u64) -> u64 { a + b } + } +"#; + +/// A contract with a bare `panic!` — triggers `panic_detection` (S002). +const PANIC_CONTRACT: &str = r#" + use soroban_sdk::{contract, contractimpl, Env}; + #[contract] pub struct Risky; + #[contractimpl] impl Risky { + pub fn boom(_env: Env) { panic!("not implemented"); } + } +"#; + +/// A contract that triggers multiple distinct rules simultaneously. +const MULTI_ISSUE_CONTRACT: &str = r#" + use soroban_sdk::{contract, contractimpl, Address, Env}; + #[contract] pub struct Multi; + #[contractimpl] impl Multi { + pub fn dangerous(_env: Env, a: u64, b: u64, recipient: Address) -> u64 { + // Missing require_auth → S001 + // Unchecked add → S003 + // Unwrap → S002 via panic_detection + let x: Option = None; + let _ = x.unwrap(); + a + b + } + } +"#; + +// ── Helper ──────────────────────────────────────────────────────────────────── + +fn registry() -> RuleRegistry { + RuleRegistry::with_default_rules() +} + +fn rule_names_for(violations: &[RuleViolation]) -> Vec<&str> { + violations.iter().map(|v| v.rule_name.as_str()).collect() +} + +// ── 1. Registry population ──────────────────────────────────────────────────── + +#[test] +fn default_registry_contains_all_expected_built_in_rules() { + let reg = registry(); + let names = reg.available_rules(); + + // Spot-check a representative subset of the 25 built-in rules. + let required = [ + "auth_gap", + "arithmetic_overflow", + "panic_detection", + "unhandled_result", + "reentrancy", + "ledger_size", + "truncation_bounds", + "unsafe_prng", + "variable_shadowing", + "instance_storage_misuse", + "missing_state_event", + "static_reentrancy", + ]; + + for r in &required { + assert!( + names.contains(r), + "built-in rule '{r}' is missing from default registry" + ); + } +} + +#[test] +fn registry_has_no_duplicate_rule_names() { + let reg = registry(); + let names = reg.available_rules(); + let mut seen = std::collections::HashSet::new(); + for n in &names { + assert!(seen.insert(*n), "duplicate rule name: {n}"); + } +} + +// ── 2. Empty-source / clean-source baseline ─────────────────────────────────── + +#[test] +fn empty_source_produces_no_violations() { + let reg = registry(); + assert!( + reg.run_all("").is_empty(), + "empty source must produce no violations" + ); +} + +#[test] +fn clean_contract_produces_no_violations() { + let reg = registry(); + let violations = reg.run_all(CLEAN_CONTRACT); + assert!( + violations.is_empty(), + "clean contract must produce no violations, got: {violations:?}" + ); +} + +// ── 3. Per-rule firing ──────────────────────────────────────────────────────── + +#[test] +fn auth_gap_rule_fires_for_missing_require_auth() { + let reg = registry(); + let violations = reg.run_by_name(AUTH_GAP_CONTRACT, "auth_gap"); + assert!( + !violations.is_empty(), + "auth_gap rule must fire for contract missing require_auth" + ); + assert!(violations.iter().all(|v| v.rule_name == "auth_gap")); +} + +#[test] +fn arithmetic_overflow_rule_fires_for_bare_addition() { + let reg = registry(); + let violations = reg.run_by_name(OVERFLOW_CONTRACT, "arithmetic_overflow"); + assert!( + !violations.is_empty(), + "arithmetic_overflow must fire for bare `+`" + ); + assert!(violations + .iter() + .all(|v| v.rule_name == "arithmetic_overflow")); +} + +#[test] +fn panic_detection_rule_fires_for_bare_panic() { + let reg = registry(); + let violations = reg.run_by_name(PANIC_CONTRACT, "panic_detection"); + assert!( + !violations.is_empty(), + "panic_detection must fire for bare panic!()" + ); +} + +// ── 4. run_all fires multiple rules independently ───────────────────────────── + +#[test] +fn run_all_fires_multiple_rules_on_multi_issue_contract() { + let reg = registry(); + let violations = reg.run_all(MULTI_ISSUE_CONTRACT); + let names = rule_names_for(&violations); + + // At minimum, two distinct rules must fire. + let unique: std::collections::HashSet<_> = names.iter().copied().collect(); + assert!( + unique.len() >= 2, + "at least 2 distinct rules must fire on multi-issue contract, got: {unique:?}" + ); +} + +#[test] +fn run_all_results_contain_all_per_rule_results() { + // Each violation returned by run_all must also be returned by run_by_name + // for the corresponding rule. + let reg = registry(); + let all_violations = reg.run_all(MULTI_ISSUE_CONTRACT); + for v in &all_violations { + let per_rule = reg.run_by_name(MULTI_ISSUE_CONTRACT, &v.rule_name); + let found = per_rule.iter().any(|p| { + p.rule_name == v.rule_name && p.location == v.location && p.message == v.message + }); + assert!( + found, + "violation from run_all not reproduced by run_by_name('{}') — location: {}", + v.rule_name, v.location + ); + } +} + +// ── 5. Severity field integrity ──────────────────────────────────────────────── + +#[test] +fn every_violation_has_a_valid_severity() { + let reg = registry(); + let violations = reg.run_all(MULTI_ISSUE_CONTRACT); + // The point here is that no violation has an unrecognised/panicking severity. + // Asserting all three variants are representable. + let valid = [Severity::Error, Severity::Warning, Severity::Info]; + for v in &violations { + assert!( + valid.contains(&v.severity), + "violation from '{}' has unrecognised severity: {:?}", + v.rule_name, + v.severity + ); + } +} + +// ── 6. Location field integrity ─────────────────────────────────────────────── + +#[test] +fn every_violation_has_non_empty_location() { + let reg = registry(); + let violations = reg.run_all(MULTI_ISSUE_CONTRACT); + for v in &violations { + assert!( + !v.location.is_empty(), + "violation from '{}' has an empty location field", + v.rule_name + ); + } +} + +// ── 7. Determinism ──────────────────────────────────────────────────────────── + +#[test] +fn run_all_is_deterministic_across_repeated_calls() { + let reg = registry(); + + // Run 10 times, collect sorted (rule_name, location) pairs each time. + let runs: Vec> = (0..10) + .map(|_| { + let mut v: Vec<(String, String)> = reg + .run_all(MULTI_ISSUE_CONTRACT) + .into_iter() + .map(|v| (v.rule_name, v.location)) + .collect(); + v.sort(); + v + }) + .collect(); + + let reference = &runs[0]; + for run in &runs[1..] { + assert_eq!( + reference, run, + "run_all must return identical findings on repeated calls" + ); + } +} + +#[test] +fn run_by_name_is_deterministic_across_repeated_calls() { + let reg = registry(); + + let runs: Vec> = (0..10) + .map(|_| { + let mut locs: Vec = reg + .run_by_name(AUTH_GAP_CONTRACT, "auth_gap") + .into_iter() + .map(|v| v.location) + .collect(); + locs.sort(); + locs + }) + .collect(); + + let reference = &runs[0]; + for run in &runs[1..] { + assert_eq!( + reference, run, + "run_by_name must return identical locations on repeated calls" + ); + } +} + +// ── 8. Analyzer integration — rule engine wired to Analyzer ────────────────── + +#[test] +fn analyzer_run_rule_delegates_to_registry() { + let a = Analyzer::new(SanctifyConfig::default()); + + // run_rule("auth_gap") must agree with a direct scan_auth_gaps call. + let via_registry = a.run_rule(AUTH_GAP_CONTRACT, "auth_gap"); + let via_scan = a.scan_auth_gaps(AUTH_GAP_CONTRACT); + + assert_eq!( + via_registry.len(), + via_scan.len(), + "Analyzer::run_rule and scan_auth_gaps must agree on the finding count" + ); +} + +#[test] +fn analyzer_run_rule_returns_empty_for_unknown_rule_name() { + let a = Analyzer::new(SanctifyConfig::default()); + let violations = a.run_rule(AUTH_GAP_CONTRACT, "nonexistent_rule_xyz"); + assert!( + violations.is_empty(), + "unknown rule name must return an empty Vec, not panic" + ); +} + +// ── 9. Custom regex rule execution ─────────────────────────────────────────── + +#[test] +fn custom_regex_rule_fires_on_matching_pattern() { + let config = SanctifyConfig { + rules: vec![sanctifier_core::CustomRule { + name: "no_unsafe_test".to_string(), + pattern: "unsafe\\s*\\{".to_string(), + description: "No unsafe blocks".to_string(), + severity: sanctifier_core::FindingSeverity::Medium, + }], + ..Default::default() + }; + let a = Analyzer::new(config); + let source = r#" + pub fn danger() { unsafe { let _x = 1; } } + "#; + let matches = a.analyze_custom_rules(source); + assert!(!matches.is_empty(), "custom regex rule must fire for `unsafe {{}}` blocks"); + assert!(matches.iter().all(|m| m.rule_name == "no_unsafe_test")); +} + +#[test] +fn custom_regex_rule_does_not_fire_on_non_matching_source() { + let config = SanctifyConfig { + rules: vec![sanctifier_core::CustomRule { + name: "no_unsafe_test".to_string(), + pattern: "unsafe\\s*\\{".to_string(), + description: "No unsafe blocks".to_string(), + severity: sanctifier_core::FindingSeverity::Medium, + }], + ..Default::default() + }; + let a = Analyzer::new(config); + let matches = a.analyze_custom_rules(CLEAN_CONTRACT); + assert!( + matches.is_empty(), + "custom rule must not fire on clean contract" + ); +} + +// ── 10. Registry is extensible without breaking existing rules ───────────────── + +#[test] +fn registering_extra_rule_does_not_break_existing_rules() { + use sanctifier_core::rules::{Rule, RuleViolation}; + + struct NoOpRule; + impl Rule for NoOpRule { + fn name(&self) -> &str { + "no_op_test_rule" + } + fn description(&self) -> &str { + "A no-op rule for testing registry extensibility" + } + fn check(&self, _source: &str) -> Vec { + vec![] + } + fn as_any(&self) -> &dyn std::any::Any { + self + } + } + + let mut reg = RuleRegistry::with_default_rules(); + let built_in_count = reg.available_rules().len(); + reg.register(NoOpRule); + + // Extra rule is visible. + assert!(reg.available_rules().contains(&"no_op_test_rule")); + // All original rules are still present. + assert_eq!(reg.available_rules().len(), built_in_count + 1); + + // Existing rules still produce the same output. + let violations = reg.run_by_name(AUTH_GAP_CONTRACT, "auth_gap"); + assert!(!violations.is_empty()); +} + +// ── 11. E2E: complete pipeline over multiple source files ───────────────────── + +#[test] +fn end_to_end_scan_of_workspace_scale_inputs() { + let reg = registry(); + + let files = [ + ("contracts/clean.rs", CLEAN_CONTRACT), + ("contracts/vault.rs", AUTH_GAP_CONTRACT), + ("contracts/calc.rs", OVERFLOW_CONTRACT), + ("contracts/risky.rs", PANIC_CONTRACT), + ("contracts/multi.rs", MULTI_ISSUE_CONTRACT), + ]; + + let mut total_violations = 0usize; + let mut files_with_violations = 0usize; + + for (name, src) in &files { + let violations = reg.run_all(src); + if !violations.is_empty() { + files_with_violations += 1; + } + total_violations += violations.len(); + + // Every violation must reference a known rule. + let known_rules = reg.available_rules(); + for v in &violations { + assert!( + known_rules.contains(&v.rule_name.as_str()), + "file {name}: violation references unknown rule '{}'", + v.rule_name + ); + } + } + + // Clean contract should not contribute. + let clean_violations = reg.run_all(CLEAN_CONTRACT).len(); + assert_eq!(clean_violations, 0); + + // At least 3 of the 5 files must have at least one finding. + assert!( + files_with_violations >= 3, + "expected ≥3 files with violations, got {files_with_violations}" + ); + assert!( + total_violations >= 3, + "expected ≥3 total violations across all files, got {total_violations}" + ); +} + +// ── 12. Output format stability ─────────────────────────────────────────────── + +/// Verifies that the JSON-serialisable shape of `RuleViolation` remains stable. +/// Any change to the required fields must be intentional and version-bumped. +#[test] +fn rule_violation_serialises_with_required_fields() { + let reg = registry(); + let violations = reg.run_by_name(AUTH_GAP_CONTRACT, "auth_gap"); + assert!(!violations.is_empty()); + + let v = &violations[0]; + let json = serde_json::to_value(v).expect("RuleViolation must be JSON-serialisable"); + + assert!( + json.get("rule_name").is_some(), + "serialised violation missing 'rule_name'" + ); + assert!( + json.get("severity").is_some(), + "serialised violation missing 'severity'" + ); + assert!( + json.get("message").is_some(), + "serialised violation missing 'message'" + ); + assert!( + json.get("location").is_some(), + "serialised violation missing 'location'" + ); +} diff --git a/tooling/sanctifier-core/tests/smt_module_boundaries_test.rs b/tooling/sanctifier-core/tests/smt_module_boundaries_test.rs new file mode 100644 index 00000000..b04d321f --- /dev/null +++ b/tooling/sanctifier-core/tests/smt_module_boundaries_test.rs @@ -0,0 +1,348 @@ +//! Integration tests for the Z3 backend module boundaries (S011). +//! +//! These tests verify that each sub-module of `sanctifier_core::smt` exposes +//! a stable, well-typed public boundary and that cross-module interactions +//! behave correctly. They are black-box: every assertion is made through the +//! public re-exports on `sanctifier_core::smt`, never against internal symbols. +//! +//! # Running locally +//! +//! ```bash +//! cargo test --test smt_module_boundaries_test -p sanctifier-core +//! ``` + +#![cfg(feature = "smt")] + +use sanctifier_core::smt::{ + parse_invariants, prove_fixed_point_mul_div_bounds, + prove_fixed_point_mul_div_bounds_with_backend, run_smt_latency_benchmark, verify_invariants, + FixedPointMulDivSpec, FixedPointProofError, SmtBackend, SmtConfig, SmtVerifier, +}; + +// ── 1. types module: data types are constructable and serialisable ───────────── + +#[test] +fn smt_config_default_has_expected_timeout() { + let cfg = SmtConfig::default(); + assert_eq!(cfg.timeout_ms, 10_000, "default timeout must be 10 000 ms"); +} + +#[test] +fn smt_backend_enum_variants_are_distinct() { + assert_ne!(SmtBackend::Z3, SmtBackend::Cvc5); +} + +#[test] +fn fixed_point_mul_div_spec_is_constructable() { + let spec = FixedPointMulDivSpec { + function_name: "test".to_string(), + multiplicand_max: 100, + multiplier_max: 100, + divisor_min: 1, + divisor_max: 10, + result_max: None, + }; + assert_eq!(spec.function_name, "test"); + assert_eq!(spec.divisor_min, 1); +} + +// ── 2. invariants module: parse_invariants boundary ────────────────────────── + +#[test] +fn parse_invariants_returns_empty_for_no_annotations() { + let source = r#" + impl Token { + pub fn transfer(&self, amount: u64) {} + } + "#; + let specs = parse_invariants(source); + assert!( + specs.is_empty(), + "source with no #[invariant] attrs must return empty vec" + ); +} + +#[test] +fn parse_invariants_extracts_multiple_annotations_from_different_functions() { + let source = r#" + impl Vault { + #[invariant = "a + b <= u64::MAX"] + pub fn deposit(&self, a: u64, b: u64) {} + + #[invariant = "x - y >= 0"] + pub fn withdraw(&self, x: u64, y: u64) {} + } + "#; + let specs = parse_invariants(source); + assert_eq!(specs.len(), 2); + + let locations: Vec<&str> = specs.iter().map(|s| s.location.as_str()).collect(); + assert!(locations.contains(&"deposit")); + assert!(locations.contains(&"withdraw")); +} + +#[test] +fn parse_invariants_is_resilient_to_invalid_rust_source() { + let specs = parse_invariants("not valid rust {{{{"); + assert!( + specs.is_empty(), + "parse error must return empty vec, not panic" + ); +} + +// ── 3. invariants module: verify_invariants boundary ───────────────────────── + +#[test] +fn verify_invariants_returns_finding_for_addition_overflow() { + let source = r#" + impl Calc { + #[invariant = "a + b is safe"] + pub fn add(&self, a: u64, b: u64) {} + } + "#; + let findings = verify_invariants(source, &SmtConfig::default()); + assert_eq!(findings.len(), 1); + assert!( + findings[0].counterexample.is_some(), + "SAT result must include a counterexample" + ); + assert!( + !findings[0].is_timeout, + "simple query must not time out with default config" + ); +} + +#[test] +fn verify_invariants_returns_no_finding_for_non_arithmetic_invariant() { + let source = r#" + impl Token { + #[invariant = "only_admin"] + pub fn pause(&self) {} + } + "#; + let findings = verify_invariants(source, &SmtConfig::default()); + assert!( + findings.is_empty(), + "non-arithmetic invariant must produce no finding" + ); +} + +#[test] +fn verify_invariants_respects_timeout_config() { + let source = r#" + impl Vault { + #[invariant = "a + b is safe"] + pub fn credit(&self, a: u64, b: u64) {} + } + "#; + // With a 1 ms timeout the solver may or may not finish. + // Either way the invariant about timed-out findings must hold. + let findings = verify_invariants(source, &SmtConfig { timeout_ms: 1 }); + for f in &findings { + if f.is_timeout { + assert!( + f.counterexample.is_none(), + "timed-out finding must not carry a counterexample" + ); + } + } +} + +#[test] +fn verify_invariants_detects_subtraction_underflow() { + let source = r#" + impl Vault { + #[invariant = "a - b does not underflow"] + pub fn withdraw(&self, a: u64, b: u64) {} + } + "#; + let findings = verify_invariants(source, &SmtConfig::default()); + assert_eq!(findings.len(), 1); + assert!( + findings[0].counterexample.is_some(), + "underflow counterexample must be present" + ); +} + +// ── 4. backend module: SmtVerifier boundary ─────────────────────────────────── + +#[test] +fn smt_verifier_finds_u64_addition_overflow() { + let cfg = z3::Config::new(); + let ctx = z3::Context::new(&cfg); + let verifier = SmtVerifier::new(&ctx); + + let issue = verifier.verify_addition_overflow("add_fn", "add_fn:10"); + assert!( + issue.is_some(), + "unconstrained u64 addition is always overflowable — SmtVerifier must detect it" + ); + let issue = issue.unwrap(); + assert_eq!(issue.function_name, "add_fn"); + assert_eq!(issue.location, "add_fn:10"); + assert!( + issue.description.contains("overflow"), + "issue description must mention overflow" + ); +} + +// ── 5. backend module: fixed-point proof boundary ──────────────────────────── + +#[test] +fn fixed_point_proof_proves_safe_bounds() { + let spec = FixedPointMulDivSpec { + function_name: "price_calc".to_string(), + multiplicand_max: 1_000_000_000, + multiplier_max: 1_000_000_000, + divisor_min: 1, + divisor_max: 1_000_000, + result_max: Some(u128::MAX), + }; + let report = prove_fixed_point_mul_div_bounds(&spec).unwrap(); + assert!(report.proven_safe); + assert_eq!(report.backend, SmtBackend::Z3); + assert!(report.counterexample.is_none()); + assert!(!report.checked_properties.is_empty()); +} + +#[test] +fn fixed_point_proof_finds_unsafe_bounds() { + let spec = FixedPointMulDivSpec { + function_name: "overflow_calc".to_string(), + multiplicand_max: u128::MAX, + multiplier_max: 2, + divisor_min: 1, + divisor_max: 1, + result_max: None, + }; + let report = prove_fixed_point_mul_div_bounds(&spec).unwrap(); + assert!(!report.proven_safe); + let witness = report.counterexample.unwrap(); + assert!(!witness.intermediate_product.is_empty()); + assert!(!witness.multiplicand.is_empty()); +} + +#[test] +fn fixed_point_proof_rejects_zero_divisor_min() { + let spec = FixedPointMulDivSpec { + function_name: "bad_spec".to_string(), + multiplicand_max: 100, + multiplier_max: 100, + divisor_min: 0, + divisor_max: 10, + result_max: None, + }; + assert_eq!( + prove_fixed_point_mul_div_bounds(&spec).unwrap_err(), + FixedPointProofError::InvalidSpec("divisor_min must be greater than zero") + ); +} + +#[test] +fn fixed_point_proof_with_backend_rejects_cvc5() { + let spec = FixedPointMulDivSpec { + function_name: "test".to_string(), + multiplicand_max: 10, + multiplier_max: 10, + divisor_min: 1, + divisor_max: 10, + result_max: None, + }; + assert_eq!( + prove_fixed_point_mul_div_bounds_with_backend(SmtBackend::Cvc5, &spec).unwrap_err(), + FixedPointProofError::UnsupportedBackend(SmtBackend::Cvc5) + ); +} + +// ── 6. benchmark module: run_smt_latency_benchmark boundary ────────────────── + +#[test] +fn latency_benchmark_returns_one_result_per_strategy() { + let report = run_smt_latency_benchmark(3); + assert_eq!( + report.strategies.len(), + 3, + "benchmark must return exactly one result per SmtProofStrategy variant" + ); + assert_eq!(report.iterations_per_strategy, 3); +} + +#[test] +fn latency_benchmark_statistics_are_internally_consistent() { + let report = run_smt_latency_benchmark(5); + for s in &report.strategies { + assert!( + s.min_micros <= s.avg_micros, + "min must not exceed avg for {:?}", + s.strategy + ); + assert!( + s.avg_micros <= s.max_micros, + "avg must not exceed max for {:?}", + s.strategy + ); + assert_eq!(s.runs, 5); + } +} + +#[test] +fn latency_benchmark_most_expensive_first_is_sorted() { + let report = run_smt_latency_benchmark(3); + let sorted = report.most_expensive_first(); + assert_eq!(sorted.len(), 3); + for pair in sorted.windows(2) { + assert!( + pair[0].avg_micros >= pair[1].avg_micros, + "most_expensive_first must be sorted by descending avg_micros" + ); + } +} + +#[test] +fn latency_benchmark_report_is_json_serialisable() { + let report = run_smt_latency_benchmark(2); + let json = serde_json::to_string(&report) + .expect("SmtLatencyBenchmarkReport must be JSON-serialisable"); + assert!(json.contains("strategies")); + assert!(json.contains("iterations_per_strategy")); + assert!(json.contains("timestamp")); +} + +// ── 7. Cross-module: types flow correctly between invariants and backend ────── + +#[test] +fn invariant_spec_location_matches_smt_finding_location() { + let source = r#" + impl Ledger { + #[invariant = "credit + debit <= u64::MAX"] + pub fn reconcile(&self, credit: u64, debit: u64) {} + } + "#; + let specs = parse_invariants(source); + assert_eq!(specs.len(), 1); + assert_eq!(specs[0].location, "reconcile"); + + let findings = verify_invariants(source, &SmtConfig::default()); + assert_eq!(findings.len(), 1); + // The location in the SmtFinding must match what parse_invariants extracted. + assert_eq!( + findings[0].location, specs[0].location, + "SmtFinding.location must equal the InvariantSpec.location" + ); +} + +#[test] +fn smt_finding_invariant_name_matches_original_expression() { + let source = r#" + impl Token { + #[invariant = "balance + amount <= u64::MAX"] + pub fn mint(&self, amount: u64) {} + } + "#; + let findings = verify_invariants(source, &SmtConfig::default()); + assert_eq!(findings.len(), 1); + assert_eq!( + findings[0].invariant_name, "balance + amount <= u64::MAX", + "SmtFinding.invariant_name must preserve the original expression verbatim" + ); +}