new example: gcd.v; add a_un_op_spec rule; put helper lemmas into separate file (derived.v)

_CoqProject

@@ -8,5 +8,7 @@ theories/lib/U.v
 theories/c_translation/monad.v
 theories/c_translation/proofmode.v
 theories/c_translation/translation.v
+theories/c_translation/derived.v
 theories/tests/test1.v
-theories/tests/fact.v
\ No newline at end of file
+theories/tests/fact.v
+theories/tests/gcd.v
\ No newline at end of file

theories/c_translation/derived.v

+From iris.heap_lang Require Export proofmode notation.
+From iris.heap_lang Require Import spin_lock assert par.
+From iris.algebra Require Import frac auth.
+From iris_c.lib Require Import locking_heap mset flock U.
+From iris_c.c_translation Require Import proofmode translation.
+
+Section Derived.
+
+  Context `{locking_heapG Σ, heapG Σ, flockG Σ, spawnG Σ}.
+
+
+  Lemma a_load_ret (l: loc) (w: val) R Φ:
+    l ↦U w ∗ (l ↦U w -∗ Φ w) -∗
+    awp (a_load (a_ret (#l)%E)) R Φ.
+  Proof.
+    iIntros "H". iApply a_load_spec.
+    iApply awp_ret. wp_value_head.
+    iExists l, w. by iFrame.
+  Qed.
+
+  Lemma a_alloc_ret (w: val) R Φ:
+    (∀ (l: loc), (l ↦U w -∗ Φ #l)) -∗
+    awp (a_alloc (a_ret w)) R Φ.
+  Proof.
+    iIntros "H". iApply a_alloc_spec.
+    iApply awp_ret. by wp_value_head.
+  Qed.
+
+  Lemma a_store_ret (l:loc) (e: expr) `{Closed [] e}  R Φ :
+    awp e R (λ w, ∃ v, l ↦U v ∗ (l ↦L w -∗ Φ w)) -∗
+    awp (a_store (a_ret #l) e) R Φ.
+  Proof.
+    iIntros "H".
+    iApply ((a_store_spec _ _
+               (λ l1, ⌜l1 = l⌝)%I
+               (λ w, ∃ v, (l ↦U v ∗ (l ↦L w -∗ Φ w)))%I ) with "[] [H] []").
+    - iApply awp_ret; iApply wp_value; eauto.
+    - done.
+    - iIntros (? w) "-> H". eauto with iFrame.
+  Qed.
+
+  Ltac awp_load_ret l w := iApply (a_load_ret l w); iFrame; eauto.
+  Ltac awp_ret_value := iApply awp_ret; iApply wp_value; eauto.
+  Ltac awp_alloc_ret w r h := iApply (a_alloc_ret w); iIntros (r) h; awp_lam.
+
+  Lemma awp_bin_op_load_load op (l r : loc) (v1 v2: val) R Φ :
+    l ↦U v1 -∗ r ↦U v2 -∗
+    (l ↦U v1 -∗ r ↦U v2 -∗ ∃ w : val, ⌜bin_op_eval op v1 v2 = Some w⌝ ∧ Φ w) -∗
+    awp (a_bin_op op (a_load (a_ret #l)) (a_load (a_ret #r))) R Φ.
+  Proof.
+    iIntros "Hl Hr HΦ".
+    iApply (a_bin_op_spec _ _
+          (λ x, ⌜x = v1⌝ ∧  l ↦U v1 )%I
+          (λ x, ⌜x = v2⌝ ∧ r ↦U v2)%I  with "[Hl] [Hr] [HΦ]").
+    - awp_load_ret l v1.
+    - awp_load_ret r v2.
+    - iIntros (??) "[-> Hl] [-> Hr]".
+      iApply ("HΦ" with "[$Hl] [$Hr]").
+  Qed.
+
+End Derived.
+
+Ltac awp_load_ret l w := iApply (a_load_ret l w); iFrame; eauto.
+Ltac awp_ret_value := iApply awp_ret; iApply wp_value; eauto.
+Ltac awp_alloc_ret w r h := iApply (a_alloc_ret w); iIntros (r) h; awp_lam.

theories/c_translation/translation.v

@@ -25,7 +25,7 @@ Definition a_load : val := λ: "x",
   ) "x".
 
 Definition a_un_op (op : un_op) : val := λ: "x",
-  a_bind (λ: "v", a_ret (λ: <>, UnOp op "v")) "x".
+  a_bind (λ: "v", a_ret (UnOp op "v")) "x".
 
 Definition a_bin_op (op : bin_op) : val := λ: "x1" "x2",
   a_bind (λ: "vv",
@@ -219,6 +219,18 @@ Section proofs.
     - iApply ("H" with "Hl'").
   Qed.
 
+  Lemma a_un_op_spec R Φ e op:
+    awp e R (λ v, ∃ w, ⌜un_op_eval op v = Some w⌝ ∧ Φ w) -∗
+    awp (a_un_op op e) R Φ.
+  Proof.
+    iIntros "H".
+    awp_apply (a_wp_awp with "H"); iIntros (v) "HΦ"; awp_lam.
+    iApply awp_bind.
+    iApply (awp_wand with "HΦ"); iIntros (w) "HΦ"; awp_lam.
+    iDestruct "HΦ" as (w0) "[% H]".
+    iApply awp_ret. by wp_op.
+  Qed.
+
   Lemma a_bin_op_spec R Φ Ψ1 Ψ2 (op : bin_op) (e1 e2: expr) :
     awp e1 R Ψ1 -∗ awp e2 R Ψ2 -∗
     (∀ v1 v2, Ψ1 v1 -∗ Ψ2 v2 -∗
@@ -288,45 +300,3 @@ Section proofs.
 
 
 End proofs.
-
-
-Section Derived.
-
-  Context `{locking_heapG Σ, heapG Σ, flockG Σ, spawnG Σ}.
-
-
-  Lemma a_load_ret (l: loc) (w: val) R Φ:
-    l ↦U w ∗ (l ↦U w -∗ Φ w) -∗
-    awp (a_load (a_ret (#l)%E)) R Φ.
-  Proof.
-    iIntros "H". iApply a_load_spec.
-    iApply awp_ret. wp_value_head.
-    iExists l, w. by iFrame.
-  Qed.
-
-  Lemma a_alloc_ret (w: val) R Φ:
-    (∀ (l: loc), (l ↦U w -∗ Φ #l)) -∗
-    awp (a_alloc (a_ret w)) R Φ.
-  Proof.
-    iIntros "H". iApply a_alloc_spec.
-    iApply awp_ret. by wp_value_head.
-  Qed.
-
-  Lemma a_store_ret (l:loc) (e: expr) `{Closed [] e}  R Φ :
-    awp e R (λ w, ∃ v, l ↦U v ∗ (l ↦L w -∗ Φ w)) -∗
-    awp (a_store (a_ret #l) e) R Φ.
-  Proof.
-    iIntros "H".
-    iApply ((a_store_spec _ _
-               (λ l1, ⌜l1 = l⌝)%I
-               (λ w, ∃ v, (l ↦U v ∗ (l ↦L w -∗ Φ w)))%I ) with "[] [H] []").
-    - iApply awp_ret; iApply wp_value; eauto.
-    - done.
-    - iIntros (? w) "-> H". eauto with iFrame.
-  Qed.
-
-End Derived.
-
-  Ltac awp_load_ret l w := iApply (a_load_ret l w); iFrame; eauto.
-  Ltac awp_ret_value := iApply awp_ret; iApply wp_value; eauto.
-  Ltac awp_alloc_ret w r h := iApply (a_alloc_ret w); iIntros (r) h; awp_lam.
\ No newline at end of file

theories/tests/fact.v

@@ -2,7 +2,7 @@ From iris.heap_lang Require Export proofmode notation.
 From iris.heap_lang Require Import spin_lock assert par.
 From iris.algebra Require Import frac auth.
 From iris_c.lib Require Import locking_heap mset flock U.
-From iris_c.c_translation Require Import proofmode translation.
+From iris_c.c_translation Require Import proofmode translation derived.
 
 
 Section factorial.

theories/tests/gcd.v

+From iris.heap_lang Require Export proofmode notation.
+From iris.heap_lang Require Import spin_lock assert par.
+From iris.algebra Require Import frac auth.
+From iris_c.lib Require Import locking_heap mset flock U.
+From iris_c.c_translation Require Import proofmode translation derived.
+
+
+Section gcd.
+
+
+  Definition gcd : val := λ: "a" "b",
+     (a_while
+       (λ:<>, a_un_op NegOp
+                (a_bin_op EqOp (a_load (a_ret "a")) (a_load (a_ret "b"))))
+       (λ:<>, a_if (a_bin_op LtOp (a_load (a_ret "a")) (a_load (a_ret "b")))
+              (λ:<>, a_store (a_ret "b")
+               ((a_bin_op MinusOp (a_load (a_ret "b")) (a_load (a_ret "a")))))
+              (λ:<>, a_store (a_ret "a")
+               ((a_bin_op MinusOp (a_load (a_ret "a")) (a_load (a_ret "b")))))))
+       ;;;; a_load (a_ret "a").
+End gcd.
+
+
+Section gcd_spec.
+
+  Require Import Coq.ZArith.Znumtheory.
+
+  Context `{locking_heapG Σ, heapG Σ, flockG Σ, spawnG Σ}.
+
+
+  Lemma gcd_spec (a b : Z) (l r: loc) R:
+    ⌜a >= 0⌝ -∗ ⌜b >= 0⌝ -∗
+    l ↦U #a -∗ r ↦U #b -∗
+    awp (gcd #l #r) R (λ v, ⌜v = #(Z.gcd a b)⌝).
+  Proof.
+    iIntros "% % Hl Hr".
+    do 2 awp_lam. iApply a_sequence_spec.
+    iApply (a_while_inv_spec
+              (∃ (x y: Z),  l ↦U #x ∗ r ↦U #y ∧
+                            ⌜x >= 0 ∧ y >= 0 ∧ Zgcd x y = Zgcd a b⌝)%I
+              with "[Hl Hr]").
+    - eauto with iFrame.
+    - iModIntro. iIntros "H".  iDestruct "H" as (x y) "(Hl & Hr & % & % & %)".
+      iApply a_un_op_spec.
+      iApply (awp_bin_op_load_load with "[$Hl] [$Hr]"). iIntros "Hl Hr".
+      assert (Hxy: x = y ∨ x < y ∨ y < x) by lia.
+      destruct Hxy as [Hxy|[Hxy|Hxy]].
+      + iExists #true. simplify_eq /=. iSplit.
+        { rewrite/ bin_op_eval //=; case_bool_decide; eauto. }
+        iExists #false; iSplit; first done. iLeft; iSplit; first done.
+        do 2 iModIntro. awp_seq. awp_load_ret l #y. iIntros.
+        rewrite- H5. iPureIntro. symmetry. rewrite Z.gcd_diag.
+        rewrite Z.abs_eq; eauto with lia.
+      + iExists #false.  simplify_eq /=. iSplit.
+        { rewrite/ bin_op_eval //=.
+          case_bool_decide. inversion H6; subst. lia. eauto. }
+        iExists #true;  iSplit; first done. iRight; iSplit; first done.
+        iApply a_if_spec.
+        iApply (awp_bin_op_load_load with "[$Hl] [$Hr]"). iIntros "Hl Hr".
+        iExists #true; iSplit.
+        { rewrite/ bin_op_eval //=. case_bool_decide; eauto. }
+        iLeft. iSplit; first done. awp_seq.
+        iApply a_store_ret.
+        iApply (awp_bin_op_load_load with "[$Hr] [$Hl]"). iIntros "Hr Hl".
+        iExists #(y - x); iSplit; first by eauto with lia.
+        iExists #y. iFrame. iIntros "Hr". iModIntro.
+        iExists x, (y-x). iFrame. iPureIntro.
+        do 2 (split; first by lia). rewrite -H5; apply Z.gcd_sub_diag_r.
+      + iExists #false.  simplify_eq /=. iSplit.
+        { rewrite/ bin_op_eval //=.
+          case_bool_decide. inversion H6; subst. lia. eauto. }
+        iExists #true;  iSplit; first done. iRight; iSplit; first done.
+        iApply a_if_spec.
+        iApply (awp_bin_op_load_load with "[$Hl] [$Hr]"). iIntros "Hl Hr".
+        iExists #false. iSplit.
+        { rewrite/ bin_op_eval //=.
+          case_bool_decide. inversion H6; subst. lia. eauto. }
+        iRight; iSplit; first done. awp_seq.
+        iApply a_store_ret.
+        iApply (awp_bin_op_load_load with "[$Hl] [$Hr]"). iIntros "Hl Hr".
+        iExists #(x - y); iSplit; first by eauto with lia.
+        iExists #x. iFrame. iIntros "Hl". iModIntro.
+        iExists (x-y), y. iFrame. iPureIntro.
+        do 2 (split; first by lia).
+        rewrite -H5 Z.gcd_comm (Z.gcd_comm x); apply Z.gcd_sub_diag_r.
+  Qed.
+
+End gcd_spec.

theories/tests/test1.v

@@ -2,7 +2,7 @@ From iris.heap_lang Require Export proofmode notation.
 From iris.heap_lang Require Import spin_lock assert par.
 From iris.algebra Require Import frac auth.
 From iris_c.lib Require Import locking_heap mset flock U.
-From iris_c.c_translation Require Import proofmode translation.
+From iris_c.c_translation Require Import proofmode translation derived.
 
 Section test.
   Context `{locking_heapG Σ, heapG Σ, flockG Σ, spawnG Σ}.