def zeros7

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/secp256k1/scalarpow.bend:104

import Base
import bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend as C
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/field.bend as FS
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/typed/width.bend as WW

104def zeros7(+one: Nat) -> {FS.digits(one, [0n, 0n, 0n, 0n, 0n, 0n, 0n]) == 0n : Nat}:
105  %Equal.sym(Nat, Nat.mul(one, 0n), 0n, NA.mul_zero(one)) : {Nat.add(_, C.shift(16n, Nat.add(Nat.mul(one, 0n), C.shift(16n, Nat.add(Nat.mul(one, 0n), C.shift(16n, Nat.add(Nat.mul(one, 0n), C.shift(16n, Nat.add(Nat.mul(one, 0n), C.shift(16n, Nat.add(Nat.mul(one, 0n), C.shift(16n, Nat.add(Nat.mul(one, 0n), C.shift(16n, 0n)))))))))))))) == 0n : Nat}
106  %Equal.sym(Nat, Nat.mul(one, 0n), 0n, NA.mul_zero(one)) : {Nat.add(0n, C.shift(16n, Nat.add(_, C.shift(16n, Nat.add(Nat.mul(one, 0n), C.shift(16n, Nat.add(Nat.mul(one, 0n), C.shift(16n, Nat.add(Nat.mul(one, 0n), C.shift(16n, Nat.add(Nat.mul(one, 0n), C.shift(16n, Nat.add(Nat.mul(one, 0n), C.shift(16n, 0n)))))))))))))) == 0n : Nat}
107  %Equal.sym(Nat, Nat.mul(one, 0n), 0n, NA.mul_zero(one)) : {Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(_, C.shift(16n, Nat.add(Nat.mul(one, 0n), C.shift(16n, Nat.add(Nat.mul(one, 0n), C.shift(16n, Nat.add(Nat.mul(one, 0n), C.shift(16n, Nat.add(Nat.mul(one, 0n), C.shift(16n, 0n)))))))))))))) == 0n : Nat}
108  %Equal.sym(Nat, Nat.mul(one, 0n), 0n, NA.mul_zero(one)) : {Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(_, C.shift(16n, Nat.add(Nat.mul(one, 0n), C.shift(16n, Nat.add(Nat.mul(one, 0n), C.shift(16n, Nat.add(Nat.mul(one, 0n), C.shift(16n, 0n)))))))))))))) == 0n : Nat}
109  %Equal.sym(Nat, Nat.mul(one, 0n), 0n, NA.mul_zero(one)) : {Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(_, C.shift(16n, Nat.add(Nat.mul(one, 0n), C.shift(16n, Nat.add(Nat.mul(one, 0n), C.shift(16n, 0n)))))))))))))) == 0n : Nat}
110  %Equal.sym(Nat, Nat.mul(one, 0n), 0n, NA.mul_zero(one)) : {Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(_, C.shift(16n, Nat.add(Nat.mul(one, 0n), C.shift(16n, 0n)))))))))))))) == 0n : Nat}
111  %Equal.sym(Nat, Nat.mul(one, 0n), 0n, NA.mul_zero(one)) : {Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(_, C.shift(16n, 0n)))))))))))))) == 0n : Nat}
112  %Equal.sym(Nat, C.shift(16n, 0n), 0n, WW.shift_zero(16n)) : {Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, _))))))))))))) == 0n : Nat}
113  %Equal.sym(Nat, Nat.add(0n, 0n), 0n, {==}) : {Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, _)))))))))))) == 0n : Nat}
114  %Equal.sym(Nat, C.shift(16n, 0n), 0n, WW.shift_zero(16n)) : {Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, _))))))))))) == 0n : Nat}
115  %Equal.sym(Nat, Nat.add(0n, 0n), 0n, {==}) : {Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, _)))))))))) == 0n : Nat}
116  %Equal.sym(Nat, C.shift(16n, 0n), 0n, WW.shift_zero(16n)) : {Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, _))))))))) == 0n : Nat}
117  %Equal.sym(Nat, Nat.add(0n, 0n), 0n, {==}) : {Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, _)))))))) == 0n : Nat}
118  %Equal.sym(Nat, C.shift(16n, 0n), 0n, WW.shift_zero(16n)) : {Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, _))))))) == 0n : Nat}
119  %Equal.sym(Nat, Nat.add(0n, 0n), 0n, {==}) : {Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, _)))))) == 0n : Nat}
120  %Equal.sym(Nat, C.shift(16n, 0n), 0n, WW.shift_zero(16n)) : {Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, _))))) == 0n : Nat}
121  %Equal.sym(Nat, Nat.add(0n, 0n), 0n, {==}) : {Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, _)))) == 0n : Nat}
122  %Equal.sym(Nat, C.shift(16n, 0n), 0n, WW.shift_zero(16n)) : {Nat.add(0n, C.shift(16n, Nat.add(0n, _))) == 0n : Nat}
123  %Equal.sym(Nat, Nat.add(0n, 0n), 0n, {==}) : {Nat.add(0n, C.shift(16n, _)) == 0n : Nat}
124  %Equal.sym(Nat, C.shift(16n, 0n), 0n, WW.shift_zero(16n)) : {Nat.add(0n, _) == 0n : Nat}
125  %Equal.sym(Nat, Nat.add(0n, 0n), 0n, {==}) : {_ == 0n : Nat}
126  {==}