refinement.v 14.3 KB
Newer Older
1 2 3
From iris.proofmode Require Import tactics.
From iris_logrel Require Import logrel.
From iris_logrel.examples.stack Require Import
Robbert Krebbers's avatar
Robbert Krebbers committed
4
  CG_stack FG_stack stack_rules.
5

6 7
Definition stackN : namespace := nroot .@ "stack".

8
Section Stack_refinement.
9
  Context `{logrelG Σ}.
Robbert Krebbers's avatar
Robbert Krebbers committed
10
  Notation D := (prodC valC valC -n> iProp Σ).
11
  Implicit Types Δ : listC D.
12
  Import lang.
Robbert Krebbers's avatar
Robbert Krebbers committed
13

14 15 16
  Program Definition R (τi : prodC valC valC -> iProp Σ) := λne ww, ( τi ww)%I.
  Next Obligation. solve_proper. Qed.

17 18 19 20
  Definition sinv' {SPG : authG Σ stackUR} γ τi stk stk' l' : iProp Σ :=
    ( (istk : loc) v h, (prestack_owns γ h)
         stk' ↦ₛ v
         stk ↦ᵢ (FoldV #istk)
21
         preStackLink γ (R τi) (#istk, v)
22 23 24
         l' ↦ₛ #false)%I.

  Context `{stackG Σ}.
Dan Frumin's avatar
Dan Frumin committed
25
  Definition sinv τi stk stk' l : iProp Σ :=
