def valid_all

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

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

267# what bpf_validate's success gives a run: the checks of every instruction,
268# and at least one instruction
269def valid_all(opts: V.BpfValidateOptions, +prog: List<&2, I.BpfOp>, ok: {V.bpf_validate_with(opts, prog) == Done{Unit{}} : Result<&2, &2, I.BpfError, Unit>}) -> {V.bpf_check.all(prog, 0n) == Done{Unit{}} : Result<&2, &2, I.BpfError, Unit>}:
270  match opts:
271    case V.BpfValidateOptions{+max, +need}:
272      Equal.trans(Result<&2, &2, I.BpfError, Unit>, V.bpf_check.all(prog, 0n), V.bpf_check.go(prog, 0n, Done{Unit{}}, V.bpf_count(prog)), Done{Unit{}}, F_check(prog),
273        mem_l(V.bpf_check.go(prog, 0n, Done{Unit{}}, V.bpf_count(prog)), need, V.bpf_count(prog), prog, ops_r(V.bpf_check.len(V.bpf_count(prog), max), V.bpf_count(prog), need, prog, ok)))