aboutsummaryrefslogtreecommitdiffstats
Commit message (Expand)AuthorAgeFilesLines
...
| * | | | | | | | | | | | | | Better mm checkNadesh Ramanathan2020-06-131-0/+23
| * | | | | | | | | | | | | | Writing to an arrayNadesh Ramanathan2020-06-131-0/+12
* | | | | | | | | | | | | | | Change name to VericertYann Herklotz2020-07-1435-136/+135
| |_|_|_|_|_|_|_|_|_|_|_|_|/ |/| | | | | | | | | | | | |
* | | | | | | | | | | | | | 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
* | | | | | | | | | Merge branch 'develop' of github.com:ymherklotz/coqup into developJames Pollard2020-07-020-0/+0
|\ \ \ \ \ \ \ \ \ \
| * | | | | | | | | | Typo fixYann Herklotz2020-07-021-1/+1
* | | | | | | | | | | 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 developdev-nadesh-mergeYann 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-305-17/+80
| |\ \ \ \ \ \ \ \ \ | | | |_|_|_|_|_|_|/ | | |/| | | | | | |
| * | | | | | | | | 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-308-12/+23
| |/ / / / / / / / |/| | | | | | | |
* | | | | | | | | Add command line flags for initial blockYann Herklotz2020-06-304-7/+22
* | | | | | | | | 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
| |\| | | | | | | |
| | * | | | | | | | Merge branch 'develop' into arrays-proofJames Pollard2020-06-294-8/+31
| | |\ \ \ \ \ \ \ \
| | * | | | | | | | | Eliminate memory bounds assumption!James Pollard2020-06-292-37/+211
generated by cgit (git 2.34.1) at 2024-07-09 04:32:56 +0000