def sq_g

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/secp256k1/fieldpow.bend:298

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/src/crypto/secp256k1/limbs.bend as L
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/consts.bend as K
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/bitsv.bend as BV

298def sq_g(+one: Nat, +h1: {one == 1n : Nat}) -> {Nat.add(Nat.add(FS.digits(one, L.norm16([975n, 0n, 1n])), one), BV.hv(L.cbits(L.bits(L.norm16([975n, 0n, 1n]))), one, 0n)) == Nat.add(Nat.add(FS.digits(one, L.norm16([975n, 0n, 1n])), one), Nat.add(1n+K.pp(one), one)) : Nat}:
299  +d = FS.digits(one, L.norm16([975n, 0n, 1n]))
300  +hv4 = BV.hv(L.cbits(L.bits(L.norm16([975n, 0n, 1n]))), one, 0n)
301  +e1 = Equal.trans(Nat, Nat.add(Nat.add(d, one), hv4), Nat.add(Nat.add(hv4, d), one), C.shift(256n, one), arr3(d, one, hv4), sq_cb(one, h1))
302  +e2 = Equal.trans(Nat, C.shift(256n, one), Nat.add(1n+K.pp(one), FS.cp(one)), Nat.add(1n+K.pp(one), Nat.add(Nat.add(d, one), one)), Equal.sym(Nat, Nat.add(1n+K.pp(one), FS.cp(one)), C.shift(256n, one), K.hm_p(one, h1)), Equal.cong(Nat, Nat, z => Nat.add(1n+K.pp(one), z), FS.cp(one), Nat.add(Nat.add(d, one), one), Equal.sym(Nat, Nat.add(Nat.add(d, one), one), FS.cp(one), yp_digits(one, h1))))
303  Equal.trans(Nat, Nat.add(Nat.add(d, one), hv4), C.shift(256n, one), Nat.add(Nat.add(d, one), Nat.add(1n+K.pp(one), one)), e1, Equal.trans(Nat, C.shift(256n, one), Nat.add(1n+K.pp(one), Nat.add(Nat.add(d, one), one)), Nat.add(Nat.add(d, one), Nat.add(1n+K.pp(one), one)), e2, arr4(1n+K.pp(one), d, one)))