aboutsummaryrefslogtreecommitdiff
path: root/src/Assembly
Commit message (Expand)AuthorAge
* Switch to bounded ZGravatar Jason Gross2016-10-25
* Add pack, unpack, ge_modulus to axioms to be reifiedGravatar Jason Gross2016-10-24
* Fix for weaker pattern matching in < 8.4pl4Gravatar Jason Gross2016-10-22
* Fix for weaker pattern matching in < 8.4pl4Gravatar Jason Gross2016-10-22
* Unfold interp stuff in Assembly/GF25519BoundedInstantiationGravatar Jason Gross2016-10-22
* Interpret LetIn to Let_In for better control of interpGravatar Jason Gross2016-10-22
* Instantiate some things with bounded thingsGravatar Jason Gross2016-10-21
* A bit of initial setup on correct_and_bounded proofs in GF25519BoundedInstant...Gravatar Jason Gross2016-10-20
* Plug bounded into assembly stuffGravatar Jason Gross2016-10-20
* Adjust bounds in assemblyGravatar Jason Gross2016-10-20
* Split up GF25519Bounded to avoid circular dependenciesGravatar Jason Gross2016-10-20
* Various fixes for Coq 8.4Gravatar Jason Gross2016-10-20
* Use carry versions of operationsGravatar Jason Gross2016-10-20
* rfreeze, not rinv; update to saner boundedness requirementsGravatar Jason Gross2016-10-20
* Start instantiating boundedness thingsGravatar Jason Gross2016-10-19
* Fast bounds-checking machinery but lower-bounds are brokenGravatar Robert Sloan2016-10-18
* Converting to bounded machineryGravatar Robert Sloan2016-10-17
* More of the Conversions.v correctness proofsGravatar Robert Sloan2016-10-14
* Use 64-bit limbs in PipelinesGravatar Robert Sloan2016-10-14
* Making sub bounds actually tightGravatar Robert Sloan2016-10-14
* Moved to non-extended operations + Extraction + Bounds-checkingGravatar Robert Sloan2016-10-14
* Well, here's the program instance. The string conversion is still running.Gravatar Robert Sloan2016-10-13
* More minor improvements in Conversions.v and Compile.vGravatar Robert Sloan2016-10-13
* More minor improvements in Conversions.v and Compile.vGravatar Robert Sloan2016-10-13
* Minor refactors waiting for the code generation to finishGravatar Robert Sloan2016-10-13
* Minor refactors waiting for the code generation to finishGravatar Robert Sloan2016-10-13
* Minor refactors waiting for the code generation to finishGravatar Robert Sloan2016-10-13
* Refactors of ge25519_ast working in Pipeline.vGravatar Rob Sloan2016-10-12
* Complete example + GF25519 outline in Pipeline.vGravatar Robert Sloan2016-10-02
* Most of our refactored compilation infrastructureGravatar Rob Sloan2016-10-02
* Fix merge with masterGravatar Robert Sloan2016-09-24
|\
* | Large-scale refactoring of src/AssemblyGravatar Robert Sloan2016-09-24
| * deduplicate Let_In into src/Util/LetIn.vGravatar Andres Erbsen2016-09-17
* | Finished more efficient WordRangeOptGravatar Robert Sloan2016-09-15
* | Most of a more efficient WordRangeOptGravatar Robert Sloan2016-09-13
| * Fully qualify [Require]sGravatar Jason Gross2016-09-08
* | Fix evalWordRangeOptGravatar Robert Sloan2016-08-26
* | Much tighter bounds in Evaluables.vGravatar Robert Sloan2016-08-26
* | Removed nat arguments to Evaluable operationsGravatar Robert Sloan2016-08-25
* | Finishing tactical machinery for bound-computingGravatar Robert Sloan2016-08-24
* | Experimental requirements for rsloan-phoasGravatar Robert Sloan2016-08-23
|/
* Remove unnecessary pseudo notations (#47)Gravatar Rob Sloan2016-08-08
* Move most notation level declarations into UtilGravatar Jason Gross2016-07-27
* Make the library 20% faster: [auto with *] is evilGravatar Jason Gross2016-07-22
* Remove examples for 8.4 compatibilityGravatar Robert Sloan2016-06-23
* Remove vestigal BoundedWord machineryGravatar Robert Sloan2016-06-23
* Make Pipeline.v Build on 8.4Gravatar Robert Sloan2016-06-23
* Add Language.v, Conversion.v to _CoqProjectGravatar Robert Sloan2016-06-23
* QhasmUtil.v: Remove 8.4-incompatible intro nameGravatar Robert Sloan2016-06-23
* Pipeline: several new examplesGravatar Robert Sloan2016-06-23
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-03 16:54:14 +0000