view release on metacpan or  search on metacpan

libsecp256k1/sage/weierstrass_prover.sage  view on Meta::CPAN

def law_jacobian_weierstrass_add_opposites(A, B, pa, pb, pA, pB, pC):
  assumeLaw = (good_affine_point(pa) +
               good_affine_point(pb) +
               good_jacobian_point(pA) +
               good_jacobian_point(pB) +
               on_weierstrass_curve(A, B, pa) +
               on_weierstrass_curve(A, B, pb) +
               finite(pA) +
               finite(pB) +
               constraints(zero={pa.x - pb.x : 'equal_x', pa.y + pb.y : 'opposite_y'}))
  require = infinite(pC)
  return (assumeLaw, require)


def law_jacobian_weierstrass_add_infinite_a(A, B, pa, pb, pA, pB, pC):
  assumeLaw = (good_affine_point(pa) +
               good_affine_point(pb) +
               good_jacobian_point(pA) +
               good_jacobian_point(pB) +
               on_weierstrass_curve(A, B, pb) +
               infinite(pA) +
               finite(pB))
  require = finite(pC, lambda pc: constraints(zero={pc.x - pb.x : 'c.x=b.x', pc.y - pb.y : 'c.y=b.y'}))
  return (assumeLaw, require)


def law_jacobian_weierstrass_add_infinite_b(A, B, pa, pb, pA, pB, pC):
  assumeLaw = (good_affine_point(pa) +
               good_affine_point(pb) +
               good_jacobian_point(pA) +
               good_jacobian_point(pB) +
               on_weierstrass_curve(A, B, pa) +
               infinite(pB) +
               finite(pA))
  require = finite(pC, lambda pc: constraints(zero={pc.x - pa.x : 'c.x=a.x', pc.y - pa.y : 'c.y=a.y'}))
  return (assumeLaw, require)


def law_jacobian_weierstrass_add_infinite_ab(A, B, pa, pb, pA, pB, pC):
  assumeLaw = (good_affine_point(pa) +
               good_affine_point(pb) +
               good_jacobian_point(pA) +
               good_jacobian_point(pB) +
               infinite(pA) +
               infinite(pB))
  require = infinite(pC)
  return (assumeLaw, require)


laws_jacobian_weierstrass = {
  'add': law_jacobian_weierstrass_add,
  'double': law_jacobian_weierstrass_double,
  'add_opposite': law_jacobian_weierstrass_add_opposites,
  'add_infinite_a': law_jacobian_weierstrass_add_infinite_a,
  'add_infinite_b': law_jacobian_weierstrass_add_infinite_b,
  'add_infinite_ab': law_jacobian_weierstrass_add_infinite_ab
}


def check_exhaustive_jacobian_weierstrass(name, A, B, branches, formula, p):
  """Verify an implementation of addition of Jacobian points on a Weierstrass curve, by executing and validating the result for every possible addition in a prime field"""
  F = Integers(p)
  print("Formula %s on Z%i:" % (name, p))
  points = []
  for x in range(0, p):
    for y in range(0, p):
      point = affinepoint(F(x), F(y))
      r, e = concrete_verify(on_weierstrass_curve(A, B, point))
      if r:
        points.append(point)

  ret = True
  for za in range(1, p):
    for zb in range(1, p):
      for pa in points:
        for pb in points:
          for ia in range(2):
            for ib in range(2):
              pA = jacobianpoint(pa.x * F(za)^2, pa.y * F(za)^3, F(za), ia)
              pB = jacobianpoint(pb.x * F(zb)^2, pb.y * F(zb)^3, F(zb), ib)
              for branch in range(0, branches):
                assumeAssert, assumeBranch, pC = formula(branch, pA, pB)
                pC.X = F(pC.X)
                pC.Y = F(pC.Y)
                pC.Z = F(pC.Z)
                pC.Infinity = F(pC.Infinity)
                r, e = concrete_verify(assumeAssert + assumeBranch)
                if r:
                  match = False
                  for key in laws_jacobian_weierstrass:
                    assumeLaw, require = laws_jacobian_weierstrass[key](A, B, pa, pb, pA, pB, pC)
                    r, e = concrete_verify(assumeLaw)
                    if r:
                      if match:
                        print("  multiple branches for (%s,%s,%s,%s) + (%s,%s,%s,%s)" % (pA.X, pA.Y, pA.Z, pA.Infinity, pB.X, pB.Y, pB.Z, pB.Infinity))
                      else:
                        match = True
                      r, e = concrete_verify(require)
                      if not r:
                        ret = False
                        print("  failure in branch %i for (%s,%s,%s,%s) + (%s,%s,%s,%s) = (%s,%s,%s,%s): %s" % (branch, pA.X, pA.Y, pA.Z, pA.Infinity, pB.X, pB.Y, pB.Z, pB.Infinity, pC.X, pC.Y, pC.Z, pC.Infinity, e))

  print()
  return ret


def check_symbolic_function(R, assumeAssert, assumeBranch, f, A, B, pa, pb, pA, pB, pC):
  assumeLaw, require = f(A, B, pa, pb, pA, pB, pC)
  return check_symbolic(R, assumeLaw, assumeAssert, assumeBranch, require)

def check_symbolic_jacobian_weierstrass(name, A, B, branches, formula):
  """Verify an implementation of addition of Jacobian points on a Weierstrass curve symbolically"""
  R.<ax,bx,ay,by,Az,Bz,Ai,Bi> = PolynomialRing(QQ,8,order='invlex')
  lift = lambda x: fastfrac(R,x)
  ax = lift(ax)
  ay = lift(ay)
  Az = lift(Az)
  bx = lift(bx)
  by = lift(by)
  Bz = lift(Bz)
  Ai = lift(Ai)
  Bi = lift(Bi)

  pa = affinepoint(ax, ay, Ai)
  pb = affinepoint(bx, by, Bi)
  pA = jacobianpoint(ax * Az^2, ay * Az^3, Az, Ai)
  pB = jacobianpoint(bx * Bz^2, by * Bz^3, Bz, Bi)

  res = {}

  for key in laws_jacobian_weierstrass:
    res[key] = []

  print("Formula " + name + ":")
  count = 0
  ret = True
  for branch in range(branches):
    assumeFormula, assumeBranch, pC = formula(branch, pA, pB)
    assumeBranch = assumeBranch.map(lift)
    assumeFormula = assumeFormula.map(lift)
    pC.X = lift(pC.X)
    pC.Y = lift(pC.Y)
    pC.Z = lift(pC.Z)
    pC.Infinity = lift(pC.Infinity)

    for key in laws_jacobian_weierstrass:
      success, msg = check_symbolic_function(R, assumeFormula, assumeBranch, laws_jacobian_weierstrass[key], A, B, pa, pb, pA, pB, pC)
      if not success:
        ret = False
      res[key].append((msg, branch))

  for key in res:
    print("  %s:" % key)
    val = res[key]
    for x in val:
      if x[0] is not None:
        print("    branch %i: %s" % (x[1], x[0]))

  print()
  return ret