proofs/crypto/secp256k1/negate.bend

bend-collections-laws-crypto@1.0.0.0 · 180 lines · 16 definitions

1# GENERATED by tools/generators/rw.py from ../../../tools/generators/secp256k1_hand/negate.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# Complements and the borrow-free negation of src/crypto/secp256k1/limbs.bend:
18# comp(x) + x + 1 = 2^(16 n) for n limbs below 2^16, and
19# negraw(c, b) + b = 2 m for m = 2^256 - c (so a + negraw(c, b) is congruent
20# to a - b), with 256 written as the symbolic 2^8 = C.shift(8n, one).
21
22def e255(+one: Nat, +h1: {one == 1n : Nat}) -> {Nat.sub(C.shift(8n, one), 1n) == 255n : Nat}:
23  %Equal.sym(Nat, one, 1n, h1) : {Nat.sub(C.shift(8n, _), 1n) == 255n : Nat}
24  {==}
25
26def bb_sq(+one: Nat, +h1: {one == 1n : Nat}) -> {Nat.mul(C.shift(8n, one), C.shift(8n, one)) == C.shift(16n, one) : Nat}:
27  %Equal.sym(Nat, Nat.mul(C.shift(8n, one), C.shift(8n, one)), C.shift(8n, Nat.mul(one, C.shift(8n, one))), WW.shift_mul_l(8n, one, C.shift(8n, one))) : {_ == C.shift(16n, one) : Nat}
28  %Equal.sym(Nat, Nat.mul(one, C.shift(8n, one)), C.shift(8n, one), LV.mul_one_l(one, h1, C.shift(8n, one))) : {C.shift(8n, _) == C.shift(16n, one) : Nat}
29  %Equal.sym(Nat, C.shift(8n, C.shift(8n, one)), C.shift(16n, one), SR.shift_shift(8n, 8n, one)) : {_ == C.shift(16n, one) : Nat}
30  {==}
31
32def bb_pos(+one: Nat, +h1: {one == 1n : Nat}) -> {Nat.is_le(1n, C.shift(8n, one)) == True{} : Bool}:
33  %Equal.sym(Nat, one, 1n, h1) : {Nat.is_le(1n, C.shift(8n, _)) == True{} : Bool}
34  {==}
35
36# (B - 1) + 1 = B
37def pred_succ(+b: Nat, +h: {Nat.is_le(1n, b) == True{} : Bool}) -> {Nat.add(Nat.sub(b, 1n), 1n) == b : Nat}:
38  %Equal.sym(Nat, Nat.add(Nat.sub(b, 1n), 1n), Nat.add(1n, Nat.sub(b, 1n)), NA.add_comm(Nat.sub(b, 1n), 1n)) : {_ == b : Nat}
39  N.sub_add(b, 1n, h)
40
41# (B - 1) + (B - 1) B + 1 = B B
42def digit_max(+b: Nat, +h: {Nat.is_le(1n, b) == True{} : Bool}) -> {Nat.add(Nat.add(Nat.sub(b, 1n), Nat.mul(Nat.sub(b, 1n), b)), 1n) == Nat.mul(b, b) : Nat}:
43  %Equal.sym(Nat, Nat.add(Nat.add(Nat.sub(b, 1n), Nat.mul(Nat.sub(b, 1n), b)), 1n), Nat.add(Nat.sub(b, 1n), Nat.add(Nat.mul(Nat.sub(b, 1n), b), 1n)), NA.add_assoc(Nat.sub(b, 1n), Nat.mul(Nat.sub(b, 1n), b), 1n)) : {_ == Nat.mul(b, b) : Nat}
44  %Equal.sym(Nat, Nat.add(Nat.mul(Nat.sub(b, 1n), b), 1n), Nat.add(1n, Nat.mul(Nat.sub(b, 1n), b)), NA.add_comm(Nat.mul(Nat.sub(b, 1n), b), 1n)) : {Nat.add(Nat.sub(b, 1n), _) == Nat.mul(b, b) : Nat}
45  %Equal.sym(Nat, Nat.add(Nat.sub(b, 1n), Nat.add(1n, Nat.mul(Nat.sub(b, 1n), b))), Nat.add(Nat.add(Nat.sub(b, 1n), 1n), Nat.mul(Nat.sub(b, 1n), b)), Equal.sym(Nat, Nat.add(Nat.add(Nat.sub(b, 1n), 1n), Nat.mul(Nat.sub(b, 1n), b)), Nat.add(Nat.sub(b, 1n), Nat.add(1n, Nat.mul(Nat.sub(b, 1n), b))), NA.add_assoc(Nat.sub(b, 1n), 1n, Nat.mul(Nat.sub(b, 1n), b)))) : {_ == Nat.mul(b, b) : Nat}
46  %Equal.sym(Nat, Nat.add(Nat.sub(b, 1n), 1n), b, pred_succ(b, h)) : {Nat.add(_, Nat.mul(Nat.sub(b, 1n), b)) == Nat.mul(b, b) : Nat}
47  %Equal.sym(Nat, b, Nat.mul(b, 1n), Equal.sym(Nat, Nat.mul(b, 1n), b, NA.mul_one(b))) : {Nat.add(_, Nat.mul(Nat.sub(b, 1n), b)) == Nat.mul(b, b) : Nat}
48  %Equal.sym(Nat, Nat.mul(b, 1n), Nat.mul(1n, b), NA.mul_comm(b, 1n)) : {Nat.add(_, Nat.mul(Nat.sub(b, 1n), b)) == Nat.mul(b, b) : Nat}
49  %Equal.sym(Nat, Nat.add(Nat.mul(1n, b), Nat.mul(Nat.sub(b, 1n), b)), Nat.mul(Nat.add(1n, Nat.sub(b, 1n)), b), Equal.sym(Nat, Nat.mul(Nat.add(1n, Nat.sub(b, 1n)), b), Nat.add(Nat.mul(1n, b), Nat.mul(Nat.sub(b, 1n), b)), NA.mul_add_right(1n, Nat.sub(b, 1n), b))) : {_ == Nat.mul(b, b) : Nat}
50  %Equal.sym(Nat, Nat.add(1n, Nat.sub(b, 1n)), Nat.add(Nat.sub(b, 1n), 1n), NA.add_comm(1n, Nat.sub(b, 1n))) : {Nat.mul(_, b) == Nat.mul(b, b) : Nat}
51  %Equal.sym(Nat, Nat.add(Nat.sub(b, 1n), 1n), b, pred_succ(b, h)) : {Nat.mul(_, b) == Nat.mul(b, b) : Nat}
52  {==}
53
54# x < 2^16: x div 256 < 256
55def hi_byte_lt(+one: Nat, +h1: {one == 1n : Nat}, +x: Nat, +hx: {Nat.is_lt(x, C.shift(16n, one)) == True{} : Bool}) -> {Nat.is_lt(Nat.div(x, 256n), 256n) == True{} : Bool}:
56  +bq = C.shift(8n, one)
57  +hi = Nat.div(x, 256n)
58  +le = I.le_subst_r(Nat.mul(hi, 256n), Nat.add(Nat.mul(hi, 256n), Nat.mod(x, 256n)), x, Equal.sym(Nat, x, Nat.add(Nat.mul(hi, 256n), Nat.mod(x, 256n)), NR.dm_eq(255n, x)), N.le_add_right(Nat.mul(hi, 256n), Nat.mod(x, 256n)))
59  +le2 = I.le_subst_l(Nat.mul(hi, 256n), Nat.mul(hi, bq), x, Equal.cong(Nat, Nat, z => Nat.mul(hi, z), 256n, bq, Equal.sym(Nat, bq, 256n, LV.b8(one, h1))), le)
60  +s1 = N.le_lt_trans(Nat.mul(hi, bq), x, C.shift(16n, one), le2, hx)
61  +s2 = I.lt_subst_r(Nat.mul(hi, bq), C.shift(16n, one), Nat.mul(bq, bq), Equal.sym(Nat, Nat.mul(bq, bq), C.shift(16n, one), bb_sq(one, h1)), s1)
62  +s3 = R.mul_lt_cancel(bq, hi, bq, s2, Nat.is_lt(hi, bq), {==})
63  I.lt_subst_r(hi, bq, 256n, LV.b8(one, h1), s3)
64
65# (l + h B) + (h' B + l') = (l' + l) + (h' + h) B
66def combine(+l: Nat, +h: Nat, +h2: Nat, +l2: Nat, +b: Nat) -> {Nat.add(Nat.add(l, Nat.mul(h, b)), Nat.add(Nat.mul(h2, b), l2)) == Nat.add(Nat.add(l2, l), Nat.mul(Nat.add(h2, h), b)) : Nat}:
67  %Equal.sym(Nat, Nat.mul(h, b), Nat.mul(b, h), NA.mul_comm(h, b)) : {Nat.add(Nat.add(l, _), Nat.add(Nat.mul(h2, b), l2)) == Nat.add(Nat.add(l2, l), Nat.mul(Nat.add(h2, h), b)) : Nat}
68  %Equal.sym(Nat, Nat.add(l, Nat.mul(b, h)), Nat.add(Nat.mul(b, h), l), NA.add_comm(l, Nat.mul(b, h))) : {Nat.add(_, Nat.add(Nat.mul(h2, b), l2)) == Nat.add(Nat.add(l2, l), Nat.mul(Nat.add(h2, h), b)) : Nat}
69  %Equal.sym(Nat, Nat.mul(h2, b), Nat.mul(b, h2), NA.mul_comm(h2, b)) : {Nat.add(Nat.add(Nat.mul(b, h), l), Nat.add(_, l2)) == Nat.add(Nat.add(l2, l), Nat.mul(Nat.add(h2, h), b)) : Nat}
70  %Equal.sym(Nat, Nat.add(Nat.add(Nat.mul(b, h), l), Nat.add(Nat.mul(b, h2), l2)), Nat.add(Nat.mul(b, h), Nat.add(l, Nat.add(Nat.mul(b, h2), l2))), NA.add_assoc(Nat.mul(b, h), l, Nat.add(Nat.mul(b, h2), l2))) : {_ == Nat.add(Nat.add(l2, l), Nat.mul(Nat.add(h2, h), b)) : Nat}
71  %Equal.sym(Nat, Nat.add(l, Nat.add(Nat.mul(b, h2), l2)), Nat.add(Nat.mul(b, h2), Nat.add(l, l2)), NA.add_swap(l, Nat.mul(b, h2), l2)) : {Nat.add(Nat.mul(b, h), _) == Nat.add(Nat.add(l2, l), Nat.mul(Nat.add(h2, h), b)) : Nat}
72  %Equal.sym(Nat, Nat.add(l2, l), Nat.add(l, l2), NA.add_comm(l2, l)) : {Nat.add(Nat.mul(b, h), Nat.add(Nat.mul(b, h2), Nat.add(l, l2))) == Nat.add(_, Nat.mul(Nat.add(h2, h), b)) : Nat}
73  %Equal.sym(Nat, Nat.add(h2, h), Nat.add(h, h2), NA.add_comm(h2, h)) : {Nat.add(Nat.mul(b, h), Nat.add(Nat.mul(b, h2), Nat.add(l, l2))) == Nat.add(Nat.add(l, l2), Nat.mul(_, b)) : Nat}
74  %Equal.sym(Nat, Nat.mul(Nat.add(h, h2), b), Nat.add(Nat.mul(h, b), Nat.mul(h2, b)), NA.mul_add_right(h, h2, b)) : {Nat.add(Nat.mul(b, h), Nat.add(Nat.mul(b, h2), Nat.add(l, l2))) == Nat.add(Nat.add(l, l2), _) : Nat}
75  %Equal.sym(Nat, Nat.mul(h, b), Nat.mul(b, h), NA.mul_comm(h, b)) : {Nat.add(Nat.mul(b, h), Nat.add(Nat.mul(b, h2), Nat.add(l, l2))) == Nat.add(Nat.add(l, l2), Nat.add(_, Nat.mul(h2, b))) : Nat}
76  %Equal.sym(Nat, Nat.mul(h2, b), Nat.mul(b, h2), NA.mul_comm(h2, b)) : {Nat.add(Nat.mul(b, h), Nat.add(Nat.mul(b, h2), Nat.add(l, l2))) == Nat.add(Nat.add(l, l2), Nat.add(Nat.mul(b, h), _)) : Nat}
77  %Equal.sym(Nat, Nat.add(Nat.add(l, l2), Nat.add(Nat.mul(b, h), Nat.mul(b, h2))), Nat.add(l, Nat.add(l2, Nat.add(Nat.mul(b, h), Nat.mul(b, h2)))), NA.add_assoc(l, l2, Nat.add(Nat.mul(b, h), Nat.mul(b, h2)))) : {Nat.add(Nat.mul(b, h), Nat.add(Nat.mul(b, h2), Nat.add(l, l2))) == _ : Nat}
78  %Equal.sym(Nat, Nat.add(l2, Nat.add(Nat.mul(b, h), Nat.mul(b, h2))), Nat.add(Nat.mul(b, h), Nat.add(l2, Nat.mul(b, h2))), NA.add_swap(l2, Nat.mul(b, h), Nat.mul(b, h2))) : {Nat.add(Nat.mul(b, h), Nat.add(Nat.mul(b, h2), Nat.add(l, l2))) == Nat.add(l, _) : Nat}
79  %Equal.sym(Nat, Nat.add(l2, Nat.mul(b, h2)), Nat.add(Nat.mul(b, h2), l2), NA.add_comm(l2, Nat.mul(b, h2))) : {Nat.add(Nat.mul(b, h), Nat.add(Nat.mul(b, h2), Nat.add(l, l2))) == Nat.add(l, Nat.add(Nat.mul(b, h), _)) : Nat}
80  %Equal.sym(Nat, Nat.add(l, Nat.add(Nat.mul(b, h), Nat.add(Nat.mul(b, h2), l2))), Nat.add(Nat.mul(b, h), Nat.add(l, Nat.add(Nat.mul(b, h2), l2))), NA.add_swap(l, Nat.mul(b, h), Nat.add(Nat.mul(b, h2), l2))) : {Nat.add(Nat.mul(b, h), Nat.add(Nat.mul(b, h2), Nat.add(l, l2))) == _ : Nat}
81  %Equal.sym(Nat, Nat.add(l, Nat.add(Nat.mul(b, h2), l2)), Nat.add(Nat.mul(b, h2), Nat.add(l, l2)), NA.add_swap(l, Nat.mul(b, h2), l2)) : {Nat.add(Nat.mul(b, h), Nat.add(Nat.mul(b, h2), Nat.add(l, l2))) == Nat.add(Nat.mul(b, h), _) : Nat}
82  {==}
83
84# comp1(x) + x + 1 = 2^16 for x < 2^16
85def comp1_v(+one: Nat, +h1: {one == 1n : Nat}, +x: Nat, +hx: {Nat.is_lt(x, C.shift(16n, one)) == True{} : Bool}) -> {Nat.add(Nat.add(L.comp1(x), x), 1n) == C.shift(16n, one) : Nat}:
86  +lo = Nat.mod(x, 256n)
87  +hi = Nat.div(x, 256n)
88  +hl = N.lt_succ_le(lo, 255n, NR.dm_lt(255n, x))
89  +hh = N.lt_succ_le(hi, 255n, hi_byte_lt(one, h1, x, hx))
90  %Equal.sym(Nat, x, Nat.add(Nat.mul(Nat.div(x, 256n), 256n), Nat.mod(x, 256n)), NR.dm_eq(255n, x)) : {Nat.add(Nat.add(Nat.add(Nat.sub(255n, Nat.mod(x, 256n)), Nat.mul(Nat.sub(255n, Nat.div(x, 256n)), 256n)), _), 1n) == C.shift(16n, one) : Nat}
91  %Equal.sym(Nat, Nat.add(Nat.add(Nat.sub(255n, Nat.mod(x, 256n)), Nat.mul(Nat.sub(255n, Nat.div(x, 256n)), 256n)), Nat.add(Nat.mul(Nat.div(x, 256n), 256n), Nat.mod(x, 256n))), Nat.add(Nat.add(Nat.mod(x, 256n), Nat.sub(255n, Nat.mod(x, 256n))), Nat.mul(Nat.add(Nat.div(x, 256n), Nat.sub(255n, Nat.div(x, 256n))), 256n)), combine(Nat.sub(255n, Nat.mod(x, 256n)), Nat.sub(255n, Nat.div(x, 256n)), Nat.div(x, 256n), Nat.mod(x, 256n), 256n)) : {Nat.add(_, 1n) == C.shift(16n, one) : Nat}
92  %Equal.sym(Nat, 256n, C.shift(8n, one), Equal.sym(Nat, C.shift(8n, one), 256n, LV.b8(one, h1))) : {Nat.add(Nat.add(Nat.add(Nat.mod(x, 256n), Nat.sub(255n, Nat.mod(x, 256n))), Nat.mul(Nat.add(Nat.div(x, 256n), Nat.sub(255n, Nat.div(x, 256n))), _)), 1n) == C.shift(16n, one) : Nat}
93  %Equal.sym(Nat, Nat.add(Nat.mod(x, 256n), Nat.sub(255n, Nat.mod(x, 256n))), 255n, N.sub_add(255n, Nat.mod(x, 256n), hl)) : {Nat.add(Nat.add(_, Nat.mul(Nat.add(Nat.div(x, 256n), Nat.sub(255n, Nat.div(x, 256n))), C.shift(8n, one))), 1n) == C.shift(16n, one) : Nat}
94  %Equal.sym(Nat, Nat.add(Nat.div(x, 256n), Nat.sub(255n, Nat.div(x, 256n))), 255n, N.sub_add(255n, Nat.div(x, 256n), hh)) : {Nat.add(Nat.add(255n, Nat.mul(_, C.shift(8n, one))), 1n) == C.shift(16n, one) : Nat}
95  %Equal.sym(Nat, 255n, Nat.sub(C.shift(8n, one), 1n), Equal.sym(Nat, Nat.sub(C.shift(8n, one), 1n), 255n, e255(one, h1))) : {Nat.add(Nat.add(_, Nat.mul(255n, C.shift(8n, one))), 1n) == C.shift(16n, one) : Nat}
96  %Equal.sym(Nat, 255n, Nat.sub(C.shift(8n, one), 1n), Equal.sym(Nat, Nat.sub(C.shift(8n, one), 1n), 255n, e255(one, h1))) : {Nat.add(Nat.add(Nat.sub(C.shift(8n, one), 1n), Nat.mul(_, C.shift(8n, one))), 1n) == C.shift(16n, one) : Nat}
97  %Equal.sym(Nat, Nat.add(Nat.add(Nat.sub(C.shift(8n, one), 1n), Nat.mul(Nat.sub(C.shift(8n, one), 1n), C.shift(8n, one))), 1n), Nat.mul(C.shift(8n, one), C.shift(8n, one)), digit_max(C.shift(8n, one), bb_pos(one, h1))) : {_ == C.shift(16n, one) : Nat}
98  bb_sq(one, h1)
99
100def comp1_o(+one: Nat, +h1: {one == 1n : Nat}, +x: Nat, +hx: {Nat.is_lt(x, C.shift(16n, one)) == True{} : Bool}) -> {Nat.add(Nat.add(L.comp1(x), x), one) == C.shift(16n, one) : Nat}:
101  %Equal.sym(Nat, one, 1n, h1) : {Nat.add(Nat.add(L.comp1(x), x), _) == C.shift(16n, one) : Nat}
102  comp1_v(one, h1, x, hx)
103
104# comp(x) + x + 1 = 2^(16 n) for n limbs below 2^16
105def comp_v(+one: Nat, +h1: {one == 1n : Nat}, n: Nat, xs: List<&2, Nat>, +h: {FS.limbs16(one, n, xs) == True{} : Bool}) -> {Nat.add(Nat.add(LV.ev(L.comp(xs)), LV.ev(xs)), one) == LV.pos(n, one) : Nat}:
106  match n xs:
107    case 0n Nil{}:
108      {==}
109    case 0n x <> t:
110      Empty.absurd({Nat.add(Nat.add(LV.ev(L.comp(x <> t)), LV.ev(x <> t)), one) == LV.pos(0n, one) : Nat}, Lg.false_true(h))
111    case 1n+k Nil{}:
112      Empty.absurd({Nat.add(Nat.add(LV.ev(L.comp([])), LV.ev([])), one) == LV.pos(1n+k, one) : Nat}, Lg.false_true(h))
113    case 1n+ +k +x <> +t:
114      +hx = Lg.and_left(Nat.is_lt(x, C.shift(16n, one)), FS.limbs16(one, k, t), h)
115      +ht = Lg.and_right(Nat.is_lt(x, C.shift(16n, one)), FS.limbs16(one, k, t), h)
116      %Equal.sym(Nat, LV.pos(k, one), Nat.add(Nat.add(LV.ev(L.comp(t)), LV.ev(t)), one), Equal.sym(Nat, Nat.add(Nat.add(LV.ev(L.comp(t)), LV.ev(t)), one), LV.pos(k, one), comp_v(one, h1, k, t, ht))) : {Nat.add(Nat.add(Nat.add(L.comp1(x), C.shift(16n, LV.ev(L.comp(t)))), Nat.add(x, C.shift(16n, LV.ev(t)))), one) == C.shift(16n, _) : Nat}
117      %Equal.sym(Nat, Nat.add(x, C.shift(16n, LV.ev(t))), Nat.add(C.shift(16n, LV.ev(t)), x), NA.add_comm(x, C.shift(16n, LV.ev(t)))) : {Nat.add(Nat.add(Nat.add(L.comp1(x), C.shift(16n, LV.ev(L.comp(t)))), _), one) == C.shift(16n, Nat.add(Nat.add(LV.ev(L.comp(t)), LV.ev(t)), one)) : Nat}
118      %Equal.sym(Nat, Nat.add(Nat.add(L.comp1(x), C.shift(16n, LV.ev(L.comp(t)))), Nat.add(C.shift(16n, LV.ev(t)), x)), Nat.add(L.comp1(x), Nat.add(C.shift(16n, LV.ev(L.comp(t))), Nat.add(C.shift(16n, LV.ev(t)), x))), NA.add_assoc(L.comp1(x), C.shift(16n, LV.ev(L.comp(t))), Nat.add(C.shift(16n, LV.ev(t)), x))) : {Nat.add(_, one) == C.shift(16n, Nat.add(Nat.add(LV.ev(L.comp(t)), LV.ev(t)), one)) : Nat}
119      %Equal.sym(Nat, Nat.add(Nat.add(L.comp1(x), Nat.add(C.shift(16n, LV.ev(L.comp(t))), Nat.add(C.shift(16n, LV.ev(t)), x))), one), Nat.add(L.comp1(x), Nat.add(Nat.add(C.shift(16n, LV.ev(L.comp(t))), Nat.add(C.shift(16n, LV.ev(t)), x)), one)), NA.add_assoc(L.comp1(x), Nat.add(C.shift(16n, LV.ev(L.comp(t))), Nat.add(C.shift(16n, LV.ev(t)), x)), one)) : {_ == C.shift(16n, Nat.add(Nat.add(LV.ev(L.comp(t)), LV.ev(t)), one)) : Nat}
120      %Equal.sym(Nat, Nat.add(Nat.add(C.shift(16n, LV.ev(L.comp(t))), Nat.add(C.shift(16n, LV.ev(t)), x)), one), Nat.add(C.shift(16n, LV.ev(L.comp(t))), Nat.add(Nat.add(C.shift(16n, LV.ev(t)), x), one)), NA.add_assoc(C.shift(16n, LV.ev(L.comp(t))), Nat.add(C.shift(16n, LV.ev(t)), x), one)) : {Nat.add(L.comp1(x), _) == C.shift(16n, Nat.add(Nat.add(LV.ev(L.comp(t)), LV.ev(t)), one)) : Nat}
121      %Equal.sym(Nat, Nat.add(Nat.add(C.shift(16n, LV.ev(t)), x), one), Nat.add(C.shift(16n, LV.ev(t)), Nat.add(x, one)), NA.add_assoc(C.shift(16n, LV.ev(t)), x, one)) : {Nat.add(L.comp1(x), Nat.add(C.shift(16n, LV.ev(L.comp(t))), _)) == C.shift(16n, Nat.add(Nat.add(LV.ev(L.comp(t)), LV.ev(t)), one)) : Nat}
122      %Equal.sym(Nat, Nat.add(x, one), Nat.add(one, x), NA.add_comm(x, one)) : {Nat.add(L.comp1(x), Nat.add(C.shift(16n, LV.ev(L.comp(t))), Nat.add(C.shift(16n, LV.ev(t)), _))) == C.shift(16n, Nat.add(Nat.add(LV.ev(L.comp(t)), LV.ev(t)), one)) : Nat}
123      %Equal.sym(Nat, Nat.add(Nat.add(LV.ev(L.comp(t)), LV.ev(t)), one), Nat.add(LV.ev(L.comp(t)), Nat.add(LV.ev(t), one)), NA.add_assoc(LV.ev(L.comp(t)), LV.ev(t), one)) : {Nat.add(L.comp1(x), Nat.add(C.shift(16n, LV.ev(L.comp(t))), Nat.add(C.shift(16n, LV.ev(t)), Nat.add(one, x)))) == C.shift(16n, _) : Nat}
124      %Equal.sym(Nat, C.shift(16n, Nat.add(LV.ev(L.comp(t)), Nat.add(LV.ev(t), one))), Nat.add(C.shift(16n, LV.ev(L.comp(t))), C.shift(16n, Nat.add(LV.ev(t), one))), WW.shift_add(16n, LV.ev(L.comp(t)), Nat.add(LV.ev(t), one))) : {Nat.add(L.comp1(x), Nat.add(C.shift(16n, LV.ev(L.comp(t))), Nat.add(C.shift(16n, LV.ev(t)), Nat.add(one, x)))) == _ : Nat}
125      %Equal.sym(Nat, C.shift(16n, Nat.add(LV.ev(t), one)), Nat.add(C.shift(16n, LV.ev(t)), C.shift(16n, one)), WW.shift_add(16n, LV.ev(t), one)) : {Nat.add(L.comp1(x), Nat.add(C.shift(16n, LV.ev(L.comp(t))), Nat.add(C.shift(16n, LV.ev(t)), Nat.add(one, x)))) == Nat.add(C.shift(16n, LV.ev(L.comp(t))), _) : Nat}
126      %Equal.sym(Nat, C.shift(16n, one), Nat.add(Nat.add(L.comp1(x), x), one), Equal.sym(Nat, Nat.add(Nat.add(L.comp1(x), x), one), C.shift(16n, one), comp1_o(one, h1, x, hx))) : {Nat.add(L.comp1(x), Nat.add(C.shift(16n, LV.ev(L.comp(t))), Nat.add(C.shift(16n, LV.ev(t)), Nat.add(one, x)))) == Nat.add(C.shift(16n, LV.ev(L.comp(t))), Nat.add(C.shift(16n, LV.ev(t)), _)) : Nat}
127      %Equal.sym(Nat, Nat.add(Nat.add(L.comp1(x), x), one), Nat.add(L.comp1(x), Nat.add(x, one)), NA.add_assoc(L.comp1(x), x, one)) : {Nat.add(L.comp1(x), Nat.add(C.shift(16n, LV.ev(L.comp(t))), Nat.add(C.shift(16n, LV.ev(t)), Nat.add(one, x)))) == Nat.add(C.shift(16n, LV.ev(L.comp(t))), Nat.add(C.shift(16n, LV.ev(t)), _)) : Nat}
128      %Equal.sym(Nat, Nat.add(x, one), Nat.add(one, x), NA.add_comm(x, one)) : {Nat.add(L.comp1(x), Nat.add(C.shift(16n, LV.ev(L.comp(t))), Nat.add(C.shift(16n, LV.ev(t)), Nat.add(one, x)))) == Nat.add(C.shift(16n, LV.ev(L.comp(t))), Nat.add(C.shift(16n, LV.ev(t)), Nat.add(L.comp1(x), _))) : Nat}
129      %Equal.sym(Nat, Nat.add(C.shift(16n, LV.ev(t)), Nat.add(L.comp1(x), Nat.add(one, x))), Nat.add(L.comp1(x), Nat.add(C.shift(16n, LV.ev(t)), Nat.add(one, x))), NA.add_swap(C.shift(16n, LV.ev(t)), L.comp1(x), Nat.add(one, x))) : {Nat.add(L.comp1(x), Nat.add(C.shift(16n, LV.ev(L.comp(t))), Nat.add(C.shift(16n, LV.ev(t)), Nat.add(one, x)))) == Nat.add(C.shift(16n, LV.ev(L.comp(t))), _) : Nat}
130      %Equal.sym(Nat, Nat.add(C.shift(16n, LV.ev(L.comp(t))), Nat.add(L.comp1(x), Nat.add(C.shift(16n, LV.ev(t)), Nat.add(one, x)))), Nat.add(L.comp1(x), Nat.add(C.shift(16n, LV.ev(L.comp(t))), Nat.add(C.shift(16n, LV.ev(t)), Nat.add(one, x)))), NA.add_swap(C.shift(16n, LV.ev(L.comp(t))), L.comp1(x), Nat.add(C.shift(16n, LV.ev(t)), Nat.add(one, x)))) : {Nat.add(L.comp1(x), Nat.add(C.shift(16n, LV.ev(L.comp(t))), Nat.add(C.shift(16n, LV.ev(t)), Nat.add(one, x)))) == _ : Nat}
131      {==}
132
133# ---- neg_raw(c, b) + b = m ----
134
135# b + c as 16 limbs, when b + c < 2^256
136def bc_limbs(+one: Nat, +h1: {one == 1n : Nat}, +c: List<&2, Nat>, +b: List<&2, Nat>) -> {FS.limbs16(one, 16n, L.norm16(L.add(b, c))) == True{} : Bool}:
137  B.carry_limbs(one, h1, 32n, 16n, L.add(b, c), 0n, {==})
138
139def bc_v(+one: Nat, +h1: {one == 1n : Nat}, +c: List<&2, Nat>, +b: List<&2, Nat>, +hbc: {Nat.is_lt(Nat.add(LV.ev(b), LV.ev(c)), C.shift(256n, one)) == True{} : Bool}) -> {LV.ev(L.norm16(L.add(b, c))) == Nat.add(LV.ev(b), LV.ev(c)) : Nat}:
140  +x = L.carry(32n, L.add(b, c), 0n)
141  +ex = Equal.trans(Nat, LV.ev(x), LV.ev(L.add(b, c)), Nat.add(LV.ev(b), LV.ev(c)), LV.carry_v(32n, L.add(b, c), 0n), LV.add_v(b, c))
142  +hx = I.lt_subst_l(Nat.add(LV.ev(b), LV.ev(c)), LV.ev(x), C.shift(256n, one), Equal.sym(Nat, LV.ev(x), Nat.add(LV.ev(b), LV.ev(c)), ex), hbc)
143  %Equal.sym(Nat, LV.ev(L.take(16n, L.carry(32n, L.add(b, c), 0n))), LV.ev(L.carry(32n, L.add(b, c), 0n)), R.take_small(one, h1, L.carry(32n, L.add(b, c), 0n), hx)) : {_ == Nat.add(LV.ev(b), LV.ev(c)) : Nat}
144  %Equal.sym(Nat, LV.ev(L.carry(32n, L.add(b, c), 0n)), Nat.add(LV.ev(b), LV.ev(c)), ex) : {_ == Nat.add(LV.ev(b), LV.ev(c)) : Nat}
145  {==}
146
147# neg_raw(c, b) + b + c = 2^256
148def neg_t(+one: Nat, +h1: {one == 1n : Nat}, +c: List<&2, Nat>, +b: List<&2, Nat>, +hbc: {Nat.is_lt(Nat.add(LV.ev(b), LV.ev(c)), C.shift(256n, one)) == True{} : Bool}) -> {Nat.add(LV.ev(L.neg_raw(c, b)), Nat.add(LV.ev(b), LV.ev(c))) == C.shift(256n, one) : Nat}:
149  %Equal.sym(Nat, LV.ev(L.add(L.comp(L.norm16(L.add(b, c))), [1n])), Nat.add(LV.ev(L.comp(L.norm16(L.add(b, c)))), LV.ev([1n])), LV.add_v(L.comp(L.norm16(L.add(b, c))), [1n])) : {Nat.add(_, Nat.add(LV.ev(b), LV.ev(c))) == C.shift(256n, one) : Nat}
150  %Equal.sym(Nat, Nat.add(LV.ev(b), LV.ev(c)), LV.ev(L.norm16(L.add(b, c))), Equal.sym(Nat, LV.ev(L.norm16(L.add(b, c))), Nat.add(LV.ev(b), LV.ev(c)), bc_v(one, h1, c, b, hbc))) : {Nat.add(Nat.add(LV.ev(L.comp(L.norm16(L.add(b, c)))), LV.ev([1n])), _) == C.shift(256n, one) : Nat}
151  %Equal.sym(Nat, C.shift(256n, one), LV.pos(16n, one), Equal.sym(Nat, LV.pos(16n, one), C.shift(256n, one), B.pos16(one))) : {Nat.add(Nat.add(LV.ev(L.comp(L.norm16(L.add(b, c)))), LV.ev([1n])), LV.ev(L.norm16(L.add(b, c)))) == _ : Nat}
152  %Equal.sym(Nat, LV.pos(16n, one), Nat.add(Nat.add(LV.ev(L.comp(L.norm16(L.add(b, c)))), LV.ev(L.norm16(L.add(b, c)))), one), Equal.sym(Nat, Nat.add(Nat.add(LV.ev(L.comp(L.norm16(L.add(b, c)))), LV.ev(L.norm16(L.add(b, c)))), one), LV.pos(16n, one), comp_v(one, h1, 16n, L.norm16(L.add(b, c)), bc_limbs(one, h1, c, b)))) : {Nat.add(Nat.add(LV.ev(L.comp(L.norm16(L.add(b, c)))), LV.ev([1n])), LV.ev(L.norm16(L.add(b, c)))) == _ : Nat}
153  %Equal.sym(Nat, one, 1n, h1) : {Nat.add(Nat.add(LV.ev(L.comp(L.norm16(L.add(b, c)))), LV.ev([1n])), LV.ev(L.norm16(L.add(b, c)))) == Nat.add(Nat.add(LV.ev(L.comp(L.norm16(L.add(b, c)))), LV.ev(L.norm16(L.add(b, c)))), _) : Nat}
154  %Equal.sym(Nat, C.shift(16n, 0n), 0n, WW.shift_zero(16n)) : {Nat.add(Nat.add(LV.ev(L.comp(L.norm16(L.add(b, c)))), Nat.add(1n, _)), LV.ev(L.norm16(L.add(b, c)))) == Nat.add(Nat.add(LV.ev(L.comp(L.norm16(L.add(b, c)))), LV.ev(L.norm16(L.add(b, c)))), 1n) : Nat}
155  %Equal.sym(Nat, Nat.add(1n, 0n), 1n, {==}) : {Nat.add(Nat.add(LV.ev(L.comp(L.norm16(L.add(b, c)))), _), LV.ev(L.norm16(L.add(b, c)))) == Nat.add(Nat.add(LV.ev(L.comp(L.norm16(L.add(b, c)))), LV.ev(L.norm16(L.add(b, c)))), 1n) : Nat}
156  %Equal.sym(Nat, Nat.add(Nat.add(LV.ev(L.comp(L.norm16(L.add(b, c)))), 1n), LV.ev(L.norm16(L.add(b, c)))), Nat.add(LV.ev(L.comp(L.norm16(L.add(b, c)))), Nat.add(1n, LV.ev(L.norm16(L.add(b, c))))), NA.add_assoc(LV.ev(L.comp(L.norm16(L.add(b, c)))), 1n, LV.ev(L.norm16(L.add(b, c))))) : {_ == Nat.add(Nat.add(LV.ev(L.comp(L.norm16(L.add(b, c)))), LV.ev(L.norm16(L.add(b, c)))), 1n) : Nat}
157  %Equal.sym(Nat, Nat.add(1n, LV.ev(L.norm16(L.add(b, c)))), Nat.add(LV.ev(L.norm16(L.add(b, c))), 1n), NA.add_comm(1n, LV.ev(L.norm16(L.add(b, c))))) : {Nat.add(LV.ev(L.comp(L.norm16(L.add(b, c)))), _) == Nat.add(Nat.add(LV.ev(L.comp(L.norm16(L.add(b, c)))), LV.ev(L.norm16(L.add(b, c)))), 1n) : Nat}
158  %Equal.sym(Nat, Nat.add(Nat.add(LV.ev(L.comp(L.norm16(L.add(b, c)))), LV.ev(L.norm16(L.add(b, c)))), 1n), Nat.add(LV.ev(L.comp(L.norm16(L.add(b, c)))), Nat.add(LV.ev(L.norm16(L.add(b, c))), 1n)), NA.add_assoc(LV.ev(L.comp(L.norm16(L.add(b, c)))), LV.ev(L.norm16(L.add(b, c))), 1n)) : {Nat.add(LV.ev(L.comp(L.norm16(L.add(b, c)))), Nat.add(LV.ev(L.norm16(L.add(b, c))), 1n)) == _ : Nat}
159  {==}
160
161# neg_raw(c, b) + b = m, for b < m = 2^256 - c
162def neg_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}, +b: List<&2, Nat>, +hb: {Nat.is_lt(LV.ev(b), 1n+mp) == True{} : Bool}) -> {Nat.add(LV.ev(L.neg_raw(c, b)), LV.ev(b)) == 1n+mp : Nat}:
163  +nb = LV.ev(L.neg_raw(c, b))
164  +bv = LV.ev(b)
165  +cv = LV.ev(c)
166  +hbc = I.lt_subst_r(Nat.add(bv, cv), Nat.add(1n+mp, cv), C.shift(256n, one), hm, N.lt_add_r2(bv, 1n+mp, cv, hb))
167  +e1 = Equal.trans(Nat, Nat.add(Nat.add(nb, bv), cv), Nat.add(nb, Nat.add(bv, cv)), Nat.add(1n+mp, cv), NA.add_assoc(nb, bv, cv), Equal.trans(Nat, Nat.add(nb, Nat.add(bv, cv)), C.shift(256n, one), Nat.add(1n+mp, cv), neg_t(one, h1, c, b, hbc), Equal.sym(Nat, Nat.add(1n+mp, cv), C.shift(256n, one), hm)))
168  NR.add_cancel(cv, Nat.add(nb, bv), 1n+mp, Equal.trans(Nat, Nat.add(cv, Nat.add(nb, bv)), Nat.add(Nat.add(nb, bv), cv), Nat.add(cv, 1n+mp), NA.add_comm(cv, Nat.add(nb, bv)), Equal.trans(Nat, Nat.add(Nat.add(nb, bv), cv), Nat.add(1n+mp, cv), Nat.add(cv, 1n+mp), e1, NA.add_comm(1n+mp, cv))))
169
170def neg_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}, +b: List<&2, Nat>, +hb: {Nat.is_lt(LV.ev(b), 1n+mp) == True{} : Bool}) -> {Nat.add(LV.ev(L.neg_raw(c, b)), LV.ev(b)) == 1n+mp : Nat}:
171  neg_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), b, hb)
172
173# a + (m - b) = (a + m) - b, for b < m
174def sub_mod(+mp: Nat, +a: Nat, +b: Nat, +nb: Nat, +hlt: {Nat.is_lt(b, 1n+mp) == True{} : Bool}, +hn: {Nat.add(nb, b) == 1n+mp : Nat}) -> {Nat.mod(Nat.add(a, nb), 1n+mp) == Nat.mod(Nat.sub(Nat.add(a, 1n+mp), Nat.mod(b, 1n+mp)), 1n+mp) : Nat}:
175  %Equal.sym(Nat, Nat.mod(b, 1n+mp), b, NR.mod_of(0n, mp, b, hlt)) : {Nat.mod(Nat.add(a, nb), 1n+mp) == Nat.mod(Nat.sub(Nat.add(a, 1n+mp), _), 1n+mp) : Nat}
176  %Equal.sym(Nat, 1n+mp, Nat.add(nb, b), Equal.sym(Nat, Nat.add(nb, b), 1n+mp, hn)) : {Nat.mod(Nat.add(a, nb), 1n+mp) == Nat.mod(Nat.sub(Nat.add(a, _), b), 1n+mp) : Nat}
177  %Equal.sym(Nat, Nat.add(a, Nat.add(nb, b)), Nat.add(Nat.add(a, nb), b), Equal.sym(Nat, Nat.add(Nat.add(a, nb), b), Nat.add(a, Nat.add(nb, b)), NA.add_assoc(a, nb, b))) : {Nat.mod(Nat.add(a, nb), 1n+mp) == Nat.mod(Nat.sub(_, b), 1n+mp) : Nat}
178  %Equal.sym(Nat, Nat.add(Nat.add(a, nb), b), Nat.add(b, Nat.add(a, nb)), NA.add_comm(Nat.add(a, nb), b)) : {Nat.mod(Nat.add(a, nb), 1n+mp) == Nat.mod(Nat.sub(_, b), 1n+mp) : Nat}
179  %Equal.sym(Nat, Nat.sub(Nat.add(b, Nat.add(a, nb)), b), Nat.add(a, nb), N.add_sub_cancel(b, Nat.add(a, nb))) : {Nat.mod(Nat.add(a, nb), 1n+mp) == Nat.mod(_, 1n+mp) : Nat}
180  {==}