1# Bend Bank: the proof of LAW privacy2# ===================================3#4# What the holder of (o, pass) sees is the view of the account at o: its5# account, if pass opens it, and Acc.locks(accts, o), the money o locked6# in each account. A request sets accounts one at a time: the sender's,7# then each gift's. Setting the account at k changes o's lock view only8# at k, by what o locked in the new account, and that agrees in both9# banks: the sender's new account is the same in both, and a gift10# changes what o locked in it as a function of what o locked before.1112import Base13import ../bank.bend as B14import ../web.bend as W15import ../LAWS.bend as Laws16import ./base.bend as L1718# Locks19# -----2021# o's lock view after a set changes only at the key set22def Acc.locks_set(k: B.Key(), +t: B.Trie<B.Acc>, +x: Maybe<&2, B.Acc>, +o: B.Key())23 -> {B.Trie.set(Nat, k, B.Acc.locks(t, o), B.Acc.locked(x, o)) == B.Acc.locks(B.Trie.set(B.Acc, k, t, x), o) : B.Trie<Nat>}:24 match k t:25 case Nil{} B.Tip{}:26 {==}27 case Nil{} B.Bin{v, lo, hi}:28 {==}29 case False{} <> ks B.Tip{}:30 +y = B.Acc.locked(x, o)31 %Acc.locks_set(ks, B.Tip{}, x, o) : {B.Bin{None{}, B.Trie.set(Nat, ks, B.Tip{}, y), B.Tip{}} == B.Bin{None{}, _, B.Tip{}} : B.Trie<Nat>}32 {==}33 case False{} <> ks B.Bin{+v, lo, +hi}:34 +y = B.Acc.locked(x, o)35 +w = B.Acc.locked(v, o)36 +h = B.Acc.locks(hi, o)37 %Acc.locks_set(ks, lo, x, o) : {B.Bin{w, B.Trie.set(Nat, ks, B.Acc.locks(lo, o), y), h} == B.Bin{w, _, h} : B.Trie<Nat>}38 {==}39 case True{} <> ks B.Tip{}:40 +y = B.Acc.locked(x, o)41 %Acc.locks_set(ks, B.Tip{}, x, o) : {B.Bin{None{}, B.Tip{}, B.Trie.set(Nat, ks, B.Tip{}, y)} == B.Bin{None{}, B.Tip{}, _} : B.Trie<Nat>}42 {==}43 case True{} <> ks B.Bin{+v, +lo, hi}:44 +y = B.Acc.locked(x, o)45 +w = B.Acc.locked(v, o)46 +l = B.Acc.locks(lo, o)47 %Acc.locks_set(ks, hi, x, o) : {B.Bin{w, l, B.Trie.set(Nat, ks, B.Acc.locks(hi, o), y)} == B.Bin{w, l, _} : B.Trie<Nat>}48 {==}4950# o's lock view at k is what o locked in the account at k51def Acc.locks_get(k: B.Key(), +t: B.Trie<B.Acc>, +o: B.Key())52 -> {B.Trie.get(Nat, k, B.Acc.locks(t, o)) == B.Acc.locked(B.Trie.get(B.Acc, k, t), o) : Maybe<&2, Nat>}:53 match k t:54 case Nil{} B.Tip{}:55 {==}56 case Nil{} B.Bin{v, lo, hi}:57 {==}58 case False{} <> ks B.Tip{}:59 Acc.locks_get(ks, B.Tip{}, o)60 case False{} <> ks B.Bin{v, lo, hi}:61 Acc.locks_get(ks, lo, o)62 case True{} <> ks B.Tip{}:63 Acc.locks_get(ks, B.Tip{}, o)64 case True{} <> ks B.Bin{v, lo, hi}:65 Acc.locks_get(ks, hi, o)6667# what o locked in an account after a gift from u, from what o locked68# before; c says whether o is u69def Gift.lock(g: B.Gift, c: Bool, +m: Maybe<&2, Nat>) -> Maybe<&2, Nat>:70 match g:71 case B.Pay{d, x}:72 m73 case B.Owe{d, x}:74 Bool.pick(Maybe<&2, Nat>, c, B.Trie.some(Nat.add(B.Trie.amount(m), x)), m)75 case B.Rel{d}:76 Bool.pick(Maybe<&2, Nat>, c, None{}, m)7778# an owe from u adds to what o locked, where o is u79def Gift.owe_pick(c: Bool, +o: B.Key(), +u: B.Key(), +held: B.Trie<Nat>, +x: Nat, e: {B.Key.eq(o, u) == c : Bool})80 -> {Bool.pick(Maybe<&2, Nat>, c, B.Trie.some(Nat.add(B.Trie.num(o, held), x)), B.Trie.get(Nat, o, held))81 == Bool.pick(Maybe<&2, Nat>, c, B.Trie.some(Nat.add(B.Trie.num(u, held), x)), B.Trie.get(Nat, o, held)) : Maybe<&2, Nat>}:82 match c:83 case True{}:84 %L.Key.eq_true(o, u, e) : {B.Trie.some(Nat.add(B.Trie.num(o, held), x)) == B.Trie.some(Nat.add(B.Trie.num(_, held), x)) : Maybe<&2, Nat>}85 {==}86 case False{}:87 {==}8889# what o locked in an account after a gift is Gift.lock of what o locked before90def Gift.locked(g: B.Gift, +u: B.Key(), a: B.Acc, +o: B.Key())91 -> {Gift.lock(g, B.Key.eq(o, u), B.Acc.locked(Some{a}, o)) == B.Acc.locked(Some{B.Gift.give(g, u, a)}, o) : Maybe<&2, Nat>}:92 match g a:93 case B.Pay{d, x} B.Acc{pass, cash, note, line, loan, held}:94 {==}95 case B.Owe{d, +x} B.Acc{pass, cash, note, line, loan, +held}:96 +n = B.Trie.some(Nat.add(B.Trie.num(u, held), x))97 %L.Trie.pick_set(Nat, o, u, held, n) : {Gift.lock(B.Owe{d, x}, B.Key.eq(o, u), B.Trie.get(Nat, o, held)) == _ : Maybe<&2, Nat>}98 Gift.owe_pick(B.Key.eq(o, u), o, u, held, x, {==})99 case B.Rel{d} B.Acc{pass, cash, note, line, loan, +held}:100 %L.Trie.pick_set(Nat, o, u, held, None{}) : {Gift.lock(B.Rel{d}, B.Key.eq(o, u), B.Trie.get(Nat, o, held)) == _ : Maybe<&2, Nat>}101 {==}102103# what o locked in the account at d after a gift, from o's lock view104def Gift.lock_at(+o: B.Key(), +d: B.Key(), +t: B.Trie<B.Acc>, +u: B.Key(), +g: B.Gift, +a: B.Acc,105 em: {B.Trie.get(B.Acc, d, t) == Some{a} : Maybe<&2, B.Acc>})106 -> {Gift.lock(g, B.Key.eq(o, u), B.Trie.get(Nat, d, B.Acc.locks(t, o))) == B.Acc.locked(Some{B.Gift.give(g, u, a)}, o) : Maybe<&2, Nat>}:107 +f = {Gift.lock(g, B.Key.eq(o, u), B.Trie.get(Nat, d, B.Acc.locks(t, o))) : Maybe<&2, Nat>}108 %Gift.locked(g, u, a, o) : {f == _ : Maybe<&2, Nat>}109 %em : {f == Gift.lock(g, B.Key.eq(o, u), B.Acc.locked(_, o)) : Maybe<&2, Nat>}110 %Acc.locks_get(d, t, o) : {f == Gift.lock(g, B.Key.eq(o, u), _) : Maybe<&2, Nat>}111 {==}112113# a gift changes what o locked in the account at d alike in two tries114# where o's lock views agree115def Gift.lock_same(+o: B.Key(), +d: B.Key(), +t1: B.Trie<B.Acc>, +t2: B.Trie<B.Acc>, +u: B.Key(), +g: B.Gift, +a1: B.Acc, +a2: B.Acc,116 em1: {B.Trie.get(B.Acc, d, t1) == Some{a1} : Maybe<&2, B.Acc>}, em2: {B.Trie.get(B.Acc, d, t2) == Some{a2} : Maybe<&2, B.Acc>},117 el: {B.Acc.locks(t1, o) == B.Acc.locks(t2, o) : B.Trie<Nat>})118 -> {B.Acc.locked(Some{B.Gift.give(g, u, a1)}, o) == B.Acc.locked(Some{B.Gift.give(g, u, a2)}, o) : Maybe<&2, Nat>}:119 +c = B.Key.eq(o, u)120 +f = {Gift.lock(g, c, B.Trie.get(Nat, d, B.Acc.locks(t1, o))) : Maybe<&2, Nat>}121 %Gift.lock_at(o, d, t1, u, g, a1, em1) : {_ == B.Acc.locked(Some{B.Gift.give(g, u, a2)}, o) : Maybe<&2, Nat>}122 %Gift.lock_at(o, d, t2, u, g, a2, em2) : {f == _ : Maybe<&2, Nat>}123 %el : {f == Gift.lock(g, c, B.Trie.get(Nat, d, _)) : Maybe<&2, Nat>}124 {==}125126# no account locked anything under j: o's lock view is blank127def Priv.blank(t: B.Trie<Unit>) -> B.Trie<Nat>:128 match t:129 case B.Tip{}:130 B.Tip{}131 case B.Bin{v, lo, hi}:132 B.Bin{None{}, Priv.blank(lo), Priv.blank(hi)}133134# o's lock view at j is blank, or some account locked money under j135def Priv.Scan(t: B.Trie<B.Acc>, j: B.Key()) -> Type:136 {B.Acc.locks(t, j) == Priv.blank(Laws.names(t)) : B.Trie<Nat>} |137 (&k: B.Key() -> ({B.Acc.locked(B.Trie.get(B.Acc, k, t), j) == None{} : Maybe<&2, Nat>} -> Empty))138139# a node whose value and children are blank is blank140def Priv.blank_bin(-v: Maybe<&2, B.Acc>, +lo: B.Trie<B.Acc>, +hi: B.Trie<B.Acc>, +j: B.Key(), e: {B.Acc.locked(v, j) == None{} : Maybe<&2, Nat>},141 el: {B.Acc.locks(lo, j) == Priv.blank(Laws.names(lo)) : B.Trie<Nat>}, eh: {B.Acc.locks(hi, j) == Priv.blank(Laws.names(hi)) : B.Trie<Nat>})142 -> {B.Acc.locks(B.Bin{v, lo, hi}, j) == Priv.blank(Laws.names(B.Bin{v, lo, hi})) : B.Trie<Nat>}:143 -w = B.Acc.locked(v, j)144 -l = B.Acc.locks(lo, j)145 -r = B.Acc.locks(hi, j)146 %e : {B.Bin{w, l, r} == B.Bin{_, Priv.blank(Laws.names(lo)), Priv.blank(Laws.names(hi))} : B.Trie<Nat>}147 %el : {B.Bin{w, l, r} == B.Bin{w, _, Priv.blank(Laws.names(hi))} : B.Trie<Nat>}148 %eh : {B.Bin{w, l, r} == B.Bin{w, l, _} : B.Trie<Nat>}149 {==}150151# a scan of a node, from the scans of its children152def Priv.scan_bin(-v: Maybe<&2, B.Acc>, +lo: B.Trie<B.Acc>, +hi: B.Trie<B.Acc>, +j: B.Key(), m: Maybe<&2, Nat>, sl: Priv.Scan(lo, j), sh: Priv.Scan(hi, j),153 e: {B.Acc.locked(v, j) == m : Maybe<&2, Nat>}) -> Priv.Scan(B.Bin{v, lo, hi}, j):154 match m sl sh:155 case Some{x} _ _:156 Inr{(Nil{}, e0 => L.Maybe.some_none(Nat, x, Empty, Equal.trans(Maybe<&2, Nat>, Some{x}, B.Acc.locked(v, j), None{}, Equal.sym(Maybe<&2, Nat>, B.Acc.locked(v, j), Some{x}, e), e0)))}157 case None{} Inr{(k, f)} _:158 Inr{(False{} <> k, f)}159 case None{} Inl{el} Inr{(k, f)}:160 Inr{(True{} <> k, f)}161 case None{} Inl{el} Inl{eh}:162 Inl{Priv.blank_bin(v, lo, hi, j, e, el, eh)}163164# every lock view at j is blank or names an account that locked under j165def Priv.scan(t: B.Trie<B.Acc>, +j: B.Key()) -> Priv.Scan(t, j):166 match t:167 case B.Tip{}:168 Inl{{==}}169 case B.Bin{+v, +lo, +hi}:170 Priv.scan_bin(v, lo, hi, j, B.Acc.locked(v, j), Priv.scan(lo, j), Priv.scan(hi, j), {==})171172# in a sound bank with no account at j, no account locked money under j:173# soundness is a function, used once, at the key a scan finds174def Priv.fresh_at(-v: Nat, -t: B.Trie<B.Acc>, +j: B.Key(), sc: Priv.Scan(t, j), ok: Laws.Sound(B.Bank{v, t}),175 em: {B.Trie.get(B.Acc, j, t) == None{} : Maybe<&2, B.Acc>}) -> {B.Acc.locks(t, j) == Priv.blank(Laws.names(t)) : B.Trie<Nat>}:176 match sc:177 case Inl{e}:178 e179 case Inr{(k, f)}:180 Empty.absurd({B.Acc.locks(t, j) == Priv.blank(Laws.names(t)) : B.Trie<Nat>}, f(ok(k, j, em)))181182# in a sound bank, the lock view of a name with no account is blank183def Priv.fresh(+v: Nat, +t: B.Trie<B.Acc>, +j: B.Key(), ok: Laws.Sound(B.Bank{v, t}), em: {B.Trie.get(B.Acc, j, t) == None{} : Maybe<&2, B.Acc>})184 -> {B.Acc.locks(t, j) == Priv.blank(Laws.names(t)) : B.Trie<Nat>}:185 Priv.fresh_at(v, t, j, Priv.scan(t, j), ok, em)186187# Views188# -----189190# the view of the account c, with lock view l191def Priv.view(l: B.Trie<Nat>, c: Maybe<&2, B.Acc>) -> Maybe<&2, B.View>:192 match c:193 case None{}:194 None{}195 case Some{a}:196 Some{B.View{a, l}}197198# Bank.view is Priv.view of the lock view199def Priv.view_eq(+t: B.Trie<B.Acc>, +o: B.Key(), c: Maybe<&2, B.Acc>) -> {Priv.view(B.Acc.locks(t, o), c) == B.Bank.view(t, o, c) : Maybe<&2, B.View>}:200 match c:201 case None{}:202 {==}203 case Some{a}:204 {==}205206# the parts of a view207def Priv.lock(m: Maybe<&2, B.View>) -> B.Trie<Nat>:208 match m:209 case None{}:210 B.Tip{}211 case Some{B.View{a, l}}:212 l213214# the account of a view215def Priv.opened(m: Maybe<&2, B.View>) -> Maybe<&2, B.Acc>:216 match m:217 case None{}:218 None{}219 case Some{B.View{a, l}}:220 Some{a}221222# a view with its lock view replaced by l223def Priv.relock(m: Maybe<&2, B.View>, l: B.Trie<Nat>) -> Maybe<&2, B.View>:224 match m:225 case None{}:226 None{}227 case Some{B.View{a, x}}:228 Some{B.View{a, l}}229230# two equal views stay equal when each lock view is set at k, to values231# that agree when the lock views do232def Priv.view_set(c1: Maybe<&2, B.Acc>, c2: Maybe<&2, B.Acc>, +l1: B.Trie<Nat>, +l2: B.Trie<Nat>, +k: B.Key(), -y1: Maybe<&2, Nat>, -y2: Maybe<&2, Nat>,233 +h: {Priv.view(l1, c1) == Priv.view(l2, c2) : Maybe<&2, B.View>}, hy: {l1 == l2 : B.Trie<Nat>} -> {y1 == y2 : Maybe<&2, Nat>})234 -> {Priv.view(B.Trie.set(Nat, k, l1, y1), c1) == Priv.view(B.Trie.set(Nat, k, l2, y2), c2) : Maybe<&2, B.View>}:235 match c1 c2:236 case None{} None{}:237 {==}238 case None{} Some{a2}:239 L.Maybe.none_some(B.View, B.View{a2, l2}, {None{} == Some{B.View{a2, B.Trie.set(Nat, k, l2, y2)}} : Maybe<&2, B.View>}, h)240 case Some{a1} None{}:241 L.Maybe.some_none(B.View, B.View{a1, l1}, {Some{B.View{a1, B.Trie.set(Nat, k, l1, y1)}} == None{} : Maybe<&2, B.View>}, h)242 case Some{+a1} Some{+a2}:243 -V = Maybe<&2, B.View>244 +x1 = {Some{B.View{a1, l1}} : Maybe<&2, B.View>}245 +x2 = {Some{B.View{a2, l2}} : Maybe<&2, B.View>}246 +el = Equal.cong(V, B.Trie<Nat>, Priv.lock, x1, x2, h)247 -s1 = B.Trie.set(Nat, k, l1, y1)248 %hy(el) : {Some{B.View{a1, s1}} == Some{B.View{a2, B.Trie.set(Nat, k, l2, _)}} : Maybe<&2, B.View>}249 %el : {Some{B.View{a1, s1}} == Some{B.View{a2, B.Trie.set(Nat, k, _, y1)}} : Maybe<&2, B.View>}250 Equal.cong(V, V, m => Priv.relock(m, s1), x1, x2, h)251252# a gift to the account a view shows, if any253def Priv.give(g: B.Gift, u: B.Key(), m: Maybe<&2, B.Acc>) -> Maybe<&2, B.Acc>:254 match m:255 case None{}:256 None{}257 case Some{a}:258 Some{B.Gift.give(g, u, a)}259260# a view with a gift to its account261def Priv.regive(g: B.Gift, u: B.Key(), m: Maybe<&2, B.View>) -> Maybe<&2, B.View>:262 match m:263 case None{}:264 None{}265 case Some{B.View{a, l}}:266 Some{B.View{B.Gift.give(g, u, a), l}}267268# two equal views stay equal after the same gift to their accounts269def Priv.view_give(+g: B.Gift, +u: B.Key(), c1: Maybe<&2, B.Acc>, c2: Maybe<&2, B.Acc>, +l1: B.Trie<Nat>, +l2: B.Trie<Nat>,270 h: {Priv.view(l1, c1) == Priv.view(l2, c2) : Maybe<&2, B.View>})271 -> {Priv.view(l1, Priv.give(g, u, c1)) == Priv.view(l2, Priv.give(g, u, c2)) : Maybe<&2, B.View>}:272 match c1 c2:273 case None{} None{}:274 {==}275 case None{} Some{a2}:276 L.Maybe.none_some(B.View, B.View{a2, l2}, {None{} == Some{B.View{B.Gift.give(g, u, a2), l2}} : Maybe<&2, B.View>}, h)277 case Some{a1} None{}:278 L.Maybe.some_none(B.View, B.View{a1, l1}, {Some{B.View{B.Gift.give(g, u, a1), l1}} == None{} : Maybe<&2, B.View>}, h)279 case Some{+a1} Some{+a2}:280 -V = Maybe<&2, B.View>281 Equal.cong(V, V, m => Priv.regive(g, u, m), Some{B.View{a1, l1}}, Some{B.View{a2, l2}}, h)282283# a gift keeps the account's key284def Priv.pass_give(g: B.Gift, +u: B.Key(), a: B.Acc) -> {B.Acc.pass(B.Gift.give(g, u, a)) == B.Acc.pass(a) : String}:285 match g a:286 case B.Pay{d, x} B.Acc{pass, cash, note, line, loan, held}:287 {==}288 case B.Owe{d, x} B.Acc{pass, cash, note, line, loan, held}:289 {==}290 case B.Rel{d} B.Acc{pass, cash, note, line, loan, held}:291 {==}292293# opening commutes with a gift294def Priv.open_give(c: Bool, +g: B.Gift, +u: B.Key(), +a: B.Acc) -> {Priv.give(g, u, B.Bank.open(a, c)) == B.Bank.open(B.Gift.give(g, u, a), c) : Maybe<&2, B.Acc>}:295 match c:296 case True{}:297 {==}298 case False{}:299 {==}300301# a key opens a gifted account as it opened the account302def Priv.check_give(+g: B.Gift, +u: B.Key(), +a: B.Acc, +pass: String)303 -> {Priv.give(g, u, B.Bank.check(Some{a}, pass)) == B.Bank.check(Some{B.Gift.give(g, u, a)}, pass) : Maybe<&2, B.Acc>}:304 +b = B.Gift.give(g, u, a)305 %Equal.sym(String, B.Acc.pass(b), B.Acc.pass(a), Priv.pass_give(g, u, a)) : {Priv.give(g, u, B.Bank.check(Some{a}, pass)) == B.Bank.open(b, String.eq(_, pass)) : Maybe<&2, B.Acc>}306 Priv.open_give(String.eq(B.Acc.pass(a), pass), g, u, a)307308# Steps309# -----310311# what the holder of (m, pass) sees in two account tries is the same312def Priv.Seen(t1: B.Trie<B.Acc>, t2: B.Trie<B.Acc>, m: Maybe<&2, B.Key()>, pass: String) -> Data:313 {B.Bank.seen.at(t1, m, pass) == B.Bank.seen.at(t2, m, pass) : Maybe<&2, B.View>}314315# what o sees, as a Priv.view316def Priv.seen_from(+t1: B.Trie<B.Acc>, +t2: B.Trie<B.Acc>, +o: B.Key(), +pass: String, h: Priv.Seen(t1, t2, Some{o}, pass))317 -> {Priv.view(B.Acc.locks(t1, o), B.Bank.check(B.Trie.get(B.Acc, o, t1), pass)) == Priv.view(B.Acc.locks(t2, o), B.Bank.check(B.Trie.get(B.Acc, o, t2), pass)) : Maybe<&2, B.View>}:318 -V = Maybe<&2, B.View>319 +c1 = B.Bank.check(B.Trie.get(B.Acc, o, t1), pass)320 +c2 = B.Bank.check(B.Trie.get(B.Acc, o, t2), pass)321 +w1 = Priv.view(B.Acc.locks(t1, o), c1)322 +w2 = Priv.view(B.Acc.locks(t2, o), c2)323 +v1 = B.Bank.view(t1, o, c1)324 +v2 = B.Bank.view(t2, o, c2)325 Equal.trans(V, w1, v1, w2, Priv.view_eq(t1, o, c1), Equal.trans(V, v1, v2, w2, h, Equal.sym(V, w2, v2, Priv.view_eq(t2, o, c2))))326327# what o sees after a set at k, from o's lock view and account before328def Priv.at_set(+o: B.Key(), +pass: String, +k: B.Key(), +t: B.Trie<B.Acc>, +x: Maybe<&2, B.Acc>)329 -> {Priv.view(B.Trie.set(Nat, k, B.Acc.locks(t, o), B.Acc.locked(x, o)), B.Bank.check(Bool.pick(Maybe<&2, B.Acc>, B.Key.eq(o, k), x, B.Trie.get(B.Acc, o, t)), pass))330 == B.Bank.seen.at(B.Trie.set(B.Acc, k, t, x), Some{o}, pass) : Maybe<&2, B.View>}:331 +t2 = B.Trie.set(B.Acc, k, t, x)332 -l = B.Trie.set(Nat, k, B.Acc.locks(t, o), B.Acc.locked(x, o))333 -w = Priv.view(l, B.Bank.check(Bool.pick(Maybe<&2, B.Acc>, B.Key.eq(o, k), x, B.Trie.get(B.Acc, o, t)), pass))334 %Priv.view_eq(t2, o, B.Bank.check(B.Trie.get(B.Acc, o, t2), pass)) : {w == _ : Maybe<&2, B.View>}335 %Acc.locks_set(k, t, x, o) : {w == Priv.view(_, B.Bank.check(B.Trie.get(B.Acc, o, t2), pass)) : Maybe<&2, B.View>}336 %L.Trie.pick_set(B.Acc, o, k, t, x) : {w == Priv.view(l, B.Bank.check(_, pass)) : Maybe<&2, B.View>}337 {==}338339# what o sees after a set at k is the same, when it was before340def Priv.lift(+o: B.Key(), +pass: String, +k: B.Key(), +t1: B.Trie<B.Acc>, +t2: B.Trie<B.Acc>, +x1: Maybe<&2, B.Acc>, +x2: Maybe<&2, B.Acc>,341 h: {Priv.view(B.Trie.set(Nat, k, B.Acc.locks(t1, o), B.Acc.locked(x1, o)), B.Bank.check(Bool.pick(Maybe<&2, B.Acc>, B.Key.eq(o, k), x1, B.Trie.get(B.Acc, o, t1)), pass))342 == Priv.view(B.Trie.set(Nat, k, B.Acc.locks(t2, o), B.Acc.locked(x2, o)), B.Bank.check(Bool.pick(Maybe<&2, B.Acc>, B.Key.eq(o, k), x2, B.Trie.get(B.Acc, o, t2)), pass)) : Maybe<&2, B.View>})343 -> Priv.Seen(B.Trie.set(B.Acc, k, t1, x1), B.Trie.set(B.Acc, k, t2, x2), Some{o}, pass):344 -w = Priv.view(B.Trie.set(Nat, k, B.Acc.locks(t1, o), B.Acc.locked(x1, o)), B.Bank.check(Bool.pick(Maybe<&2, B.Acc>, B.Key.eq(o, k), x1, B.Trie.get(B.Acc, o, t1)), pass))345 %Priv.at_set(o, pass, k, t1, x1) : {_ == B.Bank.seen.at(B.Trie.set(B.Acc, k, t2, x2), Some{o}, pass) : Maybe<&2, B.View>}346 %Priv.at_set(o, pass, k, t2, x2) : {w == _ : Maybe<&2, B.View>}347 h348349# o's lock views agree, when o is k350def Priv.LockAt(m: Maybe<&2, B.Key()>, k: B.Key(), t1: B.Trie<B.Acc>, t2: B.Trie<B.Acc>) -> Type:351 match m:352 case None{}:353 Unit354 case Some{o}:355 {B.Key.eq(o, k) == True{} : Bool} -> {B.Acc.locks(t1, o) == B.Acc.locks(t2, o) : B.Trie<Nat>}356357# o's lock views agree when o is k, as k's do358def Priv.lock_at(m: Maybe<&2, B.Key()>, +k: B.Key(), +t1: B.Trie<B.Acc>, +t2: B.Trie<B.Acc>, +el: {B.Acc.locks(t1, k) == B.Acc.locks(t2, k) : B.Trie<Nat>})359 -> Priv.LockAt(m, k, t1, t2):360 match m:361 case None{}:362 Unit{}363 case Some{+o}:364 e =>365 +ek = Equal.sym(B.Key(), o, k, L.Key.eq_true(o, k, e))366 %ek : {B.Acc.locks(t1, _) == B.Acc.locks(t2, o) : B.Trie<Nat>}367 %ek : {B.Acc.locks(t1, k) == B.Acc.locks(t2, _) : B.Trie<Nat>}368 el369370# setting k to the same account in both tries: o's lock views must agree371# when o is k372def Priv.same_at(c: Bool, +o: B.Key(), +pass: String, +k: B.Key(), +t1: B.Trie<B.Acc>, +t2: B.Trie<B.Acc>, +x: Maybe<&2, B.Acc>,373 h: {Priv.view(B.Acc.locks(t1, o), B.Bank.check(B.Trie.get(B.Acc, o, t1), pass)) == Priv.view(B.Acc.locks(t2, o), B.Bank.check(B.Trie.get(B.Acc, o, t2), pass)) : Maybe<&2, B.View>},374 hl: {c == True{} : Bool} -> {B.Acc.locks(t1, o) == B.Acc.locks(t2, o) : B.Trie<Nat>})375 -> {Priv.view(B.Trie.set(Nat, k, B.Acc.locks(t1, o), B.Acc.locked(x, o)), B.Bank.check(Bool.pick(Maybe<&2, B.Acc>, c, x, B.Trie.get(B.Acc, o, t1)), pass))376 == Priv.view(B.Trie.set(Nat, k, B.Acc.locks(t2, o), B.Acc.locked(x, o)), B.Bank.check(Bool.pick(Maybe<&2, B.Acc>, c, x, B.Trie.get(B.Acc, o, t2)), pass)) : Maybe<&2, B.View>}:377 match c:378 case True{}:379 -y = B.Acc.locked(x, o)380 -w = Priv.view(B.Trie.set(Nat, k, B.Acc.locks(t1, o), y), B.Bank.check(x, pass))381 %hl({==}) : {w == Priv.view(B.Trie.set(Nat, k, _, y), B.Bank.check(x, pass)) : Maybe<&2, B.View>}382 {==}383 case False{}:384 +c1 = B.Bank.check(B.Trie.get(B.Acc, o, t1), pass)385 +c2 = B.Bank.check(B.Trie.get(B.Acc, o, t2), pass)386 Priv.view_set(c1, c2, B.Acc.locks(t1, o), B.Acc.locks(t2, o), k, B.Acc.locked(x, o), B.Acc.locked(x, o), h, e => {==})387388# setting k to the same account keeps what (m, pass) sees the same389def Priv.seen_same(m: Maybe<&2, B.Key()>, +pass: String, +k: B.Key(), +t1: B.Trie<B.Acc>, +t2: B.Trie<B.Acc>, +x: Maybe<&2, B.Acc>,390 h: Priv.Seen(t1, t2, m, pass), hl: Priv.LockAt(m, k, t1, t2))391 -> Priv.Seen(B.Trie.set(B.Acc, k, t1, x), B.Trie.set(B.Acc, k, t2, x), m, pass):392 match m:393 case None{}:394 {==}395 case Some{+o}:396 Priv.lift(o, pass, k, t1, t2, x, x, Priv.same_at(B.Key.eq(o, k), o, pass, k, t1, t2, x, Priv.seen_from(t1, t2, o, pass, h), hl))397398# what holder o sees at d, where a is399def Priv.at_d(+o: B.Key(), +d: B.Key(), +t: B.Trie<B.Acc>, -a: B.Acc, +pass: String, eo: {o == d : B.Key()},400 em: {B.Trie.get(B.Acc, d, t) == Some{a} : Maybe<&2, B.Acc>})401 -> {B.Bank.check(B.Trie.get(B.Acc, o, t), pass) == B.Bank.check(Some{a}, pass) : Maybe<&2, B.Acc>}:402 %Equal.sym(B.Key(), o, d, eo) : {B.Bank.check(B.Trie.get(B.Acc, _, t), pass) == B.Bank.check(Some{a}, pass) : Maybe<&2, B.Acc>}403 %em : {B.Bank.check(B.Trie.get(B.Acc, d, t), pass) == B.Bank.check(_, pass) : Maybe<&2, B.Acc>}404 {==}405406# a gift to the accounts a1, a2 at d: what o sees changes alike407def Priv.gift_at(c: Bool, +o: B.Key(), +pass: String, +d: B.Key(), +t1: B.Trie<B.Acc>, +t2: B.Trie<B.Acc>, +u: B.Key(), +g: B.Gift, +a1: B.Acc, +a2: B.Acc,408 e: {B.Key.eq(o, d) == c : Bool}, +em1: {B.Trie.get(B.Acc, d, t1) == Some{a1} : Maybe<&2, B.Acc>}, +em2: {B.Trie.get(B.Acc, d, t2) == Some{a2} : Maybe<&2, B.Acc>},409 h: {Priv.view(B.Acc.locks(t1, o), B.Bank.check(B.Trie.get(B.Acc, o, t1), pass)) == Priv.view(B.Acc.locks(t2, o), B.Bank.check(B.Trie.get(B.Acc, o, t2), pass)) : Maybe<&2, B.View>})410 -> {Priv.view(B.Trie.set(Nat, d, B.Acc.locks(t1, o), B.Acc.locked(Some{B.Gift.give(g, u, a1)}, o)), B.Bank.check(Bool.pick(Maybe<&2, B.Acc>, c, Some{B.Gift.give(g, u, a1)}, B.Trie.get(B.Acc, o, t1)), pass))411 == Priv.view(B.Trie.set(Nat, d, B.Acc.locks(t2, o), B.Acc.locked(Some{B.Gift.give(g, u, a2)}, o)), B.Bank.check(Bool.pick(Maybe<&2, B.Acc>, c, Some{B.Gift.give(g, u, a2)}, B.Trie.get(B.Acc, o, t2)), pass)) : Maybe<&2, B.View>}:412 match c:413 case False{}:414 +c1 = B.Bank.check(B.Trie.get(B.Acc, o, t1), pass)415 +c2 = B.Bank.check(B.Trie.get(B.Acc, o, t2), pass)416 +y1 = B.Acc.locked(Some{B.Gift.give(g, u, a1)}, o)417 +y2 = B.Acc.locked(Some{B.Gift.give(g, u, a2)}, o)418 Priv.view_set(c1, c2, B.Acc.locks(t1, o), B.Acc.locks(t2, o), d, y1, y2, h, el => Gift.lock_same(o, d, t1, t2, u, g, a1, a2, em1, em2, el))419 case True{}:420 +eo = L.Key.eq_true(o, d, e)421 +c1 = B.Bank.check(B.Trie.get(B.Acc, o, t1), pass)422 +c2 = B.Bank.check(B.Trie.get(B.Acc, o, t2), pass)423 +y1 = B.Acc.locked(Some{B.Gift.give(g, u, a1)}, o)424 +y2 = B.Acc.locked(Some{B.Gift.give(g, u, a2)}, o)425 +l1 = B.Trie.set(Nat, d, B.Acc.locks(t1, o), y1)426 +l2 = B.Trie.set(Nat, d, B.Acc.locks(t2, o), y2)427 %Priv.check_give(g, u, a1, pass) : {Priv.view(l1, _) == Priv.view(l2, B.Bank.check(Some{B.Gift.give(g, u, a2)}, pass)) : Maybe<&2, B.View>}428 %Priv.check_give(g, u, a2, pass) : {Priv.view(l1, Priv.give(g, u, B.Bank.check(Some{a1}, pass))) == Priv.view(l2, _) : Maybe<&2, B.View>}429 %Priv.at_d(o, d, t1, a1, pass, eo, em1) : {Priv.view(l1, Priv.give(g, u, _)) == Priv.view(l2, Priv.give(g, u, B.Bank.check(Some{a2}, pass))) : Maybe<&2, B.View>}430 %Priv.at_d(o, d, t2, a2, pass, eo, em2) : {Priv.view(l1, Priv.give(g, u, c1)) == Priv.view(l2, Priv.give(g, u, _)) : Maybe<&2, B.View>}431 +hs = Priv.view_set(c1, c2, B.Acc.locks(t1, o), B.Acc.locks(t2, o), d, y1, y2, h, el => Gift.lock_same(o, d, t1, t2, u, g, a1, a2, em1, em2, el))432 Priv.view_give(g, u, c1, c2, l1, l2, hs)433434# a gift to the account at d keeps what (m, pass) sees the same435def Priv.seen_gift(m: Maybe<&2, B.Key()>, +pass: String, +d: B.Key(), +t1: B.Trie<B.Acc>, +t2: B.Trie<B.Acc>, +u: B.Key(), +g: B.Gift, +a1: B.Acc, +a2: B.Acc,436 +em1: {B.Trie.get(B.Acc, d, t1) == Some{a1} : Maybe<&2, B.Acc>}, +em2: {B.Trie.get(B.Acc, d, t2) == Some{a2} : Maybe<&2, B.Acc>}, h: Priv.Seen(t1, t2, m, pass))437 -> Priv.Seen(B.Trie.set(B.Acc, d, t1, Some{B.Gift.give(g, u, a1)}), B.Trie.set(B.Acc, d, t2, Some{B.Gift.give(g, u, a2)}), m, pass):438 match m:439 case None{}:440 {==}441 case Some{+o}:442 +x1 = {Some{B.Gift.give(g, u, a1)} : Maybe<&2, B.Acc>}443 +x2 = {Some{B.Gift.give(g, u, a2)} : Maybe<&2, B.Acc>}444 Priv.lift(o, pass, d, t1, t2, x1, x2, Priv.gift_at(B.Key.eq(o, d), o, pass, d, t1, t2, u, g, a1, a2, {==}, em1, em2, Priv.seen_from(t1, t2, o, pass, h)))445446# Names447# -----448449# the names of a tree after a set450def Priv.names_get(k: B.Key(), +t: B.Trie<B.Acc>)451 -> {B.Trie.get(Unit, k, Laws.names(t)) == Maybe.map(&2, B.Acc, Unit, a => Unit{}, B.Trie.get(B.Acc, k, t)) : Maybe<&2, Unit>}:452 match k t:453 case Nil{} B.Tip{}:454 {==}455 case Nil{} B.Bin{v, lo, hi}:456 {==}457 case False{} <> ks B.Tip{}:458 Priv.names_get(ks, B.Tip{})459 case False{} <> ks B.Bin{v, lo, hi}:460 Priv.names_get(ks, lo)461 case True{} <> ks B.Tip{}:462 Priv.names_get(ks, B.Tip{})463 case True{} <> ks B.Bin{v, lo, hi}:464 Priv.names_get(ks, hi)465466# the names of a tree after a set467def Priv.names_set(k: B.Key(), +t: B.Trie<B.Acc>, +m: Maybe<&2, B.Acc>)468 -> {B.Trie.set(Unit, k, Laws.names(t), Maybe.map(&2, B.Acc, Unit, a => Unit{}, m)) == Laws.names(B.Trie.set(B.Acc, k, t, m)) : B.Trie<Unit>}:469 match k t:470 case Nil{} B.Tip{}:471 {==}472 case Nil{} B.Bin{v, lo, hi}:473 {==}474 case False{} <> ks B.Tip{}:475 %Priv.names_set(ks, B.Tip{}, m) : {B.Bin{None{}, B.Trie.set(Unit, ks, B.Tip{}, Maybe.map(&2, B.Acc, Unit, a => Unit{}, m)), B.Tip{}} == B.Bin{None{}, _, B.Tip{}} : B.Trie<Unit>}476 {==}477 case False{} <> ks B.Bin{+v, lo, hi}:478 +u = Maybe.map(&2, B.Acc, Unit, a => Unit{}, v)479 %Priv.names_set(ks, lo, m) : {B.Bin{u, B.Trie.set(Unit, ks, Laws.names(lo), Maybe.map(&2, B.Acc, Unit, a => Unit{}, m)), Laws.names(hi)} == B.Bin{u, _, Laws.names(hi)} : B.Trie<Unit>}480 {==}481 case True{} <> ks B.Tip{}:482 %Priv.names_set(ks, B.Tip{}, m) : {B.Bin{None{}, B.Tip{}, B.Trie.set(Unit, ks, B.Tip{}, Maybe.map(&2, B.Acc, Unit, a => Unit{}, m))} == B.Bin{None{}, B.Tip{}, _} : B.Trie<Unit>}483 {==}484 case True{} <> ks B.Bin{+v, lo, hi}:485 +u = Maybe.map(&2, B.Acc, Unit, a => Unit{}, v)486 %Priv.names_set(ks, hi, m) : {B.Bin{u, Laws.names(lo), B.Trie.set(Unit, ks, Laws.names(hi), Maybe.map(&2, B.Acc, Unit, a => Unit{}, m))} == B.Bin{u, Laws.names(lo), _} : B.Trie<Unit>}487 {==}488489# setting k in two trees with the same names, to accounts or both to none,490# keeps their names the same491def Priv.set_names(+k: B.Key(), +t1: B.Trie<B.Acc>, +t2: B.Trie<B.Acc>, +m1: Maybe<&2, B.Acc>, +m2: Maybe<&2, B.Acc>,492 en: {Laws.names(t1) == Laws.names(t2) : B.Trie<Unit>}, hm: {Maybe.map(&2, B.Acc, Unit, a => Unit{}, m1) == Maybe.map(&2, B.Acc, Unit, a => Unit{}, m2) : Maybe<&2, Unit>})493 -> {Laws.names(B.Trie.set(B.Acc, k, t1, m1)) == Laws.names(B.Trie.set(B.Acc, k, t2, m2)) : B.Trie<Unit>}:494 +u1 = Maybe.map(&2, B.Acc, Unit, a => Unit{}, m1)495 %Priv.names_set(k, t1, m1) : {_ == Laws.names(B.Trie.set(B.Acc, k, t2, m2)) : B.Trie<Unit>}496 %Priv.names_set(k, t2, m2) : {B.Trie.set(Unit, k, Laws.names(t1), u1) == _ : B.Trie<Unit>}497 %en : {B.Trie.set(Unit, k, Laws.names(t1), u1) == B.Trie.set(Unit, k, _, Maybe.map(&2, B.Acc, Unit, a => Unit{}, m2)) : B.Trie<Unit>}498 %hm : {B.Trie.set(Unit, k, Laws.names(t1), u1) == B.Trie.set(Unit, k, Laws.names(t1), _) : B.Trie<Unit>}499 {==}500501# two trees with the same names have an account at d in both or in neither502def Priv.clash(+d: B.Key(), +t1: B.Trie<B.Acc>, +t2: B.Trie<B.Acc>, -m1: Maybe<&2, B.Acc>, -m2: Maybe<&2, B.Acc>,503 em1: {B.Trie.get(B.Acc, d, t1) == m1 : Maybe<&2, B.Acc>}, em2: {B.Trie.get(B.Acc, d, t2) == m2 : Maybe<&2, B.Acc>},504 en: {Laws.names(t1) == Laws.names(t2) : B.Trie<Unit>})505 -> {Maybe.map(&2, B.Acc, Unit, a => Unit{}, m1) == Maybe.map(&2, B.Acc, Unit, a => Unit{}, m2) : Maybe<&2, Unit>}:506 %em1 : {Maybe.map(&2, B.Acc, Unit, a => Unit{}, _) == Maybe.map(&2, B.Acc, Unit, a => Unit{}, m2) : Maybe<&2, Unit>}507 %em2 : {Maybe.map(&2, B.Acc, Unit, a => Unit{}, B.Trie.get(B.Acc, d, t1)) == Maybe.map(&2, B.Acc, Unit, a => Unit{}, _) : Maybe<&2, Unit>}508 %Priv.names_get(d, t1) : {_ == Maybe.map(&2, B.Acc, Unit, a => Unit{}, B.Trie.get(B.Acc, d, t2)) : Maybe<&2, Unit>}509 %Priv.names_get(d, t2) : {B.Trie.get(Unit, d, Laws.names(t1)) == _ : Maybe<&2, Unit>}510 Equal.cong(B.Trie<Unit>, Maybe<&2, Unit>, x => B.Trie.get(Unit, d, x), Laws.names(t1), Laws.names(t2), en)511512# Banks513# -----514515# two bank results agree for the holder of (name, pass): the same failure,516# or banks that agree on public data and on what the holder sees517def Priv.R(r1: Result<&2, &2, String, B.Bank>, r2: Result<&2, &2, String, B.Bank>, name: String, pass: String) -> Type:518 match r1 r2:519 case Fail{e1} Fail{e2}:520 {e1 == e2 : String}521 case Fail{e1} Done{b2}:522 Empty523 case Done{b1} Fail{e2}:524 Empty525 case Done{b1} Done{b2}:526 Laws.Public(b1, b2) & Laws.Same(b1, b2, name, pass)527528# a gift fails alike in both banks, or reaches an account in both529def Priv.gift_to(self: Bool, m1: Maybe<&2, B.Acc>, m2: Maybe<&2, B.Acc>, +v1: Nat, +t1: B.Trie<B.Acc>, +v2: Nat, +t2: B.Trie<B.Acc>, +u: B.Key(), +d: B.Key(), +g: B.Gift,530 +name: String, +pass: String, +em1: {B.Trie.get(B.Acc, d, t1) == m1 : Maybe<&2, B.Acc>}, +em2: {B.Trie.get(B.Acc, d, t2) == m2 : Maybe<&2, B.Acc>},531 ev: {v1 == v2 : Nat}, +en: {Laws.names(t1) == Laws.names(t2) : B.Trie<Unit>}, same: Laws.Same(B.Bank{v1, t1}, B.Bank{v2, t2}, name, pass))532 -> Priv.R(B.Plan.gift.to(self, m1, v1, t1, u, d, g), B.Plan.gift.to(self, m2, v2, t2, u, d, g), name, pass):533 match self m1 m2:534 case True{} _ _:535 {==}536 case False{} None{} None{}:537 {==}538 case False{} None{} Some{a2}:539 L.Maybe.none_some(Unit, Unit{}, Empty, Priv.clash(d, t1, t2, None{}, Some{a2}, em1, em2, en))540 case False{} Some{a1} None{}:541 L.Maybe.some_none(Unit, Unit{}, Empty, Priv.clash(d, t1, t2, Some{a1}, None{}, em1, em2, en))542 case False{} Some{+a1} Some{+a2}:543 +b1 = {Some{B.Gift.give(g, u, a1)} : Maybe<&2, B.Acc>}544 +b2 = {Some{B.Gift.give(g, u, a2)} : Maybe<&2, B.Acc>}545 +seen = Priv.seen_gift(B.Key.of(name), pass, d, t1, t2, u, g, a1, a2, em1, em2, same)546 ((ev, Priv.set_names(d, t1, t2, b1, b2, en, {==})), seen)547548# one more gift keeps two bank results in agreement549def Priv.gift(r1: Result<&2, &2, String, B.Bank>, r2: Result<&2, &2, String, B.Bank>, +u: B.Key(), +g: B.Gift, +name: String, +pass: String, h: Priv.R(r1, r2, name, pass))550 -> Priv.R(B.Plan.gift(r1, u, g), B.Plan.gift(r2, u, g), name, pass):551 match r1 r2:552 case Fail{e1} Fail{e2}:553 h554 case Fail{e1} Done{b2}:555 match h:556 case Done{b1} Fail{e2}:557 match h:558 case Done{B.Bank{v1, +t1}} Done{B.Bank{v2, +t2}}:559 ((ev, en), same) = h560 +d = B.Gift.dest(g)561 Priv.gift_to(B.Key.eq(d, u), B.Trie.get(B.Acc, d, t1), B.Trie.get(B.Acc, d, t2), v1, t1, v2, t2, u, d, g, name, pass, {==}, {==}, ev, en, same)562563# every gift of a plan keeps two bank results in agreement564def Priv.gifts(gs: List<&2, B.Gift>, +u: B.Key(), +r1: Result<&2, &2, String, B.Bank>, +r2: Result<&2, &2, String, B.Bank>, +name: String, +pass: String, h: Priv.R(r1, r2, name, pass))565 -> Priv.R(B.Plan.gifts(gs, u, r1), B.Plan.gifts(gs, u, r2), name, pass):566 match gs:567 case Nil{}:568 h569 case +g <> rest:570 Priv.gifts(rest, u, B.Plan.gift(r1, u, g), B.Plan.gift(r2, u, g), name, pass, Priv.gift(r1, r2, u, g, name, pass, h))571572# the same plan agrees in two banks that agree, when the sender's lock573# views agree574def Priv.apply(+v1: Nat, +t1: B.Trie<B.Acc>, +v2: Nat, +t2: B.Trie<B.Acc>, +u: B.Key(), p: B.Plan, +name: String, +pass: String,575 pub: Laws.Public(B.Bank{v1, t1}, B.Bank{v2, t2}), same: Laws.Same(B.Bank{v1, t1}, B.Bank{v2, t2}, name, pass), hl: Priv.LockAt(B.Key.of(name), u, t1, t2))576 -> Priv.R(B.Plan.apply(B.Bank{v1, t1}, u, p), B.Plan.apply(B.Bank{v2, t2}, u, p), name, pass):577 match p:578 case B.Plan{+acct, +gifts}:579 (ev, en) = pub580 +m = {Some{acct} : Maybe<&2, B.Acc>}581 +r1 = {Done{B.Bank{v1, B.Trie.set(B.Acc, u, t1, m)}} : Result<&2, &2, String, B.Bank>}582 +r2 = {Done{B.Bank{v2, B.Trie.set(B.Acc, u, t2, m)}} : Result<&2, &2, String, B.Bank>}583 +seen = Priv.seen_same(B.Key.of(name), pass, u, t1, t2, m, same, hl)584 Priv.gifts(gifts, u, r1, r2, name, pass, ((ev, Priv.set_names(u, t1, t2, m, m, en, {==})), seen))585586# a planned request agrees in two banks that agree587def Priv.plan(+v1: Nat, +t1: B.Trie<B.Acc>, +v2: Nat, +t2: B.Trie<B.Acc>, +u: B.Key(), r: Result<&2, &2, String, B.Plan>, +name: String, +pass: String,588 pub: Laws.Public(B.Bank{v1, t1}, B.Bank{v2, t2}), same: Laws.Same(B.Bank{v1, t1}, B.Bank{v2, t2}, name, pass), hl: Priv.LockAt(B.Key.of(name), u, t1, t2))589 -> Priv.R(B.Bank.plan(B.Bank{v1, t1}, u, r), B.Bank.plan(B.Bank{v2, t2}, u, r), name, pass):590 match r:591 case Fail{e}:592 {==}593 case Done{p}:594 Priv.apply(v1, t1, v2, t2, u, p, name, pass, pub, same, hl)595596# the sender sees the same view in both banks: the same account, so the597# same plan, and the same lock view598def Priv.acct(+v1: Nat, +t1: B.Trie<B.Acc>, +v2: Nat, +t2: B.Trie<B.Acc>, +u: B.Key(), m1: Maybe<&2, B.Acc>, m2: Maybe<&2, B.Acc>, +now: Nat, +cmd: B.Cmd,599 +name: String, +pass: String, +you: {Priv.view(B.Acc.locks(t1, u), m1) == Priv.view(B.Acc.locks(t2, u), m2) : Maybe<&2, B.View>},600 pub: Laws.Public(B.Bank{v1, t1}, B.Bank{v2, t2}), same: Laws.Same(B.Bank{v1, t1}, B.Bank{v2, t2}, name, pass))601 -> Priv.R(B.Bank.exec.acct(B.Bank{v1, t1}, u, m1, now, cmd), B.Bank.exec.acct(B.Bank{v2, t2}, u, m2, now, cmd), name, pass):602 match m1 m2:603 case None{} None{}:604 {==}605 case None{} Some{a2}:606 L.Maybe.none_some(B.View, B.View{a2, B.Acc.locks(t2, u)}, Priv.R(Fail{"log in first"}, B.Bank.exec.acct(B.Bank{v2, t2}, u, Some{a2}, now, cmd), name, pass), you)607 case Some{a1} None{}:608 L.Maybe.some_none(B.View, B.View{a1, B.Acc.locks(t1, u)}, Priv.R(B.Bank.exec.acct(B.Bank{v1, t1}, u, Some{a1}, now, cmd), Fail{"log in first"}, name, pass), you)609 case Some{+a1} Some{+a2}:610 -V = Maybe<&2, B.View>611 +x1 = {Some{B.View{a1, B.Acc.locks(t1, u)}} : Maybe<&2, B.View>}612 +x2 = {Some{B.View{a2, B.Acc.locks(t2, u)}} : Maybe<&2, B.View>}613 +ea = Equal.cong(V, Maybe<&2, B.Acc>, Priv.opened, x1, x2, you)614 +el = Equal.cong(V, B.Trie<Nat>, Priv.lock, x1, x2, you)615 %ea : Priv.R(B.Bank.exec.acct(B.Bank{v1, t1}, u, Some{a1}, now, cmd), B.Bank.exec.acct(B.Bank{v2, t2}, u, _, now, cmd), name, pass)616 Priv.plan(v1, t1, v2, t2, u, B.Cmd.plan(cmd, a1, now), name, pass, pub, same, Priv.lock_at(B.Key.of(name), u, t1, t2, el))617618# a request by the holder of (u, key) agrees in two banks that agree619def Priv.key(m: Maybe<&2, B.Key()>, +v1: Nat, +t1: B.Trie<B.Acc>, +v2: Nat, +t2: B.Trie<B.Acc>, +key: String, +now: Nat, +cmd: B.Cmd, +name: String, +pass: String,620 pub: Laws.Public(B.Bank{v1, t1}, B.Bank{v2, t2}), you: Priv.Seen(t1, t2, m, key), same: Laws.Same(B.Bank{v1, t1}, B.Bank{v2, t2}, name, pass))621 -> Priv.R(B.Bank.exec.key(m, B.Bank{v1, t1}, key, now, cmd), B.Bank.exec.key(m, B.Bank{v2, t2}, key, now, cmd), name, pass):622 match m:623 case None{}:624 {==}625 case Some{+u}:626 +m1 = B.Bank.check(B.Trie.get(B.Acc, u, t1), key)627 +m2 = B.Bank.check(B.Trie.get(B.Acc, u, t2), key)628 Priv.acct(v1, t1, v2, t2, u, m1, m2, now, cmd, name, pass, Priv.seen_from(t1, t2, u, key, you), pub, same)629630# a command agrees in two banks that agree on public data and on the sender631def Priv.exec(s1: B.Bank, s2: B.Bank, +user: String, +key: String, +now: Nat, +cmd: B.Cmd, +name: String, +pass: String,632 pub: Laws.Public(s1, s2), you: Laws.Same(s1, s2, user, key), same: Laws.Same(s1, s2, name, pass))633 -> Priv.R(B.Bank.exec(s1, user, key, now, cmd), B.Bank.exec(s2, user, key, now, cmd), name, pass):634 match s1 s2:635 case B.Bank{+v1, +t1} B.Bank{+v2, +t2}:636 Priv.key(B.Key.of(user), v1, t1, v2, t2, key, now, cmd, name, pass, pub, you, same)637638# Join639# ----640641# a funded join agrees, when the new banks agree642def Priv.fund(ok: Bool, -b1: B.Bank, -b2: B.Bank, -name: String, -pass: String, h: Laws.Public(b1, b2) & Laws.Same(b1, b2, name, pass))643 -> Priv.R(B.Bank.fund(ok, b1), B.Bank.fund(ok, b2), name, pass):644 match ok:645 case True{}:646 h647 case False{}:648 {==}649650# a new account at j, where neither bank has one: its holder sees no651# lock in either, as both banks are sound652def Priv.join_at(m1: Maybe<&2, B.Acc>, m2: Maybe<&2, B.Acc>, +v1: Nat, +t1: B.Trie<B.Acc>, +v2: Nat, +t2: B.Trie<B.Acc>, +j: B.Key(), +rand: String,653 +name: String, +pass: String, +em1: {B.Trie.get(B.Acc, j, t1) == m1 : Maybe<&2, B.Acc>}, +em2: {B.Trie.get(B.Acc, j, t2) == m2 : Maybe<&2, B.Acc>},654 ok1: Laws.Sound(B.Bank{v1, t1}), ok2: Laws.Sound(B.Bank{v2, t2}), +ev: {v1 == v2 : Nat}, +en: {Laws.names(t1) == Laws.names(t2) : B.Trie<Unit>},655 same: Laws.Same(B.Bank{v1, t1}, B.Bank{v2, t2}, name, pass))656 -> Priv.R(B.Bank.join.at(m1, B.Bank{v1, t1}, j, rand), B.Bank.join.at(m2, B.Bank{v2, t2}, j, rand), name, pass):657 match m1 m2:658 case Some{a1} Some{a2}:659 {==}660 case None{} Some{+a2}:661 L.Maybe.none_some(Unit, Unit{}, Priv.R(B.Bank.join.at(None{}, B.Bank{v1, t1}, j, rand), B.Bank.join.at(Some{a2}, B.Bank{v2, t2}, j, rand), name, pass),662 Priv.clash(j, t1, t2, None{}, Some{a2}, em1, em2, en))663 case Some{+a1} None{}:664 L.Maybe.some_none(Unit, Unit{}, Priv.R(B.Bank.join.at(Some{a1}, B.Bank{v1, t1}, j, rand), B.Bank.join.at(None{}, B.Bank{v2, t2}, j, rand), name, pass),665 Priv.clash(j, t1, t2, Some{a1}, None{}, em1, em2, en))666 case None{} None{}:667 +x = Nat.add(B.Acc.grant(), B.Loan.limit())668 +m = {Some{B.Acc.new(rand)} : Maybe<&2, B.Acc>}669 +b1 = {B.Bank{Nat.sub(v1, x), B.Trie.set(B.Acc, j, t1, m)} : B.Bank}670 +b2 = {B.Bank{Nat.sub(v2, x), B.Trie.set(B.Acc, j, t2, m)} : B.Bank}671 +f1 = Priv.fresh(v1, t1, j, ok1, em1)672 +f2 = Priv.fresh(v2, t2, j, ok2, em2)673 -T = B.Trie<Nat>674 +bl1 = Priv.blank(Laws.names(t1))675 +bl2 = Priv.blank(Laws.names(t2))676 +el = Equal.trans(T, B.Acc.locks(t1, j), bl1, B.Acc.locks(t2, j), f1,677 Equal.trans(T, bl1, bl2, B.Acc.locks(t2, j), Equal.cong(B.Trie<Unit>, T, Priv.blank, Laws.names(t1), Laws.names(t2), en), Equal.sym(T, B.Acc.locks(t2, j), bl2, f2)))678 +seen = Priv.seen_same(B.Key.of(name), pass, j, t1, t2, m, same, Priv.lock_at(B.Key.of(name), j, t1, t2, el))679 +pub = {(Equal.cong(Nat, Nat, n => Nat.sub(n, x), v1, v2, ev), Priv.set_names(j, t1, t2, m, m, en, {==})) : Laws.Public(b1, b2)}680 %ev : Priv.R(B.Bank.fund(Nat.is_le(x, v1), b1), B.Bank.fund(Nat.is_le(x, _), b2), name, pass)681 Priv.fund(Nat.is_le(x, v1), b1, b2, name, pass, (pub, seen))682683# a join at a valid name agrees in two banks that agree684def Priv.join_key(m: Maybe<&2, B.Key()>, +v1: Nat, +t1: B.Trie<B.Acc>, +v2: Nat, +t2: B.Trie<B.Acc>, +rand: String, +name: String, +pass: String,685 ok1: Laws.Sound(B.Bank{v1, t1}), ok2: Laws.Sound(B.Bank{v2, t2}), +ev: {v1 == v2 : Nat}, +en: {Laws.names(t1) == Laws.names(t2) : B.Trie<Unit>},686 same: Laws.Same(B.Bank{v1, t1}, B.Bank{v2, t2}, name, pass))687 -> Priv.R(B.Bank.join.key(m, B.Bank{v1, t1}, rand), B.Bank.join.key(m, B.Bank{v2, t2}, rand), name, pass):688 match m:689 case None{}:690 {==}691 case Some{+j}:692 +m1 = B.Trie.get(B.Acc, j, t1)693 +m2 = B.Trie.get(B.Acc, j, t2)694 Priv.join_at(m1, m2, v1, t1, v2, t2, j, rand, name, pass, {==}, {==}, ok1, ok2, ev, en, same)695696# a join agrees in two sound banks that agree on public data697def Priv.join(s1: B.Bank, s2: B.Bank, +who: String, +rand: String, +name: String, +pass: String, ok1: Laws.Sound(s1), ok2: Laws.Sound(s2),698 pub: Laws.Public(s1, s2), same: Laws.Same(s1, s2, name, pass))699 -> Priv.R(B.Bank.join(s1, who, rand), B.Bank.join(s2, who, rand), name, pass):700 match s1 s2:701 case B.Bank{+v1, +t1} B.Bank{+v2, +t2}:702 (ev, en) = pub703 Priv.join_key(B.Key.of(who), v1, t1, v2, t2, rand, name, pass, ok1, ok2, ev, en, same)704705# Web706# ---707708# the privacy law's conclusion, for two replies709def Priv.Out(s1: B.Bank, s2: B.Bank, r1: W.Reply, r2: W.Reply, name: String, pass: String) -> Type:710 {Laws.text(r1) == Laws.text(r2) : String} &711 Laws.Public(Laws.after(s1, r1), Laws.after(s2, r2)) &712 Laws.Same(Laws.after(s1, r1), Laws.after(s2, r2), name, pass)713714# the home page, with the same view and message715def Priv.page(+status: String, +s1: B.Bank, +s2: B.Bank, +user: String, +key: String, +time: Nat, +e1: String, -e2: String,716 you: Laws.Same(s1, s2, user, key), ee: {e1 == e2 : String})717 -> {W.Http.answer(status, "", W.Web.page(s1, user, key, time, e1)) == W.Http.answer(status, "", W.Web.page(s2, user, key, time, e2)) : String}:718 -x = W.Http.answer(status, "", W.Web.page(s1, user, key, time, e1))719 %you : {x == W.Http.answer(status, "", W.Page.home(_, user, time, e2)) : String}720 %ee : {x == W.Http.answer(status, "", W.Page.home(B.Bank.seen(s1, user, key), user, time, _)) : String}721 {==}722723# a change, or its failure page, agrees in both banks724def Priv.done(r1: Result<&2, &2, String, B.Bank>, r2: Result<&2, &2, String, B.Bank>, +see: String, +s1: B.Bank, +s2: B.Bank, +user: String, +key: String,725 +time: Nat, +name: String, +pass: String, h: Priv.R(r1, r2, name, pass), you: Laws.Same(s1, s2, user, key), pub: Laws.Public(s1, s2),726 same: Laws.Same(s1, s2, name, pass))727 -> Priv.Out(s1, s2, W.Web.done(W.Web.change(r1, see), s1, user, key, time), W.Web.done(W.Web.change(r2, see), s2, user, key, time), name, pass):728 match r1 r2:729 case Fail{+e1} Fail{e2}:730 (Priv.page("400 Bad Request", s1, s2, user, key, time, e1, e2, you, h), pub, same)731 case Fail{e1} Done{b2}:732 match h:733 case Done{b1} Fail{e2}:734 match h:735 case Done{b1} Done{b2}:736 (pb, sb) = h737 ({==}, pb, sb)738739# the same answer, given to both banks740def Priv.reply_same(m: Maybe<&2, B.Bank>, -text: String, -s1: B.Bank, -s2: B.Bank, -name: String, -pass: String,741 pub: Laws.Public(s1, s2), same: Laws.Same(s1, s2, name, pass)) -> Priv.Out(s1, s2, W.Reply{m, text}, W.Reply{m, text}, name, pass):742 match m:743 case None{}:744 ({==}, pub, same)745 case Some{b}:746 ({==}, ({==}, {==}), {==})747748# the same reply, or its failure page, agrees in both banks749def Priv.done_same(r: Result<&2, &2, String, W.Reply>, +s1: B.Bank, +s2: B.Bank, +user: String, +key: String, +time: Nat, +name: String, +pass: String,750 you: Laws.Same(s1, s2, user, key), pub: Laws.Public(s1, s2), same: Laws.Same(s1, s2, name, pass))751 -> Priv.Out(s1, s2, W.Web.done(r, s1, user, key, time), W.Web.done(r, s2, user, key, time), name, pass):752 match r:753 case Fail{+e}:754 (Priv.page("400 Bad Request", s1, s2, user, key, time, e, e, you, {==}), pub, same)755 case Done{W.Reply{m, text}}:756 Priv.reply_same(m, text, s1, s2, name, pass, pub, same)757758# every call gets the same answer and keeps the two banks in agreement759def Priv.answer(call: W.Call, +s1: B.Bank, +s2: B.Bank, +time: Nat, +rand: String, +user: String, +key: String, +name: String, +pass: String,760 ok1: Laws.Sound(s1), ok2: Laws.Sound(s2), +pub: Laws.Public(s1, s2), +you: Laws.Same(s1, s2, user, key), +same: Laws.Same(s1, s2, name, pass))761 -> Priv.Out(s1, s2, W.Web.answer(call, s1, time, rand, user, key), W.Web.answer(call, s2, time, rand, user, key), name, pass):762 match call:763 case W.Home{}:764 (Priv.page("200 OK", s1, s2, user, key, time, "", "", you, {==}), pub, same)765 case W.Join{+n}:766 h = Priv.join(s1, s2, n, rand, name, pass, ok1, ok2, pub, same)767 Priv.done(B.Bank.join(s1, n, rand), B.Bank.join(s2, n, rand), W.Http.see(n ++ "-" ++ rand), s1, s2, user, key, time, name, pass, h, you, pub, same)768 case W.Auth{+n, +k}:769 Priv.done_same(W.Web.login(n, k), s1, s2, user, key, time, name, pass, you, pub, same)770 case W.Quit{}:771 ({==}, pub, same)772 case W.Exec{+cmd}:773 h = Priv.exec(s1, s2, user, key, time, cmd, name, pass, pub, you, same)774 Priv.done(B.Bank.exec(s1, user, key, time, cmd), B.Bank.exec(s2, user, key, time, cmd), W.Http.home(), s1, s2, user, key, time, name, pass, h, you, pub, same)775 case W.Miss{}:776 ({==}, pub, same)777778# a parsed request gets the same answer from both banks779def Priv.reply(+s1: B.Bank, +s2: B.Bank, req: W.Req, +name: String, +pass: String, ok1: Laws.Sound(s1), ok2: Laws.Sound(s2), +pub: Laws.Public(s1, s2),780 +you: Laws.Same(s1, s2, Laws.Req.user(req), Laws.Req.pass(req)), +same: Laws.Same(s1, s2, name, pass))781 -> Priv.Out(s1, s2, W.Web.reply(s1, req), W.Web.reply(s2, req), name, pass):782 match req:783 case W.Req{time, rand, verb, path, user, key, form}:784 Priv.answer(W.Web.call(W.Web.find(W.Web.paths(), verb ++ " " ++ path, 0n), form), s1, s2, time, rand, user, key, name, pass, ok1, ok2, pub, you, same)785786# LAW privacy787def Laws.privacy(s1, s2, input, name, pass, ok1, ok2, pub, you, them):788 Priv.reply(s1, s2, W.Req.parse(input), name, pass, ok1, ok2, pub, you, them)