LAWS.namestring_round_trip: law of bend-osdev-acpi@0.1.1.0
Import: import bend-osdev-acpi@0.1.1.0/LAWS.bend as LAWS
Lines 43-47 of bend-osdev-acpi@0.1.1.0/LAWS.bend: https://jend.leeeet.dev/read.txt?path=bend-osdev-acpi@0.1.1.0/LAWS.bend&start_line=43&end_line=47

import Base
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/aml_name.bend as N

law namestring_round_trip:
  for +n: N.AmlName
  for +rest: B.Octets
  for +ok: {N.AmlName.valid(n) == True{} : Bool}
  {N.AmlName.decode(B.Octets.append(N.AmlName.encode(n), rest)) == Done{N.AmlNameParsed{n, rest}} : Result<&2, &2, E.AcpiError, N.AmlNameParsed>}

Uses (24):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  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=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.bend&name=dec_rt
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/aml_name.bend&name=AmlName
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/aml_name.bend&name=AmlName.decode
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/aml_name.bend&name=AmlName.encode
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/aml_name.bend&name=AmlName.valid
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/aml_name.bend&name=AmlNameParsed
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/aml_name.bend&name=nm.dec
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/aml_name.bend&name=nm.enc
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/aml_name.bend&name=nm.pub
  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-bytes@0.1.1.0/LAWS.bend&name=octets_append_list
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/LAWS.bend&name=octets_of_to
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/LAWS.bend&name=octets_to_of
  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.of_list
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/bytes.bend&name=Octets.to_list
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/bytes.bend&name=append
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/bytes.bend&name=mask