law jeq_not_taken_skips

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

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

60law jeq_not_taken_skips:
61  for jt: U32
62  for jf: U32
63  for +skipped: List<&2, I.BpfOp>
64  for +rest: List<&2, I.BpfOp>
65  for +inp: R.BpfInput
66  for e: {List.length(&2, I.BpfOp, skipped) == U32.to_nat(jf) : Nat}
67  {R.bpf_run(inp, Con{I.BpfJmp{I.BpfJeq{}, I.BpfK{1}, jt, jf}, List.append(&2, I.BpfOp, skipped, rest)}) == R.bpf_run(inp, rest) : Result<&2, &2, I.BpfError, U32>}