Something went wrong. Try again.
Coding agent with a memory of all things
Something went wrong. Try again.
2.6 kB · 72 lines
at main
12345678910111213141516171819202122232425262728293031323334353637383940414243444546474849505152535455565758596061626364656667686970717273# eukhe: the proof of LAW commit_entry_refuses## PROOF: the entry answers either a request's choice or the one error# form; every choice opens with a tag, a count or a length, never 'E'# (wire_nat_not_err); so an answer that opens with 'E' is the error form.
import Baseimport ../../bend/doc_commit.bend as Cmimport ../../bend/ffi_doc_commit.bend as FCmimport ../../bend/wire.bend as Wrimport ../../laws/doc_commit.bend as DocCommitimport ../../laws/base.bend as LawsBaseimport ../../laws/wire.bend as Wireimport ./base.bend as LAimport ../base/wire_dec.bend as LE
def dcw.ok_check(c: Cm.Check) -> {LawsBase.wire_opens_err(FCm.put_check(c)) == False{} : Bool}: match c: case Cm.Go{}: {==} case Cm.Stop{at, why}: match why: case Cm.Changed{}: {==} case Cm.Taken{}: {==}
def dcw.ok_outcome(o: Cm.Outcome) -> {LawsBase.wire_opens_err(FCm.put_outcome(o)) == False{} : Bool}: match o: case Cm.Lands{w}: {==} case Cm.Fails{}: {==}
def dcw.ok_verdict(v: Cm.Verdict) -> {LawsBase.wire_opens_err(FCm.put_verdict(v)) == False{} : Bool}: match v: case Cm.Failure{}: {==} case Cm.Summary{ns, p}: {==}
# a request's choice is a value, never the error formdef dcw.answer_ok(q: FCm.Req) -> {LawsBase.wire_opens_err(FCm.answer(q)) == False{} : Bool}: match q: case FCm.QCheck{ms}: dcw.ok_check(Cm.check(ms)) case FCm.QPublish{p}: dcw.ok_outcome(Cm.outcome(p)) case FCm.QAnswer{fs}: dcw.ok_verdict(Cm.answer(fs)) case FCm.QGate{b, d}: Wire.wire_nat_not_err(FCm.gate.tag(Cm.gate(b, d)), "") case FCm.QSeen{d, xs}: LE.dcw.fin_ok(Wr.put_list.go(~String, ~Wr.put_str, Cm.seen(d, xs), "")) case FCm.QPrefix{h}: LE.dcw.sfin_ok(Wr.put_str.go(Cm.prefix(h), SNil{}, 0n), "") case FCm.QSweep{h, es}: LE.dcw.fin_ok(Wr.put_list.go(~Nat, ~Wr.put_nat, Cm.gone(h, es), ""))
def dcw.refuse(d: Wr.Dec<FCm.Req>, bad: {LawsBase.wire_opens_err(FCm.ffi.got(d)) == True{} : Bool}) -> {FCm.ffi.got(d) == Wr.err("doc_commit: malformed request") : String}: match d: case Wr.Got{+q, rest}: match rest: case SNil{}: LA.dcw.tf({FCm.answer(q) == Wr.err("doc_commit: malformed request") : String}, Equal.trans(Bool, True{}, LawsBase.wire_opens_err(FCm.answer(q)), False{}, Equal.sym(Bool, LawsBase.wire_opens_err(FCm.answer(q)), True{}, bad), dcw.answer_ok(q))) case SCon{x, y}: {==} case Wr.Bad{}: {==}
def DocCommit.commit_entry_refuses(s, bad): dcw.refuse(FCm.get_req(s), bad)