aboutsummaryrefslogtreecommitdiff
path: root/src
Commit message (Expand)AuthorAge
* Add String_as_OTGravatar Jason Gross2019-01-15
* Ensure that we only left-shift on unsigned valuesGravatar Jason Gross2019-01-15
* Fix computation of INTX_MINGravatar Jason Gross2019-01-15
* Don't cast signed to unsigned before shiftingGravatar Jason Gross2019-01-15
* We don't need to encode c with taps in WBW montgomeryGravatar Jason Gross2019-01-14
* Autocompute s and c in WBW MontgomeryGravatar Jason Gross2019-01-14
* remove old pipelineGravatar Andres Erbsen2019-01-09
* move src/Experiments/NewPipeline/ to src/Gravatar Andres Erbsen2019-01-09
* Fix for 8.7Gravatar Jason Gross2019-01-07
* Merge remote-tracking branch 'origin/fix_fancy4'Gravatar Andres Erbsen2019-01-07
|\
* | Update README.mdGravatar Jason Gross2019-01-05
* | prove admitGravatar Andres Erbsen2019-01-05
* | build on Coq masterGravatar Andres Erbsen2019-01-05
* | new pipeline: refactor glue, split into more filesGravatar Jason Gross2019-01-05
| * Update fancy rewriter output with new compilation outputGravatar Jason Gross2019-01-03
| * Finish proving fancy rewrite rulesGravatar Jason Gross2019-01-03
| * Fix bounds checking on shiftGravatar Jason Gross2019-01-03
| * comment out broken code so things buildGravatar jadep2019-01-03
| * try to fix fancy rewrite rules; current output is incorrectGravatar jadep2019-01-03
| * WIPGravatar jadep2019-01-03
| * remove dead codeGravatar jadep2019-01-03
| * remove whitespace, print statements, and some dead tacticsGravatar jadep2019-01-03
| * fixed up some of the fancy rewrite rulesGravatar jadep2019-01-03
| * WIP: prove that barrett_red256 is a valid expression modulo some issues with ...Gravatar jadep2019-01-03
| * WIP: expand valid_ident and prove of_prefancy_correct using itGravatar jadep2019-01-03
| * WIP : made everything more concrete and proved of_Expr. Still to do for of_Ex...Gravatar jadep2019-01-03
| * WIPGravatar jadep2019-01-03
| * WIPGravatar jadep2019-01-03
| * WIPGravatar jadep2019-01-03
| * WIPGravatar jadep2019-01-03
|/
* Prove that convert_bases partitionsGravatar Jason Gross2019-01-03
* Do not rely on `Refine Instance Mode`Gravatar Maxime Dénès2019-01-02
* Remove WBW Mont lemmas from push_evalGravatar Jason Gross2018-12-26
* Add eval_* lemmas for WBW Mont Arith operationsGravatar Jason Gross2018-12-26
* Move le_{add,sub}_1_* to ZUtil.LeGravatar Jason Gross2018-12-25
* from_montgomery{_ => }mod, for consistency with other namingGravatar Jason Gross2018-12-24
* Add correctness in arithmetic for mulx, addcarryx, subborrowxGravatar Jason Gross2018-12-21
* Add has_body tacticGravatar Jason Gross2018-12-21
* Add eval_freeze_to_bytesmod to push_evalGravatar Jason Gross2018-12-21
* Add length_encode_no_reduce to distr_lengthGravatar Jason Gross2018-12-21
* Add `Proof using` directives in ArithmeticGravatar Jason Gross2018-12-21
* Fix a few minor things in ArithmeticGravatar Jason Gross2018-12-21
* remove unneeded lemma and do some micro-performance-optimization at one stick...Gravatar jadep2018-12-21
* remove proof duplicationGravatar jadep2018-12-21
* fix hints and [Proof using] statements so that proofs go throughGravatar jadep2018-12-21
* prove [small_sub_then_maybe_add]Gravatar jadep2018-12-21
* prove [eval_sub_then_maybe_add]Gravatar jadep2018-12-21
* fix hints and [Proof using] statements so that proofs go throughGravatar jadep2018-12-21
* prove [small_conditional_sub]Gravatar jadep2018-12-21
* prove [eval_conditional_sub]Gravatar jadep2018-12-21
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-13 20:43:36 +0000