Something went wrong. Try again.
Coding agent with a memory of all things
Something went wrong. Try again.
1.9 kB · 35 lines
123456789101112131415161718192021222324252627282930313233343536# eukhe: the proof of LAW command_ffi_unknown_query## PROOF of LAW command_ffi_unknown_query: after a table that reads back# (cfr_table_rt), the question tag 3 + n reads as itself when it fits# and as Bad when too long (ws_nat_read); both ways the question is Bad,# so the request is malformed.
import Baseimport ../../bend/command.bend as Cmdimport ../../bend/ffi_command.bend as FCmdimport ../../bend/wire.bend as Wrimport ../../laws/base.bend as LawsBaseimport ../../laws/wire.bend as Wireimport ../../laws/command/entry.bend as Commandimport ../wire/base/spell.bend as LAWireSpellimport ./base/entry.bend as LACommandEntryimport ../base/logic/bool.bend as LLogicBoolimport ../base/wire.bend as LWireimport ./command_ffi_round_trip.bend as PCommandFfiRoundTrip
def cuq_bad(b: Bool, -n: Nat, -rest: String) -> {FCmd.get_query.go(LAWireSpell.ws_nat_answer(b, 3n+n, rest)) == Wr.Bad{} : Wr.Dec<FCmd.Query>}: match b: case True{}: {==} case False{}: {==}
def Command.command_ffi_unknown_query(t, n, rest, h): +x = Wr.put_nat(3n+n, rest) %LACommandEntry.ce_table(t, x) : {FCmd.ffi(_) == Wr.err("command: malformed request") : String} %Equal.sym(Wr.Dec<List<&2, FCmd.EntW>>, FCmd.get_table(FCmd.put_table(t, x)), Wr.Got{t, x}, PCommandFfiRoundTrip.cfr_table_rt(t, x, h)) : {FCmd.ffi.go(FCmd.get_req.table(_)) == Wr.err("command: malformed request") : String} %Equal.sym(Wr.Dec<Nat>, Wr.get_nat(x), LAWireSpell.ws_nat_answer(LawsBase.wire_fits(3n+n), 3n+n, rest), LAWireSpell.ws_nat_read(3n+n, rest)) : {FCmd.ffi.go(FCmd.get_req.query(t, FCmd.get_query.go(_))) == Wr.err("command: malformed request") : String} %Equal.sym(Wr.Dec<FCmd.Query>, FCmd.get_query.go(LAWireSpell.ws_nat_answer(LawsBase.wire_fits(3n+n), 3n+n, rest)), Wr.Bad{}, cuq_bad(LawsBase.wire_fits(3n+n), n, rest)) : {FCmd.ffi.go(FCmd.get_req.query(t, _)) == Wr.err("command: malformed request") : String} {==}