def tb.xread

bend-osdev-acpi@0.1.1.0 · PROOF_tables.bend:353

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

353def 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>}:
354  match xs:
355    case Nil{}:
356      {==}
357    case Con{+x, t}:
358      %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>}
359      %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>}
360      %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>}
361      tb.xread(t, Con{x, acc})