aboutsummaryrefslogtreecommitdiffstats
path: root/src/translation
Commit message (Collapse)AuthorAgeFilesLines
* Fixing HTLgenproofYann Herklotz2020-07-033-28/+47
|
* Add new value type to fix Iop proofYann Herklotz2020-07-031-2/+2
|
* Updates to Iop proofYann Herklotz2020-07-032-91/+101
|
* Switch to uvalueToZ in lessdef.James Pollard2020-07-021-36/+31
|
* Complete ZToValue_valueToNat.James Pollard2020-07-021-22/+16
|
* Fix callstate proof.James Pollard2020-07-021-7/+7
|
* Stuck in Callstate proofYann Herklotz2020-07-021-20/+17
|
* Push current stateYann Herklotz2020-07-021-26/+44
|
* Remove all <> AdmittedYann Herklotz2020-07-021-23/+12
|
* Fix spec by adding details about reg valsYann Herklotz2020-07-022-36/+182
|
* 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
| | | | | | | | | | We never cons a stack frame since we don't support calls (aside from the initial call which doesn't push a stack frame); removing the cons constructor solves the issue regarding memory separation. This means we now _can't_ support calls even if we wanted to, but due to the way we implement memory, we would need quite a lot of extra work to support this.
* 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
| | | | | | | | | | | | | | * EXPR_OK proofs (Yann). * Trivial register size proof (i.e. register values < 2^32). * Read bounds (to be extracted from RTL semantics). * Stack frame proof issues.
| * 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.James 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
| |\|
| | * Admit everything temporarilyYann 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
| |\ \ \ | | | |/ | | |/|
| | * | Some fixes, but still buggy probablyYann Herklotz2020-06-201-2/+2
| | | |
| | * | Add bugs to support more operationsYann Herklotz2020-06-201-4/+4
| | | |
| * | | Merge remote-tracking branch 'james/arrays-proof' into developYann Herklotz2020-06-204-71/+369
| |\ \ \ | | |/ / | |/| |
| * | | Add more unproven instructions, Admitted equiv to specYann Herklotz2020-06-142-21/+26
| | | |
* | | | Finish ILoad proof with some assumptions:James Pollard2020-06-242-8/+34
| | | | | | | | | | | | | | | | | | | | | | | | * EXPR_OK: Yann to work on this. * READ_BOUNDS: To axiomise (or find a better solution). * 32-bit range of register values.
* | | | 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
| | |
generated by cgit (git 2.34.1) at 2024-07-07 22:34:54 +0000