tests(cargo-kani): add solana agent escrow example

Author: kamiyo-ai

tests/cargo-kani/solana-agent-escrow/Cargo.toml

@@ -0,0 +1,7 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+
+[package]
+name = "solana-agent-escrow"
+version = "0.1.0"
+edition = "2018"

tests/cargo-kani/solana-agent-escrow/README.md

@@ -0,0 +1,22 @@
+# Solana Agent Escrow Example
+
+This is a self-contained example that models a few safety-critical rules common in
+Solana-style agent payment flows:
+
+- **Timelock authorization**: only the agent can release funds before expiry; the API
+  can release only after expiry.
+- **Value conservation**: settlement splits always conserve value (refund + payment == amount).
+- **Oracle tiering**: required oracle count is tiered by value-at-risk and is monotonic.
+- **Escrow FSM**: only legal state transitions are possible.
+
+The model is intentionally minimal (no Solana runtime / Anchor modeling) and exists
+primarily to demonstrate Kani verification on agent-style programs.
+
+## Run
+
+```bash
+cargo kani --harness timelock_policy_matches_release_rule
+cargo kani --harness settlement_splits_conserve_value
+cargo kani --harness required_oracle_count_is_monotonic_and_bounded
+cargo kani --harness escrow_fsm_actions_respect_transition_table
+```

tests/cargo-kani/solana-agent-escrow/escrow_fsm_actions_respect_transition_table.expected

@@ -0,0 +1 @@
+VERIFICATION:- SUCCESSFUL

tests/cargo-kani/solana-agent-escrow/required_oracle_count_is_monotonic_and_bounded.expected

@@ -0,0 +1 @@
+VERIFICATION:- SUCCESSFUL

tests/cargo-kani/solana-agent-escrow/settlement_splits_conserve_value.expected

@@ -0,0 +1 @@
+VERIFICATION:- SUCCESSFUL

tests/cargo-kani/solana-agent-escrow/src/escrow.rs

@@ -0,0 +1,41 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+pub type Key = [u8; 32];
+
+pub fn can_release_funds(caller: Key, agent: Key, api: Key, now: i64, expires_at: i64) -> bool {
+    let is_agent = caller == agent;
+    let is_api = caller == api;
+    let time_lock_expired = now >= expires_at;
+
+    is_agent || (is_api && time_lock_expired)
+}
+
+pub fn dispute_settlement(amount: u64, refund_percentage: u8) -> (u64, u64) {
+    let refund_amount = (amount as u128 * refund_percentage as u128 / 100) as u64;
+    let payment_amount = amount - refund_amount;
+    (refund_amount, payment_amount)
+}
+
+pub fn inference_settlement(amount: u64, quality_threshold: u8, quality_score: u8) -> (u64, u64) {
+    if quality_score >= quality_threshold {
+        return (0, amount);
+    }
+
+    if quality_score >= 50 {
+        let provider_share = (amount as u128 * quality_score as u128 / 100) as u64;
+        let user_refund = amount - provider_share;
+        return (user_refund, provider_share);
+    }
+
+    (amount, 0)
+}
+
+pub fn expired_escrow_settlement(amount: u64, was_disputed: bool) -> (u64, u64) {
+    if !was_disputed {
+        return (amount, 0);
+    }
+
+    let half = amount / 2;
+    (half, amount - half)
+}

tests/cargo-kani/solana-agent-escrow/src/fsm.rs

@@ -0,0 +1,48 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+#[derive(Clone, Copy, Debug, PartialEq, Eq)]
+pub enum EscrowState {
+    Active,
+    Disputed,
+    Released,
+    Resolved,
+}
+
+#[derive(Clone, Copy, Debug, PartialEq, Eq)]
+pub enum EscrowAction {
+    Release,
+    MarkDisputed,
+    Resolve,
+    ClaimExpired,
+}
+
+pub fn is_terminal(state: EscrowState) -> bool {
+    matches!(state, EscrowState::Released | EscrowState::Resolved)
+}
+
+pub fn valid_transition(from: EscrowState, to: EscrowState) -> bool {
+    matches!(
+        (from, to),
+        (EscrowState::Active, EscrowState::Disputed)
+            | (EscrowState::Active, EscrowState::Released)
+            | (EscrowState::Active, EscrowState::Resolved)
+            | (EscrowState::Disputed, EscrowState::Resolved)
+    )
+}
+
+pub fn step(state: EscrowState, action: EscrowAction) -> Option<EscrowState> {
+    if is_terminal(state) {
+        return None;
+    }
+
+    match (state, action) {
+        (EscrowState::Active, EscrowAction::Release) => Some(EscrowState::Released),
+        (EscrowState::Active, EscrowAction::MarkDisputed) => Some(EscrowState::Disputed),
+        (EscrowState::Active, EscrowAction::Resolve) => Some(EscrowState::Resolved),
+        (EscrowState::Active, EscrowAction::ClaimExpired) => Some(EscrowState::Resolved),
+        (EscrowState::Disputed, EscrowAction::Resolve) => Some(EscrowState::Resolved),
+        (EscrowState::Disputed, EscrowAction::ClaimExpired) => Some(EscrowState::Resolved),
+        _ => None,
+    }
+}

