def g_decode

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

558def 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>>}:
559  match rs:
560    case Nil{}:
561      match a:
562        case Fail{e}:
563          {==}
564        case Done{acc}:
565          {==}
566    case Con{+r, +t}:
567      match a:
568        case Fail{e}:
569          {==}
570        case Done{+acc}:
571          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))),
572            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)

Used by (1)

bend-osdev-bpf@0.1.0.0/PROOF:F_decode