feat(stealth-registry): add Kani formal verification for top 3 invariants (#108)

.github/workflows/ci.yml

@@ -152,6 +152,21 @@ jobs:
         run: git diff --exit-code
         working-directory: .
 
+  stellar-kani:
+    needs: changes
+    if: needs.changes.outputs.stellar == 'true'
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v4
+
+      - name: Setup Rust toolchain
+        uses: dtolnay/rust-toolchain@stable
+
+      - name: Verify stealth-registry invariants with Kani
+        uses: model-checking/kani-github-action@v1
+        with:
+          working-directory: stellar/stealth-registry
+
   stellar-nightly:
     if: github.event_name == 'schedule'
     runs-on: ubuntu-latest

stellar/stealth-registry/Cargo.toml

@@ -6,7 +6,7 @@ edition = "2021"
 [lib]
 crate-type = ["cdylib", "rlib"]
 
-[dependencies]
+[target.'cfg(not(kani))'.dependencies]
 soroban-sdk = { workspace = true }
 wraith-metrics = { path = "../wraith-metrics" }
 

stellar/stealth-registry/README.md

@@ -0,0 +1,29 @@
+# Stealth Registry Contract (`stealth-registry`)
+
+The `stealth-registry` contract manages the storage and resolution of stealth meta-addresses (`spending_pubkey || viewing_pubkey`) on Soroban.
+
+## Formal Verification with Kani
+
+Formal verification harnesses are located in `src/proofs/mod.rs` and can be verified using [Kani](https://model-checking.github.io/kani/).
+
+### Running Verification Locally
+
+```bash
+cargo kani --package stealth-registry
+```
+
+---
+
+## Formally Proven Invariants
+
+### 1. Register-Then-Resolve Roundtrip (`proof_register_then_resolve`)
+* **Claim**: For any valid 64-byte payload registered under a `(registrant, scheme_id)` key, resolving that key via `stealth_meta_address_of` immediately returns the exact registered payload.
+* **Non-Goals**: Does not verify the cryptographic validity or key quality of the underlying 64-byte payload (e.g., verifying secp256k1 or ed25519 point validity), nor does it verify off-chain RPC node network transport.
+
+### 2. Key Uniqueness / No Double-Registration (`proof_no_duplicate_keys`)
+* **Claim**: The persistent storage map maintains strict key uniqueness. No two active registrations in storage share the same key `(Address, u32)`. Any new registration for an existing key safely replaces the previous entry.
+* **Non-Goals**: Does not model host-level disk persistence corruption or out-of-memory errors on ledger nodes.
+
+### 3. Expiry Monotonicity (`proof_expiry_monotonicity`)
+* **Claim**: Any state-mutating operation (`register_keys`) or read operation (`stealth_meta_address_of`) that extends entry Time-To-Live (TTL) results in an expiry ledger number that is monotonically non-decreasing (`new_expiry >= old_expiry`).
+* **Non-Goals**: Does not prevent entry expiration if an entry is left unaccessed past its TTL threshold, nor does it model host ledger clock skew bugs.

stellar/stealth-registry/src/lib.rs

@@ -1,22 +1,57 @@
 #![no_std]
 
+#[cfg(kani)]
+extern crate alloc;
+
+#[cfg(not(kani))]
 use soroban_sdk::{
     contract, contracterror, contractimpl, contracttype, symbol_short, Address, Bytes, Env,
     IntoVal, Vec,
 };
+#[cfg(not(kani))]
 use wraith_metrics::{contract_ids, dimension_names, emit_metric, metric_names};
 
+#[cfg(kani)]
+pub mod mock_sdk;
+
+#[cfg(kani)]
+pub mod soroban_sdk {
+    pub use crate::mock_sdk::*;
+    pub use crate::mock_symbol_short as symbol_short;
+    pub use crate::mock_vec as vec;
+}
+
+#[cfg(kani)]
+pub mod wraith_metrics {
+    pub use crate::mock_sdk::contract_ids;
+    pub use crate::mock_sdk::dimension_names;
+    pub use crate::mock_sdk::emit_metric;
+    pub use crate::mock_sdk::metric_names;
+}
+
+#[cfg(kani)]
+#[allow(unused_imports)]
+use mock_sdk::{
+    contract_ids, dimension_names, emit_metric, metric_names, Address, Bytes, DataKey, Env, IntoVal,
+};
+#[cfg(kani)]
+use soroban_sdk::symbol_short;
+
+#[cfg(kani)]
+mod proofs;
+
 /// Storage keys.
+#[cfg(not(kani))]
 #[contracttype]
-#[derive(Clone)]
+#[derive(Clone, PartialEq, Eq)]
 pub enum DataKey {
     /// Maps (registrant, scheme_id) to their stealth meta-address (64 bytes:
     /// spending_pubkey || viewing_pubkey).
     MetaAddress(Address, u32),
 }
 
 /// Errors that the registry can produce.
-#[contracterror]
+#[cfg_attr(not(kani), contracterror)]
 #[derive(Copy, Clone, Debug, Eq, PartialEq, PartialOrd, Ord)]
 #[repr(u32)]
 pub enum RegistryError {
@@ -29,10 +64,10 @@ pub enum RegistryError {
 const TTL_THRESHOLD: u32 = 17280; // ~1 day
 const TTL_EXTEND_TO: u32 = 518400; // ~30 days
 
-#[contract]
+#[cfg_attr(not(kani), contract)]
 pub struct StealthRegistryContract;
 
-#[contractimpl]
+#[cfg_attr(not(kani), contractimpl)]
 impl StealthRegistryContract {
     /// Register or update a stealth meta-address.
     ///

stellar/stealth-registry/src/mock_sdk.rs

@@ -0,0 +1,238 @@
+#[cfg(kani)]
+extern crate alloc;
+
+use alloc::rc::Rc;
+use core::cell::RefCell;
+use core::marker::PhantomData;
+
+pub use alloc::vec::Vec;
+
+#[derive(Clone, Debug, PartialEq, Eq)]
+pub struct Address {
+    pub id: u32,
+}
+
+impl Address {
+    pub fn require_auth(&self) {
+        // Mock authorization: no-op under Kani
+    }
+}
+
+#[derive(Clone, Debug, PartialEq, Eq)]
+pub struct Bytes {
+    pub data: [u8; 64],
+    pub len: usize,
+}
+
+impl Bytes {
+    pub fn len(&self) -> u32 {
+        self.len as u32
+    }
+
+    pub fn from_slice(data: &[u8]) -> Self {
+        let mut buf = [0u8; 64];
+        let len = data.len();
+        if len <= 64 {
+            buf[..len].copy_from_slice(data);
+        }
+        Bytes { data: buf, len }
+    }
+}
+
+#[derive(Clone, Debug, PartialEq, Eq)]
+pub enum DataKey {
+    MetaAddress(Address, u32),
+}
+
+#[derive(Clone, PartialEq, Eq)]
+pub struct StorageEntry {
+    pub key: DataKey,
+    pub value: Bytes,
+    pub expiry_ledger: u32,
+}
+
+pub struct EnvState {
+    pub storage: Vec<StorageEntry>,
+    pub ledger_sequence: u32,
+}
+
+#[derive(Clone)]
+pub struct Env {
+    pub state: Rc<RefCell<EnvState>>,
+}
+
+impl Env {
+    pub fn new(ledger_sequence: u32) -> Self {
+        Env {
+            state: Rc::new(RefCell::new(EnvState {
+                storage: Vec::new(),
+                ledger_sequence,
+            })),
+        }
+    }
+
+    pub fn storage(&self) -> Storage {
+        Storage { env: self.clone() }
+    }
+
+    pub fn events(&self) -> Events {
+        Events { _env: self.clone() }
+    }
+}
+
+pub struct Storage {
+    env: Env,
+}
+
+impl Storage {
+    pub fn persistent(&self) -> PersistentStorage {
+        PersistentStorage {
+            env: self.env.clone(),
+        }
+    }
+
+    pub fn instance(&self) -> InstanceStorage {
+        InstanceStorage {
+            _env: self.env.clone(),
+        }
+    }
+}
+
+pub struct PersistentStorage {
+    env: Env,
+}
+
+impl PersistentStorage {
+    pub fn set(&self, key: &DataKey, val: &Bytes) {
+        let mut state = self.env.state.borrow_mut();
+        if let Some(entry) = state.storage.iter_mut().find(|e| &e.key == key) {
+            entry.value = val.clone();
+        } else {
+            state.storage.push(StorageEntry {
+                key: key.clone(),
+                value: val.clone(),
+                expiry_ledger: 0,
+            });
+        }
+    }
+
+    pub fn get(&self, key: &DataKey) -> Option<Bytes> {
+        let state = self.env.state.borrow();
+        state
+            .storage
+            .iter()
+            .find(|e| &e.key == key)
+            .map(|e| e.value.clone())
+    }
+
+    pub fn has(&self, key: &DataKey) -> bool {
+        let state = self.env.state.borrow();
+        state.storage.iter().any(|e| &e.key == key)
+    }
+
+    pub fn remove(&self, key: &DataKey) {
+        let mut state = self.env.state.borrow_mut();
+        state.storage.retain(|e| &e.key != key);
+    }
+
+    pub fn extend_ttl(&self, key: &DataKey, threshold: u32, extend_to: u32) {
+        let mut state = self.env.state.borrow_mut();
+        let ledger_seq = state.ledger_sequence;
+        if let Some(entry) = state.storage.iter_mut().find(|e| &e.key == key) {
+            let current_expiry = entry.expiry_ledger;
+            let threshold_expiry = ledger_seq.saturating_add(threshold);
+            if current_expiry < threshold_expiry {
+                entry.expiry_ledger = ledger_seq.saturating_add(extend_to);
+            }
+        }
+    }
+}
+
+pub struct InstanceStorage {
+    _env: Env,
+}
+
+impl InstanceStorage {
+    pub fn extend_ttl(&self, _threshold: u32, _extend_to: u32) {
+        // Mock, no-op
+    }
+}
+
+pub struct Events {
+    _env: Env,
+}
+
+impl Events {
+    pub fn publish<T, V>(&self, _topics: T, _value: V) {
+        // Mock, no-op
+    }
+}
+
+#[derive(Clone, Debug, PartialEq, Eq)]
+pub struct Symbol;
+
+#[derive(Clone, Debug, PartialEq, Eq)]
+pub struct Val;
+
+pub trait IntoVal<E, V> {
+    fn into_val(&self, env: &E) -> V;
+}
+
+impl IntoVal<Env, Val> for u32 {
+    fn into_val(&self, _env: &Env) -> Val {
+        Val
+    }
+}
+
+#[derive(Clone, Debug, PartialEq, Eq)]
+pub struct VecMock<T> {
+    _phantom: PhantomData<T>,
+}
+
+impl<T> VecMock<T> {
+    pub fn new(_env: &Env) -> Self {
+        VecMock {
+            _phantom: PhantomData,
+        }
+    }
+}
+
+#[macro_export]
+macro_rules! mock_vec {
+    ($env:expr, $($x:expr),* $(,)?) => {
+        $crate::mock_sdk::VecMock::new($env)
+    };
+}
+
+#[macro_export]
+macro_rules! mock_symbol_short {
+    ($str:expr) => {
+        $crate::mock_sdk::Symbol
+    };
+}
+
+pub mod contract_ids {
+    use super::Symbol;
+    pub const STEALTH_REGISTRY: Symbol = Symbol;
+}
+
+pub mod metric_names {
+    use super::Symbol;
+    pub const REGISTER_COUNT: Symbol = Symbol;
+    pub const REMOVE_COUNT: Symbol = Symbol;
+}
+
+pub mod dimension_names {
+    use super::Symbol;
+    pub const SCHEME_ID: Symbol = Symbol;
+}
+
+pub fn emit_metric(
+    _env: &Env,
+    _contract: Symbol,
+    _metric_name: Symbol,
+    _value: i128,
+    _dimensions: VecMock<(Symbol, Val)>,
+) {
+    // Mock, no-op
+}