proof/atomicity.bend · raw · all files

1# Bend Bank: the proof of LAW atomicity2# =====================================3#4# Only Join and Exec can change the bank, both through Web.change, which5# answers a change with a 303 redirect. Every other answer, and every6# failure, changes nothing.78import Base9import ../bank.bend as B10import ../web.bend as W11import ../LAWS.bend as Laws12import ./base.bend as L1314# Atomicity15# ---------1617# the start of a 303 answer18def Web.prefix() -> String:19  "HTTP/1.1 303 See Other\r\n"2021# a change answers 303 See Other22def Web.Atomic(m: Maybe<&2, B.Bank>, text: String) -> Type:23  match m:24    case None{}:25      Unit26    case Some{b}:27      {String.starts_with(text, Web.prefix()) == True{} : Bool}2829# a reply that does not fail is Atomic30def Web.Done(r: Result<&2, &2, String, W.Reply>) -> Type:31  match r:32    case Fail{e}:33      Unit34    case Done{+reply}:35      Web.Atomic(Laws.change(reply), Laws.text(reply))3637# a change answered with a 303 is Atomic38def Web.change_303(r: Result<&2, &2, String, B.Bank>, -see: String, h: {String.starts_with(see, Web.prefix()) == True{} : Bool})39  -> Web.Done(W.Web.change(r, see)):40  match r:41    case Fail{e}:42      Unit{}43    case Done{s}:44      h4546# a failure answers the page, and changes nothing47def Web.done_303(r: Result<&2, &2, String, W.Reply>, -s: B.Bank, -user: String, -pass: String, -time: Nat, h: Web.Done(r))48  -> Web.Atomic(Laws.change(W.Web.done(r, s, user, pass, time)), Laws.text(W.Web.done(r, s, user, pass, time))):49  match r:50    case Fail{e}:51      Unit{}52    case Done{reply}:53      h5455# every answer that changes the bank is a 30356def Web.answer_303(call: W.Call, +s: B.Bank, +time: Nat, +rand: String, +user: String, +pass: String)57  -> Web.Atomic(Laws.change(W.Web.answer(call, s, time, rand, user, pass)), Laws.text(W.Web.answer(call, s, time, rand, user, pass))):58  match call:59    case W.Home{}:60      Unit{}61    case W.Join{+name}:62      +see = W.Http.see(name ++ "-" ++ rand)63      +r = B.Bank.join(s, name, rand)64      Web.done_303(W.Web.change(r, see), s, user, pass, time, Web.change_303(r, see, {==}))65    case W.Auth{+name, +key}:66      +d = W.Web.done(W.Web.login(name, key), s, user, pass, time)67      %L.Web.login_none(name, key, s, user, pass, time) : Web.Atomic(Laws.change(_), Laws.text(d))68      Unit{}69    case W.Quit{}:70      Unit{}71    case W.Exec{+cmd}:72      +r = B.Bank.exec(s, user, pass, time, cmd)73      Web.done_303(W.Web.change(r, W.Http.home()), s, user, pass, time, Web.change_303(r, W.Http.home(), {==}))74    case W.Miss{}:75      Unit{}7677# every reply that changes the bank is a 30378def Web.reply_303(+s: B.Bank, req: W.Req) -> Web.Atomic(Laws.change(W.Web.reply(s, req)), Laws.text(W.Web.reply(s, req))):79  match req:80    case W.Req{time, rand, verb, path, user, pass, form}:81      Web.answer_303(W.Web.call(W.Web.find(W.Web.paths(), verb ++ " " ++ path, 0n), form), s, time, rand, user, pass)8283# LAW atomicity84def Laws.atomicity(s, input, b, e):85  %e : Web.Atomic(_, Laws.text(W.Web.serve(s, input)))86  Web.reply_303(s, W.Req.parse(input))