aboutsummaryrefslogtreecommitdiffstats
path: root/src
Commit message (Collapse)AuthorAgeFilesLines
* Annonimize submissiondev/asplosYann Herklotz2023-08-1061-72/+72
|
* 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-101-0/+245
|
* Fix backend hardware generation and schedulingYann Herklotz2023-08-107-54/+95
|
* 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-2921-2671/+6806
|
* Add equivalence classesYann Herklotz2023-07-116-191/+334
|
* Add if-conversion decision procedureYann Herklotz2023-07-066-29/+60
|
* Finish some proofs and remove unnecessary AdmittedYann Herklotz2023-06-265-32/+74
|
* Finish mutual exclusivity checkYann Herklotz2023-06-255-31/+150
|
* Finish SMT proofYann Herklotz2023-06-231-3/+100
|
* Add SMTCoq solver as dependencyYann Herklotz2023-06-2110-50/+229
|
* Finish complete evaluability proofYann Herklotz2023-06-101-19/+88
|
* Try to prove main theoremYann Herklotz2023-06-101-0/+5
| | | | Missing some link between forests
* 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
|
* 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
|
* Finish max predicate proofYann Herklotz2023-05-281-1/+78
|
* Finish proofs in GiblePargenproofForward.vYann Herklotz2023-05-282-5/+49
|
* Work on forward proofsYann Herklotz2023-05-282-1/+18
|
* Finish proofs in GiblePargenproofBackward.vYann Herklotz2023-05-271-26/+101
|
* Add proofs of gather_predicatesYann Herklotz2023-05-261-25/+196
|
* Finish predicate inclusion proofsYann Herklotz2023-05-251-48/+99
|
* Finish gather_predicate proofsYann Herklotz2023-05-241-17/+502
|
* Prove evaluability of predicates throughoutYann Herklotz2023-05-221-61/+126
|
generated by cgit (git 2.34.1) at 2024-06-28 20:01:17 +0000