| Commit message (Collapse) | Author | Age | Files | Lines | |
|---|---|---|---|---|---|
| * | Icall proof progress | Michalis Pardalos | 2021-09-13 | 1 | -35/+85 |
| | | |||||
| * | Guard join state with called module finish | Michalis Pardalos | 2021-09-11 | 1 | -2/+8 |
| | | | | | | | Needed to match RTL semantics, since the join state executes once before the call is initiated, and we need the destination register to not be affected until after the call has returned. | ||||
| * | Progress with stackframe matching for Icall | Michalis Pardalos | 2021-09-10 | 1 | -1/+8 |
| | | |||||
| * | Prove that called module exists for Icall | Michalis Pardalos | 2021-09-10 | 1 | -2/+26 |
| | | |||||
| * | Get HTLgenproof to compile with RAM inference | Michalis Pardalos | 2021-08-31 | 1 | -2/+9 |
| | | |||||
| * | Merge branch 'oopsla21' into sharing-merge | Michalis Pardalos | 2021-08-26 | 1 | -18/+82 |
| |\ | |||||
| | * | Basically done with proof | Yann Herklotz | 2021-04-07 | 1 | -2/+2 |
| | | | |||||
| | * | Add negative edge reasoning to HTLgenproof | Yann Herklotz | 2021-03-09 | 1 | -12/+76 |
| | | | |||||
| | * | Add RAM semantics to HTL and fix proof | Yann Herklotz | 2021-03-03 | 1 | -6/+8 |
| | | | |||||
| | * | Add implementation | Yann Herklotz | 2021-03-02 | 1 | -1/+1 |
| | | | |||||
| * | | Use new HTLgenspec in proof | Michalis Pardalos | 2021-08-22 | 1 | -3/+27 |
| | | | |||||
| * | | More progress in Icall proof | Michalis Pardalos | 2021-08-19 | 1 | -14/+16 |
| | | | |||||
| * | | Find called module in Icall proof | Michalis Pardalos | 2021-08-19 | 1 | -13/+33 |
| | | | |||||
| * | | Get HTLgenproof passing with updated spec | Michalis Pardalos | 2021-08-06 | 1 | -3/+3 |
| | | | |||||
| * | | Correct lookup for called funcs, simplify tr_module | Michalis Pardalos | 2021-08-04 | 1 | -9/+8 |
| | | | |||||
| * | | Remove all Admitted from top-level Compiler.v | Michalis Pardalos | 2021-06-10 | 1 | -23/+199 |
| | | | |||||
| * | | Add explanations for axioms | Michalis Pardalos | 2021-05-18 | 1 | -11/+13 |
| | | | |||||
| * | | Add axiom that only the main contains stores | Michalis Pardalos | 2021-05-18 | 1 | -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 lemma | Michalis Pardalos | 2021-05-18 | 1 | -2/+2 |
| | | | |||||
| * | | Update lemmata broken by changes to semantics | Michalis Pardalos | 2021-05-18 | 1 | -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* passing | Michalis Pardalos | 2021-05-18 | 1 | -15/+17 |
| | | | |||||
| * | | Add "internal calls only" into translation spec | Michalis Pardalos | 2021-05-18 | 1 | -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 again | Michalis Pardalos | 2021-05-18 | 1 | -11/+8 |
| | | | |||||
| * | | Callstate proof with holes regarding stack | Michalis Pardalos | 2021-05-18 | 1 | -129/+97 |
| | | | |||||
| * | | Complete Returnstate proofs | Michalis Pardalos | 2021-05-18 | 1 | -19/+3 |
| | | | |||||
| * | | Complete Returnstate proofs | Michalis Pardalos | 2021-05-17 | 1 | -78/+165 |
| | | | |||||
| * | | Elaborate how stackframes match (match_frames) | Michalis Pardalos | 2021-05-17 | 1 | -3/+29 |
| | | | |||||
| * | | Add module idents to the semantics | Michalis Pardalos | 2021-05-17 | 1 | -21/+23 |
| | | | | | | | | | Necessary because they are used as pointers in externctrl | ||||
| * | | Most of Ireturn proof | Michalis Pardalos | 2021-05-16 | 1 | -5/+54 |
| | | | |||||
| * | | Update HTL proof for resource sharing (WIP) | Michalis Pardalos | 2021-05-14 | 1 | -241/+304 |
| | | | |||||
| * | | Get HTLgenproof passing again (with admits) | Michalis Pardalos | 2021-05-13 | 1 | -230/+172 |
| | | | |||||
| * | | Remove "active_call" from HTL semantics | Michalis Pardalos | 2021-05-13 | 1 | -16/+16 |
| | | | | | | | | | | | added previously to support the fork/wait/join HTL instructions which have since been removed | ||||
| * | | Tie all modules' clock to main | Michalis Pardalos | 2021-04-30 | 1 | -6/+7 |
| | | | |||||
| * | | Get HTLgenproof to compile | Michalis Pardalos | 2021-04-20 | 1 | -193/+193 |
| | | | |||||
| * | | Fix up rest of HTLgenproof | Michalis Pardalos | 2021-04-09 | 1 | -62/+46 |
| | | | |||||
| * | | Get HTLgenproof to compile | Michalis Pardalos | 2021-04-08 | 1 | -87/+89 |
| | | | |||||
| * | | Make top-level theorems pass | Yann Herklotz | 2021-02-16 | 1 | -5/+7 |
| | | | |||||
| * | | Merge branch 'michalis' of https://github.com/mpardalos/vericert into ↵ | Yann Herklotz | 2021-02-16 | 1 | -22/+27 |
| |/ | | | | michalis-merge | ||||
| * | Add match_states for RTLPargen proof | Yann Herklotz | 2021-01-22 | 1 | -4/+18 |
| | | |||||
| * | Add correct copyright notices in files | Yann Herklotz | 2021-01-10 | 1 | -0/+1 |
| | | |||||
| * | More fixes to the proof | Yann Herklotz | 2020-11-14 | 1 | -4/+5 |
| | | |||||
| * | [Fix #9] Fix correctness proof for Oshrximm | Yann Herklotz | 2020-11-14 | 1 | -4/+90 |
| | | | | | This removes all the admitted. | ||||
| * | Fix compilation issue | Yann Herklotz | 2020-11-10 | 1 | -5/+5 |
| | | |||||
| * | Change and add back HTLgen | Yann Herklotz | 2020-11-09 | 1 | -1/+24 |
| | | |||||
| * | Add RTLBlock intermediate language | Yann Herklotz | 2020-08-30 | 1 | -0/+2683 |
 |
index : vericert | |
| Vericert is a formally verified high-level synthesis tool. |
| aboutsummaryrefslogtreecommitdiffstats |