| Commit message (Collapse) | Author | Age | |
|---|---|---|---|
| * | Minor refactoring of related_Z_op |  Jason Gross | 2016-11-07 |
| | | |||
| * | Finish related_bounds_t_map1_tuple2 | Jason Gross | 2016-11-07 |
| | | |||
| * | Add push_lift_option | Jason Gross | 2016-11-07 |
| | | |||
| * | More progress on related_bounds_t_map1_tuple2 | Jason Gross | 2016-11-07 |
| | | |||
| * | More progress on t_map1_tuple2 lemmas | Jason Gross | 2016-11-07 |
| | | |||
| * | Add flat_interp_tuple_untuple' | Jason Gross | 2016-11-07 |
| | | |||
| * | Add flat_interp_untuple'_tuple | Jason Gross | 2016-11-07 |
| | | |||
| * | Add map_is_mapt' | Jason Gross | 2016-11-07 |
| | | |||
| * | Add IffT, some Proper prod lemmas | Jason Gross | 2016-11-07 |
| | | |||
| * | Add Proper prod instance | Jason Gross | 2016-11-07 |
| | | |||
| * | Add convoy_destruct | Jason Gross | 2016-11-07 |
| | | |||
| * | Add tuple hd and tl | Jason Gross | 2016-11-07 |
| | | |||
| * | Merge branch 'master' of ssh://github.com/mit-plv/fiat-crypto |  Adam Chlipala | 2016-11-07 |
| |\ | |||
| * | | Some progress on Relations admits | Adam Chlipala | 2016-11-07 |
| | | | |||
| | * | automate MxDHRepChange.Proper_loopiter intros |  Andres Erbsen | 2016-11-07 |
| |/ | |||
| * | implement X25519 | Andres Erbsen | 2016-11-06 |
| | | |||
| * | move B_order_l and prime_q | Andres Erbsen | 2016-11-06 |
| | | |||
| * | More reorg in Reflection/Z/Interpretations/Relations.v | Jason Gross | 2016-11-06 |
| | | |||
| * | Do some of the related_Z_op proofs | Jason Gross | 2016-11-06 |
| | | |||
| * | Refactor various reflective things | Jason Gross | 2016-11-06 |
| | | | | | | We now have a more principled approach in many places, and some of the tuple-specific reasoning has been filled in. | ||
| * | Add more admitted tuple lemmas | Jason Gross | 2016-11-06 |
| | | |||
| * | Add more admitted tuple lemmas | Jason Gross | 2016-11-06 |
| | | |||
| * | Add Tuple.map_map2 (admitted) | Jason Gross | 2016-11-06 |
| | | |||
| * | Add HList lemma | Jason Gross | 2016-11-06 |
| | | |||
| * | Add admitted lemma about tuple map, add hlist lem | Jason Gross | 2016-11-06 |
| | | |||
| * | Add Tuple lift push | Jason Gross | 2016-11-06 |
| | | |||
| * | Connect [is_bounded] to [bounded_by] | Jason Gross | 2016-11-06 |
| | | | | | | This hooks up the boundedness constraints on [freeze] in GF25519Bounded to those in Ed25519. | ||
| * | Fixes for Coq 8.4 | Jason Gross | 2016-11-06 |
| | | |||
| * | The fix in 8.4 broke 8.5/8.6, so we fix that | Jason Gross | 2016-11-06 |
| | | | | | Grrrr, evars | ||
| * | Preliminary support: conditional sub as primitive | Jason Gross | 2016-11-06 |
| | | | | | | | | | | | | | | | | | | | | | | | | Things to be done: - Fill in Axiom conditional_subtract_modulus in src/ModularArithmetic/ModularBaseSystemListZOperations.v (jadep) - Refactor code to make GF25519.freeze use ModularBaseSystemListZOperations.conditional_subtract_modulus in a non-unfolded form (jadep) - Check that the bounds I defined in conditional_subtract' in src/Reflection/Z/Interpretations.v are correct (jadep) - Fill in bounds checking in conditional_subtract_o in src/Reflection/Z/Interpretations.v (jgross or jadep) - Integrate boundedness lemma about conditional_subtract_modulus into BoundedWord64.conditional_subtract in src/Reflection/Z/Interpretations.v (jadep and jgross?) - Prove BoundedWord64.invert_conditional_subtract (depends on some bits of the above bullet point, but could be done by jgross) - Fill in the three admits in src/Reflection/Z/Interpretations/Relations.v (jadep or jgross?) - Verify that everything works (cc @jadephilipoom @andres-erbsen) | ||
| * | Add syntactic tuples | Jason Gross | 2016-11-06 |
| | | |||
| * | Add functions for [tuple (option _) _] | Jason Gross | 2016-11-06 |
| | | |||
| * | Add support for dependent reification | Jason Gross | 2016-11-06 |
| | | |||
| * | Work around broken evars in 8.4 | Jason Gross | 2016-11-06 |
| | | |||
| * | More partial proofs | Jason Gross | 2016-11-06 |
| | | |||
| * | Prove inversion principles for bounded words | Jason Gross | 2016-11-06 |
| | | |||
| * | Plug in boundedness proofs | Jason Gross | 2016-11-05 |
| | | | | | | We no longer admit the boundedness proofs (other than freeze); a significant chunk of the boundedness proofs now line up nicely. | ||
| * | Add better bounded lemmas to reified things | Jason Gross | 2016-11-05 |
| | | |||
| * | Add eta-expansion in GF25519BoundedCommon.v | Jason Gross | 2016-11-05 |
| | | | | | It'll be needed to vm_compute some proofs in GF25519Reflective/Reified/* | ||
| * | Add proofs about boundedness to GF25519Reflective/Common.v | Jason Gross | 2016-11-05 |
| | | |||
| * | Add unfold_is_bounded | Jason Gross | 2016-11-05 |
| | | |||
| * | Add related_word64_boundsi' | Jason Gross | 2016-11-05 |
| | | | | | This definition needs a better name... | ||
| * | Add code for overflow check (disabled bc freeze) | Jason Gross | 2016-11-05 |
| | | | | | | | | Currently freeze overflows; Jade says this is because the carry chain got reversed, and that she'll work on fixing this. We should enable the sanity checks at some point after this is fixed, to fail early if things overflow. | ||
| * | Split off some things from Interpretations | Jason Gross | 2016-11-05 |
| | | |||
| * | Fix implicit arguments | Jason Gross | 2016-11-05 |
| | | |||
| * | Remove pasted code that shouldn't've been in a file | Jason Gross | 2016-11-05 |
| | | |||
| * | Add proj1_from_option2 | Jason Gross | 2016-11-05 |
| | | |||
| * | Fix implicits | Jason Gross | 2016-11-05 |
| | | |||
| * | Fix a proof broken by previous commit | Jason Gross | 2016-11-05 |
| | | |||
| * | Another projection function | Jason Gross | 2016-11-05 |
| | | |||
 |
index : fiat-crypto | |
| fast, formally verified cryptography |
| aboutsummaryrefslogtreecommitdiff |