aboutsummaryrefslogtreecommitdiffstats
Commit message (Expand)AuthorAgeFilesLines
* 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
| * | Move forall_ptree into commonYann Herklotz2022-03-222-42/+43
| * | Fix proofs in Sat.vYann Herklotz2022-03-221-1/+1
| * | Remove main binaryYann Herklotz2022-03-221-0/+0
| * | Fix Makefiles in build and for benchmarksYann Herklotz2022-03-226-7/+17
| * | Add RTLBlockgenproofYann Herklotz2022-03-221-0/+52
| * | Delete extra data files and scriptsYann Herklotz2022-03-2216-286/+6
| |/
| * Update permissions and .gitignoreYann Herklotz2022-03-173-3/+11
| * Add a license to synthesis-resultsYann Herklotz2022-03-171-0/+15
| * Clean up scripts some moreYann Herklotz2022-03-176-40/+10
| * Update documentation filesYann Herklotz2022-03-178-35/+78
| * Remove more unnecessary scriptsYann Herklotz2022-03-173-133/+0