Skip to content
Open
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
3 changes: 3 additions & 0 deletions .config/nextest.toml
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
[profile.ci]
# Output JUnit XML for native CI tab integration (GitHub, GitLab, CircleCI)
junit = { path = "junit.xml" }
16 changes: 13 additions & 3 deletions .github/workflows/rust.yml
Original file line number Diff line number Diff line change
Expand Up @@ -38,10 +38,20 @@ jobs:
run: cargo fmt --check

- name: Run Clippy
run: cargo clippy --workspace --all-targets --all-features -- -D warnings
run: cargo clippy -p sanctifier-cli -p sanctifier-core --all-targets --all-features -- -D warnings

- name: Run tests
run: cargo test --workspace --all-features
- name: Install cargo-nextest
uses: taiki-e/install-action@nextest

- name: Run tests (JUnit XML)
run: cargo nextest run --workspace --all-features --profile ci

- name: Upload test results
if: always()
uses: actions/upload-artifact@v4
with:
name: junit-test-results
path: target/nextest/ci/junit.xml

- name: Build release binary
run: cargo build --release -p sanctifier-cli
98 changes: 96 additions & 2 deletions Cargo.lock

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

2 changes: 1 addition & 1 deletion contracts/kani-poc/Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@ version = "0.1.0"
edition = "2021"

[dependencies]
soroban-sdk = "20.0.0"
soroban-sdk = "20.3.2"

[lints.rust]
unexpected_cfgs = { level = "warn", check-cfg = ["cfg(kani)"] }
Expand Down
18 changes: 12 additions & 6 deletions contracts/kani-poc/src/lib.rs
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,7 @@
//! logic into functions that can be verified with Kani, while the contract layer that uses
//! `Env`, `Address`, `Symbol`, etc. remains unverified due to Host type limitations.

use soroban_sdk::{contract, contractimpl, Env, Symbol, symbol_short};
use soroban_sdk::{contract, contractimpl, symbol_short, Env, Symbol};

// ── Pure logic (verified with Kani) ─────────────────────────────────────────────
//
Expand Down Expand Up @@ -44,7 +44,9 @@ pub fn burn_pure(balance: i128, amount: i128) -> Result<i128, &'static str> {
if amount <= 0 {
return Err("Burn amount must be positive");
}
balance.checked_sub(amount).ok_or("Insufficient balance to burn")
balance
.checked_sub(amount)
.ok_or("Insufficient balance to burn")
}

// ── Contract (not verified: uses Host types) ────────────────────────────────────
Expand All @@ -57,14 +59,15 @@ impl TokenContract {
/// Wrapper exposing transfer_pure for contract use.
/// A full implementation would read/write balances via env.storage().
pub fn transfer(balance_from: i128, balance_to: i128, amount: i128) -> (i128, i128) {
transfer_pure(balance_from, balance_to, amount)
.expect("transfer failed")
transfer_pure(balance_from, balance_to, amount).expect("transfer failed")
}

/// A function that interacts with Env (Host types).
/// Kani cannot verify this: Env, Symbol, and storage operations require host FFI.
pub fn set_admin(env: Env, new_admin: Symbol) {
env.storage().instance().set(&symbol_short!("admin"), &new_admin);
env.storage()
.instance()
.set(&symbol_short!("admin"), &new_admin);
}
}

Expand Down Expand Up @@ -92,7 +95,10 @@ mod verification {

assert!(new_from == balance_from - amount);
assert!(new_to == balance_to + amount);
assert!(new_from + new_to == balance_from + balance_to, "Conservation of supply");
assert!(
new_from + new_to == balance_from + balance_to,
"Conservation of supply"
);
}

#[kani::proof]
Expand Down
2 changes: 1 addition & 1 deletion contracts/vulnerable-contract/Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@ version = "0.1.0"
edition = "2021"

[dependencies]
soroban-sdk = "20.0.0"
soroban-sdk = "20.3.2"

[lib]
crate-type = ["cdylib"]
2 changes: 1 addition & 1 deletion contracts/vulnerable-contract/src/lib.rs
Original file line number Diff line number Diff line change
Expand Up @@ -16,7 +16,7 @@ impl VulnerableContract {

// ✅ Secure version
pub fn set_admin_secure(env: Env, new_admin: Symbol) {
let admin: Symbol = env
let _admin: Symbol = env
.storage()
.instance()
.get(&symbol_short!("admin"))
Expand Down
6 changes: 6 additions & 0 deletions tooling/sanctifier-cli/Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -20,3 +20,9 @@ serde = { version = "1.0", features = ["derive"] }
name = "sanctifier"
path = "src/main.rs"

[dev-dependencies]
assert_cmd = "2.0"
predicates = "3.0"
tempfile = "3.0"
regex = "1.10"

1 change: 1 addition & 0 deletions tooling/sanctifier-cli/src/branding.rs
Original file line number Diff line number Diff line change
Expand Up @@ -29,6 +29,7 @@ pub fn print_logo() {
println!();
}

#[allow(dead_code)]
pub fn print_banner(title: &str) {
println!("{}", format!("━━━ {} ━━━", title).yellow().bold());
}
Loading