1# Bend Bank: the core2# ===================3#4# The bank is one value, Bank: the vault and the accounts, keyed by name.5# Two functions change it, and nothing else does: Bank.join opens an6# account, and Bank.exec runs a command of an account holder. Both return7# Fail with a message, and then the caller keeps the old bank, or Done8# with the new one.9#10# Money lives in four places: the vault, which holds what no account11# holds yet; an account's cash; an account's credit line, the bank's12# money kept for that account's loans; and escrow, money one account13# locked for another, kept in the payee's account under the payer's name14# until the payer releases it to the payee or the payee refunds it.15# Opening an account moves 1,100 credits from the vault into it: 100 in16# cash and 1,000 in its line. Nothing else touches the vault, so it says17# nothing about any account. A loan moves money from the borrower's line18# to its cash; repaying moves it back, with 10% interest, rounded up. A19# loan not repaid by its due time is written off: it can no longer be20# repaid, and its borrower can never borrow again. Nothing ever creates21# or destroys money.22#23# A command is planned first and applied after. A Plan holds the24# requester's new account and a list of gifts: what the request does to25# other accounts. A plan is computed from the requester's own account and26# the command alone, and a gift only adds to the account it reaches.27# LAWS.bend states what this buys; PROOF.bend proves it.2829import Base3031# Types32# -----3334# a map from keys (bit strings) to values: a key is the path from the35# root, False to lo and True to hi; a node holds its own path's value36type Trie<-V: Data> is Data:37 Tip{}38 Bin{val: Maybe<&2, V>, lo: Trie<V>, hi: Trie<V>}3940# a loan: nothing owed, or a debt due at a time (seconds)41type Loan is Data:42 Clear{}43 Owing{debt: Nat, till: Nat}4445# an account: its key, its cash, its private note, its credit line, its46# loan, and the money others locked for it (payer to amount)47type Acc is Data:48 Acc{pass: String, cash: Nat, note: String, line: Nat, loan: Loan, held: Trie<Nat>}4950type Bank is Data:51 Bank{vault: Nat, accts: Trie<Acc>}5253# what the holder of an account sees: the account, and the money it54# locked in other accounts (payee to amount)55type View is Data:56 View{acct: Acc, lock: Trie<Nat>}5758# what a request by u does to the account at dest59type Gift is Data:60 Pay{dest: List<&2, Bool>, cash: Nat}61 Owe{dest: List<&2, Bool>, cash: Nat}62 Rel{dest: List<&2, Bool>}6364type Plan is Data:65 Plan{acct: Acc, gifts: List<&2, Gift>}6667# a step of a plan68type Op is Data:69 Need{test: Bool, text: String}70 Memo{text: String}71 Debt{loan: Loan}72 Give{dest: List<&2, Bool>, cash: Nat}73 Lock{dest: List<&2, Bool>, cash: Nat}74 Open{dest: List<&2, Bool>}75 Drop{dest: List<&2, Bool>}76 Draw{cash: Nat}77 Fund{cash: Nat}7879# one payee of a Send80type Line is Data:81 Line{name: String, cash: Nat}8283# what an account holder can ask for84type Cmd is Data:85 Note{text: String}86 Send{rows: List<&2, Line>}87 Lend{cash: Nat}88 Back{cash: Nat}89 Hold{name: String, cash: Nat}90 Free{name: String}91 Void{name: String}9293# Constants94# ---------9596# all the money there is: the vault holds it at the start97def Bank.genesis() -> Bank:98 Bank{1000000000n, Tip{}}99100# the cash of a new account101def Acc.grant() -> Nat:102 100n103104# the largest loan, which is also the credit line of a new account, and105# how long a loan runs (seconds)106def Loan.limit() -> Nat:107 1000n108109def Loan.term() -> Nat:110 600n111112# the longest note113def Acc.room() -> Nat:114 2000n115116# Key117# ---118# An account's key is its name, 6 bits per character. A name is 1 to 12119# characters, each a lowercase letter or a digit.120121def Key() -> Data:122 List<&2, Bool>123124def Key.rule() -> String:125 "a name is 1 to 12 lowercase letters or digits"126127def Key.eq(a: Key(), b: Key()) -> Bool:128 match a b:129 case Nil{} Nil{}:130 True{}131 case Nil{} y <> ys:132 False{}133 case x <> xs Nil{}:134 False{}135 case False{} <> xs False{} <> ys:136 Key.eq(xs, ys)137 case False{} <> xs True{} <> ys:138 False{}139 case True{} <> xs False{} <> ys:140 False{}141 case True{} <> xs True{} <> ys:142 Key.eq(xs, ys)143144# the 6 bits of x, high first, before ks145def Key.bits(+x: U32, +n: Nat, ks: Key()) -> Key():146 match n:147 case 0n:148 ks149 case 1n+p:150 +b = U32.is_eq(U32.and(U32.shrn(x, p), 1), 1)151 b <> Key.bits(x, p, ks)152153def Key.digit(x: U32, ks: Key(), ok: Bool) -> Maybe<&2, Key()>:154 match ok:155 case True{}:156 Some{Key.bits(U32.sub(x, 22), 6n, ks)}157 case False{}:158 None{}159160def Key.letter(+x: U32, ks: Key(), ok: Bool) -> Maybe<&2, Key()>:161 match ok:162 case True{}:163 Some{Key.bits(U32.sub(x, 97), 6n, ks)}164 case False{}:165 Key.digit(x, ks, Bool.and(U32.is_ge(x, 48), U32.is_le(x, 57)))166167# a name character's 6 bits: a-z are 0 to 25, 0-9 are 26 to 35168def Key.char(+x: U32, ks: Key()) -> Maybe<&2, Key()>:169 Key.letter(x, ks, Bool.and(U32.is_ge(x, 97), U32.is_le(x, 122)))170171def Key.then(+x: U32, m: Maybe<&2, Key()>) -> Maybe<&2, Key()>:172 match m:173 case None{}:174 None{}175 case Some{ks}:176 Key.char(x, ks)177178# the key of the first n characters of s, before the rest's key179def Key.go(s: String, n: Nat) -> Maybe<&2, Key()>:180 match s n:181 case SNil{} _:182 Some{Nil{}}183 case SCon{h, t} 0n:184 None{}185 case SCon{Chr{x}, t} 1n+p:186 Key.then(x, Key.go(t, p))187188def Key.of(s: String) -> Maybe<&2, Key()>:189 match s:190 case SNil{}:191 None{}192 case SCon{h, t}:193 Key.go(SCon{h, t}, 12n)194195# the character of a 6-bit code196def Key.show(+i: U32) -> Char:197 Chr{U32.add(i, Bool.pick(U32, U32.is_lt(i, 26), 97, 22))}198199# the name of a key; n bits of the current character remain, read so far200# into x201def Key.code(k: Key(), n: Nat, x: U32) -> String:202 match k n:203 case Nil{} _:204 SNil{}205 case b <> ks 0n:206 SNil{}207 case b <> ks 1n:208 SCon{Key.show(U32.add(U32.shl(x), Bool.to_u32(b))), Key.code(ks, 6n, 0)}209 case b <> ks 2n+p:210 Key.code(ks, 1n+p, U32.add(U32.shl(x), Bool.to_u32(b)))211212def Key.name(k: Key()) -> String:213 Key.code(k, 6n, 0)214215# Trie216# ----217218def Trie.val(-V: Data, t: Trie<V>) -> Maybe<&2, V>:219 match t:220 case Tip{}:221 None{}222 case Bin{v, lo, hi}:223 v224225def Trie.lo(-V: Data, t: Trie<V>) -> Trie<V>:226 match t:227 case Tip{}:228 Tip{}229 case Bin{v, lo, hi}:230 lo231232def Trie.hi(-V: Data, t: Trie<V>) -> Trie<V>:233 match t:234 case Tip{}:235 Tip{}236 case Bin{v, lo, hi}:237 hi238239def Trie.get(-V: Data, k: Key(), t: Trie<V>) -> Maybe<&2, V>:240 match k:241 case Nil{}:242 Trie.val(V, t)243 case False{} <> ks:244 Trie.get(V, ks, Trie.lo(V, t))245 case True{} <> ks:246 Trie.get(V, ks, Trie.hi(V, t))247248def Trie.set(-V: Data, k: Key(), +t: Trie<V>, m: Maybe<&2, V>) -> Trie<V>:249 match k:250 case Nil{}:251 Bin{m, Trie.lo(V, t), Trie.hi(V, t)}252 case False{} <> ks:253 Bin{Trie.val(V, t), Trie.set(V, ks, Trie.lo(V, t), m), Trie.hi(V, t)}254 case True{} <> ks:255 Bin{Trie.val(V, t), Trie.lo(V, t), Trie.set(V, ks, Trie.hi(V, t), m)}256257# an amount, absent when zero258def Trie.some(n: Nat) -> Maybe<&2, Nat>:259 match n:260 case 0n:261 None{}262 case 1n+p:263 Some{1n+p}264265def Trie.amount(m: Maybe<&2, Nat>) -> Nat:266 match m:267 case None{}:268 0n269 case Some{n}:270 n271272def Trie.num(k: Key(), t: Trie<Nat>) -> Nat:273 Trie.amount(Trie.get(Nat, k, t))274275def Trie.put(k: Key(), t: Trie<Nat>, n: Nat) -> Trie<Nat>:276 Trie.set(Nat, k, t, Trie.some(n))277278def Trie.sum(t: Trie<Nat>) -> Nat:279 match t:280 case Tip{}:281 0n282 case Bin{v, lo, hi}:283 Nat.add(Trie.amount(v), Nat.add(Trie.sum(lo), Trie.sum(hi)))284285# Acc286# ---287288def Acc.pass(a: Acc) -> String:289 match a:290 case Acc{pass, cash, note, line, loan, held}:291 pass292293# a new account with key pass: the grant in cash, the largest loan in its294# line295def Acc.new(pass: String) -> Acc:296 Acc{pass, Acc.grant(), "", Loan.limit(), Clear{}, Tip{}}297298# the money in an account: its cash, its line, and what others locked in299# it300def Acc.worth(a: Acc) -> Nat:301 match a:302 case Acc{pass, cash, note, line, loan, held}:303 Nat.add(cash, Nat.add(line, Trie.sum(held)))304305def Acc.worth_of(m: Maybe<&2, Acc>) -> Nat:306 match m:307 case None{}:308 0n309 case Some{a}:310 Acc.worth(a)311312def Acc.sum(t: Trie<Acc>) -> Nat:313 match t:314 case Tip{}:315 0n316 case Bin{v, lo, hi}:317 Nat.add(Acc.worth_of(v), Nat.add(Acc.sum(lo), Acc.sum(hi)))318319# what u locked in the account m320def Acc.locked(m: Maybe<&2, Acc>, +u: Key()) -> Maybe<&2, Nat>:321 match m:322 case None{}:323 None{}324 case Some{Acc{pass, cash, note, line, loan, held}}:325 Trie.get(Nat, u, held)326327# what u locked in each account of t, by payee328def Acc.locks(t: Trie<Acc>, +u: Key()) -> Trie<Nat>:329 match t:330 case Tip{}:331 Tip{}332 case Bin{v, lo, hi}:333 Bin{Acc.locked(v, u), Acc.locks(lo, u), Acc.locks(hi, u)}334335# Bank336# ----337338# all the money in the bank339def Bank.total(s: Bank) -> Nat:340 match s:341 case Bank{vault, accts}:342 Nat.add(vault, Acc.sum(accts))343344def Bank.vault(s: Bank) -> Nat:345 match s:346 case Bank{vault, accts}:347 vault348349def Bank.open(a: Acc, ok: Bool) -> Maybe<&2, Acc>:350 match ok:351 case True{}:352 Some{a}353 case False{}:354 None{}355356# the account, if pass is its key357def Bank.check(m: Maybe<&2, Acc>, +pass: String) -> Maybe<&2, Acc>:358 match m:359 case None{}:360 None{}361 case Some{+a}:362 Bank.open(a, String.eq(Acc.pass(a), pass))363364# the view of the account m at k, among the accounts t365def Bank.view(+t: Trie<Acc>, +k: Key(), m: Maybe<&2, Acc>) -> Maybe<&2, View>:366 match m:367 case None{}:368 None{}369 case Some{a}:370 Some{View{a, Acc.locks(t, k)}}371372def Bank.seen.at(+accts: Trie<Acc>, m: Maybe<&2, Key()>, pass: String) -> Maybe<&2, View>:373 match m:374 case None{}:375 None{}376 case Some{+k}:377 Bank.view(accts, k, Bank.check(Trie.get(Acc, k, accts), pass))378379# what the holder of (name, pass) may see of the bank: the view of the380# account with that name, if pass is its key381def Bank.seen(s: Bank, name: String, pass: String) -> Maybe<&2, View>:382 match s:383 case Bank{vault, accts}:384 Bank.seen.at(accts, Key.of(name), pass)385386# Gift387# ----388389def Gift.dest(g: Gift) -> Key():390 match g:391 case Pay{dest, cash}:392 dest393 case Owe{dest, cash}:394 dest395 case Rel{dest}:396 dest397398# the money a gift brings to its account399def Gift.cash(g: Gift) -> Nat:400 match g:401 case Pay{dest, cash}:402 cash403 case Owe{dest, cash}:404 cash405 case Rel{dest}:406 0n407408def Gift.sum(gs: List<&2, Gift>) -> Nat:409 match gs:410 case Nil{}:411 0n412 case g <> rest:413 Nat.add(Gift.cash(g), Gift.sum(rest))414415# the account a after a gift from u: Pay adds cash; Owe adds to what u416# locked in a; Rel moves what u locked in a into a's cash417def Gift.give(g: Gift, +u: Key(), a: Acc) -> Acc:418 match g a:419 case Pay{dest, x} Acc{pass, cash, note, line, loan, held}:420 Acc{pass, Nat.add(cash, x), note, line, loan, held}421 case Owe{dest, x} Acc{pass, cash, note, line, loan, +held}:422 Acc{pass, cash, note, line, loan, Trie.put(u, held, Nat.add(Trie.num(u, held), x))}423 case Rel{dest} Acc{pass, cash, note, line, loan, +held}:424 Acc{pass, Nat.add(cash, Trie.num(u, held)), note, line, loan, Trie.put(u, held, 0n)}425426# Plan427# ----428429# a bank after a gift from u to the account m at k; a gift to u itself,430# or to no account, fails431def Plan.gift.to(self: Bool, m: Maybe<&2, Acc>, vault: Nat, accts: Trie<Acc>, u: Key(), +k: Key(), g: Gift) -> Result<&2, &2, String, Bank>:432 match self m:433 case True{} _:434 Fail{"that is your own account"}435 case False{} None{}:436 Fail{"there is no account named " ++ Key.name(k)}437 case False{} Some{a}:438 Done{Bank{vault, Trie.set(Acc, k, accts, Some{Gift.give(g, u, a)})}}439440# a bank after one more gift from u441def Plan.gift(r: Result<&2, &2, String, Bank>, +u: Key(), +g: Gift) -> Result<&2, &2, String, Bank>:442 match r:443 case Fail{e}:444 Fail{e}445 case Done{Bank{vault, +accts}}:446 +k = Gift.dest(g)447 Plan.gift.to(Key.eq(k, u), Trie.get(Acc, k, accts), vault, accts, u, k, g)448449def Plan.gifts(gs: List<&2, Gift>, +u: Key(), r: Result<&2, &2, String, Bank>) -> Result<&2, &2, String, Bank>:450 match gs:451 case Nil{}:452 r453 case g <> rest:454 Plan.gifts(rest, u, Plan.gift(r, u, g))455456# the bank after the plan of u's request457def Plan.apply(s: Bank, +u: Key(), p: Plan) -> Result<&2, &2, String, Bank>:458 match s p:459 case Bank{vault, accts} Plan{acct, gifts}:460 Plan.gifts(gifts, u, Done{Bank{vault, Trie.set(Acc, u, accts, Some{acct})}})461462# Op463# --464# A command is a list of ops, run in order on a plan that starts as the465# requester's account and no gifts. An op that cannot run fails the466# whole command. Every op keeps the plan's money (the account's worth and467# the gifts' cash) the same: that is conservation.468469# fail with text unless test holds470def Op.need(test: Bool, text: String, p: Plan) -> Result<&2, &2, String, Plan>:471 match test:472 case True{}:473 Done{p}474 case False{}:475 Fail{text}476477def Op.at(op: Op, a: Acc, gifts: List<&2, Gift>) -> Result<&2, &2, String, Plan>:478 match op a:479 case Need{test, text} a:480 Op.need(test, text, Plan{a, gifts})481 case Memo{t} Acc{pass, cash, note, line, loan, held}:482 Done{Plan{Acc{pass, cash, t, line, loan, held}, gifts}}483 case Debt{d} Acc{pass, cash, note, line, loan, held}:484 Done{Plan{Acc{pass, cash, note, line, d, held}, gifts}}485 case Give{k, +x} Acc{pass, +cash, note, line, loan, held}:486 Op.need(Nat.is_le(x, cash), "you do not have that much", Plan{Acc{pass, Nat.sub(cash, x), note, line, loan, held}, Pay{k, x} <> gifts})487 case Lock{k, +x} Acc{pass, +cash, note, line, loan, held}:488 Op.need(Nat.is_le(x, cash), "you do not have that much", Plan{Acc{pass, Nat.sub(cash, x), note, line, loan, held}, Owe{k, x} <> gifts})489 case Open{k} a:490 Done{Plan{a, Rel{k} <> gifts}}491 case Drop{+k} Acc{pass, cash, note, line, loan, +held}:492 Done{Plan{Acc{pass, cash, note, line, loan, Trie.put(k, held, 0n)}, Pay{k, Trie.num(k, held)} <> gifts}}493 case Draw{+x} Acc{pass, cash, note, +line, loan, held}:494 Op.need(Nat.is_le(x, line), "the bank has no more credit for you", Plan{Acc{pass, Nat.add(cash, x), note, Nat.sub(line, x), loan, held}, gifts})495 case Fund{+x} Acc{pass, +cash, note, line, loan, held}:496 Op.need(Nat.is_le(x, cash), "you do not have that much", Plan{Acc{pass, Nat.sub(cash, x), note, Nat.add(line, x), loan, held}, gifts})497498def Op.step(r: Result<&2, &2, String, Plan>, op: Op) -> Result<&2, &2, String, Plan>:499 match r:500 case Fail{e}:501 Fail{e}502 case Done{Plan{a, gifts}}:503 Op.at(op, a, gifts)504505def Op.run(ops: List<&2, Op>, r: Result<&2, &2, String, Plan>) -> Result<&2, &2, String, Plan>:506 match ops:507 case Nil{}:508 r509 case op <> rest:510 Op.run(rest, Op.step(r, op))511512# Cmd513# ---514515def Cmd.positive() -> String:516 "amounts must be positive"517518# the key of a name; Nil when the name is not valid, and then the need519# before it fails520def Cmd.key(+name: String) -> Key():521 Maybe.default(&2, Key(), Key.of(name), Nil{})522523def Cmd.named(+name: String) -> Op:524 Need{Maybe.is_some(&2, Key(), Key.of(name)), Key.rule()}525526def Cmd.fits(s: String, n: Nat) -> Bool:527 match s n:528 case SNil{} _:529 True{}530 case SCon{h, t} 0n:531 False{}532 case SCon{h, t} 1n+p:533 Cmd.fits(t, p)534535# the ops of a Send: each row names a payee and pays a positive amount536def Cmd.rows(rows: List<&2, Line>) -> List<&2, Op>:537 match rows:538 case Nil{}:539 Nil{}540 case Line{+name, +cash} <> rest:541 Cmd.named(name) <> Need{Nat.is_lt(0n, cash), Cmd.positive()} <> Give{Cmd.key(name), cash} <> Cmd.rows(rest)542543# a loan after paying n of its debt544def Loan.rest(debt: Nat, till: Nat) -> Loan:545 match debt:546 case 0n:547 Clear{}548 case 1n+p:549 Owing{1n+p, till}550551# the interest on a loan of x: 10%, rounded up552def Loan.interest(x: Nat) -> Nat:553 Nat.div(Nat.add(x, 9n), 10n)554555# the ops of a loan or a repayment, given the current loan556def Cmd.lend(+x: Nat, loan: Loan, +now: Nat) -> List<&2, Op>:557 match loan:558 case Owing{debt, till}:559 [Need{False{}, "you already have a loan"}]560 case Clear{}:561 [Need{Nat.is_lt(0n, x), Cmd.positive()},562 Need{Nat.is_le(x, Loan.limit()), "the largest loan is 1,000"},563 Draw{x}, Debt{Owing{Nat.add(x, Loan.interest(x)), Nat.add(now, Loan.term())}}]564565def Cmd.back(+x: Nat, loan: Loan, +now: Nat) -> List<&2, Op>:566 match loan:567 case Clear{}:568 [Need{False{}, "you have no loan"}]569 case Owing{+debt, +till}:570 [Need{Nat.is_lt(0n, x), Cmd.positive()},571 Need{Nat.is_le(now, till), "your loan was written off"},572 Need{Nat.is_le(x, debt), "you owe less than that"},573 Fund{x}, Debt{Loan.rest(Nat.sub(debt, x), till)}]574575# the ops of a command by the holder of a, at time now576def Cmd.ops(cmd: Cmd, a: Acc, now: Nat) -> List<&2, Op>:577 match cmd a:578 case Note{+text} a:579 [Need{Cmd.fits(text, Acc.room()), "a note is at most 2,000 characters"}, Memo{text}]580 case Send{+rows} a:581 Need{Bool.not(List.is_empty(&2, Line, rows)), "there is nothing to send"} <> Cmd.rows(rows)582 case Lend{x} Acc{pass, cash, note, line, loan, held}:583 Cmd.lend(x, loan, now)584 case Back{x} Acc{pass, cash, note, line, loan, held}:585 Cmd.back(x, loan, now)586 case Hold{+name, +x} a:587 [Cmd.named(name), Need{Nat.is_lt(0n, x), Cmd.positive()}, Lock{Cmd.key(name), x}]588 case Free{+name} a:589 [Cmd.named(name), Open{Cmd.key(name)}]590 case Void{+name} a:591 [Cmd.named(name), Drop{Cmd.key(name)}]592593# the plan of a command by the holder of a594def Cmd.plan(cmd: Cmd, +a: Acc, now: Nat) -> Result<&2, &2, String, Plan>:595 Op.run(Cmd.ops(cmd, a, now), Done{Plan{a, Nil{}}})596597# Requests598# --------599600# the bank after a plan of the holder of k601def Bank.plan(+s: Bank, +k: Key(), r: Result<&2, &2, String, Plan>) -> Result<&2, &2, String, Bank>:602 match r:603 case Fail{e}:604 Fail{e}605 case Done{p}:606 Plan.apply(s, k, p)607608# the bank with a new account, if the vault can fund it609def Bank.fund(ok: Bool, s: Bank) -> Result<&2, &2, String, Bank>:610 match ok:611 case True{}:612 Done{s}613 case False{}:614 Fail{"the bank opens no more accounts"}615616# open an account at k with key pass, unless the account m is there: it617# takes its cash and its line from the vault618def Bank.join.at(m: Maybe<&2, Acc>, s: Bank, +k: Key(), pass: String) -> Result<&2, &2, String, Bank>:619 match m s:620 case Some{a} _:621 Fail{"that name is taken"}622 case None{} Bank{+vault, accts}:623 +x = Nat.add(Acc.grant(), Loan.limit())624 Bank.fund(Nat.is_le(x, vault), Bank{Nat.sub(vault, x), Trie.set(Acc, k, accts, Some{Acc.new(pass)})})625626def Bank.join.key(m: Maybe<&2, Key()>, s: Bank, pass: String) -> Result<&2, &2, String, Bank>:627 match m s:628 case None{} _:629 Fail{Key.rule()}630 case Some{+k} Bank{vault, +accts}:631 Bank.join.at(Trie.get(Acc, k, accts), Bank{vault, accts}, k, pass)632633# open an account named name, with key pass634def Bank.join(s: Bank, name: String, pass: String) -> Result<&2, &2, String, Bank>:635 Bank.join.key(Key.of(name), s, pass)636637def Bank.exec.acct(+s: Bank, +k: Key(), m: Maybe<&2, Acc>, now: Nat, cmd: Cmd) -> Result<&2, &2, String, Bank>:638 match m:639 case None{}:640 Fail{"log in first"}641 case Some{a}:642 Bank.plan(s, k, Cmd.plan(cmd, a, now))643644def Bank.exec.key(m: Maybe<&2, Key()>, s: Bank, pass: String, now: Nat, cmd: Cmd) -> Result<&2, &2, String, Bank>:645 match m s:646 case None{} _:647 Fail{"log in first"}648 case Some{+k} Bank{+vault, +accts}:649 Bank.exec.acct(Bank{vault, accts}, k, Bank.check(Trie.get(Acc, k, accts), pass), now, cmd)650651# run cmd for the holder of (name, pass), at time now652def Bank.exec(s: Bank, name: String, pass: String, now: Nat, cmd: Cmd) -> Result<&2, &2, String, Bank>:653 Bank.exec.key(Key.of(name), s, pass, now, cmd)