tests/cargo-kani/solana-agent-escrow/src/lib.rs

@@ -0,0 +1,9 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+pub mod escrow;
+pub mod fsm;
+pub mod oracle;
+
+#[cfg(kani)]
+mod proofs;

tests/cargo-kani/solana-agent-escrow/src/oracle.rs

@@ -0,0 +1,16 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+pub const MIN_ORACLES: u8 = 3;
+pub const TIER2_ESCROW_THRESHOLD: u64 = 10;
+pub const TIER3_ESCROW_THRESHOLD: u64 = 100;
+
+pub fn required_oracle_count(escrow_amount: u64) -> u8 {
+    if escrow_amount >= TIER3_ESCROW_THRESHOLD {
+        5
+    } else if escrow_amount >= TIER2_ESCROW_THRESHOLD {
+        4
+    } else {
+        MIN_ORACLES
+    }
+}

tests/cargo-kani/solana-agent-escrow/src/proofs.rs

@@ -0,0 +1,132 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+use crate::escrow::*;
+use crate::fsm::*;
+use crate::oracle::*;
+
+#[kani::proof]
+fn timelock_policy_matches_release_rule() {
+    let caller: Key = kani::any();
+    let agent: Key = kani::any();
+    let api: Key = kani::any();
+    let now: i64 = kani::any();
+    let expires_at: i64 = kani::any();
+
+    let allowed = can_release_funds(caller, agent, api, now, expires_at);
+
+    if now < expires_at {
+        kani::assert(
+            !allowed || caller == agent,
+            "only agent can release before expiry",
+        );
+    } else {
+        kani::assert(
+            !allowed || (caller == agent || caller == api),
+            "only agent/api can release after expiry",
+        );
+    }
+}
+
+#[kani::proof]
+fn settlement_splits_conserve_value() {
+    let amount: u64 = kani::any::<u32>() as u64;
+
+    let refund_percentage: u8 = kani::any();
+    kani::assume(refund_percentage <= 100);
+
+    let (refund, payment) = dispute_settlement(amount, refund_percentage);
+    kani::assert(
+        refund as u128 + payment as u128 == amount as u128,
+        "dispute settlement must conserve value",
+    );
+
+    let quality_threshold: u8 = kani::any();
+    let quality_score: u8 = kani::any();
+    kani::assume(quality_threshold <= 100);
+    kani::assume(quality_score <= 100);
+
+    let (user_refund, provider_payment) =
+        inference_settlement(amount, quality_threshold, quality_score);
+    kani::assert(
+        user_refund as u128 + provider_payment as u128 == amount as u128,
+        "inference settlement must conserve value",
+    );
+
+    let was_disputed: bool = kani::any();
+    let (agent_amount, api_amount) = expired_escrow_settlement(amount, was_disputed);
+    kani::assert(
+        agent_amount as u128 + api_amount as u128 == amount as u128,
+        "expired escrow claim must conserve value",
+    );
+}
+
+#[kani::proof]
+fn required_oracle_count_is_monotonic_and_bounded() {
+    let amount: u64 = kani::any();
+    let r = required_oracle_count(amount);
+    kani::assert(
+        r == MIN_ORACLES || r == 4 || r == 5,
+        "required oracle count must be in {3,4,5}",
+    );
+
+    let a1: u64 = kani::any();
+    let a2: u64 = kani::any();
+    kani::assume(a1 <= a2);
+
+    let r1 = required_oracle_count(a1);
+    let r2 = required_oracle_count(a2);
+    kani::assert(r1 <= r2, "oracle requirement must be monotonic");
+
+    kani::assert(
+        required_oracle_count(TIER2_ESCROW_THRESHOLD - 1) == MIN_ORACLES,
+        "below tier2 threshold must use minimum",
+    );
+    kani::assert(
+        required_oracle_count(TIER2_ESCROW_THRESHOLD) == 4,
+        "tier2 threshold must require 4 oracles",
+    );
+    kani::assert(
+        required_oracle_count(TIER3_ESCROW_THRESHOLD - 1) == 4,
+        "just below tier3 threshold must still be tier2",
+    );
+    kani::assert(
+        required_oracle_count(TIER3_ESCROW_THRESHOLD) == 5,
+        "tier3 threshold must require 5 oracles",
+    );
+}
+
+fn any_state() -> EscrowState {
+    match kani::any::<u8>() % 4 {
+        0 => EscrowState::Active,
+        1 => EscrowState::Disputed,
+        2 => EscrowState::Released,
+        _ => EscrowState::Resolved,
+    }
+}
+
+fn any_action() -> EscrowAction {
+    match kani::any::<u8>() % 4 {
+        0 => EscrowAction::Release,
+        1 => EscrowAction::MarkDisputed,
+        2 => EscrowAction::Resolve,
+        _ => EscrowAction::ClaimExpired,
+    }
+}
+
+#[kani::proof]
+fn escrow_fsm_actions_respect_transition_table() {
+    let state = any_state();
+    let action = any_action();
+
+    let next = step(state, action);
+
+    if is_terminal(state) {
+        kani::assert(next.is_none(), "terminal states must not transition");
+        return;
+    }
+
+    if let Some(s2) = next {
+        kani::assert(valid_transition(state, s2), "transition must be valid");
+    }
+}