Extract consensus module into standalone vero-consensus crate

.github/workflows/ci.yml

@@ -49,9 +49,9 @@ jobs:
       - name: Publish coverage summary
         run: |
           LF=$(awk -F: '/^LF:/{s+=$2} END{print s+0}' coverage/lcov.info)
-          LH=$(awk -F: '/^LH:/{s+=$2} END{print s+0}')
-          BRF=$(awk -F: '/^BRF:/{s+=$2} END{print s+0}')
-          BRH=$(awk -F: '/^BRH:/{s+=$2} END{print s+0}')
+          LH=$(awk -F: '/^LH:/{s+=$2} END{print s+0}' coverage/lcov.info)
+          BRF=$(awk -F: '/^BRF:/{s+=$2} END{print s+0}' coverage/lcov.info)
+          BRH=$(awk -F: '/^BRH:/{s+=$2} END{print s+0}' coverage/lcov.info)
           PCT=$(awk -v a="$LH" -v b="$LF" 'BEGIN { if (b>0) printf "%.1f%%", 100*a/b; else printf "n/a" }')
           {
             echo "## Test coverage"

Cargo.toml

@@ -1,5 +1,5 @@
 [workspace]
-members = [".", "verification"]
+members = [".", "consensus", "verification"]
 
 [package]
 name = "vero-core-contracts"
@@ -12,6 +12,7 @@ crate-type = ["cdylib", "rlib"]
 
 [dependencies]
 soroban-sdk = { version = "21.0.0", features = ["alloc"] }
+vero-consensus = { path = "consensus", version = "0.1.0" }
 
 [dev-dependencies]
 soroban-sdk = { version = "21.0.0", features = ["testutils"] }

consensus/Cargo.toml

@@ -0,0 +1,12 @@
+[package]
+name = "vero-consensus"
+version = "0.1.0"
+edition = "2021"
+publish = false
+license = "MIT"
+description = "Pure, no_std-compatible consensus logic for the Vero protocol — no Soroban host dependency."
+
+# No external dependencies: this crate is intentionally minimal so that
+# Kani and other model checkers can consume it without mocking the Soroban
+# host environment.
+[dependencies]

consensus/src/lib.rs

@@ -0,0 +1,129 @@
+//! Pure, `no_std`-compatible consensus logic — **no Soroban `Env` dependency**.
+//!
+//! This crate contains the arithmetic and state-transition rules for the
+//! weighted guardian consensus. Keeping this logic free of SDK types allows
+//! Kani (and other model checkers) to formally verify it without mocking the
+//! Soroban host environment.
+//!
+//! The contract's `vote()` entry point delegates to [`apply_vote`] after
+//! performing all authentication, authorisation, and storage I/O.
+//!
+//! ## Test placement
+//!
+//! Unlike the rest of the contract crate, this module's unit tests are **not**
+//! inline — they live in `tests/consensus.rs` in the main contract crate, in
+//! keeping with the crate-wide convention of placing all tests under `tests/`.
+//! The tests there are deliberately Soroban-free (no `Env`, no `testutils`) for
+//! the same reason this crate is: so that Kani and other model checkers can
+//! consume them without a host-environment mock. Complementary coverage is
+//! provided by the Kani harnesses in `verification/` and the runtime invariant
+//! checks in `tests/safety_invariants.rs`.
+
+#![no_std]
+
+/// Errors that can arise purely from consensus arithmetic.
+#[derive(Clone, Copy, Debug, PartialEq, Eq)]
+pub enum ConsensusError {
+    /// Adding the guardian's weight to the accumulated total would overflow `u64`.
+    WeightOverflow,
+    /// The guardian's voting weight is zero — their vote has no effect.
+    ZeroWeight,
+}
+
+/// The mutable consensus state for a single task.
+///
+/// This is a plain data struct with no Soroban types so that Kani can create
+/// symbolic instances of it and exhaustively verify all reachable states.
+#[derive(Clone, Copy, Debug, PartialEq, Eq)]
+pub struct ConsensusState {
+    /// Cumulative reputation weight accrued from all guardian votes so far.
+    pub total_weight_accrued: u64,
+    /// Number of guardian votes cast (saturating counter).
+    pub votes: u32,
+    /// `true` once the task has been resolved (monotonically set).
+    pub is_done: bool,
+}
+
+impl ConsensusState {
+    /// Creates a fresh, unresolved consensus state.
+    pub const fn new() -> Self {
+        Self {
+            total_weight_accrued: 0,
+            votes: 0,
+            is_done: false,
+        }
+    }
+}
+
+impl Default for ConsensusState {
+    fn default() -> Self {
+        Self::new()
+    }
+}
+
+/// Applies a single guardian vote to the consensus state.
+///
+/// # Arguments
+/// * `state`     — mutable reference to the current task consensus state.
+/// * `weight`    — the guardian's voting power (their reputation score).
+/// * `threshold` — cumulative weight required to resolve the task.
+///
+/// # Behaviour
+/// 1. Rejects zero-weight votes.
+/// 2. Safely accumulates `weight` into `total_weight_accrued` via checked
+///    addition, returning `Err(ConsensusError::WeightOverflow)` on overflow.
+/// 3. Increments the vote counter with **saturating** arithmetic (never wraps).
+/// 4. Sets `is_done = true` **if and only if** `total_weight_accrued >= threshold`
+///    after the addition. `is_done` is never cleared once set.
+///
+/// # Invariants (proved by Kani harnesses in `verification/`)
+/// * Resolution ↔ `total_weight_accrued >= threshold`
+/// * No execution path sets `is_done` without meeting `threshold`
+/// * `is_done` is monotonically set (never unset)
+/// * `checked_add` prevents silent overflow
+/// * `votes` saturates at `u32::MAX`
+pub fn apply_vote(
+    state: &mut ConsensusState,
+    weight: u64,
+    threshold: u64,
+) -> Result<(), ConsensusError> {
+    if weight == 0 {
+        return Err(ConsensusError::ZeroWeight);
+    }
+
+    // Overflow-safe accumulation — the only arithmetic that matters for consensus.
+    state.total_weight_accrued = state
+        .total_weight_accrued
+        .checked_add(weight)
+        .ok_or(ConsensusError::WeightOverflow)?;
+
+    // Saturating vote count — purely informational, never drives resolution.
+    state.votes = state.votes.saturating_add(1);
+
+    // Threshold check: set is_done iff threshold is met.
+    // is_done is never cleared — once true it stays true.
+    if state.total_weight_accrued >= threshold {
+        state.is_done = true;
+    }
+
+    Ok(())
+}
+
+/// Returns `true` if the consensus state satisfies the resolution invariant:
+/// `is_done` must be `true` **if and only if** `total_weight_accrued >= threshold`.
+///
+/// Used both in runtime assertions and in Kani harnesses as a post-condition.
+pub fn resolution_invariant_holds(state: &ConsensusState, threshold: u64) -> bool {
+    let weight_meets_threshold = state.total_weight_accrued >= threshold;
+    // is_done must imply threshold met, AND threshold met must imply is_done
+    // (for a freshly-voted state — NOT for older states where votes may have
+    //  already set is_done and threshold was later lowered by admin).
+    //
+    // The minimal safety invariant (no resolution below threshold) is:
+    //   is_done == true  →  weight_meets_threshold
+    if state.is_done {
+        weight_meets_threshold
+    } else {
+        true // Not done yet is always safe regardless of weight
+    }
+}

src/consensus.rs

@@ -1,127 +1,8 @@
-//! Pure, `no_std`-compatible consensus logic — **no Soroban `Env` dependency**.
-//!
-//! This module contains the arithmetic and state-transition rules for the
-//! weighted guardian consensus. Keeping this logic free of SDK types allows
-//! Kani (and other model checkers) to formally verify it without mocking the
-//! Soroban host environment.
-//!
-//! The contract's `vote()` entry point delegates to [`apply_vote`] after
-//! performing all authentication, authorisation, and storage I/O.
-//!
-//! ## Test placement
-//!
-//! Unlike the rest of the crate, this module's unit tests are **not** inline
-//! — they live in `tests/consensus.rs` in keeping with the crate-wide
-//! convention of placing all tests under `tests/`.  The tests there are
-//! deliberately Soroban-free (no `Env`, no `testutils`) for the same reason
-//! this module is: so that Kani and other model checkers can consume them
-//! without a host-environment mock.  Complementary coverage is provided by
-//! the Kani harnesses in `verification/` and the runtime invariant checks in
-//! `tests/safety_invariants.rs`.
-
-/// Errors that can arise purely from consensus arithmetic.
-#[derive(Clone, Copy, Debug, PartialEq, Eq)]
-pub enum ConsensusError {
-    /// Adding the guardian's weight to the accumulated total would overflow `u64`.
-    WeightOverflow,
-    /// The guardian's voting weight is zero — their vote has no effect.
-    ZeroWeight,
-}
-
-/// The mutable consensus state for a single task.
-///
-/// This is a plain data struct with no Soroban types so that Kani can create
-/// symbolic instances of it and exhaustively verify all reachable states.
-#[derive(Clone, Copy, Debug, PartialEq, Eq)]
-pub struct ConsensusState {
-    /// Cumulative reputation weight accrued from all guardian votes so far.
-    pub total_weight_accrued: u64,
-    /// Number of guardian votes cast (saturating counter).
-    pub votes: u32,
-    /// `true` once the task has been resolved (monotonically set).
-    pub is_done: bool,
-}
-
-impl ConsensusState {
-    /// Creates a fresh, unresolved consensus state.
-    pub const fn new() -> Self {
-        Self {
-            total_weight_accrued: 0,
-            votes: 0,
-            is_done: false,
-        }
-    }
-}
-
-impl Default for ConsensusState {
-    fn default() -> Self {
-        Self::new()
-    }
-}
-
-/// Applies a single guardian vote to the consensus state.
-///
-/// # Arguments
-/// * `state`     — mutable reference to the current task consensus state.
-/// * `weight`    — the guardian's voting power (their reputation score).
-/// * `threshold` — cumulative weight required to resolve the task.
-///
-/// # Behaviour
-/// 1. Rejects zero-weight votes.
-/// 2. Safely accumulates `weight` into `total_weight_accrued` via checked
-///    addition, returning `Err(ConsensusError::WeightOverflow)` on overflow.
-/// 3. Increments the vote counter with **saturating** arithmetic (never wraps).
-/// 4. Sets `is_done = true` **if and only if** `total_weight_accrued >= threshold`
-///    after the addition. `is_done` is never cleared once set.
-///
-/// # Invariants (proved by Kani harnesses in `verification/`)
-/// * Resolution ↔ `total_weight_accrued >= threshold`
-/// * No execution path sets `is_done` without meeting `threshold`
-/// * `is_done` is monotonically set (never unset)
-/// * `checked_add` prevents silent overflow
-/// * `votes` saturates at `u32::MAX`
-pub fn apply_vote(
-    state: &mut ConsensusState,
-    weight: u64,
-    threshold: u64,
-) -> Result<(), ConsensusError> {
-    if weight == 0 {
-        return Err(ConsensusError::ZeroWeight);
-    }
-
-    // Overflow-safe accumulation — the only arithmetic that matters for consensus.
-    state.total_weight_accrued = state
-        .total_weight_accrued
-        .checked_add(weight)
-        .ok_or(ConsensusError::WeightOverflow)?;
-
-    // Saturating vote count — purely informational, never drives resolution.
-    state.votes = state.votes.saturating_add(1);
-
-    // Threshold check: set is_done iff threshold is met.
-    // is_done is never cleared — once true it stays true.
-    if state.total_weight_accrued >= threshold {
-        state.is_done = true;
-    }
-
-    Ok(())
-}
-
-/// Returns `true` if the consensus state satisfies the resolution invariant:
-/// `is_done` must be `true` **if and only if** `total_weight_accrued >= threshold`.
-///
-/// Used both in runtime assertions and in Kani harnesses as a post-condition.
-pub fn resolution_invariant_holds(state: &ConsensusState, threshold: u64) -> bool {
-    let weight_meets_threshold = state.total_weight_accrued >= threshold;
-    // is_done must imply threshold met, AND threshold met must imply is_done
-    // (for a freshly-voted state — NOT for older states where votes may have
-    //  already set is_done and threshold was later lowered by admin).
-    //
-    // The minimal safety invariant (no resolution below threshold) is:
-    //   is_done == true  →  weight_meets_threshold
-    if state.is_done {
-        weight_meets_threshold
-    } else {
-        true // Not done yet is always safe regardless of weight
-    }
-}
+//! Re-export of the `vero-consensus` crate.
+//!
+//! The consensus logic has been extracted into its own crate so that the
+//! formal verification harnesses in `verification/` can depend on it
+//! directly — without pulling in `soroban-sdk` or any other host-dependent
+//! code. This shim re-exports all public items so the rest of the contract
+//! crate continues to use `crate::consensus::*` paths unchanged.
+pub use vero_consensus::{apply_vote, resolution_invariant_holds, ConsensusError, ConsensusState};

src/contracts/storage_layout.rs

@@ -1,3 +1,8 @@
+// The `contracttype` macro generates associated functions that cannot carry
+// doc comments; suppress the lint at file scope so those generated items
+// don't break -D clippy::all.
+#![allow(missing_docs)]
+
 use soroban_sdk::{contracttype, Address};
 
 use crate::types::Role;
@@ -10,7 +15,6 @@ use crate::types::Role;
 ///
 /// Each enum variant namespaces a distinct domain of contract state to guarantee
 /// key uniqueness and prevent collisions across storage reads/writes.
-#[allow(missing_docs)]
 #[contracttype]
 #[derive(Clone, PartialEq, Eq)]
 pub enum DataKey {

src/migrate.rs

@@ -240,7 +240,6 @@ pub fn migrate(env: &Env) -> Result<(), ContractError> {
 #[cfg(test)]
 mod tests {
     use super::*;
-    use soroban_sdk::testutils::Address as _;
 
     // Synthetic failing migration for future v1 -> v2 authors.
     //
@@ -249,6 +248,7 @@ mod tests {
     // validation that real migrations use, and returns the validation error
     // WITHOUT committing. It is compiled only for unit-test builds and is
     // excluded from production builds via `#[cfg(test)]`.
+    #[allow(dead_code)]
     fn synthetic_failing_v1_to_v2(env: &Env) -> Result<(), ContractError> {
         let mut cache = MigrationCache::new(env);
 

src/storage.rs

@@ -1,6 +1,8 @@
 use crate::types::{ContractError, DataKey, Task};
 use soroban_sdk::{Address, Env, Vec};
 
+/// Minimum age (in seconds) a resolved task must reach before it can be archived.
+/// Equivalent to 30 days.
 pub const ARCHIVE_AFTER_SECONDS: u64 = 30 * 24 * 60 * 60;
 
 pub fn active_task_key(task_id: u64) -> DataKey {

tests/upgrade.rs

@@ -44,6 +44,7 @@ fn generate_signers(env: &Env, n: u32) -> Vec<Address> {
 }
 
 /// Helper to collect all events into a vector of event symbols for assertion.
+#[allow(dead_code)]
 fn event_symbols(env: &Env) -> Vec<soroban_sdk::Symbol> {
     let mut symbols = Vec::new(env);
     for e in env.events().all().iter() {
@@ -400,7 +401,7 @@ fn test_propose_same_hash_adds_approval() {
     // Signer 2 also proposes with same hash — acts as approval
     let signer2 = signers.get(1).unwrap();
     let result = client.try_propose_upgrade(&signer2, &wasm_hash);
-    result.unwrap();
+    let _ = result.unwrap();
 
     // Signer 3 approves via approve_upgrade
     let signer3 = signers.get(2).unwrap();