def psel1

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/secp256k1/sel.bend:102

import Base
import bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/limbs.bend as L
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

102def psel1(+one: Nat, a: P.Point, b: P.Point, +ha: {PT.pred(one, a) == True{} : Bool}, +hb: {PT.pred(one, b) == True{} : Bool}) -> {P.select(1n, a, b) == a : P.Point}:
103  match a b:
104    case P.Point{+x1, +y1, +z1} P.Point{+x2, +y2, +z2}:
105      %Equal.sym(List<&2, Nat>, L.select(1n, x1, x2), x1, sel1(one, 16n, x1, x2, rx(one, x1, y1, z1, ha), rx(one, x2, y2, z2, hb))) : {P.Point{_, L.select(1n, y1, y2), L.select(1n, z1, z2)} == P.Point{x1, y1, z1} : P.Point}
106      %Equal.sym(List<&2, Nat>, L.select(1n, y1, y2), y1, sel1(one, 16n, y1, y2, ry(one, x1, y1, z1, ha), ry(one, x2, y2, z2, hb))) : {P.Point{x1, _, L.select(1n, z1, z2)} == P.Point{x1, y1, z1} : P.Point}
107      %Equal.sym(List<&2, Nat>, L.select(1n, z1, z2), z1, sel1(one, 16n, z1, z2, rz(one, x1, y1, z1, ha), rz(one, x2, y2, z2, hb))) : {P.Point{x1, y1, _} == P.Point{x1, y1, z1} : P.Point}
108      {==}