def cn_fe_v

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/secp256k1/rconst.bend:26

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/ecdsa.bend as E
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/scalarpow.bend as SP

26def cn_fe_v(+one: Nat) -> {FS.value(one, E.cn_fe()) == FS.cn(one) : Nat}:
27  %Equal.sym(Nat, FS.digits(one, [12233n, 41331n, 16429n, 24516n, 20663n, 8985n, 17745n, 1n, 0n, 0n, 0n, 0n, 0n, 0n, 0n]), FS.digits(one, [12233n, 41331n, 16429n, 24516n, 20663n, 8985n, 17745n, 1n]), SP.zeros_tail(one)) : {Nat.add(Nat.mul(one, 48831n), C.shift(16n, _)) == Nat.add(Nat.mul(one, 48831n), C.shift(16n, FS.digits(one, [12233n, 41331n, 16429n, 24516n, 20663n, 8985n, 17745n, 1n]))) : Nat}
28  {==}