mit-plv / fiat-crypto Goto Github PK

https://travis-ci.org/mit-plv/fiat-crypto/jobs/143895375

In response to #10, I was trying to port CompleteEdwardsCurve proofs from field_algebra to super_nsatz. However, it seems that super_nsatz clears H: 1 + 1 <> 0, making a provable goal unprovable.

5f522ee

@achlipala I have measured our code against ed25519-donna and curve25519-donna, and we are doing just as well as we would have expected -- "known slowdowns only", so I guess that's a good sign. The progress towards building and comparing ecc-star can be seen at hacl-star/hacl-star#1

Our nsatz variant raises an anomaly in some cases; the standard library one does not. It's not terribly hard to work around (just clear hypotheses of the form x = x), but I figured I'd record it here.

This is why we should reserve all notations in Notations.v. I'm going through and doing this now, and will, for now, just add spaces so that ):T becomes ) : T, but we should think about changing this notation.

It runs fine in 8.5pl2, but goes for 10 minutes without producing output in 8.5 and 8.5pl1.

    x, y, sqrt_a : F
    H : sqrt_a^2 = a
    H0 : (sqrt_a / y)^2 <> d
    ============================
    d * y^2 - a <> 0

We probably want to call fsatz recursively or something, but obviously we don't want to loop...

We want to keep the travis-CI builds passing, both for our own convenience of working on master and because coq uses fiat-crypto#master as an integration test. This issue is about how to avoid needless failing travis builds. #116 was my fault, but this is not the first time we have optimistically merged something to master in hope that it will work, and saw that it actually didn't build. Ideally, we would fully re-build and test before we push. However, "just test it first" is probably not the best idea given that a complete build on one version takes roughly half an hour. Here are some other ideas on improving this general situation.

• First, let's just not put code that we already know would make travis unhappy on master. If it is a good idea to merge code that would break things, it is probably also a good idea to re-write or disable the broken things.
• Maybe we should have a Makefile target that removes files that would not be present in a clean build. This would prevent the (not that uncommon) failure mode of the build passing on our own machines due to pre-existing .vo files which are not actually built on travis. I don't know how easy it would be to implement this.
• If we really wanted to make sure master makes travis happy all the time, we could have github disallow pushes to master altogether, and require github-orchestrated merges to pass travis checks before they can be merged. This, of course, would be somewhat annoying, but it wouldn't cause huge issues with my personal workflow. @JasonGross , @jadephilipoom ?

It would be nice to move the proofs out of Experiments/Ed25519 into more appropriate files, so that the only thing we're doing in Experiments/Ed25519 is hooking everything up.

b34da8a#commitcomment-19623748

The build fails on Travis for Coq 8.4, because GF5211_32 and GF41417_32 go for 10 minutes, producing no output.

The entire project now takes over an hour to build on Coq 8.5; here are all the files that take longer than a minute to build on travis:

Time      | File Name                                                             
----------------------------------------------------------------------------------
65m35.80s | Total                                                                 
----------------------------------------------------------------------------------
11m59.10s | SpecificGen/GF5211_32                                                 
7m37.19s  | SpecificGen/GF41417_32                                                
2m31.10s  | CompleteEdwardsCurve/ExtendedCoordinates                              
2m27.94s  | Test/Curve25519SpecTestVectors                                        
2m14.14s  | Experiments/Ed25519                                                   
2m10.02s  | ModularArithmetic/Conversion                                          
2m06.50s  | Specific/GF25519Bounded                                               
1m40.32s  | EdDSARepChange                                                        
1m35.94s  | Specific/GF25519Reflective/CommonBinOp                                
1m32.26s  | Specific/GF25519                                                      
1m26.38s  | SpecificGen/GF2519_32                                                 
1m23.76s  | Specific/GF25519Reflective/CommonUnOp                                 
1m22.16s  | Specific/GF25519BoundedCommon                                         
1m20.52s  | SpecificGen/GF25519_32                                                
1m19.94s  | Specific/GF25519Reflective/CommonUnOpWireToFE                         
1m16.91s  | ModularArithmetic/ModularBaseSystemProofs                             
1m11.58s  | Algebra       

This seems rather unfortunate and perhaps a bit unreasonable to me.

It seems that 60c9043 broke the build with 8.6.

Here is code that works:

Require Import Coq.Reals.Reals Coq.nsatz.Nsatz.

Local Open Scope R.

