aboutsummaryrefslogtreecommitdiffstats
path: root/src/translation/HTLgenspec.v
Commit message (Collapse)AuthorAgeFilesLines
* Add RTLBlock intermediate languageYann Herklotz2020-08-301-641/+0
|
* Finished all the proofsv1.0.0Yann Herklotz2020-08-131-6/+6
| | | | Removed support for case statements temporarily.
* Change name to VericertYann Herklotz2020-07-141-2/+2
|
* Only translate_cond leftYann Herklotz2020-07-071-0/+18
|
* Fix InopYann Herklotz2020-07-051-8/+22
|
* Fix HTLgenspecYann Herklotz2020-07-051-3/+4
|
* Fixing HTLgenproofYann Herklotz2020-07-031-4/+4
|
* Fix spec by adding details about reg valsYann Herklotz2020-07-021-22/+181
|
* Improve (?) automation.James Pollard2020-07-011-1/+1
|
* Merge branch 'develop' of github.com:ymherklotz/coqup into arrays-proofJames Pollard2020-06-241-53/+22
|\
| * Merge branch 'master' into developYann Herklotz2020-06-241-55/+24
| |\
| | * Fix assumption of mainYann Herklotz2020-06-241-56/+25
| | |
| * | Merge branch 'master' into developYann Herklotz2020-06-221-3/+3
| |\|
| | * Admit everything temporarilyYann Herklotz2020-06-221-3/+3
| | |
| * | Merge remote-tracking branch 'james/arrays-proof' into developYann Herklotz2020-06-201-7/+20
| |\ \ | | |/ | |/|
| * | Add more unproven instructions, Admitted equiv to specYann Herklotz2020-06-141-2/+2
| | |
* | | Normalise entire expression to avoid overflow issues.James Pollard2020-06-231-3/+4
| | |
* | | Tidy up proof for Aindexed2scaled.James Pollard2020-06-221-1/+6
| |/ |/|
* | Enforce stack size alignment to fix proof.James Pollard2020-06-181-1/+2
| |
* | Use NBAs for loads and stores.James Pollard2020-06-171-2/+2
| |
* | Fix broken proof.James Pollard2020-06-121-4/+4
| |
* | Merge branch 'master' into arrays-proofJames Pollard2020-06-121-24/+81
|\|
| * Add declaration of loadsYann Herklotz2020-06-121-4/+5
| |
| * Fix declaring function arguments correctlyYann Herklotz2020-06-121-3/+59
| |
| * Declare all registers properly in HTLYann Herklotz2020-06-121-17/+17
| |
* | Working on proof.James Pollard2020-06-111-3/+15
|/
* Fix HTLgenspec proof for arrays.James Pollard2020-06-031-31/+43
|
* Merge branch 'develop' into arrays-proofJames Pollard2020-06-031-35/+38
|\
| * Uncomment proofYann Herklotz2020-06-031-31/+34
| |
* | HTLgenspec status in line with developJames Pollard2020-06-031-25/+54
|/
* Add proof for equivalence of movYann Herklotz2020-06-021-15/+17
|
* Small optimisations to proofYann Herklotz2020-05-311-5/+4
|
* Merge branch 'develop' of github.com:ymherklotz/CoqUp into developYann Herklotz2020-05-291-6/+3
|\
| * Improve automation in HTLgenspec.James Pollard2020-05-291-6/+3
| |
* | Fix compilation moving to PTreeYann Herklotz2020-05-291-2/+2
|/
* Add top level definitionYann Herklotz2020-05-271-60/+65
|
* Working on automationYann Herklotz2020-05-261-62/+48
|
* Finished proof of spec completelyYann Herklotz2020-05-261-3/+61
|
* Finished second pass and fixed bugYann Herklotz2020-05-261-17/+36
|
* Finished proving the first caseYann Herklotz2020-05-251-1/+6
|
* Continuing work on proving specificationYann Herklotz2020-05-251-15/+212
|
* Finish the proof with most assumptionsYann Herklotz2020-05-211-1/+1
|
* Add proof of translation correctnessYann Herklotz2020-05-201-8/+8
| | | | Modified-by: Yann Herklotz <git@yannherklotz.com>
* Remove HTLgen and create the specificationYann Herklotz2020-05-071-0/+92
generated by cgit (git 2.34.1) at 2024-07-05 19:07:46 +0000