diff options
| author | Justus Fasse <justus.fasse@etu.univ-grenoble-alpes.fr> | 2020-09-21 12:03:12 +0200 |
|---|---|---|
| committer | Justus Fasse <justus.fasse@etu.univ-grenoble-alpes.fr> | 2020-09-21 12:03:12 +0200 |
| commit | e9b1c64cd7da39f6697020e8a1bc610923c324e4 (patch) | |
| tree | f6be8cadb34506142a29234b0ea62a5119381828 /aarch64/Asmgenproof.v | |
| parent | 51cfd8e43bc095e567f22b1768eb2743be8ffc22 (diff) | |
| download | compcert-kvx-e9b1c64cd7da39f6697020e8a1bc610923c324e4.tar.gz compcert-kvx-e9b1c64cd7da39f6697020e8a1bc610923c324e4.zip | |
Admitted lemma for exec_basic_simulation.
Probably still missing a couple of assumptions.
Diffstat (limited to 'aarch64/Asmgenproof.v')
| -rw-r--r-- | aarch64/Asmgenproof.v | 9 |
1 files changed, 9 insertions, 0 deletions
diff --git a/aarch64/Asmgenproof.v b/aarch64/Asmgenproof.v index 5092d99b..8366ae14 100644 --- a/aarch64/Asmgenproof.v +++ b/aarch64/Asmgenproof.v @@ -878,6 +878,15 @@ Proof. generalize (list_length_z_aux_increase _ l1 2); omega. Qed. +Lemma exec_basic_simulation: + forall tf n rs1 m1 rs1' m1' rs2 m2 bi tbi + (BASIC: exec_basic lk ge bi rs1 m1 = Next rs1' m1') + (MATCHI: match_internal n (State rs1 m1) (State rs2 m2)) + (TRANSBI: basic_to_instruction bi = OK tbi), + exists rs2' m2', Asm.exec_instr tge tf tbi + rs2 m2 = Next rs2' m2' + /\ match_internal (n + 1) (State rs1' m1') (State rs2' m2'). +Admitted. Lemma exec_body_simulation_plus b ofs f bb rs m s2 rs' m': forall (ATPC: rs PC = Vptr b ofs) (FINDF: Genv.find_funct_ptr ge b = Some (Internal f)) |