1	# GENERATED by tools/generators/rw.py from ../../../tools/generators/secp256k1_hand/pmul.src; edit the .src
2	import Base
3	import ../../../spec/crypto/secp256k1/field.bend as FS
4	import ../../../spec/crypto/secp256k1/curve.bend as CV
5	import ../../../src/crypto/secp256k1/limbs.bend as L
6	import ../../../src/crypto/secp256k1/field.bend as F
7	import ../../../src/crypto/secp256k1/point.bend as P
8	import ../../lib/logic.bend as Lg
9	import ./limbs.bend as LV
10	import ./fieldops.bend as FO
11	import ./bitsv.bend as BV
12	import ./bitsrel.bend as BR
13	import ./point.bend as PT
14	import ./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	
22	def 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	
29	def 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
37	def 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	
46	def 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	
49	def 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	
57	def 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	
68	def 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	
79	def 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	
88	def 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
105	def 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	
109	def 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	
112	def 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	  {==}