| Commit message (Expand) | Author | Age |
|---|
| * | Make use of from_associational_cps in more places |  Jason Gross | 2017-11-01 |
| * | More use of Z.eqb_cps | Jason Gross | 2017-11-01 |
| * | Switch to AddWithGetCarry in ZExtended | Jason Gross | 2017-10-31 |
| * | Add MapBaseType | Jason Gross | 2017-10-31 |
| * | Add unextend_op | Jason Gross | 2017-10-31 |
| * | Generalize MapBaseType a bit | Jason Gross | 2017-10-31 |
| * | Add invert_PairsConst_gen | Jason Gross | 2017-10-31 |
| * | add ZToSignedWord, signedWordToZ | Jason Gross | 2017-10-31 |
| * | Add wneg_inj | Jason Gross | 2017-10-31 |
| * | Fix ZToWord, add wring_eq_ext, speed up some proofs | Jason Gross | 2017-10-31 |
| * | Add Bedrock.Word.ZToWord | Jason Gross | 2017-10-31 |
| * | Remove trailing spaces | Jason Gross | 2017-10-31 |
| * | Bump coq submodule | Jason Gross | 2017-10-31 |
| * | Fix smithers build | Jason Gross | 2017-10-31 |
| * | fibe: WIP scalarmult for benchmarking field operations |  Andres Erbsen | 2017-10-31 |
| * | Update display logs | Jason Gross | 2017-10-31 |
| * | Update display logs | Jason Gross | 2017-10-31 |
| * | Add more constant notations | Jason Gross | 2017-10-31 |
| * | Update display logs | Jason Gross | 2017-10-29 |
| * | Update display logs | Jason Gross | 2017-10-29 |
| * | make update-_CoqProject | Jason Gross | 2017-10-29 |
| * | Update display logs | Jason Gross | 2017-10-29 |
| * | Add more constant notations | Jason Gross | 2017-10-29 |
| * | add prettyprint.py, to eventually replace extract-*.sh | Andres Erbsen | 2017-10-28 |
| * | fix python montgomery ladder | Andres Erbsen | 2017-10-28 |
| * | check in p384 generated code | Andres Erbsen | 2017-10-26 |
| * | gmpxx.c: s/32/modulus_bytes/ | Andres Erbsen | 2017-10-26 |
| * | add python reference for x25519 | Andres Erbsen | 2017-10-26 |
| * | add gmpxx.cpp: a higher-level implementation | Andres Erbsen | 2017-10-26 |
| * | automate some proofs; also remove trace-based reasoning in favor of induction... |  jadep | 2017-10-26 |
| * | invariants don't need to know the fuel | jadep | 2017-10-26 |
| * | WIP: loops | jadep | 2017-10-26 |
| * | Remove NISTP256/AMD128 from lite target |  Jason Gross | 2017-10-25 |
| * | Add a missing line continuation in Makefile | Jason Gross | 2017-10-24 |
| * | Don't build feadd,fesub,fecarry .c files | Jason Gross | 2017-10-24 |
| * | Add inversion_wf_one_constr | Jason Gross | 2017-10-24 |
| * | Add MapBaseTypeWf, generalize src/Compilers/MapBaseType.v a bit | Jason Gross | 2017-10-24 |
| * | Generalize In_flatten_binding_list_untransfer_interp_flat_type | Jason Gross | 2017-10-24 |
| * | Add In_flatten_binding_list_untransfer_interp_flat_type | Jason Gross | 2017-10-24 |
| * | Add wff_SmartPairf_SmartValf | Jason Gross | 2017-10-24 |
| * | Add MapBaseType | Jason Gross | 2017-10-23 |
| * | Add find_Name_and_val_transfer_interp_flat_type_None | Jason Gross | 2017-10-23 |
| * | Add find_Name_and_val_transfer_interp_flat_type | Jason Gross | 2017-10-23 |
| * | Factor out some code in src/Compilers/Named/MapType.v | Jason Gross | 2017-10-23 |
| * | Add {un,}transfer_interp_flat_type, lift_flat_type | Jason Gross | 2017-10-23 |
| * | Add InlineConstAndOpByRewrite | Jason Gross | 2017-10-23 |
| * | Add nonautogenerated-specific{,-display} targets | Jason Gross | 2017-10-23 |
| * | Add inline_const_and_op{f,} specializations | Jason Gross | 2017-10-22 |
| * | Add another unfolding database | Jason Gross | 2017-10-22 |
| * | Factor out fold_right_cps2_specialized_step, add mapi_with'_cps2 | Jason Gross | 2017-10-22 |
Jason Gross
Andres Erbsen
jadep
Jason Gross