def psel0

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

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

93# b = 0 picks the second point, b = 1 the first
94def psel0(+one: Nat, a: P.Point, b: P.Point, +ha: {PT.pred(one, a) == True{} : Bool}, +hb: {PT.pred(one, b) == True{} : Bool}) -> {P.select(0n, a, b) == b : P.Point}:
95  match a b:
96    case P.Point{+x1, +y1, +z1} P.Point{+x2, +y2, +z2}:
97      %Equal.sym(List<&2, Nat>, L.select(0n, x1, x2), x2, sel0(one, 16n, x1, x2, rx(one, x1, y1, z1, ha), rx(one, x2, y2, z2, hb))) : {P.Point{_, L.select(0n, y1, y2), L.select(0n, z1, z2)} == P.Point{x2, y2, z2} : P.Point}
98      %Equal.sym(List<&2, Nat>, L.select(0n, y1, y2), y2, sel0(one, 16n, y1, y2, ry(one, x1, y1, z1, ha), ry(one, x2, y2, z2, hb))) : {P.Point{x2, _, L.select(0n, z1, z2)} == P.Point{x2, y2, z2} : P.Point}
99      %Equal.sym(List<&2, Nat>, L.select(0n, z1, z2), z2, sel0(one, 16n, z1, z2, rz(one, x1, y1, z1, ha), rz(one, x2, y2, z2, hb))) : {P.Point{x2, y2, _} == P.Point{x2, y2, z2} : P.Point}
100      {==}