def ckr.w2r

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

import Base
import bend-osdev-word64@0.1.1.1/word64.bend as W
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/rsdp.bend as P

204def ckr.w2r(+k: U32, +oem: B.Octets, +oem6: {B.Octets.len(oem) == 6n : Nat}, +rev: U32, +rsdt: U32, +x: W.W64) -> {B.Octets.concat([B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([k]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.le32(36), B.Octets.le64(x), B.Octets.zeros(4n)]) == B.Octets.append(B.Octets.append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([k]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), B.Octets.le64(x))), B.Octets.append(B.Octets.of_list([0]), B.Octets.zeros(3n))) : B.Octets}:
205  %Equal.sym(B.Octets, B.Octets.concat(Con{B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([k]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), [B.Octets.le32(36), B.Octets.le64(x), B.Octets.zeros(4n)]}), B.Octets.append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([k]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.concat([B.Octets.le32(36), B.Octets.le64(x), B.Octets.zeros(4n)])), BL.octets_concat_cons(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([k]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), [B.Octets.le32(36), B.Octets.le64(x), B.Octets.zeros(4n)])) : {_ == B.Octets.append(B.Octets.append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([k]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), B.Octets.le64(x))), B.Octets.append(B.Octets.of_list([0]), B.Octets.zeros(3n))) : B.Octets}
206  %Equal.sym(B.Octets, B.Octets.concat(Con{B.Octets.le32(36), [B.Octets.le64(x), B.Octets.zeros(4n)]}), B.Octets.append(B.Octets.le32(36), B.Octets.concat([B.Octets.le64(x), B.Octets.zeros(4n)])), BL.octets_concat_cons(B.Octets.le32(36), [B.Octets.le64(x), B.Octets.zeros(4n)])) : {B.Octets.append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([k]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), _) == B.Octets.append(B.Octets.append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([k]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), B.Octets.le64(x))), B.Octets.append(B.Octets.of_list([0]), B.Octets.zeros(3n))) : B.Octets}
207  %Equal.sym(B.Octets, B.Octets.concat(Con{B.Octets.le64(x), [B.Octets.zeros(4n)]}), B.Octets.append(B.Octets.le64(x), B.Octets.concat([B.Octets.zeros(4n)])), BL.octets_concat_cons(B.Octets.le64(x), [B.Octets.zeros(4n)])) : {B.Octets.append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([k]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), _)) == B.Octets.append(B.Octets.append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([k]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), B.Octets.le64(x))), B.Octets.append(B.Octets.of_list([0]), B.Octets.zeros(3n))) : B.Octets}
208  %Equal.sym(B.Octets, B.Octets.concat(Con{B.Octets.zeros(4n), Nil{}}), B.Octets.append(B.Octets.zeros(4n), B.Octets.concat(Nil{})), BL.octets_concat_cons(B.Octets.zeros(4n), Nil{})) : {B.Octets.append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([k]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), B.Octets.append(B.Octets.le64(x), _))) == B.Octets.append(B.Octets.append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([k]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), B.Octets.le64(x))), B.Octets.append(B.Octets.of_list([0]), B.Octets.zeros(3n))) : B.Octets}
209  %Equal.sym(B.Octets, B.Octets.concat(Nil{}), B.Octets.empty(), BL.octets_concat_nil()) : {B.Octets.append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([k]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), B.Octets.append(B.Octets.le64(x), B.Octets.append(B.Octets.zeros(4n), _)))) == B.Octets.append(B.Octets.append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([k]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), B.Octets.le64(x))), B.Octets.append(B.Octets.of_list([0]), B.Octets.zeros(3n))) : B.Octets}
210  %Equal.sym(B.Octets, B.Octets.append(B.Octets.zeros(4n), B.Octets.empty()), B.Octets.zeros(4n), BL.octets_append_empty_r(B.Octets.zeros(4n))) : {B.Octets.append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([k]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), B.Octets.append(B.Octets.le64(x), _))) == B.Octets.append(B.Octets.append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([k]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), B.Octets.le64(x))), B.Octets.append(B.Octets.of_list([0]), B.Octets.zeros(3n))) : B.Octets}
211  %Equal.sym(B.Octets, B.Octets.zeros(4n), B.Octets.append(B.Octets.of_list([0]), B.Octets.zeros(3n)), ckr.z4()) : {B.Octets.append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([k]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), B.Octets.append(B.Octets.le64(x), _))) == B.Octets.append(B.Octets.append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([k]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), B.Octets.le64(x))), B.Octets.append(B.Octets.of_list([0]), B.Octets.zeros(3n))) : B.Octets}
212  %Equal.sym(B.Octets, B.Octets.append(B.Octets.append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([k]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), B.Octets.le64(x))), B.Octets.append(B.Octets.of_list([0]), B.Octets.zeros(3n))), B.Octets.append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([k]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.append(B.Octets.le32(36), B.Octets.le64(x)), B.Octets.append(B.Octets.of_list([0]), B.Octets.zeros(3n)))), BL.octets_append_assoc(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([k]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), B.Octets.le64(x)), B.Octets.append(B.Octets.of_list([0]), B.Octets.zeros(3n)))) : {B.Octets.append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([k]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), B.Octets.append(B.Octets.le64(x), B.Octets.append(B.Octets.of_list([0]), B.Octets.zeros(3n))))) == _ : B.Octets}
213  %Equal.sym(B.Octets, B.Octets.append(B.Octets.append(B.Octets.le32(36), B.Octets.le64(x)), B.Octets.append(B.Octets.of_list([0]), B.Octets.zeros(3n))), B.Octets.append(B.Octets.le32(36), B.Octets.append(B.Octets.le64(x), B.Octets.append(B.Octets.of_list([0]), B.Octets.zeros(3n)))), BL.octets_append_assoc(B.Octets.le32(36), B.Octets.le64(x), B.Octets.append(B.Octets.of_list([0]), B.Octets.zeros(3n)))) : {B.Octets.append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([k]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), B.Octets.append(B.Octets.le32(36), B.Octets.append(B.Octets.le64(x), B.Octets.append(B.Octets.of_list([0]), B.Octets.zeros(3n))))) == B.Octets.append(B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([k]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), _) : B.Octets}
214  {==}