aboutsummaryrefslogtreecommitdiff
path: root/src/ModularArithmetic
Commit message (Collapse)AuthorAge
* proved feSign_correctGravatar jadep2016-10-29
|
* prove testbit_sub_pow2Gravatar Andres Erbsen2016-10-29
|
* prove admit about F.to_nat x mod mGravatar Andres Erbsen2016-10-27
|
* Fix a missing import in previous commitGravatar Jason Gross2016-10-27
|
* Factor out cmov{l,ne} and negGravatar Jason Gross2016-10-27
| | | | This way we will have a faster build of reification things
* Slightly loosen freeze preconditions (in particular, I had failed to ↵Gravatar jadep2016-10-27
| | | | properly account for the case when which [n] and [pred n] are BOTH out of bounds in my statement of initial bounds)
* add extra convenience lemmas about boundedness of convertGravatar jadep2016-10-27
|
* Created separate definitions for cmovne and cmovl for reificationGravatar jadep2016-10-23
|
* final touches/fixes for freeze restructuringGravatar jadep2016-10-22
|
* Modified [freeze] to be more reifyableGravatar jadep2016-10-22
|
* Removed the lingering TODO and print statement that @JasonGross helpfully ↵Gravatar jadep2016-10-19
| | | | pointed out
* Fill in admits for field with carry_add, carry_opp, and carry_subGravatar jadep2016-10-19
|
* Define carry_opp in terms of carry_subGravatar Jason Gross2016-10-19
|
* Add opt versions of add, sub, oppGravatar Jason Gross2016-10-19
|
* Fix a proofGravatar Jason Gross2016-10-16
|
* Don't inline as much in ZBoundedZGravatar Jason Gross2016-10-16
|
* Add Z as ZBoundedGravatar Jason Gross2016-10-16
|
* Added top-level modulus comparison operation so field-element decoding can ↵Gravatar jadep2016-10-12
| | | | return None if input is greater than modulus
* Bundle arguments to Barrett ReductionGravatar Jason Gross2016-10-10
|
* Fix compatibility with sigT notationGravatar Jason Gross2016-10-10
|
* More zsimplify lemmas, stronger ZtestbitGravatar Jason Gross2016-10-07
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | After | File Name | Before || Change ---------------------------------------------------------------------------------- 5m47.85s | Total | 5m48.53s || -0m00.67s ---------------------------------------------------------------------------------- 1m34.28s | Test/Curve25519SpecTestVectors | 1m35.44s || -0m01.15s 0m35.79s | ModularArithmetic/Conversion | 0m36.48s || -0m00.68s 0m27.42s | ModularArithmetic/ModularBaseSystemProofs | 0m28.32s || -0m00.89s 0m22.15s | BoundedArithmetic/DoubleBoundedProofs | 0m21.67s || +0m00.47s 0m21.62s | ModularArithmetic/Pow2BaseProofs | 0m21.38s || +0m00.24s 0m19.60s | EdDSARepChange | 0m19.98s || -0m00.37s 0m14.52s | Specific/GF25519 | 0m14.89s || -0m00.37s 0m12.99s | Util/ZUtil | 0m12.60s || +0m00.39s 0m09.80s | Testbit | 0m09.45s || +0m00.35s 0m08.85s | ModularArithmetic/Montgomery/ZProofs | 0m08.11s || +0m00.74s 0m08.21s | BoundedArithmetic/ArchitectureToZLikeProofs | 0m08.57s || -0m00.35s 0m07.85s | Encoding/PointEncoding | 0m08.24s || -0m00.39s 0m07.71s | Specific/GF1305 | 0m07.87s || -0m00.16s 0m03.94s | BaseSystemProofs | 0m03.85s || +0m00.08s 0m03.93s | ModularArithmetic/BarrettReduction/ZHandbook | 0m03.64s || +0m00.29s 0m03.52s | ModularArithmetic/Tutorial | 0m03.35s || +0m00.16s 0m03.48s | ModularArithmetic/ModularBaseSystemListProofs | 0m03.58s || -0m00.10s 0m03.36s | BoundedArithmetic/InterfaceProofs | 0m03.18s || +0m00.17s 0m03.16s | ModularArithmetic/BarrettReduction/ZGeneralized | 0m02.89s || +0m00.27s 0m02.80s | Encoding/PointEncodingPre | 0m02.87s || -0m00.07s 0m02.65s | ModularArithmetic/ModularArithmeticTheorems | 0m02.59s || +0m00.06s 0m02.48s | ModularArithmetic/BarrettReduction/ZBounded | 0m02.32s || +0m00.16s 0m02.36s | ModularArithmetic/ModularBaseSystemOpt | 0m02.35s || +0m00.00s 0m02.24s | Specific/FancyMachine256/Montgomery | 0m02.01s || +0m00.23s 0m02.14s | Specific/FancyMachine256/Barrett | 0m02.11s || +0m00.03s 0m01.89s | Specific/FancyMachine256/Core | 0m01.68s || +0m00.20s 0m01.86s | ModularArithmetic/Montgomery/ZBounded | 0m01.83s || +0m00.03s 0m01.55s | ModularArithmetic/BarrettReduction/Z | 0m01.50s || +0m00.05s 0m01.27s | ModularArithmetic/PrimeFieldTheorems | 0m01.36s || -0m00.09s 0m01.26s | BaseSystem | 0m01.35s || -0m00.09s 0m01.12s | ModularArithmetic/ExtendedBaseVector | 0m01.17s || -0m00.04s 0m00.92s | Util/NumTheoryUtil | 0m00.87s || +0m00.05s 0m00.89s | Experiments/EncodingLemmas | 0m00.84s || +0m00.05s 0m00.67s | Encoding/ModularWordEncodingTheorems | 0m00.64s || +0m00.03s 0m00.66s | ModularArithmetic/PseudoMersenneBaseParamProofs | 0m00.74s || -0m00.07s 0m00.64s | Spec/EdDSA | 0m00.58s || +0m00.06s 0m00.60s | ModularArithmetic/ExtPow2BaseMulProofs | 0m00.63s || -0m00.03s 0m00.60s | Encoding/ModularWordEncodingPre | 0m00.60s || +0m00.00s 0m00.60s | ModularArithmetic/ModularBaseSystem | 0m00.61s || -0m00.01s 0m00.59s | BoundedArithmetic/Interface | 0m00.62s || -0m00.03s 0m00.58s | ModularArithmetic/ModularBaseSystemList | 0m00.60s || -0m00.02s 0m00.56s | Spec/Ed25519 | 0m00.55s || +0m00.01s 0m00.55s | Spec/ModularWordEncoding | 0m00.59s || -0m00.03s 0m00.54s | BoundedArithmetic/StripCF | 0m00.44s || +0m00.10s 0m00.52s | ModularArithmetic/ZBounded | 0m00.44s || +0m00.08s 0m00.49s | ModularArithmetic/PseudoMersenneBaseParams | 0m00.37s || +0m00.12s 0m00.48s | BoundedArithmetic/DoubleBounded | 0m00.53s || -0m00.05s 0m00.47s | ModularArithmetic/Pre | 0m00.47s || +0m00.00s 0m00.46s | BoundedArithmetic/ArchitectureToZLike | 0m00.50s || -0m00.03s 0m00.43s | ModularArithmetic/Pow2Base | 0m00.44s || -0m00.01s 0m00.42s | Spec/ModularArithmetic | 0m00.38s || +0m00.03s 0m00.38s | ModularArithmetic/Montgomery/Z | 0m00.46s || -0m00.08s
* Moved lemma to ZUtil and added an extra lemma jgross neededGravatar jadep2016-10-06
|
* Moved conversion logic out of Pow2BaseProofs into its own fileGravatar jadep2016-10-06
|
* map -> List.map (not Tuple.map)Gravatar Jason Gross2016-09-29
|
* Merge pull request #69 from JasonGross/scalable-scalarsGravatar Jason Gross2016-09-26
|\ | | | | Scalable Scalars, Dead Code Removal, Register Assignment
* | Finished remaining admits in [freeze] proofsGravatar jadep2016-09-23
| |
| * Drop CSE from Fancy MachineGravatar Jason Gross2016-09-22
|/ | | | | By being careful about building the expressions in the first place, we no longer need it, and can rely on dead code elimination.
* alternative signing derivationGravatar Andres Erbsen2016-09-22
| | | | cleanup
* Reorganization, moving of lemmas to correct files, and 8.4 compatibilityGravatar jadep2016-09-21
|
* Proved specification of constant-time modulus comparison (except for one ↵Gravatar jadep2016-09-21
| | | | ZUtil lemma)
* Fix the 8.4 build by changing a couple standard library namesGravatar jadep2016-09-18
|
* Add reserved notation for Let, change #Gravatar Jason Gross2016-09-17
| | | | | We reserve [a # b] in Notations.v, and make it's level compatible with the notation declared in the std lib for Q.
* Move side lemmas to appropriate filesGravatar jadep2016-09-17
|
* Partially flesh out [freeze] proofs; also parameterize [sqrt_5mod8] over ↵Gravatar jadep2016-09-17
| | | | implementations of [mul] and [pow] so bounds can be threaded through
* Proved bounds for [encode] results; fleshed out some structure for [freeze] ↵Gravatar jadep2016-09-17
| | | | proofs; bundled [freeze] preconditions.
* Fix missing parenthesisGravatar jadep2016-09-17
|
* Remove unused lemma and standardized use of notations for [freeze] proofsGravatar jadep2016-09-17
|
* deduplicate Let_In into src/Util/LetIn.vGravatar Andres Erbsen2016-09-17
|
* ModularArithmetic: conversions between [F] and [nat]Gravatar Andres Erbsen2016-09-16
|
* Tweaked automation for 8.4 compatibilityGravatar jadep2016-09-14
|
* Automated and cleaned up [freeze] carry-loop proofsGravatar jadep2016-09-13
|
* Update old carry loop bounds proof; now is automated and also has analogous ↵Gravatar jadep2016-09-13
| | | | structure to subsequent carry loop proofs
* Moved lemmas to ZUtilGravatar jadep2016-09-13
|
* Finished off last admits for proofs of bounds after 3 carry loops.Gravatar jadep2016-09-13
|
* [freeze] proofs : Mostly-complete proofs of bounds after 3 carry loopsGravatar jadep2016-09-13
|
* [freeze] proofs : proved bounds for second carry loop.Gravatar jadep2016-09-13
|
* Fully qualify [Require]sGravatar Jason Gross2016-09-08
| | | | This way they won't become ambiguous if we add new files
* Better spec in Montgomery.ZBoundedGravatar Jason Gross2016-09-07
|
* Finished sqrt in GF25519Gravatar jadep2016-09-06
|
* Pushed [freeze] through to GF25519 in preparation for defining [sqrt], ↵Gravatar jadep2016-09-06
| | | | cleaning up freeze-related organization and definitions along the way
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-06 04:53:54 +0000