def exec_ok

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

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

113# every instruction that passed its checks steps to an instruction that exists
114def 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}:
115  match op:
116    case I.BpfLdAbs{+size, +k}:
117      step_of_ok(R.bpf_set_a.m(R.bpf_load(inp, size, k), st), r, nxt(pc, r, h))
118    case I.BpfLdInd{+size, +k}:
119      match st:
120        case R.BpfState{+a, +x, +mem}:
121          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))
122    case I.BpfLdImm{+k}:
123      nxt(pc, r, h)
124    case I.BpfLdLen{}:
125      nxt(pc, r, h)
126    case I.BpfLdMem{+k}:
127      mem_ok(k, R.bpf_mem.lda(st, k), pc, r, h)
128    case I.BpfLdxImm{+k}:
129      nxt(pc, r, h)
130    case I.BpfLdxMem{+k}:
131      mem_ok(k, R.bpf_mem.ldx(st, k), pc, r, h)
132    case I.BpfLdxLen{}:
133      nxt(pc, r, h)
134    case I.BpfLdxMsh{+k}:
135      step_of_ok(R.bpf_set_x.m(R.bpf_load.msh(inp, k), st), r, nxt(pc, r, h))
136    case I.BpfSt{+k}:
137      mem_ok(k, R.bpf_mem.st(st, k), pc, r, h)
138    case I.BpfStx{+k}:
139      mem_ok(k, R.bpf_mem.stx(st, k), pc, r, h)
140    case I.BpfAlu{+o, +src}:
141      match st:
142        case R.BpfState{+a, +x, +mem}:
143          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)))
144    case I.BpfNeg{}:
145      nxt(pc, r, h)
146    case I.BpfJa{+k}:
147      need_ok(Nat.is_lt(U32.to_nat(k), r), I.BpfErrJump{pc}, h)
148    case I.BpfJmp{+c, +src, +jt, +jf}:
149      match st:
150        case R.BpfState{+a, +x, +mem}:
151          jmp_ok(jt, jf, pc, r, R.bpf_test(c, a, R.bpf_src(src, x)), h)
152    case I.BpfRet{+v}:
153      match v:
154        case I.BpfRetK{+k}:
155          {==}
156        case I.BpfRetA{}:
157          {==}
158    case I.BpfTax{}:
159      nxt(pc, r, h)
160    case I.BpfTxa{}:
161      nxt(pc, r, h)