~/jendhub

def bpf_check.all

bend-osdev-bpf@0.1.0.0 · validate.bend:102

import bend-osdev-bpf@0.1.0.0/validate.bend as Validate
import Base
import bend-osdev-bpf@0.1.0.0/insn.bend as I

102# the instructions' own checks, structurally: the reference the proofs
103# reason about (PROOF.bend: F_check ties bpf_check.go to it)
104def bpf_check.all(xs: List<&2, I.BpfOp>, +pc: Nat) -> Result<&2, &2, I.BpfError, Unit>:
105  match xs:
106    case Nil{}:
107      Done{Unit{}}
108    case Con{op, +t}:
109      bpf_both(bpf_check.op(op, pc, List.length(&2, I.BpfOp, t)), bpf_check.all(t, 1n+pc))

Uses (9)

Used by (5)