def tb.cvals
bend-osdev-acpi@0.1.1.0 · PROOF_tables.bend:407
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/fields.bend as F
import bend-osdev-acpi@0.1.1.0/mcfg.bend as Mc
407def tb.cvals(+ah: U32, +al: U32, +s: U32, +lo: U32, +hi: U32) -> {Mc.AcpiMcfgEntry{W.W64.from_parts(ah, al), B.low16(s), B.byte(lo), B.byte(hi)} == Mc.AcpiMcfgEntry{F.AcpiF.u64(B.Octets.concat([B.Octets.le64(W.W64.from_parts(ah, al)), B.Octets.le16(s), B.Octets.of_list([lo, hi]), B.Octets.zeros(4n)]), 0n), F.AcpiF.u16(B.Octets.concat([B.Octets.le64(W.W64.from_parts(ah, al)), B.Octets.le16(s), B.Octets.of_list([lo, hi]), B.Octets.zeros(4n)]), 8n), F.AcpiF.u8(B.Octets.concat([B.Octets.le64(W.W64.from_parts(ah, al)), B.Octets.le16(s), B.Octets.of_list([lo, hi]), B.Octets.zeros(4n)]), 10n), F.AcpiF.u8(B.Octets.concat([B.Octets.le64(W.W64.from_parts(ah, al)), B.Octets.le16(s), B.Octets.of_list([lo, hi]), B.Octets.zeros(4n)]), 11n)} : Mc.AcpiMcfgEntry}:
408 match ah al s:
409 case 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{s0, WCon{s1, WCon{s2, WCon{s3, WCon{s4, WCon{s5, WCon{s6, WCon{s7, WCon{s8, WCon{s9, WCon{s10, WCon{s11, WCon{s12, WCon{s13, WCon{s14, WCon{s15, WCon{s16, WCon{s17, WCon{s18, WCon{s19, WCon{s20, WCon{s21, WCon{s22, WCon{s23, WCon{s24, WCon{s25, WCon{s26, WCon{s27, WCon{s28, WCon{s29, WCon{s30, WCon{s31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}:
410 {==}