Commit message (Collapse) | Author | Age | Files | Lines | |
---|---|---|---|---|---|
* | 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 |
| | |||||
* | backward decomposition of the proof | Sylvain Boulmé | 2020-07-22 | 1 | -20/+165 |
| | |||||
* | suggestion of simpler name | Sylvain Boulmé | 2020-07-17 | 1 | -1/+1 |
| | |||||
* | suggestion of translation from find_bblock to find_instr | Sylvain Boulmé | 2020-07-17 | 1 | -0/+22 |
| | |||||
* | Less auto-generated names | Justus Fasse | 2020-07-15 | 1 | -36/+36 |
| | |||||
* | First go at showing that translated cfi behave the same | Justus Fasse | 2020-07-15 | 1 | -0/+191 |
| | | | | Import Axioms in order to use functional extensionality | ||||
* | Add lemma showing 1 <= Ptrofs.max_unsigned | Justus Fasse | 2020-07-15 | 1 | -2/+8 |
| | |||||
* | Miscellaneous lemmas that I used at some point while experimenting | Justus Fasse | 2020-07-15 | 1 | -0/+84 |
| | |||||
* | Add definition of match_internal | Justus Fasse | 2020-07-15 | 1 | -0/+18 |
| | | | | | This relation will hold between Asmblock and Asm states while inside an Asmblock block. | ||||
* | Revert back to original definition of match_states | Justus Fasse | 2020-07-12 | 1 | -172/+8 |
| | | | | (The simulation relation between aarch64's Asmblock and Asm as equality) | ||||
* | Change definition of match_states | Justus Fasse | 2020-07-10 | 1 | -8/+172 |
| | | | | | | | | | | | | | | Introduce agree which says that all registers *except* the PC return the same values. The idea behind this change is that agree can be preserved across e.g. an Asmblock basic step, which does not update the PC. In addition to agree, the simualation relation requires the PC to agree. Right now the memory needs to be exactly the same which could be a problem. Since Asmblock's and Asm's set_pair is defined with preg it is more difficult to show that set_pair preserves the agree relation since SP is a preg and must not be Vundef. This commit does not solve the problem. | ||||
* | Start Asmgenproof | Justus Fasse | 2020-07-09 | 1 | -3/+69 |
| | | | | | | - Define simulation relation as equality. - Prove the easy cases, transf_initial_states, transf_final_states, and begin with the proof for the step simulation (external calls) | ||||
* | Finish proof of Lemma symbol_high_low | Justus Fasse | 2020-07-09 | 1 | -3/+8 |
| | |||||
* | fix linker model in Asmblock | Sylvain Boulmé | 2020-06-22 | 1 | -2/+13 |
| | |||||
* | restauring Coq compilation with STUBS | Sylvain Boulmé | 2020-06-22 | 1 | -0/+127 |
| | |||||
* | [WIP: Coq compilation broken] Stub for Asmgen | Sylvain Boulmé | 2020-06-21 | 1 | -1101/+0 |
| | |||||
* | disable leaf function removal of return address restoration due to memcpy ↵ | David Monniaux | 2020-03-27 | 1 | -2/+2 |
| | | | | overwriting the return address register | ||||
* | Merge branch 'dm-leaf' of https://github.com/monniaux/CompCert into mppa-work | David Monniaux | 2020-03-27 | 1 | -1/+6 |
|\ |