law bgrt_round_trip

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

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/header.bend as H
import bend-osdev-acpi@0.1.1.0/bgrt.bend as Bg

76# The BGRT table's body, read back with any header h
77law bgrt_round_trip:
78  for +h: H.AcpiHeader
79  for +sig4: {B.Octets.len(H.AcpiHeader.signature(h)) == 4n : Nat}
80  for +oem6: {B.Octets.len(H.AcpiHeader.oem_id(h)) == 6n : Nat}
81  for +tid8: {B.Octets.len(H.AcpiHeader.oem_table_id(h)) == 8n : Nat}
82  for +cid4: {B.Octets.len(H.AcpiHeader.creator_id(h)) == 4n : Nat}
83  for +h0: H.AcpiHeader
84  for +oem6b: {B.Octets.len(H.AcpiHeader.oem_id(h0)) == 6n : Nat}
85  for +tid8b: {B.Octets.len(H.AcpiHeader.oem_table_id(h0)) == 8n : Nat}
86  for +cid4b: {B.Octets.len(H.AcpiHeader.creator_id(h0)) == 4n : Nat}
87  for +v: U32
88  for +st: U32
89  for +it: U32
90  for +a: W.W64
91  for +x: U32
92  for +y: U32
93  for +v16: {B.low16(v) == v : U32}
94  for +st8: {B.byte(st) == st : U32}
95  for +it8: {B.byte(it) == it : U32}
96  {Bg.AcpiBgrt.of_sdt(H.AcpiSdt{h, B.Octets.drop(36n, Bg.AcpiBgrt.build(Bg.AcpiBgrt{h0, v, st, it, a, x, y}))}) == Done{Bg.AcpiBgrt{h, v, st, it, a, x, y}} : Result<&2, &2, E.AcpiError, Bg.AcpiBgrt>}