Checkpoint. Work on k_spec and contains_UB.

vellvm · Aug 10, 2023 · ff3952a · ff3952a
1 parent b32e45a
commit ff3952a
Show file tree

Hide file tree

Showing 4 changed files with 125 additions and 4 deletions.
diff --git a/src/coq/QC/GenAST.v b/src/coq/QC/GenAST.v
@@ -22,6 +22,10 @@ Require Import List.
 
 Import ListNotations.
 
+(* TODO: Probably should try to remove these... *)
+Unset Universe Checking.
+Unset Auto Template Polymorphism.
+
 From Vellvm Require Import LLVMAst Utilities AstLib Syntax.CFG Syntax.TypeUtil Syntax.TypToDtyp DynamicTypes Semantics.TopLevel QC.Generators QC.Utils Handlers.Handlers.
 Require Import Integers.
 

diff --git a/src/coq/Semantics/InfiniteToFinite.v b/src/coq/Semantics/InfiniteToFinite.v
@@ -19997,6 +19997,24 @@ intros addr_fin addr_inf ms_fin ms_inf byte_inf byte_fin MSR ADDR_CONV BYTE_REF
                   setoid_rewrite bind_trigger in HSPEC.
                   red in KS.
                   rewrite HSPEC in KS.
+                  destruct KS as [CONTRA | KS].
+                  { exfalso.
+                    inv CONTRA.
+                    - pinversion H0.
+                      inv CHECK1.
+                    - pinversion H0.
+                      subst_existT.
+                      subst_existT.
+                      inv H0.
+                      subst_existT.
+                      specialize (REL0 x).
+                      red in REL0.
+                      pclearbot.
+                      eapply ret_not_contains_UB; [| eapply H1].
+                      rewrite <- REL0 in H1.
+                      pinversion H1.
+                    pinversion H0
+                  }
                   setoid_rewrite bind_vis in KS.
                   punfold KS; red in KS; cbn in KS.
                   dependent induction KS.
@@ -20231,7 +20249,6 @@ intros addr_fin addr_inf ms_fin ms_inf byte_inf byte_fin MSR ADDR_CONV BYTE_REF
                               red.
                               rewrite VIS_HANDLED.
                               cbn in *.
