def step_r

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

import Base
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

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