1	# GENERATED by tools/generators/rw.py from ../../../tools/generators/secp256k1_hand/consts.src; edit the .src
2	import Base
3	import ../../../spec/lib/common.bend as C
4	import ../../../spec/crypto/secp256k1/field.bend as FS
5	import ../../../src/crypto/secp256k1/limbs.bend as L
6	import ../../lib/nat.bend as N
7	import ../../lib/arith.bend as AR
8	import ../../lib/lemmas/proofs/nat_algebra.bend as NA
9	import ../../math/typed/width.bend as WW
10	import ./semiring.bend as SR
11	import ./limbs.bend as LV
12	import ./ineq.bend as I
13	import ./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	
20	def T(+one: Nat) -> Nat:
21	  C.shift(256n, one)
22	
23	# ---- powers of two ----
24	
25	def 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
29	def 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	
36	def 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)
40	def 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
47	def 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
52	def 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	
58	def 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	
69	def 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)
75	def 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	
79	def 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
83	def 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	
89	def 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	
92	def 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
101	def pp(+one: Nat) -> Nat:
102	  Nat.sub(C.shift(256n, one), Nat.add(FS.cp(one), 1n))
103	
104	def 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
110	def 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	
113	def 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	
123	def 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	
130	def 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	
153	def 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	
157	def cn8() -> List<&2, Nat>:
158	  [48831n, 12233n, 41331n, 16429n, 24516n, 20663n, 8985n, 17745n]
159	
160	def 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	
164	def 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	
171	def 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
178	def 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	
184	def 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	
191	def 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	
197	def 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	
200	def 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	
211	def 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
220	def np(+one: Nat) -> Nat:
221	  Nat.sub(C.shift(256n, one), Nat.add(FS.cn(one), 1n))
222	
223	def 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	
227	def 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	
230	def 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	
240	def 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))