1 # GENERATED by tools/generators/rw.py from ../../../tools/generators/secp256k1_hand/rconst.src; edit the .src 2 import Base 3 import ./limbs.bend as LV 4 import ../../../spec/lib/common.bend as C 5 import ../../../spec/crypto/secp256k1/field.bend as FS 6 import ../../../src/crypto/secp256k1/ecdsa.bend as E 7 import ../../lib/nat.bend as N 8 import ../../lib/lemmas/proofs/nat_algebra.bend as NA 9 import ../../math/natural/arith.bend as NR 10 import ../../math/typed/width.bend as WW 11 import ./semiring.bend as SR 12 import ./ineq.bend as I 13 import ./bounds.bend as B2 14 import ./consts.bend as K 15 import ./lits.bend as LT 16 import ./fieldops.bend as FO 17 import ./fieldpow.bend as FP 18 import ./scalarpow.bend as SP 19 20 # The constants of public key recovery (src/crypto/secp256k1/ecdsa.bend 21 # cn_fe, cp_fe) and the arithmetic of x = r + n: c_p < c_n, n < p, and 22 # (r - c_n + c_p) mod p = (r + n) mod p. 23 24 # ---- the constants ---- 25 26 def cn_fe_v(+one: Nat) -> {FS.value(one, E.cn_fe()) == FS.cn(one) : Nat}: 27 %Equal.sym(Nat, FS.digits(one, [12233n, 41331n, 16429n, 24516n, 20663n, 8985n, 17745n, 1n, 0n, 0n, 0n, 0n, 0n, 0n, 0n]), FS.digits(one, [12233n, 41331n, 16429n, 24516n, 20663n, 8985n, 17745n, 1n]), SP.zeros_tail(one)) : {Nat.add(Nat.mul(one, 48831n), C.shift(16n, _)) == Nat.add(Nat.mul(one, 48831n), C.shift(16n, FS.digits(one, [12233n, 41331n, 16429n, 24516n, 20663n, 8985n, 17745n, 1n]))) : Nat} 28 {==} 29 30 def cp_fe_v(+one: Nat) -> {FS.value(one, E.cp_fe()) == FS.cp(one) : Nat}: 31 %Equal.sym(Nat, FS.digits(one, [0n, 0n, 0n, 0n, 0n, 0n, 0n, 0n, 0n, 0n, 0n, 0n, 0n]), 0n, FP.zeros13(one)) : {Nat.add(Nat.mul(one, 977n), C.shift(16n, Nat.add(Nat.mul(one, 0n), C.shift(16n, Nat.add(Nat.mul(one, 1n), C.shift(16n, _)))))) == Nat.add(Nat.mul(one, 977n), C.shift(16n, Nat.add(Nat.mul(one, 0n), C.shift(16n, Nat.add(Nat.mul(one, 1n), C.shift(16n, 0n)))))) : Nat} 32 {==} 33 34 def cn_fe_l(+one: Nat, +h1: {one == 1n : Nat}) -> {FS.limbs16(one, 16n, E.cn_fe()) == True{} : Bool}: 35 LT.lits16(one, h1, 16n, E.cn_fe(), {==}) 36 37 def cp_fe_l(+one: Nat, +h1: {one == 1n : Nat}) -> {FS.limbs16(one, 16n, E.cp_fe()) == True{} : Bool}: 38 LT.lits16(one, h1, 16n, E.cp_fe(), {==}) 39 40 # ---- sizes: c_p <= 2^33 < 2^128 <= c_n < 2^129 <= 2^255 <= p ---- 41 42 def cn_ge(+one: Nat, +h1: {one == 1n : Nat}) -> {Nat.is_le(C.shift(128n, one), FS.cn(one)) == True{} : Bool}: 43 %Equal.sym(Nat, FS.cn(one), Nat.add(FS.digits(one, K.cn8()), LV.pos(8n, one)), K.cn_split(one, h1)) : {Nat.is_le(C.shift(128n, one), _) == True{} : Bool} 44 %Equal.sym(Nat, LV.pos(8n, one), C.shift(128n, one), B2.pos_shift(8n, one)) : {Nat.is_le(C.shift(128n, one), Nat.add(FS.digits(one, K.cn8()), _)) == True{} : Bool} 45 %Equal.sym(Nat, Nat.add(FS.digits(one, K.cn8()), C.shift(128n, one)), Nat.add(C.shift(128n, one), FS.digits(one, K.cn8())), NA.add_comm(FS.digits(one, K.cn8()), C.shift(128n, one))) : {Nat.is_le(C.shift(128n, one), _) == True{} : Bool} 46 N.le_add_right(C.shift(128n, one), FS.digits(one, K.cn8())) 47 48 def cp_lt_cn(+one: Nat, +h1: {one == 1n : Nat}) -> {Nat.is_lt(FS.cp(one), FS.cn(one)) == True{} : Bool}: 49 N.le_lt_trans(FS.cp(one), C.shift(33n, one), FS.cn(one), K.cp_le(one, h1), N.lt_le_trans(C.shift(33n, one), C.shift(128n, one), FS.cn(one), K.shift_lt_k(one, h1, 33n, 128n, 94n, {==}), cn_ge(one, h1))) 50 51 # 2^255 <= p 52 def p_ge(+one: Nat, +h1: {one == 1n : Nat}) -> {Nat.is_le(C.shift(255n, one), 1n+K.pp(one)) == True{} : Bool}: 53 +pp = K.pp(one) 54 +c = FS.cp(one) 55 +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_p(one, h1), Equal.sym(Nat, Nat.add(C.shift(255n, one), C.shift(255n, one)), C.shift(256n, one), K.shift_twice(255n, one))) 56 +ch = N.le_trans(c, C.shift(33n, one), C.shift(255n, one), K.cp_le(one, h1), K.shift_le_k(33n, 255n, one, 222n, {==})) 57 FO.lt_p_half(C.shift(255n, one), 1n+pp, c, e1, ch) 58 59 def cn_lt_p(+one: Nat, +h1: {one == 1n : Nat}) -> {Nat.is_lt(FS.cn(one), 1n+K.pp(one)) == True{} : Bool}: 60 N.lt_le_trans(FS.cn(one), C.shift(255n, one), 1n+K.pp(one), N.lt_le_trans(FS.cn(one), C.shift(129n, one), C.shift(255n, one), K.cn_lt(one, h1), K.shift_le_k(129n, 255n, one, 126n, {==})), p_ge(one, h1)) 61 62 def cp_lt_p(+one: Nat, +h1: {one == 1n : Nat}) -> {Nat.is_lt(FS.cp(one), 1n+K.pp(one)) == True{} : Bool}: 63 N.lt_trans(FS.cp(one), FS.cn(one), 1n+K.pp(one), cp_lt_cn(one, h1), cn_lt_p(one, h1)) 64 65 # p + c_p = n + c_n (= 2^256) 66 def pn_sum(+one: Nat, +h1: {one == 1n : Nat}) -> {Nat.add(1n+K.pp(one), FS.cp(one)) == Nat.add(1n+K.np(one), FS.cn(one)) : Nat}: 67 Equal.trans(Nat, Nat.add(1n+K.pp(one), FS.cp(one)), C.shift(256n, one), Nat.add(1n+K.np(one), FS.cn(one)), K.hm_p(one, h1), Equal.sym(Nat, Nat.add(1n+K.np(one), FS.cn(one)), C.shift(256n, one), K.hm_n(one, h1))) 68 69 # ---- generic arithmetic (P = 1 + pp) ---- 70 71 def le_cancel_l(+c: Nat, +x: Nat, +y: Nat, +h: {Nat.is_le(Nat.add(c, x), Nat.add(c, y)) == True{} : Bool}) -> {Nat.is_le(x, y) == True{} : Bool}: 72 Equal.trans(Bool, Nat.is_le(x, y), Nat.is_le(Nat.add(c, x), Nat.add(c, y)), True{}, Equal.sym(Bool, Nat.is_le(Nat.add(c, x), Nat.add(c, y)), Nat.is_le(x, y), NR.le_add_cancel(c, x, y)), h) 73 74 def sc(+b: Nat, +c: Nat) -> {1n+Nat.add(b, c) == Nat.add(c, 1n+b) : Nat}: 75 %Equal.sym(Nat, 1n+Nat.add(b, c), Nat.add(Nat.add(b, c), 1n), SR.succ_add(1n, Nat.add(b, c))) : {_ == Nat.add(c, 1n+b) : Nat} 76 %Equal.sym(Nat, Nat.add(Nat.add(b, c), 1n), Nat.add(b, Nat.add(c, 1n)), NA.add_assoc(b, c, 1n)) : {_ == Nat.add(c, 1n+b) : Nat} 77 %Equal.sym(Nat, 1n+b, Nat.add(b, 1n), SR.succ_add(1n, b)) : {Nat.add(b, Nat.add(c, 1n)) == Nat.add(c, _) : Nat} 78 %Equal.sym(Nat, Nat.add(c, Nat.add(b, 1n)), Nat.add(b, Nat.add(c, 1n)), NA.add_swap(c, b, 1n)) : {Nat.add(b, Nat.add(c, 1n)) == _ : Nat} 79 {==} 80 81 # a + c = b + d and c < d give b < a 82 def lt_of_sum(+a: Nat, +b: Nat, +c: Nat, +d: Nat, +e: {Nat.add(a, c) == Nat.add(b, d) : Nat}, +h: {Nat.is_lt(c, d) == True{} : Bool}) -> {Nat.is_lt(b, a) == True{} : Bool}: 83 +h2 = N.lt_succ_le_succ(c, d, h) 84 +h3 = N.le_add_left(1n+c, d, b, h2) 85 +h4 = I.le_subst_r(Nat.add(b, 1n+c), Nat.add(b, d), Nat.add(a, c), Equal.sym(Nat, Nat.add(a, c), Nat.add(b, d), e), h3) 86 +e2 = Equal.trans(Nat, Nat.add(b, 1n+c), 1n+Nat.add(b, c), Nat.add(c, 1n+b), NA.add_succ(b, c), sc(b, c)) 87 +h5 = I.le_subst_l(Nat.add(b, 1n+c), Nat.add(c, 1n+b), Nat.add(a, c), e2, h4) 88 +h6 = I.le_subst_r(Nat.add(c, 1n+b), Nat.add(a, c), Nat.add(c, a), NA.add_comm(a, c), h5) 89 N.succ_le_lt(b, a, le_cancel_l(c, 1n+b, a, h6)) 90 91 def m1(+x: Nat) -> {Nat.mul(1n, x) == x : Nat}: 92 SR.one_mul(x) 93 94 # x mod P = x for x < P 95 def mod_small(+pp: Nat, +x: Nat, +h: {Nat.is_lt(x, 1n+pp) == True{} : Bool}) -> {Nat.mod(x, 1n+pp) == x : Nat}: 96 NR.mod_of(0n, pp, x, h) 97 98 # (P + e) mod P = e for e < P 99 def mod_p1(+pp: Nat, +e: Nat, +h: {Nat.is_lt(e, 1n+pp) == True{} : Bool}) -> {Nat.mod(Nat.add(1n+pp, e), 1n+pp) == e : Nat}: 100 %Equal.sym(Nat, 1n+pp, Nat.mul(1n, 1n+pp), Equal.sym(Nat, Nat.mul(1n, 1n+pp), 1n+pp, m1(1n+pp))) : {Nat.mod(Nat.add(_, e), 1n+pp) == e : Nat} 101 NR.mod_of(1n, pp, e, h) 102 103 def rn_sum_c(+r: Nat, +nn: Nat, +pp: Nat, +cn: Nat, +cp: Nat, +hs: {Nat.add(1n+pp, cp) == Nat.add(nn, cn) : Nat}, +sa: {Nat.add(cn, Nat.sub(Nat.add(r, 1n+pp), cn)) == Nat.add(r, 1n+pp) : Nat}) -> {Nat.add(cn, Nat.add(Nat.sub(Nat.add(r, 1n+pp), cn), cp)) == Nat.add(cn, Nat.add(r, nn)) : Nat}: 104 %Equal.sym(Nat, Nat.add(cn, Nat.add(Nat.sub(Nat.add(r, 1n+pp), cn), cp)), Nat.add(Nat.add(cn, Nat.sub(Nat.add(r, 1n+pp), cn)), cp), Equal.sym(Nat, Nat.add(Nat.add(cn, Nat.sub(Nat.add(r, 1n+pp), cn)), cp), Nat.add(cn, Nat.add(Nat.sub(Nat.add(r, 1n+pp), cn), cp)), NA.add_assoc(cn, Nat.sub(Nat.add(r, 1n+pp), cn), cp))) : {_ == Nat.add(cn, Nat.add(r, nn)) : Nat} 105 %Equal.sym(Nat, Nat.add(cn, Nat.sub(Nat.add(r, 1n+pp), cn)), Nat.add(r, 1n+pp), sa) : {Nat.add(_, cp) == Nat.add(cn, Nat.add(r, nn)) : Nat} 106 %Equal.sym(Nat, Nat.add(Nat.add(r, 1n+pp), cp), Nat.add(r, Nat.add(1n+pp, cp)), NA.add_assoc(r, 1n+pp, cp)) : {_ == Nat.add(cn, Nat.add(r, nn)) : Nat} 107 %Equal.sym(Nat, Nat.add(1n+pp, cp), Nat.add(nn, cn), hs) : {Nat.add(r, _) == Nat.add(cn, Nat.add(r, nn)) : Nat} 108 %Equal.sym(Nat, Nat.add(nn, cn), Nat.add(cn, nn), NA.add_comm(nn, cn)) : {Nat.add(r, _) == Nat.add(cn, Nat.add(r, nn)) : Nat} 109 %Equal.sym(Nat, Nat.add(r, Nat.add(cn, nn)), Nat.add(cn, Nat.add(r, nn)), NA.add_swap(r, cn, nn)) : {_ == Nat.add(cn, Nat.add(r, nn)) : Nat} 110 %Equal.sym(Nat, Nat.add(r, nn), Nat.add(nn, r), NA.add_comm(r, nn)) : {Nat.add(cn, _) == Nat.add(cn, Nat.add(r, nn)) : Nat} 111 %Equal.sym(Nat, Nat.add(r, nn), Nat.add(nn, r), NA.add_comm(r, nn)) : {Nat.add(cn, Nat.add(nn, r)) == Nat.add(cn, _) : Nat} 112 {==} 113 114 # with P + c_p = N + c_n and c_n <= r + P: (r + P - c_n) + c_p = r + N 115 def rn_sum(+r: Nat, +nn: Nat, +pp: Nat, +cn: Nat, +cp: Nat, +hs: {Nat.add(1n+pp, cp) == Nat.add(nn, cn) : Nat}, +hl: {Nat.is_le(cn, Nat.add(r, 1n+pp)) == True{} : Bool}) -> {Nat.add(Nat.sub(Nat.add(r, 1n+pp), cn), cp) == Nat.add(r, nn) : Nat}: 116 +d = Nat.sub(Nat.add(r, 1n+pp), cn) 117 +sa = N.sub_add(Nat.add(r, 1n+pp), cn, hl) 118 NR.add_cancel(cn, Nat.add(d, cp), Nat.add(r, nn), rn_sum_c(r, nn, pp, cn, cp, hs, sa)) 119 120 # ((r + P - (c_n mod P)) mod P + c_p) mod P = (r + N) mod P 121 def rn_val(+r: Nat, +nn: Nat, +pp: Nat, +cn: Nat, +cp: Nat, +hs: {Nat.add(1n+pp, cp) == Nat.add(nn, cn) : Nat}, +hcn: {Nat.is_lt(cn, 1n+pp) == True{} : Bool}) -> {Nat.mod(Nat.add(Nat.mod(Nat.sub(Nat.add(r, 1n+pp), Nat.mod(cn, 1n+pp)), 1n+pp), cp), 1n+pp) == Nat.mod(Nat.add(r, nn), 1n+pp) : Nat}: 122 +hl = N.le_trans(cn, 1n+pp, Nat.add(r, 1n+pp), N.lt_le(cn, 1n+pp, hcn), I.le_add_l(r, 1n+pp)) 123 %Equal.sym(Nat, Nat.mod(cn, 1n+pp), cn, mod_small(pp, cn, hcn)) : {Nat.mod(Nat.add(Nat.mod(Nat.sub(Nat.add(r, 1n+pp), _), 1n+pp), cp), 1n+pp) == Nat.mod(Nat.add(r, nn), 1n+pp) : Nat} 124 %Equal.sym(Nat, Nat.mod(Nat.add(Nat.mod(Nat.sub(Nat.add(r, 1n+pp), cn), 1n+pp), cp), 1n+pp), Nat.mod(Nat.add(Nat.sub(Nat.add(r, 1n+pp), cn), cp), 1n+pp), NR.mod_add_l(pp, Nat.sub(Nat.add(r, 1n+pp), cn), cp)) : {_ == Nat.mod(Nat.add(r, nn), 1n+pp) : Nat} 125 %Equal.sym(Nat, Nat.add(Nat.sub(Nat.add(r, 1n+pp), cn), cp), Nat.add(r, nn), rn_sum(r, nn, pp, cn, cp, hs, hl)) : {Nat.mod(_, 1n+pp) == Nat.mod(Nat.add(r, nn), 1n+pp) : Nat} 126 {==} 127 128 def rc_true(+r: Nat, +nn: Nat, +pp: Nat, +h: {Nat.is_lt(Nat.add(r, nn), 1n+pp) == True{} : Bool}) -> {Bool.not(Nat.is_lt(Nat.mod(Nat.add(r, nn), 1n+pp), nn)) == True{} : Bool}: 129 %Equal.sym(Nat, Nat.mod(Nat.add(r, nn), 1n+pp), Nat.add(r, nn), mod_small(pp, Nat.add(r, nn), h)) : {Bool.not(Nat.is_lt(_, nn)) == True{} : Bool} 130 %Equal.sym(Bool, Nat.is_lt(Nat.add(r, nn), nn), False{}, N.le_not_lt(Nat.add(r, nn), nn, I.le_add_l(r, nn))) : {Bool.not(_) == True{} : Bool} 131 {==} 132 133 def rc_false(+r: Nat, +nn: Nat, +pp: Nat, +hr: {Nat.is_lt(r, nn) == True{} : Bool}, +hn: {Nat.is_lt(nn, 1n+pp) == True{} : Bool}, +h: {Nat.is_lt(Nat.add(r, nn), 1n+pp) == False{} : Bool}) -> {Bool.not(Nat.is_lt(Nat.mod(Nat.add(r, nn), 1n+pp), nn)) == False{} : Bool}: 134 +x = Nat.add(r, nn) 135 +le1 = N.not_lt_le(x, 1n+pp, h) 136 +sa = N.sub_add(x, 1n+pp, le1) 137 +rp = N.lt_trans(r, nn, 1n+pp, hr, hn) 138 +he = N.sub_lt(x, 1n+pp, 1n+pp, le1, I.lt_le_add(r, nn, 1n+pp, 1n+pp, rp, N.lt_le(nn, 1n+pp, hn))) 139 +hen = N.sub_lt(x, 1n+pp, nn, le1, N.lt_add_r2(r, 1n+pp, nn, rp)) 140 %Equal.sym(Nat, Nat.add(r, nn), Nat.add(1n+pp, Nat.sub(Nat.add(r, nn), 1n+pp)), Equal.sym(Nat, Nat.add(1n+pp, Nat.sub(Nat.add(r, nn), 1n+pp)), Nat.add(r, nn), sa)) : {Bool.not(Nat.is_lt(Nat.mod(_, 1n+pp), nn)) == False{} : Bool} 141 %Equal.sym(Nat, Nat.mod(Nat.add(1n+pp, Nat.sub(Nat.add(r, nn), 1n+pp)), 1n+pp), Nat.sub(Nat.add(r, nn), 1n+pp), mod_p1(pp, Nat.sub(Nat.add(r, nn), 1n+pp), he)) : {Bool.not(Nat.is_lt(_, nn)) == False{} : Bool} 142 %Equal.sym(Bool, Nat.is_lt(Nat.sub(Nat.add(r, nn), 1n+pp), nn), True{}, hen) : {Bool.not(_) == False{} : Bool} 143 {==} 144 145 # for r < N < P: (r + N) mod P >= N exactly when r + N < P 146 def rn_cond(+r: Nat, +nn: Nat, +pp: Nat, +hr: {Nat.is_lt(r, nn) == True{} : Bool}, +hn: {Nat.is_lt(nn, 1n+pp) == True{} : Bool}, c: Bool, +hc: {Nat.is_lt(Nat.add(r, nn), 1n+pp) == c : Bool}) -> {Bool.not(Nat.is_lt(Nat.mod(Nat.add(r, nn), 1n+pp), nn)) == c : Bool}: 147 match c: 148 case True{}: 149 rc_true(r, nn, pp, hc) 150 case False{}: 151 rc_false(r, nn, pp, hr, hn, hc) 152 153 # n < p 154 def n_lt_p(+one: Nat, +h1: {one == 1n : Nat}) -> {Nat.is_lt(1n+K.np(one), 1n+K.pp(one)) == True{} : Bool}: 155 lt_of_sum(1n+K.pp(one), 1n+K.np(one), FS.cp(one), FS.cn(one), pn_sum(one, h1), cp_lt_cn(one, h1))