def skip_app

bend-osdev-bpf@0.1.0.0 · PROOF.bend:327

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

327def skip_app(skipped: List<&2, I.BpfOp>, +rest: List<&2, I.BpfOp>, +st: R.BpfState, +inp: R.BpfInput) -> {R.bpf_run.go(List.append(&2, I.BpfOp, skipped, rest), R.BpfNext{List.length(&2, I.BpfOp, skipped), st}, inp) == R.bpf_run.go(rest, R.BpfNext{0n, st}, inp) : Result<&2, &2, I.BpfError, U32>}:
328  match skipped:
329    case Nil{}:
330      {==}
331    case Con{h, t}:
332      skip_app(t, rest, st, inp)