1# Bend Bank: the proof of LAW escrow2# ==================================3#4# Take the sender uk and another key q. Of all ops, only Drop{q} lowers5# what q holds in the plan's account, and it adds the gift Pay{q} of6# that amount; so what q holds there, plus the Pay cash of the gifts to7# q, never falls (Op.run_grows). The plan's account is uk's final8# account, since a gift to uk itself fails; and the gifts add at least9# their Pay cash to q's cash (Esc.gifts). A join keeps both accounts10# (LAW authority, Keep.join).1112import Base13import ../bank.bend as B14import ../web.bend as W15import ../LAWS.bend as Laws16import ./base.bend as L17import ./authority.bend as A1819# Gift20# ----2122# a gift to another account pays q nothing23def Gift.pay_other(g: B.Gift, +q: B.Key(),24 e: {B.Key.eq(B.Gift.dest(g), q) == False{} : Bool}) -> {L.Gift.pay(g, q) == 0n : Nat}:25 match g:26 case B.Pay{d, x}:27 %Equal.sym(Bool, B.Key.eq(d, q), False{}, e) : {Bool.pick(Nat, _, x, 0n) == 0n : Nat}28 {==}29 case B.Owe{d, x}:30 {==}31 case B.Rel{d}:32 {==}3334# a gift to q's account adds at least its pay to the cash35def Gift.pay_cash(g: B.Gift, +uk: B.Key(), a: B.Acc, +q: B.Key(),36 e: {B.Key.eq(B.Gift.dest(g), q) == True{} : Bool})37 -> Laws.LE(Nat.add(Laws.cash(Some{a}), L.Gift.pay(g, q)), Laws.cash(Some{B.Gift.give(g, uk, a)})):38 match g a:39 case B.Pay{d, +x} B.Acc{pass, +cash, note, line, loan, held}:40 %Equal.sym(Bool, B.Key.eq(d, q), True{}, e) : Laws.LE(Nat.add(cash, Bool.pick(Nat, _, x, 0n)), Nat.add(cash, x))41 L.Nat.le_refl(Nat.add(cash, x))42 case B.Owe{d, x} B.Acc{pass, +cash, note, line, loan, held}:43 %L.Nat.add_zero(cash) : Laws.LE(_, cash)44 L.Nat.le_refl(cash)45 case B.Rel{d} B.Acc{pass, +cash, note, line, loan, +held}:46 %L.Nat.add_zero(cash) : Laws.LE(_, Nat.add(cash, B.Trie.num(uk, held)))47 L.Nat.le_add(cash, B.Trie.num(uk, held))4849# Op50# --5152# what q holds in a plan's account, plus what its gifts pay q53def Plan.val(p: B.Plan, +q: B.Key()) -> Nat:54 match p:55 case B.Plan{acct, gifts}:56 Nat.add(Laws.held(Some{acct}, q), L.Gift.paid(gifts, q))5758# a planned request that does not fail has a value of at least n59def Plan.Grows(r: Result<&2, &2, String, B.Plan>, q: B.Key(), n: Nat) -> Type:60 match r:61 case Fail{e}:62 Unit63 case Done{p}:64 Laws.LE(n, Plan.val(p, q))6566def Op.need_grows(test: Bool, -text: String, -p: B.Plan, -q: B.Key(), -n: Nat,67 h: Laws.LE(n, Plan.val(p, q)))68 -> Plan.Grows(B.Op.need(test, text, p), q, n):69 match test:70 case True{}:71 h72 case False{}:73 Unit{}7475# a Pay adds to the value76def Op.give_le(+h: Nat, +y: Nat, +g: Nat) -> Laws.LE(Nat.add(h, g), Nat.add(h, Nat.add(y, g))):77 %L.Nat.add_comm(g, y) : Laws.LE(Nat.add(h, g), Nat.add(h, _))78 L.Nat.le_addl(h, g, Nat.add(g, y), L.Nat.le_add(g, y))7980# a Drop at k moves what q held there into its pay81def Op.drop_at(c: Bool, +q: B.Key(), +k: B.Key(), +held: B.Trie<Nat>, +g: Nat,82 ec: {B.Key.eq(k, q) == c : Bool})83 -> {Nat.add(B.Trie.num(q, held), g) == Nat.add(B.Trie.amount(Bool.pick(Maybe<&2, Nat>, c, None{}, B.Trie.get(Nat, q, held))), Nat.add(Bool.pick(Nat, c, B.Trie.num(k, held), 0n), g)) : Nat}:84 match c:85 case True{}:86 %L.Key.eq_true(k, q, ec) : {Nat.add(B.Trie.num(_, held), g) == Nat.add(B.Trie.num(k, held), g) : Nat}87 {==}88 case False{}:89 {==}9091def Op.drop(+k: B.Key(), +q: B.Key(), +held: B.Trie<Nat>, +g: Nat)92 -> {Nat.add(B.Trie.num(q, held), g) == Nat.add(B.Trie.num(q, B.Trie.put(k, held, 0n)), Nat.add(L.Gift.pay(B.Pay{k, B.Trie.num(k, held)}, q), g)) : Nat}:93 +n = Nat.add(B.Trie.num(q, held), g)94 +y = Nat.add(L.Gift.pay(B.Pay{k, B.Trie.num(k, held)}, q), g)95 %L.Trie.pick_set(Nat, q, k, held, None{}) : {n == Nat.add(B.Trie.amount(_), y) : Nat}96 %L.Key.eq_sym(k, q) : {n == Nat.add(B.Trie.amount(Bool.pick(Maybe<&2, Nat>, _, None{}, B.Trie.get(Nat, q, held))), y) : Nat}97 Op.drop_at(B.Key.eq(k, q), q, k, held, g, {==})9899# every op keeps the value of at least n100def Op.at_grows(op: B.Op, a: B.Acc, +gifts: List<&2, B.Gift>, +q: B.Key(), +n: Nat,101 h: Laws.LE(n, Plan.val(B.Plan{a, gifts}, q)))102 -> Plan.Grows(B.Op.at(op, a, gifts), q, n):103 match op a:104 case B.Need{test, text} a:105 Op.need_grows(test, text, B.Plan{a, gifts}, q, n, h)106 case B.Memo{t} B.Acc{pass, cash, note, line, loan, held}:107 h108 case B.Debt{d} B.Acc{pass, cash, note, line, loan, held}:109 h110 case B.Give{+k, +x} B.Acc{pass, +cash, note, line, loan, +held}:111 +p = {B.Plan{B.Acc{pass, Nat.sub(cash, x), note, line, loan, held}, B.Pay{k, x} <> gifts} : B.Plan}112 +hn = B.Trie.num(q, held)113 +g = L.Gift.paid(gifts, q)114 +y = L.Gift.pay(B.Pay{k, x}, q)115 h2 = L.Nat.le_trans(n, Nat.add(hn, g), Nat.add(hn, Nat.add(y, g)), h, Op.give_le(hn, y, g))116 Op.need_grows(Nat.is_le(x, cash), "you do not have that much", p, q, n, h2)117 case B.Lock{k, +x} B.Acc{pass, +cash, note, line, loan, held}:118 +p = {B.Plan{B.Acc{pass, Nat.sub(cash, x), note, line, loan, held}, B.Owe{k, x} <> gifts} : B.Plan}119 Op.need_grows(Nat.is_le(x, cash), "you do not have that much", p, q, n, h)120 case B.Open{k} a:121 h122 case B.Drop{+k} B.Acc{pass, cash, note, line, loan, +held}:123 %Op.drop(k, q, held, L.Gift.paid(gifts, q)) : Laws.LE(n, _)124 h125 case B.Draw{+x} B.Acc{pass, cash, note, +line, loan, held}:126 +p = {B.Plan{B.Acc{pass, Nat.add(cash, x), note, Nat.sub(line, x), loan, held}, gifts} : B.Plan}127 Op.need_grows(Nat.is_le(x, line), "the bank has no more credit for you", p, q, n, h)128 case B.Fund{+x} B.Acc{pass, +cash, note, line, loan, held}:129 +p = {B.Plan{B.Acc{pass, Nat.sub(cash, x), note, Nat.add(line, x), loan, held}, gifts} : B.Plan}130 Op.need_grows(Nat.is_le(x, cash), "you do not have that much", p, q, n, h)131132def Op.step_grows(r: Result<&2, &2, String, B.Plan>, +op: B.Op, +q: B.Key(), +n: Nat,133 h: Plan.Grows(r, q, n))134 -> Plan.Grows(B.Op.step(r, op), q, n):135 match r:136 case Fail{e}:137 Unit{}138 case Done{B.Plan{a, gifts}}:139 Op.at_grows(op, a, gifts, q, n, h)140141def Op.run_grows(ops: List<&2, B.Op>, +r: Result<&2, &2, String, B.Plan>, +q: B.Key(), +n: Nat,142 h: Plan.Grows(r, q, n))143 -> Plan.Grows(B.Op.run(ops, r), q, n):144 match ops:145 case Nil{}:146 h147 case +op <> rest:148 Op.run_grows(rest, B.Op.step(r, op), q, n, Op.step_grows(r, op, q, n, h))149150# Esc151# ---152153# what q holds in the account at k, and q's cash154def Esc.sum(+s: B.Bank, +k: B.Key(), +q: B.Key()) -> Nat:155 Nat.add(Laws.held(Laws.acct(s, k), q), Laws.cash(Laws.acct(s, q)))156157# a bank result that does not fail has a sum of at least n158def Esc.R(n: Nat, r: Result<&2, &2, String, B.Bank>, k: B.Key(), q: B.Key()) -> Type:159 L.Bank.If(r, +b => Laws.LE(n, Esc.sum(b, k, q)))160161# the same, with the pay of the gifts gs still to give162def Esc.G(r: Result<&2, &2, String, B.Bank>, gs: List<&2, B.Gift>, k: B.Key(), +q: B.Key(),163 n: Nat) -> Type:164 L.Bank.If(r, +b => Laws.LE(n, Nat.add(Laws.held(Laws.acct(b, k), q), Nat.add(Laws.cash(Laws.acct(b, q)), L.Gift.paid(gs, q)))))165166# h0 + c <= h1 + (c + g), when h0 <= h1 + g167def Esc.start(+h0: Nat, +h1: Nat, +c: Nat, +g: Nat,168 h: Laws.LE(h0, Nat.add(h1, g))) -> Laws.LE(Nat.add(h0, c), Nat.add(h1, Nat.add(c, g))):169 %L.Nat.add_assoc(h1, c, g) : Laws.LE(Nat.add(h0, c), _)170 %L.Nat.right_comm(h1, g, c) : Laws.LE(Nat.add(h0, c), _)171 L.Nat.le_addr(h0, Nat.add(h1, g), c, h)172173# c + (y + g) <= c2 + g, when c + y <= c2174def Esc.pay_le(+c: Nat, +y: Nat, +c2: Nat, +g: Nat,175 le: Laws.LE(Nat.add(c, y), c2)) -> Laws.LE(Nat.add(c, Nat.add(y, g)), Nat.add(c2, g)):176 %L.Nat.add_assoc(c, y, g) : Laws.LE(_, Nat.add(c2, g))177 L.Nat.le_addr(Nat.add(c, y), c2, g, le)178179# n <= h + (c2 + g), when n <= h + (c + (y + g)) and c + y <= c2180def Esc.more(+n: Nat, +h: Nat, +c: Nat, +y: Nat, +c2: Nat, +g: Nat,181 e: Laws.LE(n, Nat.add(h, Nat.add(c, Nat.add(y, g)))), le: Laws.LE(Nat.add(c, y), c2))182 -> Laws.LE(n, Nat.add(h, Nat.add(c2, g))):183 +x = Nat.add(c, Nat.add(y, g))184 +z = Nat.add(c2, g)185 L.Nat.le_trans(n, Nat.add(h, x), Nat.add(h, z), e, L.Nat.le_addl(h, x, z, Esc.pay_le(c, y, c2, g, le)))186187# a gift to the account a at q adds at least its pay to q's cash188def Esc.cash_at(+q: B.Key(), +accts: B.Trie<B.Acc>, +uk: B.Key(), +g: B.Gift, +a: B.Acc,189 +ec: {B.Key.eq(q, B.Gift.dest(g)) == True{} : Bool},190 em: {B.Trie.get(B.Acc, B.Gift.dest(g), accts) == Some{a} : Maybe<&2, B.Acc>})191 -> Laws.LE(Nat.add(Laws.cash(B.Trie.get(B.Acc, q, accts)), L.Gift.pay(g, q)), Laws.cash(Some{B.Gift.give(g, uk, a)})):192 +d = B.Gift.dest(g)193 +y = L.Gift.pay(g, q)194 +c1 = Laws.cash(Some{B.Gift.give(g, uk, a)})195 %Equal.sym(B.Key(), q, d, L.Key.eq_true(q, d, ec)) : Laws.LE(Nat.add(Laws.cash(B.Trie.get(B.Acc, _, accts)), y), c1)196 %Equal.sym(Maybe<&2, B.Acc>, B.Trie.get(B.Acc, d, accts), Some{a}, em) : Laws.LE(Nat.add(Laws.cash(_), y), c1)197 Gift.pay_cash(g, uk, a, q, L.Key.flip(q, d, True{}, ec))198199# the cash at q after a gift g to the account a200def Esc.gift_at(c: Bool, +q: B.Key(), +accts: B.Trie<B.Acc>, +uk: B.Key(), +g: B.Gift,201 +a: B.Acc, +h: Nat, +rest: List<&2, B.Gift>, +n: Nat,202 ec: {B.Key.eq(q, B.Gift.dest(g)) == c : Bool},203 em: {B.Trie.get(B.Acc, B.Gift.dest(g), accts) == Some{a} : Maybe<&2, B.Acc>},204 e: Laws.LE(n, Nat.add(h, Nat.add(Laws.cash(B.Trie.get(B.Acc, q, accts)), Nat.add(L.Gift.pay(g, q), L.Gift.paid(rest, q))))))205 -> Laws.LE(n, Nat.add(h, Nat.add(Laws.cash(Bool.pick(Maybe<&2, B.Acc>, c, Some{B.Gift.give(g, uk, a)}, B.Trie.get(B.Acc, q, accts))), L.Gift.paid(rest, q)))):206 match c:207 case True{}:208 +y = L.Gift.pay(g, q)209 +r = L.Gift.paid(rest, q)210 +c0 = Laws.cash(B.Trie.get(B.Acc, q, accts))211 +c1 = Laws.cash(Some{B.Gift.give(g, uk, a)})212 Esc.more(n, h, c0, y, c1, r, e, Esc.cash_at(q, accts, uk, g, a, ec, em))213 case False{}:214 +r = L.Gift.paid(rest, q)215 %Gift.pay_other(g, q, L.Key.flip(q, B.Gift.dest(g), False{}, ec)) : Laws.LE(n, Nat.add(h, Nat.add(Laws.cash(B.Trie.get(B.Acc, q, accts)), Nat.add(_, r))))216 e217218def Esc.gift_to(c: Bool, m: Maybe<&2, B.Acc>, +vault: Nat, +accts: B.Trie<B.Acc>, +uk: B.Key(),219 +g: B.Gift, +rest: List<&2, B.Gift>, +q: B.Key(), +n: Nat,220 ec: {B.Key.eq(B.Gift.dest(g), uk) == c : Bool},221 em: {B.Trie.get(B.Acc, B.Gift.dest(g), accts) == m : Maybe<&2, B.Acc>},222 e: Esc.G(Done{B.Bank{vault, accts}}, g <> rest, uk, q, n))223 -> Esc.G(B.Plan.gift.to(c, m, vault, accts, uk, B.Gift.dest(g), g), rest, uk, q, n):224 match c m:225 case True{} _:226 Unit{}227 case False{} None{}:228 Unit{}229 case False{} Some{+a}:230 +d = B.Gift.dest(g)231 +t1 = B.Trie.set(B.Acc, d, accts, Some{B.Gift.give(g, uk, a)})232 +r = L.Gift.paid(rest, q)233 +h = Laws.held(B.Trie.get(B.Acc, uk, accts), q)234 %L.Trie.get_other(B.Acc, uk, d, accts, Some{B.Gift.give(g, uk, a)}, L.Key.flip(d, uk, False{}, ec)) : Laws.LE(n, Nat.add(Laws.held(_, q), Nat.add(Laws.cash(B.Trie.get(B.Acc, q, t1)), r)))235 %L.Trie.pick_set(B.Acc, q, d, accts, Some{B.Gift.give(g, uk, a)}) : Laws.LE(n, Nat.add(h, Nat.add(Laws.cash(_), r)))236 Esc.gift_at(B.Key.eq(q, d), q, accts, uk, g, a, h, rest, n, {==}, em, e)237238# a gift from uk keeps uk's account, and adds its pay to q's cash239def Esc.gift(r: Result<&2, &2, String, B.Bank>, +uk: B.Key(), +g: B.Gift,240 +rest: List<&2, B.Gift>, +q: B.Key(), +n: Nat, e: Esc.G(r, g <> rest, uk, q, n))241 -> Esc.G(B.Plan.gift(r, uk, g), rest, uk, q, n):242 match r:243 case Fail{x}:244 Unit{}245 case Done{B.Bank{vault, +accts}}:246 +d = B.Gift.dest(g)247 Esc.gift_to(B.Key.eq(d, uk), B.Trie.get(B.Acc, d, accts), vault, accts, uk, g, rest, q, n, {==}, {==}, e)248249def Esc.gifts(gs: List<&2, B.Gift>, +uk: B.Key(), +r: Result<&2, &2, String, B.Bank>,250 +q: B.Key(), +n: Nat, e: Esc.G(r, gs, uk, q, n))251 -> Esc.G(B.Plan.gifts(gs, uk, r), Nil{}, uk, q, n):252 match gs:253 case Nil{}:254 e255 case +g <> +rest:256 Esc.gifts(rest, uk, B.Plan.gift(r, uk, g), q, n, Esc.gift(r, uk, g, rest, q, n, e))257258# with no gifts left, the sum is the sum259def Esc.end(r: Result<&2, &2, String, B.Bank>, +k: B.Key(), +q: B.Key(), -n: Nat,260 e: Esc.G(r, Nil{}, k, q, n)) -> Esc.R(n, r, k, q):261 match r:262 case Fail{x}:263 Unit{}264 case Done{+b}:265 +h = Laws.held(Laws.acct(b, k), q)266 %L.Nat.zero_r(Laws.cash(Laws.acct(b, q))) : Laws.LE(n, Nat.add(h, _))267 e268269# setting uk's account to the plan's starts the gifts at the plan's value270def Esc.first(+v: Nat, +t: B.Trie<B.Acc>, +uk: B.Key(), +acct: B.Acc, +gifts: List<&2, B.Gift>,271 +q: B.Key(), +a: B.Acc, eg: {Some{a} == B.Trie.get(B.Acc, uk, t) : Maybe<&2, B.Acc>},272 ne: {B.Key.eq(q, uk) == False{} : Bool},273 e: Laws.LE(Laws.held(Some{a}, q), Plan.val(B.Plan{acct, gifts}, q)))274 -> Esc.G(Done{B.Bank{v, B.Trie.set(B.Acc, uk, t, Some{acct})}}, gifts, uk, q, Esc.sum(B.Bank{v, t}, uk, q)):275 +g = L.Gift.paid(gifts, q)276 +t1 = B.Trie.set(B.Acc, uk, t, Some{acct})277 +h1 = Laws.held(Some{acct}, q)278 +c0 = Laws.cash(B.Trie.get(B.Acc, q, t))279 +h0 = Laws.held(B.Trie.get(B.Acc, uk, t), q)280 %L.Trie.get_same(B.Acc, uk, t, Some{acct}) : Laws.LE(Nat.add(h0, c0), Nat.add(Laws.held(_, q), Nat.add(Laws.cash(B.Trie.get(B.Acc, q, t1)), g)))281 %L.Trie.get_other(B.Acc, q, uk, t, Some{acct}, ne) : Laws.LE(Nat.add(h0, c0), Nat.add(h1, Nat.add(Laws.cash(_), g)))282 %eg : Laws.LE(Nat.add(Laws.held(_, q), c0), Nat.add(h1, Nat.add(c0, g)))283 Esc.start(Laws.held(Some{a}, q), h1, c0, g, e)284285def Esc.apply(+v: Nat, +t: B.Trie<B.Acc>, +uk: B.Key(), p: B.Plan, +q: B.Key(), +a: B.Acc,286 eg: {Some{a} == B.Trie.get(B.Acc, uk, t) : Maybe<&2, B.Acc>},287 ne: {B.Key.eq(q, uk) == False{} : Bool}, e: Laws.LE(Laws.held(Some{a}, q), Plan.val(p, q)))288 -> Esc.R(Esc.sum(B.Bank{v, t}, uk, q), B.Plan.apply(B.Bank{v, t}, uk, p), uk, q):289 match p:290 case B.Plan{+acct, +gifts}:291 +n = Esc.sum(B.Bank{v, t}, uk, q)292 +r = {Done{B.Bank{v, B.Trie.set(B.Acc, uk, t, Some{acct})}} : Result<&2, &2, String, B.Bank>}293 h = Esc.first(v, t, uk, acct, gifts, q, a, eg, ne, e)294 Esc.end(B.Plan.gifts(gifts, uk, r), uk, q, n, Esc.gifts(gifts, uk, r, q, n, h))295296def Esc.plan(+v: Nat, +t: B.Trie<B.Acc>, +uk: B.Key(), r: Result<&2, &2, String, B.Plan>,297 +q: B.Key(), +a: B.Acc, eg: {Some{a} == B.Trie.get(B.Acc, uk, t) : Maybe<&2, B.Acc>},298 ne: {B.Key.eq(q, uk) == False{} : Bool}, e: Plan.Grows(r, q, Laws.held(Some{a}, q)))299 -> Esc.R(Esc.sum(B.Bank{v, t}, uk, q), B.Bank.plan(B.Bank{v, t}, uk, r), uk, q):300 match r:301 case Fail{x}:302 Unit{}303 case Done{p}:304 Esc.apply(v, t, uk, p, q, a, eg, ne, e)305306# Exec307# ----308309# q is not k, and k is uk, so q is not uk310def Esc.ne(+q: B.Key(), -uk: B.Key(), -k: B.Key(), ek: {uk == k : B.Key()},311 no: {B.Key.eq(q, k) == False{} : Bool}) -> {B.Key.eq(q, uk) == False{} : Bool}:312 %Equal.sym(B.Key(), uk, k, ek) : {B.Key.eq(q, _) == False{} : Bool}313 no314315# the sender uk is k, the holder of a316def Esc.sent(+v: Nat, +t: B.Trie<B.Acc>, +uk: B.Key(), +a: B.Acc, +now: Nat, +cmd: B.Cmd, +k: B.Key(), +q: B.Key(),317 eg: {Some{a} == B.Trie.get(B.Acc, uk, t) : Maybe<&2, B.Acc>}, me: {B.Key.eq(uk, k) == True{} : Bool},318 no: {B.Key.eq(q, k) == False{} : Bool})319 -> Esc.R(Esc.sum(B.Bank{v, t}, k, q), B.Bank.plan(B.Bank{v, t}, uk, B.Cmd.plan(cmd, a, now)), k, q):320 +ek = L.Key.eq_true(uk, k, me)321 +r = B.Cmd.plan(cmd, a, now)322 +h = Laws.held(Some{a}, q)323 e = Op.run_grows(B.Cmd.ops(cmd, a, now), Done{B.Plan{a, Nil{}}}, q, h, L.Nat.le_add(h, 0n))324 ne = Esc.ne(q, uk, k, ek, no)325 %ek : Esc.R(Esc.sum(B.Bank{v, t}, _, q), B.Bank.plan(B.Bank{v, t}, uk, r), _, q)326 Esc.plan(v, t, uk, r, q, a, eg, ne, e)327328# a command of k keeps what q holds at k, plus q's cash329def Esc.exec(s: B.Bank, +name: String, +pass: String, +now: Nat, +cmd: B.Cmd, +k: B.Key(),330 +q: B.Key(), me: {Laws.Key.is(Laws.Bank.sender(s, name, pass), k) == True{} : Bool},331 no: {B.Key.eq(q, k) == False{} : Bool})332 -> Esc.R(Esc.sum(s, k, q), B.Bank.exec(s, name, pass, now, cmd), k, q):333 match s:334 case B.Bank{+v, +t}:335 L.Bank.exec_by(B.Key.of(name), v, t, pass, now, cmd,336 u => +b => Laws.LE(Esc.sum(B.Bank{v, t}, k, q), Esc.sum(b, k, q)),337 u => {Laws.Key.is(u, k) == True{} : Bool}, me,338 +uk => +a => eg => me => Esc.sent(v, t, uk, a, now, cmd, k, q, eg, me, no))339340# Join341# ----342343# what u's request keeps, it keeps of q's money344def Esc.held_kept(m0: Maybe<&2, B.Acc>, m1: Maybe<&2, B.Acc>, +q: B.Key(),345 h: Laws.Kept(m0, m1, None{}))346 -> Laws.LE(Laws.held(m0, q), Laws.held(m1, q)):347 match m0 m1:348 case None{} _:349 L.Nat.le_add(0n, Laws.held(m1, q))350 case Some{a} None{}:351 match h:352 case Some{B.Acc{p1, c1, n1, l1, d1, +w1}} Some{B.Acc{p2, c2, n2, l2, d2, +w2}}:353 (ep, en, el, ed, le, f, g) = h354 %g(q, {==}) : Laws.LE(_, B.Trie.num(q, w2))355 L.Nat.le_refl(B.Trie.num(q, w2))356357def Esc.cash_kept(m0: Maybe<&2, B.Acc>, m1: Maybe<&2, B.Acc>, -u: Maybe<&2, B.Key()>,358 h: Laws.Kept(m0, m1, u))359 -> Laws.LE(Laws.cash(m0), Laws.cash(m1)):360 match m0 m1:361 case None{} _:362 L.Nat.le_add(0n, Laws.cash(m1))363 case Some{a} None{}:364 match h:365 case Some{B.Acc{p1, c1, n1, l1, d1, w1}} Some{B.Acc{p2, c2, n2, l2, d2, w2}}:366 (ep, en, el, ed, le, f, g) = h367 le368369def Esc.kept(r: Result<&2, &2, String, B.Bank>, +s: B.Bank, +k: B.Key(), +q: B.Key(),370 hk: A.Keep.R(Laws.acct(s, k), r, k, None{}), hq: A.Keep.R(Laws.acct(s, q), r, q, None{}))371 -> Esc.R(Esc.sum(s, k, q), r, k, q):372 match r:373 case Fail{x}:374 Unit{}375 case Done{+b}:376 +h0 = Laws.held(Laws.acct(s, k), q)377 +h1 = Laws.held(Laws.acct(b, k), q)378 +c0 = Laws.cash(Laws.acct(s, q))379 +c1 = Laws.cash(Laws.acct(b, q))380 e1 = Esc.held_kept(Laws.acct(s, k), Laws.acct(b, k), q, hk)381 e2 = Esc.cash_kept(Laws.acct(s, q), Laws.acct(b, q), None{}, hq)382 L.Nat.le_mono(h0, h1, c0, c1, e1, e2)383384def Esc.join(+s: B.Bank, +name: String, +pass: String, +k: B.Key(),385 +q: B.Key()) -> Esc.R(Esc.sum(s, k, q), B.Bank.join(s, name, pass), k, q):386 hk = A.Keep.join(s, name, pass, k, None{})387 hq = A.Keep.join(s, name, pass, q, None{})388 Esc.kept(B.Bank.join(s, name, pass), s, k, q, hk, hq)389390# LAW escrow391def Laws.escrow(s, input, k, q, me, no):392 +n = Esc.sum(s, k, q)393 -P = {b => Laws.LE(n, Esc.sum(b, k, q)) : B.Bank -> Type}394 L.Web.reply_by(s, W.Req.parse(input), P, L.Nat.le_refl(n),395 +name => Esc.join(s, name, Laws.rand(input), k, q),396 +cmd => Esc.exec(s, Laws.user(input), Laws.key(input), Laws.time(input), cmd, k, q, me, no))