| Commit message (Expand) | Author | Age |
* | PrimeFieldTheorems: inv for isomorphic fields | Andres Erbsen | 2017-03-02 |
* | use [positive] for [F] modulus, char_ge_C instead of char_gt_C | Andres Erbsen | 2017-03-02 |
* | split the algebra library; use fsatz more | Andres Erbsen | 2017-03-02 |
* | Handle more kinds of ops in fixed_size_op_to_word | Jason Gross | 2017-02-03 |
* | Only unfold the non-zpecialized versions of wcmovl, wcmovne, wneg | Jason Gross | 2017-02-03 |
* | Also unfold wcmovl, wcmovne, wneg in fixed_size_constants | Jason Gross | 2017-02-03 |
* | Better word operations | Jason Gross | 2017-01-03 |
* | Add word versions of ModularBaseSystemListZOperations | Jason Gross | 2017-01-03 |
* | Update bounds things with prefreeze | Jason Gross | 2016-11-14 |
* | Proper_sqrt_3mod4 Proper_sqrt_5mod8 | Andres Erbsen | 2016-11-13 |
* | Define word version of conditional subtraction | jadep | 2016-11-11 |
* | separate freeze into two parts | jadep | 2016-11-11 |
* | Remove special code for reified conditional sub | Jason Gross | 2016-11-11 |
* | Silence a warning about name collision | Jason Gross | 2016-11-09 |
* | Prove things in ModularBaseSystemListZOperationsProofs | Jason Gross | 2016-11-08 |
* | Factor related_Z_op (except conditional_sub) | Jason Gross | 2016-11-08 |
* | Preliminary support: conditional sub as primitive | Jason Gross | 2016-11-06 |
* | Fix 8.4 build partially | Jason Gross | 2016-11-03 |
* | Make [freeze] proofs consider machine integer width and hard input bounds sep... | jadep | 2016-11-03 |
* | Lift conversion correctness proofs to ModularBaseSystem by providing [pack_re... | jadep | 2016-11-02 |
* | Changes to sqrt for easier bounds proofs; currently blocked on broken proof i... | jadep | 2016-11-02 |
* | Progress proving ERepDec_correct (included tweaking preconditions for Modular... | jadep | 2016-11-02 |
* | remove commented-out lemma | jadep | 2016-10-30 |
* | revived accidentally deleted lemma | jadep | 2016-10-30 |
* | proved feSign_correct | jadep | 2016-10-29 |
* | prove testbit_sub_pow2 | Andres Erbsen | 2016-10-29 |
* | prove admit about F.to_nat x mod m | Andres Erbsen | 2016-10-27 |
* | Fix a missing import in previous commit | Jason Gross | 2016-10-27 |
* | Factor out cmov{l,ne} and neg | Jason Gross | 2016-10-27 |
* | Slightly loosen freeze preconditions (in particular, I had failed to properly... | jadep | 2016-10-27 |
* | add extra convenience lemmas about boundedness of convert | jadep | 2016-10-27 |
* | Created separate definitions for cmovne and cmovl for reification | jadep | 2016-10-23 |
* | final touches/fixes for freeze restructuring | jadep | 2016-10-22 |
* | Modified [freeze] to be more reifyable | jadep | 2016-10-22 |
* | Removed the lingering TODO and print statement that @JasonGross helpfully poi... | jadep | 2016-10-19 |
* | Fill in admits for field with carry_add, carry_opp, and carry_sub | jadep | 2016-10-19 |
* | Define carry_opp in terms of carry_sub | Jason Gross | 2016-10-19 |
* | Add opt versions of add, sub, opp | Jason Gross | 2016-10-19 |
* | Fix a proof | Jason Gross | 2016-10-16 |
* | Don't inline as much in ZBoundedZ | Jason Gross | 2016-10-16 |
* | Add Z as ZBounded | Jason Gross | 2016-10-16 |
* | Added top-level modulus comparison operation so field-element decoding can re... | jadep | 2016-10-12 |
* | Bundle arguments to Barrett Reduction | Jason Gross | 2016-10-10 |
* | Fix compatibility with sigT notation | Jason Gross | 2016-10-10 |
* | More zsimplify lemmas, stronger Ztestbit | Jason Gross | 2016-10-07 |
* | Moved lemma to ZUtil and added an extra lemma jgross needed | jadep | 2016-10-06 |
* | Moved conversion logic out of Pow2BaseProofs into its own file | jadep | 2016-10-06 |
* | map -> List.map (not Tuple.map) | Jason Gross | 2016-09-29 |
* | Merge pull request #69 from JasonGross/scalable-scalars | Jason Gross | 2016-09-26 |
|\ |
|
* | | Finished remaining admits in [freeze] proofs | jadep | 2016-09-23 |