def wand

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

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

77# THEOREM: Word.and is and_bits on the values
78def wand(+n: Nat, +a: Word(n), +b: Word(n)) -> {Word.to_nat(n, Word.and(n, a, b)) == SR.and_bits(n, Word.to_nat(n, a), Word.to_nat(n, b)) : Nat}:
79  match n a b:
80    case 0n WNil{} WNil{}:
81      {==}
82    case 1n+p WCon{+x, +t} WCon{+y, +u}:
83      +e1 = to_nat_con(p, Bool.and(x, y), Word.and(p, t, u))
84      +e2 = Equal.cong(Nat, Nat, z => Nat.add(bv(Bool.and(x, y)), Nat.double(z)), Word.to_nat(p, Word.and(p, t, u)), SR.and_bits(p, Word.to_nat(p, t), Word.to_nat(p, u)), wand(p, t, u))
85      +e3 = Equal.cong(Nat, Nat, z => Nat.add(z, Nat.double(SR.and_bits(p, Word.to_nat(p, t), Word.to_nat(p, u)))), bv(Bool.and(x, y)), Nat.mul(bv(x), bv(y)), bv_and(x, y))
86      +e4 = Equal.sym(Nat, SR.and_bits(1n+p, Nat.add(bv(x), Nat.double(Word.to_nat(p, t))), Nat.add(bv(y), Nat.double(Word.to_nat(p, u)))), Nat.add(Nat.mul(bv(x), bv(y)), Nat.double(SR.and_bits(p, Word.to_nat(p, t), Word.to_nat(p, u)))), and_step(p, bv(x), Word.to_nat(p, t), bv(y), Word.to_nat(p, u), bv_le(x), bv_le(y)))
87      %Equal.sym(Nat, Word.to_nat(1n+p, WCon{x, t}), Nat.add(bv(x), Nat.double(Word.to_nat(p, t))), to_nat_con(p, x, t)) : {Word.to_nat(1n+p, WCon{Bool.and(x, y), Word.and(p, t, u)}) == SR.and_bits(1n+p, _, Word.to_nat(1n+p, WCon{y, u})) : Nat}
88      %Equal.sym(Nat, Word.to_nat(1n+p, WCon{y, u}), Nat.add(bv(y), Nat.double(Word.to_nat(p, u))), to_nat_con(p, y, u)) : {Word.to_nat(1n+p, WCon{Bool.and(x, y), Word.and(p, t, u)}) == SR.and_bits(1n+p, Nat.add(bv(x), Nat.double(Word.to_nat(p, t))), _) : Nat}
89      Equal.trans(Nat, Word.to_nat(1n+p, WCon{Bool.and(x, y), Word.and(p, t, u)}), Nat.add(bv(Bool.and(x, y)), Nat.double(Word.to_nat(p, Word.and(p, t, u)))), SR.and_bits(1n+p, Nat.add(bv(x), Nat.double(Word.to_nat(p, t))), Nat.add(bv(y), Nat.double(Word.to_nat(p, u)))), e1,
90        Equal.trans(Nat, Nat.add(bv(Bool.and(x, y)), Nat.double(Word.to_nat(p, Word.and(p, t, u)))), Nat.add(bv(Bool.and(x, y)), Nat.double(SR.and_bits(p, Word.to_nat(p, t), Word.to_nat(p, u)))), SR.and_bits(1n+p, Nat.add(bv(x), Nat.double(Word.to_nat(p, t))), Nat.add(bv(y), Nat.double(Word.to_nat(p, u)))), e2,
91          Equal.trans(Nat, Nat.add(bv(Bool.and(x, y)), Nat.double(SR.and_bits(p, Word.to_nat(p, t), Word.to_nat(p, u)))), Nat.add(Nat.mul(bv(x), bv(y)), Nat.double(SR.and_bits(p, Word.to_nat(p, t), Word.to_nat(p, u)))), SR.and_bits(1n+p, Nat.add(bv(x), Nat.double(Word.to_nat(p, t))), Nat.add(bv(y), Nat.double(Word.to_nat(p, u)))), e3, e4)))