def and32

bend-collections-laws-crypto@1.0.0.0 · proofs/math/u64/u64div.bend:68

import Base
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend as L
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/word.bend as WD
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/u32div.bend as UD

68def and32(+k: Nat, +x: U32, +m: U32, +hm: {m == U32{WD.mask(32n, k)} : U32}) -> {UD.v(x) == Nat.add(UD.v(U32.and(x, m)), WD.sc(k, hp32(k, x))) : Nat}:
69  L.subst(U32, z => {UD.v(x) == Nat.add(UD.v(U32.and(x, z)), WD.sc(k, hp32(k, x))) : Nat}, U32{WD.mask(32n, k)}, m, Equal.sym(U32, m, U32{WD.mask(32n, k)}, hm), and32w(k, x))