Something went wrong. Try again.
Coding agent with a memory of all things
Something went wrong. Try again.
974 B · 23 lines
123456789101112131415161718192021222324# eukhe: the proof of LAW command_ffi_unknown_res## PROOF of LAW command_ffi_unknown_res: the tag 4n + n reads as itself when# it fits and as Bad when too long (ws_nat_read); both ways the resolve reply# decoder answers Bad.
import Baseimport ../../bend/ffi_command.bend as FCmdimport ../../bend/wire.bend as Wrimport ../../laws/base.bend as LawsBaseimport ../../laws/command/entry.bend as Commandimport ../wire/base/spell.bend as LAWireSpell
def cus_bad(b: Bool, -n: Nat, -rest: String) -> {FCmd.get_res.go(LAWireSpell.ws_nat_answer(b, 4n+n, rest)) == Wr.Bad{} : Wr.Dec<FCmd.ResW>}: match b: case True{}: {==} case False{}: {==}
def Command.command_ffi_unknown_res(n, rest): %Equal.sym(Wr.Dec<Nat>, Wr.get_nat(Wr.put_nat(4n+n, rest)), LAWireSpell.ws_nat_answer(LawsBase.wire_fits(4n+n), 4n+n, rest), LAWireSpell.ws_nat_read(4n+n, rest)) : {FCmd.get_res.go(_) == Wr.Bad{} : Wr.Dec<FCmd.ResW>} cus_bad(LawsBase.wire_fits(4n+n), n, rest)