proofs/crypto/secp256k1/listops.bend

bend-collections-laws-crypto@1.0.0.0 · 216 lines · 26 definitions

1# GENERATED by tools/generators/rw.py from ../../../tools/generators/secp256k1_hand/listops.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/logic.bend as Lg
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/natural/arith.bend as NR
10import bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/width.bend as WW
11import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/semiring.bend as SR
12import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/limbs.bend as LV
13import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/ineq.bend as I
14import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/bounds.bend as B
15import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/reduce.bend as R
16
17# Zero tests, equality, parity, comparison with m and small constants of
18# src/crypto/secp256k1/limbs.bend, against the values of the limbs.
19
20# ---- Bool facts ----
21
22def is_eq_add0(a: Nat, +b: Nat) -> {Nat.is_eq(Nat.add(a, b), 0n) == Bool.and(Nat.is_eq(a, 0n), Nat.is_eq(b, 0n)) : Bool}:
23  match a:
24    case 0n:
25      {==}
26    case 1n+k:
27      {==}
28
29def and_true(+b: Bool) -> {Bool.and(True{}, b) == b : Bool}:
30  {==}
31
32def and_assoc(a: Bool, +b: Bool, +c: Bool) -> {Bool.and(Bool.and(a, b), c) == Bool.and(a, Bool.and(b, c)) : Bool}:
33  match a:
34    case True{}:
35      {==}
36    case False{}:
37      {==}
38
39# 2^16 y == 0 exactly when y == 0
40def sh_eq0(+y: Nat) -> {Nat.is_eq(C.shift(16n, y), 0n) == Nat.is_eq(y, 0n) : Bool}:
41  WW.shift_eq0(16n, y)
42
43# ---- is_zero ----
44
45def and_true_r(b: Bool) -> {Bool.and(b, True{}) == b : Bool}:
46  match b:
47    case True{}:
48      {==}
49    case False{}:
50      {==}
51
52
53def nonzero_v(xs: List<&2, Nat>, +acc: Nat) -> {Nat.is_eq(L.nonzero(xs, acc), 0n) == Bool.and(Nat.is_eq(acc, 0n), Nat.is_eq(LV.ev(xs), 0n)) : Bool}:
54  match xs:
55    case Nil{}:
56      Equal.sym(Bool, Bool.and(Nat.is_eq(acc, 0n), True{}), Nat.is_eq(acc, 0n), and_true_r(Nat.is_eq(acc, 0n)))
57    case +x <> +t:
58      %Equal.sym(Bool, Nat.is_eq(L.nonzero(t, Nat.add(acc, x)), 0n), Bool.and(Nat.is_eq(Nat.add(acc, x), 0n), Nat.is_eq(LV.ev(t), 0n)), nonzero_v(t, Nat.add(acc, x))) : {_ == Bool.and(Nat.is_eq(acc, 0n), Nat.is_eq(Nat.add(x, C.shift(16n, LV.ev(t))), 0n)) : Bool}
59      %Equal.sym(Bool, Nat.is_eq(Nat.add(acc, x), 0n), Bool.and(Nat.is_eq(acc, 0n), Nat.is_eq(x, 0n)), is_eq_add0(acc, x)) : {Bool.and(_, Nat.is_eq(LV.ev(t), 0n)) == Bool.and(Nat.is_eq(acc, 0n), Nat.is_eq(Nat.add(x, C.shift(16n, LV.ev(t))), 0n)) : Bool}
60      %Equal.sym(Bool, Nat.is_eq(Nat.add(x, C.shift(16n, LV.ev(t))), 0n), Bool.and(Nat.is_eq(x, 0n), Nat.is_eq(C.shift(16n, LV.ev(t)), 0n)), is_eq_add0(x, C.shift(16n, LV.ev(t)))) : {Bool.and(Bool.and(Nat.is_eq(acc, 0n), Nat.is_eq(x, 0n)), Nat.is_eq(LV.ev(t), 0n)) == Bool.and(Nat.is_eq(acc, 0n), _) : Bool}
61      %Equal.sym(Bool, Nat.is_eq(C.shift(16n, LV.ev(t)), 0n), Nat.is_eq(LV.ev(t), 0n), sh_eq0(LV.ev(t))) : {Bool.and(Bool.and(Nat.is_eq(acc, 0n), Nat.is_eq(x, 0n)), Nat.is_eq(LV.ev(t), 0n)) == Bool.and(Nat.is_eq(acc, 0n), Bool.and(Nat.is_eq(x, 0n), _)) : Bool}
62      %Equal.sym(Bool, Bool.and(Bool.and(Nat.is_eq(acc, 0n), Nat.is_eq(x, 0n)), Nat.is_eq(LV.ev(t), 0n)), Bool.and(Nat.is_eq(acc, 0n), Bool.and(Nat.is_eq(x, 0n), Nat.is_eq(LV.ev(t), 0n))), and_assoc(Nat.is_eq(acc, 0n), Nat.is_eq(x, 0n), Nat.is_eq(LV.ev(t), 0n))) : {_ == Bool.and(Nat.is_eq(acc, 0n), Bool.and(Nat.is_eq(x, 0n), Nat.is_eq(LV.ev(t), 0n))) : Bool}
63      {==}
64
65def is_zero_v(+xs: List<&2, Nat>) -> {L.is_zero(xs) == Nat.is_eq(LV.ev(xs), 0n) : Bool}:
66  nonzero_v(xs, 0n)
67
68# ---- parity ----
69
70def parity_v(+xs: List<&2, Nat>) -> {Nat.mod(L.hd0(xs), 2n) == Nat.mod(LV.ev(xs), 2n) : Nat}:
71  match xs:
72    case Nil{}:
73      {==}
74    case +x <> +t:
75      Equal.sym(Nat, Nat.mod(Nat.add(x, C.shift(16n, LV.ev(t))), 2n), Nat.mod(x, 2n), WW.odd_limb(15n, x, LV.ev(t)))
76
77# ---- Bool from implications ----
78
79def iff_bool(p: Bool, q: Bool, f: {p == True{} : Bool} -> {q == True{} : Bool}, g: {q == True{} : Bool} -> {p == True{} : Bool}) -> {p == q : Bool}:
80  match p q:
81    case True{} True{}:
82      {==}
83    case False{} False{}:
84      {==}
85    case True{} False{}:
86      Empty.absurd({True{} == False{} : Bool}, Lg.false_true(f({==})))
87    case False{} True{}:
88      Empty.absurd({False{} == True{} : Bool}, Lg.false_true(g({==})))
89
90# ---- a limb and the rest are unique (x, y < 2^16) ----
91
92def w_succ(+one: Nat, +h1: {one == 1n : Nat}) -> {1n+Nat.sub(C.shift(16n, one), 1n) == C.shift(16n, one) : Nat}:
93  N.sub_add(C.shift(16n, one), 1n, N.lt_succ_le_succ(0n, C.shift(16n, one), B.pos_pos(one, h1, 1n)))
94
95# x + 2^16 a = a W + x with W = 1 + wp
96def digit_form(+one: Nat, +h1: {one == 1n : Nat}, +x: Nat, +a: Nat) -> {Nat.add(x, C.shift(16n, a)) == Nat.add(Nat.mul(a, 1n+Nat.sub(C.shift(16n, one), 1n)), x) : Nat}:
97  %Equal.sym(Nat, 1n+Nat.sub(C.shift(16n, one), 1n), C.shift(16n, one), w_succ(one, h1)) : {Nat.add(x, C.shift(16n, a)) == Nat.add(Nat.mul(a, _), x) : Nat}
98  %Equal.sym(Nat, C.shift(16n, a), Nat.mul(a, C.shift(16n, one)), WW.shift_mul_one(16n, one, h1, a)) : {Nat.add(x, _) == Nat.add(Nat.mul(a, C.shift(16n, one)), x) : Nat}
99  %Equal.sym(Nat, Nat.add(x, Nat.mul(a, C.shift(16n, one))), Nat.add(Nat.mul(a, C.shift(16n, one)), x), NA.add_comm(x, Nat.mul(a, C.shift(16n, one)))) : {_ == Nat.add(Nat.mul(a, C.shift(16n, one)), x) : Nat}
100  {==}
101
102def lt_w(+one: Nat, +h1: {one == 1n : Nat}, +x: Nat, +hx: {Nat.is_lt(x, C.shift(16n, one)) == True{} : Bool}) -> {Nat.is_lt(x, 1n+Nat.sub(C.shift(16n, one), 1n)) == True{} : Bool}:
103  %Equal.sym(Nat, 1n+Nat.sub(C.shift(16n, one), 1n), C.shift(16n, one), w_succ(one, h1)) : {Nat.is_lt(x, _) == True{} : Bool}
104  hx
105
106def uniq_lo(+one: Nat, +h1: {one == 1n : Nat}, +x: Nat, +y: Nat, +a: Nat, +b: Nat, +hx: {Nat.is_lt(x, C.shift(16n, one)) == True{} : Bool}, +hy: {Nat.is_lt(y, C.shift(16n, one)) == True{} : Bool}, +e: {Nat.add(x, C.shift(16n, a)) == Nat.add(y, C.shift(16n, b)) : Nat}) -> {x == y : Nat}:
107  +wp = Nat.sub(C.shift(16n, one), 1n)
108  +ex = Equal.sym(Nat, Nat.mod(Nat.add(Nat.mul(a, 1n+wp), x), 1n+wp), x, NR.mod_of(a, wp, x, lt_w(one, h1, x, hx)))
109  +ey = NR.mod_of(b, wp, y, lt_w(one, h1, y, hy))
110  +e2 = Equal.trans(Nat, Nat.add(Nat.mul(a, 1n+wp), x), Nat.add(x, C.shift(16n, a)), Nat.add(Nat.mul(b, 1n+wp), y), Equal.sym(Nat, Nat.add(x, C.shift(16n, a)), Nat.add(Nat.mul(a, 1n+wp), x), digit_form(one, h1, x, a)), Equal.trans(Nat, Nat.add(x, C.shift(16n, a)), Nat.add(y, C.shift(16n, b)), Nat.add(Nat.mul(b, 1n+wp), y), e, digit_form(one, h1, y, b)))
111  Equal.trans(Nat, x, Nat.mod(Nat.add(Nat.mul(a, 1n+wp), x), 1n+wp), y, ex, Equal.trans(Nat, Nat.mod(Nat.add(Nat.mul(a, 1n+wp), x), 1n+wp), Nat.mod(Nat.add(Nat.mul(b, 1n+wp), y), 1n+wp), y, Equal.cong(Nat, Nat, z => Nat.mod(z, 1n+wp), Nat.add(Nat.mul(a, 1n+wp), x), Nat.add(Nat.mul(b, 1n+wp), y), e2), ey))
112
113def uniq_hi(+one: Nat, +h1: {one == 1n : Nat}, +x: Nat, +y: Nat, +a: Nat, +b: Nat, +hx: {Nat.is_lt(x, C.shift(16n, one)) == True{} : Bool}, +hy: {Nat.is_lt(y, C.shift(16n, one)) == True{} : Bool}, +e: {Nat.add(x, C.shift(16n, a)) == Nat.add(y, C.shift(16n, b)) : Nat}) -> {a == b : Nat}:
114  +wp = Nat.sub(C.shift(16n, one), 1n)
115  +ex = Equal.sym(Nat, Nat.div(Nat.add(Nat.mul(a, 1n+wp), x), 1n+wp), a, NR.div_of(a, wp, x, lt_w(one, h1, x, hx)))
116  +ey = NR.div_of(b, wp, y, lt_w(one, h1, y, hy))
117  +e2 = Equal.trans(Nat, Nat.add(Nat.mul(a, 1n+wp), x), Nat.add(x, C.shift(16n, a)), Nat.add(Nat.mul(b, 1n+wp), y), Equal.sym(Nat, Nat.add(x, C.shift(16n, a)), Nat.add(Nat.mul(a, 1n+wp), x), digit_form(one, h1, x, a)), Equal.trans(Nat, Nat.add(x, C.shift(16n, a)), Nat.add(y, C.shift(16n, b)), Nat.add(Nat.mul(b, 1n+wp), y), e, digit_form(one, h1, y, b)))
118  Equal.trans(Nat, a, Nat.div(Nat.add(Nat.mul(a, 1n+wp), x), 1n+wp), b, ex, Equal.trans(Nat, Nat.div(Nat.add(Nat.mul(a, 1n+wp), x), 1n+wp), Nat.div(Nat.add(Nat.mul(b, 1n+wp), y), 1n+wp), b, Equal.cong(Nat, Nat, z => Nat.div(z, 1n+wp), Nat.add(Nat.mul(a, 1n+wp), x), Nat.add(Nat.mul(b, 1n+wp), y), e2), ey))
119
120def eq_digit_f(+one: Nat, +h1: {one == 1n : Nat}, +x: Nat, +y: Nat, +a: Nat, +b: Nat, +hx: {Nat.is_lt(x, C.shift(16n, one)) == True{} : Bool}, +hy: {Nat.is_lt(y, C.shift(16n, one)) == True{} : Bool}, +h: {Nat.is_eq(Nat.add(x, C.shift(16n, a)), Nat.add(y, C.shift(16n, b))) == True{} : Bool}) -> {Bool.and(Nat.is_eq(x, y), Nat.is_eq(a, b)) == True{} : Bool}:
121  +e = N.eq_from_is_eq(Nat.add(x, C.shift(16n, a)), Nat.add(y, C.shift(16n, b)), h)
122  +exy = uniq_lo(one, h1, x, y, a, b, hx, hy, e)
123  +eab = uniq_hi(one, h1, x, y, a, b, hx, hy, e)
124  Lg.and_intro(Nat.is_eq(x, y), Nat.is_eq(a, b), Lg.subst(Nat, z => {Nat.is_eq(x, z) == True{} : Bool}, x, y, exy, N.is_eq_refl(x)), Lg.subst(Nat, z => {Nat.is_eq(a, z) == True{} : Bool}, a, b, eab, N.is_eq_refl(a)))
125
126def eq_digit_g(+x: Nat, +y: Nat, +a: Nat, +b: Nat, +h: {Bool.and(Nat.is_eq(x, y), Nat.is_eq(a, b)) == True{} : Bool}) -> {Nat.is_eq(Nat.add(x, C.shift(16n, a)), Nat.add(y, C.shift(16n, b))) == True{} : Bool}:
127  +exy = N.eq_from_is_eq(x, y, Lg.and_left(Nat.is_eq(x, y), Nat.is_eq(a, b), h))
128  +eab = N.eq_from_is_eq(a, b, Lg.and_right(Nat.is_eq(x, y), Nat.is_eq(a, b), h))
129  %Equal.sym(Nat, x, y, exy) : {Nat.is_eq(Nat.add(_, C.shift(16n, a)), Nat.add(y, C.shift(16n, b))) == True{} : Bool}
130  %Equal.sym(Nat, a, b, eab) : {Nat.is_eq(Nat.add(y, C.shift(16n, _)), Nat.add(y, C.shift(16n, b))) == True{} : Bool}
131  N.is_eq_refl(Nat.add(y, C.shift(16n, b)))
132
133def eq_digit(+one: Nat, +h1: {one == 1n : Nat}, +x: Nat, +y: Nat, +a: Nat, +b: Nat, +hx: {Nat.is_lt(x, C.shift(16n, one)) == True{} : Bool}, +hy: {Nat.is_lt(y, C.shift(16n, one)) == True{} : Bool}) -> {Nat.is_eq(Nat.add(x, C.shift(16n, a)), Nat.add(y, C.shift(16n, b))) == Bool.and(Nat.is_eq(x, y), Nat.is_eq(a, b)) : Bool}:
134  iff_bool(Nat.is_eq(Nat.add(x, C.shift(16n, a)), Nat.add(y, C.shift(16n, b))), Bool.and(Nat.is_eq(x, y), Nat.is_eq(a, b)), h => eq_digit_f(one, h1, x, y, a, b, hx, hy, h), h => eq_digit_g(x, y, a, b, h))
135
136# ---- eq ----
137
138# (x - y) + (y - x) == 0 exactly when x == y
139def absdiff(x: Nat, y: Nat) -> {Nat.is_eq(Nat.add(Nat.sub(x, y), Nat.sub(y, x)), 0n) == Nat.is_eq(x, y) : Bool}:
140  match x y:
141    case 0n 0n:
142      {==}
143    case 0n 1n+q:
144      {==}
145    case 1n+p 0n:
146      {==}
147    case 1n+p 1n+q:
148      absdiff(p, q)
149
150def diff_v(+one: Nat, +h1: {one == 1n : Nat}, n: Nat, xs: List<&2, Nat>, ys: List<&2, Nat>, +acc: Nat, +hx: {FS.limbs16(one, n, xs) == True{} : Bool}, +hy: {FS.limbs16(one, n, ys) == True{} : Bool}) -> {Nat.is_eq(L.diff(xs, ys, acc), 0n) == Bool.and(Nat.is_eq(acc, 0n), Nat.is_eq(LV.ev(xs), LV.ev(ys))) : Bool}:
151  match n xs ys:
152    case 0n Nil{} Nil{}:
153      Equal.sym(Bool, Bool.and(Nat.is_eq(acc, 0n), True{}), Nat.is_eq(acc, 0n), and_true_r(Nat.is_eq(acc, 0n)))
154    case 0n Nil{} y <> yt:
155      Empty.absurd({Nat.is_eq(L.diff([], y <> yt, acc), 0n) == Bool.and(Nat.is_eq(acc, 0n), Nat.is_eq(LV.ev([]), LV.ev(y <> yt))) : Bool}, Lg.false_true(hy))
156    case 0n x <> xt _:
157      Empty.absurd({Nat.is_eq(L.diff(x <> xt, ys, acc), 0n) == Bool.and(Nat.is_eq(acc, 0n), Nat.is_eq(LV.ev(x <> xt), LV.ev(ys))) : Bool}, Lg.false_true(hx))
158    case 1n+k Nil{} _:
159      Empty.absurd({Nat.is_eq(L.diff([], ys, acc), 0n) == Bool.and(Nat.is_eq(acc, 0n), Nat.is_eq(LV.ev([]), LV.ev(ys))) : Bool}, Lg.false_true(hx))
160    case 1n+k x <> xt Nil{}:
161      Empty.absurd({Nat.is_eq(L.diff(x <> xt, [], acc), 0n) == Bool.and(Nat.is_eq(acc, 0n), Nat.is_eq(LV.ev(x <> xt), LV.ev([]))) : Bool}, Lg.false_true(hy))
162    case 1n+ +k +x <> +xt +y <> +yt:
163      +hx0 = Lg.and_left(Nat.is_lt(x, C.shift(16n, one)), FS.limbs16(one, k, xt), hx)
164      +hy0 = Lg.and_left(Nat.is_lt(y, C.shift(16n, one)), FS.limbs16(one, k, yt), hy)
165      +hxt = Lg.and_right(Nat.is_lt(x, C.shift(16n, one)), FS.limbs16(one, k, xt), hx)
166      +hyt = Lg.and_right(Nat.is_lt(y, C.shift(16n, one)), FS.limbs16(one, k, yt), hy)
167      %Equal.sym(Bool, Nat.is_eq(L.diff(xt, yt, Nat.add(acc, Nat.add(Nat.sub(x, y), Nat.sub(y, x)))), 0n), Bool.and(Nat.is_eq(Nat.add(acc, Nat.add(Nat.sub(x, y), Nat.sub(y, x))), 0n), Nat.is_eq(LV.ev(xt), LV.ev(yt))), diff_v(one, h1, k, xt, yt, Nat.add(acc, Nat.add(Nat.sub(x, y), Nat.sub(y, x))), hxt, hyt)) : {_ == Bool.and(Nat.is_eq(acc, 0n), Nat.is_eq(Nat.add(x, C.shift(16n, LV.ev(xt))), Nat.add(y, C.shift(16n, LV.ev(yt))))) : Bool}
168      %Equal.sym(Bool, Nat.is_eq(Nat.add(acc, Nat.add(Nat.sub(x, y), Nat.sub(y, x))), 0n), Bool.and(Nat.is_eq(acc, 0n), Nat.is_eq(Nat.add(Nat.sub(x, y), Nat.sub(y, x)), 0n)), is_eq_add0(acc, Nat.add(Nat.sub(x, y), Nat.sub(y, x)))) : {Bool.and(_, Nat.is_eq(LV.ev(xt), LV.ev(yt))) == Bool.and(Nat.is_eq(acc, 0n), Nat.is_eq(Nat.add(x, C.shift(16n, LV.ev(xt))), Nat.add(y, C.shift(16n, LV.ev(yt))))) : Bool}
169      %Equal.sym(Bool, Nat.is_eq(Nat.add(Nat.sub(x, y), Nat.sub(y, x)), 0n), Nat.is_eq(x, y), absdiff(x, y)) : {Bool.and(Bool.and(Nat.is_eq(acc, 0n), _), Nat.is_eq(LV.ev(xt), LV.ev(yt))) == Bool.and(Nat.is_eq(acc, 0n), Nat.is_eq(Nat.add(x, C.shift(16n, LV.ev(xt))), Nat.add(y, C.shift(16n, LV.ev(yt))))) : Bool}
170      %Equal.sym(Bool, Nat.is_eq(Nat.add(x, C.shift(16n, LV.ev(xt))), Nat.add(y, C.shift(16n, LV.ev(yt)))), Bool.and(Nat.is_eq(x, y), Nat.is_eq(LV.ev(xt), LV.ev(yt))), eq_digit(one, h1, x, y, LV.ev(xt), LV.ev(yt), hx0, hy0)) : {Bool.and(Bool.and(Nat.is_eq(acc, 0n), Nat.is_eq(x, y)), Nat.is_eq(LV.ev(xt), LV.ev(yt))) == Bool.and(Nat.is_eq(acc, 0n), _) : Bool}
171      %Equal.sym(Bool, Bool.and(Bool.and(Nat.is_eq(acc, 0n), Nat.is_eq(x, y)), Nat.is_eq(LV.ev(xt), LV.ev(yt))), Bool.and(Nat.is_eq(acc, 0n), Bool.and(Nat.is_eq(x, y), Nat.is_eq(LV.ev(xt), LV.ev(yt)))), and_assoc(Nat.is_eq(acc, 0n), Nat.is_eq(x, y), Nat.is_eq(LV.ev(xt), LV.ev(yt)))) : {_ == Bool.and(Nat.is_eq(acc, 0n), Bool.and(Nat.is_eq(x, y), Nat.is_eq(LV.ev(xt), LV.ev(yt)))) : Bool}
172      {==}
173
174def eq_v(+one: Nat, +h1: {one == 1n : Nat}, +xs: List<&2, Nat>, +ys: List<&2, Nat>, +hx: {FS.limbs16(one, 16n, xs) == True{} : Bool}, +hy: {FS.limbs16(one, 16n, ys) == True{} : Bool}) -> {L.eq(xs, ys) == Nat.is_eq(LV.ev(xs), LV.ev(ys)) : Bool}:
175  diff_v(one, h1, 16n, xs, ys, 0n, hx, hy)
176
177# ---- x < m through the carry out of x + c ----
178
179def hz(+lo: Nat, hi: Nat, +t: Nat, +hl: {Nat.is_lt(lo, t) == True{} : Bool}) -> {Nat.is_eq(hi, 0n) == Nat.is_lt(Nat.add(lo, Nat.mul(hi, t)), t) : Bool}:
180  match hi:
181    case 0n:
182      %Equal.sym(Nat, Nat.add(lo, 0n), lo, NA.add_zero(lo)) : {True{} == Nat.is_lt(_, t) : Bool}
183      Equal.sym(Bool, Nat.is_lt(lo, t), True{}, hl)
184    case 1n+ +k:
185      Equal.sym(Bool, Nat.is_lt(Nat.add(lo, Nat.add(t, Nat.mul(k, t))), t), False{}, N.le_not_lt(Nat.add(lo, Nat.add(t, Nat.mul(k, t))), t, N.le_trans(t, Nat.add(t, Nat.mul(k, t)), Nat.add(lo, Nat.add(t, Nat.mul(k, t))), N.le_add_right(t, Nat.mul(k, t)), I.le_add_l(lo, Nat.add(t, Nat.mul(k, t))))))
186
187def ltm_v(+one: Nat, +h1: {one == 1n : Nat}, +mp: Nat, +c: List<&2, Nat>, +hm: {Nat.add(1n+mp, LV.ev(c)) == C.shift(256n, one) : Nat}, +x: List<&2, Nat>) -> {L.ltm(c, x) == Nat.is_lt(LV.ev(x), 1n+mp) : Bool}:
188  +u = L.carry(32n, L.add(x, c), 0n)
189  +hu16 = B.carry_limbs(one, h1, 32n, 16n, L.add(x, c), 0n, {==})
190  +ll = I.lt_subst_r(LV.ev(L.take(16n, u)), LV.pos(16n, one), C.shift(256n, one), B.pos16(one), B.limbs_lt(one, h1, 16n, L.take(16n, u), hu16))
191  %Equal.sym(Nat, L.horner(L.drop(16n, L.carry(32n, L.add(x, c), 0n))), LV.ev(L.drop(16n, L.carry(32n, L.add(x, c), 0n))), LV.horner_v(L.drop(16n, L.carry(32n, L.add(x, c), 0n)))) : {Nat.is_eq(_, 0n) == Nat.is_lt(LV.ev(x), 1n+mp) : Bool}
192  %Equal.sym(Bool, Nat.is_eq(LV.ev(L.drop(16n, L.carry(32n, L.add(x, c), 0n))), 0n), Nat.is_lt(Nat.add(LV.ev(L.take(16n, L.carry(32n, L.add(x, c), 0n))), Nat.mul(LV.ev(L.drop(16n, L.carry(32n, L.add(x, c), 0n))), C.shift(256n, one))), C.shift(256n, one)), hz(LV.ev(L.take(16n, L.carry(32n, L.add(x, c), 0n))), LV.ev(L.drop(16n, L.carry(32n, L.add(x, c), 0n))), C.shift(256n, one), ll)) : {_ == Nat.is_lt(LV.ev(x), 1n+mp) : Bool}
193  %Equal.sym(Nat, Nat.add(LV.ev(L.take(16n, L.carry(32n, L.add(x, c), 0n))), Nat.mul(LV.ev(L.drop(16n, L.carry(32n, L.add(x, c), 0n))), C.shift(256n, one))), LV.ev(L.carry(32n, L.add(x, c), 0n)), Equal.sym(Nat, LV.ev(L.carry(32n, L.add(x, c), 0n)), Nat.add(LV.ev(L.take(16n, L.carry(32n, L.add(x, c), 0n))), Nat.mul(LV.ev(L.drop(16n, L.carry(32n, L.add(x, c), 0n))), C.shift(256n, one))), R.split256(one, h1, L.carry(32n, L.add(x, c), 0n)))) : {Nat.is_lt(_, C.shift(256n, one)) == Nat.is_lt(LV.ev(x), 1n+mp) : Bool}
194  %Equal.sym(Nat, LV.ev(L.carry(32n, L.add(x, c), 0n)), Nat.add(LV.ev(x), LV.ev(c)), R.u_val(c, x)) : {Nat.is_lt(_, C.shift(256n, one)) == Nat.is_lt(LV.ev(x), 1n+mp) : Bool}
195  %Equal.sym(Nat, C.shift(256n, one), Nat.add(1n+mp, LV.ev(c)), Equal.sym(Nat, Nat.add(1n+mp, LV.ev(c)), C.shift(256n, one), hm)) : {Nat.is_lt(Nat.add(LV.ev(x), LV.ev(c)), _) == Nat.is_lt(LV.ev(x), 1n+mp) : Bool}
196  WW.lt_cancel_r(LV.ev(x), 1n+mp, LV.ev(c))
197
198def ltm_vv(+one: Nat, +h1: {one == 1n : Nat}, +mp: Nat, +c: List<&2, Nat>, +hm: {Nat.add(1n+mp, FS.value(one, c)) == C.shift(256n, one) : Nat}, +x: List<&2, Nat>) -> {L.ltm(c, x) == Nat.is_lt(LV.ev(x), 1n+mp) : Bool}:
199  ltm_v(one, h1, mp, c, Lg.subst(Nat, z => {Nat.add(1n+mp, z) == C.shift(256n, one) : Nat}, FS.value(one, c), LV.ev(c), LV.ev_value(one, h1, c), hm), x)
200
201# ---- small constants: norm16([k]) for k < 2^16 ----
202
203def small_ev(+k: Nat) -> {LV.ev([k]) == k : Nat}:
204  %Equal.sym(Nat, C.shift(16n, 0n), 0n, WW.shift_zero(16n)) : {Nat.add(k, _) == k : Nat}
205  %Equal.sym(Nat, Nat.add(k, 0n), k, NA.add_zero(k)) : {_ == k : Nat}
206  {==}
207
208def small_v(+one: Nat, +h1: {one == 1n : Nat}, +k: Nat, +hk: {Nat.is_lt(k, C.shift(256n, one)) == True{} : Bool}) -> {LV.ev(L.norm16([k])) == k : Nat}:
209  +x = L.carry(32n, [k], 0n)
210  +ex = Equal.trans(Nat, LV.ev(x), LV.ev([k]), k, LV.carry_v(32n, [k], 0n), small_ev(k))
211  %Equal.sym(Nat, LV.ev(L.take(16n, L.carry(32n, [k], 0n))), LV.ev(L.carry(32n, [k], 0n)), R.take_small(one, h1, L.carry(32n, [k], 0n), I.lt_subst_l(k, LV.ev(x), C.shift(256n, one), Equal.sym(Nat, LV.ev(x), k, ex), hk))) : {_ == k : Nat}
212  %Equal.sym(Nat, LV.ev(L.carry(32n, [k], 0n)), k, ex) : {_ == k : Nat}
213  {==}
214
215def small_l(+one: Nat, +h1: {one == 1n : Nat}, +k: Nat) -> {FS.limbs16(one, 16n, L.norm16([k])) == True{} : Bool}:
216  B.carry_limbs(one, h1, 32n, 16n, [k], 0n, {==})