aboutsummaryrefslogtreecommitdiffstats
path: root/src/translation
Commit message (Expand)AuthorAgeFilesLines
* Add html generation and clean Coq filesYann Herklotz2020-08-131-2/+1
* Finished all the proofsv1.0.0Yann Herklotz2020-08-133-39/+46
* 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
* 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
* Fix InopYann Herklotz2020-07-054-47/+58
* Fix HTLgenspecYann Herklotz2020-07-051-3/+4
* No addmitted in VeriloggenproofYann Herklotz2020-07-053-92/+233
* 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
* 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-03 12:16:04 +0000