aboutsummaryrefslogtreecommitdiffstats
path: root/src
Commit message (Collapse)AuthorAgeFilesLines
* Improve (?) automation.James Pollard2020-07-015-451/+380
|
* Remove some explicit evar instantiations.James Pollard2020-06-301-23/+28
|
* Heavy automation of proofs.James Pollard2020-06-302-307/+87
|
* Merge branch 'develop' of github.com:ymherklotz/coqup into developJames Pollard2020-06-303-10/+73
|\
| * Add command line flags for initial blockYann Herklotz2020-06-302-0/+15
| |
| * Merge branch 'develop' of github.com:ymherklotz/CoqUp into developYann Herklotz2020-06-302-36/+210
| |\
| | * Merge pull request #8 from p0llard/developYann Herklotz2020-06-302-36/+210
| | |\ | | | | | | | | Eliminate memory bounds assumptions
| * | | Make the proofs more conciseYann Herklotz2020-06-301-17/+21
| |/ /
| * | Add equivalence between int add value addYann Herklotz2020-06-301-10/+54
| | |
* | | 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-293-8/+30
|\|
| * Develop compiles againYann Herklotz2020-06-293-8/+10
| |
| * Merge remote-tracking branch 'james/arrays-proof' into developYann Herklotz2020-06-291-0/+34
| |\
| * | Work on addition proofYann Herklotz2020-06-291-1/+21
| | |
* | | Eliminate memory bounds assumption!James Pollard2020-06-292-37/+211
| |/ |/|
* | Add missing file.James Pollard2020-06-291-0/+34
|/
* Fix proof again with Verilog semantics changesYann Herklotz2020-06-282-1/+23
|
* Merge remote-tracking branch 'james/arrays-proof' into developYann Herklotz2020-06-285-101/+961
|\
| * 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-282-69/+305
| |
| * Fix unsigned/signed issues.James Pollard2020-06-284-97/+92
| |
| * Work on proof.James Pollard2020-06-284-2/+405
| |
* | Fix Verilog semantics and fix order of always blocksYann Herklotz2020-06-263-8/+5
| |
* | Progress on proof of VeriloggenYann Herklotz2020-06-253-15/+24
| |
* | Work on Veriloggen proofYann Herklotz2020-06-253-6/+55
| |
* | 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-242-9/+5
|\
| * Fixes to make develop compileYann Herklotz2020-06-244-8/+6
| |
* | Merge branch 'develop' of github.com:ymherklotz/coqup into arrays-proofJames Pollard2020-06-247-113/+219
|\|
| * Merge branch 'master' into developYann Herklotz2020-06-243-81/+96
| |\
| | * Fix assumption of mainYann Herklotz2020-06-243-83/+97
| | |
| * | More to proofYann Herklotz2020-06-231-7/+9
| | |
| * | Merge branch 'master' into developYann Herklotz2020-06-223-9/+58
| |\|
| | * Admit everything temporarilyYann Herklotz2020-06-223-9/+58
| | |
| * | Admit the value proofYann Herklotz2020-06-221-3/+5
| | |
| * | Merge branch 'arrays-proof' into developYann Herklotz2020-06-223-31/+204
| |\ \
| * \ \ Merge branch 'master' into developYann Herklotz2020-06-223-18/+33
| |\ \ \ | | | |/ | | |/|
| | * | Only print out main as everything is inlinedYann Herklotz2020-06-221-8/+10
| | | |
| | * | Add print for debug always block in moduleYann Herklotz2020-06-222-6/+19
| | | |
| | * | Some fixes, but still buggy probablyYann Herklotz2020-06-201-2/+2
| | | |
| | * | Add bugs to support more operationsYann Herklotz2020-06-201-4/+4
| | | |
| * | | Add proof of nat equivYann Herklotz2020-06-201-2/+15
| | | |
| * | | Merge remote-tracking branch 'james/arrays-proof' into developYann Herklotz2020-06-209-111/+725
| |\ \ \ | | |/ / | |/| |
| * | | Add more unproven instructions, Admitted equiv to specYann Herklotz2020-06-144-23/+31
| | | |
* | | | Finish ILoad proof with some assumptions:James Pollard2020-06-243-192/+197
| | | | | | | | | | | | | | | | | | | | | | | | * 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-235-272/+523
| | | |
* | | | Finish off Load proof sketches.James Pollard2020-06-221-35/+17
| | | |
generated by cgit (git 2.34.1) at 2024-07-05 00:43:07 +0000