aboutsummaryrefslogtreecommitdiff
path: root/src/ModularArithmetic
Commit message (Expand)AuthorAge
* Better word operationsGravatar Jason Gross2017-01-03
* Add word versions of ModularBaseSystemListZOperationsGravatar Jason Gross2017-01-03
* Update bounds things with prefreezeGravatar Jason Gross2016-11-14
* Proper_sqrt_3mod4 Proper_sqrt_5mod8Gravatar Andres Erbsen2016-11-13
* Define word version of conditional subtractionGravatar jadep2016-11-11
* separate freeze into two partsGravatar jadep2016-11-11
* Remove special code for reified conditional subGravatar Jason Gross2016-11-11
* Silence a warning about name collisionGravatar Jason Gross2016-11-09
* Prove things in ModularBaseSystemListZOperationsProofsGravatar Jason Gross2016-11-08
* Factor related_Z_op (except conditional_sub)Gravatar Jason Gross2016-11-08
* Preliminary support: conditional sub as primitiveGravatar Jason Gross2016-11-06
* Fix 8.4 build partiallyGravatar Jason Gross2016-11-03
* Make [freeze] proofs consider machine integer width and hard input bounds sep...Gravatar jadep2016-11-03
* Lift conversion correctness proofs to ModularBaseSystem by providing [pack_re...Gravatar jadep2016-11-02
* Changes to sqrt for easier bounds proofs; currently blocked on broken proof i...Gravatar jadep2016-11-02
* Progress proving ERepDec_correct (included tweaking preconditions for Modular...Gravatar jadep2016-11-02
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-16 07:49:05 +0000