Add sage verification script for the group laws #302

sipa commented at 3:04 AM on September 3, 2015: contributor

This adds a SAGE script for verifying the implemented group laws.

The output should be:

Formula secp256k1_gej_add_var:
  add_infinite_ab:
    branch 0: OK
  double:
    branch 2: OK
  add:
    branch 4: OK
  add_infinite_b:
    branch 1: OK
  add_infinite_a:
    branch 0: OK
  add_opposite:
    branch 3: OK

Formula secp256k1_gej_add_ge_var:
  add_infinite_ab:
    branch 0: OK (assuming Bz - 1 = 0 [b.z=1])
  double:
    branch 2: OK (assuming Bz - 1 = 0 [b.z=1])
  add:
    branch 4: OK (assuming Bz - 1 = 0 [b.z=1])
  add_infinite_b:
    branch 1: OK (assuming Bz - 1 = 0 [b.z=1])
  add_infinite_a:
    branch 0: OK (assuming Bz - 1 = 0 [b.z=1])
  add_opposite:
    branch 3: OK (assuming Bz - 1 = 0 [b.z=1])

Formula secp256k1_gej_add_zinv_var:
  add_infinite_ab:
    branch 0: OK
  double:
    branch 2: OK
  add:
    branch 4: OK
  add_infinite_b:
    branch 0: OK
  add_infinite_a:
    branch 1: OK
  add_opposite:
    branch 3: OK

Formula secp256k1_gej_add_ge:
  add_infinite_ab:
  double:
    branch 0: OK (assuming Bz - 1 = 0 [b.z=1], Bi = 0 [b_finite])
  add:
    branch 0: OK (assuming Bz - 1 = 0 [b.z=1], Bi = 0 [b_finite])
    branch 2: OK (assuming Bz - 1 = 0 [b.z=1], Bi = 0 [b_finite])
    branch 3: OK (assuming Bz - 1 = 0 [b.z=1], Bi = 0 [b_finite])
  add_infinite_b:
  add_infinite_a:
    branch 4: OK (assuming Bz - 1 = 0 [b.z=1], Bi = 0 [b_finite])
    branch 6: OK (assuming Bz - 1 = 0 [b.z=1], Bi = 0 [b_finite])
    branch 7: OK (assuming Bz - 1 = 0 [b.z=1], Bi = 0 [b_finite])
    branch 13: OK (assuming Bz - 1 = 0 [b.z=1], Bi = 0 [b_finite])
  add_opposite:
    branch 9: OK (assuming Bz - 1 = 0 [b.z=1], Bi = 0 [b_finite])

Formula secp256k1_gej_add_ge_old [should fail]:
  add_infinite_ab:
  double:
    branch 0: OK (assuming Bz - 1 = 0 [b.z=1], Bi = 0 [b_finite])
  add:
    branch 0: OK (assuming Bz - 1 = 0 [b.z=1], Bi = 0 [b_finite])
    branch 2: FAIL, ['on_curve', 'finite_point', 'colinear_2', 'colinear_1', 'colinear_3'] fails (assuming Bz - 1 = 0 [b.z=1], Bi = 0 [b_finite])
  add_infinite_b:
  add_infinite_a:
    branch 1: OK (assuming Bz - 1 = 0 [b.z=1], Bi = 0 [b_finite])
  add_opposite:
    branch 2: OK (assuming Bz - 1 = 0 [b.z=1], Bi = 0 [b_finite])

sipa force-pushed on Sep 3, 2015

sipa commented at 4:49 PM on September 3, 2015: contributor

Updated with more comments.

sipa force-pushed on Sep 4, 2015

sipa commented at 2:03 PM on September 4, 2015: contributor

Added exhaustive verification in Z43.

sipa force-pushed on Sep 4, 2015

sipa force-pushed on Sep 17, 2015

sipa commented at 6:23 PM on September 17, 2015: contributor

Significantly rewrote the code, it now prints assumptions more explicitly, and can deal with cases involving infinity. On the downside, the exhaustive check is too slow now, so it's disabled.

sipa force-pushed on Sep 22, 2015

sipa commented at 7:10 PM on September 22, 2015: contributor

Update: make prove_zero call prove_nonzero on the denominators, to prevent 0/0. This shouldn't ever occur in reality, as the formulas should never result in 0/0, and the implementations don't return fractions... but better be safe.

