def sc_l

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

import Base
import bend-osdev-bpf@0.1.0.0/insn.bend as I
import bend-osdev-bpf@0.1.0.0/seccomp.bend as S

1964def sc_l(v: Result<&2, &2, I.BpfError, Unit>, -prog: List<&2, I.BpfOp>, h: {S.seccomp_validate.go(v, prog) == Done{Unit{}} : Result<&2, &2, I.BpfError, Unit>}) -> {v == Done{Unit{}} : Result<&2, &2, I.BpfError, Unit>}:
1965  match v:
1966    case Fail{e}:
1967      Empty.absurd({Fail{e} == Done{Unit{}} : Result<&2, &2, I.BpfError, Unit>}, absurd.fd(e, h))
1968    case Done{u}:
1969      match u:
1970        case Unit{}:
1971          {==}