mit-plv / fiat-crypto Goto Github PK
View Code? Open in Web Editor NEWCryptographic Primitive Code Generation by Fiat
Home Page: http://adam.chlipala.net/papers/FiatCryptoSP19/FiatCryptoSP19.pdf
License: Other
Cryptographic Primitive Code Generation by Fiat
Home Page: http://adam.chlipala.net/papers/FiatCryptoSP19/FiatCryptoSP19.pdf
License: Other
The file src/Experiments/Ed25519.v
does not build. See 9855192#commitcomment-19625309
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.
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.)
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.
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.
Travis kills it after 10 minutes with no output. I suspect it's either looping or stuck in a Qed.
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 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.
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
@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.
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.
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.
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.
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.
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.
It runs fine in 8.5pl2, but goes for 10 minutes without producing output in 8.5 and 8.5pl1.
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?
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?
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.
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:
let
s, or that you don't have trees of operations?bool
and of type word?There are some questions of what constructions we should support. I need the following features:
bool
constants (for adc
)Z
constants (for ldi
, shl
, shr
)Z
constants (things whose identity should be fixed at reification time, which are of type Z
, but which Z_beq
will block on)let ... in ...
(and a variant for handling n-to-2 operators)The things I want to be able to do with the language are:
fst
of an adc
and a snd
of the same adc
into a single "carry-let-binding")
What do we need elsewhere?
There are also some design questions:
let ... in ...
be different for different numbers of arguments?let ... in ...
?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.
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
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).
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)
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.
File "/home/jgross/Documents/repos/fiat-crypto-8.4/src/Experiments/Ed25519Extraction.v", line 289, characters 0-84:
Error: The 1st argument (n) of WordUtil.cast_word still occurs after extraction.
Please check the Extraction Implicit declarations.
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.
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.
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...
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.)
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'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:
carry_gen
to also return the value it carries, make variants of carry_simple
and carry_simple_sequence
that do the sameThis is to instantiate ZLikeOps
from #49.
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.
/usr/bin/time -f "src/CompleteEdwardsCurve/ExtendedCoordinates (real: %e, user: %U, sys: %S, mem: %M ko)" "coqc" -q -R "src" Crypto -R "Bedrock" Bedrock src/CompleteEdwardsCurve/ExtendedCoordinates.v
File "./src/CompleteEdwardsCurve/ExtendedCoordinates.v", line 74, characters 85-89:
Error: Attempt to save an incomplete proof (in proof Equivalence_eq)
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?
It seems that 60c9043 broke the build with 8.6.
$ make specific-gen COQBIN="$HOME/.local64/coq/coq-v8.6/bin/"
make -C coqprime
make[1]: Entering directory '/home/jgross/Documents/repos/fiat-crypto/coqprime'
make[1]: Nothing to be done for 'all'.
make[1]: Leaving directory '/home/jgross/Documents/repos/fiat-crypto/coqprime'
COQC src/SpecificGen/GF2213_32.v
File "./src/SpecificGen/GF2213_32.v", line 29, characters 50-57:
Error:
The term "modulus" has type "Z" while it is expected to have type "positive".
Makefile.coq:779: recipe for target 'src/SpecificGen/GF2213_32.vo' failed
make: *** [src/SpecificGen/GF2213_32.vo] Error 1
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.
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))
@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.
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.
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.
FCF (paper, code) seems like the way to go (but see adampetcher/fcf#2 before jumping in).
@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
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.rewrite
first). In particular I cannot rewrite<-
with Let_In (f e) C = Let_In e (fun v => C (f v))
.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.
A declarative, efficient, and flexible JavaScript library for building user interfaces.
๐ Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
An Open Source Machine Learning Framework for Everyone
The Web framework for perfectionists with deadlines.
A PHP framework for web artisans
Bring data to life with SVG, Canvas and HTML. ๐๐๐
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
Some thing interesting about web. New door for the world.
A server is a program made to process requests and deliver data to clients.
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
Some thing interesting about visualization, use data art
Some thing interesting about game, make everyone happy.
We are working to build community through open source technology. NB: members must have two-factor auth.
Open source projects and samples from Microsoft.
Google โค๏ธ Open Source for everyone.
Alibaba Open Source for everyone
Data-Driven Documents codes.
China tencent open source team.