Locked requirements Owner-reviewed and hash-locked. Manifest 53e32ebeda25c170
REQ-VALID-SUCCEEDS
Every valid payout succeeds.
theorem req_valid_succeeds : ValidSucceeds stepDefinition of ValidSucceeds def ValidSucceeds (step : Impl) : Prop :=
∀ s r, ValidPayout s r → (step s r).1 = .okStatement sha256 d8ef199351b9
REQ-INVALID-NOOP
Every invalid payout is rejected and leaves the state unchanged.
theorem req_invalid_noop : InvalidNoop stepDefinition of InvalidNoop def InvalidNoop (step : Impl) : Prop :=
∀ s r, ¬ ValidPayout s r → step s r = (.rejected, s)Statement sha256 5a0c4f002248
REQ-AUTHORIZATION
Success implies the requester is authorized for the source.
theorem req_authorization : AuthorizedOnly stepDefinition of AuthorizedOnly def AuthorizedOnly (step : Impl) : Prop :=
∀ s r, (step s r).1 = .ok → s.auth r.requester r.source = trueStatement sha256 9546dbe11b8d
REQ-EFFECTS
On success, the whole next state (other than applied IDs, see REQ-IDEMPOTENCY) is determined: balances are exactly `expectedBalance`, and the account universe and authorization relation are unchanged.
theorem req_effects : Effects stepDefinition of Effects def Effects (step : Impl) : Prop :=
∀ s r, (step s r).1 = .ok →
(step s r).2.accounts = s.accounts ∧
(step s r).2.auth = s.auth ∧
∀ a, (step s r).2.balance a = expectedBalance s r aStatement sha256 06d053c0e722
REQ-IDEMPOTENCY
On success, the applied IDs are exactly the old ones plus this one, and resubmitting the same request is rejected without changing the state.
theorem req_idempotency : Idempotent stepDefinition of Idempotent def Idempotent (step : Impl) : Prop :=
∀ s r, (step s r).1 = .ok →
(∀ x, x ∈ (step s r).2.applied ↔ x = r.txId ∨ x ∈ s.applied) ∧
step (step s r).2 r = (.rejected, (step s r).2)Statement sha256 5b16ad1efc68
REQ-NONNEGATIVE
Nonnegative balances stay nonnegative.
theorem req_nonnegative : NonNegative stepDefinition of NonNegative def NonNegative (step : Impl) : Prop :=
∀ s r, (∀ a ∈ s.accounts, 0 ≤ s.balance a) →
∀ a ∈ (step s r).2.accounts, 0 ≤ (step s r).2.balance aStatement sha256 c9c71dd7bcd0
REQ-FAIR-SHARES
On success, recipient `i` receives exactly `fairShare amount n i`.
theorem req_fair_shares : FairShares stepDefinition of FairShares def FairShares (step : Impl) : Prop :=
∀ s r, (step s r).1 = .ok →
∀ (i : Nat) (h : i < r.recipients.length),
(step s r).2.balance r.recipients[i] - s.balance r.recipients[i]
= (fairShare r.amount r.recipients.length i : Int)Statement sha256 f3e3da1e7ab8
REQ-CONSERVATION
On success, total money is unchanged.
theorem req_conservation : Conserves stepDefinition of Conserves def Conserves (step : Impl) : Prop :=
∀ s r, (step s r).1 = .ok → total (step s r).2 = total sStatement sha256 3553d7218bb8