def decode_go

bend-osdev-bpf@0.1.0.0 · PROOF.bend:487

import Base
import bend-osdev-bpf@0.1.0.0/insn.bend as I
import bend-osdev-bpf@0.1.0.0/LAWS.bend as Laws

487def decode_go(prog: List<&2, I.BpfOp>, +pc: Nat) -> {I.bpf_decode.ref.go(I.bpf_encode.ref(prog), pc) == Done{prog} : Result<&2, &2, I.BpfError, List<&2, I.BpfOp>>}:
488  match prog:
489    case Nil{}:
490      {==}
491    case Con{+op, +t}:
492      %Equal.sym(Maybe<&2, I.BpfOp>, I.BpfRaw.decode(I.BpfOp.encode(op)), Some{op}, Laws.insn_round_trip(op)) : {I.bpf_decode.cons(_, I.BpfErrBadCode{pc, I.BpfRaw.code(I.BpfOp.encode(op))}, I.bpf_decode.ref.go(I.bpf_encode.ref(t), 1n+pc)) == Done{Con{op, t}} : Result<&2, &2, I.BpfError, List<&2, I.BpfOp>>}
493      %Equal.sym(Result<&2, &2, I.BpfError, List<&2, I.BpfOp>>, I.bpf_decode.ref.go(I.bpf_encode.ref(t), 1n+pc), Done{t}, decode_go(t, 1n+pc)) : {I.bpf_decode.cons(Some{op}, I.BpfErrBadCode{pc, I.BpfRaw.code(I.BpfOp.encode(op))}, _) == Done{Con{op, t}} : Result<&2, &2, I.BpfError, List<&2, I.BpfOp>>}
494      {==}