def scratch_ok

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

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

88def scratch_ok(ok: Bool, -k: U32, -st: R.BpfState, -r: Nat, e1: {ok == True{} : Bool}, e2: {Nat.is_lt(0n, r) == True{} : Bool}) -> {step_ok(R.bpf_scratch(ok, k, st), r) == True{} : Bool}:
89  match ok:
90    case True{}:
91      e2
92    case False{}:
93      Empty.absurd({step_ok(R.bpf_scratch(False{}, k, st), r) == True{} : Bool}, absurd.ft(e1))