proofs/crypto/secp256k1/consts.bend

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

1# GENERATED by tools/generators/rw.py from ../../../tools/generators/secp256k1_hand/consts.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/proofs/lib/nat.bend as N
7import bend-collections-laws-crypto@1.0.0.0/proofs/lib/arith.bend as AR
8import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as NA
9import bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/width.bend as WW
10import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/semiring.bend as SR
11import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/limbs.bend as LV
12import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/ineq.bend as I
13import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/bounds.bend as B
14
15# The constants of spec/crypto/secp256k1/field.bend, kept symbolic in one:
16# 2^256 - p = 2^32 + 977 < 2^33, 2^256 - n < 2^129, and the bounds the
17# folding reductions need. No 256-bit number is ever formed: every
18# comparison with a closed number is of a small one (977, a 16-bit digit).
19
20def T(+one: Nat) -> Nat:
21  C.shift(256n, one)
22
23# ---- powers of two ----
24
25def shift_twice(+k: Nat, +x: Nat) -> {Nat.add(C.shift(k, x), C.shift(k, x)) == C.shift(1n+k, x) : Nat}:
26  Equal.sym(Nat, Nat.double(C.shift(k, x)), Nat.add(C.shift(k, x), C.shift(k, x)), NA.double_self(C.shift(k, x)))
27
28# 2^k x <= 2^(d + k) x
29def shift_more(d: Nat, +k: Nat, +x: Nat) -> {Nat.is_le(C.shift(k, x), C.shift(Nat.add(d, k), x)) == True{} : Bool}:
30  match d:
31    case 0n:
32      N.le_refl(C.shift(k, x))
33    case 1n+ +e:
34      N.le_trans(C.shift(k, x), C.shift(Nat.add(e, k), x), Nat.double(C.shift(Nat.add(e, k), x)), shift_more(e, k, x), N.double_self_le(C.shift(Nat.add(e, k), x)))
35
36def shift_le_k(+j: Nat, +k: Nat, +x: Nat, +d: Nat, +hd: {Nat.add(d, j) == k : Nat}) -> {Nat.is_le(C.shift(j, x), C.shift(k, x)) == True{} : Bool}:
37  I.le_subst_r(C.shift(j, x), C.shift(Nat.add(d, j), x), C.shift(k, x), Equal.cong(Nat, Nat, z => C.shift(z, x), Nat.add(d, j), k, hd), shift_more(d, j, x))
38
39# 2^a 2^b = 2^(a + b)
40def shift_mul2(+one: Nat, +h1: {one == 1n : Nat}, +a: Nat, +b: Nat) -> {Nat.mul(C.shift(a, one), C.shift(b, one)) == C.shift(Nat.add(a, b), one) : Nat}:
41  %Equal.sym(Nat, Nat.mul(C.shift(a, one), C.shift(b, one)), C.shift(a, Nat.mul(one, C.shift(b, one))), WW.shift_mul_l(a, one, C.shift(b, one))) : {_ == C.shift(Nat.add(a, b), one) : Nat}
42  %Equal.sym(Nat, Nat.mul(one, C.shift(b, one)), C.shift(b, one), LV.mul_one_l(one, h1, C.shift(b, one))) : {C.shift(a, _) == C.shift(Nat.add(a, b), one) : Nat}
43  %Equal.sym(Nat, C.shift(a, C.shift(b, one)), C.shift(Nat.add(a, b), one), SR.shift_shift(a, b, one)) : {_ == C.shift(Nat.add(a, b), one) : Nat}
44  {==}
45
46# 0 < 2^k
47def shift_pos(+one: Nat, +h1: {one == 1n : Nat}, +k: Nat) -> {Nat.is_lt(0n, C.shift(k, one)) == True{} : Bool}:
48  %Equal.sym(Nat, 0n, C.shift(k, 0n), Equal.sym(Nat, C.shift(k, 0n), 0n, WW.shift_zero(k))) : {Nat.is_lt(_, C.shift(k, one)) == True{} : Bool}
49  I.shift_lt(k, 0n, one, B.lt_one(one, h1))
50
51# a small closed number below 2^k
52def small_le(+one: Nat, +h1: {one == 1n : Nat}, +k: Nat, +a: Nat, +h: {Nat.is_le(a, C.shift(k, 1n)) == True{} : Bool}) -> {Nat.is_le(a, C.shift(k, one)) == True{} : Bool}:
53  %Equal.sym(Nat, one, 1n, h1) : {Nat.is_le(a, C.shift(k, _)) == True{} : Bool}
54  h
55
56# ---- 2^256 - p = 2^32 + 977 ----
57
58def cp_eq(+one: Nat, +h1: {one == 1n : Nat}) -> {FS.cp(one) == Nat.add(C.shift(32n, one), 977n) : Nat}:
59  %Equal.sym(Nat, Nat.mul(one, 977n), 977n, LV.mul_one_l(one, h1, 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(C.shift(32n, one), 977n) : Nat}
60  %Equal.sym(Nat, Nat.mul(one, 0n), 0n, NA.mul_zero(one)) : {Nat.add(977n, C.shift(16n, Nat.add(_, C.shift(16n, Nat.add(Nat.mul(one, 1n), C.shift(16n, 0n)))))) == Nat.add(C.shift(32n, one), 977n) : Nat}
61  %Equal.sym(Nat, Nat.mul(one, 1n), one, NA.mul_one(one)) : {Nat.add(977n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(_, C.shift(16n, 0n)))))) == Nat.add(C.shift(32n, one), 977n) : Nat}
62  %Equal.sym(Nat, C.shift(16n, 0n), 0n, WW.shift_zero(16n)) : {Nat.add(977n, C.shift(16n, Nat.add(0n, C.shift(16n, Nat.add(one, _))))) == Nat.add(C.shift(32n, one), 977n) : Nat}
63  %Equal.sym(Nat, Nat.add(one, 0n), one, NA.add_zero(one)) : {Nat.add(977n, C.shift(16n, Nat.add(0n, C.shift(16n, _)))) == Nat.add(C.shift(32n, one), 977n) : Nat}
64  %Equal.sym(Nat, Nat.add(0n, C.shift(16n, one)), C.shift(16n, one), SR.zero_add(C.shift(16n, one))) : {Nat.add(977n, C.shift(16n, _)) == Nat.add(C.shift(32n, one), 977n) : Nat}
65  %Equal.sym(Nat, C.shift(16n, C.shift(16n, one)), C.shift(32n, one), SR.shift_shift(16n, 16n, one)) : {Nat.add(977n, _) == Nat.add(C.shift(32n, one), 977n) : Nat}
66  %Equal.sym(Nat, Nat.add(977n, C.shift(32n, one)), Nat.add(C.shift(32n, one), 977n), NA.add_comm(977n, C.shift(32n, one))) : {_ == Nat.add(C.shift(32n, one), 977n) : Nat}
67  {==}
68
69def cp_le(+one: Nat, +h1: {one == 1n : Nat}) -> {Nat.is_le(FS.cp(one), C.shift(33n, one)) == True{} : Bool}:
70  %Equal.sym(Nat, FS.cp(one), Nat.add(C.shift(32n, one), 977n), cp_eq(one, h1)) : {Nat.is_le(_, C.shift(33n, one)) == True{} : Bool}
71  %Equal.sym(Nat, C.shift(33n, one), Nat.add(C.shift(32n, one), C.shift(32n, one)), Equal.sym(Nat, Nat.add(C.shift(32n, one), C.shift(32n, one)), C.shift(33n, one), shift_twice(32n, one))) : {Nat.is_le(Nat.add(C.shift(32n, one), 977n), _) == True{} : Bool}
72  I.le_add2(C.shift(32n, one), 977n, C.shift(32n, one), C.shift(32n, one), N.le_refl(C.shift(32n, one)), small_le(one, h1, 32n, 977n, {==}))
73
74# 2^j < 2^(1 + j), and 2^j < 2^k for j < k (k = d + 1 + j)
75def shift_lt_succ(+one: Nat, +h1: {one == 1n : Nat}, +j: Nat) -> {Nat.is_lt(C.shift(j, one), C.shift(1n+j, one)) == True{} : Bool}:
76  %Equal.sym(Nat, Nat.double(C.shift(j, one)), Nat.add(C.shift(j, one), C.shift(j, one)), NA.double_self(C.shift(j, one))) : {Nat.is_lt(C.shift(j, one), _) == True{} : Bool}
77  I.lt_add_pos(C.shift(j, one), C.shift(j, one), shift_pos(one, h1, j))
78
79def shift_lt_k(+one: Nat, +h1: {one == 1n : Nat}, +j: Nat, +k: Nat, +d: Nat, +hd: {Nat.add(d, 1n+j) == k : Nat}) -> {Nat.is_lt(C.shift(j, one), C.shift(k, one)) == True{} : Bool}:
80  N.lt_le_trans(C.shift(j, one), C.shift(1n+j, one), C.shift(k, one), shift_lt_succ(one, h1, j), shift_le_k(1n+j, k, one, d, hd))
81
82# the fold bounds for p: 2 c < 2^256 and (1 + c) c + c <= 2^256
83def cp_cc(+one: Nat, +h1: {one == 1n : Nat}) -> {Nat.is_lt(Nat.add(FS.cp(one), FS.cp(one)), C.shift(256n, one)) == True{} : Bool}:
84  +c = FS.cp(one)
85  +s1 = I.le_add2(c, c, C.shift(33n, one), C.shift(33n, one), cp_le(one, h1), cp_le(one, h1))
86  +s2 = I.le_subst_r(Nat.add(c, c), Nat.add(C.shift(33n, one), C.shift(33n, one)), C.shift(34n, one), shift_twice(33n, one), s1)
87  N.le_lt_trans(Nat.add(c, c), C.shift(34n, one), C.shift(256n, one), s2, shift_lt_k(one, h1, 34n, 256n, 221n, {==}))
88
89def cp_succ_le(+one: Nat, +h1: {one == 1n : Nat}) -> {Nat.is_le(1n+FS.cp(one), C.shift(34n, one)) == True{} : Bool}:
90  N.lt_succ_le_succ(FS.cp(one), C.shift(34n, one), N.le_lt_trans(FS.cp(one), C.shift(33n, one), C.shift(34n, one), cp_le(one, h1), shift_lt_succ(one, h1, 33n)))
91
92def cp_hb(+one: Nat, +h1: {one == 1n : Nat}) -> {Nat.is_le(Nat.add(Nat.mul(1n+FS.cp(one), FS.cp(one)), FS.cp(one)), C.shift(256n, one)) == True{} : Bool}:
93  +c = FS.cp(one)
94  +s1 = I.le_mul2(1n+c, c, C.shift(34n, one), C.shift(33n, one), cp_succ_le(one, h1), cp_le(one, h1))
95  +s2 = I.le_subst_r(Nat.mul(1n+c, c), Nat.mul(C.shift(34n, one), C.shift(33n, one)), C.shift(67n, one), shift_mul2(one, h1, 34n, 33n), s1)
96  +s3 = I.le_add2(Nat.mul(1n+c, c), c, C.shift(67n, one), C.shift(67n, one), s2, N.le_trans(c, C.shift(33n, one), C.shift(67n, one), cp_le(one, h1), shift_le_k(33n, 67n, one, 34n, {==})))
97  +s4 = I.le_subst_r(Nat.add(Nat.mul(1n+c, c), c), Nat.add(C.shift(67n, one), C.shift(67n, one)), C.shift(68n, one), shift_twice(67n, one), s3)
98  N.le_trans(Nat.add(Nat.mul(1n+c, c), c), C.shift(68n, one), C.shift(256n, one), s4, shift_le_k(68n, 256n, one, 188n, {==}))
99
100# p = 1 + pp, m + c = 2^256
101def pp(+one: Nat) -> Nat:
102  Nat.sub(C.shift(256n, one), Nat.add(FS.cp(one), 1n))
103
104def cp1_le(+one: Nat, +h1: {one == 1n : Nat}) -> {Nat.is_le(Nat.add(FS.cp(one), 1n), C.shift(256n, one)) == True{} : Bool}:
105  +c = FS.cp(one)
106  +s1 = I.lt_succ_le(c, C.shift(256n, one), N.le_lt_trans(c, Nat.add(c, c), C.shift(256n, one), N.le_add_right(c, c), cp_cc(one, h1)))
107  s1
108
109# (c + 1) + pp = 2^256
110def pp_sum(+one: Nat, +h1: {one == 1n : Nat}) -> {Nat.add(Nat.add(FS.cp(one), 1n), pp(one)) == C.shift(256n, one) : Nat}:
111  N.sub_add(C.shift(256n, one), Nat.add(FS.cp(one), 1n), cp1_le(one, h1))
112
113def hm_p(+one: Nat, +h1: {one == 1n : Nat}) -> {Nat.add(1n+pp(one), FS.cp(one)) == C.shift(256n, one) : Nat}:
114  %Equal.sym(Nat, C.shift(256n, one), Nat.add(Nat.add(FS.cp(one), 1n), pp(one)), Equal.sym(Nat, Nat.add(Nat.add(FS.cp(one), 1n), pp(one)), C.shift(256n, one), pp_sum(one, h1))) : {Nat.add(1n+pp(one), FS.cp(one)) == _ : Nat}
115  %Equal.sym(Nat, 1n+pp(one), Nat.add(pp(one), 1n), SR.succ_add(1n, pp(one))) : {Nat.add(_, FS.cp(one)) == Nat.add(Nat.add(FS.cp(one), 1n), pp(one)) : Nat}
116  %Equal.sym(Nat, Nat.add(Nat.add(pp(one), 1n), FS.cp(one)), Nat.add(pp(one), Nat.add(1n, FS.cp(one))), NA.add_assoc(pp(one), 1n, FS.cp(one))) : {_ == Nat.add(Nat.add(FS.cp(one), 1n), pp(one)) : Nat}
117  %Equal.sym(Nat, Nat.add(1n, FS.cp(one)), Nat.add(FS.cp(one), 1n), NA.add_comm(1n, FS.cp(one))) : {Nat.add(pp(one), _) == Nat.add(Nat.add(FS.cp(one), 1n), pp(one)) : Nat}
118  %Equal.sym(Nat, Nat.add(pp(one), Nat.add(FS.cp(one), 1n)), Nat.add(FS.cp(one), Nat.add(pp(one), 1n)), NA.add_swap(pp(one), FS.cp(one), 1n)) : {_ == Nat.add(Nat.add(FS.cp(one), 1n), pp(one)) : Nat}
119  %Equal.sym(Nat, Nat.add(Nat.add(FS.cp(one), 1n), pp(one)), Nat.add(FS.cp(one), Nat.add(1n, pp(one))), NA.add_assoc(FS.cp(one), 1n, pp(one))) : {Nat.add(FS.cp(one), Nat.add(pp(one), 1n)) == _ : Nat}
120  %Equal.sym(Nat, Nat.add(1n, pp(one)), Nat.add(pp(one), 1n), NA.add_comm(1n, pp(one))) : {Nat.add(FS.cp(one), Nat.add(pp(one), 1n)) == Nat.add(FS.cp(one), _) : Nat}
121  {==}
122
123def prime_eq(+one: Nat, +h1: {one == 1n : Nat}) -> {FS.prime(one) == 1n+pp(one) : Nat}:
124  %Equal.sym(Nat, C.shift(256n, one), Nat.add(1n+pp(one), FS.cp(one)), Equal.sym(Nat, Nat.add(1n+pp(one), FS.cp(one)), C.shift(256n, one), hm_p(one, h1))) : {Nat.sub(_, FS.cp(one)) == 1n+pp(one) : Nat}
125  %Equal.sym(Nat, Nat.add(1n+pp(one), FS.cp(one)), Nat.add(FS.cp(one), 1n+pp(one)), NA.add_comm(1n+pp(one), FS.cp(one))) : {Nat.sub(_, FS.cp(one)) == 1n+pp(one) : Nat}
126  N.add_sub_cancel(FS.cp(one), 1n+pp(one))
127
128# ---- 2^256 - n < 2^129 ----
129
130def digits_split(+one: Nat, n: Nat, ds: List<&2, Nat>) -> {FS.digits(one, ds) == Nat.add(FS.digits(one, L.take(n, ds)), LV.pos(n, FS.digits(one, L.drop(n, ds)))) : Nat}:
131  match n ds:
132    case 0n Nil{}:
133      {==}
134    case 0n d <> t:
135      {==}
136    case 1n+ +k Nil{}:
137      %Equal.sym(Nat, LV.pos(k, 0n), 0n, LV.pos_zero(k)) : {0n == Nat.add(0n, C.shift(16n, _)) : Nat}
138      %Equal.sym(Nat, C.shift(16n, 0n), 0n, WW.shift_zero(16n)) : {0n == Nat.add(0n, _) : Nat}
139      %Equal.sym(Nat, Nat.add(0n, 0n), 0n, {==}) : {0n == _ : Nat}
140      {==}
141    case 1n+ +k +d <> +t:
142      %Equal.sym(Nat, FS.digits(one, t), Nat.add(FS.digits(one, L.take(k, t)), LV.pos(k, FS.digits(one, L.drop(k, t)))), digits_split(one, k, t)) : {Nat.add(Nat.mul(one, d), C.shift(16n, _)) == Nat.add(Nat.add(Nat.mul(one, d), C.shift(16n, FS.digits(one, L.take(k, t)))), C.shift(16n, LV.pos(k, FS.digits(one, L.drop(k, t))))) : Nat}
143      %Equal.sym(Nat, Nat.mul(one, d), Nat.mul(d, one), NA.mul_comm(one, d)) : {Nat.add(_, C.shift(16n, Nat.add(FS.digits(one, L.take(k, t)), LV.pos(k, FS.digits(one, L.drop(k, t)))))) == Nat.add(Nat.add(Nat.mul(one, d), C.shift(16n, FS.digits(one, L.take(k, t)))), C.shift(16n, LV.pos(k, FS.digits(one, L.drop(k, t))))) : Nat}
144      %Equal.sym(Nat, C.shift(16n, Nat.add(FS.digits(one, L.take(k, t)), LV.pos(k, FS.digits(one, L.drop(k, t))))), Nat.add(C.shift(16n, FS.digits(one, L.take(k, t))), C.shift(16n, LV.pos(k, FS.digits(one, L.drop(k, t))))), WW.shift_add(16n, FS.digits(one, L.take(k, t)), LV.pos(k, FS.digits(one, L.drop(k, t))))) : {Nat.add(Nat.mul(d, one), _) == Nat.add(Nat.add(Nat.mul(one, d), C.shift(16n, FS.digits(one, L.take(k, t)))), C.shift(16n, LV.pos(k, FS.digits(one, L.drop(k, t))))) : Nat}
145      %Equal.sym(Nat, Nat.add(Nat.mul(d, one), Nat.add(C.shift(16n, FS.digits(one, L.take(k, t))), C.shift(16n, LV.pos(k, FS.digits(one, L.drop(k, t)))))), Nat.add(C.shift(16n, FS.digits(one, L.take(k, t))), Nat.add(Nat.mul(d, one), C.shift(16n, LV.pos(k, FS.digits(one, L.drop(k, t)))))), NA.add_swap(Nat.mul(d, one), C.shift(16n, FS.digits(one, L.take(k, t))), C.shift(16n, LV.pos(k, FS.digits(one, L.drop(k, t)))))) : {_ == Nat.add(Nat.add(Nat.mul(one, d), C.shift(16n, FS.digits(one, L.take(k, t)))), C.shift(16n, LV.pos(k, FS.digits(one, L.drop(k, t))))) : Nat}
146      %Equal.sym(Nat, Nat.add(Nat.mul(d, one), C.shift(16n, LV.pos(k, FS.digits(one, L.drop(k, t))))), Nat.add(C.shift(16n, LV.pos(k, FS.digits(one, L.drop(k, t)))), Nat.mul(d, one)), NA.add_comm(Nat.mul(d, one), C.shift(16n, LV.pos(k, FS.digits(one, L.drop(k, t)))))) : {Nat.add(C.shift(16n, FS.digits(one, L.take(k, t))), _) == Nat.add(Nat.add(Nat.mul(one, d), C.shift(16n, FS.digits(one, L.take(k, t)))), C.shift(16n, LV.pos(k, FS.digits(one, L.drop(k, t))))) : Nat}
147      %Equal.sym(Nat, Nat.mul(one, d), Nat.mul(d, one), NA.mul_comm(one, d)) : {Nat.add(C.shift(16n, FS.digits(one, L.take(k, t))), Nat.add(C.shift(16n, LV.pos(k, FS.digits(one, L.drop(k, t)))), Nat.mul(d, one))) == Nat.add(Nat.add(_, C.shift(16n, FS.digits(one, L.take(k, t)))), C.shift(16n, LV.pos(k, FS.digits(one, L.drop(k, t))))) : Nat}
148      %Equal.sym(Nat, Nat.add(Nat.mul(d, one), C.shift(16n, FS.digits(one, L.take(k, t)))), Nat.add(C.shift(16n, FS.digits(one, L.take(k, t))), Nat.mul(d, one)), NA.add_comm(Nat.mul(d, one), C.shift(16n, FS.digits(one, L.take(k, t))))) : {Nat.add(C.shift(16n, FS.digits(one, L.take(k, t))), Nat.add(C.shift(16n, LV.pos(k, FS.digits(one, L.drop(k, t)))), Nat.mul(d, one))) == Nat.add(_, C.shift(16n, LV.pos(k, FS.digits(one, L.drop(k, t))))) : Nat}
149      %Equal.sym(Nat, Nat.add(Nat.add(C.shift(16n, FS.digits(one, L.take(k, t))), Nat.mul(d, one)), C.shift(16n, LV.pos(k, FS.digits(one, L.drop(k, t))))), Nat.add(C.shift(16n, FS.digits(one, L.take(k, t))), Nat.add(Nat.mul(d, one), C.shift(16n, LV.pos(k, FS.digits(one, L.drop(k, t)))))), NA.add_assoc(C.shift(16n, FS.digits(one, L.take(k, t))), Nat.mul(d, one), C.shift(16n, LV.pos(k, FS.digits(one, L.drop(k, t)))))) : {Nat.add(C.shift(16n, FS.digits(one, L.take(k, t))), Nat.add(C.shift(16n, LV.pos(k, FS.digits(one, L.drop(k, t)))), Nat.mul(d, one))) == _ : Nat}
150      %Equal.sym(Nat, Nat.add(Nat.mul(d, one), C.shift(16n, LV.pos(k, FS.digits(one, L.drop(k, t))))), Nat.add(C.shift(16n, LV.pos(k, FS.digits(one, L.drop(k, t)))), Nat.mul(d, one)), NA.add_comm(Nat.mul(d, one), C.shift(16n, LV.pos(k, FS.digits(one, L.drop(k, t)))))) : {Nat.add(C.shift(16n, FS.digits(one, L.take(k, t))), Nat.add(C.shift(16n, LV.pos(k, FS.digits(one, L.drop(k, t)))), Nat.mul(d, one))) == Nat.add(C.shift(16n, FS.digits(one, L.take(k, t))), _) : Nat}
151      {==}
152
153def digits_lt(+one: Nat, +h1: {one == 1n : Nat}, +k: Nat, +ys: List<&2, Nat>, +h: {FS.limbs16(one, k, ys) == True{} : Bool}) -> {Nat.is_lt(FS.digits(one, ys), LV.pos(k, one)) == True{} : Bool}:
154  %Equal.sym(Nat, FS.digits(one, ys), LV.ev(ys), LV.ev_value(one, h1, ys)) : {Nat.is_lt(_, LV.pos(k, one)) == True{} : Bool}
155  B.limbs_lt(one, h1, k, ys, h)
156
157def cn8() -> List<&2, Nat>:
158  [48831n, 12233n, 41331n, 16429n, 24516n, 20663n, 8985n, 17745n]
159
160def cn8_limbs(+one: Nat, +h1: {one == 1n : Nat}) -> {FS.limbs16(one, 8n, cn8()) == True{} : Bool}:
161  %Equal.sym(Nat, one, 1n, h1) : {FS.limbs16(_, 8n, cn8()) == True{} : Bool}
162  {==}
163
164def cn_split(+one: Nat, +h1: {one == 1n : Nat}) -> {FS.cn(one) == Nat.add(FS.digits(one, cn8()), LV.pos(8n, one)) : Nat}:
165  %Equal.sym(Nat, FS.cn(one), Nat.add(FS.digits(one, cn8()), LV.pos(8n, Nat.add(Nat.mul(one, 1n), C.shift(16n, 0n)))), digits_split(one, 8n, [48831n, 12233n, 41331n, 16429n, 24516n, 20663n, 8985n, 17745n, 1n])) : {_ == Nat.add(FS.digits(one, cn8()), LV.pos(8n, one)) : Nat}
166  %Equal.sym(Nat, Nat.mul(one, 1n), one, NA.mul_one(one)) : {Nat.add(FS.digits(one, cn8()), LV.pos(8n, Nat.add(_, C.shift(16n, 0n)))) == Nat.add(FS.digits(one, cn8()), LV.pos(8n, one)) : Nat}
167  %Equal.sym(Nat, C.shift(16n, 0n), 0n, WW.shift_zero(16n)) : {Nat.add(FS.digits(one, cn8()), LV.pos(8n, Nat.add(one, _))) == Nat.add(FS.digits(one, cn8()), LV.pos(8n, one)) : Nat}
168  %Equal.sym(Nat, Nat.add(one, 0n), one, NA.add_zero(one)) : {Nat.add(FS.digits(one, cn8()), LV.pos(8n, _)) == Nat.add(FS.digits(one, cn8()), LV.pos(8n, one)) : Nat}
169  {==}
170
171def cn_lt(+one: Nat, +h1: {one == 1n : Nat}) -> {Nat.is_lt(FS.cn(one), C.shift(129n, one)) == True{} : Bool}:
172  %Equal.sym(Nat, FS.cn(one), Nat.add(FS.digits(one, cn8()), LV.pos(8n, one)), cn_split(one, h1)) : {Nat.is_lt(_, C.shift(129n, one)) == True{} : Bool}
173  %Equal.sym(Nat, LV.pos(8n, one), C.shift(128n, one), B.pos_shift(8n, one)) : {Nat.is_lt(Nat.add(FS.digits(one, cn8()), _), C.shift(129n, one)) == True{} : Bool}
174  %Equal.sym(Nat, C.shift(129n, one), Nat.add(C.shift(128n, one), C.shift(128n, one)), Equal.sym(Nat, Nat.add(C.shift(128n, one), C.shift(128n, one)), C.shift(129n, one), shift_twice(128n, one))) : {Nat.is_lt(Nat.add(FS.digits(one, cn8()), C.shift(128n, one)), _) == True{} : Bool}
175  I.lt_le_add(FS.digits(one, cn8()), C.shift(128n, one), C.shift(128n, one), C.shift(128n, one), I.lt_subst_r(FS.digits(one, cn8()), LV.pos(8n, one), C.shift(128n, one), B.pos_shift(8n, one), digits_lt(one, h1, 8n, cn8(), cn8_limbs(one, h1))), N.le_refl(C.shift(128n, one)))
176
177# the fold bounds for n: 2 c < 2^256, (1 + c) c <= 4 2^256, 5 c + c <= 2^256
178def cn_cc(+one: Nat, +h1: {one == 1n : Nat}) -> {Nat.is_lt(Nat.add(FS.cn(one), FS.cn(one)), C.shift(256n, one)) == True{} : Bool}:
179  +c = FS.cn(one)
180  +s1 = I.lt_le_add(c, c, C.shift(129n, one), C.shift(129n, one), cn_lt(one, h1), N.lt_le(c, C.shift(129n, one), cn_lt(one, h1)))
181  +s2 = I.lt_subst_r(Nat.add(c, c), Nat.add(C.shift(129n, one), C.shift(129n, one)), C.shift(130n, one), shift_twice(129n, one), s1)
182  N.lt_trans(Nat.add(c, c), C.shift(130n, one), C.shift(256n, one), s2, shift_lt_k(one, h1, 130n, 256n, 125n, {==}))
183
184def four_t(+one: Nat) -> {C.shift(258n, one) == Nat.mul(4n, C.shift(256n, one)) : Nat}:
185  %Equal.sym(Nat, Nat.double(C.shift(256n, one)), Nat.add(C.shift(256n, one), C.shift(256n, one)), NA.double_self(C.shift(256n, one))) : {Nat.double(_) == Nat.add(C.shift(256n, one), Nat.add(C.shift(256n, one), Nat.add(C.shift(256n, one), Nat.add(C.shift(256n, one), 0n)))) : Nat}
186  %Equal.sym(Nat, Nat.double(Nat.add(C.shift(256n, one), C.shift(256n, one))), Nat.add(Nat.add(C.shift(256n, one), C.shift(256n, one)), Nat.add(C.shift(256n, one), C.shift(256n, one))), NA.double_self(Nat.add(C.shift(256n, one), C.shift(256n, one)))) : {_ == Nat.add(C.shift(256n, one), Nat.add(C.shift(256n, one), Nat.add(C.shift(256n, one), Nat.add(C.shift(256n, one), 0n)))) : Nat}
187  %Equal.sym(Nat, Nat.add(Nat.add(C.shift(256n, one), C.shift(256n, one)), Nat.add(C.shift(256n, one), C.shift(256n, one))), Nat.add(C.shift(256n, one), Nat.add(C.shift(256n, one), Nat.add(C.shift(256n, one), C.shift(256n, one)))), NA.add_assoc(C.shift(256n, one), C.shift(256n, one), Nat.add(C.shift(256n, one), C.shift(256n, one)))) : {_ == Nat.add(C.shift(256n, one), Nat.add(C.shift(256n, one), Nat.add(C.shift(256n, one), Nat.add(C.shift(256n, one), 0n)))) : Nat}
188  %Equal.sym(Nat, Nat.add(C.shift(256n, one), 0n), C.shift(256n, one), NA.add_zero(C.shift(256n, one))) : {Nat.add(C.shift(256n, one), Nat.add(C.shift(256n, one), Nat.add(C.shift(256n, one), C.shift(256n, one)))) == Nat.add(C.shift(256n, one), Nat.add(C.shift(256n, one), Nat.add(C.shift(256n, one), _))) : Nat}
189  {==}
190
191def cn_hb1(+one: Nat, +h1: {one == 1n : Nat}) -> {Nat.is_le(Nat.mul(1n+FS.cn(one), FS.cn(one)), Nat.mul(4n, C.shift(256n, one))) == True{} : Bool}:
192  +c = FS.cn(one)
193  +s1 = I.le_mul2(1n+c, c, C.shift(129n, one), C.shift(129n, one), N.lt_succ_le_succ(c, C.shift(129n, one), cn_lt(one, h1)), N.lt_le(c, C.shift(129n, one), cn_lt(one, h1)))
194  +s2 = I.le_subst_r(Nat.mul(1n+c, c), Nat.mul(C.shift(129n, one), C.shift(129n, one)), C.shift(258n, one), shift_mul2(one, h1, 129n, 129n), s1)
195  I.le_subst_r(Nat.mul(1n+c, c), C.shift(258n, one), Nat.mul(4n, C.shift(256n, one)), four_t(one), s2)
196
197def six(+x: Nat) -> {Nat.add(Nat.mul(5n, x), x) == Nat.mul(6n, x) : Nat}:
198  NA.add_comm(Nat.mul(5n, x), x)
199
200def eight(+x: Nat) -> {Nat.mul(8n, x) == C.shift(3n, x) : Nat}:
201  %Equal.sym(Nat, Nat.add(x, 0n), x, NA.add_zero(x)) : {Nat.add(x, Nat.add(x, Nat.add(x, Nat.add(x, Nat.add(x, Nat.add(x, Nat.add(x, _))))))) == Nat.double(Nat.double(Nat.double(x))) : Nat}
202  %Equal.sym(Nat, Nat.double(x), Nat.add(x, x), NA.double_self(x)) : {Nat.add(x, Nat.add(x, Nat.add(x, Nat.add(x, Nat.add(x, Nat.add(x, Nat.add(x, x))))))) == Nat.double(Nat.double(_)) : Nat}
203  %Equal.sym(Nat, Nat.double(Nat.add(x, x)), Nat.add(Nat.add(x, x), Nat.add(x, x)), NA.double_self(Nat.add(x, x))) : {Nat.add(x, Nat.add(x, Nat.add(x, Nat.add(x, Nat.add(x, Nat.add(x, Nat.add(x, x))))))) == Nat.double(_) : Nat}
204  %Equal.sym(Nat, Nat.add(Nat.add(x, x), Nat.add(x, x)), Nat.add(x, Nat.add(x, Nat.add(x, x))), NA.add_assoc(x, x, Nat.add(x, x))) : {Nat.add(x, Nat.add(x, Nat.add(x, Nat.add(x, Nat.add(x, Nat.add(x, Nat.add(x, x))))))) == Nat.double(_) : Nat}
205  %Equal.sym(Nat, Nat.double(Nat.add(x, Nat.add(x, Nat.add(x, x)))), Nat.add(Nat.add(x, Nat.add(x, Nat.add(x, x))), Nat.add(x, Nat.add(x, Nat.add(x, x)))), NA.double_self(Nat.add(x, Nat.add(x, Nat.add(x, x))))) : {Nat.add(x, Nat.add(x, Nat.add(x, Nat.add(x, Nat.add(x, Nat.add(x, Nat.add(x, x))))))) == _ : Nat}
206  %Equal.sym(Nat, Nat.add(Nat.add(x, Nat.add(x, Nat.add(x, x))), Nat.add(x, Nat.add(x, Nat.add(x, x)))), Nat.add(x, Nat.add(Nat.add(x, Nat.add(x, x)), Nat.add(x, Nat.add(x, Nat.add(x, x))))), NA.add_assoc(x, Nat.add(x, Nat.add(x, x)), Nat.add(x, Nat.add(x, Nat.add(x, x))))) : {Nat.add(x, Nat.add(x, Nat.add(x, Nat.add(x, Nat.add(x, Nat.add(x, Nat.add(x, x))))))) == _ : Nat}
207  %Equal.sym(Nat, Nat.add(Nat.add(x, Nat.add(x, x)), Nat.add(x, Nat.add(x, Nat.add(x, x)))), Nat.add(x, Nat.add(Nat.add(x, x), Nat.add(x, Nat.add(x, Nat.add(x, x))))), NA.add_assoc(x, Nat.add(x, x), Nat.add(x, Nat.add(x, Nat.add(x, x))))) : {Nat.add(x, Nat.add(x, Nat.add(x, Nat.add(x, Nat.add(x, Nat.add(x, Nat.add(x, x))))))) == Nat.add(x, _) : Nat}
208  %Equal.sym(Nat, Nat.add(Nat.add(x, x), Nat.add(x, Nat.add(x, Nat.add(x, x)))), Nat.add(x, Nat.add(x, Nat.add(x, Nat.add(x, Nat.add(x, x))))), NA.add_assoc(x, x, Nat.add(x, Nat.add(x, Nat.add(x, x))))) : {Nat.add(x, Nat.add(x, Nat.add(x, Nat.add(x, Nat.add(x, Nat.add(x, Nat.add(x, x))))))) == Nat.add(x, Nat.add(x, _)) : Nat}
209  {==}
210
211def cn_hb2(+one: Nat, +h1: {one == 1n : Nat}) -> {Nat.is_le(Nat.add(Nat.mul(5n, FS.cn(one)), FS.cn(one)), C.shift(256n, one)) == True{} : Bool}:
212  +c = FS.cn(one)
213  +l = N.lt_le(c, C.shift(129n, one), cn_lt(one, h1))
214  +s1 = I.le_add2(Nat.mul(5n, c), c, Nat.mul(5n, C.shift(129n, one)), C.shift(129n, one), I.le_mul_r(5n, c, C.shift(129n, one), l), l)
215  +s2 = I.le_subst_r(Nat.add(Nat.mul(5n, c), c), Nat.add(Nat.mul(5n, C.shift(129n, one)), C.shift(129n, one)), Nat.mul(6n, C.shift(129n, one)), six(C.shift(129n, one)), s1)
216  +s3 = N.le_trans(Nat.mul(6n, C.shift(129n, one)), Nat.mul(8n, C.shift(129n, one)), C.shift(132n, one), AR.mul_le(6n, 8n, C.shift(129n, one), {==}), I.le_subst_r(Nat.mul(8n, C.shift(129n, one)), C.shift(132n, one), C.shift(132n, one), {==}, N.eq_le(Nat.mul(8n, C.shift(129n, one)), C.shift(132n, one), eight(C.shift(129n, one)))))
217  N.le_trans(Nat.add(Nat.mul(5n, c), c), Nat.mul(6n, C.shift(129n, one)), C.shift(256n, one), s2, N.le_trans(Nat.mul(6n, C.shift(129n, one)), C.shift(132n, one), C.shift(256n, one), s3, shift_le_k(132n, 256n, one, 124n, {==})))
218
219# n = 1 + np, n + c = 2^256
220def np(+one: Nat) -> Nat:
221  Nat.sub(C.shift(256n, one), Nat.add(FS.cn(one), 1n))
222
223def cn1_le(+one: Nat, +h1: {one == 1n : Nat}) -> {Nat.is_le(Nat.add(FS.cn(one), 1n), C.shift(256n, one)) == True{} : Bool}:
224  +c = FS.cn(one)
225  I.lt_succ_le(c, C.shift(256n, one), N.le_lt_trans(c, Nat.add(c, c), C.shift(256n, one), N.le_add_right(c, c), cn_cc(one, h1)))
226
227def np_sum(+one: Nat, +h1: {one == 1n : Nat}) -> {Nat.add(Nat.add(FS.cn(one), 1n), np(one)) == C.shift(256n, one) : Nat}:
228  N.sub_add(C.shift(256n, one), Nat.add(FS.cn(one), 1n), cn1_le(one, h1))
229
230def hm_n(+one: Nat, +h1: {one == 1n : Nat}) -> {Nat.add(1n+np(one), FS.cn(one)) == C.shift(256n, one) : Nat}:
231  %Equal.sym(Nat, C.shift(256n, one), Nat.add(Nat.add(FS.cn(one), 1n), np(one)), Equal.sym(Nat, Nat.add(Nat.add(FS.cn(one), 1n), np(one)), C.shift(256n, one), np_sum(one, h1))) : {Nat.add(1n+np(one), FS.cn(one)) == _ : Nat}
232  %Equal.sym(Nat, 1n+np(one), Nat.add(np(one), 1n), SR.succ_add(1n, np(one))) : {Nat.add(_, FS.cn(one)) == Nat.add(Nat.add(FS.cn(one), 1n), np(one)) : Nat}
233  %Equal.sym(Nat, Nat.add(Nat.add(np(one), 1n), FS.cn(one)), Nat.add(np(one), Nat.add(1n, FS.cn(one))), NA.add_assoc(np(one), 1n, FS.cn(one))) : {_ == Nat.add(Nat.add(FS.cn(one), 1n), np(one)) : Nat}
234  %Equal.sym(Nat, Nat.add(1n, FS.cn(one)), Nat.add(FS.cn(one), 1n), NA.add_comm(1n, FS.cn(one))) : {Nat.add(np(one), _) == Nat.add(Nat.add(FS.cn(one), 1n), np(one)) : Nat}
235  %Equal.sym(Nat, Nat.add(np(one), Nat.add(FS.cn(one), 1n)), Nat.add(FS.cn(one), Nat.add(np(one), 1n)), NA.add_swap(np(one), FS.cn(one), 1n)) : {_ == Nat.add(Nat.add(FS.cn(one), 1n), np(one)) : Nat}
236  %Equal.sym(Nat, Nat.add(Nat.add(FS.cn(one), 1n), np(one)), Nat.add(FS.cn(one), Nat.add(1n, np(one))), NA.add_assoc(FS.cn(one), 1n, np(one))) : {Nat.add(FS.cn(one), Nat.add(np(one), 1n)) == _ : Nat}
237  %Equal.sym(Nat, Nat.add(1n, np(one)), Nat.add(np(one), 1n), NA.add_comm(1n, np(one))) : {Nat.add(FS.cn(one), Nat.add(np(one), 1n)) == Nat.add(FS.cn(one), _) : Nat}
238  {==}
239
240def order_eq(+one: Nat, +h1: {one == 1n : Nat}) -> {FS.order(one) == 1n+np(one) : Nat}:
241  %Equal.sym(Nat, C.shift(256n, one), Nat.add(1n+np(one), FS.cn(one)), Equal.sym(Nat, Nat.add(1n+np(one), FS.cn(one)), C.shift(256n, one), hm_n(one, h1))) : {Nat.sub(_, FS.cn(one)) == 1n+np(one) : Nat}
242  %Equal.sym(Nat, Nat.add(1n+np(one), FS.cn(one)), Nat.add(FS.cn(one), 1n+np(one)), NA.add_comm(1n+np(one), FS.cn(one))) : {Nat.sub(_, FS.cn(one)) == 1n+np(one) : Nat}
243  N.add_sub_cancel(FS.cn(one), 1n+np(one))