~/jendhub

def ckp.e1g

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

import bend-osdev-acpi@0.1.2.0/PROOF_checksum.bend as PROOFChecksum
import Base
import bend-osdev-u32@0.1.0.0/u32.bend as U
import bend-osdev-u32@0.1.0.0/LAWS.bend as UL

246def ckp.e1g(+so: U32, +b: U32, +n: Nat, +ev: {U32.to_nat(so) == U.U32Nat.low(8n, n) : Nat}) -> {U.U32Nat.low(8n, Nat.add(U32.to_nat(U32.and(255, U32.sub(so, b))), U32.to_nat(b))) == U.U32Nat.low(8n, n) : Nat}:
247  %Equal.sym(Nat, U32.to_nat(U32.and(255, U32.sub(so, b))), U.U32Nat.low(8n, U32.to_nat(U32.sub(so, b))), ckp.am(U32.sub(so, b))) : {U.U32Nat.low(8n, Nat.add(_, U32.to_nat(b))) == U.U32Nat.low(8n, n) : Nat}
248  %ckp.l1(U32.to_nat(U32.sub(so, b)), U32.to_nat(b)) : {_ == U.U32Nat.low(8n, n) : Nat}
249  %Equal.sym(Nat, Nat.add(U32.to_nat(U32.sub(so, b)), U32.to_nat(b)), Nat.add(U32.to_nat(so), U.U32Nat.dbl(32n, U.U32Nat.bit(U32.is_lt(so, b)))), UL.u32_sub_wrap(so, b)) : {U.U32Nat.low(8n, _) == U.U32Nat.low(8n, n) : Nat}
250  %Equal.sym(Nat, U.U32Nat.low(8n, Nat.add(U32.to_nat(so), U.U32Nat.dbl(32n, U.U32Nat.bit(U32.is_lt(so, b))))), U.U32Nat.low(8n, U32.to_nat(so)), ckp.l2(U32.to_nat(so), U.U32Nat.bit(U32.is_lt(so, b)))) : {_ == U.U32Nat.low(8n, n) : Nat}
251  %Equal.sym(Nat, U32.to_nat(so), U.U32Nat.low(8n, n), ev) : {U.U32Nat.low(8n, _) == U.U32Nat.low(8n, n) : Nat}
252  ckp.ll(n)

Uses (16)

Used by (1)