aboutsummaryrefslogtreecommitdiffstats
path: root/src/translation
Commit message (Expand)AuthorAgeFilesLines
...
* | | Lea op now checks alignment.James Pollard2020-06-211-12/+15
* | | Finish structure of Aindexed2scaled ILoad proof.James Pollard2020-06-201-14/+172
| |/ |/|
* | Working on proof.James Pollard2020-06-191-10/+86
* | Enforce stack size alignment to fix proof.James Pollard2020-06-183-10/+22
* | Tidy up proof.James Pollard2020-06-181-12/+15
* | Finish AInStack proof with minor assertions.James Pollard2020-06-181-32/+21
* | Fix up ILoad proof.James Pollard2020-06-181-95/+58
* | Fix Inop proof to work with new array semantics.James Pollard2020-06-171-7/+36
* | Some (very) useful lemmas about arrays.James Pollard2020-06-171-4/+32
* | Use NBAs for loads and stores.James Pollard2020-06-172-4/+4
* | Array semantics now uses dependent Array type.James Pollard2020-06-142-9/+10
* | Fix broken proof.James Pollard2020-06-121-4/+4
* | Merge branch 'master' into arrays-proofJames Pollard2020-06-121-4/+6
|\|
| * Fix addressing bug.James Pollard2020-06-121-4/+6
* | Merge branch 'master' into arrays-proofJames Pollard2020-06-126-834/+205
|\|
| * Add declaration of loadsYann Herklotz2020-06-122-4/+6
| * Fix declaring function arguments correctlyYann Herklotz2020-06-122-9/+66
| * Remove Verilog proofsYann Herklotz2020-06-122-132/+4
| * Declare all registers properly in HTLYann Herklotz2020-06-123-51/+95
| * Generate Verilog from HTLYann Herklotz2020-06-121-644/+40
* | Some work on store proof.James Pollard2020-06-121-11/+38
* | Rough outline of stack address proofJames Pollard2020-06-112-30/+105
* | Working on proof.James Pollard2020-06-113-41/+136
|/
* Start fixing proofJames Pollard2020-06-091-94/+116
* Fix automation tactic for modified constructorJames Pollard2020-06-091-2/+4
* Start extending HTL proof to cover arrays.James Pollard2020-06-091-18/+31
* Merge branch 'develop' into arrays-proofJames Pollard2020-06-091-31/+92
|\
| * Finished main proof with small assumptionsYann Herklotz2020-06-042-34/+94
* | Fix HTLgenspec proof for arrays.James Pollard2020-06-031-31/+43
* | Merge branch 'develop' into arrays-proofJames Pollard2020-06-032-47/+45
|\|
| * Uncomment proofYann Herklotz2020-06-032-43/+41
* | HTLgenspec status in line with developJames Pollard2020-06-032-26/+56
* | Copy over load/store from Veriloggen to HTLgen.James Pollard2020-06-031-5/+36
* | Merge branch 'develop' into arrays-proofJames Pollard2020-06-032-4/+30
|\|
| * Add proof to final_statesYann Herklotz2020-06-021-1/+3
| * Add proof for initial stateYann Herklotz2020-06-022-3/+27
* | Keep track of declarations in HTLgen.James Pollard2020-06-031-23/+62
* | Merge branch 'develop' into arrays-proofJames Pollard2020-06-023-82/+152
|\|
| * Get whole proof to compileYann Herklotz2020-06-021-14/+17
| * Shorten the proof a bitYann Herklotz2020-06-021-41/+15
| * Add proof for equivalence of movYann Herklotz2020-06-022-38/+110
| * Add lemmas for preservation of globalsYann Herklotz2020-06-012-29/+50
* | Merge branch 'develop' into arrays-proofJames Pollard2020-06-011-5/+4
|\|
| * Small optimisations to proofYann Herklotz2020-05-311-5/+4
* | Merge branch 'develop' into arrays-proofJames Pollard2020-05-306-162/+1327
|\|
| * 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-293-25/+34
| |/
| * Change AssocMap to Maps.PTreeYann Herklotz2020-05-291-3/+5
| * Add more proofs and remove AdmittedYann Herklotz2020-05-271-49/+43
generated by cgit (git 2.34.1) at 2024-07-07 12:57:40 +0000