1# Bend Bank: the web2# ==================3#4# Web.serve is the whole server as one pure function: it takes the bank5# and one request, and returns the bank's change (None when nothing6# changed) and the bytes of the answer. The host (host.mjs) only moves7# bytes: it reads a request off a socket, prefixes the time and a fresh8# random key, calls Web.serve, appends the request to the log when the9# bank changed, and writes the answer back.10#11# The input is "<time>\n<rand>\n<HTTP request>", one character per byte.12# A request names its holder by the cookie "bank=<name>-<key>". Pages are13# plain HTML forms, with no JavaScript. A change answers 303 See Other; a14# failed request answers 400 with the page and the reason.15#16# Loops over text are tail calls, so they run in constant stack. Where a17# loop stops on a computed test, it hands the rest of the loop to18# Bool.when as a closure.1920import Base21import ./bank.bend as B2223# Types24# -----2526# a form field27type Field is Data:28 Field{name: String, text: String}2930# a parsed request: the host's time and random key, the method, the path,31# the cookie's name and key, and the form32type Req is Data:33 Req{time: Nat, rand: String, verb: String, path: String, user: String, pass: String, form: List<&2, Field>}3435# what a request asks for36type Call is Data:37 Home{}38 Join{name: String}39 Auth{name: String, pass: String}40 Quit{}41 Exec{cmd: B.Cmd}42 Miss{}4344# the answer: the new bank, if it changed, and the bytes to send45type Reply is Data:46 Reply{bank: Maybe<&2, B.Bank>, text: String}4748# Constants49# ---------5051# the public copy of the code this site runs (deploy/pub.mjs)52def Web.code() -> String:53 "https://bend-lang.com/dl/bank/"5455# the largest request the host passes on56def Web.room() -> Nat:57 16384n5859# Text60# ----6162# found when hit holds, else the rest of the loop63def Bool.when(-R: Type, hit: Bool, miss: Unit -> R, found: R) -> R:64 match hit:65 case True{}:66 found67 case False{}:68 miss(Unit{})6970def Text.push(acc: String, c: Char) -> String:71 acc ++ SCon{c, SNil{}}7273# s up to the first c; all of s when there is no c74def Text.before(s: String, +c: Char, +acc: String) -> String:75 match s:76 case SNil{}:77 acc78 case SCon{+h, t}:79 Bool.when(String, Char.is_eq(h, c), u => Text.before(t, c, Text.push(acc, h)), acc)8081# s after the first c; "" when there is no c82def Text.after(s: String, +c: Char) -> String:83 match s:84 case SNil{}:85 SNil{}86 case SCon{h, +t}:87 Bool.when(String, Char.is_eq(h, c), u => Text.after(t, c), t)8889# the pieces of s between each c, in reverse, after out90def Text.split(s: String, +c: Char, +acc: String, +out: List<&2, String>) -> List<&2, String>:91 match s:92 case SNil{}:93 acc <> out94 case SCon{+h, t}:95 +hit = Char.is_eq(h, c)96 Text.split(t, c, Bool.pick(String, hit, "", Text.push(acc, h)), Bool.pick(List<&2, String>, hit, acc <> out, out))9798def Text.pieces(s: String, +c: Char) -> List<&2, String>:99 List.reverse(&2, String, Text.split(s, c, "", Nil{}))100101def Text.lower(s: String, acc: String) -> String:102 match s:103 case SNil{}:104 acc105 case SCon{h, t}:106 Text.lower(t, Text.push(acc, Char.to_lower(h)))107108def Text.trim(s: String) -> String:109 match s:110 case SCon{' ', t}:111 Text.trim(t)112 case t:113 t114115# s without a trailing "\r"116def Text.chomp(s: String, acc: String) -> String:117 match s:118 case SNil{}:119 acc120 case SCon{'\r', SNil{}}:121 acc122 case SCon{h, t}:123 Text.chomp(t, Text.push(acc, h))124125# the number in s, at most n more digits, else 0126def Text.num(s: String, n: Nat, acc: Nat) -> Nat:127 match s n:128 case SNil{} _:129 acc130 case SCon{h, t} 0n:131 0n132 case SCon{Chr{x}, t} 1n+p:133 +d = U32.sub(x, 48)134 +ok = U32.is_lt(d, 10)135 Bool.when(Nat, Bool.not(ok), u => Text.num(t, p, Nat.add(Nat.mul(acc, 10n), U32.to_nat(d))), 0n)136137# the number in s: 1 to 12 digits, else 0138def Text.nat(s: String) -> Nat:139 match s:140 case SNil{}:141 0n142 case SCon{h, t}:143 Text.num(SCon{h, t}, 12n, 0n)144145# a hex digit's value, or 16 for any other character146def Text.hex(c: Char) -> U32:147 match c:148 case Chr{+x}:149 +d = U32.sub(x, 48)150 +l = U32.sub(U32.or(x, 32), 97)151 Bool.pick(U32, U32.is_lt(d, 10), d, Bool.pick(U32, U32.is_lt(l, 6), U32.add(l, 10), 16))152153# a form value decoded: "+" is a space and "%41" is "A"154def Text.decode(s: String, acc: String) -> String:155 match s:156 case SNil{}:157 acc158 case SCon{'+', t}:159 Text.decode(t, Text.push(acc, ' '))160 case SCon{'%', SCon{a, SCon{b, t}}}:161 +x = Text.hex(a)162 +y = Text.hex(b)163 +ok = Bool.and(U32.is_lt(x, 16), U32.is_lt(y, 16))164 Text.decode(t, Text.push(acc, Bool.pick(Char, ok, Chr{U32.add(U32.mul(x, 16), y)}, '?')))165 case SCon{h, t}:166 Text.decode(t, Text.push(acc, h))167168# s with HTML's special characters escaped169def Text.html(s: String, acc: String) -> String:170 match s:171 case SNil{}:172 acc173 case SCon{'&', t}:174 Text.html(t, acc ++ "&")175 case SCon{'<', t}:176 Text.html(t, acc ++ "<")177 case SCon{'>', t}:178 Text.html(t, acc ++ ">")179 case SCon{'"', t}:180 Text.html(t, acc ++ """)181 case SCon{'\'', t}:182 Text.html(t, acc ++ "'")183 case SCon{h, t}:184 Text.html(t, Text.push(acc, h))185186def Text.len(s: String, n: Nat) -> Nat:187 match s:188 case SNil{}:189 n190 case SCon{h, t}:191 Text.len(t, 1n+n)192193# whether s is 1 to 64 letters and digits, so it can go in a cookie194def Text.safe(s: String, n: Nat) -> Bool:195 match s n:196 case SNil{} _:197 True{}198 case SCon{h, t} 0n:199 False{}200 case SCon{Chr{+x}, t} 1n+p:201 +ok = Bool.or(Bool.and(U32.is_ge(x, 48), U32.is_le(x, 57)), Char.is_alpha(Chr{x}))202 Bool.and(ok, Text.safe(t, p))203204def Text.esc(s: String) -> String:205 Text.html(s, "")206207# n with its thousands grouped: 1234567 is "1,234,567"208def Text.group(f: Nat, +n: Nat) -> String:209 match f:210 case 0n:211 Nat.show(n)212 case 1n+g:213 +r = Nat.mod(n, 1000n)214 +pad = Bool.pick(String, Nat.is_lt(r, 10n), "00", Bool.pick(String, Nat.is_lt(r, 100n), "0", ""))215 +big = Text.group(g, Nat.div(n, 1000n)) ++ "," ++ pad ++ Nat.show(r)216 Bool.pick(String, Nat.is_lt(n, 1000n), Nat.show(n), big)217218def Text.money(n: Nat) -> String:219 Text.group(4n, n)220221# Parse222# -----223224# the bank cookie's value among the parts of a cookie header225def Req.crumb(parts: List<&2, String>) -> String:226 match parts:227 case Nil{}:228 ""229 case p <> rest:230 +q = Text.trim(p)231 +hit = String.eq(Text.before(q, '=', ""), "bank")232 Bool.when(String, hit, u => Req.crumb(rest), Text.after(q, '='))233234# the bank cookie's value, "<name>-<key>", among the header lines; ""235# when there is none236def Req.cookie(lines: List<&2, String>) -> String:237 match lines:238 case Nil{}:239 ""240 case +l <> rest:241 +hit = String.eq(Text.lower(Text.before(l, ':', ""), ""), "cookie")242 Bool.when(String, hit, u => Req.cookie(rest), Req.crumb(Text.pieces(Text.after(l, ':'), ';')))243244# the header lines, up to the blank line, and the line after it: the body245def Req.head(lines: List<&2, String>, +acc: List<&2, String>) -> List<&2, String> & String:246 match lines:247 case Nil{}:248 (acc, "")249 case l <> +rest:250 +h = Text.chomp(l, "")251 +body = List.head(&2, String, rest)252 Bool.when(List<&2, String> & String, String.is_empty(h), u => Req.head(rest, h <> acc), (acc, Maybe.default(&2, String, body, "")))253254def Req.field(+s: String) -> Field:255 Field{Text.decode(Text.before(s, '=', ""), ""), Text.decode(Text.after(s, '='), "")}256257def Req.fields(parts: List<&2, String>, acc: List<&2, Field>) -> List<&2, Field>:258 match parts:259 case Nil{}:260 acc261 case p <> rest:262 Req.fields(rest, Req.field(p) <> acc)263264# the first value of the field name, or ""265def Req.get(form: List<&2, Field>, +name: String) -> String:266 match form:267 case Nil{}:268 ""269 case Field{k, +v} <> rest:270 Bool.when(String, String.eq(k, name), u => Req.get(rest, name), v)271272def Req.at(lines: List<&2, String>, n: Nat) -> String:273 Maybe.default(&2, String, List.get(&2, String, lines, n), "")274275def Req.parse.at(+lines: List<&2, String>, +line: List<&2, String>, hb: List<&2, String> & String) -> Req:276 (head, body) = hb277 +who = Req.cookie(head)278 +path = Text.before(Req.at(line, 1n), '?', "")279 +form = Req.fields(Text.pieces(body, '&'), Nil{})280 +user = Text.before(who, '-', "")281 Req{Text.nat(Req.at(lines, 0n)), Req.at(lines, 1n), Req.at(line, 0n), path, user, Text.after(who, '-'), form}282283# the request in the host's input284def Req.parse(input: String) -> Req:285 +lines = Text.pieces(input, '\n')286 +line = Text.pieces(Text.chomp(Req.at(lines, 2n), ""), ' ')287 Req.parse.at(lines, line, Req.head(List.drop(&2, String, lines, 3n), Nil{}))288289# the length of the HTTP request whose lines are lines, once its head has290# arrived: n characters so far, and its Content-Length so far291def Req.size.go(lines: List<&2, String>, +n: Nat, +len: Nat) -> Maybe<&2, Nat>:292 match lines:293 case Nil{}:294 None{}295 case +l <> rest:296 +m = Nat.add(n, Text.len(l, 1n))297 +h = Text.chomp(l, "")298 +hit = String.eq(Text.lower(Text.before(h, ':', ""), ""), "content-length")299 +len2 = Bool.pick(Nat, hit, Text.nat(Text.trim(Text.after(h, ':'))), len)300 Bool.when(Maybe<&2, Nat>, String.is_empty(h), u => Req.size.go(rest, m, len2), Some{Nat.add(m, len)})301302# the length of the HTTP request at the start of buf, once its head has303# arrived: the head, its blank line and its Content-Length304def Req.size(buf: String) -> Maybe<&2, Nat>:305 Req.size.go(Text.pieces(buf, '\n'), 0n, 0n)306307# Route308# -----309310def Web.paths() -> List<&2, String>:311 ["GET /", "POST /join", "POST /login", "POST /logout", "POST /note",312 "POST /send", "POST /borrow", "POST /repay", "POST /hold",313 "POST /release", "POST /refund"]314315# the position of s in xs, past n316def Web.find(xs: List<&2, String>, +s: String, +n: Nat) -> Nat:317 match xs:318 case Nil{}:319 n320 case x <> rest:321 Bool.when(Nat, String.eq(x, s), u => Web.find(rest, s, 1n+n), n)322323# the rows of a Send: the fields to1, cash1 up to to3, cash3, skipping324# rows where both fields are empty325def Web.rows(+form: List<&2, Field>, +n: Nat) -> List<&2, B.Line>:326 match n:327 case 0n:328 Nil{}329 case 1n+p:330 +i = Nat.show(1n+p)331 +to = Req.get(form, "to" ++ i)332 +cash = Req.get(form, "cash" ++ i)333 +rest = Web.rows(form, p)334 +blank = Bool.and(String.is_empty(to), String.is_empty(cash))335 Bool.pick(List<&2, B.Line>, blank, rest, List.append(&2, B.Line, rest, [B.Line{to, Text.nat(cash)}]))336337def Web.call(i: Nat, +form: List<&2, Field>) -> Call:338 match i:339 case 0n:340 Home{}341 case 1n:342 Join{Req.get(form, "name")}343 case 2n:344 Auth{Req.get(form, "name"), Req.get(form, "key")}345 case 3n:346 Quit{}347 case 4n:348 Exec{B.Note{Req.get(form, "text")}}349 case 5n:350 Exec{B.Send{Web.rows(form, 3n)}}351 case 6n:352 Exec{B.Lend{Text.nat(Req.get(form, "cash"))}}353 case 7n:354 Exec{B.Back{Text.nat(Req.get(form, "cash"))}}355 case 8n:356 Exec{B.Hold{Req.get(form, "name"), Text.nat(Req.get(form, "cash"))}}357 case 9n:358 Exec{B.Free{Req.get(form, "name")}}359 case 10n:360 Exec{B.Void{Req.get(form, "name")}}361 case 11n+p:362 Miss{}363364# Page365# ----366367def Page.style() -> String:368 "*{box-sizing:border-box}body{margin:0;font:15px/1.5 system-ui,-apple-system,'Segoe UI',Roboto,sans-serif;color:#1a2433;background:#f3f5f8}" ++369 "a{color:#0b5cad}.in{max-width:1120px;margin:0 auto;padding:0 32px}" ++370 ".bar{background:#0f2a44}.bar .in{display:flex;align-items:center;justify-content:space-between;height:56px}" ++371 ".brand{color:#fff;font-size:19px;font-weight:700;text-decoration:none}.bar a{color:#cfe0f5}" ++372 ".dare{background:#b42318;color:#fff}.dare .in{padding-top:20px;padding-bottom:22px}" ++373 ".dare h1{margin:0;font-size:34px;line-height:1.15;font-weight:800}.dare p{margin:8px 0 0;font-size:17px;max-width:780px}.dare a{color:#fff;font-weight:700}" ++374 "main.in{padding-top:28px;padding-bottom:48px}" ++375 ".grid{display:grid;grid-template-columns:minmax(0,1fr) minmax(0,1fr);gap:28px;align-items:start}@media(max-width:860px){.grid{grid-template-columns:1fr}}" ++376 ".card{background:#fff;border:1px solid #e1e6ec;border-radius:12px;padding:20px 22px;margin-bottom:16px}" ++377 "h2{font-size:16px;margin:0 0 10px}p{margin:0 0 8px}.muted{color:#5b6878;font-size:13px}" ++378 ".err{background:#fef3f2;border:1px solid #fecdca;color:#b42318;border-radius:10px;padding:10px 14px;margin-bottom:16px}" ++379 ".head{display:flex;justify-content:space-between;align-items:flex-start;gap:12px}.bal{font-size:34px;font-weight:700;line-height:1.2}" ++380 ".row{display:flex;gap:8px;align-items:center;flex-wrap:wrap;margin:8px 0}.line{display:flex;justify-content:space-between;align-items:center;gap:8px;padding:8px 0;border-top:1px solid #eef1f4}" ++381 "input,textarea,button{font:inherit}input{height:36px;width:160px;flex:1 1 120px;max-width:200px;min-width:0;padding:0 10px;border:1px solid #c7d0db;border-radius:7px}" ++382 "textarea{width:100%;height:84px;padding:8px 10px;border:1px solid #c7d0db;border-radius:7px;resize:vertical}" ++383 "button{height:36px;padding:0 16px;white-space:nowrap;border:1px solid #0f2a44;border-radius:7px;background:#0f2a44;color:#fff;font-weight:600;cursor:pointer}button.alt{background:#fff;color:#0f2a44}" ++384 ".laws{list-style:none;margin:6px 0 10px;padding:0}.laws li{padding:6px 0;border-top:1px solid #eef1f4}.laws li:first-child{border-top:0}" ++385 "code{background:#eef1f5;padding:1px 5px;border-radius:4px;font-size:13px;word-break:break-all}" ++386 "@media(max-width:600px){.in{padding:0 16px}.dare h1{font-size:28px}.bal{font-size:28px}.card{padding:16px}}"387388# words of a rule, linked to the law that states them: check/links.mjs389# checks the line390def Page.law(name: String, line: String, text: String) -> String:391 "<a id=" ++ name ++ " href=\"" ++ Web.code() ++ "LAWS.bend.html#L" ++ line ++ "\">" ++ text ++ "</a>"392393def Page.laws() -> String:394 "<div class=card><h2>Proven in Bend</h2><ul class=laws>" ++395 "<li>" ++ Page.law("privacy", "262", "Only you can see your account.") ++ "</li>" ++396 "<li>" ++ Page.law("authority", "291", "No one else can take your money.") ++ "</li>" ++397 "<li>" ++ Page.law("conservation", "339", "Money is never created or destroyed.") ++ "</li>" ++398 "</ul><p class=muted>Check: <code>bend PROOF.bend --verdict</code></p></div>"399400# one escrow: its amount, the other account, and the button that settles it401def Page.escrow(m: Maybe<&2, Nat>, +name: String, +act: String, +label: String, text: String) -> String:402 match m:403 case None{}:404 ""405 case Some{x}:406 "<form method=post action=/" ++ act ++ " class=line><input type=hidden name=name value=" ++ name ++ ">" ++407 "<span><b>" ++ Text.money(x) ++ "</b> " ++ text ++ " <b>" ++ name ++ "</b></span><button class=alt>" ++ label ++ "</button></form>"408409# the escrows of a trie of amounts, one per account; path is the key so410# far, reversed411def Page.escrows(t: B.Trie<Nat>, +path: List<&2, Bool>, +act: String, +label: String, +text: String, acc: String) -> String:412 match t:413 case B.Tip{}:414 acc415 case B.Bin{v, lo, hi}:416 +row = Page.escrow(v, B.Key.name(List.reverse(&2, Bool, path)), act, label, text)417 +acc = Page.escrows(lo, False{} <> path, act, label, text, acc ++ row)418 Page.escrows(hi, True{} <> path, act, label, text, acc)419420def Page.loan(l: B.Loan, +now: Nat) -> String:421 match l:422 case B.Clear{}:423 "<p>Borrow up to 1,000. Pay back 10% more within 10 minutes.</p>" ++424 "<form method=post action=/borrow class=row><input name=cash placeholder=Amount><button>Borrow</button></form>"425 case B.Owing{+debt, +till}:426 +mins = Nat.div(Nat.add(Nat.sub(till, now), 59n), 60n)427 +due = "<p>You owe <b>" ++ Text.money(debt) ++ "</b>, due in " ++ Nat.show(mins) ++ " min.</p>" ++428 "<form method=post action=/repay class=row><input name=cash placeholder=Amount><button>Repay</button></form>"429 +off = "<p>Your loan of <b>" ++ Text.money(debt) ++ "</b> is overdue and written off. No more loans.</p>"430 Bool.pick(String, Nat.is_le(now, till), due, off)431432def Page.send(+n: Nat) -> String:433 match n:434 case 0n:435 ""436 case 1n+p:437 +i = Nat.show(1n+p)438 Page.send(p) ++ "<div class=row><input name=to" ++ i ++ " placeholder=Name><input name=cash" ++ i ++ " placeholder=Amount></div>"439440def Page.acct(+user: String, v: B.View, +now: Nat) -> String:441 match v:442 case B.View{B.Acc{pass, cash, note, line, loan, held}, lock}:443 "<div class=card><div class=head><div><div class=muted>" ++ Text.esc(user) ++ "</div><div class=bal>" ++ Text.money(cash) ++ " credits</div></div>" ++444 "<form method=post action=/logout><button class=alt>Log out</button></form></div>" ++445 "<p class=muted>Your key: <code>" ++ Text.esc(pass) ++ "</code>. Keep it secret.</p></div>" ++446 "<div class=card><h2>Send money</h2><form method=post action=/send>" ++ Page.send(3n) ++ "<div class=row><button>Send</button></div></form></div>" ++447 "<div class=card><h2>Loan</h2>" ++ Page.loan(loan, now) ++ "</div>" ++448 "<div class=card><h2>Escrow</h2><form method=post action=/hold class=row><input name=cash placeholder=Amount><span>for</span><input name=name placeholder=Name><button>Lock</button></form>" ++449 Page.escrows(lock, Nil{}, "release", "Release", "locked for", "") ++450 Page.escrows(held, Nil{}, "refund", "Refund", "locked for you by", "") ++ "</div>" ++451 "<div class=card><h2>Private note</h2><form method=post action=/note><textarea name=text>" ++ Text.esc(note) ++ "</textarea>" ++452 "<div class=row><button>Save</button></div></form></div>"453454def Page.guest() -> String:455 "<div class=card><h2>Open an account</h2><form method=post action=/join class=row><input name=name placeholder=\"Name: a-z, 0-9\" maxlength=12><button>Open</button></form></div>" ++456 "<div class=card><h2>Log in</h2><form method=post action=/login class=row><input name=name placeholder=Name><input name=key placeholder=Key><button>Log in</button></form></div>"457458def Page.error(e: String) -> String:459 match e:460 case SNil{}:461 ""462 case SCon{h, t}:463 "<div class=err>" ++ Text.esc(SCon{h, t}) ++ "</div>"464465# the top of every page: the bar, and the challenge466def Page.top() -> String:467 "<!doctype html><html lang=en><head><meta charset=utf-8><meta name=viewport content=\"width=device-width,initial-scale=1\">" ++468 "<title>Bend Bank</title><style>" ++ Page.style() ++ "</style></head><body>" ++469 "<div class=bar><div class=in><a class=brand href=/>Bend Bank</a><a href=\"" ++ Web.code() ++ "\">Source code</a></div></div>" ++470 "<div class=dare><div class=in><h1>Break this bank.</h1><p>Read the flag in <b>company</b>'s private note, " ++471 "or make money appear. The <a href=\"" ++ Web.code() ++ "\">code</a> is open.</p></div></div>"472473def Page.end() -> String:474 "</div></main></body></html>"475476# the page for the holder of user's cookie, who sees seen, after err477def Page.home(seen: Maybe<&2, B.View>, user: String, now: Nat, err: String) -> String:478 match seen:479 case None{}:480 +hint = Bool.pick(String, String.is_empty(user), "", "that name and key open no account")481 Page.top() ++ "<main class=in>" ++ Page.error(err) ++ Page.error(hint) ++ "<div class=grid><div>" ++ Page.guest() ++ "</div>" ++ Page.laws() ++ Page.end()482 case Some{v}:483 Page.top() ++ "<main class=in>" ++ Page.error(err) ++ "<div class=grid><div>" ++ Page.acct(user, v, now) ++ "</div>" ++ Page.laws() ++ Page.end()484485# HTTP486# ----487488def Http.head() -> String:489 "Content-Type: text/html; charset=utf-8\r\nCache-Control: no-store\r\n" ++490 "Content-Security-Policy: default-src 'none'; style-src 'unsafe-inline'; form-action 'self'; frame-ancestors 'none'; base-uri 'none'\r\n" ++491 "X-Content-Type-Options: nosniff\r\nReferrer-Policy: no-referrer\r\n"492493# an answer with a status line, extra headers and a body494def Http.answer(status: String, extra: String, +body: String) -> String:495 "HTTP/1.1 " ++ status ++ "\r\n" ++ extra ++ Http.head() ++ "Content-Length: " ++ Nat.show(Text.len(body, 0n)) ++ "\r\n\r\n" ++ body496497# a redirect home, setting the bank cookie to v ("" logs out)498def Http.see(+v: String) -> String:499 +age = Bool.pick(String, String.is_empty(v), "0", "31536000")500 Http.answer("303 See Other", "Location: /\r\nSet-Cookie: bank=" ++ v ++ "; Path=/; Max-Age=" ++ age ++ "; HttpOnly; Secure; SameSite=Strict\r\n", "")501502def Http.home() -> String:503 Http.answer("303 See Other", "Location: /\r\n", "")504505# Serve506# -----507508# the home page for the holder of (user, pass), with a message509def Web.page(s: B.Bank, +user: String, pass: String, time: Nat, err: String) -> String:510 Page.home(B.Bank.seen(s, user, pass), user, time, err)511512# the answer to a request that can fail: on Fail, the page with the513# reason, as the bank was514def Web.done(r: Result<&2, &2, String, Reply>, s: B.Bank, +user: String, pass: String, time: Nat) -> Reply:515 match r:516 case Fail{e}:517 Reply{None{}, Http.answer("400 Bad Request", "", Web.page(s, user, pass, time, e))}518 case Done{reply}:519 reply520521# a change of the bank, answered with see522def Web.change(r: Result<&2, &2, String, B.Bank>, see: String) -> Result<&2, &2, String, Reply>:523 match r:524 case Fail{e}:525 Fail{e}526 case Done{s}:527 Done{Reply{Some{s}, see}}528529# a login: the cookie, if the name and the key can be in one530def Web.login(+name: String, +key: String) -> Result<&2, &2, String, Reply>:531 +ok = Bool.and(Bool.not(String.is_empty(name)), Bool.and(Text.safe(name, 64n), Text.safe(key, 64n)))532 Bool.pick(Result<&2, &2, String, Reply>, ok, Done{Reply{None{}, Http.see(name ++ "-" ++ key)}}, Fail{"a name and a key are letters and digits"})533534def Web.answer(call: Call, +s: B.Bank, +time: Nat, +rand: String, +user: String, +pass: String) -> Reply:535 match call:536 case Home{}:537 Reply{None{}, Http.answer("200 OK", "", Web.page(s, user, pass, time, ""))}538 case Join{+name}:539 +see = Http.see(name ++ "-" ++ rand)540 Web.done(Web.change(B.Bank.join(s, name, rand), see), s, user, pass, time)541 case Auth{name, key}:542 Web.done(Web.login(name, key), s, user, pass, time)543 case Quit{}:544 Reply{None{}, Http.see("")}545 case Exec{cmd}:546 Web.done(Web.change(B.Bank.exec(s, user, pass, time, cmd), Http.home()), s, user, pass, time)547 case Miss{}:548 Reply{None{}, Http.answer("404 Not Found", "", "not found")}549550def Web.reply(+s: B.Bank, req: Req) -> Reply:551 match req:552 case Req{time, rand, verb, path, user, pass, form}:553 Web.answer(Web.call(Web.find(Web.paths(), verb ++ " " ++ path, 0n), form), s, time, rand, user, pass)554555# the bank's change and the answer, for one input from the host556def Web.serve(+s: B.Bank, input: String) -> Reply:557 Web.reply(s, Req.parse(input))