~/jendhub

proofs/crypto/secp256k1/fieldops.bend

bend-collections-laws-crypto@1.0.0.0 · 222 lines · 33 definitions

1# GENERATED by tools/generators/rw.py from ../../../tools/generators/secp256k1_hand/fieldops.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/arith.bend as AR
10import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as NA
11import bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/arith.bend as NR
12import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/limbs.bend as LV
13import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/fprot.bend as FR
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/reducek.bend as RK
17import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/consts.bend as K
18import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/negate.bend as NG
19import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/listops.bend as LO
20
21# GF(p) of src/crypto/secp256k1/field.bend against spec/crypto/secp256k1/field.bend:
22# on reduced inputs (16 limbs below 2^16, value below p) every operation
23# returns a reduced element whose value is the specified one, exactly.
24
25# ---- sizes ----
26
27def tt_lt(+one: Nat, +h1: {one == 1n : Nat}, +x: List<&2, Nat>, +h: {FS.limbs16(one, 16n, x) == True{} : Bool}) -> {Nat.is_lt(LV.ev(x), C.shift(256n, one)) == True{} : Bool}:
28  I.lt_subst_r(LV.ev(x), LV.pos(16n, one), C.shift(256n, one), B.pos16(one), B.limbs_lt(one, h1, 16n, x, h))
29
30def three_le(+one: Nat, +h1: {one == 1n : Nat}) -> {Nat.is_le(3n, C.shift(256n, one)) == True{} : Bool}:
31  K.small_le(one, h1, 256n, 3n, {==})
32
33# below 3 2^256 is below 2^512
34def lt3(+one: Nat, +h1: {one == 1n : Nat}, +x: Nat, +hx: {Nat.is_lt(x, Nat.add(C.shift(256n, one), Nat.add(C.shift(256n, one), C.shift(256n, one)))) == True{} : Bool}) -> {Nat.is_lt(x, Nat.mul(C.shift(256n, one), C.shift(256n, one))) == True{} : Bool}:
35  +t = C.shift(256n, one)
36  +e3 = Equal.trans(Nat, Nat.add(t, Nat.add(t, t)), Nat.add(t, Nat.add(t, Nat.add(t, 0n))), Nat.mul(3n, t), Equal.cong(Nat, Nat, z => Nat.add(t, Nat.add(t, z)), t, Nat.add(t, 0n), Equal.sym(Nat, Nat.add(t, 0n), t, NA.add_zero(t))), {==})
37  N.lt_le_trans(x, Nat.mul(3n, t), Nat.mul(t, t), I.lt_subst_r(x, Nat.add(t, Nat.add(t, t)), Nat.mul(3n, t), e3, hx), AR.mul_le(3n, t, t, three_le(one, h1)))
38
39def sum_lt(+one: Nat, +h1: {one == 1n : Nat}, +a: Nat, +b: Nat, +ha: {Nat.is_lt(a, C.shift(256n, one)) == True{} : Bool}, +hb: {Nat.is_lt(b, C.shift(256n, one)) == True{} : Bool}) -> {Nat.is_lt(Nat.add(a, b), Nat.mul(C.shift(256n, one), C.shift(256n, one))) == True{} : Bool}:
40  +t = C.shift(256n, one)
41  lt3(one, h1, Nat.add(a, b), I.lt_le_add(a, b, t, Nat.add(t, t), ha, N.le_trans(b, t, Nat.add(t, t), N.lt_le(b, t, hb), N.le_add_right(t, t))))
42
43def mul_lt(+a: Nat, +b: Nat, +t: Nat, +ha: {Nat.is_lt(a, t) == True{} : Bool}, +hb: {Nat.is_lt(b, t) == True{} : Bool}) -> {Nat.is_lt(Nat.mul(a, b), Nat.mul(t, t)) == True{} : Bool}:
44  match t:
45    case 0n:
46      Empty.absurd({Nat.is_lt(Nat.mul(a, b), Nat.mul(0n, 0n)) == True{} : Bool}, N.lt_zero_absurd(a, ha))
47    case 1n+ +tp:
48      +s1 = I.le_mul2(a, b, tp, 1n+tp, N.lt_succ_le(a, tp, ha), N.lt_le(b, 1n+tp, hb))
49      +mm = Nat.mul(tp, 1n+tp)
50      +s2 = I.lt_subst_r(mm, Nat.add(mm, 1n+tp), Nat.add(1n+tp, mm), NA.add_comm(mm, 1n+tp), I.lt_add_pos(mm, 1n+tp, {==}))
51      N.le_lt_trans(Nat.mul(a, b), mm, Nat.add(1n+tp, mm), s1, s2)
52
53# ---- the reduction mod p ----
54
55def red_e(+one: Nat, +h1: {one == 1n : Nat}, +xs: List<&2, Nat>, +hx: {Nat.is_lt(LV.ev(xs), Nat.mul(C.shift(256n, one), C.shift(256n, one))) == True{} : Bool}) -> {LV.ev(F.reduce(xs)) == Nat.mod(LV.ev(xs), 1n+K.pp(one)) : Nat}:
56  RK.reduce3_vv(one, h1, K.pp(one), F.c(), K.hm_p(one, h1), K.cp_cc(one, h1), K.cp_hb(one, h1), xs, hx)
57
58def red_l(+one: Nat, +h1: {one == 1n : Nat}, +xs: List<&2, Nat>, +hx: {Nat.is_lt(LV.ev(xs), Nat.mul(C.shift(256n, one), C.shift(256n, one))) == True{} : Bool}) -> {FS.limbs16(one, 16n, F.reduce(xs)) == True{} : Bool}:
59  RK.reduce3_lv(one, h1, F.c(), K.cp_cc(one, h1), K.cp_hb(one, h1), xs, hx)
60
61# the reduced value below p, in the specification's terms
62def red_r(+one: Nat, +h1: {one == 1n : Nat}, +xs: List<&2, Nat>, +hx: {Nat.is_lt(LV.ev(xs), Nat.mul(C.shift(256n, one), C.shift(256n, one))) == True{} : Bool}) -> {FS.reduced(one, FS.prime(one), F.reduce(xs)) == True{} : Bool}:
63  +lt = I.lt_subst_l(Nat.mod(LV.ev(xs), 1n+K.pp(one)), LV.ev(F.reduce(xs)), 1n+K.pp(one), Equal.sym(Nat, LV.ev(F.reduce(xs)), Nat.mod(LV.ev(xs), 1n+K.pp(one)), red_e(one, h1, xs, hx)), NR.dm_lt(K.pp(one), LV.ev(xs)))
64  +lt2 = I.lt_subst_l(LV.ev(F.reduce(xs)), FS.value(one, F.reduce(xs)), 1n+K.pp(one), Equal.sym(Nat, FS.value(one, F.reduce(xs)), LV.ev(F.reduce(xs)), LV.ev_value(one, h1, F.reduce(xs))), lt)
65  +lt3 = I.lt_subst_r(FS.value(one, F.reduce(xs)), 1n+K.pp(one), FS.prime(one), Equal.sym(Nat, FS.prime(one), 1n+K.pp(one), K.prime_eq(one, h1)), lt2)
66  Lg.and_intro(FS.limbs16(one, 16n, F.reduce(xs)), Nat.is_lt(FS.value(one, F.reduce(xs)), FS.prime(one)), red_l(one, h1, xs, hx), lt3)
67
68def red_v(+one: Nat, +h1: {one == 1n : Nat}, +xs: List<&2, Nat>, +hx: {Nat.is_lt(LV.ev(xs), Nat.mul(C.shift(256n, one), C.shift(256n, one))) == True{} : Bool}) -> {FS.value(one, F.reduce(xs)) == Nat.mod(LV.ev(xs), FS.prime(one)) : Nat}:
69  %Equal.sym(Nat, FS.value(one, F.reduce(xs)), LV.ev(F.reduce(xs)), LV.ev_value(one, h1, F.reduce(xs))) : {_ == Nat.mod(LV.ev(xs), FS.prime(one)) : Nat}
70  %Equal.sym(Nat, LV.ev(F.reduce(xs)), Nat.mod(LV.ev(xs), 1n+K.pp(one)), red_e(one, h1, xs, hx)) : {_ == Nat.mod(LV.ev(xs), FS.prime(one)) : Nat}
71  %Equal.sym(Nat, 1n+K.pp(one), FS.prime(one), Equal.sym(Nat, FS.prime(one), 1n+K.pp(one), K.prime_eq(one, h1))) : {Nat.mod(LV.ev(xs), _) == Nat.mod(LV.ev(xs), FS.prime(one)) : Nat}
72  {==}
73
74# ---- reduced inputs ----
75
76def r16(+one: Nat, +x: List<&2, Nat>, +h: {FS.reduced(one, FS.prime(one), x) == True{} : Bool}) -> {FS.limbs16(one, 16n, x) == True{} : Bool}:
77  Lg.and_left(FS.limbs16(one, 16n, x), Nat.is_lt(FS.value(one, x), FS.prime(one)), h)
78
79def rlt(+one: Nat, +h1: {one == 1n : Nat}, +x: List<&2, Nat>, +h: {FS.reduced(one, FS.prime(one), x) == True{} : Bool}) -> {Nat.is_lt(LV.ev(x), 1n+K.pp(one)) == True{} : Bool}:
80  +l = Lg.and_right(FS.limbs16(one, 16n, x), Nat.is_lt(FS.value(one, x), FS.prime(one)), h)
81  +l2 = I.lt_subst_l(FS.value(one, x), LV.ev(x), FS.prime(one), LV.ev_value(one, h1, x), l)
82  I.lt_subst_r(LV.ev(x), FS.prime(one), 1n+K.pp(one), K.prime_eq(one, h1), l2)
83
84def rtt(+one: Nat, +h1: {one == 1n : Nat}, +x: List<&2, Nat>, +h: {FS.reduced(one, FS.prime(one), x) == True{} : Bool}) -> {Nat.is_lt(LV.ev(x), C.shift(256n, one)) == True{} : Bool}:
85  tt_lt(one, h1, x, r16(one, x, h))
86
87# ---- add, mul ----
88
89def add_hx(+one: Nat, +h1: {one == 1n : Nat}, +a: List<&2, Nat>, +b: List<&2, Nat>, +ha: {FS.reduced(one, FS.prime(one), a) == True{} : Bool}, +hb: {FS.reduced(one, FS.prime(one), b) == True{} : Bool}) -> {Nat.is_lt(LV.ev(L.add(a, b)), Nat.mul(C.shift(256n, one), C.shift(256n, one))) == True{} : Bool}:
90  %Equal.sym(Nat, LV.ev(L.add(a, b)), Nat.add(LV.ev(a), LV.ev(b)), LV.add_v(a, b)) : {Nat.is_lt(_, Nat.mul(C.shift(256n, one), C.shift(256n, one))) == True{} : Bool}
91  sum_lt(one, h1, LV.ev(a), LV.ev(b), rtt(one, h1, a, ha), rtt(one, h1, b, hb))
92
93def add_v(+one: Nat, +h1: {one == 1n : Nat}, +a: List<&2, Nat>, +b: List<&2, Nat>, +ha: {FS.reduced(one, FS.prime(one), a) == True{} : Bool}, +hb: {FS.reduced(one, FS.prime(one), b) == True{} : Bool}) -> {FS.value(one, F.add(a, b)) == FS.madd(FS.prime(one), FS.value(one, a), FS.value(one, b)) : Nat}:
94  %Equal.sym(List<&2, Nat>, F.add(a, b), F.add_u(a, b), FR.f_add(a, b)) : {FS.value(one, _) == FS.madd(FS.prime(one), FS.value(one, a), FS.value(one, b)) : Nat}
95  %Equal.sym(Nat, FS.value(one, F.reduce(L.add(a, b))), Nat.mod(LV.ev(L.add(a, b)), FS.prime(one)), red_v(one, h1, L.add(a, b), add_hx(one, h1, a, b, ha, hb))) : {_ == Nat.mod(Nat.add(FS.value(one, a), FS.value(one, b)), FS.prime(one)) : Nat}
96  %Equal.sym(Nat, LV.ev(L.add(a, b)), Nat.add(LV.ev(a), LV.ev(b)), LV.add_v(a, b)) : {Nat.mod(_, FS.prime(one)) == Nat.mod(Nat.add(FS.value(one, a), FS.value(one, b)), FS.prime(one)) : Nat}
97  %Equal.sym(Nat, LV.ev(a), FS.value(one, a), Equal.sym(Nat, FS.value(one, a), LV.ev(a), LV.ev_value(one, h1, a))) : {Nat.mod(Nat.add(_, LV.ev(b)), FS.prime(one)) == Nat.mod(Nat.add(FS.value(one, a), FS.value(one, b)), FS.prime(one)) : Nat}
98  %Equal.sym(Nat, LV.ev(b), FS.value(one, b), Equal.sym(Nat, FS.value(one, b), LV.ev(b), LV.ev_value(one, h1, b))) : {Nat.mod(Nat.add(FS.value(one, a), _), FS.prime(one)) == Nat.mod(Nat.add(FS.value(one, a), FS.value(one, b)), FS.prime(one)) : Nat}
99  {==}
100
101def add_r(+one: Nat, +h1: {one == 1n : Nat}, +a: List<&2, Nat>, +b: List<&2, Nat>, +ha: {FS.reduced(one, FS.prime(one), a) == True{} : Bool}, +hb: {FS.reduced(one, FS.prime(one), b) == True{} : Bool}) -> {FS.reduced(one, FS.prime(one), F.add(a, b)) == True{} : Bool}:
102  %Equal.sym(List<&2, Nat>, F.add(a, b), F.add_u(a, b), FR.f_add(a, b)) : {FS.reduced(one, FS.prime(one), _) == True{} : Bool}
103  red_r(one, h1, L.add(a, b), add_hx(one, h1, a, b, ha, hb))
104
105def mul_hx(+one: Nat, +h1: {one == 1n : Nat}, +a: List<&2, Nat>, +b: List<&2, Nat>, +ha: {FS.reduced(one, FS.prime(one), a) == True{} : Bool}, +hb: {FS.reduced(one, FS.prime(one), b) == True{} : Bool}) -> {Nat.is_lt(LV.ev(L.conv(a, b)), Nat.mul(C.shift(256n, one), C.shift(256n, one))) == True{} : Bool}:
106  %Equal.sym(Nat, LV.ev(L.conv(a, b)), Nat.mul(LV.ev(a), LV.ev(b)), LV.conv_v(a, b)) : {Nat.is_lt(_, Nat.mul(C.shift(256n, one), C.shift(256n, one))) == True{} : Bool}
107  mul_lt(LV.ev(a), LV.ev(b), C.shift(256n, one), rtt(one, h1, a, ha), rtt(one, h1, b, hb))
108
109def mul_v(+one: Nat, +h1: {one == 1n : Nat}, +a: List<&2, Nat>, +b: List<&2, Nat>, +ha: {FS.reduced(one, FS.prime(one), a) == True{} : Bool}, +hb: {FS.reduced(one, FS.prime(one), b) == True{} : Bool}) -> {FS.value(one, F.mul(a, b)) == FS.mmul(FS.prime(one), FS.value(one, a), FS.value(one, b)) : Nat}:
110  %Equal.sym(List<&2, Nat>, F.mul(a, b), F.mul_u(a, b), FR.f_mul(a, b)) : {FS.value(one, _) == FS.mmul(FS.prime(one), FS.value(one, a), FS.value(one, b)) : Nat}
111  %Equal.sym(Nat, FS.value(one, F.reduce(L.conv(a, b))), Nat.mod(LV.ev(L.conv(a, b)), FS.prime(one)), red_v(one, h1, L.conv(a, b), mul_hx(one, h1, a, b, ha, hb))) : {_ == Nat.mod(Nat.mul(FS.value(one, a), FS.value(one, b)), FS.prime(one)) : Nat}
112  %Equal.sym(Nat, LV.ev(L.conv(a, b)), Nat.mul(LV.ev(a), LV.ev(b)), LV.conv_v(a, b)) : {Nat.mod(_, FS.prime(one)) == Nat.mod(Nat.mul(FS.value(one, a), FS.value(one, b)), FS.prime(one)) : Nat}
113  %Equal.sym(Nat, LV.ev(a), FS.value(one, a), Equal.sym(Nat, FS.value(one, a), LV.ev(a), LV.ev_value(one, h1, a))) : {Nat.mod(Nat.mul(_, LV.ev(b)), FS.prime(one)) == Nat.mod(Nat.mul(FS.value(one, a), FS.value(one, b)), FS.prime(one)) : Nat}
114  %Equal.sym(Nat, LV.ev(b), FS.value(one, b), Equal.sym(Nat, FS.value(one, b), LV.ev(b), LV.ev_value(one, h1, b))) : {Nat.mod(Nat.mul(FS.value(one, a), _), FS.prime(one)) == Nat.mod(Nat.mul(FS.value(one, a), FS.value(one, b)), FS.prime(one)) : Nat}
115  {==}
116
117def mul_r(+one: Nat, +h1: {one == 1n : Nat}, +a: List<&2, Nat>, +b: List<&2, Nat>, +ha: {FS.reduced(one, FS.prime(one), a) == True{} : Bool}, +hb: {FS.reduced(one, FS.prime(one), b) == True{} : Bool}) -> {FS.reduced(one, FS.prime(one), F.mul(a, b)) == True{} : Bool}:
118  %Equal.sym(List<&2, Nat>, F.mul(a, b), F.mul_u(a, b), FR.f_mul(a, b)) : {FS.reduced(one, FS.prime(one), _) == True{} : Bool}
119  red_r(one, h1, L.conv(a, b), mul_hx(one, h1, a, b, ha, hb))
120
121# ---- sub, neg ----
122
123def negr_e(+one: Nat, +h1: {one == 1n : Nat}, +b: List<&2, Nat>, +hb: {FS.reduced(one, FS.prime(one), b) == True{} : Bool}) -> {Nat.add(LV.ev(L.neg_raw(F.c(), b)), LV.ev(b)) == 1n+K.pp(one) : Nat}:
124  NG.neg_vv(one, h1, K.pp(one), F.c(), K.hm_p(one, h1), b, rlt(one, h1, b, hb))
125
126def negr_le(+one: Nat, +h1: {one == 1n : Nat}, +b: List<&2, Nat>, +hb: {FS.reduced(one, FS.prime(one), b) == True{} : Bool}) -> {Nat.is_le(LV.ev(L.neg_raw(F.c(), b)), C.shift(256n, one)) == True{} : Bool}:
127  +m = {1n+K.pp(one) : Nat}
128  +nb = LV.ev(L.neg_raw(F.c(), b))
129  +mt = I.le_subst_r(m, Nat.add(m, FS.cp(one)), C.shift(256n, one), K.hm_p(one, h1), N.le_add_right(m, FS.cp(one)))
130  N.le_trans(nb, m, C.shift(256n, one), I.le_subst_r(nb, Nat.add(nb, LV.ev(b)), m, negr_e(one, h1, b, hb), N.le_add_right(nb, LV.ev(b))), mt)
131
132def sub_hx(+one: Nat, +h1: {one == 1n : Nat}, +a: List<&2, Nat>, +b: List<&2, Nat>, +ha: {FS.reduced(one, FS.prime(one), a) == True{} : Bool}, +hb: {FS.reduced(one, FS.prime(one), b) == True{} : Bool}) -> {Nat.is_lt(LV.ev(L.add(a, L.neg_raw(F.c(), b))), Nat.mul(C.shift(256n, one), C.shift(256n, one))) == True{} : Bool}:
133  %Equal.sym(Nat, LV.ev(L.add(a, L.neg_raw(F.c(), b))), Nat.add(LV.ev(a), LV.ev(L.neg_raw(F.c(), b))), LV.add_v(a, L.neg_raw(F.c(), b))) : {Nat.is_lt(_, Nat.mul(C.shift(256n, one), C.shift(256n, one))) == True{} : Bool}
134  lt3(one, h1, Nat.add(LV.ev(a), LV.ev(L.neg_raw(F.c(), b))), I.lt_le_add(LV.ev(a), LV.ev(L.neg_raw(F.c(), b)), C.shift(256n, one), Nat.add(C.shift(256n, one), C.shift(256n, one)), rtt(one, h1, a, ha), N.le_trans(LV.ev(L.neg_raw(F.c(), b)), C.shift(256n, one), Nat.add(C.shift(256n, one), C.shift(256n, one)), negr_le(one, h1, b, hb), N.le_add_right(C.shift(256n, one), C.shift(256n, one)))))
135
136# F.sub looks at a first; a reduced a has 16 limbs
137def sub_go(+one: Nat, +h1: {one == 1n : Nat}, a: List<&2, Nat>, +b: List<&2, Nat>, +ha: {FS.reduced(one, FS.prime(one), a) == True{} : Bool}) -> {F.sub(a, b) == F.reduce(L.add(a, L.neg_raw(F.c(), b))) : List<&2, Nat>}:
138  match a:
139    case Nil{}:
140      Empty.absurd({F.sub([], b) == F.reduce(L.add([], L.neg_raw(F.c(), b))) : List<&2, Nat>}, Lg.false_true(Lg.and_left(FS.limbs16(one, 16n, []), Nat.is_lt(FS.value(one, []), FS.prime(one)), ha)))
141    case x <> t:
142      {==}
143
144def sub_v(+one: Nat, +h1: {one == 1n : Nat}, +a: List<&2, Nat>, +b: List<&2, Nat>, +ha: {FS.reduced(one, FS.prime(one), a) == True{} : Bool}, +hb: {FS.reduced(one, FS.prime(one), b) == True{} : Bool}) -> {FS.value(one, F.sub(a, b)) == FS.msub(FS.prime(one), FS.value(one, a), FS.value(one, b)) : Nat}:
145  %Equal.sym(List<&2, Nat>, F.sub(a, b), F.reduce(L.add(a, L.neg_raw(F.c(), b))), sub_go(one, h1, a, b, ha)) : {FS.value(one, _) == FS.msub(FS.prime(one), FS.value(one, a), FS.value(one, b)) : Nat}
146  %Equal.sym(Nat, FS.value(one, F.reduce(L.add(a, L.neg_raw(F.c(), b)))), Nat.mod(LV.ev(L.add(a, L.neg_raw(F.c(), b))), FS.prime(one)), red_v(one, h1, L.add(a, L.neg_raw(F.c(), b)), sub_hx(one, h1, a, b, ha, hb))) : {_ == Nat.mod(Nat.sub(Nat.add(FS.value(one, a), FS.prime(one)), Nat.mod(FS.value(one, b), FS.prime(one))), FS.prime(one)) : Nat}
147  %Equal.sym(Nat, LV.ev(L.add(a, L.neg_raw(F.c(), b))), Nat.add(LV.ev(a), LV.ev(L.neg_raw(F.c(), b))), LV.add_v(a, L.neg_raw(F.c(), b))) : {Nat.mod(_, FS.prime(one)) == Nat.mod(Nat.sub(Nat.add(FS.value(one, a), FS.prime(one)), Nat.mod(FS.value(one, b), FS.prime(one))), FS.prime(one)) : Nat}
148  %Equal.sym(Nat, FS.value(one, a), LV.ev(a), LV.ev_value(one, h1, a)) : {Nat.mod(Nat.add(LV.ev(a), LV.ev(L.neg_raw(F.c(), b))), FS.prime(one)) == Nat.mod(Nat.sub(Nat.add(_, FS.prime(one)), Nat.mod(FS.value(one, b), FS.prime(one))), FS.prime(one)) : Nat}
149  %Equal.sym(Nat, FS.value(one, b), LV.ev(b), LV.ev_value(one, h1, b)) : {Nat.mod(Nat.add(LV.ev(a), LV.ev(L.neg_raw(F.c(), b))), FS.prime(one)) == Nat.mod(Nat.sub(Nat.add(LV.ev(a), FS.prime(one)), Nat.mod(_, FS.prime(one))), FS.prime(one)) : Nat}
150  %Equal.sym(Nat, FS.prime(one), 1n+K.pp(one), K.prime_eq(one, h1)) : {Nat.mod(Nat.add(LV.ev(a), LV.ev(L.neg_raw(F.c(), b))), _) == Nat.mod(Nat.sub(Nat.add(LV.ev(a), FS.prime(one)), Nat.mod(LV.ev(b), FS.prime(one))), FS.prime(one)) : Nat}
151  %Equal.sym(Nat, FS.prime(one), 1n+K.pp(one), K.prime_eq(one, h1)) : {Nat.mod(Nat.add(LV.ev(a), LV.ev(L.neg_raw(F.c(), b))), 1n+K.pp(one)) == Nat.mod(Nat.sub(Nat.add(LV.ev(a), _), Nat.mod(LV.ev(b), FS.prime(one))), FS.prime(one)) : Nat}
152  %Equal.sym(Nat, FS.prime(one), 1n+K.pp(one), K.prime_eq(one, h1)) : {Nat.mod(Nat.add(LV.ev(a), LV.ev(L.neg_raw(F.c(), b))), 1n+K.pp(one)) == Nat.mod(Nat.sub(Nat.add(LV.ev(a), 1n+K.pp(one)), Nat.mod(LV.ev(b), _)), FS.prime(one)) : Nat}
153  %Equal.sym(Nat, FS.prime(one), 1n+K.pp(one), K.prime_eq(one, h1)) : {Nat.mod(Nat.add(LV.ev(a), LV.ev(L.neg_raw(F.c(), b))), 1n+K.pp(one)) == Nat.mod(Nat.sub(Nat.add(LV.ev(a), 1n+K.pp(one)), Nat.mod(LV.ev(b), 1n+K.pp(one))), _) : Nat}
154  NG.sub_mod(K.pp(one), LV.ev(a), LV.ev(b), LV.ev(L.neg_raw(F.c(), b)), rlt(one, h1, b, hb), negr_e(one, h1, b, hb))
155
156def sub_r(+one: Nat, +h1: {one == 1n : Nat}, +a: List<&2, Nat>, +b: List<&2, Nat>, +ha: {FS.reduced(one, FS.prime(one), a) == True{} : Bool}, +hb: {FS.reduced(one, FS.prime(one), b) == True{} : Bool}) -> {FS.reduced(one, FS.prime(one), F.sub(a, b)) == True{} : Bool}:
157  %Equal.sym(List<&2, Nat>, F.sub(a, b), F.reduce(L.add(a, L.neg_raw(F.c(), b))), sub_go(one, h1, a, b, ha)) : {FS.reduced(one, FS.prime(one), _) == True{} : Bool}
158  red_r(one, h1, L.add(a, L.neg_raw(F.c(), b)), sub_hx(one, h1, a, b, ha, hb))
159
160def neg_hx(+one: Nat, +h1: {one == 1n : Nat}, +b: List<&2, Nat>, +hb: {FS.reduced(one, FS.prime(one), b) == True{} : Bool}) -> {Nat.is_lt(LV.ev(L.neg_raw(F.c(), b)), Nat.mul(C.shift(256n, one), C.shift(256n, one))) == True{} : Bool}:
161  +t = C.shift(256n, one)
162  lt3(one, h1, LV.ev(L.neg_raw(F.c(), b)), N.le_lt_trans(LV.ev(L.neg_raw(F.c(), b)), t, Nat.add(t, Nat.add(t, t)), negr_le(one, h1, b, hb), I.lt_add_pos(t, Nat.add(t, t), N.lt_le_trans(0n, t, Nat.add(t, t), K.shift_pos(one, h1, 256n), N.le_add_right(t, t)))))
163
164def neg_v(+one: Nat, +h1: {one == 1n : Nat}, +b: List<&2, Nat>, +hb: {FS.reduced(one, FS.prime(one), b) == True{} : Bool}) -> {FS.value(one, F.neg(b)) == FS.mneg(FS.prime(one), FS.value(one, b)) : Nat}:
165  %Equal.sym(List<&2, Nat>, F.neg(b), F.neg_u(b), FR.f_neg(b)) : {FS.value(one, _) == FS.mneg(FS.prime(one), FS.value(one, b)) : Nat}
166  %Equal.sym(Nat, FS.value(one, F.reduce(L.neg_raw(F.c(), b))), Nat.mod(LV.ev(L.neg_raw(F.c(), b)), FS.prime(one)), red_v(one, h1, L.neg_raw(F.c(), b), neg_hx(one, h1, b, hb))) : {_ == Nat.mod(Nat.sub(Nat.add(0n, FS.prime(one)), Nat.mod(FS.value(one, b), FS.prime(one))), FS.prime(one)) : Nat}
167  %Equal.sym(Nat, FS.value(one, b), LV.ev(b), LV.ev_value(one, h1, b)) : {Nat.mod(LV.ev(L.neg_raw(F.c(), b)), FS.prime(one)) == Nat.mod(Nat.sub(Nat.add(0n, FS.prime(one)), Nat.mod(_, FS.prime(one))), FS.prime(one)) : Nat}
168  %Equal.sym(Nat, FS.prime(one), 1n+K.pp(one), K.prime_eq(one, h1)) : {Nat.mod(LV.ev(L.neg_raw(F.c(), b)), _) == Nat.mod(Nat.sub(Nat.add(0n, FS.prime(one)), Nat.mod(LV.ev(b), FS.prime(one))), FS.prime(one)) : Nat}
169  %Equal.sym(Nat, FS.prime(one), 1n+K.pp(one), K.prime_eq(one, h1)) : {Nat.mod(LV.ev(L.neg_raw(F.c(), b)), 1n+K.pp(one)) == Nat.mod(Nat.sub(Nat.add(0n, _), Nat.mod(LV.ev(b), FS.prime(one))), FS.prime(one)) : Nat}
170  %Equal.sym(Nat, FS.prime(one), 1n+K.pp(one), K.prime_eq(one, h1)) : {Nat.mod(LV.ev(L.neg_raw(F.c(), b)), 1n+K.pp(one)) == Nat.mod(Nat.sub(Nat.add(0n, 1n+K.pp(one)), Nat.mod(LV.ev(b), _)), FS.prime(one)) : Nat}
171  %Equal.sym(Nat, FS.prime(one), 1n+K.pp(one), K.prime_eq(one, h1)) : {Nat.mod(LV.ev(L.neg_raw(F.c(), b)), 1n+K.pp(one)) == Nat.mod(Nat.sub(Nat.add(0n, 1n+K.pp(one)), Nat.mod(LV.ev(b), 1n+K.pp(one))), _) : Nat}
172  NG.sub_mod(K.pp(one), 0n, LV.ev(b), LV.ev(L.neg_raw(F.c(), b)), rlt(one, h1, b, hb), negr_e(one, h1, b, hb))
173
174def neg_r(+one: Nat, +h1: {one == 1n : Nat}, +b: List<&2, Nat>, +hb: {FS.reduced(one, FS.prime(one), b) == True{} : Bool}) -> {FS.reduced(one, FS.prime(one), F.neg(b)) == True{} : Bool}:
175  %Equal.sym(List<&2, Nat>, F.neg(b), F.neg_u(b), FR.f_neg(b)) : {FS.reduced(one, FS.prime(one), _) == True{} : Bool}
176  red_r(one, h1, L.neg_raw(F.c(), b), neg_hx(one, h1, b, hb))
177
178# ---- in the limb value ev ----
179
180def mul_e(+one: Nat, +h1: {one == 1n : Nat}, +a: List<&2, Nat>, +b: List<&2, Nat>, +ha: {FS.reduced(one, FS.prime(one), a) == True{} : Bool}, +hb: {FS.reduced(one, FS.prime(one), b) == True{} : Bool}) -> {LV.ev(F.mul(a, b)) == Nat.mod(Nat.mul(LV.ev(a), LV.ev(b)), 1n+K.pp(one)) : Nat}:
181  %Equal.sym(List<&2, Nat>, F.mul(a, b), F.mul_u(a, b), FR.f_mul(a, b)) : {LV.ev(_) == Nat.mod(Nat.mul(LV.ev(a), LV.ev(b)), 1n+K.pp(one)) : Nat}
182  %Equal.sym(Nat, LV.ev(F.reduce(L.conv(a, b))), Nat.mod(LV.ev(L.conv(a, b)), 1n+K.pp(one)), red_e(one, h1, L.conv(a, b), mul_hx(one, h1, a, b, ha, hb))) : {_ == Nat.mod(Nat.mul(LV.ev(a), LV.ev(b)), 1n+K.pp(one)) : Nat}
183  %Equal.sym(Nat, LV.ev(L.conv(a, b)), Nat.mul(LV.ev(a), LV.ev(b)), LV.conv_v(a, b)) : {Nat.mod(_, 1n+K.pp(one)) == Nat.mod(Nat.mul(LV.ev(a), LV.ev(b)), 1n+K.pp(one)) : Nat}
184  {==}
185
186# ---- small constants ----
187
188def small_r(+one: Nat, +h1: {one == 1n : Nat}, +k: Nat, +hk: {Nat.is_lt(k, FS.prime(one)) == True{} : Bool}) -> {FS.reduced(one, FS.prime(one), F.small(k)) == True{} : Bool}:
189  +hk2 = I.lt_subst_r(k, FS.prime(one), 1n+K.pp(one), K.prime_eq(one, h1), hk)
190  +hkt = N.lt_le_trans(k, 1n+K.pp(one), C.shift(256n, one), hk2, I.le_subst_r(1n+K.pp(one), Nat.add(1n+K.pp(one), FS.cp(one)), C.shift(256n, one), K.hm_p(one, h1), N.le_add_right(1n+K.pp(one), FS.cp(one))))
191  +ev = LO.small_v(one, h1, k, hkt)
192  +lt = I.lt_subst_l(k, FS.value(one, F.small(k)), FS.prime(one), Equal.sym(Nat, FS.value(one, F.small(k)), k, Equal.trans(Nat, FS.value(one, F.small(k)), LV.ev(F.small(k)), k, LV.ev_value(one, h1, F.small(k)), ev)), hk)
193  Lg.and_intro(FS.limbs16(one, 16n, F.small(k)), Nat.is_lt(FS.value(one, F.small(k)), FS.prime(one)), LO.small_l(one, h1, k), lt)
194
195def small_val(+one: Nat, +h1: {one == 1n : Nat}, +k: Nat, +hk: {Nat.is_lt(k, FS.prime(one)) == True{} : Bool}) -> {FS.value(one, F.small(k)) == k : Nat}:
196  +hk2 = I.lt_subst_r(k, FS.prime(one), 1n+K.pp(one), K.prime_eq(one, h1), hk)
197  +hkt = N.lt_le_trans(k, 1n+K.pp(one), C.shift(256n, one), hk2, I.le_subst_r(1n+K.pp(one), Nat.add(1n+K.pp(one), FS.cp(one)), C.shift(256n, one), K.hm_p(one, h1), N.le_add_right(1n+K.pp(one), FS.cp(one))))
198  Equal.trans(Nat, FS.value(one, F.small(k)), LV.ev(F.small(k)), k, LV.ev_value(one, h1, F.small(k)), LO.small_v(one, h1, k, hkt))
199
200# m + c = h + h and c <= h: h <= m
201def le_cancel_r(+x: Nat, +y: Nat, +c: Nat) -> {Nat.is_le(Nat.add(x, c), Nat.add(y, c)) == Nat.is_le(x, y) : Bool}:
202  %Equal.sym(Nat, Nat.add(x, c), Nat.add(c, x), NA.add_comm(x, c)) : {Nat.is_le(_, Nat.add(y, c)) == Nat.is_le(x, y) : Bool}
203  %Equal.sym(Nat, Nat.add(y, c), Nat.add(c, y), NA.add_comm(y, c)) : {Nat.is_le(Nat.add(c, x), _) == Nat.is_le(x, y) : Bool}
204  NR.le_add_cancel(c, x, y)
205
206# small k < 2^32 is below p
207def lt_p_half(+h: Nat, +m: Nat, +c: Nat, +e: {Nat.add(m, c) == Nat.add(h, h) : Nat}, +hc: {Nat.is_le(c, h) == True{} : Bool}) -> {Nat.is_le(h, m) == True{} : Bool}:
208  +s1 = N.le_add_left(c, h, h, hc)
209  +s2 = I.le_subst_r(Nat.add(h, c), Nat.add(h, h), Nat.add(m, c), Equal.sym(Nat, Nat.add(m, c), Nat.add(h, h), e), s1)
210  +s3 = Equal.trans(Bool, Nat.is_le(h, m), Nat.is_le(Nat.add(h, c), Nat.add(m, c)), True{}, Equal.sym(Bool, Nat.is_le(Nat.add(h, c), Nat.add(m, c)), Nat.is_le(h, m), le_cancel_r(h, m, c)), s2)
211  s3
212
213def small_lt_p(+one: Nat, +h1: {one == 1n : Nat}, +k: Nat, +hk: {Nat.is_lt(k, C.shift(10n, 1n)) == True{} : Bool}) -> {Nat.is_lt(k, FS.prime(one)) == True{} : Bool}:
214  +hk1 = I.lt_subst_r(k, C.shift(10n, 1n), C.shift(10n, one), Equal.cong(Nat, Nat, z => C.shift(10n, z), 1n, one, Equal.sym(Nat, one, 1n, h1)), hk)
215  +s1 = N.lt_le_trans(k, C.shift(10n, one), C.shift(255n, one), hk1, K.shift_le_k(10n, 255n, one, 245n, {==}))
216  +pp = K.pp(one)
217  # 2^255 <= p: p + c = 2^256 = 2^255 + 2^255 and c <= 2^33 <= 2^255
218  +c = FS.cp(one)
219  +e1 = Equal.trans(Nat, Nat.add(1n+pp, c), C.shift(256n, one), Nat.add(C.shift(255n, one), C.shift(255n, one)), K.hm_p(one, h1), Equal.sym(Nat, Nat.add(C.shift(255n, one), C.shift(255n, one)), C.shift(256n, one), K.shift_twice(255n, one)))
220  +ch = N.le_trans(c, C.shift(33n, one), C.shift(255n, one), K.cp_le(one, h1), K.shift_le_k(33n, 255n, one, 222n, {==}))
221  +s2 = lt_p_half(C.shift(255n, one), 1n+pp, c, e1, ch)
222  I.lt_subst_r(k, 1n+pp, FS.prime(one), Equal.sym(Nat, FS.prime(one), 1n+pp, K.prime_eq(one, h1)), N.lt_le_trans(k, C.shift(255n, one), 1n+pp, s1, s2))