LAWSTables.gas_round_trip: law of bend-osdev-acpi@0.1.1.0
Import: import bend-osdev-acpi@0.1.1.0/LAWS_tables.bend as LAWSTables
Lines 32-45 of bend-osdev-acpi@0.1.1.0/LAWS_tables.bend: https://jend.leeeet.dev/read.txt?path=bend-osdev-acpi@0.1.1.0/LAWS_tables.bend&start_line=32&end_line=45

import Base
import bend-osdev-word64@0.1.1.0/word64.bend as W
import bend-osdev-bytes@0.1.1.0/bytes.bend as B
import bend-osdev-acpi@0.1.1.0/gas.bend as G

# A Generic Address Structure, at offset len(a) of a ++ encode(g) ++ b
law gas_round_trip:
  for +a: B.Octets
  for +s: U32
  for +w: U32
  for +off: U32
  for +acc: U32
  for +addr: W.W64
  for +b: B.Octets
  for +s8: {B.byte(s) == s : U32}
  for +w8: {B.byte(w) == w : U32}
  for +off8: {B.byte(off) == off : U32}
  for +acc8: {B.byte(acc) == acc : U32}
  {G.AcpiGas.at(B.Octets.append(a, B.Octets.append(G.AcpiGas.encode(G.AcpiGas{s, w, off, acc, addr}), b)), B.Octets.len(a)) == G.AcpiGas{s, w, off, acc, addr} : G.AcpiGas}

Uses (22):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Maybe.default
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.add
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/PROOF_tables.bend&name=tb.gas_a
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/PROOF_tables.bend&name=tb.gas_b
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/fields.bend&name=AcpiF.u64
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/fields.bend&name=AcpiF.u8
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/gas.bend&name=AcpiGas
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/gas.bend&name=AcpiGas.at
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/gas.bend&name=AcpiGas.encode
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/LAWS.bend&name=octets_append_assoc
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/bytes.bend&name=Octets
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/bytes.bend&name=Octets.append
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/bytes.bend&name=Octets.le64
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/bytes.bend&name=Octets.len
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/bytes.bend&name=Octets.of_list
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/bytes.bend&name=byte
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/LAWS.bend&name=nat_add_zero
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/word64.bend&name=W64
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/word64.bend&name=W64.zero