Merge branch 'vcgen' of gitlab.science.ru.nl:lgg/iris-c-monad into vcgen

theories/vcgen/vcgen.v

@@ -415,7 +415,7 @@ Section vcg_spec.
     awp (dcexpr_interp E de) R
       (λ v, ∃ E' dv m', ⌜dval_interp E' dv = v⌝ ∧ denv_interp E' m' ∗ wp_interp E' (Φ E' m' dv)).
   Proof.
-    revert Φ m. induction de; intros Φ m; iIntros "Hm Hwp".
+    revert Φ E m. induction de; intros Φ E m; iIntros "Hm Hwp".
     - iApply awp_ret. wp_value_head.  iExists E, d, m. iSplit; first done; iFrame.
     - iApply (vcg_wp_unknown_correct with "Hm Hwp").
     - rewrite IHde. iSpecialize ("Hm" with "Hwp"); simpl.
@@ -424,8 +424,26 @@ Section vcg_spec.
       iApply (vcg_wp_load_correct with "Hm Hwp").
     - admit.
     - admit.
-    - admit.
-    - admit.
+    - rewrite IHde. iApply a_un_op_spec. iSpecialize ("Hm" with "Hwp").
+      iApply (awp_wand with "Hm"). iIntros (v) "Hex".
+      iDestruct "Hex" as (E' dv m' <-) "(Hm & Hwp)".
+      destruct (dun_op_eval E' u dv) as [| dw | dw] eqn:Hop; simpl.
+      + iDestruct "Hwp" as (?) "[% _]"; simplify_eq /=.
+      + iExists (dval_interp E' dw); iSplit.
+        iPureIntro. apply dun_op_eval_correct. by rewrite Hop.
+        eauto with iFrame.
+      + iDestruct "Hwp" as (w) "[% Hwp]"; simplify_eq /=.
+        iExists (dval_interp E' w). iSplit. iPureIntro.
+        apply dun_op_eval_correct. by rewrite Hop.
+        eauto with iFrame.
+    - rewrite IHde1.  iSpecialize ("Hm" with "Hwp"); fold vcg_wp.
+      iApply (a_sequence_spec with "[Hm]"); fold dcexpr_interp.
+      { exists (λ: <>, dcexpr_interp E de2)%V. by unlock. }
+      iApply (awp_wand with "Hm").  iIntros (v) "Hex".
+      iDestruct "Hex" as (Enew dv m' <-) "(Hm & Hwp)". simpl. rewrite denv_unlock_interp.
+      iModIntro. rewrite IHde2. awp_seq. iSpecialize ("Hm" with "Hwp").
+    (* TODO: Need to make the main statement stronger by requiring that
+      E `prefix_of` E', just as in unknown case. *) admit.
     - iApply (vcg_wp_unknown_correct with "Hm Hwp").
    Admitted.