aboutsummaryrefslogtreecommitdiffstats
path: root/aarch64/Asmgenproof.v
Commit message (Expand)AuthorAgeFilesLines
...
* | | Other subcases for PArith are done.Léo Gourdin2020-10-141-8/+29
* | | Draft commit on the PArithComparisonPP ProofLéo Gourdin2020-10-141-14/+72
* | | Simplifying Ltac and fixing a bug in AsmBlock semanticsLéo Gourdin2020-10-131-10/+30
* | | Fixing the propagation of the new BOUNDED hypLéo Gourdin2020-10-131-8/+20
* | | Proof for PmovzLéo Gourdin2020-10-131-7/+29
* | | Adding a lemma next_instr_preservedLéo Gourdin2020-10-121-7/+56
* | | Continue the proof of exec_basic_simulationLéo Gourdin2020-10-111-18/+12
* | | Adding a lemma for exec load propagation.Léo Gourdin2020-10-111-25/+27
* | | Merge branch 'aarch64_block_bodystar' of gricad-gitlab.univ-grenoble-alpes.fr...Léo Gourdin2020-10-101-10/+14
|\ \ \
| * \ \ Merge branch 'aarch64_block_bodystar' of gricad-gitlab.univ-grenoble-alpes.fr...Sylvain Boulmé2020-10-101-0/+14
| |\ \ \
| * | | | Still generalizing exec_body_simulation_plus for an inductive proofSylvain Boulmé2020-10-091-10/+14
* | | | | More general version of load preservation lemma.Léo Gourdin2020-10-101-7/+25
| |/ / / |/| | |
* | | | 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-181-1/+64
* | | 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-291-3/+74
* | | 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-221-20/+165
* | | 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
generated by cgit (git 2.34.1) at 2024-07-06 16:27:23 +0000