-                              rewrite 
                             }
 
                             2: {

diff --git a/src/coq/Theory/ContainsUB.v b/src/coq/Theory/ContainsUB.v
@@ -40,7 +40,7 @@ Section contains_UB.
   Inductive contains_UB {R} : itree Eff R -> Prop :=
   | CrawlTau  : forall t1 t2, t2 ≅ Tau t1 -> contains_UB t1 -> contains_UB t2
   | CrawlVis : forall Y (e : Eff Y) x k t2, t2 ≅ (vis e k) -> contains_UB (k x) -> contains_UB t2
-  | FindUB    : forall `{UB_EFF : UBE -< Eff} s k t2, t2 ≅ (vis (@subevent UBE Eff UB_EFF _ (ThrowUB s)) k) -> contains_UB t2.
+  | FindUB    : forall `{Eff_UBE : UBE -< Eff} s k t2, t2 ≅ (vis (@subevent UBE Eff Eff_UBE void (ThrowUB s)) k) -> contains_UB t2.
 
   #[global] Instance proper_eutt_contains_UB {R} {RR : relation R} : Proper (@eqit Eff _ _ RR true true ==> iff) contains_UB.
   Proof.
@@ -269,7 +269,8 @@ Section contains_UB_lemmas.
 End contains_UB_lemmas.
 
 Section bind_lemmas.
-  Context {Eff : Type -> Type}.
+  Context {E F G : Type -> Type}.
+  Local Notation Eff := (E +' F +' UBE +' G).
 
   (* TODO: Move this somewhere more useful? *)
   Class SubeventInversion (Eff : Type -> Type) : Prop :=

diff --git a/src/coq/Theory/OOMRefinementExamples.v b/src/coq/Theory/OOMRefinementExamples.v
@@ -761,6 +761,7 @@ Module Infinite.
 
   Lemma interp_memory_prop_vis_inv:
     forall E R X
+      (ENUB : E <> UBE)
       (e : (E +' LLVMParamsBigIntptr.Events.IntrinsicE +' LLVMParamsBigIntptr.Events.MemoryE +' LLVMParamsBigIntptr.Events.PickUvalueE +' OOME +' UBE +' DebugE +' FailureE) X)
       k sid m x,
       interp_memory_prop (E:=E) (R2 := R) eq (Vis e k) sid m x ->
@@ -801,7 +802,105 @@ Module Infinite.
       right.
       exists A. exists e0. exists k0.
       reflexivity.
-    - dependent destruction H1.
+    - subst_existT.
+      red in KS.
+      destruct KS as [UB | KS].
+      { (* UB... *)
+        exfalso.
+        repeat red in HSPEC.
+        destruct e.
+        - repeat red in HSPEC.
+          rewrite HSPEC in UB.
+          setoid_rewrite bind_trigger in UB.
+          dependent induction UB.
+          + pinversion H; subst.
+            inv CHECK.
+          + (* CrawlVis *)
+          (* Should mean that k0 is just a ret, which should lead to a contradiction in UB *)
+            eapply eqit_inv_Vis_weak in H.
+            destruct H as (?&?&?); subst.
+            red in H0.
+            rewrite <- H0 in UB.
+            eapply ContainsUB.ret_not_contains_UB.
+            2: {
+              eapply UB.
+            }
+
+            inv UB.
+            pinversion H1.
+            punfold H; red in H; cbn in H.
+
+            inv H.
+            subst_existT.
+
+            Set Printing Implicit.
+            assert
+              (
+(@subevent E (E +' LLVMParamsBigIntptr.Events.PickUvalueE +' OOME +' UBE +' DebugE +' FailureE)
+              (@ReSum_inl (Type -> Type) IFun sum1 Cat_IFun Inl_sum1 E E
+                 (LLVMParamsBigIntptr.Events.PickUvalueE +' OOME +' UBE +' DebugE +' FailureE)
+                 (@ReSum_id (Type -> Type) IFun Id_IFun E)) X e) =
+(@subevent (E +' LLVMParamsBigIntptr.Events.PickUvalueE +' OOME +' UBE +' DebugE +' FailureE)
+              (E +' LLVMParamsBigIntptr.Events.PickUvalueE +' OOME +' UBE +' DebugE +' FailureE)
+              (@ReSum_id (Type -> Type) IFun Id_IFun
+                 (E +' LLVMParamsBigIntptr.Events.PickUvalueE +' OOME +' UBE +' DebugE +' FailureE)) Y e0)).
+
+
+                (@subevent E (E +' LLVMParamsBigIntptr.Events.PickUvalueE +' OOME +' UBE +' DebugE +' FailureE)
+                  (@ReSum_inl (Type -> Type) IFun sum1 Cat_IFun Inl_sum1 E E
+                     (LLVMParamsBigIntptr.Events.PickUvalueE +' OOME +' UBE +' DebugE +' FailureE) =
+                     (@subevent (E +' LLVMParamsBigIntptr.Events.PickUvalueE +' OOME +' UBE +' DebugE +' FailureE)
+                        (E +' LLVMParamsBigIntptr.Events.PickUvalueE +' OOME +' UBE +' DebugE +' FailureE)
+                        (@ReSum_id (Type -> Type) IFun Id_IFun
+                           (E +' LLVMParamsBigIntptr.Events.PickUvalueE +' OOME +' UBE +' DebugE +' FailureE)) Y e0)
+                      (@ReSum_id (Type -> Type) IFun Id_IFun E)) X e)).
+                subevent X e = subevent Y e0).
+            inv H.
+            subst_existT.
+
+          + pinversion H; repeat subst_existT.
+            unfold subevent in H5.
+            unfold resum in H5.
+            unfold ReSum_inl, ReSum_id in H5.
+            unfold id_, Id_IFun in H5.
+            unfold cat, Cat_IFun in H5.
+            unfold inl_, Inl_sum1 in H5.
+            unfold resum in H5.
+
+
+          + subst.
+            pinversion H.
+            repeat subst_existT.
+
+            unfold subevent in *.
+            unfold resum in H6.
+            cbn in H6.
+          rw
+          rewrite vis_ret in UB.
+          dependent induction UB.
+          + pinversion H; subst_existT.
+            inv CHECK.
+          + pinversion H; subst_existT.
+            subst_existT.
+            inv H5.
+
+          admit. (* Need to know that E is not UBE, so UB is a contradiction *)
+        - repeat red in HSPEC.
+          destruct s.
+          + repeat red in HSPEC.
+            destruct HSPEC as [UB' | [ERR | [OOM | HSPEC]]].
+            * destruct UB'.
+              repeat red in H.
+              destruct i.
+              break_match_hyp.
+              -- cbn in H.
+                 cbn in H.
+          rewrite HSPEC in UB.
+          setoid_rewrite bind_trigger in UB.
+
+      }
+
+      dependent destruction H1.
       left.
       eexists _,_,_,_; split; eauto.
       + rewrite <- itree_eta; eauto.