view release on metacpan or  search on metacpan

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

    return (True, None)
  ok = True
  for expr in exprs:
    for (f,n) in zero.reduce(numerator(expr)).factor():
      if normalize_factor(f) not in nonzero:
        expl.add(exprs[expr])
  if expl:
    return (False, list(expl))
  else:
    return (True, None)


def prove_zero(R, exprs, assume):
  """Check whether all of the passed expressions are provably zero, given assumptions"""
  r, e = prove_nonzero(R, dict(map(lambda x: (fastfrac(R, x.bot, 1), exprs[x]), exprs)), assume)
  if not r:
    return (False, list(map(lambda x: "Possibly zero denominator: %s" % x, e)))
  zero = R.ideal(list(map(numerator, assume.zero)))
  nonzero = prod(x for x in assume.nonzero)
  expl = []
  for expr in exprs:
    if not expr.iszero(zero):
      expl.append(exprs[expr])
  if not expl:
    return (True, None)
  return (False, expl)


def describe_extra(R, assume, assumeExtra):
  """Describe what assumptions are added, given existing assumptions"""
  zerox = assume.zero.copy()
  zerox.update(assumeExtra.zero)
  zero = R.ideal(list(map(numerator, assume.zero)))
  zeroextra = R.ideal(list(map(numerator, zerox)))
  nonzero = get_nonzero_set(R, assume)
  ret = set()
  # Iterate over the extra zero expressions
  for base in assumeExtra.zero:
    if base not in zero:
      add = []
      for (f, n) in numerator(base).factor():
        if normalize_factor(f) not in nonzero:
          add += ["%s" % normalize_factor(f)]
      if add:
        ret.add((" * ".join(add)) + " = 0 [%s]" % assumeExtra.zero[base])
  # Iterate over the extra nonzero expressions
  for nz in assumeExtra.nonzero:
    nzr = zeroextra.reduce(numerator(nz))
    if nzr not in zeroextra:
      for (f,n) in nzr.factor():
        if normalize_factor(zeroextra.reduce(f)) not in nonzero:
          ret.add("%s != 0" % normalize_factor(zeroextra.reduce(f)))
  return ", ".join(x for x in ret)


def check_symbolic(R, assumeLaw, assumeAssert, assumeBranch, require):
  """Check a set of zero and nonzero requirements, given a set of zero and nonzero assumptions"""
  assume = assumeLaw + assumeAssert + assumeBranch

  if conflicts(R, assume):
    # This formula does not apply
    return (True, None)

  describe = describe_extra(R, assumeLaw + assumeBranch, assumeAssert)
  if describe != "":
    describe = " (assuming " + describe + ")"

  ok, msg = prove_zero(R, require.zero, assume)
  if not ok:
    return (False, "FAIL, %s fails%s" % (str(msg), describe))

  res, expl = prove_nonzero(R, require.nonzero, assume)
  if not res:
    return (False, "FAIL, %s fails%s" % (str(expl), describe))

  return (True, "OK%s" % describe)


def concrete_verify(c):
  for k in c.zero:
    if k != 0:
      return (False, c.zero[k])
  for k in c.nonzero:
    if k == 0:
      return (False, c.nonzero[k])
  return (True, None)