aboutsummaryrefslogtreecommitdiff
path: root/src/Specific
Commit message (Collapse)AuthorAge
* move B_order_l and prime_qGravatar Andres Erbsen2016-11-06
|
* Refactor various reflective thingsGravatar Jason Gross2016-11-06
| | | | | We now have a more principled approach in many places, and some of the tuple-specific reasoning has been filled in.
* Connect [is_bounded] to [bounded_by]Gravatar Jason Gross2016-11-06
| | | | | This hooks up the boundedness constraints on [freeze] in GF25519Bounded to those in Ed25519.
* The fix in 8.4 broke 8.5/8.6, so we fix thatGravatar Jason Gross2016-11-06
| | | | Grrrr, evars
* Add syntactic tuplesGravatar Jason Gross2016-11-06
|
* Add support for dependent reificationGravatar Jason Gross2016-11-06
|
* Work around broken evars in 8.4Gravatar Jason Gross2016-11-06
|
* Plug in boundedness proofsGravatar Jason Gross2016-11-05
| | | | | We no longer admit the boundedness proofs (other than freeze); a significant chunk of the boundedness proofs now line up nicely.
* Add better bounded lemmas to reified thingsGravatar Jason Gross2016-11-05
|
* Add eta-expansion in GF25519BoundedCommon.vGravatar Jason Gross2016-11-05
| | | | It'll be needed to vm_compute some proofs in GF25519Reflective/Reified/*
* Add proofs about boundedness to GF25519Reflective/Common.vGravatar Jason Gross2016-11-05
|
* Add unfold_is_boundedGravatar Jason Gross2016-11-05
|
* Add code for overflow check (disabled bc freeze)Gravatar Jason Gross2016-11-05
| | | | | | | Currently freeze overflows; Jade says this is because the carry chain got reversed, and that she'll work on fixing this. We should enable the sanity checks at some point after this is fixed, to fail early if things overflow.
* Split off some things from InterpretationsGravatar Jason Gross2016-11-05
|
* separate Ed25519Extraction.v, add extraction to MakefileGravatar Andres Erbsen2016-11-03
| | | | | @JasonGross: src/Specific/GF25519Bounded.v has another constant that I think needs a extraction-friendly version, I added a comment
* Shove Z.Interpretations into closer alignmentGravatar Jason Gross2016-11-03
| | | | There's some really terrible code taking advantage of the fact that we only interpret a single type
* Fix buildGravatar Jason Gross2016-11-03
|
* Make [freeze] proofs consider machine integer width and hard input bounds ↵Gravatar jadep2016-11-03
| | | | separately
* Fix bounds that were reversedGravatar Jason Gross2016-11-03
|
* Clean up fe25519_word64ize, give examplesGravatar Jason Gross2016-11-02
| | | | | | | | | | | | | | As per https://github.com/mit-plv/fiat-crypto/commit/dc8a141d13984bc39cf7523856b678a48428dbcc#commitcomment-19672297 Previously, the proofs were not unfolding the boolean comparisons that eliminate opaque proofs from the resulting proof term. We have to jump through a number of hoops because Coq is really bad at dealing with big terms, and so since we can't unfold all of the identifiers early, we unfold some of them and alias other ones, so that we can unfold the right ones with a hopefully-not-too-long cbv list at the end. (This would be a lot prettier if wish #4473 (https://coq.inria.fr/bugs/show_bug.cgi?id=4473) were granted.)
* GF25519BoundedCommon.v: require less higher order unification (8.4)Gravatar Andres Erbsen2016-11-02
|
* fix lingering reference to old name of renamed lemmaGravatar jadep2016-11-02
|
* Fix GF25519Bounded in a different wayGravatar Jason Gross2016-11-02
| | | | This only builds if current master is merged into this branch
* Fix [sqrtW_sig]Gravatar Jason Gross2016-11-02
|
* Changes to sqrt for easier bounds proofs; currently blocked on broken proof ↵Gravatar jadep2016-11-02
| | | | in GF25519Bounded
* Prove fe25519WToZ_ZToW, rename FooToBarToFoo to BarToFoo_FooToBarGravatar Jason Gross2016-11-01
| | | | The renaming brings things in line with the rest of the library
* Export strings in GF25519Reflective/CommonGravatar Jason Gross2016-11-01
| | | | This makes pretty-printing of bounds easier
* Print out the computed bounds on the various opsGravatar Jason Gross2016-11-01
| | | | | | | | | Apparently some of them overflow (carry_opp, opp, sub, carry_sub) Also the bounds on ge_modulus are probably wrong, given that it's claiming that the function always returns 0. cc @andres-erbsen @jadep
* Parameterize bounded things over the limb lengthGravatar Jason Gross2016-11-01
| | | | | | | | | | It should now be possible to use sed to change to other limbs. Alas, there are a lot of files that need to be copied over (including about 5-10 in src/Specific/GF25519Reflective/Refied/) cc @jadep cc @andres-erbsen @jadep about my change to feDec
* Add fe25519WToZToWGravatar Jason Gross2016-11-01
|
* Make it easier to extract word64Gravatar Jason Gross2016-10-31
| | | | | | This makes syntax trees not rely on WS and WO in extraction (cc @andres-erbsen)
* Add bounds type in Specific/GF25519Reflective/Common.vGravatar Jason Gross2016-10-31
|
* Make it so that changing the list of wire bounds doesn't break the buildGravatar Jason Gross2016-10-31
|
* Revert "Switch from word to Z"Gravatar Jason Gross2016-10-31
| | | | This reverts commit ac46ff22a9f6a279068ebdb897498e8dd14b1916.
* Switch from word to ZGravatar Jason Gross2016-10-31
|
* Switch to reflective bounded word in Ed25519Gravatar Jason Gross2016-10-31
| | | | (cc @andres-erbsen)
* Use sigma types to fix extractionGravatar Jason Gross2016-10-31
| | | | | | | This should get rid of the extra data being carried around after extraction. (cc @andres-erbsen)
* Add src/Specific/GF25519Reflective.vGravatar Jason Gross2016-10-31
|
* Also construct relatedness proofs in reifiedGravatar Jason Gross2016-10-30
|
* Minor changes to GF25519 reflectiveGravatar Jason Gross2016-10-30
|
* Add reification of various operationsGravatar Jason Gross2016-10-30
| | | | | We split the reification up into separate files, one operation per file, so that we can run all the reification in parallel when building.
* Add initial work on reifying GF25519 stuffGravatar Jason Gross2016-10-30
|
* Add things like app_7 to GF25519BoundedCommonWord.vGravatar Jason Gross2016-10-29
|
* Add interp_type_gen_rel_pointwise2, *_gen => *Gravatar Jason Gross2016-10-28
|
* Add {un,}curry_wire_digitsGravatar Jason Gross2016-10-27
|
* Add {un,}curry_{bin,un}op_fe25519Gravatar Jason Gross2016-10-27
|
* Add length_fe25519Gravatar Jason Gross2016-10-27
| | | | It'll be needed for generic reification and uncurrying
* Factor out cmov{l,ne} and negGravatar Jason Gross2016-10-27
| | | | This way we will have a faster build of reification things
* Simplify proof of proj1_fe25519_encodeGravatar Jason Gross2016-10-27
|
* Add lemmas about GF25519BoundedCommon.{encode,decode}Gravatar Jason Gross2016-10-27
|
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-08 01:31:02 +0000