aboutsummaryrefslogtreecommitdiffstats
path: root/src
Commit message (Expand)AuthorAgeFilesLines
...
* Fix first part of istoreYann Herklotz2020-08-041-40/+43
* Fix iload proofYann Herklotz2020-08-042-43/+52
* Add proof of divisibilityYann Herklotz2020-08-041-21/+14
* Remove check mpassYann Herklotz2020-07-241-2/+0
* More renames to get it to compileYann Herklotz2020-07-244-6/+9
* Rename to VericertlibYann Herklotz2020-07-171-0/+0
* Change name to VericertYann Herklotz2020-07-1423-53/+52
* Fixes to operatorsYann Herklotz2020-07-074-6/+12
* Finished transl_condYann Herklotz2020-07-072-62/+45
* Only translate_cond leftYann Herklotz2020-07-074-17/+252
* No admitted in Deterministic proofYann Herklotz2020-07-073-14/+10
* A few operations leftYann Herklotz2020-07-071-30/+88
* Proof of TransfHTLLink DONEYann Herklotz2020-07-071-1/+14
* Rename asm to verilogYann Herklotz2020-07-061-9/+10
* Add top level backward simulationYann Herklotz2020-07-063-95/+191
* HTLgenproof compiles againYann Herklotz2020-07-064-22/+47
* Fix InopYann Herklotz2020-07-054-47/+58
* Fix HTLgenspecYann Herklotz2020-07-051-3/+4
* No addmitted in VeriloggenproofYann Herklotz2020-07-054-100/+245
* Remove admitted in mis_stepp_VdeclYann Herklotz2020-07-053-9/+12
* Finish most of VeriloggenproofYann Herklotz2020-07-055-31/+205
* Merge remote-tracking branch 'james/develop' into developYann Herklotz2020-07-042-12/+175
|\
| * Working on determinacy proof.James Pollard2020-07-042-12/+175
* | Define ofbytesYann Herklotz2020-07-041-1/+72
* | Make HTLgen compile againYann Herklotz2020-07-041-3/+11
|/
* Fixing HTLgenproofYann Herklotz2020-07-036-41/+67
* Add new value type to fix Iop proofYann Herklotz2020-07-035-67/+217
* Addition to int_add_v2Yann Herklotz2020-07-031-3/+13
* Updates to Iop proofYann Herklotz2020-07-033-92/+179
* Switch to uvalueToZ in lessdef.James Pollard2020-07-024-67/+87
* Complete ZToValue_valueToNat.James Pollard2020-07-022-31/+34
* Fix callstate proof.James Pollard2020-07-021-7/+7
* Stuck in Callstate proofYann Herklotz2020-07-021-20/+17
* Push current stateYann Herklotz2020-07-022-26/+46
* Remove all <> AdmittedYann Herklotz2020-07-022-23/+27
* Fix spec by adding details about reg valsYann Herklotz2020-07-022-36/+182
* Merge remote-tracking branch 'james/develop' into developYann Herklotz2020-07-015-451/+377
|\
| * Tidy up (?) automation slightly...James Pollard2020-07-011-20/+17
| * Improve (?) automation.James Pollard2020-07-015-451/+380
* | Merge remote-tracking branch 'james/develop' into developYann Herklotz2020-07-012-1721/+1629
|\|
| * 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
| |\
| * | Factor out lemmas in main induction proof.James Pollard2020-06-301-1669/+1813
| * | Fix stack frame issue.James Pollard2020-06-301-46/+25
* | | Add HTL pretty printerYann Herklotz2020-06-301-0/+81
* | | Add htl pretty printingYann Herklotz2020-06-305-1/+7
| |/ |/|
* | 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
| |\|
generated by cgit (git 2.34.1) at 2024-06-30 23:50:50 +0000