aboutsummaryrefslogtreecommitdiff
Commit message (Collapse)AuthorAge
* Add a ListUtil lemmaGravatar Jason Gross2016-07-08
|
* Add Z.div_0_l to ZUtilGravatar Jason Gross2016-07-08
|
* Fix ListUtil for Coq 8.4Gravatar Jason Gross2016-07-08
| | | | | [rewrite_strat] ignores [using tac] sometimes, and [Hint Rewrite] only accepts one database in 8.4.
* Add update_nth out of boundsGravatar Jason Gross2016-07-07
|
* Add hint db in ListUtilGravatar Jason Gross2016-07-07
|
* More ListUtil factsGravatar Jason Gross2016-07-07
|
* Slightly better arguments in ListUtilGravatar Jason Gross2016-07-07
|
* Correct hintdb namesGravatar Jason Gross2016-07-07
|
* Add more about firstn to listutilGravatar Jason Gross2016-07-07
|
* Add more update_nth to ListUtilGravatar Jason Gross2016-07-07
|
* Fix ListUtil for Coq 8.4Gravatar Jason Gross2016-07-07
|
* Add pow2_mod to ZUtilGravatar Jason Gross2016-07-07
|
* Changed [auto]s to [eauto]s in ModularBaseSystemProofs for 8.5 compatibility.Gravatar jadep2016-07-07
|
* Merge branch 'master' of github.com:mit-plv/fiat-cryptoGravatar jadep2016-07-07
|\
| * Fix notations, add &Gravatar Jason Gross2016-07-06
| |
| * Add [update_nth] to ListUtil, change [set_nth]Gravatar Jason Gross2016-07-06
| | | | | | | | Define [set_nth] in terms of [update_nth]
| * Add notations for Z.shift{r,l} to ZUtilGravatar Jason Gross2016-07-06
| |
| * Improve some reserved notationsGravatar Jason Gross2016-07-06
| | | | | | | | Compatibility with theories/Numbers/NatInt/NZBits.v
| * Add a TODO commentGravatar Jason Gross2016-07-06
| | | | | | | | For jadep, or for me, after the 8.5 build is fixed.
* | Proved lingering lemmas in PointEncodingPre.Gravatar jadep2016-07-06
| |
| * Clean up the makefile a bitGravatar Jason Gross2016-07-06
| |
| * Fix coqprime clean, install targets, add cleanallGravatar Jason Gross2016-07-06
| |
| * Fix for broken 8.5 build in ListUtilGravatar Jason Gross2016-07-06
|/
* fixed indentation for new lemmas in ZUtilGravatar jadep2016-07-06
|
* Merged changes, including new ZUtil conventions.Gravatar jadep2016-07-06
|\
* \ Merge branch 'master' of github.mit.edu:plv/fiat-cryptoGravatar jadep2016-07-06
|\ \
* | | Factored out some proofs that rely only on base being powers of two, and ↵Gravatar jadep2016-07-06
| | | | | | | | | | | | defined conversion between two such bases. This will allow conversion between the pseudomersenne base representation and the wire format. Also relocated some lemmas to Util.
| | * Define the spec of Weierstrass curves (#6)Gravatar Jason Gross2016-07-03
| | | | | | | | | | | | | | | Define the spec of Weierstrass curves This is the start of work on P256.
| | * Implement and prove Barrett reduction on Z (#18)Gravatar Jason Gross2016-07-03
| | | | | | | | | | | | | | | | | | | | | | | | Implement and prove Barrett reduction on Z This will serve as the high-level algorithm for modular reduction. We follow Wikipedia very closely, except where we can do better (I believe @jadephilipoom is updating Wikipedia).
| | * Merge pull request #19 from JasonGross/rename-z-lemmasGravatar Jason Gross2016-07-03
| | |\ | | | | | | | | Rename lemmas about Z in ZUtil
| | * \ Merge pull request #12 from mit-plv/licenseGravatar Andres Erbsen2016-07-02
| | |\ \ | | | | | | | | | | update licensing information for #5
| | | | * Indentation in ZUtilGravatar Jason Gross2016-07-02
| | | | |
| | | | * Make ZUtil more uniformGravatar Jason Gross2016-07-02
| | | |/ | | |/| | | | | | | | | | | | | | | | | | | | | | | | | The standard library uses Z.*, and Z* and Z_* are compatibility notations. We follow suit. Also, eliminate a few lemmas that are duplicates of ones in the standard library.
| | * | super_nsatz: Handle x^2 = y^2 -> x <> -y -> x = yGravatar Jason Gross2016-07-02
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | After | File Name | Before || Change ------------------------------------------------------------------------------------ 2m38.35s | Total | 2m36.78s || +0m01.57s ------------------------------------------------------------------------------------ 0m27.68s | Specific/GF25519 | 0m27.26s || +0m00.41s 0m25.00s | CompleteEdwardsCurve/ExtendedCoordinates | 0m24.87s || +0m00.12s 0m24.96s | ModularArithmetic/ModularBaseSystemProofs | 0m24.84s || +0m00.12s 0m21.55s | Experiments/SpecEd25519 | 0m21.39s || +0m00.16s 0m19.82s | CompleteEdwardsCurve/CompleteEdwardsCurveTheorems | 0m19.65s || +0m00.17s 0m08.29s | ModularArithmetic/PrimeFieldTheorems | 0m08.30s || -0m00.01s 0m07.13s | Specific/GF1305 | 0m06.69s || +0m00.43s 0m03.75s | ModularArithmetic/Tutorial | 0m03.77s || -0m00.02s 0m03.69s | ModularArithmetic/ModularBaseSystemOpt | 0m03.71s || -0m00.02s 0m03.64s | CompleteEdwardsCurve/Pre | 0m03.67s || -0m00.02s 0m02.11s | Algebra | 0m01.96s || +0m00.14s 0m01.81s | Experiments/DerivationsOptionRectLetInEncoding | 0m01.83s || -0m00.02s 0m01.73s | Experiments/EdDSARefinement | 0m01.71s || +0m00.02s 0m01.67s | ModularArithmetic/ModularArithmeticTheorems | 0m01.65s || +0m00.02s 0m00.91s | ModularArithmetic/ExtendedBaseVector | 0m00.92s || -0m00.01s 0m00.80s | ModularArithmetic/PseudoMersenneBaseParamProofs | 0m00.85s || -0m00.04s 0m00.60s | Encoding/ModularWordEncodingPre | 0m00.59s || +0m00.01s 0m00.59s | Encoding/ModularWordEncodingTheorems | 0m00.61s || -0m00.02s 0m00.58s | ModularArithmetic/ModularBaseSystem | 0m00.52s || +0m00.05s 0m00.57s | Spec/ModularWordEncoding | 0m00.53s || +0m00.03s 0m00.56s | Spec/EdDSA | 0m00.56s || +0m00.00s 0m00.56s | ModularArithmetic/PseudoMersenneBaseRep | 0m00.54s || +0m00.02s 0m00.36s | Spec/CompleteEdwardsCurve | 0m00.36s || +0m00.00s
| | * | Fix for 8.4 evarsGravatar Jason Gross2016-07-01
| | | |
| | * | Add ZUtil hintsGravatar Jason Gross2016-07-01
| | | |
| | * | Add more hints to ZUtilGravatar Jason Gross2016-07-01
| | | |
| | * | Add more hints in ZUtilGravatar Jason Gross2016-07-01
| | | |
| | * | Add more ZUtil hintsGravatar Jason Gross2016-07-01
| | | |
| | * | Add more hints to ZUtilGravatar Jason Gross2016-07-01
| | | |
| | * | Simplify a proof that no longer needs more hintsGravatar Jason Gross2016-07-01
| | | | | | | | | | | | | | | | [intuition] is overpowered and does [auto with *] or something
| | * | Add hint databases and a proof about Z.log2Gravatar Jason Gross2016-07-01
| | | |
| | * | Add some proofs about Z.div and Z.mulGravatar Jason Gross2016-07-01
| | | |
| | * | Add [specialize_by] tacticGravatar Jason Gross2016-07-01
| | | |
| | * | Fix a typo in Zsplit_sumsGravatar Jason Gross2016-07-01
| | | |
| | * | Add tactic to split sums and differences in inequalitiesGravatar Jason Gross2016-07-01
| | | |
| | * | Add more caches to .gitignore (nra, csdp)Gravatar Jason Gross2016-07-01
| | | |
| | * | Add fraction inequality reasoning tactics to ZUtilGravatar Jason Gross2016-07-01
| | | |
| | * | Update .gitignore with lia, nia cachesGravatar Jason Gross2016-07-01
| | | |
| | * | Add a proof of 2 * x - x = xGravatar Jason Gross2016-06-30
| | | |
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-01 14:17:18 +0000