Commit 49c15360 authored by Simon Spies's avatar Simon Spies

nits

parent c56b93ab
Pipeline #19779 failed with stage
From iris.algebra Require Import auth agree.
From iris.base_logic.lib Require Import invariants.
From iris.heap_lang Require Export lifting metatheory.
From iris.heap_lang Require Import notation proofmode.
......@@ -15,7 +14,7 @@ Ltac bool_decide H :=
[rewrite bool_decide_true; [|exact H]|rewrite bool_decide_false; [|exact H]]
end.
Lemma Z_to_nat n: n >= 0 -> m: nat, n = m.
Lemma Z_to_nat (n: Z): 0 n -> m: nat, n = m.
Proof.
intros; exists (Z.to_nat n); rewrite Z2Nat.id; lia.
Qed.
......@@ -46,7 +45,6 @@ Section Arrays.
λ: "a" "i" "x", if: ((#-1) < "i") && ("i" < !"a") then (unsafe_set "a" "i" "x") else #().
(* Verification *)
Variable (N: namespace).
Definition array (n: Z) (l: loc) : iProp Σ :=
( zs: list Z, n = length zs l ↦∗ (#n :: ((LitV LitInt) <$> zs)))%I.
......@@ -143,7 +141,7 @@ Section Arrays.
Qed.
(** ** Specs *)
Lemma unsafe_arr_spec n: {{{ n >= 0 }}} unsafe_arr #n {{{ (l: loc), RET #l; array n l }}}.
Lemma unsafe_arr_spec n: {{{ 0 n }}} unsafe_arr #n {{{ (l: loc), RET #l; array n l }}}.
Proof.
iIntros (ϕ) "% Post". wp_lam. wp_pures. wp_bind (AllocN _ _).
wp_apply (wp_allocN); eauto. lia.
......@@ -176,13 +174,11 @@ Section Arrays.
now iApply "Post".
Qed.
(** Semantic Types *)
Definition Option (S: lty Σ) : lty Σ :=
Lty (fun v => ( v = NONEV s, S s v = SOMEV s)%I).
Lty (λ v, ( v = NONEV s, S s v = SOMEV s)%I).
Definition Array : lty Σ :=
Lty (fun v => ( (a: loc) (m: mnat), inv N (array m a) v = #a)%I).
Lty (λ v, ( (a: loc) (m: mnat), inv N (array m a) v = #a)%I).
Lemma typing_arr: arr : lty_int Option Array.
Proof.
......@@ -192,7 +188,7 @@ Section Arrays.
bool_decide H; wp_pures.
- iLeft. eauto.
- wp_apply wp_fupd.
wp_apply (unsafe_arr_spec); eauto with lia.
wp_apply (unsafe_arr_spec with "[]"); eauto with lia.
iIntros (l) "A".
edestruct (Z_to_nat z) as [m ->]; try lia.
wp_pures.
......@@ -219,7 +215,6 @@ Section Arrays.
- wp_pures. now iLeft.
Qed.
Lemma typing_set: set : Array lty_int lty_int lty_unit.
Proof.
iIntros (s) "!# _ /=". iApply wp_value.
......@@ -238,8 +233,6 @@ Section Arrays.
- now wp_pures.
Qed.
(** Copying Arrays *)
Definition copy_rec : val :=
rec: "f" "old" "new" "n" :=
......@@ -249,9 +242,8 @@ Section Arrays.
Definition copy : val :=
λ: "a" "n", let: "b" := unsafe_arr "n" in copy_rec "a" "b" (!"a");; "b".
Lemma copy_rec_spec (a1 a2: loc) (n1 n2 n: Z):
{{{ inv N (body n1 a1) body n2 a2 n <= n1 n <= n2 }}}
{{{ inv N (body n1 a1) body n2 a2 n n1 n n2 }}}
copy_rec #a1 #a2 #n
{{{ RET #(); body n2 a2 }}}.
Proof.
......@@ -275,9 +267,8 @@ Section Arrays.
- wp_pures; iApply "Post"; eauto.
Qed.
Lemma copy_spec (a: loc) (m n: Z):
{{{ inv N (array m a) 0 <= m <= n}}}
{{{ inv N (array m a) 0 m n}}}
copy #a #n
{{{ (b: loc), RET #b; array n b }}}.
Proof.
......@@ -291,6 +282,4 @@ Section Arrays.
{ repeat iSplit; eauto with lia. iApply array_body_inv; eauto. }
iIntros "?". wp_pures. iApply "Post". by iApply "Bclose".
Qed.
End Arrays.
......@@ -6,9 +6,8 @@ From iris_examples.logrel_heaplang.lib Require Import invariants arrays.
Set Default Proof Using "Type".
Section Vectors.
(* vec = ref array *)
(* vec = ref array *)
Section Vectors.
(* API *)
Definition use : val :=
......@@ -32,8 +31,7 @@ Set Default Proof Using "Type".
"b" + !"a" + #1 <- "x";;
if: CAS "v" "a" "b" then #() else "f" "v" "x".
(* History *)
(* History *)
Definition Hist := gmap loc nat.
Definition HistUR := gmapUR loc (agreeR (leibnizO nat)).
Definition hist : Hist HistUR := fmap (λ v: nat, to_agree (v : leibnizO nat)).
......@@ -43,6 +41,7 @@ Set Default Proof Using "Type".
!inG Σ (authR mnatUR), (* maximum length *)
!inG Σ (authR HistUR) (* history *)
}.
Variable (N: namespace).
(* Maximum Length *)
Global Instance auth_mnat_persistent (n: mnat) γ: Persistent (own γ ( n)).
......@@ -58,7 +57,7 @@ Set Default Proof Using "Type".
Qed.
Lemma auth_mnat_agree γ (m n : mnat):
own γ ( m) - own γ ( n) - n <= m.
own γ ( m) - own γ ( n) - n m.
Proof.
iIntros "Hγ● Hγ◯".
iDestruct (own_valid_2 with "Hγ● Hγ◯") as "%".
......@@ -75,13 +74,13 @@ Set Default Proof Using "Type".
Qed.
Lemma auth_mnat_previous γ (n m: mnat):
n <= m -> own γ ( m) - own γ ( n).
n m own γ ( m) - own γ ( n).
Proof.
intros H. eapply own_mono. eapply (auth_frag_mono n m), mnat_included. lia.
Qed.
Lemma auth_mnat_update γ (n p: mnat):
n <= p -> own γ ( n) == own γ ( p).
n p own γ ( n) == own γ ( p).
Proof.
iIntros (H) "Hγ●".
iMod (auth_mnat_fork with "Hγ●") as "[Hγ● Hγ◯]"; eauto.
......@@ -89,9 +88,6 @@ Set Default Proof Using "Type".
eapply auth_update, mnat_local_update; lia.
Qed.
Section hist.
(** Conversion to hists and back *)
Lemma hist_valid h : hist h.
......@@ -131,9 +127,8 @@ Set Default Proof Using "Type".
eauto with iFrame.
Qed.
Lemma hist_update γ h a m:
(h !! a = None) ->
(h !! a = None)
hist_all γ h == hist_all γ (<[a := m]> h) hist_entry γ a m.
Proof.
intros H. iIntros "Hγ●".
......@@ -161,12 +156,6 @@ Set Default Proof Using "Type".
now eapply hist_singleton_included in H.
Qed.
Variable (N: namespace).
Definition Vec_inv γ1 γ2 (l: loc) : iProp Σ :=
( (h: Hist) (a: loc) (m: mnat),
l #a
......@@ -178,7 +167,6 @@ Set Default Proof Using "Type".
Definition Vec γ1 γ2 l := inv N (Vec_inv γ1 γ2 l).
Definition Idx (γ1: gname) (i: mnat) := own γ1 ( (S i: mnat)).
Lemma Vec_project_array γ1 γ2 a m l:
hist_entry γ2 a m - Vec γ1 γ2 l - inv N (array m a).
Proof.
......@@ -194,18 +182,13 @@ Set Default Proof Using "Type".
iExists h, b, n. iFrame. now iApply "Hst".
Qed.
(* Function Verification *)
Definition ι γ1 γ2 : val := PairV (#(Z.pos γ1)) (#(Z.pos γ2)).
Definition β γ1 γ2 : lty Σ := Lty (fun v => v = ι γ1 γ2)%I.
Definition β γ1 γ2 : lty Σ := Lty (λ v, v = ι γ1 γ2)%I.
Definition Index (S: lty Σ) : lty Σ :=
Lty (fun v => ( γ1 γ2 (i: mnat), ( v, S v - β γ1 γ2 v) v = #i Idx γ1 i)%I).
Lty (λ v, ( γ1 γ2 (i: mnat), ( v, S v - β γ1 γ2 v) v = #i Idx γ1 i)%I).
Definition Vector (S: lty Σ) : lty Σ :=
Lty (fun v => ( γ1 γ2 (l: loc), ( v, S v - β γ1 γ2 v) v = #l Vec γ1 γ2 l)%I).
Lty (λ v, ( γ1 γ2 (l: loc), ( v, S v - β γ1 γ2 v) v = #l Vec γ1 γ2 l)%I).
Lemma typing_use: use : T, Array N ( S, Vector S T) T.
Proof. unfold use.
......@@ -232,8 +215,6 @@ Set Default Proof Using "Type".
iExists γ1, γ2, l. repeat iSplit; eauto.
Qed.
Lemma typing_idx: idx : ( S, Vector S lty_int Option (Index S)).
Proof. unfold idx.
iIntros (s) "!# T /=". iApply wp_value.
......@@ -259,7 +240,6 @@ Set Default Proof Using "Type".
iApply auth_mnat_previous; eauto. lia.
Qed.
Lemma typing_get: get : ( S, Vector S Index S lty_int).
Proof. unfold get.
iIntros (s) "!# T /=". iApply wp_value.
......@@ -279,8 +259,6 @@ Set Default Proof Using "Type".
iApply Vec_project_array; eauto. iPureIntro; lia.
Qed.
Lemma typing_set: set : ( S, Vector S Index S lty_int lty_unit).
Proof. unfold set.
iIntros (s) "!# T /=". iApply wp_value.
......@@ -302,7 +280,6 @@ Set Default Proof Using "Type".
iApply Vec_project_array; eauto. iPureIntro; lia.
Qed.
Lemma typing_app: app : ( S, Vector S lty_int lty_unit).
Proof.
iIntros (s) "!# #T /=".
......@@ -353,5 +330,4 @@ Set Default Proof Using "Type".
iApply "IH". iModIntro. iExists γ1, γ2, l. repeat iSplit; eauto.
iModIntro. iExists n. done.
Qed.
End Vectors.
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment