aboutsummaryrefslogtreecommitdiffstats
path: root/src/translation/HTLgenspec.v
Commit message (Expand)AuthorAgeFilesLines
* Add RTLBlock intermediate languageYann Herklotz2020-08-301-641/+0
* Finished all the proofsv1.0.0Yann Herklotz2020-08-131-6/+6
* 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
* Remove HTLgen and create the specificationYann Herklotz2020-05-071-0/+92
generated by cgit (git 2.34.1) at 2024-07-01 12:22:44 +0000