aboutsummaryrefslogtreecommitdiffstats
path: root/src/translation/HTLgenproof.v
Commit message (Expand)AuthorAgeFilesLines
* HTLgenproof compiles againYann Herklotz2020-07-061-14/+30
* Fix InopYann Herklotz2020-07-051-11/+14
* No addmitted in VeriloggenproofYann Herklotz2020-07-051-1/+0
* Make HTLgen compile againYann Herklotz2020-07-041-3/+11
* Fixing HTLgenproofYann Herklotz2020-07-031-13/+32
* Updates to Iop proofYann Herklotz2020-07-031-89/+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-021-14/+1
* Tidy up (?) automation slightly...James Pollard2020-07-011-20/+17
* Improve (?) automation.James Pollard2020-07-011-407/+301
* 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
* Eliminate memory bounds assumption!James Pollard2020-06-291-35/+209
* Fix proof again with Verilog semantics changesYann Herklotz2020-06-281-1/+11
* Merge remote-tracking branch 'james/arrays-proof' into developYann Herklotz2020-06-281-68/+809
|\
| * 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-281-57/+293
| * Fix unsigned/signed issues.James Pollard2020-06-281-64/+46
| * Work on proof.James Pollard2020-06-281-2/+299
* | Work on Veriloggen proofYann Herklotz2020-06-251-1/+1
* | Finish Internal main proofYann Herklotz2020-06-241-14/+29
|/
* HTLgenproof passing.arrays-proofJames Pollard2020-06-241-46/+127
* Merge branch 'develop' of github.com:ymherklotz/coqup into arrays-proofJames Pollard2020-06-241-15/+54
|\
| * Merge branch 'master' into developYann Herklotz2020-06-241-19/+58
| |\
| | * Fix assumption of mainYann Herklotz2020-06-241-19/+58
| * | Merge branch 'master' into developYann Herklotz2020-06-221-5/+5
| |\|
| | * Admit everything temporarilyYann Herklotz2020-06-221-5/+5
* | | Finish ILoad proof with some assumptions:James Pollard2020-06-241-7/+29
* | | Normalise entire expression to avoid overflow issues.James Pollard2020-06-231-264/+268
* | | Finish off Load proof sketches.James Pollard2020-06-221-35/+17
* | | Start Aindexed proof.James Pollard2020-06-221-17/+219
* | | Tidy up proof for Aindexed2scaled.James Pollard2020-06-221-86/+166
|/ /
* | Finish structure of Aindexed2scaled ILoad proof.James Pollard2020-06-201-14/+172
* | Working on proof.James Pollard2020-06-191-10/+86
* | Enforce stack size alignment to fix proof.James Pollard2020-06-181-8/+17
* | Tidy up proof.James Pollard2020-06-181-12/+15
* | Finish AInStack proof with minor assertions.James Pollard2020-06-181-32/+21
* | Fix up ILoad proof.James Pollard2020-06-181-95/+58
* | Fix Inop proof to work with new array semantics.James Pollard2020-06-171-7/+36
* | Some (very) useful lemmas about arrays.James Pollard2020-06-171-4/+32
* | Merge branch 'master' into arrays-proofJames Pollard2020-06-121-2/+4
|\|
| * Declare all registers properly in HTLYann Herklotz2020-06-121-2/+4
generated by cgit (git 2.34.1) at 2024-07-05 21:12:14 +0000