From 1ed5afe12dcf340d398637e2582ee5cd5a9eec1a Mon Sep 17 00:00:00 2001
From: Cyril SIX <cyril.six@kalray.eu>
Date: Wed, 11 Sep 2019 17:38:57 +0200
Subject: Proof of first axiom

---
 backend/Duplicate.v      | 18 +++++++++++++++---
 backend/Duplicateproof.v | 11 ++++++++++-
 2 files changed, 25 insertions(+), 4 deletions(-)

(limited to 'backend')

diff --git a/backend/Duplicate.v b/backend/Duplicate.v
index cb3936bb..a18892cd 100644
--- a/backend/Duplicate.v
+++ b/backend/Duplicate.v
@@ -5,6 +5,7 @@ Require Import AST RTL Maps Globalenvs.
 Require Import Coqlib Errors.
 
 Local Open Scope error_monad_scope.
+Local Open Scope positive_scope.
 
 (** External oracle returning the new RTL code (entry point unchanged),
     along with the new entrypoint, and a mapping of new nodes to old nodes *)
@@ -29,8 +30,19 @@ Definition fundef_RTL (fu: xfundef) : fundef :=
 
 (** * Verification of node duplications *)
 
-(** Verifies that the mapping [mp] is giving correct information *)
-Definition verify_mapping (xf: xfunction) (tc: code) (tentry: node) : res unit := OK tt. (* TODO *)
+Definition verify_mapping_entrypoint (f: function) (xf: xfunction) : res unit :=
+  match ((fn_revmap xf)!(fn_entrypoint (fn_RTL xf))) with
+  | None => Error (msg "verify_mapping: No node in xf revmap for entrypoint")
+  | Some n => match (Pos.compare n (fn_entrypoint f)) with
+              | Eq => OK tt
+              | _ => Error (msg "verify_mapping_entrypoint: xf revmap for entrypoint does not correspond to the entrypoint of f")
+              end
+  end.
+
+(** Verifies that the [fn_revmap] of the translated function [xf] is giving correct information in regards to [f] *)
+Definition verify_mapping (f: function) (xf: xfunction) : res unit :=
+  do u <- verify_mapping_entrypoint f xf; OK tt.
+(* TODO - verify the other axiom *)
 
 (** * Entry points *)
 
@@ -38,7 +50,7 @@ Definition transf_function_aux (f: function) : res xfunction :=
   let (tcte, mp) := duplicate_aux f in
   let (tc, te) := tcte in
   let xf := {| fn_RTL := (mkfunction (fn_sig f) (fn_params f) (fn_stacksize f) tc te); fn_revmap := mp |} in
-  do u <- verify_mapping xf tc te;
+  do u <- verify_mapping f xf;
   OK xf.
 
 Theorem transf_function_aux_preserves:
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.
 
-- 
cgit