sipa force-pushed on Oct 19, 2015

sipa commented at 3:23 PM on October 19, 2015: contributor

Refactored the code into multiple files, in their own directory, and updated the comments.

sipa cross-referenced this on Nov 2, 2015 from issue Using HD tree branch for encryption with Curve25519? by christianlundkvist

in sage/group_prover.sage:None in c7e9038831 outdated

 160 | +    return "%s" % self
 161 | +
 162 | +
 163 | +def conflicts(R, con):
 164 | +  """Check whether any of the passed non-zero assumptions is implied by the zero assumptions"""
 165 | +  zero = R.ideal(map((lambda x: mynumerator(R, x)), con.zero))

apoelstra commented at 5:37 PM on November 27, 2015:

These double-parens are unnecessary and a bit confusing because you don't always use them (eg the reduce call a few lines down does not), and also because the eye tends to match (( with )) which is wrong. Recommend removing them everywhere (several calls to map are like this; I don't think anything else is).

sipa commented at 3:44 PM on November 28, 2015:

Fixed in next push.

in sage/group_prover.sage:None in c7e9038831 outdated

 162 | +
 163 | +def conflicts(R, con):
 164 | +  """Check whether any of the passed non-zero assumptions is implied by the zero assumptions"""
 165 | +  zero = R.ideal(map((lambda x: mynumerator(R, x)), con.zero))
 166 | +  if len(con.nonzero) > 0 and 1 in zero:
 167 | +    return True

apoelstra commented at 5:44 PM on November 27, 2015:

I think len(con.nonzero) shouldn't be checked here. If one is implied to be zero that's a contradiction by itself.

(I also checked that the result of tests were unchanged by removing the check -- had they not been I'd have been very surprised!)

sipa commented at 3:46 PM on November 28, 2015:

Fixed in next push.

in sage/group_prover.sage:None in c7e9038831 outdated

 167 | +    return True
 168 | +  for nonzero in con.nonzero:
 169 | +    if nonzero.iszero(zero):
 170 | +      return True
 171 | +  if reduce(lambda a,b: a * b, con.nonzero, fastfrac(R, 1)).iszero(zero):
 172 | +    return True

apoelstra commented at 6:06 PM on November 27, 2015:

Should this check be here? If so, the previous check implies it and can be removed.

apoelstra commented at 6:11 PM on November 27, 2015:

This check actually weirds me out because it implies that conflicts(zero, nonzero1) and conflicts(zero, nonzero2) might be OK while conflicts(zero, nonzero1 union nonzero2) fails, which is counterintuitive.

sipa commented at 5:06 PM on November 28, 2015:

It's true, however.

Say that you know that either x=0 or y=0. That's represented as putting x*y in the zero set.

Knowing that x is nonzero or y is nonzero individually does not conflict with that. Both at the same time do conflict, however.

sipa commented at 5:08 PM on November 28, 2015:

Added a comment in the next push.

in sage/group_prover.sage:None in c7e9038831 outdated

  63 | +  def iszero(self,I):
  64 | +    """Return whether this fraction is zero given an ideal."""
  65 | +    return self.top in I and self.bot not in I
  66 | +
  67 | +  def reduce(self,assumeZero):
  68 | +    zero = self.R.ideal(map((lambda x: mynumerator(R, x)), assumeZero))

apoelstra commented at 6:23 PM on November 27, 2015:

By mynumerator(R, x) do you mean mynumerator(self.R, x)? (This is more of a "how does Python interpret this?" question than a code nit.)

apoelstra commented at 6:27 PM on November 27, 2015:

Ah, I think this code is invalid but is never called.

sipa commented at 3:41 PM on November 28, 2015:

Fixed in next push.

in sage/group_prover.sage:None in c7e9038831 outdated

 127 | +    return self.top
 128 | +
 129 | +def mynumerator(R,x):
 130 | +  """Compute the numerator of a fraction."""
 131 | +  if parent(x) == R:
 132 | +    return x

apoelstra commented at 7:28 PM on November 27, 2015:

This branch is also never called, but I think if R is a ring then x will equal numerator(x) in that case, so I think the branch is unnecessary.

apoelstra commented at 7:32 PM on November 27, 2015:

Oh, and without this branch you can s/mynumerator/numerator/ the whole code :)

sipa commented at 3:41 PM on November 28, 2015:

Fixed in next push.

