Simuliris automation working nicely except for val_discr_source stuff. First...

Simuliris automation working nicely except for val_discr_source stuff. First steps for na_inv working.

theories/examples/external/simuliris/paper.v → theories/examples/external/simuliris/paper_simple.v

@@ -15,73 +15,6 @@ From iris_automation.examples.external.simuliris Require Import simuliris_automa
    interested in is the contextual refinement.
  *)
 
-From iris_automation.symb_exec Require Import defs.
-From iris_automation Require Import solve_defs proofmode_base lib.intuitionistically.
-
-Global Opaque update_si update_si_strong.
-
-
-Section collect_modal.
-  Context {PROP : bi} `{!BiBUpd PROP, !BiAffine PROP, !BiPureForall PROP}.
-  Context {Λ : language}.
-  Context {s : simulirisGS PROP Λ}.
-
-  Global Instance collect_modal_update_si_strong (P : PROP) e π  :
-    CollectModal (update_si_strong e π P) (update_si_strong e π) P | 45.
-  Proof. rewrite /CollectModal //. Qed.
-
-  Global Instance collect_modal_update_si_strong_twice (P : PROP) e π  :
-    CollectModal (update_si_strong e π (update_si_strong e π P)) (update_si_strong e π) P | 40.
-  Proof using BiAffine0.
-    rewrite /CollectModal. apply: anti_symm. 
-    - iMod 1. by do 2 (iApply update_si_stronger_update_si_strong; iApply mod_weaker).
-    - by iMod 1.
-  Qed.
-
-  Global Instance collect_modal_update_si_strong_bupd (P : PROP) e π  :
-    CollectModal (update_si_strong e π (|==> P)) (update_si_strong e π) P | 40.
-  Proof using BiAffine0.
-    rewrite /CollectModal. apply: anti_symm. 
-    - iMod 1. (iApply update_si_stronger_update_si_strong; iApply mod_weaker). iStepsS.
-    - iMod 1 as ">HP". (iApply update_si_stronger_update_si_strong; iApply mod_weaker). iStepsS.
-  Qed.
-End collect_modal.
-
-Section temp.
-  Context `{!sheapGS Σ, !sheapInv Σ}.
-
-  Global Instance sim_call_abd π Φ fname arg_l arg_lv el Kl el_f er Kr er_f arg_r arg_rv :
-    ReshapeExprAnd expr el Kl el_f (
-      TCAnd (TCEq el_f (Call f#fname arg_l)) $
-      TCAnd (TCEq (to_val arg_l) (Some arg_lv)) $
-      ReshapeExprAnd expr er Kr er_f (
-        TCAnd (TCEq er_f (Call f#fname arg_r)) $
-               TCEq (to_val arg_r) (Some arg_rv)
-      )
-    ) →
-    SatisfiesContextCondition context_as_item_condition Kl →
-    SatisfiesContextCondition context_as_item_condition Kr →
-    Abduct (TT := [tele]) false empty_hyp_first (el ⪯{π} er [{Φ}])%I id 
-        (update_si_strong (Kr $ Call f#fname arg_r) π (ext_rel π arg_lv arg_rv ∗ 
-        (∀ v_t' v_s', ext_rel π v_t' v_s' -∗ (Kl (of_val v_t') ⪯{π} Kr (of_val v_s') [{Φ}])))) | 10.
-  Proof.
-    rewrite /Abduct /= empty_hyp_first_eq left_id. iStepsS.
-    destruct x as [-> [-> [Hlv [-> [-> Hrv]]]]].
-    destruct x0 as [Kl Kl' HKl'].
-    destruct x1 as [Kr Kr' HKr'].
-    rewrite -HKl' -HKr'.
-    iApply sim_update_si_strong.
-    iStopProof. apply util_classes.modality_mono.
-    iStepS. iApply sim_bind.
-    iApply (sim_call with "H1") => //.
-    - rewrite Hlv //.
-    - rewrite Hrv //.
-    - simpl.
-      iStepsS. rewrite HKl' HKr'. iStepsS.
-  Qed.
-
-End temp.
-
 
 Section fix_bi.
   Context `{!simpleGS Σ}.
@@ -94,7 +27,7 @@ Section fix_bi.
     (l_s ↦s v_s ∗ †l_t…t 1 ∗ †l_s…s 1 ∗ val_rel v_t v_s)%I (l_t ↔h l_s)%I.
   Proof.
     rewrite /BiAbd /=.
-    iStepS. Transparent update_si.
+    iStepS.
     rewrite /update_si.
     iIntros (?????) "(HP_t & HP_s & Hσ_t & Hσ_s & (%L&Hinv&#Hgs))".
     iMod (heapbij_insertN _ l_t l_s [v_t] [v_s] 1 with "Hinv [H1] [H2] [H5] [H3] [H4]") as "[Hb #Ha]"; try (done || eauto).
@@ -105,6 +38,16 @@ Section fix_bi.
   Qed.
   Typeclasses Opaque loc_rel heap_freeable.
 
+  Global Instance sim_load_spec (l_t l_s : loc) :
+    SimultaneousSpec (! #l_t) (! #l_s) empty_hyp_last (λ π Φ, 
+      l_t ↔h l_s ∗ (∀ v_t v_s, val_rel v_t v_s -∗ Φ (of_val v_t) (of_val v_s)))%I.
+  Proof.
+    split.
+    - iStepsS. sim_load v_t v_s as "Hv".
+      iStepsS.
+    - iStepsS. iSplit; iStepsS; iApply x2; iStepsS.
+  Qed.
+
   (** Example from 2.1 *)
   Definition ex_2_1_unopt : expr := let: "y" := ref(#42) in !"y".
   Definition ex_2_1_opt : expr := let: "y" := ref(#42) in #42.
@@ -119,10 +62,7 @@ Section fix_bi.
   (* for completeness : log_rel as described in Sec 4 *)
   Lemma ex_2_1_log :
     ⊢ log_rel ex_2_1_opt ex_2_1_unopt.
-  Proof.
-    log_rel. iModIntro. iIntros (π) "_".
-    iStepsS.
-  Qed.
+  Proof. log_rel. iStepsS. Qed.
 
   (** First example from 2.2 *)
   Definition ex_2_2_1_unopt : expr :=
@@ -143,9 +83,7 @@ Section fix_bi.
 
   Lemma ex_2_2_1_log :
     ⊢ log_rel ex_2_2_1_opt ex_2_2_1_unopt.
-  Proof.
-    log_rel. iStepsS.
-  Qed.
+  Proof. log_rel. iStepsS. Qed.
 
   (** Second example from 2.2 *)
   Definition ex_2_2_2_unopt : expr :=
@@ -159,24 +97,21 @@ Section fix_bi.
     Call f#"f" "y";;
     !"y" + "z".
 
+  Arguments gen_val_rel : simpl nomatch.
+
   Lemma ex_2_2_2 π :
     ⊢ {{{ True }}} ex_2_2_2_opt ⪯[π] ex_2_2_2_unopt {{{ lift_post (λ v_t v_s, ⌜v_t = v_s⌝) }}}.
   Proof.
     iIntros "!> _". rewrite /ex_2_2_2_opt /ex_2_2_2_unopt.
-    iStepsS. sim_load v_t v_s as "Hv".
-    iStepS.
-    iStepS. Arguments gen_val_rel : simpl nomatch.
-    iStepS. val_discr_source "Hv".
+    do 45 iStepS. val_discr_source "H3".
     iStepsS.
   Qed.
 
   Lemma ex_2_2_2_log :
     ⊢ log_rel ex_2_2_2_opt ex_2_2_2_unopt.
   Proof.
-    log_rel. iStepsS.
-    sim_load v_t v_s as "Hv".
-    do 3 iStepS.
-    val_discr_source "Hv". iStepsS.
+    log_rel. do 45 iStepS.
+    val_discr_source "H4". iStepsS.
   Qed.
 
   (** Example from 2.3 *)
@@ -196,64 +131,6 @@ Section fix_bi.
     let: "z" := "x" `quot` "y" in
     Call f#"g" "z".
 
-  Lemma eval_quot_cond (x y : Z) (r : val) :
-    y ≠ 0 →
-    r = #(x `quot` y) →
-    bin_op_eval QuotOp #x #y = Some r.
-  Proof.
-    rewrite /bin_op_eval => Hx -> /=.
-    rewrite decide_False //.
-  Qed.
-
-  Hint Extern 4 (vals_compare_safe _ _) => (left; pure_solver.trySolvePure || right; pure_solver.trySolvePure) : solve_pure_add. 
-  Hint Extern 4 (bin_op_eval QuotOp _ _ = Some _) => apply eval_quot_cond; pure_solver.trySolvePure : solve_pure_eq_add.
-
-Lemma W_tac_to_expr_subst' :
-∀ (x : string) (v : val) (e : expr) (P : expr → Prop) (e' : W.expr) e'',
-  e = W.to_expr e' → (∀ v, W.subst x v e' = e'' v) → P (W.to_expr $ e'' v) → P (subst x v e).
-Proof.
-  intros. specialize (H0 v).
-  eapply W.tac_to_expr_subst => //.
-Qed.
-
-Lemma W_tac_to_expr_combine_subst_map' v :
-∀ (e : val → W.expr) (P : expr → Prop) e', (∀ v, W.combine_subst_map [] (e v) = (e' v)) → P (W.to_expr $ e' v) → P (W.to_expr $ e v).
-Proof.
-  intros. specialize (H v).
-  eapply W.tac_to_expr_combine_subst_map => //.
-Qed.
-
-Ltac simpl_subst' :=
-  repeat match goal with
-    | |- context C [apply_func ?fn ?v] =>
-      (* Unfold [apply_func] if the function's components are available *)
-      let arg := open_constr:(_ : string) in
-      let body := open_constr:(_ : expr) in
-      unify fn (arg, body);
-      change (apply_func fn v) with (subst arg v body)
-    end;
-  repeat match goal with
-    | |- context C [subst ?x ?v ?e] =>
-      lazymatch e with
-      | subst _ _ _ => fail
-      | _ => idtac
-      end;
-      pattern (subst x v e);
-      let e' := W.of_expr e in
-      simple refine (W_tac_to_expr_subst' _ _ _ _ e' _ _ _ _); [ shelve
-      | simpl; rewrite ?list_to_map_to_list; reflexivity
-      | intros ?; vm_compute W.subst; reflexivity
-      |];
-      simple refine (W_tac_to_expr_combine_subst_map' _ _ _ _ _ _); [ shelve
-      | intros ?; vm_compute W.combine_subst_map; reflexivity
-      | ];
-      simpl
-    end.
-
-
-Hint Extern 3 (SimplSubst ?e ?e') =>
-  simpl; simpl_subst'; reflexivity : typeclass_instances.
-
   Lemma ex_2_3 π :
     ⊢ {{{ True }}} ex_2_3_opt ⪯[π] ex_2_3_unopt {{{ lift_post (λ v_t v_s, True) }}}.
   Proof.

theories/examples/external/simuliris/simuliris_automation_base.v

-From iris_automation Require Import proofmode_base.
+From iris_automation Require Export proofmode_base.
 From iris_automation.symb_exec Require Import defs.
+From iris_automation.lib Require Import intuitionistically.
 
 From simuliris.simulation Require Import lifting.
 From simuliris.simulang Require Import primitive_laws.
@@ -325,8 +326,50 @@ End modalities.
 Class SimplSubst (e e' : expr) :=
   is_simpl_subst : e = e'.
 
+Lemma W_tac_to_expr_subst' :
+∀ (x : string) (v : val) (e : expr) (P : expr → Prop) (e' : W.expr) e'',
+  e = W.to_expr e' → (∀ v, W.subst x v e' = e'' v) → P (W.to_expr $ e'' v) → P (subst x v e).
+Proof.
+  intros. specialize (H0 v).
+  eapply W.tac_to_expr_subst => //.
+Qed.
+
+Lemma W_tac_to_expr_combine_subst_map' v :
+∀ (e : val → W.expr) (P : expr → Prop) e', (∀ v, W.combine_subst_map [] (e v) = (e' v)) → P (W.to_expr $ e' v) → P (W.to_expr $ e v).
+Proof.
+  intros. specialize (H v).
+  eapply W.tac_to_expr_combine_subst_map => //.
+Qed. (* abstracts over v so that vm_compute does not unfold value computations *)
+
+Ltac simpl_subst' :=
+  repeat match goal with
+    | |- context C [apply_func ?fn ?v] =>
+      (* Unfold [apply_func] if the function's components are available *)
+      let arg := open_constr:(_ : string) in
+      let body := open_constr:(_ : expr) in
+      unify fn (arg, body);
+      change (apply_func fn v) with (subst arg v body)
+    end;
+  repeat match goal with
+    | |- context C [subst ?x ?v ?e] =>
+      lazymatch e with
+      | subst _ _ _ => fail
+      | _ => idtac
+      end;
+      pattern (subst x v e);
+      let e' := W.of_expr e in
+      simple refine (W_tac_to_expr_subst' _ _ _ _ e' _ _ _ _); [ shelve
+      | simpl; rewrite ?list_to_map_to_list; reflexivity
+      | intros ?; vm_compute W.subst; reflexivity
+      |];
+      simple refine (W_tac_to_expr_combine_subst_map' _ _ _ _ _ _); [ shelve
+      | intros ?; vm_compute W.combine_subst_map; reflexivity
+      | ];
+      simpl
+    end.
+
 Global Hint Extern 4 (SimplSubst ?e ?e') =>
-  simpl; simpl_subst; reflexivity : typeclass_instances.
+  simpl; simpl_subst'; reflexivity : typeclass_instances.
 
 
 Section specs.
@@ -583,9 +626,102 @@ End abducts.
 
 
 
+Lemma eval_quot_cond (x y : Z) (r : val) :
+  y ≠ 0 →
+  r = #(x `quot` y) →
+  bin_op_eval QuotOp #x #y = Some r.
+Proof.
+  rewrite /bin_op_eval => Hx -> /=.
+  rewrite decide_False //.
+Qed.
 
 
 
+Global Hint Extern 4 (vals_compare_safe _ _) => (left; pure_solver.trySolvePure || right; pure_solver.trySolvePure) : solve_pure_add. 
+Global Hint Extern 4 (bin_op_eval QuotOp _ _ = Some _) => apply eval_quot_cond; pure_solver.trySolvePure : solve_pure_eq_add.
+
+
+Typeclasses Opaque update_si update_si_strong.
+Global Arguments update_si_strong : simpl never.
+Global Arguments update_si : simpl never.
+
+
+Section collect_modal.
+  Context {PROP : bi} `{!BiBUpd PROP, !BiAffine PROP, !BiPureForall PROP}.
+  Context {Λ : language}.
+  Context {s : simulirisGS PROP Λ}.
+
+  Global Instance collect_modal_update_si_strong (P : PROP) e π  :
+    CollectModal (update_si_strong e π P) (update_si_strong e π) P | 45.
+  Proof. rewrite /CollectModal //. Qed.
+
+  Global Instance collect_modal_update_si_strong_twice (P : PROP) e π  :
+    CollectModal (update_si_strong e π (update_si_strong e π P)) (update_si_strong e π) P | 40.
+  Proof using BiAffine0.
+    rewrite /CollectModal. apply: anti_symm. 
+    - iMod 1. by do 2 (iApply update_si_stronger_update_si_strong; iApply mod_weaker).
+    - by iMod 1.
+  Qed.
+
+  Global Instance collect_modal_update_si_strong_bupd (P : PROP) e π  :
+    CollectModal (update_si_strong e π (|==> P)) (update_si_strong e π) P | 40.
+  Proof using BiAffine0.
+    rewrite /CollectModal. apply: anti_symm. 
+    - iMod 1. (iApply update_si_stronger_update_si_strong; iApply mod_weaker). iStepsS.
+    - iMod 1 as ">HP". (iApply update_si_stronger_update_si_strong; iApply mod_weaker). iStepsS.
+  Qed.
+End collect_modal.
+
+
+Section sim_specs.
+  Context `{!sheapGS Σ, !sheapInv Σ}.
+
+  Class SimultaneousSpec el er H (P : thread_id → (expr → expr → iProp Σ) → iProp Σ) := {
+    simultaneous_spec Φ π : H ∗ P π Φ ⊢ el ⪯{π} er [{Φ}];
+    simultaneous_spec_funex Φ Ψ π : (∀ e1 e2, Φ e1 e2 ⊣⊢ Ψ e1 e2) → P π Φ ⊣⊢ P π Ψ
+  }.
+
+  Global Instance sim_call_sim_spec π Φ el er Kl Kr el_f er_f H P :
+    ReshapeExprAnd expr el Kl el_f (
+      ReshapeExprAnd expr er Kr er_f (
+        SimultaneousSpec el_f er_f H P
+      )
+    ) →
+    SatisfiesContextCondition context_as_item_condition Kl →
+    SatisfiesContextCondition context_as_item_condition Kr →
+    Abduct (TT := [tele]) false H (el ⪯{π} er [{Φ}])%I id 
+        (update_si_strong er π $ P π $ λ e_t' e_s', Kl e_t' ⪯{π} Kr e_s' [{Φ}])%I | 10.
+  Proof.
+    rewrite /Abduct /=. iStepsS.
+    destruct x as [-> [-> Hspec]].
+    destruct x0 as [Kl Kl' HKl'].
+    destruct x1 as [Kr Kr' HKr'].
+    rewrite -HKl' -HKr'.
+    iApply sim_update_si_strong.
+    iStopProof. rewrite modality_ec_frame_r.
+    apply util_classes.modality_mono.
+    iStepS. iApply sim_expr_bind.
+    destruct Hspec as [H1 H2].
+    iApply H1. iFrame. iStopProof. simpl.
+    erewrite H2; first done.
+    move => e1 e2 /=. rewrite HKl' HKr' //.
+  Qed.
+
+  Global Instance call_sim_spec fname arg_l arg_lv arg_r arg_rv :
+    TCEq (to_val arg_l) (Some arg_lv) →
+    TCEq (to_val arg_r) (Some arg_rv) →
+    SimultaneousSpec (Call f#fname arg_l) (Call f#fname arg_r) empty_hyp_first (λ π Φ,
+      ext_rel π arg_lv arg_rv ∗ (∀ v_t' v_s', ext_rel π v_t' v_s' -∗ Φ v_t' v_s'))%I.
+  Proof.
+    move => Hl Hr; split.
+    - move => Φ π. iStepS.
+      iApply (sim_call with "H1") => //; [rewrite Hl| rewrite Hr]; done.
+    - move => Φ Ψ π HΦΨ. apply: anti_symm.
+      * iStepsS. iApply HΦΨ. iStepsS.
+      * iStepsS. iApply HΦΨ. iStepsS.
+  Qed.
+End sim_specs.
+