Commit 1ed41018 authored by Ralf Jung's avatar Ralf Jung
Browse files

make Z.of_nat not a Coercion any more

parent 846d5cff
......@@ -185,10 +185,10 @@ Section list.
Proof. intros f f' Hf l ? <-. apply big_opL_proper; intros; apply Hf. Qed.
Lemma big_opL_consZ_l (f : Z A M) x l :
([^o list] ky x :: l, f k y) = f 0 x `o` [^o list] ky l, f (1 + k)%Z y.
([^o list] ky x :: l, f (Z.of_nat k) y) = f 0%Z x `o` [^o list] ky l, f (1 + Z.of_nat k)%Z y.
Proof. rewrite big_opL_cons. auto using big_opL_ext with f_equal lia. Qed.
Lemma big_opL_consZ_r (f : Z A M) x l :
([^o list] ky x :: l, f k y) = f 0 x `o` [^o list] ky l, f (k + 1)%Z y.
([^o list] ky x :: l, f (Z.of_nat k) y) = f 0%Z x `o` [^o list] ky l, f (Z.of_nat k + 1)%Z y.
Proof. rewrite big_opL_cons. auto using big_opL_ext with f_equal lia. Qed.
Lemma big_opL_fmap {B} (h : A B) (f : nat B M) l :
......
......@@ -4,6 +4,3 @@ From iris.prelude Require Import options.
Global Open Scope general_if_scope.
Global Set SsrOldRewriteGoalsOrder. (* See Coq issue #5706 *)
Ltac done := stdpp.tactics.done.
(** Iris itself and many dependencies still rely on this coercion. *)
Coercion Z.of_nat : nat >-> Z.
......@@ -15,7 +15,7 @@ From iris.prelude Require Import options.
with lists of values. *)
Definition array `{!heapG Σ} (l : loc) (dq : dfrac) (vs : list val) : iProp Σ :=
([ list] i v vs, (l + i) {dq} v)%I.
([ list] i v vs, (l + Z.of_nat i) {dq} v)%I.
(** FIXME: Refactor these notations using custom entries once Coq bug #13654
has been fixed. *)
......@@ -56,7 +56,7 @@ Lemma array_singleton l dq v : l ↦∗{dq} [v] ⊣⊢ l ↦{dq} v.
Proof. by rewrite /array /= right_id loc_add_0. Qed.
Lemma array_app l dq vs ws :
l ↦∗{dq} (vs ++ ws) l ↦∗{dq} vs (l + length vs) ↦∗{dq} ws.
l ↦∗{dq} (vs ++ ws) l ↦∗{dq} vs (l + Z.of_nat (length vs)) ↦∗{dq} ws.
Proof.
rewrite /array big_sepL_app.
setoid_rewrite Nat2Z.inj_add.
......@@ -78,7 +78,9 @@ Proof. by rewrite /Frame array_cons. Qed.
Lemma update_array l dq vs off v :
vs !! off = Some v
l ↦∗{dq} vs - ((l + off) {dq} v v', (l + off) {dq} v' - l ↦∗{dq} <[off:=v']>vs).
l ↦∗{dq} vs -
((l + Z.of_nat off) {dq} v
v', (l + Z.of_nat off) {dq} v' - l ↦∗{dq} <[off:=v']>vs).
Proof.
iIntros (Hlookup) "Hl".
rewrite -[X in (l ↦∗{_} X)%I](take_drop_middle _ off v); last done.
......@@ -97,7 +99,7 @@ Qed.
(** * Rules for allocation *)
Lemma mapsto_seq_array l dq v n :
([ list] i seq 0 n, (l + (i : nat)) {dq} v) -
([ list] i seq 0 n, (l + (Z.of_nat i)) {dq} v) -
l ↦∗{dq} replicate n v.
Proof.
rewrite /array. iInduction n as [|n'] "IH" forall (l); simpl.
......@@ -111,7 +113,7 @@ Lemma twp_allocN s E v n :
(0 < n)%Z
[[{ True }]] AllocN (Val $ LitV $ LitInt $ n) (Val v) @ s; E
[[{ l, RET LitV (LitLoc l); l ↦∗ replicate (Z.to_nat n) v
[ list] i seq 0 (Z.to_nat n), meta_token (l + (i : nat)) }]].
[ list] i seq 0 (Z.to_nat n), meta_token (l + (Z.of_nat i)) }]].
Proof.
iIntros (Hzs Φ) "_ HΦ". iApply twp_allocN_seq; [done..|].
iIntros (l) "Hlm". iApply "HΦ".
......@@ -122,7 +124,7 @@ Lemma wp_allocN s E v n :
(0 < n)%Z
{{{ True }}} AllocN (Val $ LitV $ LitInt $ n) (Val v) @ s; E
{{{ l, RET LitV (LitLoc l); l ↦∗ replicate (Z.to_nat n) v
[ list] i seq 0 (Z.to_nat n), meta_token (l + (i : nat)) }}}.
[ list] i seq 0 (Z.to_nat n), meta_token (l + (Z.of_nat i)) }}}.
Proof.
iIntros (? Φ) "_ HΦ". iApply (twp_wp_step with "HΦ").
iApply twp_allocN; [auto..|]; iIntros (l) "H HΦ". by iApply "HΦ".
......@@ -133,7 +135,7 @@ Lemma twp_allocN_vec s E v n :
[[{ True }]]
AllocN #n v @ s ; E
[[{ l, RET #l; l ↦∗ vreplicate (Z.to_nat n) v
[ list] i seq 0 (Z.to_nat n), meta_token (l + (i : nat)) }]].
[ list] i seq 0 (Z.to_nat n), meta_token (l + (Z.of_nat i)) }]].
Proof.
iIntros (Hzs Φ) "_ HΦ". iApply twp_allocN; [ lia | done | .. ].
iIntros (l) "[Hl Hm]". iApply "HΦ". rewrite vec_to_list_replicate. iFrame.
......@@ -143,7 +145,7 @@ Lemma wp_allocN_vec s E v n :
{{{ True }}}
AllocN #n v @ s ; E
{{{ l, RET #l; l ↦∗ vreplicate (Z.to_nat n) v
[ list] i seq 0 (Z.to_nat n), meta_token (l + (i : nat)) }}}.
[ list] i seq 0 (Z.to_nat n), meta_token (l + (Z.of_nat i)) }}}.
Proof.
iIntros (? Φ) "_ HΦ". iApply (twp_wp_step with "HΦ").
iApply twp_allocN_vec; [auto..|]; iIntros (l) "H HΦ". by iApply "HΦ".
......@@ -152,7 +154,7 @@ Qed.
(** * Rules for accessing array elements *)
Lemma twp_load_offset s E l dq off vs v :
vs !! off = Some v
[[{ l ↦∗{dq} vs }]] ! #(l + off) @ s; E [[{ RET v; l ↦∗{dq} vs }]].
[[{ l ↦∗{dq} vs }]] ! #(l + Z.of_nat off) @ s; E [[{ RET v; l ↦∗{dq} vs }]].
Proof.
iIntros (Hlookup Φ) "Hl HΦ".
iDestruct (update_array l _ _ _ _ Hlookup with "Hl") as "[Hl1 Hl2]".
......@@ -162,22 +164,22 @@ Proof.
Qed.
Lemma wp_load_offset s E l dq off vs v :
vs !! off = Some v
{{{ l ↦∗{dq} vs }}} ! #(l + off) @ s; E {{{ RET v; l ↦∗{dq} vs }}}.
{{{ l ↦∗{dq} vs }}} ! #(l + Z.of_nat off) @ s; E {{{ RET v; l ↦∗{dq} vs }}}.
Proof.
iIntros (? Φ) ">H HΦ". iApply (twp_wp_step with "HΦ").
iApply (twp_load_offset with "H"); [eauto..|]; iIntros "H HΦ". by iApply "HΦ".
Qed.
Lemma twp_load_offset_vec s E l dq sz (off : fin sz) (vs : vec val sz) :
[[{ l ↦∗{dq} vs }]] ! #(l + off) @ s; E [[{ RET vs !!! off; l ↦∗{dq} vs }]].
[[{ l ↦∗{dq} vs }]] ! #(l + Z.of_nat off) @ s; E [[{ RET vs !!! off; l ↦∗{dq} vs }]].
Proof. apply twp_load_offset. by apply vlookup_lookup. Qed.
Lemma wp_load_offset_vec s E l dq sz (off : fin sz) (vs : vec val sz) :
{{{ l ↦∗{dq} vs }}} ! #(l + off) @ s; E {{{ RET vs !!! off; l ↦∗{dq} vs }}}.
{{{ l ↦∗{dq} vs }}} ! #(l + Z.of_nat off) @ s; E {{{ RET vs !!! off; l ↦∗{dq} vs }}}.
Proof. apply wp_load_offset. by apply vlookup_lookup. Qed.
Lemma twp_store_offset s E l off vs v :
is_Some (vs !! off)
[[{ l ↦∗ vs }]] #(l + off) <- v @ s; E [[{ RET #(); l ↦∗ <[off:=v]> vs }]].
[[{ l ↦∗ vs }]] #(l + Z.of_nat off) <- v @ s; E [[{ RET #(); l ↦∗ <[off:=v]> vs }]].
Proof.
iIntros ([w Hlookup] Φ) "Hl HΦ".
iDestruct (update_array l _ _ _ _ Hlookup with "Hl") as "[Hl1 Hl2]".
......@@ -186,20 +188,20 @@ Proof.
Qed.
Lemma wp_store_offset s E l off vs v :
is_Some (vs !! off)
{{{ l ↦∗ vs }}} #(l + off) <- v @ s; E {{{ RET #(); l ↦∗ <[off:=v]> vs }}}.
{{{ l ↦∗ vs }}} #(l + Z.of_nat off) <- v @ s; E {{{ RET #(); l ↦∗ <[off:=v]> vs }}}.
Proof.
iIntros (? Φ) ">H HΦ". iApply (twp_wp_step with "HΦ").
iApply (twp_store_offset with "H"); [eauto..|]; iIntros "H HΦ". by iApply "HΦ".
Qed.
Lemma twp_store_offset_vec s E l sz (off : fin sz) (vs : vec val sz) v :
[[{ l ↦∗ vs }]] #(l + off) <- v @ s; E [[{ RET #(); l ↦∗ vinsert off v vs }]].
[[{ l ↦∗ vs }]] #(l + Z.of_nat off) <- v @ s; E [[{ RET #(); l ↦∗ vinsert off v vs }]].
Proof.
setoid_rewrite vec_to_list_insert. apply twp_store_offset.
eexists. by apply vlookup_lookup.
Qed.
Lemma wp_store_offset_vec s E l sz (off : fin sz) (vs : vec val sz) v :
{{{ l ↦∗ vs }}} #(l + off) <- v @ s; E {{{ RET #(); l ↦∗ vinsert off v vs }}}.
{{{ l ↦∗ vs }}} #(l + Z.of_nat off) <- v @ s; E {{{ RET #(); l ↦∗ vinsert off v vs }}}.
Proof.
iIntros (Φ) ">H HΦ". iApply (twp_wp_step with "HΦ").
iApply (twp_store_offset_vec with "H"); [eauto..|]; iIntros "H HΦ". by iApply "HΦ".
......@@ -207,7 +209,7 @@ Qed.
Lemma twp_xchg_offset s E l off vs v v' :
vs !! off = Some v
[[{ l ↦∗ vs }]] Xchg #(l + off) v' @ s; E [[{ RET v; l ↦∗ <[off:=v']> vs }]].
[[{ l ↦∗ vs }]] Xchg #(l + Z.of_nat off) v' @ s; E [[{ RET v; l ↦∗ <[off:=v']> vs }]].
Proof.
iIntros (Hlookup Φ) "Hl HΦ".
iDestruct (update_array l _ _ _ _ Hlookup with "Hl") as "[Hl1 Hl2]".
......@@ -216,20 +218,20 @@ Proof.
Qed.
Lemma wp_xchg_offset s E l off vs v v' :
vs !! off = Some v
{{{ l ↦∗ vs }}} Xchg #(l + off) v' @ s; E {{{ RET v; l ↦∗ <[off:=v']> vs }}}.
{{{ l ↦∗ vs }}} Xchg #(l + Z.of_nat off) v' @ s; E {{{ RET v; l ↦∗ <[off:=v']> vs }}}.
Proof.
iIntros (? Φ) ">H HΦ". iApply (twp_wp_step with "HΦ").
iApply (twp_xchg_offset with "H"); [eauto..|]; iIntros "H HΦ". by iApply "HΦ".
Qed.
Lemma twp_xchg_offset_vec s E l sz (off : fin sz) (vs : vec val sz) v :
[[{ l ↦∗ vs }]] Xchg #(l + off) v @ s; E [[{ RET (vs !!! off); l ↦∗ vinsert off v vs }]].
[[{ l ↦∗ vs }]] Xchg #(l + Z.of_nat off) v @ s; E [[{ RET (vs !!! off); l ↦∗ vinsert off v vs }]].
Proof.
setoid_rewrite vec_to_list_insert. apply twp_xchg_offset => //.
by apply vlookup_lookup.
Qed.
Lemma wp_xchg_offset_vec s E l sz (off : fin sz) (vs : vec val sz) v :
{{{ l ↦∗ vs }}} Xchg #(l + off) v @ s; E {{{ RET (vs !!! off); l ↦∗ vinsert off v vs }}}.
{{{ l ↦∗ vs }}} Xchg #(l + Z.of_nat off) v @ s; E {{{ RET (vs !!! off); l ↦∗ vinsert off v vs }}}.
Proof.
iIntros (Φ) ">H HΦ". iApply (twp_wp_step with "HΦ").
iApply (twp_xchg_offset_vec with "H"); [eauto..|]; iIntros "H HΦ". by iApply "HΦ".
......@@ -240,7 +242,7 @@ Lemma twp_cmpxchg_suc_offset s E l off vs v' v1 v2 :
v' = v1
vals_compare_safe v' v1
[[{ l ↦∗ vs }]]
CmpXchg #(l + off) v1 v2 @ s; E
CmpXchg #(l + Z.of_nat off) v1 v2 @ s; E
[[{ RET (v', #true); l ↦∗ <[off:=v2]> vs }]].
Proof.
iIntros (Hlookup ?? Φ) "Hl HΦ".
......@@ -253,7 +255,7 @@ Lemma wp_cmpxchg_suc_offset s E l off vs v' v1 v2 :
v' = v1
vals_compare_safe v' v1
{{{ l ↦∗ vs }}}
CmpXchg #(l + off) v1 v2 @ s; E
CmpXchg #(l + Z.of_nat off) v1 v2 @ s; E
{{{ RET (v', #true); l ↦∗ <[off:=v2]> vs }}}.
Proof.
iIntros (??? Φ) ">H HΦ". iApply (twp_wp_step with "HΦ").
......@@ -264,7 +266,7 @@ Lemma twp_cmpxchg_suc_offset_vec s E l sz (off : fin sz) (vs : vec val sz) v1 v2
vs !!! off = v1
vals_compare_safe (vs !!! off) v1
[[{ l ↦∗ vs }]]
CmpXchg #(l + off) v1 v2 @ s; E
CmpXchg #(l + Z.of_nat off) v1 v2 @ s; E
[[{ RET (vs !!! off, #true); l ↦∗ vinsert off v2 vs }]].
Proof.
intros. setoid_rewrite vec_to_list_insert. eapply twp_cmpxchg_suc_offset=> //.
......@@ -274,7 +276,7 @@ Lemma wp_cmpxchg_suc_offset_vec s E l sz (off : fin sz) (vs : vec val sz) v1 v2
vs !!! off = v1
vals_compare_safe (vs !!! off) v1
{{{ l ↦∗ vs }}}
CmpXchg #(l + off) v1 v2 @ s; E
CmpXchg #(l + Z.of_nat off) v1 v2 @ s; E
{{{ RET (vs !!! off, #true); l ↦∗ vinsert off v2 vs }}}.
Proof.
iIntros (?? Φ) ">H HΦ". iApply (twp_wp_step with "HΦ").
......@@ -286,7 +288,7 @@ Lemma twp_cmpxchg_fail_offset s E l dq off vs v0 v1 v2 :
v0 v1
vals_compare_safe v0 v1
[[{ l ↦∗{dq} vs }]]
CmpXchg #(l + off) v1 v2 @ s; E
CmpXchg #(l + Z.of_nat off) v1 v2 @ s; E
[[{ RET (v0, #false); l ↦∗{dq} vs }]].
Proof.
iIntros (Hlookup HNEq Hcmp Φ) "Hl HΦ".
......@@ -301,7 +303,7 @@ Lemma wp_cmpxchg_fail_offset s E l dq off vs v0 v1 v2 :
v0 v1
vals_compare_safe v0 v1
{{{ l ↦∗{dq} vs }}}
CmpXchg #(l + off) v1 v2 @ s; E
CmpXchg #(l + Z.of_nat off) v1 v2 @ s; E
{{{ RET (v0, #false); l ↦∗{dq} vs }}}.
Proof.
iIntros (??? Φ) ">H HΦ". iApply (twp_wp_step with "HΦ").
......@@ -312,20 +314,20 @@ Lemma twp_cmpxchg_fail_offset_vec s E l dq sz (off : fin sz) (vs : vec val sz) v
vs !!! off v1
vals_compare_safe (vs !!! off) v1
[[{ l ↦∗{dq} vs }]]
CmpXchg #(l + off) v1 v2 @ s; E
CmpXchg #(l + Z.of_nat off) v1 v2 @ s; E
[[{ RET (vs !!! off, #false); l ↦∗{dq} vs }]].
Proof. intros. eapply twp_cmpxchg_fail_offset=> //. by apply vlookup_lookup. Qed.
Lemma wp_cmpxchg_fail_offset_vec s E l dq sz (off : fin sz) (vs : vec val sz) v1 v2 :
vs !!! off v1
vals_compare_safe (vs !!! off) v1
{{{ l ↦∗{dq} vs }}}
CmpXchg #(l + off) v1 v2 @ s; E
CmpXchg #(l + Z.of_nat off) v1 v2 @ s; E
{{{ RET (vs !!! off, #false); l ↦∗{dq} vs }}}.
Proof. intros. eapply wp_cmpxchg_fail_offset=> //. by apply vlookup_lookup. Qed.
Lemma twp_faa_offset s E l off vs (i1 i2 : Z) :
vs !! off = Some #i1
[[{ l ↦∗ vs }]] FAA #(l + off) #i2 @ s; E
[[{ l ↦∗ vs }]] FAA #(l + Z.of_nat off) #i2 @ s; E
[[{ RET LitV (LitInt i1); l ↦∗ <[off:=#(i1 + i2)]> vs }]].
Proof.
iIntros (Hlookup Φ) "Hl HΦ".
......@@ -335,7 +337,7 @@ Proof.
Qed.
Lemma wp_faa_offset s E l off vs (i1 i2 : Z) :
vs !! off = Some #i1
{{{ l ↦∗ vs }}} FAA #(l + off) #i2 @ s; E
{{{ l ↦∗ vs }}} FAA #(l + Z.of_nat off) #i2 @ s; E
{{{ RET LitV (LitInt i1); l ↦∗ <[off:=#(i1 + i2)]> vs }}}.
Proof.
iIntros (? Φ) ">H HΦ". iApply (twp_wp_step with "HΦ").
......@@ -344,7 +346,7 @@ Qed.
Lemma twp_faa_offset_vec s E l sz (off : fin sz) (vs : vec val sz) (i1 i2 : Z) :
vs !!! off = #i1
[[{ l ↦∗ vs }]] FAA #(l + off) #i2 @ s; E
[[{ l ↦∗ vs }]] FAA #(l + Z.of_nat off) #i2 @ s; E
[[{ RET LitV (LitInt i1); l ↦∗ vinsert off #(i1 + i2) vs }]].
Proof.
intros. setoid_rewrite vec_to_list_insert. apply twp_faa_offset=> //.
......@@ -352,7 +354,7 @@ Proof.
Qed.
Lemma wp_faa_offset_vec s E l sz (off : fin sz) (vs : vec val sz) (i1 i2 : Z) :
vs !!! off = #i1
{{{ l ↦∗ vs }}} FAA #(l + off) #i2 @ s; E
{{{ l ↦∗ vs }}} FAA #(l + Z.of_nat off) #i2 @ s; E
{{{ RET LitV (LitInt i1); l ↦∗ vinsert off #(i1 + i2) vs }}}.
Proof.
iIntros (? Φ) ">H HΦ". iApply (twp_wp_step with "HΦ").
......
......@@ -595,9 +595,9 @@ Proof.
{ rewrite lookup_empty. naive_solver lia. }
rewrite -insert_union_singleton_l lookup_insert_Some IH. split.
- intros [[-> ?] | (Hl & j & w & ? & -> & -> & ?)].
{ eexists 0, _. rewrite loc_add_0. naive_solver lia. }
{ eexists 0%Z, _. rewrite loc_add_0. naive_solver lia. }
eexists (1 + j)%Z, _. rewrite loc_add_assoc !Z.add_1_l Z2Nat.inj_succ; auto with lia.
- intros (j & w & ? & -> & -> & Hil). destruct (decide (j = 0)); simplify_eq/=.
- intros (j & w & ? & -> & -> & Hil). destruct (decide (j = 0%Z)); simplify_eq/=.
{ rewrite loc_add_0; eauto. }
right. split.
{ rewrite -{1}(loc_add_0 l). intros ?%(inj (loc_add _)); lia. }
......@@ -609,7 +609,7 @@ Proof.
Qed.
Lemma heap_array_map_disjoint (h : gmap loc (option val)) (l : loc) (vs : list val) :
( i, (0 i)%Z (i < length vs)%Z h !! (l + i) = None)
( i, (0 i)%Z (i < Z.of_nat (length vs))%Z h !! (l + i) = None)
(heap_array l vs) ## h.
Proof.
intros Hdisj. apply map_disjoint_spec=> l' v1 v2.
......
......@@ -26,7 +26,7 @@ Qed.
Lemma minimum_spec_nat `{!heapG Σ} s E (Φ : val iProp Σ) (m n : nat) :
Φ #(m `min` n)%nat -
WP minimum #m #n @ s;E {{ Φ }}.
Proof. iIntros "HΦ". iApply minimum_spec. by rewrite Nat2Z.inj_min. Qed.
Proof. iIntros "HΦ". iApply minimum_spec. by rewrite /LitNat Nat2Z.inj_min. Qed.
Lemma maximum_spec `{!heapG Σ} s E (Φ : val iProp Σ) (m n : Z) :
Φ #(m `max` n) -
......@@ -40,4 +40,4 @@ Qed.
Lemma maximum_spec_nat `{!heapG Σ} s E (Φ : val iProp Σ) (m n : nat) :
Φ #(m `max` n)%nat -
WP maximum #m #n @ s;E {{ Φ }}.
Proof. iIntros "HΦ". iApply maximum_spec. by rewrite Nat2Z.inj_max. Qed.
Proof. iIntros "HΦ". iApply maximum_spec. by rewrite /LitNat Nat2Z.inj_max. Qed.
......@@ -53,7 +53,7 @@ Section proof.
Context `{!heapG Σ}.
Lemma twp_array_free s E l vs (n : Z) :
n = length vs
n = Z.of_nat (length vs)
[[{ l ↦∗ vs }]] array_free #l #n @ s; E [[{ RET #(); True }]].
Proof.
iIntros (Hlen Φ) "Hl HΦ".
......@@ -63,7 +63,7 @@ Section proof.
wp_free. wp_pures. iApply ("IH" with "[] Hl"); eauto with lia.
Qed.
Lemma wp_array_free s E l vs (n : Z) :
n = length vs
n = Z.of_nat (length vs)
{{{ l ↦∗ vs }}} array_free #l #n @ s; E {{{ RET #(); True }}}.
Proof.
iIntros (? Φ) "H HΦ". iApply (twp_wp_step with "HΦ").
......@@ -132,12 +132,12 @@ Section proof.
Local Lemma wp_array_init_loop stk E l i n k f :
n = Z.of_nat (i + k)
{{{
(l + i) ↦∗ replicate k #()
[ list] j seq i k, WP f #(j : nat) @ stk; E {{ Q j }}
(l + Z.of_nat i) ↦∗ replicate k #()
[ list] j seq i k, WP f #(Z.of_nat j) @ stk; E {{ Q j }}
}}}
array_init_loop #l #i #n f @ stk; E
array_init_loop #l #(Z.of_nat i) #n f @ stk; E
{{{ vs, RET #();
length vs = k (l + i) ↦∗ vs [ list] jv vs, Q (i + j) v
length vs = k (l + Z.of_nat i) ↦∗ vs [ list] jv vs, Q (i + j) v
}}}.
Proof.
iIntros (Hn Φ) "[Hl Hf] HΦ".
......@@ -159,12 +159,12 @@ Section proof.
Local Lemma twp_array_init_loop stk E l i n k f :
n = Z.of_nat (i + k)
[[{
(l + i) ↦∗ replicate k #()
[ list] j seq i k, WP f #(j : nat) @ stk; E [{ Q j }]
(l + Z.of_nat i) ↦∗ replicate k #()
[ list] j seq i k, WP f #(Z.of_nat j) @ stk; E [{ Q j }]
}]]
array_init_loop #l #i #n f @ stk; E
array_init_loop #l #(Z.of_nat i) #n f @ stk; E
[[{ vs, RET #();
length vs = k (l + i) ↦∗ vs [ list] jv vs, Q (i + j) v
length vs = k (l + Z.of_nat i) ↦∗ vs [ list] jv vs, Q (i + j) v
}]].
Proof.
iIntros (Hn Φ) "[Hl Hf] HΦ".
......@@ -187,7 +187,7 @@ Section proof.
Lemma wp_array_init stk E n f :
(0 < n)%Z
{{{
[ list] i seq 0 (Z.to_nat n), WP f #(i : nat) @ stk; E {{ Q i }}
[ list] i seq 0 (Z.to_nat n), WP f #(Z.of_nat i) @ stk; E {{ Q i }}
}}}
array_init #n f @ stk; E
{{{ l vs, RET #l;
......@@ -206,7 +206,7 @@ Section proof.
Lemma twp_array_init stk E n f :
(0 < n)%Z
[[{
[ list] i seq 0 (Z.to_nat n), WP f #(i : nat) @ stk; E [{ Q i }]
[ list] i seq 0 (Z.to_nat n), WP f #(Z.of_nat i) @ stk; E [{ Q i }]
}]]
array_init #n f @ stk; E
[[{ l vs, RET #l;
......@@ -243,7 +243,7 @@ Section proof.
(0 < n)%Z
{{{
[ list] i seq 0 (Z.to_nat n),
WP f #(i : nat) @ stk; E {{ v, x, v = g x Q i x }}
WP f #(Z.of_nat i) @ stk; E {{ v, x, v = g x Q i x }}
}}}
array_init #n f @ stk; E
{{{ l xs, RET #l;
......@@ -259,7 +259,7 @@ Section proof.
(0 < n)%Z
[[{
[ list] i seq 0 (Z.to_nat n),
WP f #(i : nat) @ stk; E [{ v, x, v = g x Q i x }]
WP f #(Z.of_nat i) @ stk; E [{ v, x, v = g x Q i x }]
}]]
array_init #n f @ stk; E
[[{ l xs, RET #l;
......
......@@ -58,7 +58,7 @@ Section mono_proof.
iMod (own_update_2 with "Hγ Hγf") as "[Hγ Hγf]".
{ apply auth_update, (max_nat_local_update _ _ (MaxNat (S c))). simpl. auto. }
wp_cmpxchg_suc. iModIntro. iSplitL "Hl Hγ".
{ iNext. iExists (S c). rewrite Nat2Z.inj_succ Z.add_1_l. by iFrame. }
{ iNext. iExists (S c). rewrite /LitNat Nat2Z.inj_succ Z.add_1_l. by iFrame. }
wp_pures. iApply "HΦ". iModIntro. iExists γ; repeat iSplit; eauto.
iApply (own_mono with "Hγf").
(* FIXME: FIXME(Coq #6294): needs new unification *)
......@@ -135,7 +135,7 @@ Section contrib_spec.
- iMod (own_update_2 with "Hγ Hγf") as "[Hγ Hγf]".
{ apply frac_auth_update, (nat_local_update _ _ (S c) (S n)); lia. }
wp_cmpxchg_suc. iModIntro. iSplitL "Hl Hγ".
{ iNext. iExists (S c). rewrite Nat2Z.inj_succ Z.add_1_l. by iFrame. }
{ iNext. iExists (S c). rewrite /LitNat Nat2Z.inj_succ Z.add_1_l. by iFrame. }
wp_pures. by iApply "HΦ".
- wp_cmpxchg_fail; first (by intros [= ?%Nat2Z.inj]).
iModIntro. iSplitL "Hl Hγ"; [iNext; iExists c'; by iFrame|].
......
......@@ -131,7 +131,7 @@ Section proof.
rewrite -(set_seq_S_end_union_L 0).
wp_cmpxchg_suc. iModIntro. iSplitL "Hlo' Hln' Haown Hauth".
{ iNext. iExists o', (S n).
rewrite Nat2Z.inj_succ -Z.add_1_r. by iFrame. }
rewrite /LitNat Nat2Z.inj_succ -Z.add_1_r. by iFrame. }
wp_pures.
iApply (wait_loop_spec γ (#lo, #ln) with "[-HΦ]").
+ iFrame. rewrite /is_lock; eauto 10.
......@@ -166,7 +166,7 @@ Section proof.
by apply option_local_update, (exclusive_local_update _ (Excl (S o))). }
iModIntro. iSplitR "HΦ"; last by iApply "HΦ".
iIntros "!> !>". iExists (S o), n'.
rewrite Nat2Z.inj_succ -Z.add_1_r. iFrame. iLeft. by iFrame.
rewrite /LitNat Nat2Z.inj_succ -Z.add_1_r. iFrame. iLeft. by iFrame.
Qed.
End proof.
......
......@@ -7,6 +7,7 @@ Coercion LitInt : Z >-> base_lit.
Coercion LitBool : bool >-> base_lit.
Coercion LitLoc : loc >-> base_lit.
Coercion LitProphecy : proph_id >-> base_lit.
Coercion LitNat (n : nat) : base_lit := LitInt (Z.of_nat n).
Coercion App : expr >-> Funclass.
......
......@@ -188,7 +188,7 @@ are derived in te file [array]. *)
Lemma heap_array_to_seq_meta l vs (n : nat) :
length vs = n
([ map] l' _ heap_array l vs, meta_token l' ) -
[ list] i seq 0 n, meta_token (l + (i : nat)) .
[ list] i seq 0 n, meta_token (l + (Z.of_nat i)) .
Proof.
iIntros (<-) "Hvs". iInduction vs as [|v vs] "IH" forall (l)=> //=.
rewrite big_opM_union; last first.
......@@ -203,7 +203,7 @@ Qed.
Lemma heap_array_to_seq_mapsto l v (n : nat) :
([ map] l' ov heap_array l (replicate n v), gen_heap.mapsto l' (DfracOwn 1) ov) -
[ list] i seq 0 n, (l + (i : nat)) v.
[ list] i seq 0 n, (l + (Z.of_nat i)) v.
Proof.
iIntros "Hvs". iInduction n as [|n] "IH" forall (l); simpl.
{ done. }
......@@ -221,7 +221,7 @@ Lemma twp_allocN_seq s E v n :
(0 < n)%Z
[[{ True }]] AllocN (Val $ LitV $ LitInt $ n) (Val v) @ s; E
[[{ l, RET LitV (LitLoc l); [ list] i seq 0 (Z.to_nat n),
(l + (i : nat)) v meta_token (l + (i : nat)) }]].
(l + (Z.of_nat i)) v meta_token (l + (Z.of_nat i)) }]].
Proof.
iIntros (Hn Φ) "_ HΦ". iApply twp_lift_atomic_head_step_no_fork; first done.
iIntros (σ1 ns κs nt) "[Hσ Hκs] !>"; iSplit; first by destruct n; auto with lia head_step.
......@@ -239,7 +239,7 @@ Lemma wp_allocN_seq s E v n :
(0 < n)%Z
{{{ True }}} AllocN (Val $ LitV $ LitInt $ n) (Val v) @ s; E
{{{ l, RET LitV (LitLoc l); [ list] i seq 0 (Z.to_nat n),
(l + (i : nat)) v meta_token (l + (i : nat)) }}}.
(l + (Z.of_nat i)) v meta_token (l + (Z.of_nat i)) }}}.
Proof.
iIntros (Hn Φ) "_ HΦ". iApply (twp_wp_step with "HΦ").
iApply twp_allocN_seq; [by auto..|]; iIntros (l) "H HΦ". by iApply "HΦ".
......
......@@ -512,7 +512,7 @@ Section interpreter.
l interp_alloc n;
_ interp_modify_state (state_init_heap l n v);
mret (LitV (LitLoc l))
else (error $ if decide (n = 0)
else (error $ if decide (n = 0%Z)
then "alloc: cannot allocate 0 elements"
else "alloc: negative number of elements (first argument) " + n)