def and64_value

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

import Base
import bend-collections-laws-math@1.0.0.0/spec/lib/common.bend as C
import bend-collections-laws-math@1.0.0.0/spec/math/w64.bend as SW
import bend-collections-laws-math@1.0.0.0/spec/math/random/rand.bend as SR
import bend-collections-laws-math@1.0.0.0/src/math/u64.bend as WU
import bend-collections-laws-math@1.0.0.0/src/math/random/rand.bend as R
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64add.bend as WA

119# THEOREM: the 64-bit and of rand.bend is and_bits on the values
120def and64_value(+a: WU.U64, +b: WU.U64) -> {SW.value(R.and64(a, b)) == SR.and_bits(64n, SW.value(a), SW.value(b)) : Nat}:
121  match a b:
122    case WU.U64{+al, +ah} WU.U64{+bl, +bh}:
123      %Equal.sym(Nat, U32.to_nat(U32.and(al, bl)), SR.and_bits(32n, U32.to_nat(al), U32.to_nat(bl)), uand(al, bl)) : {Nat.add(_, C.shift(32n, U32.to_nat(U32.and(ah, bh)))) == SR.and_bits(64n, SW.value(WU.U64{al, ah}), SW.value(WU.U64{bl, bh})) : Nat}
124      %Equal.sym(Nat, U32.to_nat(U32.and(ah, bh)), SR.and_bits(32n, U32.to_nat(ah), U32.to_nat(bh)), uand(ah, bh)) : {Nat.add(SR.and_bits(32n, U32.to_nat(al), U32.to_nat(bl)), C.shift(32n, _)) == SR.and_bits(64n, SW.value(WU.U64{al, ah}), SW.value(WU.U64{bl, bh})) : Nat}
125      Equal.sym(Nat, SR.and_bits(64n, SW.value(WU.U64{al, ah}), SW.value(WU.U64{bl, bh})), Nat.add(SR.and_bits(32n, U32.to_nat(al), U32.to_nat(bl)), C.shift(32n, SR.and_bits(32n, U32.to_nat(ah), U32.to_nat(bh)))), and_join(32n, 32n, U32.to_nat(al), U32.to_nat(ah), U32.to_nat(bl), U32.to_nat(bh), WA.vb(al), WA.vb(bl)))