Goal forall a b yx xz : R,
  yx^2 = xz^3 + a * xz + b ->
  (- yx)^2 = xz^3 + a * xz + b ->
  xz * (2 * yx)^2 - ((3 * xz^2 + a)^2 - xz * (2 * yx)^2 - xz * (2 * yx)^2) = 0 ->
  (3 * xz^2 + a)^2 - 2 * (2 * yx)^2 * xz = (2 * yx)^2 * xz.
Proof.
  intros ???? H0 H1 H2.
  nsatz.
Qed.

And here is code that doesn't:

Require Import Crypto.Tactics.Nsatz Crypto.Algebra Crypto.Util.Notations.

Section F.
  Context {F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv}
          {field:@field F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv}.
  Local Infix "=" := Feq : type_scope. Local Notation "a <> b" := (not (a = b)) : type_scope.
  Local Infix "+" := Fadd. Local Infix "*" := Fmul.
  Local Infix "-" := Fsub. Local Infix "/" := Fdiv.
  Local Notation "- x" := (Fopp x).
  Local Notation "x ^ 2" := (x*x). Local Notation "x ^ 3" := (x*x^2).
  Local Notation "0" := Fzero.  Local Notation "1" := Fone.
  Notation "2" := (1+1). Notation "3" := (1+2).
  Local Open Scope core_scope.

  Goal forall a b yx xz : F,
    yx^2 = xz^3 + a * xz + b ->
    (- yx)^2 = xz^3 + a * xz + b ->
    xz * (2 * yx)^2 - ((3 * xz^2 + a)^2 - xz * (2 * yx)^2 - xz * (2 * yx)^2) = 0 ->
    (3 * xz^2 + a)^2 - 2 * (2 * yx)^2 * xz = (2 * yx)^2 * xz.
  Proof.
    intros ???? H0 H1 H2.
    nsatz. (* In nested Ltac calls to "nsatz", "nsatz", "nsatz_sugar_power" and "nsatz_domain_sugar_power", last
call failed.
Error: No applicable tactic.
computation without sugar
p: [9]*b^4 + [(-12)]*a^2*b + [6]*b^2*c + [1]*c^2 
lp:
[(-1)]*b^3 + [1]*a^2 + [(-1)]*b*c + [(-1)]*d 
[(-1)]*b^3 + [1]*a^2 + [(-1)]*b*c + [(-1)]*d 
[(-9)]*b^4 + [12]*a^2*b + [(-6)]*b^2*c + [(-1)]*c^2 
remainder: [3]*a^2*b + [3]*b^2*c + [(-1)]*c^2 + [9]*b*d 
computation of the Groebner basis
[3,3]0[3,2]
new polynomial: [3]*a^2*b + [3]*b^2*c + [(-1)]*c^2 + [9]*b*d 
remainder: 0
polynomial reduced to 0
r ok
r: 0
verif sum: [9]*b^4 + [(-9)]*a^2*b + [9]*b^2*c + [9]*b*d 
coefficient: [(-1)] 
computed
time:      0.000s
cert ok
useless spolynomials: 0
useful spolynomials: 2
number of parametres: -1
term computed
term computed
computation without sugar
p: [81]*b^8 + [(-216)]*a^2*b^5 + [108]*b^6*c + [144]*a^4*b^2 + [(-144)]*a^2*b^3*c + [54]*b^4*c^2 + [(-24)]*a^2*b*c^2 + [12]*b^2*c^3 + [1]*c^4 
lp:
[(-1)]*b^3 + [1]*a^2 + [(-1)]*b*c + [(-1)]*d 
[(-1)]*b^3 + [1]*a^2 + [(-1)]*b*c + [(-1)]*d 
[(-9)]*b^4 + [12]*a^2*b + [(-6)]*b^2*c + [(-1)]*c^2 
remainder: [(-9)]*a^4*b^2 + [(-18)]*a^2*b^3*c + [(-27)]*b^4*c^2 + [81]*b^5*d + [24]*a^2*b*c^2 + [(-12)]*b^2*c^3 + [(-135)]*a^2*b^2*d + [27]*b^3*c*d + [(-1)]*c^4 
computation of the Groebner basis
[3,3]0[3,2]
new polynomial: [3]*a^2*b + [3]*b^2*c + [(-1)]*c^2 + [9]*b*d 
remainder: [9]*a^4*c + [(-3)]*a^2*b*c^2 + [(-15)]*b^2*c^3 + [27]*a^2*b^2*d + [54]*b^3*c*d + [1]*c^4 + [(-9)]*a^2*c*d + [(-27)]*b*c^2*d + [81]*b^2*d^2 
[4,4]c[4,3]
new polynomial: [(-3)]*a^4 + [4]*b^2*c^2 + [(-9)]*b^3*d + [3]*a^2*d + [3]*b*c*d 
remainder: 0
polynomial reduced to 0
r ok
r: 0
verif sum: [81]*b^8 + [(-216)]*a^2*b^5 + [108]*b^6*c + [135]*a^4*b^2 + [(-153)]*a^2*b^3*c + [54]*b^4*c^2 + [(-9)]*a^4*c + [(-18)]*a^2*b*c^2 + [27]*b^2*c^3 + [(-54)]*a^2*b^2*d + [(-54)]*b^3*c*d + [9]*a^2*c*d + [27]*b*c^2*d + [(-81)]*b^2*d^2 
coefficient: [(-1)] 
computed
time:      0.000s
cert ok
useless spolynomials: 0
useful spolynomials: 3
number of parametres: -1
term computed
term computed
computation without sugar
p: [729]*b^12  + 16 terms
lp:
[(-1)]*b^3 + [1]*a^2 + [(-1)]*b*c + [(-1)]*d 
[(-1)]*b^3 + [1]*a^2 + [(-1)]*b*c + [(-1)]*d 
[(-9)]*b^4 + [12]*a^2*b + [(-6)]*b^2*c + [(-1)]*c^2 
remainder: [(-27)]*a^8  + 17 terms
computation of the Groebner basis
[3,3]0[3,2]
new polynomial: [3]*a^2*b + [3]*b^2*c + [(-1)]*c^2 + [9]*b*d 
remainder: [(-27)]*a^8  + 17 terms
[4,4]c[4,3]
new polynomial: [(-3)]*a^4 + [4]*b^2*c^2 + [(-9)]*b^3*d + [3]*a^2*d + [3]*b*c*d 
remainder: 0
polynomial reduced to 0
r ok
r: 0
verif sum: [729]*b^12 + [(-2916)]*a^2*b^9 + [1458]*b^10*c + [3888]*a^4*b^6 + [(-3888)]*a^2*b^7*c + [1215]*b^8*c^2 + [(-1728)]*a^6*b^3 + [2592]*a^4*b^4*c + [(-1944)]*a^2*b^5*c^2 + [540]*b^6*c^3 + [27]*a^8 + [54]*a^6*b*c + [405]*a^4*b^2*c^2 + [(-477)]*a^2*b^3*c^3 + [135]*b^4*c^4 + [81]*a^4*b^3*d + [(-63)]*a^4*c^3 + [(-18)]*a^2*b*c^4 + [81]*b^2*c^5 + [135]*a^6*d + [243]*a^4*b*c*d + [(-486)]*a^2*b^2*c^2*d + [(-378)]*b^3*c^3*d + [486]*a^2*b^3*d^2 + [9]*a^2*c^3*d + [135]*b*c^4*d + [81]*a^4*d^2 + [(-1215)]*b^2*c^2*d^2 + [729]*b^3*d^3 + [54]*c^3*d^2 + [(-243)]*a^2*d^3 + [(-729)]*b*c*d^3 
coefficient: [(-1)] 
computed
time:      0.000s
cert ok
useless spolynomials: 0
useful spolynomials: 3
number of parametres: -1
term computed
term computed
computation without sugar
p: [6561]*b^16  + 25 terms
lp:
[(-1)]*b^3 + [1]*a^2 + [(-1)]*b*c + [(-1)]*d 
[(-1)]*b^3 + [1]*a^2 + [(-1)]*b*c + [(-1)]*d 
[(-9)]*b^4 + [12]*a^2*b + [(-6)]*b^2*c + [(-1)]*c^2 
remainder: [81]*a^10*b  + 27 terms
computation of the Groebner basis
[3,3]0[3,2]
new polynomial: [3]*a^2*b + [3]*b^2*c + [(-1)]*c^2 + [9]*b*d 
remainder: [(-81)]*a^8*c^2  + 27 terms
[4,4]c[4,3]
new polynomial: [(-3)]*a^4 + [4]*b^2*c^2 + [(-9)]*b^3*d + [3]*a^2*d + [3]*b*c*d 
remainder: 0
polynomial reduced to 0
r ok
r: 0
verif sum: [(-6561)]*b^16 + [34992]*a^2*b^13 + [(-17496)]*b^14*c + [(-69984)]*a^4*b^10 + [69984]*a^2*b^11*c + [(-20412)]*b^12*c^2 + [62208]*a^6*b^7 + [(-93312)]*a^4*b^8*c + [58320]*a^2*b^9*c^2 + [(-13608)]*b^10*c^3 + [(-20736)]*a^8*b^4 + [41472]*a^6*b^5*c + [(-46656)]*a^4*b^6*c^2 + [25920]*a^2*b^7*c^3 + [(-5670)]*b^8*c^4 + [81]*a^10*b + [243]*a^8*b^2*c + [7074]*a^6*b^3*c^2 + [(-10368)]*a^4*b^4*c^3 + [6480]*a^2*b^5*c^4 + [(-1512)]*b^6*c^5 + [(-108)]*a^8*c^2 + [(-378)]*a^6*b*c^3 + [(-891)]*a^4*b^2*c^4 + [1053]*a^2*b^3*c^5 + [(-252)]*b^4*c^6 + [891]*a^8*b*d + [1620]*a^6*b^2*c*d + [243]*a^4*b^3*c^2*d + [297]*a^4*c^5 + [(-18)]*a^2*b*c^6 + [(-279)]*b^2*c^7 + [(-1593)]*a^6*c^2*d + [(-2025)]*a^4*b*c^3*d + [3078]*a^2*b^2*c^4*d + [2106]*b^3*c^5*d + [3402]*a^6*b*d^2 + [1458]*a^4*b^2*c*d^2 + [(-5832)]*a^2*b^3*c^2*d^2 + [135]*a^2*c^5*d + [(-711)]*b*c^6*d + [(-2673)]*a^4*c^2*d^2 + [324]*a^2*b*c^3*d^2 + [10773]*b^2*c^4*d^2 + [4374]*a^4*b*d^3 + [(-8748)]*a^2*b^2*c*d^3 + [(-15309)]*b^3*c^2*d^3 + [(-432)]*c^5*d^2 + [3645]*a^2*c^2*d^3 + [8991]*b*c^3*d^3 + [(-2187)]*a^2*b*d^4 + [(-15309)]*b^2*c*d^4 + [729]*c^2*d^4 + [(-6561)]*b*d^5 
coefficient: [1] 
computed
time:      0.001s
cert ok
useless spolynomials: 0
useful spolynomials: 3
number of parametres: -1
term computed
term computed
computation without sugar
p: [59049]*b^20  + 36 terms
lp:
[(-1)]*b^3 + [1]*a^2 + [(-1)]*b*c + [(-1)]*d 
[(-1)]*b^3 + [1]*a^2 + [(-1)]*b*c + [(-1)]*d 
[(-9)]*b^4 + [12]*a^2*b + [(-6)]*b^2*c + [(-1)]*c^2 
remainder: [(-243)]*a^12*b^2  + 38 terms
computation of the Groebner basis
[3,3]0[3,2]
new polynomial: [3]*a^2*b + [3]*b^2*c + [(-1)]*c^2 + [9]*b*d 
remainder: [729]*a^12*c  + 39 terms
[4,4]c[4,3]
new polynomial: [(-3)]*a^4 + [4]*b^2*c^2 + [(-9)]*b^3*d + [3]*a^2*d + [3]*b*c*d 
remainder: 0
polynomial reduced to 0
r ok
r: 0
verif sum: [59049]*b^20 + [(-393660)]*a^2*b^17 + [196830]*b^18*c + [1049760]*a^4*b^14 + [(-1049760)]*a^2*b^15*c + [295245]*b^16*c^2 + [(-1399680)]*a^6*b^11 + [2099520]*a^4*b^12*c + [(-1224720)]*a^2*b^13*c^2 + [262440]*b^14*c^3 + [933120]*a^8*b^8 + [(-1866240)]*a^6*b^9*c + [1749600]*a^4*b^10*c^2 + [(-816480)]*a^2*b^11*c^3 + [153090]*b^12*c^4 + [(-248832)]*a^10*b^5 + [622080]*a^8*b^6*c + [(-933120)]*a^6*b^7*c^2 + [777600]*a^4*b^8*c^3 + [(-340200)]*a^2*b^9*c^4 + [61236]*b^10*c^5 + [243]*a^12*b^2 + [243]*a^10*b^3*c + [103680]*a^8*b^4*c^2 + [(-207360)]*a^6*b^5*c^3 + [194400]*a^4*b^6*c^4 + [(-90720)]*a^2*b^7*c^5 + [17010]*b^8*c^6 + [729]*a^12*c + [81]*a^10*b*c^2 + [(-2430)]*a^8*b^2*c^3 + [(-18900)]*a^6*b^3*c^4 + [25920]*a^4*b^4*c^5 + [(-15120)]*a^2*b^5*c^6 + [3240]*b^6*c^7 + [3402]*a^10*b^2*d + [4860]*a^8*b^3*c*d + [(-135)]*a^8*c^4 + [1998]*a^6*b*c^5 + [2241]*a^4*b^2*c^6 + [(-2205)]*a^2*b^3*c^7 + [405]*b^4*c^8 + [4131]*a^10*c*d + [(-5670)]*a^8*b*c^2*d + [(-22680)]*a^6*b^2*c^3*d + [(-7047)]*a^4*b^3*c^4*d + [18225]*a^8*b^2*d^2 + [24786]*a^6*b^3*c*d^2 + [(-1251)]*a^4*c^7 + [198]*a^2*b*c^8 + [1053]*b^2*c^9 + [10827]*a^6*c^4*d + [12879]*a^4*b*c^5*d + [(-16902)]*a^2*b^2*c^6*d + [(-10746)]*b^3*c^7*d + [(-486)]*a^8*c*d^2 + [(-48114)]*a^6*b*c^2*d^2 + [(-34020)]*a^4*b^2*c^3*d^2 + [46170]*a^2*b^3*c^4*d^2 + [43740]*a^6*b^2*d^3 + [26244]*a^4*b^3*c*d^3 + [(-1287)]*a^2*c^7*d + [3591]*b*c^8*d + [31833]*a^4*c^4*d^2 + [(-4536)]*a^2*b*c^5*d^2 + [(-76059)]*b^2*c^6*d^2 + [(-30618)]*a^6*c*d^3 + [(-104976)]*a^4*b*c^2*d^3 + [145800]*a^2*b^2*c^3*d^3 + [169857]*b^3*c^4*d^3 + [32805]*a^4*b^2*d^4 + [(-85293)]*a^2*b^3*c*d^4 + [2538]*c^7*d^2 + [(-26487)]*a^2*c^4*d^3 + [(-79461)]*b*c^5*d^3 + [(-19683)]*a^4*c*d^4 + [24057]*a^2*b*c^2*d^4 + [328050]*b^2*c^3*d^4 + [(-39366)]*a^2*b^2*d^5 + [(-157464)]*b^3*c*d^5 + [(-16038)]*c^4*d^4 + [45927]*a^2*c*d^5 + [196830]*b*c^2*d^5 + [(-59049)]*b^2*d^6 
coefficient: [(-1)] 
computed
time:      0.001s
cert ok
useless spolynomials: 0
useful spolynomials: 3
number of parametres: -1
term computed
term computed
 *)
  Qed.