Robbert Krebbers's avatar
Robbert Krebbers committed
26
    ( (istk : loc) v h, (stack_owns h)
27
         stk' ↦ₛ v
Robbert Krebbers's avatar
Robbert Krebbers committed
28
         stk ↦ᵢ (FoldV #istk)
29
         StackLink (R τi) (#istk, v)
30 31 32 33
         l ↦ₛ #false)%I.
  Lemma sinv_unfold τi stk stk' l :
    sinv τi stk stk' l = sinv' stack_name τi stk stk' l.
  Proof. reflexivity. Qed.
34 35 36 37 38

  Ltac close_sinv Hcl asn :=
    iMod (Hcl with asn) as "_";
    [iNext; rewrite /sinv; iExists _,_,_; by iFrame |]; try iModIntro.

39
  Lemma FG_CG_push_refinement N st st' (τi : D) (v v' : val) l Γ :
Dan Frumin's avatar
Dan Frumin committed
40
    N ## logrelN 
41
    inv N (sinv τi st st' l) - (R τi) (v,v') -
Robbert Krebbers's avatar
Robbert Krebbers committed
42
    Γ  (FG_push $/ (LitV (Loc st))) v log (CG_locked_push $/ (LitV (Loc st')) $/ (LitV (Loc l))) v' : TUnit.
43
  Proof.
44
    iIntros (?) "#Hinv #Hvv'". iIntros (Δ).
45 46 47 48
    Transparent FG_push.
    unfold FG_push. unlock. simpl_subst/=.
    iLöb as "IH".
    rel_rec_l.
Dan Frumin's avatar
Dan Frumin committed
49
    rel_load_l_atomic.
50
    iInv N as (istk w h) "[Hoe [>Hst' [Hst [HLK >Hl]]]]" "Hclose".
Dan Frumin's avatar
Dan Frumin committed
51 52
    iExists (FoldV #istk). iFrame.
    iModIntro. iNext. iIntros "Hst".
53 54
    close_sinv "Hclose" "[Hst Hoe Hst' Hl HLK]". clear w h.
    rel_rec_l.
Dan Frumin's avatar
Dan Frumin committed
55 56
    rel_alloc_l as nstk "Hnstk". simpl.
    rel_cas_l_atomic.
57
    iInv N as (istk' w h) "[Hoe [>Hst' [Hst [HLK >Hl]]]]" "Hclose".
Dan Frumin's avatar
Dan Frumin committed
58 59
    iExists (FoldV #istk'). iFrame.
    iModIntro.
60
    destruct (decide (istk' = istk)) as [e | nestk]; subst.
Dan Frumin's avatar
Dan Frumin committed
61 62 63
    - (* CAS succeeds *)
      iSplitR; first by iIntros ([]).
      iIntros (?). iNext. iIntros "Hst".
64
      rel_apply_r (CG_push_r with "Hst' Hl").
65
      { solve_ndisj. }
66
      iIntros "Hst' Hl".
67 68 69 70
      iMod (stack_owns_alloc with "[$Hoe $Hnstk]") as "[Hoe Hnstk]".
      iMod ("Hclose" with "[Hst Hoe Hst' Hl HLK Hnstk]").
      { iNext. rewrite {2}/sinv. iExists _,_,_.
        iFrame "Hoe Hst' Hst Hl".
71
        rewrite (StackLink_unfold _ (# nstk, _)).
Dan Frumin's avatar
Dan Frumin committed
72
        iExists _, _. iSplitR; auto.
73 74
        iFrame "Hnstk".
        iRight. iExists _, _, _, _. auto. }
Dan Frumin's avatar
Dan Frumin committed
75
      rel_if_true_l.
76
      by rel_vals.
Dan Frumin's avatar
Dan Frumin committed
77 78 79
    - (* CAS fails *)
      iSplitL; last by (iIntros (?); congruence).
      iIntros (?); iNext; iIntros "Hst".
80 81 82 83
      close_sinv "Hclose" "[Hst Hoe Hst' Hl HLK]". clear w h.
      rel_if_false_l. simpl.
      rel_rec_l.
      by iApply "IH".
84 85
  Qed.

86
  Lemma FG_CG_pop_refinement' N st st' (τi : D) l Δ Γ :
Dan Frumin's avatar
Dan Frumin committed
87
    N ## logrelN 
88
    inv N (sinv τi st st' l) -
89
    {τi::Δ;Γ}  (FG_pop $/ LitV (Loc st)) #() log (CG_locked_pop $/ LitV (Loc st') $/ LitV (Loc l)) #() : TSum TUnit (TVar 0).
90
  Proof.
91
Transparent CG_locked_pop FG_pop CG_pop.
92
    iIntros (?) "#Hinv".
93
    iLöb as "IH".
94
    rewrite {2}/FG_pop. unlock.  simpl_subst/=.
95 96 97 98 99 100 101 102 103 104 105 106

replace ((rec: "pop" "st" <> :=
             let: "stv" := ! "st" in
             let: "x" := ! (Unfold "stv") in
             match: "x" with
               InjL <> => InjL #()
             | InjR "x" =>
               let: "y" := Fst "x" in let: "ys" := Snd "x" in if: CAS "st" "stv" "ys" then InjR "y" else ("pop" "st") #()
             end))%E with
(of_val FG_pop) by (by rewrite /FG_pop; unlock).

    rel_rec_l.
Dan Frumin's avatar
Dan Frumin committed
107
    rel_load_l_atomic.
108
    iInv N as (istk v h) "[Hoe [Hst' [Hst [#HLK Hl]]]]" "Hclose".
Dan Frumin's avatar
Dan Frumin committed
109 110 111 112
    iExists _. iFrame.
    iModIntro. iNext. iIntros "Hst /=".
    rel_rec_l.
    rel_unfold_l.
113 114 115
    iPoseProof "HLK" as "HLK'".

    rewrite {1}StackLink_unfold.
Dan Frumin's avatar
Dan Frumin committed
116 117 118
    iDestruct "HLK" as (istk2 w) "(% & Histk & HLK)". simplify_eq/=.
    iDestruct "HLK" as "[[% %] | HLK]"; simplify_eq/=.
    - (* The stack is empty *)
119
      rel_apply_r (CG_pop_fail_r with "Hst' Hl").
120
      { solve_ndisj. }
121
      iIntros "Hst' Hl".
Dan Frumin's avatar
Dan Frumin committed
122 123
      close_sinv "Hclose" "[Hoe Hst' Hst Hl HLK']". clear h. iClear "HLK'".
      rel_load_l_atomic.
124
      iInv N as (istk v h) "[Hoe [Hst' [Hst [#HLK Hl]]]]" "Hclose".
Dan Frumin's avatar
Dan Frumin committed
125 126 127 128
      iDestruct (stack_owns_later_open_close with "Hoe Histk") as "[Histk_i Hoe]".
      iExists _. iFrame "Histk_i".
      iModIntro. iNext. iIntros "Histk_i /=".
      iSpecialize ("Hoe" with "Histk_i").
129
      rel_rec_l.
Dan Frumin's avatar
Dan Frumin committed
130
      rel_case_l.
131
      rel_rec_l.
Dan Frumin's avatar
Dan Frumin committed
132 133 134 135

      close_sinv "Hclose" "[Hoe Hst' Hst Hl HLK]".
      rel_vals.
      { iModIntro. iLeft. iExists (_,_). eauto. }
136 137
    - (* The stack has a value *)
      iDestruct "HLK" as (y1 z1 y2 z2) "(% & % & Hτ & HLK_tail)"; simplify_eq/=.
Dan Frumin's avatar
Dan Frumin committed
138 139
      close_sinv "Hclose" "[Hoe Hst' Hst Hl HLK']". clear h.
      rel_load_l_atomic.
140
      iInv N as (istk v h) "[Hoe [Hst' [Hst [HLK Hl]]]]" "Hclose".
Dan Frumin's avatar
Dan Frumin committed
141 142 143 144
      iDestruct (stack_owns_later_open_close with "Hoe Histk") as "[Histk_i Hoe]".
      iExists _. iFrame.
      iModIntro. iNext. iIntros "Histk_i /=".
      iSpecialize ("Hoe" with "Histk_i").
145
      rel_rec_l.
Dan Frumin's avatar
Dan Frumin committed
146
      rel_case_l.
147
      rel_rec_l.
Dan Frumin's avatar
Dan Frumin committed
148 149 150
      do 2 (rel_proj_l; rel_rec_l).
      close_sinv "Hclose" "[Hoe Hst' Hst Hl HLK]". clear h istk v.
      rel_cas_l_atomic.
151
      iInv N as (istk v h) "[Hoe [Hst' [Hst [HLK2 Hl]]]]" "Hclose".
Dan Frumin's avatar
Dan Frumin committed
152 153 154 155 156 157 158 159 160 161 162 163 164
      iExists _. iFrame.
      iModIntro.
      destruct (decide (istk = istk2)) as [? |NE]; simplify_eq/=.
      + (* CAS succeeds *)
        iSplitR; first by (iIntros (?); contradiction).
        iIntros "%". iNext. iIntros "Hst".
        rel_if_l.
        rewrite (StackLink_unfold _ (#istk2, v)).
        iDestruct "HLK2" as (istk2' v') "[% [#Histk' HLK2]]"; simplify_eq/=.
        iDestruct (stack_mapstos_agree with "Histk Histk'") as "%"; simplify_eq/=.
        iDestruct "HLK2" as "[[% %]|HLK2]"; simplify_eq/=.
        iDestruct "HLK2" as (ym1 ym2 zm1 zm2)
                              "[% [% [#Hrel #HLK2_tail]]]"; simplify_eq/=.
165
        rel_apply_r (CG_pop_suc_r with "Hst' Hl").
166
        { solve_ndisj. }
167
        iIntros "Hst' Hl".
168 169 170 171
        iMod ("Hclose" with "[-]").
        { iNext. rewrite /sinv.
          rewrite (StackLink_unfold _ (ym2, z2)).
          iDestruct "HLK_tail" as (yn2loc ?) "[% _]"; simplify_eq /=.
Dan Frumin's avatar
Dan Frumin committed
172 173 174 175 176 177 178 179
          iExists _,_,_. by iFrame. }
        rel_vals.
        { iModIntro. iRight.
          iExists (_,_). eauto. }
      + (* CAS fails *)
        iSplitL; last by (iIntros (?); congruence).
        iIntros (?). iNext. iIntros "Hst".
        rel_if_l.
180
        close_sinv "Hclose" "[Hoe Hst Hst' Hl HLK2]".
181 182
        rel_rec_l.
        iApply "IH".
183
  Qed.
184

185
  Lemma FG_CG_pop_refinement st st' (τi : D) l Δ Γ :
186
    inv stackN (sinv τi st st' l) -
187
    {τi::Δ;Γ}  FG_pop $/ LitV (Loc st) log CG_locked_pop $/ LitV (Loc st') $/ LitV (Loc l) : TArrow TUnit (TSum TUnit (TVar 0)).
188 189 190 191 192 193 194 195
  Proof.
    iIntros "#Hinv".
    iApply bin_log_related_arrow_val; eauto.
    { unlock FG_pop CG_locked_pop. reflexivity. }
    { unlock FG_pop CG_locked_pop. reflexivity. }
    { unlock FG_pop CG_locked_pop. simpl_subst/=. solve_closed. }
    { unlock FG_pop CG_locked_pop. simpl_subst/=. solve_closed. }
    iAlways. iIntros (? ?) "[% %]". simplify_eq/=.
196 197
    iApply (FG_CG_pop_refinement' stackN); eauto.
    { solve_ndisj. }
198 199
  Qed.

200
  Lemma FG_CG_iter_refinement st st' (τi : D) l Δ Γ:
Dan Frumin's avatar
Dan Frumin committed
201
    inv stackN (sinv τi st st' l) -
202
    {τi::Δ;Γ}  FG_read_iter $/ LitV (Loc st) log CG_snap_iter $/ LitV (Loc st') $/ LitV (Loc l) : TArrow (TArrow (TVar 0) TUnit) TUnit.
203
  Proof.
Dan Frumin's avatar
Dan Frumin committed
204 205 206 207
    iIntros "#Hinv".
    Transparent FG_read_iter CG_snap_iter.
    unfold FG_read_iter, CG_snap_iter. unlock.
    simpl_subst/=.
208 209
    iApply bin_log_related_arrow_val; eauto.
    iAlways. iIntros (f1 f2) "#Hff /=".
Dan Frumin's avatar
Dan Frumin committed
210 211 212 213 214 215 216 217 218 219 220
    rel_rec_r.
    rel_rec_l.
    Transparent FG_iter CG_iter. unlock FG_iter CG_iter.
    rel_rec_l.
    rel_rec_r.
    Transparent CG_snap. unlock CG_snap.
    rel_rec_r.
    rel_rec_r.
    rel_rec_r.

    rel_load_l_atomic.
221
    iInv stackN as (istk v h) "[Hoe [Hst' [Hst [#HLK Hl]]]]" "Hclose".
Dan Frumin's avatar
Dan Frumin committed
222 223 224 225 226 227 228 229 230 231 232 233 234 235
    iExists _. iFrame.
    iModIntro. iNext. iIntros "Hst /=".

    rel_apply_r (bin_log_related_acquire_r with "Hl").
    { solve_ndisj. }
    iIntros "Hl /=".
    rel_rec_r.
    rel_load_r.
    rel_rec_r.
    rel_apply_r (bin_log_related_release_r with "Hl").
    { solve_ndisj. }
    iIntros "Hl /=".
    rel_rec_r.
    close_sinv "Hclose" "[Hoe Hst' Hst Hl HLK]". clear h.
236 237

    iLöb as "IH" forall (istk v) "HLK".
Dan Frumin's avatar
Dan Frumin committed
238 239 240 241 242 243 244 245 246 247 248 249
    rel_rec_l.
    rel_unfold_l.
    rel_rec_r.
    iPoseProof "HLK" as "HLK'".

    rewrite {1}StackLink_unfold.
    iDestruct "HLK" as (istk2 w) "(% & Histk & HLK)". simplify_eq/=.
    iDestruct "HLK" as "[[% %] | HLK]"; simplify_eq/=.
    - (* The stack is empty *)
      rel_fold_r.
      rel_case_r.
      rel_rec_r.
250

Dan Frumin's avatar
Dan Frumin committed
251
      rel_load_l_atomic.
Dan Frumin's avatar
Dan Frumin committed
252
      iInv stackN as (istk v h) "[Hoe [Hst' [Hst [#HLK Hl]]]]" "Hclose".
Dan Frumin's avatar
Dan Frumin committed
253 254 255 256 257 258
      iDestruct (stack_owns_later_open_close with "Hoe Histk") as "[Histk_i Hoe]".
      iExists _. iFrame "Histk_i".
      iModIntro. iNext. iIntros "Histk_i /=".
      iSpecialize ("Hoe" with "Histk_i").
      rel_case_l.
      rel_rec_l.
259

Dan Frumin's avatar
Dan Frumin committed
260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280
      close_sinv "Hclose" "[Hoe Hst' Hst Hl HLK]". iClear "HLK".
      by rel_vals.
    - (* The stack has a value *)
      iDestruct "HLK" as (y1 z1 y2 z2) "(% & % & Hτ & HLK_tail)"; simplify_eq/=.
      rel_fold_r.
      rel_case_r.
      rel_rec_r.
      rel_fst_r.

      rel_load_l_atomic.
      iInv stackN as (istk v h) "[Hoe [Hst' [Hst [#HLK Hl]]]]" "Hclose".
      iDestruct (stack_owns_later_open_close with "Hoe Histk") as "[Histk_i Hoe]".
      iExists _. iFrame "Histk_i".
      iModIntro. iNext. iIntros "Histk_i /=".
      iSpecialize ("Hoe" with "Histk_i").
      rel_case_l.
      rel_rec_l.
      rel_fst_l.
      rel_rec_l.
      rel_snd_l.
      rel_rec_l.
Dan Frumin's avatar
Dan Frumin committed
281
      close_sinv "Hclose" "[Hoe Hst' Hst Hl HLK]".
282
      simpl.
283
      iApply (bin_log_related_app _ _ _ _ _ _ TUnit with "[] [Hτ]"). (* TODO: abbreivate this as related_let *)
Dan Frumin's avatar
Dan Frumin committed
284
      + iApply bin_log_related_arrow; eauto.
285
        iAlways. iIntros (? ?) "?"; simplify_eq/=.
Dan Frumin's avatar
Dan Frumin committed
286 287 288 289 290 291 292 293 294 295
        rel_rec_l.
        rel_rec_l.
        rel_rec_r.
        rel_rec_r.
        rel_proj_r.
        iPoseProof "HLK_tail" as "HLK_tail.bak".
        rewrite {1}StackLink_unfold.
        iDestruct "HLK_tail" as (? ?) "[% [? HLK_tail]]"; simplify_eq/=.
        by iApply "IH".
      + clear.
296 297
        iClear "IH Histk HLK_tail HLK HLK'".
        iSpecialize ("Hff" $! (y1,y2) with "Hτ").
Dan Frumin's avatar
Dan Frumin committed
298
        iApply (related_ret with "[Hff]").
299
        done.
300
  Qed.
301

Dan Frumin's avatar
Dan Frumin committed
302 303 304 305 306
End Stack_refinement.

Section Full_refinement.
  Local Ltac replace_l c :=
    lazymatch goal with
307
    | [|- envs_entails _ (bin_log_related _ _ _ ?e _ _) ] =>
Dan Frumin's avatar
Dan Frumin committed
308 309 310 311
      replace e with c; last first
    end.
  Local Ltac replace_r c :=
    lazymatch goal with
312
    | [|- envs_entails _ (bin_log_related _ _ _ _ ?e' _) ] =>
Dan Frumin's avatar
Dan Frumin committed
313 314 315
      replace e' with c; last first
    end.

316
  (*  α. (α  Unit) * (Unit  Unit + α) * ((α  Unit)  Unit) *)
317
  Lemma FG_CG_stack_refinement `{SPG: stackPreG Σ, logrelG Σ} Δ Γ :
318
     {Δ;Γ}  FG_stack log CG_stack : TForall (TProd (TProd
319 320 321
           (TArrow (TVar 0) TUnit)
           (TArrow TUnit (TSum TUnit (TVar 0))))
           (TArrow (TArrow (TVar 0) TUnit) TUnit)).
322
  Proof.
Dan Frumin's avatar
Dan Frumin committed
323 324
    unfold FG_stack. unfold CG_stack.
    iApply bin_log_related_tlam; auto.
325
    iIntros (τi) "!#".
Dan Frumin's avatar
Dan Frumin committed
326 327 328 329 330
    rel_alloc_r as l "Hl".
    rel_rec_r.
    rel_alloc_r as st' "Hst'".
    unlock CG_stack_body.
    repeat rel_rec_r.
331 332
    (* TODO: i have to do a bind before allocation, otherwise it doesn't pick the correct reduct. *)
    rel_bind_l (ref (InjL #()))%E.
Dan Frumin's avatar
Dan Frumin committed
333 334 335 336 337
    rel_alloc_l as istk "Histk".
    simpl.
    rel_alloc_l as st "Hst".
    simpl.
    rel_rec_l.
338
    iMod (own_alloc ( ( : stackUR))) as (γ) "Hemp"; first done.
339 340
    set (istkG := StackG _ _ γ).
    change γ with (@stack_name _ istkG).
341 342
    change (@stack_pre_inG _ SPG) with (@stack_inG _ istkG).
    clearbody istkG. clear γ SPG.
343
    iAssert (@stack_owns _ istkG _ ) with "[Hemp]" as "Hoe".
344
    { rewrite /stack_owns /prestack_owns big_sepM_empty fmap_empty.
Dan Frumin's avatar
Dan Frumin committed
345 346
      iFrame "Hemp". }
    iMod (stack_owns_alloc with "[$Hoe $Histk]") as "[Hoe #Histk]".
347
    iAssert (StackLink (R τi) (#istk, FoldV (InjLV Unit))) with "[Histk]" as "#HLK".
348 349
    { rewrite StackLink_unfold.
      iExists _, _. iSplitR; simpl; trivial.
Dan Frumin's avatar
Dan Frumin committed
350 351 352 353 354 355 356 357 358 359 360 361
      iFrame "Histk". iLeft. iSplit; trivial. }
    iAssert (sinv τi st st' l) with "[Hoe Hst Hst' HLK Hl]" as "Hinv".
    { iExists _, _, _. by iFrame. }
    iMod (inv_alloc stackN with "[Hinv]") as "#Hinv".
    { iNext. iExact "Hinv". }
    unlock FG_stack_body.
    unlock FG_push.
    repeat rel_rec_l.
    unlock FG_pop.
    repeat rel_rec_l. simpl_subst/=.
    unlock FG_read_iter.
    repeat rel_rec_l.
362

Dan Frumin's avatar
Dan Frumin committed
363 364 365 366 367 368 369 370
    unlock CG_locked_push. simpl_subst/=.
    repeat rel_rec_r.
    unlock CG_locked_pop. simpl_subst/=.
    repeat rel_rec_r.
    unlock CG_snap_iter. simpl_subst/=.
    repeat rel_rec_r.

    repeat iApply bin_log_related_pair.
371 372
    - iApply bin_log_related_arrow_val; eauto.
      iAlways. iIntros (v1 v2) "#Hτ /=".
373
      replace_l ((FG_push $/ LitV (Loc st)) v1)%E.
Dan Frumin's avatar
Dan Frumin committed
374
      { unlock FG_push. simpl_subst/=. reflexivity. }
375
      replace_r ((CG_locked_push $/ LitV (Loc st') $/ LitV (Loc l)) v2)%E.
Dan Frumin's avatar
Dan Frumin committed
376 377
      { unlock CG_locked_push. simpl_subst/=. reflexivity. }
      iApply (FG_CG_push_refinement with "Hinv Hτ").
378
      { solve_ndisj. }
379
    - replace_l (FG_pop $/ LitV (Loc st))%E.
Dan Frumin's avatar
Dan Frumin committed
380
      { unlock FG_pop. by simpl_subst/=. }
381
      replace_r (CG_locked_pop $/ LitV (Loc st') $/ LitV (Loc l))%E.
Dan Frumin's avatar
Dan Frumin committed
382 383
      { unlock CG_locked_pop. by simpl_subst/=. }
      iApply (FG_CG_pop_refinement with "Hinv").
384
    - replace_l (FG_read_iter $/ LitV (Loc st))%E.
Dan Frumin's avatar
Dan Frumin committed
385
      { unlock FG_read_iter. by simpl_subst/=. }
386
      replace_r (CG_snap_iter $/ LitV (Loc st') $/ LitV (Loc l))%E.
Dan Frumin's avatar
Dan Frumin committed
387 388
      { unlock CG_snap_iter. by simpl_subst/=. }
      iApply (FG_CG_iter_refinement with "Hinv").
389
  Qed.
390

Dan Frumin's avatar
Dan Frumin committed
391 392 393 394 395 396 397 398 399 400 401
  Theorem stack_ctx_refinement :
      FG_stack ctx CG_stack :
      TForall (TProd (TProd (TArrow (TVar 0) TUnit)
                            (TArrow TUnit (TSum TUnit (TVar 0))))
                            (TArrow (TArrow (TVar 0) TUnit) TUnit)).
  Proof.
    set (Σ := #[logrelΣ; GFunctor (authR stackUR)]).
    eapply (logrel_ctxequiv Σ); [solve_closed.. | intros ].
    apply FG_CG_stack_refinement.
  Qed.
End Full_refinement.