aboutsummaryrefslogtreecommitdiffstats
Commit message (Collapse)AuthorAgeFilesLines
* Add new block generation for GibleYann Herklotz2022-05-266-457/+298
|
* Translate the base languagesYann Herklotz2022-05-257-437/+431
|
* Famous proven but not tested has been fixedYann Herklotz2022-05-124-14/+14
|
* Completely finish RTLBlockgenproofYann Herklotz2022-05-122-24/+171
|
* Remove imm_succ from match_blockYann Herklotz2022-05-121-100/+27
|
* Add rest of the proofsYann Herklotz2022-05-121-12/+272
|
* Up to Icall is now provenYann Herklotz2022-05-122-86/+382
|
* Try to expand the definition of match_codeYann Herklotz2022-05-121-23/+35
|
* Finish Inop proof for basic block generationYann Herklotz2022-05-111-12/+24
|
* Add new definitions of match_codeYann Herklotz2022-05-111-8/+13
|
* Change the specification of the RTLBlockgenproofYann Herklotz2022-05-091-31/+45
|
* Try to work on refining the match_states predicateYann Herklotz2022-05-061-9/+22
|
* Try out a new match_code predicateYann Herklotz2022-04-251-13/+30
|
* Work on proof of InopYann Herklotz2022-04-241-32/+145
|
* Fix translation passes with new semanticsYann Herklotz2022-04-235-72/+75
|
* Change the definition of RTLBlockYann Herklotz2022-04-212-97/+93
|
* Work on smallstep proofYann Herklotz2022-04-211-2/+22
|
* Start work on Inop proofYann Herklotz2022-04-201-0/+3
|
* Extract some lemmas from the main proofYann Herklotz2022-04-182-24/+87
|
* Proof of the initial state matchingYann Herklotz2022-04-122-3/+38
|
* Add intermediate filesYann Herklotz2022-04-084-78/+143
|
* Work on the match_states definitionYann Herklotz2022-04-053-17/+26
|
* Add basic blocks to the stackframeYann Herklotz2022-04-055-32/+54
|
* Add whole basic block into stateYann Herklotz2022-04-023-73/+48
|
* Merge branch 'dev/scheduling'Yann Herklotz2022-03-31130-1639/+9403
|\
| * Add list of bb to semanticsYann Herklotz2022-03-317-96/+99
| |
| * Work on semantics for RTLBlockInstrYann Herklotz2022-03-284-22/+57
| |
| * Add specification for RTLBlockgenproofYann Herklotz2022-03-282-16/+53
| |
| * Work on specification of RTLBlock generationYann Herklotz2022-03-284-162/+258
| |
| * Add to documentationYann Herklotz2022-03-286-29/+69
| |
| * Add vericert logoYann Herklotz2022-03-261-0/+500
| |
| * Add theme optionsYann Herklotz2022-03-261-0/+19
| |
| * Add sphinx documentationYann Herklotz2022-03-2623-93/+854
| |
| * Add more files to .gitignoreYann Herklotz2022-03-261-0/+3
| |
| * Remove literal files againYann Herklotz2022-03-2626-3770/+582
| |
| * Add more documentationYann Herklotz2022-03-247-268/+207
| |
| * Force _CoqProject generation and fix namespacesYann Herklotz2022-03-241-5/+2
| |
| * Update makefile and remove _CoqProjectYann Herklotz2022-03-242-23/+11
| |
| * Rename lit directoryYann Herklotz2022-03-249-16/+137
| |
| * Rename changelogYann Herklotz2022-03-241-0/+0
| |
| * Change origin of tangled filesYann Herklotz2022-03-239-22/+20
| |
| * Create a few more org files about specific topicsYann Herklotz2022-03-233-1011/+1070
| |
| * Add back equalitiesYann Herklotz2022-03-222-126/+117
| |
| * Add first descriptions to org fileYann Herklotz2022-03-224-183/+199
| |
| * Merge remote-tracking branch 'origin/dev/scheduling' into dev/schedulingYann Herklotz2022-03-220-0/+0
| |\
| | * Delete extra data files and scriptsYann Herklotz2022-03-1915-286/+6
| | |
| * | Add literate Coq fileYann Herklotz2022-03-224-9/+3287
| | |
| * | Add comments to allow for literate detanglingYann Herklotz2022-03-227-18/+362
| | |
| * | Add nops to partition generationYann Herklotz2022-03-221-4/+4
| | |
| * | Add to benchmark scriptYann Herklotz2022-03-221-36/+70
| | |
generated by cgit (git 2.34.1) at 2024-07-05 05:22:40 +0000