Commit message (Collapse) | Author | Age | Files | Lines | |
---|---|---|---|---|---|
* | Remove RTLParFu and fix DMemorygen.v | Yann Herklotz | 2023-07-31 | 5 | -1974/+1949 |
| | |||||
* | Add beginning to memory generation proof | Yann Herklotz | 2023-07-29 | 21 | -2671/+6806 |
| | |||||
* | Add equivalence classes | Yann Herklotz | 2023-07-11 | 6 | -191/+334 |
| | |||||
* | Add if-conversion decision procedure | Yann Herklotz | 2023-07-06 | 6 | -29/+60 |
| | |||||
* | Finish some proofs and remove unnecessary Admitted | Yann Herklotz | 2023-06-26 | 5 | -32/+74 |
| | |||||
* | Finish mutual exclusivity check | Yann Herklotz | 2023-06-25 | 5 | -31/+150 |
| | |||||
* | Finish SMT proof | Yann Herklotz | 2023-06-23 | 1 | -3/+100 |
| | |||||
* | Add SMTCoq solver as dependency | Yann Herklotz | 2023-06-21 | 10 | -50/+229 |
| | |||||
* | Finish complete evaluability proof | Yann Herklotz | 2023-06-10 | 1 | -19/+88 |
| | |||||
* | Try to prove main theorem | Yann Herklotz | 2023-06-10 | 1 | -0/+5 |
| | | | | Missing some link between forests | ||||
* | Add more to proof of evaluability | Yann Herklotz | 2023-06-10 | 2 | -1/+57 |
| | |||||
* | Finish abstract_sequence_evaluable_m | Yann Herklotz | 2023-06-09 | 1 | -1/+104 |
| | |||||
* | Prove abstract_sequence_evaluable | Yann Herklotz | 2023-06-09 | 1 | -0/+2 |
| | |||||
* | Finish abstract_sequence_evaluable_fold2 | Yann Herklotz | 2023-06-09 | 1 | -5/+42 |
| | |||||
* | Finish abstract_sequence_evaluable_fold | Yann Herklotz | 2023-06-09 | 1 | -12/+68 |
| | |||||
* | Add outline of proof of evaluable when predicate is false | Yann Herklotz | 2023-06-09 | 1 | -19/+54 |
| | |||||
* | Add proof outline for evaluability | Yann Herklotz | 2023-06-08 | 2 | -20/+44 |
| | |||||
* | Work towards proving evaluability | Yann Herklotz | 2023-06-05 | 3 | -38/+169 |
| | |||||
* | Move around generating functions | Yann Herklotz | 2023-06-03 | 2 | -68/+68 |
| | |||||
* | Fix proof of predicates completely | Yann Herklotz | 2023-06-02 | 2 | -7/+24 |
| | |||||
* | Fix top-level proof with Isetpred missing | Yann Herklotz | 2023-06-02 | 1 | -12/+55 |
| | |||||
* | Finished the propert version of from_predicated_sem_pred_expr2 | Yann Herklotz | 2023-06-02 | 7 | -44/+316 |
| | |||||
* | Finish from_predicated_sem_pred_expr | Yann Herklotz | 2023-05-31 | 1 | -8/+97 |
| | |||||
* | Remove unnecessary assumption from sem_merge_list | Yann Herklotz | 2023-05-30 | 1 | -4/+3 |
| | |||||
* | Fix other proofs and attempt from_predicated proof | Yann Herklotz | 2023-05-30 | 1 | -7/+26 |
| | |||||
* | Prove merge list_translation | Yann Herklotz | 2023-05-30 | 1 | -2/+16 |
| | |||||
* | Prove fold_right over Elist | Yann Herklotz | 2023-05-30 | 1 | -4/+74 |
| | |||||
* | Finish second flap2 proof | Yann Herklotz | 2023-05-30 | 1 | -1/+9 |
| | |||||
* | Finished painful product proof | Yann Herklotz | 2023-05-30 | 5 | -13/+127 |
| | |||||
* | Prove more admitted theorems | Yann Herklotz | 2023-05-29 | 6 | -47/+190 |
| | |||||
* | Finish two AbstrSemIdent false proofs | Yann Herklotz | 2023-05-28 | 1 | -11/+50 |
| | |||||
* | Finish max predicate proof | Yann Herklotz | 2023-05-28 | 1 | -1/+78 |
| | |||||
* | Finish proofs in GiblePargenproofForward.v | Yann Herklotz | 2023-05-28 | 2 | -5/+49 |
| | |||||
* | Work on forward proofs | Yann Herklotz | 2023-05-28 | 2 | -1/+18 |
| | |||||
* | Finish proofs in GiblePargenproofBackward.v | Yann Herklotz | 2023-05-27 | 1 | -26/+101 |
| | |||||
* | Add proofs of gather_predicates | Yann Herklotz | 2023-05-26 | 1 | -25/+196 |
| | |||||
* | Finish predicate inclusion proofs | Yann Herklotz | 2023-05-25 | 1 | -48/+99 |
| | |||||
* | Finish gather_predicate proofs | Yann Herklotz | 2023-05-24 | 1 | -17/+502 |
| | |||||
* | Prove evaluability of predicates throughout | Yann Herklotz | 2023-05-22 | 1 | -61/+126 |
| | |||||
* | Work on smaller evaluability proof | Yann Herklotz | 2023-05-22 | 1 | -49/+88 |
| | |||||
* | Finish abstr_seq_reverse_correct_fold | Yann Herklotz | 2023-05-21 | 3 | -35/+116 |
| | |||||
* | Add proof about preds_empty | Yann Herklotz | 2023-05-21 | 1 | -3/+12 |
| | |||||
* | Add proofs about RBexit | Yann Herklotz | 2023-05-21 | 1 | -2/+63 |
| | |||||
* | Prove evaluable_pred_expr_exists_RBsetpred | Yann Herklotz | 2023-05-21 | 5 | -100/+506 |
| | |||||
* | Work on evaluability proof | Yann Herklotz | 2023-05-19 | 1 | -0/+37 |
| | |||||
* | Prepare work on evaluability of instructions | Yann Herklotz | 2023-05-19 | 3 | -71/+133 |
| | |||||
* | Finish evaluability proof of RBop | Yann Herklotz | 2023-05-19 | 5 | -210/+338 |
| | |||||
* | Add new proofs about semantic identity | Yann Herklotz | 2023-05-18 | 5 | -600/+937 |
| | |||||
* | Work on scheduling proof | Yann Herklotz | 2023-05-16 | 4 | -25/+154 |
| | |||||
* | Add start of backward proof | Yann Herklotz | 2023-05-16 | 1 | -3/+39 |
| |