Skip to content

formal-verification scoping placeholder #375

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
nayt9 wants to merge 1 commit into
base: master
Choose a base branch
from
Open

formal-verification scoping placeholder #375

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
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
73 changes: 55 additions & 18 deletions contracts/commitment_core/src/fee_tests.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -11,13 +11,47 @@

use crate::{CommitmentCoreContract, CommitmentCoreContractClient, CommitmentRules};
use soroban_sdk::{
testutils::{Address as _, AuthorizedFunction, AuthorizedInvocation},
token, Address, Env, IntoVal, String, Symbol,
contract, contractimpl,
testutils::{Address as _, Ledger},
token, Address, Env, String,
};

fn create_token_contract<'a>(e: &Env, admin: &Address) -> (Address, token::Client<'a>) {
let addr = e.register_stellar_asset_contract(admin.clone());
(addr.clone(), token::Client::new(e, &addr))
#[contract]
struct FeeMockNftContract;

#[contractimpl]
impl FeeMockNftContract {
pub fn mint(
_e: Env,
_caller: Address,
_owner: Address,
_commitment_id: String,
_duration_days: u32,
_max_loss_percent: u32,
_commitment_type: String,
_initial_amount: i128,
_asset_address: Address,
_early_exit_penalty: u32,
) -> u32 {
1
}

pub fn settle(_e: Env, _caller: Address, _token_id: u32) {}

pub fn mark_inactive(_e: Env, _caller: Address, _token_id: u32) {}
}

fn create_token_contract<'a>(
e: &Env,
admin: &Address,
) -> (Address, token::Client<'a>, token::StellarAssetClient<'a>) {
let token_contract = e.register_stellar_asset_contract_v2(admin.clone());
let addr = token_contract.address();
(
addr.clone(),
token::Client::new(e, &addr),
token::StellarAssetClient::new(e, &addr),
)
}

