def tb.rlen

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

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

308def tb.rlen(+xs: List<&2, W.W64>) -> {Nat.mul(List.length(&2, W.W64, xs), 4n) == B.Octets.len(B.Octets.concat(R.sl.enc(xs, False{}))) : Nat}:
309  match xs:
310    case Nil{}:
311      {==}
312    case Con{x, t}:
313      %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{}))) : {Nat.mul(List.length(&2, W.W64, Con{x, t}), 4n) == B.Octets.len(_) : Nat}
314      %tb.la(B.Octets.le32(W.W64.lo(x)), B.Octets.concat(R.sl.enc(t, False{}))) : {Nat.mul(List.length(&2, W.W64, Con{x, t}), 4n) == _ : Nat}
315      %Equal.sym(Nat, B.Octets.len(B.Octets.le32(W.W64.lo(x))), 4n, BL.octets_len_le32(W.W64.lo(x))) : {Nat.mul(List.length(&2, W.W64, Con{x, t}), 4n) == Nat.add(_, B.Octets.len(B.Octets.concat(R.sl.enc(t, False{})))) : Nat}
316      %tb.rlen(t) : {Nat.mul(List.length(&2, W.W64, Con{x, t}), 4n) == Nat.add(4n, _) : Nat}
317      {==}