Something went wrong. Try again.
Coding agent with a memory of all things
Something went wrong. Try again.
978 B · 23 lines
123456789101112131415161718192021222324# eukhe: the proof of LAW command_ffi_unknown_menu## PROOF of LAW command_ffi_unknown_menu: the tag 3n + n reads as itself when# it fits and as Bad when too long (ws_nat_read); both ways the menu 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 cum_bad(b: Bool, -n: Nat, -rest: String) -> {FCmd.get_menu.go(LAWireSpell.ws_nat_answer(b, 3n+n, rest)) == Wr.Bad{} : Wr.Dec<FCmd.MenuW>}: match b: case True{}: {==} case False{}: {==}
def Command.command_ffi_unknown_menu(n, rest): %Equal.sym(Wr.Dec<Nat>, Wr.get_nat(Wr.put_nat(3n+n, rest)), LAWireSpell.ws_nat_answer(LawsBase.wire_fits(3n+n), 3n+n, rest), LAWireSpell.ws_nat_read(3n+n, rest)) : {FCmd.get_menu.go(_) == Wr.Bad{} : Wr.Dec<FCmd.MenuW>} cum_bad(LawsBase.wire_fits(3n+n), n, rest)