def nxt

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

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

66def nxt(-pc: Nat, r: Nat, h: {V.bpf_check.next(pc, r) == Done{Unit{}} : Result<&2, &2, I.BpfError, Unit>}) -> {Nat.is_lt(0n, r) == True{} : Bool}:
67  need_ok(Nat.is_lt(0n, r), I.BpfErrNoReturn{pc}, h)