def ckw.plen

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

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

117def ckw.plen(+s: B.Octets, +l: U32, +r: U32, +sig4: {B.Octets.len(s) == 4n : Nat}) -> {B.Octets.len(B.Octets.append(s, B.Octets.append(B.Octets.le32(l), H.hd.byte(r)))) == 9n : Nat}:
118  %Equal.sym(Nat, B.Octets.len(B.Octets.append(s, B.Octets.append(B.Octets.le32(l), H.hd.byte(r)))), Nat.add(B.Octets.len(s), B.Octets.len(B.Octets.append(B.Octets.le32(l), H.hd.byte(r)))), BL.octets_len_append(s, B.Octets.append(B.Octets.le32(l), H.hd.byte(r)))) : {_ == 9n : Nat}
119  %Equal.sym(Nat, B.Octets.len(B.Octets.append(B.Octets.le32(l), H.hd.byte(r))), Nat.add(B.Octets.len(B.Octets.le32(l)), B.Octets.len(H.hd.byte(r))), BL.octets_len_append(B.Octets.le32(l), H.hd.byte(r))) : {Nat.add(B.Octets.len(s), _) == 9n : Nat}
120  %Equal.sym(Nat, B.Octets.len(s), 4n, sig4) : {Nat.add(_, Nat.add(B.Octets.len(B.Octets.le32(l)), B.Octets.len(H.hd.byte(r)))) == 9n : Nat}
121  %Equal.sym(Nat, B.Octets.len(B.Octets.le32(l)), 4n, BL.octets_len_le32(l)) : {Nat.add(4n, Nat.add(_, B.Octets.len(H.hd.byte(r)))) == 9n : Nat}
122  %Equal.sym(Nat, B.Octets.len(B.Octets.of_list([r])), B.len([r]), BL.octets_len_of_list([r])) : {Nat.add(4n, Nat.add(4n, _)) == 9n : Nat}
123  {==}