def xn_digits

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

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

135# c_n + 1
136def xn_digits(+one: Nat, +h1: {one == 1n : Nat}) -> {FS.digits(one, xn()) == Nat.add(FS.cn(one), one) : Nat}:
137  %Equal.sym(Nat, Nat.mul(one, 48832n), Nat.add(one, Nat.mul(one, 48831n)), NA.mul_succ(one, 48831n)) : {Nat.add(_, C.shift(16n, FS.digits(one, [12233n, 41331n, 16429n, 24516n, 20663n, 8985n, 17745n, 1n, 0n, 0n, 0n, 0n, 0n, 0n, 0n]))) == Nat.add(Nat.add(Nat.mul(one, 48831n), C.shift(16n, FS.digits(one, [12233n, 41331n, 16429n, 24516n, 20663n, 8985n, 17745n, 1n]))), one) : Nat}
138  %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]), zeros_tail(one)) : {Nat.add(Nat.add(one, Nat.mul(one, 48831n)), C.shift(16n, _)) == Nat.add(Nat.add(Nat.mul(one, 48831n), C.shift(16n, FS.digits(one, [12233n, 41331n, 16429n, 24516n, 20663n, 8985n, 17745n, 1n]))), one) : Nat}
139  %Equal.sym(Nat, Nat.add(Nat.add(one, Nat.mul(one, 48831n)), C.shift(16n, FS.digits(one, [12233n, 41331n, 16429n, 24516n, 20663n, 8985n, 17745n, 1n]))), Nat.add(one, Nat.add(Nat.mul(one, 48831n), C.shift(16n, FS.digits(one, [12233n, 41331n, 16429n, 24516n, 20663n, 8985n, 17745n, 1n])))), NA.add_assoc(one, Nat.mul(one, 48831n), C.shift(16n, FS.digits(one, [12233n, 41331n, 16429n, 24516n, 20663n, 8985n, 17745n, 1n])))) : {_ == Nat.add(Nat.add(Nat.mul(one, 48831n), C.shift(16n, FS.digits(one, [12233n, 41331n, 16429n, 24516n, 20663n, 8985n, 17745n, 1n]))), one) : Nat}
140  %Equal.sym(Nat, Nat.add(Nat.mul(one, 48831n), C.shift(16n, FS.digits(one, [12233n, 41331n, 16429n, 24516n, 20663n, 8985n, 17745n, 1n]))), Nat.add(C.shift(16n, FS.digits(one, [12233n, 41331n, 16429n, 24516n, 20663n, 8985n, 17745n, 1n])), Nat.mul(one, 48831n)), NA.add_comm(Nat.mul(one, 48831n), C.shift(16n, FS.digits(one, [12233n, 41331n, 16429n, 24516n, 20663n, 8985n, 17745n, 1n])))) : {Nat.add(one, _) == Nat.add(Nat.add(Nat.mul(one, 48831n), C.shift(16n, FS.digits(one, [12233n, 41331n, 16429n, 24516n, 20663n, 8985n, 17745n, 1n]))), one) : Nat}
141  %Equal.sym(Nat, Nat.add(one, Nat.add(C.shift(16n, FS.digits(one, [12233n, 41331n, 16429n, 24516n, 20663n, 8985n, 17745n, 1n])), Nat.mul(one, 48831n))), Nat.add(C.shift(16n, FS.digits(one, [12233n, 41331n, 16429n, 24516n, 20663n, 8985n, 17745n, 1n])), Nat.add(one, Nat.mul(one, 48831n))), NA.add_swap(one, C.shift(16n, FS.digits(one, [12233n, 41331n, 16429n, 24516n, 20663n, 8985n, 17745n, 1n])), Nat.mul(one, 48831n))) : {_ == Nat.add(Nat.add(Nat.mul(one, 48831n), C.shift(16n, FS.digits(one, [12233n, 41331n, 16429n, 24516n, 20663n, 8985n, 17745n, 1n]))), one) : Nat}
142  %Equal.sym(Nat, Nat.add(Nat.mul(one, 48831n), C.shift(16n, FS.digits(one, [12233n, 41331n, 16429n, 24516n, 20663n, 8985n, 17745n, 1n]))), Nat.add(C.shift(16n, FS.digits(one, [12233n, 41331n, 16429n, 24516n, 20663n, 8985n, 17745n, 1n])), Nat.mul(one, 48831n)), NA.add_comm(Nat.mul(one, 48831n), C.shift(16n, FS.digits(one, [12233n, 41331n, 16429n, 24516n, 20663n, 8985n, 17745n, 1n])))) : {Nat.add(C.shift(16n, FS.digits(one, [12233n, 41331n, 16429n, 24516n, 20663n, 8985n, 17745n, 1n])), Nat.add(one, Nat.mul(one, 48831n))) == Nat.add(_, one) : Nat}
143  %Equal.sym(Nat, Nat.add(Nat.add(C.shift(16n, FS.digits(one, [12233n, 41331n, 16429n, 24516n, 20663n, 8985n, 17745n, 1n])), Nat.mul(one, 48831n)), one), Nat.add(C.shift(16n, FS.digits(one, [12233n, 41331n, 16429n, 24516n, 20663n, 8985n, 17745n, 1n])), Nat.add(Nat.mul(one, 48831n), one)), NA.add_assoc(C.shift(16n, FS.digits(one, [12233n, 41331n, 16429n, 24516n, 20663n, 8985n, 17745n, 1n])), Nat.mul(one, 48831n), one)) : {Nat.add(C.shift(16n, FS.digits(one, [12233n, 41331n, 16429n, 24516n, 20663n, 8985n, 17745n, 1n])), Nat.add(one, Nat.mul(one, 48831n))) == _ : Nat}
144  %Equal.sym(Nat, Nat.add(Nat.mul(one, 48831n), one), Nat.add(one, Nat.mul(one, 48831n)), NA.add_comm(Nat.mul(one, 48831n), one)) : {Nat.add(C.shift(16n, FS.digits(one, [12233n, 41331n, 16429n, 24516n, 20663n, 8985n, 17745n, 1n])), Nat.add(one, Nat.mul(one, 48831n))) == Nat.add(C.shift(16n, FS.digits(one, [12233n, 41331n, 16429n, 24516n, 20663n, 8985n, 17745n, 1n])), _) : Nat}
145  {==}