def F_check

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

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

237def F_check(+xs: List<&2, I.BpfOp>) -> {V.bpf_check.all(xs, 0n) == V.bpf_check.go(xs, 0n, Done{Unit{}}, V.bpf_count(xs)) : Result<&2, &2, I.BpfError, Unit>}:
238  %F_count(xs) : {V.bpf_check.all(xs, 0n) == V.bpf_check.go(xs, 0n, Done{Unit{}}, _) : Result<&2, &2, I.BpfError, Unit>}
239  Equal.sym(Result<&2, &2, I.BpfError, Unit>, V.bpf_check.go(xs, 0n, Done{Unit{}}, List.length(&2, I.BpfOp, xs)), V.bpf_check.all(xs, 0n), g_check(xs, 0n, Done{Unit{}}))