aboutsummaryrefslogtreecommitdiff
Commit message (Expand)AuthorAge
* Fix a missing import in previous commitGravatar Jason Gross2016-10-27
* Factor out cmov{l,ne} and negGravatar Jason Gross2016-10-27
* PHOAS notation fixupsGravatar Jason Gross2016-10-27
* Make it easier to export only phoas notationsGravatar Jason Gross2016-10-27
* add wf, not only rel_wf, to MapInterpWfGravatar Jason Gross2016-10-27
* Add WfRelReflectiveGravatar Jason Gross2016-10-27
* Factor WfReflective through WfReflectiveGenGravatar Jason Gross2016-10-27
* removed now irrelevant commented-out codeGravatar jadep2016-10-27
* convert feEnc correctness proof to bounded typeGravatar jadep2016-10-27
* finished feEnc correctnessGravatar jadep2016-10-27
* most of feEnc correctness proofGravatar jadep2016-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
* removed lingering TODOGravatar jadep2016-10-27
* Implicits for reflect_wfTGravatar Jason Gross2016-10-27
* Add WfReflectiveGenGravatar Jason Gross2016-10-27
* Move interp_flat_type_gen_rel_pointwise2 to SyntaxGravatar Jason Gross2016-10-27
* Add Wf proofs about MapInterpGravatar Jason Gross2016-10-27
* Add arguments to mapf_interp_flat_type_genGravatar Jason Gross2016-10-27
* Add implicits to interp_flat_type_gen_rel_pointwise2Gravatar Jason Gross2016-10-27
* Change the argument implicits on rel_wffGravatar Jason Gross2016-10-27
* Revert change to [nsatz] (it was making Coq run out of memory)Gravatar Jason Gross2016-10-27
* Simplify proof of proj1_fe25519_encodeGravatar Jason Gross2016-10-27
* Add lemmas about GF25519BoundedCommon.{encode,decode}Gravatar Jason Gross2016-10-27
* Various fixes in alternative nsatzGravatar Jason Gross2016-10-27
* Handle folded [not] in nsatz_strip_fractionsGravatar Jason Gross2016-10-26
* Split inequalities before specializingGravatar Jason Gross2016-10-26
* Fix nsatz: don't clear inequalitiesGravatar Jason Gross2016-10-26
* Fix a missing case in generalize_invGravatar Jason Gross2016-10-26
* Fix typosGravatar Jason Gross2016-10-26
* Add tactics to implement better fraction removalGravatar Jason Gross2016-10-26
* Add lemmas about algebraGravatar Jason Gross2016-10-26
* Fix for Coq 8.4 (f_equiv changed behavior)Gravatar Jason Gross2016-10-26
* Initial work on filling ed25519 with bounded thingsGravatar Jason Gross2016-10-25
* Switch to bounded ZGravatar Jason Gross2016-10-25
* prove SRepMul admitGravatar Andres Erbsen2016-10-25
* Proved homomorphism between curve groups (Twisted Edwards Curve representatio...Gravatar jadep2016-10-24
* Freeze before packing to get canonical encodingsGravatar jadep2016-10-24
* ed25519: prove some admitsGravatar Andres Erbsen2016-10-24
* Fix for Coq 8.4Gravatar Jason Gross2016-10-24
* Add more relations about fieldwiseGravatar Jason Gross2016-10-24
* Adjust bound on final word in wire_digits to 31Gravatar Jason Gross2016-10-24
* Fix bounds on wire_digitsGravatar Jason Gross2016-10-24
* Add pack, unpack, ge_modulus to axioms to be reifiedGravatar Jason Gross2016-10-24
* Modify point_phi (from PointEncodings) to use ref_phiGravatar jadep2016-10-23
* Created separate definitions for cmovne and cmovl for reificationGravatar jadep2016-10-23
* More 8.4 fixesGravatar Jason Gross2016-10-23
* Fix 8.4 build issueGravatar Jason Gross2016-10-23
* Prove an admitted NatUtil lemmaGravatar Jason Gross2016-10-23
* Prove more things in WordUtilGravatar Jason Gross2016-10-23
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-30 03:00:31 +0000