aboutsummaryrefslogtreecommitdiffstats
Commit message (Expand)AuthorAgeFilesLines
* Annonimize submissiondev/asplosYann Herklotz2023-08-1081-216/+120
* Add comments next to admitted theoremsYann Herklotz2023-08-103-6/+6
* Finish final forward simulation correctnessYann Herklotz2023-08-1015-7305/+172
* Abort steytin proofsYann Herklotz2023-08-101-2/+2
* Add Bambu synthesis and ClockRegistersYann Herklotz2023-08-104-0/+414
* Fix backend hardware generation and schedulingYann Herklotz2023-08-1013-66/+114
* Remove tseytin transformation temporarilyYann Herklotz2023-08-101-1/+1
* Put every load/store into it's own cycleYann Herklotz2023-08-023-179/+204
* Finish datapath memory generationYann Herklotz2023-08-022-409/+546
* Fixing store transformationYann Herklotz2023-08-013-96/+179
* Add fixes to main memory generation proofYann Herklotz2023-07-312-799/+808
* Remove RTLParFu and fix DMemorygen.vYann Herklotz2023-07-315-1974/+1949
* Add beginning to memory generation proofYann Herklotz2023-07-2922-2671/+6810
* Add equivalence classesYann Herklotz2023-07-1110-192/+552
* Add if-conversion decision procedureYann Herklotz2023-07-066-29/+60
* Fix man file generationYann Herklotz2023-06-262-4/+3
* Update cohpred with renamed filesYann Herklotz2023-06-261-0/+0
* Add COHPREDSTAMP to .gitignoreYann Herklotz2023-06-261-0/+2
* Finish some proofs and remove unnecessary AdmittedYann Herklotz2023-06-267-33/+76
* Finish mutual exclusivity checkYann Herklotz2023-06-255-31/+150
* Finish SMT proofYann Herklotz2023-06-231-3/+100
* Add SMTCoq solver as dependencyYann Herklotz2023-06-2114-71/+233
* Update makefile to build cohpredYann Herklotz2023-06-191-2/+6
* Update cohpred libraryYann Herklotz2023-06-181-0/+0
* Update cohpred git submoduleYann Herklotz2023-06-142-1/+1
* Add CohPred and SMTCoq dependencyYann Herklotz2023-06-124-2/+29
* Finish complete evaluability proofYann Herklotz2023-06-101-19/+88
* Try to prove main theoremYann Herklotz2023-06-101-0/+5
* Add more to proof of evaluabilityYann Herklotz2023-06-102-1/+57
* Finish abstract_sequence_evaluable_mYann Herklotz2023-06-091-1/+104
* Prove abstract_sequence_evaluableYann Herklotz2023-06-091-0/+2
* Finish abstract_sequence_evaluable_fold2Yann Herklotz2023-06-091-5/+42
* Finish abstract_sequence_evaluable_foldYann Herklotz2023-06-091-12/+68
* Add outline of proof of evaluable when predicate is falseYann Herklotz2023-06-091-19/+54
* Add proof outline for evaluabilityYann Herklotz2023-06-082-20/+44
* Work towards proving evaluabilityYann Herklotz2023-06-053-38/+169
* Move around generating functionsYann Herklotz2023-06-032-68/+68
* Add lp_solve dependency to nixYann Herklotz2023-06-021-1/+1
* Fix proof of predicates completelyYann Herklotz2023-06-022-7/+24
* Fix top-level proof with Isetpred missingYann Herklotz2023-06-021-12/+55
* Finished the propert version of from_predicated_sem_pred_expr2Yann Herklotz2023-06-027-44/+316
* Finish from_predicated_sem_pred_exprYann Herklotz2023-05-311-8/+97
* Remove unnecessary assumption from sem_merge_listYann Herklotz2023-05-301-4/+3
* Fix other proofs and attempt from_predicated proofYann Herklotz2023-05-301-7/+26
* Prove merge list_translationYann Herklotz2023-05-301-2/+16
* Prove fold_right over ElistYann Herklotz2023-05-301-4/+74
* Finish second flap2 proofYann Herklotz2023-05-301-1/+9
* Finished painful product proofYann Herklotz2023-05-305-13/+127
* Prove more admitted theoremsYann Herklotz2023-05-296-47/+190
* Finish two AbstrSemIdent false proofsYann Herklotz2023-05-281-11/+50
generated by cgit (git 2.34.1) at 2024-04-28 21:59:48 +0000