notes and some lemma statements

theories/vir/contextual.v

-From Coq Require Import Lists.List.
+From Coq Require Import Lists.List String.
 
 From ExtLib Require Import
      Core.RelDec
@@ -12,16 +12,36 @@ From Vellvm Require Import
      Theory
      Utils.PostConditions.
 
-From ITree Require Import ITree Eq.Eqit.
+From ITree Require Import
+     ITree
+     Eq.Eqit
+     RecursionFacts.
 
 From Paco Require Import paco.
 
 Import ListNotations.
 Import MonadNotation.
 
+
 (* Syntactic formulation of contexts that work for transformations at the
   block-level on the context of open cfg's *)
-Section ctxt.
+
+(* Example transformation (within a block, doesn't change control flow)
+
+  f (x) -> int y = x;
+          while (true) { print 4; read x }
+
+  g () -> int x = 0; f (x)
+
+  ---"optimized"---
+
+  f (x) -> int y = x;
+          while (true) { read x; print 4 }
+
+  g () -> int x = 0; f (x)
+
+  *)
+Section block_ctxt.
 
   Notation ocfg := (ocfg dtyp).
   Notation code := (code dtyp).
@@ -64,22 +84,6 @@ Section ctxt.
       | None => bks
       end.
 
-  Lemma unchanged_blocks_ocfg :
-    forall bid id,
-      bid <> id ->
-      forall CFG code entry,
-        denote_ocfg (mk_ctxt CFG id code) (bid, entry) ≈
-        denote_ocfg CFG (bid, entry).
-  Proof.
-  Abort.
-
-  (* TBD: Add preconditions here *)
-  Lemma changed_blocks_cfg :
-    forall id entry CFG code,
-      denote_ocfg (mk_ctxt CFG id code) (id, entry) ≈
-      denote_code (code) ;; ret (inl (id, entry)).
-  Abort.
-
   Definition code_of_block : ocfg -> block_id -> option code :=
     fun bks id =>
       x <- find_block bks id ;; ret (blk_code x).
@@ -176,6 +180,7 @@ Section ctxt.
       auto.
   Qed.
 
+  (* FIXME: Reformulate CR as a definition *)
   Lemma ocfg_contextual_refinement :
     forall blk id entry CFG code,
       find_block CFG (blk_id blk) = Some blk ->
@@ -209,4 +214,92 @@ Section ctxt.
       + efinal; reflexivity.
   Qed.
 
-End ctxt.
+  (* Lemma ocfg_contextual_refinement_interp : *)
+  (*   forall blk id entry CFG code, *)
+  (*     find_block CFG (blk_id blk) = Some blk -> *)
+  (*     (forall id σ_t σ_s, ⟦ denote_block blk id ⟧ σ_t ≈ ⟦ denote_block (bk_change_code code blk) id ⟧ σ_s) -> *)
+  (*     forall σ_t σ_s, *)
+  (*     ⟦ denote_ocfg (mk_ctxt CFG (blk_id blk) (blk_code blk)) (id, entry) ⟧ σ_t ≈ *)
+  (*     ⟦ denote_ocfg (mk_ctxt CFG (blk_id blk) code) (id, entry) ⟧ σ_s. *)
+  (* Proof. *)
+  (* Admitted. *)
+
+  (* TODO: Prove this in the Iris logic *)
+
+End block_ctxt.
+
+(* Function-level CR : we can replace any internal function definition with an
+  equivalent definition *)
+Section fn_ctxt.
+
+  (* N.B: Ideal target for adequacy from the Iris logic
+     -> Refer to Simuliris paper adequacy/CR diagram
+   *)
+  Lemma fndef_contextual_refinement :
+    forall dv f f' fundefs dt f_value args,
+      (forall args, f args ≈ f' args) ->
+      denote_mcfg ((dv, f) :: fundefs) dt f_value args ≈
+      denote_mcfg ((dv, f') :: fundefs) dt f_value args.
+  Proof.
+    unfold denote_mcfg.
+    setoid_rewrite RecursionFacts.mrec_as_interp.
+    einit. ecofix CIH.
+    intros.
+  Admitted.
+
+  (* Structural lemma about [denote_mcfg] allowing an arbitrary permutation of
+    fndefs *)
+
+End fn_ctxt.
+
+(* Linking CR : we can replace any linked mcfg with an equivalent definition *)
+Section mcfg_ctxt.
+
+  Definition denote_vellvm_link_mcfg
+            (ret_typ : dtyp)
+            (entry : string)
+            (args : list uvalue)
+            (mcfg1 mcfg2 : CFG.mcfg dtyp) : itree L0 uvalue :=
+    build_global_environment mcfg1 ;;
+    build_global_environment mcfg2 ;;
+    'defns1 <- map_monad address_one_function (m_definitions mcfg1) ;;
+    'defns2 <- map_monad address_one_function (m_definitions mcfg2) ;;
+    'addr <- trigger (GlobalRead (Name entry)) ;;
+    denote_mcfg (defns1 ++ defns2) ret_typ (dvalue_to_uvalue addr) args.
+
+  Lemma denote_vellvm_global_env :
+    forall ret_typ entry args mcfg mcfg',
+      denote_vellvm ret_typ entry args mcfg ≈ denote_vellvm ret_typ entry args mcfg' ->
+      build_global_environment mcfg ≈ build_global_environment mcfg'.
+  Proof.
+    intros.
+    unfold denote_vellvm in H.
+    cbn in H.
+    remember (fun x : list (dvalue * function_denotation) =>
+            ITree.bind (trigger (GlobalRead (Name entry)))
+              (fun x0 : dvalue => denote_mcfg x ret_typ (dvalue_to_uvalue x0) args)).
+    repeat setoid_rewrite bind_bind in H.
+    repeat setoid_rewrite bind_ret_l in H.
+    (* Prove by induction on the lists *)
+  Admitted.
+
+  Lemma denote_vellvm_address_one_function :
+    forall ret_typ entry args mcfg mcfg',
+      denote_vellvm ret_typ entry args mcfg ≈ denote_vellvm ret_typ entry args mcfg' ->
+      map_monad address_one_function (m_definitions mcfg) ≈ map_monad address_one_function (m_definitions mcfg').
+  Admitted.
+
+  Lemma mcfg_contextual_refinement :
+    forall ret_typ entry args mcfg1 mcfg1' mcfg2,
+      denote_vellvm ret_typ entry args mcfg1 ≈ denote_vellvm ret_typ entry args mcfg1' ->
+      denote_vellvm_link_mcfg ret_typ entry args mcfg1 mcfg2 ≈
+      denote_vellvm_link_mcfg ret_typ entry args mcfg1' mcfg2.
+  Proof.
+    intros. unfold denote_vellvm_link_mcfg.
+    pose proof (denote_vellvm_global_env _ _ _ _ _ H).
+    pose proof (denote_vellvm_address_one_function _ _ _ _ _ H).
+    repeat (eapply eutt_clo_bind; [ solve [eauto | reflexivity] | intros; subst ]).
+    reflexivity.
+  Qed.
+
+End mcfg_ctxt.