def ckp.one

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

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

177def ckp.one(+l: List<&2, U32>, +hl: {B.len(l) == 1n : Nat}) -> {ckp.ns(l) == U32.to_nat(U32.and(255, Maybe.default(&2, U32, B.at(l, 0n), 0))) : Nat}:
178  match l:
179    case Nil{}:
180      Empty.absurd({ckp.ns(Nil{}) == U32.to_nat(U32.and(255, Maybe.default(&2, U32, B.at(Nil{}, 0n), 0))) : Nat}, ckp.nz0(hl))
181    case Con{+h, +t}:
182      match t:
183        case Nil{}:
184          %Equal.sym(U32, U32.and(255, B.byte(h)), U32.and(255, h), ckp.bb3(h)) : {Nat.add(U32.to_nat(U32.and(255, h)), 0n) == U32.to_nat(_) : Nat}
185          UL.nat_add_zero(U32.to_nat(U32.and(255, h)))
186        case Con{h2, t2}:
187          Empty.absurd({ckp.ns(Con{h, Con{h2, t2}}) == U32.to_nat(U32.and(255, Maybe.default(&2, U32, B.at(Con{h, Con{h2, t2}}, 0n), 0))) : Nat}, ckp.nz1(B.len(t2), hl))