encodable.v 5.8 KB
Newer Older
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
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
From iris.proofmode Require Import tactics.
From iris.program_logic Require Export weakestpre.
From iris.heap_lang Require Import proofmode notation.
From osiris Require Import typing channel logrel.
From iris.algebra Require Import list auth excl.
From iris.base_logic Require Import invariants.

Class Encodable A := encode : A -> val.
Instance val_encodable : Encodable val := id.
Instance int_encodable : Encodable Z := λ n, #n.
Instance bool_encodable : Encodable bool := λ b, #b.
Instance unit_encodable : Encodable unit := λ _, #().
Instance loc_encodable : Encodable loc := λ l, #l.

Class Decodable A := decode : val -> option A.
Instance val_decodable : Decodable val := id $ Some.
Instance int_decodable : Decodable Z :=
  λ v, match v with
       | LitV (LitInt z) => Some z
       | _ => None
       end.
Instance bool_decodable : Decodable bool :=
  λ v, match v with
       | LitV (LitBool b) => Some b
       | _ => None
       end.
Instance loc_decodable : Decodable loc :=
  λ v, match v with
       | LitV (LitLoc l) => Some l
       | _ => None
       end.

Class EncDec (A : Type) {EA : Encodable A} {DA : Decodable A} :=
{
  encdec :  v, decode (encode v) = Some v;
  decenc :  (v : val) (w : A) , decode v = Some w -> encode w = v
}.

Ltac solve_encdec := intros v; by unfold decode, encode.
Ltac solve_decenc :=
  intros v w H;
  destruct v as [l | | | | ]; try by inversion H;
  destruct l; try by inversion H.

Ltac solve_encdec_decenc :=
  split; [solve_encdec | solve_decenc].

Instance val_encdec : EncDec val.
Proof.
  split.
  - intros v. unfold decode, encode. eauto.
  - intros v w H. by destruct v; inversion H.
Qed.
Instance int_encdec : EncDec Z.
Proof. solve_encdec_decenc. Qed.
Instance bool_encdec : EncDec bool.
Proof. solve_encdec_decenc. Qed.
Instance loc_encdec : EncDec loc.
Proof. solve_encdec_decenc. Qed.

Lemma enc_dec {A : Type} `{ED : EncDec A}
      v (w : A) : encode w = v <-> decode v = Some w.
Proof.
  split.
  - intros.
    rewrite -encdec.
    rewrite -H.
    reflexivity.
  - intros.
    apply decenc. eauto.
Qed.

Inductive stype' (A : Type) :=
| TEnd'
| TSR' {V : Type} {EV : Encodable V} {DV : Decodable V}
       (a : action) (P : V  A) (st : V  stype' A).
Arguments TEnd' {_}.
Arguments TSR' {_ _ _ _} _ _ _.
Instance: Params (@TSR') 4.

Fixpoint dual_stype' {A} (st : stype' A) :=
  match st with
  | TEnd' => TEnd'
  | TSR' a P st => TSR' (dual_action a) P (λ v, dual_stype' (st v))
  end.
Instance: Params (@dual_stype') 2.
Arguments dual_stype : simpl never.

Section Encodings.
  Context `{!heapG Σ} (N : namespace).
  Context `{!logrelG val Σ}.

  Example ex_st : stype' (iProp Σ) :=
    (TSR' Receive
          (λ v', v' = 5%I)
          (λ v', TEnd')).
  
  Example ex_st2 : stype' (iProp Σ) :=
    TSR' Send
         (λ b, b = true%I)
         (λ b,
          (TSR' Receive
              (λ v', (v' > 5) = b%I)
              (λ _, TEnd'))).

  Fixpoint stype'_to_stype (st : stype' (iProp Σ)) : stype val (iProp Σ) :=
    match st with
    | TEnd' => TEnd
    | TSR' a P st => TSR a
                         (λ v, match decode v with
                               | Some v => P v
                               | None => False
                               end%I)
                         (λ v, match decode v with
                               | Some v => stype'_to_stype (st v)
                               | None => TEnd
                               end)
    end.
  Global Instance: Params (@stype'_to_stype) 1.
  Global Arguments stype'_to_stype : simpl never.

  Lemma dual_stype'_comm st :
    dual_stype (stype'_to_stype st)  stype'_to_stype (dual_stype' st).
  Proof. 
    induction st.
    - by simpl.
    - unfold stype'_to_stype. simpl.
      constructor.
      + intros v. eauto.
      + intros v. destruct (decode v); eauto.
  Qed.

  Lemma dual_stype'_comm_eq st :
    dual_stype (stype'_to_stype st) = stype'_to_stype (dual_stype' st).
  Proof. Admitted.

  Notation "⟦ c @ s : sτ ⟧{ γ }" := (interp_st N γ sτ c s)
    (at level 10, s at next level, sτ at next level, γ at next level,
     format "⟦  c  @  s  :  sτ  ⟧{ γ }").

  Lemma new_chan_st_enc_spec st :
    {{{ True }}}
      new_chan #()
    {{{ c γ, RET c;   c @ Left : (stype'_to_stype st) {γ} 
                      c @ Right : (stype'_to_stype (dual_stype' st)) {γ} }}}.
  Proof.
    iIntros (Φ _) "HΦ".
    iApply (new_chan_st_spec). eauto.
    iNext.
    iIntros (c γ) "[Hl Hr]".
    iApply "HΦ".
    iFrame. 
    rewrite dual_stype'_comm_eq.    
    iFrame.
  Qed.

  Lemma send_st_enc_spec (A : Type) `{Encodable A} `{Decodable A} `{EncDec A}
        st γ c s (P : A  iProp Σ) v w :
    decode v = Some w 
    {{{ P w   c @ s : (stype'_to_stype (TSR' Send P st)) {γ} }}}
      send c #s v
    {{{ RET #();  c @ s : stype'_to_stype (st w) {γ} }}}.
  Proof.
    intros Henc.
    iIntros (Φ) "[HP Hsend] HΦ".
    iApply (send_st_spec with "[HP Hsend]").
    simpl.
    iFrame.
    by destruct (decode v); inversion Henc.
    iNext.
    destruct (decode v); inversion Henc.
    by iApply "HΦ".
  Qed.
    
  Lemma recv_st_enc_spec (A : Type) `{EncDec A}
        st γ c s (P : A  iProp Σ) :
    {{{  c @ s : (stype'_to_stype (TSR' Receive P st)) {γ} }}}
      recv c #s
    {{{ v w, RET v;  c @ s : stype'_to_stype (st w) {γ}  P w 
        encode w = v }}}.
  Proof.
    iIntros (Φ) "Hrecv HΦ".
    iApply (recv_st_spec with "Hrecv").
    iNext. iIntros (v). iSpecialize ("HΦ" $!v).
    iIntros "[H HP]".
    iAssert (( w, decode v = Some w  P w)%I) with "[HP]" as (w Hw) "HP".
    destruct (decode v). iExists a. by iFrame. iDestruct "HP" as %HP=>//.
    assert (encode w = v). by apply decenc.
    destruct (decode v); inversion Hw.
    iApply "HΦ".
    iFrame.
    iPureIntro. eauto.
  Qed.

End Encodings.