{"ok":true,"provable":[{"key":"per-trade-cap","label":"a ceiling on any single spend","plain":"No one payment from this agent's wallet can exceed the ceiling, whatever asks for it.","lean":"theorem seal_never_passes_over_per_tx (s : Seal) (v : Nat) : s.perTx ≠ none → verdict s v = ok → v ≤ s.perTx.get"},{"key":"daily-cap","label":"a ceiling on a rolling day","plain":"The payments this agent makes in any rolling day cannot add up past the daily ceiling.","lean":"theorem seal_daily_never_exceeded (s : Seal) (spent v : Nat) : s.daily ≠ none → verdict s spent v = ok → spent + v ≤ s.daily.get"},{"key":"pause-stops-everything","label":"a pause that stops every payment","plain":"While this agent is paused nothing signs, at any size, including nothing at all.","lean":"theorem paused_seal_signs_nothing (s : Seal) (v : Nat) : s.paused → verdict s v ≠ ok"},{"key":"revoke-is-final","label":"a revocation nothing gets past","plain":"Once revoked, this agent's wallet signs nothing again. A revocation outranks every other setting.","lean":"theorem revoked_seal_is_final (s : Seal) (v : Nat) : s.revoked → verdict s v = refused REVOKED"},{"key":"day-holds-a-trade","label":"a daily ceiling that can always hold one trade","plain":"The daily ceiling is never set below the per-trade ceiling, so the agent can never be given a limit it cannot use.","lean":"theorem day_cap_never_below_trade_cap (m : Mandate) : (normalize m).perDay ≥ (normalize m).perCycle"},{"key":"caps-stay-inside-bounds","label":"limits that cannot be set outside the house bounds","plain":"Every limit on this agent lands inside the published range, whatever number was typed, including a negative one or a nonsense one.","lean":"theorem every_cap_within_bounds (spec : Spec) (f : Field) : inBounds f ((normalize spec).get f)"},{"key":"book-never-over-whole","label":"a book that cannot add up past the whole","plain":"The holdings this agent is told to keep can never sum past one hundred percent, and whatever is left over stays in ETH.","lean":"theorem book_sums_to_whole (m : Mandate) : legsTotal m + cashPct m = 100 ∧ legsTotal m ≤ 100"},{"key":"no-asset-twice","label":"no holding counted twice","plain":"The same asset cannot appear twice in this agent's book, so a weight can never be quietly doubled.","lean":"theorem no_duplicate_legs (m : Mandate) : (normalize m).legs.Nodup"},{"key":"payee-allowlist","label":"a list of addresses it may pay, and nothing else","plain":"When this agent is given a list of addresses, the wallet signs toward those and refuses every other destination, checked at the moment of signature rather than earlier.","lean":"theorem payee_list_is_exclusive (s : Seal) (v : Nat) (d : Addr) : s.payees ≠ [] → verdict s v d = ok → d ∈ s.payees"},{"key":"no-list-is-not-an-empty-list","label":"an agent given no list is not an agent that can pay nobody","plain":"A wallet that was never given a list of addresses keeps signing exactly as it did before. Reading a missing list as an empty one would stop every existing wallet at once, so the two are kept apart deliberately.","lean":"theorem no_list_allows_every_destination (s : Seal) (v : Nat) (d : Addr) : s.payees = [] → verdict s v d = ok"},{"key":"raise-waits","label":"a delay before any limit can rise","plain":"Raising a limit on this agent does not take effect immediately. There is a fixed wait, so a stolen key cannot widen the limits and drain the wallet in the same minute.","lean":"theorem raise_takes_effect_only_after_delay (s : Seal) (t : Time) : raisedAt s + delay > t → effective s t = old s"}],"notProvable":[{"key":"leverage","why":"nothing in the signing path knows what leverage a position carries, so a ceiling on it cannot be checked here"},{"key":"drawdown","why":"a loss limit needs the position's value over time, which the signing gate does not see; the desk's own halt is separate and is not proved here"},{"key":"asset-allowlist","why":"naming assets by ticker is not the same as naming the addresses they live at, and the gate checks addresses; give the agent a destination list and the check becomes a proved one"},{"key":"time-window","why":"the signing gate has no clock condition, so a trading window cannot be checked here"}],"enforcedBy":[{"fn":"sealVerdict","what":"decides every spend: a ceiling on one payment, a ceiling on a rolling day, a pause, a revocation, and the list of addresses the wallet may sign toward"},{"fn":"normalizeMandate","what":"decides what a mandate may say: every limit pulled inside its bounds, a book that adds up, no asset counted twice"}],"maxCapEth":100,"maxLegs":8,"raiseDelayMins":60}