1# Bend Bank: the laws2# ===================3#4# Each law is a claim about Web.serve, the one function the server runs:5# it takes the bank and one input (the time, a random key, and the bytes6# of an HTTP request) and returns the bank's change and the answer's7# bytes. PROOF.bend proves every law; `bend PROOF.bend --verdict` checks8# the proofs. The words above each law say what the claim means.910import Base11import ./bank.bend as B12import ./web.bend as W1314# Terms15# -----1617# the bank after a reply: its change, or the same bank18def after(s: B.Bank, r: W.Reply) -> B.Bank:19 match r:20 case W.Reply{bank, text}:21 Maybe.default(&2, B.Bank, bank, s)2223# the change and the bytes of a reply24def change(r: W.Reply) -> Maybe<&2, B.Bank>:25 match r:26 case W.Reply{bank, text}:27 bank2829def text(r: W.Reply) -> String:30 match r:31 case W.Reply{bank, text}:32 text3334# the parts of a request: the cookie's name and key, the host's time and35# random key, and what it asks for36def Req.user(r: W.Req) -> String:37 match r:38 case W.Req{time, rand, verb, path, user, pass, form}:39 user4041def Req.pass(r: W.Req) -> String:42 match r:43 case W.Req{time, rand, verb, path, user, pass, form}:44 pass4546def Req.time(r: W.Req) -> Nat:47 match r:48 case W.Req{time, rand, verb, path, user, pass, form}:49 time5051def Req.rand(r: W.Req) -> String:52 match r:53 case W.Req{time, rand, verb, path, user, pass, form}:54 rand5556def Req.route(r: W.Req) -> String:57 match r:58 case W.Req{time, rand, verb, path, user, pass, form}:59 verb ++ " " ++ path6061def Req.form(r: W.Req) -> List<&2, W.Field>:62 match r:63 case W.Req{time, rand, verb, path, user, pass, form}:64 form6566# who sends an input (the name and key in its cookie), when, the key the67# host made for it, its method and path, and its form68def user(input: String) -> String:69 Req.user(W.Req.parse(input))7071def key(input: String) -> String:72 Req.pass(W.Req.parse(input))7374def time(input: String) -> Nat:75 Req.time(W.Req.parse(input))7677def rand(input: String) -> String:78 Req.rand(W.Req.parse(input))7980def route(input: String) -> String:81 Req.route(W.Req.parse(input))8283def form(input: String) -> List<&2, W.Field>:84 Req.form(W.Req.parse(input))8586# the names taken in a tree of accounts: the tree, each account blanked87def names(t: B.Trie<B.Acc>) -> B.Trie<Unit>:88 match t:89 case B.Tip{}:90 B.Tip{}91 case B.Bin{v, lo, hi}:92 B.Bin{Maybe.map(&2, B.Acc, Unit, a => Unit{}, v), names(lo), names(hi)}9394def Bank.names(s: B.Bank) -> B.Trie<Unit>:95 match s:96 case B.Bank{vault, accts}:97 names(accts)9899# what everyone may know of a bank: the vault, and the names taken. The100# vault changes only when an account opens (LAW join), so it tells no101# more than the names do.102def Public(s1: B.Bank, s2: B.Bank) -> Data:103 Sigma<&2, &2, {B.Bank.vault(s1) == B.Bank.vault(s2) : Nat}, _ => {Bank.names(s1) == Bank.names(s2) : B.Trie<Unit>}>104105# what the holder of (name, pass) sees in two banks is the same: the view106# of the account with that name if pass is its key (the account, and the107# money it locked in others), else nothing108def Same(s1: B.Bank, s2: B.Bank, name: String, pass: String) -> Data:109 {B.Bank.seen(s1, name, pass) == B.Bank.seen(s2, name, pass) : Maybe<&2, B.View>}110111# a <= b112def LE(a: Nat, b: Nat) -> Type:113 {Nat.is_le(a, b) == True{} : Bool}114115# whether the key u is the key k116def Key.is(u: Maybe<&2, B.Key()>, k: B.Key()) -> Bool:117 match u:118 case None{}:119 False{}120 case Some{u}:121 B.Key.eq(u, k)122123# the account at k124def acct(s: B.Bank, k: B.Key()) -> Maybe<&2, B.Acc>:125 match s:126 case B.Bank{vault, accts}:127 B.Trie.get(B.Acc, k, accts)128129# the cash of an account, and the money q locked in it; none when there130# is no account131def cash(m: Maybe<&2, B.Acc>) -> Nat:132 match m:133 case None{}:134 0n135 case Some{B.Acc{pass, cash, note, line, loan, held}}:136 cash137138def held(m: Maybe<&2, B.Acc>, q: B.Key()) -> Nat:139 match m:140 case None{}:141 0n142 case Some{B.Acc{pass, cash, note, line, loan, held}}:143 B.Trie.num(q, held)144145def opened(+k: B.Key(), m: Maybe<&2, B.Acc>) -> Maybe<&2, B.Key()>:146 match m:147 case None{}:148 None{}149 case Some{a}:150 Some{k}151152def Bank.sender.at(accts: B.Trie<B.Acc>, m: Maybe<&2, B.Key()>, key: String) -> Maybe<&2, B.Key()>:153 match m:154 case None{}:155 None{}156 case Some{+k}:157 opened(k, B.Bank.check(B.Trie.get(B.Acc, k, accts), key))158159# the account that the name and key open, if any160def Bank.sender(s: B.Bank, user: String, key: String) -> Maybe<&2, B.Key()>:161 match s:162 case B.Bank{vault, accts}:163 Bank.sender.at(accts, B.Key.of(user), key)164165# the account that an input's cookie opens, if any: who sends it166def sender(s: B.Bank, +input: String) -> Maybe<&2, B.Key()>:167 Bank.sender(s, user(input), key(input))168169# a bank is sound when every account holds money only under the name of170# an account that exists: the genesis bank is (it has no account), and171# every request keeps it so (LAW sound)172def Sound(s: B.Bank) -> Type:173 @k: B.Key() -> @q: B.Key() -> {acct(s, q) == None{} : Maybe<&2, B.Acc>} -> {B.Acc.locked(acct(s, k), q) == None{} : Maybe<&2, Nat>}174175# the account b is the account a, as far as its holder cares, after a176# request by u: the same key, note, line and loan, no less cash, no less177# cash and money held from u, and the same money held from anyone else178def Keeps(a: B.Acc, b: B.Acc, u: Maybe<&2, B.Key()>) -> Type:179 match a b:180 case B.Acc{p1, c1, n1, l1, d1, h1} B.Acc{p2, c2, n2, l2, d2, h2}:181 {p2 == p1 : String} & {n2 == n1 : String} & {l2 == l1 : Nat} & {d2 == d1 : B.Loan} & LE(c1, c2) &182 (@q: B.Key() -> {Key.is(u, q) == True{} : Bool} ->183 LE(Nat.add(c1, B.Trie.num(q, h1)), Nat.add(c2, B.Trie.num(q, h2)))) &184 (@q: B.Key() -> {Key.is(u, q) == False{} : Bool} ->185 {B.Trie.num(q, h2) == B.Trie.num(q, h1) : Nat})186187# an account that existed still exists, and Keeps188def Kept(a: Maybe<&2, B.Acc>, b: Maybe<&2, B.Acc>, u: Maybe<&2, B.Key()>) -> Type:189 match a b:190 case None{} _:191 Unit192 case Some{a} None{}:193 Empty194 case Some{a} Some{b}:195 Keeps(a, b, u)196197# the loan of an account a, at time now, became the loan of b by one of:198# no change to its loan and line; a loan of x, from the line to the cash,199# owing x and 10% of it, rounded up, due in 600 seconds; or a payment of200# y, from the cash to the line, before the due time, lowering the debt by201# y. A loan past its due time is written off: no step repays it, and no202# step lends to its borrower again.203def Lent(c1: Nat, l1: Nat, d1: B.Loan, c2: Nat, l2: Nat, d2: B.Loan, now: Nat) -> Type:204 &x: Nat -> {d1 == B.Clear{} : B.Loan} & LE(1n, x) & LE(x, 1000n) &205 {c2 == Nat.add(c1, x) : Nat} & {Nat.add(l2, x) == l1 : Nat} &206 {d2 == B.Owing{Nat.add(x, Nat.div(Nat.add(x, 9n), 10n)), Nat.add(now, 600n)} : B.Loan}207208def Repaid(c1: Nat, l1: Nat, d1: B.Loan, c2: Nat, l2: Nat, d2: B.Loan, now: Nat) -> Type:209 match d1:210 case B.Clear{}:211 Empty212 case B.Owing{debt, till}:213 &y: Nat -> LE(now, till) & LE(1n, y) & LE(y, debt) &214 {Nat.add(c2, y) == c1 : Nat} & {l2 == Nat.add(l1, y) : Nat} &215 {d2 == B.Loan.rest(Nat.sub(debt, y), till) : B.Loan}216217def Step(a: B.Acc, b: B.Acc, now: Nat) -> Type:218 match a b:219 case B.Acc{p1, c1, n1, l1, d1, h1} B.Acc{p2, c2, n2, l2, d2, h2}:220 ({d2 == d1 : B.Loan} & {l2 == l1 : Nat}) | (Lent(c1, l1, d1, c2, l2, d2, now) | Repaid(c1, l1, d1, c2, l2, d2, now))221222# an account that existed still exists, and its loan took a Step223def Stepped(a: Maybe<&2, B.Acc>, b: Maybe<&2, B.Acc>, now: Nat) -> Type:224 match a b:225 case None{} _:226 Unit227 case Some{a} None{}:228 Empty229 case Some{a} Some{b}:230 Step(a, b, now)231232# the money rows 1 to n of a send's form pay the account at k: row i233# pays the amount in field cash<i> to the account named in field to<i>234def paid(+form: List<&2, W.Field>, +k: B.Key(), +n: Nat) -> Nat:235 match n:236 case 0n:237 0n238 case 1n+p:239 +i = Nat.show(1n+p)240 +hit = Key.is(B.Key.of(W.Req.get(form, "to" ++ i)), k)241 Nat.add(Bool.pick(Nat, hit, W.Text.nat(W.Req.get(form, "cash" ++ i)), 0n), paid(form, k, p))242243# all that rows 1 to n of a send's form pay244def spent(+form: List<&2, W.Field>, +n: Nat) -> Nat:245 match n:246 case 0n:247 0n248 case 1n+p:249 Nat.add(W.Text.nat(W.Req.get(form, "cash" ++ Nat.show(1n+p))), spent(form, p))250251# an account that a request opened at k: none was there, and now there252# is one with key pass, 100 in cash and 1,000 in its line, taken from the253# vault254def Opened(s1: B.Bank, s2: B.Bank, pass: String, k: B.Key()) -> Type:255 {acct(s1, k) == None{} : Maybe<&2, B.Acc>} &256 {acct(s2, k) == Some{B.Acc{pass, 100n, "", 1000n, B.Clear{}, B.Tip{}}} : Maybe<&2, B.Acc>} &257 {Nat.add(B.Bank.vault(s2), 1100n) == B.Bank.vault(s1) : Nat}258259# Laws260# ----261262# LAW privacy: take two sound banks that agree on public data, on what263# the sender of an input sees, and on what some holder (name, pass) sees.264# Then the input gets the same answer from both, and after it they still265# agree on public data and on what (name, pass) sees. So an answer shows266# nothing but your own account and public data, and no request, yours or267# anyone's, can move another account's data into what you see, except268# what that account's holder sends you.269law privacy:270 for +s1: B.Bank271 for +s2: B.Bank272 for +input: String273 for +name: String274 for +pass: String275 for ok1: Sound(s1)276 for ok2: Sound(s2)277 for pub: Public(s1, s2)278 for you: Same(s1, s2, user(input), key(input))279 for them: Same(s1, s2, name, pass)280 {text(W.Web.serve(s1, input)) == text(W.Web.serve(s2, input)) : String} &281 Public(after(s1, W.Web.serve(s1, input)), after(s2, W.Web.serve(s2, input))) &282 Same(after(s1, W.Web.serve(s1, input)), after(s2, W.Web.serve(s2, input)), name, pass)283284# LAW sound: every request keeps a bank sound.285law sound:286 for +s: B.Bank287 for +input: String288 for ok: Sound(s)289 Sound(after(s, W.Web.serve(s, input)))290291# LAW authority: a request leaves every account but its sender's no worse292# off for its holder: the account still exists, with the same key, note,293# line and loan, no less cash, and the same money held from others,294# except from the sender, which can only grow or be paid out into the295# account's cash.296law authority:297 for +s: B.Bank298 for +input: String299 for +k: B.Key()300 for no: {Key.is(sender(s, input), k) == False{} : Bool}301 Kept(acct(s, k), acct(after(s, W.Web.serve(s, input)), k), sender(s, input))302303# LAW escrow: money that q locked in the sender's account leaves it only304# back into q's cash. With authority: money a locks for b leaves the305# lock only into b's cash, on a's request (a release), or into a's cash,306# on b's request (a refund).307law escrow:308 for +s: B.Bank309 for +input: String310 for +k: B.Key()311 for +q: B.Key()312 for me: {Key.is(sender(s, input), k) == True{} : Bool}313 for no: {B.Key.eq(q, k) == False{} : Bool}314 LE(Nat.add(held(acct(s, k), q), cash(acct(s, q))),315 Nat.add(held(acct(after(s, W.Web.serve(s, input)), k), q), cash(acct(after(s, W.Web.serve(s, input)), q))))316317# LAW loan: a request changes its sender's loan and credit line only by318# a Step: a loan from the line, owing 10% more, or a repayment before the319# due time.320law loan:321 for +s: B.Bank322 for +input: String323 for +k: B.Key()324 for me: {Key.is(sender(s, input), k) == True{} : Bool}325 Stepped(acct(s, k), acct(after(s, W.Web.serve(s, input)), k), time(input))326327# LAW split: a send that changes the bank pays every row of its form,328# rows 1 to 3, exactly: each account ends with its cash before, plus329# what the rows pay it, less, for the sender, what all the rows pay.330law split:331 for +s: B.Bank332 for +input: String333 for +k: B.Key()334 for +b: B.Bank335 for send: {route(input) == "POST /send" : String}336 for e: {change(W.Web.serve(s, input)) == Some{b} : Maybe<&2, B.Bank>}337 {Nat.add(cash(acct(b, k)), Bool.pick(Nat, Key.is(sender(s, input), k), spent(form(input), 3n), 0n)) == Nat.add(cash(acct(s, k)), paid(form(input), k, 3n)) : Nat}338339# LAW conservation: no request changes the total money: the vault, and340# every account's cash, credit line and money held. The bank starts as341# Bank.genesis(), with 1,000,000,000 credits in the vault and no account,342# so the total is always that. Balances are natural numbers, so none is343# ever negative.344law conservation:345 for +s: B.Bank346 for +input: String347 {B.Bank.total(after(s, W.Web.serve(s, input))) == B.Bank.total(s) : Nat}348349# LAW join: a request changes the vault only by opening one account,350# which takes exactly 1,100 credits from it: 100 in cash and 1,000 in its351# credit line, with the random key of the input as its key. The vault352# only falls, so it funds at most 909,090 accounts.353law join:354 for +s: B.Bank355 for +input: String356 {B.Bank.vault(after(s, W.Web.serve(s, input))) == B.Bank.vault(s) : Nat} |357 (&k: B.Key() -> Opened(s, after(s, W.Web.serve(s, input)), rand(input), k))358359# LAW atomicity: a request changes the bank only when it succeeds, and then360# it answers 303 See Other. A request that fails changes nothing.361law atomicity:362 for +s: B.Bank363 for +input: String364 for +b: B.Bank365 for e: {change(W.Web.serve(s, input)) == Some{b} : Maybe<&2, B.Bank>}366 {String.starts_with(text(W.Web.serve(s, input)), "HTTP/1.1 303 See Other\r\n") == True{} : Bool}367368# LAW totality: every input gets a reply. Bend accepts a def only when it369# handles every case and its recursion terminates, so this holds of any370# def the checker accepts; it is here to say so.371law totality:372 for +s: B.Bank373 for +input: String374 exs r: W.Reply375 {W.Web.serve(s, input) == r : W.Reply}376377# whether pass is the key of the account m378def keyed(m: Maybe<&2, B.Acc>, pass: String) -> Bool:379 match m:380 case None{}:381 False{}382 case Some{B.Acc{p, cash, note, line, loan, held}}:383 String.eq(p, pass)384385# LAW access: an input acts for an account only through that account's386# name and its own key: if the cookie opens the account at k, the name387# in the cookie is k's, and the key in the cookie is k's key.388law access:389 for +s: B.Bank390 for +input: String391 for +k: B.Key()392 for me: {Key.is(sender(s, input), k) == True{} : Bool}393 {Key.is(B.Key.of(user(input)), k) == True{} : Bool} & {keyed(acct(s, k), key(input)) == True{} : Bool}