proof/base.bend · raw · all files

1# Bend Bank: lemmas the proofs share2# ==================================3#4# Facts about Nat, Bool, Maybe, keys, tries, accounts and replies, used5# by the proofs of the laws. A reply changes the bank only by a join or a6# command (Web.reply_by), so a fact about every bank those make is a fact7# about Web.serve. Each law has its own file in proof/; PROOF.bend imports8# them all.910import Base11import ../bank.bend as B12import ../web.bend as W13import ../LAWS.bend as Laws1415# Logic16# -----1718# G when m is Some, Unit when None19def Maybe.If(-A: Data, m: Maybe<&2, A>, G: Type) -> Type:20  match m:21    case None{}:22      Unit23    case Some{x}:24      G2526# None is not Some: anything follows27def Maybe.none_some(-A: Data, -b: A, -G: Type, e: {None{} == Some{b} : Maybe<&2, A>}) -> G:28  %e : Maybe.If(A, _, G)29  Unit{}3031# Some is not None: anything follows32def Maybe.some_none(-A: Data, -b: A, -G: Type, e: {Some{b} == None{} : Maybe<&2, A>}) -> G:33  Maybe.none_some(A, b, G, Equal.sym(Maybe<&2, A>, Some{b}, None{}, e))3435# Nat36# ---3738def Nat.add_zero(a: Nat) -> {a == Nat.add(a, 0n) : Nat}:39  match a:40    case 0n:41      {==}42    case 1n+p:43      %Nat.add_zero(p) : {1n+p == 1n+_ : Nat}44      {==}4546def Nat.zero_r(a: Nat) -> {Nat.add(a, 0n) == a : Nat}:47  Equal.sym(Nat, a, Nat.add(a, 0n), Nat.add_zero(a))4849def Nat.add_succ(a: Nat, -b: Nat) -> {1n+Nat.add(a, b) == Nat.add(a, 1n+b) : Nat}:50  match a:51    case 0n:52      {==}53    case 1n+p:54      %Nat.add_succ(p, b) : {2n+Nat.add(p, b) == 1n+_ : Nat}55      {==}5657def Nat.add_comm(a: Nat, +b: Nat) -> {Nat.add(a, b) == Nat.add(b, a) : Nat}:58  match a:59    case 0n:60      %Nat.add_zero(b) : {b == _ : Nat}61      {==}62    case 1n+p:63      %Nat.add_succ(b, p) : {1n+Nat.add(p, b) == _ : Nat}64      %Nat.add_comm(p, b) : {1n+Nat.add(p, b) == 1n+_ : Nat}65      {==}6667def Nat.add_assoc(a: Nat, -b: Nat, -c: Nat) -> {Nat.add(Nat.add(a, b), c) == Nat.add(a, Nat.add(b, c)) : Nat}:68  match a:69    case 0n:70      {==}71    case 1n+p:72      %Nat.add_assoc(p, b, c) : {1n+Nat.add(Nat.add(p, b), c) == 1n+_ : Nat}73      {==}7475# the middle terms of a triple sum swap76def Nat.add_swap(x: Nat, +y: Nat, -z: Nat) -> {Nat.add(x, Nat.add(y, z)) == Nat.add(y, Nat.add(x, z)) : Nat}:77  match x:78    case 0n:79      {==}80    case 1n+q:81      %Nat.add_succ(y, Nat.add(q, z)) : {1n+Nat.add(q, Nat.add(y, z)) == _ : Nat}82      %Nat.add_swap(q, y, z) : {1n+Nat.add(q, Nat.add(y, z)) == 1n+_ : Nat}83      {==}8485def Nat.assoc_r(a: Nat, -b: Nat, -c: Nat) -> {Nat.add(a, Nat.add(b, c)) == Nat.add(Nat.add(a, b), c) : Nat}:86  Equal.sym(Nat, Nat.add(Nat.add(a, b), c), Nat.add(a, Nat.add(b, c)), Nat.add_assoc(a, b, c))8788# (x + r) + y == (y + r) + x89def Nat.swap13(+x: Nat, +r: Nat, +y: Nat) -> {Nat.add(Nat.add(x, r), y) == Nat.add(Nat.add(y, r), x) : Nat}:90  %Nat.assoc_r(x, r, y) : {_ == Nat.add(Nat.add(y, r), x) : Nat}91  %Nat.assoc_r(y, r, x) : {Nat.add(x, Nat.add(r, y)) == _ : Nat}92  %Nat.add_comm(y, r) : {Nat.add(x, _) == Nat.add(y, Nat.add(r, x)) : Nat}93  %Nat.add_comm(x, r) : {Nat.add(x, Nat.add(y, r)) == Nat.add(y, _) : Nat}94  Nat.add_swap(x, y, r)9596# a + (h + (x + y)) == (a + (x + h)) + y97def Nat.mid(+a: Nat, +x: Nat, +h: Nat, +y: Nat) -> {Nat.add(a, Nat.add(h, Nat.add(x, y))) == Nat.add(Nat.add(a, Nat.add(x, h)), y) : Nat}:98  %Nat.assoc_r(a, Nat.add(x, h), y) : {Nat.add(a, Nat.add(h, Nat.add(x, y))) == _ : Nat}99  %Nat.assoc_r(x, h, y) : {Nat.add(a, Nat.add(h, Nat.add(x, y))) == Nat.add(a, _) : Nat}100  %Nat.add_swap(x, h, y) : {Nat.add(a, _) == Nat.add(a, Nat.add(x, Nat.add(h, y))) : Nat}101  {==}102103# a + (l + (x + y)) == (a + (l + x)) + y104def Nat.mid2(+a: Nat, +l: Nat, +x: Nat, +y: Nat) -> {Nat.add(a, Nat.add(l, Nat.add(x, y))) == Nat.add(Nat.add(a, Nat.add(l, x)), y) : Nat}:105  %Nat.assoc_r(a, Nat.add(l, x), y) : {Nat.add(a, Nat.add(l, Nat.add(x, y))) == _ : Nat}106  %Nat.assoc_r(l, x, y) : {Nat.add(a, Nat.add(l, Nat.add(x, y))) == Nat.add(a, _) : Nat}107  {==}108109# (a + b) + c == (a + c) + b110def Nat.right_comm(+a: Nat, +b: Nat, +c: Nat) -> {Nat.add(Nat.add(a, b), c) == Nat.add(Nat.add(a, c), b) : Nat}:111  %Nat.assoc_r(a, b, c) : {_ == Nat.add(Nat.add(a, c), b) : Nat}112  %Nat.assoc_r(a, c, b) : {Nat.add(a, Nat.add(b, c)) == _ : Nat}113  %Nat.add_comm(b, c) : {Nat.add(a, Nat.add(b, c)) == Nat.add(a, _) : Nat}114  {==}115116# G when b is True, Unit when False117def Bool.If(b: Bool, G: Type) -> Type:118  match b:119    case True{}:120      G121    case False{}:122      Unit123124# False is not True: anything follows125def Bool.false_true(-G: Type, e: {False{} == True{} : Bool}) -> G:126  %e : Bool.If(_, G)127  Unit{}128129# (x - y) + y == x, when y <= x130def Nat.sub_add(+x: Nat, +y: Nat, h: {Nat.is_le(y, x) == True{} : Bool}) -> {Nat.add(Nat.sub(x, y), y) == x : Nat}:131  match x y:132    case 0n 0n:133      {==}134    case 0n 1n+q:135      Bool.false_true({Nat.add(Nat.sub(0n, 1n+q), 1n+q) == 0n : Nat}, h)136    case 1n+p 0n:137      %Nat.add_zero(1n+p) : {_ == 1n+p : Nat}138      {==}139    case 1n+p 1n+q:140      %Nat.add_succ(Nat.sub(p, q), q) : {_ == 1n+p : Nat}141      %Nat.sub_add(p, q, h) : {1n+Nat.add(Nat.sub(p, q), q) == 1n+_ : Nat}142      {==}143144def Nat.le_refl(c: Nat) -> Laws.LE(c, c):145  match c:146    case 0n:147      {==}148    case 1n+p:149      Nat.le_refl(p)150151def Nat.le_add(c: Nat, +x: Nat) -> Laws.LE(c, Nat.add(c, x)):152  match c x:153    case 0n 0n:154      {==}155    case 0n 1n+q:156      {==}157    case 1n+p _:158      Nat.le_add(p, x)159160def Nat.le_trans(a: Nat, b: Nat, c: Nat, h1: Laws.LE(a, b), h2: Laws.LE(b, c)) -> Laws.LE(a, c):161  match a b c:162    case 0n _ 0n:163      {==}164    case 0n _ 1n+r:165      {==}166    case 1n+p 0n _:167      Bool.false_true(Laws.LE(1n+p, c), h1)168    case 1n+p 1n+q 0n:169      Bool.false_true(Laws.LE(1n+p, 0n), h2)170    case 1n+p 1n+q 1n+r:171      Nat.le_trans(p, q, r, h1, h2)172173# c <= d gives a + c <= a + d174def Nat.le_addl(a: Nat, -c: Nat, -d: Nat,175  h: Laws.LE(c, d)) -> Laws.LE(Nat.add(a, c), Nat.add(a, d)):176  match a:177    case 0n:178      h179    case 1n+p:180      Nat.le_addl(p, c, d, h)181182# a <= b gives a + d <= b + d183def Nat.le_addr(a: Nat, +b: Nat, +d: Nat,184  h: Laws.LE(a, b)) -> Laws.LE(Nat.add(a, d), Nat.add(b, d)):185  match a b:186    case 0n _:187      %Nat.add_comm(d, b) : Laws.LE(d, _)188      Nat.le_add(d, b)189    case 1n+p 0n:190      Bool.false_true(Laws.LE(Nat.add(1n+p, d), d), h)191    case 1n+p 1n+r:192      Nat.le_addr(p, r, d, h)193194# a <= b and c <= d give a + c <= b + d195def Nat.le_mono(+a: Nat, +b: Nat, +c: Nat, +d: Nat, h1: Laws.LE(a, b),196  h2: Laws.LE(c, d)) -> Laws.LE(Nat.add(a, c), Nat.add(b, d)):197  Nat.le_trans(Nat.add(a, c), Nat.add(a, d), Nat.add(b, d), Nat.le_addl(a, c, d, h2), Nat.le_addr(a, b, d, h1))198199def Nat.pred(n: Nat) -> Nat:200  match n:201    case 0n:202      0n203    case 1n+p:204      p205206# a + c == b + c gives a == b207def Nat.cancel(+a: Nat, +b: Nat, +c: Nat, h: {Nat.add(a, c) == Nat.add(b, c) : Nat}) -> {a == b : Nat}:208  match c:209    case 0n:210      %Nat.zero_r(a) : {_ == b : Nat}211      %Nat.zero_r(b) : {Nat.add(a, 0n) == _ : Nat}212      h213    case 1n+q:214      +x = Nat.add(a, q)215      +y = Nat.add(b, q)216      e1 = Equal.trans(Nat, 1n+x, Nat.add(a, 1n+q), Nat.add(b, 1n+q), Nat.add_succ(a, q), h)217      e2 = Equal.trans(Nat, 1n+x, Nat.add(b, 1n+q), 1n+y, e1, Equal.sym(Nat, 1n+y, Nat.add(b, 1n+q), Nat.add_succ(b, q)))218      Nat.cancel(a, b, q, Equal.cong(Nat, Nat, Nat.pred, 1n+x, 1n+y, e2))219220# Trie221# ----222223# the value at j after a set at k: the new one if j is k, else the old224def Trie.pick_set(-V: Data, +j: B.Key(), +k: B.Key(), +t: B.Trie<V>, +m: Maybe<&2, V>)225  -> {Bool.pick(Maybe<&2, V>, B.Key.eq(j, k), m, B.Trie.get(V, j, t)) == B.Trie.get(V, j, B.Trie.set(V, k, t, m)) : Maybe<&2, V>}:226  match j k:227    case Nil{} Nil{}:228      {==}229    case Nil{} False{} <> ys:230      {==}231    case Nil{} True{} <> ys:232      {==}233    case False{} <> xs Nil{}:234      {==}235    case True{} <> xs Nil{}:236      {==}237    case False{} <> xs False{} <> ys:238      Trie.pick_set(V, xs, ys, B.Trie.lo(V, t), m)239    case False{} <> xs True{} <> ys:240      {==}241    case True{} <> xs False{} <> ys:242      {==}243    case True{} <> xs True{} <> ys:244      Trie.pick_set(V, xs, ys, B.Trie.hi(V, t), m)245246# a key holds what was just set at it247def Trie.get_same(-V: Data, k: B.Key(), +t: B.Trie<V>, +m: Maybe<&2, V>) -> {m == B.Trie.get(V, k, B.Trie.set(V, k, t, m)) : Maybe<&2, V>}:248  match k:249    case Nil{}:250      {==}251    case False{} <> ks:252      Trie.get_same(V, ks, B.Trie.lo(V, t), m)253    case True{} <> ks:254      Trie.get_same(V, ks, B.Trie.hi(V, t), m)255256# setting k leaves the value at another key257def Trie.get_other(-V: Data, +q: B.Key(), +k: B.Key(), +t: B.Trie<V>, +m: Maybe<&2, V>, ne: {B.Key.eq(q, k) == False{} : Bool})258  -> {B.Trie.get(V, q, t) == B.Trie.get(V, q, B.Trie.set(V, k, t, m)) : Maybe<&2, V>}:259  %Trie.pick_set(V, q, k, t, m) : {B.Trie.get(V, q, t) == _ : Maybe<&2, V>}260  %Equal.sym(Bool, B.Key.eq(q, k), False{}, ne) : {B.Trie.get(V, q, t) == Bool.pick(Maybe<&2, V>, _, m, B.Trie.get(V, q, t)) : Maybe<&2, V>}261  {==}262263def Key.eq_true(a: B.Key(), b: B.Key(), e: {B.Key.eq(a, b) == True{} : Bool}) -> {a == b : B.Key()}:264  match a b:265    case Nil{} Nil{}:266      {==}267    case Nil{} False{} <> ys:268      Bool.false_true({Nil{} == False{} <> ys : B.Key()}, e)269    case Nil{} True{} <> ys:270      Bool.false_true({Nil{} == True{} <> ys : B.Key()}, e)271    case False{} <> xs Nil{}:272      Bool.false_true({False{} <> xs == Nil{} : B.Key()}, e)273    case True{} <> xs Nil{}:274      Bool.false_true({True{} <> xs == Nil{} : B.Key()}, e)275    case False{} <> xs False{} <> ys:276      %Key.eq_true(xs, ys, e) : {False{} <> xs == False{} <> _ : B.Key()}277      {==}278    case False{} <> xs True{} <> ys:279      Bool.false_true({False{} <> xs == True{} <> ys : B.Key()}, e)280    case True{} <> xs False{} <> ys:281      Bool.false_true({True{} <> xs == False{} <> ys : B.Key()}, e)282    case True{} <> xs True{} <> ys:283      %Key.eq_true(xs, ys, e) : {True{} <> xs == True{} <> _ : B.Key()}284      {==}285286def Key.eq_sym(a: B.Key(), b: B.Key()) -> {B.Key.eq(a, b) == B.Key.eq(b, a) : Bool}:287  match a b:288    case Nil{} Nil{}:289      {==}290    case Nil{} False{} <> ys:291      {==}292    case Nil{} True{} <> ys:293      {==}294    case False{} <> xs Nil{}:295      {==}296    case True{} <> xs Nil{}:297      {==}298    case False{} <> xs False{} <> ys:299      Key.eq_sym(xs, ys)300    case False{} <> xs True{} <> ys:301      {==}302    case True{} <> xs False{} <> ys:303      {==}304    case True{} <> xs True{} <> ys:305      Key.eq_sym(xs, ys)306307# eq(a, b) is c, so eq(b, a) is308def Key.flip(+a: B.Key(), +b: B.Key(), -c: Bool, e: {B.Key.eq(a, b) == c : Bool}) -> {B.Key.eq(b, a) == c : Bool}:309  %Key.eq_sym(a, b) : {_ == c : Bool}310  e311312# setting k to m swaps k's old amount for m's in the sum313def Trie.sum_set(+k: B.Key(), +t: B.Trie<Nat>, +m: Maybe<&2, Nat>)314  -> {Nat.add(B.Trie.sum(B.Trie.set(Nat, k, t, m)), B.Trie.amount(B.Trie.get(Nat, k, t))) == Nat.add(B.Trie.sum(t), B.Trie.amount(m)) : Nat}:315  match k t:316    case Nil{} B.Tip{}:317      +am = B.Trie.amount(m)318      %Nat.add_zero(Nat.add(am, 0n)) : {_ == am : Nat}319      %Nat.add_zero(am) : {_ == am : Nat}320      {==}321    case Nil{} B.Bin{v, lo, hi}:322      Nat.swap13(B.Trie.amount(m), Nat.add(B.Trie.sum(lo), B.Trie.sum(hi)), B.Trie.amount(v))323    case False{} <> ks B.Tip{}:324      +s1 = B.Trie.sum(B.Trie.set(Nat, ks, B.Tip{}, m))325      %Nat.add_zero(s1) : {Nat.add(_, B.Trie.amount(B.Trie.get(Nat, ks, B.Tip{}))) == B.Trie.amount(m) : Nat}326      Trie.sum_set(ks, B.Tip{}, m)327    case False{} <> ks B.Bin{v, lo, hi}:328      +av = B.Trie.amount(v)329      +s1 = B.Trie.sum(B.Trie.set(Nat, ks, lo, m))330      +g = B.Trie.amount(B.Trie.get(Nat, ks, lo))331      +h = B.Trie.sum(hi)332      +l = B.Trie.sum(lo)333      +am = B.Trie.amount(m)334      %Nat.mid(av, s1, h, g) : {_ == Nat.add(Nat.add(av, Nat.add(l, h)), am) : Nat}335      %Nat.mid(av, l, h, am) : {Nat.add(av, Nat.add(h, Nat.add(s1, g))) == _ : Nat}336      %Trie.sum_set(ks, lo, m) : {Nat.add(av, Nat.add(h, Nat.add(s1, g))) == Nat.add(av, Nat.add(h, _)) : Nat}337      {==}338    case True{} <> ks B.Tip{}:339      Trie.sum_set(ks, B.Tip{}, m)340    case True{} <> ks B.Bin{v, lo, hi}:341      +av = B.Trie.amount(v)342      +s1 = B.Trie.sum(B.Trie.set(Nat, ks, hi, m))343      +g = B.Trie.amount(B.Trie.get(Nat, ks, hi))344      +h = B.Trie.sum(hi)345      +l = B.Trie.sum(lo)346      +am = B.Trie.amount(m)347      %Nat.mid2(av, l, s1, g) : {_ == Nat.add(Nat.add(av, Nat.add(l, h)), am) : Nat}348      %Nat.mid2(av, l, h, am) : {Nat.add(av, Nat.add(l, Nat.add(s1, g))) == _ : Nat}349      %Trie.sum_set(ks, hi, m) : {Nat.add(av, Nat.add(l, Nat.add(s1, g))) == Nat.add(av, Nat.add(l, _)) : Nat}350      {==}351352# setting k to m swaps k's old account's worth for m's in the sum353def Acc.sum_set(+k: B.Key(), +t: B.Trie<B.Acc>, +m: Maybe<&2, B.Acc>)354  -> {Nat.add(B.Acc.sum(B.Trie.set(B.Acc, k, t, m)), B.Acc.worth_of(B.Trie.get(B.Acc, k, t))) == Nat.add(B.Acc.sum(t), B.Acc.worth_of(m)) : Nat}:355  match k t:356    case Nil{} B.Tip{}:357      +am = B.Acc.worth_of(m)358      %Nat.add_zero(Nat.add(am, 0n)) : {_ == am : Nat}359      %Nat.add_zero(am) : {_ == am : Nat}360      {==}361    case Nil{} B.Bin{v, lo, hi}:362      Nat.swap13(B.Acc.worth_of(m), Nat.add(B.Acc.sum(lo), B.Acc.sum(hi)), B.Acc.worth_of(v))363    case False{} <> ks B.Tip{}:364      +s1 = B.Acc.sum(B.Trie.set(B.Acc, ks, B.Tip{}, m))365      %Nat.add_zero(s1) : {Nat.add(_, B.Acc.worth_of(B.Trie.get(B.Acc, ks, B.Tip{}))) == B.Acc.worth_of(m) : Nat}366      Acc.sum_set(ks, B.Tip{}, m)367    case False{} <> ks B.Bin{v, lo, hi}:368      +av = B.Acc.worth_of(v)369      +s1 = B.Acc.sum(B.Trie.set(B.Acc, ks, lo, m))370      +g = B.Acc.worth_of(B.Trie.get(B.Acc, ks, lo))371      +h = B.Acc.sum(hi)372      +l = B.Acc.sum(lo)373      +am = B.Acc.worth_of(m)374      %Nat.mid(av, s1, h, g) : {_ == Nat.add(Nat.add(av, Nat.add(l, h)), am) : Nat}375      %Nat.mid(av, l, h, am) : {Nat.add(av, Nat.add(h, Nat.add(s1, g))) == _ : Nat}376      %Acc.sum_set(ks, lo, m) : {Nat.add(av, Nat.add(h, Nat.add(s1, g))) == Nat.add(av, Nat.add(h, _)) : Nat}377      {==}378    case True{} <> ks B.Tip{}:379      Acc.sum_set(ks, B.Tip{}, m)380    case True{} <> ks B.Bin{v, lo, hi}:381      +av = B.Acc.worth_of(v)382      +s1 = B.Acc.sum(B.Trie.set(B.Acc, ks, hi, m))383      +g = B.Acc.worth_of(B.Trie.get(B.Acc, ks, hi))384      +h = B.Acc.sum(hi)385      +l = B.Acc.sum(lo)386      +am = B.Acc.worth_of(m)387      %Nat.mid2(av, l, s1, g) : {_ == Nat.add(Nat.add(av, Nat.add(l, h)), am) : Nat}388      %Nat.mid2(av, l, h, am) : {Nat.add(av, Nat.add(l, Nat.add(s1, g))) == _ : Nat}389      %Acc.sum_set(ks, hi, m) : {Nat.add(av, Nat.add(l, Nat.add(s1, g))) == Nat.add(av, Nat.add(l, _)) : Nat}390      {==}391392# an amount that is absent when zero is still that amount393def Trie.amount_some(n: Nat) -> {B.Trie.amount(B.Trie.some(n)) == n : Nat}:394  match n:395    case 0n:396      {==}397    case 1n+p:398      {==}399400# putting n at k swaps k's old amount for n in the sum401def Trie.sum_put(+k: B.Key(), +t: B.Trie<Nat>, +n: Nat)402  -> {Nat.add(B.Trie.sum(B.Trie.put(k, t, n)), B.Trie.num(k, t)) == Nat.add(B.Trie.sum(t), n) : Nat}:403  %Trie.amount_some(n) : {Nat.add(B.Trie.sum(B.Trie.put(k, t, n)), B.Trie.num(k, t)) == Nat.add(B.Trie.sum(t), _) : Nat}404  Trie.sum_set(k, t, B.Trie.some(n))405406# putting at k leaves the amounts at other keys407def Trie.num_put_other(+q: B.Key(), +k: B.Key(), +t: B.Trie<Nat>, +n: Nat, e: {B.Key.eq(q, k) == False{} : Bool})408  -> {B.Trie.num(q, B.Trie.put(k, t, n)) == B.Trie.num(q, t) : Nat}:409  %Trie.get_other(Nat, q, k, t, B.Trie.some(n), e) : {B.Trie.amount(_) == B.Trie.num(q, t) : Nat}410  {==}411412# the amount just put at k is there413def Trie.num_put_same(+k: B.Key(), +t: B.Trie<Nat>, +n: Nat) -> {n == B.Trie.num(k, B.Trie.put(k, t, n)) : Nat}:414  %Trie.get_same(Nat, k, t, B.Trie.some(n)) : {n == B.Trie.amount(_) : Nat}415  Equal.sym(Nat, B.Trie.amount(B.Trie.some(n)), n, Trie.amount_some(n))416417# Gift418# ----419420# the cash a gift pays to the account at k, and all the gifts pay it421def Gift.pay(g: B.Gift, +k: B.Key()) -> Nat:422  match g:423    case B.Pay{d, x}:424      Bool.pick(Nat, B.Key.eq(d, k), x, 0n)425    case B.Owe{d, x}:426      0n427    case B.Rel{d}:428      0n429430def Gift.paid(gs: List<&2, B.Gift>, +k: B.Key()) -> Nat:431  match gs:432    case Nil{}:433      0n434    case g <> rest:435      Nat.add(Gift.pay(g, k), Gift.paid(rest, k))436437# Bank438# ----439440# P holds of the bank of a result that does not fail441def Bank.If(r: Result<&2, &2, String, B.Bank>, P: B.Bank -> Type) -> Type:442  match r:443    case Fail{e}:444      Unit445    case Done{b}:446      P(b)447448# an account that a key opens is the account there449def Bank.open_some(+x: B.Acc, ok: Bool, -a: B.Acc, e: {B.Bank.open(x, ok) == Some{a} : Maybe<&2, B.Acc>})450  -> {Some{a} == Some{x} : Maybe<&2, B.Acc>}:451  match ok:452    case True{}:453      Equal.sym(Maybe<&2, B.Acc>, Some{x}, Some{a}, e)454    case False{}:455      Maybe.none_some(B.Acc, a, {Some{a} == Some{x} : Maybe<&2, B.Acc>}, e)456457# an account that a key opens is the account at that key458def Bank.check_some(m: Maybe<&2, B.Acc>, +pass: String, -a: B.Acc, e: {B.Bank.check(m, pass) == Some{a} : Maybe<&2, B.Acc>})459  -> {Some{a} == m : Maybe<&2, B.Acc>}:460  match m:461    case None{}:462      Maybe.none_some(B.Acc, a, {Some{a} == None{} : Maybe<&2, B.Acc>}, e)463    case Some{+x}:464      Bank.open_some(x, String.eq(B.Acc.pass(x), pass), a, e)465466# the bank v, t with a new account at k, with key pass, funded by 1,100467# from the vault468def Bank.opening(v: Nat, t: B.Trie<B.Acc>, k: B.Key(), pass: String) -> B.Bank:469  B.Bank{Nat.sub(v, 1100n), B.Trie.set(B.Acc, k, t, Some{B.Acc.new(pass)})}470471# a funded bank is the bank, when the vault has 1,100472def Bank.fund_by(ok: Bool, -v: Nat, -b: B.Bank, -P: B.Bank -> Type, o: {Nat.is_le(1100n, v) == ok : Bool},473  h: Laws.LE(1100n, v) -> P(b)) -> Bank.If(B.Bank.fund(ok, b), P):474  match ok:475    case True{}:476      h(o)477    case False{}:478      Unit{}479480# a join at a free key opens an account; at a taken one it fails481def Bank.join_at_by(m: Maybe<&2, B.Acc>, +v: Nat, +t: B.Trie<B.Acc>, +k: B.Key(), +pass: String, -P: B.Bank -> Type,482  em: {B.Trie.get(B.Acc, k, t) == m : Maybe<&2, B.Acc>},483  h: {B.Trie.get(B.Acc, k, t) == None{} : Maybe<&2, B.Acc>} -> Laws.LE(1100n, v) -> P(Bank.opening(v, t, k, pass)))484  -> Bank.If(B.Bank.join.at(m, B.Bank{v, t}, k, pass), P):485  match m:486    case Some{a}:487      Unit{}488    case None{}:489      Bank.fund_by(Nat.is_le(1100n, v), v, Bank.opening(v, t, k, pass), P, {==}, h(em))490491# P holds of the bank after a join at the key m, when it holds of every492# bank that opens an account at a key that had none493def Bank.join_by(m: Maybe<&2, B.Key()>, +v: Nat, +t: B.Trie<B.Acc>, +pass: String, -P: B.Bank -> Type,494  h: @k: B.Key() -> {B.Trie.get(B.Acc, k, t) == None{} : Maybe<&2, B.Acc>} -> Laws.LE(1100n, v) -> P(Bank.opening(v, t, k, pass)))495  -> Bank.If(B.Bank.join.key(m, B.Bank{v, t}, pass), P):496  match m:497    case None{}:498      Unit{}499    case Some{+k}:500      Bank.join_at_by(B.Trie.get(B.Acc, k, t), v, t, k, pass, P, {==}, h(k))501502# a command of the account m at uk: what the plan of its command makes503def Bank.exec_acct_by(m: Maybe<&2, B.Acc>, +v: Nat, +t: B.Trie<B.Acc>, +uk: B.Key(), +pass: String, +now: Nat, +cmd: B.Cmd,504  -P: Maybe<&2, B.Key()> -> B.Bank -> Type, -R: Maybe<&2, B.Key()> -> Type,505  em: {B.Bank.check(B.Trie.get(B.Acc, uk, t), pass) == m : Maybe<&2, B.Acc>}, hr: R(Laws.opened(uk, m)),506  h: @a: B.Acc -> {Some{a} == B.Trie.get(B.Acc, uk, t) : Maybe<&2, B.Acc>} -> R(Some{uk})507    -> Bank.If(B.Bank.plan(B.Bank{v, t}, uk, B.Cmd.plan(cmd, a, now)), P(Some{uk})))508  -> Bank.If(B.Bank.exec.acct(B.Bank{v, t}, uk, m, now, cmd), P(Laws.opened(uk, m))):509  match m:510    case None{}:511      Unit{}512    case Some{+a}:513      h(a, Bank.check_some(B.Trie.get(B.Acc, uk, t), pass, a, em), hr)514515# P(u) holds of the bank after a command of the key m, where u is its516# sender, when, for every account a at uk that the key opens, R(uk) gives517# P(uk) of the bank that the plan of a makes518def Bank.exec_by(m: Maybe<&2, B.Key()>, +v: Nat, +t: B.Trie<B.Acc>, +pass: String, +now: Nat, +cmd: B.Cmd,519  -P: Maybe<&2, B.Key()> -> B.Bank -> Type, -R: Maybe<&2, B.Key()> -> Type, hr: R(Laws.Bank.sender.at(t, m, pass)),520  h: @uk: B.Key() -> @a: B.Acc -> {Some{a} == B.Trie.get(B.Acc, uk, t) : Maybe<&2, B.Acc>} -> R(Some{uk})521    -> Bank.If(B.Bank.plan(B.Bank{v, t}, uk, B.Cmd.plan(cmd, a, now)), P(Some{uk})))522  -> Bank.If(B.Bank.exec.key(m, B.Bank{v, t}, pass, now, cmd), P(Laws.Bank.sender.at(t, m, pass))):523  match m:524    case None{}:525      Unit{}526    case Some{+uk}:527      Bank.exec_acct_by(B.Bank.check(B.Trie.get(B.Acc, uk, t), pass), v, t, uk, pass, now, cmd, P, R, {==}, hr, h(uk))528529# Web530# ---531532# a cookie or a failure, answered: a reply with no change533def Web.login_pick(ok: Bool, -see: String, -e: String, -s: B.Bank, -user: String, -pass: String, -time: Nat)534  -> {W.Reply{None{}, Laws.text(W.Web.done(Bool.pick(Result<&2, &2, String, W.Reply>, ok, Done{W.Reply{None{}, see}}, Fail{e}), s, user, pass, time))}535      == W.Web.done(Bool.pick(Result<&2, &2, String, W.Reply>, ok, Done{W.Reply{None{}, see}}, Fail{e}), s, user, pass, time) : W.Reply}:536  match ok:537    case True{}:538      {==}539    case False{}:540      {==}541542# a login, answered: a reply with no change543def Web.login_none(+name: String, +key: String, -s: B.Bank, -user: String, -pass: String, -time: Nat)544  -> {W.Reply{None{}, Laws.text(W.Web.done(W.Web.login(name, key), s, user, pass, time))} == W.Web.done(W.Web.login(name, key), s, user, pass, time) : W.Reply}:545  +ok = Bool.and(Bool.not(String.is_empty(name)), Bool.and(W.Text.safe(name, 64n), W.Text.safe(key, 64n)))546  Web.login_pick(ok, W.Http.see(name ++ "-" ++ key), "a name and a key are letters and digits", s, user, pass, time)547548# the bank after a change: the change, or s549def Web.done_by(r: Result<&2, &2, String, B.Bank>, -see: String, -s: B.Bank, -user: String, -pass: String, -time: Nat,550  -P: B.Bank -> Type, h0: P(s), h: Bank.If(r, P))551  -> P(Laws.after(s, W.Web.done(W.Web.change(r, see), s, user, pass, time))):552  match r:553    case Fail{e}:554      h0555    case Done{b}:556      h557558# P holds of the bank after an answer, when it holds of s and of every559# bank that a join or a command of (user, pass) makes560def Web.answer_by(call: W.Call, +s: B.Bank, +time: Nat, +rand: String, +user: String, +pass: String, -P: B.Bank -> Type, h0: P(s),561  hj: @name: String -> Bank.If(B.Bank.join(s, name, rand), P),562  hx: @cmd: B.Cmd -> Bank.If(B.Bank.exec(s, user, pass, time, cmd), P))563  -> P(Laws.after(s, W.Web.answer(call, s, time, rand, user, pass))):564  match call:565    case W.Home{}:566      h0567    case W.Join{+name}:568      Web.done_by(B.Bank.join(s, name, rand), W.Http.see(name ++ "-" ++ rand), s, user, pass, time, P, h0, hj(name))569    case W.Auth{+name, +key}:570      %Web.login_none(name, key, s, user, pass, time) : P(Laws.after(s, _))571      h0572    case W.Quit{}:573      h0574    case W.Exec{+cmd}:575      Web.done_by(B.Bank.exec(s, user, pass, time, cmd), W.Http.home(), s, user, pass, time, P, h0, hx(cmd))576    case W.Miss{}:577      h0578579# P holds of the bank after a reply, when it holds of s and of every bank580# that a join or a command of the request's sender makes581def Web.reply_by(+s: B.Bank, req: W.Req, -P: B.Bank -> Type, h0: P(s),582  hj: @name: String -> Bank.If(B.Bank.join(s, name, Laws.Req.rand(req)), P),583  hx: @cmd: B.Cmd -> Bank.If(B.Bank.exec(s, Laws.Req.user(req), Laws.Req.pass(req), Laws.Req.time(req), cmd), P))584  -> P(Laws.after(s, W.Web.reply(s, req))):585  match req:586    case W.Req{+time, +rand, verb, path, +user, +pass, form}:587      +call = W.Web.call(W.Web.find(W.Web.paths(), verb ++ " " ++ path, 0n), form)588      Web.answer_by(call, s, time, rand, user, pass, P, h0, hj, hx)