Something went wrong. Try again.
Coding agent with a memory of all things
Something went wrong. Try again.
9.3 kB · 216 lines
123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217# eukhe: lemmas the proofs of area shell share
import Baseimport ../../bend/ffi_shell.bend as FShimport ../../bend/tools.bend as Tlimport ../../bend/wire.bend as Wrimport ../../bend/wire_flat.bend as Flimport ../../laws/base.bend as LawsBaseimport ../../laws/shell.bend as Shellimport ../../laws/wire.bend as Wireimport ../base/logic/bool.bend as LLogicBoolimport ../base/wire.bend as LWire
# The entry reads every input as the laws' reader does# -----------------------------------------------------
def sh.part(xs: List<&2, Nat>) -> {Shell.read_part(xs) == FSh.part.of(xs) : Maybe<&2, Tl.Part>}: match xs: case Nil{}: {==} case f <> o: match f: case 0n: {==} case 1n+g: match g: case 0n: {==} case 1n+h: {==}
def sh.cons(m: Maybe<&2, Tl.Part>, ms: Maybe<&2, List<&2, Tl.Part>>) -> {Shell.read_parts.cons(m, ms) == FSh.parts.cons(m, ms) : Maybe<&2, List<&2, Tl.Part>>}: match m: case None{}: {==} case Some{p}: match ms: case None{}: {==} case Some{ps}: {==}
def sh.parts(xss: List<&2, List<&2, Nat>>) -> {Shell.read_parts(xss) == FSh.parts.of(xss) : Maybe<&2, List<&2, Tl.Part>>}: match xss: case Nil{}: {==} case +xs <> +rest: %sh.part(xs) : {Shell.read_parts.cons(Shell.read_part(xs), Shell.read_parts(rest)) == FSh.parts.cons(_, FSh.parts.of(rest)) : Maybe<&2, List<&2, Tl.Part>>} %sh.parts(rest) : {Shell.read_parts.cons(Shell.read_part(xs), Shell.read_parts(rest)) == FSh.parts.cons(Shell.read_part(xs), _) : Maybe<&2, List<&2, Tl.Part>>} sh.cons(Shell.read_part(xs), Shell.read_parts(rest))
def sh.flat(m: Maybe<&2, List<&2, List<&2, Nat>>>) -> {Shell.read_parts.flat(m) == FSh.parts.flat(m) : Maybe<&2, List<&2, Tl.Part>>}: match m: case None{}: {==} case Some{xss}: sh.parts(xss)
def sh.step_parts(a: List<&2, Nat>, m: Maybe<&2, List<&2, Tl.Part>>, s: String) -> {Shell.read_step.parts(a, m, s) == FSh.get_step.parts(a, m, s) : Wr.Dec<FSh.Req>}: match m: case None{}: {==} case Some{ps}: {==}
def sh.step_flat(+a: List<&2, Nat>, r: Wr.Dec<List<&2, Nat>>) -> {Shell.read_step.flat(a, r) == FSh.get_step.flat(a, r) : Wr.Dec<FSh.Req>}: match r: case Wr.Got{+ns, +s}: %sh.flat(Fl.unflat(ns)) : {Shell.read_step.parts(a, Shell.read_parts.flat(Fl.unflat(ns)), s) == FSh.get_step.parts(a, _, s) : Wr.Dec<FSh.Req>} sh.step_parts(a, Shell.read_parts.flat(Fl.unflat(ns)), s) case Wr.Bad{}: {==}
def sh.step(r: Wr.Dec<List<&2, Nat>>) -> {Shell.read_step(r) == FSh.get_step(r) : Wr.Dec<FSh.Req>}: match r: case Wr.Got{a, s}: sh.step_flat(a, Wr.get_list(~Nat, ~Wr.get_nat, s)) case Wr.Bad{}: {==}
def sh.allows_effs(a: List<&2, Nat>, r: Wr.Dec<List<&2, Nat>>) -> {Shell.read_allows.effs(a, r) == FSh.get_allows.effs(a, r) : Wr.Dec<FSh.Req>}: match r: case Wr.Got{es, s}: {==} case Wr.Bad{}: {==}
def sh.allows(r: Wr.Dec<List<&2, Nat>>) -> {Shell.read_allows(r) == FSh.get_allows(r) : Wr.Dec<FSh.Req>}: match r: case Wr.Got{a, s}: sh.allows_effs(a, Wr.get_list(~Nat, ~Wr.get_nat, s)) case Wr.Bad{}: {==}
def sh.answer_yes(i: Nat, r: Wr.Dec<Bool>) -> {Shell.read_answer.yes(i, r) == FSh.get_answer.yes(i, r) : Wr.Dec<FSh.Req>}: match r: case Wr.Got{y, s}: {==} case Wr.Bad{}: {==}
def sh.answer(r: Wr.Dec<Nat>) -> {Shell.read_answer(r) == FSh.get_answer(r) : Wr.Dec<FSh.Req>}: match r: case Wr.Got{i, s}: sh.answer_yes(i, Wr.get_bool(s)) case Wr.Bad{}: {==}
def sh.tag(t: Nat, s: String) -> {Shell.read_req.tag(t, s) == FSh.get_req.tag(t, s) : Wr.Dec<FSh.Req>}: match t: case 0n: sh.step(Wr.get_list(~Nat, ~Wr.get_nat, s)) case 1n: sh.allows(Wr.get_list(~Nat, ~Wr.get_nat, s)) case 2n: sh.answer(Wr.get_nat(s)) case 3n+u: {==}
def sh.go(r: Wr.Dec<Nat>) -> {Shell.read_req.go(r) == FSh.get_req.go(r) : Wr.Dec<FSh.Req>}: match r: case Wr.Got{t, s}: sh.tag(t, s) case Wr.Bad{}: {==}
def sh.req(s: String) -> {Shell.read_req(s) == FSh.get_req(s) : Wr.Dec<FSh.Req>}: sh.go(Wr.get_nat(s))
# The entry answers as the laws spell the model's decision# --------------------------------------------------------
def sh.reply(q: FSh.Req) -> {FSh.answer(q) == Shell.spell_answer(q) : String}: match q: case FSh.QStep{a, ps}: {==} case FSh.QAllows{a, es}: {==} case FSh.QAnswer{i, y}: match y: case True{}: {==} case False{}: {==}
def sh.end(b: Bool, q: FSh.Req) -> {FSh.run.end(b, q) == Shell.spec.end(b, q) : String}: match b: case True{}: sh.reply(q) case False{}: {==}
def sh.run(r: Wr.Dec<FSh.Req>) -> {FSh.run(r) == Shell.spec.run(r) : String}: match r: case Wr.Got{q, s}: sh.end(Wr.end(s), q) case Wr.Bad{}: {==}
def sh.exact(+s: String) -> {FSh.ffi(s) == Shell.spec(s) : String}: %sh.req(s) : {FSh.run(_) == Shell.spec(s) : String} sh.run(Shell.read_req(s))
# The reader reads back what Rust writes# --------------------------------------
def sh.parts_rt(ps: List<&2, Tl.Part>) -> {Shell.read_parts(Shell.spell_parts(ps)) == Some{ps} : Maybe<&2, List<&2, Tl.Part>>}: match ps: case Nil{}: {==} case p <> t: match p: case Tl.Part{o, s}: match s: case True{}: %Equal.sym(Maybe<&2, List<&2, Tl.Part>>, Shell.read_parts(Shell.spell_parts(t)), Some{t}, sh.parts_rt(t)) : {Shell.read_parts.cons(Some{Tl.Part{o, True{}}}, _) == Some{Tl.Part{o, True{}} <> t} : Maybe<&2, List<&2, Tl.Part>>} {==} case False{}: %Equal.sym(Maybe<&2, List<&2, Tl.Part>>, Shell.read_parts(Shell.spell_parts(t)), Some{t}, sh.parts_rt(t)) : {Shell.read_parts.cons(Some{Tl.Part{o, False{}}}, _) == Some{Tl.Part{o, False{}} <> t} : Maybe<&2, List<&2, Tl.Part>>} {==}
def sh.rt_step(+a: List<&2, Nat>, +ps: List<&2, Tl.Part>, +rest: String, +fits: {Shell.req_fits(FSh.QStep{a, ps}) == True{} : Bool}) -> {Shell.read_req(Shell.spell_req(FSh.QStep{a, ps}, rest)) == Wr.Got{FSh.QStep{a, ps}, rest} : Wr.Dec<FSh.Req>}: +sp = Shell.spell_parts(ps) +f = Fl.flat(sp) +ha = LLogicBool.wr_and_l(Shell.ns_fit(a), Shell.ns_fit(f), fits) +hf = LLogicBool.wr_and_r(Shell.ns_fit(a), Shell.ns_fit(f), fits) %Equal.sym(Wr.Dec<List<&2, Nat>>, Wr.get_list(~Nat, ~Wr.get_nat, Shell.spell_ns(a, Shell.spell_ns(f, rest))), Wr.Got{a, Shell.spell_ns(f, rest)}, Wire.wire_list_round_trip(a, Shell.spell_ns(f, rest), ha)) : {Shell.read_step(_) == Wr.Got{FSh.QStep{a, ps}, rest} : Wr.Dec<FSh.Req>} %Equal.sym(Wr.Dec<List<&2, Nat>>, Wr.get_list(~Nat, ~Wr.get_nat, Shell.spell_ns(f, rest)), Wr.Got{f, rest}, Wire.wire_list_round_trip(f, rest, hf)) : {Shell.read_step.flat(a, _) == Wr.Got{FSh.QStep{a, ps}, rest} : Wr.Dec<FSh.Req>} %Equal.sym(Maybe<&2, List<&2, List<&2, Nat>>>, Fl.unflat(f), Some{sp}, LWire.fe.unflat_flat(sp)) : {Shell.read_step.parts(a, Shell.read_parts.flat(_), rest) == Wr.Got{FSh.QStep{a, ps}, rest} : Wr.Dec<FSh.Req>} %Equal.sym(Maybe<&2, List<&2, Tl.Part>>, Shell.read_parts(sp), Some{ps}, sh.parts_rt(ps)) : {Shell.read_step.parts(a, _, rest) == Wr.Got{FSh.QStep{a, ps}, rest} : Wr.Dec<FSh.Req>} {==}
def sh.rt_allows(+a: List<&2, Nat>, +es: List<&2, Nat>, +rest: String, +fits: {Shell.req_fits(FSh.QAllows{a, es}) == True{} : Bool}) -> {Shell.read_req(Shell.spell_req(FSh.QAllows{a, es}, rest)) == Wr.Got{FSh.QAllows{a, es}, rest} : Wr.Dec<FSh.Req>}: +ha = LLogicBool.wr_and_l(Shell.ns_fit(a), Shell.ns_fit(es), fits) +he = LLogicBool.wr_and_r(Shell.ns_fit(a), Shell.ns_fit(es), fits) %Equal.sym(Wr.Dec<List<&2, Nat>>, Wr.get_list(~Nat, ~Wr.get_nat, Shell.spell_ns(a, Shell.spell_ns(es, rest))), Wr.Got{a, Shell.spell_ns(es, rest)}, Wire.wire_list_round_trip(a, Shell.spell_ns(es, rest), ha)) : {Shell.read_allows(_) == Wr.Got{FSh.QAllows{a, es}, rest} : Wr.Dec<FSh.Req>} %Equal.sym(Wr.Dec<List<&2, Nat>>, Wr.get_list(~Nat, ~Wr.get_nat, Shell.spell_ns(es, rest)), Wr.Got{es, rest}, Wire.wire_list_round_trip(es, rest, he)) : {Shell.read_allows.effs(a, _) == Wr.Got{FSh.QAllows{a, es}, rest} : Wr.Dec<FSh.Req>} {==}
def sh.rt_answer(+i: Nat, y: Bool, +rest: String, fits: {Shell.req_fits(FSh.QAnswer{i, y}) == True{} : Bool}) -> {Shell.read_req(Shell.spell_req(FSh.QAnswer{i, y}, rest)) == Wr.Got{FSh.QAnswer{i, y}, rest} : Wr.Dec<FSh.Req>}: match y: case True{}: %LWire.pw6.nat(i, Wr.put_bool(True{}, rest), fits) : {Shell.read_answer(_) == Wr.Got{FSh.QAnswer{i, True{}}, rest} : Wr.Dec<FSh.Req>} {==} case False{}: %LWire.pw6.nat(i, Wr.put_bool(False{}, rest), fits) : {Shell.read_answer(_) == Wr.Got{FSh.QAnswer{i, False{}}, rest} : Wr.Dec<FSh.Req>} {==}
def sh.rt(q: FSh.Req, +rest: String, fits: {Shell.req_fits(q) == True{} : Bool}) -> {Shell.read_req(Shell.spell_req(q, rest)) == Wr.Got{q, rest} : Wr.Dec<FSh.Req>}: match q: case FSh.QStep{a, ps}: sh.rt_step(a, ps, rest, fits) case FSh.QAllows{a, es}: sh.rt_allows(a, es, rest, fits) case FSh.QAnswer{i, y}: sh.rt_answer(i, y, rest, fits)