def sq_pow

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/curve25519/pow.bend:144

import Base
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as NA
import bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/arith.bend as NR

144# (a^2 y)^(2^m) z == a^(2^(m+1)) (y^(2^m) z)
145def sq_pow(+a: Nat, +y: Nat, +s: Nat, +z: Nat, +s2: Nat, +hs: {Nat.add(s, s) == s2 : Nat}) -> {Nat.mul(Nat.pow(Nat.mul(Nat.mul(a, a), y), s), z) == Nat.mul(Nat.pow(a, s2), Nat.mul(Nat.pow(y, s), z)) : Nat}:
146  +e1 = Equal.cong(Nat, Nat, t => Nat.mul(t, z), Nat.pow(Nat.mul(Nat.mul(a, a), y), s), Nat.mul(Nat.pow(Nat.mul(a, a), s), Nat.pow(y, s)), NR.mul_pow(Nat.mul(a, a), y, s))
147  +e2a = Equal.trans(Nat, Nat.pow(Nat.mul(a, a), s), Nat.mul(Nat.pow(a, s), Nat.pow(a, s)), Nat.pow(a, s2), NR.mul_pow(a, a, s), Equal.trans(Nat, Nat.mul(Nat.pow(a, s), Nat.pow(a, s)), Nat.pow(a, Nat.add(s, s)), Nat.pow(a, s2), Equal.sym(Nat, Nat.pow(a, Nat.add(s, s)), Nat.mul(Nat.pow(a, s), Nat.pow(a, s)), NR.pow_add(a, s, s)), Equal.cong(Nat, Nat, t => Nat.pow(a, t), Nat.add(s, s), s2, hs)))
148  +e2 = Equal.cong(Nat, Nat, t => Nat.mul(Nat.mul(t, Nat.pow(y, s)), z), Nat.pow(Nat.mul(a, a), s), Nat.pow(a, s2), e2a)
149  +e3 = NA.mul_assoc(Nat.pow(a, s2), Nat.pow(y, s), z)
150  Equal.trans(Nat, Nat.mul(Nat.pow(Nat.mul(Nat.mul(a, a), y), s), z), Nat.mul(Nat.mul(Nat.pow(Nat.mul(a, a), s), Nat.pow(y, s)), z), Nat.mul(Nat.pow(a, s2), Nat.mul(Nat.pow(y, s), z)), e1, Equal.trans(Nat, Nat.mul(Nat.mul(Nat.pow(Nat.mul(a, a), s), Nat.pow(y, s)), z), Nat.mul(Nat.mul(Nat.pow(a, s2), Nat.pow(y, s)), z), Nat.mul(Nat.pow(a, s2), Nat.mul(Nat.pow(y, s), z)), e2, e3))