aboutsummaryrefslogtreecommitdiff
Commit message (Expand)AuthorAge
* proved an admit (eq_enc_S_iff) in Ed25519.vGravatar jadep2016-10-27
* Add Inline importGravatar Jason Gross2016-10-27
* Add {un,}curry_wire_digitsGravatar Jason Gross2016-10-27
* CompleteEdwardsCurve.ExtendedCoordinates: remove admitted lift_homomorphism l...Gravatar Andres Erbsen2016-10-27
* Add {un,}curry_{bin,un}op_fe25519Gravatar Jason Gross2016-10-27
* Add length_fe25519Gravatar Jason Gross2016-10-27
* Fix implicit status of curryGravatar Jason Gross2016-10-27
* Add curry and uncurry to tupleGravatar Jason Gross2016-10-27
* Add syntax and reification for the ops in GF25519Gravatar Jason Gross2016-10-27
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-06 06:53:05 +0000