law validated_ignores_tail

bend-osdev-bpf@0.1.0.0 · LAWS.bend:30

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
import bend-osdev-bpf@0.1.0.0/bpf.bend as R

30law validated_ignores_tail:
31  for +opts: V.BpfValidateOptions
32  for +prog: List<&2, I.BpfOp>
33  for +rest: List<&2, I.BpfOp>
34  for +inp: R.BpfInput
35  for +ok: {V.bpf_validate_with(opts, prog) == Done{Unit{}} : Result<&2, &2, I.BpfError, Unit>}
36  {R.bpf_run(inp, List.append(&2, I.BpfOp, prog, rest)) == R.bpf_run(inp, prog) : Result<&2, &2, I.BpfError, U32>}