law ja_skips

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

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

43law ja_skips:
44  for k: U32
45  for +skipped: List<&2, I.BpfOp>
46  for +rest: List<&2, I.BpfOp>
47  for +inp: R.BpfInput
48  for e: {List.length(&2, I.BpfOp, skipped) == U32.to_nat(k) : Nat}
49  {R.bpf_run(inp, Con{I.BpfJa{k}, List.append(&2, I.BpfOp, skipped, rest)}) == R.bpf_run(inp, rest) : Result<&2, &2, I.BpfError, U32>}