law jeq_taken_skips

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

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

51law jeq_taken_skips:
52  for jt: U32
53  for jf: U32
54  for +skipped: List<&2, I.BpfOp>
55  for +rest: List<&2, I.BpfOp>
56  for +inp: R.BpfInput
57  for e: {List.length(&2, I.BpfOp, skipped) == U32.to_nat(jt) : Nat}
58  {R.bpf_run(inp, Con{I.BpfJmp{I.BpfJeq{}, I.BpfK{0}, jt, jf}, List.append(&2, I.BpfOp, skipped, rest)}) == R.bpf_run(inp, rest) : Result<&2, &2, I.BpfError, U32>}