def mem_l

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

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

258def mem_l(v: Result<&2, &2, I.BpfError, Unit>, -need: Bool, -n: Nat, -prog: List<&2, I.BpfOp>, h: {V.bpf_validate.mem(v, need, n, prog) == Done{Unit{}} : Result<&2, &2, I.BpfError, Unit>}) -> {v == Done{Unit{}} : Result<&2, &2, I.BpfError, Unit>}:
259  match v:
260    case Fail{e}:
261      Empty.absurd({Fail{e} == Done{Unit{}} : Result<&2, &2, I.BpfError, Unit>}, absurd.fd(e, h))
262    case Done{u}:
263      match u:
264        case Unit{}:
265          {==}