Chapter Γʹ · reference

The covenants

Five Simplicity programs, about 1,200 lines in total, enforce the whole protocol. This chapter is the reference: what each program guards, arm by arm, with the load-bearing asserts cited by line. Where this text and the source disagree, the source wins.

All ratio math shares one helper. Collateral requirements are expressed as coll_at_cr(debt_cents, price, k) = divide_64(debt_cents * k, price * 200) with k = CR_percent * 2,000,000 vault.simf:130-139. The k-values used below: 150% = 300000000, 130% = 260000000, 137% = 274000000, 132% = 264000000, 115% = 230000000, 100% = 200000000, 20% = 40000000, 5% = 10000000, 0.5% = 1000000.

1vault.simf - the position

Per-vault covenant, 471 lines. Holds L-BTC; state (debt, owner, last_height) in the 45-byte data leaf. Two guards run on every arm:

• Self-binding: the witnessed state must reconstruct the UTXO's own address vault.simf:244, and debt < 2^32 cents vault.simf:251 (conjured out-of-range vaults are excluded from every arm).
• One vault per transaction: current_index() == 0 vault.simf:258. Two equal-debt vaults once aliased a single shared pot output, extinguishing two debts for one repayment; the index pin closes the class.

The vault recognizes its siblings entirely by flat pins: the pot by POT_SPK + the OBOL asset id, the reserve by STABILITY_SPK + the POLICY asset. Its helper guards pin both ends of every pot move (pot_grows_by, vault.simf:159-175; pot_shrinks_by, vault.simf:178-192): input 1 and output 1 must both be the genuine pot, and the balance must change by exactly the stated delta. Without the input-side pin, the genuine pot could be left unspent while the delta was minted into a fresh UTXO at the same address from an arbitrary OBOL coin.

2The pot - two leaves, one address

The pot holds the entire OBOL supply at one constant address with two Simplicity leaves. It is the compile root and reconstructs nobody, which is what lets every other covenant pin it flatly.

reserve_repay.simf - inflow (47 lines)

OBOL returning on repay, close, liquidate, redeem, and bad-debt. Guards: the pot sits at input 1 on every inflow path (current_index() == 1, an anti-aliasing pin reserve_repay.simf:33); it recurses to output 1 at its own address in OBOL reserve_repay.simf:36-37; and the balance is grow-only (le_64(reserve_in, reserve_out) reserve_repay.simf:46). The exact inflow amount is pinned by the vault, not here.

pot_outflow.simf - outflow (44 lines)

OBOL leaving on OPEN and DRAW. The leaf checks exactly one thing: the issuer's identity token is co-spent at the input immediately after the pot (ISSUER_TOKEN_ID == input_asset(current_index + 1) pot_outflow.simf:37-39), and the pot recurses to output 1. The amount is deliberately not pinned here - the issuer pins it - and the token gate is what makes that delegation safe.

3issuer.simf - the authority

529 lines. Holds the one-unit token; carries the global last_mint_height anchor in its 5-byte data leaf; the only covenant that reconstructs vault addresses. All four arms end in recurse_token (asset == token, amount == 1, successor at the advanced anchor) issuer.simf:215-222. Freshness on this covenant is non-strict, le_32(last_mint_height, height): the global anchor must reject older ticks without serializing several legitimate mints that share one fresh tick issuer.simf:29-33.

4stability.simf - the reserve

118 lines, one leaf, no data leaf: a constant address, so peers pin it flatly. Its own recency need rides on the issuer's anchor instead of a per-reserve ratchet - an earlier mutable (ratcheted) reserve address opened a sybil-reserve fee diversion and was simplified away stability.simf:14-25. Every path asserts its own input is POLICY (anyone can send junk assets to a public address) stability.simf:62-63.

• ACCUMULATE: pinned to current_index() == 3; recurses to output 3 at its own address; balance grow-only. The exact fee amount is pinned by the vault or issuer arm in the same transaction stability.simf:69-77.
• BAD-DEBT: pinned to current_index() == 3; requires the issuer token at input 4 stability.simf:98; requires the pot to strictly grow (lt_64, input 1 to output 1, both pinned to POT_SPK + OBOL) stability.simf:100-109; recurses to output 2 and only self-defends downward (output <= balance) - the exact shrink is authored by the issuer's ATTEST stability.simf:111-116.

5The OP witness sums

Each covenant dispatches through a single nested Either witness. These shapes are consensus-critical for builders: a wrong nesting does not fail loudly, it prunes to a different arm. In all of the following, tick = (height: u32, (backing_k: u32, [Either<(), (price: u32, sig)>; 5])) - five quote slots, exactly three of which are Right((price, sig)).

Vault vault.simf:263-266

OP = Either<
  (owner_sig, Either<                     // Left           = owner ops
      (),                                 //   L(sig, Left)         CLOSE
      Either<u64,                         //   L(sig, R(Left r))    REPAY r
             (u64, tick)>>),              //   L(sig, R(R(d,tick))) DRAW d
  Either<(u64, tick),                     // R(Left)              LIQUIDATE (dd, tick)
    Either<tick,                          // R(R(Left))           FULL-LIQ
      Either<tick,                        // R(R(R(Left)))        BAD-DEBT
        Either<(u64, tick),               // R(R(R(R(Left))))     REDEEM (x, tick)
               tick>>>>>                  // R(R(R(R(Right))))    REFRESH

Issuer issuer.simf:232-238

OP = Either<
  (u64, (u256, tick)),                    // Left                 OPEN (principal, owner, tick)
  Either<
    (u64, (u256, (u32, (u64, u32)))),     // R(Left)              DRAW (old_debt, owner,
                                          //                        old_lh, new_debt, draw_height)
    Either<tick,                          // R(R(Left))           POKE
           (u64, (u256, (u32, tick)))>>>  // R(R(Right))          ATTEST (debt, owner, lh, tick)

Stability stability.simf:67

OP = Either<(), ()>                       // Left ACCUMULATE · Right BAD-DEBT

The pot's two leaves take no witness values at all; the operation is selected by the taproot script path. A conforming SDK must carry a total encoder per sum and prove each variant prunes to the intended arm (see chapter Ιʹ).

6Local pins added at freeze

Three defense-in-depth pins were added in the final hardening round. None fixed a live exploit; each removes a reliance on a sibling covenant that an immutable artifact should not carry:

• ATTEST pins its own position, current_index() == 4 - previously implied by the reserve's gate, now local issuer.simf:402-408.
• ATTEST pins input_asset(1) == OBOL locally before reading the pot amount - previously guaranteed by the co-spent reserve arm issuer.simf:496-501.
• pot_grows_by pins the input side to POT_SPK, symmetric with pot_shrinks_by vault.simf:160-166.