aboutsummaryrefslogtreecommitdiff
Commit message (Expand)AuthorAge
* Karatsuba in gallinaGravatar Jason Gross2017-10-18
* Explicitly specify baseGravatar Jason Gross2017-10-18
* Move more of carry_sig, zero_sig, one_sig, etc to gallinaGravatar Jason Gross2017-10-18
* Allow forcing a bitwidth to workGravatar Jason Gross2017-10-18
* Add a few more base thingsGravatar Jason Gross2017-10-18
* Add sz2'_nonzeroGravatar Jason Gross2017-10-18
* Move coef, coef_mod to gallinaGravatar Jason Gross2017-10-18
* Add some more helper lemmas to synthesisGravatar Jason Gross2017-10-18
* Better error messages when m_enc_correct_montgomery failsGravatar Jason Gross2017-10-18
* Run remake_curves.pyGravatar Jason Gross2017-10-18
* Fix make_curve.py to handle files from generate_parametersGravatar Jason Gross2017-10-18
* Add chained_carries_cps' lemmasGravatar Jason Gross2017-10-18
* Extract rexpr_sig from the recordGravatar Jason Gross2017-10-18
* Extract evars from reflective pipelineGravatar Jason Gross2017-10-18
* Add a commentGravatar Jason Gross2017-10-18
* Fix synthesis output recordGravatar Jason Gross2017-10-18
* Package reflective pipeline side-conditions into a recordGravatar Jason Gross2017-10-18
* Remove admitted encode_correct proofGravatar Jason Gross2017-10-18
* Lemmas about wt_genGravatar Jason Gross2017-10-18
* Stronger pose_proof_tupleGravatar Jason Gross2017-10-18
* Update OutputTypeGravatar Jason Gross2017-10-18
* Add final synthesis output typeGravatar Jason Gross2017-10-18
* Turn CurveParameters into a recordGravatar Jason Gross2017-10-18
* Add newline at end of CurveParametersGravatar Jason Gross2017-10-18
* Support p256 / montgomery in json formatGravatar Jason Gross2017-10-18
* Reorganize the curve-specific synthesis frameworkGravatar Jason Gross2017-10-18
* Support curves with +2^... in themGravatar Jason Gross2017-10-18
* Add default computation for goldilocksGravatar Jason Gross2017-10-18
* Fix Makefile deps with move of IntegrationTestDisplayCommonGravatar Jason Gross2017-10-18
* Default carry chains in json filesGravatar Jason Gross2017-10-18
* Handle generating the correct c from 2^448-2^224-1Gravatar Jason Gross2017-10-18
* Fold Karatsuba into json format and synthesisGravatar Jason Gross2017-10-18
* Build curve-specific files from jsonGravatar Jason Gross2017-10-18
* Generate C64 from python script and jsonGravatar Jason Gross2017-10-18
* Reorgainze synthesis framework files into a Framework folderGravatar Jason Gross2017-10-18
* Replace curve-specific definitions with tacticsGravatar Jason Gross2017-10-18
* Factor out specific code underlying ReificationTypesGravatar Jason Gross2017-10-18
* Add 8.7-only CacheTermGravatar Jason Gross2017-10-18
* Add more notation constantsGravatar Jason Gross2017-10-18
* Update .travis.yml from 8.7+beta2 to 8.7.0Gravatar Jason Gross2017-10-18
* Update .travis.yml to be 8.7-onlyGravatar Jason Gross2017-10-18
* projective Weierstrass: (P2 = 2Q -> P = Q) -> not exceptionalGravatar Andres Erbsen2017-10-18
* Revert "Add -compat 8.6 to _CoqProject"Gravatar Jason Gross2017-10-18
* Add a Require Import FunInd (Function isn't loaded by default anymore)Gravatar Pierre Letouzey2017-10-18
* Add some more things to basesystem_partial_evaluation_unfolderGravatar Jason Gross2017-10-18
* Add basesystem_partial_evaluation_unfolder dbGravatar Jason Gross2017-10-18
* Unfold more things in core unfolderGravatar Jason Gross2017-10-18
* Allow instantiating type arguments without reducing matchesGravatar Jason Gross2017-10-18
* Allow instantiating type arguments without reducing matchesGravatar Jason Gross2017-10-17
* Allow instantiating type arguments without reducing matchesGravatar Jason Gross2017-10-17
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-04 16:54:25 +0000