PROOFTables.tb.mread: def of bend-osdev-acpi@0.1.1.0
Import: import bend-osdev-acpi@0.1.1.0/PROOF_tables.bend as PROOFTables
Lines 469-480 of bend-osdev-acpi@0.1.1.0/PROOF_tables.bend: https://jend.leeeet.dev/read.txt?path=bend-osdev-acpi@0.1.1.0/PROOF_tables.bend&start_line=469&end_line=480

import Base
import bend-osdev-bytes@0.1.1.0/bytes.bend as B
import bend-osdev-bytes@0.1.1.0/LAWS.bend as BL
import bend-osdev-acpi@0.1.1.0/fields.bend as F
import bend-osdev-acpi@0.1.1.0/mcfg.bend as Mc
import bend-osdev-acpi@0.1.1.0/LAWS_tables.bend as Laws

def tb.mread(+es: List<&2, Mc.AcpiMcfgEntry>) -> {Laws.acpilaw.mcfg_fit(es) == Mc.mcfg.read(List.length(&2, Mc.AcpiMcfgEntry, es), B.Octets.concat(Mc.mcfg.enc(es))) : List<&2, Mc.AcpiMcfgEntry>}:
  match es:
    case Nil{}:
      {==}
    case Con{e, t}:
      match e:
        case Mc.AcpiMcfgEntry{+b, +s, +lo, +hi}:
          %Equal.sym(B.Octets, B.Octets.concat(Con{B.Octets.concat([B.Octets.le64(b), B.Octets.le16(s), B.Octets.of_list([lo, hi]), B.Octets.zeros(4n)]), Mc.mcfg.enc(t)}), B.Octets.append(B.Octets.concat([B.Octets.le64(b), B.Octets.le16(s), B.Octets.of_list([lo, hi]), B.Octets.zeros(4n)]), B.Octets.concat(Mc.mcfg.enc(t))), BL.octets_concat_cons(B.Octets.concat([B.Octets.le64(b), B.Octets.le16(s), B.Octets.of_list([lo, hi]), B.Octets.zeros(4n)]), Mc.mcfg.enc(t))) : {Con{Mc.AcpiMcfgEntry{b, B.low16(s), B.byte(lo), B.byte(hi)}, Laws.acpilaw.mcfg_fit(t)} == Con{Mc.AcpiMcfgEntry{F.AcpiF.u64(_, 0n), F.AcpiF.u16(_, 8n), F.AcpiF.u8(_, 10n), F.AcpiF.u8(_, 11n)}, Mc.mcfg.read(List.length(&2, Mc.AcpiMcfgEntry, t), B.Octets.drop(16n, _))} : List<&2, Mc.AcpiMcfgEntry>}
          %tb.mdrop(b, s, lo, hi, B.Octets.concat(Mc.mcfg.enc(t))) : {Con{Mc.AcpiMcfgEntry{b, B.low16(s), B.byte(lo), B.byte(hi)}, Laws.acpilaw.mcfg_fit(t)} == Con{Mc.AcpiMcfgEntry{F.AcpiF.u64(B.Octets.append(B.Octets.concat([B.Octets.le64(b), B.Octets.le16(s), B.Octets.of_list([lo, hi]), B.Octets.zeros(4n)]), B.Octets.concat(Mc.mcfg.enc(t))), 0n), F.AcpiF.u16(B.Octets.append(B.Octets.concat([B.Octets.le64(b), B.Octets.le16(s), B.Octets.of_list([lo, hi]), B.Octets.zeros(4n)]), B.Octets.concat(Mc.mcfg.enc(t))), 8n), F.AcpiF.u8(B.Octets.append(B.Octets.concat([B.Octets.le64(b), B.Octets.le16(s), B.Octets.of_list([lo, hi]), B.Octets.zeros(4n)]), B.Octets.concat(Mc.mcfg.enc(t))), 10n), F.AcpiF.u8(B.Octets.append(B.Octets.concat([B.Octets.le64(b), B.Octets.le16(s), B.Octets.of_list([lo, hi]), B.Octets.zeros(4n)]), B.Octets.concat(Mc.mcfg.enc(t))), 11n)}, Mc.mcfg.read(List.length(&2, Mc.AcpiMcfgEntry, t), _)} : List<&2, Mc.AcpiMcfgEntry>}
          %tb.mread(t) : {Con{Mc.AcpiMcfgEntry{b, B.low16(s), B.byte(lo), B.byte(hi)}, Laws.acpilaw.mcfg_fit(t)} == Con{Mc.AcpiMcfgEntry{F.AcpiF.u64(B.Octets.append(B.Octets.concat([B.Octets.le64(b), B.Octets.le16(s), B.Octets.of_list([lo, hi]), B.Octets.zeros(4n)]), B.Octets.concat(Mc.mcfg.enc(t))), 0n), F.AcpiF.u16(B.Octets.append(B.Octets.concat([B.Octets.le64(b), B.Octets.le16(s), B.Octets.of_list([lo, hi]), B.Octets.zeros(4n)]), B.Octets.concat(Mc.mcfg.enc(t))), 8n), F.AcpiF.u8(B.Octets.append(B.Octets.concat([B.Octets.le64(b), B.Octets.le16(s), B.Octets.of_list([lo, hi]), B.Octets.zeros(4n)]), B.Octets.concat(Mc.mcfg.enc(t))), 10n), F.AcpiF.u8(B.Octets.append(B.Octets.concat([B.Octets.le64(b), B.Octets.le16(s), B.Octets.of_list([lo, hi]), B.Octets.zeros(4n)]), B.Octets.concat(Mc.mcfg.enc(t))), 11n)}, _} : List<&2, Mc.AcpiMcfgEntry>}
          %tb.ment(b, s, lo, hi, B.Octets.concat(Mc.mcfg.enc(t))) : {Con{Mc.AcpiMcfgEntry{b, B.low16(s), B.byte(lo), B.byte(hi)}, Laws.acpilaw.mcfg_fit(t)} == Con{_, Laws.acpilaw.mcfg_fit(t)} : List<&2, Mc.AcpiMcfgEntry>}
          {==}

Uses (23):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List.length
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/LAWS_tables.bend&name=acpilaw.mcfg_fit
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/PROOF_tables.bend&name=tb.mdrop
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/PROOF_tables.bend&name=tb.ment
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/fields.bend&name=AcpiF.u16
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/fields.bend&name=AcpiF.u64
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/fields.bend&name=AcpiF.u8
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/mcfg.bend&name=AcpiMcfgEntry
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/mcfg.bend&name=mcfg.enc
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/mcfg.bend&name=mcfg.read
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/LAWS.bend&name=octets_concat_cons
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/bytes.bend&name=Octets
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/bytes.bend&name=Octets.append
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/bytes.bend&name=Octets.concat
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/bytes.bend&name=Octets.drop
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/bytes.bend&name=Octets.le16
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/bytes.bend&name=Octets.le64
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/bytes.bend&name=Octets.of_list
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/bytes.bend&name=Octets.zeros
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/bytes.bend&name=byte
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/bytes.bend&name=low16