~/jendhub

proofs/crypto/secp256k1/pmul.bend

bend-collections-laws-crypto@1.0.0.0 · 116 lines · 12 definitions

1# GENERATED by tools/generators/rw.py from ../../../tools/generators/secp256k1_hand/pmul.src; edit the .src
2import Base
3import bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/field.bend as FS
4import bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/curve.bend as CV
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/src/crypto/secp256k1/field.bend as F
7import bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/point.bend as P
8import bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend as Lg
9import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/limbs.bend as LV
10import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/fieldops.bend as FO
11import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/bitsv.bend as BV
12import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/bitsrel.bend as BR
13import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/point.bend as PT
14import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/sel.bend as SL
15
16# Scalar multiplication (src/crypto/secp256k1/point.bend mul: masked
17# double-and-add over the 256 bits of the scalar, most significant first)
18# computes the specification's pmul (spec/crypto/secp256k1/curve.bend) on
19# the values of the coordinates.
20# ---- the specification's loop over a list of bits ----
21
22def go_sb(i: Nat, +k: Nat) -> {CV.bits_go(i, k) == BR.sb(i, 0n, k) : List<&2, Nat>}:
23  match i:
24    case 0n:
25      {==}
26    case 1n+ +j:
27      Equal.cong(List<&2, Nat>, List<&2, Nat>, l => CV.bit(j, k) <> l, CV.bits_go(j, k), BR.sb(j, 0n, k), go_sb(j, k))
28
29def bits_is(+i: Nat, k: Nat) -> {CV.bits(i, k) == CV.bits_go(i, k) : List<&2, Nat>}:
30  match k:
31    case 0n:
32      {==}
33    case 1n+j:
34      {==}
35
36# the bits of a scalar's limbs are the specification's bits of its value
37def lbits(+one: Nat, +h1: {one == 1n : Nat}, +ks: List<&2, Nat>, +hk: {FS.limbs16(one, 16n, ks) == True{} : Bool}) -> {L.bits(ks) == CV.bits(256n, FS.value(one, ks)) : List<&2, Nat>}:
38  %Equal.sym(List<&2, Nat>, L.bits(ks), BR.sb(256n, 0n, LV.ev(ks)), BR.bits_sb(one, h1, 16n, ks, hk)) : {_ == CV.bits(256n, FS.value(one, ks)) : List<&2, Nat>}
39  %Equal.sym(List<&2, Nat>, CV.bits(256n, FS.value(one, ks)), CV.bits_go(256n, FS.value(one, ks)), bits_is(256n, FS.value(one, ks))) : {BR.sb(256n, 0n, LV.ev(ks)) == _ : List<&2, Nat>}
40  %Equal.sym(List<&2, Nat>, CV.bits_go(256n, FS.value(one, ks)), BR.sb(256n, 0n, FS.value(one, ks)), go_sb(256n, FS.value(one, ks))) : {BR.sb(256n, 0n, LV.ev(ks)) == _ : List<&2, Nat>}
41  %Equal.sym(Nat, FS.value(one, ks), LV.ev(ks), LV.ev_value(one, h1, ks)) : {BR.sb(256n, 0n, LV.ev(ks)) == BR.sb(256n, 0n, _) : List<&2, Nat>}
42  {==}
43
44# ---- the point at infinity ----
45
46def pinf_r(+one: Nat, +h1: {one == 1n : Nat}) -> {PT.pred(one, P.infinity()) == True{} : Bool}:
47  PT.pr3(one, F.zero(), F.one(), F.zero(), PT.zero_r(one, h1), FO.small_r(one, h1, 1n, SL.one_lt(one, h1)), PT.zero_r(one, h1))
48
49def pinf_v(+one: Nat, +h1: {one == 1n : Nat}) -> {PT.pv(one, P.infinity()) == CV.infinity() : CV.SPoint}:
50  %Equal.sym(Nat, FS.value(one, F.zero()), 0n, PT.zero_v(one, h1)) : {CV.SPoint{_, FS.value(one, F.small(1n)), FS.value(one, F.zero())} == CV.SPoint{0n, 1n, 0n} : CV.SPoint}
51  %Equal.sym(Nat, FS.value(one, F.zero()), 0n, PT.zero_v(one, h1)) : {CV.SPoint{0n, FS.value(one, F.small(1n)), _} == CV.SPoint{0n, 1n, 0n} : CV.SPoint}
52  %Equal.sym(Nat, FS.value(one, F.small(1n)), 1n, FO.small_val(one, h1, 1n, SL.one_lt(one, h1))) : {CV.SPoint{0n, _, 0n} == CV.SPoint{0n, 1n, 0n} : CV.SPoint}
53  {==}
54
55# ---- one step: double, then add when the bit is set ----
56
57def step_r(+one: Nat, +h1: {one == 1n : Nat}, b: Nat, +pp: P.Point, +d: P.Point, +hb: {Nat.is_lt(b, 2n) == True{} : Bool}, +hp: {PT.pred(one, pp) == True{} : Bool}, +hd: {PT.pred(one, d) == True{} : Bool}) -> {PT.pred(one, P.step(b, pp, d)) == True{} : Bool}:
58  match b:
59    case 0n:
60      %Equal.sym(P.Point, P.select(0n, P.add(d, pp), d), d, SL.psel0(one, P.add(d, pp), d, PT.padd_r(one, h1, d, pp, hd, hp), hd)) : {PT.pred(one, _) == True{} : Bool}
61      hd
62    case 1n:
63      %Equal.sym(P.Point, P.select(1n, P.add(d, pp), d), P.add(d, pp), SL.psel1(one, P.add(d, pp), d, PT.padd_r(one, h1, d, pp, hd, hp), hd)) : {PT.pred(one, _) == True{} : Bool}
64      PT.padd_r(one, h1, d, pp, hd, hp)
65    case 2n+ +c:
66      Empty.absurd({PT.pred(one, P.step(2n+c, pp, d)) == True{} : Bool}, SL.not01(c, hb))
67
68def step_v(+one: Nat, +h1: {one == 1n : Nat}, b: Nat, +pp: P.Point, +d: P.Point, +hb: {Nat.is_lt(b, 2n) == True{} : Bool}, +hp: {PT.pred(one, pp) == True{} : Bool}, +hd: {PT.pred(one, d) == True{} : Bool}) -> {PT.pv(one, P.step(b, pp, d)) == CV.step(b, FS.prime(one), PT.pv(one, pp), PT.pv(one, d)) : CV.SPoint}:
69  match b:
70    case 0n:
71      %Equal.sym(P.Point, P.select(0n, P.add(d, pp), d), d, SL.psel0(one, P.add(d, pp), d, PT.padd_r(one, h1, d, pp, hd, hp), hd)) : {PT.pv(one, _) == PT.pv(one, d) : CV.SPoint}
72      {==}
73    case 1n:
74      %Equal.sym(P.Point, P.select(1n, P.add(d, pp), d), P.add(d, pp), SL.psel1(one, P.add(d, pp), d, PT.padd_r(one, h1, d, pp, hd, hp), hd)) : {PT.pv(one, _) == CV.padd(FS.prime(one), PT.pv(one, d), PT.pv(one, pp)) : CV.SPoint}
75      PT.padd_v(one, h1, d, pp, hd, hp)
76    case 2n+ +c:
77      Empty.absurd({PT.pv(one, P.step(2n+c, pp, d)) == CV.step(2n+c, FS.prime(one), PT.pv(one, pp), PT.pv(one, d)) : CV.SPoint}, SL.not01(c, hb))
78
79def mul_go_r(+one: Nat, +h1: {one == 1n : Nat}, bs: List<&2, Nat>, +pp: P.Point, +r: P.Point, +hbs: {BV.all01(bs) == True{} : Bool}, +hp: {PT.pred(one, pp) == True{} : Bool}, +hr: {PT.pred(one, r) == True{} : Bool}) -> {PT.pred(one, P.mul_go(bs, pp, r)) == True{} : Bool}:
80  match bs:
81    case Nil{}:
82      hr
83    case +b <> +t:
84      +hb = Lg.and_left(Nat.is_lt(b, 2n), BV.all01(t), hbs)
85      +ht = Lg.and_right(Nat.is_lt(b, 2n), BV.all01(t), hbs)
86      mul_go_r(one, h1, t, pp, P.step(b, pp, P.dbl(r)), ht, hp, step_r(one, h1, b, pp, P.dbl(r), hb, hp, PT.pdbl_r(one, h1, r, hr)))
87
88def mul_go_v(+one: Nat, +h1: {one == 1n : Nat}, bs: List<&2, Nat>, +pp: P.Point, +r: P.Point, +hbs: {BV.all01(bs) == True{} : Bool}, +hp: {PT.pred(one, pp) == True{} : Bool}, +hr: {PT.pred(one, r) == True{} : Bool}) -> {PT.pv(one, P.mul_go(bs, pp, r)) == CV.lmul(FS.prime(one), bs, PT.pv(one, pp), PT.pv(one, r)) : CV.SPoint}:
89  match bs:
90    case Nil{}:
91      {==}
92    case +b <> +t:
93      +hb = Lg.and_left(Nat.is_lt(b, 2n), BV.all01(t), hbs)
94      +ht = Lg.and_right(Nat.is_lt(b, 2n), BV.all01(t), hbs)
95      +hd = PT.pdbl_r(one, h1, r, hr)
96      +hs = step_r(one, h1, b, pp, P.dbl(r), hb, hp, hd)
97      %Equal.sym(CV.SPoint, PT.pv(one, P.mul_go(t, pp, P.step(b, pp, P.dbl(r)))), CV.lmul(FS.prime(one), t, PT.pv(one, pp), PT.pv(one, P.step(b, pp, P.dbl(r)))), mul_go_v(one, h1, t, pp, P.step(b, pp, P.dbl(r)), ht, hp, hs)) : {_ == CV.lmul(FS.prime(one), t, PT.pv(one, pp), CV.step(b, FS.prime(one), PT.pv(one, pp), CV.pdbl(FS.prime(one), PT.pv(one, r)))) : CV.SPoint}
98      %Equal.sym(CV.SPoint, PT.pv(one, P.step(b, pp, P.dbl(r))), CV.step(b, FS.prime(one), PT.pv(one, pp), PT.pv(one, P.dbl(r))), step_v(one, h1, b, pp, P.dbl(r), hb, hp, hd)) : {CV.lmul(FS.prime(one), t, PT.pv(one, pp), _) == CV.lmul(FS.prime(one), t, PT.pv(one, pp), CV.step(b, FS.prime(one), PT.pv(one, pp), CV.pdbl(FS.prime(one), PT.pv(one, r)))) : CV.SPoint}
99      %Equal.sym(CV.SPoint, PT.pv(one, P.dbl(r)), CV.pdbl(FS.prime(one), PT.pv(one, r)), PT.pdbl_v(one, h1, r, hr)) : {CV.lmul(FS.prime(one), t, PT.pv(one, pp), CV.step(b, FS.prime(one), PT.pv(one, pp), _)) == CV.lmul(FS.prime(one), t, PT.pv(one, pp), CV.step(b, FS.prime(one), PT.pv(one, pp), CV.pdbl(FS.prime(one), PT.pv(one, r)))) : CV.SPoint}
100      {==}
101
102# ---- [k] P ----
103
104# the bits of a scalar are bits
105def lbits01(+one: Nat, +h1: {one == 1n : Nat}, +ks: List<&2, Nat>, +hk: {FS.limbs16(one, 16n, ks) == True{} : Bool}) -> {BV.all01(L.bits(ks)) == True{} : Bool}:
106  %Equal.sym(List<&2, Nat>, L.bits(ks), BR.sb(256n, 0n, LV.ev(ks)), BR.bits_sb(one, h1, 16n, ks, hk)) : {BV.all01(_) == True{} : Bool}
107  SL.sb01(256n, 0n, LV.ev(ks))
108
109def mul_r(+one: Nat, +h1: {one == 1n : Nat}, +ks: List<&2, Nat>, +pp: P.Point, +hk: {FS.limbs16(one, 16n, ks) == True{} : Bool}, +hp: {PT.pred(one, pp) == True{} : Bool}) -> {PT.pred(one, P.mul(ks, pp)) == True{} : Bool}:
110  mul_go_r(one, h1, L.bits(ks), pp, P.infinity(), lbits01(one, h1, ks, hk), hp, pinf_r(one, h1))
111
112def mul_v(+one: Nat, +h1: {one == 1n : Nat}, +ks: List<&2, Nat>, +pp: P.Point, +hk: {FS.limbs16(one, 16n, ks) == True{} : Bool}, +hp: {PT.pred(one, pp) == True{} : Bool}) -> {PT.pv(one, P.mul(ks, pp)) == CV.pmul(FS.prime(one), FS.value(one, ks), PT.pv(one, pp)) : CV.SPoint}:
113  %Equal.sym(CV.SPoint, PT.pv(one, P.mul_go(L.bits(ks), pp, P.infinity())), CV.lmul(FS.prime(one), L.bits(ks), PT.pv(one, pp), PT.pv(one, P.infinity())), mul_go_v(one, h1, L.bits(ks), pp, P.infinity(), lbits01(one, h1, ks, hk), hp, pinf_r(one, h1))) : {_ == CV.lmul(FS.prime(one), CV.bits(256n, FS.value(one, ks)), PT.pv(one, pp), CV.infinity()) : CV.SPoint}
114  %Equal.sym(CV.SPoint, PT.pv(one, P.infinity()), CV.infinity(), pinf_v(one, h1)) : {CV.lmul(FS.prime(one), L.bits(ks), PT.pv(one, pp), _) == CV.lmul(FS.prime(one), CV.bits(256n, FS.value(one, ks)), PT.pv(one, pp), CV.infinity()) : CV.SPoint}
115  %Equal.sym(List<&2, Nat>, L.bits(ks), CV.bits(256n, FS.value(one, ks)), lbits(one, h1, ks, hk)) : {CV.lmul(FS.prime(one), _, PT.pv(one, pp), CV.infinity()) == CV.lmul(FS.prime(one), CV.bits(256n, FS.value(one, ks)), PT.pv(one, pp), CV.infinity()) : CV.SPoint}
116  {==}