Something went wrong. Try again.
Coding agent with a memory of all things
Something went wrong. Try again.
5.3 kB · 107 lines
123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108# eukhe: lemmas of the doc_commit entry proofs: the wire primitives## Each decoder answers Got{x, rest} only for the spelling of x before# rest (dcw.nat, dcw.str: wire_nat_exact, wire_str_exact, and a too long# count refused by wire_nat_too_long); the round trips turned around to# rewrite a decode of a spelling into its value; a count or a length# never opens with 'E'.
import Baseimport ../../../bend/wire.bend as Wrimport ../../../laws/base.bend as LawsBaseimport ../../../laws/wire.bend as Wireimport ../../wire/wire_nat_exact.bend as PWireNatExactimport ../../wire/wire_nat_decoded_fits.bend as PWireNatDecodedFitsimport ../../wire/wire_nat_too_long.bend as PWireNatTooLongimport ../../wire/wire_nat_not_err.bend as PWireNatNotErrimport ../../wire/wire_str_exact.bend as PWireStrExactimport ../../wire/wire_bool_exact.bend as PWireBoolExactimport ../../wire/wire_bool_round_trip.bend as PWireBoolRoundTripimport ../../base/wire.bend as LWireimport ../../base/logic/string.bend as LLogicString
def dcw.DT(-A: Data, d: Wr.Dec<A>, G: Type) -> Type: match d: case Wr.Got{x, r}: Unit case Wr.Bad{}: G
# a decoder answered Got and Baddef dcw.got_bad(-A: Data, -G: Type, -x: A, -r: String, e: {Wr.Got{x, r} == Wr.Bad{} : Wr.Dec<A>}) -> G: %e : dcw.DT(A, _, G) Unit{}
# s is the tag t then s1, and s1 is x: s is the tag t then xdef dcw.after(-s: String, +t: Nat, -s1: String, -x: String, pre: {s == Wr.put_nat(t, s1) : String}, e: {s1 == x : String}) -> {s == Wr.put_nat(t, x) : String}: Equal.trans(String, s, Wr.put_nat(t, s1), Wr.put_nat(t, x), pre, Equal.cong(String, String, z => Wr.put_nat(t, z), s1, x, e))
def dcw.NP(s: String, d: Wr.Dec<Nat>) -> Type: match d: case Wr.Got{n, r}: {s == Wr.put_nat(n, r) : String} case Wr.Bad{}: Unit
def dcw.nat.at(+s: String, d: Wr.Dec<Nat>, ed: {Wr.get_nat(s) == d : Wr.Dec<Nat>}) -> dcw.NP(s, d): match d: case Wr.Got{+n, +r}: Wire.wire_nat_exact(s, n, r, ed) case Wr.Bad{}: Unit{}
# a Nat decoded is spelleddef dcw.nat(+s: String) -> dcw.NP(s, Wr.get_nat(s)): dcw.nat.at(s, Wr.get_nat(s), {==})
# a decoded string's length fits: a longer one's count is refuseddef dcw.str_fits.at(b: Bool, +s: String, +a: String, +r: String, eb: {LawsBase.wire_fits(String.length(a)) == b : Bool}, e1: {s == Wr.put_str(a, r) : String}, ed: {Wr.get_str(s) == Wr.Got{a, r} : Wr.Dec<String>}) -> {LawsBase.wire_fits(String.length(a)) == True{} : Bool}: match b: case True{}: eb case False{}: +x = LLogicString.wr_app(a, r) +c1 = Equal.trans(Wr.Dec<String>, Wr.Got{a, r}, Wr.get_str(s), Wr.get_str(Wr.put_str(a, r)), Equal.sym(Wr.Dec<String>, Wr.get_str(s), Wr.Got{a, r}, ed), Equal.cong(String, Wr.Dec<String>, z => Wr.get_str(z), s, Wr.put_str(a, r), e1)) +c2 = Equal.trans(Wr.Dec<String>, Wr.Got{a, r}, Wr.get_str(Wr.put_str(a, r)), Wr.get_str(Wr.put_nat(String.length(a), x)), c1, Equal.cong(String, Wr.Dec<String>, z => Wr.get_str(z), Wr.put_str(a, r), Wr.put_nat(String.length(a), x), LWire.wr_put_str(a, r))) +c3 = Equal.trans(Wr.Dec<String>, Wr.Got{a, r}, Wr.get_str(Wr.put_nat(String.length(a), x)), Wr.Bad{}, c2, Equal.cong(Wr.Dec<Nat>, Wr.Dec<String>, z => Wr.get_str.go(z), Wr.get_nat(Wr.put_nat(String.length(a), x)), Wr.Bad{}, Wire.wire_nat_too_long(String.length(a), x, eb))) dcw.got_bad(String, {LawsBase.wire_fits(String.length(a)) == True{} : Bool}, a, r, c3)
def dcw.SP(s: String, d: Wr.Dec<String>) -> Type: match d: case Wr.Got{a, r}: {s == Wr.put_str(a, r) : String} & {LawsBase.wire_fits(String.length(a)) == True{} : Bool} case Wr.Bad{}: Unit
def dcw.str.at(+s: String, d: Wr.Dec<String>, ed: {Wr.get_str(s) == d : Wr.Dec<String>}) -> dcw.SP(s, d): match d: case Wr.Got{+a, +r}: +e2 = ed +e1 = Wire.wire_str_exact(s, a, r, e2) (e1, dcw.str_fits.at(LawsBase.wire_fits(String.length(a)), s, a, r, {==}, e1, e2)) case Wr.Bad{}: Unit{}
# a string decoded is spelled, and its length fitsdef dcw.str(+s: String) -> dcw.SP(s, Wr.get_str(s)): dcw.str.at(s, Wr.get_str(s), {==})
# a string that fits reads back (wire_str_round_trip, turned around)def dcw.str_back(+a: String, +rest: String, h: {LawsBase.wire_fits(String.length(a)) == True{} : Bool}) -> {Wr.Got{a, rest} == Wr.get_str(Wr.put_str(a, rest)) : Wr.Dec<String>}: Equal.sym(Wr.Dec<String>, Wr.get_str(Wr.put_str(a, rest)), Wr.Got{a, rest}, Wire.wire_str_round_trip(a, rest, h))
# a Bool reads back (wire_bool_round_trip, turned around)def dcw.bool_back(+b: Bool, +rest: String) -> {Wr.Got{b, rest} == Wr.get_bool(Wr.put_bool(b, rest)) : Wr.Dec<Bool>}: Equal.sym(Wr.Dec<Bool>, Wr.get_bool(Wr.put_bool(b, rest)), Wr.Got{b, rest}, Wire.wire_bool_round_trip(b, rest))
# a list's spelling opens with its count: never 'E'def dcw.fin_ok(p: Nat & String) -> {LawsBase.wire_opens_err(Wr.put_list.fin(p)) == False{} : Bool}: match p: case (n, s): Wire.wire_nat_not_err(n, s)
# a string's spelling opens with its length: never 'E'def dcw.sfin_ok(p: Nat & String, rest: String) -> {LawsBase.wire_opens_err(Wr.put_str.fin(p, rest)) == False{} : Bool}: match p: case (n, b): Wire.wire_nat_not_err(n, String.reverse.go(b, rest))