End F.

This seems somehow related to the fact that we have duplicate information in the hypotheses.

Travis kills it after 10 minutes with no output. I suspect it's either looping or stuck in a Qed.

It seems that field_simplify_eq puts the original goal first, while field_simplify_eq in H puts it last. This makes it a pain to write automation that calls both of them. I'm going to try to work around this in common_denominator_in, so that tactics above that don't see this issue (I'm going to arbitrarily pick that the original goal should come first, but feel free to suggest otherwise). We could also see if we could do anything about field_simplify_eq in itself.

It would be nice to have make create files with the generated specific code in them (and then cat those files at the end of the Travis build). We will eventually be generating qhasm code, currently most of Specific/ goes down to Z expressions. I don't know how much the process for outputing stuff depends on what is being output, so it may make sense to punt this for a while.

We now have something like eight different variants of reflected syntax: Input.expr and Output.expr in https://github.com/mit-plv/fiat-crypto/blob/jgross-phoas/src/Experiments/FancyMachineMontgomery256.v (mine) , https://github.com/mit-plv/fiat-crypto/blob/rsloan-phoas/src/Experiments/SpecificCurve25519.v (@varomodt 's), and https://github.com/mit-plv/fiat-crypto/blob/phoas/src/Experiments/SpecificCurve25519.v (@andres-erbsen 's), my untyped symbolic (SymbolicExpr) in https://github.com/mit-plv/fiat-crypto/blob/jgross-phoas/src/Experiments/FancyMachineMontgomery256.v (I also have Syntax, which I use only for notations), and possibly another one that is the input to @varomodt 's assembly pipeline. We should probably unify them, to some extend, so that we're not duplicating work and copy-pasting.

I propose that we settle on how to design the inductive syntax here. There are some high-level questions:

• How much do we want to enforce by construction?
  • Should the input and output languages for linearization be the same?
  • Should the output language enforce things like that you don't have wrongly-nested lets, or that you don't have trees of operations?
  • Should we enforce that we only have variables of type bool and of type word?

There are some questions of what constructions we should support. I need the following features:

• Kinds of operators:
  • 1-to-1 (ldi)
  • 2-to-1 (e.g., mulhwll)
  • 3-to-1 (e.g., selc)
  • 3-to-2 (e.g., adc, subc)
• types:
  • booleans (for the carry bit)
  • words (or whatever type is carrying bounded integers)
  • literal bool constants (for adc)
  • literal Z constants (for ldi, shl, shr)
  • abstract Z constants (things whose identity should be fixed at reification time, which are of type Z, but which Z_beq will block on)
• generic operations:
  • let ... in ... (and a variant for handling n-to-2 operators)
  • possibly: function abstraction, for things like parameterizing multiplication over its word arguments

The things I want to be able to do with the language are:

• reification & interpretation
• linearization of lets and of function application
• common-subexpression-elimination (including combining a fst of an adc and a snd of the same adc into a single "carry-let-binding")
  • note that cse for PHOAS seems to require a variant of the syntax with decidable equality, to be used for keys / indexing of variables
• notations that let it look like assembly (since I'm too lazy to write stringification at the moment)

What do we need elsewhere?

There are also some design questions:

• How should we represent abstract constants?
• Should the let ... in ... be different for different numbers of arguments?
• Should we fuse operator application and let ... in ...?

We should pick a convention for our lemmas. Currently we have foo_length, length_foo, and we also have _exact and _full variants in a few places.

In most of my arithmetic proofs, Z.div and Z.modulo are the source of most of my problems. push_Zmod and pull_Zmod do a reasonable job at dealing with Z.modulo (though I think I need to add a case that relates (a mod b) * c and (a * c) mod (b * c)), though it's just a building block, not anything like a solver. By contrast, I've been handling Z.div with a plethora of lemmas in zsimplfy that I've been generating in Python and Mathematica. The most recent batch slowed down GF25519 by 7 seconds (fixed by #54), and they're very ad-hoc. What I'm lacking is a systematic procedure that says how to deal with Z.div in most cases. Any ideas?

Currently bounded is defined for limb_widths in Pow2Base. It seems like it'd be more natural in BaseSystem. Is there any reason not to move it (and upper_bound) there?

FCF (paper, code) seems like the way to go (but see adampetcher/fcf#2 before jumping in).

Parametrizing every definition in a module individually leads to explosion in the number of parameters. See https://gist.github.com/andres-erbsen/3c4989ad05673f6807728b9ecccd0557 for an example. It would be nice if we figured out to how to modularize our code in a way that does not cause that.

In particular, I am thinking of the following:

Record field := { F:Type; add : F->F->F; ...; is_field F add ... }

Section Edwards.
  Context {f:field}.
  (* "from f import *" *)
  Let add := F.(add)
  Let mul := F.(mul)
  ...

 Lemma edwards_curve_is_group : is group ... .
 Qed.

  (* only this would be used from outside *)
 Definition edwards_curve_group : group := {
   op := point_addition;
   ...
   is_group := edwards_curve_is_group
 }

The module system could do this automatically for us, but would not let us Check module instantiations, determine module parameters from Ltac, or parametrize modules by something other than modules.

I am not sure how mechanically we could convert the existing codebase, but let's figure out what to do first.

Another question is how liberally we should use this construction. I definitely wouldn't want generic lemmas (e.g., about properties of fields) to talk about projections from bundles -- it is important that a lemma can be applied even if the goal is not in bundled form.

If copyright authors are listed in a LICENSE, COPYING, AUTHORS or similar file, please add Google Inc. if it's not already there.

We should do this, if Copyright (c) 2015 Programming Languages and Verification Group at MIT CSAIL counts as listing authors. (If not, just close this issue.)

We very briefly had a working 8.4 build! (daff502) However, the next commit broke the build. I've pushed a fix for a Not_found exception but am going to sleep now, and there may be more issues.

modulus m = 2^252 + 27742317777372353535851937790883648493, length k = 256, (precomputed mu = 1852673427797059126777135760139006525645217721299241702126143248052143860224795,) input a < 2^512. As in https://github.com/floodyberry/supercop/blob/master/crypto_sign/ed25519/ref/sc25519.c#L41.

ZUtil is a bit slow to compile. It'd be faster (on parallel machines) if we split it up into preliminaries (database creation, adding standard lemmas to them), theorems about + and -, theorems about *, theorems about /, theorems about mod, misc theorems/tactics, and ones that make use of the theorems in the aforementioned parts. I might do this myself at some point soon. The structure should probably be:

ZUtil/
  Core.v
  AddSub.v
  Mul.v
  Div.v
  Modulo.v
  Misc.v
ZUtil.v # exports the above

I will hopefully fix this myself, but I'm marking it here so it's common knowledge. I suspect the issue is that the typeclass resolution I do to reify operators does matching on the entire expression under the operators, and the fix to this would be to only key on the head of the expression when reifying an operator. (So Coq doesn't repeatedly typecheck large terms / build them into the expression tree.)

https://travis-ci.org/mit-plv/fiat-crypto/jobs/141910711

As the Specific/ code becomes more developed, build times go up. It woud be nice to have Makefile target that builds everything but the Specific directory for use while pushing changes through the rest of the codebase. This would be especially useful when refactoring irrelevant proofs.

Is there any reason that we use CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v rather than CompleteEdwardsCurve/Theorems.v? From my experience with the category theory library in HoTT, managing the complete namespace in each file independently of the directory structure becomes a headache, and can easily lead to inconsistent styling.

You wanted word 64 rather than Z, right @andres-erbsen?

I'm making this an issue so that I don't forget to do it, and so that this is recorded somewhere.

@JasonGross @achlipala: I am failing to derive a version of EdDSA.sign where types of Let-bound variables are changed to an efficient representation.

There seem to be three issues

• The definition of sign is not parametrized over nat, so I cannot do representation changes by plugging in both spec and optimized parameters and proving relatedness as we ended up doing for the field and elliptic curve levels.
• unification fails on pattern fragment modulo beta (cfdc423#diff-5366caedd04016399124d528353b4a5cR258, of course I tried to do this using rewrite first). In particular I cannot rewrite<- with Let_In (f e) C = Let_In e (fun v => C (f v)).
• the return type of sign is determined by combine : forall a, word a -> forall b, word b -> word (a+b), which prevents most tactics from filling in the return type automatically; specifying it manually works but makes tactic code quite verbose.

Unless something comes up from this thread that bypasses all three issues, I will give up on synthesizing the representation change part of optimizing signing, and write and verify the fast version manually.

We should revert 4d3d21d but use 6 rather than 10, to remove the dummies from https://github.com/mit-plv/fiat-crypto/blob/master/src/Specific/GF25519Reflective/Reified/LadderStep.v#L32

The file src/Experiments/Ed25519.v does not build. See 9855192#commitcomment-19625309

The f_equiv tactic behaves differently in Coq 8.4 and Coq 8.5/8.6. We should either roll our own, or stop using it.

As Travis alerted me, making Let ... in ... a notation conflicts with the vernacular Let id := body. in Coq 8.4. Thus we should pick a better name. What should we pick? dlet (for definition)? let'? Let'?

We should have a .dir-locals.el that sets COQPATH, so we don't have to set it in emacs. Preferably, we should have a target in the makefile that makes it based on which version of coq is in COQBIN. Maybe something like (untested):

ifneq ($(filter 8.4%,$(COQ_VERSION)),) # 8.4
COQPRIME_FOLDER := coqprime-8.4
else
COQPRIME_FODLER := coqprime
endif

.dir-locals.el::
    sed 's:@COQPRIME@:$(COQPRIME_FOLDER):g' .dir-locals.el.in > $@

with .dir-locals.el.in being

((coq-mode . ((eval . (let ((default-directory (locate-dominating-file
                                                buffer-file-name ".dir-locals.el"))
                             (cur-COQPATH (getenv "COQPATH")))
                        (setenv "COQPATH" (concat (expand-file-name "@COQPRIME@") (if (string= "" cur-COQPATH) "" (concat ":" cur-COQPATH))))))))

(@cpitclaudel might have useful input here)

https://s3.amazonaws.com/archive.travis-ci.org/jobs/207100793/log.txt
"The job exceeded the maximum time limit for jobs, and has been terminated."

src/WeierstrassCurve/WeierstrassCurveTheorems (real: 2073.61, user: 2070.73, sys: 1.44, mem: 2009060 ko) is new, of course other stuff is slow as well.

I'm trying to get an add-with-carry on digits that gives me both the resulting sum, modulo upper_bound limb_widths, and a boolean indicating whether or not there's a carry in the most significant bit. I'm looking for something that will be most reusable / best-suited to the underlying assembly. Options I see are:

1. Build it on top of what's already existing: first add, then return, separately, both the result of carrying, and the boolean given by testing whether the decoded value (pre-carrying) is too big / matches with the result of decoding the carried value
2. Generalize carry_gen to also return the value it carries, make variants of carry_simple and carry_simple_sequence that do the same
3. Inject the digits into a larger base, compute the addition in the larger base, and then check the high bit, and return that, together with the truncated digits

This is to instantiate ZLikeOps from #49.

@JasonGross, I dug into the attempt to prove Weierstrass associativity directly at master...JasonGross:wip-weierstrass#diff-ac5f33d32601c240bed22e951c18f7d1R166. The most interesting goal is https://gist.github.com/andres-erbsen/bf8d8a98c490ff898aec23eb21ae75d8, which nsatz is still running on (10min, I will leave it overnight). Sage/libsingular can check this goal and, unless I am misunderstanding something, produce a witness as well https://gist.github.com/andres-erbsen/2ca17a4f0d458eee160d76bf2da48abf.

This bug should probably be reported upstream.

Maybe it would be a good idea to replace nsatz_compute with libsingular's lift? They are not quite the same, but, well, so far the latter has worked in cases where the former doesn't.

The build produces more than 10000 lines of output. This makes the Travis web interface slow, and one needs to click on "raw log" to see the remaining lines of output.

I think we don't need 10000 lines of output. Most of the spew seems to come from src/Specific/GF25519Reflective/Reified/.*Display.v. Could we just disable this, or redirect it into a file?

Here's the root of the apparent lack of linearization: at the bottom of Ed25519Extraction, if I do:

Require Import Util.LetIn.
Definition foo := dlet x := 1 + 2 in dlet y := x + x in dlet z := y + 1 in z + 2.
Recursive Extraction foo.

I get out

module Main where

import qualified Prelude

foo :: Prelude.Integer
foo =
  let {x = (Prelude.+) (Prelude.succ 0) (Prelude.succ (Prelude.succ 0))} in
  (Prelude.+) ((Prelude.+) ((Prelude.+) x x) (Prelude.succ 0)) (Prelude.succ (Prelude.succ 0))

The definitions and lemmas used (not defined) in Ed25519 take different arguments in different coq versions. I am guessing that this is similar to the issue we had with Shrink Obligations (discussed at
#57 and https://coq.inria.fr/bugs/show_bug.cgi?id=5044).

https://travis-ci.org/mit-plv/fiat-crypto/jobs/146216010#L671

Traceback (most recent call last):
  File "etc/coq-scripts/timing/make-one-time-file.py", line 35, in <module>
    table = make_table_string(times_dict)
  File "etc/coq-scripts/timing/make-one-time-file.py", line 17, in make_table_string
    times_width = max(max(map(len, times_dict.values())), len(sum_times(times_dict.values())))
ValueError: max() arg is an empty sequence

An easy (and probably acceptable) fix would be to just not run this in the cases it fails.

Probably a missing change x with x_opt somewhere in opt.

 let x'29 := x'28 & (33554432 + -1) in
 let y' := x'27 & (67108864 + -1) in
 let y'0 := x'26 & (33554432 + -1) in
 let y'1 := x'25 & (67108864 + -1) in
 let y'2 := x'24 & (33554432 + -1) in

I added a version of common_denominator that is faster and cleaner; it does not perform simplification in portions of the term that it doesn't need to. (2b7e454)

However, I can't use it in field_algebra, because various code depends on the exact way in which field_algebra calls field_simplify_eq. If we can, I'd like to head off this issue early; this is the first hint of something like the design flaw in Coq's unification where the devs can't touch anything without breaking backwards compatibility, because they've extended it ad-hoc without any specification.

(@andres-erbsen @achlipala)