From 06cdb5ad16a91b6ee95330bdd2f53b818dec46d1 Mon Sep 17 00:00:00 2001
From: Simon Spies <simonspies@icloud.com>
Date: Mon, 16 Dec 2024 11:44:11 +0100
Subject: [PATCH] additional examples

---
 _CoqProject                              |   1 +
 theories/examples/refinements/examples.v | 256 +++++++++++++++++++++++
 2 files changed, 257 insertions(+)
 create mode 100644 theories/examples/refinements/examples.v

diff --git a/_CoqProject b/_CoqProject
index 9aae01c8..c1e67b7d 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -136,6 +136,7 @@ theories/examples/transfinite.v
 # derived Hoare triples
 theories/examples/refinements/derived.v
 theories/examples/termination/derived.v
+theories/examples/refinements/examples.v
 
 # key ideas
 theories/examples/keyideas/simulations.v
diff --git a/theories/examples/refinements/examples.v b/theories/examples/refinements/examples.v
new file mode 100644
index 00000000..700a04c2
--- /dev/null
+++ b/theories/examples/refinements/examples.v
@@ -0,0 +1,256 @@
+
+From iris.program_logic.refinement Require Export ref_weakestpre ref_source seq_weakestpre.
+From iris.base_logic.lib Require Export invariants na_invariants.
+From iris.examples.refinements Require Export refinement.
+From iris.proofmode Require Import tactics.
+From iris.heap_lang Require Import proofmode notation metatheory.
+Set Default Proof Using "Type".
+
+
+Section implementation.
+
+  (* first examples *)
+  Definition first (p: val) : val :=
+    rec: "first" "x" := if: p "x" then "x" else "first" ("x" + #1).
+
+  Definition f_ex : val :=
+    λ: "x", #41 ≤ "x" - #1.
+
+  Definition g_ex : val :=
+    λ: "x", #42 ≤ "x".
+
+
+  (* fib refinement *)
+  Definition fib_exp : val :=
+    rec: "fib" "n" := if: "n" ≤ #1 then "n" else "fib" ("n" - #1) + "fib" ("n" - #2).
+
+  Definition fibl : val :=
+    rec: "f" "n" := if: "n" = #0 then (#0, #1) else
+                    let: "r" := "f" ("n" - #1) in
+                    let: "x" := Fst "r" in
+                    let: "y" := Snd "r" in
+                    ("y", "x" + "y").
+
+  Definition fib_lin : val :=
+    λ: "x", Fst (fibl "x").
+
+End implementation.
+
+
+
+
+Definition seq_rswp {SI: indexT} `{Σ: gFunctors SI} `{!rheapG Σ} `{!auth_sourceG Σ (natA SI)} `{!seqG Σ} E e φ : iProp Σ := (na_own seqG_name E -∗ RSWP e at 0 ⟨⟨ v, na_own seqG_name E ∗ φ v ⟩⟩)%I.
+Notation "⟨⟨ P ⟩ ⟩ e ⟨⟨ v , Q ⟩ ⟩" := (□ (P -∗ (seq_rswp ⊤ e (λ v, Q))))%I
+(at level 20, P, e, Q at level 200, format "⟨⟨  P  ⟩ ⟩  e  ⟨⟨  v ,  Q  ⟩ ⟩") : stdpp_scope.
+Notation "{{ P } } e {{ v , Q } }" := (□ (P -∗ SEQ e ⟨⟨ v, Q ⟩⟩))%I
+(at level 20, P, e, Q at level 200, format "{{  P  } }  e  {{  v ,  Q  } }") : stdpp_scope.
+Notation "'|==>src' P" := (weak_src_update ⊤ P)%I (at level 99) : stdpp_scope.
+
+Definition ground_ref {SI: indexT} `{Σ: gFunctors SI} `{!rheapG Σ} `{Cred: !auth_sourceG Σ (natA SI)} `{!seqG Σ} (e1 e2: expr) (G: val → Prop) : iProp Σ :=
+  (∀ K, {{ src (fill K e2) }} e1 {{ v, src (fill K v) ∗ ⌜G v⌝ }})%I.
+
+
+Section first_proofs.
+  Context {SI: indexT} {A: Type} `{Σ: gFunctors SI} `{Heap: !rheapG Σ} `{Cred: !auth_sourceG Σ (natA SI)} `{Seq: !seqG Σ}.
+
+  Lemma first_spec (f g: val) (m: nat):
+    (∀ n: nat, ⊢ ground_ref (f #n) (g #n) (λ v, ∃ b: bool, v = #b)%type) →
+    (⊢ ground_ref (first f #m) (first g #m) (λ v, ∃ n: nat, v = #n)%type).
+  Proof.
+    intros Hfg. iStartProof. iRevert (m). iLöb as "IH".
+    iIntros (m K) "!# Hsrc Hna".
+    iApply (rwp_take_step with "[Hna]"); first done; last first.
+    { rewrite /first. src_pure _ in "Hsrc". fold (first g). iApply weak_src_update_return. iExact "Hsrc". }
+    iIntros "Hsrc". wp_rec. wp_bind (f _).
+    src_bind (g _) in "Hsrc".
+    iPoseProof (Hfg with "Hsrc Hna") as "Hfg".
+    iApply (rwp_wand with "Hfg"). iIntros (v) "[Hna [Hsrc H]]".
+    iDestruct "H" as (b) "->". destruct b.
+    - simpl. src_pure _ in "Hsrc". wp_pures. iFrame. iExists _. done.
+    - simpl. do 2 src_pure _ in "Hsrc". wp_pures.
+      replace (m + 1)%Z with (S m: Z) by lia.
+      iApply ("IH" with "Hsrc Hna").
+  Qed.
+
+  Lemma fg_ref (n: nat):
+    ⊢ ground_ref (f_ex #n) (g_ex #n) (λ v, ∃ b: bool, v = #b)%type.
+  Proof.
+    iIntros (K) "!# Hsrc Hna".
+    (* we step the source to allocate a credit *)
+    iApply (rwp_take_step with "[Hna] [Hsrc]"); first done; last first.
+    { iApply (step_pure_cred 1%nat with "Hsrc").
+      apply pure_step_ctx; first apply _.
+      eapply nsteps_once_inv. rewrite /g_ex. by apply: pure_exec. }
+    simpl. iIntros "[Hsrc Hcred]".
+    rewrite /f_ex. wp_pure _.
+    (* we stutter one source step by spending the credit *)
+    iApply (rwp_take_step with "[Hna Hsrc] [Hcred]"); first done; last first.
+    { iApply step_stutter. iFrame. }
+    iIntros "_". wp_pure _.
+    (* we can now execute both in lock step *)
+    iApply (rwp_take_step with "[Hna] [Hsrc]"); first done; last first.
+    { src_pure _ in "Hsrc". iApply weak_src_update_return. iExact "Hsrc". }
+    iIntros "Hsrc". wp_pure _.
+    (* we prove the postcondition *)
+    iFrame. rewrite !bool_decide_decide. destruct decide, decide; try lia.
+    - iFrame. iPureIntro. by eexists _.
+    - iFrame. iPureIntro. by eexists _.
+  Qed.
+
+  Corollary first_ref (m: nat):
+    ⊢ ground_ref (first f_ex #m) (first g_ex #m) (λ v, ∃ n: nat, v = #n)%type.
+  Proof. apply first_spec, fg_ref. Qed.
+
+End first_proofs.
+
+
+Section fib_stuttering_proof.
+  Context {SI: indexT} {A: Type} `{Σ: gFunctors SI} `{Heap: !rheapG Σ} `{Cred: !auth_sourceG Σ (natA SI)} `{Seq: !seqG Σ}.
+
+  Fixpoint fib_spec (n: nat) : nat :=
+    match n with
+    | O => O
+    | S n =>
+    match n with
+    | O => S O
+    | S n' => fib_spec n + fib_spec n'
+    end
+    end.
+
+  Lemma fib_spec_eq n : (fib_spec (S (S n)): Z) = (fib_spec (S n) + fib_spec n)%Z.
+  Proof.
+    rewrite -Nat2Z.inj_add //.
+  Qed.
+
+  Lemma fib_exp_wp (n: nat) :
+    ⊢ RWP fib_exp #n ⟨⟨ v, ⌜v = #(fib_spec n)⌝ ⟩⟩.
+  Proof.
+    induction (lt_wf n) as [n _ IH].
+    destruct n as [|[|n]].
+    - wp_rec. wp_pures. iPureIntro. done.
+    - wp_rec. wp_pures. iPureIntro. done.
+    - wp_rec. wp_pures. rewrite bool_decide_decide.
+      destruct decide; first lia. wp_pures.
+      wp_bind (fib_exp _). replace (S (S n) - 2)%Z with (n: Z) by lia.
+      iApply rwp_wand; first by iApply IH; lia.
+      iIntros (v) "->". wp_bind (fib_exp _). wp_pures.
+      replace (S (S n) - 1)%Z with (S n: Z) by lia.
+      iApply rwp_wand; first by iApply IH; lia.
+      iIntros (v') "->". wp_pures. iPureIntro.
+      rewrite fib_spec_eq //.
+  Qed.
+
+  Lemma fibl_wp (n: nat) :
+    ⊢ RWP fibl #n ⟨⟨ v, ⌜v = (#(fib_spec n), #(fib_spec (S n)))%V⌝ ⟩⟩.
+  Proof.
+    induction n as [|n IH]; first simpl.
+    - wp_rec. wp_op; first by left. wp_pures. iPureIntro. done.
+    - wp_rec. wp_op; first by left. wp_pures. wp_bind (fibl _).
+      replace (S n - 1)%Z with (n: Z) by lia.
+      iApply rwp_wand; first iApply IH.
+      iIntros (v) "->". wp_pures. iPureIntro. f_equal.
+      rewrite fib_spec_eq Z.add_comm //.
+  Qed.
+
+  Lemma fib_lin_wp (n: nat) :
+    ⊢ RWP fib_lin #n ⟨⟨ v, ⌜v = #(fib_spec n)⌝ ⟩⟩.
+  Proof.
+    wp_lam. wp_bind (fibl _).
+    iApply rwp_wand; first iApply (fibl_wp n).
+    iIntros (v) "->". wp_pures. done.
+  Qed.
+
+  Definition eval (e: expr) (v: val) : iProp Σ :=
+    (∀ K, src (fill K e) -∗ weak_src_update ⊤ (src (fill K v)))%I.
+
+  Lemma fib_exp_upd (n: nat) : eval (fib_exp #n) #(fib_spec n).
+  Proof.
+    induction (lt_wf n) as [n _ IH].
+    destruct n as [|[|n]].
+    - iIntros (K) "Hsrc". rewrite /fib_exp.
+      src_pure _ in "Hsrc". fold fib_exp.
+      repeat src_pure _ in "Hsrc".
+      iApply weak_src_update_return. done.
+    - iIntros (K) "Hsrc". rewrite /fib_exp.
+      src_pure _ in "Hsrc". fold fib_exp.
+      repeat src_pure _ in "Hsrc".
+      iApply weak_src_update_return. done.
+    - iIntros (K) "Hsrc". rewrite /fib_exp.
+      src_pure _ in "Hsrc". fold fib_exp.
+      repeat src_pure _ in "Hsrc".
+      rewrite bool_decide_decide.
+      destruct decide; first lia.
+      repeat src_pure _ in "Hsrc".
+      src_bind (fib_exp _) in "Hsrc".
+      replace (S (S n) - 2)%Z with (n: Z) by lia.
+      iPoseProof (IH with "Hsrc") as "H1"; first lia.
+      iApply weak_src_update_bind; iFrame.
+      Local Arguments fib_spec : simpl never.
+      simpl. iIntros "Hsrc".
+      repeat src_pure _ in "Hsrc".
+      replace (S (S n) - 1)%Z with (S n: Z) by lia.
+      src_bind (fib_exp _) in "Hsrc".
+      iPoseProof (IH with "Hsrc") as "H2"; first lia.
+      iApply weak_src_update_bind; iFrame.
+      iIntros "Hsrc". simpl.
+      repeat src_pure _ in "Hsrc".
+      iApply weak_src_update_return.
+      rewrite fib_spec_eq //.
+  Qed.
+
+  Lemma fibl_upd (n: nat) : eval (fibl #n) (#(fib_spec n), #(fib_spec (S n))).
+  Proof.
+    induction n as [|n IH].
+    - iIntros (K) "Hsrc". rewrite /fibl.
+      src_pure _ in "Hsrc". fold fibl.
+      repeat src_pure _ in "Hsrc".
+      iApply weak_src_update_return. done.
+    - iIntros (K) "Hsrc". rewrite /fibl.
+      src_pure _ in "Hsrc". fold fibl.
+      repeat src_pure _ in "Hsrc".
+      src_bind (fibl _) in "Hsrc".
+      replace (S n - 1)%Z with (n: Z) by lia.
+      iPoseProof (IH with "Hsrc") as "H".
+      iApply weak_src_update_bind; iFrame.
+      iIntros "Hsrc". simpl.
+      repeat src_pure _ in "Hsrc".
+      iApply weak_src_update_return.
+      f_equal. rewrite fib_spec_eq Z.add_comm //.
+  Qed.
+
+  Lemma fib_lin_upd (n: nat) : eval (fib_lin #n) #(fib_spec n).
+  Proof.
+    iIntros (K) "Hsrc". rewrite /fib_lin.
+    src_pure _ in "Hsrc". fold fib_lin.
+    src_bind (fibl _) in "Hsrc".
+    iPoseProof (fibl_upd with "Hsrc") as "H".
+    iApply weak_src_update_bind; iFrame.
+    iIntros "Hsrc". simpl.
+    src_pure _ in "Hsrc".
+    iApply weak_src_update_return. done.
+  Qed.
+
+
+  Lemma fib_exp_lin_ref (n: nat) :
+    ⊢ ground_ref (fib_exp #n) (fib_lin #n) (λ v, ∃ n: nat, v = #n)%type.
+  Proof.
+    iIntros (K) "!# Hsrc Hna".
+    iApply (rwp_weaken' with "[Hna]"); first done; last first.
+    { iApply fib_lin_upd. done. }
+    iIntros "Hsrc".
+    iApply (rwp_wand); first iApply fib_exp_wp.
+    iIntros (v) "->". iFrame. iExists _. done.
+  Qed.
+
+  Lemma fib_exp_ref (n: nat) :
+    ⊢ ground_ref (fib_lin #n) (fib_exp #n) (λ v, ∃ n: nat, v = #n)%type.
+  Proof.
+    iIntros (K) "!# Hsrc Hna".
+    iApply (rwp_weaken' with "[Hna]"); first done; last first.
+    { iApply fib_exp_upd. done. }
+    iIntros "Hsrc".
+    iApply (rwp_wand); first iApply fib_lin_wp.
+    iIntros (v) "->". iFrame. iExists _. done.
+  Qed.
+
+End fib_stuttering_proof.
\ No newline at end of file
-- 
GitLab