aboutsummaryrefslogtreecommitdiff
path: root/src/ModularArithmetic
Commit message (Expand)AuthorAge
* remove commented-out lemmaGravatar jadep2016-10-30
* revived accidentally deleted lemmaGravatar jadep2016-10-30
* 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
* Slightly loosen freeze preconditions (in particular, I had failed to properly...Gravatar jadep2016-10-27
* 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 poi...Gravatar jadep2016-10-19
* 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 re...Gravatar jadep2016-10-12
* 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
* 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
|\
* | Finished remaining admits in [freeze] proofsGravatar jadep2016-09-23
| * Drop CSE from Fancy MachineGravatar Jason Gross2016-09-22
|/
* alternative signing derivationGravatar Andres Erbsen2016-09-22
* Reorganization, moving of lemmas to correct files, and 8.4 compatibilityGravatar jadep2016-09-21
* Proved specification of constant-time modulus comparison (except for one ZUti...Gravatar jadep2016-09-21
* 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
* Move side lemmas to appropriate filesGravatar jadep2016-09-17
* Partially flesh out [freeze] proofs; also parameterize [sqrt_5mod8] over impl...Gravatar jadep2016-09-17
* Proved bounds for [encode] results; fleshed out some structure for [freeze] p...Gravatar jadep2016-09-17
* 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 s...Gravatar jadep2016-09-13
* 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
* Better spec in Montgomery.ZBoundedGravatar Jason Gross2016-09-07
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-03 19:36:41 +0000