PROOF.go_ok: def of bend-osdev-bpf@0.1.0.0
Import: import bend-osdev-bpf@0.1.0.0/PROOF.bend as PROOF
Lines 163-186 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=163&end_line=186

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

# A run from a fine step, over instructions that passed their checks,
# answers Done: induction on the instructions
def 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}:
  match xs:
    case Nil{}:
      match cur:
        case R.BpfNext{+skip, +st}:
          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)))
        case R.BpfStop{w}:
          {==}
        case R.BpfFault{e}:
          Empty.absurd({Result.is_done(&2, &2, I.BpfError, U32, R.bpf_run.go(Nil{}, R.BpfFault{e}, inp)) == True{} : Bool}, absurd.ft(p))
    case Con{+op, +t}:
      match cur:
        case R.BpfNext{+skip, +st}:
          match skip:
            case 0n:
              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)))
            case 1n+s:
              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)
        case R.BpfStop{w}:
          {==}
        case R.BpfFault{e}:
          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))

Uses (26):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Empty.absurd
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List.length
  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=Result.is_done
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  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=absurd.ft
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/PROOF.bend&name=both_l
  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=exec_ok
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/PROOF.bend&name=nat.lt_zero
  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=BpfStep
  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_run.go
  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/validate.bend&name=bpf_check.all
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/validate.bend&name=bpf_check.op