def ops_r

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

import Base
import bend-osdev-bpf@0.1.0.0/insn.bend as I
import bend-osdev-bpf@0.1.0.0/validate.bend as V

251def ops_r(v: Result<&2, &2, I.BpfError, Unit>, -n: Nat, -need: Bool, -prog: List<&2, I.BpfOp>, h: {V.bpf_validate.ops(v, n, need, prog) == Done{Unit{}} : Result<&2, &2, I.BpfError, Unit>}) -> {V.bpf_validate.mem(V.bpf_check.go(prog, 0n, Done{Unit{}}, n), need, n, prog) == Done{Unit{}} : Result<&2, &2, I.BpfError, Unit>}:
252  match v:
253    case Fail{e}:
254      Empty.absurd({V.bpf_validate.mem(V.bpf_check.go(prog, 0n, Done{Unit{}}, n), need, n, prog) == Done{Unit{}} : Result<&2, &2, I.BpfError, Unit>}, absurd.fd(e, h))
255    case Done{u}:
256      h