LAWS.insn_round_trip: law of bend-osdev-bpf@0.1.0.0
Import: import bend-osdev-bpf@0.1.0.0/LAWS.bend as LAWS
Lines 69-71 of bend-osdev-bpf@0.1.0.0/LAWS.bend: https://jend.leeeet.dev/read.txt?path=bend-osdev-bpf@0.1.0.0/LAWS.bend&start_line=69&end_line=71

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

law insn_round_trip:
  for op: I.BpfOp
  {I.BpfRaw.decode(I.BpfOp.encode(op)) == Some{op} : Maybe<&2, I.BpfOp>}

Uses (9):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Maybe
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/insn.bend&name=BpfAluOp
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/insn.bend&name=BpfCond
  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=BpfOp.encode
  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=BpfRval
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/insn.bend&name=BpfSize
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/insn.bend&name=BpfSrc