Something went wrong. Try again.
Coding agent with a memory of all things
Something went wrong. Try again.
11 kB · 267 lines
at main
123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241242243244245246247248249250251252253254255256257258259260261262263264265266267268# eukhe: lemmas of the doc_commit entry proofs: the fields of a request## A spelled Pub, Base and Disk reads back (dcw.rd_*), and each decoder of# bend/ffi_doc_commit.bend answers Got only for the spec's spelling, with# what it holds within the wire (dcw.pub, dcw.base, dcw.disk).
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 LEimport ../../base/wire_strs.bend as LS
# Read back# ---------
def dcw.rd_pub(p: Cm.Pub, +rest: String) -> {FCm.get_pub(Wr.get_nat(DocCommit.sp_w_pub(p, rest))) == Wr.Got{p, rest} : Wr.Dec<Cm.Pub>}: match p: case Cm.Updated{x}: match x: case Cm.NotPlaced{}: {==} case Cm.Placed{s}: match s: case True{}: {==} case False{}: {==} case Cm.Deleted{r}: match r: case True{}: {==} case False{}: {==} case Cm.Moved{x, r}: match x: case Cm.NotPlaced{}: match r: case True{}: {==} case False{}: {==} case Cm.Placed{s}: match s: case True{}: match r: case True{}: {==} case False{}: {==} case False{}: match r: case True{}: {==} case False{}: {==}
def dcw.rd_pub_back(+p: Cm.Pub, +rest: String) -> {Wr.Got{p, rest} == FCm.get_pub(Wr.get_nat(DocCommit.sp_w_pub(p, rest))) : Wr.Dec<Cm.Pub>}: Equal.sym(Wr.Dec<Cm.Pub>, FCm.get_pub(Wr.get_nat(DocCommit.sp_w_pub(p, rest))), Wr.Got{p, rest}, dcw.rd_pub(p, rest))
def dcw.rd_base(b: Cm.Base, +rest: String, h: {DocCommit.sp_fit_base(b) == True{} : Bool}) -> {FCm.get_base(Wr.get_nat(DocCommit.sp_w_base(b, rest))) == Wr.Got{b, rest} : Wr.Dec<Cm.Base>}: match b: case Cm.OnSeen{+xs}: +hh = h %LS.dcw.strs.back(xs, rest, LA.dcw.and_l(LawsBase.wire_fits(List.length(&2, String, xs)), DocCommit.sp_fit_strs(xs), hh), LA.dcw.and_r(LawsBase.wire_fits(List.length(&2, String, xs)), DocCommit.sp_fit_strs(xs), hh)) : {FCm.get_base.seen(_) == Wr.Got{Cm.OnSeen{xs}, rest} : Wr.Dec<Cm.Base>} {==} case Cm.OnBytes{}: {==}
def dcw.rd_base_back(+b: Cm.Base, +rest: String, h: {DocCommit.sp_fit_base(b) == True{} : Bool}) -> {Wr.Got{b, rest} == FCm.get_base(Wr.get_nat(DocCommit.sp_w_base(b, rest))) : Wr.Dec<Cm.Base>}: Equal.sym(Wr.Dec<Cm.Base>, FCm.get_base(Wr.get_nat(DocCommit.sp_w_base(b, rest))), Wr.Got{b, rest}, dcw.rd_base(b, rest, h))
def dcw.rd_disk(d: Cm.Disk, +rest: String, h: {DocCommit.sp_fit_disk(d) == True{} : Bool}) -> {FCm.get_disk(Wr.get_nat(DocCommit.sp_w_disk(d, rest))) == Wr.Got{d, rest} : Wr.Dec<Cm.Disk>}: match d: case Cm.Absent{}: {==} case Cm.Present{+g, +e}: %LE.dcw.str_back(g, Wr.put_bool(e, rest), h) : {FCm.get_disk.digest(_) == Wr.Got{Cm.Present{g, e}, rest} : Wr.Dec<Cm.Disk>} %LE.dcw.bool_back(e, rest) : {FCm.get_disk.expected(g, _) == Wr.Got{Cm.Present{g, e}, rest} : Wr.Dec<Cm.Disk>} {==}
def dcw.rd_disk_back(+d: Cm.Disk, +rest: String, h: {DocCommit.sp_fit_disk(d) == True{} : Bool}) -> {Wr.Got{d, rest} == FCm.get_disk(Wr.get_nat(DocCommit.sp_w_disk(d, rest))) : Wr.Dec<Cm.Disk>}: Equal.sym(Wr.Dec<Cm.Disk>, FCm.get_disk(Wr.get_nat(DocCommit.sp_w_disk(d, rest))), Wr.Got{d, rest}, dcw.rd_disk(d, rest, h))
# Placed# ------
def dcw.PlP(s: String, d: Wr.Dec<Cm.Placed>) -> Type: match d: case Wr.Got{x, r}: {s == DocCommit.sp_w_placed(x, r) : String} case Wr.Bad{}: Unit
def dcw.placed.synced(-s: String, +s1: String, pre: {s == Wr.put_nat(1n, s1) : String}, d: Wr.Dec<Bool>, ed: {Wr.get_bool(s1) == d : Wr.Dec<Bool>}) -> dcw.PlP(s, FCm.get_placed.synced(d)): match d: case Wr.Got{+b, +s2}: LE.dcw.after(s, 1n, s1, Wr.put_bool(b, s2), pre, Wire.wire_bool_exact(s1, b, s2, ed)) case Wr.Bad{}: Unit{}
def dcw.placed.tag(t: Nat, +s1: String, -s: String, pre: {s == Wr.put_nat(t, s1) : String}) -> dcw.PlP(s, FCm.get_placed.tag(t, s1)): match t: case 0n: pre case 1n: dcw.placed.synced(s, s1, pre, Wr.get_bool(s1), {==}) case 2n+u: Unit{}
def dcw.placed.go(-s: String, d: Wr.Dec<Nat>, np: LE.dcw.NP(s, d)) -> dcw.PlP(s, FCm.get_placed(d)): match d: case Wr.Got{t, s1}: dcw.placed.tag(t, s1, s, np) case Wr.Bad{}: Unit{}
def dcw.placed(+s: String) -> dcw.PlP(s, FCm.get_placed(Wr.get_nat(s))): dcw.placed.go(s, Wr.get_nat(s), LE.dcw.nat(s))
# Pub# ---
def dcw.PbP(s: String, d: Wr.Dec<Cm.Pub>) -> Type: match d: case Wr.Got{p, r}: {s == DocCommit.sp_w_pub(p, r) : String} case Wr.Bad{}: Unit
def dcw.pub.updated(-s: String, -s1: String, pre: {s == Wr.put_nat(0n, s1) : String}, d: Wr.Dec<Cm.Placed>, pp: dcw.PlP(s1, d)) -> dcw.PbP(s, FCm.get_pub.updated(d)): match d: case Wr.Got{+x, +r}: LE.dcw.after(s, 0n, s1, DocCommit.sp_w_placed(x, r), pre, pp) case Wr.Bad{}: Unit{}
def dcw.pub.deleted(-s: String, +s1: String, pre: {s == Wr.put_nat(1n, s1) : String}, d: Wr.Dec<Bool>, ed: {Wr.get_bool(s1) == d : Wr.Dec<Bool>}) -> dcw.PbP(s, FCm.get_pub.deleted(d)): match d: case Wr.Got{+b, +r}: LE.dcw.after(s, 1n, s1, Wr.put_bool(b, r), pre, Wire.wire_bool_exact(s1, b, r, ed)) case Wr.Bad{}: Unit{}
def dcw.pub.removed(-s: String, +x: Cm.Placed, +s2: String, pre: {s == Wr.put_nat(2n, DocCommit.sp_w_placed(x, s2)) : String}, d: Wr.Dec<Bool>, ed: {Wr.get_bool(s2) == d : Wr.Dec<Bool>}) -> dcw.PbP(s, FCm.get_pub.removed(x, d)): match d: case Wr.Got{+b, +r}: Equal.trans(String, s, Wr.put_nat(2n, DocCommit.sp_w_placed(x, s2)), Wr.put_nat(2n, DocCommit.sp_w_placed(x, Wr.put_bool(b, r))), pre, Equal.cong(String, String, z => Wr.put_nat(2n, DocCommit.sp_w_placed(x, z)), s2, Wr.put_bool(b, r), Wire.wire_bool_exact(s2, b, r, ed))) case Wr.Bad{}: Unit{}
def dcw.pub.moved(-s: String, -s1: String, pre: {s == Wr.put_nat(2n, s1) : String}, d: Wr.Dec<Cm.Placed>, pp: dcw.PlP(s1, d)) -> dcw.PbP(s, FCm.get_pub.moved(d)): match d: case Wr.Got{+x, +s2}: dcw.pub.removed(s, x, s2, LE.dcw.after(s, 2n, s1, DocCommit.sp_w_placed(x, s2), pre, pp), Wr.get_bool(s2), {==}) case Wr.Bad{}: Unit{}
def dcw.pub.tag(t: Nat, +s1: String, -s: String, pre: {s == Wr.put_nat(t, s1) : String}) -> dcw.PbP(s, FCm.get_pub.tag(t, s1)): match t: case 0n: dcw.pub.updated(s, s1, pre, FCm.get_placed(Wr.get_nat(s1)), dcw.placed(s1)) case 1n: dcw.pub.deleted(s, s1, pre, Wr.get_bool(s1), {==}) case 2n: dcw.pub.moved(s, s1, pre, FCm.get_placed(Wr.get_nat(s1)), dcw.placed(s1)) case 3n+u: Unit{}
def dcw.pub.go(-s: String, d: Wr.Dec<Nat>, np: LE.dcw.NP(s, d)) -> dcw.PbP(s, FCm.get_pub(d)): match d: case Wr.Got{t, s1}: dcw.pub.tag(t, s1, s, np) case Wr.Bad{}: Unit{}
# a Pub decoded is spelleddef dcw.pub(+s: String) -> dcw.PbP(s, FCm.get_pub(Wr.get_nat(s))): dcw.pub.go(s, Wr.get_nat(s), LE.dcw.nat(s))
# Base# ----
def dcw.BP(s: String, d: Wr.Dec<Cm.Base>) -> Type: match d: case Wr.Got{b, r}: {s == DocCommit.sp_w_base(b, r) : String} & {DocCommit.sp_fit_base(b) == True{} : Bool} case Wr.Bad{}: Unit
def dcw.base.seen(-s: String, -s1: String, pre: {s == Wr.put_nat(0n, s1) : String}, d: Wr.Dec<List<&2, String>>, ls: LS.dcw.strs.LS(s1, d)) -> dcw.BP(s, FCm.get_base.seen(d)): match d: case Wr.Got{+xs, +r}: (e, fg) = ls (f, g) = fg (LE.dcw.after(s, 0n, s1, Wr.put_list(~String, ~Wr.put_str, xs, r), pre, e), LA.dcw.and_tt(LawsBase.wire_fits(List.length(&2, String, xs)), DocCommit.sp_fit_strs(xs), f, g)) case Wr.Bad{}: Unit{}
def dcw.base.tag(t: Nat, +s1: String, -s: String, pre: {s == Wr.put_nat(t, s1) : String}) -> dcw.BP(s, FCm.get_base.tag(t, s1)): match t: case 0n: dcw.base.seen(s, s1, pre, FCm.get_strs(s1), LS.dcw.strs.list(s1)) case 1n: (pre, {==}) case 2n+u: Unit{}
def dcw.base.go(-s: String, d: Wr.Dec<Nat>, np: LE.dcw.NP(s, d)) -> dcw.BP(s, FCm.get_base(d)): match d: case Wr.Got{t, s1}: dcw.base.tag(t, s1, s, np) case Wr.Bad{}: Unit{}
# a Base decoded is spelled, and fitsdef dcw.base(+s: String) -> dcw.BP(s, FCm.get_base(Wr.get_nat(s))): dcw.base.go(s, Wr.get_nat(s), LE.dcw.nat(s))
# Disk# ----
def dcw.DP(s: String, d: Wr.Dec<Cm.Disk>) -> Type: match d: case Wr.Got{x, r}: {s == DocCommit.sp_w_disk(x, r) : String} & {DocCommit.sp_fit_disk(x) == True{} : Bool} case Wr.Bad{}: Unit
def dcw.disk.expected(-s: String, +g: String, +s2: String, pre: {s == Wr.put_nat(1n, Wr.put_str(g, s2)) : String}, fg: {LawsBase.wire_fits(String.length(g)) == True{} : Bool}, d: Wr.Dec<Bool>, ed: {Wr.get_bool(s2) == d : Wr.Dec<Bool>}) -> dcw.DP(s, FCm.get_disk.expected(g, d)): match d: case Wr.Got{+e, +s3}: (Equal.trans(String, s, Wr.put_nat(1n, Wr.put_str(g, s2)), Wr.put_nat(1n, Wr.put_str(g, Wr.put_bool(e, s3))), pre, Equal.cong(String, String, z => Wr.put_nat(1n, Wr.put_str(g, z)), s2, Wr.put_bool(e, s3), Wire.wire_bool_exact(s2, e, s3, ed))), fg) case Wr.Bad{}: Unit{}
def dcw.disk.digest(-s: String, -s1: String, pre: {s == Wr.put_nat(1n, s1) : String}, d: Wr.Dec<String>, sp: LE.dcw.SP(s1, d)) -> dcw.DP(s, FCm.get_disk.digest(d)): match d: case Wr.Got{+g, +s2}: (e, f) = sp dcw.disk.expected(s, g, s2, LE.dcw.after(s, 1n, s1, Wr.put_str(g, s2), pre, e), f, Wr.get_bool(s2), {==}) case Wr.Bad{}: Unit{}
def dcw.disk.tag(t: Nat, +s1: String, -s: String, pre: {s == Wr.put_nat(t, s1) : String}) -> dcw.DP(s, FCm.get_disk.tag(t, s1)): match t: case 0n: (pre, {==}) case 1n: dcw.disk.digest(s, s1, pre, Wr.get_str(s1), LE.dcw.str(s1)) case 2n+u: Unit{}
def dcw.disk.go(-s: String, d: Wr.Dec<Nat>, np: LE.dcw.NP(s, d)) -> dcw.DP(s, FCm.get_disk(d)): match d: case Wr.Got{t, s1}: dcw.disk.tag(t, s1, s, np) case Wr.Bad{}: Unit{}
# a Disk decoded is spelled, and fitsdef dcw.disk(+s: String) -> dcw.DP(s, FCm.get_disk(Wr.get_nat(s))): dcw.disk.go(s, Wr.get_nat(s), LE.dcw.nat(s))