~/jendhub

proofs/crypto/secp256k1/limbs.bend

bend-collections-laws-crypto@1.0.0.0 · 227 lines · 17 definitions

1# GENERATED by tools/generators/rw.py from ../../../tools/generators/secp256k1_hand/limbs.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/lemmas/proofs/nat_algebra.bend as NA
7import bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/arith.bend as NR
8import bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/width.bend as WW
9import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/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
18def 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)
24def 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)
31def 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
35def 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
39def 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
43def 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
54def 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
76def 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
92def 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
110def 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
119def 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
128def 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)
138def 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
159def 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
168def 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
183def 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
196def 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      {==}