aboutsummaryrefslogtreecommitdiff
path: root/src/Assembly
Commit message (Expand)AuthorAge
* 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
* Pseudize Lemmas for Dual OperationsGravatar Robert Sloan2016-06-23
* Integrate Pseudize into Pipeline.vGravatar Robert Sloan2016-06-23
* Integrate Pseudize into Pipeline.vGravatar Robert Sloan2016-06-23
* Pseudize Let_In with minor notationsGravatar Robert Sloan2016-06-23
* Pseudize Let_InGravatar Robert Sloan2016-06-23
* Add Pseudize, Vectorize, Wordize to the build processGravatar Robert Sloan2016-06-22
* Make Assembly modules 8.5-compatibleGravatar Robert Sloan2016-06-22
* Replace NPeano -> Nat in src/Spec/EdDSAGravatar Robert Sloan2016-06-22
* Fix build processGravatar Robert Sloan2016-06-22
* Full automation for relevant parts of pseudo conversion except letsGravatar Robert Sloan2016-06-22
* Decent machinery for automatic pseudo-conversionGravatar Robert Sloan2016-06-19
* Decent machinery for automatic pseudo-conversionGravatar Robert Sloan2016-06-19
* Decent machinery for automatic pseudo-conversionGravatar Robert Sloan2016-06-18
* first pseudo conversion lemmaGravatar Robert Sloan2016-06-14
* Reorganization of wordize.vGravatar Robert Sloan2016-06-14
* Merging wordization and bounding together in Wordize.vGravatar Robert Sloan2016-06-08
* Really complex derivation of wand correctnessGravatar Robert Sloan2016-06-07
* Really complex derivation of wand correctnessGravatar Robert Sloan2016-06-07
* Basic wordization lemmasGravatar Robert Sloan2016-06-06
* Proper word-based vectorizationGravatar Robert Sloan2016-06-06
* merging with masterGravatar Robert Sloan2016-06-06
|\
* | Full pipeline working againGravatar Robert Sloan2016-06-06
* | Huge Language / Conversion refactorsGravatar Robert Sloan2016-06-04
* | More refactors that will make this whole thing very unstableGravatar Robert Sloan2016-06-03
* | Running PipelineExampleGravatar Robert Sloan2016-06-02
* | Running PipelineExampleGravatar Robert Sloan2016-06-01
* | Running PipelineExampleGravatar Robert Sloan2016-06-01
* | Running PipelineExampleGravatar Robert Sloan2016-06-01
* | Parsing portion of StringConversionGravatar Robert Sloan2016-06-01
* | Parsing portion of StringConversionGravatar Robert Sloan2016-06-01
* | AlmostConversion and part of StringConversionGravatar Robert Sloan2016-05-31
* | PseudoMedialConversion doneGravatar Robert Sloan2016-05-31
* | Pseudo conversionsGravatar Robert Sloan2016-05-31
* | Generalized and cleaned up state modelGravatar Robert Sloan2016-05-31
* | Generalized and cleaned up state modelGravatar Robert Sloan2016-05-30
* | Generalized and cleaned up state modelGravatar Robert Sloan2016-05-28
* | Finished proofs in QhasmEvalCommon for formalizing mappingsGravatar Robert Sloan2016-05-27
* | Finished proofs in QhasmEvalCommon for formalizing mappingsGravatar Robert Sloan2016-05-27
* | Major language refactoring to support Memory and AddWithCarryGravatar Robert Sloan2016-05-26
* | Major language refactoring to support Memory and AddWithCarryGravatar Robert Sloan2016-05-26
* | MedialConversions doneGravatar Robert Sloan2016-05-25
* | MedialConversions doneGravatar Robert Sloan2016-05-25