in sage/group_prover.sage:None in c7e9038831 outdated

 176 | +def get_nonzero_set(R, assume):
 177 | +  """Calculate a simple set of nonzero expressions"""
 178 | +  zero = R.ideal(map((lambda x: mynumerator(R, x)), assume.zero))
 179 | +  nonzero = set()
 180 | +  for nz in assume.nonzero:
 181 | +    if mynumerator(R, nz) != 0:

apoelstra commented at 9:30 PM on November 27, 2015:

I'd prefer this check not be here. If a literal zero is in assume.nonzero your constraints are inherently inconsistent and should get flagged. If you remove the check then factor will throw an exception on the next line, which is I think is fine.

I also think the check is confusingly written, since R appears but as I pointed out in the definition of mynumerator it is not actually used.

sipa commented at 5:20 PM on November 28, 2015:

Done in next push.

in sage/group_prover.sage:None in c7e9038831 outdated

 175 | +
 176 | +def get_nonzero_set(R, assume):
 177 | +  """Calculate a simple set of nonzero expressions"""
 178 | +  zero = R.ideal(map((lambda x: mynumerator(R, x)), assume.zero))
 179 | +  nonzero = set()
 180 | +  for nz in assume.nonzero:

apoelstra commented at 9:32 PM on November 27, 2015:

We only ever use nz as mynumerator(nz). Prefer iterating over assume.nonzero.map(numerator) (or whatever the correct Python for that is)

sipa commented at 5:20 PM on November 28, 2015:

Done in next push.

in sage/group_prover.sage:None in c7e9038831 outdated

 180 | +  for nz in assume.nonzero:
 181 | +    if mynumerator(R, nz) != 0:
 182 | +      for (f,n) in mynumerator(R, nz).factor():
 183 | +        nonzero.add(f)
 184 | +    rnz = zero.reduce(mynumerator(R, nz))
 185 | +    if rnz != 0:

apoelstra commented at 9:38 PM on November 27, 2015:

If you move the definition of describe below if conflicts(R, assume) in check_symbolic, this function will only ever be called after conflicts() has been run, so this check should never trigger.

I'll add a note below to suggest that move. For here, I think it suffices to remove this check and add a comment at the top of the function saying we assume we have consistent assumptions.

sipa commented at 5:21 PM on November 28, 2015:

Done in next push.

in sage/group_prover.sage:None in c7e9038831 outdated

 188 | +  return nonzero
 189 | +
 190 | +
 191 | +def prove_nonzero(R, exprs, assume):
 192 | +  """Check whether an expression is provably nonzero, given assumptions"""
 193 | +  zero = R.ideal(map((lambda x: mynumerator(R, x)), assume.zero))

apoelstra commented at 9:40 PM on November 27, 2015:

change to map(numerator, assume.zero) as per above comments about mynumerator

apoelstra commented at 10:38 PM on November 27, 2015:

Also all the loops over expr should be over expr.map(numerator)

sipa commented at 5:22 PM on November 28, 2015:

Not possible, as that way you can't find the name in exprs anymore.

in sage/group_prover.sage:None in c7e9038831 outdated

 195 | +  expl = set()
 196 | +  ok = True
 197 | +  for expr in exprs:
 198 | +    if mynumerator(R, expr) in zero:
 199 | +      return (False, [exprs[expr]])
 200 | +  allexprs = reduce(lambda a,b: a*b, exprs, fastfrac(R, 1))

apoelstra commented at 10:39 PM on November 27, 2015:

If you did lambda a, b: numerator(a) * numerator(b), you could start with 1, and the function could take a list of numbers (rather than just fastfracs) as expr

sipa commented at 5:24 PM on November 28, 2015:

Done in next push.

in sage/group_prover.sage:None in c7e9038831 outdated

 227 | +    return (True, None)
 228 | +
 229 | +
 230 | +def prove_zero(R, exprs, assume):
 231 | +  """Check whether all of the passed expressions are provably zero, given assumptions"""
 232 | +  r, e = prove_nonzero(R, dict(map(lambda x: (fastfrac(R, x.bot, 1), exprs[x]), exprs)), assume)

apoelstra commented at 10:40 PM on November 27, 2015:

If prove_nonzero could take a dict of numbers as expr (which it almost can, see above) then fastfrac(R, x.bot, 1) can be replaced with just x.bot.

