Library zoo_persistent.suf
Require Import zoo.prelude.
Require Import zoo.common.fin_maps.
Require Import zoo.base.
Require Export zoo_persistent.suf__code.
Require Import zoo_persistent.suf__types.
Require Import zoo.options.
Implicit Type rank : Z.
Implicit Type elt repr parent : location.
Implicit Type t s descr : val.
Implicit Type reprs : gmap location location.
Implicit Type descrs : gmap location val.
Class SufG Σ `{zoo۰G : !ZooG Σ} :=
{ #[local] suf۰G۰sstore۰G :: Sstore2G Σ
}.
Definition suf۰Σ :=
#[sstore_2۰Σ
].
#[global] Instance subGｰsuf۰Σ Σ `{zoo۰G : !ZooG Σ} :
subG suf۰Σ Σ →
SufG Σ.
Section unify.
#[local] Definition unify_at repr1 repr2 repr :=
if decide (repr = repr1) then
repr2
else
repr.
#[local] Lemma unify_at₁ repr1 repr2 :
unify_at repr1 repr2 repr1 = repr2.
#[local] Lemma unify_at₂ repr1 repr2 repr :
repr ≠ repr1 →
unify_at repr1 repr2 repr = repr.
#[local] Definition unify repr1 repr2 reprs :=
unify_at repr1 repr2 <$> reprs.
#[local] Lemma unifyｰlookup₁ reprs repr1 repr2 elt :
reprs !! elt = Some repr1 →
unify repr1 repr2 reprs !! elt = Some repr2.
#[local] Lemma unifyｰlookup₂ {reprs repr1 repr2 elt} repr :
reprs !! elt = Some repr →
repr ≠ repr1 →
unify repr1 repr2 reprs !! elt = Some repr.
#[local] Lemma unifyｰlookup₂' reprs repr1 repr2 :
reprs !! repr2 = Some repr2 →
repr1 ≠ repr2 →
unify repr1 repr2 reprs !! repr2 = Some repr2.
#[local] Lemma domｰunify repr1 repr2 reprs :
dom (unify repr1 repr2 reprs) = dom reprs.
End unify.
Opaque unify_at.
Opaque unify.
Section consistent.
#[local] Definition consistent_at reprs elt repr descr :=
( ∃ rank,
repr = elt ∧
descr = ‘Root( #rank )%V
) ∨ (
∃ parent,
elt ≠ repr ∧
descr = ‘Link( #parent )%V ∧
reprs !! parent = Some repr ∧
reprs !! repr = Some repr
).
#[local] Definition consistent reprs descrs :=
map_Forall2 (consistent_at reprs) reprs descrs.
#[local] Lemma consistentｰempty :
consistent ∅ ∅.
#[local] Lemma consistentｰlookupｰNone {reprs descrs} elt :
consistent reprs descrs →
descrs !! elt = None →
reprs !! elt = None.
#[local] Lemma consistentｰlookupｰSome {reprs descrs} elt repr :
consistent reprs descrs →
reprs !! elt = Some repr →
∃ descr,
descrs !! elt = Some descr ∧
consistent_at reprs elt repr descr.
#[local] Lemma consistentｰinsert {reprs descrs} elt :
descrs !! elt = None →
consistent reprs descrs →
consistent
(<[elt := elt]> reprs)
(<[elt := ‘Root( 0 )%V]> descrs).
#[local] Lemma consistentｰlinkｰrepr {reprs descrs} elt repr :
elt ≠ repr →
reprs !! elt = Some repr →
reprs !! repr = Some repr →
consistent reprs descrs →
consistent
reprs
(<[elt := ‘Link( #repr )%V]> descrs).
#[local] Lemma consistentｰlinkｰunion {reprs descrs} repr1 repr2 :
repr1 ≠ repr2 →
reprs !! repr1 = Some repr1 →
reprs !! repr2 = Some repr2 →
consistent reprs descrs →
consistent
(unify repr1 repr2 reprs)
(<[repr1 := ‘Link( #repr2 )%V]> descrs).
#[local] Lemma consistentｰupdateｰrank {reprs descrs} repr rank :
reprs !! repr = Some repr →
consistent reprs descrs →
consistent
reprs
(<[repr := ‘Root( #rank )%V]> descrs).
End consistent.
Opaque consistent_at.
Opaque consistent.
Section suf۰G.
Context `{suf۰G : SufG Σ}.
Definition suf۰model t reprs : iProp Σ :=
∃ descrs,
sstore_2۰model t descrs ∗
⌜consistent reprs descrs⌝.
#[local] Instance : CustomIpat "model" :=
" ( %descrs{} & Hmodel{} & %Hconsistent{} ) ".
Definition suf۰snapshot s t reprs : iProp Σ :=
∃ descrs,
sstore_2۰snapshot s t descrs ∗
⌜consistent reprs descrs⌝.
#[local] Instance : CustomIpat "snapshot" :=
" ( %descrs{} & Hsnapshot{} & %Hconsistent{} ) ".
#[global] Instance suf۰modelｰtimeless t reprs :
Timeless (suf۰model t reprs).
#[global] Instance suf۰snapshotｰpersistent s t reprs :
Persistent (suf۰snapshot s t reprs).
Lemma suf۰modelｰvalid {t reprs} elt repr :
reprs !! elt = Some repr →
suf۰model t reprs ⊢
⌜reprs !! repr = Some repr⌝.
Lemma suf۰modelｰexclusive t reprs1 reprs2 :
suf۰model t reprs1 -∗
suf۰model t reprs2 -∗
False.
Lemma suf٠createｰspec :
{{{
True
}}}
suf٠create ()
{{{
t
, RET t;
suf۰model t ∅
}}}.
Lemma suf٠makeｰspec t reprs :
{{{
suf۰model t reprs
}}}
suf٠make t
{{{
elt
, RET #elt;
suf۰model t (<[elt := elt]> reprs)
}}}.
Lemma suf٠reprｰspec {t reprs elt} repr :
reprs !! elt = Some repr →
{{{
suf۰model t reprs
}}}
suf٠repr t #elt
{{{
RET #repr;
suf۰model t reprs
}}}.
Lemma suf٠equivｰspec {t reprs elt1} repr1 {elt2} repr2 :
reprs !! elt1 = Some repr1 →
reprs !! elt2 = Some repr2 →
{{{
suf۰model t reprs
}}}
suf٠equiv t #elt1 #elt2
{{{
RET #(bool_decide (repr1 = repr2));
suf۰model t reprs
}}}.
#[local] Lemma suf٠rankｰspec t reprs elt :
reprs !! elt = Some elt →
{{{
suf۰model t reprs
}}}
suf٠rank t #elt
{{{
rank
, RET #rank;
suf۰model t reprs
}}}.
Definition suf۰union_condition reprs repr1 repr2 reprs' :=
dom reprs = dom reprs' ∧
( ∀ elt repr,
reprs !! elt = Some repr →
repr ≠ repr1 →
repr ≠ repr2 →
reprs' !! elt = Some repr
) ∧
( ∃ repr12,
(repr12 = repr1 ∨ repr12 = repr2) ∧
∀ elt repr,
reprs !! elt = Some repr →
repr = repr1 ∨ repr = repr2 →
reprs' !! elt = Some repr12
).
#[local] Lemma suf۰union_conditionｰrefl reprs repr :
suf۰union_condition reprs repr repr reprs.
#[local] Lemma suf۰union_conditionｰsym reprs repr1 repr2 reprs' :
suf۰union_condition reprs repr1 repr2 reprs' →
suf۰union_condition reprs repr2 repr1 reprs'.
#[local] Lemma unifyｰunion_condition₁ reprs repr1 repr2 :
repr1 ≠ repr2 →
suf۰union_condition reprs repr1 repr2 (unify repr1 repr2 reprs).
#[local] Lemma unifyｰunion_condition₂ reprs repr1 repr2 :
repr1 ≠ repr2 →
suf۰union_condition reprs repr2 repr1 (unify repr1 repr2 reprs).
#[local] Opaque suf۰union_condition.
Lemma suf٠unionｰspec {t reprs elt1} repr1 {elt2} repr2 :
reprs !! elt1 = Some repr1 →
reprs !! elt2 = Some repr2 →
{{{
suf۰model t reprs
}}}
suf٠union t #elt1 #elt2
{{{
reprs'
, RET ();
suf۰model t reprs' ∗
⌜suf۰union_condition reprs repr1 repr2 reprs'⌝
}}}.
Lemma suf٠captureｰspec t reprs :
{{{
suf۰model t reprs
}}}
suf٠capture t
{{{
s
, RET s;
suf۰model t reprs ∗
suf۰snapshot s t reprs
}}}.
Lemma suf٠restoreｰspec t reprs s reprs' :
{{{
suf۰model t reprs ∗
suf۰snapshot s t reprs'
}}}
suf٠restore t s
{{{
RET ();
suf۰model t reprs'
}}}.
End suf۰G.
Require zoo_persistent.suf__opaque.
#[global] Opaque suf۰model.
#[global] Opaque suf۰snapshot.
Require Import zoo.common.fin_maps.
Require Import zoo.base.
Require Export zoo_persistent.suf__code.
Require Import zoo_persistent.suf__types.
Require Import zoo.options.
Implicit Type rank : Z.
Implicit Type elt repr parent : location.
Implicit Type t s descr : val.
Implicit Type reprs : gmap location location.
Implicit Type descrs : gmap location val.
Class SufG Σ `{zoo۰G : !ZooG Σ} :=
{ #[local] suf۰G۰sstore۰G :: Sstore2G Σ
}.
Definition suf۰Σ :=
#[sstore_2۰Σ
].
#[global] Instance subGｰsuf۰Σ Σ `{zoo۰G : !ZooG Σ} :
subG suf۰Σ Σ →
SufG Σ.
Section unify.
#[local] Definition unify_at repr1 repr2 repr :=
if decide (repr = repr1) then
repr2
else
repr.
#[local] Lemma unify_at₁ repr1 repr2 :
unify_at repr1 repr2 repr1 = repr2.
#[local] Lemma unify_at₂ repr1 repr2 repr :
repr ≠ repr1 →
unify_at repr1 repr2 repr = repr.
#[local] Definition unify repr1 repr2 reprs :=
unify_at repr1 repr2 <$> reprs.
#[local] Lemma unifyｰlookup₁ reprs repr1 repr2 elt :
reprs !! elt = Some repr1 →
unify repr1 repr2 reprs !! elt = Some repr2.
#[local] Lemma unifyｰlookup₂ {reprs repr1 repr2 elt} repr :
reprs !! elt = Some repr →
repr ≠ repr1 →
unify repr1 repr2 reprs !! elt = Some repr.
#[local] Lemma unifyｰlookup₂' reprs repr1 repr2 :
reprs !! repr2 = Some repr2 →
repr1 ≠ repr2 →
unify repr1 repr2 reprs !! repr2 = Some repr2.
#[local] Lemma domｰunify repr1 repr2 reprs :
dom (unify repr1 repr2 reprs) = dom reprs.
End unify.
Opaque unify_at.
Opaque unify.
Section consistent.
#[local] Definition consistent_at reprs elt repr descr :=
( ∃ rank,
repr = elt ∧
descr = ‘Root( #rank )%V
) ∨ (
∃ parent,
elt ≠ repr ∧
descr = ‘Link( #parent )%V ∧
reprs !! parent = Some repr ∧
reprs !! repr = Some repr
).
#[local] Definition consistent reprs descrs :=
map_Forall2 (consistent_at reprs) reprs descrs.
#[local] Lemma consistentｰempty :
consistent ∅ ∅.
#[local] Lemma consistentｰlookupｰNone {reprs descrs} elt :
consistent reprs descrs →
descrs !! elt = None →
reprs !! elt = None.
#[local] Lemma consistentｰlookupｰSome {reprs descrs} elt repr :
consistent reprs descrs →
reprs !! elt = Some repr →
∃ descr,
descrs !! elt = Some descr ∧
consistent_at reprs elt repr descr.
#[local] Lemma consistentｰinsert {reprs descrs} elt :
descrs !! elt = None →
consistent reprs descrs →
consistent
(<[elt := elt]> reprs)
(<[elt := ‘Root( 0 )%V]> descrs).
#[local] Lemma consistentｰlinkｰrepr {reprs descrs} elt repr :
elt ≠ repr →
reprs !! elt = Some repr →
reprs !! repr = Some repr →
consistent reprs descrs →
consistent
reprs
(<[elt := ‘Link( #repr )%V]> descrs).
#[local] Lemma consistentｰlinkｰunion {reprs descrs} repr1 repr2 :
repr1 ≠ repr2 →
reprs !! repr1 = Some repr1 →
reprs !! repr2 = Some repr2 →
consistent reprs descrs →
consistent
(unify repr1 repr2 reprs)
(<[repr1 := ‘Link( #repr2 )%V]> descrs).
#[local] Lemma consistentｰupdateｰrank {reprs descrs} repr rank :
reprs !! repr = Some repr →
consistent reprs descrs →
consistent
reprs
(<[repr := ‘Root( #rank )%V]> descrs).
End consistent.
Opaque consistent_at.
Opaque consistent.
Section suf۰G.
Context `{suf۰G : SufG Σ}.
Definition suf۰model t reprs : iProp Σ :=
∃ descrs,
sstore_2۰model t descrs ∗
⌜consistent reprs descrs⌝.
#[local] Instance : CustomIpat "model" :=
" ( %descrs{} & Hmodel{} & %Hconsistent{} ) ".
Definition suf۰snapshot s t reprs : iProp Σ :=
∃ descrs,
sstore_2۰snapshot s t descrs ∗
⌜consistent reprs descrs⌝.
#[local] Instance : CustomIpat "snapshot" :=
" ( %descrs{} & Hsnapshot{} & %Hconsistent{} ) ".
#[global] Instance suf۰modelｰtimeless t reprs :
Timeless (suf۰model t reprs).
#[global] Instance suf۰snapshotｰpersistent s t reprs :
Persistent (suf۰snapshot s t reprs).
Lemma suf۰modelｰvalid {t reprs} elt repr :
reprs !! elt = Some repr →
suf۰model t reprs ⊢
⌜reprs !! repr = Some repr⌝.
Lemma suf۰modelｰexclusive t reprs1 reprs2 :
suf۰model t reprs1 -∗
suf۰model t reprs2 -∗
False.
Lemma suf٠createｰspec :
{{{
True
}}}
suf٠create ()
{{{
t
, RET t;
suf۰model t ∅
}}}.
Lemma suf٠makeｰspec t reprs :
{{{
suf۰model t reprs
}}}
suf٠make t
{{{
elt
, RET #elt;
suf۰model t (<[elt := elt]> reprs)
}}}.
Lemma suf٠reprｰspec {t reprs elt} repr :
reprs !! elt = Some repr →
{{{
suf۰model t reprs
}}}
suf٠repr t #elt
{{{
RET #repr;
suf۰model t reprs
}}}.
Lemma suf٠equivｰspec {t reprs elt1} repr1 {elt2} repr2 :
reprs !! elt1 = Some repr1 →
reprs !! elt2 = Some repr2 →
{{{
suf۰model t reprs
}}}
suf٠equiv t #elt1 #elt2
{{{
RET #(bool_decide (repr1 = repr2));
suf۰model t reprs
}}}.
#[local] Lemma suf٠rankｰspec t reprs elt :
reprs !! elt = Some elt →
{{{
suf۰model t reprs
}}}
suf٠rank t #elt
{{{
rank
, RET #rank;
suf۰model t reprs
}}}.
Definition suf۰union_condition reprs repr1 repr2 reprs' :=
dom reprs = dom reprs' ∧
( ∀ elt repr,
reprs !! elt = Some repr →
repr ≠ repr1 →
repr ≠ repr2 →
reprs' !! elt = Some repr
) ∧
( ∃ repr12,
(repr12 = repr1 ∨ repr12 = repr2) ∧
∀ elt repr,
reprs !! elt = Some repr →
repr = repr1 ∨ repr = repr2 →
reprs' !! elt = Some repr12
).
#[local] Lemma suf۰union_conditionｰrefl reprs repr :
suf۰union_condition reprs repr repr reprs.
#[local] Lemma suf۰union_conditionｰsym reprs repr1 repr2 reprs' :
suf۰union_condition reprs repr1 repr2 reprs' →
suf۰union_condition reprs repr2 repr1 reprs'.
#[local] Lemma unifyｰunion_condition₁ reprs repr1 repr2 :
repr1 ≠ repr2 →
suf۰union_condition reprs repr1 repr2 (unify repr1 repr2 reprs).
#[local] Lemma unifyｰunion_condition₂ reprs repr1 repr2 :
repr1 ≠ repr2 →
suf۰union_condition reprs repr2 repr1 (unify repr1 repr2 reprs).
#[local] Opaque suf۰union_condition.
Lemma suf٠unionｰspec {t reprs elt1} repr1 {elt2} repr2 :
reprs !! elt1 = Some repr1 →
reprs !! elt2 = Some repr2 →
{{{
suf۰model t reprs
}}}
suf٠union t #elt1 #elt2
{{{
reprs'
, RET ();
suf۰model t reprs' ∗
⌜suf۰union_condition reprs repr1 repr2 reprs'⌝
}}}.
Lemma suf٠captureｰspec t reprs :
{{{
suf۰model t reprs
}}}
suf٠capture t
{{{
s
, RET s;
suf۰model t reprs ∗
suf۰snapshot s t reprs
}}}.
Lemma suf٠restoreｰspec t reprs s reprs' :
{{{
suf۰model t reprs ∗
suf۰snapshot s t reprs'
}}}
suf٠restore t s
{{{
RET ();
suf۰model t reprs'
}}}.
End suf۰G.
Require zoo_persistent.suf__opaque.
#[global] Opaque suf۰model.
#[global] Opaque suf۰snapshot.