aboutsummaryrefslogtreecommitdiffstats
path: root/src/translation
Commit message (Expand)AuthorAgeFilesLines
* Merge branch 'dev-nadesh-merge' into dev-nadeshdev-nadeshYann Herklotz2020-07-025-354/+2009
|\
| * Tidy up (?) automation slightly...James Pollard2020-07-011-20/+17
| * Improve (?) automation.James Pollard2020-07-012-408/+302
| * Remove some explicit evar instantiations.James Pollard2020-06-301-23/+28
| * Heavy automation of proofs.James Pollard2020-06-301-306/+79
| * Factor out lemmas in main induction proof.James Pollard2020-06-301-1669/+1813
| * Fix stack frame issue.James Pollard2020-06-301-46/+25
| * Merge branch 'develop' into arrays-proofJames Pollard2020-06-292-7/+9
| |\
| | * Develop compiles againYann Herklotz2020-06-293-8/+10
| * | Eliminate memory bounds assumption!James Pollard2020-06-291-35/+209
| |/
| * Fix proof again with Verilog semantics changesYann Herklotz2020-06-281-1/+11
| * Merge remote-tracking branch 'james/arrays-proof' into developYann Herklotz2020-06-282-80/+825
| |\
| | * Finish store proof modulo:James Pollard2020-06-281-1/+206
| | * Fix second IStore proof.James Pollard2020-06-281-29/+50
| | * Finish first IStore proof (modulo some admissions).James Pollard2020-06-281-57/+293
| | * Fix unsigned/signed issues.James Pollard2020-06-282-76/+62
| | * Work on proof.James Pollard2020-06-281-2/+299
| * | Fix Verilog semantics and fix order of always blocksYann Herklotz2020-06-262-7/+4
| * | Progress on proof of VeriloggenYann Herklotz2020-06-251-14/+19
| * | Work on Veriloggen proofYann Herklotz2020-06-252-3/+51
| * | Finish Internal main proofYann Herklotz2020-06-241-14/+29
| |/
| * HTLgenproof passing.arrays-proofJames Pollard2020-06-242-50/+127
| * Merge branch 'develop' into arrays-proofJames Pollard2020-06-241-3/+2
| |\
| | * Fixes to make develop compileYann Herklotz2020-06-243-3/+3
| * | Merge branch 'develop' of github.com:ymherklotz/coqup into arrays-proofJames Pollard2020-06-243-96/+166
| |\|
| | * Merge branch 'master' into developYann Herklotz2020-06-243-81/+96
| | |\
| | | * Fix assumption of mainYann Herklotz2020-06-243-83/+97
| | * | Merge branch 'master' into developYann Herklotz2020-06-223-9/+58
| | |\|
| | * | Merge branch 'arrays-proof' into developYann Herklotz2020-06-222-31/+199
| | |\ \
| | * \ \ Merge branch 'master' into developYann Herklotz2020-06-221-5/+5
| | |\ \ \
| | * \ \ \ Merge remote-tracking branch 'james/arrays-proof' into developYann Herklotz2020-06-204-71/+369
| | |\ \ \ \
| * | | | | | Finish ILoad proof with some assumptions:James Pollard2020-06-242-8/+34
| * | | | | | Normalise entire expression to avoid overflow issues.James Pollard2020-06-233-272/+278
| * | | | | | Finish off Load proof sketches.James Pollard2020-06-221-35/+17
| * | | | | | Start Aindexed proof.James Pollard2020-06-222-19/+226
| * | | | | | Tidy up proof for Aindexed2scaled.James Pollard2020-06-223-89/+177
| | |_|_|/ / | |/| | | |
| * | | | | 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-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
| |\ \ \ \
generated by cgit (git 2.34.1) at 2024-07-05 21:17:54 +0000