hypercall_state_commitment/
leaves.rs

1use serde::{Deserialize, Serialize};
2
3/// Fixed-point scale: 1e8 (same as engine contract units).
4/// All monetary values in leaves are stored as i128 scaled by 1e8.
5/// Example: $95,000.50 = 9_500_050_000_000i128
6pub const PRICE_SCALE: i128 = 100_000_000;
7
8/// Account metadata leaf.
9/// Key: keccak256(address || "account")
10///
11/// `cash` is the ledger balance scaled by 1e8 (from `Decimal`).
12/// `margin_mode`: 0 = Standard, 1 = Portfolio.
13/// `liquidation_state`: 0 = Healthy, 1 = PreLiquidation, 2 = InLiquidation, 3 = Liquidated.
14#[derive(
15    Debug, Clone, Serialize, Deserialize, PartialEq, borsh::BorshSerialize, borsh::BorshDeserialize,
16)]
17pub struct AccountLeaf {
18    /// Ledger cash balance, scaled 1e8. Preserves full `Decimal` precision.
19    pub cash: i128,
20    pub nonce: u64,
21    pub margin_mode: u8,
22    pub liquidation_state: u8,
23}
24
25/// Option position leaf.
26/// Key: keccak256(address || "pos" || symbol)
27///
28/// Both fields scaled 1e8, matching engine's `Decimal` via `to_contract_units()`.
29#[derive(
30    Debug, Clone, Serialize, Deserialize, PartialEq, borsh::BorshSerialize, borsh::BorshDeserialize,
31)]
32pub struct OptionPositionLeaf {
33    /// Signed quantity scaled 1e8. Positive = long, negative = short.
34    pub quantity: i128,
35    /// Average entry price scaled 1e8.
36    pub entry_price: i128,
37}
38
39/// Open order leaf.
40/// Key: keccak256(address || "order" || order_id_be_bytes)
41///
42/// All prices/sizes scaled 1e8.
43#[derive(
44    Debug, Clone, Serialize, Deserialize, PartialEq, borsh::BorshSerialize, borsh::BorshDeserialize,
45)]
46pub struct OrderLeaf {
47    /// Order ID.
48    pub order_id: u64,
49    /// Instrument symbol (variable length, borsh length-prefixed).
50    pub symbol: String,
51    /// 0 = Buy, 1 = Sell.
52    pub side: u8,
53    /// Limit price scaled 1e8.
54    pub price: i128,
55    /// Remaining size scaled 1e8.
56    pub remaining_size: i128,
57    /// Original size scaled 1e8.
58    pub original_size: i128,
59    /// Client-assigned ID (optional).
60    pub client_id: Option<String>,
61    /// Whether MMP is enabled for this order.
62    pub mmp_enabled: bool,
63}
64
65/// Perp position leaf.
66/// Key: keccak256(address || "perp" || coin)
67///
68/// Stored as i128 scaled 1e8 to avoid f64 non-determinism in commitments.
69/// Conversion from engine's `f64`: `(size * 1e8) as i128`.
70#[derive(
71    Debug, Clone, Serialize, Deserialize, PartialEq, borsh::BorshSerialize, borsh::BorshDeserialize,
72)]
73pub struct PerpPositionLeaf {
74    /// Signed size scaled 1e8. Positive = long, negative = short.
75    pub size: i128,
76    /// Entry price scaled 1e8.
77    pub entry_price: i128,
78}
79
80/// MMP config leaf.
81/// Key: keccak256(address || "mmp" || currency)
82///
83/// Limits stored as i128 scaled 1e8 (from engine's `f64`).
84#[derive(
85    Debug, Clone, Serialize, Deserialize, PartialEq, borsh::BorshSerialize, borsh::BorshDeserialize,
86)]
87pub struct MmpConfigLeaf {
88    pub enabled: bool,
89    pub interval_ms: i64,
90    pub frozen_time_ms: i64,
91    /// Quantity limit scaled 1e8. None = no limit.
92    pub qty_limit: Option<i128>,
93    /// Delta limit scaled 1e8. None = no limit.
94    pub delta_limit: Option<i128>,
95    /// Vega limit scaled 1e8. None = no limit.
96    pub vega_limit: Option<i128>,
97}
98
99/// Instrument metadata leaf (global).
100/// Key: keccak256("instrument" || symbol)
101///
102/// Strike scaled 1e8.
103#[derive(
104    Debug, Clone, Serialize, Deserialize, PartialEq, borsh::BorshSerialize, borsh::BorshDeserialize,
105)]
106pub struct InstrumentLeaf {
107    pub expired: bool,
108    /// 0 = OrderbookOnly, 1 = RfqOnly, 2 = Both
109    pub trading_mode: u8,
110    pub expiry: u64,
111    /// Strike price scaled 1e8.
112    pub strike: i128,
113    /// 0 = Call, 1 = Put
114    pub option_type: u8,
115}
116
117/// Oracle anchor leaf (global).
118/// Key: keccak256("oracle" || underlying)
119///
120/// Spot price scaled 1e8 (from engine's `Decimal`).
121/// IV surface is too large to store inline -- we commit its hash only.
122#[derive(
123    Debug, Clone, Serialize, Deserialize, PartialEq, borsh::BorshSerialize, borsh::BorshDeserialize,
124)]
125pub struct OracleLeaf {
126    /// Spot price scaled 1e8.
127    pub spot_price: i128,
128    /// keccak256 hash of the serialized VolatilitySurface.
129    pub iv_surface_hash: [u8; 32],
130}
131
132/// Global counters leaf (singleton).
133/// Key: keccak256("global")
134#[derive(
135    Debug, Clone, Serialize, Deserialize, PartialEq, borsh::BorshSerialize, borsh::BorshDeserialize,
136)]
137pub struct GlobalLeaf {
138    pub next_order_id: u64,
139    pub next_trade_id: u64,
140    pub command_chain_root: [u8; 32],
141    pub command_chain_seq: u64,
142}
143
144/// Risk leaf (separate JMT).
145/// Key: keccak256(address)
146///
147/// All monetary fields scaled 1e8 to preserve sub-cent precision from
148/// the engine's `Decimal`/`f64` risk computations.
149#[derive(
150    Debug, Clone, Serialize, Deserialize, PartialEq, borsh::BorshSerialize, borsh::BorshDeserialize,
151)]
152pub struct RiskLeaf {
153    /// Equity = cash + option UPNL + perp UPNL, scaled 1e8.
154    pub equity: i128,
155    /// Initial margin required, scaled 1e8.
156    pub initial_margin: i128,
157    /// Maintenance margin required, scaled 1e8.
158    pub maintenance_margin: i128,
159    /// SPAN scanning risk, scaled 1e8.
160    pub scanning_risk: i128,
161    /// Incremented on every risk recomputation for this account.
162    pub health_nonce: u64,
163}
164
165/// Serialize a leaf to bytes using borsh for deterministic encoding.
166pub fn leaf_to_bytes<T: borsh::BorshSerialize>(leaf: &T) -> Vec<u8> {
167    borsh::to_vec(leaf).expect("borsh serialization should not fail for fixed-size types")
168}
169
170/// Deserialize a leaf from borsh bytes.
171pub fn leaf_from_bytes<T: borsh::BorshDeserialize>(bytes: &[u8]) -> Result<T, std::io::Error> {
172    borsh::from_slice(bytes)
173}
174
175#[cfg(test)]
176mod tests {
177    use super::*;
178
179    #[test]
180    fn account_leaf_round_trip() {
181        let leaf = AccountLeaf {
182            cash: 1_000_000 * PRICE_SCALE,
183            nonce: 42,
184            margin_mode: 1,
185            liquidation_state: 0,
186        };
187        let bytes = leaf_to_bytes(&leaf);
188        let decoded: AccountLeaf = leaf_from_bytes(&bytes).unwrap();
189        assert_eq!(leaf, decoded);
190    }
191
192    #[test]
193    fn risk_leaf_round_trip() {
194        let leaf = RiskLeaf {
195            equity: 500_000 * PRICE_SCALE,
196            initial_margin: 200_000 * PRICE_SCALE,
197            maintenance_margin: 100_000 * PRICE_SCALE,
198            scanning_risk: 150_000 * PRICE_SCALE,
199            health_nonce: 7,
200        };
201        let bytes = leaf_to_bytes(&leaf);
202        let decoded: RiskLeaf = leaf_from_bytes(&bytes).unwrap();
203        assert_eq!(leaf, decoded);
204    }
205
206    #[test]
207    fn global_leaf_round_trip() {
208        let leaf = GlobalLeaf {
209            next_order_id: 12345,
210            next_trade_id: 6789,
211            command_chain_root: [0xAB; 32],
212            command_chain_seq: 100,
213        };
214        let bytes = leaf_to_bytes(&leaf);
215        let decoded: GlobalLeaf = leaf_from_bytes(&bytes).unwrap();
216        assert_eq!(leaf, decoded);
217    }
218
219    #[test]
220    fn borsh_encoding_is_deterministic() {
221        let leaf = OptionPositionLeaf {
222            quantity: 100_000_000,
223            entry_price: 9500000,
224        };
225        let a = leaf_to_bytes(&leaf);
226        let b = leaf_to_bytes(&leaf);
227        assert_eq!(a, b);
228    }
229
230    #[test]
231    fn perp_leaf_i128_preserves_precision() {
232        let leaf = PerpPositionLeaf {
233            size: 1_234_567_89,             // 0.12345679 BTC in 1e8
234            entry_price: 95_000_50_000_000, // $95,000.50 in 1e8
235        };
236        let bytes = leaf_to_bytes(&leaf);
237        let decoded: PerpPositionLeaf = leaf_from_bytes(&bytes).unwrap();
238        assert_eq!(leaf, decoded);
239    }
240
241    #[test]
242    fn mmp_limits_i128_preserves_fractional() {
243        let leaf = MmpConfigLeaf {
244            enabled: true,
245            interval_ms: 1000,
246            frozen_time_ms: 5000,
247            qty_limit: Some(1_50_000_000), // 1.5 in 1e8
248            delta_limit: Some(50_000_000), // 0.5 in 1e8
249            vega_limit: Some(25_000_000),  // 0.25 in 1e8
250        };
251        let bytes = leaf_to_bytes(&leaf);
252        let decoded: MmpConfigLeaf = leaf_from_bytes(&bytes).unwrap();
253        assert_eq!(leaf, decoded);
254    }
255}
256
257// ============================================================
258// Kani formal verification harnesses
259// ============================================================
260
261#[cfg(kani)]
262mod kani_proofs {
263    use super::*;
264
265    /// Prove: AccountLeaf serialization round-trips for ALL possible values.
266    #[kani::proof]
267    fn fast_account_leaf_round_trip_all() {
268        let leaf = AccountLeaf {
269            cash: kani::any(),
270            nonce: kani::any(),
271            margin_mode: kani::any(),
272            liquidation_state: kani::any(),
273        };
274        let bytes = leaf_to_bytes(&leaf);
275        let decoded: AccountLeaf = leaf_from_bytes(&bytes).unwrap();
276        assert_eq!(leaf.cash, decoded.cash);
277        assert_eq!(leaf.nonce, decoded.nonce);
278        assert_eq!(leaf.margin_mode, decoded.margin_mode);
279        assert_eq!(leaf.liquidation_state, decoded.liquidation_state);
280    }
281
282    /// Prove: OptionPositionLeaf serialization round-trips for ALL possible values.
283    #[kani::proof]
284    fn fast_option_position_leaf_round_trip_all() {
285        let leaf = OptionPositionLeaf {
286            quantity: kani::any(),
287            entry_price: kani::any(),
288        };
289        let bytes = leaf_to_bytes(&leaf);
290        let decoded: OptionPositionLeaf = leaf_from_bytes(&bytes).unwrap();
291        assert_eq!(leaf.quantity, decoded.quantity);
292        assert_eq!(leaf.entry_price, decoded.entry_price);
293    }
294
295    /// Prove: PerpPositionLeaf serialization round-trips for ALL possible values.
296    #[kani::proof]
297    fn fast_perp_position_leaf_round_trip_all() {
298        let leaf = PerpPositionLeaf {
299            size: kani::any(),
300            entry_price: kani::any(),
301        };
302        let bytes = leaf_to_bytes(&leaf);
303        let decoded: PerpPositionLeaf = leaf_from_bytes(&bytes).unwrap();
304        assert_eq!(leaf.size, decoded.size);
305        assert_eq!(leaf.entry_price, decoded.entry_price);
306    }
307
308    /// Prove: RiskLeaf serialization round-trips for ALL possible values.
309    #[kani::proof]
310    fn fast_risk_leaf_round_trip_all() {
311        let leaf = RiskLeaf {
312            equity: kani::any(),
313            initial_margin: kani::any(),
314            maintenance_margin: kani::any(),
315            scanning_risk: kani::any(),
316            health_nonce: kani::any(),
317        };
318        let bytes = leaf_to_bytes(&leaf);
319        let decoded: RiskLeaf = leaf_from_bytes(&bytes).unwrap();
320        assert_eq!(leaf.equity, decoded.equity);
321        assert_eq!(leaf.initial_margin, decoded.initial_margin);
322        assert_eq!(leaf.maintenance_margin, decoded.maintenance_margin);
323        assert_eq!(leaf.scanning_risk, decoded.scanning_risk);
324        assert_eq!(leaf.health_nonce, decoded.health_nonce);
325    }
326
327    /// Prove: GlobalLeaf serialization round-trips for ALL possible values
328    /// (excluding command_chain_root which is fixed-size [u8;32]).
329    #[kani::proof]
330    fn fast_global_leaf_round_trip_all() {
331        let leaf = GlobalLeaf {
332            next_order_id: kani::any(),
333            next_trade_id: kani::any(),
334            command_chain_root: kani::any(),
335            command_chain_seq: kani::any(),
336        };
337        let bytes = leaf_to_bytes(&leaf);
338        let decoded: GlobalLeaf = leaf_from_bytes(&bytes).unwrap();
339        assert_eq!(leaf.next_order_id, decoded.next_order_id);
340        assert_eq!(leaf.next_trade_id, decoded.next_trade_id);
341        assert_eq!(leaf.command_chain_root, decoded.command_chain_root);
342        assert_eq!(leaf.command_chain_seq, decoded.command_chain_seq);
343    }
344
345    /// Prove: leaf_to_bytes never panics for any AccountLeaf.
346    #[kani::proof]
347    fn fast_account_leaf_serialize_no_panic() {
348        let leaf = AccountLeaf {
349            cash: kani::any(),
350            nonce: kani::any(),
351            margin_mode: kani::any(),
352            liquidation_state: kani::any(),
353        };
354        let _ = leaf_to_bytes(&leaf);
355    }
356
357    /// Prove: borsh encoding is deterministic -- same input always produces same output.
358    #[kani::proof]
359    fn fast_borsh_deterministic() {
360        let quantity: i128 = kani::any();
361        let entry_price: i128 = kani::any();
362        let leaf = OptionPositionLeaf {
363            quantity,
364            entry_price,
365        };
366        let a = leaf_to_bytes(&leaf);
367        let b = leaf_to_bytes(&leaf);
368        assert_eq!(a, b);
369    }
370}
hypercall_state_commitment/leaves.rs

hypercall_state_commitment/
leaves.rs
