aboutsummaryrefslogtreecommitdiffstats
Commit message (Collapse)AuthorAgeFilesLines
...
| * | | Adding a lemma for load preservationLéo Gourdin2020-10-101-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-091-40/+36
| | |
| * | exec_body_simulation without star'Léo Gourdin2020-10-091-0/+101
|/ /
* | Replace common pattern with simpler lemma.Justus Fasse2020-09-211-29/+16
| | | | | | | | | | Turns two rewrites and a simplification into a single rewrite via list_length_z_cons.
* | Proof of exec_body_simulation_plusJustus Fasse2020-09-211-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 fileJustus Fasse2020-09-211-68/+68
| |
* | Admitted lemma for exec_basic_simulation.Justus Fasse2020-09-211-0/+9
| | | | | | | | Probably still missing a couple of assumptions.
* | Prove exec_body_dont_move_PCJustus Fasse2020-08-184-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_posJustus Fasse2020-08-051-18/+50
| |
* | Minor cleanup of find_instr_bblockJustus Fasse2020-07-301-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_bblockJustus Fasse2020-07-301-3/+30
| | | | | | | | Cleanup is still TODO
* | Absurd case in find_instr_bblockJustus Fasse2020-07-301-1/+107
| | | | | | | | | | n points to neither label nor basic instruction but there is also no final exit instruction
* | Prove find_instr_bblock_tailJustus Fasse2020-07-301-2/+89
| |
* | Simplify unfold_bblock and complete unfold_body's case in find_instr_bblockJustus Fasse2020-07-292-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_bblockJustus Fasse2020-07-281-2/+18
| |
* | Messy progress on builtin-case of exec_exit_simulation_plusJustus Fasse2020-07-281-10/+25
| |
* | Messy progress on exec_exit_simulation_plusJustus Fasse2020-07-281-3/+27
| | | | | | | | | | Proves exec_exit_simulation_plus for cf_instruction (as opposed to builtins)
* | Rename/repurpose cf_instruction_simulated for exec_cfi_simulationJustus Fasse2020-07-281-179/+150
| | | | | | | | | | exec_cfi_simulation's rephrasing is inspired by the needs of exec_exit_simulation_plus.
* | Begin proof of exec_exit_simulation_plusJustus Fasse2020-07-271-0/+42
| | | | | | | | Mostly proving the absurd cases following inversion of is_nth_inst
* | Playing around with find_instr_bblock's base caseJustus Fasse2020-07-271-7/+25
| |
* | Replace some auto-generated namesJustus Fasse2020-07-271-3/+3
| |
* | Move position of n in formulation of find_instr_bblockJustus Fasse2020-07-271-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 caseJustus Fasse2020-07-271-7/+35
| |
* | Factorize common proof-pattern as lemmasJustus Fasse2020-07-271-8/+30
| | | | | | | | | | unfolding a non-empty list of basic blocks will unfold the head (unfold_bblock) and then recur on the tail.
* | Simplify premisesJustus Fasse2020-07-241-12/+9
| |
* | Remove unnecessary premiseJustus Fasse2020-07-241-4/+3
| |
* | Remove trailing whitespaceJustus Fasse2020-07-241-4/+4
| |
* | Complete size_headerJustus Fasse2020-07-241-1/+66
| |
* | Complete bblock_size_auxJustus Fasse2020-07-241-1/+24
| |
* | Complete bblock_size_aux_posJustus Fasse2020-07-241-1/+6
| | | | | | | | Steal use of list_length_z_aux_increase from exec_header_simulation.
* | proof of exec_header_simulationSylvain Boulmé2020-07-231-10/+91
| |
* | Complete bblock_non_emptyJustus Fasse2020-07-231-1/+10
| |
* | Remove trailing whitespaceJustus Fasse2020-07-221-6/+6
| |
* | Complete proof of exec_exit_simulation_starJustus Fasse2020-07-221-2/+10
| |
* | backward decomposition of the proofSylvain Boulmé2020-07-223-22/+167
| |
* | Add dynamically checked assumption to simplify AsmgenproofJustus Fasse2020-07-212-10/+24
| | | | | | | | | | Previously Asmblock.label_pos and Asm.label_pos could point to different memory location for the same label.
* | suggestion of simpler nameSylvain Boulmé2020-07-171-1/+1
| |
* | suggestion of translation from find_bblock to find_instrSylvain Boulmé2020-07-171-0/+22
| |
* | Less auto-generated namesJustus Fasse2020-07-151-36/+36
| |
* | First go at showing that translated cfi behave the sameJustus Fasse2020-07-151-0/+191
| | | | | | | | Import Axioms in order to use functional extensionality
* | Add lemma showing 1 <= Ptrofs.max_unsignedJustus Fasse2020-07-151-2/+8
| |
* | Miscellaneous lemmas that I used at some point while experimentingJustus Fasse2020-07-151-0/+84
| |
* | Add definition of match_internalJustus Fasse2020-07-151-0/+18
| | | | | | | | | | This relation will hold between Asmblock and Asm states while inside an Asmblock block.
* | "we must check that the generated code contains less than [2^32] ↵Justus Fasse2020-07-151-2/+3
| | | | | | | | | | | | instructions otherwise the offset part of the [PC] code pointer could wrap around, leading to incorrect executions" -- From the original aarch64/Asmgen.v
* | Generate both Pcsel and PfselJustus Fasse2020-07-132-2/+13
| | | | | | | | | | | | | | In Asmblock, Pcsel is used for both integer and floating-point conditional selection. A previous commit (c764ff84) had incorrectly reverted the merging of Pfsel into Pcsel.
* | Revert back to original definition of match_statesJustus Fasse2020-07-121-172/+8
| | | | | | | | (The simulation relation between aarch64's Asmblock and Asm as equality)
* | fix size of block in AsmblockSylvain Boulmé2020-07-101-5/+2
| | | | | | | | Due to the fact that, at the Asm level, Plabel runs PC++
* | Change definition of match_statesJustus Fasse2020-07-101-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 AsmgenproofJustus Fasse2020-07-091-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_lowJustus Fasse2020-07-092-6/+11
| |
generated by cgit (git 2.34.1) at 2024-07-14 04:17:59 +0000