def ckw.p1

bend-osdev-acpi@0.1.2.0 · PROOF_whole.bend:165

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/header.bend as H

165def ckw.p1(+s: B.Octets, +l: U32, +r: U32, +k: U32, +o: B.Octets, +t: B.Octets, +orv: U32, +ci: B.Octets, +cr: U32, +sig4: {B.Octets.len(s) == 4n : Nat}, +body: B.Octets) -> {B.Octets.le32_at(B.Octets.append(H.AcpiHeader.encode(H.AcpiHeader{s, l, r, k, o, t, orv, ci, cr}), body), 4n) == Some{l} : Maybe<&2, U32>}:
166  %Equal.sym(B.Octets, B.Octets.append(H.AcpiHeader.encode(H.AcpiHeader{s, l, r, k, o, t, orv, ci, cr}), body), B.Octets.append(s, B.Octets.append(B.Octets.le32(l), B.Octets.append(H.hd.byte(r), B.Octets.append(H.hd.byte(k), B.Octets.append(o, B.Octets.append(t, B.Octets.append(B.Octets.le32(orv), B.Octets.append(ci, B.Octets.append(B.Octets.le32(cr), body))))))))), ckw.ra(s, l, r, k, o, t, orv, ci, cr, body)) : {B.Octets.le32_at(_, 4n) == Some{l} : Maybe<&2, U32>}
167  %Equal.cong(Nat, Nat, z => Nat.add(z, 0n), B.Octets.len(s), 4n, sig4) : {B.Octets.le32_at(B.Octets.append(s, B.Octets.append(B.Octets.le32(l), B.Octets.append(H.hd.byte(r), B.Octets.append(H.hd.byte(k), B.Octets.append(o, B.Octets.append(t, B.Octets.append(B.Octets.le32(orv), B.Octets.append(ci, B.Octets.append(B.Octets.le32(cr), body))))))))), _) == Some{l} : Maybe<&2, U32>}
168  %Equal.sym(Maybe<&2, U32>, B.Octets.le32_at(B.Octets.append(s, B.Octets.append(B.Octets.le32(l), B.Octets.append(H.hd.byte(r), B.Octets.append(H.hd.byte(k), B.Octets.append(o, B.Octets.append(t, B.Octets.append(B.Octets.le32(orv), B.Octets.append(ci, B.Octets.append(B.Octets.le32(cr), body))))))))), Nat.add(B.Octets.len(s), 0n)), B.Octets.le32_at(B.Octets.append(B.Octets.le32(l), B.Octets.append(H.hd.byte(r), B.Octets.append(H.hd.byte(k), B.Octets.append(o, B.Octets.append(t, B.Octets.append(B.Octets.le32(orv), B.Octets.append(ci, B.Octets.append(B.Octets.le32(cr), body)))))))), 0n), BL.octets_le32_at_append_add(s, B.Octets.append(B.Octets.le32(l), B.Octets.append(H.hd.byte(r), B.Octets.append(H.hd.byte(k), B.Octets.append(o, B.Octets.append(t, B.Octets.append(B.Octets.le32(orv), B.Octets.append(ci, B.Octets.append(B.Octets.le32(cr), body)))))))), 0n)) : {_ == Some{l} : Maybe<&2, U32>}
169  %Equal.sym(Maybe<&2, U32>, B.Octets.le32_at(B.Octets.append(B.Octets.le32(l), B.Octets.append(H.hd.byte(r), B.Octets.append(H.hd.byte(k), B.Octets.append(o, B.Octets.append(t, B.Octets.append(B.Octets.le32(orv), B.Octets.append(ci, B.Octets.append(B.Octets.le32(cr), body)))))))), 0n), B.Octets.le32_at(B.Octets.le32(l), 0n), BL.octets_le32_at_append_le(B.Octets.le32(l), B.Octets.append(H.hd.byte(r), B.Octets.append(H.hd.byte(k), B.Octets.append(o, B.Octets.append(t, B.Octets.append(B.Octets.le32(orv), B.Octets.append(ci, B.Octets.append(B.Octets.le32(cr), body))))))), 0n, ckw.l4(l))) : {_ == Some{l} : Maybe<&2, U32>}
170  BL.octets_le32_round_trip(l)