law gas_round_trip

bend-osdev-acpi@0.1.1.0 · LAWS_tables.bend:32

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

32# A Generic Address Structure, at offset len(a) of a ++ encode(g) ++ b
33law gas_round_trip:
34  for +a: B.Octets
35  for +s: U32
36  for +w: U32
37  for +off: U32
38  for +acc: U32
39  for +addr: W.W64
40  for +b: B.Octets
41  for +s8: {B.byte(s) == s : U32}
42  for +w8: {B.byte(w) == w : U32}
43  for +off8: {B.byte(off) == off : U32}
44  for +acc8: {B.byte(acc) == acc : U32}
45  {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}