aboutsummaryrefslogtreecommitdiffstats
Commit message (Expand)AuthorAgeFilesLines
* HTLgenproof passing.arrays-proofJames Pollard2020-06-242-50/+127
* Merge branch 'develop' into arrays-proofJames Pollard2020-06-242-9/+5
|\
| * Fixes to make develop compileYann Herklotz2020-06-244-8/+6
* | Merge branch 'develop' of github.com:ymherklotz/coqup into arrays-proofJames Pollard2020-06-2480-115/+15708
|\|
| * Merge branch 'master' into developYann Herklotz2020-06-243-81/+96
| |\
| | * Fix assumption of mainYann Herklotz2020-06-243-83/+97
| * | More to proofYann Herklotz2020-06-231-7/+9
| * | Merge branch 'master' into developYann Herklotz2020-06-223-9/+58
| |\|
| | * Admit everything temporarilyYann Herklotz2020-06-223-9/+58
| * | Admit the value proofYann Herklotz2020-06-221-3/+5
| * | Merge branch 'arrays-proof' into developYann Herklotz2020-06-223-31/+204
| |\ \
| * \ \ Merge branch 'master' into developYann Herklotz2020-06-2276-20/+15522
| |\ \ \ | | | |/ | | |/|
| | * | Only print out main as everything is inlinedYann Herklotz2020-06-221-8/+10
| | * | Add print for debug always block in moduleYann Herklotz2020-06-223-7/+23
| | * | Some fixes, but still buggy probablyYann Herklotz2020-06-201-2/+2
| | * | Add bugs to support more operationsYann Herklotz2020-06-201-4/+4
| | * | Add CHstoneYann Herklotz2020-06-1972-1/+15485
| | * | Merge branch 'develop'Yann Herklotz2020-06-145-24/+32
| | |\ \
| * | | | Add proof of nat equivYann Herklotz2020-06-201-2/+15
| * | | | Merge remote-tracking branch 'james/arrays-proof' into developYann Herklotz2020-06-209-111/+725
| |\ \ \ \ | | |_|/ / | |/| | |
| * | | | Fix coqprojectYann Herklotz2020-06-141-1/+1
| * | | | Add more unproven instructions, Admitted equiv to specYann Herklotz2020-06-144-23/+31
| | |/ / | |/| |
* | | | Finish ILoad proof with some assumptions:James Pollard2020-06-243-192/+197
* | | | Normalise entire expression to avoid overflow issues.James Pollard2020-06-235-272/+523
* | | | Finish off Load proof sketches.James Pollard2020-06-221-35/+17
* | | | Start Aindexed proof.James Pollard2020-06-222-19/+226
* | | | Tidy up proof for Aindexed2scaled.James Pollard2020-06-224-90/+231
| |_|/ |/| |
* | | Factor out addressing checks, check signed range.James Pollard2020-06-211-10/+17
* | | Lea op now checks alignment.James Pollard2020-06-211-12/+15
* | | Finish structure of Aindexed2scaled ILoad proof.James Pollard2020-06-202-14/+177
| |/ |/|
* | Working on proof.James Pollard2020-06-191-10/+86
* | Enforce stack size alignment to fix proof.James Pollard2020-06-183-10/+22
* | Tidy up proof.James Pollard2020-06-182-13/+16
* | Finish AInStack proof with minor assertions.James Pollard2020-06-181-32/+21
* | Fix up ILoad proof.James Pollard2020-06-181-95/+58
* | Fix array semantics behaviour for undefined values.James Pollard2020-06-181-1/+1
* | Fix Inop proof to work with new array semantics.James Pollard2020-06-172-7/+44
* | Some (very) useful lemmas about arrays.James Pollard2020-06-173-7/+139
* | Use NBAs for loads and stores.James Pollard2020-06-172-4/+4
* | Fix array semantics merge granularity.James Pollard2020-06-174-30/+87
* | Array semantics now uses dependent Array type.James Pollard2020-06-145-49/+50
* | Move some standard tactics to Coquplib.James Pollard2020-06-141-0/+10
* | Add a basic length-indexed list type.James Pollard2020-06-131-0/+123
* | Merge branch 'develop' into arrays-proofJames Pollard2020-06-123-4/+27
|\|
| * Update matrix and use 32 bitYann Herklotz2020-06-123-12/+14
| * Add matrix testYann Herklotz2020-06-121-0/+21
* | Fix broken proof.James Pollard2020-06-121-4/+4
* | Merge branch 'master' into arrays-proofJames Pollard2020-06-121-4/+6
|\|
| * Merge pull request #7 from p0llard/hotfixYann Herklotz2020-06-121-4/+6
| |\
| | * Fix addressing bug.James Pollard2020-06-121-4/+6
| |/
generated by cgit (git 2.34.1) at 2024-05-21 21:12:49 +0000