PROOFTables.tb.xread: def of bend-osdev-acpi@0.1.1.0
Import: import bend-osdev-acpi@0.1.1.0/PROOF_tables.bend as PROOFTables
Lines 353-361 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=353&end_line=361

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-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/rsdt.bend as R

def tb.xread(+xs: List<&2, W.W64>, +acc: List<&2, W.W64>) -> {R.sl.read(List.length(&2, W.W64, xs), True{}, B.Octets.concat(R.sl.enc(xs, True{})), acc) == R.sl.rev(R.sl.rev(xs, acc), Nil{}) : List<&2, W.W64>}:
  match xs:
    case Nil{}:
      {==}
    case Con{+x, t}:
      %Equal.sym(B.Octets, B.Octets.concat(Con{B.Octets.le64(x), R.sl.enc(t, True{})}), B.Octets.append(B.Octets.le64(x), B.Octets.concat(R.sl.enc(t, True{}))), BL.octets_concat_cons(B.Octets.le64(x), R.sl.enc(t, True{}))) : {R.sl.read(List.length(&2, W.W64, t), True{}, B.Octets.drop(8n, _), Con{F.AcpiF.u64(_, 0n), acc}) == R.sl.rev(R.sl.rev(Con{x, t}, acc), Nil{}) : List<&2, W.W64>}
      %tb.d8(x, B.Octets.concat(R.sl.enc(t, True{}))) : {R.sl.read(List.length(&2, W.W64, t), True{}, _, Con{F.AcpiF.u64(B.Octets.append(B.Octets.le64(x), B.Octets.concat(R.sl.enc(t, True{}))), 0n), acc}) == R.sl.rev(R.sl.rev(Con{x, t}, acc), Nil{}) : List<&2, W.W64>}
      %tb.g8(x, B.Octets.concat(R.sl.enc(t, True{}))) : {R.sl.read(List.length(&2, W.W64, t), True{}, B.Octets.concat(R.sl.enc(t, True{})), Con{_, acc}) == R.sl.rev(R.sl.rev(Con{x, t}, acc), Nil{}) : List<&2, W.W64>}
      tb.xread(t, Con{x, acc})

Uses (17):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  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/PROOF_tables.bend&name=tb.d8
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/PROOF_tables.bend&name=tb.g8
  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/rsdt.bend&name=sl.enc
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/rsdt.bend&name=sl.read
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/rsdt.bend&name=sl.rev
  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.le64
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/word64.bend&name=W64