feat(tri27): token system specs — types, staking, rewards, CLI, FFI (Closes #440-#447)

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"

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"

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"

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 <amount> [--duration <seconds>]"
+    params:
+      - name: amount
+        type: u128
+      - name: duration
+        type: i64
+        default: 2592000
+    returns: StakePosition
+
+  unstake:
+    description: "Unstake a position"
+    usage: "tri27 unstake <position-index>"
+    params:
+      - name: position_index
+        type: u32
+    returns: u128
+
+  positions:
+    description: "List all stake positions"
+    usage: "tri27 stake positions [--address <addr>]"
+    params:
+      - name: address
+        type: "[32]u8"
+    returns: "[]StakePosition"
+
+  rewards:
+    description: "View pending rewards"
+    usage: "tri27 stake rewards [--address <addr>]"
+    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"