aboutsummaryrefslogtreecommitdiff
path: root/src
Commit message (Expand)AuthorAge
* fix src/Specific/GF25519Reflective/Reified/AddCoordinates.vGravatar Andres Erbsen2017-03-02
* remove PointEncodingGravatar Andres Erbsen2017-03-02
* CompleteEdwardsCurveTheorems: point compressionGravatar Andres Erbsen2017-03-02
* PrimeFieldTheorems: inv for isomorphic fieldsGravatar Andres Erbsen2017-03-02
* use [positive] for [F] modulus, char_ge_C instead of char_gt_CGravatar Andres Erbsen2017-03-02
* rewrite ExtendedCoordinates, fix Ed25519Gravatar Andres Erbsen2017-03-02
* edwards curves over isomorphic fieldsGravatar Andres Erbsen2017-03-02
* src/Tactics/Algebra_syntax/Nsatz.v: power 1 onlyGravatar Andres Erbsen2017-03-02
* WIPGravatar Andres Erbsen2017-03-02
* address some code review commentsGravatar Andres Erbsen2017-03-02
* Weierstrass curve is a groupGravatar Andres Erbsen2017-03-02
* Attempt Weierstrass associativity again, good progress.Gravatar Andres Erbsen2017-03-02
* change weierstrass spec, prove most cases of associativityGravatar Andres Erbsen2017-03-02
* split the algebra library; use fsatz moreGravatar Andres Erbsen2017-03-02
* fsatz, nsatz_solve_nonzeroGravatar Andres Erbsen2017-03-02
* use field_nsatz in CompleteEdwardsCurve.PreGravatar Andres Erbsen2017-03-02
* field_nsatzGravatar Andres Erbsen2017-03-02
* make assert_preconditions way more sane; use vm_decide to kill most subgoalsGravatar jadep2017-03-02
* Separated out [carry] from other operations.Gravatar jadep2017-03-02
* Modify/add to NewBaseSystem to match with what is needed for proof of ring is...Gravatar jadep2017-03-01
* Fixed carry bugs (indexes need to be reversed, and we need to convert to/from...Gravatar jadep2017-03-01
* Defined [div] and [mod]; removed liftn_sig lemmas because they were actually ...Gravatar jadep2017-03-01
* Adjust implicits of flatten_binding_list_same_in_eqGravatar Jason Gross2017-03-01
* Add flatten_binding_list_In_eq_iff, flatten_binding_list_same_in_eqGravatar Jason Gross2017-03-01
* Add η principles for sigma typesGravatar Jason Gross2017-03-01
* Add dlet_nd notationGravatar Jason Gross2017-03-01
* Switch to fully uncurried form for reflectionGravatar Jason Gross2017-03-01
* Add interp_flat_type_rel_pointwise_SmartVarfMap, interp_flat_type_rel_pointwi...Gravatar Jason Gross2017-02-28
* Add SmartVarfMap Proper instanceGravatar Jason Gross2017-02-28
* Add strip_eta_tuple lemmasGravatar Jason Gross2017-02-28
* Better tuple_eta argumentsGravatar Jason Gross2017-02-28
* Add eta_tuple functionsGravatar Jason Gross2017-02-28
* Deduplicate codeGravatar Jason Gross2017-02-28
* Defined zero and one for NewBaseSystemGravatar jadep2017-02-27
* Added operation (including creating )Gravatar jadep2017-02-27
* Added subtractionGravatar jadep2017-02-27
* added Positional wrappers for Associational operations, added correctness pro...Gravatar jadep2017-02-27
* changed names of ops in NewBaseSystem to reflect that they are sig and not sigTGravatar jadep2017-02-27
* Modified lemma and created tactic to handle it; added reduce step to multipl...Gravatar jadep2017-02-26
* removed leftover saturated stuff (will probably end up in a separate file som...Gravatar jadep2017-02-26
* speed up NewBaseystem synthesisGravatar Andres Erbsen2017-02-23
* Add BoundsInterpretationsGravatar Jason Gross2017-02-23
* Add log and non-log versions of FixedWordSizes lemGravatar Jason Gross2017-02-23
* Add invert_Some; add nat_N_Z to push_Zof_NGravatar Jason Gross2017-02-23
* Minor change to reflection namingGravatar Jason Gross2017-02-23
* added explanation of why CPS is usefulGravatar jadep2017-02-23
* Removed code that will be completely replaced in the future; replaced some po...Gravatar jadep2017-02-22
* move lemmas from Ed25519 to WordUtilGravatar jadep2017-02-22
* move some lemmas from Ed25519 to ZUtilGravatar jadep2017-02-22
* moved more stuff to NUtilGravatar jadep2017-02-22
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-02 16:59:27 +0000