def ckr.sl9

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

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/rsdp.bend as P

106def ckr.sl9(+k: U32, +oem: B.Octets, +oem6: {B.Octets.len(oem) == 6n : Nat}, +rev: U32, +rsdt: U32) -> {B.Octets.slice(9n, 6n, 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)))))) == oem : B.Octets}:
107  %Equal.sym(B.Octets, B.Octets.slice(Nat.add(B.Octets.len(P.AcpiRsdp.signature()), 1n), 6n, 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.slice(1n, 6n, B.Octets.append(B.Octets.of_list([k]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))), BL.octets_slice_append_add(P.AcpiRsdp.signature(), 1n, 6n, B.Octets.append(B.Octets.of_list([k]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt)))))) : {_ == oem : B.Octets}
108  %Equal.cong(Nat, Nat, z => Nat.add(z, 0n), B.Octets.len(B.Octets.of_list([k])), B.len([k]), BL.octets_len_of_list([k])) : {B.Octets.slice(_, 6n, B.Octets.append(B.Octets.of_list([k]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))) == oem : B.Octets}
109  %Equal.sym(B.Octets, B.Octets.slice(Nat.add(B.Octets.len(B.Octets.of_list([k])), 0n), 6n, 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.slice(0n, 6n, B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt)))), BL.octets_slice_append_add(B.Octets.of_list([k]), 0n, 6n, B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))) : {_ == oem : B.Octets}
110  %Equal.sym(B.Octets, B.Octets.slice(0n, 6n, B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt)))), B.Octets.slice(0n, 6n, oem), BL.octets_slice_append_le(0n, 6n, oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt)), ckr.le6(oem, oem6))) : {_ == oem : B.Octets}
111  %Equal.sym(B.Octets, B.Octets.drop(0n, oem), oem, BL.octets_drop_zero(oem)) : {B.Octets.take(6n, _) == oem : B.Octets}
112  %oem6 : {B.Octets.take(_, oem) == oem : B.Octets}
113  BL.octets_take_len(oem)