aboutsummaryrefslogtreecommitdiffstats
Commit message (Expand)AuthorAgeFilesLines
* 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.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
| | |\
| | | * 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
| |\
* | | 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
|\|
| * Add optimisationsYann Herklotz2020-06-051-0/+1
| * Add dhrystone benchmarkYann Herklotz2020-06-054-0/+1003
| * Finished main proof with small assumptionsYann Herklotz2020-06-045-59/+157
* | Fix HTLgenspec proof for arrays.James Pollard2020-06-031-31/+43
* | Merge branch 'develop' into arrays-proofJames Pollard2020-06-033-47/+50
|\|
| * Uncomment proofYann Herklotz2020-06-033-43/+46
* | HTLgenspec status in line with developJames Pollard2020-06-033-26/+57
* | Copy over load/store from Veriloggen to HTLgen.James Pollard2020-06-031-5/+36
* | Merge branch 'develop' into arrays-proofJames Pollard2020-06-033-6/+32
|\|
| * Add proof to final_statesYann Herklotz2020-06-022-3/+5
| * Add proof for initial stateYann Herklotz2020-06-022-3/+27
* | Keep track of declarations in HTLgen.James Pollard2020-06-031-23/+62
* | Update HTL semantics to support arrays.James Pollard2020-06-022-19/+32
* | Merge branch 'develop' into arrays-proofJames Pollard2020-06-024-84/+185
|\|
generated by cgit (git 2.34.1) at 2024-07-03 11:06:11 +0000