~/jendhub

proofs/crypto/secp256k1/scalarpow.bend

bend-collections-laws-crypto@1.0.0.0 · 218 lines · 27 definitions

1# GENERATED by tools/generators/rw.py from ../../../tools/generators/secp256k1_hand/scalarpow.src; edit the .src
2import Base
3import bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend as C
4import bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/field.bend as FS
5import bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/limbs.bend as L
6import bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/scalar.bend as S
7import bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend as N
8import bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend as Lg
9import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as NA
10import bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/arith.bend as NR
11import bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/width.bend as WW
12import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/semiring.bend as SR
13import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/limbs.bend as LV
14import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/ineq.bend as I
15import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/consts.bend as K
16import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/bitsv.bend as BV
17import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/modexp.bend as ME
18import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/scalarops.bend as SO
19import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/lits.bend as LT
20
21# Exponentiation modulo n (src/crypto/secp256k1/scalar.bend pow, inv):
22# square-and-multiply over the exponent's bits computes x^e mod n, and the
23# bits of inv spell n - 2.
24
25def m(+one: Nat) -> Nat:
26  1n+K.np(one)
27
28# one square-and-multiply step
29def step_e(+one: Nat, +h1: {one == 1n : Nat}, +x: List<&2, Nat>, +hx: {FS.reduced(one, FS.order(one), x) == True{} : Bool}, +acc: List<&2, Nat>, +ha: {FS.reduced(one, FS.order(one), acc) == True{} : Bool}, +e: Nat, +he: {LV.ev(acc) == Nat.mod(Nat.pow(LV.ev(x), e), 1n+K.np(one)) : Nat}, b: Nat, +hb: {Nat.is_lt(b, 2n) == True{} : Bool}) -> {LV.ev(S.pow_step(b, x, S.mul(acc, acc))) == Nat.mod(Nat.pow(LV.ev(x), Nat.add(Nat.mul(b, one), Nat.double(e))), 1n+K.np(one)) : Nat}:
30  match b:
31    case 0n:
32      %Equal.sym(Nat, LV.ev(S.mul(acc, acc)), Nat.mod(Nat.mul(LV.ev(acc), LV.ev(acc)), 1n+K.np(one)), SO.mul_e(one, h1, acc, acc, ha, ha)) : {_ == Nat.mod(Nat.pow(LV.ev(x), Nat.double(e)), 1n+K.np(one)) : Nat}
33      ME.sq_step(K.np(one), LV.ev(x), e, LV.ev(acc), he)
34    case 1n:
35      +sq = S.mul(acc, acc)
36      +es = Equal.trans(Nat, LV.ev(sq), Nat.mod(Nat.mul(LV.ev(acc), LV.ev(acc)), 1n+K.np(one)), Nat.mod(Nat.pow(LV.ev(x), Nat.double(e)), 1n+K.np(one)), SO.mul_e(one, h1, acc, acc, ha, ha), ME.sq_step(K.np(one), LV.ev(x), e, LV.ev(acc), he))
37      %Equal.sym(Nat, Nat.mul(1n, one), one, SR.one_mul(one)) : {LV.ev(S.mul(S.mul(acc, acc), x)) == Nat.mod(Nat.pow(LV.ev(x), Nat.add(_, Nat.double(e))), 1n+K.np(one)) : Nat}
38      %Equal.sym(Nat, one, 1n, h1) : {LV.ev(S.mul(S.mul(acc, acc), x)) == Nat.mod(Nat.pow(LV.ev(x), Nat.add(_, Nat.double(e))), 1n+K.np(one)) : Nat}
39      %Equal.sym(Nat, Nat.add(1n, Nat.double(e)), Nat.add(Nat.double(e), 1n), NA.add_comm(1n, Nat.double(e))) : {LV.ev(S.mul(S.mul(acc, acc), x)) == Nat.mod(Nat.pow(LV.ev(x), _), 1n+K.np(one)) : Nat}
40      %Equal.sym(Nat, LV.ev(S.mul(S.mul(acc, acc), x)), Nat.mod(Nat.mul(LV.ev(S.mul(acc, acc)), LV.ev(x)), 1n+K.np(one)), SO.mul_e(one, h1, S.mul(acc, acc), x, SO.mul_r(one, h1, acc, acc, ha, ha), hx)) : {_ == Nat.mod(Nat.pow(LV.ev(x), Nat.add(Nat.double(e), 1n)), 1n+K.np(one)) : Nat}
41      ME.mul_step(K.np(one), LV.ev(x), Nat.double(e), LV.ev(S.mul(acc, acc)), es)
42    case 2n+ +k:
43      Empty.absurd({LV.ev(S.pow_step(2n+k, x, S.mul(acc, acc))) == Nat.mod(Nat.pow(LV.ev(x), Nat.add(Nat.mul(2n+k, one), Nat.double(e))), 1n+K.np(one)) : Nat}, N.lt_zero_absurd(k, hb))
44
45def step_r(+one: Nat, +h1: {one == 1n : Nat}, +x: List<&2, Nat>, +hx: {FS.reduced(one, FS.order(one), x) == True{} : Bool}, +acc: List<&2, Nat>, +ha: {FS.reduced(one, FS.order(one), acc) == True{} : Bool}, b: Nat, +hb: {Nat.is_lt(b, 2n) == True{} : Bool}) -> {FS.reduced(one, FS.order(one), S.pow_step(b, x, S.mul(acc, acc))) == True{} : Bool}:
46  match b:
47    case 0n:
48      SO.mul_r(one, h1, acc, acc, ha, ha)
49    case 1n:
50      SO.mul_r(one, h1, S.mul(acc, acc), x, SO.mul_r(one, h1, acc, acc, ha, ha), hx)
51    case 2n+ +k:
52      Empty.absurd({FS.reduced(one, FS.order(one), S.pow_step(2n+k, x, S.mul(acc, acc))) == True{} : Bool}, N.lt_zero_absurd(k, hb))
53
54def pow_r(+one: Nat, +h1: {one == 1n : Nat}, +x: List<&2, Nat>, +hx: {FS.reduced(one, FS.order(one), x) == True{} : Bool}, bs: List<&2, Nat>, +acc: List<&2, Nat>, +ha: {FS.reduced(one, FS.order(one), acc) == True{} : Bool}, +hb: {BV.all01(bs) == True{} : Bool}) -> {FS.reduced(one, FS.order(one), S.pow_go(x, bs, acc)) == True{} : Bool}:
55  match bs:
56    case Nil{}:
57      ha
58    case +b <> +t:
59      +h0 = Lg.and_left(Nat.is_lt(b, 2n), BV.all01(t), hb)
60      pow_r(one, h1, x, hx, t, S.pow_step(b, x, S.mul(acc, acc)), step_r(one, h1, x, hx, acc, ha, b, h0), Lg.and_right(Nat.is_lt(b, 2n), BV.all01(t), hb))
61
62# x^e for the exponent spelled by the bits, from acc = x^e0
63def pow_e(+one: Nat, +h1: {one == 1n : Nat}, +x: List<&2, Nat>, +hx: {FS.reduced(one, FS.order(one), x) == True{} : Bool}, bs: List<&2, Nat>, +acc: List<&2, Nat>, +ha: {FS.reduced(one, FS.order(one), acc) == True{} : Bool}, +e: Nat, +he: {LV.ev(acc) == Nat.mod(Nat.pow(LV.ev(x), e), 1n+K.np(one)) : Nat}, +hb: {BV.all01(bs) == True{} : Bool}) -> {LV.ev(S.pow_go(x, bs, acc)) == Nat.mod(Nat.pow(LV.ev(x), BV.hv(bs, one, e)), 1n+K.np(one)) : Nat}:
64  match bs:
65    case Nil{}:
66      he
67    case +b <> +t:
68      +h0 = Lg.and_left(Nat.is_lt(b, 2n), BV.all01(t), hb)
69      pow_e(one, h1, x, hx, t, S.pow_step(b, x, S.mul(acc, acc)), step_r(one, h1, x, hx, acc, ha, b, h0), Nat.add(Nat.mul(b, one), Nat.double(e)), step_e(one, h1, x, hx, acc, ha, e, he, b, h0), Lg.and_right(Nat.is_lt(b, 2n), BV.all01(t), hb))
70
71# S.pow looks at x first
72def pow_is(+one: Nat, x: List<&2, Nat>, +hx: {FS.reduced(one, FS.order(one), x) == True{} : Bool}, +bs: List<&2, Nat>, +acc: List<&2, Nat>) -> {S.pow(x, bs, acc) == S.pow_go(x, bs, acc) : List<&2, Nat>}:
73  match x:
74    case Nil{}:
75      Empty.absurd({S.pow([], bs, acc) == S.pow_go([], bs, acc) : List<&2, Nat>}, Lg.false_true(Lg.and_left(FS.limbs16(one, 16n, []), Nat.is_lt(FS.value(one, []), FS.order(one)), hx)))
76    case y <> t:
77      {==}
78
79def pow_ev(+one: Nat, +h1: {one == 1n : Nat}, +x: List<&2, Nat>, +hx: {FS.reduced(one, FS.order(one), x) == True{} : Bool}, +bs: List<&2, Nat>, +acc: List<&2, Nat>, +ha: {FS.reduced(one, FS.order(one), acc) == True{} : Bool}, +e: Nat, +he: {LV.ev(acc) == Nat.mod(Nat.pow(LV.ev(x), e), 1n+K.np(one)) : Nat}, +hb: {BV.all01(bs) == True{} : Bool}) -> {LV.ev(S.pow(x, bs, acc)) == Nat.mod(Nat.pow(LV.ev(x), BV.hv(bs, one, e)), 1n+K.np(one)) : Nat}:
80  %Equal.sym(List<&2, Nat>, S.pow(x, bs, acc), S.pow_go(x, bs, acc), pow_is(one, x, hx, bs, acc)) : {LV.ev(_) == Nat.mod(Nat.pow(LV.ev(x), BV.hv(bs, one, e)), 1n+K.np(one)) : Nat}
81  pow_e(one, h1, x, hx, bs, acc, ha, e, he, hb)
82
83def pow_rv(+one: Nat, +h1: {one == 1n : Nat}, +x: List<&2, Nat>, +hx: {FS.reduced(one, FS.order(one), x) == True{} : Bool}, +bs: List<&2, Nat>, +acc: List<&2, Nat>, +ha: {FS.reduced(one, FS.order(one), acc) == True{} : Bool}, +hb: {BV.all01(bs) == True{} : Bool}) -> {FS.reduced(one, FS.order(one), S.pow(x, bs, acc)) == True{} : Bool}:
84  %Equal.sym(List<&2, Nat>, S.pow(x, bs, acc), S.pow_go(x, bs, acc), pow_is(one, x, hx, bs, acc)) : {FS.reduced(one, FS.order(one), _) == True{} : Bool}
85  pow_r(one, h1, x, hx, bs, acc, ha, hb)
86
87# ---- one ----
88
89def one_lt(+one: Nat, +h1: {one == 1n : Nat}) -> {Nat.is_lt(1n, FS.order(one)) == True{} : Bool}:
90  SO.small_lt_n(one, h1, 1n, {==})
91
92def one_r(+one: Nat, +h1: {one == 1n : Nat}) -> {FS.reduced(one, FS.order(one), S.one()) == True{} : Bool}:
93  SO.small_r(one, h1, 1n, one_lt(one, h1))
94
95def one_e(+one: Nat, +h1: {one == 1n : Nat}, +x: Nat) -> {LV.ev(S.one()) == Nat.mod(Nat.pow(x, 0n), 1n+K.np(one)) : Nat}:
96  +ev = Equal.trans(Nat, LV.ev(S.one()), FS.value(one, S.one()), 1n, Equal.sym(Nat, FS.value(one, S.one()), LV.ev(S.one()), LV.ev_value(one, h1, S.one())), SO.small_val(one, h1, 1n, one_lt(one, h1)))
97  Equal.trans(Nat, LV.ev(S.one()), 1n, Nat.mod(Nat.pow(x, 0n), 1n+K.np(one)), ev, ME.pow0(K.np(one), x, I.lt_subst_r(1n, FS.order(one), 1n+K.np(one), K.order_eq(one, h1), one_lt(one, h1))))
98
99# ---- the exponent of inv: n - 2 ----
100
101def xn() -> List<&2, Nat>:
102  [48832n, 12233n, 41331n, 16429n, 24516n, 20663n, 8985n, 17745n, 1n, 0n, 0n, 0n, 0n, 0n, 0n, 0n]
103
104def zeros7(+one: Nat) -> {FS.digits(one, [0n, 0n, 0n, 0n, 0n, 0n, 0n]) == 0n : Nat}:
105  %Equal.sym(Nat, Nat.mul(one, 0n), 0n, NA.mul_zero(one)) : {Nat.add(_, C.shift(16n, Nat.add(Nat.mul(one, 0n), C.shift(16n, Nat.add(Nat.mul(one, 0n), C.shift(16n, Nat.add(Nat.mul(one, 0n), C.shift(16n, Nat.add(Nat.mul(one, 0n), C.shift(16n, Nat.add(Nat.mul(one, 0n), C.shift(16n, Nat.add(Nat.mul(one, 0n), C.shift(16n, 0n)))))))))))))) == 0n : Nat}
106  %Equal.sym(Nat, Nat.mul(one, 0n), 0n, NA.mul_zero(one)) : {Nat.add(0n, C.shift(16n, Nat.add(_, C.shift(16n, Nat.add(Nat.mul(one, 0n), C.shift(16n, Nat.add(Nat.mul(one, 0n), C.shift(16n, Nat.add(Nat.mul(one, 0n), C.shift(16n, Nat.add(Nat.mul(one, 0n), C.shift(16n, Nat.add(Nat.mul(one, 0n), C.shift(16n, 0n)))))))))))))) == 0n : Nat}
107  %Equal.sym(Nat, Nat.mul(one, 0n), 0n, NA.mul_zero(one)) : {Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(_, C.shift(16n, Nat.add(Nat.mul(one, 0n), C.shift(16n, Nat.add(Nat.mul(one, 0n), C.shift(16n, Nat.add(Nat.mul(one, 0n), C.shift(16n, Nat.add(Nat.mul(one, 0n), C.shift(16n, 0n)))))))))))))) == 0n : Nat}
108  %Equal.sym(Nat, Nat.mul(one, 0n), 0n, NA.mul_zero(one)) : {Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(_, C.shift(16n, Nat.add(Nat.mul(one, 0n), C.shift(16n, Nat.add(Nat.mul(one, 0n), C.shift(16n, Nat.add(Nat.mul(one, 0n), C.shift(16n, 0n)))))))))))))) == 0n : Nat}
109  %Equal.sym(Nat, Nat.mul(one, 0n), 0n, NA.mul_zero(one)) : {Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(_, C.shift(16n, Nat.add(Nat.mul(one, 0n), C.shift(16n, Nat.add(Nat.mul(one, 0n), C.shift(16n, 0n)))))))))))))) == 0n : Nat}
110  %Equal.sym(Nat, Nat.mul(one, 0n), 0n, NA.mul_zero(one)) : {Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(_, C.shift(16n, Nat.add(Nat.mul(one, 0n), C.shift(16n, 0n)))))))))))))) == 0n : Nat}
111  %Equal.sym(Nat, Nat.mul(one, 0n), 0n, NA.mul_zero(one)) : {Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(_, C.shift(16n, 0n)))))))))))))) == 0n : Nat}
112  %Equal.sym(Nat, C.shift(16n, 0n), 0n, WW.shift_zero(16n)) : {Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, _))))))))))))) == 0n : Nat}
113  %Equal.sym(Nat, Nat.add(0n, 0n), 0n, {==}) : {Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, _)))))))))))) == 0n : Nat}
114  %Equal.sym(Nat, C.shift(16n, 0n), 0n, WW.shift_zero(16n)) : {Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, _))))))))))) == 0n : Nat}
115  %Equal.sym(Nat, Nat.add(0n, 0n), 0n, {==}) : {Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, _)))))))))) == 0n : Nat}
116  %Equal.sym(Nat, C.shift(16n, 0n), 0n, WW.shift_zero(16n)) : {Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, _))))))))) == 0n : Nat}
117  %Equal.sym(Nat, Nat.add(0n, 0n), 0n, {==}) : {Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, _)))))))) == 0n : Nat}
118  %Equal.sym(Nat, C.shift(16n, 0n), 0n, WW.shift_zero(16n)) : {Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, _))))))) == 0n : Nat}
119  %Equal.sym(Nat, Nat.add(0n, 0n), 0n, {==}) : {Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, _)))))) == 0n : Nat}
120  %Equal.sym(Nat, C.shift(16n, 0n), 0n, WW.shift_zero(16n)) : {Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, _))))) == 0n : Nat}
121  %Equal.sym(Nat, Nat.add(0n, 0n), 0n, {==}) : {Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, _)))) == 0n : Nat}
122  %Equal.sym(Nat, C.shift(16n, 0n), 0n, WW.shift_zero(16n)) : {Nat.add(0n, C.shift(16n, Nat.add(0n, _))) == 0n : Nat}
123  %Equal.sym(Nat, Nat.add(0n, 0n), 0n, {==}) : {Nat.add(0n, C.shift(16n, _)) == 0n : Nat}
124  %Equal.sym(Nat, C.shift(16n, 0n), 0n, WW.shift_zero(16n)) : {Nat.add(0n, _) == 0n : Nat}
125  %Equal.sym(Nat, Nat.add(0n, 0n), 0n, {==}) : {_ == 0n : Nat}
126  {==}
127
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  {==}
134
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  {==}
146
147def xn_limbs(+one: Nat, +h1: {one == 1n : Nat}) -> {FS.limbs16(one, 16n, xn()) == True{} : Bool}:
148  LT.lits16(one, h1, 16n, xn(), {==})
149
150# the bits of c_n + 1, most significant first
151def xb() -> List<&2, Nat>:
152  [0n, 0n, 0n, 0n, 0n, 0n, 0n, 0n, 0n, 0n, 0n, 0n, 0n, 0n, 0n, 0n, 0n, 0n, 0n, 0n, 0n, 0n, 0n, 0n, 0n, 0n, 0n, 0n, 0n, 0n, 0n, 0n,
153   0n, 0n, 0n, 0n, 0n, 0n, 0n, 0n, 0n, 0n, 0n, 0n, 0n, 0n, 0n, 0n, 0n, 0n, 0n, 0n, 0n, 0n, 0n, 0n, 0n, 0n, 0n, 0n, 0n, 0n, 0n, 0n,
154   0n, 0n, 0n, 0n, 0n, 0n, 0n, 0n, 0n, 0n, 0n, 0n, 0n, 0n, 0n, 0n, 0n, 0n, 0n, 0n, 0n, 0n, 0n, 0n, 0n, 0n, 0n, 0n, 0n, 0n, 0n, 0n,
155   0n, 0n, 0n, 0n, 0n, 0n, 0n, 0n, 0n, 0n, 0n, 0n, 0n, 0n, 0n, 0n, 0n, 0n, 0n, 0n, 0n, 0n, 0n, 0n, 0n, 0n, 0n, 0n, 0n, 0n, 0n, 1n,
156   0n, 1n, 0n, 0n, 0n, 1n, 0n, 1n, 0n, 1n, 0n, 1n, 0n, 0n, 0n, 1n, 0n, 0n, 1n, 0n, 0n, 0n, 1n, 1n, 0n, 0n, 0n, 1n, 1n, 0n, 0n, 1n,
157   0n, 1n, 0n, 1n, 0n, 0n, 0n, 0n, 1n, 0n, 1n, 1n, 0n, 1n, 1n, 1n, 0n, 1n, 0n, 1n, 1n, 1n, 1n, 1n, 1n, 1n, 0n, 0n, 0n, 1n, 0n, 0n,
158   0n, 1n, 0n, 0n, 0n, 0n, 0n, 0n, 0n, 0n, 1n, 0n, 1n, 1n, 0n, 1n, 1n, 0n, 1n, 0n, 0n, 0n, 0n, 1n, 0n, 1n, 1n, 1n, 0n, 0n, 1n, 1n,
159   0n, 0n, 1n, 0n, 1n, 1n, 1n, 1n, 1n, 1n, 0n, 0n, 1n, 0n, 0n, 1n, 1n, 0n, 1n, 1n, 1n, 1n, 1n, 0n, 1n, 1n, 0n, 0n, 0n, 0n, 0n, 0n]
160
161def bits_xb() -> {L.bits(xn()) == xb() : List<&2, Nat>}:
162  {==}
163
164def ib_lit() -> {S.inv_bits() == L.cbits(xb()) : List<&2, Nat>}:
165  {==}
166
167def xb01() -> {BV.all01(xb()) == True{} : Bool}:
168  {==}
169
170def xb_len() -> {List.length(&2, Nat, xb()) == 256n : Nat}:
171  {==}
172
173# hv(xb) = c_n + 1
174def xb_v(+one: Nat, +h1: {one == 1n : Nat}) -> {BV.hv(xb(), one, 0n) == Nat.add(FS.cn(one), one) : Nat}:
175  %Equal.sym(List<&2, Nat>, xb(), L.bits(xn()), Equal.sym(List<&2, Nat>, L.bits(xn()), xb(), bits_xb())) : {BV.hv(_, one, 0n) == Nat.add(FS.cn(one), one) : Nat}
176  %Equal.sym(Nat, BV.hv(L.bits(xn()), one, 0n), Nat.add(LV.pos(16n, 0n), FS.digits(one, xn())), BV.bits_v(one, h1, 16n, xn(), 0n, xn_limbs(one, h1))) : {_ == Nat.add(FS.cn(one), one) : Nat}
177  %Equal.sym(Nat, LV.pos(16n, 0n), 0n, LV.pos_zero(16n)) : {Nat.add(_, FS.digits(one, xn())) == Nat.add(FS.cn(one), one) : Nat}
178  %Equal.sym(Nat, FS.digits(one, xn()), Nat.add(FS.cn(one), one), xn_digits(one, h1)) : {Nat.add(0n, _) == Nat.add(FS.cn(one), one) : Nat}
179  %Equal.sym(Nat, Nat.add(0n, Nat.add(FS.cn(one), one)), Nat.add(FS.cn(one), one), SR.zero_add(Nat.add(FS.cn(one), one))) : {_ == Nat.add(FS.cn(one), one) : Nat}
180  {==}
181
182def inv_h2(+one: Nat, +h1: {one == 1n : Nat}) -> {Nat.add(FS.cn(one), Nat.add(BV.hv(S.inv_bits(), one, 0n), 2n)) == Nat.add(FS.cn(one), 1n+K.np(one)) : Nat}:
183  +hcb = BV.cb(one, xb(), 0n, 0n, xb01())
184  %Equal.sym(List<&2, Nat>, S.inv_bits(), L.cbits(xb()), ib_lit()) : {Nat.add(FS.cn(one), Nat.add(BV.hv(_, one, 0n), 2n)) == Nat.add(FS.cn(one), 1n+K.np(one)) : Nat}
185  %Equal.sym(Nat, Nat.add(FS.cn(one), 1n+K.np(one)), Nat.add(1n+K.np(one), FS.cn(one)), NA.add_comm(FS.cn(one), 1n+K.np(one))) : {Nat.add(FS.cn(one), Nat.add(BV.hv(L.cbits(xb()), one, 0n), 2n)) == _ : Nat}
186  %Equal.sym(Nat, Nat.add(1n+K.np(one), FS.cn(one)), C.shift(256n, one), K.hm_n(one, h1)) : {Nat.add(FS.cn(one), Nat.add(BV.hv(L.cbits(xb()), one, 0n), 2n)) == _ : Nat}
187  %Equal.sym(Nat, C.shift(256n, one), Nat.add(Nat.add(BV.hv(L.cbits(xb()), one, 0n), BV.hv(xb(), one, 0n)), one), Equal.sym(Nat, Nat.add(Nat.add(BV.hv(L.cbits(xb()), one, 0n), BV.hv(xb(), one, 0n)), one), C.shift(256n, one), hcb)) : {Nat.add(FS.cn(one), Nat.add(BV.hv(L.cbits(xb()), one, 0n), 2n)) == _ : Nat}
188  %Equal.sym(Nat, BV.hv(xb(), one, 0n), Nat.add(FS.cn(one), one), xb_v(one, h1)) : {Nat.add(FS.cn(one), Nat.add(BV.hv(L.cbits(xb()), one, 0n), 2n)) == Nat.add(Nat.add(BV.hv(L.cbits(xb()), one, 0n), _), one) : Nat}
189  %Equal.sym(Nat, one, 1n, h1) : {Nat.add(FS.cn(one), Nat.add(BV.hv(L.cbits(xb()), one, 0n), 2n)) == Nat.add(Nat.add(BV.hv(L.cbits(xb()), one, 0n), Nat.add(FS.cn(one), _)), one) : Nat}
190  %Equal.sym(Nat, one, 1n, h1) : {Nat.add(FS.cn(one), Nat.add(BV.hv(L.cbits(xb()), one, 0n), 2n)) == Nat.add(Nat.add(BV.hv(L.cbits(xb()), one, 0n), Nat.add(FS.cn(one), 1n)), _) : Nat}
191  %Equal.sym(Nat, Nat.add(FS.cn(one), Nat.add(BV.hv(L.cbits(xb()), one, 0n), 2n)), Nat.add(BV.hv(L.cbits(xb()), one, 0n), Nat.add(FS.cn(one), 2n)), NA.add_swap(FS.cn(one), BV.hv(L.cbits(xb()), one, 0n), 2n)) : {_ == Nat.add(Nat.add(BV.hv(L.cbits(xb()), one, 0n), Nat.add(FS.cn(one), 1n)), 1n) : Nat}
192  %Equal.sym(Nat, Nat.add(Nat.add(BV.hv(L.cbits(xb()), one, 0n), Nat.add(FS.cn(one), 1n)), 1n), Nat.add(BV.hv(L.cbits(xb()), one, 0n), Nat.add(Nat.add(FS.cn(one), 1n), 1n)), NA.add_assoc(BV.hv(L.cbits(xb()), one, 0n), Nat.add(FS.cn(one), 1n), 1n)) : {Nat.add(BV.hv(L.cbits(xb()), one, 0n), Nat.add(FS.cn(one), 2n)) == _ : Nat}
193  %Equal.sym(Nat, Nat.add(Nat.add(FS.cn(one), 1n), 1n), Nat.add(FS.cn(one), Nat.add(1n, 1n)), NA.add_assoc(FS.cn(one), 1n, 1n)) : {Nat.add(BV.hv(L.cbits(xb()), one, 0n), Nat.add(FS.cn(one), 2n)) == Nat.add(BV.hv(L.cbits(xb()), one, 0n), _) : Nat}
194  %Equal.sym(Nat, Nat.add(1n, 1n), 2n, {==}) : {Nat.add(BV.hv(L.cbits(xb()), one, 0n), Nat.add(FS.cn(one), 2n)) == Nat.add(BV.hv(L.cbits(xb()), one, 0n), Nat.add(FS.cn(one), _)) : Nat}
195  {==}
196
197def exp_inv(+one: Nat, +h1: {one == 1n : Nat}) -> {BV.hv(S.inv_bits(), one, 0n) == Nat.sub(1n+K.np(one), 2n) : Nat}:
198  +h = BV.hv(S.inv_bits(), one, 0n)
199  +e = NR.add_cancel(FS.cn(one), Nat.add(h, 2n), 1n+K.np(one), inv_h2(one, h1))
200  %Equal.sym(Nat, 1n+K.np(one), Nat.add(BV.hv(S.inv_bits(), one, 0n), 2n), Equal.sym(Nat, Nat.add(BV.hv(S.inv_bits(), one, 0n), 2n), 1n+K.np(one), e)) : {BV.hv(S.inv_bits(), one, 0n) == Nat.sub(_, 2n) : Nat}
201  %Equal.sym(Nat, Nat.add(BV.hv(S.inv_bits(), one, 0n), 2n), Nat.add(2n, BV.hv(S.inv_bits(), one, 0n)), NA.add_comm(BV.hv(S.inv_bits(), one, 0n), 2n)) : {BV.hv(S.inv_bits(), one, 0n) == Nat.sub(_, 2n) : Nat}
202  %Equal.sym(Nat, Nat.sub(Nat.add(2n, BV.hv(S.inv_bits(), one, 0n)), 2n), BV.hv(S.inv_bits(), one, 0n), N.add_sub_cancel(2n, BV.hv(S.inv_bits(), one, 0n))) : {BV.hv(S.inv_bits(), one, 0n) == _ : Nat}
203  {==}
204
205def inv_bits01(+one: Nat) -> {BV.all01(S.inv_bits()) == True{} : Bool}:
206  {==}
207
208def inv_v(+one: Nat, +h1: {one == 1n : Nat}, +a: List<&2, Nat>, +ha: {FS.reduced(one, FS.order(one), a) == True{} : Bool}) -> {FS.value(one, S.inv(a)) == FS.minv(FS.order(one), FS.value(one, a)) : Nat}:
209  %Equal.sym(Nat, FS.value(one, S.pow(a, S.inv_bits(), S.one())), LV.ev(S.pow(a, S.inv_bits(), S.one())), LV.ev_value(one, h1, S.pow(a, S.inv_bits(), S.one()))) : {_ == Nat.mod(Nat.pow(FS.value(one, a), Nat.sub(FS.order(one), 2n)), FS.order(one)) : Nat}
210  %Equal.sym(Nat, LV.ev(S.pow(a, S.inv_bits(), S.one())), Nat.mod(Nat.pow(LV.ev(a), BV.hv(S.inv_bits(), one, 0n)), 1n+K.np(one)), pow_ev(one, h1, a, ha, S.inv_bits(), S.one(), one_r(one, h1), 0n, one_e(one, h1, LV.ev(a)), inv_bits01(one))) : {_ == Nat.mod(Nat.pow(FS.value(one, a), Nat.sub(FS.order(one), 2n)), FS.order(one)) : Nat}
211  %Equal.sym(Nat, BV.hv(S.inv_bits(), one, 0n), Nat.sub(1n+K.np(one), 2n), exp_inv(one, h1)) : {Nat.mod(Nat.pow(LV.ev(a), _), 1n+K.np(one)) == Nat.mod(Nat.pow(FS.value(one, a), Nat.sub(FS.order(one), 2n)), FS.order(one)) : Nat}
212  %Equal.sym(Nat, FS.value(one, a), LV.ev(a), LV.ev_value(one, h1, a)) : {Nat.mod(Nat.pow(LV.ev(a), Nat.sub(1n+K.np(one), 2n)), 1n+K.np(one)) == Nat.mod(Nat.pow(_, Nat.sub(FS.order(one), 2n)), FS.order(one)) : Nat}
213  %Equal.sym(Nat, FS.order(one), 1n+K.np(one), K.order_eq(one, h1)) : {Nat.mod(Nat.pow(LV.ev(a), Nat.sub(1n+K.np(one), 2n)), 1n+K.np(one)) == Nat.mod(Nat.pow(LV.ev(a), Nat.sub(_, 2n)), FS.order(one)) : Nat}
214  %Equal.sym(Nat, FS.order(one), 1n+K.np(one), K.order_eq(one, h1)) : {Nat.mod(Nat.pow(LV.ev(a), Nat.sub(1n+K.np(one), 2n)), 1n+K.np(one)) == Nat.mod(Nat.pow(LV.ev(a), Nat.sub(1n+K.np(one), 2n)), _) : Nat}
215  {==}
216
217def inv_r(+one: Nat, +h1: {one == 1n : Nat}, +a: List<&2, Nat>, +ha: {FS.reduced(one, FS.order(one), a) == True{} : Bool}) -> {FS.reduced(one, FS.order(one), S.inv(a)) == True{} : Bool}:
218  pow_rv(one, h1, a, ha, S.inv_bits(), S.one(), one_r(one, h1), inv_bits01(one))