fn setup_test() -> (
Expand All @@ -33,12 +67,12 @@ fn setup_test() -> (
e.mock_all_auths();

let admin = Address::generate(&e);
let nft_contract = Address::generate(&e);
let nft_contract = e.register_contract(None, FeeMockNftContract);
let user = Address::generate(&e);
let (token_address, token_client) = create_token_contract(&e, &admin);
let (token_address, token_client, token_admin_client) = create_token_contract(&e, &admin);

// Mint tokens to user
token_client.mint(&user, &10_000_000);
token_admin_client.mint(&user, &10_000_000);

let contract_id = e.register_contract(None, CommitmentCoreContract);
let client = CommitmentCoreContractClient::new(&e, &contract_id);
Expand Down Expand Up @@ -221,12 +255,13 @@ fn test_early_exit_penalty_retained_as_fee() {

let expected_penalty = 100_000i128; // 10% of 1,000,000
let expected_returned = amount - expected_penalty;
let expected_user_balance = 10_000_000i128 - amount + expected_returned;

// Verify penalty was added to collected fees
assert_eq!(client.get_collected_fees(&token_address), expected_penalty);

// Verify user received net amount
assert_eq!(token_client.balance(&user), expected_returned);
assert_eq!(token_client.balance(&user), expected_user_balance);
}

#[test]
Expand All @@ -251,12 +286,13 @@ fn test_early_exit_with_creation_fee_and_penalty() {
let exit_penalty = 99_000i128; // 10% of 990,000
let expected_returned = net_amount - exit_penalty;
let total_fees = creation_fee + exit_penalty;
let expected_user_balance = 10_000_000i128 - amount + expected_returned;

// Verify both fees were collected
assert_eq!(client.get_collected_fees(&token_address), total_fees);

// Verify user received correct amount
assert_eq!(token_client.balance(&user), expected_returned);
assert_eq!(token_client.balance(&user), expected_user_balance);
}

// ============================================================================
Expand Down Expand Up @@ -442,11 +478,11 @@ fn test_get_collected_fees_multiple_assets() {
let (e, admin, _, user, _, _, client) = setup_test();

// Create two different tokens
let (token1, token1_client) = create_token_contract(&e, &admin);
let (token2, token2_client) = create_token_contract(&e, &admin);
let (token1, _token1_client, token1_admin_client) = create_token_contract(&e, &admin);
let (token2, _token2_client, token2_admin_client) = create_token_contract(&e, &admin);

token1_client.mint(&user, &10_000_000);
token2_client.mint(&user, &10_000_000);
token1_admin_client.mint(&user, &10_000_000);
token2_admin_client.mint(&user, &10_000_000);

// Set creation fee
client.set_creation_fee_bps(&admin, &100);
Expand Down Expand Up @@ -476,21 +512,22 @@ fn test_fee_collection_with_settle() {
let amount = 1_000_000i128;
let creation_fee = 10_000i128;
let net_amount = amount - creation_fee;
let expected_user_balance = 10_000_000i128 - amount + net_amount;

let mut rules = default_rules(&e);
rules.duration_days = 0; // Expires immediately
let rules = default_rules(&e);

let commitment_id = client.create_commitment(&user, &amount, &token_address, &rules);

// Settle commitment
e.ledger().with_mut(|li| li.timestamp = li.timestamp + 1);
e.ledger()
.with_mut(|li| li.timestamp = li.timestamp + (rules.duration_days as u64 * 86_400) + 1);
client.settle(&commitment_id);

// Verify creation fee still collected
assert_eq!(client.get_collected_fees(&token_address), creation_fee);

// Verify user got back net amount
assert_eq!(token_client.balance(&user), net_amount);
assert_eq!(token_client.balance(&user), expected_user_balance);
}

#[test]
Expand Down
30 changes: 15 additions & 15 deletions contracts/commitment_core/src/lib.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -11,6 +11,9 @@
//! The end-to-end review for the `commitment_core <-> commitment_nft <-> attestation_engine`
//! call graph lives in:
//! [`docs/CORE_NFT_ATTESTATION_THREAT_REVIEW.md#core-nft-attestation-call-graph`](../../../docs/CORE_NFT_ATTESTATION_THREAT_REVIEW.md#core-nft-attestation-call-graph)
//!
//! Formal verification planning placeholder:
//! [`docs/COMMITMENT_CORE_FORMAL_VERIFICATION_SCOPE.md`](../../../docs/COMMITMENT_CORE_FORMAL_VERIFICATION_SCOPE.md)

use shared_utils::{
emit_error_event, fees, EmergencyControl, Pausable, RateLimiter, SafeMath, TimeUtils,
Expand Down Expand Up @@ -383,6 +386,18 @@ impl CommitmentCoreContract {
Self::validate_rules(&e, &rules);
check_sufficient_balance(&e, &owner, &asset_address, amount);

let creation_fee_bps: u32 = e
.storage()
.instance()
.get(&DataKey::CreationFeeBps)
.unwrap_or(0);
let creation_fee = if creation_fee_bps > 0 {
fees::fee_from_bps(amount, creation_fee_bps)
} else {
0
};
let net_amount = amount - creation_fee;

let expires_at = TimeUtils::checked_calculate_expiration(&e, rules.duration_days)
.unwrap_or_else(|| { set_reentrancy_guard(&e, false); fail(&e, CommitmentError::ExpirationOverflow, "create") });

Expand Down Expand Up @@ -435,18 +450,6 @@ impl CommitmentCoreContract {
let contract_address = e.current_contract_address();
transfer_assets(&e, &owner, &contract_address, &asset_address, amount);

// Collect creation fee if configured
let creation_fee_bps: u32 = e
.storage()
.instance()
.get(&DataKey::CreationFeeBps)
.unwrap_or(0);
let creation_fee = if creation_fee_bps > 0 {
fees::fee_from_bps(amount, creation_fee_bps)
} else {
0
};

// Add creation fee to collected fees
if creation_fee > 0 {
let fee_key = DataKey::CollectedFees(asset_address.clone());
Expand All @@ -456,9 +459,6 @@ impl CommitmentCoreContract {
.set(&fee_key, &(current_fees + creation_fee));
}

// Net amount locked in commitment (after fee deduction)
let net_amount = amount - creation_fee;

let nft_token_id = call_nft_mint(
&e,
&nft_contract,
Expand Down
15 changes: 10 additions & 5 deletions contracts/commitment_core/src/test_zero_address.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,10 @@
extern crate std;

use crate::*;
use soroban_sdk::{Address, Env, String};
use soroban_sdk::{
testutils::Address as _,
Address, Env, String,
};

fn generate_zero_address(env: &Env) -> Address {
Address::from_string(&String::from_str(
Expand All @@ -27,10 +30,12 @@ fn test_create_commitment_zero_owner_fails() {

// Corrected field names for the Commitlabs CommitmentRules struct
let rules = CommitmentRules {
min_commitment_amount: 0,
max_commitment_amount: i128::MAX,
min_duration: 0,
max_duration: u64::MAX,
duration_days: 30,
max_loss_percent: 10,
commitment_type: String::from_str(&env, "safe"),
early_exit_penalty: 15,
min_fee_threshold: 0,
grace_period_days: 0,
};

client.create_commitment(&zero_owner, &amount, &asset_address, &rules);
Expand Down
12 changes: 10 additions & 2 deletions contracts/commitment_core/src/tests.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -587,9 +587,13 @@ fn test_create_commitment_expiration_overflow() {

let contract_id = e.register_contract(None, CommitmentCoreContract);
let admin = Address::generate(&e);
let nft_contract = Address::generate(&e);
let nft_contract = e.register_contract(None, MockNftContract);
let owner = Address::generate(&e);
let asset_address = Address::generate(&e);
let token_admin = Address::generate(&e);
let token_contract = e.register_stellar_asset_contract_v2(token_admin);
let asset_address = token_contract.address();
let token_admin_client = StellarAssetClient::new(&e, &asset_address);
token_admin_client.mint(&owner, &1000);

e.as_contract(&contract_id, || {
CommitmentCoreContract::initialize(e.clone(), admin.clone(), nft_contract.clone());
Expand Down Expand Up @@ -1756,6 +1760,7 @@ fn test_allocate_when_settled_fails() {
e.as_contract(&contract_id, || {
CommitmentCoreContract::allocate(
e.clone(),
admin.clone(),
String::from_str(&e, commitment_id),
target_pool.clone(),
100,
Expand Down Expand Up @@ -1788,6 +1793,7 @@ fn test_allocate_when_violated_fails() {
e.as_contract(&contract_id, || {
CommitmentCoreContract::allocate(
e.clone(),
admin.clone(),
String::from_str(&e, commitment_id),
target_pool.clone(),
100,
Expand Down Expand Up @@ -1820,6 +1826,7 @@ fn test_allocate_when_early_exit_fails() {
e.as_contract(&contract_id, || {
CommitmentCoreContract::allocate(
e.clone(),
admin.clone(),
String::from_str(&e, commitment_id),
target_pool.clone(),
100,
Expand Down Expand Up @@ -1858,6 +1865,7 @@ fn test_allocate_when_active_succeeds() {
store_commitment(&e, &contract_id, &commitment);

client.allocate(
&admin,
&String::from_str(&e, commitment_id),
&target_pool,
&allocation_amount,
Expand Down
Loading