| Commit message (Collapse) | Author | Age | Files | Lines | ||
|---|---|---|---|---|---|---|
| ... | ||||||
| * | | | 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 | 1 | -10/+30 | |
| | | | | | | | | | | 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 | 1 | -1/+64 | |
| | | | | | | | | | | | | | | | | | | | 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 | 1 | -3/+74 | |
| | | | | | | | | | | | | | | | | | | | | | | 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 | |
| | | | | ||||||
| * | | | Complete proof of exec_exit_simulation_star | Justus Fasse | 2020-07-22 | 1 | -2/+10 | |
| | | | | ||||||
 |
index : compcert-kvx | |
| Unnamed repository; edit this file 'description' to name the repository. |
| aboutsummaryrefslogtreecommitdiffstats |