LAWSTables.facs_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 98-109 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=98&end_line=109

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/error.bend as E
import bend-osdev-acpi@0.1.1.0/facs.bend as Fa

# The FACS: parsed back as built, with the Length 64 that build writes
law facs_round_trip:
  for +l: U32
  for +hs: U32
  for +wv: U32
  for +gl: U32
  for +fl: U32
  for +xw: W.W64
  for +v: U32
  for +of: U32
  for +v8: {B.byte(v) == v : U32}
  {Fa.AcpiFacs.parse(Fa.AcpiFacs.build(Fa.AcpiFacs{l, hs, wv, gl, fl, xw, v, of})) == Done{Fa.AcpiFacs{64, hs, wv, gl, fl, xw, v, of}} : Result<&2, &2, E.AcpiError, Fa.AcpiFacs>}

Uses (13):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Result
  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.facs_bits
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/error.bend&name=AcpiError
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/facs.bend&name=AcpiFacs
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/facs.bend&name=AcpiFacs.build
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/facs.bend&name=AcpiFacs.parse
  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-word64@0.1.1.0/LAWS.bend&name=parts_of
  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.from_parts
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/word64.bend&name=W64.hi
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/word64.bend&name=W64.lo