1# Bend Bank: the proof of LAW split2# =================================3#4# The route of the input is POST /send, so a change of the bank comes5# from Bank.exec running a Send of the form's rows, which Web.rows reads6# from fields to1, cash1 up to to3, cash3, skipping only blank rows; a7# blank row pays nothing, so the rows pay what the form's fields do8# (Rows). The Send's ops (Plan) take each row's cash from the sender's9# and leave one Pay gift per row, to the key of the row's name, which its10# need checked. Plan.apply then sets the sender's account and runs the11# gifts (Gifts): each adds its cash to its account, and none reaches the12# sender, since a gift to the sender fails. So every account ends with13# its cash before, plus what the rows pay it, and the sender with its14# cash less what it sent (Send).1516import Base17import ../bank.bend as B18import ../web.bend as W19import ../LAWS.bend as Laws20import ./base.bend as L2122# Gift23# ----2425# a gift that pays cash26def Gift.Pay(g: B.Gift) -> Type:27 match g:28 case B.Pay{dest, cash}:29 Unit30 case o:31 Empty3233# gifts that all pay cash34def Gift.Pays(gs: List<&2, B.Gift>) -> Type:35 match gs:36 case Nil{}:37 Unit38 case g <> rest:39 Gift.Pay(g) & Gift.Pays(rest)4041# Rows42# ----4344# the money rows pay the account at k, and all they pay45def Rows.paid(rows: List<&2, B.Line>, +k: B.Key()) -> Nat:46 match rows:47 case Nil{}:48 0n49 case B.Line{name, cash} <> rest:50 Nat.add(Bool.pick(Nat, Laws.Key.is(B.Key.of(name), k), cash, 0n), Rows.paid(rest, k))5152def Rows.spent(rows: List<&2, B.Line>) -> Nat:53 match rows:54 case Nil{}:55 0n56 case B.Line{name, cash} <> rest:57 Nat.add(cash, Rows.spent(rest))5859# a row put last is spent as if it were first60def Rows.spent_last(rows: List<&2, B.Line>, +name: String, +x: Nat)61 -> {Rows.spent(List.append(&2, B.Line, rows, [B.Line{name, x}]))62 == Nat.add(x, Rows.spent(rows)) : Nat}:63 match rows:64 case Nil{}:65 {==}66 case B.Line{n, +y} <> +rest:67 +r = Rows.spent(rest)68 +e = Rows.spent_last(rest, name, x)69 +a = Rows.spent(List.append(&2, B.Line, rest, [B.Line{name, x}]))70 %Equal.sym(Nat, a, Nat.add(x, r), e) : {Nat.add(y, _) == Nat.add(x, Nat.add(y, r)) : Nat}71 L.Nat.add_swap(y, x, r)7273# a row put last pays as if it were first74def Rows.paid_last(rows: List<&2, B.Line>, +name: String, +x: Nat, +k: B.Key())75 -> {Rows.paid(List.append(&2, B.Line, rows, [B.Line{name, x}]), k)76 == Nat.add(Bool.pick(Nat, Laws.Key.is(B.Key.of(name), k), x, 0n), Rows.paid(rows, k)) : Nat}:77 match rows:78 case Nil{}:79 {==}80 case B.Line{+n, +y} <> +rest:81 +q = Bool.pick(Nat, Laws.Key.is(B.Key.of(name), k), x, 0n)82 +p = Bool.pick(Nat, Laws.Key.is(B.Key.of(n), k), y, 0n)83 +r = Rows.paid(rest, k)84 +e = Rows.paid_last(rest, name, x, k)85 +a = Rows.paid(List.append(&2, B.Line, rest, [B.Line{name, x}]), k)86 %Equal.sym(Nat, a, Nat.add(q, r), e) : {Nat.add(p, _) == Nat.add(q, Nat.add(p, r)) : Nat}87 L.Nat.add_swap(p, q, r)8889# a form row, skipped only when both its fields are blank, spends its cash90def Rows.spent_row(+to: String, +cash: String, +rest: List<&2, B.Line>)91 -> {Rows.spent(Bool.pick(List<&2, B.Line>, Bool.and(String.is_empty(to), String.is_empty(cash)),92 rest, List.append(&2, B.Line, rest, [B.Line{to, W.Text.nat(cash)}])))93 == Nat.add(W.Text.nat(cash), Rows.spent(rest)) : Nat}:94 match to cash:95 case SNil{} SNil{}:96 {==}97 case SNil{} SCon{h, t}:98 Rows.spent_last(rest, SNil{}, W.Text.nat(SCon{h, t}))99 case SCon{h, t} _:100 Rows.spent_last(rest, SCon{h, t}, W.Text.nat(cash))101102# a form row, skipped only when both its fields are blank, pays its cash103# to its name104def Rows.paid_row(+to: String, +cash: String, +rest: List<&2, B.Line>, +k: B.Key())105 -> {Rows.paid(Bool.pick(List<&2, B.Line>, Bool.and(String.is_empty(to), String.is_empty(cash)),106 rest, List.append(&2, B.Line, rest, [B.Line{to, W.Text.nat(cash)}])), k)107 == Nat.add(Bool.pick(Nat, Laws.Key.is(B.Key.of(to), k), W.Text.nat(cash), 0n),108 Rows.paid(rest, k)) : Nat}:109 match to cash:110 case SNil{} SNil{}:111 {==}112 case SNil{} SCon{h, t}:113 Rows.paid_last(rest, SNil{}, W.Text.nat(SCon{h, t}), k)114 case SCon{h, t} _:115 Rows.paid_last(rest, SCon{h, t}, W.Text.nat(cash), k)116117# the rows of a form spend what its fields do118def Rows.spent_form(+form: List<&2, W.Field>, +n: Nat)119 -> {Rows.spent(W.Web.rows(form, n)) == Laws.spent(form, n) : Nat}:120 match n:121 case 0n:122 {==}123 case 1n+p:124 +i = Nat.show(1n+p)125 +to = W.Req.get(form, "to" ++ i)126 +cash = W.Req.get(form, "cash" ++ i)127 +rest = W.Web.rows(form, p)128 +l = Rows.spent(Bool.pick(List<&2, B.Line>,129 Bool.and(String.is_empty(to), String.is_empty(cash)), rest,130 List.append(&2, B.Line, rest, [B.Line{to, W.Text.nat(cash)}])))131 %Rows.spent_form(form, p) : {l == Nat.add(W.Text.nat(cash), _) : Nat}132 Rows.spent_row(to, cash, rest)133134# the rows of a form pay what its fields do135def Rows.paid_form(+form: List<&2, W.Field>, +k: B.Key(), +n: Nat)136 -> {Rows.paid(W.Web.rows(form, n), k) == Laws.paid(form, k, n) : Nat}:137 match n:138 case 0n:139 {==}140 case 1n+p:141 +i = Nat.show(1n+p)142 +to = W.Req.get(form, "to" ++ i)143 +cash = W.Req.get(form, "cash" ++ i)144 +rest = W.Web.rows(form, p)145 +q = Bool.pick(Nat, Laws.Key.is(B.Key.of(to), k), W.Text.nat(cash), 0n)146 +l = Rows.paid(Bool.pick(List<&2, B.Line>,147 Bool.and(String.is_empty(to), String.is_empty(cash)), rest,148 List.append(&2, B.Line, rest, [B.Line{to, W.Text.nat(cash)}])), k)149 %Rows.paid_form(form, k, p) : {l == Nat.add(q, _) : Nat}150 Rows.paid_row(to, cash, rest, k)151152# Plan153# ----154155# a planned send that does not fail: its account's cash plus x is c, its156# gifts all pay, and they bring n to the account at k157def Split.Plan(r: Result<&2, &2, String, B.Plan>, c: Nat, x: Nat, n: Nat, k: B.Key()) -> Type:158 match r:159 case Fail{e}:160 Unit161 case Done{B.Plan{B.Acc{pass, cash, note, line, loan, held}, gifts}}:162 {Nat.add(cash, x) == c : Nat} & Gift.Pays(gifts) & {L.Gift.paid(gifts, k) == n : Nat}163164# the first need of a send keeps the account, with no gifts165def Split.start(t: Bool, a: B.Acc, -text: String, -k: B.Key())166 -> Split.Plan(B.Op.need(t, text, B.Plan{a, Nil{}}), Laws.cash(Some{a}), 0n, 0n, k):167 match t a:168 case True{} B.Acc{p, c, n, l, d, h}:169 (L.Nat.zero_r(c), Unit{}, {==})170 case False{} _:171 Unit{}172173# (c - y) + (x + y) == c, when y <= c and c + x is the start174def Split.spend(+c: Nat, +y: Nat, +x: Nat, -c0: Nat, e: {Nat.is_le(y, c) == True{} : Bool},175 h: {Nat.add(c, x) == c0 : Nat})176 -> {Nat.add(Nat.sub(c, y), Nat.add(x, y)) == c0 : Nat}:177 +r = Nat.sub(c, y)178 %L.Nat.add_comm(y, x) : {Nat.add(r, _) == c0 : Nat}179 %L.Nat.add_assoc(r, y, x) : {_ == c0 : Nat}180 %Equal.sym(Nat, Nat.add(r, y), c, L.Nat.sub_add(c, y, e)) : {Nat.add(_, x) == c0 : Nat}181 h182183# q + g == n + q, when g is n184def Split.count(+q: Nat, +g: Nat, -n: Nat, e: {g == n : Nat})185 -> {Nat.add(q, g) == Nat.add(n, q) : Nat}:186 %e : {Nat.add(q, g) == Nat.add(_, q) : Nat}187 L.Nat.add_comm(q, g)188189# the Give of a row, once its needs passed: the cash has y for it190def Split.give(t: Bool, +y: Nat, -p: String, +c: Nat, -nt: String, -l: Nat, -d: B.Loan,191 -h: B.Trie<Nat>, +kk: B.Key(), +gs: List<&2, B.Gift>, -c0: Nat, +x: Nat, -n: Nat, +k: B.Key(),192 -text: String, e: {Nat.is_le(y, c) == t : Bool},193 hp: {Nat.add(c, x) == c0 : Nat} & Gift.Pays(gs) & {L.Gift.paid(gs, k) == n : Nat})194 -> Split.Plan(B.Op.need(t, text,195 B.Plan{B.Acc{p, Nat.sub(c, y), nt, l, d, h}, B.Pay{kk, y} <> gs}), c0, Nat.add(x, y),196 Nat.add(n, Bool.pick(Nat, B.Key.eq(kk, k), y, 0n)), k):197 match t:198 case True{}:199 (e1, ps, e2) = hp200 +q = Bool.pick(Nat, B.Key.eq(kk, k), y, 0n)201 (Split.spend(c, y, x, c0, e, e1), (Unit{}, ps), Split.count(q, L.Gift.paid(gs, k), n, e2))202 case False{}:203 Unit{}204205# the needs of a row: the name is valid, and the amount positive206def Split.named(m: Maybe<&2, B.Key()>, t: Bool, +y: Nat, +p: String, +c: Nat, +nt: String, +l: Nat,207 +d: B.Loan, +h: B.Trie<Nat>, +gs: List<&2, B.Gift>, -c0: Nat, +x: Nat, -n: Nat, +k: B.Key(),208 -s1: String, -s2: String,209 hp: {Nat.add(c, x) == c0 : Nat} & Gift.Pays(gs) & {L.Gift.paid(gs, k) == n : Nat})210 -> Split.Plan(B.Op.step(B.Op.step(B.Op.need(Maybe.is_some(&2, B.Key(), m), s1,211 B.Plan{B.Acc{p, c, nt, l, d, h}, gs}), B.Need{t, s2}),212 B.Give{Maybe.default(&2, B.Key(), m, Nil{}), y}), c0, Nat.add(x, y),213 Nat.add(n, Bool.pick(Nat, Laws.Key.is(m, k), y, 0n)), k):214 match m t:215 case Some{+kk} True{}:216 Split.give(Nat.is_le(y, c), y, p, c, nt, l, d, h, kk, gs, c0, x, n, k,217 "you do not have that much", {==}, hp)218 case Some{kk} False{}:219 Unit{}220 case None{} _:221 Unit{}222223# a row takes its cash from the account and pays it to its name224def Split.row(r: Result<&2, &2, String, B.Plan>, +name: String, +y: Nat, -c0: Nat, +x: Nat, -n: Nat,225 +k: B.Key(), h: Split.Plan(r, c0, x, n, k))226 -> Split.Plan(B.Op.step(B.Op.step(B.Op.step(r, B.Cmd.named(name)),227 B.Need{Nat.is_lt(0n, y), B.Cmd.positive()}), B.Give{B.Cmd.key(name), y}), c0, Nat.add(x, y),228 Nat.add(n, Bool.pick(Nat, Laws.Key.is(B.Key.of(name), k), y, 0n)), k):229 match r:230 case Fail{e}:231 Unit{}232 case Done{B.Plan{B.Acc{+p, +c, +nt, +l, +d, +hd}, +gs}}:233 Split.named(B.Key.of(name), Nat.is_lt(0n, y), y, p, c, nt, l, d, hd, gs, c0, x, n, k,234 B.Key.rule(), B.Cmd.positive(), h)235236# the rows take what they spend from the account and pay what they pay237def Split.rows(rows: List<&2, B.Line>, +r: Result<&2, &2, String, B.Plan>, -c0: Nat, +x: Nat,238 +n: Nat, +k: B.Key(), h: Split.Plan(r, c0, x, n, k))239 -> Split.Plan(B.Op.run(B.Cmd.rows(rows), r), c0, Nat.add(x, Rows.spent(rows)),240 Nat.add(n, Rows.paid(rows, k)), k):241 match rows:242 case Nil{}:243 %L.Nat.add_zero(x) : Split.Plan(r, c0, _, Nat.add(n, 0n), k)244 %L.Nat.add_zero(n) : Split.Plan(r, c0, x, _, k)245 h246 case B.Line{+name, +y} <> +rest:247 +q = Bool.pick(Nat, Laws.Key.is(B.Key.of(name), k), y, 0n)248 +o = B.Op.run(B.Cmd.rows(B.Line{name, y} <> rest), r)249 +s = Rows.spent(rest)250 +g = Rows.paid(rest, k)251 +r1 = {B.Op.step(B.Op.step(B.Op.step(r, B.Cmd.named(name)),252 B.Need{Nat.is_lt(0n, y), B.Cmd.positive()}), B.Give{B.Cmd.key(name), y}) : Result<&2, &2,253 String, B.Plan>}254 %L.Nat.add_assoc(x, y, s) : Split.Plan(o, c0, _, Nat.add(n, Nat.add(q, g)), k)255 %L.Nat.add_assoc(n, q, g) : Split.Plan(o, c0, Nat.add(Nat.add(x, y), s), _, k)256 Split.rows(rest, r1, c0, Nat.add(x, y), Nat.add(n, q), k,257 Split.row(r, name, y, c0, x, n, k, h))258259# the plan of a send by the holder of a260def Split.cmd(+a: B.Acc, +rows: List<&2, B.Line>, +k: B.Key(), -now: Nat)261 -> Split.Plan(B.Cmd.plan(B.Send{rows}, a, now), Laws.cash(Some{a}), Rows.spent(rows),262 Rows.paid(rows, k), k):263 +t = Bool.not(List.is_empty(&2, B.Line, rows))264 +r = {B.Op.need(t, "there is nothing to send", B.Plan{a, Nil{}}) : Result<&2, &2, String, B.Plan>}265 Split.rows(rows, r, Laws.cash(Some{a}), 0n, 0n, k,266 Split.start(t, a, "there is nothing to send", k))267268# Gifts269# -----270271# a bank result that does not fail: the account at k has cash cb, and272# the gifts so far brought pu to the sender273def Split.Bank(r: Result<&2, &2, String, B.Bank>, k: B.Key(), cb: Nat, pu: Nat) -> Type:274 L.Bank.If(r, b => {Laws.cash(Laws.acct(b, k)) == cb : Nat} & {pu == 0n : Nat})275276# the cash at k after a payment of x to the account a at d277def Split.at(c: Bool, +k: B.Key(), +d: B.Key(), +accts: B.Trie<B.Acc>, a: B.Acc, -u: B.Key(),278 +x: Nat, +cb: Nat, ec: {B.Key.eq(k, d) == c : Bool},279 em: {B.Trie.get(B.Acc, d, accts) == Some{a} : Maybe<&2, B.Acc>},280 h: {Laws.cash(B.Trie.get(B.Acc, k, accts)) == cb : Nat})281 -> {Laws.cash(Bool.pick(Maybe<&2, B.Acc>, c, Some{B.Gift.give(B.Pay{d, x}, u, a)},282 B.Trie.get(B.Acc, k, accts))) == Nat.add(cb, Bool.pick(Nat, c, x, 0n)) : Nat}:283 match c:284 case True{}:285 match a:286 case B.Acc{p, +ca, n, l, dd, hd}:287 +a = {B.Acc{p, ca, n, l, dd, hd} : B.Acc}288 %h : {Nat.add(ca, x) == Nat.add(_, x) : Nat}289 %Equal.sym(B.Key(), k, d,290 L.Key.eq_true(k, d, ec)) : {Nat.add(ca,291 x) == Nat.add(Laws.cash(B.Trie.get(B.Acc, _, accts)), x) : Nat}292 %Equal.sym(Maybe<&2, B.Acc>, B.Trie.get(B.Acc, d, accts), Some{a},293 em) : {Nat.add(ca, x) == Nat.add(Laws.cash(_), x) : Nat}294 {==}295 case False{}:296 %L.Nat.add_zero(cb) : {Laws.cash(B.Trie.get(B.Acc, k, accts)) == _ : Nat}297 h298299# a payment of x from u to the account m at d; one to u itself fails300def Split.gift_to(self: Bool, m: Maybe<&2, B.Acc>, +vault: Nat, +accts: B.Trie<B.Acc>, +u: B.Key(),301 +d: B.Key(), +x: Nat, +k: B.Key(), +cb: Nat, +pu: Nat,302 em: {B.Trie.get(B.Acc, d, accts) == m : Maybe<&2, B.Acc>},303 h: Split.Bank(Done{B.Bank{vault, accts}}, k, cb, pu))304 -> Split.Bank(B.Plan.gift.to(self, m, vault, accts, u, d, B.Pay{d, x}), k,305 Nat.add(cb, Bool.pick(Nat, B.Key.eq(d, k), x, 0n)), Nat.add(pu, Bool.pick(Nat, self, x, 0n))):306 match self m:307 case True{} _:308 Unit{}309 case False{} None{}:310 Unit{}311 case False{} Some{+a}:312 (h1, h2) = h313 +b = B.Gift.give(B.Pay{d, x}, u, a)314 +m = B.Trie.get(B.Acc, k, accts)315 -z = {Nat.add(pu, 0n) == 0n : Nat}316 %L.Trie.pick_set(B.Acc, k, d, accts,317 Some{b}) : {Laws.cash(_) == Nat.add(cb, Bool.pick(Nat, B.Key.eq(d, k), x, 0n)) : Nat} & z318 %L.Key.eq_sym(k,319 d) : {Laws.cash(Bool.pick(Maybe<&2, B.Acc>, B.Key.eq(k, d), Some{b}, m)) == Nat.add(cb,320 Bool.pick(Nat, _, x, 0n)) : Nat} & z321 (Split.at(B.Key.eq(k, d), k, d, accts, a, u, x, cb, {==}, em, h1),322 Equal.trans(Nat, Nat.add(pu, 0n), pu, 0n, L.Nat.zero_r(pu), h2))323324# one more payment adds its cash at k, and pays u nothing325def Split.gift(r: Result<&2, &2, String, B.Bank>, +u: B.Key(), g: B.Gift, +k: B.Key(), +cb: Nat,326 +pu: Nat, pg: Gift.Pay(g), h: Split.Bank(r, k, cb, pu))327 -> Split.Bank(B.Plan.gift(r, u, g), k, Nat.add(cb, L.Gift.pay(g, k)),328 Nat.add(pu, L.Gift.pay(g, u))):329 match r g:330 case Fail{e} _:331 Unit{}332 case Done{B.Bank{vault, +accts}} B.Pay{+d, +x}:333 Split.gift_to(B.Key.eq(d, u), B.Trie.get(B.Acc, d, accts), vault, accts, u, d, x, k, cb, pu,334 {==}, h)335 case Done{b} B.Owe{d, x}:336 match pg:337 case Done{b} B.Rel{d}:338 match pg:339340# the gifts bring their cash to the account at k, and none to u341def Split.gifts(gs: List<&2, B.Gift>, +u: B.Key(), +r: Result<&2, &2, String, B.Bank>, +k: B.Key(),342 +cb: Nat, +pu: Nat, ps: Gift.Pays(gs), h: Split.Bank(r, k, cb, pu))343 -> Split.Bank(B.Plan.gifts(gs, u, r), k, Nat.add(cb, L.Gift.paid(gs, k)),344 Nat.add(pu, L.Gift.paid(gs, u))):345 match gs:346 case Nil{}:347 %L.Nat.add_zero(cb) : Split.Bank(r, k, _, Nat.add(pu, 0n))348 %L.Nat.add_zero(pu) : Split.Bank(r, k, cb, _)349 h350 case +g <> +rest:351 (pg, ps) = ps352 +o = B.Plan.gifts(g <> rest, u, r)353 +ik = L.Gift.pay(g, k)354 +iu = L.Gift.pay(g, u)355 +gk = L.Gift.paid(rest, k)356 +gu = L.Gift.paid(rest, u)357 %L.Nat.add_assoc(cb, ik, gk) : Split.Bank(o, k, _, Nat.add(pu, Nat.add(iu, gu)))358 %L.Nat.add_assoc(pu, iu, gu) : Split.Bank(o, k, Nat.add(Nat.add(cb, ik), gk), _)359 Split.gifts(rest, u, B.Plan.gift(r, u, g), k, Nat.add(cb, ik), Nat.add(pu, iu), ps,360 Split.gift(r, u, g, k, cb, pu, pg, h))361362# Send363# ----364365# what the law states of the bank b after a send by u that spends sp366# and pays pd to the account at k367def Split.Eq(b: B.Bank, s: B.Bank, sp: Nat, pd: Nat, k: B.Key(), u: Maybe<&2, B.Key()>) -> Type:368 {Nat.add(Laws.cash(Laws.acct(b, k)),369 Bool.pick(Nat, Laws.Key.is(u, k), sp, 0n)) == Nat.add(Laws.cash(Laws.acct(s, k)), pd) : Nat}370371# a bank result of a send of rows that does not fail is what the law states372def Split.R(r: Result<&2, &2, String, B.Bank>, s: B.Bank, +rows: List<&2, B.Line>, +k: B.Key(),373 u: Maybe<&2, B.Key()>)374 -> Type:375 L.Bank.If(r, b => Split.Eq(b, s, Rows.spent(rows), Rows.paid(rows, k), k, u))376377# a change of the bank is what the law states378def Split.Out(m: Maybe<&2, B.Bank>, s: B.Bank, sp: Nat, pd: Nat, k: B.Key(), u: Maybe<&2, B.Key()>)379 -> Type:380 match m:381 case None{}:382 Unit383 case Some{b}:384 Split.Eq(b, s, sp, pd, k, u)385386# the sum at k: the sender's cash is what the plan left it, plus nothing,387# and any other account's is its own plus what the rows pay it388def Split.sum(c: Bool, +k: B.Key(), +u: B.Key(), +t: B.Trie<B.Acc>, acct: B.Acc,389 +gs: List<&2, B.Gift>, +rows: List<&2, B.Line>, -a: B.Acc, ec: {B.Key.eq(k, u) == c : Bool},390 e1: {Nat.add(Laws.cash(Some{acct}), Rows.spent(rows)) == Laws.cash(Some{a}) : Nat},391 e2: {L.Gift.paid(gs, k) == Rows.paid(rows, k) : Nat}, e3: {L.Gift.paid(gs, u) == 0n : Nat},392 eg: {Some{a} == B.Trie.get(B.Acc, u, t) : Maybe<&2, B.Acc>})393 -> {Nat.add(Nat.add(Laws.cash(Bool.pick(Maybe<&2, B.Acc>, c, Some{acct},394 B.Trie.get(B.Acc, k, t))), L.Gift.paid(gs, k)),395 Bool.pick(Nat, c, Rows.spent(rows), 0n)) == Nat.add(Laws.cash(B.Trie.get(B.Acc, k, t)),396 Rows.paid(rows, k)) : Nat}:397 match c:398 case True{}:399 match acct:400 case B.Acc{p, +ca, n, l, d, h}:401 +s = Rows.spent(rows)402 +gk = L.Gift.paid(gs, k)403 %e2 : {Nat.add(Nat.add(ca, gk), s) == Nat.add(Laws.cash(B.Trie.get(B.Acc, k, t)),404 _) : Nat}405 %Equal.sym(B.Key(), k, u, L.Key.eq_true(k, u, ec))406 : {Nat.add(Nat.add(ca, L.Gift.paid(gs, _)),407 s) == Nat.add(Laws.cash(B.Trie.get(B.Acc, _, t)), L.Gift.paid(gs, _)) : Nat}408 %Equal.sym(Nat, L.Gift.paid(gs, u), 0n,409 e3) : {Nat.add(Nat.add(ca, _), s) == Nat.add(Laws.cash(B.Trie.get(B.Acc, u, t)),410 _) : Nat}411 %eg : {Nat.add(Nat.add(ca, 0n), s) == Nat.add(Laws.cash(_), 0n) : Nat}412 %e1 : {Nat.add(Nat.add(ca, 0n), s) == Nat.add(_, 0n) : Nat}413 %L.Nat.add_zero(ca) : {Nat.add(_, s) == Nat.add(Nat.add(ca, s), 0n) : Nat}414 %L.Nat.add_zero(Nat.add(ca, s)) : {Nat.add(ca, s) == _ : Nat}415 {==}416 case False{}:417 +gk = L.Gift.paid(gs, k)418 +c0 = Laws.cash(B.Trie.get(B.Acc, k, t))419 %e2 : {Nat.add(Nat.add(c0, gk), 0n) == Nat.add(c0, _) : Nat}420 %L.Nat.add_zero(Nat.add(c0, gk)) : {_ == Nat.add(c0, gk) : Nat}421 {==}422423# the bank after the gifts of a send by u, from the plan's account acct424def Split.end(r: Result<&2, &2, String, B.Bank>, -v: Nat, +t: B.Trie<B.Acc>, +u: B.Key(),425 +k: B.Key(), +acct: B.Acc, +gs: List<&2, B.Gift>, +rows: List<&2, B.Line>, -a: B.Acc,426 h: Split.Bank(r, k,427 Nat.add(Laws.cash(B.Trie.get(B.Acc, k, B.Trie.set(B.Acc, u, t, Some{acct}))), L.Gift.paid(gs, k)),428 L.Gift.paid(gs, u)),429 e1: {Nat.add(Laws.cash(Some{acct}), Rows.spent(rows)) == Laws.cash(Some{a}) : Nat},430 e2: {L.Gift.paid(gs, k) == Rows.paid(rows, k) : Nat},431 eg: {Some{a} == B.Trie.get(B.Acc, u, t) : Maybe<&2, B.Acc>})432 -> Split.R(r, B.Bank{v, t}, rows, k, Some{u}):433 match r:434 case Fail{e}:435 Unit{}436 case Done{b}:437 (h1, h2) = h438 +gk = L.Gift.paid(gs, k)439 +q = Bool.pick(Nat, B.Key.eq(u, k), Rows.spent(rows), 0n)440 +o = Nat.add(Laws.cash(B.Trie.get(B.Acc, k, t)), Rows.paid(rows, k))441 +m = B.Trie.get(B.Acc, k, B.Trie.set(B.Acc, u, t, Some{acct}))442 +n = Bool.pick(Maybe<&2, B.Acc>, B.Key.eq(k, u), Some{acct}, B.Trie.get(B.Acc, k, t))443 %Equal.sym(Nat, Laws.cash(Laws.acct(b, k)), Nat.add(Laws.cash(m), gk),444 h1) : {Nat.add(_, q) == o : Nat}445 %L.Trie.pick_set(B.Acc, k, u, t,446 Some{acct}) : {Nat.add(Nat.add(Laws.cash(_), gk), q) == o : Nat}447 %L.Key.eq_sym(k,448 u) : {Nat.add(Nat.add(Laws.cash(n), gk),449 Bool.pick(Nat, _, Rows.spent(rows), 0n)) == o : Nat}450 Split.sum(B.Key.eq(k, u), k, u, t, acct, gs, rows, a, {==}, e1, e2, h2, eg)451452# a send's plan, applied453def Split.plan(+v: Nat, +t: B.Trie<B.Acc>, +u: B.Key(), r: Result<&2, &2, String, B.Plan>,454 -a: B.Acc, +rows: List<&2, B.Line>, +k: B.Key(),455 h: Split.Plan(r, Laws.cash(Some{a}), Rows.spent(rows), Rows.paid(rows, k), k),456 eg: {Some{a} == B.Trie.get(B.Acc, u, t) : Maybe<&2, B.Acc>})457 -> Split.R(B.Bank.plan(B.Bank{v, t}, u, r), B.Bank{v, t}, rows, k, Some{u}):458 match r:459 case Fail{e}:460 Unit{}461 case Done{B.Plan{B.Acc{+p, +c, +n, +l, +d, +hd}, +gs}}:462 (e1, ps, e2) = h463 +acct = {B.Acc{p, c, n, l, d, hd} : B.Acc}464 +t1 = B.Trie.set(B.Acc, u, t, Some{acct})465 +r0 = {Done{B.Bank{v, t1}} : Result<&2, &2, String, B.Bank>}466 +c0 = Laws.cash(B.Trie.get(B.Acc, k, t1))467 hg = Split.gifts(gs, u, r0, k, c0, 0n, ps, ({==}, {==}))468 Split.end(B.Plan.gifts(gs, u, r0), v, t, u, k, acct, gs, rows, a, hg, e1, e2, eg)469470# Exec471# ----472473# a send that does not fail is what the law states474def Split.exec(s: B.Bank, +name: String, +pass: String, +now: Nat, +rows: List<&2, B.Line>,475 +k: B.Key())476 -> Split.R(B.Bank.exec(s, name, pass, now, B.Send{rows}), s, rows, k,477 Laws.Bank.sender(s, name, pass)):478 match s:479 case B.Bank{+v, +t}:480 L.Bank.exec_by(B.Key.of(name), v, t, pass, now, B.Send{rows},481 u => b => Split.Eq(b, B.Bank{v, t}, Rows.spent(rows), Rows.paid(rows, k), k, u),482 u => Unit, Unit{},483 +uk => +a => eg => r => Split.plan(v, t, uk, B.Cmd.plan(B.Send{rows}, a, now), a, rows, k,484 Split.cmd(a, rows, k, now), eg))485486# Web487# ---488489# a send that changes the bank changes it to its result490def Split.done(r: Result<&2, &2, String, B.Bank>, +see: String, +s: B.Bank, +user: String,491 +pass: String, +time: Nat, -rows: List<&2, B.Line>, -k: B.Key(), -u: Maybe<&2, B.Key()>,492 h: Split.R(r, s, rows, k, u))493 -> Split.Out(Laws.change(W.Web.done(W.Web.change(r, see), s, user, pass, time)), s,494 Rows.spent(rows), Rows.paid(rows, k), k, u):495 match r:496 case Fail{e}:497 Unit{}498 case Done{b}:499 h500501# the request's route is POST /send, so its answer runs a Send of the502# form's rows, which pay what the form's fields do503def Split.reply(+s: B.Bank, req: W.Req, +k: B.Key(),504 send: {Laws.Req.route(req) == "POST /send" : String})505 -> Split.Out(Laws.change(W.Web.reply(s, req)), s, Laws.spent(Laws.Req.form(req), 3n),506 Laws.paid(Laws.Req.form(req), k, 3n), k,507 Laws.Bank.sender(s, Laws.Req.user(req), Laws.Req.pass(req))):508 match req:509 case W.Req{+time, rand, +verb, +path, +user, +pass, +form}:510 +u = Laws.Bank.sender(s, user, pass)511 +rows = W.Web.rows(form, 3n)512 +sp = Rows.spent(rows)513 +pd = Rows.paid(rows, k)514 +r = B.Bank.exec(s, user, pass, time, B.Send{rows})515 -out = Laws.change(W.Web.answer(W.Web.call(W.Web.find(W.Web.paths(), verb ++ " " ++ path, 0n),516 form), s, time, rand, user, pass))517 %Rows.spent_form(form, 3n) : Split.Out(out, s, _, Laws.paid(form, k, 3n), k, u)518 %Rows.paid_form(form, k, 3n) : Split.Out(out, s, sp, _, k, u)519 %Equal.sym(String, verb ++ " " ++ path, "POST /send", send)520 : Split.Out(Laws.change(W.Web.answer(W.Web.call(W.Web.find(W.Web.paths(), _, 0n), form), s,521 time, rand, user, pass)), s, sp, pd, k, u)522 Split.done(r, W.Http.home(), s, user, pass, time, rows, k, u,523 Split.exec(s, user, pass, time, rows, k))524525# LAW split526def Laws.split(s, input, k, b, send, e):527 %e : Split.Out(_, s, Laws.spent(Laws.form(input), 3n), Laws.paid(Laws.form(input), k, 3n), k,528 Laws.sender(s, input))529 Split.reply(s, W.Req.parse(input), k, send)