def uand

bend-collections-laws-crypto@1.0.0.0 · proofs/math/random/bits.bend:93

import Base
import bend-collections-laws-crypto@1.0.0.0/spec/math/random/rand.bend as SR

93def uand(+x: U32, +y: U32) -> {U32.to_nat(U32.and(x, y)) == SR.and_bits(32n, U32.to_nat(x), U32.to_nat(y)) : Nat}:
94  match x y:
95    case U32{+a} U32{+b}:
96      wand(32n, a, b)