1# Bend Bank: the proof of LAW join2# ================================3#4# An exec keeps the vault: a plan's gifts and its account only touch the5# accounts. A successful join opens a new account at the name's key and6# takes 1,100 from the vault. Every other request changes nothing.78import Base9import ../bank.bend as B10import ../web.bend as W11import ../LAWS.bend as Laws12import ./base.bend as L1314# Exec15# ----1617# a bank result that does not fail has the vault v18def Bank.Keeps(r: Result<&2, &2, String, B.Bank>, v: Nat) -> Type:19 L.Bank.If(r, b => {B.Bank.vault(b) == v : Nat})2021# a gift to an account keeps the vault22def Plan.gift_to_keeps(self: Bool, m: Maybe<&2, B.Acc>, +vault: Nat, -accts: B.Trie<B.Acc>, -u: B.Key(), -k: B.Key(), -g: B.Gift, -v: Nat, h: {vault == v : Nat})23 -> Bank.Keeps(B.Plan.gift.to(self, m, vault, accts, u, k, g), v):24 match self m:25 case True{} _:26 Unit{}27 case False{} None{}:28 Unit{}29 case False{} Some{a}:30 h3132# one more gift keeps the vault33def Plan.gift_keeps(r: Result<&2, &2, String, B.Bank>, +u: B.Key(), +g: B.Gift, -v: Nat, h: Bank.Keeps(r, v))34 -> Bank.Keeps(B.Plan.gift(r, u, g), v):35 match r:36 case Fail{e}:37 Unit{}38 case Done{B.Bank{vault, +accts}}:39 +k = B.Gift.dest(g)40 Plan.gift_to_keeps(B.Key.eq(k, u), B.Trie.get(B.Acc, k, accts), vault, accts, u, k, g, v, h)4142# the gifts keep the vault43def Plan.gifts_keeps(gs: List<&2, B.Gift>, +u: B.Key(), +r: Result<&2, &2, String, B.Bank>, -v: Nat, h: Bank.Keeps(r, v))44 -> Bank.Keeps(B.Plan.gifts(gs, u, r), v):45 match gs:46 case Nil{}:47 h48 case +g <> rest:49 Plan.gifts_keeps(rest, u, B.Plan.gift(r, u, g), v, Plan.gift_keeps(r, u, g, v, h))5051# a planned request keeps the vault: it sets accounts only52def Bank.plan_keeps(+v: Nat, +t: B.Trie<B.Acc>, +k: B.Key(), r: Result<&2, &2, String, B.Plan>)53 -> Bank.Keeps(B.Bank.plan(B.Bank{v, t}, k, r), v):54 match r:55 case Fail{e}:56 Unit{}57 case Done{B.Plan{+acct, gifts}}:58 +r = {Done{B.Bank{v, B.Trie.set(B.Acc, k, t, Some{acct})}} : Result<&2, &2, String, B.Bank>}59 Plan.gifts_keeps(gifts, k, r, v, {==})6061# an exec keeps the vault62def Bank.exec_keeps(s: B.Bank, +name: String, +pass: String, +now: Nat, +cmd: B.Cmd) -> Bank.Keeps(B.Bank.exec(s, name, pass, now, cmd), B.Bank.vault(s)):63 match s:64 case B.Bank{+v, +t}:65 L.Bank.exec_by(B.Key.of(name), v, t, pass, now, cmd,66 u => b => {B.Bank.vault(b) == v : Nat},67 u => Unit, Unit{},68 +k => a => eg => r => Bank.plan_keeps(v, t, k, B.Cmd.plan(cmd, a, now)))6970# Join71# ----7273# the law for a bank s2 after s1: the same vault, or one account opened74def Join.Law(s1: B.Bank, s2: B.Bank, pass: String) -> Type:75 {B.Bank.vault(s2) == B.Bank.vault(s1) : Nat} | (&k: B.Key() -> Laws.Opened(s1, s2, pass, k))7677# a bank result that does not fail obeys the law78def Join.Res(s: B.Bank, r: Result<&2, &2, String, B.Bank>, pass: String) -> Type:79 L.Bank.If(r, b => Join.Law(s, b, pass))8081# a result that keeps the vault obeys the law82def Join.keeps(r: Result<&2, &2, String, B.Bank>, -s: B.Bank, -pass: String, h: Bank.Keeps(r, B.Bank.vault(s))) -> Join.Res(s, r, pass):83 match r:84 case Fail{e}:85 Unit{}86 case Done{b}:87 Inl{h}8889# the account set at k is there90def Join.get_new(+k: B.Key(), +t: B.Trie<B.Acc>, +a: B.Acc) -> {B.Trie.get(B.Acc, k, B.Trie.set(B.Acc, k, t, Some{a})) == Some{a} : Maybe<&2, B.Acc>}:91 +m = {Some{a} : Maybe<&2, B.Acc>}92 %L.Trie.get_same(B.Acc, k, t, m) : {_ == m : Maybe<&2, B.Acc>}93 {==}9495# a join obeys the law, with its key as the account's96def Join.bank(s: B.Bank, +name: String, +pass: String) -> Join.Res(s, B.Bank.join(s, name, pass), pass):97 match s:98 case B.Bank{+v, +t}:99 L.Bank.join_by(B.Key.of(name), v, t, pass, b => Join.Law(B.Bank{v, t}, b, pass),100 +k => em => o => Inr{(k, em, Join.get_new(k, t, B.Acc.new(pass)), L.Nat.sub_add(v, 1100n, o))})101102# LAW join103def Laws.join(s, input):104 +rand = Laws.rand(input)105 -P = {b => Join.Law(s, b, rand) : B.Bank -> Type}106 L.Web.reply_by(s, W.Req.parse(input), P, Inl{{==}},107 +name => Join.bank(s, name, rand),108 +cmd => Join.keeps(B.Bank.exec(s, Laws.user(input), Laws.key(input), Laws.time(input), cmd), s, rand,109 Bank.exec_keeps(s, Laws.user(input), Laws.key(input), Laws.time(input), cmd)))