~/jendhub

def jmp_ok

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

import bend-osdev-bpf@0.1.0.0/PROOF.bend as PROOF
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
import bend-osdev-bpf@0.1.0.0/bpf.bend as R

109def jmp_ok(+jt: U32, +jf: U32, +pc: Nat, +r: Nat, hit: Bool, h: {V.bpf_check.jmp(jt, jf, pc, r) == Done{Unit{}} : Result<&2, &2, I.BpfError, Unit>}) -> {Nat.is_lt(R.bpf_jsel(hit, jt, jf), r) == True{} : Bool}:
110  +g = jmp_ranges(jt, jf, pc, r, h)
111  jsel_ok(hit, jt, jf, r, need_ok(Nat.is_lt(U32.to_nat(jt), r), I.BpfErrJump{pc}, both_l(V.bpf_chk(Nat.is_lt(U32.to_nat(jt), r), I.BpfErrJump{pc}), V.bpf_chk(Nat.is_lt(U32.to_nat(jf), r), I.BpfErrJump{pc}), g)), need_ok(Nat.is_lt(U32.to_nat(jf), r), I.BpfErrJump{pc}, both_r(V.bpf_chk(Nat.is_lt(U32.to_nat(jt), r), I.BpfErrJump{pc}), V.bpf_chk(Nat.is_lt(U32.to_nat(jf), r), I.BpfErrJump{pc}), g)))

Uses (16)

Used by (1)