1# Bend Bank: the proof of LAW sound2# =================================3#4# Accounts are never removed; a plan's account only drops what it held;5# a gift puts money only under its sender's name, whose account exists;6# a new account holds nothing.78import Base9import ../bank.bend as B10import ../web.bend as W11import ../LAWS.bend as Laws12import ./base.bend as L1314# Tries15# -----1617# the empty trie holds nothing18def Trie.get_tip(-V: Data, k: B.Key()) -> {B.Trie.get(V, k, B.Tip{}) == None{} : Maybe<&2, V>}:19 match k:20 case Nil{}:21 {==}22 case False{} <> ks:23 Trie.get_tip(V, ks)24 case True{} <> ks:25 Trie.get_tip(V, ks)2627# a pick of an account or x that is nothing is x, which is nothing28def Trie.none_pick(c: Bool, -b: B.Acc, -x: Maybe<&2, B.Acc>, e: {Bool.pick(Maybe<&2, B.Acc>, c, Some{b}, x) == None{} : Maybe<&2, B.Acc>})29 -> {x == None{} : Maybe<&2, B.Acc>}:30 match c:31 case True{}:32 L.Maybe.some_none(B.Acc, b, {x == None{} : Maybe<&2, B.Acc>}, e)33 case False{}:34 e3536# a key that holds nothing after a set to an account held nothing before37def Trie.none_set(+q: B.Key(), +k: B.Key(), +t: B.Trie<B.Acc>, +b: B.Acc, e: {B.Trie.get(B.Acc, q, B.Trie.set(B.Acc, k, t, Some{b})) == None{} : Maybe<&2, B.Acc>})38 -> {B.Trie.get(B.Acc, q, t) == None{} : Maybe<&2, B.Acc>}:39 +x = B.Trie.get(B.Acc, q, t)40 +p = Bool.pick(Maybe<&2, B.Acc>, B.Key.eq(q, k), Some{b}, x)41 +y = B.Trie.get(B.Acc, q, B.Trie.set(B.Acc, k, t, Some{b}))42 Trie.none_pick(B.Key.eq(q, k), b, x, Equal.trans(Maybe<&2, B.Acc>, p, y, None{}, L.Trie.pick_set(B.Acc, q, k, t, Some{b}), e))4344# Sound45# -----4647# every account of t holds money only under the name of an account of t48def Sound.T(t: B.Trie<B.Acc>) -> Type:49 @k: B.Key() -> @q: B.Key() -> {B.Trie.get(B.Acc, q, t) == None{} : Maybe<&2, B.Acc>} -> {B.Acc.locked(B.Trie.get(B.Acc, k, t), q) == None{} : Maybe<&2, Nat>}5051# the account a holds money only under the name of an account of t52def Sound.Held(a: B.Acc, t: B.Trie<B.Acc>) -> Type:53 @q: B.Key() -> {B.Trie.get(B.Acc, q, t) == None{} : Maybe<&2, B.Acc>} -> {B.Acc.locked(Some{a}, q) == None{} : Maybe<&2, Nat>}5455# the account a is sound when t is: a proof that can be used once per56# use of Sound.T(t), as proofs of functions are used at most once57def Sound.If(a: B.Acc, t: B.Trie<B.Acc>) -> Type:58 Sound.T(t) -> Sound.Held(a, t)5960# t has an account at u61def Sound.Has(u: B.Key(), t: B.Trie<B.Acc>) -> Data:62 {Maybe.is_some(&2, B.Acc, B.Trie.get(B.Acc, u, t)) == True{} : Bool}6364# a bank result that does not fail is sound65def Sound.R(r: Result<&2, &2, String, B.Bank>) -> Type:66 L.Bank.If(r, Laws.Sound)6768# the account at k of a sound trie is sound69def Sound.at(+k: B.Key(), +t: B.Trie<B.Acc>, -a: B.Acc, +e: {Some{a} == B.Trie.get(B.Acc, k, t) : Maybe<&2, B.Acc>}) -> Sound.If(a, t):70 hs => q => hq =>71 %Equal.sym(Maybe<&2, B.Acc>, Some{a}, B.Trie.get(B.Acc, k, t), e) : {B.Acc.locked(_, q) == None{} : Maybe<&2, Nat>}72 hs(k, q, hq)7374# the account at j after a set at k is sound: the new one, or the old75def Sound.pick(c: Bool, +j: B.Key(), +q: B.Key(), -t: B.Trie<B.Acc>, -b: B.Acc, hs: Sound.T(t), hb: Sound.If(b, t),76 +hq: {B.Trie.get(B.Acc, q, t) == None{} : Maybe<&2, B.Acc>})77 -> {B.Acc.locked(Bool.pick(Maybe<&2, B.Acc>, c, Some{b}, B.Trie.get(B.Acc, j, t)), q) == None{} : Maybe<&2, Nat>}:78 match c:79 case True{}:80 hb(hs, q, hq)81 case False{}:82 hs(j, q, hq)8384# setting k to a sound account keeps a trie sound85def Sound.set(+k: B.Key(), +t: B.Trie<B.Acc>, +b: B.Acc, hs: Sound.T(t), hb: Sound.If(b, t)) -> Sound.T(B.Trie.set(B.Acc, k, t, Some{b})):86 +j => +q => hq =>87 %L.Trie.pick_set(B.Acc, j, k, t, Some{b}) : {B.Acc.locked(_, q) == None{} : Maybe<&2, Nat>}88 Sound.pick(B.Key.eq(j, k), j, q, t, b, hs, hb, Trie.none_set(q, k, t, b, hq))8990# a pick of an account and an account is an account91def Sound.some_pick(c: Bool, -b: B.Acc, -x: Maybe<&2, B.Acc>, h: {Maybe.is_some(&2, B.Acc, x) == True{} : Bool})92 -> {Maybe.is_some(&2, B.Acc, Bool.pick(Maybe<&2, B.Acc>, c, Some{b}, x)) == True{} : Bool}:93 match c:94 case True{}:95 {==}96 case False{}:97 h9899# a set to an account keeps an account at u100def Sound.keep(+u: B.Key(), +k: B.Key(), +t: B.Trie<B.Acc>, +b: B.Acc, hu: Sound.Has(u, t)) -> Sound.Has(u, B.Trie.set(B.Acc, k, t, Some{b})):101 %L.Trie.pick_set(B.Acc, u, k, t, Some{b}) : {Maybe.is_some(&2, B.Acc, _) == True{} : Bool}102 Sound.some_pick(B.Key.eq(u, k), b, B.Trie.get(B.Acc, u, t), hu)103104# Plan105# ----106107# a planned request that does not fail plans a sound account108def Sound.Plan(r: Result<&2, &2, String, B.Plan>, t: B.Trie<B.Acc>) -> Type:109 match r:110 case Fail{e}:111 Unit112 case Done{B.Plan{a, gifts}}:113 Sound.If(a, t)114115# a need keeps a plan sound116def Sound.need(test: Bool, -text: String, -p: B.Plan, -t: B.Trie<B.Acc>, h: Sound.Plan(Done{p}, t)) -> Sound.Plan(B.Op.need(test, text, p), t):117 match test:118 case True{}:119 h120 case False{}:121 Unit{}122123# what a pick of nothing and nothing holds is nothing124def Sound.none(c: Bool, -y: Maybe<&2, Nat>, h: {y == None{} : Maybe<&2, Nat>}) -> {Bool.pick(Maybe<&2, Nat>, c, None{}, y) == None{} : Maybe<&2, Nat>}:125 match c:126 case True{}:127 {==}128 case False{}:129 h130131# clearing what k held keeps an account sound132def Sound.clear(+k: B.Key(), +held: B.Trie<Nat>, -t: B.Trie<B.Acc>,133 h: @q: B.Key() -> {B.Trie.get(B.Acc, q, t) == None{} : Maybe<&2, B.Acc>} -> {B.Trie.get(Nat, q, held) == None{} : Maybe<&2, Nat>})134 -> @q: B.Key() -> {B.Trie.get(B.Acc, q, t) == None{} : Maybe<&2, B.Acc>} -> {B.Trie.get(Nat, q, B.Trie.put(k, held, 0n)) == None{} : Maybe<&2, Nat>}:135 +q => hq =>136 %L.Trie.pick_set(Nat, q, k, held, None{}) : {_ == None{} : Maybe<&2, Nat>}137 Sound.none(B.Key.eq(q, k), B.Trie.get(Nat, q, held), h(q, hq))138139# every op plans a sound account140def Sound.op(op: B.Op, a: B.Acc, gifts: List<&2, B.Gift>, -t: B.Trie<B.Acc>, h: Sound.If(a, t)) -> Sound.Plan(B.Op.at(op, a, gifts), t):141 match op a:142 case B.Need{test, text} a:143 Sound.need(test, text, B.Plan{a, gifts}, t, h)144 case B.Memo{x} B.Acc{pass, cash, note, line, loan, held}:145 h146 case B.Debt{d} B.Acc{pass, cash, note, line, loan, held}:147 h148 case B.Give{k, +x} B.Acc{pass, +cash, note, line, loan, held}:149 Sound.need(Nat.is_le(x, cash), "you do not have that much", B.Plan{B.Acc{pass, Nat.sub(cash, x), note, line, loan, held}, B.Pay{k, x} <> gifts}, t, h)150 case B.Lock{k, +x} B.Acc{pass, +cash, note, line, loan, held}:151 Sound.need(Nat.is_le(x, cash), "you do not have that much", B.Plan{B.Acc{pass, Nat.sub(cash, x), note, line, loan, held}, B.Owe{k, x} <> gifts}, t, h)152 case B.Open{k} a:153 h154 case B.Drop{+k} B.Acc{pass, cash, note, line, loan, +held}:155 hs => Sound.clear(k, held, t, h(hs))156 case B.Draw{+x} B.Acc{pass, cash, note, +line, loan, held}:157 Sound.need(Nat.is_le(x, line), "the bank has no more credit for you", B.Plan{B.Acc{pass, Nat.add(cash, x), note, Nat.sub(line, x), loan, held}, gifts}, t, h)158 case B.Fund{+x} B.Acc{pass, +cash, note, line, loan, held}:159 Sound.need(Nat.is_le(x, cash), "you do not have that much", B.Plan{B.Acc{pass, Nat.sub(cash, x), note, Nat.add(line, x), loan, held}, gifts}, t, h)160161# a step of a plan keeps it sound162def Sound.step(r: Result<&2, &2, String, B.Plan>, +op: B.Op, -t: B.Trie<B.Acc>, h: Sound.Plan(r, t)) -> Sound.Plan(B.Op.step(r, op), t):163 match r:164 case Fail{e}:165 Unit{}166 case Done{B.Plan{a, gifts}}:167 Sound.op(op, a, gifts, t, h)168169# every op of a plan keeps it sound170def Sound.run(ops: List<&2, B.Op>, +r: Result<&2, &2, String, B.Plan>, -t: B.Trie<B.Acc>, h: Sound.Plan(r, t)) -> Sound.Plan(B.Op.run(ops, r), t):171 match ops:172 case Nil{}:173 h174 case +op <> rest:175 Sound.run(rest, B.Op.step(r, op), t, Sound.step(r, op, t, h))176177# Gifts178# -----179180# the pick of an owe at q is nothing, as q is not u, whose account exists181def Sound.owe(c: Bool, +q: B.Key(), +u: B.Key(), +t: B.Trie<B.Acc>, -x: Maybe<&2, Nat>, -y: Maybe<&2, Nat>, e: {B.Key.eq(q, u) == c : Bool},182 hq: {B.Trie.get(B.Acc, q, t) == None{} : Maybe<&2, B.Acc>}, hu: Sound.Has(u, t), h: {y == None{} : Maybe<&2, Nat>})183 -> {Bool.pick(Maybe<&2, Nat>, c, x, y) == None{} : Maybe<&2, Nat>}:184 match c:185 case True{}:186 -M = Maybe<&2, B.Acc>187 +gq = B.Trie.get(B.Acc, q, t)188 +gu = B.Trie.get(B.Acc, u, t)189 +eq = Equal.cong(B.Key(), M, k => B.Trie.get(B.Acc, k, t), q, u, L.Key.eq_true(q, u, e))190 +eu = Equal.trans(M, None{}, gq, gu, Equal.sym(M, gq, None{}, hq), eq)191 +ef = Equal.cong(M, Bool, m => Maybe.is_some(&2, B.Acc, m), None{}, gu, eu)192 L.Bool.false_true({x == None{} : Maybe<&2, Nat>}, Equal.trans(Bool, False{}, Maybe.is_some(&2, B.Acc, gu), True{}, ef, hu))193 case False{}:194 h195196# a gift from u, whose account exists, keeps an account sound197def Sound.give(g: B.Gift, +u: B.Key(), a: B.Acc, +t: B.Trie<B.Acc>, h: Sound.Held(a, t), +hu: Sound.Has(u, t)) -> Sound.Held(B.Gift.give(g, u, a), t):198 match g a:199 case B.Pay{d, x} B.Acc{pass, cash, note, line, loan, held}:200 h201 case B.Owe{d, +x} B.Acc{pass, cash, note, line, loan, +held}:202 +q => +hq =>203 +n = B.Trie.some(Nat.add(B.Trie.num(u, held), x))204 %L.Trie.pick_set(Nat, q, u, held, n) : {_ == None{} : Maybe<&2, Nat>}205 Sound.owe(B.Key.eq(q, u), q, u, t, n, B.Trie.get(Nat, q, held), {==}, hq, hu, h(q, hq))206 case B.Rel{d} B.Acc{pass, cash, note, line, loan, +held}:207 Sound.clear(u, held, t, h)208209# a bank result that does not fail is sound, with an account at u210def Sound.Gifts(r: Result<&2, &2, String, B.Bank>, u: B.Key()) -> Type:211 match r:212 case Fail{e}:213 Unit214 case Done{B.Bank{v, t}}:215 Sound.T(t) & Sound.Has(u, t)216217# a gift to the account at d keeps a bank sound218def Sound.gift_to(self: Bool, m: Maybe<&2, B.Acc>, +v: Nat, +t: B.Trie<B.Acc>, +u: B.Key(), +d: B.Key(), +g: B.Gift,219 +em: {m == B.Trie.get(B.Acc, d, t) : Maybe<&2, B.Acc>}, hs: Sound.T(t), +hu: Sound.Has(u, t))220 -> Sound.Gifts(B.Plan.gift.to(self, m, v, t, u, d, g), u):221 match self m:222 case True{} _:223 Unit{}224 case False{} None{}:225 Unit{}226 case False{} Some{+a}:227 +b = B.Gift.give(g, u, a)228 hb = {hs => Sound.give(g, u, a, t, Sound.at(d, t, a, em, hs), hu) : Sound.If(b, t)}229 (Sound.set(d, t, b, hs, hb), Sound.keep(u, d, t, b, hu))230231# one more gift keeps a bank result sound232def Sound.gift(r: Result<&2, &2, String, B.Bank>, +u: B.Key(), +g: B.Gift, h: Sound.Gifts(r, u)) -> Sound.Gifts(B.Plan.gift(r, u, g), u):233 match r:234 case Fail{e}:235 Unit{}236 case Done{B.Bank{v, +t}}:237 (hs, hu) = h238 +d = B.Gift.dest(g)239 Sound.gift_to(B.Key.eq(d, u), B.Trie.get(B.Acc, d, t), v, t, u, d, g, {==}, hs, hu)240241# every gift of a plan keeps a bank result sound242def Sound.gifts(gs: List<&2, B.Gift>, +u: B.Key(), +r: Result<&2, &2, String, B.Bank>, h: Sound.Gifts(r, u)) -> Sound.Gifts(B.Plan.gifts(gs, u, r), u):243 match gs:244 case Nil{}:245 h246 case +g <> rest:247 Sound.gifts(rest, u, B.Plan.gift(r, u, g), Sound.gift(r, u, g, h))248249# a sound bank result with an account at u is sound250def Sound.forget(r: Result<&2, &2, String, B.Bank>, -u: B.Key(), h: Sound.Gifts(r, u)) -> Sound.R(r):251 match r:252 case Fail{e}:253 Unit{}254 case Done{B.Bank{v, t}}:255 (hs, hu) = h256 hs257258# Requests259# --------260261# a key holds an account just set at it262def Sound.has_set(+u: B.Key(), +t: B.Trie<B.Acc>, +a: B.Acc) -> Sound.Has(u, B.Trie.set(B.Acc, u, t, Some{a})):263 +m = {Some{a} : Maybe<&2, B.Acc>}264 %L.Trie.get_same(B.Acc, u, t, m) : {Maybe.is_some(&2, B.Acc, _) == True{} : Bool}265 {==}266267# the plan of u, whose account is sound, keeps a trie sound268def Sound.apply(+v: Nat, +t: B.Trie<B.Acc>, +u: B.Key(), p: B.Plan, hs: Sound.T(t), hp: Sound.Plan(Done{p}, t))269 -> Sound.R(B.Plan.apply(B.Bank{v, t}, u, p)):270 match p:271 case B.Plan{+acct, +gifts}:272 +m = {Some{acct} : Maybe<&2, B.Acc>}273 +t1 = B.Trie.set(B.Acc, u, t, m)274 +hu = Sound.has_set(u, t, acct)275 +r = {Done{B.Bank{v, t1}} : Result<&2, &2, String, B.Bank>}276 Sound.forget(B.Plan.gifts(gifts, u, r), u, Sound.gifts(gifts, u, r, (Sound.set(u, t, acct, hs, hp), hu)))277278# a planned request keeps a bank sound279def Sound.plan(+v: Nat, +t: B.Trie<B.Acc>, +u: B.Key(), r: Result<&2, &2, String, B.Plan>, hs: Sound.T(t), hp: Sound.Plan(r, t))280 -> Sound.R(B.Bank.plan(B.Bank{v, t}, u, r)):281 match r:282 case Fail{e}:283 Unit{}284 case Done{p}:285 Sound.apply(v, t, u, p, hs, hp)286287# a command keeps a bank sound288def Sound.exec(s: B.Bank, +user: String, +key: String, +now: Nat, +cmd: B.Cmd, h: Laws.Sound(s)) -> Sound.R(B.Bank.exec(s, user, key, now, cmd)):289 match s:290 case B.Bank{+v, +t}:291 L.Bank.exec_by(B.Key.of(user), v, t, key, now, cmd, u => Laws.Sound, u => Unit, Unit{},292 +u => +a => eg => r => Sound.plan(v, t, u, B.Cmd.plan(cmd, a, now), h,293 Sound.run(B.Cmd.ops(cmd, a, now), Done{B.Plan{a, Nil{}}}, t, Sound.at(u, t, a, eg))))294295# a join keeps a bank sound296def Sound.join(s: B.Bank, +name: String, +pass: String, h: Laws.Sound(s)) -> Sound.R(B.Bank.join(s, name, pass)):297 match s:298 case B.Bank{+v, +t}:299 L.Bank.join_by(B.Key.of(name), v, t, pass, Laws.Sound,300 +k => em => o => Sound.set(k, t, B.Acc.new(pass), h, hs => q => hq => Trie.get_tip(Nat, q)))301302# Web303# ---304305# a result that is sound when s is: its bank is sound when s is306def Sound.imp(r: Result<&2, &2, String, B.Bank>, -s: B.Bank, h: Laws.Sound(s) -> Sound.R(r))307 -> L.Bank.If(r, b => Laws.Sound(s) -> Laws.Sound(b)):308 match r:309 case Fail{e}:310 Unit{}311 case Done{b}:312 h313314# LAW sound315def Laws.sound(s, input, ok):316 +rand = Laws.rand(input)317 +user = Laws.user(input)318 +key = Laws.key(input)319 +time = Laws.time(input)320 -P = {b => Laws.Sound(s) -> Laws.Sound(b) : B.Bank -> Type}321 h = L.Web.reply_by(s, W.Req.parse(input), P, h => h,322 +name => Sound.imp(B.Bank.join(s, name, rand), s, h => Sound.join(s, name, rand, h)),323 +cmd => Sound.imp(B.Bank.exec(s, user, key, time, cmd), s, h => Sound.exec(s, user, key, time, cmd, h)))324 h(ok)