aboutsummaryrefslogtreecommitdiffstats
Commit message (Collapse)AuthorAgeFilesLines
* Tidy up proof for Aindexed2scaled.James Pollard2020-06-224-90/+231
|
* Factor out addressing checks, check signed range.James Pollard2020-06-211-10/+17
|
* Lea op now checks alignment.James Pollard2020-06-211-12/+15
|
* Finish structure of Aindexed2scaled ILoad proof.James Pollard2020-06-202-14/+177
|
* 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-182-13/+16
|
* Finish AInStack proof with minor assertions.James Pollard2020-06-181-32/+21
|
* Fix up ILoad proof.James Pollard2020-06-181-95/+58
|
* Fix array semantics behaviour for undefined values.James Pollard2020-06-181-1/+1
|
* Fix Inop proof to work with new array semantics.James Pollard2020-06-172-7/+44
|
* Some (very) useful lemmas about arrays.James Pollard2020-06-173-7/+139
|
* Use NBAs for loads and stores.James Pollard2020-06-172-4/+4
|
* Fix array semantics merge granularity.James Pollard2020-06-174-30/+87
|
* Array semantics now uses dependent Array type.James Pollard2020-06-145-49/+50
|
* Move some standard tactics to Coquplib.James Pollard2020-06-141-0/+10
|
* Add a basic length-indexed list type.James Pollard2020-06-131-0/+123
|
* Merge branch 'develop' into arrays-proofJames Pollard2020-06-123-4/+27
|\
| * Update matrix and use 32 bitYann Herklotz2020-06-123-12/+14
| |
| * Add matrix testYann Herklotz2020-06-121-0/+21
| |
* | Fix broken proof.James Pollard2020-06-121-4/+4
| |
* | Merge branch 'master' into arrays-proofJames Pollard2020-06-121-4/+6
|\|
| * Merge pull request #7 from p0llard/hotfixYann Herklotz2020-06-121-4/+6
| |\ | | | | | | Fix addressing bug.
| | * Fix addressing bug.James Pollard2020-06-121-4/+6
| |/
* | Merge branch 'master' into arrays-proofJames Pollard2020-06-1234-1046/+19571
|\|
| * Add declaration of loadsYann Herklotz2020-06-122-4/+6
| |
| * Merge branch 'master' of github.com:ymherklotz/CoqUpYann Herklotz2020-06-1215-0/+19189
| |\
| | * Merge pull request #6 from ymherklotz/branch_jcYann Herklotz2020-06-1215-0/+19189
| | |\ | | | | | | | | Branch jc
| | | * fixed my grammarJianyi Cheng2020-06-121-2/+2
| | | |
| | | * Adding benchmarks to branch_jcJianyi Cheng2020-06-1215-0/+19189
| | |/
| * / Fix declaring function arguments correctlyYann Herklotz2020-06-123-12/+69
| |/
| * Add function call testYann Herklotz2020-06-121-0/+10
| |
| * Update compcert to always inline functionsYann Herklotz2020-06-121-0/+0
| |
| * Fix main functionYann Herklotz2020-06-121-17/+3
| |
| * Add array to testYann Herklotz2020-06-122-1/+5
| |
| * Fix printing of Verilog with new datatypesYann Herklotz2020-06-122-17/+27
| |
| * Remove Verilog proofsYann Herklotz2020-06-123-133/+10
| |
| * Declare all registers properly in HTLYann Herklotz2020-06-123-51/+95
| |
| * Remove extraction of simulatorYann Herklotz2020-06-121-2/+2
| |
| * Fix top level invocation to translate through HTLYann Herklotz2020-06-122-4/+8
| |
| * Remove Test.vYann Herklotz2020-06-121-99/+0
| |
| * Generate Verilog from HTLYann Herklotz2020-06-122-713/+154
| |
| * Merge pull request #5 from p0llard/arrays-proofYann Herklotz2020-06-107-351/+643
| |\ | | | | | | Array/memory functionality
* | | Some work on store proof.James Pollard2020-06-121-11/+38
| | |
* | | Rough outline of stack address proofJames Pollard2020-06-113-34/+109
| | |
* | | Working on proof.James Pollard2020-06-115-47/+156
| |/ |/|
* | 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-098-56/+1160
|\|
generated by cgit (git 2.34.1) at 2024-07-07 18:16:56 +0000