Something went wrong. Try again.
Coding agent with a memory of all things
Something went wrong. Try again.
840 B · 16 lines
1234567891011121314151617# eukhe: the proof of LAW command_ffi_left_over## PROOF of LAW command_ffi_left_over: the encoding of a request that fits# reads back as the request with rest left (command_ffi_round_trip); rest# is not empty, so the entry answers the left-over error.
import Baseimport ../../bend/ffi_command.bend as FCmdimport ../../bend/wire.bend as Wrimport ../../laws/command/entry.bend as Commandimport ./command_ffi_round_trip.bend as PCommandFfiRoundTrip
def Command.command_ffi_left_over(r, rest, h, more): %Equal.sym(Wr.Dec<FCmd.Req>, FCmd.get_req(FCmd.put_req(r, rest)), Wr.Got{r, rest}, Command.command_ffi_round_trip(r, rest, h)) : {FCmd.ffi.go(_) == Wr.err("command: input left over") : String} %Equal.sym(Bool, String.is_empty(rest), False{}, more) : {FCmd.ffi.whole(r, _) == Wr.err("command: input left over") : String} {==}