Commit message (Collapse) | Author | Age | Files | Lines | |
---|---|---|---|---|---|
* | Progress in exec_basic_simu | Léo Gourdin | 2020-10-15 | 1 | -104/+148 |
| | | | | | | - New ltacs - simplifications - new subcases - two lemmas for nextinstr agree | ||||
* | Some subcases for exec_basic_simu | Léo Gourdin | 2020-10-14 | 1 | -86/+49 |
| | | | | | | | - Ploadsymbol - Pcvtsw2x - Pcvtuw2x - Pcvtx2w - First subcase for PArithCompPP | ||||
* | an idea to tackle PArithComparisonPP | Sylvain Boulmé | 2020-10-14 | 1 | -2/+43 |
| | |||||
* | draft commit for the Pallocframe proof subcase | Léo Gourdin | 2020-10-14 | 1 | -2/+15 |
| | |||||
* | Pstore preserved lemma | Léo Gourdin | 2020-10-14 | 1 | -3/+64 |
| | |||||
* | Other subcases for PArith are done. | Léo Gourdin | 2020-10-14 | 1 | -8/+29 |
| | |||||
* | Draft commit on the PArithComparisonPP Proof | Léo Gourdin | 2020-10-14 | 1 | -14/+72 |
| | | | in exec_basic_simulation | ||||
* | Simplifying Ltac and fixing a bug in AsmBlock semantics | Léo Gourdin | 2020-10-13 | 2 | -11/+31 |
| | | | The bug was a typo on the PArithPPP subl inst | ||||
* | Fixing the propagation of the new BOUNDED hyp | Léo Gourdin | 2020-10-13 | 1 | -8/+20 |
| | |||||
* | Proof for Pmovz | Léo Gourdin | 2020-10-13 | 1 | -7/+29 |
| | | | Adding Ltac to simplify code and improve readability | ||||
* | Adding a lemma next_instr_preserved | Léo Gourdin | 2020-10-12 | 1 | -7/+56 |
| | | | this is useful in the exec_basic_simu proof | ||||
* | Continue the proof of exec_basic_simulation | Léo Gourdin | 2020-10-11 | 1 | -18/+12 |
| | |||||
* | Adding a lemma for exec load propagation. | Léo Gourdin | 2020-10-11 | 1 | -25/+27 |
| | | | | The commit also contains an incomplete proof for assert (BDYLENPOS: ((length li) < length (body bb))%nat). | ||||
* | Merge branch 'aarch64_block_bodystar' of ↵ | Léo Gourdin | 2020-10-10 | 1 | -10/+14 |
|\ | | | | | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into aarch64_block_bodystar | ||||
| * | Merge branch 'aarch64_block_bodystar' of ↵ | Sylvain Boulmé | 2020-10-10 | 1 | -0/+14 |
| |\ | | | | | | | | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into aarch64_block_bodystar | ||||
| * | | Still generalizing exec_body_simulation_plus for an inductive proof | Sylvain Boulmé | 2020-10-09 | 1 | -10/+14 |
| | | | | | | | | | | | | This will require some lemma about is_tail... | ||||
* | | | More general version of load preservation lemma. | Léo Gourdin | 2020-10-10 | 1 | -7/+25 |
| |/ |/| | | | | | Problem with the ptr bounds. | ||||
* | | Adding a lemma for load preservation | Léo Gourdin | 2020-10-10 | 1 | -0/+14 |
|/ | | | | This is a test lemma, I may remove the exists predicate later. | ||||
* | slight refactoring, in order to avoid a duplication of the proof. | Sylvain Boulmé | 2020-10-09 | 1 | -40/+36 |
| | |||||
* | exec_body_simulation without star' | Léo Gourdin | 2020-10-09 | 1 | -0/+101 |
| | |||||
* | Replace common pattern with simpler lemma. | Justus Fasse | 2020-09-21 | 1 | -29/+16 |
| | | | | | Turns two rewrites and a simplification into a single rewrite via list_length_z_cons. | ||||
* | Proof of exec_body_simulation_plus | Justus Fasse | 2020-09-21 | 1 | -1/+238 |
| | | | | | | | | | | | Added exec_body_simulation_star' in order to prove it. exec_body_simulation_star' could also be used to prove exec_body_simulation_star directly (without using exec_body_simulation_plus). However, at least the way I did it the proof turns out to be longer. eexec_body_simulation_plus is still required/useful for exec_bblock_simulation. | ||||
* | Move a couple of lemmas up in the file | Justus Fasse | 2020-09-21 | 1 | -68/+68 |
| | |||||
* | Admitted lemma for exec_basic_simulation. | Justus Fasse | 2020-09-21 | 1 | -0/+9 |
| | | | | Probably still missing a couple of assumptions. | ||||
* | Prove exec_body_dont_move_PC | Justus Fasse | 2020-08-18 | 4 | -42/+112 |
| | | | | | | Modify Asmblock.preg to combine iregsp and freg into dreg (dreg might be a misnomer since not all iregs are data regs) TODO: Adjust names of PArithP, PArithPP and the like | ||||
* | Proof for size_of_blocks_max_pos | Justus Fasse | 2020-08-05 | 1 | -18/+50 |
| | |||||
* | Minor cleanup of find_instr_bblock | Justus Fasse | 2020-07-30 | 1 | -11/+10 |
| | | | | | | | | - Remove one auto-generated name - Move assertion on n's size up - Clear unnecessary hypothesis (iirc generalize worked better than exploit here) - Rewrite progress of Asm.find_instr only in the case that needs it | ||||
* | Complete proof of find_instr_bblock | Justus Fasse | 2020-07-30 | 1 | -3/+30 |
| | | | | Cleanup is still TODO | ||||
* | Absurd case in find_instr_bblock | Justus Fasse | 2020-07-30 | 1 | -1/+107 |
| | | | | | n points to neither label nor basic instruction but there is also no final exit instruction | ||||
* | Prove find_instr_bblock_tail | Justus Fasse | 2020-07-30 | 1 | -2/+89 |
| | |||||
* | Simplify unfold_bblock and complete unfold_body's case in find_instr_bblock | Justus Fasse | 2020-07-29 | 2 | -12/+76 |
| | | | | | | | The previous version of unfold_bblock was copied from kvx/Asm.v. kvx's version is slightly different in that for the (here removed) special case it does not put a semicolon to separate bundles. Since aarch64 does not have kvx's bundles the two versions should be equivalent. | ||||
* | Find label in base case of find_instr_bblock | Justus Fasse | 2020-07-28 | 1 | -2/+18 |
| | |||||
* | Messy progress on builtin-case of exec_exit_simulation_plus | Justus Fasse | 2020-07-28 | 1 | -10/+25 |
| | |||||
* | Messy progress on exec_exit_simulation_plus | Justus Fasse | 2020-07-28 | 1 | -3/+27 |
| | | | | | Proves exec_exit_simulation_plus for cf_instruction (as opposed to builtins) | ||||
* | Rename/repurpose cf_instruction_simulated for exec_cfi_simulation | Justus Fasse | 2020-07-28 | 1 | -179/+150 |
| | | | | | exec_cfi_simulation's rephrasing is inspired by the needs of exec_exit_simulation_plus. | ||||
* | Begin proof of exec_exit_simulation_plus | Justus Fasse | 2020-07-27 | 1 | -0/+42 |
| | | | | Mostly proving the absurd cases following inversion of is_nth_inst | ||||
* | Playing around with find_instr_bblock's base case | Justus Fasse | 2020-07-27 | 1 | -7/+25 |
| | |||||
* | Replace some auto-generated names | Justus Fasse | 2020-07-27 | 1 | -3/+3 |
| | |||||
* | Move position of n in formulation of find_instr_bblock | Justus Fasse | 2020-07-27 | 1 | -4/+4 |
| | | | | | | This way exec_header_simulation does not break (without any changes). Depending on the base case of find_instr_bblock this may need to change again. | ||||
* | Idea for find_instr_bblock's recursive case | Justus Fasse | 2020-07-27 | 1 | -7/+35 |
| | |||||
* | Factorize common proof-pattern as lemmas | Justus Fasse | 2020-07-27 | 1 | -8/+30 |
| | | | | | unfolding a non-empty list of basic blocks will unfold the head (unfold_bblock) and then recur on the tail. | ||||
* | Simplify premises | Justus Fasse | 2020-07-24 | 1 | -12/+9 |
| | |||||
* | Remove unnecessary premise | Justus Fasse | 2020-07-24 | 1 | -4/+3 |
| | |||||
* | Remove trailing whitespace | Justus Fasse | 2020-07-24 | 1 | -4/+4 |
| | |||||
* | Complete size_header | Justus Fasse | 2020-07-24 | 1 | -1/+66 |
| | |||||
* | Complete bblock_size_aux | Justus Fasse | 2020-07-24 | 1 | -1/+24 |
| | |||||
* | Complete bblock_size_aux_pos | Justus Fasse | 2020-07-24 | 1 | -1/+6 |
| | | | | Steal use of list_length_z_aux_increase from exec_header_simulation. | ||||
* | proof of exec_header_simulation | Sylvain Boulmé | 2020-07-23 | 1 | -10/+91 |
| | |||||
* | Complete bblock_non_empty | Justus Fasse | 2020-07-23 | 1 | -1/+10 |
| | |||||
* | Remove trailing whitespace | Justus Fasse | 2020-07-22 | 1 | -6/+6 |
| |