Chapter ΙΒʹ · the frozen source

Covenant source

The five frozen Simplicity programs, verbatim. Every file.simf:line cross-reference in this spec links here, to the exact line. This is the artifact the golden CMRs in chapter Θʹ pin.

vault.simf reserve_repay.simf pot_outflow.simf issuer.simf stability.simf

vault.simf the per-position covenant

Holds L-BTC collateral; commits (debt, owner, last_height) in an unspendable data leaf; owner and permissionless ops.

reserve_repay.simf the pot inflow leaf

OBOL returning to the pot on repay, close, liquidate, redeem, and bad-debt. Grow-only, pinned to input 1.

1/* 2 * STYX MULTIVAULT - reserve REPAY leaf. 3 * 4 * OBOL flows back into the shared reserve when a vault is liquidated (the keeper 5 * returns the vault's debt). The reserve may only grow or stay on this leaf, so it 6 * can never be drained here; the vault's LIQUIDATE leaf is what pins the exact amount 7 * returned (reserve_in + that vault's debt). Recurses to output 1. 8 * 9 * The pot sits at input 1 on every inflow path (repay / close / liquidate / redeem / bad-debt), so 10 * this leaf pins current_index == 1 (H4, defense in depth): a second same-address pot input cannot be 11 * co-spent to alias the single output-1 recursion. (Safe even without it - the recursion is grow-only 12 * and the protocol keeps exactly one pot UTXO - but the pin removes the aliasing surface entirely.) 13 * 14 * Param: OBOL_ID. 15 */ 16fn explicit_output_amount(idx: u32) -> u64 { 17 let pair: (Asset1, Amount1) = unwrap(jet::output_amount(idx)); 18 let (_asset, amount): (Asset1, Amount1) = pair; 19 unwrap_right::<(u1, u256)>(amount) 20} 21 22fn explicit_output_asset(idx: u32) -> u256 { 23 let pair: (Asset1, Amount1) = unwrap(jet::output_amount(idx)); 24 let (asset, _amount): (Asset1, Amount1) = pair; 25 unwrap_right::<(u1, u256)>(asset) 26} 27 28fn main() { 29 let obol: u256 = param::OBOL_ID; 30 31 // the pot is always at input 1 on inflow paths; pin it so a second same-address input cannot 32 // alias the single output-1 recursion (H4). 33 assert!(jet::eq_32(jet::current_index(), 1)); 34 35 // recurse: the reserve successor is output 1, and must be OBOL 36 assert!(jet::eq_256(jet::current_script_hash(), unwrap(jet::output_script_hash(1)))); 37 assert!(jet::eq_256(obol, explicit_output_asset(1))); 38 let reserve_out: u64 = explicit_output_amount(1); 39 40 // reserve input (this input) must be OBOL 41 let (in_asset, in_amount): (Asset1, Amount1) = jet::current_amount(); 42 assert!(jet::eq_256(obol, unwrap_right::<(u1, u256)>(in_asset))); 43 let reserve_in: u64 = unwrap_right::<(u1, u256)>(in_amount); 44 45 // inflow only: the reserve may grow or stay, never shrink on this leaf 46 assert!(jet::le_64(reserve_in, reserve_out)); 47}

pot_outflow.simf the pot outflow leaf

OBOL leaving the pot on OPEN and DRAW, gated on the issuer token co-spent at the adjacent input.

1/* 2 * STYX v1 - OBOL pot OUTFLOW leaf. 3 * 4 * The OBOL pot holds the supply and is vault-independent (it reconstructs nobody), so the vault 5 * can pin it by a flat POT_SPK param without a CMR cycle. OBOL leaves the pot only on OPEN and 6 * DRAW, and only when authorized by the issuer - the covenant that reconstructs the vault and 7 * enforces 150% health. This leaf is the gate: it recurses the pot (output 1) and requires the 8 * issuer's unique token to be co-spent at the next input. The issuer (input pot_index + 1) does 9 * the real work (vault genuineness, the released amount, health); this leaf only ensures a 10 * genuine issuer authorized the release, so the pot cannot be drained by a bare spend. 11 * 12 * Tx layout (OPEN): inputs [pot(0), issuer(1), collateral(2)]; (DRAW): [vault(0), pot(1), issuer(2)]. 13 * In both the pot successor is output 1 and the issuer is at the input right after the pot. 14 * 15 * Params: OBOL_ID, ISSUER_TOKEN_ID (a 1-unit genesis asset held only by the issuer - a flat 16 * asset id, not a CMR, so this gate adds no covenant dependency). 17 */ 18fn explicit_output_asset(idx: u32) -> u256 { 19 let pair: (Asset1, Amount1) = unwrap(jet::output_amount(idx)); 20 let (asset, _amount): (Asset1, Amount1) = pair; 21 unwrap_right::<(u1, u256)>(asset) 22} 23fn explicit_input_asset(idx: u32) -> u256 { 24 let pair: (Asset1, Amount1) = unwrap(jet::input_amount(idx)); 25 let (asset, _amount): (Asset1, Amount1) = pair; 26 unwrap_right::<(u1, u256)>(asset) 27} 28 29fn main() { 30 // this pot input holds OBOL (explicit local check - the issuer reads this input's amount by index 31 // and pins the release against it, so making the asset explicit here removes the reliance on 32 // per-asset conservation to catch a non-OBOL UTXO funded at the public POT_SPK address). 33 let idx: u32 = jet::current_index(); 34 assert!(jet::eq_256(param::OBOL_ID, explicit_input_asset(idx))); 35 36 // the issuer (its unique token) must be co-spent at the input right after the pot. 37 let (of, next): (bool, u32) = jet::add_32(idx, 1); 38 assert!(jet::eq_8(jet::left_pad_low_1_8(<bool>::into(of)), 0)); 39 assert!(jet::eq_256(param::ISSUER_TOKEN_ID, explicit_input_asset(next))); 40 41 // recurse: the pot successor is output 1, in OBOL. The issuer pins the released amount. 42 assert!(jet::eq_256(jet::current_script_hash(), unwrap(jet::output_script_hash(1)))); 43 assert!(jet::eq_256(param::OBOL_ID, explicit_output_asset(1))); 44}

issuer.simf the mint authority

Holds the 1-unit identity token; the only vault reconstructor; global mint anchor; bad-debt attester.

stability.simf the reserve

Constant-address L-BTC backstop. Accumulate (grow-only) and issuer-attested bad-debt shrink.