aboutsummaryrefslogtreecommitdiff
path: root/src/Specific/GF25519BoundedCommon.v
Commit message (Collapse)AuthorAge
* Get rid of list-based Tuple.mapGravatar Jason Gross2017-03-30
|
* Switch to fully uncurried form for reflectionGravatar Jason Gross2017-03-01
| | | | | | | | | | | This will eventually make a number of proofs easier. Unfortunately, the correctness lemmas for AddCoordinates and LadderStep no longer work (because of different arities), and there's a proof in Experiments/Ed25519 that I've admitted. The correctness lemmas will be easy to re-add when we have a more general version that handle arbitrary type shapes.
* Revert "Add apply10"Gravatar Jason Gross2017-01-07
| | | | | | | | | | | | | | | | | | | | | | | | This reverts commit fe7e75f74cc3b18f87c13b2aeadaf24f12f0001b. Revert "copy_bounds" This reverts commit 4c395e83de3c0baf7f8639fa2fbe2b62ba509682. Revert "Add Common10_4Op" This reverts commit 677733838139ff09d4a2dd9ff82258492a9a5bab. Revert "Add Expr10_4Op" This reverts commit 540740e8a423d0ec9d1dddb173f772c441dc0a1a. Revert "Add i10top_correct_and_bounded" This reverts commit bc4184ce6086971799630a0419881c8d344811ca. Revert "Add appify10" This reverts commit 66b63b406d9c78a0cecbbf89e5baf282231215c5.
* Add i10top_correct_and_boundedGravatar Jason Gross2017-01-07
|
* Add appify10Gravatar Jason Gross2017-01-07
| | | | Grrrrrr, code duplication for ladderstep
* Minor change to inm_op_correct_and_bounded_prefixGravatar Jason Gross2016-11-25
|
* Fix a typoGravatar Jason Gross2016-11-25
|
* Add inm_op_correct_and_bounded_iff_prefixGravatar Jason Gross2016-11-25
|
* Add inm_op_correct_and_boundedGravatar Jason Gross2016-11-25
|
* Update AddCoordinatesGravatar Jason Gross2016-11-17
| | | | Now the _correct_and_bounded lemma goes through
* Fix postfreezeW_correct_and_boundedGravatar Jason Gross2016-11-14
|
* Speed up some GF25519 tacticsGravatar Jason Gross2016-11-14
|
* Begin filling in @JasonGross's stubsGravatar jadep2016-11-11
|
* Remove 8.6 only syntaxGravatar Jason Gross2016-11-11
|
* Freeze stubsGravatar Jason Gross2016-11-11
|
* 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.
* Add eta-expansion in GF25519BoundedCommon.vGravatar Jason Gross2016-11-05
| | | | It'll be needed to vm_compute some proofs in GF25519Reflective/Reified/*
* Add unfold_is_boundedGravatar Jason Gross2016-11-05
|
* 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
|
* Prove fe25519WToZ_ZToW, rename FooToBarToFoo to BarToFoo_FooToBarGravatar Jason Gross2016-11-01
| | | | The renaming brings things in line with the rest of the library
* 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)
* 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)
* Simplify proof of proj1_fe25519_encodeGravatar Jason Gross2016-10-27
|
* Add lemmas about GF25519BoundedCommon.{encode,decode}Gravatar Jason Gross2016-10-27
|
* Switch to bounded ZGravatar Jason Gross2016-10-25
| | | | | We don't have working word code yet, because the reification code currently does spurious word->N->Z->N->word conversions everywhere. So we use Z instead.
* Adjust bound on final word in wire_digits to 31Gravatar Jason Gross2016-10-24
|
* Fix bounds on wire_digitsGravatar Jason Gross2016-10-24
| | | | | As per https://github.com/mit-plv/fiat-crypto/pull/86#issuecomment-255839706
* Add pack, unpack, ge_modulus to axioms to be reifiedGravatar Jason Gross2016-10-24
|
* Add decode to GF25519BoundedCommonGravatar Jason Gross2016-10-22
|
* Make [vm_compute] on Bounded word reasonableGravatar Jason Gross2016-10-22
| | | | We no longer store the type of proofs of [<=] in the term itself; this makes it amenable to vm_compute
* Add word64eqb_ZeqbGravatar Jason Gross2016-10-21
|
* A bit of initial setup on correct_and_bounded proofs in ↵Gravatar Jason Gross2016-10-20
| | | | GF25519BoundedInstantiation
* Plug bounded into assembly stuffGravatar Jason Gross2016-10-20
|
* Split up GF25519Bounded to avoid circular dependenciesGravatar Jason Gross2016-10-20
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-01 05:27:54 +0000