clutch.elton.proofmode

From clutch.delay_prob_lang Require Import lang notation class_instances tactics.
From clutch.delay_prob_lang Require Export wp_tactics.
From clutch.elton Require Import weakestpre primitive_laws derived_laws.
From iris.prelude Require Import options.

#[global] Program Instance logic_wptactics_base `{!eltonGS Σ} : GwpTacticsBase Σ unit wp.
Next Obligation. intros. by apply pgl_wp_value. Qed.
Next Obligation. intros. by apply pgl_wp_fupd. Qed.

#[global] Program Instance logic_wptactics_bind `{!eltonGS Σ} : GwpTacticsBind Σ unit wp.
Next Obligation. intros. by apply pgl_wp_bind. Qed.

#[global] Program Instance logic_wptactics_pure `{!eltonGS Σ} : GwpTacticsPure Σ unit true wp.
Next Obligation. intros. by eapply lifting.wp_pure_step_later. Qed.

#[global] Program Instance logic_wptactics_heap `{!eltonGS Σ} : GwpTacticsHeap Σ unit true wp :=
  Build_GwpTacticsHeap _ _ _ _ (λ l q v, (l ↦{q} v)%I) (λ l q vs, (l ↦∗{q} vs)%I) _ _ _ _.
Next Obligation. intros. by apply wp_alloc. Qed.
Next Obligation. intros. by apply wp_allocN. Qed.
Next Obligation. intros. by apply wp_load. Qed.
Next Obligation. intros. by apply wp_store. Qed.

(* [global] Program Instance logic_wptactics_tape `{!eltonGS Σ} : GwpTacticsTapes Σ unit true wp := *)
(*   Build_GwpTacticsTapes _ _ _ _ (λ l q N ns, (l ↪N ( N ; ns ))*)
(* Next Obligation. intros. by apply wp_alloc_tape. Qed. *)
(* Next Obligation. intros. rewrite (bi.wand_curry (l↪N(N;ns))). by apply wp_rand_tape. Qed. *)

(* [global] Program Instance logic_wptactics_atomic_concurrency `{!eltonGS Σ} : GwpTacticsAtomicConcurrency Σ unit true wp := *)
(*   Build_GwpTacticsAtomicConcurrency _ _ _ _ (λ l q v, (l ↦{q} v)*)
(* Next Obligation. intros. by apply wp_cmpxchg_fail. Qed. *)
(* Next Obligation. intros. by apply wp_cmpxchg_suc. Qed.  *)
(* Next Obligation. intros. by apply wp_xchg. Qed. *)
(* Next Obligation. intros. by apply wp_faa. Qed.  *)

(* only needed for awp, so not useful since we do not have concurrency *)
#[global] Program Instance logic_wptactics_frame_wand `{!eltonGS Σ} : GwpTacticsFrameWand Σ unit true wp :=
  Build_GwpTacticsFrameWand _ _ _ _ _.
Next Obligation. iIntros (???????) "H1 H2". by iApply (pgl_wp_frame_wand with "[H1][$]"). Qed.


Section elton_test.
  Context `{!eltonGS Σ}.

  Local Lemma test_wp_tp_pures E l:
    {{{ l ↪ urn_unif ∅ }}} #3 + #3 @ E {{{ RET #6; l ↪ urn_unif ∅ }}}.
  Proof.
    iIntros (Ψ) "Hs HΦ".
    wp_pures.
    by iApply "HΦ".
  Qed.
End elton_test.