def ckp.nsapp

bend-osdev-acpi@0.1.2.0 · PROOF_checksum.bend:166

import Base
import bend-osdev-bytes@0.1.1.1/bytes.bend as B
import bend-osdev-u32@0.1.0.0/LAWS.bend as UL

166def ckp.nsapp(+xs: List<&2, U32>, +ys: List<&2, U32>) -> {ckp.ns(B.append(xs, ys)) == Nat.add(ckp.ns(xs), ckp.ns(ys)) : Nat}:
167  match xs:
168    case Nil{}:
169      {==}
170    case Con{+h, +t}:
171      %Equal.sym(Nat, ckp.ns(B.append(t, ys)), Nat.add(ckp.ns(t), ckp.ns(ys)), ckp.nsapp(t, ys)) : {Nat.add(U32.to_nat(U32.and(255, h)), _) == Nat.add(ckp.ns(Con{h, t}), ckp.ns(ys)) : Nat}
172      Equal.sym(Nat, Nat.add(Nat.add(U32.to_nat(U32.and(255, h)), ckp.ns(t)), ckp.ns(ys)), Nat.add(U32.to_nat(U32.and(255, h)), Nat.add(ckp.ns(t), ckp.ns(ys))), UL.nat_add_assoc(U32.to_nat(U32.and(255, h)), ckp.ns(t), ckp.ns(ys)))