aboutsummaryrefslogtreecommitdiffstats
Commit message (Expand)AuthorAgeFilesLines
...
| * | | Adding a lemma for load preservationLéo Gourdin2020-10-101-0/+14
| |/ /
| * | 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
* | Proof of exec_body_simulation_plusJustus Fasse2020-09-211-1/+238
* | 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
* | Prove exec_body_dont_move_PCJustus Fasse2020-08-184-42/+112
* | Proof for size_of_blocks_max_posJustus Fasse2020-08-051-18/+50
* | Minor cleanup of find_instr_bblockJustus Fasse2020-07-301-11/+10
* | Complete proof of find_instr_bblockJustus Fasse2020-07-301-3/+30
* | Absurd case in find_instr_bblockJustus Fasse2020-07-301-1/+107
* | 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
* | 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
* | Rename/repurpose cf_instruction_simulated for exec_cfi_simulationJustus Fasse2020-07-281-179/+150
* | Begin proof of exec_exit_simulation_plusJustus Fasse2020-07-271-0/+42
* | 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
* | Idea for find_instr_bblock's recursive caseJustus Fasse2020-07-271-7/+35
* | Factorize common proof-pattern as lemmasJustus Fasse2020-07-271-8/+30
* | 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
* | 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
* | 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
* | 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
* | "we must check that the generated code contains less than [2^32] instructions...Justus Fasse2020-07-151-2/+3
* | Generate both Pcsel and PfselJustus Fasse2020-07-132-2/+13
* | Revert back to original definition of match_statesJustus Fasse2020-07-121-172/+8
* | fix size of block in AsmblockSylvain Boulmé2020-07-101-5/+2
* | Change definition of match_statesJustus Fasse2020-07-101-8/+172
* | Start AsmgenproofJustus Fasse2020-07-091-3/+69
* | Finish proof of Lemma symbol_high_lowJustus Fasse2020-07-092-6/+11
generated by cgit (git 2.34.1) at 2024-07-07 04:04:09 +0000