aboutsummaryrefslogtreecommitdiffstats
path: root/src/translation
Commit message (Collapse)AuthorAgeFilesLines
* Add html generation and clean Coq filesYann Herklotz2020-08-131-2/+1
|
* Finished all the proofsv1.0.0Yann Herklotz2020-08-133-39/+46
| | | | 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-112-67/+69
| | | | 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-145-19/+18
|
* Fixes to operatorsYann Herklotz2020-07-072-3/+8
|
* Finished transl_condYann Herklotz2020-07-072-62/+45
|
* Only translate_cond leftYann Herklotz2020-07-073-16/+249
|
* 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-054-47/+58
|
* Fix HTLgenspecYann Herklotz2020-07-051-3/+4
|
* No addmitted in VeriloggenproofYann Herklotz2020-07-053-92/+233
| | | | However, there may have been breaking changes to HTLgenproof.
* Remove admitted in mis_stepp_VdeclYann Herklotz2020-07-052-5/+9
|
* Finish most of VeriloggenproofYann Herklotz2020-07-052-24/+196
|
* Make HTLgen compile againYann Herklotz2020-07-041-3/+11
|
* 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
|/
generated by cgit (git 2.34.1) at 2024-07-09 06:04:42 +0000