1# Bend Bank: the proof of LAW loan2# ================================3#4# A request changes its sender's account only through the plan of its5# command: Plan.apply sets the sender's account to the plan's, and no6# gift reaches it after, since a gift to the sender fails (Self). So the7# proof follows the ops of each command (Loan): every command but Lend8# and Back runs only ops that keep the loan and the line, and Lend and9# Back are followed op by op. A join keeps every account that existed,10# with its loan and line (Keep.join, of LAW authority), and the other11# requests change no account (Web.reply_by).1213import Base14import ../bank.bend as B15import ../web.bend as W16import ../LAWS.bend as Laws17import ./base.bend as L18import ./authority.bend as A1920# Self21# ----2223# a bank result that does not fail has the account acct at u24def Self.R(r: Result<&2, &2, String, B.Bank>, u: B.Key(), acct: B.Acc) -> Type:25 L.Bank.If(r, b => {Some{acct} == Laws.acct(b, u) : Maybe<&2, B.Acc>})2627# a gift from u to the account m at d is not to u, so it keeps u's28# account29def Self.gift_to(self: Bool, m: Maybe<&2, B.Acc>, +vault: Nat, +accts: B.Trie<B.Acc>, +u: B.Key(),30 +d: B.Key(), +g: B.Gift, -acct: B.Acc, es: {B.Key.eq(d, u) == self : Bool},31 h: {Some{acct} == B.Trie.get(B.Acc, u, accts) : Maybe<&2, B.Acc>})32 -> Self.R(B.Plan.gift.to(self, m, vault, accts, u, d, g), u, acct):33 match self m:34 case True{} _:35 Unit{}36 case False{} None{}:37 Unit{}38 case False{} Some{a}:39 +b = {Some{B.Gift.give(g, u, a)} : Maybe<&2, B.Acc>}40 %L.Trie.get_other(B.Acc, u, d, accts, b,41 L.Key.flip(d, u, False{}, es)) : {Some{acct} == _ : Maybe<&2, B.Acc>}42 h4344# one more gift keeps u's account45def Self.gift(r: Result<&2, &2, String, B.Bank>, +u: B.Key(), +g: B.Gift, -acct: B.Acc,46 h: Self.R(r, u, acct))47 -> Self.R(B.Plan.gift(r, u, g), u, acct):48 match r:49 case Fail{e}:50 Unit{}51 case Done{B.Bank{vault, +accts}}:52 +d = B.Gift.dest(g)53 Self.gift_to(B.Key.eq(d, u), B.Trie.get(B.Acc, d, accts), vault, accts, u, d, g, acct, {==},54 h)5556# the gifts keep u's account57def Self.gifts(gs: List<&2, B.Gift>, +u: B.Key(), +r: Result<&2, &2, String, B.Bank>, -acct: B.Acc,58 h: Self.R(r, u, acct))59 -> Self.R(B.Plan.gifts(gs, u, r), u, acct):60 match gs:61 case Nil{}:62 h63 case +g <> rest:64 Self.gifts(rest, u, B.Plan.gift(r, u, g), acct, Self.gift(r, u, g, acct, h))6566# a plan of u leaves u with the plan's account67def Self.apply(+v: Nat, +t: B.Trie<B.Acc>, +u: B.Key(), +acct: B.Acc, gifts: List<&2, B.Gift>)68 -> Self.R(B.Plan.apply(B.Bank{v, t}, u, B.Plan{acct, gifts}), u, acct):69 +r = {Done{B.Bank{v, B.Trie.set(B.Acc, u, t, Some{acct})}} : Result<&2, &2, String, B.Bank>}70 Self.gifts(gifts, u, r, acct, L.Trie.get_same(B.Acc, u, t, Some{acct}))7172# Loan73# ----7475# a planned request that does not fail has the loan d and the line l76def Loan.Is(r: Result<&2, &2, String, B.Plan>, d: B.Loan, l: Nat) -> Type:77 match r:78 case Fail{e}:79 Unit80 case Done{B.Plan{B.Acc{pass, cash, note, line, loan, held}, gifts}}:81 {loan == d : B.Loan} & {line == l : Nat}8283# a planned request that does not fail took a Step from the account a84def Loan.P(a: B.Acc, r: Result<&2, &2, String, B.Plan>, now: Nat) -> Type:85 match r:86 case Fail{e}:87 Unit88 case Done{B.Plan{b, gifts}}:89 Laws.Step(a, b, now)9091# an op that keeps the loan and the line: a calm op92def Op.Calm(op: B.Op) -> Type:93 match op:94 case B.Debt{loan}:95 Empty96 case B.Draw{cash}:97 Empty98 case B.Fund{cash}:99 Empty100 case o:101 Unit102103# ops that are all calm104def Op.Calms(ops: List<&2, B.Op>) -> Type:105 match ops:106 case Nil{}:107 Unit108 case op <> rest:109 Op.Calm(op) & Op.Calms(rest)110111# a need keeps the plan, or fails112def Loan.need(test: Bool, -text: String, -p: B.Plan, -d: B.Loan, -l: Nat, h: Loan.Is(Done{p}, d, l))113 -> Loan.Is(B.Op.need(test, text, p), d, l):114 match test:115 case True{}:116 h117 case False{}:118 Unit{}119120# a calm op keeps the plan's loan and line121def Loan.at(op: B.Op, a: B.Acc, gifts: List<&2, B.Gift>, -d: B.Loan, -l: Nat,122 h: Loan.Is(Done{B.Plan{a, gifts}}, d, l), c: Op.Calm(op))123 -> Loan.Is(B.Op.at(op, a, gifts), d, l):124 match op a:125 case B.Need{test, text} a:126 Loan.need(test, text, B.Plan{a, gifts}, d, l, h)127 case B.Memo{t} B.Acc{pass, cash, note, line, loan, held}:128 h129 case B.Debt{x} _:130 match c:131 case B.Give{k, +x} B.Acc{pass, +cash, note, line, loan, held}:132 +p = {B.Plan{B.Acc{pass, Nat.sub(cash, x), note, line, loan, held},133 B.Pay{k, x} <> gifts} : B.Plan}134 Loan.need(Nat.is_le(x, cash), "you do not have that much", p, d, l, h)135 case B.Lock{k, +x} B.Acc{pass, +cash, note, line, loan, held}:136 +p = {B.Plan{B.Acc{pass, Nat.sub(cash, x), note, line, loan, held},137 B.Owe{k, x} <> gifts} : B.Plan}138 Loan.need(Nat.is_le(x, cash), "you do not have that much", p, d, l, h)139 case B.Open{k} B.Acc{pass, cash, note, line, loan, held}:140 h141 case B.Drop{k} B.Acc{pass, cash, note, line, loan, held}:142 h143 case B.Draw{x} _:144 match c:145 case B.Fund{x} _:146 match c:147148# a calm step keeps the loan and the line149def Loan.step(r: Result<&2, &2, String, B.Plan>, op: B.Op, -d: B.Loan, -l: Nat, h: Loan.Is(r, d, l),150 c: Op.Calm(op))151 -> Loan.Is(B.Op.step(r, op), d, l):152 match r:153 case Fail{e}:154 Unit{}155 case Done{B.Plan{a, gifts}}:156 Loan.at(op, a, gifts, d, l, h, c)157158# calm ops keep the loan and the line159def Loan.run(ops: List<&2, B.Op>, +r: Result<&2, &2, String, B.Plan>, -d: B.Loan, -l: Nat,160 h: Loan.Is(r, d, l), c: Op.Calms(ops))161 -> Loan.Is(B.Op.run(ops, r), d, l):162 match ops:163 case Nil{}:164 h165 case +op <> rest:166 (c1, c2) = c167 Loan.run(rest, B.Op.step(r, op), d, l, Loan.step(r, op, d, l, h, c1), c2)168169# the ops of a Send are calm170def Loan.rows(rows: List<&2, B.Line>) -> Op.Calms(B.Cmd.rows(rows)):171 match rows:172 case Nil{}:173 Unit{}174 case B.Line{name, cash} <> rest:175 (Unit{}, Unit{}, Unit{}, Loan.rows(rest))176177# a plan that keeps the loan and the line took a Step178def Loan.kept(r: Result<&2, &2, String, B.Plan>, -p: String, -c: Nat, -n: String, -l: Nat,179 -d: B.Loan, -h: B.Trie<Nat>, -now: Nat, e: Loan.Is(r, d, l))180 -> Loan.P(B.Acc{p, c, n, l, d, h}, r, now):181 match r:182 case Fail{x}:183 Unit{}184 case Done{B.Plan{B.Acc{p2, c2, n2, l2, d2, h2}, gifts}}:185 Inl{e}186187# a command of calm ops took a Step188def Loan.calm(+cmd: B.Cmd, a: B.Acc, +now: Nat, c: Op.Calms(B.Cmd.ops(cmd, a, now)))189 -> Loan.P(a, B.Cmd.plan(cmd, a, now), now):190 match a:191 case B.Acc{+p, +cash, +n, +l, +d, +h}:192 +a = {B.Acc{p, cash, n, l, d, h} : B.Acc}193 +r = {Done{B.Plan{a, Nil{}}} : Result<&2, &2, String, B.Plan>}194 Loan.kept(B.Cmd.plan(cmd, a, now), p, cash, n, l, d, h, now,195 Loan.run(B.Cmd.ops(cmd, a, now), r, d, l, ({==}, {==}), c))196197# 0 < x gives 1 <= x198def Loan.pos(+x: Nat, e: {Nat.is_lt(0n, x) == True{} : Bool}) -> Laws.LE(1n, x):199 match x:200 case 0n:201 L.Bool.false_true(Laws.LE(1n, 0n), e)202 case 1n+q:203 L.Nat.le_add(1n, q)204205# the loan of x, once its need passed: the line has x for it206def Loan.draw(t: Bool, +x: Nat, -p: String, +c: Nat, -n: String, +l: Nat, -h: B.Trie<Nat>,207 +now: Nat, -text: String, e: {Nat.is_le(x, l) == t : Bool}, e1: Laws.LE(1n, x),208 e2: Laws.LE(x, 1000n))209 -> Loan.P(B.Acc{p, c, n, l, B.Clear{}, h},210 B.Op.run([B.Debt{B.Owing{Nat.add(x, B.Loan.interest(x)), Nat.add(now, B.Loan.term())}}],211 B.Op.need(t, text, B.Plan{B.Acc{p, Nat.add(c, x), n, Nat.sub(l, x), B.Clear{}, h}, Nil{}})),212 now):213 match t:214 case True{}:215 Inr{Inl{(x, {==}, e1, e2, {==}, L.Nat.sub_add(l, x, e), {==})}}216 case False{}:217 Unit{}218219# a loan of x, when nothing is owed: a positive amount up to the limit220def Loan.lend(t1: Bool, t2: Bool, +x: Nat, -p: String, +c: Nat, -n: String, +l: Nat,221 -h: B.Trie<Nat>, +now: Nat, -s1: String, -s2: String, e1: {Nat.is_lt(0n, x) == t1 : Bool},222 e2: {Nat.is_le(x, B.Loan.limit()) == t2 : Bool})223 -> Loan.P(B.Acc{p, c, n, l, B.Clear{}, h},224 B.Op.run([B.Need{t2, s2}, B.Draw{x},225 B.Debt{B.Owing{Nat.add(x, B.Loan.interest(x)), Nat.add(now, B.Loan.term())}}],226 B.Op.need(t1, s1, B.Plan{B.Acc{p, c, n, l, B.Clear{}, h}, Nil{}})), now):227 match t1 t2:228 case True{} True{}:229 Loan.draw(Nat.is_le(x, l), x, p, c, n, l, h, now, "the bank has no more credit for you", {==},230 Loan.pos(x, e1), e2)231 case True{} False{}:232 Unit{}233 case False{} _:234 Unit{}235236# the repayment of x, once its needs passed: the cash has x for it237def Loan.fund(t: Bool, +x: Nat, -p: String, +c: Nat, -n: String, +l: Nat, -h: B.Trie<Nat>,238 -now: Nat, +debt: Nat, +till: Nat, -text: String, e: {Nat.is_le(x, c) == t : Bool},239 e1: Laws.LE(now, till), e2: Laws.LE(1n, x), e3: Laws.LE(x, debt))240 -> Loan.P(B.Acc{p, c, n, l, B.Owing{debt, till}, h},241 B.Op.run([B.Debt{B.Loan.rest(Nat.sub(debt, x), till)}],242 B.Op.need(t, text,243 B.Plan{B.Acc{p, Nat.sub(c, x), n, Nat.add(l, x), B.Owing{debt, till}, h}, Nil{}})), now):244 match t:245 case True{}:246 Inr{Inr{(x, e1, e2, e3, L.Nat.sub_add(c, x, e), {==}, {==})}}247 case False{}:248 Unit{}249250# a repayment of x: a positive amount, before the due time, up to the debt251def Loan.back(t1: Bool, t2: Bool, t3: Bool, +x: Nat, -p: String, +c: Nat, -n: String, +l: Nat,252 -h: B.Trie<Nat>, +now: Nat, +debt: Nat, +till: Nat, -s1: String, -s2: String, -s3: String,253 e1: {Nat.is_lt(0n, x) == t1 : Bool}, e2: {Nat.is_le(now, till) == t2 : Bool},254 e3: {Nat.is_le(x, debt) == t3 : Bool})255 -> Loan.P(B.Acc{p, c, n, l, B.Owing{debt, till}, h},256 B.Op.run([B.Need{t2, s2}, B.Need{t3, s3}, B.Fund{x},257 B.Debt{B.Loan.rest(Nat.sub(debt, x), till)}],258 B.Op.need(t1, s1, B.Plan{B.Acc{p, c, n, l, B.Owing{debt, till}, h}, Nil{}})), now):259 match t1 t2 t3:260 case True{} True{} True{}:261 Loan.fund(Nat.is_le(x, c), x, p, c, n, l, h, now, debt, till, "you do not have that much",262 {==}, e2, Loan.pos(x, e1), e3)263 case True{} True{} False{}:264 Unit{}265 case True{} False{} _:266 Unit{}267 case False{} _ _:268 Unit{}269270# the plan of every command took a Step271def Loan.cmd(cmd: B.Cmd, a: B.Acc, +now: Nat) -> Loan.P(a, B.Cmd.plan(cmd, a, now), now):272 match cmd a:273 case B.Note{+text} a:274 Loan.calm(B.Note{text}, a, now, (Unit{}, Unit{}, Unit{}))275 case B.Send{+rows} a:276 Loan.calm(B.Send{rows}, a, now, (Unit{}, Loan.rows(rows)))277 case B.Lend{+x} B.Acc{p, +c, n, +l, d, h}:278 match d:279 case B.Owing{debt, till}:280 Unit{}281 case B.Clear{}:282 Loan.lend(Nat.is_lt(0n, x), Nat.is_le(x, B.Loan.limit()), x, p, c, n, l, h, now,283 B.Cmd.positive(), "the largest loan is 1,000", {==}, {==})284 case B.Back{+x} B.Acc{p, +c, n, +l, d, h}:285 match d:286 case B.Clear{}:287 Unit{}288 case B.Owing{+debt, +till}:289 Loan.back(Nat.is_lt(0n, x), Nat.is_le(now, till), Nat.is_le(x, debt), x, p, c, n, l, h,290 now, debt, till,291 B.Cmd.positive(), "your loan was written off", "you owe less than that", {==}, {==},292 {==})293 case B.Hold{+name, +x} a:294 Loan.calm(B.Hold{name, x}, a, now, (Unit{}, Unit{}, Unit{}, Unit{}))295 case B.Free{+name} a:296 Loan.calm(B.Free{name}, a, now, (Unit{}, Unit{}, Unit{}))297 case B.Void{+name} a:298 Loan.calm(B.Void{name}, a, now, (Unit{}, Unit{}, Unit{}))299300# Exec301# ----302303# a bank result that does not fail took a Step at k, from m0304def Loan.R(m0: Maybe<&2, B.Acc>, r: Result<&2, &2, String, B.Bank>, k: B.Key(), now: Nat) -> Type:305 L.Bank.If(r, b => Laws.Stepped(m0, Laws.acct(b, k), now))306307# the sender's account after the plan of its command is the plan's308def Loan.self(r: Result<&2, &2, String, B.Bank>, -a: B.Acc, -acct: B.Acc, -u: B.Key(), -now: Nat,309 hs: Self.R(r, u, acct), h: Laws.Step(a, acct, now))310 -> Loan.R(Some{a}, r, u, now):311 match r:312 case Fail{e}:313 Unit{}314 case Done{b}:315 %hs : Laws.Stepped(Some{a}, _, now)316 h317318# a plan of u that took a Step leaves u's account Stepped319def Loan.plan(+v: Nat, +t: B.Trie<B.Acc>, +u: B.Key(), r: Result<&2, &2, String, B.Plan>, -a: B.Acc,320 -now: Nat, h: Loan.P(a, r, now))321 -> Loan.R(Some{a}, B.Bank.plan(B.Bank{v, t}, u, r), u, now):322 match r:323 case Fail{e}:324 Unit{}325 case Done{B.Plan{+acct, +gifts}}:326 +r = B.Plan.apply(B.Bank{v, t}, u, B.Plan{acct, gifts})327 Loan.self(r, a, acct, u, now, Self.apply(v, t, u, acct, gifts), h)328329# the sender uk is k, the holder of a330def Loan.sent(+v: Nat, +t: B.Trie<B.Acc>, +uk: B.Key(), +a: B.Acc, +now: Nat, +cmd: B.Cmd,331 +k: B.Key(), eg: {Some{a} == B.Trie.get(B.Acc, uk, t) : Maybe<&2, B.Acc>},332 me: {B.Key.eq(uk, k) == True{} : Bool})333 -> Loan.R(B.Trie.get(B.Acc, k, t), B.Bank.plan(B.Bank{v, t}, uk, B.Cmd.plan(cmd, a, now)), k,334 now):335 +r = B.Bank.plan(B.Bank{v, t}, uk, B.Cmd.plan(cmd, a, now))336 %L.Key.eq_true(uk, k, me) : Loan.R(B.Trie.get(B.Acc, _, t), r, _, now)337 %eg : Loan.R(_, r, uk, now)338 Loan.plan(v, t, uk, B.Cmd.plan(cmd, a, now), a, now, Loan.cmd(cmd, a, now))339340# a command changes its sender's loan and line only by a Step341def Loan.exec(s: B.Bank, +name: String, +pass: String, +now: Nat, +cmd: B.Cmd, +k: B.Key(),342 me: {Laws.Key.is(Laws.Bank.sender(s, name, pass), k) == True{} : Bool})343 -> Loan.R(Laws.acct(s, k), B.Bank.exec(s, name, pass, now, cmd), k, now):344 match s:345 case B.Bank{+v, +t}:346 L.Bank.exec_by(B.Key.of(name), v, t, pass, now, cmd,347 u => b => Laws.Stepped(B.Trie.get(B.Acc, k, t), Laws.acct(b, k), now),348 u => {Laws.Key.is(u, k) == True{} : Bool}, me,349 +uk => +a => eg => me => Loan.sent(v, t, uk, a, now, cmd, k, eg, me))350351# Join352# ----353354# a kept account took a Step: its loan and line are the same355def Loan.of_kept(m0: Maybe<&2, B.Acc>, m1: Maybe<&2, B.Acc>, -u: Maybe<&2, B.Key()>, -now: Nat,356 h: Laws.Kept(m0, m1, u)) -> Laws.Stepped(m0, m1, now):357 match m0 m1:358 case None{} _:359 Unit{}360 case Some{a} None{}:361 match h:362 case Some{B.Acc{p1, c1, n1, l1, d1, w1}} Some{B.Acc{p2, c2, n2, l2, d2, w2}}:363 (ep, en, el, ed, le, f, g) = h364 Inl{(ed, el)}365366# a join keeps every account that existed (LAW authority), so it took a367# Step368def Loan.join(r: Result<&2, &2, String, B.Bank>, m0: Maybe<&2, B.Acc>, k: B.Key(), -now: Nat,369 h: A.Keep.R(m0, r, k, None{})) -> Loan.R(m0, r, k, now):370 match r:371 case Fail{e}:372 Unit{}373 case Done{b}:374 Loan.of_kept(m0, Laws.acct(b, k), None{}, now, h)375376# LAW loan377def Laws.loan(s, input, k, me):378 +m0 = Laws.acct(s, k)379 +now = Laws.time(input)380 -P = {b => Laws.Stepped(m0, Laws.acct(b, k), now) : B.Bank -> Type}381 L.Web.reply_by(s, W.Req.parse(input), P,382 Loan.of_kept(m0, m0, None{}, now, A.Keep.kept_refl(m0, None{})),383 +name => Loan.join(B.Bank.join(s, name, Laws.rand(input)), m0, k, now,384 A.Keep.join(s, name, Laws.rand(input), k, None{})),385 +cmd => Loan.exec(s, Laws.user(input), Laws.key(input), now, cmd, k, me))