def go_app
bend-osdev-bpf@0.1.0.0 · PROOF.bend:295
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
295def go_app(xs: List<&2, I.BpfOp>, +q: 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}) -> {R.bpf_run.go(List.append(&2, I.BpfOp, xs, q), cur, inp) == R.bpf_run.go(xs, cur, inp) : Result<&2, &2, I.BpfError, U32>}:
296 match xs:
297 case Nil{}:
298 match cur:
299 case R.BpfNext{+skip, +st}:
300 Empty.absurd({R.bpf_run.go(q, R.BpfNext{skip, st}, inp) == R.bpf_run.go(Nil{}, R.BpfNext{skip, st}, inp) : Result<&2, &2, I.BpfError, U32>}, 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)))
301 case R.BpfStop{w}:
302 go_stop(q, w, inp)
303 case R.BpfFault{e}:
304 Empty.absurd({R.bpf_run.go(q, R.BpfFault{e}, inp) == R.bpf_run.go(Nil{}, R.BpfFault{e}, inp) : Result<&2, &2, I.BpfError, U32>}, absurd.ft(p))
305 case Con{+op, +t}:
306 match cur:
307 case R.BpfNext{+skip, +st}:
308 match skip:
309 case 0n:
310 go_app(t, q, 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)))
311 case 1n+s:
312 go_app(t, q, 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)
313 case R.BpfStop{w}:
314 {==}
315 case R.BpfFault{e}:
316 Empty.absurd({R.bpf_run.go(Con{op, List.append(&2, I.BpfOp, t, q)}, R.BpfFault{e}, inp) == R.bpf_run.go(Con{op, t}, R.BpfFault{e}, inp) : Result<&2, &2, I.BpfError, U32>}, absurd.ft(p))