1# Bend Bank: the proof of LAW access2# ==================================34import Base5import ../bank.bend as B6import ../LAWS.bend as Laws7import ./base.bend as L89# keyed of an account is its own pass test10def Access.pass(a: B.Acc, +key: String, eb: {String.eq(B.Acc.pass(a), key) == True{} : Bool})11 -> {Laws.keyed(Some{a}, key) == True{} : Bool}:12 match a:13 case B.Acc{p, c, n, l, d, h}:14 eb1516# an account opened by its pass test: the test passed, at the key j17def Access.open(+j: B.Key(), +k: B.Key(), +accts: B.Trie<B.Acc>, +a: B.Acc, +key: String, b: Bool,18 eb: {String.eq(B.Acc.pass(a), key) == b : Bool}, ea: {B.Trie.get(B.Acc, j, accts) == Some{a} : Maybe<&2, B.Acc>},19 +me: {Laws.Key.is(Laws.opened(j, B.Bank.open(a, b)), k) == True{} : Bool})20 -> {Laws.Key.is(Some{j}, k) == True{} : Bool} & {Laws.keyed(B.Trie.get(B.Acc, k, accts), key) == True{} : Bool}:21 match b:22 case False{}:23 L.Bool.false_true({Laws.Key.is(Some{j}, k) == True{} : Bool} & {Laws.keyed(B.Trie.get(B.Acc, k, accts), key) == True{} : Bool}, me)24 case True{}:25 %L.Key.eq_true(j, k, me) : {Laws.Key.is(Some{j}, k) == True{} : Bool} & {Laws.keyed(B.Trie.get(B.Acc, _, accts), key) == True{} : Bool}26 %Equal.sym(Maybe<&2, B.Acc>, B.Trie.get(B.Acc, j, accts), Some{a}, ea) : {Laws.Key.is(Some{j}, k) == True{} : Bool} & {Laws.keyed(_, key) == True{} : Bool}27 (me, Access.pass(a, key, eb))2829# the account at j, which the cookie's key opened30def Access.acct(c: Maybe<&2, B.Acc>, +j: B.Key(), +k: B.Key(), +accts: B.Trie<B.Acc>, +key: String,31 ec: {B.Trie.get(B.Acc, j, accts) == c : Maybe<&2, B.Acc>},32 me: {Laws.Key.is(Laws.opened(j, B.Bank.check(c, key)), k) == True{} : Bool})33 -> {Laws.Key.is(Some{j}, k) == True{} : Bool} & {Laws.keyed(B.Trie.get(B.Acc, k, accts), key) == True{} : Bool}:34 match c:35 case None{}:36 L.Bool.false_true({Laws.Key.is(Some{j}, k) == True{} : Bool} & {Laws.keyed(B.Trie.get(B.Acc, k, accts), key) == True{} : Bool}, me)37 case Some{+a}:38 Access.open(j, k, accts, a, key, String.eq(B.Acc.pass(a), key), {==}, ec, me)3940# the key of the cookie's name, and the account there41def Access.at(m: Maybe<&2, B.Key()>, +accts: B.Trie<B.Acc>, +key: String, +k: B.Key(),42 me: {Laws.Key.is(Laws.Bank.sender.at(accts, m, key), k) == True{} : Bool})43 -> {Laws.Key.is(m, k) == True{} : Bool} & {Laws.keyed(B.Trie.get(B.Acc, k, accts), key) == True{} : Bool}:44 match m:45 case None{}:46 L.Bool.false_true({Laws.Key.is(None{}, k) == True{} : Bool} & {Laws.keyed(B.Trie.get(B.Acc, k, accts), key) == True{} : Bool}, me)47 case Some{+j}:48 Access.acct(B.Trie.get(B.Acc, j, accts), j, k, accts, key, {==}, me)4950def Access.bank(s: B.Bank, +user: String, +key: String, +k: B.Key(), me: {Laws.Key.is(Laws.Bank.sender(s, user, key), k) == True{} : Bool})51 -> {Laws.Key.is(B.Key.of(user), k) == True{} : Bool} & {Laws.keyed(Laws.acct(s, k), key) == True{} : Bool}:52 match s:53 case B.Bank{vault, +accts}:54 Access.at(B.Key.of(user), accts, key, k, me)5556# LAW access57def Laws.access(s, input, k, me):58 Access.bank(s, Laws.user(input), Laws.key(input), k, me)