def need_ok

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

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

43def need_ok(b: Bool, -e: I.BpfError, h: {V.bpf_chk(b, e) == Done{Unit{}} : Result<&2, &2, I.BpfError, Unit>}) -> {b == True{} : Bool}:
44  match b:
45    case True{}:
46      {==}
47    case False{}:
48      Empty.absurd({False{} == True{} : Bool}, absurd.fd(e, h))