proof/conservation.bend · raw · all files

1# Bend Bank: the proof of LAW conservation2# ========================================3#4# A plan's money is its account's worth and its gifts' cash. Every op5# keeps it; applying a plan swaps the sender's worth for the account's6# new worth, and each gift adds its cash to the account it reaches, so7# the total stays. A join takes 1,100 from the vault and opens an8# account worth 1,100 at a key that had none.910import Base11import ../bank.bend as B12import ../web.bend as W13import ../LAWS.bend as Laws14import ./base.bend as L1516# Op17# --1819# the money in a plan: the account's worth and the gifts' cash20def Plan.money(p: B.Plan) -> Nat:21  match p:22    case B.Plan{a, gifts}:23      Nat.add(B.Acc.worth(a), B.Gift.sum(gifts))2425# a planned request that does not fail holds money n26def Plan.Holds(r: Result<&2, &2, String, B.Plan>, n: Nat) -> Type:27  match r:28    case Fail{e}:29      Unit30    case Done{p}:31      {Plan.money(p) == n : Nat}3233# a need keeps the plan, when it holds34def Op.need_holds(test: Bool, -text: String, -p: B.Plan, -n: Nat, h: {test == True{} : Bool} -> {Plan.money(p) == n : Nat}) -> Plan.Holds(B.Op.need(test, text, p), n):35  match test:36    case True{}:37      h({==})38    case False{}:39      Unit{}4041# x of the cash moves into a gift42def Op.give_sum(+c: Nat, +x: Nat, +w: Nat, +g: Nat, -n: Nat, t: {Nat.is_le(x, c) == True{} : Bool}, h: {Nat.add(Nat.add(c, w), g) == n : Nat})43  -> {Nat.add(Nat.add(Nat.sub(c, x), w), Nat.add(x, g)) == n : Nat}:44  +d = Nat.sub(c, x)45  %h : {Nat.add(Nat.add(d, w), Nat.add(x, g)) == _ : Nat}46  %L.Nat.sub_add(c, x, t) : {Nat.add(Nat.add(d, w), Nat.add(x, g)) == Nat.add(Nat.add(_, w), g) : Nat}47  %L.Nat.add_assoc(Nat.add(d, w), x, g) : {_ == Nat.add(Nat.add(Nat.add(d, x), w), g) : Nat}48  %L.Nat.right_comm(d, x, w) : {Nat.add(_, g) == Nat.add(Nat.add(Nat.add(d, x), w), g) : Nat}49  {==}5051# money moves between the cash and the line52def Op.shift_sum(+c: Nat, +l: Nat, +c2: Nat, +l2: Nat, +v: Nat, +g: Nat, -n: Nat,53  e: {Nat.add(c2, l2) == Nat.add(c, l) : Nat}, h: {Nat.add(Nat.add(c, Nat.add(l, v)), g) == n : Nat})54  -> {Nat.add(Nat.add(c2, Nat.add(l2, v)), g) == n : Nat}:55  %h : {Nat.add(Nat.add(c2, Nat.add(l2, v)), g) == _ : Nat}56  %L.Nat.add_assoc(c, l, v) : {Nat.add(Nat.add(c2, Nat.add(l2, v)), g) == Nat.add(_, g) : Nat}57  %e : {Nat.add(Nat.add(c2, Nat.add(l2, v)), g) == Nat.add(Nat.add(_, v), g) : Nat}58  %L.Nat.add_assoc(c2, l2, v) : {Nat.add(_, g) == Nat.add(Nat.add(Nat.add(c2, l2), v), g) : Nat}59  {==}6061# a draw of x from the line: (c + x) + (l - x) == c + l62def Op.draw_eq(+c: Nat, +x: Nat, +l: Nat, t: {Nat.is_le(x, l) == True{} : Bool})63  -> {Nat.add(Nat.add(c, x), Nat.sub(l, x)) == Nat.add(c, l) : Nat}:64  +m = Nat.sub(l, x)65  %L.Nat.sub_add(l, x, t) : {Nat.add(Nat.add(c, x), m) == Nat.add(c, _) : Nat}66  %L.Nat.add_comm(x, m) : {Nat.add(Nat.add(c, x), m) == Nat.add(c, _) : Nat}67  L.Nat.add_assoc(c, x, m)6869# a fund of x into the line: (c - x) + (l + x) == c + l70def Op.fund_eq(+c: Nat, +x: Nat, +l: Nat, t: {Nat.is_le(x, c) == True{} : Bool})71  -> {Nat.add(Nat.sub(c, x), Nat.add(l, x)) == Nat.add(c, l) : Nat}:72  +d = Nat.sub(c, x)73  %L.Nat.sub_add(c, x, t) : {Nat.add(d, Nat.add(l, x)) == Nat.add(_, l) : Nat}74  %L.Nat.add_comm(x, l) : {Nat.add(d, _) == Nat.add(Nat.add(d, x), l) : Nat}75  L.Nat.assoc_r(d, x, l)7677# the money u had held moves into a gift78def Op.drop_sum(+c: Nat, +l: Nat, +s: Nat, +s2: Nat, +y: Nat, +g: Nat, -n: Nat,79  e: {Nat.add(s2, y) == Nat.add(s, 0n) : Nat}, h: {Nat.add(Nat.add(c, Nat.add(l, s)), g) == n : Nat})80  -> {Nat.add(Nat.add(c, Nat.add(l, s2)), Nat.add(y, g)) == n : Nat}:81  %h : {Nat.add(Nat.add(c, Nat.add(l, s2)), Nat.add(y, g)) == _ : Nat}82  +x = Nat.add(Nat.add(c, Nat.add(l, s2)), y)83  %L.Nat.add_assoc(Nat.add(c, Nat.add(l, s2)), y, g) : {_ == Nat.add(Nat.add(c, Nat.add(l, s)), g) : Nat}84  %L.Nat.zero_r(s) : {Nat.add(x, g) == Nat.add(Nat.add(c, Nat.add(l, _)), g) : Nat}85  %e : {Nat.add(x, g) == Nat.add(Nat.add(c, Nat.add(l, _)), g) : Nat}86  %L.Nat.mid2(c, l, s2, y) : {Nat.add(_, g) == Nat.add(Nat.add(c, Nat.add(l, Nat.add(s2, y))), g) : Nat}87  {==}8889# every op keeps the plan's money90def Op.at_holds(op: B.Op, a: B.Acc, gifts: List<&2, B.Gift>, -n: Nat, h: {Plan.money(B.Plan{a, gifts}) == n : Nat})91  -> Plan.Holds(B.Op.at(op, a, gifts), n):92  match op a:93    case B.Need{test, text} a:94      Op.need_holds(test, text, B.Plan{a, gifts}, n, e => h)95    case B.Memo{t} B.Acc{pass, cash, note, line, loan, held}:96      h97    case B.Debt{d} B.Acc{pass, cash, note, line, loan, held}:98      h99    case B.Give{+k, +x} B.Acc{pass, +cash, note, +line, loan, +held}:100      +w = Nat.add(line, B.Trie.sum(held))101      +a = {B.Acc{pass, Nat.sub(cash, x), note, line, loan, held} : B.Acc}102      Op.need_holds(Nat.is_le(x, cash), "you do not have that much", B.Plan{a, B.Pay{k, x} <> gifts}, n,103        t => Op.give_sum(cash, x, w, B.Gift.sum(gifts), n, t, h))104    case B.Lock{+k, +x} B.Acc{pass, +cash, note, +line, loan, +held}:105      +w = Nat.add(line, B.Trie.sum(held))106      +a = {B.Acc{pass, Nat.sub(cash, x), note, line, loan, held} : B.Acc}107      Op.need_holds(Nat.is_le(x, cash), "you do not have that much", B.Plan{a, B.Owe{k, x} <> gifts}, n,108        t => Op.give_sum(cash, x, w, B.Gift.sum(gifts), n, t, h))109    case B.Open{k} B.Acc{pass, cash, note, line, loan, held}:110      h111    case B.Drop{+k} B.Acc{pass, +cash, note, +line, loan, +held}:112      +s2 = B.Trie.sum(B.Trie.put(k, held, 0n))113      +y = B.Trie.num(k, held)114      Op.drop_sum(cash, line, B.Trie.sum(held), s2, y, B.Gift.sum(gifts), n, L.Trie.sum_put(k, held, 0n), h)115    case B.Draw{+x} B.Acc{pass, +cash, note, +line, loan, +held}:116      +a = {B.Acc{pass, Nat.add(cash, x), note, Nat.sub(line, x), loan, held} : B.Acc}117      Op.need_holds(Nat.is_le(x, line), "the bank has no more credit for you", B.Plan{a, gifts}, n,118        t => Op.shift_sum(cash, line, Nat.add(cash, x), Nat.sub(line, x), B.Trie.sum(held), B.Gift.sum(gifts), n, Op.draw_eq(cash, x, line, t), h))119    case B.Fund{+x} B.Acc{pass, +cash, note, +line, loan, +held}:120      +a = {B.Acc{pass, Nat.sub(cash, x), note, Nat.add(line, x), loan, held} : B.Acc}121      Op.need_holds(Nat.is_le(x, cash), "you do not have that much", B.Plan{a, gifts}, n,122        t => Op.shift_sum(cash, line, Nat.sub(cash, x), Nat.add(line, x), B.Trie.sum(held), B.Gift.sum(gifts), n, Op.fund_eq(cash, x, line, t), h))123124# one more op keeps the money125def Op.step_holds(r: Result<&2, &2, String, B.Plan>, +op: B.Op, -n: Nat, h: Plan.Holds(r, n)) -> Plan.Holds(B.Op.step(r, op), n):126  match r:127    case Fail{e}:128      Unit{}129    case Done{B.Plan{a, gifts}}:130      Op.at_holds(op, a, gifts, n, h)131132# a run of ops keeps the money133def Op.run_holds(ops: List<&2, B.Op>, +r: Result<&2, &2, String, B.Plan>, -n: Nat, h: Plan.Holds(r, n)) -> Plan.Holds(B.Op.run(ops, r), n):134  match ops:135    case Nil{}:136      h137    case +op <> rest:138      Op.run_holds(rest, B.Op.step(r, op), n, Op.step_holds(r, op, n, h))139140# Gift141# ----142143# l + (k + x) == (l + x) + k144def Gift.swap(+l: Nat, +k: Nat, +x: Nat) -> {Nat.add(l, Nat.add(k, x)) == Nat.add(Nat.add(l, x), k) : Nat}:145  %L.Nat.add_comm(x, k) : {Nat.add(l, _) == Nat.add(Nat.add(l, x), k) : Nat}146  L.Nat.assoc_r(l, x, k)147148# a gift adds its cash to the account's worth149def Gift.worth(g: B.Gift, +u: B.Key(), a: B.Acc) -> {B.Acc.worth(B.Gift.give(g, u, a)) == Nat.add(B.Acc.worth(a), B.Gift.cash(g)) : Nat}:150  match g a:151    case B.Pay{d, x} B.Acc{pass, cash, note, line, loan, held}:152      L.Nat.right_comm(cash, x, Nat.add(line, B.Trie.sum(held)))153    case B.Owe{d, +x} B.Acc{pass, +cash, note, +line, loan, +held}:154      +k = B.Trie.num(u, held)155      +p = B.Trie.sum(B.Trie.put(u, held, Nat.add(k, x)))156      +t = B.Trie.sum(held)157      +e1 = Equal.trans(Nat, Nat.add(p, k), Nat.add(t, Nat.add(k, x)), Nat.add(Nat.add(t, x), k), L.Trie.sum_put(u, held, Nat.add(k, x)), Gift.swap(t, k, x))158      +e2 = Equal.sym(Nat, p, Nat.add(t, x), L.Nat.cancel(p, Nat.add(t, x), k, e1))159      %e2 : {Nat.add(cash, Nat.add(line, _)) == Nat.add(Nat.add(cash, Nat.add(line, t)), x) : Nat}160      L.Nat.mid2(cash, line, t, x)161    case B.Rel{d} B.Acc{pass, +cash, note, +line, loan, +held}:162      +k = B.Trie.num(u, held)163      +p = B.Trie.sum(B.Trie.put(u, held, 0n))164      +t = B.Trie.sum(held)165      +x = Nat.add(Nat.add(cash, k), Nat.add(line, p))166      %L.Nat.add_zero(Nat.add(cash, Nat.add(line, t))) : {x == _ : Nat}167      %L.Nat.zero_r(t) : {x == Nat.add(cash, Nat.add(line, _)) : Nat}168      %L.Trie.sum_put(u, held, 0n) : {x == Nat.add(cash, Nat.add(line, _)) : Nat}169      %L.Nat.add_assoc(line, p, k) : {x == Nat.add(cash, _) : Nat}170      %L.Nat.add_comm(k, Nat.add(line, p)) : {x == Nat.add(cash, _) : Nat}171      %L.Nat.add_assoc(cash, k, Nat.add(line, p)) : {x == _ : Nat}172      {==}173174# Plan175# ----176177# a bank result that does not fail holds total n178def Bank.Holds(r: Result<&2, &2, String, B.Bank>, n: Nat) -> Type:179  L.Bank.If(r, b => {B.Bank.total(b) == n : Nat})180181# swapping one account's old worth w for w + x adds x to the sum182def Acc.sum_gift(+s2: Nat, +w: Nat, +t: Nat, +x: Nat, +v: Nat, -n: Nat, e: {Nat.add(s2, w) == Nat.add(t, Nat.add(w, x)) : Nat}, h: {Nat.add(v, t) == n : Nat})183  -> {Nat.add(v, s2) == Nat.add(n, x) : Nat}:184  %h : {Nat.add(v, s2) == Nat.add(_, x) : Nat}185  +e1 = Equal.trans(Nat, Nat.add(s2, w), Nat.add(t, Nat.add(w, x)), Nat.add(Nat.add(t, x), w), e, Gift.swap(t, w, x))186  +e2 = Equal.sym(Nat, s2, Nat.add(t, x), L.Nat.cancel(s2, Nat.add(t, x), w, e1))187  %e2 : {Nat.add(v, _) == Nat.add(Nat.add(v, t), x) : Nat}188  L.Nat.assoc_r(v, t, x)189190# the account sum after a gift to the account a at k191def Plan.gift_eq(+k: B.Key(), +accts: B.Trie<B.Acc>, +u: B.Key(), +g: B.Gift, +a: B.Acc, em: {B.Trie.get(B.Acc, k, accts) == Some{a} : Maybe<&2, B.Acc>})192  -> {Nat.add(B.Acc.sum(B.Trie.set(B.Acc, k, accts, Some{B.Gift.give(g, u, a)})), B.Acc.worth(a)) == Nat.add(B.Acc.sum(accts), Nat.add(B.Acc.worth(a), B.Gift.cash(g))) : Nat}:193  +b = B.Gift.give(g, u, a)194  +s2 = B.Acc.sum(B.Trie.set(B.Acc, k, accts, Some{b}))195  %Gift.worth(g, u, a) : {Nat.add(s2, B.Acc.worth(a)) == Nat.add(B.Acc.sum(accts), _) : Nat}196  %em : {Nat.add(s2, B.Acc.worth_of(_)) == Nat.add(B.Acc.sum(accts), B.Acc.worth(b)) : Nat}197  L.Acc.sum_set(k, accts, Some{b})198199# a gift to an account adds its cash to the total200def Plan.gift_to_holds(self: Bool, m: Maybe<&2, B.Acc>, +vault: Nat, +accts: B.Trie<B.Acc>, +u: B.Key(), +k: B.Key(), +g: B.Gift, -n: Nat,201  em: {B.Trie.get(B.Acc, k, accts) == m : Maybe<&2, B.Acc>}, h: {Nat.add(vault, B.Acc.sum(accts)) == n : Nat})202  -> Bank.Holds(B.Plan.gift.to(self, m, vault, accts, u, k, g), Nat.add(n, B.Gift.cash(g))):203  match self m:204    case True{} _:205      Unit{}206    case False{} None{}:207      Unit{}208    case False{} Some{+a}:209      +s2 = B.Acc.sum(B.Trie.set(B.Acc, k, accts, Some{B.Gift.give(g, u, a)}))210      Acc.sum_gift(s2, B.Acc.worth(a), B.Acc.sum(accts), B.Gift.cash(g), vault, n, Plan.gift_eq(k, accts, u, g, a, em), h)211212# one more gift adds its cash to the total213def Plan.gift_holds(r: Result<&2, &2, String, B.Bank>, +u: B.Key(), +g: B.Gift, -n: Nat, h: Bank.Holds(r, n))214  -> Bank.Holds(B.Plan.gift(r, u, g), Nat.add(n, B.Gift.cash(g))):215  match r:216    case Fail{e}:217      Unit{}218    case Done{B.Bank{vault, +accts}}:219      +k = B.Gift.dest(g)220      Plan.gift_to_holds(B.Key.eq(k, u), B.Trie.get(B.Acc, k, accts), vault, accts, u, k, g, n, {==}, h)221222# the gifts add all their cash to the total223def Plan.gifts_holds(gs: List<&2, B.Gift>, +u: B.Key(), +r: Result<&2, &2, String, B.Bank>, +n: Nat, h: Bank.Holds(r, n))224  -> Bank.Holds(B.Plan.gifts(gs, u, r), Nat.add(n, B.Gift.sum(gs))):225  match gs:226    case Nil{}:227      %L.Nat.add_zero(n) : Bank.Holds(r, _)228      h229    case +g <> rest:230      %L.Nat.add_assoc(n, B.Gift.cash(g), B.Gift.sum(rest)) : Bank.Holds(B.Plan.gifts(rest, u, B.Plan.gift(r, u, g)), _)231      Plan.gifts_holds(rest, u, B.Plan.gift(r, u, g), Nat.add(n, B.Gift.cash(g)), Plan.gift_holds(r, u, g, n, h))232233# (a + g) + w0 == t + w0, when a + w0 == t + wn and wn + g == w0 + 0234def Plan.balance_w(+a: Nat, +g: Nat, +w0: Nat, +t: Nat, +wn: Nat,235  e1: {Nat.add(a, w0) == Nat.add(t, wn) : Nat}, e2: {Nat.add(wn, g) == Nat.add(w0, 0n) : Nat})236  -> {Nat.add(Nat.add(a, g), w0) == Nat.add(t, w0) : Nat}:237  +x = Nat.add(Nat.add(a, w0), g)238  %L.Nat.right_comm(a, w0, g) : {_ == Nat.add(t, w0) : Nat}239  %L.Nat.zero_r(w0) : {x == Nat.add(t, _) : Nat}240  %e2 : {x == Nat.add(t, _) : Nat}241  %L.Nat.add_assoc(t, wn, g) : {x == _ : Nat}242  %e1 : {x == Nat.add(_, g) : Nat}243  {==}244245# (v + a) + g == v + t: the plan's money replaces the sender's worth246def Plan.balance(+v: Nat, +a: Nat, +g: Nat, +w0: Nat, +t: Nat, +wn: Nat,247  e1: {Nat.add(a, w0) == Nat.add(t, wn) : Nat}, e2: {Nat.add(wn, g) == Nat.add(w0, 0n) : Nat})248  -> {Nat.add(Nat.add(v, a), g) == Nat.add(v, t) : Nat}:249  +e3 = L.Nat.cancel(Nat.add(a, g), t, w0, Plan.balance_w(a, g, w0, t, wn, e1, e2))250  %e3 : {Nat.add(Nat.add(v, a), g) == Nat.add(v, _) : Nat}251  %L.Nat.add_assoc(v, a, g) : {Nat.add(Nat.add(v, a), g) == _ : Nat}252  {==}253254# applying a plan that holds the sender's worth keeps the total255def Plan.apply_holds(+v: Nat, +t: B.Trie<B.Acc>, +u: B.Key(), p: B.Plan,256  e: {Plan.money(p) == Nat.add(B.Acc.worth_of(B.Trie.get(B.Acc, u, t)), 0n) : Nat})257  -> Bank.Holds(B.Plan.apply(B.Bank{v, t}, u, p), Nat.add(v, B.Acc.sum(t))):258  match p:259    case B.Plan{+acct, +gifts}:260      +a = B.Acc.sum(B.Trie.set(B.Acc, u, t, Some{acct}))261      +r = {Done{B.Bank{v, B.Trie.set(B.Acc, u, t, Some{acct})}} : Result<&2, &2, String, B.Bank>}262      +w0 = B.Acc.worth_of(B.Trie.get(B.Acc, u, t))263      +g = B.Gift.sum(gifts)264      %Plan.balance(v, a, g, w0, B.Acc.sum(t), B.Acc.worth(acct), L.Acc.sum_set(u, t, Some{acct}), e) : Bank.Holds(B.Plan.gifts(gifts, u, r), _)265      Plan.gifts_holds(gifts, u, r, Nat.add(v, a), {==})266267# Bank268# ----269270# a planned request keeps the total271def Bank.plan_holds(+v: Nat, +t: B.Trie<B.Acc>, +k: B.Key(), r: Result<&2, &2, String, B.Plan>,272  h: Plan.Holds(r, Nat.add(B.Acc.worth_of(B.Trie.get(B.Acc, k, t)), 0n)))273  -> Bank.Holds(B.Bank.plan(B.Bank{v, t}, k, r), Nat.add(v, B.Acc.sum(t))):274  match r:275    case Fail{e}:276      Unit{}277    case Done{p}:278      Plan.apply_holds(v, t, k, p, h)279280# a command's plan holds the money its account started with281def Bank.plan_start(+t: B.Trie<B.Acc>, +k: B.Key(), +a: B.Acc, +now: Nat, +cmd: B.Cmd, eg: {Some{a} == B.Trie.get(B.Acc, k, t) : Maybe<&2, B.Acc>})282  -> Plan.Holds(B.Cmd.plan(cmd, a, now), Nat.add(B.Acc.worth_of(B.Trie.get(B.Acc, k, t)), 0n)):283  %eg : Plan.Holds(B.Cmd.plan(cmd, a, now), Nat.add(B.Acc.worth_of(_), 0n))284  Op.run_holds(B.Cmd.ops(cmd, a, now), Done{B.Plan{a, Nil{}}}, Nat.add(B.Acc.worth(a), 0n), {==})285286# an exec keeps the total287def Bank.exec_holds(s: B.Bank, +name: String, +pass: String, +now: Nat, +cmd: B.Cmd) -> Bank.Holds(B.Bank.exec(s, name, pass, now, cmd), B.Bank.total(s)):288  match s:289    case B.Bank{+v, +t}:290      L.Bank.exec_by(B.Key.of(name), v, t, pass, now, cmd,291        u => b => {B.Bank.total(b) == Nat.add(v, B.Acc.sum(t)) : Nat},292        u => Unit, Unit{},293        +k => +a => eg => r => Bank.plan_holds(v, t, k, B.Cmd.plan(cmd, a, now), Bank.plan_start(t, k, a, now, cmd, eg)))294295# Join296# ----297298# (v - 1100) + a == v + t, when the vault has 1,100 and a + 0 == t + 1100299def Bank.join_sum(+v: Nat, +a: Nat, +t: Nat, o: {Nat.is_le(1100n, v) == True{} : Bool}, e: {Nat.add(a, 0n) == Nat.add(t, 1100n) : Nat})300  -> {Nat.add(Nat.sub(v, 1100n), a) == Nat.add(v, t) : Nat}:301  +d = Nat.sub(v, 1100n)302  +e2 = Equal.trans(Nat, Nat.add(t, 1100n), Nat.add(a, 0n), a, Equal.sym(Nat, Nat.add(a, 0n), Nat.add(t, 1100n), e), L.Nat.zero_r(a))303  %e2 : {Nat.add(d, _) == Nat.add(v, t) : Nat}304  %L.Nat.sub_add(v, 1100n, o) : {Nat.add(d, Nat.add(t, 1100n)) == Nat.add(_, t) : Nat}305  %L.Nat.add_comm(1100n, t) : {Nat.add(d, _) == Nat.add(Nat.add(d, 1100n), t) : Nat}306  %L.Nat.assoc_r(d, 1100n, t) : {Nat.add(d, Nat.add(1100n, t)) == _ : Nat}307  {==}308309# an account worth 1,100, opened where there was none, keeps the total310def Bank.open_holds(+v: Nat, +t: B.Trie<B.Acc>, +k: B.Key(), +pass: String,311  em: {B.Trie.get(B.Acc, k, t) == None{} : Maybe<&2, B.Acc>}, o: {Nat.is_le(1100n, v) == True{} : Bool})312  -> {B.Bank.total(L.Bank.opening(v, t, k, pass)) == Nat.add(v, B.Acc.sum(t)) : Nat}:313  +a = B.Acc.sum(B.Trie.set(B.Acc, k, t, Some{B.Acc.new(pass)}))314  +m = B.Trie.get(B.Acc, k, t)315  +w = Equal.cong(Maybe<&2, B.Acc>, Nat, x => Nat.add(a, B.Acc.worth_of(x)), None{}, m, Equal.sym(Maybe<&2, B.Acc>, m, None{}, em))316  +e = Equal.trans(Nat, Nat.add(a, 0n), Nat.add(a, B.Acc.worth_of(m)), Nat.add(B.Acc.sum(t), 1100n), w, L.Acc.sum_set(k, t, Some{B.Acc.new(pass)}))317  Bank.join_sum(v, a, B.Acc.sum(t), o, e)318319# a join keeps the total320def Bank.join_holds(s: B.Bank, +name: String, +pass: String) -> Bank.Holds(B.Bank.join(s, name, pass), B.Bank.total(s)):321  match s:322    case B.Bank{+v, +t}:323      L.Bank.join_by(B.Key.of(name), v, t, pass,324        b => {B.Bank.total(b) == Nat.add(v, B.Acc.sum(t)) : Nat},325        +k => em => o => Bank.open_holds(v, t, k, pass, em, o))326327# LAW conservation328def Laws.conservation(s, input):329  +t = B.Bank.total(s)330  -P = {b => {B.Bank.total(b) == t : Nat} : B.Bank -> Type}331  L.Web.reply_by(s, W.Req.parse(input), P, {==},332    +name => Bank.join_holds(s, name, Laws.rand(input)),333    +cmd => Bank.exec_holds(s, Laws.user(input), Laws.key(input), Laws.time(input), cmd))