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

import Base
import bend-osdev-bpf@0.1.0.0/insn.bend as I

def g_decode(rs: List<&2, I.BpfRaw>, +pc: Nat, a: Result<&2, &2, I.BpfError, List<&2, I.BpfOp>>) -> {I.bpf_decode.go(rs, pc, a) == dec.after2(a, I.bpf_decode.ref.go(rs, pc)) : Result<&2, &2, I.BpfError, List<&2, I.BpfOp>>}:
  match rs:
    case Nil{}:
      match a:
        case Fail{e}:
          {==}
        case Done{acc}:
          {==}
    case Con{+r, +t}:
      match a:
        case Fail{e}:
          {==}
        case Done{+acc}:
          Equal.trans(Result<&2, &2, I.BpfError, List<&2, I.BpfOp>>, I.bpf_decode.go(t, 1n+pc, I.bpf_decode.push(I.BpfRaw.decode(r), I.BpfErrBadCode{pc, I.BpfRaw.code(r)}, acc)), dec.after2(I.bpf_decode.push(I.BpfRaw.decode(r), I.BpfErrBadCode{pc, I.BpfRaw.code(r)}, acc), I.bpf_decode.ref.go(t, 1n+pc)), dec.after(acc, I.bpf_decode.cons(I.BpfRaw.decode(r), I.BpfErrBadCode{pc, I.BpfRaw.code(r)}, I.bpf_decode.ref.go(t, 1n+pc))),
            g_decode(t, 1n+pc, I.bpf_decode.push(I.BpfRaw.decode(r), I.BpfErrBadCode{pc, I.BpfRaw.code(r)}, acc)), dec_step(I.BpfRaw.decode(r), I.BpfErrBadCode{pc, I.BpfRaw.code(r)}, acc, I.bpf_decode.ref.go(t, 1n+pc)))

Uses (16):
  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=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Result
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/PROOF.bend&name=dec.after
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/PROOF.bend&name=dec.after2
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/PROOF.bend&name=dec_step
  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/insn.bend&name=BpfRaw
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/insn.bend&name=BpfRaw.code
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/insn.bend&name=BpfRaw.decode
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/insn.bend&name=bpf_decode.cons
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/insn.bend&name=bpf_decode.go
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/insn.bend&name=bpf_decode.push
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/insn.bend&name=bpf_decode.ref.go