aboutsummaryrefslogtreecommitdiffstats
path: root/src
Commit message (Collapse)AuthorAgeFilesLines
* Merge remote-tracking branch 'upstream/develop' into dev-nadeshJames Pollard2020-07-073-13/+57
|\
| * Only translate_cond leftYann Herklotz2020-07-074-17/+252
| |
* | Get Coqup compiling again on dev-nadesh.James Pollard2020-07-073-1937/+1938
| |
* | Merge branch 'byte-addressing' into dev-nadeshJames Pollard2020-07-0722-2202/+3420
|\ \
| * | Merge branch 'develop' of github.com:ymherklotz/coqup into byte-addressingJames Pollard2020-07-075-124/+293
| |\|
| | * 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
| | |
| * | Concatenation style loads.James Pollard2020-07-063-49/+54
| | |
| * | Reduce number of array addressing modes.James Pollard2020-07-062-6/+27
| | |
| * | Check chunk size during translation.James Pollard2020-07-062-19/+33
| | |
| * | Remove alignment requirement for lessdef.James Pollard2020-07-061-9/+3
| | |
| * | Merge branch 'develop' of github.com:ymherklotz/coqup into byte-addressingJames Pollard2020-07-067-2201/+2238
| |\|
| | * HTLgenproof compiles againYann Herklotz2020-07-064-22/+47
| | | | | | | | | | | | - Commented out Iload, Istore proofs for now
| | * Fix InopYann Herklotz2020-07-054-47/+58
| | |
| * | Fix HTLgenspec.James Pollard2020-07-062-476/+467
| | |
| * | Implemented algorithm for new byte-addressed stack.James Pollard2020-07-0611-2682/+2730
| |/
| * Fix HTLgenspecYann Herklotz2020-07-051-3/+4
| |
| * No addmitted in VeriloggenproofYann Herklotz2020-07-054-100/+245
| | | | | | | | However, there may have been breaking changes to HTLgenproof.
| * 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 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-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
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We never cons a stack frame since we don't support calls (aside from the initial call which doesn't push a stack frame); removing the cons constructor solves the issue regarding memory separation. This means we now _can't_ support calls even if we wanted to, but due to the way we implement memory, we would need quite a lot of extra work to support this.
| * | | Add HTL pretty printerYann Herklotz2020-06-301-0/+81
| | | |
| * | | Add htl pretty printingYann Herklotz2020-06-305-1/+7
| | |/ | |/|
* | | Merge branch 'develop' into dev-nadeshYann Herklotz2020-06-307-32/+332
|\| |
generated by cgit (git 2.34.1) at 2024-07-11 08:55:13 +0000