aboutsummaryrefslogtreecommitdiffstats
Commit message (Collapse)AuthorAgeFilesLines
...
* | | Get top-level proof passingMichalis Pardalos2021-09-011-12/+14
| | |
* | | Get HTLgenproof to compile with RAM inferenceMichalis Pardalos2021-08-311-2/+9
| | |
* | | Get Memorygen to compile againMichalis Pardalos2021-08-311-475/+484
| | |
* | | Get HTLgenspec compiling with RAM inferenceMichalis Pardalos2021-08-311-2/+2
| | |
* | | Get HTLgen compiling with RAM inferenceMichalis Pardalos2021-08-311-9/+9
| | |
* | | Get Renaming compiling with RAM inferenceMichalis Pardalos2021-08-313-24/+37
| | |
* | | Get ApplyExternctrl compiling with RAM inferenceMichalis Pardalos2021-08-311-8/+16
| | |
* | | WIPMichalis Pardalos2021-08-306-140/+160
| | |
* | | Merge branch 'oopsla21' into sharing-mergeMichalis Pardalos2021-08-2691-1720/+8072
|\| |
| * | Use main instead of top for synthesising Vericert designsYann Herklotz2021-07-241-1/+1
| | |
| * | Update instructions and fix testv1.2.1Yann Herklotz2021-07-124-6/+5
| | |
| * | Remove comments in docker fileYann Herklotz2021-07-121-3/+3
| | |
| * | Update the artifact descriptionYann Herklotz2021-07-127-4/+204
| | |
| * | Remove more OCaml files to compile successfully without admits.Yann Herklotz2021-07-115-1085/+0
| | |
| * | Remove unnecessary files and proofsYann Herklotz2021-07-117-16/+19
| | |
| * | Update the run-legup.sh fileYann Herklotz2021-07-111-0/+4
| | |
| * | Add legup scriptYann Herklotz2021-07-114-4/+74
| | |
| * | Fix the small test bench for VericertYann Herklotz2021-07-117-137/+67
| | |
| * | Fix some more of the benchmarksYann Herklotz2021-07-118-49/+35
| | |
| * | Add divider benchmarksYann Herklotz2021-07-1144-0/+3581
| | |
| * | Fix makefiles and add a parent makefileYann Herklotz2021-07-104-3/+18
| | |
| * | Fix Makefiles slightlyYann Herklotz2021-07-108-7/+12
| | |
| * | Add more documentation and clean up benchmarksYann Herklotz2021-07-1012-158/+139
| | |
| * | Add docker file and some commentsYann Herklotz2021-07-092-0/+6
| |/
| * Clean up Memorygen fileYann Herklotz2021-04-071-219/+1
| |
| * Remove Admitted in the highest of top-levelsv1.2.0Yann Herklotz2021-04-071-5/+10
| |
| * No admitted theorems in Memorygen proof (~‾▿‾)~Yann Herklotz2021-04-071-76/+99
| |
| * Basically done with proofYann Herklotz2021-04-076-18/+62
| |
| * Let everything compile againYann Herklotz2021-04-061-7/+18
| |
| * Finish load and store proof, but broke top-levelYann Herklotz2021-04-067-289/+317
| |
| * Finish Veriloggenproof completelyYann Herklotz2021-04-044-57/+339
| |
| * Prove all admit in load but oneYann Herklotz2021-04-041-162/+183
| |
| * Finish most of load proofYann Herklotz2021-04-041-21/+167
| |
| * Finish store proof without admitYann Herklotz2021-04-042-189/+533
| |
| * Add logo to readmeYann Herklotz2021-04-021-6/+3
| |
| * Fix initialisation moreYann Herklotz2021-04-011-7/+7
| |
| * Add 0 initialisationYann Herklotz2021-04-011-1/+1
| |
| * Add declarationsYann Herklotz2021-04-011-6/+7
| |
| * Add new enable interfaceYann Herklotz2021-04-014-53/+66
| |
| * Add memory disableYann Herklotz2021-03-314-163/+306
| |
| * Temporary doneYann Herklotz2021-03-301-48/+247
| |
| * Add more checks to the implementationYann Herklotz2021-03-291-27/+82
| |
| * Update declared sizeYann Herklotz2021-03-281-1/+1
| |
| * Finish main match proof in storeYann Herklotz2021-03-281-50/+555
| |
| * Add proofs of size preservation of statements and ramYann Herklotz2021-03-251-47/+92
| |
| * Work more on size-preserving lemmasYann Herklotz2021-03-251-104/+129
| |
| * Add forall_ram proofYann Herklotz2021-03-251-6/+40
| |
| * Prove lt property for statementsYann Herklotz2021-03-251-4/+67
| |
| * Add many more array theoremsYann Herklotz2021-03-241-4/+100
| |
| * Completed match_arrs_gss proofYann Herklotz2021-03-231-21/+100
| |
generated by cgit (git 2.34.1) at 2024-07-04 20:49:18 +0000