From e4289b144b65c8b24362f4f6d04da50a186be543 Mon Sep 17 00:00:00 2001 From: Dmitriy Vasilev Date: Thu, 30 Apr 2026 06:55:02 +0700 Subject: [PATCH] =?UTF-8?q?feat(tri27):=20token=20system=20specs=20?= =?UTF-8?q?=E2=80=94=20types,=20staking,=20rewards,=20CLI,=20FFI=20(Closes?= =?UTF-8?q?=20#441,=20Closes=20#442,=20Closes=20#443,=20Closes=20#444,=20C?= =?UTF-8?q?loses=20#445,=20Closes=20#446,=20Closes=20#447)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit - token_types.tri: TokenAccount, TokenStake, Coptic register mapping t18-t20 - token_ffi.tri: FFI bridge for external runtime integration - staking.tri: StakePosition, StakePool, phi-aligned emission rate - reward_distribution.tri: 60/30/10 split, epoch-based distribution - token_cli.tri: balance/transfer/approve/allowance/supply commands - staking_cli.tri: stake/unstake/positions/rewards/pool commands - claim_cli.tri: claim/history/estimate commands --- specs/tri27/claim_cli.tri | 61 ++++++++ specs/tri27/reward_distribution.tri | 121 ++++++++++++++++ specs/tri27/staking.tri | 144 +++++++++++++++++++ specs/tri27/staking_cli.tri | 63 +++++++++ specs/tri27/token_cli.tri | 67 +++++++++ specs/tri27/token_ffi.tri | 85 +++++++++++ specs/tri27/token_types.tri | 211 ++++++++++++++++++++++++++++ 7 files changed, 752 insertions(+) create mode 100644 specs/tri27/claim_cli.tri create mode 100644 specs/tri27/reward_distribution.tri create mode 100644 specs/tri27/staking.tri create mode 100644 specs/tri27/staking_cli.tri create mode 100644 specs/tri27/token_cli.tri create mode 100644 specs/tri27/token_ffi.tri create mode 100644 specs/tri27/token_types.tri diff --git a/specs/tri27/claim_cli.tri b/specs/tri27/claim_cli.tri new file mode 100644 index 0000000000..72e688c2bd --- /dev/null +++ b/specs/tri27/claim_cli.tri @@ -0,0 +1,61 @@ +# TRI-27 Claim Commands — Source of Truth +# Issue: #447 +# phi^2 + 1/phi^2 = 3 | TRINITY + +name: claim_cli +version: "1.0.0" +module: tri27.cli.claim +description: "CLI commands for TRI-27 reward claiming" + +commands: + claim: + description: "Claim accumulated staking rewards" + usage: "tri27 claim [--all]" + params: + - name: all + type: bool + default: false + description: "Claim from all positions" + returns: u128 + + claim_history: + description: "Show claim history" + usage: "tri27 claim history [--limit N]" + params: + - name: limit + type: u32 + default: 10 + returns: "[]ClaimRecord" + + claim_estimate: + description: "Estimate future rewards" + usage: "tri27 claim estimate [--hours N]" + params: + - name: hours + type: u32 + default: 24 + returns: u128 + +types: + ClaimRecord: + description: "Past claim record" + fields: + - name: amount + type: u128 + - name: timestamp + type: i64 + - name: epoch_id + type: u64 + +tests: + test_claim_returns_amount: + assertions: + - "claim() returns claimed amount > 0 if rewards pending" + + test_claim_resets_pending: + assertions: + - "claim() sets pending_rewards to 0" + + test_claim_history_ordered: + assertions: + - "claim_history() returns records newest-first" diff --git a/specs/tri27/reward_distribution.tri b/specs/tri27/reward_distribution.tri new file mode 100644 index 0000000000..23972e478b --- /dev/null +++ b/specs/tri27/reward_distribution.tri @@ -0,0 +1,121 @@ +# TRI-27 Reward Distribution — Source of Truth +# Issue: #444 +# phi^2 + 1/phi^2 = 3 | TRINITY + +name: reward_distribution +version: "1.0.0" +module: tri27.reward +description: "Reward distribution system for TRI-27 stakers" + +types: + RewardConfig: + description: "Reward distribution parameters" + fields: + - name: emission_rate + type: u128 + description: "Tokens emitted per second" + - name: treasury_share_bps + type: u16 + description: "Treasury share in basis points" + - name: staker_share_bps + type: u16 + description: "Staker share in basis points" + - name: team_share_bps + type: u16 + description: "Team share in basis points" + + RewardEpoch: + description: "A reward distribution epoch" + fields: + - name: epoch_id + type: u64 + description: "Sequential epoch number" + - name: start_time + type: i64 + description: "Epoch start timestamp" + - name: end_time + type: i64 + description: "Epoch end timestamp" + - name: total_rewards + type: u128 + description: "Total rewards distributed" + - name: staker_count + type: u32 + description: "Number of stakers receiving rewards" + +constants: + DISTRIBUTION_INTERVAL: + type: i64 + value: 86400 + description: "Daily reward distribution" + + TREASURY_BPS: + type: u16 + value: 3000 + description: "30% to treasury" + + STAKER_BPS: + type: u16 + value: 6000 + description: "60% to stakers" + + TEAM_BPS: + type: u16 + value: 1000 + description: "10% to team" + + TOTAL_BPS: + type: u16 + value: 10000 + description: "Must sum to 100%" + +functions: + distribute_epoch: + description: "Distribute rewards for an epoch" + params: + - name: epoch_id + type: u64 + returns: RewardEpoch + + calculate_staker_reward: + description: "Calculate individual staker reward" + params: + - name: staker + type: "[32]u8" + - name: epoch_id + type: u64 + returns: u128 + + get_reward_history: + description: "Get reward history for staker" + params: + - name: staker + type: "[32]u8" + - name: limit + type: u32 + returns: "[]RewardEpoch" + +tests: + test_shares_sum_to_100: + description: "Distribution shares sum to 100%" + assertions: + - "TREASURY_BPS + STAKER_BPS + TEAM_BPS == TOTAL_BPS" + + test_staker_reward_proportional: + description: "Staker reward proportional to stake" + assertions: + - "stake(A) > stake(B) implies reward(A) > reward(B)" + + test_epoch_distributes_total: + description: "Epoch distributes full allocation" + assertions: + - "sum(epoch rewards) == total_rewards" + +invariants: + shares_sum_to_10000: + description: "Distribution shares always sum to 100%" + expression: "TREASURY_BPS + STAKER_BPS + TEAM_BPS == 10000" + + no_negative_rewards: + description: "Rewards are never negative" + expression: "forall e: RewardEpoch :: e.total_rewards >= 0" diff --git a/specs/tri27/staking.tri b/specs/tri27/staking.tri new file mode 100644 index 0000000000..855755aa42 --- /dev/null +++ b/specs/tri27/staking.tri @@ -0,0 +1,144 @@ +# TRI-27 Staking Module — Source of Truth +# Issue: #443 +# phi^2 + 1/phi^2 = 3 | TRINITY + +name: staking +version: "1.0.0" +module: tri27.staking +description: "Staking module for TRI-27 token system" + +types: + StakePosition: + description: "Individual stake position" + fields: + - name: index + type: u32 + description: "Position index" + - name: amount + type: u128 + description: "Staked amount" + - name: lock_time + type: i64 + description: "When stake was created" + - name: unlock_time + type: i64 + description: "When stake can be withdrawn" + - name: reward_debt + type: u128 + description: "Reward debt at time of staking" + + StakePool: + description: "Global staking pool state" + fields: + - name: total_staked + type: u128 + description: "Total tokens staked across all stakers" + - name: reward_rate + type: u128 + description: "Reward per second per staked token" + - name: last_update_time + type: i64 + description: "Last time rewards were accumulated" + - name: reward_per_token_stored + type: u128 + description: "Accumulated reward per token" + +constants: + MIN_STAKE: + type: u128 + value: "1000000000000000000" + description: "Minimum 1 token to stake" + + MAX_STAKE_POSITIONS: + type: u32 + value: 27 + description: "Max concurrent stake positions per user (one per register)" + + EARLY_UNSTAKE_PENALTY: + type: u16 + value: 1000 + description: "10% penalty in basis points for early unstake" + + REWARD_EMISSION_RATE: + type: u128 + value: "3141592653589793" + description: "phi-aligned emission rate per second" + +functions: + stake: + description: "Create a new stake position" + params: + - name: staker + type: "[32]u8" + - name: amount + type: u128 + - name: duration_seconds + type: i64 + returns: StakePosition + + unstake: + description: "Withdraw a mature stake position" + params: + - name: staker + type: "[32]u8" + - name: position_index + type: u32 + returns: u128 + + claim_rewards: + description: "Claim accumulated staking rewards" + params: + - name: staker + type: "[32]u8" + returns: u128 + + pending_rewards: + description: "View pending unclaimed rewards" + params: + - name: staker + type: "[32]u8" + returns: u128 + + pool_info: + description: "Get global staking pool info" + params: [] + returns: StakePool + +tests: + test_stake_creates_position: + description: "Staking creates a new position" + assertions: + - "stake(A, 1000, 86400).amount == 1000" + + test_unstake_returns_principal_plus_reward: + description: "Mature unstake returns principal + rewards" + assertions: + - "unstake after unlock_time >= principal" + + test_early_unstake_applies_penalty: + description: "Early unstake deducts penalty" + assertions: + - "unstake before unlock_time returns amount * (1 - EARLY_UNSTAKE_PENALTY/10000)" + + test_max_27_positions: + description: "Cannot exceed 27 stake positions" + assertions: + - "stake beyond MAX_STAKE_POSITIONS fails" + + test_reward_accumulates: + description: "Rewards accumulate over time" + assertions: + - "pending_rewards(A, t+1000) > pending_rewards(A, t)" + +invariants: + total_staked_conservation: + description: "Sum of all stakes equals pool total_staked" + expression: "sum(positions.amount) == pool.total_staked" + + no_double_claim: + description: "Rewards can only be claimed once" + expression: "claim_rewards resets pending to 0" + + stake_amount_positive: + description: "All stake amounts are positive" + expression: "forall p: StakePosition :: p.amount >= MIN_STAKE" diff --git a/specs/tri27/staking_cli.tri b/specs/tri27/staking_cli.tri new file mode 100644 index 0000000000..4d9be6b6f7 --- /dev/null +++ b/specs/tri27/staking_cli.tri @@ -0,0 +1,63 @@ +# TRI-27 Staking Commands — Source of Truth +# Issue: #446 +# phi^2 + 1/phi^2 = 3 | TRINITY + +name: staking_cli +version: "1.0.0" +module: tri27.cli.staking +description: "CLI commands for TRI-27 staking operations" + +commands: + stake: + description: "Stake tokens with lock duration" + usage: "tri27 stake [--duration ]" + params: + - name: amount + type: u128 + - name: duration + type: i64 + default: 2592000 + returns: StakePosition + + unstake: + description: "Unstake a position" + usage: "tri27 unstake " + params: + - name: position_index + type: u32 + returns: u128 + + positions: + description: "List all stake positions" + usage: "tri27 stake positions [--address ]" + params: + - name: address + type: "[32]u8" + returns: "[]StakePosition" + + rewards: + description: "View pending rewards" + usage: "tri27 stake rewards [--address ]" + params: + - name: address + type: "[32]u8" + returns: u128 + + pool: + description: "Show staking pool info" + usage: "tri27 stake pool" + params: [] + returns: StakePool + +tests: + test_stake_creates_position: + assertions: + - "stake(1000) creates position with amount=1000" + + test_positions_lists_all: + assertions: + - "positions() returns all active stakes" + + test_rewards_shows_pending: + assertions: + - "rewards() returns pending_rewards value" diff --git a/specs/tri27/token_cli.tri b/specs/tri27/token_cli.tri new file mode 100644 index 0000000000..6b4fcb8866 --- /dev/null +++ b/specs/tri27/token_cli.tri @@ -0,0 +1,67 @@ +# TRI-27 Token CLI Commands — Source of Truth +# Issue: #445 +# phi^2 + 1/phi^2 = 3 | TRINITY + +name: token_cli +version: "1.0.0" +module: tri27.cli.token +description: "CLI commands for TRI-27 token operations" + +commands: + balance: + description: "Check token balance" + usage: "tri27 token balance [--address ]" + params: + - name: address + type: "[32]u8" + description: "Address to check (default: current)" + returns: u128 + + transfer: + description: "Transfer tokens" + usage: "tri27 token transfer " + params: + - name: to + type: "[32]u8" + - name: amount + type: u128 + returns: bool + + approve: + description: "Approve spender allowance" + usage: "tri27 token approve " + params: + - name: spender + type: "[32]u8" + - name: amount + type: u128 + returns: bool + + allowance: + description: "Check approved allowance" + usage: "tri27 token allowance " + params: + - name: owner + type: "[32]u8" + - name: spender + type: "[32]u8" + returns: u128 + + total_supply: + description: "Get total token supply" + usage: "tri27 token supply" + params: [] + returns: u128 + +tests: + test_balance_shows_correct_amount: + assertions: + - "balance(addr) returns current balance" + + test_transfer_requires_sufficient_balance: + assertions: + - "transfer with amount > balance fails" + + test_approve_sets_allowance: + assertions: + - "approve(spender, 1000) sets allowance(spender) == 1000" diff --git a/specs/tri27/token_ffi.tri b/specs/tri27/token_ffi.tri new file mode 100644 index 0000000000..21ae397a0a --- /dev/null +++ b/specs/tri27/token_ffi.tri @@ -0,0 +1,85 @@ +# TRI-27 Token FFI — Source of Truth +# Issue: #442 +# phi^2 + 1/phi^2 = 3 | TRINITY + +name: token_ffi +version: "1.0.0" +module: tri27.ffi.token +description: "FFI bridge for TRI-27 token operations from external runtimes" + +ffi_functions: + tri27_token_balance: + description: "Get balance via FFI" + params: + - name: address_ptr + type: "*const u8" + - name: address_len + type: usize + returns: u128 + + tri27_token_transfer: + description: "Transfer via FFI" + params: + - name: from_ptr + type: "*const u8" + - name: from_len + type: usize + - name: to_ptr + type: "*const u8" + - name: to_len + type: usize + - name: amount + type: u128 + returns: bool + + tri27_token_stake: + description: "Stake via FFI" + params: + - name: staker_ptr + type: "*const u8" + - name: staker_len + type: usize + - name: amount + type: u128 + - name: duration + type: i64 + returns: u32 + + tri27_token_claim: + description: "Claim rewards via FFI" + params: + - name: staker_ptr + type: "*const u8" + - name: staker_len + type: usize + returns: u128 + + tri27_token_pending_rewards: + description: "Get pending rewards via FFI" + params: + - name: staker_ptr + type: "*const u8" + - name: staker_len + type: usize + returns: u128 + +tests: + test_ffi_balance_null_safe: + description: "FFI returns 0 for null address" + assertions: + - "tri27_token_balance(null, 0) == 0" + + test_ffi_transfer_returns_bool: + description: "FFI transfer returns success boolean" + assertions: + - "tri27_token_transfer returns true on success, false on failure" + + test_ffi_stake_returns_index: + description: "FFI stake returns position index" + assertions: + - "tri27_token_stake returns valid position index >= 0" + +invariants: + ffi_null_safe: + description: "All FFI functions handle null pointers safely" + expression: "forall fn: ffi_function :: fn(null, 0) does not crash" diff --git a/specs/tri27/token_types.tri b/specs/tri27/token_types.tri new file mode 100644 index 0000000000..ce618a24a2 --- /dev/null +++ b/specs/tri27/token_types.tri @@ -0,0 +1,211 @@ +# TRI-27 Token Types — Source of Truth +# Issue: #441 +# phi^2 + 1/phi^2 = 3 | TRINITY + +name: token_types +version: "1.0.0" +module: tri27.token_types +description: "Token types for TRI-27 staking and reward system" + +types: + TokenAccount: + description: "Account balance and allowance state" + fields: + - name: balance + type: u128 + description: "Token balance with 18 decimal places" + - name: nonce + type: u64 + description: "Transaction counter for replay protection" + - name: staked_amount + type: u128 + description: "Currently staked tokens" + + TokenStake: + description: "Staking position with lock period" + fields: + - name: staker + type: "[32]u8" + description: "Staker public key (ed25519)" + - name: amount + type: u128 + description: "Staked token amount" + - name: lock_time + type: i64 + description: "Unix timestamp when stake was created" + - name: unlock_time + type: i64 + description: "Unix timestamp when stake unlocks" + - name: reward_debt + type: u128 + description: "Accumulated reward debt for distribution" + + TokenTransfer: + description: "Transfer event record" + fields: + - name: from_addr + type: "[32]u8" + description: "Sender address" + - name: to_addr + type: "[32]u8" + description: "Recipient address" + - name: amount + type: u128 + description: "Transfer amount" + - name: nonce + type: u64 + description: "Sender nonce at time of transfer" + + TokenAllowance: + description: "Approved spending allowance" + fields: + - name: owner + type: "[32]u8" + description: "Token owner address" + - name: spender + type: "[32]u8" + description: "Approved spender address" + - name: amount + type: u128 + description: "Maximum spendable amount" + +constants: + DECIMALS: + type: u8 + value: 18 + description: "Token decimal places" + + MAX_SUPPLY: + type: u128 + value: "270000000000000000000000000" + description: "Max supply: 270M tokens (27 * 10M * 10^18)" + + MIN_STAKE_AMOUNT: + type: u128 + value: "1000000000000000000" + description: "Minimum stake: 1 token" + + DEFAULT_LOCK_DURATION: + type: i64 + value: 2592000 + description: "Default lock: 30 days in seconds" + + TOTAL_COPTIC_REGISTERS: + type: u8 + value: 27 + description: "Total Coptic registers for token operations" + +functions: + token_balance_of: + description: "Get token balance for address" + params: + - name: account + type: "[32]u8" + description: "Account address" + returns: u128 + + token_transfer: + description: "Transfer tokens between addresses" + params: + - name: from + type: "[32]u8" + - name: to + type: "[32]u8" + - name: amount + type: u128 + returns: bool + + token_approve: + description: "Approve spender for allowance" + params: + - name: owner + type: "[32]u8" + - name: spender + type: "[32]u8" + - name: amount + type: u128 + returns: bool + + token_stake: + description: "Stake tokens with lock duration" + params: + - name: staker + type: "[32]u8" + - name: amount + type: u128 + - name: lock_duration + type: i64 + returns: TokenStake + + token_unstake: + description: "Unstake after lock period expires" + params: + - name: staker + type: "[32]u8" + - name: stake_index + type: u32 + returns: bool + + token_reward_pending: + description: "Calculate pending reward for staker" + params: + - name: staker + type: "[32]u8" + returns: u128 + +tests: + test_max_supply_is_27m: + description: "Verify max supply = 270M tokens" + assertions: + - "MAX_SUPPLY == 270_000_000 * 10^DECIMALS" + + test_balance_starts_zero: + description: "New accounts have zero balance" + assertions: + - "token_balance_of(new_address) == 0" + + test_transfer_reduces_sender: + description: "Transfer reduces sender balance" + assertions: + - "token_transfer(A, B, 100) implies balance(A) decreases by 100" + + test_stake_locks_tokens: + description: "Staking locks tokens for duration" + assertions: + - "token_stake(A, 1000, 86400) implies balance(A) reduced by 1000" + + test_cannot_unstake_before_unlock: + description: "Unstake fails before unlock time" + assertions: + - "token_unstake(A, 0) fails if now < stake.unlock_time" + +invariants: + supply_conservation: + description: "Total supply never exceeds MAX_SUPPLY" + expression: "sum(balances) + sum(staked) <= MAX_SUPPLY" + + nonce_monotonic: + description: "Account nonce only increases" + expression: "forall tx: tx.nonce > previous_nonce(sender)" + + stake_non_negative: + description: "Stake amounts are positive" + expression: "forall s: TokenStake :: s.amount > 0" + + balance_non_negative: + description: "Balances cannot go negative" + expression: "forall a: TokenAccount :: a.balance >= 0" + +coptic_registers: + t18: + description: "Current token balance (read-only)" + type: u128 + access: RO + t19: + description: "Pending staking rewards (read-only)" + type: u128 + access: RO + t20: + description: "Currently staked amount (read-only)" + type: u128 + access: RO