Something went wrong. Try again.
Coding agent with a memory of all things
Something went wrong. Try again.
1.5 kB · 51 lines
at bend/all
12345678910111213141516171819202122232425262728293031323334353637383940414243444546474849505152# eukhe: the proof of LAW commit_gate_spec## PROOF: membership by the code's char-by-char comparison is the spec's# (dcw.same); the rest computes.
import Baseimport ../../bend/doc_commit.bend as Cmimport ../../laws/doc_commit.bend as DocCommitimport ./base.bend as LA
def dcw.member(+d: String, s: List<&2, String>) -> {Cm.member(d, s) == DocCommit.sp_in(d, s) : Bool}: match s: case Nil{}: {==} case +x <> rest: %LA.dcw.same(x, d) : {Cm.member(d, x <> rest) == Bool.or(_, DocCommit.sp_in(d, rest)) : Bool} %dcw.member(d, rest) : {Cm.member(d, x <> rest) == Bool.or(Cm.same(x, d), _) : Bool} {==}
def dcw.seen(b: Bool) -> {Cm.gate.seen(b) == DocCommit.sp_if(b, Cm.Proceed{}, Cm.Unseen{}) : Cm.Gate}: match b: case True{}: {==} case False{}: {==}
def dcw.bytes(b: Bool) -> {Cm.gate.bytes(b) == DocCommit.sp_if(b, Cm.Proceed{}, Cm.Stale{}) : Cm.Gate}: match b: case True{}: {==} case False{}: {==}
def dcw.gate(b: Cm.Base, d: Cm.Disk) -> {Cm.gate(b, d) == DocCommit.sp_gate(b, d) : Cm.Gate}: match b: case Cm.OnSeen{+s}: match d: case Cm.Absent{}: {==} case Cm.Present{+g, e}: %dcw.member(g, s) : {Cm.gate.seen(Cm.member(g, s)) == DocCommit.sp_if(_, Cm.Proceed{}, Cm.Unseen{}) : Cm.Gate} dcw.seen(Cm.member(g, s)) case Cm.OnBytes{}: match d: case Cm.Absent{}: {==} case Cm.Present{g, e}: dcw.bytes(e)
def DocCommit.commit_gate_spec(b, d): dcw.gate(b, d)