diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2019-09-11 17:38:57 +0200 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2019-09-11 17:38:57 +0200 |
| commit | 1ed5afe12dcf340d398637e2582ee5cd5a9eec1a (patch) | |
| tree | a8eb39cd3dabaf8d9bc8a92842cc6323668090bd /backend/Duplicateproof.v | |
| parent | 417b6e77e5a0c4ea3431d5f379ff054a26b1e326 (diff) | |
| download | compcert-kvx-1ed5afe12dcf340d398637e2582ee5cd5a9eec1a.tar.gz compcert-kvx-1ed5afe12dcf340d398637e2582ee5cd5a9eec1a.zip | |
Proof of first axiom
Diffstat (limited to 'backend/Duplicateproof.v')
| -rw-r--r-- | backend/Duplicateproof.v | 11 |
1 files changed, 10 insertions, 1 deletions
diff --git a/backend/Duplicateproof.v b/backend/Duplicateproof.v index a368174f..fe26db55 100644 --- a/backend/Duplicateproof.v +++ b/backend/Duplicateproof.v @@ -3,6 +3,8 @@ Require Import AST Linking Errors Globalenvs Smallstep. Require Import Coqlib Maps Events Values. Require Import Op RTL Duplicate. +Local Open Scope positive_scope. + Definition match_prog (p tp: program) := match_program (fun _ f tf => transf_fundef f = OK tf) eq p tp. @@ -41,8 +43,15 @@ Axiom revmap_correct: forall f xf n n', (fn_revmap xf)!n' = Some n -> (forall i, (fn_code f)!n = Some i -> exists i', (fn_code (fn_RTL xf))!n' = Some i' /\ match_inst (fun n => (fn_revmap xf)!n) i i'). -Axiom revmap_entrypoint: +Theorem revmap_entrypoint: forall f xf, transf_function_aux f = OK xf -> (fn_revmap xf)!(fn_entrypoint (fn_RTL xf)) = Some (fn_entrypoint f). +Proof. + intros. unfold transf_function_aux in H. destruct (duplicate_aux _) as (tcte & mp). destruct tcte as (tc & te). + monadInv H. simpl. monadInv EQ. unfold verify_mapping_entrypoint in EQ0. simpl in EQ0. + destruct (mp ! te) eqn:PT; try discriminate. + destruct (n ?= fn_entrypoint f) eqn:EQ; try discriminate. inv EQ0. + apply Pos.compare_eq in EQ. congruence. +Qed. Section PRESERVATION. |