1	# GENERATED by tools/generators/rw.py from ../../../tools/generators/secp256k1_hand/limbs.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/lemmas/proofs/nat_algebra.bend as NA
7	import ../../math/natural/arith.bend as NR
8	import ../../math/typed/width.bend as WW
9	import ./semiring.bend as SR
10	
11	# The limb lists of src/crypto/secp256k1/limbs.bend and their values: every
12	# operation is exact on natural numbers (Fiat-Crypto's unsaturated limbs,
13	# Erbsen et al. 2019: the value of the limb list is the number; with Nat
14	# limbs there is no overflow to rule out in the value, and the run-time
15	# bound 2^48 is a separate statement). ev is the value without `one`;
16	# ev_value relates it to spec/crypto/secp256k1/field.bend's value.
17	
18	def ev(xs: List<&2, Nat>) -> Nat:
19	  match xs:
20	    case Nil{}: 0n
21	    case x <> t: Nat.add(x, C.shift(16n, ev(t)))
22	
23	# y at limb position n: y 2^(16 n)
24	def pos(n: Nat, +y: Nat) -> Nat:
25	  match n:
26	    case 0n: y
27	    case 1n+k: C.shift(16n, pos(k, y))
28	
29	# 256 as a shift of one (the checker expands 2^8 in 256 steps, well
30	# within its depth)
31	def b8(+one: Nat, +h1: {one == 1n : Nat}) -> {C.shift(8n, one) == 256n : Nat}:
32	  %Equal.sym(Nat, one, 1n, h1) : {C.shift(8n, _) == 256n : Nat}
33	  {==}
34	
35	def m256(+y: Nat) -> {Nat.mul(y, 256n) == C.shift(8n, y) : Nat}:
36	  %Equal.sym(Nat, C.shift(8n, y), Nat.mul(y, C.shift(8n, 1n)), WW.shift_mul(8n, y)) : {Nat.mul(y, 256n) == _ : Nat}
37	  {==}
38	
39	def mul_one_l(+one: Nat, +h1: {one == 1n : Nat}, +x: Nat) -> {Nat.mul(one, x) == x : Nat}:
40	  %Equal.sym(Nat, one, 1n, h1) : {Nat.mul(_, x) == x : Nat}
41	  SR.one_mul(x)
42	
43	def ev_value(+one: Nat, +h1: {one == 1n : Nat}, xs: List<&2, Nat>) -> {FS.value(one, xs) == ev(xs) : Nat}:
44	  match xs:
45	    case Nil{}:
46	      {==}
47	    case +x <> +t:
48	      %Equal.sym(Nat, Nat.mul(one, x), x, mul_one_l(one, h1, x)) : {Nat.add(_, C.shift(16n, FS.digits(one, t))) == Nat.add(x, C.shift(16n, ev(t))) : Nat}
49	      %Equal.sym(Nat, FS.digits(one, t), ev(t), ev_value(one, h1, t)) : {Nat.add(x, C.shift(16n, _)) == Nat.add(x, C.shift(16n, ev(t))) : Nat}
50	      {==}
51	
52	# ---- sums, scalings, products ----
53	
54	def add_v(xs: List<&2, Nat>, ys: List<&2, Nat>) -> {ev(L.add(xs, ys)) == Nat.add(ev(xs), ev(ys)) : Nat}:
55	  match xs ys:
56	    case Nil{} Nil{}:
57	      {==}
58	    case Nil{} y <> yt:
59	      {==}
60	    case +x <> +xt Nil{}:
61	      Equal.sym(Nat, Nat.add(ev(x <> xt), 0n), ev(x <> xt), NA.add_zero(ev(x <> xt)))
62	    case +x <> +xt +y <> +yt:
63	      %Equal.sym(Nat, ev(L.add(xt, yt)), Nat.add(ev(xt), ev(yt)), add_v(xt, yt)) : {Nat.add(Nat.add(x, y), C.shift(16n, _)) == Nat.add(Nat.add(x, C.shift(16n, ev(xt))), Nat.add(y, C.shift(16n, ev(yt)))) : Nat}
64	      %Equal.sym(Nat, C.shift(16n, Nat.add(ev(xt), ev(yt))), Nat.add(C.shift(16n, ev(xt)), C.shift(16n, ev(yt))), WW.shift_add(16n, ev(xt), ev(yt))) : {Nat.add(Nat.add(x, y), _) == Nat.add(Nat.add(x, C.shift(16n, ev(xt))), Nat.add(y, C.shift(16n, ev(yt)))) : Nat}
65	      %Equal.sym(Nat, Nat.add(Nat.add(x, y), Nat.add(C.shift(16n, ev(xt)), C.shift(16n, ev(yt)))), Nat.add(x, Nat.add(y, Nat.add(C.shift(16n, ev(xt)), C.shift(16n, ev(yt))))), NA.add_assoc(x, y, Nat.add(C.shift(16n, ev(xt)), C.shift(16n, ev(yt))))) : {_ == Nat.add(Nat.add(x, C.shift(16n, ev(xt))), Nat.add(y, C.shift(16n, ev(yt)))) : Nat}
66	      %Equal.sym(Nat, Nat.add(y, Nat.add(C.shift(16n, ev(xt)), C.shift(16n, ev(yt)))), Nat.add(C.shift(16n, ev(xt)), Nat.add(y, C.shift(16n, ev(yt)))), NA.add_swap(y, C.shift(16n, ev(xt)), C.shift(16n, ev(yt)))) : {Nat.add(x, _) == Nat.add(Nat.add(x, C.shift(16n, ev(xt))), Nat.add(y, C.shift(16n, ev(yt)))) : Nat}
67	      %Equal.sym(Nat, Nat.add(y, C.shift(16n, ev(yt))), Nat.add(C.shift(16n, ev(yt)), y), NA.add_comm(y, C.shift(16n, ev(yt)))) : {Nat.add(x, Nat.add(C.shift(16n, ev(xt)), _)) == Nat.add(Nat.add(x, C.shift(16n, ev(xt))), Nat.add(y, C.shift(16n, ev(yt)))) : Nat}
68	      %Equal.sym(Nat, Nat.add(x, Nat.add(C.shift(16n, ev(xt)), Nat.add(C.shift(16n, ev(yt)), y))), Nat.add(C.shift(16n, ev(xt)), Nat.add(x, Nat.add(C.shift(16n, ev(yt)), y))), NA.add_swap(x, C.shift(16n, ev(xt)), Nat.add(C.shift(16n, ev(yt)), y))) : {_ == Nat.add(Nat.add(x, C.shift(16n, ev(xt))), Nat.add(y, C.shift(16n, ev(yt)))) : Nat}
69	      %Equal.sym(Nat, Nat.add(x, Nat.add(C.shift(16n, ev(yt)), y)), Nat.add(C.shift(16n, ev(yt)), Nat.add(x, y)), NA.add_swap(x, C.shift(16n, ev(yt)), y)) : {Nat.add(C.shift(16n, ev(xt)), _) == Nat.add(Nat.add(x, C.shift(16n, ev(xt))), Nat.add(y, C.shift(16n, ev(yt)))) : Nat}
70	      %Equal.sym(Nat, Nat.add(x, C.shift(16n, ev(xt))), Nat.add(C.shift(16n, ev(xt)), x), NA.add_comm(x, C.shift(16n, ev(xt)))) : {Nat.add(C.shift(16n, ev(xt)), Nat.add(C.shift(16n, ev(yt)), Nat.add(x, y))) == Nat.add(_, Nat.add(y, C.shift(16n, ev(yt)))) : Nat}
71	      %Equal.sym(Nat, Nat.add(y, C.shift(16n, ev(yt))), Nat.add(C.shift(16n, ev(yt)), y), NA.add_comm(y, C.shift(16n, ev(yt)))) : {Nat.add(C.shift(16n, ev(xt)), Nat.add(C.shift(16n, ev(yt)), Nat.add(x, y))) == Nat.add(Nat.add(C.shift(16n, ev(xt)), x), _) : Nat}
72	      %Equal.sym(Nat, Nat.add(Nat.add(C.shift(16n, ev(xt)), x), Nat.add(C.shift(16n, ev(yt)), y)), Nat.add(C.shift(16n, ev(xt)), Nat.add(x, Nat.add(C.shift(16n, ev(yt)), y))), NA.add_assoc(C.shift(16n, ev(xt)), x, Nat.add(C.shift(16n, ev(yt)), y))) : {Nat.add(C.shift(16n, ev(xt)), Nat.add(C.shift(16n, ev(yt)), Nat.add(x, y))) == _ : Nat}
73	      %Equal.sym(Nat, Nat.add(x, Nat.add(C.shift(16n, ev(yt)), y)), Nat.add(C.shift(16n, ev(yt)), Nat.add(x, y)), NA.add_swap(x, C.shift(16n, ev(yt)), y)) : {Nat.add(C.shift(16n, ev(xt)), Nat.add(C.shift(16n, ev(yt)), Nat.add(x, y))) == Nat.add(C.shift(16n, ev(xt)), _) : Nat}
74	      {==}
75	
76	def scal_v(+a: Nat, ys: List<&2, Nat>) -> {ev(L.scal(a, ys)) == Nat.mul(ev(ys), a) : Nat}:
77	  match ys:
78	    case Nil{}:
79	      {==}
80	    case +y <> +yt:
81	      %Equal.sym(Nat, ev(L.scal(a, yt)), Nat.mul(ev(yt), a), scal_v(a, yt)) : {Nat.add(Nat.mul(y, a), C.shift(16n, _)) == Nat.mul(Nat.add(y, C.shift(16n, ev(yt))), a) : Nat}
82	      %Equal.sym(Nat, Nat.mul(y, a), Nat.mul(a, y), NA.mul_comm(y, a)) : {Nat.add(_, C.shift(16n, Nat.mul(ev(yt), a))) == Nat.mul(Nat.add(y, C.shift(16n, ev(yt))), a) : Nat}
83	      %Equal.sym(Nat, Nat.mul(ev(yt), a), Nat.mul(a, ev(yt)), NA.mul_comm(ev(yt), a)) : {Nat.add(Nat.mul(a, y), C.shift(16n, _)) == Nat.mul(Nat.add(y, C.shift(16n, ev(yt))), a) : Nat}
84	      %Equal.sym(Nat, Nat.add(Nat.mul(a, y), C.shift(16n, Nat.mul(a, ev(yt)))), Nat.add(C.shift(16n, Nat.mul(a, ev(yt))), Nat.mul(a, y)), NA.add_comm(Nat.mul(a, y), C.shift(16n, Nat.mul(a, ev(yt))))) : {_ == Nat.mul(Nat.add(y, C.shift(16n, ev(yt))), a) : Nat}
85	      %Equal.sym(Nat, Nat.add(y, C.shift(16n, ev(yt))), Nat.add(C.shift(16n, ev(yt)), y), NA.add_comm(y, C.shift(16n, ev(yt)))) : {Nat.add(C.shift(16n, Nat.mul(a, ev(yt))), Nat.mul(a, y)) == Nat.mul(_, a) : Nat}
86	      %Equal.sym(Nat, Nat.mul(Nat.add(C.shift(16n, ev(yt)), y), a), Nat.add(Nat.mul(C.shift(16n, ev(yt)), a), Nat.mul(y, a)), NA.mul_add_right(C.shift(16n, ev(yt)), y, a)) : {Nat.add(C.shift(16n, Nat.mul(a, ev(yt))), Nat.mul(a, y)) == _ : Nat}
87	      %Equal.sym(Nat, Nat.mul(C.shift(16n, ev(yt)), a), C.shift(16n, Nat.mul(ev(yt), a)), WW.shift_mul_l(16n, ev(yt), a)) : {Nat.add(C.shift(16n, Nat.mul(a, ev(yt))), Nat.mul(a, y)) == Nat.add(_, Nat.mul(y, a)) : Nat}
88	      %Equal.sym(Nat, Nat.mul(ev(yt), a), Nat.mul(a, ev(yt)), NA.mul_comm(ev(yt), a)) : {Nat.add(C.shift(16n, Nat.mul(a, ev(yt))), Nat.mul(a, y)) == Nat.add(C.shift(16n, _), Nat.mul(y, a)) : Nat}
89	      %Equal.sym(Nat, Nat.mul(y, a), Nat.mul(a, y), NA.mul_comm(y, a)) : {Nat.add(C.shift(16n, Nat.mul(a, ev(yt))), Nat.mul(a, y)) == Nat.add(C.shift(16n, Nat.mul(a, ev(yt))), _) : Nat}
90	      {==}
91	
92	def conv_v(xs: List<&2, Nat>, +ys: List<&2, Nat>) -> {ev(L.conv(xs, ys)) == Nat.mul(ev(xs), ev(ys)) : Nat}:
93	  match xs:
94	    case Nil{}:
95	      {==}
96	    case +x <> +xt:
97	      %Equal.sym(Nat, ev(L.add(L.scal(x, ys), 0n <> L.conv(xt, ys))), Nat.add(ev(L.scal(x, ys)), ev(0n <> L.conv(xt, ys))), add_v(L.scal(x, ys), 0n <> L.conv(xt, ys))) : {_ == Nat.mul(Nat.add(x, C.shift(16n, ev(xt))), ev(ys)) : Nat}
98	      %Equal.sym(Nat, ev(L.scal(x, ys)), Nat.mul(ev(ys), x), scal_v(x, ys)) : {Nat.add(_, ev(0n <> L.conv(xt, ys))) == Nat.mul(Nat.add(x, C.shift(16n, ev(xt))), ev(ys)) : Nat}
99	      %Equal.sym(Nat, ev(L.conv(xt, ys)), Nat.mul(ev(xt), ev(ys)), conv_v(xt, ys)) : {Nat.add(Nat.mul(ev(ys), x), Nat.add(0n, C.shift(16n, _))) == Nat.mul(Nat.add(x, C.shift(16n, ev(xt))), ev(ys)) : Nat}
100	      %Equal.sym(Nat, Nat.add(0n, C.shift(16n, Nat.mul(ev(xt), ev(ys)))), C.shift(16n, Nat.mul(ev(xt), ev(ys))), SR.zero_add(C.shift(16n, Nat.mul(ev(xt), ev(ys))))) : {Nat.add(Nat.mul(ev(ys), x), _) == Nat.mul(Nat.add(x, C.shift(16n, ev(xt))), ev(ys)) : Nat}
101	      %Equal.sym(Nat, Nat.add(Nat.mul(ev(ys), x), C.shift(16n, Nat.mul(ev(xt), ev(ys)))), Nat.add(C.shift(16n, Nat.mul(ev(xt), ev(ys))), Nat.mul(ev(ys), x)), NA.add_comm(Nat.mul(ev(ys), x), C.shift(16n, Nat.mul(ev(xt), ev(ys))))) : {_ == Nat.mul(Nat.add(x, C.shift(16n, ev(xt))), ev(ys)) : Nat}
102	      %Equal.sym(Nat, Nat.add(x, C.shift(16n, ev(xt))), Nat.add(C.shift(16n, ev(xt)), x), NA.add_comm(x, C.shift(16n, ev(xt)))) : {Nat.add(C.shift(16n, Nat.mul(ev(xt), ev(ys))), Nat.mul(ev(ys), x)) == Nat.mul(_, ev(ys)) : Nat}
103	      %Equal.sym(Nat, Nat.mul(Nat.add(C.shift(16n, ev(xt)), x), ev(ys)), Nat.add(Nat.mul(C.shift(16n, ev(xt)), ev(ys)), Nat.mul(x, ev(ys))), NA.mul_add_right(C.shift(16n, ev(xt)), x, ev(ys))) : {Nat.add(C.shift(16n, Nat.mul(ev(xt), ev(ys))), Nat.mul(ev(ys), x)) == _ : Nat}
104	      %Equal.sym(Nat, Nat.mul(C.shift(16n, ev(xt)), ev(ys)), C.shift(16n, Nat.mul(ev(xt), ev(ys))), WW.shift_mul_l(16n, ev(xt), ev(ys))) : {Nat.add(C.shift(16n, Nat.mul(ev(xt), ev(ys))), Nat.mul(ev(ys), x)) == Nat.add(_, Nat.mul(x, ev(ys))) : Nat}
105	      %Equal.sym(Nat, Nat.mul(x, ev(ys)), Nat.mul(ev(ys), x), NA.mul_comm(x, ev(ys))) : {Nat.add(C.shift(16n, Nat.mul(ev(xt), ev(ys))), Nat.mul(ev(ys), x)) == Nat.add(C.shift(16n, Nat.mul(ev(xt), ev(ys))), _) : Nat}
106	      {==}
107	
108	# ---- positions ----
109	
110	def pos_add(n: Nat, +x: Nat, +y: Nat) -> {pos(n, Nat.add(x, y)) == Nat.add(pos(n, x), pos(n, y)) : Nat}:
111	  match n:
112	    case 0n:
113	      {==}
114	    case 1n+ +k:
115	      %Equal.sym(Nat, pos(k, Nat.add(x, y)), Nat.add(pos(k, x), pos(k, y)), pos_add(k, x, y)) : {C.shift(16n, _) == Nat.add(C.shift(16n, pos(k, x)), C.shift(16n, pos(k, y))) : Nat}
116	      %Equal.sym(Nat, C.shift(16n, Nat.add(pos(k, x), pos(k, y))), Nat.add(C.shift(16n, pos(k, x)), C.shift(16n, pos(k, y))), WW.shift_add(16n, pos(k, x), pos(k, y))) : {_ == Nat.add(C.shift(16n, pos(k, x)), C.shift(16n, pos(k, y))) : Nat}
117	      {==}
118	
119	def pos_zero(n: Nat) -> {pos(n, 0n) == 0n : Nat}:
120	  match n:
121	    case 0n:
122	      {==}
123	    case 1n+ +k:
124	      %Equal.sym(Nat, pos(k, 0n), 0n, pos_zero(k)) : {C.shift(16n, _) == 0n : Nat}
125	      %Equal.sym(Nat, C.shift(16n, 0n), 0n, WW.shift_zero(16n)) : {_ == 0n : Nat}
126	      {==}
127	
128	def pos_mul(n: Nat, +x: Nat, +y: Nat) -> {pos(n, Nat.mul(x, y)) == Nat.mul(pos(n, x), y) : Nat}:
129	  match n:
130	    case 0n:
131	      {==}
132	    case 1n+ +k:
133	      %Equal.sym(Nat, pos(k, Nat.mul(x, y)), Nat.mul(pos(k, x), y), pos_mul(k, x, y)) : {C.shift(16n, _) == Nat.mul(C.shift(16n, pos(k, x)), y) : Nat}
134	      %Equal.sym(Nat, Nat.mul(C.shift(16n, pos(k, x)), y), C.shift(16n, Nat.mul(pos(k, x), y)), WW.shift_mul_l(16n, pos(k, x), y)) : {C.shift(16n, Nat.mul(pos(k, x), y)) == _ : Nat}
135	      {==}
136	
137	# ev(xs) = ev(take n xs) + 2^(16 n) ev(drop n xs)
138	def take_drop_v(n: Nat, xs: List<&2, Nat>) -> {ev(xs) == Nat.add(ev(L.take(n, xs)), pos(n, ev(L.drop(n, xs)))) : Nat}:
139	  match n xs:
140	    case 0n Nil{}:
141	      {==}
142	    case 0n x <> t:
143	      {==}
144	    case 1n+ +k Nil{}:
145	      %Equal.sym(Nat, pos(k, 0n), 0n, pos_zero(k)) : {0n == Nat.add(0n, C.shift(16n, _)) : Nat}
146	      %Equal.sym(Nat, C.shift(16n, 0n), 0n, WW.shift_zero(16n)) : {0n == Nat.add(0n, _) : Nat}
147	      %Equal.sym(Nat, Nat.add(0n, 0n), 0n, {==}) : {0n == _ : Nat}
148	      {==}
149	    case 1n+ +k +x <> +t:
150	      %Equal.sym(Nat, ev(t), Nat.add(ev(L.take(k, t)), pos(k, ev(L.drop(k, t)))), take_drop_v(k, t)) : {Nat.add(x, C.shift(16n, _)) == Nat.add(Nat.add(x, C.shift(16n, ev(L.take(k, t)))), C.shift(16n, pos(k, ev(L.drop(k, t))))) : Nat}
151	      %Equal.sym(Nat, C.shift(16n, Nat.add(ev(L.take(k, t)), pos(k, ev(L.drop(k, t))))), Nat.add(C.shift(16n, ev(L.take(k, t))), C.shift(16n, pos(k, ev(L.drop(k, t))))), WW.shift_add(16n, ev(L.take(k, t)), pos(k, ev(L.drop(k, t))))) : {Nat.add(x, _) == Nat.add(Nat.add(x, C.shift(16n, ev(L.take(k, t)))), C.shift(16n, pos(k, ev(L.drop(k, t))))) : Nat}
152	      %Equal.sym(Nat, Nat.add(x, Nat.add(C.shift(16n, ev(L.take(k, t))), C.shift(16n, pos(k, ev(L.drop(k, t)))))), Nat.add(C.shift(16n, ev(L.take(k, t))), Nat.add(x, C.shift(16n, pos(k, ev(L.drop(k, t)))))), NA.add_swap(x, C.shift(16n, ev(L.take(k, t))), C.shift(16n, pos(k, ev(L.drop(k, t)))))) : {_ == Nat.add(Nat.add(x, C.shift(16n, ev(L.take(k, t)))), C.shift(16n, pos(k, ev(L.drop(k, t))))) : Nat}
153	      %Equal.sym(Nat, Nat.add(x, C.shift(16n, pos(k, ev(L.drop(k, t))))), Nat.add(C.shift(16n, pos(k, ev(L.drop(k, t)))), x), NA.add_comm(x, C.shift(16n, pos(k, ev(L.drop(k, t)))))) : {Nat.add(C.shift(16n, ev(L.take(k, t))), _) == Nat.add(Nat.add(x, C.shift(16n, ev(L.take(k, t)))), C.shift(16n, pos(k, ev(L.drop(k, t))))) : Nat}
154	      %Equal.sym(Nat, Nat.add(x, C.shift(16n, ev(L.take(k, t)))), Nat.add(C.shift(16n, ev(L.take(k, t))), x), NA.add_comm(x, C.shift(16n, ev(L.take(k, t))))) : {Nat.add(C.shift(16n, ev(L.take(k, t))), Nat.add(C.shift(16n, pos(k, ev(L.drop(k, t)))), x)) == Nat.add(_, C.shift(16n, pos(k, ev(L.drop(k, t))))) : Nat}
155	      %Equal.sym(Nat, Nat.add(Nat.add(C.shift(16n, ev(L.take(k, t))), x), C.shift(16n, pos(k, ev(L.drop(k, t))))), Nat.add(C.shift(16n, ev(L.take(k, t))), Nat.add(x, C.shift(16n, pos(k, ev(L.drop(k, t)))))), NA.add_assoc(C.shift(16n, ev(L.take(k, t))), x, C.shift(16n, pos(k, ev(L.drop(k, t)))))) : {Nat.add(C.shift(16n, ev(L.take(k, t))), Nat.add(C.shift(16n, pos(k, ev(L.drop(k, t)))), x)) == _ : Nat}
156	      %Equal.sym(Nat, Nat.add(x, C.shift(16n, pos(k, ev(L.drop(k, t))))), Nat.add(C.shift(16n, pos(k, ev(L.drop(k, t)))), x), NA.add_comm(x, C.shift(16n, pos(k, ev(L.drop(k, t)))))) : {Nat.add(C.shift(16n, ev(L.take(k, t))), Nat.add(C.shift(16n, pos(k, ev(L.drop(k, t)))), x)) == Nat.add(C.shift(16n, ev(L.take(k, t))), _) : Nat}
157	      {==}
158	
159	def hd_tl_v(xs: List<&2, Nat>) -> {ev(xs) == Nat.add(L.hd0(xs), C.shift(16n, ev(L.tl(xs)))) : Nat}:
160	  match xs:
161	    case Nil{}:
162	      {==}
163	    case x <> t:
164	      {==}
165	
166	# ---- 16-bit limbs from bytes ----
167	
168	def lohi(+s: Nat) -> {Nat.add(L.lo16(s), C.shift(16n, L.hi16(s))) == s : Nat}:
169	  %Equal.sym(Nat, s, Nat.add(Nat.mul(Nat.div(s, 256n), 256n), Nat.mod(s, 256n)), NR.dm_eq(255n, s)) : {Nat.add(Nat.add(Nat.mod(s, 256n), Nat.mul(Nat.mod(Nat.div(s, 256n), 256n), 256n)), C.shift(16n, Nat.div(Nat.div(s, 256n), 256n))) == _ : Nat}
170	  %Equal.sym(Nat, Nat.div(s, 256n), Nat.add(Nat.mul(Nat.div(Nat.div(s, 256n), 256n), 256n), Nat.mod(Nat.div(s, 256n), 256n)), NR.dm_eq(255n, Nat.div(s, 256n))) : {Nat.add(Nat.add(Nat.mod(s, 256n), Nat.mul(Nat.mod(Nat.div(s, 256n), 256n), 256n)), C.shift(16n, Nat.div(Nat.div(s, 256n), 256n))) == Nat.add(Nat.mul(_, 256n), Nat.mod(s, 256n)) : Nat}
171	  %Equal.sym(Nat, Nat.mul(Nat.mod(Nat.div(s, 256n), 256n), 256n), C.shift(8n, Nat.mod(Nat.div(s, 256n), 256n)), m256(Nat.mod(Nat.div(s, 256n), 256n))) : {Nat.add(Nat.add(Nat.mod(s, 256n), _), C.shift(16n, Nat.div(Nat.div(s, 256n), 256n))) == Nat.add(Nat.mul(Nat.add(Nat.mul(Nat.div(Nat.div(s, 256n), 256n), 256n), Nat.mod(Nat.div(s, 256n), 256n)), 256n), Nat.mod(s, 256n)) : Nat}
172	  %Equal.sym(Nat, Nat.mul(Nat.add(Nat.mul(Nat.div(Nat.div(s, 256n), 256n), 256n), Nat.mod(Nat.div(s, 256n), 256n)), 256n), C.shift(8n, Nat.add(Nat.mul(Nat.div(Nat.div(s, 256n), 256n), 256n), Nat.mod(Nat.div(s, 256n), 256n))), m256(Nat.add(Nat.mul(Nat.div(Nat.div(s, 256n), 256n), 256n), Nat.mod(Nat.div(s, 256n), 256n)))) : {Nat.add(Nat.add(Nat.mod(s, 256n), C.shift(8n, Nat.mod(Nat.div(s, 256n), 256n))), C.shift(16n, Nat.div(Nat.div(s, 256n), 256n))) == Nat.add(_, Nat.mod(s, 256n)) : Nat}
173	  %Equal.sym(Nat, Nat.mul(Nat.div(Nat.div(s, 256n), 256n), 256n), C.shift(8n, Nat.div(Nat.div(s, 256n), 256n)), m256(Nat.div(Nat.div(s, 256n), 256n))) : {Nat.add(Nat.add(Nat.mod(s, 256n), C.shift(8n, Nat.mod(Nat.div(s, 256n), 256n))), C.shift(16n, Nat.div(Nat.div(s, 256n), 256n))) == Nat.add(C.shift(8n, Nat.add(_, Nat.mod(Nat.div(s, 256n), 256n))), Nat.mod(s, 256n)) : Nat}
174	  %Equal.sym(Nat, Nat.add(Nat.mod(s, 256n), C.shift(8n, Nat.mod(Nat.div(s, 256n), 256n))), Nat.add(C.shift(8n, Nat.mod(Nat.div(s, 256n), 256n)), Nat.mod(s, 256n)), NA.add_comm(Nat.mod(s, 256n), C.shift(8n, Nat.mod(Nat.div(s, 256n), 256n)))) : {Nat.add(_, C.shift(16n, Nat.div(Nat.div(s, 256n), 256n))) == Nat.add(C.shift(8n, Nat.add(C.shift(8n, Nat.div(Nat.div(s, 256n), 256n)), Nat.mod(Nat.div(s, 256n), 256n))), Nat.mod(s, 256n)) : Nat}
175	  %Equal.sym(Nat, Nat.add(Nat.add(C.shift(8n, Nat.mod(Nat.div(s, 256n), 256n)), Nat.mod(s, 256n)), C.shift(16n, Nat.div(Nat.div(s, 256n), 256n))), Nat.add(C.shift(8n, Nat.mod(Nat.div(s, 256n), 256n)), Nat.add(Nat.mod(s, 256n), C.shift(16n, Nat.div(Nat.div(s, 256n), 256n)))), NA.add_assoc(C.shift(8n, Nat.mod(Nat.div(s, 256n), 256n)), Nat.mod(s, 256n), C.shift(16n, Nat.div(Nat.div(s, 256n), 256n)))) : {_ == Nat.add(C.shift(8n, Nat.add(C.shift(8n, Nat.div(Nat.div(s, 256n), 256n)), Nat.mod(Nat.div(s, 256n), 256n))), Nat.mod(s, 256n)) : Nat}
176	  %Equal.sym(Nat, Nat.add(Nat.mod(s, 256n), C.shift(16n, Nat.div(Nat.div(s, 256n), 256n))), Nat.add(C.shift(16n, Nat.div(Nat.div(s, 256n), 256n)), Nat.mod(s, 256n)), NA.add_comm(Nat.mod(s, 256n), C.shift(16n, Nat.div(Nat.div(s, 256n), 256n)))) : {Nat.add(C.shift(8n, Nat.mod(Nat.div(s, 256n), 256n)), _) == Nat.add(C.shift(8n, Nat.add(C.shift(8n, Nat.div(Nat.div(s, 256n), 256n)), Nat.mod(Nat.div(s, 256n), 256n))), Nat.mod(s, 256n)) : Nat}
177	  %Equal.sym(Nat, Nat.add(C.shift(8n, Nat.mod(Nat.div(s, 256n), 256n)), Nat.add(C.shift(16n, Nat.div(Nat.div(s, 256n), 256n)), Nat.mod(s, 256n))), Nat.add(C.shift(16n, Nat.div(Nat.div(s, 256n), 256n)), Nat.add(C.shift(8n, Nat.mod(Nat.div(s, 256n), 256n)), Nat.mod(s, 256n))), NA.add_swap(C.shift(8n, Nat.mod(Nat.div(s, 256n), 256n)), C.shift(16n, Nat.div(Nat.div(s, 256n), 256n)), Nat.mod(s, 256n))) : {_ == Nat.add(C.shift(8n, Nat.add(C.shift(8n, Nat.div(Nat.div(s, 256n), 256n)), Nat.mod(Nat.div(s, 256n), 256n))), Nat.mod(s, 256n)) : Nat}
178	  %Equal.sym(Nat, C.shift(8n, Nat.add(C.shift(8n, Nat.div(Nat.div(s, 256n), 256n)), Nat.mod(Nat.div(s, 256n), 256n))), Nat.add(C.shift(8n, C.shift(8n, Nat.div(Nat.div(s, 256n), 256n))), C.shift(8n, Nat.mod(Nat.div(s, 256n), 256n))), WW.shift_add(8n, C.shift(8n, Nat.div(Nat.div(s, 256n), 256n)), Nat.mod(Nat.div(s, 256n), 256n))) : {Nat.add(C.shift(16n, Nat.div(Nat.div(s, 256n), 256n)), Nat.add(C.shift(8n, Nat.mod(Nat.div(s, 256n), 256n)), Nat.mod(s, 256n))) == Nat.add(_, Nat.mod(s, 256n)) : Nat}
179	  %Equal.sym(Nat, C.shift(8n, C.shift(8n, Nat.div(Nat.div(s, 256n), 256n))), C.shift(16n, Nat.div(Nat.div(s, 256n), 256n)), SR.shift_shift(8n, 8n, Nat.div(Nat.div(s, 256n), 256n))) : {Nat.add(C.shift(16n, Nat.div(Nat.div(s, 256n), 256n)), Nat.add(C.shift(8n, Nat.mod(Nat.div(s, 256n), 256n)), Nat.mod(s, 256n))) == Nat.add(Nat.add(_, C.shift(8n, Nat.mod(Nat.div(s, 256n), 256n))), Nat.mod(s, 256n)) : Nat}
180	  %Equal.sym(Nat, Nat.add(Nat.add(C.shift(16n, Nat.div(Nat.div(s, 256n), 256n)), C.shift(8n, Nat.mod(Nat.div(s, 256n), 256n))), Nat.mod(s, 256n)), Nat.add(C.shift(16n, Nat.div(Nat.div(s, 256n), 256n)), Nat.add(C.shift(8n, Nat.mod(Nat.div(s, 256n), 256n)), Nat.mod(s, 256n))), NA.add_assoc(C.shift(16n, Nat.div(Nat.div(s, 256n), 256n)), C.shift(8n, Nat.mod(Nat.div(s, 256n), 256n)), Nat.mod(s, 256n))) : {Nat.add(C.shift(16n, Nat.div(Nat.div(s, 256n), 256n)), Nat.add(C.shift(8n, Nat.mod(Nat.div(s, 256n), 256n)), Nat.mod(s, 256n))) == _ : Nat}
181	  {==}
182	
183	def horner_v(xs: List<&2, Nat>) -> {L.horner(xs) == ev(xs) : Nat}:
184	  match xs:
185	    case Nil{}:
186	      {==}
187	    case +x <> +t:
188	      %Equal.sym(Nat, L.horner(t), ev(t), horner_v(t)) : {Nat.add(Nat.mul(Nat.mul(_, 256n), 256n), x) == Nat.add(x, C.shift(16n, ev(t))) : Nat}
189	      %Equal.sym(Nat, Nat.mul(ev(t), 256n), C.shift(8n, ev(t)), m256(ev(t))) : {Nat.add(Nat.mul(_, 256n), x) == Nat.add(x, C.shift(16n, ev(t))) : Nat}
190	      %Equal.sym(Nat, Nat.mul(C.shift(8n, ev(t)), 256n), C.shift(8n, C.shift(8n, ev(t))), m256(C.shift(8n, ev(t)))) : {Nat.add(_, x) == Nat.add(x, C.shift(16n, ev(t))) : Nat}
191	      %Equal.sym(Nat, C.shift(8n, C.shift(8n, ev(t))), C.shift(16n, ev(t)), SR.shift_shift(8n, 8n, ev(t))) : {Nat.add(_, x) == Nat.add(x, C.shift(16n, ev(t))) : Nat}
192	      %Equal.sym(Nat, Nat.add(x, C.shift(16n, ev(t))), Nat.add(C.shift(16n, ev(t)), x), NA.add_comm(x, C.shift(16n, ev(t)))) : {Nat.add(C.shift(16n, ev(t)), x) == _ : Nat}
193	      {==}
194	
195	# a carry pass keeps the value: the carry in plus the limbs
196	def carry_v(n: Nat, xs: List<&2, Nat>, +u: Nat) -> {ev(L.carry(n, xs, u)) == Nat.add(u, ev(xs)) : Nat}:
197	  match n xs:
198	    case 0n Nil{}:
199	      %Equal.sym(Nat, C.shift(16n, 0n), 0n, WW.shift_zero(16n)) : {Nat.add(u, _) == Nat.add(u, 0n) : Nat}
200	      %Equal.sym(Nat, Nat.add(u, 0n), u, NA.add_zero(u)) : {_ == Nat.add(u, 0n) : Nat}
201	      %Equal.sym(Nat, Nat.add(u, 0n), u, NA.add_zero(u)) : {u == _ : Nat}
202	      {==}
203	    case 0n +x <> +t:
204	      %Equal.sym(Nat, L.horner(x <> t), ev(x <> t), horner_v(x <> t)) : {Nat.add(Nat.add(u, _), C.shift(16n, 0n)) == Nat.add(u, Nat.add(x, C.shift(16n, ev(t)))) : Nat}
205	      %Equal.sym(Nat, Nat.add(x, C.shift(16n, ev(t))), Nat.add(C.shift(16n, ev(t)), x), NA.add_comm(x, C.shift(16n, ev(t)))) : {Nat.add(Nat.add(u, _), C.shift(16n, 0n)) == Nat.add(u, Nat.add(x, C.shift(16n, ev(t)))) : Nat}
206	      %Equal.sym(Nat, Nat.add(u, Nat.add(C.shift(16n, ev(t)), x)), Nat.add(C.shift(16n, ev(t)), Nat.add(u, x)), NA.add_swap(u, C.shift(16n, ev(t)), x)) : {Nat.add(_, C.shift(16n, 0n)) == Nat.add(u, Nat.add(x, C.shift(16n, ev(t)))) : Nat}
207	      %Equal.sym(Nat, C.shift(16n, 0n), 0n, WW.shift_zero(16n)) : {Nat.add(Nat.add(C.shift(16n, ev(t)), Nat.add(u, x)), _) == Nat.add(u, Nat.add(x, C.shift(16n, ev(t)))) : Nat}
208	      %Equal.sym(Nat, Nat.add(Nat.add(C.shift(16n, ev(t)), Nat.add(u, x)), 0n), Nat.add(C.shift(16n, ev(t)), Nat.add(u, x)), NA.add_zero(Nat.add(C.shift(16n, ev(t)), Nat.add(u, x)))) : {_ == Nat.add(u, Nat.add(x, C.shift(16n, ev(t)))) : Nat}
209	      %Equal.sym(Nat, Nat.add(x, C.shift(16n, ev(t))), Nat.add(C.shift(16n, ev(t)), x), NA.add_comm(x, C.shift(16n, ev(t)))) : {Nat.add(C.shift(16n, ev(t)), Nat.add(u, x)) == Nat.add(u, _) : Nat}
210	      %Equal.sym(Nat, Nat.add(u, Nat.add(C.shift(16n, ev(t)), x)), Nat.add(C.shift(16n, ev(t)), Nat.add(u, x)), NA.add_swap(u, C.shift(16n, ev(t)), x)) : {Nat.add(C.shift(16n, ev(t)), Nat.add(u, x)) == _ : Nat}
211	      {==}
212	    case 1n+ +k Nil{}:
213	      %Equal.sym(Nat, ev(L.carry(k, [], L.hi16(Nat.add(u, 0n)))), Nat.add(L.hi16(Nat.add(u, 0n)), ev([])), carry_v(k, [], L.hi16(Nat.add(u, 0n)))) : {Nat.add(L.lo16(Nat.add(u, 0n)), C.shift(16n, _)) == Nat.add(u, 0n) : Nat}
214	      %Equal.sym(Nat, Nat.add(L.hi16(Nat.add(u, 0n)), 0n), L.hi16(Nat.add(u, 0n)), NA.add_zero(L.hi16(Nat.add(u, 0n)))) : {Nat.add(L.lo16(Nat.add(u, 0n)), C.shift(16n, _)) == Nat.add(u, 0n) : Nat}
215	      %Equal.sym(Nat, Nat.add(L.lo16(Nat.add(u, 0n)), C.shift(16n, L.hi16(Nat.add(u, 0n)))), Nat.add(u, 0n), lohi(Nat.add(u, 0n))) : {_ == Nat.add(u, 0n) : Nat}
216	      {==}
217	    case 1n+ +k +x <> +t:
218	      %Equal.sym(Nat, ev(L.carry(k, t, L.hi16(Nat.add(u, x)))), Nat.add(L.hi16(Nat.add(u, x)), ev(t)), carry_v(k, t, L.hi16(Nat.add(u, x)))) : {Nat.add(L.lo16(Nat.add(u, x)), C.shift(16n, _)) == Nat.add(u, Nat.add(x, C.shift(16n, ev(t)))) : Nat}
219	      %Equal.sym(Nat, C.shift(16n, Nat.add(L.hi16(Nat.add(u, x)), ev(t))), Nat.add(C.shift(16n, L.hi16(Nat.add(u, x))), C.shift(16n, ev(t))), WW.shift_add(16n, L.hi16(Nat.add(u, x)), ev(t))) : {Nat.add(L.lo16(Nat.add(u, x)), _) == Nat.add(u, Nat.add(x, C.shift(16n, ev(t)))) : Nat}
220	      %Equal.sym(Nat, Nat.add(L.lo16(Nat.add(u, x)), Nat.add(C.shift(16n, L.hi16(Nat.add(u, x))), C.shift(16n, ev(t)))), Nat.add(Nat.add(L.lo16(Nat.add(u, x)), C.shift(16n, L.hi16(Nat.add(u, x)))), C.shift(16n, ev(t))), Equal.sym(Nat, Nat.add(Nat.add(L.lo16(Nat.add(u, x)), C.shift(16n, L.hi16(Nat.add(u, x)))), C.shift(16n, ev(t))), Nat.add(L.lo16(Nat.add(u, x)), Nat.add(C.shift(16n, L.hi16(Nat.add(u, x))), C.shift(16n, ev(t)))), NA.add_assoc(L.lo16(Nat.add(u, x)), C.shift(16n, L.hi16(Nat.add(u, x))), C.shift(16n, ev(t))))) : {_ == Nat.add(u, Nat.add(x, C.shift(16n, ev(t)))) : Nat}
221	      %Equal.sym(Nat, Nat.add(L.lo16(Nat.add(u, x)), C.shift(16n, L.hi16(Nat.add(u, x)))), Nat.add(u, x), lohi(Nat.add(u, x))) : {Nat.add(_, C.shift(16n, ev(t))) == Nat.add(u, Nat.add(x, C.shift(16n, ev(t)))) : Nat}
222	      %Equal.sym(Nat, Nat.add(Nat.add(u, x), C.shift(16n, ev(t))), Nat.add(u, Nat.add(x, C.shift(16n, ev(t)))), NA.add_assoc(u, x, C.shift(16n, ev(t)))) : {_ == Nat.add(u, Nat.add(x, C.shift(16n, ev(t)))) : Nat}
223	      %Equal.sym(Nat, Nat.add(x, C.shift(16n, ev(t))), Nat.add(C.shift(16n, ev(t)), x), NA.add_comm(x, C.shift(16n, ev(t)))) : {Nat.add(u, _) == Nat.add(u, Nat.add(x, C.shift(16n, ev(t)))) : Nat}
224	      %Equal.sym(Nat, Nat.add(u, Nat.add(C.shift(16n, ev(t)), x)), Nat.add(C.shift(16n, ev(t)), Nat.add(u, x)), NA.add_swap(u, C.shift(16n, ev(t)), x)) : {_ == Nat.add(u, Nat.add(x, C.shift(16n, ev(t)))) : Nat}
225	      %Equal.sym(Nat, Nat.add(x, C.shift(16n, ev(t))), Nat.add(C.shift(16n, ev(t)), x), NA.add_comm(x, C.shift(16n, ev(t)))) : {Nat.add(C.shift(16n, ev(t)), Nat.add(u, x)) == Nat.add(u, _) : Nat}
226	      %Equal.sym(Nat, Nat.add(u, Nat.add(C.shift(16n, ev(t)), x)), Nat.add(C.shift(16n, ev(t)), Nat.add(u, x)), NA.add_swap(u, C.shift(16n, ev(t)), x)) : {Nat.add(C.shift(16n, ev(t)), Nat.add(u, x)) == _ : Nat}
227	      {==}