def go_ok

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

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

163# A run from a fine step, over instructions that passed their checks,
164# answers Done: induction on the instructions
165def go_ok(xs: List<&2, I.BpfOp>, cur: R.BpfStep, +inp: R.BpfInput, +pc: Nat, +v: {V.bpf_check.all(xs, pc) == Done{Unit{}} : Result<&2, &2, I.BpfError, Unit>}, p: {step_ok(cur, List.length(&2, I.BpfOp, xs)) == True{} : Bool}) -> {Result.is_done(&2, &2, I.BpfError, U32, R.bpf_run.go(xs, cur, inp)) == True{} : Bool}:
166  match xs:
167    case Nil{}:
168      match cur:
169        case R.BpfNext{+skip, +st}:
170          Empty.absurd({Result.is_done(&2, &2, I.BpfError, U32, R.bpf_run.go(Nil{}, R.BpfNext{skip, st}, inp)) == True{} : Bool}, absurd.ft(Equal.trans(Bool, False{}, Nat.is_lt(skip, 0n), True{}, Equal.sym(Bool, Nat.is_lt(skip, 0n), False{}, nat.lt_zero(skip)), p)))
171        case R.BpfStop{w}:
172          {==}
173        case R.BpfFault{e}:
174          Empty.absurd({Result.is_done(&2, &2, I.BpfError, U32, R.bpf_run.go(Nil{}, R.BpfFault{e}, inp)) == True{} : Bool}, absurd.ft(p))
175    case Con{+op, +t}:
176      match cur:
177        case R.BpfNext{+skip, +st}:
178          match skip:
179            case 0n:
180              go_ok(t, R.bpf_exec(op, st, inp), inp, 1n+pc, both_r(V.bpf_check.op(op, pc, List.length(&2, I.BpfOp, t)), V.bpf_check.all(t, 1n+pc), v), exec_ok(op, st, inp, pc, List.length(&2, I.BpfOp, t), both_l(V.bpf_check.op(op, pc, List.length(&2, I.BpfOp, t)), V.bpf_check.all(t, 1n+pc), v)))
181            case 1n+s:
182              go_ok(t, R.BpfNext{s, st}, inp, 1n+pc, both_r(V.bpf_check.op(op, pc, List.length(&2, I.BpfOp, t)), V.bpf_check.all(t, 1n+pc), v), p)
183        case R.BpfStop{w}:
184          {==}
185        case R.BpfFault{e}:
186          Empty.absurd({Result.is_done(&2, &2, I.BpfError, U32, R.bpf_run.go(Con{op, t}, R.BpfFault{e}, inp)) == True{} : Bool}, absurd.ft(p))