Fieldpow.sq_g: def of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/fieldpow.bend as Fieldpow
Lines 298-303 of bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/fieldpow.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/fieldpow.bend&start_line=298&end_line=303

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

def 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}:
  +d = FS.digits(one, L.norm16([975n, 0n, 1n]))
  +hv4 = BV.hv(L.cbits(L.bits(L.norm16([975n, 0n, 1n]))), one, 0n)
  +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))
  +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))))
  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)))

Uses (19):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.add
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/bitsv.bend&name=hv
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/consts.bend&name=hm_p
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/consts.bend&name=pp
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/fieldpow.bend&name=arr3
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/fieldpow.bend&name=arr4
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/fieldpow.bend&name=sq_cb
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/fieldpow.bend&name=yp_digits
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/field.bend&name=cp
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/field.bend&name=digits
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend&name=shift
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/limbs.bend&name=bits
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/limbs.bend&name=cbits
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/limbs.bend&name=norm16