def step_v

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/secp256k1/pmul.bend:68

import Base
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/field.bend as FS
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/curve.bend as CV
import bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/point.bend as P
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/point.bend as PT
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/sel.bend as SL

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))