Commit message (Collapse) | Author | Age | Files | Lines | |
---|---|---|---|---|---|
* | Clarify ireturn proof | Michalis Pardalos | 2021-09-30 | 1 | -5/+5 |
| | |||||
* | Prove match_arrs_empty | Michalis Pardalos | 2021-09-30 | 1 | -1/+19 |
| | |||||
* | Complete alloc/free zero proofs | Michalis Pardalos | 2021-09-30 | 1 | -8/+15 |
| | |||||
* | Complete call/return proofs | Michalis Pardalos | 2021-09-30 | 1 | -68/+122 |
| | |||||
* | [WIP] Updating proof for new state matching | Michalis Pardalos | 2021-09-29 | 1 | -39/+69 |
| | |||||
* | Update match_states. Pointers based on main's sp | Michalis Pardalos | 2021-09-29 | 1 | -21/+27 |
| | |||||
* | Add assumptions about externctrl finish registers | Michalis Pardalos | 2021-09-21 | 1 | -21/+131 |
| | |||||
* | [WIP] Reset finish register after returning | Michalis Pardalos | 2021-09-20 | 1 | -8/+56 |
| | |||||
* | Merge remote-tracking branch 'upstream/dev-michalis' into dev-michalis | Michalis Pardalos | 2021-09-19 | 1 | -3/+3 |
|\ | |||||
| * | Fix infinite loop in proofdev-michalis | Yann Herklotz | 2021-09-19 | 1 | -3/+3 |
| | | |||||
* | | [WIP] Fix usage of externctrl property in proof | Michalis Pardalos | 2021-09-19 | 1 | -6/+6 |
| | | |||||
* | | Address admits relating to externctrl params | Michalis Pardalos | 2021-09-16 | 1 | -8/+35 |
|/ | |||||
* | Complete callstate proof | Michalis Pardalos | 2021-09-16 | 1 | -6/+43 |
| | |||||
* | Progress with callstate proof | Michalis Pardalos | 2021-09-15 | 1 | -8/+11 |
| | |||||
* | Progress with icall proof | Michalis Pardalos | 2021-09-15 | 1 | -16/+106 |
| | |||||
* | Progress with mem_alloc_zero | Michalis Pardalos | 2021-09-15 | 1 | -3/+85 |
| | |||||
* | Prove mem_free_stack_match | Michalis Pardalos | 2021-09-14 | 1 | -6/+86 |
| | |||||
* | Add hammer tactics | Michalis Pardalos | 2021-09-13 | 1 | -0/+3 |
| | |||||
* | 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 |