law whole_example

bend-osdev-acpi@0.1.2.0 · LAWS_whole.bend:138

import Base
import bend-osdev-bytes@0.1.1.1/bytes.bend as B
import bend-osdev-acpi@0.1.2.0/header.bend as H

138# the hypotheses hold at an example: a header AcpiHeader.make fits, and a
139# 39-byte table
140law whole_example:
141  {(B.Octets.len(H.AcpiHeader.signature(H.AcpiHeader.make(B.Octets.of_string("SSDT"), 2, B.Octets.of_string("BEND"), B.Octets.of_string("TABLE")))), B.Octets.len(H.AcpiHeader.oem_id(H.AcpiHeader.make(B.Octets.of_string("SSDT"), 2, B.Octets.of_string("BEND"), B.Octets.of_string("TABLE")))), B.Octets.len(H.AcpiHeader.oem_table_id(H.AcpiHeader.make(B.Octets.of_string("SSDT"), 2, B.Octets.of_string("BEND"), B.Octets.of_string("TABLE")))), B.Octets.len(H.AcpiHeader.creator_id(H.AcpiHeader.make(B.Octets.of_string("SSDT"), 2, B.Octets.of_string("BEND"), B.Octets.of_string("TABLE")))), B.byte(H.AcpiHeader.revision(H.AcpiHeader.make(B.Octets.of_string("SSDT"), 2, B.Octets.of_string("BEND"), B.Octets.of_string("TABLE")))), Nat.is_le(B.Octets.len(H.AcpiSdt.build(H.AcpiHeader.make(B.Octets.of_string("SSDT"), 2, B.Octets.of_string("BEND"), B.Octets.of_string("TABLE")), B.Octets.of_list([1, 2, 3]))), U32.to_nat(39))) == (4n, 6n, 8n, 4n, 2, True{}) : Nat & Nat & Nat & Nat & U32 & Bool}