diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-03-31 00:45:57 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-03-31 00:45:57 +0200 |
| commit | 2ebd2eced4437aea823442dd15f160917590cb8a (patch) | |
| tree | d32894364e999b77ef3fa2a8bd67d5d7ca3ca26c /backend/Injectproof.v | |
| parent | 1ba9cba60f5cf4fe0a2c1d620881cad2383c0027 (diff) | |
| download | compcert-kvx-2ebd2eced4437aea823442dd15f160917590cb8a.tar.gz compcert-kvx-2ebd2eced4437aea823442dd15f160917590cb8a.zip | |
injector "ghost steps"
Diffstat (limited to 'backend/Injectproof.v')
| -rw-r--r-- | backend/Injectproof.v | 39 |
1 files changed, 35 insertions, 4 deletions
diff --git a/backend/Injectproof.v b/backend/Injectproof.v index c3de5e47..dac93d41 100644 --- a/backend/Injectproof.v +++ b/backend/Injectproof.v @@ -775,7 +775,17 @@ Section INJECTOR. * apply assign_above; auto. Qed. - Lemma transf_function_inj_starstep : + Lemma bounded_nth_In: forall {T : Type} (l : list T) k LESS, + In (bounded_nth k l LESS) l. + Proof. + induction l; simpl; intros. + lia. + destruct k; simpl. + - left; trivial. + - right. apply IHl. + Qed. + + Lemma transf_function_inj_starstep_rec : forall ts f tf sp m inj_n src_pc inj_pc inj_code (FUN : transf_function gen_injections f = OK tf) (INJ : nth_error (PTree.elements (gen_injections f)) inj_n = @@ -849,7 +859,7 @@ Section INJECTOR. intros (SRC & ALL_VALID). rewrite forallb_forall in ALL_VALID. apply ALL_VALID. - admit. + apply bounded_nth_In. } apply nth_error_In with (n := inj_n). assumption. @@ -863,7 +873,28 @@ Section INJECTOR. destruct ALLx as [ALLx1 ALLx2]. rewrite Pos.leb_le in ALLx1. lia. - Admitted. - + Qed. + + Lemma transf_function_inj_starstep : + forall ts f tf sp m inj_n src_pc inj_pc inj_code + (FUN : transf_function gen_injections f = OK tf) + (INJ : nth_error (PTree.elements (gen_injections f)) inj_n = + Some (src_pc, inj_code)) + (POSITION : inject_l_position (Pos.succ (max_pc_function f)) + (PTree.elements (gen_injections f)) inj_n = inj_pc) + (trs : regset), + exists trs', + match_regs (f : function) trs trs' /\ + Smallstep.star RTL.step ge + (State ts tf sp inj_pc trs m) E0 + (State ts tf sp (pos_add_nat inj_pc (List.length inj_code)) trs' m). + Proof. + intros. + replace (State ts tf sp inj_pc trs m) with (State ts tf sp (pos_add_nat inj_pc ((List.length inj_code) - (List.length inj_code))%nat) trs m). + eapply transf_function_inj_starstep_rec; eauto. + f_equal. + rewrite <- minus_n_n. + reflexivity. + Qed. End PRESERVATION. End INJECTOR. |