def ckp.l2

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

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

99def ckp.l2(+z: Nat, +k: Nat) -> {U.U32Nat.low(8n, Nat.add(z, U.U32Nat.dbl(32n, k))) == U.U32Nat.low(8n, z) : Nat}:
100  %UL.dbl_dbl(8n, 24n, k) : {U.U32Nat.low(8n, Nat.add(z, _)) == U.U32Nat.low(8n, z) : Nat}
101  UL.low_add_dbl(8n, z, U.U32Nat.dbl(24n, k))

Uses (6)

Used by (3)