def dec_step

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

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

547def dec_step(m: Maybe<&2, I.BpfOp>, -e: I.BpfError, -acc: List<&2, I.BpfOp>, r: Result<&2, &2, I.BpfError, List<&2, I.BpfOp>>) -> {dec.after2(I.bpf_decode.push(m, e, acc), r) == dec.after(acc, I.bpf_decode.cons(m, e, r)) : Result<&2, &2, I.BpfError, List<&2, I.BpfOp>>}:
548  match m:
549    case None{}:
550      {==}
551    case Some{op}:
552      match r:
553        case Fail{f}:
554          {==}
555        case Done{ops}:
556          {==}