Add sage verification script for the group laws #302

pull sipa wants to merge 1 commits into bitcoin-core:master from sipa:sage changing 3 files +892 −0
  1. 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:

     0Formula secp256k1_gej_add_var:
 1  add_infinite_ab:
 2    branch 0: OK
 3  double:
 4    branch 2: OK
 5  add:
 6    branch 4: OK
 7  add_infinite_b:
 8    branch 1: OK
 9  add_infinite_a:
10    branch 0: OK
11  add_opposite:
12    branch 3: OK
13
14Formula secp256k1_gej_add_ge_var:
15  add_infinite_ab:
16    branch 0: OK (assuming Bz - 1 = 0 [b.z=1])
17  double:
18    branch 2: OK (assuming Bz - 1 = 0 [b.z=1])
19  add:
20    branch 4: OK (assuming Bz - 1 = 0 [b.z=1])
21  add_infinite_b:
22    branch 1: OK (assuming Bz - 1 = 0 [b.z=1])
23  add_infinite_a:
24    branch 0: OK (assuming Bz - 1 = 0 [b.z=1])
25  add_opposite:
26    branch 3: OK (assuming Bz - 1 = 0 [b.z=1])
27
28Formula secp256k1_gej_add_zinv_var:
29  add_infinite_ab:
30    branch 0: OK
31  double:
32    branch 2: OK
33  add:
34    branch 4: OK
35  add_infinite_b:
36    branch 0: OK
37  add_infinite_a:
38    branch 1: OK
39  add_opposite:
40    branch 3: OK
41
42Formula secp256k1_gej_add_ge:
43  add_infinite_ab:
44  double:
45    branch 0: OK (assuming Bz - 1 = 0 [b.z=1], Bi = 0 [b_finite])
46  add:
47    branch 0: OK (assuming Bz - 1 = 0 [b.z=1], Bi = 0 [b_finite])
48    branch 2: OK (assuming Bz - 1 = 0 [b.z=1], Bi = 0 [b_finite])
49    branch 3: OK (assuming Bz - 1 = 0 [b.z=1], Bi = 0 [b_finite])
50  add_infinite_b:
51  add_infinite_a:
52    branch 4: OK (assuming Bz - 1 = 0 [b.z=1], Bi = 0 [b_finite])
53    branch 6: OK (assuming Bz - 1 = 0 [b.z=1], Bi = 0 [b_finite])
54    branch 7: OK (assuming Bz - 1 = 0 [b.z=1], Bi = 0 [b_finite])
55    branch 13: OK (assuming Bz - 1 = 0 [b.z=1], Bi = 0 [b_finite])
56  add_opposite:
57    branch 9: OK (assuming Bz - 1 = 0 [b.z=1], Bi = 0 [b_finite])
58
59Formula secp256k1_gej_add_ge_old [should fail]:
60  add_infinite_ab:
61  double:
62    branch 0: OK (assuming Bz - 1 = 0 [b.z=1], Bi = 0 [b_finite])
63  add:
64    branch 0: OK (assuming Bz - 1 = 0 [b.z=1], Bi = 0 [b_finite])
65    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])
66  add_infinite_b:
67  add_infinite_a:
68    branch 1: OK (assuming Bz - 1 = 0 [b.z=1], Bi = 0 [b_finite])
69  add_opposite:
70    branch 2: OK (assuming Bz - 1 = 0 [b.z=1], Bi = 0 [b_finite])
  2. sipa force-pushed on Sep 3, 2015
  3. sipa commented at 4:49 pm on September 3, 2015: contributor
    Updated with more comments.
  4. sipa force-pushed on Sep 4, 2015
  5. sipa commented at 2:03 pm on September 4, 2015: contributor
    Added exhaustive verification in Z43.
  6. sipa force-pushed on Sep 4, 2015
  7. sipa force-pushed on Sep 17, 2015
  8. 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.
  9. sipa force-pushed on Sep 22, 2015
  10. 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.
  11. sipa force-pushed on Oct 19, 2015
  12. 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.
  13. sipa cross-referenced this on Nov 2, 2015 from issue Using HD tree branch for encryption with Curve25519? by christianlundkvist
  14. in sage/group_prover.sage: 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.
  15. in sage/group_prover.sage: 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.
  16. in sage/group_prover.sage: 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.
  17. in sage/group_prover.sage: 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.
  18. in sage/group_prover.sage: 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.
  19. in sage/group_prover.sage: 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.
  20. in sage/group_prover.sage: 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.
  21. in sage/group_prover.sage: 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.
  22. in sage/group_prover.sage: 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.
  23. in sage/group_prover.sage: 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.
  24. in sage/group_prover.sage: 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.
  25. in sage/group_prover.sage: 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.
  26. in sage/group_prover.sage: 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.
  27. in sage/group_prover.sage: 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.
  28. sipa force-pushed on Nov 28, 2015
  29. sipa commented at 5:42 pm on November 28, 2015: contributor
    Pushed new version to address @apoelstra’s nits.
  30. in sage/group_prover.sage: 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 :)
  31. in sage/group_prover.sage: 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
  32. in sage/group_prover.sage: 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.

  33. in sage/group_prover.sage: 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
  34. sipa force-pushed on Nov 28, 2015
  35. sipa force-pushed on Nov 28, 2015
  36. sipa force-pushed on Nov 28, 2015
  37. sipa force-pushed on Nov 28, 2015
  38. in sage/secp256k1.sage: 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
  39. in sage/secp256k1.sage: 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
  40. in sage/secp256k1.sage: 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
  41. 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!

  42. Add sage verification script for the group laws 03d4611c81
  43. sipa force-pushed on Nov 29, 2015
  44. sipa commented at 3:03 pm on November 29, 2015: contributor
    Fixed the incorrect finite/infinite descriptions.
  45. apoelstra commented at 5:42 pm on November 29, 2015: contributor
    ACK
  46. sipa merged this on Dec 1, 2015
  47. sipa closed this on Dec 1, 2015
  48. sipa referenced this in commit 3026daa095 on Dec 1, 2015
  49. sipa cross-referenced this on Nov 28, 2016 from issue Algebraic verification of group law by gmaxwell


sipa apoelstra

github-metadata-mirror

This is a metadata mirror of the GitHub repository bitcoin-core/secp256k1. This site is not affiliated with GitHub. Content is generated from a GitHub metadata backup.
generated: 2025-11-04 11:15 UTC
This site is hosted by @0xB10C
More mirrored repositories can be found on mirror.b10c.me