def ops_l

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

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

241# each pass of bpf_validate_with runs only once the one before it holds
242def ops_l(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 == Done{Unit{}} : Result<&2, &2, I.BpfError, Unit>}:
243  match v:
244    case Fail{e}:
245      Empty.absurd({Fail{e} == Done{Unit{}} : Result<&2, &2, I.BpfError, Unit>}, absurd.fd(e, h))
246    case Done{u}:
247      match u:
248        case Unit{}:
249          {==}