def valid_nonempty

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

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

275def valid_nonempty(opts: V.BpfValidateOptions, +prog: List<&2, I.BpfOp>, ok: {V.bpf_validate_with(opts, prog) == Done{Unit{}} : Result<&2, &2, I.BpfError, Unit>}) -> {Nat.is_lt(0n, List.length(&2, I.BpfOp, prog)) == True{} : Bool}:
276  match opts:
277    case V.BpfValidateOptions{+max, +need}:
278      +n = V.bpf_count(prog)
279      %Equal.sym(Nat, List.length(&2, I.BpfOp, prog), V.bpf_count(prog), F_count(prog)) : {Nat.is_lt(0n, _) == True{} : Bool}
280      need_ok(Nat.is_lt(0n, n), I.BpfErrEmpty{}, both_l(V.bpf_chk(Nat.is_lt(0n, n), I.BpfErrEmpty{}), V.bpf_chk(Nat.is_le(n, max), I.BpfErrTooLong{n}), ops_l(V.bpf_check.len(n, max), n, need, prog, ok)))