def tb.mlen

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

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/mcfg.bend as Mc

456def tb.mlen(+es: List<&2, Mc.AcpiMcfgEntry>) -> {Nat.mul(List.length(&2, Mc.AcpiMcfgEntry, es), 16n) == B.Octets.len(B.Octets.concat(Mc.mcfg.enc(es))) : Nat}:
457  match es:
458    case Nil{}:
459      {==}
460    case Con{e, t}:
461      match e:
462        case Mc.AcpiMcfgEntry{+b, +s, +lo, +hi}:
463          %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))) : {Nat.mul(List.length(&2, Mc.AcpiMcfgEntry, Con{Mc.AcpiMcfgEntry{b, s, lo, hi}, t}), 16n) == B.Octets.len(_) : Nat}
464          %tb.la(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))) : {Nat.mul(List.length(&2, Mc.AcpiMcfgEntry, Con{Mc.AcpiMcfgEntry{b, s, lo, hi}, t}), 16n) == _ : Nat}
465          %tb.clen_g(b, s, lo, hi) : {Nat.mul(List.length(&2, Mc.AcpiMcfgEntry, Con{Mc.AcpiMcfgEntry{b, s, lo, hi}, t}), 16n) == Nat.add(_, B.Octets.len(B.Octets.concat(Mc.mcfg.enc(t)))) : Nat}
466          %tb.mlen(t) : {Nat.mul(List.length(&2, Mc.AcpiMcfgEntry, Con{Mc.AcpiMcfgEntry{b, s, lo, hi}, t}), 16n) == Nat.add(16n, _) : Nat}
467          {==}