1 # GENERATED by tools/generators/rw.py from ../../../tools/generators/secp256k1_hand/scalarops.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 ../../../src/crypto/secp256k1/scalar.bend as S 7 import ../../lib/nat.bend as N 8 import ../../lib/logic.bend as Lg 9 import ../../lib/arith.bend as AR 10 import ../../lib/lemmas/proofs/nat_algebra.bend as NA 11 import ../../math/natural/arith.bend as NR 12 import ./limbs.bend as LV 13 import ./fprot.bend as FR 14 import ./ineq.bend as I 15 import ./bounds.bend as B 16 import ./reducek.bend as RK 17 import ./consts.bend as K 18 import ./negate.bend as NG 19 import ./listops.bend as LO 20 21 # Z/nZ of src/crypto/secp256k1/scalar.bend against spec/crypto/secp256k1/field.bend: 22 # on reduced inputs (16 limbs below 2^16, value below n) every operation 23 # returns a reduced scalar whose value is the specified one, exactly. 24 25 # ---- sizes ---- 26 27 def tt_lt(+one: Nat, +h1: {one == 1n : Nat}, +x: List<&2, Nat>, +h: {FS.limbs16(one, 16n, x) == True{} : Bool}) -> {Nat.is_lt(LV.ev(x), C.shift(256n, one)) == True{} : Bool}: 28 I.lt_subst_r(LV.ev(x), LV.pos(16n, one), C.shift(256n, one), B.pos16(one), B.limbs_lt(one, h1, 16n, x, h)) 29 30 def three_le(+one: Nat, +h1: {one == 1n : Nat}) -> {Nat.is_le(3n, C.shift(256n, one)) == True{} : Bool}: 31 K.small_le(one, h1, 256n, 3n, {==}) 32 33 # below 3 2^256 is below 2^512 34 def lt3(+one: Nat, +h1: {one == 1n : Nat}, +x: Nat, +hx: {Nat.is_lt(x, Nat.add(C.shift(256n, one), Nat.add(C.shift(256n, one), C.shift(256n, one)))) == True{} : Bool}) -> {Nat.is_lt(x, Nat.mul(C.shift(256n, one), C.shift(256n, one))) == True{} : Bool}: 35 +t = C.shift(256n, one) 36 +e3 = Equal.trans(Nat, Nat.add(t, Nat.add(t, t)), Nat.add(t, Nat.add(t, Nat.add(t, 0n))), Nat.mul(3n, t), Equal.cong(Nat, Nat, z => Nat.add(t, Nat.add(t, z)), t, Nat.add(t, 0n), Equal.sym(Nat, Nat.add(t, 0n), t, NA.add_zero(t))), {==}) 37 N.lt_le_trans(x, Nat.mul(3n, t), Nat.mul(t, t), I.lt_subst_r(x, Nat.add(t, Nat.add(t, t)), Nat.mul(3n, t), e3, hx), AR.mul_le(3n, t, t, three_le(one, h1))) 38 39 def sum_lt(+one: Nat, +h1: {one == 1n : Nat}, +a: Nat, +b: Nat, +ha: {Nat.is_lt(a, C.shift(256n, one)) == True{} : Bool}, +hb: {Nat.is_lt(b, C.shift(256n, one)) == True{} : Bool}) -> {Nat.is_lt(Nat.add(a, b), Nat.mul(C.shift(256n, one), C.shift(256n, one))) == True{} : Bool}: 40 +t = C.shift(256n, one) 41 lt3(one, h1, Nat.add(a, b), I.lt_le_add(a, b, t, Nat.add(t, t), ha, N.le_trans(b, t, Nat.add(t, t), N.lt_le(b, t, hb), N.le_add_right(t, t)))) 42 43 def mul_lt(+a: Nat, +b: Nat, +t: Nat, +ha: {Nat.is_lt(a, t) == True{} : Bool}, +hb: {Nat.is_lt(b, t) == True{} : Bool}) -> {Nat.is_lt(Nat.mul(a, b), Nat.mul(t, t)) == True{} : Bool}: 44 match t: 45 case 0n: 46 Empty.absurd({Nat.is_lt(Nat.mul(a, b), Nat.mul(0n, 0n)) == True{} : Bool}, N.lt_zero_absurd(a, ha)) 47 case 1n+ +tp: 48 +s1 = I.le_mul2(a, b, tp, 1n+tp, N.lt_succ_le(a, tp, ha), N.lt_le(b, 1n+tp, hb)) 49 +mm = Nat.mul(tp, 1n+tp) 50 +s2 = I.lt_subst_r(mm, Nat.add(mm, 1n+tp), Nat.add(1n+tp, mm), NA.add_comm(mm, 1n+tp), I.lt_add_pos(mm, 1n+tp, {==})) 51 N.le_lt_trans(Nat.mul(a, b), mm, Nat.add(1n+tp, mm), s1, s2) 52 53 # ---- the reduction mod p ---- 54 55 def red_e(+one: Nat, +h1: {one == 1n : Nat}, +xs: List<&2, Nat>, +hx: {Nat.is_lt(LV.ev(xs), Nat.mul(C.shift(256n, one), C.shift(256n, one))) == True{} : Bool}) -> {LV.ev(S.reduce_u(xs)) == Nat.mod(LV.ev(xs), 1n+K.np(one)) : Nat}: 56 RK.reduce4_vv(one, h1, K.np(one), S.c(), K.hm_n(one, h1), K.cn_cc(one, h1), K.cn_hb1(one, h1), K.cn_hb2(one, h1), xs, hx) 57 58 def red_l(+one: Nat, +h1: {one == 1n : Nat}, +xs: List<&2, Nat>, +hx: {Nat.is_lt(LV.ev(xs), Nat.mul(C.shift(256n, one), C.shift(256n, one))) == True{} : Bool}) -> {FS.limbs16(one, 16n, S.reduce_u(xs)) == True{} : Bool}: 59 RK.reduce4_lv(one, h1, S.c(), K.cn_cc(one, h1), K.cn_hb1(one, h1), K.cn_hb2(one, h1), xs, hx) 60 61 # the reduced value below p, in the specification's terms 62 def red_r(+one: Nat, +h1: {one == 1n : Nat}, +xs: List<&2, Nat>, +hx: {Nat.is_lt(LV.ev(xs), Nat.mul(C.shift(256n, one), C.shift(256n, one))) == True{} : Bool}) -> {FS.reduced(one, FS.order(one), S.reduce_u(xs)) == True{} : Bool}: 63 +lt = I.lt_subst_l(Nat.mod(LV.ev(xs), 1n+K.np(one)), LV.ev(S.reduce_u(xs)), 1n+K.np(one), Equal.sym(Nat, LV.ev(S.reduce_u(xs)), Nat.mod(LV.ev(xs), 1n+K.np(one)), red_e(one, h1, xs, hx)), NR.dm_lt(K.np(one), LV.ev(xs))) 64 +lt2 = I.lt_subst_l(LV.ev(S.reduce_u(xs)), FS.value(one, S.reduce_u(xs)), 1n+K.np(one), Equal.sym(Nat, FS.value(one, S.reduce_u(xs)), LV.ev(S.reduce_u(xs)), LV.ev_value(one, h1, S.reduce_u(xs))), lt) 65 +lt3 = I.lt_subst_r(FS.value(one, S.reduce_u(xs)), 1n+K.np(one), FS.order(one), Equal.sym(Nat, FS.order(one), 1n+K.np(one), K.order_eq(one, h1)), lt2) 66 Lg.and_intro(FS.limbs16(one, 16n, S.reduce_u(xs)), Nat.is_lt(FS.value(one, S.reduce_u(xs)), FS.order(one)), red_l(one, h1, xs, hx), lt3) 67 68 def red_v(+one: Nat, +h1: {one == 1n : Nat}, +xs: List<&2, Nat>, +hx: {Nat.is_lt(LV.ev(xs), Nat.mul(C.shift(256n, one), C.shift(256n, one))) == True{} : Bool}) -> {FS.value(one, S.reduce_u(xs)) == Nat.mod(LV.ev(xs), FS.order(one)) : Nat}: 69 %Equal.sym(Nat, FS.value(one, S.reduce_u(xs)), LV.ev(S.reduce_u(xs)), LV.ev_value(one, h1, S.reduce_u(xs))) : {_ == Nat.mod(LV.ev(xs), FS.order(one)) : Nat} 70 %Equal.sym(Nat, LV.ev(S.reduce_u(xs)), Nat.mod(LV.ev(xs), 1n+K.np(one)), red_e(one, h1, xs, hx)) : {_ == Nat.mod(LV.ev(xs), FS.order(one)) : Nat} 71 %Equal.sym(Nat, 1n+K.np(one), FS.order(one), Equal.sym(Nat, FS.order(one), 1n+K.np(one), K.order_eq(one, h1))) : {Nat.mod(LV.ev(xs), _) == Nat.mod(LV.ev(xs), FS.order(one)) : Nat} 72 {==} 73 74 # ---- reduced inputs ---- 75 76 def r16(+one: Nat, +x: List<&2, Nat>, +h: {FS.reduced(one, FS.order(one), x) == True{} : Bool}) -> {FS.limbs16(one, 16n, x) == True{} : Bool}: 77 Lg.and_left(FS.limbs16(one, 16n, x), Nat.is_lt(FS.value(one, x), FS.order(one)), h) 78 79 def rlt(+one: Nat, +h1: {one == 1n : Nat}, +x: List<&2, Nat>, +h: {FS.reduced(one, FS.order(one), x) == True{} : Bool}) -> {Nat.is_lt(LV.ev(x), 1n+K.np(one)) == True{} : Bool}: 80 +l = Lg.and_right(FS.limbs16(one, 16n, x), Nat.is_lt(FS.value(one, x), FS.order(one)), h) 81 +l2 = I.lt_subst_l(FS.value(one, x), LV.ev(x), FS.order(one), LV.ev_value(one, h1, x), l) 82 I.lt_subst_r(LV.ev(x), FS.order(one), 1n+K.np(one), K.order_eq(one, h1), l2) 83 84 def rtt(+one: Nat, +h1: {one == 1n : Nat}, +x: List<&2, Nat>, +h: {FS.reduced(one, FS.order(one), x) == True{} : Bool}) -> {Nat.is_lt(LV.ev(x), C.shift(256n, one)) == True{} : Bool}: 85 tt_lt(one, h1, x, r16(one, x, h)) 86 87 # ---- add, mul ---- 88 89 def add_hx(+one: Nat, +h1: {one == 1n : Nat}, +a: List<&2, Nat>, +b: List<&2, Nat>, +ha: {FS.reduced(one, FS.order(one), a) == True{} : Bool}, +hb: {FS.reduced(one, FS.order(one), b) == True{} : Bool}) -> {Nat.is_lt(LV.ev(L.add(a, b)), Nat.mul(C.shift(256n, one), C.shift(256n, one))) == True{} : Bool}: 90 %Equal.sym(Nat, LV.ev(L.add(a, b)), Nat.add(LV.ev(a), LV.ev(b)), LV.add_v(a, b)) : {Nat.is_lt(_, Nat.mul(C.shift(256n, one), C.shift(256n, one))) == True{} : Bool} 91 sum_lt(one, h1, LV.ev(a), LV.ev(b), rtt(one, h1, a, ha), rtt(one, h1, b, hb)) 92 93 def add_v(+one: Nat, +h1: {one == 1n : Nat}, +a: List<&2, Nat>, +b: List<&2, Nat>, +ha: {FS.reduced(one, FS.order(one), a) == True{} : Bool}, +hb: {FS.reduced(one, FS.order(one), b) == True{} : Bool}) -> {FS.value(one, S.add(a, b)) == FS.madd(FS.order(one), FS.value(one, a), FS.value(one, b)) : Nat}: 94 %Equal.sym(List<&2, Nat>, S.add(a, b), S.add_u(a, b), FR.s_add(a, b)) : {FS.value(one, _) == FS.madd(FS.order(one), FS.value(one, a), FS.value(one, b)) : Nat} 95 %Equal.sym(Nat, FS.value(one, S.reduce_u(L.add(a, b))), Nat.mod(LV.ev(L.add(a, b)), FS.order(one)), red_v(one, h1, L.add(a, b), add_hx(one, h1, a, b, ha, hb))) : {_ == Nat.mod(Nat.add(FS.value(one, a), FS.value(one, b)), FS.order(one)) : Nat} 96 %Equal.sym(Nat, LV.ev(L.add(a, b)), Nat.add(LV.ev(a), LV.ev(b)), LV.add_v(a, b)) : {Nat.mod(_, FS.order(one)) == Nat.mod(Nat.add(FS.value(one, a), FS.value(one, b)), FS.order(one)) : Nat} 97 %Equal.sym(Nat, LV.ev(a), FS.value(one, a), Equal.sym(Nat, FS.value(one, a), LV.ev(a), LV.ev_value(one, h1, a))) : {Nat.mod(Nat.add(_, LV.ev(b)), FS.order(one)) == Nat.mod(Nat.add(FS.value(one, a), FS.value(one, b)), FS.order(one)) : Nat} 98 %Equal.sym(Nat, LV.ev(b), FS.value(one, b), Equal.sym(Nat, FS.value(one, b), LV.ev(b), LV.ev_value(one, h1, b))) : {Nat.mod(Nat.add(FS.value(one, a), _), FS.order(one)) == Nat.mod(Nat.add(FS.value(one, a), FS.value(one, b)), FS.order(one)) : Nat} 99 {==} 100 101 def add_r(+one: Nat, +h1: {one == 1n : Nat}, +a: List<&2, Nat>, +b: List<&2, Nat>, +ha: {FS.reduced(one, FS.order(one), a) == True{} : Bool}, +hb: {FS.reduced(one, FS.order(one), b) == True{} : Bool}) -> {FS.reduced(one, FS.order(one), S.add(a, b)) == True{} : Bool}: 102 %Equal.sym(List<&2, Nat>, S.add(a, b), S.add_u(a, b), FR.s_add(a, b)) : {FS.reduced(one, FS.order(one), _) == True{} : Bool} 103 red_r(one, h1, L.add(a, b), add_hx(one, h1, a, b, ha, hb)) 104 105 def mul_hx(+one: Nat, +h1: {one == 1n : Nat}, +a: List<&2, Nat>, +b: List<&2, Nat>, +ha: {FS.reduced(one, FS.order(one), a) == True{} : Bool}, +hb: {FS.reduced(one, FS.order(one), b) == True{} : Bool}) -> {Nat.is_lt(LV.ev(L.conv(a, b)), Nat.mul(C.shift(256n, one), C.shift(256n, one))) == True{} : Bool}: 106 %Equal.sym(Nat, LV.ev(L.conv(a, b)), Nat.mul(LV.ev(a), LV.ev(b)), LV.conv_v(a, b)) : {Nat.is_lt(_, Nat.mul(C.shift(256n, one), C.shift(256n, one))) == True{} : Bool} 107 mul_lt(LV.ev(a), LV.ev(b), C.shift(256n, one), rtt(one, h1, a, ha), rtt(one, h1, b, hb)) 108 109 def mul_v(+one: Nat, +h1: {one == 1n : Nat}, +a: List<&2, Nat>, +b: List<&2, Nat>, +ha: {FS.reduced(one, FS.order(one), a) == True{} : Bool}, +hb: {FS.reduced(one, FS.order(one), b) == True{} : Bool}) -> {FS.value(one, S.mul(a, b)) == FS.mmul(FS.order(one), FS.value(one, a), FS.value(one, b)) : Nat}: 110 %Equal.sym(List<&2, Nat>, S.mul(a, b), S.mul_u(a, b), FR.s_mul(a, b)) : {FS.value(one, _) == FS.mmul(FS.order(one), FS.value(one, a), FS.value(one, b)) : Nat} 111 %Equal.sym(Nat, FS.value(one, S.reduce_u(L.conv(a, b))), Nat.mod(LV.ev(L.conv(a, b)), FS.order(one)), red_v(one, h1, L.conv(a, b), mul_hx(one, h1, a, b, ha, hb))) : {_ == Nat.mod(Nat.mul(FS.value(one, a), FS.value(one, b)), FS.order(one)) : Nat} 112 %Equal.sym(Nat, LV.ev(L.conv(a, b)), Nat.mul(LV.ev(a), LV.ev(b)), LV.conv_v(a, b)) : {Nat.mod(_, FS.order(one)) == Nat.mod(Nat.mul(FS.value(one, a), FS.value(one, b)), FS.order(one)) : Nat} 113 %Equal.sym(Nat, LV.ev(a), FS.value(one, a), Equal.sym(Nat, FS.value(one, a), LV.ev(a), LV.ev_value(one, h1, a))) : {Nat.mod(Nat.mul(_, LV.ev(b)), FS.order(one)) == Nat.mod(Nat.mul(FS.value(one, a), FS.value(one, b)), FS.order(one)) : Nat} 114 %Equal.sym(Nat, LV.ev(b), FS.value(one, b), Equal.sym(Nat, FS.value(one, b), LV.ev(b), LV.ev_value(one, h1, b))) : {Nat.mod(Nat.mul(FS.value(one, a), _), FS.order(one)) == Nat.mod(Nat.mul(FS.value(one, a), FS.value(one, b)), FS.order(one)) : Nat} 115 {==} 116 117 def mul_r(+one: Nat, +h1: {one == 1n : Nat}, +a: List<&2, Nat>, +b: List<&2, Nat>, +ha: {FS.reduced(one, FS.order(one), a) == True{} : Bool}, +hb: {FS.reduced(one, FS.order(one), b) == True{} : Bool}) -> {FS.reduced(one, FS.order(one), S.mul(a, b)) == True{} : Bool}: 118 %Equal.sym(List<&2, Nat>, S.mul(a, b), S.mul_u(a, b), FR.s_mul(a, b)) : {FS.reduced(one, FS.order(one), _) == True{} : Bool} 119 red_r(one, h1, L.conv(a, b), mul_hx(one, h1, a, b, ha, hb)) 120 121 # ---- sub, neg ---- 122 123 def negr_e(+one: Nat, +h1: {one == 1n : Nat}, +b: List<&2, Nat>, +hb: {FS.reduced(one, FS.order(one), b) == True{} : Bool}) -> {Nat.add(LV.ev(L.neg_raw(S.c(), b)), LV.ev(b)) == 1n+K.np(one) : Nat}: 124 NG.neg_vv(one, h1, K.np(one), S.c(), K.hm_n(one, h1), b, rlt(one, h1, b, hb)) 125 126 def negr_le(+one: Nat, +h1: {one == 1n : Nat}, +b: List<&2, Nat>, +hb: {FS.reduced(one, FS.order(one), b) == True{} : Bool}) -> {Nat.is_le(LV.ev(L.neg_raw(S.c(), b)), C.shift(256n, one)) == True{} : Bool}: 127 +m = {1n+K.np(one) : Nat} 128 +nb = LV.ev(L.neg_raw(S.c(), b)) 129 +mt = I.le_subst_r(m, Nat.add(m, FS.cn(one)), C.shift(256n, one), K.hm_n(one, h1), N.le_add_right(m, FS.cn(one))) 130 N.le_trans(nb, m, C.shift(256n, one), I.le_subst_r(nb, Nat.add(nb, LV.ev(b)), m, negr_e(one, h1, b, hb), N.le_add_right(nb, LV.ev(b))), mt) 131 132 def neg_hx(+one: Nat, +h1: {one == 1n : Nat}, +b: List<&2, Nat>, +hb: {FS.reduced(one, FS.order(one), b) == True{} : Bool}) -> {Nat.is_lt(LV.ev(L.neg_raw(S.c(), b)), Nat.mul(C.shift(256n, one), C.shift(256n, one))) == True{} : Bool}: 133 +t = C.shift(256n, one) 134 lt3(one, h1, LV.ev(L.neg_raw(S.c(), b)), N.le_lt_trans(LV.ev(L.neg_raw(S.c(), b)), t, Nat.add(t, Nat.add(t, t)), negr_le(one, h1, b, hb), I.lt_add_pos(t, Nat.add(t, t), N.lt_le_trans(0n, t, Nat.add(t, t), K.shift_pos(one, h1, 256n), N.le_add_right(t, t))))) 135 136 def neg_v(+one: Nat, +h1: {one == 1n : Nat}, +b: List<&2, Nat>, +hb: {FS.reduced(one, FS.order(one), b) == True{} : Bool}) -> {FS.value(one, S.neg(b)) == FS.mneg(FS.order(one), FS.value(one, b)) : Nat}: 137 %Equal.sym(List<&2, Nat>, S.neg(b), S.neg_u(b), FR.s_neg(b)) : {FS.value(one, _) == FS.mneg(FS.order(one), FS.value(one, b)) : Nat} 138 %Equal.sym(Nat, FS.value(one, S.reduce_u(L.neg_raw(S.c(), b))), Nat.mod(LV.ev(L.neg_raw(S.c(), b)), FS.order(one)), red_v(one, h1, L.neg_raw(S.c(), b), neg_hx(one, h1, b, hb))) : {_ == Nat.mod(Nat.sub(Nat.add(0n, FS.order(one)), Nat.mod(FS.value(one, b), FS.order(one))), FS.order(one)) : Nat} 139 %Equal.sym(Nat, FS.value(one, b), LV.ev(b), LV.ev_value(one, h1, b)) : {Nat.mod(LV.ev(L.neg_raw(S.c(), b)), FS.order(one)) == Nat.mod(Nat.sub(Nat.add(0n, FS.order(one)), Nat.mod(_, FS.order(one))), FS.order(one)) : Nat} 140 %Equal.sym(Nat, FS.order(one), 1n+K.np(one), K.order_eq(one, h1)) : {Nat.mod(LV.ev(L.neg_raw(S.c(), b)), _) == Nat.mod(Nat.sub(Nat.add(0n, FS.order(one)), Nat.mod(LV.ev(b), FS.order(one))), FS.order(one)) : Nat} 141 %Equal.sym(Nat, FS.order(one), 1n+K.np(one), K.order_eq(one, h1)) : {Nat.mod(LV.ev(L.neg_raw(S.c(), b)), 1n+K.np(one)) == Nat.mod(Nat.sub(Nat.add(0n, _), Nat.mod(LV.ev(b), FS.order(one))), FS.order(one)) : Nat} 142 %Equal.sym(Nat, FS.order(one), 1n+K.np(one), K.order_eq(one, h1)) : {Nat.mod(LV.ev(L.neg_raw(S.c(), b)), 1n+K.np(one)) == Nat.mod(Nat.sub(Nat.add(0n, 1n+K.np(one)), Nat.mod(LV.ev(b), _)), FS.order(one)) : Nat} 143 %Equal.sym(Nat, FS.order(one), 1n+K.np(one), K.order_eq(one, h1)) : {Nat.mod(LV.ev(L.neg_raw(S.c(), b)), 1n+K.np(one)) == Nat.mod(Nat.sub(Nat.add(0n, 1n+K.np(one)), Nat.mod(LV.ev(b), 1n+K.np(one))), _) : Nat} 144 NG.sub_mod(K.np(one), 0n, LV.ev(b), LV.ev(L.neg_raw(S.c(), b)), rlt(one, h1, b, hb), negr_e(one, h1, b, hb)) 145 146 def neg_r(+one: Nat, +h1: {one == 1n : Nat}, +b: List<&2, Nat>, +hb: {FS.reduced(one, FS.order(one), b) == True{} : Bool}) -> {FS.reduced(one, FS.order(one), S.neg(b)) == True{} : Bool}: 147 %Equal.sym(List<&2, Nat>, S.neg(b), S.neg_u(b), FR.s_neg(b)) : {FS.reduced(one, FS.order(one), _) == True{} : Bool} 148 red_r(one, h1, L.neg_raw(S.c(), b), neg_hx(one, h1, b, hb)) 149 150 # ---- in the limb value ev ---- 151 152 def mul_e(+one: Nat, +h1: {one == 1n : Nat}, +a: List<&2, Nat>, +b: List<&2, Nat>, +ha: {FS.reduced(one, FS.order(one), a) == True{} : Bool}, +hb: {FS.reduced(one, FS.order(one), b) == True{} : Bool}) -> {LV.ev(S.mul(a, b)) == Nat.mod(Nat.mul(LV.ev(a), LV.ev(b)), 1n+K.np(one)) : Nat}: 153 %Equal.sym(List<&2, Nat>, S.mul(a, b), S.mul_u(a, b), FR.s_mul(a, b)) : {LV.ev(_) == Nat.mod(Nat.mul(LV.ev(a), LV.ev(b)), 1n+K.np(one)) : Nat} 154 %Equal.sym(Nat, LV.ev(S.reduce_u(L.conv(a, b))), Nat.mod(LV.ev(L.conv(a, b)), 1n+K.np(one)), red_e(one, h1, L.conv(a, b), mul_hx(one, h1, a, b, ha, hb))) : {_ == Nat.mod(Nat.mul(LV.ev(a), LV.ev(b)), 1n+K.np(one)) : Nat} 155 %Equal.sym(Nat, LV.ev(L.conv(a, b)), Nat.mul(LV.ev(a), LV.ev(b)), LV.conv_v(a, b)) : {Nat.mod(_, 1n+K.np(one)) == Nat.mod(Nat.mul(LV.ev(a), LV.ev(b)), 1n+K.np(one)) : Nat} 156 {==} 157 158 # ---- small constants ---- 159 160 def small_r(+one: Nat, +h1: {one == 1n : Nat}, +k: Nat, +hk: {Nat.is_lt(k, FS.order(one)) == True{} : Bool}) -> {FS.reduced(one, FS.order(one), S.small(k)) == True{} : Bool}: 161 +hk2 = I.lt_subst_r(k, FS.order(one), 1n+K.np(one), K.order_eq(one, h1), hk) 162 +hkt = N.lt_le_trans(k, 1n+K.np(one), C.shift(256n, one), hk2, I.le_subst_r(1n+K.np(one), Nat.add(1n+K.np(one), FS.cn(one)), C.shift(256n, one), K.hm_n(one, h1), N.le_add_right(1n+K.np(one), FS.cn(one)))) 163 +ev = LO.small_v(one, h1, k, hkt) 164 +lt = I.lt_subst_l(k, FS.value(one, S.small(k)), FS.order(one), Equal.sym(Nat, FS.value(one, S.small(k)), k, Equal.trans(Nat, FS.value(one, S.small(k)), LV.ev(S.small(k)), k, LV.ev_value(one, h1, S.small(k)), ev)), hk) 165 Lg.and_intro(FS.limbs16(one, 16n, S.small(k)), Nat.is_lt(FS.value(one, S.small(k)), FS.order(one)), LO.small_l(one, h1, k), lt) 166 167 def small_val(+one: Nat, +h1: {one == 1n : Nat}, +k: Nat, +hk: {Nat.is_lt(k, FS.order(one)) == True{} : Bool}) -> {FS.value(one, S.small(k)) == k : Nat}: 168 +hk2 = I.lt_subst_r(k, FS.order(one), 1n+K.np(one), K.order_eq(one, h1), hk) 169 +hkt = N.lt_le_trans(k, 1n+K.np(one), C.shift(256n, one), hk2, I.le_subst_r(1n+K.np(one), Nat.add(1n+K.np(one), FS.cn(one)), C.shift(256n, one), K.hm_n(one, h1), N.le_add_right(1n+K.np(one), FS.cn(one)))) 170 Equal.trans(Nat, FS.value(one, S.small(k)), LV.ev(S.small(k)), k, LV.ev_value(one, h1, S.small(k)), LO.small_v(one, h1, k, hkt)) 171 172 # m + c = h + h and c <= h: h <= m 173 def le_cancel_r(+x: Nat, +y: Nat, +c: Nat) -> {Nat.is_le(Nat.add(x, c), Nat.add(y, c)) == Nat.is_le(x, y) : Bool}: 174 %Equal.sym(Nat, Nat.add(x, c), Nat.add(c, x), NA.add_comm(x, c)) : {Nat.is_le(_, Nat.add(y, c)) == Nat.is_le(x, y) : Bool} 175 %Equal.sym(Nat, Nat.add(y, c), Nat.add(c, y), NA.add_comm(y, c)) : {Nat.is_le(Nat.add(c, x), _) == Nat.is_le(x, y) : Bool} 176 NR.le_add_cancel(c, x, y) 177 178 # small k < 2^32 is below p 179 def lt_p_half(+h: Nat, +m: Nat, +c: Nat, +e: {Nat.add(m, c) == Nat.add(h, h) : Nat}, +hc: {Nat.is_le(c, h) == True{} : Bool}) -> {Nat.is_le(h, m) == True{} : Bool}: 180 +s1 = N.le_add_left(c, h, h, hc) 181 +s2 = I.le_subst_r(Nat.add(h, c), Nat.add(h, h), Nat.add(m, c), Equal.sym(Nat, Nat.add(m, c), Nat.add(h, h), e), s1) 182 +s3 = Equal.trans(Bool, Nat.is_le(h, m), Nat.is_le(Nat.add(h, c), Nat.add(m, c)), True{}, Equal.sym(Bool, Nat.is_le(Nat.add(h, c), Nat.add(m, c)), Nat.is_le(h, m), le_cancel_r(h, m, c)), s2) 183 s3 184 185 def small_lt_n(+one: Nat, +h1: {one == 1n : Nat}, +k: Nat, +hk: {Nat.is_lt(k, C.shift(10n, 1n)) == True{} : Bool}) -> {Nat.is_lt(k, FS.order(one)) == True{} : Bool}: 186 +hk1 = I.lt_subst_r(k, C.shift(10n, 1n), C.shift(10n, one), Equal.cong(Nat, Nat, z => C.shift(10n, z), 1n, one, Equal.sym(Nat, one, 1n, h1)), hk) 187 +s1 = N.lt_le_trans(k, C.shift(10n, one), C.shift(255n, one), hk1, K.shift_le_k(10n, 255n, one, 245n, {==})) 188 +pp = K.np(one) 189 # 2^255 <= p: p + c = 2^256 = 2^255 + 2^255 and c <= 2^33 <= 2^255 190 +c = FS.cn(one) 191 +e1 = Equal.trans(Nat, Nat.add(1n+pp, c), C.shift(256n, one), Nat.add(C.shift(255n, one), C.shift(255n, one)), K.hm_n(one, h1), Equal.sym(Nat, Nat.add(C.shift(255n, one), C.shift(255n, one)), C.shift(256n, one), K.shift_twice(255n, one))) 192 +ch = N.le_trans(c, C.shift(129n, one), C.shift(255n, one), N.lt_le(c, C.shift(129n, one), K.cn_lt(one, h1)), K.shift_le_k(129n, 255n, one, 126n, {==})) 193 +s2 = lt_p_half(C.shift(255n, one), 1n+pp, c, e1, ch) 194 I.lt_subst_r(k, 1n+pp, FS.order(one), Equal.sym(Nat, FS.order(one), 1n+pp, K.order_eq(one, h1)), N.lt_le_trans(k, C.shift(255n, one), 1n+pp, s1, s2))