Commit message (Expand) | Author | Age | Files | Lines | ||
---|---|---|---|---|---|---|
... | ||||||
| * | | Minimise the proof a bit | Yann Herklotz | 2021-05-16 | 1 | -18/+12 | |
| * | | Finish up step_cf_instr_correct again | Yann Herklotz | 2021-05-16 | 2 | -19/+43 | |
| * | | Fix the top-level proofs with new state_match | Yann Herklotz | 2021-05-15 | 2 | -27/+164 | |
| * | | Finish abstract interpretation | Yann Herklotz | 2021-05-12 | 1 | -75/+199 | |
| * | | Fix admitted in first proof of sem. preservation | Yann Herklotz | 2021-05-10 | 1 | -19/+68 | |
| * | | Finish correctness of semantics wrt. RTBlock | Yann Herklotz | 2021-05-06 | 1 | -84/+327 | |
| * | | Add admitted proof of translations in RTLPargen | Yann Herklotz | 2021-05-03 | 1 | -27/+177 | |
* | | | Check: only main uses ainstack, no calls to main | Michalis Pardalos | 2021-10-17 | 1 | -20/+66 | |
* | | | Check that only main has a stacksize | Michalis Pardalos | 2021-10-11 | 2 | -12/+47 | |
* | | | Get all call and return proofs passing again | Michalis Pardalos | 2021-10-08 | 1 | -4/+25 | |
* | | | Maintain that initial call does not have arguments | Michalis Pardalos | 2021-10-07 | 1 | -0/+1 | |
* | | | [WIP] Handle empty stack case for empty stack case | Michalis Pardalos | 2021-10-07 | 1 | -39/+65 | |
* | | | 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 | 2 | -9/+66 | |
* | | | Merge remote-tracking branch 'upstream/dev-michalis' into dev-michalis | Michalis Pardalos | 2021-09-19 | 5 | -15/+57 | |
|\ \ \ | ||||||
| * | | | Fix infinite loop in proofdev-michalis | Yann Herklotz | 2021-09-19 | 1 | -3/+3 | |
| * | | | Add xomega tactic into Vericertlib | Yann Herklotz | 2021-09-17 | 1 | -0/+2 | |
| * | | | Merge remote-tracking branch 'upstream/master' into dev-michalis | Yann Herklotz | 2021-09-17 | 3 | -12/+52 | |
| |\ \ \ | | | |/ | | |/| | ||||||
| | * | | Merge remote-tracking branch 'origin/master' | Yann Herklotz | 2021-09-17 | 1 | -0/+19 | |
| | |\ \ | ||||||
| | | * | | Move license to the SoftwarePipelining directory | Yann Herklotz | 2021-09-15 | 1 | -0/+19 | |
| | * | | | Fix compilation with new CompCert version | Yann Herklotz | 2021-09-17 | 1 | -8/+8 | |
| | |/ / | ||||||
| | * | | Fix proofs for SAT | Yann Herklotz | 2021-08-12 | 1 | -6/+27 | |
| | * | | Fix pretty printing issue in Verilog | Yann Herklotz | 2021-08-12 | 1 | -1/+1 | |
* | | | | [WIP] Fix usage of externctrl property in proof | Michalis Pardalos | 2021-09-19 | 1 | -6/+6 | |
* | | | | Add new externctrl_params_mapped to HTLspec | Michalis Pardalos | 2021-09-19 | 1 | -36/+53 | |
* | | | | [WIP] Progress on Icall proof | Michalis Pardalos | 2021-09-19 | 2 | -13/+94 | |
* | | | | 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 | |
* | | | Name the externctrl correctness clauses | Michalis Pardalos | 2021-09-12 | 1 | -11/+18 | |
* | | | Guard join state with called module finish | Michalis Pardalos | 2021-09-11 | 3 | -6/+14 | |
* | | | 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 | |
* | | | Fix duplicated verilog module instantiations | Michalis Pardalos | 2021-09-08 | 1 | -75/+92 | |
* | | | Print declarations in HTL output | Michalis Pardalos | 2021-09-08 | 2 | -0/+18 | |
* | | | Fix renamer skipping ram_mem | Michalis Pardalos | 2021-09-03 | 1 | -1/+2 | |
* | | | Print control registers in HTL output | Michalis Pardalos | 2021-09-03 | 1 | -0/+13 | |
* | | | Print RAM in HTL output | Michalis Pardalos | 2021-09-03 | 1 | -0/+17 | |
* | | | Fix error in map_externctrl | Michalis Pardalos | 2021-09-03 | 1 | -1/+1 |