def jsel_ok

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

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

98def jsel_ok(hit: Bool, -jt: U32, -jf: U32, -r: Nat, e1: {Nat.is_lt(U32.to_nat(jt), r) == True{} : Bool}, e2: {Nat.is_lt(U32.to_nat(jf), r) == True{} : Bool}) -> {Nat.is_lt(R.bpf_jsel(hit, jt, jf), r) == True{} : Bool}:
99  match hit:
100    case True{}:
101      e1
102    case False{}:
103      e2