aboutsummaryrefslogtreecommitdiffstats
path: root/src/translation/HTLgenproof.v
Commit message (Collapse)AuthorAgeFilesLines
* Add html generation and clean Coq filesYann Herklotz2020-08-131-2/+1
|
* Finished all the proofsv1.0.0Yann Herklotz2020-08-131-31/+37
| | | | Removed support for case statements temporarily.
* Remove unnecessary commented proofYann Herklotz2020-08-121-23/+0
|
* Finish proof of conditionalsYann Herklotz2020-08-121-4/+11
|
* Nearly finished all proofsYann Herklotz2020-08-121-48/+228
|
* Remove alignment constraint during translation.James Pollard2020-08-111-55/+59
| | | | This is now inferred from the memory model.
* Remove last admits from istoreYann Herklotz2020-08-041-2/+3
|
* Finish istore and iload without any admitsYann Herklotz2020-08-041-118/+113
|
* No admitted in iload proofYann Herklotz2020-08-041-38/+72
|
* Merge remote-tracking branch 'james/develop' into developYann Herklotz2020-08-041-5/+6
|\
| * Fix broken proof.James Pollard2020-08-041-5/+6
| |
* | Add expr_ok proofYann Herklotz2020-08-041-11/+25
|/
* Fix first part of istoreYann Herklotz2020-08-041-40/+43
|
* Fix iload proofYann Herklotz2020-08-041-43/+48
|
* Add proof of divisibilityYann Herklotz2020-08-041-21/+14
|
* More renames to get it to compileYann Herklotz2020-07-241-2/+3
|
* Change name to VericertYann Herklotz2020-07-141-10/+9
|
* Fixes to operatorsYann Herklotz2020-07-071-2/+5
|
* Finished transl_condYann Herklotz2020-07-071-58/+45
|
* Only translate_cond leftYann Herklotz2020-07-071-6/+197
|
* No admitted in Deterministic proofYann Herklotz2020-07-071-2/+2
|
* A few operations leftYann Herklotz2020-07-071-30/+88
|
* Proof of TransfHTLLink DONEYann Herklotz2020-07-071-1/+14
|
* Add top level backward simulationYann Herklotz2020-07-061-72/+77
|
* HTLgenproof compiles againYann Herklotz2020-07-061-14/+30
| | | | - Commented out Iload, Istore proofs for now
* Fix InopYann Herklotz2020-07-051-11/+14
|
* No addmitted in VeriloggenproofYann Herklotz2020-07-051-1/+0
| | | | However, there may have been breaking changes to HTLgenproof.
* Make HTLgen compile againYann Herklotz2020-07-041-3/+11
|
* Fixing HTLgenproofYann Herklotz2020-07-031-13/+32
|
* Updates to Iop proofYann Herklotz2020-07-031-89/+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-021-14/+1
|
* Tidy up (?) automation slightly...James Pollard2020-07-011-20/+17
|
* Improve (?) automation.James Pollard2020-07-011-407/+301
|
* 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.
* 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-281-68/+809
|\
| * 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-281-64/+46
| |
generated by cgit (git 2.34.1) at 2024-07-05 21:35:55 +0000