def step_ok

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

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

72def step_ok(cur: R.BpfStep, r: Nat) -> Bool:
73  match cur:
74    case R.BpfNext{+skip, +st}:
75      Nat.is_lt(skip, r)
76    case R.BpfStop{v}:
77      True{}
78    case R.BpfFault{e}:
79      False{}