proof/authority.bend · raw · all files

1# Bend Bank: the proof of LAW authority2# =====================================3#4# A reply changes the bank only by a join or a command (Web.reply_by), so5# a fact about every bank those make is a fact about Web.serve. A join6# opens an account where there was none, and touches no other. A command7# of uk sets uk's own account, then gives its gifts; each gift keeps the8# account it reaches, as uk's request may (Gift.keeps). So every account9# but uk's is Kept.1011import Base12import ../bank.bend as B13import ../web.bend as W14import ../LAWS.bend as Laws15import ./base.bend as L1617# Keep18# ----1920def Keep.refl(a: B.Acc, -u: Maybe<&2, B.Key()>) -> Laws.Keeps(a, a, u):21  match a:22    case B.Acc{pass, +cash, note, line, loan, +held}:23      ({==}, {==}, {==}, {==}, L.Nat.le_refl(cash), +q => e => L.Nat.le_refl(Nat.add(cash, B.Trie.num(q, held))), q => e => {==})2425def Keep.kept_refl(m: Maybe<&2, B.Acc>, -u: Maybe<&2, B.Key()>) -> Laws.Kept(m, m, u):26  match m:27    case None{}:28      Unit{}29    case Some{a}:30      Keep.refl(a, u)3132def Keep.trans(a: B.Acc, b: B.Acc, c: B.Acc, -u: Maybe<&2, B.Key()>, h1: Laws.Keeps(a, b, u),33  h2: Laws.Keeps(b, c, u)) -> Laws.Keeps(a, c, u):34  match a b c:35    case B.Acc{p1, +c1, n1, l1, d1, +w1} B.Acc{p2, +c2, n2, l2, d2, +w2} B.Acc{p3, +c3, n3, l3, d3, +w3}:36      (ep1, en1, el1, ed1, le1, f1, g1) = h137      (ep2, en2, el2, ed2, le2, f2, g2) = h238      (Equal.trans(String, p3, p2, p1, ep2, ep1), Equal.trans(String, n3, n2, n1, en2, en1),39       Equal.trans(Nat, l3, l2, l1, el2, el1), Equal.trans(B.Loan, d3, d2, d1, ed2, ed1),40       L.Nat.le_trans(c1, c2, c3, le1, le2),41       +q => +e => L.Nat.le_trans(Nat.add(c1, B.Trie.num(q, w1)), Nat.add(c2, B.Trie.num(q, w2)), Nat.add(c3, B.Trie.num(q, w3)), f1(q, e), f2(q, e)),42       +q => +e => Equal.trans(Nat, B.Trie.num(q, w3), B.Trie.num(q, w2), B.Trie.num(q, w1), g2(q, e), g1(q, e)))4344def Keep.kept_trans(m0: Maybe<&2, B.Acc>, m1: Maybe<&2, B.Acc>, m2: Maybe<&2, B.Acc>,45  -u: Maybe<&2, B.Key()>, h1: Laws.Kept(m0, m1, u), h2: Laws.Kept(m1, m2, u))46  -> Laws.Kept(m0, m2, u):47  match m0 m1 m2:48    case None{} _ _:49      Unit{}50    case Some{a} None{} _:51      match h1:52    case Some{a} Some{b} None{}:53      match h2:54    case Some{a} Some{b} Some{c}:55      Keep.trans(a, b, c, u, h1, h2)5657# a bank result that does not fail keeps the account at k, which was m058def Keep.R(m0: Maybe<&2, B.Acc>, r: Result<&2, &2, String, B.Bank>, k: B.Key(),59  u: Maybe<&2, B.Key()>) -> Type:60  L.Bank.If(r, b => Laws.Kept(m0, Laws.acct(b, k), u))6162# Gift63# ----6465# an Owe adds to what uk holds66def Keep.owe_le(+uk: B.Key(), +q: B.Key(), +c: Nat, +held: B.Trie<Nat>, +x: Nat,67  e: {Laws.Key.is(Some{uk}, q) == True{} : Bool})68  -> Laws.LE(Nat.add(c, B.Trie.num(q, held)), Nat.add(c, B.Trie.num(q, B.Trie.put(uk, held, Nat.add(B.Trie.num(uk, held), x))))):69  +n = B.Trie.num(uk, held)70  +y = Nat.add(n, x)71  %L.Key.eq_true(uk, q, e) : Laws.LE(Nat.add(c, B.Trie.num(_, held)), Nat.add(c, B.Trie.num(_, B.Trie.put(uk, held, y))))72  %L.Trie.num_put_same(uk, held, y) : Laws.LE(Nat.add(c, n), Nat.add(c, _))73  %L.Nat.add_assoc(c, n, x) : Laws.LE(Nat.add(c, n), _)74  L.Nat.le_add(Nat.add(c, n), x)7576# a Rel moves what uk holds into the cash77def Keep.rel_le(+uk: B.Key(), +q: B.Key(), +c: Nat, +held: B.Trie<Nat>,78  e: {Laws.Key.is(Some{uk}, q) == True{} : Bool})79  -> Laws.LE(Nat.add(c, B.Trie.num(q, held)), Nat.add(Nat.add(c, B.Trie.num(uk, held)), B.Trie.num(q, B.Trie.put(uk, held, 0n)))):80  +n = Nat.add(c, B.Trie.num(uk, held))81  %L.Key.eq_true(uk, q, e) : Laws.LE(Nat.add(c, B.Trie.num(_, held)), Nat.add(n, B.Trie.num(_, B.Trie.put(uk, held, 0n))))82  %L.Trie.num_put_same(uk, held, 0n) : Laws.LE(n, Nat.add(n, _))83  L.Nat.le_add(n, 0n)8485# a gift from uk keeps the account it reaches, as uk's request may86def Gift.keeps(g: B.Gift, +uk: B.Key(),87  a: B.Acc) -> Laws.Keeps(a, B.Gift.give(g, uk, a), Some{uk}):88  match g a:89    case B.Pay{d, +x} B.Acc{pass, +cash, note, line, loan, +held}:90      ({==}, {==}, {==}, {==}, L.Nat.le_add(cash, x), +q => e => L.Nat.le_addr(cash, Nat.add(cash, x), B.Trie.num(q, held), L.Nat.le_add(cash, x)), q => e => {==})91    case B.Owe{d, +x} B.Acc{pass, +cash, note, line, loan, +held}:92      +y = Nat.add(B.Trie.num(uk, held), x)93      ({==}, {==}, {==}, {==}, L.Nat.le_refl(cash), +q => e => Keep.owe_le(uk, q, cash, held, x, e),94       +q => e => L.Trie.num_put_other(q, uk, held, y, L.Key.flip(uk, q, False{}, e)))95    case B.Rel{d} B.Acc{pass, +cash, note, line, loan, +held}:96      ({==}, {==}, {==}, {==}, L.Nat.le_add(cash, B.Trie.num(uk, held)), +q => e => Keep.rel_le(uk, q, cash, held, e),97       +q => e => L.Trie.num_put_other(q, uk, held, 0n, L.Key.flip(uk, q, False{}, e)))9899# h, about the account at k, is about a, since k is d and a is at d100def Keep.at_key(+k: B.Key(), +d: B.Key(), +accts: B.Trie<B.Acc>, +a: B.Acc,101  +m0: Maybe<&2, B.Acc>, +uk: B.Key(), ek: {k == d : B.Key()},102  em: {B.Trie.get(B.Acc, d, accts) == Some{a} : Maybe<&2, B.Acc>},103  h: Laws.Kept(m0, B.Trie.get(B.Acc, k, accts), Some{uk}))104  -> Laws.Kept(m0, Some{a}, Some{uk}):105  %em : Laws.Kept(m0, _, Some{uk})106  %ek : Laws.Kept(m0, B.Trie.get(B.Acc, _, accts), Some{uk})107  h108109# the account at k after a gift to the account a at d110def Keep.gift_at(c: Bool, +k: B.Key(), +d: B.Key(), +accts: B.Trie<B.Acc>, +uk: B.Key(),111  +g: B.Gift, +a: B.Acc, +m0: Maybe<&2, B.Acc>, ec: {B.Key.eq(k, d) == c : Bool},112  em: {B.Trie.get(B.Acc, d, accts) == Some{a} : Maybe<&2, B.Acc>},113  h: Laws.Kept(m0, B.Trie.get(B.Acc, k, accts), Some{uk}))114  -> Laws.Kept(m0, Bool.pick(Maybe<&2, B.Acc>, c, Some{B.Gift.give(g, uk, a)}, B.Trie.get(B.Acc, k, accts)), Some{uk}):115  match c:116    case True{}:117      h2 = Keep.at_key(k, d, accts, a, m0, uk, L.Key.eq_true(k, d, ec), em, h)118      Keep.kept_trans(m0, Some{a}, Some{B.Gift.give(g, uk, a)}, Some{uk}, h2, Gift.keeps(g, uk, a))119    case False{}:120      h121122def Keep.gift_to(c: Bool, m: Maybe<&2, B.Acc>, +vault: Nat, +accts: B.Trie<B.Acc>, +uk: B.Key(),123  +d: B.Key(), +g: B.Gift, +k: B.Key(), +m0: Maybe<&2, B.Acc>,124  em: {B.Trie.get(B.Acc, d, accts) == m : Maybe<&2, B.Acc>},125  h: Laws.Kept(m0, B.Trie.get(B.Acc, k, accts), Some{uk}))126  -> Keep.R(m0, B.Plan.gift.to(c, m, vault, accts, uk, d, g), k, Some{uk}):127  match c m:128    case True{} _:129      Unit{}130    case False{} None{}:131      Unit{}132    case False{} Some{+a}:133      +b = B.Gift.give(g, uk, a)134      %L.Trie.pick_set(B.Acc, k, d, accts, Some{b}) : Laws.Kept(m0, _, Some{uk})135      Keep.gift_at(B.Key.eq(k, d), k, d, accts, uk, g, a, m0, {==}, em, h)136137def Keep.gift(r: Result<&2, &2, String, B.Bank>, +uk: B.Key(), +g: B.Gift, +k: B.Key(),138  +m0: Maybe<&2, B.Acc>, h: Keep.R(m0, r, k, Some{uk}))139  -> Keep.R(m0, B.Plan.gift(r, uk, g), k, Some{uk}):140  match r:141    case Fail{e}:142      Unit{}143    case Done{B.Bank{vault, +accts}}:144      +d = B.Gift.dest(g)145      Keep.gift_to(B.Key.eq(d, uk), B.Trie.get(B.Acc, d, accts), vault, accts, uk, d, g, k, m0, {==}, h)146147def Keep.gifts(gs: List<&2, B.Gift>, +uk: B.Key(), +r: Result<&2, &2, String, B.Bank>,148  +k: B.Key(), +m0: Maybe<&2, B.Acc>, h: Keep.R(m0, r, k, Some{uk}))149  -> Keep.R(m0, B.Plan.gifts(gs, uk, r), k, Some{uk}):150  match gs:151    case Nil{}:152      h153    case +g <> rest:154      Keep.gifts(rest, uk, B.Plan.gift(r, uk, g), k, m0, Keep.gift(r, uk, g, k, m0, h))155156# Exec157# ----158159# setting uk's account keeps the others160def Keep.first(+t: B.Trie<B.Acc>, +uk: B.Key(), +acct: B.Acc, +k: B.Key(),161  ne: {B.Key.eq(k, uk) == False{} : Bool})162  -> Laws.Kept(B.Trie.get(B.Acc, k, t), B.Trie.get(B.Acc, k, B.Trie.set(B.Acc, uk, t, Some{acct})), Some{uk}):163  +m0 = B.Trie.get(B.Acc, k, t)164  %L.Trie.get_other(B.Acc, k, uk, t, Some{acct}, ne) : Laws.Kept(m0, _, Some{uk})165  Keep.kept_refl(m0, Some{uk})166167# a plan of uk keeps every account other than uk's168def Keep.apply(+v: Nat, +t: B.Trie<B.Acc>, +uk: B.Key(), p: B.Plan, +k: B.Key(),169  ne: {B.Key.eq(k, uk) == False{} : Bool})170  -> Keep.R(B.Trie.get(B.Acc, k, t), B.Plan.apply(B.Bank{v, t}, uk, p), k, Some{uk}):171  match p:172    case B.Plan{+acct, gifts}:173      +m0 = B.Trie.get(B.Acc, k, t)174      +r = {Done{B.Bank{v, B.Trie.set(B.Acc, uk, t, Some{acct})}} : Result<&2, &2, String, B.Bank>}175      Keep.gifts(gifts, uk, r, k, m0, Keep.first(t, uk, acct, k, ne))176177def Keep.plan(+v: Nat, +t: B.Trie<B.Acc>, +uk: B.Key(), r: Result<&2, &2, String, B.Plan>,178  +k: B.Key(), ne: {B.Key.eq(k, uk) == False{} : Bool})179  -> Keep.R(B.Trie.get(B.Acc, k, t), B.Bank.plan(B.Bank{v, t}, uk, r), k, Some{uk}):180  match r:181    case Fail{e}:182      Unit{}183    case Done{p}:184      Keep.apply(v, t, uk, p, k, ne)185186# a command keeps every account other than its sender's187def Keep.exec(s: B.Bank, +name: String, +pass: String, +now: Nat, +cmd: B.Cmd, +k: B.Key(),188  no: {Laws.Key.is(Laws.Bank.sender(s, name, pass), k) == False{} : Bool})189  -> Keep.R(Laws.acct(s, k), B.Bank.exec(s, name, pass, now, cmd), k, Laws.Bank.sender(s, name, pass)):190  match s:191    case B.Bank{+v, +t}:192      L.Bank.exec_by(B.Key.of(name), v, t, pass, now, cmd,193        u => b => Laws.Kept(B.Trie.get(B.Acc, k, t), Laws.acct(b, k), u),194        u => {Laws.Key.is(u, k) == False{} : Bool}, no,195        +uk => a => eg => no => Keep.plan(v, t, uk, B.Cmd.plan(cmd, a, now), k, L.Key.flip(uk, k, False{}, no)))196197# Join198# ----199200# the account at k after a new account at j, where there was none201def Keep.new_at(c: Bool, +k: B.Key(), +j: B.Key(), +t: B.Trie<B.Acc>, +acct: B.Acc,202  -u: Maybe<&2, B.Key()>, ec: {B.Key.eq(k, j) == c : Bool},203  ej: {B.Trie.get(B.Acc, j, t) == None{} : Maybe<&2, B.Acc>})204  -> Laws.Kept(B.Trie.get(B.Acc, k, t), Bool.pick(Maybe<&2, B.Acc>, c, Some{acct}, B.Trie.get(B.Acc, k, t)), u):205  match c:206    case True{}:207      %Equal.sym(B.Key(), k, j, L.Key.eq_true(k, j, ec)) : Laws.Kept(B.Trie.get(B.Acc, _, t), Some{acct}, u)208      %Equal.sym(Maybe<&2, B.Acc>, B.Trie.get(B.Acc, j, t), None{}, ej) : Laws.Kept(_, Some{acct}, u)209      Unit{}210    case False{}:211      Keep.kept_refl(B.Trie.get(B.Acc, k, t), u)212213def Keep.new(+k: B.Key(), +j: B.Key(), +t: B.Trie<B.Acc>, +acct: B.Acc, -u: Maybe<&2, B.Key()>,214  ej: {B.Trie.get(B.Acc, j, t) == None{} : Maybe<&2, B.Acc>})215  -> Laws.Kept(B.Trie.get(B.Acc, k, t), B.Trie.get(B.Acc, k, B.Trie.set(B.Acc, j, t, Some{acct})), u):216  +m0 = B.Trie.get(B.Acc, k, t)217  %L.Trie.pick_set(B.Acc, k, j, t, Some{acct}) : Laws.Kept(m0, _, u)218  Keep.new_at(B.Key.eq(k, j), k, j, t, acct, u, {==}, ej)219220# a join opens an account where there was none, and keeps the others221def Keep.join(s: B.Bank, +name: String, +pass: String, +k: B.Key(), -u: Maybe<&2, B.Key()>)222  -> Keep.R(Laws.acct(s, k), B.Bank.join(s, name, pass), k, u):223  match s:224    case B.Bank{+v, +t}:225      L.Bank.join_by(B.Key.of(name), v, t, pass,226        b => Laws.Kept(B.Trie.get(B.Acc, k, t), Laws.acct(b, k), u),227        +j => ej => o => Keep.new(k, j, t, B.Acc.new(pass), u, ej))228229# LAW authority230def Laws.authority(s, input, k, no):231  +u = Laws.sender(s, input)232  +m0 = Laws.acct(s, k)233  -P = {b => Laws.Kept(m0, Laws.acct(b, k), u) : B.Bank -> Type}234  L.Web.reply_by(s, W.Req.parse(input), P, Keep.kept_refl(m0, u),235    +name => Keep.join(s, name, Laws.rand(input), k, u),236    +cmd => Keep.exec(s, Laws.user(input), Laws.key(input), Laws.time(input), cmd, k, no))