sipa commented at 5:28 PM on November 28, 2015:

It seems it can't, will look later.

in sage/group_prover.sage:None in c7e9038831 outdated

 230 | +def prove_zero(R, exprs, assume):
 231 | +  """Check whether all of the passed expressions are provably zero, given assumptions"""
 232 | +  r, e = prove_nonzero(R, dict(map(lambda x: (fastfrac(R, x.bot, 1), exprs[x]), exprs)), assume)
 233 | +  if not r:
 234 | +    return (False, map(lambda x: "Possibly zero denominator: %s" % x, e))
 235 | +  zero = R.ideal(map((lambda x: mynumerator(R, x)), assume.zero))

apoelstra commented at 10:41 PM on November 27, 2015:

map(numerator, assume.zero)

sipa commented at 5:29 PM on November 28, 2015:

Fixed in next push.

in sage/group_prover.sage:None in c7e9038831 outdated

 231 | +  """Check whether all of the passed expressions are provably zero, given assumptions"""
 232 | +  r, e = prove_nonzero(R, dict(map(lambda x: (fastfrac(R, x.bot, 1), exprs[x]), exprs)), assume)
 233 | +  if not r:
 234 | +    return (False, map(lambda x: "Possibly zero denominator: %s" % x, e))
 235 | +  zero = R.ideal(map((lambda x: mynumerator(R, x)), assume.zero))
 236 | +  nonzero = reduce((lambda x, y: x * y), assume.nonzero, fastfrac(R, 1))

apoelstra commented at 10:43 PM on November 27, 2015:

Can this reduce (and all other instances of it) be replaced with the prod function?

sipa commented at 5:32 PM on November 28, 2015:

Fixed in next push.

in sage/group_prover.sage:None in c7e9038831 outdated

 234 | +    return (False, map(lambda x: "Possibly zero denominator: %s" % x, e))
 235 | +  zero = R.ideal(map((lambda x: mynumerator(R, x)), assume.zero))
 236 | +  nonzero = reduce((lambda x, y: x * y), assume.nonzero, fastfrac(R, 1))
 237 | +  expl = []
 238 | +  for expr in exprs:
 239 | +    if not (expr * nonzero).iszero(zero):

apoelstra commented at 10:45 PM on November 27, 2015:

I'm a little confused by this use of nonzero as a witness. I guess the idea is that your ring of fractions is localized at all nonzero expressions (or something algebraic like that). Can you add a comment clarifying this?

sipa commented at 5:41 PM on November 28, 2015:

There was a reason for this, but it seems it's no longer needed. Gone in next push.

sipa force-pushed on Nov 28, 2015

sipa commented at 5:42 PM on November 28, 2015: contributor

Pushed new version to address @apoelstra's nits.

in sage/group_prover.sage:None in b471a87727 outdated

  63 | +  def iszero(self,I):
  64 | +    """Return whether this fraction is zero given an ideal."""
  65 | +    return self.top in I and self.bot not in I
  66 | +
  67 | +  def reduce(self,assumeZero):
  68 | +    zero = self.R.ideal(map(lambda x: numerator(x), assumeZero))

apoelstra commented at 6:26 PM on November 28, 2015:

lambda x: numerator(x) can just be numerator :)

in sage/group_prover.sage:None in b471a87727 outdated

 154 | +    return "%s" % self
 155 | +
 156 | +
 157 | +def conflicts(R, con):
 158 | +  """Check whether any of the passed non-zero assumptions is implied by the zero assumptions"""
 159 | +  zero = R.ideal(map(lambda x: numerator(x), con.zero))

apoelstra commented at 6:26 PM on November 28, 2015:

ditto

in sage/group_prover.sage:None in b471a87727 outdated

 164 | +      return True
 165 | +  # It can be the case that entries in the nonzero set do not individually
 166 | +  # conflict with the zero set, but their combination does. For example, if we
 167 | +  # know that either x or y is zero, x*y would be in the zero set. Having x or y
 168 | +  # individually in the nonzero set is not a conflict, but both simultaneously
 169 | +  # is.

apoelstra commented at 6:28 PM on November 28, 2015:

Suppose that our ring is Z, and our zero set is the ideal (6). Then neither 3 nor 2 is zero, but the product is. So I don't get why we can't simultaneously have 3 and 2 in the nonzero set? It seems like you're testing for something stronger than "for all nonzero things x, x is not zero".

