Something went wrong. Try again.
Coding agent with a memory of all things
Something went wrong. Try again.
1.8 kB · 43 lines
1234567891011121314151617181920212223242526272829303132333435363738394041424344# eukhe: the proof of LAW tiny_elect_entry_refuses## PROOF: the entry answers either a request's choice, a Nat that never# opens with 'E' (wire_nat_not_err), or the one error form; so an answer# that opens with 'E' is that error form.
import Baseimport ../../bend/tiny.bend as Tnimport ../../bend/ffi_tiny_elect.bend as FTeimport ../../bend/wire.bend as Wrimport ../../laws/base.bend as LawsBaseimport ../../laws/tiny.bend as Tinyimport ../../laws/wire.bend as Wireimport ../wire/wire_nat_not_err.bend as PWireNatNotErrimport ./base.bend as LA
# a request's choice is a value, never the error formdef te.answer_ok(q: FTe.Req) -> {LawsBase.wire_opens_err(FTe.answer(q)) == False{} : Bool}: match q: case FTe.QElect{p, m}: Wire.wire_nat_not_err(FTe.act.tag(Tn.elect(p, m)), "") case FTe.QShut{hd}: Wire.wire_nat_not_err(FTe.shut.tag(Tn.shut(hd)), "") case FTe.QLaunched{f, l}: Wire.wire_nat_not_err(FTe.got.tag(Tn.launched(f, l)), "") case FTe.QConfirm{p, m}: Wire.wire_nat_not_err(FTe.check.tag(Tn.confirm(p, m)), "") case FTe.QBind{p}: Wire.wire_nat_not_err(FTe.seat.tag(Tn.bind(p)), "")
def te.refuse(d: Wr.Dec<FTe.Req>, bad: {LawsBase.wire_opens_err(FTe.ffi.got(d)) == True{} : Bool}) -> {FTe.ffi.got(d) == Wr.err("tiny_elect: malformed request") : String}: match d: case Wr.Got{+q, rest}: match rest: case SNil{}: LA.te.tf({FTe.answer(q) == Wr.err("tiny_elect: malformed request") : String}, Equal.trans(Bool, True{}, LawsBase.wire_opens_err(FTe.answer(q)), False{}, Equal.sym(Bool, LawsBase.wire_opens_err(FTe.answer(q)), True{}, bad), te.answer_ok(q))) case SCon{x, y}: {==} case Wr.Bad{}: {==}
def Tiny.tiny_elect_entry_refuses(s, bad): te.refuse(FTe.get_req(s), bad)