aboutsummaryrefslogtreecommitdiff
path: root/src
Commit message (Collapse)AuthorAge
...
| * automate a proofGravatar Andres Erbsen2016-07-20
| |
| * compute on [F q]!Gravatar Andres Erbsen2016-07-20
| |
| * experiments wd25519: simplify proof for aGravatar Andres Erbsen2016-07-20
| |
* | Merge branch 'master' of github.com:mit-plv/fiat-cryptoGravatar jadep2016-07-20
|\|
* | mergeGravatar jadep2016-07-20
|\ \
| | * Move mul_rep_extended (do we actually care about this?)Gravatar Jason Gross2016-07-20
| |/
| * Don't use auto with *Gravatar Jason Gross2016-07-20
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | It's fragile and slow. Now we're 45 seconds faster. After | File Name | Before || Change ------------------------------------------------------------------------------- 1m03.42s | Total | 1m49.00s || -0m45.57s ------------------------------------------------------------------------------- 0m20.01s | ModularArithmetic/ModularBaseSystemProofs | 1m05.69s || -0m45.67s 0m32.14s | Specific/GF25519 | 0m31.92s || +0m00.21s 0m07.05s | Specific/GF1305 | 0m07.07s || -0m00.02s 0m02.84s | ModularArithmetic/ModularBaseSystemOpt | 0m02.90s || -0m00.06s 0m00.69s | Experiments/SpecificCurve25519 | 0m00.69s || +0m00.00s 0m00.69s | ModularArithmetic/ModularBaseSystemInterface | 0m00.73s || -0m00.04s
* | restructured ModularBaseSystem pipeline to put tuple conversion before ↵Gravatar jadep2016-07-20
| | | | | | | | ModularBaseSystem is fully defined, rather than after ModularBaseSystemOpt
| * Absolutize some importsGravatar Jason Gross2016-07-20
| |
| * Remove dependency of ext_base on pseudomersenneGravatar Jason Gross2016-07-20
| |
| * Add Z.lt_le_incl to zarithGravatar Jason Gross2016-07-20
| |
| * Add another lemma about +, <= to arithGravatar Jason Gross2016-07-20
| |
| * Use a proof that doesn't require as many assumptions in extended_base_lengthGravatar Jason Gross2016-07-20
| |
| * Work around bad design in CoqGravatar Jason Gross2016-07-19
| | | | | | | | | | This is https://coq.inria.fr/bugs/show_bug.cgi?id=4949, [intuition] should not use [auto with *] by default
| * Add a distr_length databaseGravatar Jason Gross2016-07-19
| |
| * Remove stuff from PseudoMersenneBaseParamProofs.vGravatar Jason Gross2016-07-19
| |
| * {base} -> baseGravatar Jason Gross2016-07-19
| |
| * Move two_k_nonzero to PseudoMersenneBaseParamProofs.vGravatar Jason Gross2016-07-19
| | | | | | | | It has nothing to do with ext_base
| * Fix side-condition from previous commitGravatar Jason Gross2016-07-19
| |
| * Add another lemma to distr_lengthGravatar Jason Gross2016-07-19
| |
* | mergeGravatar jadep2016-07-19
|\|
* | Converted non-canonicalization sections of ModularBaseSystemProofs to tuples.Gravatar jadep2016-07-19
| |
| * Use update_nth in add_to_nth (#26)Gravatar Jason Gross2016-07-19
| | | | | | | | | | | | It leads to a slightly more transparent and clearer definition. If I got everything right, nothing should depend on the judgmental definition of [add_to_nth] anymore.
* | mergeGravatar jadep2016-07-19
|\ \
| | * ext_base: now defined in terms of ext_limb_widthsGravatar Jason Gross2016-07-18
| | |
| | * Add a lemma about base_from_limb_widths and appGravatar Jason Gross2016-07-18
| | |
| | * Add a lemma about sum_firstnGravatar Jason Gross2016-07-18
| | |
| | * Add a ListUtil lemmaGravatar Jason Gross2016-07-18
| | |
| | * Move more proofs earlierGravatar Jason Gross2016-07-18
| | |
| | * Make Pow2BaseProofs independent of the def of add_to_nthGravatar Jason Gross2016-07-18
| | |
| | * Silence a warningGravatar Jason Gross2016-07-18
| | | | | | | | | | | | | | | | | | | | | | | | | | | File "./src/Experiments/GenericFieldPow.v", line 130, characters 4-471: Warning: Casts are ignored in patterns [cast-in-pattern,automation] @andres-erbsen Did you intend for the cast at https://github.com/mit-plv/fiat-crypto/commit/6823b63275333ebb11c7f84068894f76cdb06068#diff-078114b2627a38e74938989c7ca2f6d1R131 to have semantic meaning for some reason, performance or otherwise?
| | * Express carry_simple in terms of carry_genGravatar Jason Gross2016-07-18
| | | | | | | | | | | | | | | | | | Also make much of the remaining code outside of Pow2BaseProofs independent of the precise definition of carry_simple. (We use [Local Opaque] to enforce this modularity.
| | * Fix for Coq 8.4 (missing lemmas)Gravatar Jason Gross2016-07-18
| | |
| | * Fix for Coq 8.4 (omega used to be weaker)Gravatar Jason Gross2016-07-18
| | |
| | * Add more distr_length proofs in BaseSystemProofsGravatar Jason Gross2016-07-18
| | |
| | * Add more natsimplify le_dec lemmasGravatar Jason Gross2016-07-18
| | |
| | * Add more NatUtil lemmasGravatar Jason Gross2016-07-18
| | |
| | * Add natsimplify lemmas about eq_nat_decGravatar Jason Gross2016-07-18
| | |
| | * Fix some typos in the previous commitGravatar Jason Gross2016-07-18
| | |
| | * Add some lemmas about nth_default in boundsGravatar Jason Gross2016-07-18
| | |
| | * Remove a nested proofGravatar Jason Gross2016-07-18
| |/ | | | | | | | | Fix for Warning: Nested proofs are deprecated and will stop working in a future Coq version [deprecated-nested-proofs,deprecated]
* | changed base notationGravatar jadep2016-07-18
| |
| * Move some definitions to Pow2Base (#24)Gravatar Jason Gross2016-07-18
|/ | | | | | | | | * Move some definitions to Pow2Base These definitions don't depend on PseudoMersenneBaseParams, only on limb_widths, and we'll want them for BarrettReduction / P256. * Fix for Coq 8.4
* ported IterAssocOp to use monoid rather than a billion context variables ↵Gravatar jadep2016-07-18
| | | | that add up to a monoid
* rewrote Testbit and factored out some necessary lemmas about 'uniform' bases ↵Gravatar jadep2016-07-18
| | | | (bases that are repeats of the same power of 2) into Pow2Base
* Added lemmas to ZUtil and NatUtil (for Testbit)Gravatar jadep2016-07-18
|
* Fixed unsimplified multiplication definitions in Specific by separating out ↵Gravatar jadep2016-07-18
| | | | the zsimplify step; after inserting clauses, we can't rewrite under the binders, but we can do the rewrite and insertions in different definitions.
* Merge branch 'master' of github.com:mit-plv/fiat-cryptoGravatar jadep2016-07-15
|\
* | proved an admit in field homomorphisms that turned out to be unprovable; I ↵Gravatar jadep2016-07-15
| | | | | | | | added another precondition and pushed it through everywhere but one place in ExtendedCoordinates, where I was stuck.
* | more changes to Specific for 8.4 compatibilityGravatar jadep2016-07-15
| |
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-18 21:26:39 +0000