spirea/src/examples/simple.v at main · logsem/spirea · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
From iris.proofmode Require Import tactics.
From iris.bi Require Import monpred.

From self.base Require Import primitive_laws.
From self.lang Require Import lang.
From self.high Require Import dprop.

From self.lang Require Import notation lang.
From self.algebra Require Import view.
From self.base Require Import primitive_laws class_instances adequacy.
From self.high Require Import proofmode wpc_proofmode.
From self.high Require Import dprop resources crash_weakestpre weakestpre
     weakestpre_na recovery_weakestpre lifted_modalities modalities
     post_crash_modality protocol no_buffer abstract_state_instances locations protocol
     adequacy.
From self.high.modalities Require Import fence.

Definition prog : expr := let: "l" := ref_NA #1 in !_NA "l".

Definition pure : expr :=
  let: "a" := #1 in
  let: "b" := #7 in
  "a" + "b".

Section specs.
  Context `{!nvmG Σ}.

  Lemma wp_bin_op : ⊢ WP (#1 + #2) {{ v, ⌜1 = 1⌝ }}.
  Proof.
    wp_pures.
    iModIntro.
    done.
  Qed.

  Lemma wp_with_let :
    {{{ True }}} pure {{{ RET (#8); True }}}.
  Proof.
    iIntros (Φ) "_ Post".
    rewrite /pure.
    wp_pures.
    iModIntro.
    iApply "Post".
    done.
  Qed.

  Lemma wpc_bin_op t E : ⊢ WPC (#1 + #2) @ t; E {{ v, ⌜1 = 1⌝ }}{{ True }}.
  Proof.
    iStartProof.
    (* wpc_pure_smart wp_pure_filter as H. *)
    (* wpc_pure_smart wp_pure_filter as H. *)
    wpc_pures.
    { auto. }
    auto.
  Qed.

  Lemma wpc_with_let t E :
    ⊢ WPC pure @ t; E {{ v, ⌜ v = #8 ⌝ }}{{ True }}.
  Proof.
    rewrite /pure.
    iStartProof.
    wpc_pures. { auto. }
    auto.
  Qed.

End specs.

Lemma wpr_pure `{!nvmG Σ} s E :
  ⊢ wpr s E pure pure (λ v, ⌜ v = #8 ⌝)%I (λ v, ⌜ v = #8 ⌝)%I.
Proof.
  iApply idempotence_wpr.
  2: { iApply wpc_with_let. }
  { apply _. }
  iModIntro. iModIntro.
  iIntros "H".
  iModIntro.
  iApply wpc_with_let.
Qed.

Lemma wpr_pure_safe :
  recv_adequate NotStuck (pure `at` ⊥) (pure `at` ⊥) (∅, ∅)
                (λ v _, v.(val_val) = #8) (λ v _, v.(val_val) = #8).
Proof.
  apply (high_recv_adequacy nvmΣ NotStuck pure pure ∅ ∅ (λ v, v = #8) (λ v, v = #8) 0).
  - done.
  - iIntros (??) "_". iApply wpr_pure.
Qed.

Definition program (ℓ : loc) : expr :=
  #ℓ <-_NA #1 ;;
  Flush #ℓ ;;
  FenceSync ;;
  #().

Section fence_sync.
  Context `{!nvmG Σ}.

  (* Predicate used for the location [a]. *)
  Definition prot : LocationProtocol nat :=
    {| p_inv := λ (n : nat) v, ⌜ v = #n ⌝%I;
       p_bumper n := n |}.

  Global Instance prot_cond : ProtocolConditions prot.
  Proof. split; try apply _. iIntros. by iApply post_crash_flush_pure. Qed.

  Lemma spec ℓ st E :
    {{{ ℓ ↦_{prot} [0] }}}
      program ℓ @ st; E
    {{{ RET #(); ℓ ↦_{prot} [1] }}}.
  Proof.
    iIntros (Φ) "pts Φpost".
    rewrite /program.
    wp_apply (wp_store_na with "[$pts]"); first done.
    { suff leq : (0 ≤ 1); first apply leq. lia. }
    { done. }
    iIntros "pts".
    wp_pures.
    wp_apply (wp_flush_na with "pts").
    iIntros "(pts & _ & lb) /=".
    wp_pures.
    wp_apply wp_fence_sync.
    iModIntro.
    simpl.
    wp_pures.
    iModIntro.
    iApply "Φpost".
    iApply (mapsto_na_persist_lb with "pts lb").
    cbn. lia.
  Qed.

End fence_sync.