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

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
import bend-osdev-acpi@0.1.1.0/LAWS_tables.bend as Laws

def tb.rread(+xs: List<&2, W.W64>, +acc: List<&2, W.W64>) -> {R.sl.read(List.length(&2, W.W64, xs), False{}, B.Octets.concat(R.sl.enc(xs, False{})), acc) == R.sl.rev(R.sl.rev(Laws.acpilaw.low32(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.le32(W.W64.lo(x)), R.sl.enc(t, False{})}), B.Octets.append(B.Octets.le32(W.W64.lo(x)), B.Octets.concat(R.sl.enc(t, False{}))), BL.octets_concat_cons(B.Octets.le32(W.W64.lo(x)), R.sl.enc(t, False{}))) : {R.sl.read(List.length(&2, W.W64, t), False{}, B.Octets.drop(4n, _), Con{W.W64.from_u32(F.AcpiF.u32(_, 0n)), acc}) == R.sl.rev(R.sl.rev(Laws.acpilaw.low32(Con{x, t}), acc), Nil{}) : List<&2, W.W64>}
      %tb.d4(W.W64.lo(x), B.Octets.concat(R.sl.enc(t, False{}))) : {R.sl.read(List.length(&2, W.W64, t), False{}, _, Con{W.W64.from_u32(F.AcpiF.u32(B.Octets.append(B.Octets.le32(W.W64.lo(x)), B.Octets.concat(R.sl.enc(t, False{}))), 0n)), acc}) == R.sl.rev(R.sl.rev(Laws.acpilaw.low32(Con{x, t}), acc), Nil{}) : List<&2, W.W64>}
      %tb.g4(W.W64.lo(x), B.Octets.concat(R.sl.enc(t, False{}))) : {R.sl.read(List.length(&2, W.W64, t), False{}, B.Octets.concat(R.sl.enc(t, False{})), Con{W.W64.from_u32(_), acc}) == R.sl.rev(R.sl.rev(Laws.acpilaw.low32(Con{x, t}), acc), Nil{}) : List<&2, W.W64>}
      tb.rread(t, Con{W.W64.from_u32(W.W64.lo(x)), acc})

Uses (20):
  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/LAWS_tables.bend&name=acpilaw.low32
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/PROOF_tables.bend&name=tb.d4
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/PROOF_tables.bend&name=tb.g4
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/fields.bend&name=AcpiF.u32
  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.le32
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/word64.bend&name=W64
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/word64.bend&name=W64.from_u32
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/word64.bend&name=W64.lo