def g_check

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

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

219# the tail form, from any verdict so far, with n the length
220def g_check(xs: List<&2, I.BpfOp>, +pc: Nat, ok: Result<&2, &2, I.BpfError, Unit>) -> {V.bpf_check.go(xs, pc, ok, List.length(&2, I.BpfOp, xs)) == V.bpf_both(ok, V.bpf_check.all(xs, pc)) : Result<&2, &2, I.BpfError, Unit>}:
221  match xs:
222    case Nil{}:
223      match ok:
224        case Fail{e}:
225          {==}
226        case Done{u}:
227          match u:
228            case Unit{}:
229              {==}
230    case Con{op, +t}:
231      match ok:
232        case Fail{e}:
233          {==}
234        case Done{u}:
235          g_check(t, 1n+pc, V.bpf_check.op(op, pc, List.length(&2, I.BpfOp, t)))