aboutsummaryrefslogtreecommitdiff
path: root/src/ModularArithmetic
Commit message (Expand)AuthorAge
* PrimeFieldTheorems: inv for isomorphic fieldsGravatar Andres Erbsen2017-03-02
* use [positive] for [F] modulus, char_ge_C instead of char_gt_CGravatar Andres Erbsen2017-03-02
* split the algebra library; use fsatz moreGravatar Andres Erbsen2017-03-02
* Handle more kinds of ops in fixed_size_op_to_wordGravatar Jason Gross2017-02-03
* Only unfold the non-zpecialized versions of wcmovl, wcmovne, wnegGravatar Jason Gross2017-02-03
* Also unfold wcmovl, wcmovne, wneg in fixed_size_constantsGravatar Jason Gross2017-02-03
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-10 21:33:15 +0000