def zeros_tail

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

import Base
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/limbs.bend as LV
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/consts.bend as K

128# the trailing zero limbs add nothing
129def zeros_tail(+one: 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]) : Nat}:
130  %Equal.sym(Nat, FS.digits(one, [12233n, 41331n, 16429n, 24516n, 20663n, 8985n, 17745n, 1n, 0n, 0n, 0n, 0n, 0n, 0n, 0n]), Nat.add(FS.digits(one, L.take(8n, [12233n, 41331n, 16429n, 24516n, 20663n, 8985n, 17745n, 1n, 0n, 0n, 0n, 0n, 0n, 0n, 0n])), LV.pos(8n, FS.digits(one, L.drop(8n, [12233n, 41331n, 16429n, 24516n, 20663n, 8985n, 17745n, 1n, 0n, 0n, 0n, 0n, 0n, 0n, 0n])))), K.digits_split(one, 8n, [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]) : Nat}
131  %Equal.sym(Nat, FS.digits(one, [12233n, 41331n, 16429n, 24516n, 20663n, 8985n, 17745n, 1n]), Nat.add(FS.digits(one, L.take(8n, [12233n, 41331n, 16429n, 24516n, 20663n, 8985n, 17745n, 1n])), LV.pos(8n, FS.digits(one, L.drop(8n, [12233n, 41331n, 16429n, 24516n, 20663n, 8985n, 17745n, 1n])))), K.digits_split(one, 8n, [12233n, 41331n, 16429n, 24516n, 20663n, 8985n, 17745n, 1n])) : {Nat.add(FS.digits(one, L.take(8n, [12233n, 41331n, 16429n, 24516n, 20663n, 8985n, 17745n, 1n, 0n, 0n, 0n, 0n, 0n, 0n, 0n])), LV.pos(8n, FS.digits(one, L.drop(8n, [12233n, 41331n, 16429n, 24516n, 20663n, 8985n, 17745n, 1n, 0n, 0n, 0n, 0n, 0n, 0n, 0n])))) == _ : Nat}
132  %Equal.sym(Nat, FS.digits(one, [0n, 0n, 0n, 0n, 0n, 0n, 0n]), 0n, zeros7(one)) : {Nat.add(FS.digits(one, [12233n, 41331n, 16429n, 24516n, 20663n, 8985n, 17745n, 1n]), LV.pos(8n, _)) == Nat.add(FS.digits(one, [12233n, 41331n, 16429n, 24516n, 20663n, 8985n, 17745n, 1n]), LV.pos(8n, 0n)) : Nat}
133  {==}