aboutsummaryrefslogtreecommitdiffstats
path: root/src/hls/HTLgenproof.v
Commit message (Collapse)AuthorAgeFilesLines
* Get HTLgenproof to compile with RAM inferenceMichalis Pardalos2021-08-311-2/+9
|
* Merge branch 'oopsla21' into sharing-mergeMichalis Pardalos2021-08-261-18/+82
|\
| * Basically done with proofYann Herklotz2021-04-071-2/+2
| |
| * Add negative edge reasoning to HTLgenproofYann Herklotz2021-03-091-12/+76
| |
| * Add RAM semantics to HTL and fix proofYann Herklotz2021-03-031-6/+8
| |
| * Add implementationYann Herklotz2021-03-021-1/+1
| |
* | Use new HTLgenspec in proofMichalis Pardalos2021-08-221-3/+27
| |
* | More progress in Icall proofMichalis Pardalos2021-08-191-14/+16
| |
* | Find called module in Icall proofMichalis Pardalos2021-08-191-13/+33
| |
* | Get HTLgenproof passing with updated specMichalis Pardalos2021-08-061-3/+3
| |
* | Correct lookup for called funcs, simplify tr_moduleMichalis Pardalos2021-08-041-9/+8
| |
* | Remove all Admitted from top-level Compiler.vMichalis Pardalos2021-06-101-23/+199
| |
* | Add explanations for axiomsMichalis Pardalos2021-05-181-11/+13
| |
* | Add axiom that only the main contains storesMichalis Pardalos2021-05-181-4/+10
| | | | | | | | | | This is true due to the inlining pass. It should be checked in the translation and be added in the translation spec.
* | Qed on top-level correctness lemmaMichalis Pardalos2021-05-181-2/+2
| |
* | Update lemmata broken by changes to semanticsMichalis Pardalos2021-05-181-42/+35
| | | | | | | | | | | | * Removed calls to match_externctrl_tac. Carried forward without need for the tactic * Admitted match_frames goals. They should be easy enough to fix
* | Get Icall translation lemma *statement* passingMichalis Pardalos2021-05-181-15/+17
| |
* | Add "internal calls only" into translation specMichalis Pardalos2021-05-181-50/+64
| | | | | | | | | | | | | | Necessary, as external calls are present in RTL, but we should not translate them. This will need to be added as a check into the HTL translation. Admitted in HTLgenspec for now.
* | Get Ireturn proof to pass againMichalis Pardalos2021-05-181-11/+8
| |
* | Callstate proof with holes regarding stackMichalis Pardalos2021-05-181-129/+97
| |
* | Complete Returnstate proofsMichalis Pardalos2021-05-181-19/+3
| |
* | Complete Returnstate proofsMichalis Pardalos2021-05-171-78/+165
| |
* | Elaborate how stackframes match (match_frames)Michalis Pardalos2021-05-171-3/+29
| |
* | Add module idents to the semanticsMichalis Pardalos2021-05-171-21/+23
| | | | | | | | Necessary because they are used as pointers in externctrl
* | Most of Ireturn proofMichalis Pardalos2021-05-161-5/+54
| |
* | Update HTL proof for resource sharing (WIP)Michalis Pardalos2021-05-141-241/+304
| |
* | Get HTLgenproof passing again (with admits)Michalis Pardalos2021-05-131-230/+172
| |
* | Remove "active_call" from HTL semanticsMichalis Pardalos2021-05-131-16/+16
| | | | | | | | | | added previously to support the fork/wait/join HTL instructions which have since been removed
* | Tie all modules' clock to mainMichalis Pardalos2021-04-301-6/+7
| |
* | Get HTLgenproof to compileMichalis Pardalos2021-04-201-193/+193
| |
* | Fix up rest of HTLgenproofMichalis Pardalos2021-04-091-62/+46
| |
* | Get HTLgenproof to compileMichalis Pardalos2021-04-081-87/+89
| |
* | Make top-level theorems passYann Herklotz2021-02-161-5/+7
| |
* | Merge branch 'michalis' of https://github.com/mpardalos/vericert into ↵Yann Herklotz2021-02-161-22/+27
|/ | | | michalis-merge
* Add match_states for RTLPargen proofYann Herklotz2021-01-221-4/+18
|
* Add correct copyright notices in filesYann Herklotz2021-01-101-0/+1
|
* More fixes to the proofYann Herklotz2020-11-141-4/+5
|
* [Fix #9] Fix correctness proof for OshrximmYann Herklotz2020-11-141-4/+90
| | | | This removes all the admitted.
* Fix compilation issueYann Herklotz2020-11-101-5/+5
|
* Change and add back HTLgenYann Herklotz2020-11-091-1/+24
|
* Add RTLBlock intermediate languageYann Herklotz2020-08-301-0/+2683
generated by cgit (git 2.34.1) at 2024-07-15 19:51:07 +0000