bend-osdev-acpi Releases (3): 0.1.2.0 0x437a65a35fd0c02411bea19819f9b33f invalid https://jend.leeeet.dev/files.txt?path=bend-osdev-acpi@0.1.2.0 expected a package named bend-osdev-word64@0.1.1.1 on https://hub.bend-lang.com At https://jend.leeeet.dev/read.txt?path=bend-osdev-acpi@0.1.2.0/LAWS.bend&start_line=16, https://jend.leeeet.dev/read.txt?path=bend-osdev-acpi@0.1.2.0/LAWS_rsdp.bend&start_line=8, https://jend.leeeet.dev/read.txt?path=bend-osdev-acpi@0.1.2.0/LAWS_tables.bend&start_line=20, https://jend.leeeet.dev/read.txt?path=bend-osdev-acpi@0.1.2.0/LAWS_whole.bend&start_line=14, https://jend.leeeet.dev/read.txt?path=bend-osdev-acpi@0.1.2.0/PROOF.bend&start_line=2, https://jend.leeeet.dev/read.txt?path=bend-osdev-acpi@0.1.2.0/PROOF_rsdp.bend&start_line=13, https://jend.leeeet.dev/read.txt?path=bend-osdev-acpi@0.1.2.0/PROOF_tables.bend&start_line=2, https://jend.leeeet.dev/read.txt?path=bend-osdev-acpi@0.1.2.0/PROOF_whole.bend&start_line=17, https://jend.leeeet.dev/read.txt?path=bend-osdev-acpi@0.1.2.0/acpi.bend&start_line=15, https://jend.leeeet.dev/read.txt?path=bend-osdev-acpi@0.1.2.0/aml.bend&start_line=14, https://jend.leeeet.dev/read.txt?path=bend-osdev-acpi@0.1.2.0/aml_device.bend&start_line=7, https://jend.leeeet.dev/read.txt?path=bend-osdev-acpi@0.1.2.0/aml_field.bend&start_line=14, https://jend.leeeet.dev/read.txt?path=bend-osdev-acpi@0.1.2.0/aml_host.bend&start_line=25, https://jend.leeeet.dev/read.txt?path=bend-osdev-acpi@0.1.2.0/aml_interp.bend&start_line=23, https://jend.leeeet.dev/read.txt?path=bend-osdev-acpi@0.1.2.0/aml_ns.bend&start_line=10, https://jend.leeeet.dev/read.txt?path=bend-osdev-acpi@0.1.2.0/aml_resource.bend&start_line=16, https://jend.leeeet.dev/read.txt?path=bend-osdev-acpi@0.1.2.0/aml_term.bend&start_line=16, https://jend.leeeet.dev/read.txt?path=bend-osdev-acpi@0.1.2.0/aml_value.bend&start_line=6, https://jend.leeeet.dev/read.txt?path=bend-osdev-acpi@0.1.2.0/bgrt.bend&start_line=13, https://jend.leeeet.dev/read.txt?path=bend-osdev-acpi@0.1.2.0/check.bend&start_line=2, https://jend.leeeet.dev/read.txt?path=bend-osdev-acpi@0.1.2.0/error.bend&start_line=5, https://jend.leeeet.dev/read.txt?path=bend-osdev-acpi@0.1.2.0/example.bend&start_line=13, https://jend.leeeet.dev/read.txt?path=bend-osdev-acpi@0.1.2.0/facs.bend&start_line=18, https://jend.leeeet.dev/read.txt?path=bend-osdev-acpi@0.1.2.0/fadt.bend&start_line=22, https://jend.leeeet.dev/read.txt?path=bend-osdev-acpi@0.1.2.0/fields.bend&start_line=6, https://jend.leeeet.dev/read.txt?path=bend-osdev-acpi@0.1.2.0/gas.bend&start_line=14, https://jend.leeeet.dev/read.txt?path=bend-osdev-acpi@0.1.2.0/hpet.bend&start_line=16, https://jend.leeeet.dev/read.txt?path=bend-osdev-acpi@0.1.2.0/madt.bend&start_line=29, https://jend.leeeet.dev/read.txt?path=bend-osdev-acpi@0.1.2.0/mcfg.bend&start_line=18, https://jend.leeeet.dev/read.txt?path=bend-osdev-acpi@0.1.2.0/rsdp.bend&start_line=22, https://jend.leeeet.dev/read.txt?path=bend-osdev-acpi@0.1.2.0/rsdt.bend&start_line=6, https://jend.leeeet.dev/read.txt?path=bend-osdev-acpi@0.1.2.0/show.bend&start_line=6, https://jend.leeeet.dev/read.txt?path=bend-osdev-acpi@0.1.2.0/slit.bend&start_line=7, https://jend.leeeet.dev/read.txt?path=bend-osdev-acpi@0.1.2.0/srat.bend&start_line=19, https://jend.leeeet.dev/read.txt?path=bend-osdev-bytes@0.1.1.1/bytes.bend&start_line=12. Files that do not load: LAWS.bend, LAWS_checksum.bend, LAWS_rsdp.bend, LAWS_tables.bend, LAWS_whole.bend and 39 more. 0.1.1.0 0x62173b4e9e82dde7465c7018262f0baa indexed https://jend.leeeet.dev/files.txt?path=bend-osdev-acpi@0.1.1.0 0.1.0.0 0x29fa0aa629b7afe02bc50bfd713bc39b unindexed https://jend.leeeet.dev/files.txt?path=bend-osdev-acpi@0.1.0.0 Definitions (1637, 1 to 100 shown): LAWS.pkglength_round_trip (https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/LAWS.bend&name=pkglength_round_trip) law pkglength_round_trip: for +v: U32 for +rest: B.Octets for +fits: {K.AmlPkgLength.fits(v) == True{} : Bool} {K.AmlPkgLength.decode(B.Octets.append(K.AmlPkgLength.encode(v), rest)) == Done{K.AmlPkgLen{v, rest}} : Result<&2, &2, E.AcpiError, K.AmlPkgLen>} LAWS.namestring_round_trip (https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/LAWS.bend&name=namestring_round_trip) law namestring_round_trip: for +n: N.AmlName for +rest: B.Octets for +ok: {N.AmlName.valid(n) == True{} : Bool} {N.AmlName.decode(B.Octets.append(N.AmlName.encode(n), rest)) == Done{N.AmlNameParsed{n, rest}} : Result<&2, &2, E.AcpiError, N.AmlNameParsed>} LAWS.header_round_trip (https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/LAWS.bend&name=header_round_trip) law header_round_trip: for +h: H.AcpiHeader for +sig4: {B.Octets.len(H.AcpiHeader.signature(h)) == 4n : Nat} for +oem6: {B.Octets.len(H.AcpiHeader.oem_id(h)) == 6n : Nat} for +tid8: {B.Octets.len(H.AcpiHeader.oem_table_id(h)) == 8n : Nat} for +cid4: {B.Octets.len(H.AcpiHeader.creator_id(h)) == 4n : Nat} for +rev8: {B.byte(H.AcpiHeader.revision(h)) == H.AcpiHeader.revision(h) : U32} for +ck8: {B.byte(H.AcpiHeader.checksum(h)) == H.AcpiHeader.checksum(h) : U32} {H.AcpiHeader.decode(H.AcpiHeader.encode(h)) == Done{h} : Result<&2, &2, E.AcpiError, H.AcpiHeader>} LAWS.sdt_check_sums (https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/LAWS.bend&name=sdt_check_sums) law sdt_check_sums: for +o: B.Octets for +raw: B.Octets for +e: {H.AcpiSdt.check(o) == Done{raw} : Result<&2, &2, E.AcpiError, B.Octets>} {C.AcpiChecksum.ok(raw) == True{} : Bool} LAWS.table_checksums (https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/LAWS.bend&name=table_checksums) law table_checksums: for +reg: R.AcpiRegistry for +o: B.Octets for +t: R.AcpiTable for +e: {R.AcpiTable.parse(reg, o) == Done{t} : Result<&2, &2, E.AcpiError, R.AcpiTable>} {C.AcpiChecksum.ok(H.AcpiSdt.bytes(o)) == True{} : Bool} LAWS.rsdp_checksum (https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/LAWS.bend&name=rsdp_checksum) law rsdp_checksum: for +o: B.Octets for +r: P.AcpiRsdp for +e: {P.AcpiRsdp.parse(o) == Done{r} : Result<&2, &2, E.AcpiError, P.AcpiRsdp>} {C.AcpiChecksum.ok(B.Octets.take(20n, o)) == True{} : Bool} LAWS.rsdp_ext_checksum (https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/LAWS.bend&name=rsdp_ext_checksum) law rsdp_ext_checksum: for +o: B.Octets for +r: P.AcpiRsdp for +e: {P.AcpiRsdp.parse(o) == Done{r} : Result<&2, &2, E.AcpiError, P.AcpiRsdp>} {C.AcpiChecksum.ok(B.Octets.take(P.AcpiRsdp.checked(r), o)) == True{} : Bool} LAWS.run_steps_bound (https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/LAWS.bend&name=run_steps_bound) law run_steps_bound: for +n: Nat for +m: I.AmlMachine {Nat.is_le(I.AmlRun.steps(Hs.AmlMemHost, I.AmlM.run(~Hs.AmlMemHost, ~Hs.AmlMemHost.io, n, m)), n) == True{} : Bool} LAWS.load_steps_bound (https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/LAWS.bend&name=load_steps_bound) law load_steps_bound: for +s: A.AmlSystem for +aml: B.Octets for +n: Nat {Nat.is_le(A.AmlOutcome.steps(Hs.AmlMemHost, A.Aml.load(~Hs.AmlMemHost, ~Hs.AmlMemHost.io, s, aml, n)), n) == True{} : Bool} LAWS.eval_steps_bound (https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/LAWS.bend&name=eval_steps_bound) law eval_steps_bound: for +s: A.AmlSystem for +p: String for +args: List<&2, V.AmlValue> for +n: Nat {Nat.is_le(A.AmlOutcome.steps(Hs.AmlMemHost, A.Aml.eval(~Hs.AmlMemHost, ~Hs.AmlMemHost.io, s, p, args, n)), n) == True{} : Bool} LAWS.pkglength_example (https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/LAWS.bend&name=pkglength_example) law pkglength_example: {K.AmlPkgLength.decode(B.Octets.append(K.AmlPkgLength.encode(1000), B.Octets.of_string("AML"))) == Done{K.AmlPkgLen{1000, B.Octets.of_string("AML")}} : Result<&2, &2, E.AcpiError, K.AmlPkgLen>} LAWS.namestring_example (https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/LAWS.bend&name=namestring_example) law namestring_example: {N.AmlName.decode(B.Octets.append(N.AmlName.encode(N.AmlName.of_text("\\_SB.PCI0.LPCB")), B.Octets.of_string("x"))) == Done{N.AmlNameParsed{N.AmlName.of_text("\\_SB.PCI0.LPCB"), B.Octets.of_string("x")}} : Result<&2, &2, E.AcpiError, N.AmlNameParsed>} LAWS.header_example (https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/LAWS.bend&name=header_example) law header_example: {H.AcpiHeader.decode(H.AcpiHeader.encode(X.ex.hdr("APIC", 5))) == Done{X.ex.hdr("APIC", 5)} : Result<&2, &2, E.AcpiError, H.AcpiHeader>} LAWS.check_example (https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/LAWS.bend&name=check_example) # the checks pass for a table and an RSDP of each revision law check_example: {Result.is_done(&2, &2, E.AcpiError, B.Octets, H.AcpiSdt.check(Mc.AcpiMcfg.build(X.AcpiExample.mcfg()))) == True{} : Bool} LAWS.parse_example (https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/LAWS.bend&name=parse_example) law parse_example: {Result.is_done(&2, &2, E.AcpiError, R.AcpiTable, R.AcpiTable.parse(R.AcpiRegistry.default(), Mc.AcpiMcfg.build(X.AcpiExample.mcfg()))) == True{} : Bool} LAWS.rsdp_example (https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/LAWS.bend&name=rsdp_example) law rsdp_example: {Result.is_done(&2, &2, E.AcpiError, P.AcpiRsdp, P.AcpiRsdp.parse(P.AcpiRsdp.build(X.AcpiExample.rsdp()))) == True{} : Bool} LAWS.rsdp_v1_example (https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/LAWS.bend&name=rsdp_v1_example) law rsdp_v1_example: {Result.is_done(&2, &2, E.AcpiError, P.AcpiRsdp, P.AcpiRsdp.parse(P.AcpiRsdp.build(P.AcpiRsdp{B.Octets.of_string("BENDOS"), 0, 4096, None{}}))) == True{} : Bool} LAWS.pkglength_63 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/LAWS.bend&name=pkglength_63) # PkgLength (20.2.4): the boundaries of the four forms law pkglength_63: {B.Octets.hex(K.AmlPkgLength.encode(63)) == "3f" : String} LAWS.pkglength_64 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/LAWS.bend&name=pkglength_64) law pkglength_64: {B.Octets.hex(K.AmlPkgLength.encode(64)) == "4004" : String} LAWS.pkglength_4095 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/LAWS.bend&name=pkglength_4095) law pkglength_4095: {B.Octets.hex(K.AmlPkgLength.encode(4095)) == "4fff" : String} LAWS.pkglength_4096 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/LAWS.bend&name=pkglength_4096) law pkglength_4096: {B.Octets.hex(K.AmlPkgLength.encode(4096)) == "800001" : String} LAWS.pkglength_max (https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/LAWS.bend&name=pkglength_max) law pkglength_max: {B.Octets.hex(K.AmlPkgLength.encode(268435455)) == "cfffffff" : String} LAWS.pkglength_reserved (https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/LAWS.bend&name=pkglength_reserved) # bits 5-4 set in a multi-byte form law pkglength_reserved: {K.AmlPkgLength.decode(B.Octets.of_list([112, 0])) == Fail{E.AcpiAmlBadPkgLength{}} : Result<&2, &2, E.AcpiError, K.AmlPkgLen>} LAWS.name_dual (https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/LAWS.bend&name=name_dual) # NameString (20.2.2): a DualNamePath, a MultiNamePath, parent prefixes, # the root alone (NullName), and a segment that is not a NameSeg law name_dual: {B.Octets.hex(N.AmlName.encode(N.AmlName.of_text("\\_SB.PCI0"))) == "5c2e5f53425f50434930" : String} LAWS.name_multi (https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/LAWS.bend&name=name_multi) law name_multi: {B.Octets.hex(N.AmlName.encode(N.AmlName.of_text("\\_SB.PCI0.LPCB"))) == "5c2f035f53425f504349304c504342" : String} LAWS.name_parents (https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/LAWS.bend&name=name_parents) law name_parents: {B.Octets.hex(N.AmlName.encode(N.AmlName.of_text("^^_STA"))) == "5e5e5f535441" : String} LAWS.name_root (https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/LAWS.bend&name=name_root) law name_root: {B.Octets.hex(N.AmlName.encode(N.AmlName.of_text("\\"))) == "5c00" : String} LAWS.name_bad_seg (https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/LAWS.bend&name=name_bad_seg) law name_bad_seg: {N.AmlName.decode(B.Octets.of_string("1ABC")) == Fail{E.AcpiAmlBadName{}} : Result<&2, &2, E.AcpiError, N.AmlNameParsed>} LAWS.eisaid_power_button (https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/LAWS.bend&name=eisaid_power_button) # EISAID (chapter 19, the ASL operator), with the IDs of the examples of # 6.1.5 (the power button) and 6.1.2 (a PCI root bridge's compatible ID) law eisaid_power_button: {T.AmlT.eisaid_value("PNP0C0C") == 202166337 : U32} LAWS.eisaid_pci (https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/LAWS.bend&name=eisaid_pci) law eisaid_pci: {Dv.AmlEisaId.text(51040321) == "PNP0A03" : String} LAWS.aml_name_hid (https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/LAWS.bend&name=aml_name_hid) # AML encodings (20.2.5.2, DefName; 20.2.5.2, DefMethod; 20.2.5.3, # DefReturn): Name (_HID, EISAID ("PNP0C0C")) and # Method (_STA) { Return (0x0F) }, as ASL compilers write them law aml_name_hid: {B.Octets.hex(T.AmlT.encode1(T.AmlT.name("_HID", T.AmlT.eisaid("PNP0C0C")))) == "085f4849440c41d00c0c" : String} LAWS.aml_method_sta (https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/LAWS.bend&name=aml_method_sta) law aml_method_sta: {B.Octets.hex(T.AmlT.encode1(T.AmlT.method("_STA", 0n, False{}, [T.AmlT.ret(T.AmlT.int32(15))]))) == "14095f53544100a40a0f" : String} LAWS.checksum_built (https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/LAWS.bend&name=checksum_built) # Checksums: a table built here sums to zero; one byte changed, it does not law checksum_built: {C.AcpiChecksum.ok(Mc.AcpiMcfg.build(X.AcpiExample.mcfg())) == True{} : Bool} LAWS.checksum_broken (https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/LAWS.bend&name=checksum_broken) law checksum_broken: {C.AcpiChecksum.ok(B.Octets.append(Mc.AcpiMcfg.build(X.AcpiExample.mcfg()), B.Octets.of_list([1]))) == False{} : Bool} LAWS.aml_eval_sta (https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/LAWS.bend&name=aml_eval_sta) # the interpreter: Method (_STA) { Return (0x0F) } loaded at the root, and # called law aml_eval_sta: {A.AmlOutcome.result(Hs.AmlMemHost, A.Aml.eval_mem(A.AmlSystem.after(Hs.AmlMemHost, A.Aml.mem_system(True{}), A.Aml.load_mem(A.Aml.mem_system(True{}), T.AmlT.encode([T.AmlT.method("_STA", 0n, False{}, [T.AmlT.ret(T.AmlT.int32(15))])]), 100n)), "\\_STA", Nil{}, 100n)) == Done{V.AmlInt{W.W64.from_u32(15)}} : Result<&2, &2, E.AcpiError, V.AmlValue>} LAWSTables.gas_round_trip (https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/LAWS_tables.bend&name=gas_round_trip) # A Generic Address Structure, at offset len(a) of a ++ encode(g) ++ b law gas_round_trip: for +a: B.Octets for +s: U32 for +w: U32 for +off: U32 for +acc: U32 for +addr: W.W64 for +b: B.Octets for +s8: {B.byte(s) == s : U32} for +w8: {B.byte(w) == w : U32} … LAWSTables.hpet_round_trip (https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/LAWS_tables.bend&name=hpet_round_trip) # The HPET table's body, read back with any header h law hpet_round_trip: for +h: H.AcpiHeader for +sig4: {B.Octets.len(H.AcpiHeader.signature(h)) == 4n : Nat} for +oem6: {B.Octets.len(H.AcpiHeader.oem_id(h)) == 6n : Nat} for +tid8: {B.Octets.len(H.AcpiHeader.oem_table_id(h)) == 8n : Nat} for +cid4: {B.Octets.len(H.AcpiHeader.creator_id(h)) == 4n : Nat} for +h0: H.AcpiHeader for +oem6b: {B.Octets.len(H.AcpiHeader.oem_id(h0)) == 6n : Nat} for +tid8b: {B.Octets.len(H.AcpiHeader.oem_table_id(h0)) == 8n : Nat} for +cid4b: {B.Octets.len(H.AcpiHeader.creator_id(h0)) == 4n : Nat} … LAWSTables.bgrt_round_trip (https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/LAWS_tables.bend&name=bgrt_round_trip) # The BGRT table's body, read back with any header h law bgrt_round_trip: for +h: H.AcpiHeader for +sig4: {B.Octets.len(H.AcpiHeader.signature(h)) == 4n : Nat} for +oem6: {B.Octets.len(H.AcpiHeader.oem_id(h)) == 6n : Nat} for +tid8: {B.Octets.len(H.AcpiHeader.oem_table_id(h)) == 8n : Nat} for +cid4: {B.Octets.len(H.AcpiHeader.creator_id(h)) == 4n : Nat} for +h0: H.AcpiHeader for +oem6b: {B.Octets.len(H.AcpiHeader.oem_id(h0)) == 6n : Nat} for +tid8b: {B.Octets.len(H.AcpiHeader.oem_table_id(h0)) == 8n : Nat} for +cid4b: {B.Octets.len(H.AcpiHeader.creator_id(h0)) == 4n : Nat} … LAWSTables.facs_round_trip (https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/LAWS_tables.bend&name=facs_round_trip) # The FACS: parsed back as built, with the Length 64 that build writes law facs_round_trip: for +l: U32 for +hs: U32 for +wv: U32 for +gl: U32 for +fl: U32 for +xw: W.W64 for +v: U32 for +of: U32 for +v8: {B.byte(v) == v : U32} {Fa.AcpiFacs.parse(Fa.AcpiFacs.build(Fa.AcpiFacs{l, hs, wv, gl, fl, xw, v, of})) == Done{Fa.AcpiFacs{64, hs, wv, gl, fl, xw, v, of}} : Result<&2, &2, E.AcpiError, Fa.AcpiFacs>} LAWSTables.acpilaw.low32 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/LAWS_tables.bend&name=acpilaw.low32) # the low 32 bits of each address, as a W64 (what an RSDT entry holds) def acpilaw.low32(xs: List<&2, W.W64>) -> List<&2, W.W64>: LAWSTables.acpilaw.mcfg_fit (https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/LAWS_tables.bend&name=acpilaw.mcfg_fit) # each MCFG structure as it is stored: the segment group's low 16 bits, the # bus numbers' low 8 bits def acpilaw.mcfg_fit(es: List<&2, Mc.AcpiMcfgEntry>) -> List<&2, Mc.AcpiMcfgEntry>: LAWSTables.xsdt_round_trip (https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/LAWS_tables.bend&name=xsdt_round_trip) # The XSDT's entries, read back with any header h law xsdt_round_trip: for +h: H.AcpiHeader for +h0: H.AcpiHeader for +oem6b: {B.Octets.len(H.AcpiHeader.oem_id(h0)) == 6n : Nat} for +tid8b: {B.Octets.len(H.AcpiHeader.oem_table_id(h0)) == 8n : Nat} for +cid4b: {B.Octets.len(H.AcpiHeader.creator_id(h0)) == 4n : Nat} for +xs: List<&2, W.W64> {R.AcpiXsdt.of_sdt(H.AcpiSdt{h, B.Octets.drop(36n, R.AcpiXsdt.build(h0, xs))}) == Done{R.AcpiSdtList{h, xs}} : Result<&2, &2, E.AcpiError, R.AcpiSdtList>} LAWSTables.rsdt_round_trip (https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/LAWS_tables.bend&name=rsdt_round_trip) # The RSDT's entries: each address's low 32 bits law rsdt_round_trip: for +h: H.AcpiHeader for +h0: H.AcpiHeader for +oem6b: {B.Octets.len(H.AcpiHeader.oem_id(h0)) == 6n : Nat} for +tid8b: {B.Octets.len(H.AcpiHeader.oem_table_id(h0)) == 8n : Nat} for +cid4b: {B.Octets.len(H.AcpiHeader.creator_id(h0)) == 4n : Nat} for +xs: List<&2, W.W64> {R.AcpiRsdt.of_sdt(H.AcpiSdt{h, B.Octets.drop(36n, R.AcpiRsdt.build(h0, xs))}) == Done{R.AcpiSdtList{h, acpilaw.low32(xs)}} : Result<&2, &2, E.AcpiError, R.AcpiSdtList>} LAWSTables.mcfg_round_trip (https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/LAWS_tables.bend&name=mcfg_round_trip) # The MCFG's allocation structures, as stored law mcfg_round_trip: for +h: H.AcpiHeader for +h0: H.AcpiHeader for +oem6b: {B.Octets.len(H.AcpiHeader.oem_id(h0)) == 6n : Nat} for +tid8b: {B.Octets.len(H.AcpiHeader.oem_table_id(h0)) == 8n : Nat} for +cid4b: {B.Octets.len(H.AcpiHeader.creator_id(h0)) == 4n : Nat} for +es: List<&2, Mc.AcpiMcfgEntry> {Mc.AcpiMcfg.of_sdt(H.AcpiSdt{h, B.Octets.drop(36n, Mc.AcpiMcfg.build(Mc.AcpiMcfg{h0, es}))}) == Done{Mc.AcpiMcfg{h, acpilaw.mcfg_fit(es)}} : Result<&2, &2, E.AcpiError, Mc.AcpiMcfg>} LAWSTables.aml_round_trip (https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/LAWS_tables.bend&name=aml_round_trip) # A DSDT's or SSDT's definition block (the header's signature is kept, so # it too must have its size) law aml_round_trip: for +h: H.AcpiHeader for +h0: H.AcpiHeader for +sig4b: {B.Octets.len(H.AcpiHeader.signature(h0)) == 4n : Nat} for +oem6b: {B.Octets.len(H.AcpiHeader.oem_id(h0)) == 6n : Nat} for +tid8b: {B.Octets.len(H.AcpiHeader.oem_table_id(h0)) == 8n : Nat} for +cid4b: {B.Octets.len(H.AcpiHeader.creator_id(h0)) == 4n : Nat} for +a: B.Octets {Ds.AcpiAml.of_sdt(H.AcpiSdt{h, B.Octets.drop(36n, Ds.AcpiAml.build(Ds.AcpiAml{h0, a}))}) == Done{Ds.AcpiAml{h, a}} : Result<&2, &2, E.AcpiError, Ds.AcpiAml>} PROOF.bdisc (https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/PROOF.bend&name=bdisc) def bdisc(+b: Bool) -> Type: PROOF.ft_absurd (https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/PROOF.bend&name=ft_absurd) def ft_absurd(+e: {False{} == True{} : Bool}) -> Empty: PROOF.pk_abs (https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/PROOF.bend&name=pk_abs) def pk_abs(+v: U32, +r: List<&2, U32>, e: Empty) -> {K.pk.pub(K.pk.dec(B.append(B.mask(K.pk.enc(v)), r))) == Done{K.AmlPkgLen{v, B.Octets.of_list(r)}} : Result<&2, &2, E.AcpiError, K.AmlPkgLen>}: PROOF.pk_bits (https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/PROOF.bend&name=pk_bits) # the bits from the top down, so that they are matched in binder order def pk_bits(+b31: Bool, +b30: Bool, +b29: Bool, +b28: Bool, +b27: Bool, +b26: Bool, +b25: Bool, +b24: Bool, +b23: Bool, +b22: Bool, +b21: Bool, +b20: Bool, +b19: Bool, +b18: Bool, +b17: Bool, +b16: Bool, +b15: Bool, +b14: Bool, +b13: Bool, +b12: Bool, +b11: Bool, +b10: Bool, +b9: Bool, +b8: Bool, +b7: Bool, +b6: Bool, +b5: Bool, +b4: Bool, +b3: Bool, +b2: Bool, +b1: Bool, +b0: Bool, +r: List<&2, U32>, +fits: {K.AmlPkgLength.fits(U32{WCon{b0, WCon{b1, WCon{b2, WCon{b3, WCon{b4, WCon{b5, WCon{b6, WCon{b7, WCon{b8, WCon{b9, WCon{b10, WCon{b11, WCon{b12, WCon{b13, WCon{b14, WCon{b15, WCon{b16, WCon{b17, WCon{b18, WCon{b19, WCon{b20, WCon{b21, WCon{b22, WCon{b23, WCon{b24, WCon{b25, WCon{b26, WCon{b27, WCon{b28, WCon{b29, WCon{b30, WCon{b31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}) == True{} : Bool}) -> {K.pk.pub(K.pk.dec(B.append(B.mask(K.pk.enc(U32{WCon{b0, WCon{b1, WCon{b2, WCon{b3, WCon{b4, WCon{b5, WCon{b6, WCon{b7, WCon{b8, WCon{b9, WCon{b10, WCon{b11, WCon{b12, WCon{b13, WCon{b14, WCon{b15, WCon{b16, WCon{b17, WCon{b18, WCon{b19, WCon{b20, WCon{b21, WCon{b22, WCon{b23, WCon{b24, WCon{b25, WCon{b26, WCon{b27, WCon{b28, WCon{b29, WCon{b30, WCon{b31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}})), r))) == Done{K.AmlPkgLen{U32{WCon{b0, WCon{b1, WCon{b2, WCon{b3, WCon{b4, WCon{b5, WCon{b6, WCon{b7, WCon{b8, WCon{b9, WCon{b10, WCon{b11, WCon{b12, WCon{b13, WCon{b14, WCon{b15, WCon{b16, WCon{b17, WCon{b18, WCon{b19, WCon{b20, WCon{b21, WCon{b22, WCon{b23, WCon{b24, WCon{b25, WCon{b26, WCon{b27, WCon{b28, WCon{b29, WCon{b30, WCon{b31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}, B.Octets.of_list(r)}} : Result<&2, &2, E.AcpiError, K.AmlPkgLen>}: PROOF.pk_rt (https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/PROOF.bend&name=pk_rt) def pk_rt(+v: U32, +r: List<&2, U32>, +fits: {K.AmlPkgLength.fits(v) == True{} : Bool}) -> {K.pk.pub(K.pk.dec(B.append(B.mask(K.pk.enc(v)), r))) == Done{K.AmlPkgLen{v, B.Octets.of_list(r)}} : Result<&2, &2, E.AcpiError, K.AmlPkgLen>}: PROOF.cnt_abs (https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/PROOF.bend&name=cnt_abs) def cnt_abs(+k: Nat, e: Empty) -> {U32.to_nat(B.byte(U32.from_nat(k))) == k : Nat}: PROOF.cnt.d256 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/PROOF.bend&name=cnt.d256) def cnt.d256(+k: Nat, +lt: {Nat.is_lt(Nat.add(256n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(256n, k)))) == Nat.add(256n, k) : Nat}: PROOF.cnt.d255 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/PROOF.bend&name=cnt.d255) def cnt.d255(+k: Nat, +lt: {Nat.is_lt(Nat.add(255n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(255n, k)))) == Nat.add(255n, k) : Nat}: PROOF.cnt.d254 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/PROOF.bend&name=cnt.d254) def cnt.d254(+k: Nat, +lt: {Nat.is_lt(Nat.add(254n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(254n, k)))) == Nat.add(254n, k) : Nat}: PROOF.cnt.d253 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/PROOF.bend&name=cnt.d253) def cnt.d253(+k: Nat, +lt: {Nat.is_lt(Nat.add(253n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(253n, k)))) == Nat.add(253n, k) : Nat}: PROOF.cnt.d252 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/PROOF.bend&name=cnt.d252) def cnt.d252(+k: Nat, +lt: {Nat.is_lt(Nat.add(252n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(252n, k)))) == Nat.add(252n, k) : Nat}: PROOF.cnt.d251 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/PROOF.bend&name=cnt.d251) def cnt.d251(+k: Nat, +lt: {Nat.is_lt(Nat.add(251n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(251n, k)))) == Nat.add(251n, k) : Nat}: PROOF.cnt.d250 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/PROOF.bend&name=cnt.d250) def cnt.d250(+k: Nat, +lt: {Nat.is_lt(Nat.add(250n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(250n, k)))) == Nat.add(250n, k) : Nat}: PROOF.cnt.d249 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/PROOF.bend&name=cnt.d249) def cnt.d249(+k: Nat, +lt: {Nat.is_lt(Nat.add(249n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(249n, k)))) == Nat.add(249n, k) : Nat}: PROOF.cnt.d248 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/PROOF.bend&name=cnt.d248) def cnt.d248(+k: Nat, +lt: {Nat.is_lt(Nat.add(248n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(248n, k)))) == Nat.add(248n, k) : Nat}: PROOF.cnt.d247 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/PROOF.bend&name=cnt.d247) def cnt.d247(+k: Nat, +lt: {Nat.is_lt(Nat.add(247n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(247n, k)))) == Nat.add(247n, k) : Nat}: PROOF.cnt.d246 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/PROOF.bend&name=cnt.d246) def cnt.d246(+k: Nat, +lt: {Nat.is_lt(Nat.add(246n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(246n, k)))) == Nat.add(246n, k) : Nat}: PROOF.cnt.d245 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/PROOF.bend&name=cnt.d245) def cnt.d245(+k: Nat, +lt: {Nat.is_lt(Nat.add(245n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(245n, k)))) == Nat.add(245n, k) : Nat}: PROOF.cnt.d244 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/PROOF.bend&name=cnt.d244) def cnt.d244(+k: Nat, +lt: {Nat.is_lt(Nat.add(244n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(244n, k)))) == Nat.add(244n, k) : Nat}: PROOF.cnt.d243 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/PROOF.bend&name=cnt.d243) def cnt.d243(+k: Nat, +lt: {Nat.is_lt(Nat.add(243n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(243n, k)))) == Nat.add(243n, k) : Nat}: PROOF.cnt.d242 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/PROOF.bend&name=cnt.d242) def cnt.d242(+k: Nat, +lt: {Nat.is_lt(Nat.add(242n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(242n, k)))) == Nat.add(242n, k) : Nat}: PROOF.cnt.d241 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/PROOF.bend&name=cnt.d241) def cnt.d241(+k: Nat, +lt: {Nat.is_lt(Nat.add(241n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(241n, k)))) == Nat.add(241n, k) : Nat}: PROOF.cnt.d240 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/PROOF.bend&name=cnt.d240) def cnt.d240(+k: Nat, +lt: {Nat.is_lt(Nat.add(240n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(240n, k)))) == Nat.add(240n, k) : Nat}: PROOF.cnt.d239 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/PROOF.bend&name=cnt.d239) def cnt.d239(+k: Nat, +lt: {Nat.is_lt(Nat.add(239n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(239n, k)))) == Nat.add(239n, k) : Nat}: PROOF.cnt.d238 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/PROOF.bend&name=cnt.d238) def cnt.d238(+k: Nat, +lt: {Nat.is_lt(Nat.add(238n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(238n, k)))) == Nat.add(238n, k) : Nat}: PROOF.cnt.d237 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/PROOF.bend&name=cnt.d237) def cnt.d237(+k: Nat, +lt: {Nat.is_lt(Nat.add(237n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(237n, k)))) == Nat.add(237n, k) : Nat}: PROOF.cnt.d236 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/PROOF.bend&name=cnt.d236) def cnt.d236(+k: Nat, +lt: {Nat.is_lt(Nat.add(236n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(236n, k)))) == Nat.add(236n, k) : Nat}: PROOF.cnt.d235 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/PROOF.bend&name=cnt.d235) def cnt.d235(+k: Nat, +lt: {Nat.is_lt(Nat.add(235n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(235n, k)))) == Nat.add(235n, k) : Nat}: PROOF.cnt.d234 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/PROOF.bend&name=cnt.d234) def cnt.d234(+k: Nat, +lt: {Nat.is_lt(Nat.add(234n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(234n, k)))) == Nat.add(234n, k) : Nat}: PROOF.cnt.d233 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/PROOF.bend&name=cnt.d233) def cnt.d233(+k: Nat, +lt: {Nat.is_lt(Nat.add(233n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(233n, k)))) == Nat.add(233n, k) : Nat}: PROOF.cnt.d232 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/PROOF.bend&name=cnt.d232) def cnt.d232(+k: Nat, +lt: {Nat.is_lt(Nat.add(232n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(232n, k)))) == Nat.add(232n, k) : Nat}: PROOF.cnt.d231 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/PROOF.bend&name=cnt.d231) def cnt.d231(+k: Nat, +lt: {Nat.is_lt(Nat.add(231n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(231n, k)))) == Nat.add(231n, k) : Nat}: PROOF.cnt.d230 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/PROOF.bend&name=cnt.d230) def cnt.d230(+k: Nat, +lt: {Nat.is_lt(Nat.add(230n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(230n, k)))) == Nat.add(230n, k) : Nat}: PROOF.cnt.d229 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/PROOF.bend&name=cnt.d229) def cnt.d229(+k: Nat, +lt: {Nat.is_lt(Nat.add(229n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(229n, k)))) == Nat.add(229n, k) : Nat}: PROOF.cnt.d228 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/PROOF.bend&name=cnt.d228) def cnt.d228(+k: Nat, +lt: {Nat.is_lt(Nat.add(228n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(228n, k)))) == Nat.add(228n, k) : Nat}: PROOF.cnt.d227 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/PROOF.bend&name=cnt.d227) def cnt.d227(+k: Nat, +lt: {Nat.is_lt(Nat.add(227n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(227n, k)))) == Nat.add(227n, k) : Nat}: PROOF.cnt.d226 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/PROOF.bend&name=cnt.d226) def cnt.d226(+k: Nat, +lt: {Nat.is_lt(Nat.add(226n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(226n, k)))) == Nat.add(226n, k) : Nat}: PROOF.cnt.d225 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/PROOF.bend&name=cnt.d225) def cnt.d225(+k: Nat, +lt: {Nat.is_lt(Nat.add(225n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(225n, k)))) == Nat.add(225n, k) : Nat}: PROOF.cnt.d224 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/PROOF.bend&name=cnt.d224) def cnt.d224(+k: Nat, +lt: {Nat.is_lt(Nat.add(224n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(224n, k)))) == Nat.add(224n, k) : Nat}: PROOF.cnt.d223 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/PROOF.bend&name=cnt.d223) def cnt.d223(+k: Nat, +lt: {Nat.is_lt(Nat.add(223n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(223n, k)))) == Nat.add(223n, k) : Nat}: PROOF.cnt.d222 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/PROOF.bend&name=cnt.d222) def cnt.d222(+k: Nat, +lt: {Nat.is_lt(Nat.add(222n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(222n, k)))) == Nat.add(222n, k) : Nat}: PROOF.cnt.d221 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/PROOF.bend&name=cnt.d221) def cnt.d221(+k: Nat, +lt: {Nat.is_lt(Nat.add(221n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(221n, k)))) == Nat.add(221n, k) : Nat}: PROOF.cnt.d220 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/PROOF.bend&name=cnt.d220) def cnt.d220(+k: Nat, +lt: {Nat.is_lt(Nat.add(220n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(220n, k)))) == Nat.add(220n, k) : Nat}: PROOF.cnt.d219 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/PROOF.bend&name=cnt.d219) def cnt.d219(+k: Nat, +lt: {Nat.is_lt(Nat.add(219n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(219n, k)))) == Nat.add(219n, k) : Nat}: PROOF.cnt.d218 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/PROOF.bend&name=cnt.d218) def cnt.d218(+k: Nat, +lt: {Nat.is_lt(Nat.add(218n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(218n, k)))) == Nat.add(218n, k) : Nat}: PROOF.cnt.d217 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/PROOF.bend&name=cnt.d217) def cnt.d217(+k: Nat, +lt: {Nat.is_lt(Nat.add(217n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(217n, k)))) == Nat.add(217n, k) : Nat}: PROOF.cnt.d216 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/PROOF.bend&name=cnt.d216) def cnt.d216(+k: Nat, +lt: {Nat.is_lt(Nat.add(216n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(216n, k)))) == Nat.add(216n, k) : Nat}: PROOF.cnt.d215 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/PROOF.bend&name=cnt.d215) def cnt.d215(+k: Nat, +lt: {Nat.is_lt(Nat.add(215n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(215n, k)))) == Nat.add(215n, k) : Nat}: PROOF.cnt.d214 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/PROOF.bend&name=cnt.d214) def cnt.d214(+k: Nat, +lt: {Nat.is_lt(Nat.add(214n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(214n, k)))) == Nat.add(214n, k) : Nat}: PROOF.cnt.d213 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/PROOF.bend&name=cnt.d213) def cnt.d213(+k: Nat, +lt: {Nat.is_lt(Nat.add(213n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(213n, k)))) == Nat.add(213n, k) : Nat}: PROOF.cnt.d212 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/PROOF.bend&name=cnt.d212) def cnt.d212(+k: Nat, +lt: {Nat.is_lt(Nat.add(212n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(212n, k)))) == Nat.add(212n, k) : Nat}: PROOF.cnt.d211 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/PROOF.bend&name=cnt.d211) def cnt.d211(+k: Nat, +lt: {Nat.is_lt(Nat.add(211n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(211n, k)))) == Nat.add(211n, k) : Nat}: PROOF.cnt.d210 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/PROOF.bend&name=cnt.d210) def cnt.d210(+k: Nat, +lt: {Nat.is_lt(Nat.add(210n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(210n, k)))) == Nat.add(210n, k) : Nat}: PROOF.cnt.d209 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/PROOF.bend&name=cnt.d209) def cnt.d209(+k: Nat, +lt: {Nat.is_lt(Nat.add(209n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(209n, k)))) == Nat.add(209n, k) : Nat}: PROOF.cnt.d208 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/PROOF.bend&name=cnt.d208) def cnt.d208(+k: Nat, +lt: {Nat.is_lt(Nat.add(208n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(208n, k)))) == Nat.add(208n, k) : Nat}: More: https://jend.leeeet.dev/packages/bend-osdev-acpi.txt?definitions_offset=100