apoelstra commented at 8:05 PM on November 28, 2015:

As @sipa explained to me on IRC, if the zero set is the ideal (6), it will be so because the tester wanted to encode "2 OR 3 is zero".

apoelstra commented at 8:10 PM on November 28, 2015:

And since we have a polynomial ring over a finite field, it will have no zero divisors, so this will always be the case. That is, f(x)*g(x) being zero is equivalent to either f(x) or g(x) being zero.

Also, by design "being zero" and "being in the zero ideal" mean the same thing in this function. The zero ideal is not some arbitrary ideal; my example with (6) being a zero ideal would mean that somebody literally encoded "6 = 0" as a condition on a formula which of course is nonsense.

in sage/group_prover.sage:None in b471a87727 outdated

 227 | +def prove_zero(R, exprs, assume):
 228 | +  """Check whether all of the passed expressions are provably zero, given assumptions"""
 229 | +  r, e = prove_nonzero(R, dict(map(lambda x: (fastfrac(R, x.bot, 1), exprs[x]), exprs)), assume)
 230 | +  if not r:
 231 | +    return (False, map(lambda x: "Possibly zero denominator: %s" % x, e))
 232 | +  zero = R.ideal(map(lambda x: numerator(x), assume.zero))

apoelstra commented at 6:29 PM on November 28, 2015:

lambda x: numerator(x) -> numerator

sipa force-pushed on Nov 28, 2015

in sage/secp256k1.sage:None in 18b717eb53 outdated

  32 | +def formula_secp256k1_gej_add_var(branch, a, b):
  33 | +  """libsecp256k1's secp256k1_gej_add_var"""
  34 | +  if branch == 0:
  35 | +    return (constraints(), constraints(nonzero={a.Infinity : 'a_finite'}), b)
  36 | +  if branch == 1:
  37 | +    return (constraints(), constraints(zero={a.Infinity : 'a_infinite'}, nonzero={b.Infinity : 'b_infinite'}), a)

apoelstra commented at 8:51 PM on November 28, 2015:

The description string for a.Infinity should be finite; two lines above finite should be infinite

in sage/secp256k1.sage:None in 18b717eb53 outdated

  49 | +  i = i + s2
  50 | +  if branch == 2:
  51 | +    r = formula_secp256k1_gej_double_var(a)
  52 | +    return (constraints(), constraints(zero={h : 'h=0', i : 'i=0', a.Infinity : 'a_finite', b.Infinity : 'b_finite'}), r)
  53 | +  if branch == 3:
  54 | +    return (constraints(), constraints(zero={h : 'h=0', a.Infinity : 'a_infinite', b.Infinity : 'b_infinite'}, nonzero={i : 'i!=0'}), point_at_infinity())

apoelstra commented at 8:53 PM on November 28, 2015:

both _infinite here should be _finite

in sage/secp256k1.sage:None in 18b717eb53 outdated

  74 | +def formula_secp256k1_gej_add_ge_var(branch, a, b):
  75 | +  """libsecp256k1's secp256k1_gej_add_ge_var, which assume bz==1"""
  76 | +  if branch == 0:
  77 | +    return (constraints(zero={b.Z - 1 : 'b.z=1'}), constraints(nonzero={a.Infinity : 'a_infinite'}), b)
  78 | +  if branch == 1:
  79 | +    return (constraints(zero={b.Z - 1 : 'b.z=1'}), constraints(zero={a.Infinity : 'a_infinite'}, nonzero={b.Infinity : 'b_infinite'}), a)

apoelstra commented at 8:54 PM on November 28, 2015:

a_infinite -> a_finite

apoelstra commented at 10:35 PM on November 28, 2015: contributor

Except for the finite/infinite typos in description strings (I think I noted them all), ACK.

Thanks for clarifying the comments!

Add sage verification script for the group laws 03d4611c81

sipa force-pushed on Nov 29, 2015

sipa commented at 3:03 PM on November 29, 2015: contributor

Fixed the incorrect finite/infinite descriptions.

apoelstra commented at 5:42 PM on November 29, 2015: contributor

ACK

sipa merged this on Dec 1, 2015

sipa closed this on Dec 1, 2015

sipa referenced this in commit 3026daa095 on Dec 1, 2015

sipa cross-referenced this on Nov 28, 2016 from issue Algebraic verification of group law by gmaxwell