proofs/crypto/secp256k1/fieldpow.bend

bend-collections-laws-crypto@1.0.0.0 · 346 lines · 36 definitions

1# GENERATED by tools/generators/rw.py from ../../../tools/generators/secp256k1_hand/fieldpow.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/field.bend as F
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/bounds.bend as B
16import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/consts.bend as K
17import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/bitsv.bend as BV
18import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/modexp.bend as ME
19import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/fieldops.bend as FO
20
21# Exponentiation in GF(p) (src/crypto/secp256k1/field.bend pow, inv, sqrt):
22# square-and-multiply over the exponent's bits computes x^e mod p, and the
23# bits of inv and sqrt spell p - 2 and (p + 1) / 4.
24
25def m(+one: Nat) -> Nat:
26  1n+K.pp(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.prime(one), x) == True{} : Bool}, +acc: List<&2, Nat>, +ha: {FS.reduced(one, FS.prime(one), acc) == True{} : Bool}, +e: Nat, +he: {LV.ev(acc) == Nat.mod(Nat.pow(LV.ev(x), e), 1n+K.pp(one)) : Nat}, b: Nat, +hb: {Nat.is_lt(b, 2n) == True{} : Bool}) -> {LV.ev(F.pow_step(b, x, F.sq(acc))) == Nat.mod(Nat.pow(LV.ev(x), Nat.add(Nat.mul(b, one), Nat.double(e))), 1n+K.pp(one)) : Nat}:
30  match b:
31    case 0n:
32      %Equal.sym(Nat, LV.ev(F.mul(acc, acc)), Nat.mod(Nat.mul(LV.ev(acc), LV.ev(acc)), 1n+K.pp(one)), FO.mul_e(one, h1, acc, acc, ha, ha)) : {_ == Nat.mod(Nat.pow(LV.ev(x), Nat.double(e)), 1n+K.pp(one)) : Nat}
33      ME.sq_step(K.pp(one), LV.ev(x), e, LV.ev(acc), he)
34    case 1n:
35      +sq = F.mul(acc, acc)
36      +es = Equal.trans(Nat, LV.ev(sq), Nat.mod(Nat.mul(LV.ev(acc), LV.ev(acc)), 1n+K.pp(one)), Nat.mod(Nat.pow(LV.ev(x), Nat.double(e)), 1n+K.pp(one)), FO.mul_e(one, h1, acc, acc, ha, ha), ME.sq_step(K.pp(one), LV.ev(x), e, LV.ev(acc), he))
37      %Equal.sym(Nat, Nat.mul(1n, one), one, SR.one_mul(one)) : {LV.ev(F.mul(F.mul(acc, acc), x)) == Nat.mod(Nat.pow(LV.ev(x), Nat.add(_, Nat.double(e))), 1n+K.pp(one)) : Nat}
38      %Equal.sym(Nat, one, 1n, h1) : {LV.ev(F.mul(F.mul(acc, acc), x)) == Nat.mod(Nat.pow(LV.ev(x), Nat.add(_, Nat.double(e))), 1n+K.pp(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(F.mul(F.mul(acc, acc), x)) == Nat.mod(Nat.pow(LV.ev(x), _), 1n+K.pp(one)) : Nat}
40      %Equal.sym(Nat, LV.ev(F.mul(F.mul(acc, acc), x)), Nat.mod(Nat.mul(LV.ev(F.mul(acc, acc)), LV.ev(x)), 1n+K.pp(one)), FO.mul_e(one, h1, F.mul(acc, acc), x, FO.mul_r(one, h1, acc, acc, ha, ha), hx)) : {_ == Nat.mod(Nat.pow(LV.ev(x), Nat.add(Nat.double(e), 1n)), 1n+K.pp(one)) : Nat}
41      ME.mul_step(K.pp(one), LV.ev(x), Nat.double(e), LV.ev(F.mul(acc, acc)), es)
42    case 2n+ +k:
43      Empty.absurd({LV.ev(F.pow_step(2n+k, x, F.sq(acc))) == Nat.mod(Nat.pow(LV.ev(x), Nat.add(Nat.mul(2n+k, one), Nat.double(e))), 1n+K.pp(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.prime(one), x) == True{} : Bool}, +acc: List<&2, Nat>, +ha: {FS.reduced(one, FS.prime(one), acc) == True{} : Bool}, b: Nat, +hb: {Nat.is_lt(b, 2n) == True{} : Bool}) -> {FS.reduced(one, FS.prime(one), F.pow_step(b, x, F.sq(acc))) == True{} : Bool}:
46  match b:
47    case 0n:
48      FO.mul_r(one, h1, acc, acc, ha, ha)
49    case 1n:
50      FO.mul_r(one, h1, F.mul(acc, acc), x, FO.mul_r(one, h1, acc, acc, ha, ha), hx)
51    case 2n+ +k:
52      Empty.absurd({FS.reduced(one, FS.prime(one), F.pow_step(2n+k, x, F.sq(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.prime(one), x) == True{} : Bool}, bs: List<&2, Nat>, +acc: List<&2, Nat>, +ha: {FS.reduced(one, FS.prime(one), acc) == True{} : Bool}, +hb: {BV.all01(bs) == True{} : Bool}) -> {FS.reduced(one, FS.prime(one), F.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, F.pow_step(b, x, F.sq(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.prime(one), x) == True{} : Bool}, bs: List<&2, Nat>, +acc: List<&2, Nat>, +ha: {FS.reduced(one, FS.prime(one), acc) == True{} : Bool}, +e: Nat, +he: {LV.ev(acc) == Nat.mod(Nat.pow(LV.ev(x), e), 1n+K.pp(one)) : Nat}, +hb: {BV.all01(bs) == True{} : Bool}) -> {LV.ev(F.pow_go(x, bs, acc)) == Nat.mod(Nat.pow(LV.ev(x), BV.hv(bs, one, e)), 1n+K.pp(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, F.pow_step(b, x, F.sq(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# F.pow looks at x first
72def pow_is(+one: Nat, x: List<&2, Nat>, +hx: {FS.reduced(one, FS.prime(one), x) == True{} : Bool}, +bs: List<&2, Nat>, +acc: List<&2, Nat>) -> {F.pow(x, bs, acc) == F.pow_go(x, bs, acc) : List<&2, Nat>}:
73  match x:
74    case Nil{}:
75      Empty.absurd({F.pow([], bs, acc) == F.pow_go([], bs, acc) : List<&2, Nat>}, Lg.false_true(Lg.and_left(FS.limbs16(one, 16n, []), Nat.is_lt(FS.value(one, []), FS.prime(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.prime(one), x) == True{} : Bool}, +bs: List<&2, Nat>, +acc: List<&2, Nat>, +ha: {FS.reduced(one, FS.prime(one), acc) == True{} : Bool}, +e: Nat, +he: {LV.ev(acc) == Nat.mod(Nat.pow(LV.ev(x), e), 1n+K.pp(one)) : Nat}, +hb: {BV.all01(bs) == True{} : Bool}) -> {LV.ev(F.pow(x, bs, acc)) == Nat.mod(Nat.pow(LV.ev(x), BV.hv(bs, one, e)), 1n+K.pp(one)) : Nat}:
80  %Equal.sym(List<&2, Nat>, F.pow(x, bs, acc), F.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.pp(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.prime(one), x) == True{} : Bool}, +bs: List<&2, Nat>, +acc: List<&2, Nat>, +ha: {FS.reduced(one, FS.prime(one), acc) == True{} : Bool}, +hb: {BV.all01(bs) == True{} : Bool}) -> {FS.reduced(one, FS.prime(one), F.pow(x, bs, acc)) == True{} : Bool}:
84  %Equal.sym(List<&2, Nat>, F.pow(x, bs, acc), F.pow_go(x, bs, acc), pow_is(one, x, hx, bs, acc)) : {FS.reduced(one, FS.prime(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.prime(one)) == True{} : Bool}:
90  FO.small_lt_p(one, h1, 1n, {==})
91
92def one_r(+one: Nat, +h1: {one == 1n : Nat}) -> {FS.reduced(one, FS.prime(one), F.one()) == True{} : Bool}:
93  FO.small_r(one, h1, 1n, one_lt(one, h1))
94
95def one_e(+one: Nat, +h1: {one == 1n : Nat}, +x: Nat) -> {LV.ev(F.one()) == Nat.mod(Nat.pow(x, 0n), 1n+K.pp(one)) : Nat}:
96  +ev = Equal.trans(Nat, LV.ev(F.one()), FS.value(one, F.one()), 1n, Equal.sym(Nat, FS.value(one, F.one()), LV.ev(F.one()), LV.ev_value(one, h1, F.one())), FO.small_val(one, h1, 1n, one_lt(one, h1)))
97  Equal.trans(Nat, LV.ev(F.one()), 1n, Nat.mod(Nat.pow(x, 0n), 1n+K.pp(one)), ev, ME.pow0(K.pp(one), x, I.lt_subst_r(1n, FS.prime(one), 1n+K.pp(one), K.prime_eq(one, h1), one_lt(one, h1))))
98
99# ---- the exponent of inv: p - 2 ----
100
101def xp_lit() -> {L.norm16([978n, 0n, 1n]) == [978n, 0n, 1n, 0n, 0n, 0n, 0n, 0n, 0n, 0n, 0n, 0n, 0n, 0n, 0n, 0n] : List<&2, Nat>}:
102  {==}
103
104def zeros13(+one: Nat) -> {FS.digits(one, [0n, 0n, 0n, 0n, 0n, 0n, 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, 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, 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}
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, 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}
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, 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}
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, 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}
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, 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}
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, 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}
112  %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(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}
113  %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(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}
114  %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(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}
115  %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(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}
116  %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(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}
117  %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(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}
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, 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, 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, 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, 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, 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, C.shift(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, 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, C.shift(16n, 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, 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, C.shift(16n, Nat.add(0n, C.shift(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, 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, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, _)))))))))))))))))))) == 0n : Nat}
124  %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, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, _))))))))))))))))))) == 0n : Nat}
125  %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, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, _)))))))))))))))))) == 0n : Nat}
126  %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, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(0n, _))))))))))))))))) == 0n : Nat}
127  %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, Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, _)))))))))))))))) == 0n : Nat}
128  %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, C.shift(16n, Nat.add(0n, _))))))))))))))) == 0n : Nat}
129  %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, Nat.add(0n, C.shift(16n, _)))))))))))))) == 0n : Nat}
130  %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}
131  %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}
132  %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}
133  %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}
134  %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}
135  %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}
136  %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}
137  %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}
138  %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}
139  %Equal.sym(Nat, Nat.add(0n, 0n), 0n, {==}) : {Nat.add(0n, C.shift(16n, Nat.add(0n, C.shift(16n, _)))) == 0n : Nat}
140  %Equal.sym(Nat, C.shift(16n, 0n), 0n, WW.shift_zero(16n)) : {Nat.add(0n, C.shift(16n, Nat.add(0n, _))) == 0n : Nat}
141  %Equal.sym(Nat, Nat.add(0n, 0n), 0n, {==}) : {Nat.add(0n, C.shift(16n, _)) == 0n : Nat}
142  %Equal.sym(Nat, C.shift(16n, 0n), 0n, WW.shift_zero(16n)) : {Nat.add(0n, _) == 0n : Nat}
143  %Equal.sym(Nat, Nat.add(0n, 0n), 0n, {==}) : {_ == 0n : Nat}
144  {==}
145
146# 978 + 2^32 = c_p + 1
147def xp_digits(+one: Nat, +h1: {one == 1n : Nat}) -> {FS.digits(one, L.norm16([978n, 0n, 1n])) == Nat.add(FS.cp(one), one) : Nat}:
148  %Equal.sym(List<&2, Nat>, L.norm16([978n, 0n, 1n]), [978n, 0n, 1n, 0n, 0n, 0n, 0n, 0n, 0n, 0n, 0n, 0n, 0n, 0n, 0n, 0n], xp_lit()) : {FS.digits(one, _) == Nat.add(FS.cp(one), one) : Nat}
149  %Equal.sym(Nat, FS.digits(one, [0n, 0n, 0n, 0n, 0n, 0n, 0n, 0n, 0n, 0n, 0n, 0n, 0n]), 0n, zeros13(one)) : {Nat.add(Nat.mul(one, 978n), C.shift(16n, Nat.add(Nat.mul(one, 0n), C.shift(16n, Nat.add(Nat.mul(one, 1n), C.shift(16n, _)))))) == Nat.add(Nat.add(Nat.mul(one, 977n), C.shift(16n, Nat.add(Nat.mul(one, 0n), C.shift(16n, Nat.add(Nat.mul(one, 1n), C.shift(16n, 0n)))))), one) : Nat}
150  %Equal.sym(Nat, Nat.mul(one, 978n), Nat.add(one, Nat.mul(one, 977n)), NA.mul_succ(one, 977n)) : {Nat.add(_, C.shift(16n, Nat.add(Nat.mul(one, 0n), C.shift(16n, Nat.add(Nat.mul(one, 1n), C.shift(16n, 0n)))))) == Nat.add(Nat.add(Nat.mul(one, 977n), C.shift(16n, Nat.add(Nat.mul(one, 0n), C.shift(16n, Nat.add(Nat.mul(one, 1n), C.shift(16n, 0n)))))), one) : Nat}
151  %Equal.sym(Nat, Nat.mul(one, 0n), 0n, NA.mul_zero(one)) : {Nat.add(Nat.add(one, Nat.mul(one, 977n)), C.shift(16n, Nat.add(_, C.shift(16n, Nat.add(Nat.mul(one, 1n), C.shift(16n, 0n)))))) == Nat.add(Nat.add(Nat.mul(one, 977n), C.shift(16n, Nat.add(Nat.mul(one, 0n), C.shift(16n, Nat.add(Nat.mul(one, 1n), C.shift(16n, 0n)))))), one) : Nat}
152  %Equal.sym(Nat, Nat.mul(one, 1n), one, NA.mul_one(one)) : {Nat.add(Nat.add(one, Nat.mul(one, 977n)), C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(_, C.shift(16n, 0n)))))) == Nat.add(Nat.add(Nat.mul(one, 977n), C.shift(16n, Nat.add(Nat.mul(one, 0n), C.shift(16n, Nat.add(Nat.mul(one, 1n), C.shift(16n, 0n)))))), one) : Nat}
153  %Equal.sym(Nat, C.shift(16n, 0n), 0n, WW.shift_zero(16n)) : {Nat.add(Nat.add(one, Nat.mul(one, 977n)), C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(one, _))))) == Nat.add(Nat.add(Nat.mul(one, 977n), C.shift(16n, Nat.add(Nat.mul(one, 0n), C.shift(16n, Nat.add(Nat.mul(one, 1n), C.shift(16n, 0n)))))), one) : Nat}
154  %Equal.sym(Nat, Nat.add(one, 0n), one, NA.add_zero(one)) : {Nat.add(Nat.add(one, Nat.mul(one, 977n)), C.shift(16n, Nat.add(0n, C.shift(16n, _)))) == Nat.add(Nat.add(Nat.mul(one, 977n), C.shift(16n, Nat.add(Nat.mul(one, 0n), C.shift(16n, Nat.add(Nat.mul(one, 1n), C.shift(16n, 0n)))))), one) : Nat}
155  %Equal.sym(Nat, Nat.add(0n, C.shift(16n, one)), C.shift(16n, one), SR.zero_add(C.shift(16n, one))) : {Nat.add(Nat.add(one, Nat.mul(one, 977n)), C.shift(16n, _)) == Nat.add(Nat.add(Nat.mul(one, 977n), C.shift(16n, Nat.add(Nat.mul(one, 0n), C.shift(16n, Nat.add(Nat.mul(one, 1n), C.shift(16n, 0n)))))), one) : Nat}
156  %Equal.sym(Nat, C.shift(16n, C.shift(16n, one)), C.shift(32n, one), SR.shift_shift(16n, 16n, one)) : {Nat.add(Nat.add(one, Nat.mul(one, 977n)), _) == Nat.add(Nat.add(Nat.mul(one, 977n), C.shift(16n, Nat.add(Nat.mul(one, 0n), C.shift(16n, Nat.add(Nat.mul(one, 1n), C.shift(16n, 0n)))))), one) : Nat}
157  %Equal.sym(Nat, Nat.add(Nat.add(one, Nat.mul(one, 977n)), C.shift(32n, one)), Nat.add(one, Nat.add(Nat.mul(one, 977n), C.shift(32n, one))), NA.add_assoc(one, Nat.mul(one, 977n), C.shift(32n, one))) : {_ == Nat.add(Nat.add(Nat.mul(one, 977n), C.shift(16n, Nat.add(Nat.mul(one, 0n), C.shift(16n, Nat.add(Nat.mul(one, 1n), C.shift(16n, 0n)))))), one) : Nat}
158  %Equal.sym(Nat, Nat.add(Nat.mul(one, 977n), C.shift(32n, one)), Nat.add(C.shift(32n, one), Nat.mul(one, 977n)), NA.add_comm(Nat.mul(one, 977n), C.shift(32n, one))) : {Nat.add(one, _) == Nat.add(Nat.add(Nat.mul(one, 977n), C.shift(16n, Nat.add(Nat.mul(one, 0n), C.shift(16n, Nat.add(Nat.mul(one, 1n), C.shift(16n, 0n)))))), one) : Nat}
159  %Equal.sym(Nat, Nat.mul(one, 0n), 0n, NA.mul_zero(one)) : {Nat.add(one, Nat.add(C.shift(32n, one), Nat.mul(one, 977n))) == Nat.add(Nat.add(Nat.mul(one, 977n), C.shift(16n, Nat.add(_, C.shift(16n, Nat.add(Nat.mul(one, 1n), C.shift(16n, 0n)))))), one) : Nat}
160  %Equal.sym(Nat, Nat.mul(one, 1n), one, NA.mul_one(one)) : {Nat.add(one, Nat.add(C.shift(32n, one), Nat.mul(one, 977n))) == Nat.add(Nat.add(Nat.mul(one, 977n), C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(_, C.shift(16n, 0n)))))), one) : Nat}
161  %Equal.sym(Nat, C.shift(16n, 0n), 0n, WW.shift_zero(16n)) : {Nat.add(one, Nat.add(C.shift(32n, one), Nat.mul(one, 977n))) == Nat.add(Nat.add(Nat.mul(one, 977n), C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(one, _))))), one) : Nat}
162  %Equal.sym(Nat, Nat.add(one, 0n), one, NA.add_zero(one)) : {Nat.add(one, Nat.add(C.shift(32n, one), Nat.mul(one, 977n))) == Nat.add(Nat.add(Nat.mul(one, 977n), C.shift(16n, Nat.add(0n, C.shift(16n, _)))), one) : Nat}
163  %Equal.sym(Nat, Nat.add(0n, C.shift(16n, one)), C.shift(16n, one), SR.zero_add(C.shift(16n, one))) : {Nat.add(one, Nat.add(C.shift(32n, one), Nat.mul(one, 977n))) == Nat.add(Nat.add(Nat.mul(one, 977n), C.shift(16n, _)), one) : Nat}
164  %Equal.sym(Nat, C.shift(16n, C.shift(16n, one)), C.shift(32n, one), SR.shift_shift(16n, 16n, one)) : {Nat.add(one, Nat.add(C.shift(32n, one), Nat.mul(one, 977n))) == Nat.add(Nat.add(Nat.mul(one, 977n), _), one) : Nat}
165  %Equal.sym(Nat, Nat.add(Nat.mul(one, 977n), C.shift(32n, one)), Nat.add(C.shift(32n, one), Nat.mul(one, 977n)), NA.add_comm(Nat.mul(one, 977n), C.shift(32n, one))) : {Nat.add(one, Nat.add(C.shift(32n, one), Nat.mul(one, 977n))) == Nat.add(_, one) : Nat}
166  %Equal.sym(Nat, Nat.add(Nat.add(C.shift(32n, one), Nat.mul(one, 977n)), one), Nat.add(C.shift(32n, one), Nat.add(Nat.mul(one, 977n), one)), NA.add_assoc(C.shift(32n, one), Nat.mul(one, 977n), one)) : {Nat.add(one, Nat.add(C.shift(32n, one), Nat.mul(one, 977n))) == _ : Nat}
167  %Equal.sym(Nat, Nat.add(Nat.mul(one, 977n), one), Nat.add(one, Nat.mul(one, 977n)), NA.add_comm(Nat.mul(one, 977n), one)) : {Nat.add(one, Nat.add(C.shift(32n, one), Nat.mul(one, 977n))) == Nat.add(C.shift(32n, one), _) : Nat}
168  %Equal.sym(Nat, Nat.add(C.shift(32n, one), Nat.add(one, Nat.mul(one, 977n))), Nat.add(one, Nat.add(C.shift(32n, one), Nat.mul(one, 977n))), NA.add_swap(C.shift(32n, one), one, Nat.mul(one, 977n))) : {Nat.add(one, Nat.add(C.shift(32n, one), Nat.mul(one, 977n))) == _ : Nat}
169  {==}
170
171def xp_limbs(+one: Nat, +h1: {one == 1n : Nat}) -> {FS.limbs16(one, 16n, L.norm16([978n, 0n, 1n])) == True{} : Bool}:
172  B.carry_limbs(one, h1, 32n, 16n, [978n, 0n, 1n], 0n, {==})
173
174# hv(bits of p - 2) + 2 = p
175def inv_h2(+one: Nat, +h1: {one == 1n : Nat}) -> {Nat.add(FS.cp(one), Nat.add(BV.hv(F.inv_bits(), one, 0n), 2n)) == Nat.add(FS.cp(one), 1n+K.pp(one)) : Nat}:
176  +bs = L.bits(L.norm16([978n, 0n, 1n]))
177  +hcb = BV.cb(one, bs, 0n, 0n, BV.bits01(L.norm16([978n, 0n, 1n])))
178  %Equal.sym(Nat, Nat.add(FS.cp(one), 1n+K.pp(one)), Nat.add(1n+K.pp(one), FS.cp(one)), NA.add_comm(FS.cp(one), 1n+K.pp(one))) : {Nat.add(FS.cp(one), Nat.add(BV.hv(F.inv_bits(), one, 0n), 2n)) == _ : Nat}
179  %Equal.sym(Nat, Nat.add(1n+K.pp(one), FS.cp(one)), C.shift(256n, one), K.hm_p(one, h1)) : {Nat.add(FS.cp(one), Nat.add(BV.hv(F.inv_bits(), one, 0n), 2n)) == _ : Nat}
180  %Equal.sym(Nat, C.shift(256n, one), Nat.add(Nat.add(BV.hv(L.cbits(L.bits(L.norm16([978n, 0n, 1n]))), one, 0n), BV.hv(L.bits(L.norm16([978n, 0n, 1n])), one, 0n)), one), Equal.sym(Nat, Nat.add(Nat.add(BV.hv(L.cbits(L.bits(L.norm16([978n, 0n, 1n]))), one, 0n), BV.hv(L.bits(L.norm16([978n, 0n, 1n])), one, 0n)), one), C.shift(256n, one), hcb)) : {Nat.add(FS.cp(one), Nat.add(BV.hv(F.inv_bits(), one, 0n), 2n)) == _ : Nat}
181  %Equal.sym(Nat, BV.hv(L.bits(L.norm16([978n, 0n, 1n])), one, 0n), Nat.add(LV.pos(16n, 0n), FS.digits(one, L.norm16([978n, 0n, 1n]))), BV.bits_v(one, h1, 16n, L.norm16([978n, 0n, 1n]), 0n, xp_limbs(one, h1))) : {Nat.add(FS.cp(one), Nat.add(BV.hv(F.inv_bits(), one, 0n), 2n)) == Nat.add(Nat.add(BV.hv(L.cbits(L.bits(L.norm16([978n, 0n, 1n]))), one, 0n), _), one) : Nat}
182  %Equal.sym(Nat, LV.pos(16n, 0n), 0n, LV.pos_zero(16n)) : {Nat.add(FS.cp(one), Nat.add(BV.hv(F.inv_bits(), one, 0n), 2n)) == Nat.add(Nat.add(BV.hv(L.cbits(L.bits(L.norm16([978n, 0n, 1n]))), one, 0n), Nat.add(_, FS.digits(one, L.norm16([978n, 0n, 1n])))), one) : Nat}
183  %Equal.sym(Nat, FS.digits(one, L.norm16([978n, 0n, 1n])), Nat.add(FS.cp(one), one), xp_digits(one, h1)) : {Nat.add(FS.cp(one), Nat.add(BV.hv(F.inv_bits(), one, 0n), 2n)) == Nat.add(Nat.add(BV.hv(L.cbits(L.bits(L.norm16([978n, 0n, 1n]))), one, 0n), Nat.add(0n, _)), one) : Nat}
184  %Equal.sym(Nat, one, 1n, h1) : {Nat.add(FS.cp(one), Nat.add(BV.hv(F.inv_bits(), one, 0n), 2n)) == Nat.add(Nat.add(BV.hv(L.cbits(L.bits(L.norm16([978n, 0n, 1n]))), one, 0n), Nat.add(0n, Nat.add(FS.cp(one), _))), one) : Nat}
185  %Equal.sym(Nat, one, 1n, h1) : {Nat.add(FS.cp(one), Nat.add(BV.hv(F.inv_bits(), one, 0n), 2n)) == Nat.add(Nat.add(BV.hv(L.cbits(L.bits(L.norm16([978n, 0n, 1n]))), one, 0n), Nat.add(0n, Nat.add(FS.cp(one), 1n))), _) : Nat}
186  %Equal.sym(Nat, Nat.add(FS.cp(one), Nat.add(BV.hv(L.cbits(L.bits(L.norm16([978n, 0n, 1n]))), one, 0n), 2n)), Nat.add(BV.hv(L.cbits(L.bits(L.norm16([978n, 0n, 1n]))), one, 0n), Nat.add(FS.cp(one), 2n)), NA.add_swap(FS.cp(one), BV.hv(L.cbits(L.bits(L.norm16([978n, 0n, 1n]))), one, 0n), 2n)) : {_ == Nat.add(Nat.add(BV.hv(L.cbits(L.bits(L.norm16([978n, 0n, 1n]))), one, 0n), Nat.add(0n, Nat.add(FS.cp(one), 1n))), 1n) : Nat}
187  %Equal.sym(Nat, Nat.add(0n, Nat.add(FS.cp(one), 1n)), Nat.add(FS.cp(one), 1n), SR.zero_add(Nat.add(FS.cp(one), 1n))) : {Nat.add(BV.hv(L.cbits(L.bits(L.norm16([978n, 0n, 1n]))), one, 0n), Nat.add(FS.cp(one), 2n)) == Nat.add(Nat.add(BV.hv(L.cbits(L.bits(L.norm16([978n, 0n, 1n]))), one, 0n), _), 1n) : Nat}
188  %Equal.sym(Nat, Nat.add(Nat.add(BV.hv(L.cbits(L.bits(L.norm16([978n, 0n, 1n]))), one, 0n), Nat.add(FS.cp(one), 1n)), 1n), Nat.add(BV.hv(L.cbits(L.bits(L.norm16([978n, 0n, 1n]))), one, 0n), Nat.add(Nat.add(FS.cp(one), 1n), 1n)), NA.add_assoc(BV.hv(L.cbits(L.bits(L.norm16([978n, 0n, 1n]))), one, 0n), Nat.add(FS.cp(one), 1n), 1n)) : {Nat.add(BV.hv(L.cbits(L.bits(L.norm16([978n, 0n, 1n]))), one, 0n), Nat.add(FS.cp(one), 2n)) == _ : Nat}
189  %Equal.sym(Nat, Nat.add(Nat.add(FS.cp(one), 1n), 1n), Nat.add(FS.cp(one), Nat.add(1n, 1n)), NA.add_assoc(FS.cp(one), 1n, 1n)) : {Nat.add(BV.hv(L.cbits(L.bits(L.norm16([978n, 0n, 1n]))), one, 0n), Nat.add(FS.cp(one), 2n)) == Nat.add(BV.hv(L.cbits(L.bits(L.norm16([978n, 0n, 1n]))), one, 0n), _) : Nat}
190  %Equal.sym(Nat, Nat.add(1n, 1n), 2n, {==}) : {Nat.add(BV.hv(L.cbits(L.bits(L.norm16([978n, 0n, 1n]))), one, 0n), Nat.add(FS.cp(one), 2n)) == Nat.add(BV.hv(L.cbits(L.bits(L.norm16([978n, 0n, 1n]))), one, 0n), Nat.add(FS.cp(one), _)) : Nat}
191  {==}
192
193def exp_inv(+one: Nat, +h1: {one == 1n : Nat}) -> {BV.hv(F.inv_bits(), one, 0n) == Nat.sub(1n+K.pp(one), 2n) : Nat}:
194  +h = BV.hv(F.inv_bits(), one, 0n)
195  +e = NR.add_cancel(FS.cp(one), Nat.add(h, 2n), 1n+K.pp(one), inv_h2(one, h1))
196  %Equal.sym(Nat, 1n+K.pp(one), Nat.add(BV.hv(F.inv_bits(), one, 0n), 2n), Equal.sym(Nat, Nat.add(BV.hv(F.inv_bits(), one, 0n), 2n), 1n+K.pp(one), e)) : {BV.hv(F.inv_bits(), one, 0n) == Nat.sub(_, 2n) : Nat}
197  %Equal.sym(Nat, Nat.add(BV.hv(F.inv_bits(), one, 0n), 2n), Nat.add(2n, BV.hv(F.inv_bits(), one, 0n)), NA.add_comm(BV.hv(F.inv_bits(), one, 0n), 2n)) : {BV.hv(F.inv_bits(), one, 0n) == Nat.sub(_, 2n) : Nat}
198  %Equal.sym(Nat, Nat.sub(Nat.add(2n, BV.hv(F.inv_bits(), one, 0n)), 2n), BV.hv(F.inv_bits(), one, 0n), N.add_sub_cancel(2n, BV.hv(F.inv_bits(), one, 0n))) : {BV.hv(F.inv_bits(), one, 0n) == _ : Nat}
199  {==}
200
201def inv_bits01(+one: Nat) -> {BV.all01(F.inv_bits()) == True{} : Bool}:
202  BV.cbits01(L.bits(L.norm16([978n, 0n, 1n])))
203
204def inv_v(+one: Nat, +h1: {one == 1n : Nat}, +a: List<&2, Nat>, +ha: {FS.reduced(one, FS.prime(one), a) == True{} : Bool}) -> {FS.value(one, F.inv(a)) == FS.minv(FS.prime(one), FS.value(one, a)) : Nat}:
205  %Equal.sym(Nat, FS.value(one, F.pow(a, F.inv_bits(), F.one())), LV.ev(F.pow(a, F.inv_bits(), F.one())), LV.ev_value(one, h1, F.pow(a, F.inv_bits(), F.one()))) : {_ == Nat.mod(Nat.pow(FS.value(one, a), Nat.sub(FS.prime(one), 2n)), FS.prime(one)) : Nat}
206  %Equal.sym(Nat, LV.ev(F.pow(a, F.inv_bits(), F.one())), Nat.mod(Nat.pow(LV.ev(a), BV.hv(F.inv_bits(), one, 0n)), 1n+K.pp(one)), pow_ev(one, h1, a, ha, F.inv_bits(), F.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.prime(one), 2n)), FS.prime(one)) : Nat}
207  %Equal.sym(Nat, BV.hv(F.inv_bits(), one, 0n), Nat.sub(1n+K.pp(one), 2n), exp_inv(one, h1)) : {Nat.mod(Nat.pow(LV.ev(a), _), 1n+K.pp(one)) == Nat.mod(Nat.pow(FS.value(one, a), Nat.sub(FS.prime(one), 2n)), FS.prime(one)) : Nat}
208  %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.pp(one), 2n)), 1n+K.pp(one)) == Nat.mod(Nat.pow(_, Nat.sub(FS.prime(one), 2n)), FS.prime(one)) : Nat}
209  %Equal.sym(Nat, FS.prime(one), 1n+K.pp(one), K.prime_eq(one, h1)) : {Nat.mod(Nat.pow(LV.ev(a), Nat.sub(1n+K.pp(one), 2n)), 1n+K.pp(one)) == Nat.mod(Nat.pow(LV.ev(a), Nat.sub(_, 2n)), FS.prime(one)) : Nat}
210  %Equal.sym(Nat, FS.prime(one), 1n+K.pp(one), K.prime_eq(one, h1)) : {Nat.mod(Nat.pow(LV.ev(a), Nat.sub(1n+K.pp(one), 2n)), 1n+K.pp(one)) == Nat.mod(Nat.pow(LV.ev(a), Nat.sub(1n+K.pp(one), 2n)), _) : Nat}
211  {==}
212
213def inv_r(+one: Nat, +h1: {one == 1n : Nat}, +a: List<&2, Nat>, +ha: {FS.reduced(one, FS.prime(one), a) == True{} : Bool}) -> {FS.reduced(one, FS.prime(one), F.inv(a)) == True{} : Bool}:
214  pow_rv(one, h1, a, ha, F.inv_bits(), F.one(), one_r(one, h1), inv_bits01(one))
215
216# ---- the exponent of sqrt: (p + 1) / 4 ----
217
218def yp_lit() -> {L.norm16([975n, 0n, 1n]) == [975n, 0n, 1n, 0n, 0n, 0n, 0n, 0n, 0n, 0n, 0n, 0n, 0n, 0n, 0n, 0n] : List<&2, Nat>}:
219  {==}
220
221# 975 + 2^32 + 2 = c_p
222def yp_digits(+one: Nat, +h1: {one == 1n : Nat}) -> {Nat.add(Nat.add(FS.digits(one, L.norm16([975n, 0n, 1n])), one), one) == FS.cp(one) : Nat}:
223  %Equal.sym(List<&2, Nat>, L.norm16([975n, 0n, 1n]), [975n, 0n, 1n, 0n, 0n, 0n, 0n, 0n, 0n, 0n, 0n, 0n, 0n, 0n, 0n, 0n], yp_lit()) : {Nat.add(Nat.add(FS.digits(one, _), one), one) == FS.cp(one) : Nat}
224  %Equal.sym(Nat, FS.digits(one, [0n, 0n, 0n, 0n, 0n, 0n, 0n, 0n, 0n, 0n, 0n, 0n, 0n]), 0n, zeros13(one)) : {Nat.add(Nat.add(Nat.add(Nat.mul(one, 975n), C.shift(16n, Nat.add(Nat.mul(one, 0n), C.shift(16n, Nat.add(Nat.mul(one, 1n), C.shift(16n, _)))))), one), one) == Nat.add(Nat.mul(one, 977n), C.shift(16n, Nat.add(Nat.mul(one, 0n), C.shift(16n, Nat.add(Nat.mul(one, 1n), C.shift(16n, 0n)))))) : Nat}
225  %Equal.sym(Nat, Nat.mul(one, 977n), Nat.add(one, Nat.mul(one, 976n)), NA.mul_succ(one, 976n)) : {Nat.add(Nat.add(Nat.add(Nat.mul(one, 975n), C.shift(16n, Nat.add(Nat.mul(one, 0n), C.shift(16n, Nat.add(Nat.mul(one, 1n), C.shift(16n, 0n)))))), one), one) == Nat.add(_, C.shift(16n, Nat.add(Nat.mul(one, 0n), C.shift(16n, Nat.add(Nat.mul(one, 1n), C.shift(16n, 0n)))))) : Nat}
226  %Equal.sym(Nat, Nat.mul(one, 976n), Nat.add(one, Nat.mul(one, 975n)), NA.mul_succ(one, 975n)) : {Nat.add(Nat.add(Nat.add(Nat.mul(one, 975n), C.shift(16n, Nat.add(Nat.mul(one, 0n), C.shift(16n, Nat.add(Nat.mul(one, 1n), C.shift(16n, 0n)))))), one), one) == Nat.add(Nat.add(one, _), C.shift(16n, Nat.add(Nat.mul(one, 0n), C.shift(16n, Nat.add(Nat.mul(one, 1n), C.shift(16n, 0n)))))) : Nat}
227  %Equal.sym(Nat, Nat.mul(one, 0n), 0n, NA.mul_zero(one)) : {Nat.add(Nat.add(Nat.add(Nat.mul(one, 975n), C.shift(16n, Nat.add(_, C.shift(16n, Nat.add(Nat.mul(one, 1n), C.shift(16n, 0n)))))), one), one) == Nat.add(Nat.add(one, Nat.add(one, Nat.mul(one, 975n))), C.shift(16n, Nat.add(Nat.mul(one, 0n), C.shift(16n, Nat.add(Nat.mul(one, 1n), C.shift(16n, 0n)))))) : Nat}
228  %Equal.sym(Nat, Nat.mul(one, 1n), one, NA.mul_one(one)) : {Nat.add(Nat.add(Nat.add(Nat.mul(one, 975n), C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(_, C.shift(16n, 0n)))))), one), one) == Nat.add(Nat.add(one, Nat.add(one, Nat.mul(one, 975n))), C.shift(16n, Nat.add(Nat.mul(one, 0n), C.shift(16n, Nat.add(Nat.mul(one, 1n), C.shift(16n, 0n)))))) : Nat}
229  %Equal.sym(Nat, C.shift(16n, 0n), 0n, WW.shift_zero(16n)) : {Nat.add(Nat.add(Nat.add(Nat.mul(one, 975n), C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(one, _))))), one), one) == Nat.add(Nat.add(one, Nat.add(one, Nat.mul(one, 975n))), C.shift(16n, Nat.add(Nat.mul(one, 0n), C.shift(16n, Nat.add(Nat.mul(one, 1n), C.shift(16n, 0n)))))) : Nat}
230  %Equal.sym(Nat, Nat.add(one, 0n), one, NA.add_zero(one)) : {Nat.add(Nat.add(Nat.add(Nat.mul(one, 975n), C.shift(16n, Nat.add(0n, C.shift(16n, _)))), one), one) == Nat.add(Nat.add(one, Nat.add(one, Nat.mul(one, 975n))), C.shift(16n, Nat.add(Nat.mul(one, 0n), C.shift(16n, Nat.add(Nat.mul(one, 1n), C.shift(16n, 0n)))))) : Nat}
231  %Equal.sym(Nat, Nat.add(0n, C.shift(16n, one)), C.shift(16n, one), SR.zero_add(C.shift(16n, one))) : {Nat.add(Nat.add(Nat.add(Nat.mul(one, 975n), C.shift(16n, _)), one), one) == Nat.add(Nat.add(one, Nat.add(one, Nat.mul(one, 975n))), C.shift(16n, Nat.add(Nat.mul(one, 0n), C.shift(16n, Nat.add(Nat.mul(one, 1n), C.shift(16n, 0n)))))) : Nat}
232  %Equal.sym(Nat, C.shift(16n, C.shift(16n, one)), C.shift(32n, one), SR.shift_shift(16n, 16n, one)) : {Nat.add(Nat.add(Nat.add(Nat.mul(one, 975n), _), one), one) == Nat.add(Nat.add(one, Nat.add(one, Nat.mul(one, 975n))), C.shift(16n, Nat.add(Nat.mul(one, 0n), C.shift(16n, Nat.add(Nat.mul(one, 1n), C.shift(16n, 0n)))))) : Nat}
233  %Equal.sym(Nat, Nat.add(Nat.mul(one, 975n), C.shift(32n, one)), Nat.add(C.shift(32n, one), Nat.mul(one, 975n)), NA.add_comm(Nat.mul(one, 975n), C.shift(32n, one))) : {Nat.add(Nat.add(_, one), one) == Nat.add(Nat.add(one, Nat.add(one, Nat.mul(one, 975n))), C.shift(16n, Nat.add(Nat.mul(one, 0n), C.shift(16n, Nat.add(Nat.mul(one, 1n), C.shift(16n, 0n)))))) : Nat}
234  %Equal.sym(Nat, Nat.add(Nat.add(C.shift(32n, one), Nat.mul(one, 975n)), one), Nat.add(C.shift(32n, one), Nat.add(Nat.mul(one, 975n), one)), NA.add_assoc(C.shift(32n, one), Nat.mul(one, 975n), one)) : {Nat.add(_, one) == Nat.add(Nat.add(one, Nat.add(one, Nat.mul(one, 975n))), C.shift(16n, Nat.add(Nat.mul(one, 0n), C.shift(16n, Nat.add(Nat.mul(one, 1n), C.shift(16n, 0n)))))) : Nat}
235  %Equal.sym(Nat, Nat.add(Nat.mul(one, 975n), one), Nat.add(one, Nat.mul(one, 975n)), NA.add_comm(Nat.mul(one, 975n), one)) : {Nat.add(Nat.add(C.shift(32n, one), _), one) == Nat.add(Nat.add(one, Nat.add(one, Nat.mul(one, 975n))), C.shift(16n, Nat.add(Nat.mul(one, 0n), C.shift(16n, Nat.add(Nat.mul(one, 1n), C.shift(16n, 0n)))))) : Nat}
236  %Equal.sym(Nat, Nat.add(C.shift(32n, one), Nat.add(one, Nat.mul(one, 975n))), Nat.add(one, Nat.add(C.shift(32n, one), Nat.mul(one, 975n))), NA.add_swap(C.shift(32n, one), one, Nat.mul(one, 975n))) : {Nat.add(_, one) == Nat.add(Nat.add(one, Nat.add(one, Nat.mul(one, 975n))), C.shift(16n, Nat.add(Nat.mul(one, 0n), C.shift(16n, Nat.add(Nat.mul(one, 1n), C.shift(16n, 0n)))))) : Nat}
237  %Equal.sym(Nat, Nat.add(Nat.add(one, Nat.add(C.shift(32n, one), Nat.mul(one, 975n))), one), Nat.add(one, Nat.add(Nat.add(C.shift(32n, one), Nat.mul(one, 975n)), one)), NA.add_assoc(one, Nat.add(C.shift(32n, one), Nat.mul(one, 975n)), one)) : {_ == Nat.add(Nat.add(one, Nat.add(one, Nat.mul(one, 975n))), C.shift(16n, Nat.add(Nat.mul(one, 0n), C.shift(16n, Nat.add(Nat.mul(one, 1n), C.shift(16n, 0n)))))) : Nat}
238  %Equal.sym(Nat, Nat.add(Nat.add(C.shift(32n, one), Nat.mul(one, 975n)), one), Nat.add(C.shift(32n, one), Nat.add(Nat.mul(one, 975n), one)), NA.add_assoc(C.shift(32n, one), Nat.mul(one, 975n), one)) : {Nat.add(one, _) == Nat.add(Nat.add(one, Nat.add(one, Nat.mul(one, 975n))), C.shift(16n, Nat.add(Nat.mul(one, 0n), C.shift(16n, Nat.add(Nat.mul(one, 1n), C.shift(16n, 0n)))))) : Nat}
239  %Equal.sym(Nat, Nat.add(Nat.mul(one, 975n), one), Nat.add(one, Nat.mul(one, 975n)), NA.add_comm(Nat.mul(one, 975n), one)) : {Nat.add(one, Nat.add(C.shift(32n, one), _)) == Nat.add(Nat.add(one, Nat.add(one, Nat.mul(one, 975n))), C.shift(16n, Nat.add(Nat.mul(one, 0n), C.shift(16n, Nat.add(Nat.mul(one, 1n), C.shift(16n, 0n)))))) : Nat}
240  %Equal.sym(Nat, Nat.add(C.shift(32n, one), Nat.add(one, Nat.mul(one, 975n))), Nat.add(one, Nat.add(C.shift(32n, one), Nat.mul(one, 975n))), NA.add_swap(C.shift(32n, one), one, Nat.mul(one, 975n))) : {Nat.add(one, _) == Nat.add(Nat.add(one, Nat.add(one, Nat.mul(one, 975n))), C.shift(16n, Nat.add(Nat.mul(one, 0n), C.shift(16n, Nat.add(Nat.mul(one, 1n), C.shift(16n, 0n)))))) : Nat}
241  %Equal.sym(Nat, Nat.mul(one, 0n), 0n, NA.mul_zero(one)) : {Nat.add(one, Nat.add(one, Nat.add(C.shift(32n, one), Nat.mul(one, 975n)))) == Nat.add(Nat.add(one, Nat.add(one, Nat.mul(one, 975n))), C.shift(16n, Nat.add(_, C.shift(16n, Nat.add(Nat.mul(one, 1n), C.shift(16n, 0n)))))) : Nat}
242  %Equal.sym(Nat, Nat.mul(one, 1n), one, NA.mul_one(one)) : {Nat.add(one, Nat.add(one, Nat.add(C.shift(32n, one), Nat.mul(one, 975n)))) == Nat.add(Nat.add(one, Nat.add(one, Nat.mul(one, 975n))), C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(_, C.shift(16n, 0n)))))) : Nat}
243  %Equal.sym(Nat, C.shift(16n, 0n), 0n, WW.shift_zero(16n)) : {Nat.add(one, Nat.add(one, Nat.add(C.shift(32n, one), Nat.mul(one, 975n)))) == Nat.add(Nat.add(one, Nat.add(one, Nat.mul(one, 975n))), C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(one, _))))) : Nat}
244  %Equal.sym(Nat, Nat.add(one, 0n), one, NA.add_zero(one)) : {Nat.add(one, Nat.add(one, Nat.add(C.shift(32n, one), Nat.mul(one, 975n)))) == Nat.add(Nat.add(one, Nat.add(one, Nat.mul(one, 975n))), C.shift(16n, Nat.add(0n, C.shift(16n, _)))) : Nat}
245  %Equal.sym(Nat, Nat.add(0n, C.shift(16n, one)), C.shift(16n, one), SR.zero_add(C.shift(16n, one))) : {Nat.add(one, Nat.add(one, Nat.add(C.shift(32n, one), Nat.mul(one, 975n)))) == Nat.add(Nat.add(one, Nat.add(one, Nat.mul(one, 975n))), C.shift(16n, _)) : Nat}
246  %Equal.sym(Nat, C.shift(16n, C.shift(16n, one)), C.shift(32n, one), SR.shift_shift(16n, 16n, one)) : {Nat.add(one, Nat.add(one, Nat.add(C.shift(32n, one), Nat.mul(one, 975n)))) == Nat.add(Nat.add(one, Nat.add(one, Nat.mul(one, 975n))), _) : Nat}
247  %Equal.sym(Nat, Nat.add(Nat.add(one, Nat.add(one, Nat.mul(one, 975n))), C.shift(32n, one)), Nat.add(one, Nat.add(Nat.add(one, Nat.mul(one, 975n)), C.shift(32n, one))), NA.add_assoc(one, Nat.add(one, Nat.mul(one, 975n)), C.shift(32n, one))) : {Nat.add(one, Nat.add(one, Nat.add(C.shift(32n, one), Nat.mul(one, 975n)))) == _ : Nat}
248  %Equal.sym(Nat, Nat.add(Nat.add(one, Nat.mul(one, 975n)), C.shift(32n, one)), Nat.add(one, Nat.add(Nat.mul(one, 975n), C.shift(32n, one))), NA.add_assoc(one, Nat.mul(one, 975n), C.shift(32n, one))) : {Nat.add(one, Nat.add(one, Nat.add(C.shift(32n, one), Nat.mul(one, 975n)))) == Nat.add(one, _) : Nat}
249  %Equal.sym(Nat, Nat.add(Nat.mul(one, 975n), C.shift(32n, one)), Nat.add(C.shift(32n, one), Nat.mul(one, 975n)), NA.add_comm(Nat.mul(one, 975n), C.shift(32n, one))) : {Nat.add(one, Nat.add(one, Nat.add(C.shift(32n, one), Nat.mul(one, 975n)))) == Nat.add(one, Nat.add(one, _)) : Nat}
250  {==}
251
252def yp_limbs(+one: Nat, +h1: {one == 1n : Nat}) -> {FS.limbs16(one, 16n, L.norm16([975n, 0n, 1n])) == True{} : Bool}:
253  B.carry_limbs(one, h1, 32n, 16n, [975n, 0n, 1n], 0n, {==})
254
255def sq_split() -> {L.cbits(L.bits(L.norm16([975n, 0n, 1n]))) == List.append(&2, Nat, F.sqrt_bits(), [0n, 0n]) : List<&2, Nat>}:
256  {==}
257
258# hv of the bits of p + 1 is 4 hv(sqrt bits)
259def sq_four(+one: Nat) -> {BV.hv(L.cbits(L.bits(L.norm16([975n, 0n, 1n]))), one, 0n) == Nat.add(Nat.add(BV.hv(F.sqrt_bits(), one, 0n), BV.hv(F.sqrt_bits(), one, 0n)), Nat.add(BV.hv(F.sqrt_bits(), one, 0n), BV.hv(F.sqrt_bits(), one, 0n))) : Nat}:
260  %Equal.sym(List<&2, Nat>, L.cbits(L.bits(L.norm16([975n, 0n, 1n]))), List.append(&2, Nat, F.sqrt_bits(), [0n, 0n]), sq_split()) : {BV.hv(_, one, 0n) == Nat.add(Nat.add(BV.hv(F.sqrt_bits(), one, 0n), BV.hv(F.sqrt_bits(), one, 0n)), Nat.add(BV.hv(F.sqrt_bits(), one, 0n), BV.hv(F.sqrt_bits(), one, 0n))) : Nat}
261  %Equal.sym(Nat, BV.hv(List.append(&2, Nat, F.sqrt_bits(), [0n, 0n]), one, 0n), BV.hv([0n, 0n], one, BV.hv(F.sqrt_bits(), one, 0n)), BV.hv_app(one, F.sqrt_bits(), 0n, [0n, 0n])) : {_ == Nat.add(Nat.add(BV.hv(F.sqrt_bits(), one, 0n), BV.hv(F.sqrt_bits(), one, 0n)), Nat.add(BV.hv(F.sqrt_bits(), one, 0n), BV.hv(F.sqrt_bits(), one, 0n))) : Nat}
262  %Equal.sym(Nat, Nat.mul(0n, one), 0n, SR.zero_mul(one)) : {Nat.add(_, Nat.double(Nat.add(Nat.mul(0n, one), Nat.double(BV.hv(F.sqrt_bits(), one, 0n))))) == Nat.add(Nat.add(BV.hv(F.sqrt_bits(), one, 0n), BV.hv(F.sqrt_bits(), one, 0n)), Nat.add(BV.hv(F.sqrt_bits(), one, 0n), BV.hv(F.sqrt_bits(), one, 0n))) : Nat}
263  %Equal.sym(Nat, Nat.mul(0n, one), 0n, SR.zero_mul(one)) : {Nat.add(0n, Nat.double(Nat.add(_, Nat.double(BV.hv(F.sqrt_bits(), one, 0n))))) == Nat.add(Nat.add(BV.hv(F.sqrt_bits(), one, 0n), BV.hv(F.sqrt_bits(), one, 0n)), Nat.add(BV.hv(F.sqrt_bits(), one, 0n), BV.hv(F.sqrt_bits(), one, 0n))) : Nat}
264  %Equal.sym(Nat, Nat.double(BV.hv(F.sqrt_bits(), one, 0n)), Nat.add(BV.hv(F.sqrt_bits(), one, 0n), BV.hv(F.sqrt_bits(), one, 0n)), NA.double_self(BV.hv(F.sqrt_bits(), one, 0n))) : {Nat.add(0n, Nat.double(Nat.add(0n, _))) == Nat.add(Nat.add(BV.hv(F.sqrt_bits(), one, 0n), BV.hv(F.sqrt_bits(), one, 0n)), Nat.add(BV.hv(F.sqrt_bits(), one, 0n), BV.hv(F.sqrt_bits(), one, 0n))) : Nat}
265  %Equal.sym(Nat, Nat.add(0n, Nat.add(BV.hv(F.sqrt_bits(), one, 0n), BV.hv(F.sqrt_bits(), one, 0n))), Nat.add(BV.hv(F.sqrt_bits(), one, 0n), BV.hv(F.sqrt_bits(), one, 0n)), SR.zero_add(Nat.add(BV.hv(F.sqrt_bits(), one, 0n), BV.hv(F.sqrt_bits(), one, 0n)))) : {Nat.add(0n, Nat.double(_)) == Nat.add(Nat.add(BV.hv(F.sqrt_bits(), one, 0n), BV.hv(F.sqrt_bits(), one, 0n)), Nat.add(BV.hv(F.sqrt_bits(), one, 0n), BV.hv(F.sqrt_bits(), one, 0n))) : Nat}
266  %Equal.sym(Nat, Nat.double(Nat.add(BV.hv(F.sqrt_bits(), one, 0n), BV.hv(F.sqrt_bits(), one, 0n))), Nat.add(Nat.add(BV.hv(F.sqrt_bits(), one, 0n), BV.hv(F.sqrt_bits(), one, 0n)), Nat.add(BV.hv(F.sqrt_bits(), one, 0n), BV.hv(F.sqrt_bits(), one, 0n))), NA.double_self(Nat.add(BV.hv(F.sqrt_bits(), one, 0n), BV.hv(F.sqrt_bits(), one, 0n)))) : {Nat.add(0n, _) == Nat.add(Nat.add(BV.hv(F.sqrt_bits(), one, 0n), BV.hv(F.sqrt_bits(), one, 0n)), Nat.add(BV.hv(F.sqrt_bits(), one, 0n), BV.hv(F.sqrt_bits(), one, 0n))) : Nat}
267  %Equal.sym(Nat, Nat.add(Nat.add(BV.hv(F.sqrt_bits(), one, 0n), BV.hv(F.sqrt_bits(), one, 0n)), Nat.add(BV.hv(F.sqrt_bits(), one, 0n), BV.hv(F.sqrt_bits(), one, 0n))), Nat.add(BV.hv(F.sqrt_bits(), one, 0n), Nat.add(BV.hv(F.sqrt_bits(), one, 0n), Nat.add(BV.hv(F.sqrt_bits(), one, 0n), BV.hv(F.sqrt_bits(), one, 0n)))), NA.add_assoc(BV.hv(F.sqrt_bits(), one, 0n), BV.hv(F.sqrt_bits(), one, 0n), Nat.add(BV.hv(F.sqrt_bits(), one, 0n), BV.hv(F.sqrt_bits(), one, 0n)))) : {Nat.add(0n, _) == Nat.add(Nat.add(BV.hv(F.sqrt_bits(), one, 0n), BV.hv(F.sqrt_bits(), one, 0n)), Nat.add(BV.hv(F.sqrt_bits(), one, 0n), BV.hv(F.sqrt_bits(), one, 0n))) : Nat}
268  %Equal.sym(Nat, Nat.add(0n, Nat.add(BV.hv(F.sqrt_bits(), one, 0n), Nat.add(BV.hv(F.sqrt_bits(), one, 0n), Nat.add(BV.hv(F.sqrt_bits(), one, 0n), BV.hv(F.sqrt_bits(), one, 0n))))), Nat.add(BV.hv(F.sqrt_bits(), one, 0n), Nat.add(BV.hv(F.sqrt_bits(), one, 0n), Nat.add(BV.hv(F.sqrt_bits(), one, 0n), BV.hv(F.sqrt_bits(), one, 0n)))), SR.zero_add(Nat.add(BV.hv(F.sqrt_bits(), one, 0n), Nat.add(BV.hv(F.sqrt_bits(), one, 0n), Nat.add(BV.hv(F.sqrt_bits(), one, 0n), BV.hv(F.sqrt_bits(), one, 0n)))))) : {_ == Nat.add(Nat.add(BV.hv(F.sqrt_bits(), one, 0n), BV.hv(F.sqrt_bits(), one, 0n)), Nat.add(BV.hv(F.sqrt_bits(), one, 0n), BV.hv(F.sqrt_bits(), one, 0n))) : Nat}
269  %Equal.sym(Nat, Nat.add(Nat.add(BV.hv(F.sqrt_bits(), one, 0n), BV.hv(F.sqrt_bits(), one, 0n)), Nat.add(BV.hv(F.sqrt_bits(), one, 0n), BV.hv(F.sqrt_bits(), one, 0n))), Nat.add(BV.hv(F.sqrt_bits(), one, 0n), Nat.add(BV.hv(F.sqrt_bits(), one, 0n), Nat.add(BV.hv(F.sqrt_bits(), one, 0n), BV.hv(F.sqrt_bits(), one, 0n)))), NA.add_assoc(BV.hv(F.sqrt_bits(), one, 0n), BV.hv(F.sqrt_bits(), one, 0n), Nat.add(BV.hv(F.sqrt_bits(), one, 0n), BV.hv(F.sqrt_bits(), one, 0n)))) : {Nat.add(BV.hv(F.sqrt_bits(), one, 0n), Nat.add(BV.hv(F.sqrt_bits(), one, 0n), Nat.add(BV.hv(F.sqrt_bits(), one, 0n), BV.hv(F.sqrt_bits(), one, 0n)))) == _ : Nat}
270  {==}
271
272def yp_hv(+one: Nat, +h1: {one == 1n : Nat}) -> {BV.hv(L.bits(L.norm16([975n, 0n, 1n])), one, 0n) == FS.digits(one, L.norm16([975n, 0n, 1n])) : Nat}:
273  %Equal.sym(Nat, BV.hv(L.bits(L.norm16([975n, 0n, 1n])), one, 0n), Nat.add(LV.pos(16n, 0n), FS.digits(one, L.norm16([975n, 0n, 1n]))), BV.bits_v(one, h1, 16n, L.norm16([975n, 0n, 1n]), 0n, yp_limbs(one, h1))) : {_ == FS.digits(one, L.norm16([975n, 0n, 1n])) : Nat}
274  %Equal.sym(Nat, LV.pos(16n, 0n), 0n, LV.pos_zero(16n)) : {Nat.add(_, FS.digits(one, L.norm16([975n, 0n, 1n]))) == FS.digits(one, L.norm16([975n, 0n, 1n])) : Nat}
275  {==}
276
277# hv(bits of p + 1) + d + one = 2^256 with d = (c_p - 2)
278def sq_cb(+one: Nat, +h1: {one == 1n : Nat}) -> {Nat.add(Nat.add(BV.hv(L.cbits(L.bits(L.norm16([975n, 0n, 1n]))), one, 0n), FS.digits(one, L.norm16([975n, 0n, 1n]))), one) == C.shift(256n, one) : Nat}:
279  +bs = L.bits(L.norm16([975n, 0n, 1n]))
280  +hcb = BV.cb(one, bs, 0n, 0n, BV.bits01(L.norm16([975n, 0n, 1n])))
281  %Equal.sym(Nat, FS.digits(one, L.norm16([975n, 0n, 1n])), BV.hv(L.bits(L.norm16([975n, 0n, 1n])), one, 0n), Equal.sym(Nat, BV.hv(L.bits(L.norm16([975n, 0n, 1n])), one, 0n), FS.digits(one, L.norm16([975n, 0n, 1n])), yp_hv(one, h1))) : {Nat.add(Nat.add(BV.hv(L.cbits(L.bits(L.norm16([975n, 0n, 1n]))), one, 0n), _), one) == C.shift(256n, one) : Nat}
282  hcb
283
284def arr3(+d: Nat, +o: Nat, +h: Nat) -> {Nat.add(Nat.add(d, o), h) == Nat.add(Nat.add(h, d), o) : Nat}:
285  %Equal.sym(Nat, Nat.add(Nat.add(d, o), h), Nat.add(d, Nat.add(o, h)), NA.add_assoc(d, o, h)) : {_ == Nat.add(Nat.add(h, d), o) : Nat}
286  %Equal.sym(Nat, Nat.add(o, h), Nat.add(h, o), NA.add_comm(o, h)) : {Nat.add(d, _) == Nat.add(Nat.add(h, d), o) : Nat}
287  %Equal.sym(Nat, Nat.add(h, d), Nat.add(d, h), NA.add_comm(h, d)) : {Nat.add(d, Nat.add(h, o)) == Nat.add(_, o) : Nat}
288  %Equal.sym(Nat, Nat.add(Nat.add(d, h), o), Nat.add(d, Nat.add(h, o)), NA.add_assoc(d, h, o)) : {Nat.add(d, Nat.add(h, o)) == _ : Nat}
289  {==}
290
291def arr4(+m: Nat, +d: Nat, +o: Nat) -> {Nat.add(m, Nat.add(Nat.add(d, o), o)) == Nat.add(Nat.add(d, o), Nat.add(m, o)) : Nat}:
292  %Equal.sym(Nat, Nat.add(Nat.add(d, o), o), Nat.add(d, Nat.add(o, o)), NA.add_assoc(d, o, o)) : {Nat.add(m, _) == Nat.add(Nat.add(d, o), Nat.add(m, o)) : Nat}
293  %Equal.sym(Nat, Nat.add(m, Nat.add(d, Nat.add(o, o))), Nat.add(d, Nat.add(m, Nat.add(o, o))), NA.add_swap(m, d, Nat.add(o, o))) : {_ == Nat.add(Nat.add(d, o), Nat.add(m, o)) : Nat}
294  %Equal.sym(Nat, Nat.add(Nat.add(d, o), Nat.add(m, o)), Nat.add(d, Nat.add(o, Nat.add(m, o))), NA.add_assoc(d, o, Nat.add(m, o))) : {Nat.add(d, Nat.add(m, Nat.add(o, o))) == _ : Nat}
295  %Equal.sym(Nat, Nat.add(o, Nat.add(m, o)), Nat.add(m, Nat.add(o, o)), NA.add_swap(o, m, o)) : {Nat.add(d, Nat.add(m, Nat.add(o, o))) == Nat.add(d, _) : Nat}
296  {==}
297
298def 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}:
299  +d = FS.digits(one, L.norm16([975n, 0n, 1n]))
300  +hv4 = BV.hv(L.cbits(L.bits(L.norm16([975n, 0n, 1n]))), one, 0n)
301  +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))
302  +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))))
303  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)))
304
305def four_h(+h: Nat) -> {Nat.add(Nat.add(h, h), Nat.add(h, h)) == Nat.add(Nat.mul(h, 4n), 0n) : Nat}:
306  %Equal.sym(Nat, Nat.add(Nat.add(h, h), Nat.add(h, h)), Nat.add(h, Nat.add(h, Nat.add(h, h))), NA.add_assoc(h, h, Nat.add(h, h))) : {_ == Nat.add(Nat.mul(h, 4n), 0n) : Nat}
307  %Equal.sym(Nat, Nat.mul(h, 4n), Nat.add(h, Nat.mul(h, 3n)), NA.mul_succ(h, 3n)) : {Nat.add(h, Nat.add(h, Nat.add(h, h))) == Nat.add(_, 0n) : Nat}
308  %Equal.sym(Nat, Nat.mul(h, 3n), Nat.add(h, Nat.mul(h, 2n)), NA.mul_succ(h, 2n)) : {Nat.add(h, Nat.add(h, Nat.add(h, h))) == Nat.add(Nat.add(h, _), 0n) : Nat}
309  %Equal.sym(Nat, Nat.mul(h, 2n), Nat.add(h, Nat.mul(h, 1n)), NA.mul_succ(h, 1n)) : {Nat.add(h, Nat.add(h, Nat.add(h, h))) == Nat.add(Nat.add(h, Nat.add(h, _)), 0n) : Nat}
310  %Equal.sym(Nat, Nat.mul(h, 1n), h, NA.mul_one(h)) : {Nat.add(h, Nat.add(h, Nat.add(h, h))) == Nat.add(Nat.add(h, Nat.add(h, Nat.add(h, _))), 0n) : Nat}
311  %Equal.sym(Nat, Nat.add(Nat.add(h, Nat.add(h, Nat.add(h, h))), 0n), Nat.add(h, Nat.add(h, Nat.add(h, h))), NA.add_zero(Nat.add(h, Nat.add(h, Nat.add(h, h))))) : {Nat.add(h, Nat.add(h, Nat.add(h, h))) == _ : Nat}
312  {==}
313
314# 4 hv(sqrt bits) = p + 1, so hv(sqrt bits) = (p + 1) / 4
315def exp_sqrt(+one: Nat, +h1: {one == 1n : Nat}) -> {BV.hv(F.sqrt_bits(), one, 0n) == Nat.div(Nat.add(1n+K.pp(one), 1n), 4n) : Nat}:
316  +d = FS.digits(one, L.norm16([975n, 0n, 1n]))
317  +h = BV.hv(F.sqrt_bits(), one, 0n)
318  +e = NR.add_cancel(Nat.add(d, one), BV.hv(L.cbits(L.bits(L.norm16([975n, 0n, 1n]))), one, 0n), Nat.add(1n+K.pp(one), one), sq_g(one, h1))
319  +e4 = Equal.trans(Nat, Nat.add(Nat.add(h, h), Nat.add(h, h)), BV.hv(L.cbits(L.bits(L.norm16([975n, 0n, 1n]))), one, 0n), Nat.add(1n+K.pp(one), one), Equal.sym(Nat, BV.hv(L.cbits(L.bits(L.norm16([975n, 0n, 1n]))), one, 0n), Nat.add(Nat.add(h, h), Nat.add(h, h)), sq_four(one)), e)
320  %Equal.sym(Nat, 1n, one, Equal.sym(Nat, one, 1n, h1)) : {BV.hv(F.sqrt_bits(), one, 0n) == Nat.div(Nat.add(1n+K.pp(one), _), 4n) : Nat}
321  %Equal.sym(Nat, Nat.add(1n+K.pp(one), one), Nat.add(Nat.add(BV.hv(F.sqrt_bits(), one, 0n), BV.hv(F.sqrt_bits(), one, 0n)), Nat.add(BV.hv(F.sqrt_bits(), one, 0n), BV.hv(F.sqrt_bits(), one, 0n))), Equal.sym(Nat, Nat.add(Nat.add(BV.hv(F.sqrt_bits(), one, 0n), BV.hv(F.sqrt_bits(), one, 0n)), Nat.add(BV.hv(F.sqrt_bits(), one, 0n), BV.hv(F.sqrt_bits(), one, 0n))), Nat.add(1n+K.pp(one), one), e4)) : {BV.hv(F.sqrt_bits(), one, 0n) == Nat.div(_, 4n) : Nat}
322  %Equal.sym(Nat, Nat.add(Nat.add(BV.hv(F.sqrt_bits(), one, 0n), BV.hv(F.sqrt_bits(), one, 0n)), Nat.add(BV.hv(F.sqrt_bits(), one, 0n), BV.hv(F.sqrt_bits(), one, 0n))), Nat.add(Nat.mul(BV.hv(F.sqrt_bits(), one, 0n), 4n), 0n), four_h(BV.hv(F.sqrt_bits(), one, 0n))) : {BV.hv(F.sqrt_bits(), one, 0n) == Nat.div(_, 4n) : Nat}
323  Equal.sym(Nat, Nat.div(Nat.add(Nat.mul(BV.hv(F.sqrt_bits(), one, 0n), 4n), 0n), 4n), BV.hv(F.sqrt_bits(), one, 0n), NR.div_of(BV.hv(F.sqrt_bits(), one, 0n), 3n, 0n, {==}))
324
325def sq01(xs: List<&2, Nat>, +ys: List<&2, Nat>, +h: {BV.all01(List.append(&2, Nat, xs, ys)) == True{} : Bool}) -> {BV.all01(xs) == True{} : Bool}:
326  match xs:
327    case Nil{}:
328      {==}
329    case +x <> +t:
330      Lg.and_intro(Nat.is_lt(x, 2n), BV.all01(t), Lg.and_left(Nat.is_lt(x, 2n), BV.all01(List.append(&2, Nat, t, ys)), h), sq01(t, ys, Lg.and_right(Nat.is_lt(x, 2n), BV.all01(List.append(&2, Nat, t, ys)), h)))
331
332def sqrt_bits01(+one: Nat) -> {BV.all01(F.sqrt_bits()) == True{} : Bool}:
333  +bs = L.cbits(L.bits(L.norm16([975n, 0n, 1n])))
334  sq01(F.sqrt_bits(), [0n, 0n], Lg.subst(List<&2, Nat>, z => {BV.all01(z) == True{} : Bool}, bs, List.append(&2, Nat, F.sqrt_bits(), [0n, 0n]), sq_split(), BV.cbits01(L.bits(L.norm16([975n, 0n, 1n])))))
335
336def sqrt_v(+one: Nat, +h1: {one == 1n : Nat}, +a: List<&2, Nat>, +ha: {FS.reduced(one, FS.prime(one), a) == True{} : Bool}) -> {FS.value(one, F.sqrt(a)) == FS.fsqrt(FS.prime(one), FS.value(one, a)) : Nat}:
337  %Equal.sym(Nat, FS.value(one, F.pow(a, F.sqrt_bits(), F.one())), LV.ev(F.pow(a, F.sqrt_bits(), F.one())), LV.ev_value(one, h1, F.pow(a, F.sqrt_bits(), F.one()))) : {_ == Nat.mod(Nat.pow(FS.value(one, a), Nat.div(Nat.add(FS.prime(one), 1n), 4n)), FS.prime(one)) : Nat}
338  %Equal.sym(Nat, LV.ev(F.pow(a, F.sqrt_bits(), F.one())), Nat.mod(Nat.pow(LV.ev(a), BV.hv(F.sqrt_bits(), one, 0n)), 1n+K.pp(one)), pow_ev(one, h1, a, ha, F.sqrt_bits(), F.one(), one_r(one, h1), 0n, one_e(one, h1, LV.ev(a)), sqrt_bits01(one))) : {_ == Nat.mod(Nat.pow(FS.value(one, a), Nat.div(Nat.add(FS.prime(one), 1n), 4n)), FS.prime(one)) : Nat}
339  %Equal.sym(Nat, BV.hv(F.sqrt_bits(), one, 0n), Nat.div(Nat.add(1n+K.pp(one), 1n), 4n), exp_sqrt(one, h1)) : {Nat.mod(Nat.pow(LV.ev(a), _), 1n+K.pp(one)) == Nat.mod(Nat.pow(FS.value(one, a), Nat.div(Nat.add(FS.prime(one), 1n), 4n)), FS.prime(one)) : Nat}
340  %Equal.sym(Nat, FS.value(one, a), LV.ev(a), LV.ev_value(one, h1, a)) : {Nat.mod(Nat.pow(LV.ev(a), Nat.div(Nat.add(1n+K.pp(one), 1n), 4n)), 1n+K.pp(one)) == Nat.mod(Nat.pow(_, Nat.div(Nat.add(FS.prime(one), 1n), 4n)), FS.prime(one)) : Nat}
341  %Equal.sym(Nat, FS.prime(one), 1n+K.pp(one), K.prime_eq(one, h1)) : {Nat.mod(Nat.pow(LV.ev(a), Nat.div(Nat.add(1n+K.pp(one), 1n), 4n)), 1n+K.pp(one)) == Nat.mod(Nat.pow(LV.ev(a), Nat.div(Nat.add(_, 1n), 4n)), FS.prime(one)) : Nat}
342  %Equal.sym(Nat, FS.prime(one), 1n+K.pp(one), K.prime_eq(one, h1)) : {Nat.mod(Nat.pow(LV.ev(a), Nat.div(Nat.add(1n+K.pp(one), 1n), 4n)), 1n+K.pp(one)) == Nat.mod(Nat.pow(LV.ev(a), Nat.div(Nat.add(1n+K.pp(one), 1n), 4n)), _) : Nat}
343  {==}
344
345def sqrt_r(+one: Nat, +h1: {one == 1n : Nat}, +a: List<&2, Nat>, +ha: {FS.reduced(one, FS.prime(one), a) == True{} : Bool}) -> {FS.reduced(one, FS.prime(one), F.sqrt(a)) == True{} : Bool}:
346  pow_rv(one, h1, a, ha, F.sqrt_bits(), F.one(), one_r(one, h1), sqrt_bits01(one))