PROOF.exec_ok: def of bend-osdev-bpf@0.1.0.0
Import: import bend-osdev-bpf@0.1.0.0/PROOF.bend as PROOF
Lines 113-161 of bend-osdev-bpf@0.1.0.0/PROOF.bend: https://jend.leeeet.dev/read.txt?path=bend-osdev-bpf@0.1.0.0/PROOF.bend&start_line=113&end_line=161

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

# every instruction that passed its checks steps to an instruction that exists
def exec_ok(op: I.BpfOp, st: R.BpfState, +inp: R.BpfInput, +pc: Nat, +r: Nat, h: {V.bpf_check.op(op, pc, r) == Done{Unit{}} : Result<&2, &2, I.BpfError, Unit>}) -> {step_ok(R.bpf_exec(op, st, inp), r) == True{} : Bool}:
  match op:
    case I.BpfLdAbs{+size, +k}:
      step_of_ok(R.bpf_set_a.m(R.bpf_load(inp, size, k), st), r, nxt(pc, r, h))
    case I.BpfLdInd{+size, +k}:
      match st:
        case R.BpfState{+a, +x, +mem}:
          step_of_ok(R.bpf_set_a.m(R.bpf_load.ind(inp, size, x, k), R.BpfState{a, x, mem}), r, nxt(pc, r, h))
    case I.BpfLdImm{+k}:
      nxt(pc, r, h)
    case I.BpfLdLen{}:
      nxt(pc, r, h)
    case I.BpfLdMem{+k}:
      mem_ok(k, R.bpf_mem.lda(st, k), pc, r, h)
    case I.BpfLdxImm{+k}:
      nxt(pc, r, h)
    case I.BpfLdxMem{+k}:
      mem_ok(k, R.bpf_mem.ldx(st, k), pc, r, h)
    case I.BpfLdxLen{}:
      nxt(pc, r, h)
    case I.BpfLdxMsh{+k}:
      step_of_ok(R.bpf_set_x.m(R.bpf_load.msh(inp, k), st), r, nxt(pc, r, h))
    case I.BpfSt{+k}:
      mem_ok(k, R.bpf_mem.st(st, k), pc, r, h)
    case I.BpfStx{+k}:
      mem_ok(k, R.bpf_mem.stx(st, k), pc, r, h)
    case I.BpfAlu{+o, +src}:
      match st:
        case R.BpfState{+a, +x, +mem}:
          step_of_ok(R.bpf_set_a.m(R.bpf_alu(o, a, R.bpf_src(src, x)), R.BpfState{a, x, mem}), r, nxt(pc, r, both_r(V.bpf_check.div(o, src, pc), V.bpf_check.next(pc, r), h)))
    case I.BpfNeg{}:
      nxt(pc, r, h)
    case I.BpfJa{+k}:
      need_ok(Nat.is_lt(U32.to_nat(k), r), I.BpfErrJump{pc}, h)
    case I.BpfJmp{+c, +src, +jt, +jf}:
      match st:
        case R.BpfState{+a, +x, +mem}:
          jmp_ok(jt, jf, pc, r, R.bpf_test(c, a, R.bpf_src(src, x)), h)
    case I.BpfRet{+v}:
      match v:
        case I.BpfRetK{+k}:
          {==}
        case I.BpfRetA{}:
          {==}
    case I.BpfTax{}:
      nxt(pc, r, h)
    case I.BpfTxa{}:
      nxt(pc, r, h)

Uses (34):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_lt
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Result
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.to_nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Unit
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/PROOF.bend&name=both_r
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/PROOF.bend&name=jmp_ok
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/PROOF.bend&name=mem_ok
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/PROOF.bend&name=need_ok
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/PROOF.bend&name=nxt
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/PROOF.bend&name=step_of_ok
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/PROOF.bend&name=step_ok
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/bpf.bend&name=BpfInput
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/bpf.bend&name=BpfState
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/bpf.bend&name=bpf_alu
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/bpf.bend&name=bpf_exec
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/bpf.bend&name=bpf_load
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/bpf.bend&name=bpf_load.ind
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/bpf.bend&name=bpf_load.msh
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/bpf.bend&name=bpf_mem.lda
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/bpf.bend&name=bpf_mem.ldx
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/bpf.bend&name=bpf_mem.st
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/bpf.bend&name=bpf_mem.stx
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/bpf.bend&name=bpf_set_a.m
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/bpf.bend&name=bpf_set_x.m
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/bpf.bend&name=bpf_src
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/bpf.bend&name=bpf_test
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/insn.bend&name=BpfError
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/insn.bend&name=BpfOp
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/insn.bend&name=BpfRval
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/validate.bend&name=bpf_check.div
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/validate.bend&name=bpf_check.next
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/validate.bend&name=bpf_check.op