aboutsummaryrefslogtreecommitdiffstats
Commit message (Collapse)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
| |
generated by cgit (git 2.34.1) at 2024-07-01 01:20:23 +0000