aboutsummaryrefslogtreecommitdiffstats
Commit message (Expand)AuthorAgeFilesLines
...
* | | | | | | | | | | 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
* | | | | | | | | | | Make the proofs more conciseYann Herklotz2020-06-301-17/+21
|/ / / / / / / / / /
* | / / / / / / / / Add equivalence between int add value addYann Herklotz2020-06-301-10/+54
| |/ / / / / / / / |/| | | | | | | |
* | | | | | | | | Develop compiles againYann Herklotz2020-06-294-8/+11
* | | | | | | | | Merge remote-tracking branch 'james/arrays-proof' into developYann Herklotz2020-06-291-0/+34
|\| | | | | | | |
| * | | | | | | | Add missing file.James Pollard2020-06-291-0/+34
| | |_|_|_|_|_|/ | |/| | | | | |
* / | | | | | | Work on addition proofYann Herklotz2020-06-291-1/+21
|/ / / / / / /
* | | | | | | Fix proof again with Verilog semantics changesYann Herklotz2020-06-282-1/+23
* | | | | | | Merge remote-tracking branch 'james/arrays-proof' into developYann Herklotz2020-06-285-101/+961
|\ \ \ \ \ \ \
| * | | | | | | Finish store proof modulo:James Pollard2020-06-281-1/+206
| * | | | | | | Fix second IStore proof.James Pollard2020-06-281-29/+50
| * | | | | | | Finish first IStore proof (modulo some admissions).James Pollard2020-06-282-69/+305
| * | | | | | | Fix unsigned/signed issues.James Pollard2020-06-284-97/+92
| * | | | | | | Work on proof.James Pollard2020-06-284-2/+405
* | | | | | | | Add yosys to dependenciesYann Herklotz2020-06-282-2/+2
* | | | | | | | Fix Verilog semantics and fix order of always blocksYann Herklotz2020-06-263-8/+5
* | | | | | | | Progress on proof of VeriloggenYann Herklotz2020-06-253-15/+24
* | | | | | | | Work on Veriloggen proofYann Herklotz2020-06-253-6/+55
* | | | | | | | Finish Internal main proofYann Herklotz2020-06-241-14/+29
|/ / / / / / /
* | | | | | | HTLgenproof passing.arrays-proofJames Pollard2020-06-242-50/+127
* | | | | | | Merge branch 'develop' into arrays-proofJames Pollard2020-06-242-9/+5
|\ \ \ \ \ \ \
generated by cgit (git 2.34.1) at 2024-07-08 22:46:00 +0000