def tb.hp_len
bend-osdev-acpi@0.1.1.0 · PROOF_tables.bend:160
import bend-osdev-acpi@0.1.1.0/PROOF_tables.bend as PROOFTables
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
160def tb.hp_len(+id: U32, +gs: U32, +gw: U32, +go: U32, +ga: U32, +ah: U32, +al: U32, +n: U32, +m: U32, +p: U32) -> {56n == Nat.add(36n, B.Octets.len(B.Octets.concat([B.Octets.le32(id), G.AcpiGas.encode(G.AcpiGas{gs, gw, go, ga, W.W64.from_parts(ah, al)}), B.Octets.of_list([n]), B.Octets.le16(m), B.Octets.of_list([p])]))) : Nat}:
161 match id ah al m:
162 case U32{WCon{id0, WCon{id1, WCon{id2, WCon{id3, WCon{id4, WCon{id5, WCon{id6, WCon{id7, WCon{id8, WCon{id9, WCon{id10, WCon{id11, WCon{id12, WCon{id13, WCon{id14, WCon{id15, WCon{id16, WCon{id17, WCon{id18, WCon{id19, WCon{id20, WCon{id21, WCon{id22, WCon{id23, WCon{id24, WCon{id25, WCon{id26, WCon{id27, WCon{id28, WCon{id29, WCon{id30, WCon{id31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} U32{WCon{ah0, WCon{ah1, WCon{ah2, WCon{ah3, WCon{ah4, WCon{ah5, WCon{ah6, WCon{ah7, WCon{ah8, WCon{ah9, WCon{ah10, WCon{ah11, WCon{ah12, WCon{ah13, WCon{ah14, WCon{ah15, WCon{ah16, WCon{ah17, WCon{ah18, WCon{ah19, WCon{ah20, WCon{ah21, WCon{ah22, WCon{ah23, WCon{ah24, WCon{ah25, WCon{ah26, WCon{ah27, WCon{ah28, WCon{ah29, WCon{ah30, WCon{ah31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} U32{WCon{al0, WCon{al1, WCon{al2, WCon{al3, WCon{al4, WCon{al5, WCon{al6, WCon{al7, WCon{al8, WCon{al9, WCon{al10, WCon{al11, WCon{al12, WCon{al13, WCon{al14, WCon{al15, WCon{al16, WCon{al17, WCon{al18, WCon{al19, WCon{al20, WCon{al21, WCon{al22, WCon{al23, WCon{al24, WCon{al25, WCon{al26, WCon{al27, WCon{al28, WCon{al29, WCon{al30, WCon{al31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} U32{WCon{m0, WCon{m1, WCon{m2, WCon{m3, WCon{m4, WCon{m5, WCon{m6, WCon{m7, WCon{m8, WCon{m9, WCon{m10, WCon{m11, WCon{m12, WCon{m13, WCon{m14, WCon{m15, WCon{m16, WCon{m17, WCon{m18, WCon{m19, WCon{m20, WCon{m21, WCon{m22, WCon{m23, WCon{m24, WCon{m25, WCon{m26, WCon{m27, WCon{m28, WCon{m29, WCon{m30, WCon{m31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}:
163 {==}