def ckr.vr

bend-osdev-acpi@0.1.2.0 · PROOF_rsdp.bend:51

import Base
import bend-osdev-bytes@0.1.1.1/bytes.bend as B
import bend-osdev-bytes@0.1.1.1/LAWS.bend as BL
import bend-osdev-acpi@0.1.2.0/fields.bend as F
import bend-osdev-acpi@0.1.2.0/rsdp.bend as P

51def ckr.vr(+oem: B.Octets, +oem6: {B.Octets.len(oem) == 6n : Nat}, +rev: U32, +rsdt: U32) -> {B.Octets.concat([P.AcpiRsdp.signature(), B.Octets.of_list([0]), F.AcpiF.fit(6n, oem), B.Octets.of_list([rev]), B.Octets.le32(rsdt)]) == B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))) : B.Octets}:
52  %Equal.sym(B.Octets, B.Octets.concat(Con{P.AcpiRsdp.signature(), [B.Octets.of_list([0]), F.AcpiF.fit(6n, oem), B.Octets.of_list([rev]), B.Octets.le32(rsdt)]}), B.Octets.append(P.AcpiRsdp.signature(), B.Octets.concat([B.Octets.of_list([0]), F.AcpiF.fit(6n, oem), B.Octets.of_list([rev]), B.Octets.le32(rsdt)])), BL.octets_concat_cons(P.AcpiRsdp.signature(), [B.Octets.of_list([0]), F.AcpiF.fit(6n, oem), B.Octets.of_list([rev]), B.Octets.le32(rsdt)])) : {_ == B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))) : B.Octets}
53  %Equal.sym(B.Octets, B.Octets.concat(Con{B.Octets.of_list([0]), [F.AcpiF.fit(6n, oem), B.Octets.of_list([rev]), B.Octets.le32(rsdt)]}), B.Octets.append(B.Octets.of_list([0]), B.Octets.concat([F.AcpiF.fit(6n, oem), B.Octets.of_list([rev]), B.Octets.le32(rsdt)])), BL.octets_concat_cons(B.Octets.of_list([0]), [F.AcpiF.fit(6n, oem), B.Octets.of_list([rev]), B.Octets.le32(rsdt)])) : {B.Octets.append(P.AcpiRsdp.signature(), _) == B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))) : B.Octets}
54  %Equal.sym(B.Octets, B.Octets.concat(Con{F.AcpiF.fit(6n, oem), [B.Octets.of_list([rev]), B.Octets.le32(rsdt)]}), B.Octets.append(F.AcpiF.fit(6n, oem), B.Octets.concat([B.Octets.of_list([rev]), B.Octets.le32(rsdt)])), BL.octets_concat_cons(F.AcpiF.fit(6n, oem), [B.Octets.of_list([rev]), B.Octets.le32(rsdt)])) : {B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), _)) == B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))) : B.Octets}
55  %Equal.sym(B.Octets, B.Octets.concat(Con{B.Octets.of_list([rev]), [B.Octets.le32(rsdt)]}), B.Octets.append(B.Octets.of_list([rev]), B.Octets.concat([B.Octets.le32(rsdt)])), BL.octets_concat_cons(B.Octets.of_list([rev]), [B.Octets.le32(rsdt)])) : {B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(F.AcpiF.fit(6n, oem), _))) == B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))) : B.Octets}
56  %Equal.sym(B.Octets, B.Octets.concat(Con{B.Octets.le32(rsdt), Nil{}}), B.Octets.append(B.Octets.le32(rsdt), B.Octets.concat(Nil{})), BL.octets_concat_cons(B.Octets.le32(rsdt), Nil{})) : {B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(F.AcpiF.fit(6n, oem), B.Octets.append(B.Octets.of_list([rev]), _)))) == B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))) : B.Octets}
57  %Equal.sym(B.Octets, B.Octets.concat(Nil{}), B.Octets.empty(), BL.octets_concat_nil()) : {B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(F.AcpiF.fit(6n, oem), B.Octets.append(B.Octets.of_list([rev]), B.Octets.append(B.Octets.le32(rsdt), _))))) == B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))) : B.Octets}
58  %Equal.sym(B.Octets, B.Octets.append(B.Octets.le32(rsdt), B.Octets.empty()), B.Octets.le32(rsdt), BL.octets_append_empty_r(B.Octets.le32(rsdt))) : {B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(F.AcpiF.fit(6n, oem), B.Octets.append(B.Octets.of_list([rev]), _)))) == B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))) : B.Octets}
59  %Equal.sym(B.Octets, F.AcpiF.fit(6n, oem), oem, ckr.fit(oem, oem6)) : {B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(_, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))) == B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))) : B.Octets}
60  {==}