Skip to content

GitLab

Commit 62de96aa authored by Michael Sammler's avatar Michael Sammler
Browse files

add provenance in bytes

parent 9c785dbe
Pipeline #49274 passed with stage
in 22 minutes and 22 seconds
Hide whitespace changes
Inline Side-by-side
examples/proofs/wrapping_add/wrapping_rules.v
View file @ 62de96aa
......@@ -21,17 +21,17 @@ Section type.
iDestruct ("HT" with "Hty2") as (Hv2) "HT".
iIntros (Φ) "HΦ".
iDestruct ("HT" with "[] []" ) as (??) "HT".
1-2: iPureIntro; by apply: val_to_Z_weak_in_range.
have /val_of_Z_is_Some[v Hv] : ((n1 + n2) `mod` int_modulus it1) ∈ it1 by apply int_modulus_mod_in_range.
1-2: iPureIntro; by apply: val_to_Z_in_range.
have /(val_of_Z_is_Some None)[v Hv] : ((n1 + n2) `mod` int_modulus it1) ∈ it1 by apply int_modulus_mod_in_range.
subst it2.
iApply (wp_binop_det v). iSplit.
- iIntros (σ v') "_ !%". split.
+ inversion 1; simplify_eq/=.
by destruct it1 as [? []]; simplify_eq/=.
+ move => ->. econstructor => //.
+ move => ->. apply: ArithOpII => //.
by destruct it1 as [? []]; simplify_eq/=.
- iIntros "!>". iApply "HΦ"; last done. iPureIntro.
apply val_to_of_Z in Hv. by apply val_to_Z_to_int_repr_Z.
by eapply val_to_of_Z.
Qed.
Global Instance macro_wrapping_add_inst it1 it2 e1 e2 :
......
linux/pkvm/proofs/spinlock/spinlock_proof.v
View file @ 62de96aa
......@@ -280,7 +280,7 @@ Section proofs.
iDestruct "Hcases" as "[[Hticket' %] | Htok]".
{ iExFalso. by iApply (ticket_non_duplicable with "Hticket Hticket'"). }
iAssert (⌜owner ∈ u16⌝)%I as %[??].
{ rewrite /ty_own_val /=. by iDestruct "Hv" as %Hv%val_to_Z_weak_in_range. }
{ rewrite /ty_own_val /=. by iDestruct "Hv" as %Hv%val_to_Z_in_range. }
iAssert (⌜owner < next⌝)%I as %?.
{ destruct (decide (owner < next)); first done. iExFalso.
iDestruct (ty_size_eq with "Hv") as %?.
......@@ -382,7 +382,7 @@ Section proofs.
(* Learn that [next'] actually is [max_int u16]. *)
iAssert ⌜next' = max_int u16⌝%I as %->.
{ iDestruct (ty_deref with "Hnext") as (w) "[_ H]". iDestruct "H" as %Hnext.
iPureIntro. apply val_to_Z_weak_in_range in Hnext as [??]. lia. }
iPureIntro. apply val_to_Z_in_range in Hnext as [??]. lia. }
(* We perform the write and close the invariant. *)
iDestruct (ty_aligned with "Howner") as %?.
iDestruct (ty_deref with "Howner") as (v') "[Hl Hv]".
......@@ -410,7 +410,7 @@ Section proofs.
iAssert ⌜owner' = 0⌝%I as %->.
{ destruct (decide (owner' = 0)) => //. iExFalso.
iDestruct (ty_deref with "Howner") as (?) "[? Hv]".
iDestruct "Hv" as %Howner%val_to_Z_weak_in_range.
iDestruct "Hv" as %Howner%val_to_Z_in_range.
destruct Howner as [Howner ?].
iDestruct (overlaping_ticket_ranges with "[] Htk Htr1") as "$".
iPureIntro. exists 0. split; apply elem_of_seqZ; try done.
......@@ -459,7 +459,7 @@ Section proofs.
iDestruct (ty_aligned with "Howner") as %?.
iDestruct (ty_deref with "Howner") as (v') "[Hl Hv]".
iDestruct (ty_size_eq with "Hv") as %?.
iDestruct "Hv" as %?%val_to_Z_weak_in_range.
iDestruct "Hv" as %?%val_to_Z_in_range.
iSplitL "Hl". { iExists _. by iFrame "Hl". }
iIntros "!> Hl".
iRename select (_ ◁ᵥ (owner + 1) @ int u16)%I into "Howner+1".
......
theories/lang/ghost_state.v
View file @ 62de96aa
......@@ -406,6 +406,12 @@ Section loc_in_bounds.
move => [??]. split; cbn; first by lia.
rewrite /max_int /= /int_modulus /bits_per_int /bytes_per_int /=. lia.
Qed.
Lemma loc_in_bounds_has_alloc_id l n: loc_in_bounds l n -∗ ⌜∃ aid, l.1 = ProvAlloc (Some aid)⌝.
Proof.
rewrite loc_in_bounds_eq. iIntros "H". iDestruct "H" as (id ?????) "H".
iPureIntro. by exists id.
Qed.
End loc_in_bounds.
Section heap.
......@@ -444,12 +450,6 @@ Section heap.
l ↦{q} v -∗ loc_in_bounds l (length v).
Proof. rewrite heap_mapsto_eq. iIntros "[$ _]". Qed.
Lemma loc_in_bounds_has_alloc_id l n: loc_in_bounds l n -∗ ⌜∃ aid, l.1 = ProvAlloc (Some aid)⌝.
Proof.
rewrite loc_in_bounds_eq. iIntros "H". iDestruct "H" as (id ?????) "H".
iPureIntro. by exists id.
Qed.
Lemma heap_mapsto_has_alloc_id l q v : l ↦{q} v -∗ ⌜∃ aid, l.1 = ProvAlloc (Some aid)⌝.
Proof.
iIntros "Hl". iApply loc_in_bounds_has_alloc_id.
......
theories/lang/lang.v
View file @ 62de96aa
......@@ -227,13 +227,13 @@ Definition subst_function (xs : list (var_name * val)) (f : function) : function
(* evaluation can be non-deterministic for comparing pointers *)
Inductive eval_bin_op : bin_op → op_type → op_type → state → val → val → val → Prop :=
| PtrOffsetOpIP v1 v2 σ o l ly it:
val_to_Z_weak v1 it = Some o →
val_to_Z v1 it = Some o →
val_to_loc v2 = Some l →
(* TODO: should we have an alignment check here? *)
heap_state_loc_in_bounds (l offset{ly}ₗ o) 0 σ.(st_heap) →
eval_bin_op (PtrOffsetOp ly) (IntOp it) PtrOp σ v1 v2 (val_of_loc (l offset{ly}ₗ o))
| PtrNegOffsetOpIP v1 v2 σ o l ly it:
val_to_Z_weak v1 it = Some o →
val_to_Z v1 it = Some o →
val_to_loc v2 = Some l →
heap_state_loc_in_bounds (l offset{ly}ₗ -o) 0 σ.(st_heap) →
(* TODO: should we have an alignment check here? *)
......@@ -243,23 +243,23 @@ Inductive eval_bin_op : bin_op → op_type → op_type → state → val → val
val_to_loc v1 = Some l →
v2 = NULL →
(* TODO ( see below ): Should we really hard code i32 here because of C? *)
i2v (Z_of_bool false) i32 = v →
val_of_Z (Z_of_bool false) i32 None = Some v →
eval_bin_op EqOp PtrOp PtrOp σ v1 v2 v
| NeOpPNull v1 v2 σ l v:
heap_state_loc_in_bounds l 0%nat σ.(st_heap) →
val_to_loc v1 = Some l →
v2 = NULL →
i2v (Z_of_bool true) i32 = v →
val_of_Z (Z_of_bool true) i32 None = Some v→
eval_bin_op NeOp PtrOp PtrOp σ v1 v2 v
| EqOpNullNull v1 v2 σ v:
v1 = NULL →
v2 = NULL →
i2v (Z_of_bool true) i32 = v →
val_of_Z (Z_of_bool true) i32 None = Some v →
eval_bin_op EqOp PtrOp PtrOp σ v1 v2 v
| NeOpNullNull v1 v2 σ v:
v1 = NULL →
v2 = NULL →
i2v (Z_of_bool false) i32 = v →
val_of_Z (Z_of_bool false) i32 None = Some v →
eval_bin_op NeOp PtrOp PtrOp σ v1 v2 v
| RelOpPP v1 v2 σ l1 l2 v b op:
val_to_loc v1 = Some l1 →
......@@ -274,9 +274,9 @@ Inductive eval_bin_op : bin_op → op_type → op_type → state → val → val
| GeOp => if bool_decide (l1.1 = l2.1) then Some (bool_decide (l1.2 >= l2.2)) else None
| _ => None
end = Some b →
i2v (Z_of_bool b) i32 = v →
val_of_Z (Z_of_bool b) i32 None = Some v →
eval_bin_op op PtrOp PtrOp σ v1 v2 v
| RelOpII op v1 v2 σ n1 n2 it b:
| RelOpII op v1 v2 v σ n1 n2 it b:
match op with
| EqOp => Some (bool_decide (n1 = n2))
| NeOp => Some (bool_decide (n1 ≠ n2))
......@@ -286,11 +286,12 @@ Inductive eval_bin_op : bin_op → op_type → op_type → state → val → val
| GeOp => Some (bool_decide (n1 >= n2))
| _ => None
end = Some b →
val_to_Z_weak v1 it = Some n1 →
val_to_Z_weak v2 it = Some n2 →
val_to_Z v1 it = Some n1 →
val_to_Z v2 it = Some n2 →
(* TODO: What is the right int type of the result here? C seems to
use i32 but maybe we don't want to hard code that. *)
eval_bin_op op (IntOp it) (IntOp it) σ v1 v2 (i2v (Z_of_bool b) i32)
val_of_Z (Z_of_bool b) i32 None = Some v →
eval_bin_op op (IntOp it) (IntOp it) σ v1 v2 v
| ArithOpII op v1 v2 σ n1 n2 it n v:
match op with
| AddOp => Some (n1 + n2)
......@@ -315,9 +316,9 @@ Inductive eval_bin_op : bin_op → op_type → op_type → state → val → val
| ShrOp => if bool_decide (0 ≤ n1 ∧ 0 ≤ n2 < bits_per_int it) then Some (n1 ≫ n2) else None
| _ => None
end = Some n →
val_to_Z_weak v1 it = Some n1 →
val_to_Z_weak v2 it = Some n2 →
val_of_Z (if it_signed it then n else n `mod` int_modulus it) it = Some v →
val_to_Z v1 it = Some n1 →
val_to_Z v2 it = Some n2 →
val_of_Z (if it_signed it then n else n `mod` int_modulus it) it None = Some v →
eval_bin_op op (IntOp it) (IntOp it) σ v1 v2 v
| CommaOp ot1 ot2 σ v1 v2:
eval_bin_op Comma ot1 ot2 σ v1 v2 v2
......@@ -325,36 +326,38 @@ Inductive eval_bin_op : bin_op → op_type → op_type → state → val → val
Inductive eval_un_op : un_op → op_type → state → val → val → Prop :=
| CastOpII itt its σ vs vt i:
val_to_int_repr vs its = Some i →
val_of_int_repr i itt = Some vt →
val_to_Z vs its = Some i →
val_of_Z i itt (val_to_byte_prov vs) = Some vt →
eval_un_op (CastOp (IntOp itt)) (IntOp its) σ vs vt
| CastOpPP σ vs vt l:
val_to_loc vs = Some l →
val_of_loc l = vt →
eval_un_op (CastOp PtrOp) PtrOp σ vs vt
| CastOpPI it σ vs vt l:
| CastOpPI it σ vs vt l p:
val_to_loc vs = Some l →
val_of_int_repr (IRLoc l) it = Some vt →
l.1 = ProvAlloc p →
val_of_Z l.2 it p = Some vt →
block_alive l σ.(st_heap) →
eval_un_op (CastOp (IntOp it)) PtrOp σ vs vt
| CastOpPINull it σ vs vt:
vs = NULL →
val_of_Z 0 it = Some vt →
val_of_Z 0 it None = Some vt →
eval_un_op (CastOp (IntOp it)) PtrOp σ vs vt
| CastOpIP it σ vs vt l l':
val_to_loc_weak vs it = Some l →
val_of_loc l' = vt →
| CastOpIP it σ vs vt l l' a:
val_to_Z vs it = Some a →
l = (ProvAlloc (val_to_byte_prov vs), a) →
(** This is using that the address 0 is never alive. *)
l' = (if bool_decide (valid_ptr l σ.(st_heap)) then l else
(if bool_decide (l.2 = 0) then NULL_loc else (ProvAlloc None, l.2))) →
(if bool_decide (a = 0) then NULL_loc else (ProvAlloc None, a))) →
val_of_loc l' = vt →
eval_un_op (CastOp PtrOp) (IntOp it) σ vs vt
| NegOpI it σ vs vt n:
val_to_Z_weak vs it = Some n →
val_of_Z (-n) it = Some vt →
val_to_Z vs it = Some n →
val_of_Z (-n) it None = Some vt →
eval_un_op NegOp (IntOp it) σ vs vt
| NotIntOpI it σ vs vt n:
val_to_Z_weak vs it = Some n →
val_of_Z (if it_signed it then Z.lnot n else Z_lunot (bits_per_int it) n) it = Some vt →
val_to_Z vs it = Some n →
val_of_Z (if it_signed it then Z.lnot n else Z_lunot (bits_per_int it) n) it None = Some vt →
eval_un_op NotIntOp (IntOp it) σ vs vt
.
......@@ -391,8 +394,8 @@ comparing pointers? (see lambda rust) *)
heap_at l1 (it_layout it) vo (λ st, ∃ n, st = RSt n) σ.(st_heap).(hs_heap) →
val_to_loc v2 = Some l2 →
heap_at l2 (it_layout it) ve (λ st, st = RSt 0%nat) σ.(st_heap).(hs_heap) →
val_to_Z_weak vo it = Some z1 →
val_to_Z_weak ve it = Some z2 →
val_to_Z vo it = Some z1 →
val_to_Z ve it = Some z2 →
v3 `has_layout_val` it_layout it →
(bytes_per_int it ≤ bytes_per_addr)%nat →
z1 ≠ z2 →
......@@ -403,8 +406,8 @@ comparing pointers? (see lambda rust) *)
heap_at l1 (it_layout it) vo (λ st, st = RSt 0%nat) σ.(st_heap).(hs_heap) →
val_to_loc v2 = Some l2 →
heap_at l2 (it_layout it) ve (λ st, ∃ n, st = RSt n) σ.(st_heap).(hs_heap) →
val_to_Z_weak vo it = Some z1 →
val_to_Z_weak ve it = Some z2 →
val_to_Z vo it = Some z1 →
val_to_Z ve it = Some z2 →
v3 `has_layout_val` it_layout it →
(bytes_per_int it ≤ bytes_per_addr)%nat →
z1 = z2 →
......@@ -439,12 +442,12 @@ comparing pointers? (see lambda rust) *)
| ConcatS vs σ:
expr_step (Concat (Val <$> vs)) σ [] (Val (mjoin vs)) σ []
| CopyAllocIdS σ v1 v2 a it l:
val_to_Z_weak v1 it = Some a →
val_to_Z v1 it = Some a →
val_to_loc v2 = Some l →
valid_ptr (l.1, a) σ.(st_heap) →
expr_step (CopyAllocId (IntOp it) (Val v1) (Val v2)) σ [] (Val (val_of_loc (l.1, a))) σ []
| IfES v it e1 e2 n σ:
val_to_Z_weak v it = Some n →
val_to_Z v it = Some n →
expr_step (IfE (IntOp it) (Val v) e1 e2) σ [] (if bool_decide (n ≠ 0) then e1 else e2) σ []
(* no rule for StuckE *)
.
......@@ -461,7 +464,7 @@ Inductive stmt_step : stmt → runtime_function → state → list Empty_set →
heap_at l ly v' start_st σ.(st_heap).(hs_heap) →
stmt_step (Assign o ly (Val v1) (Val v2) s) rf σ [] (to_rtstmt rf end_stmt) (heap_fmap (heap_upd l end_val end_st) σ) []
| SwitchS rf σ v n m bs s def it :
val_to_Z_weak v it = Some n →
val_to_Z v it = Some n →
(∀ i : nat, m !! n = Some i → is_Some (bs !! i)) →
stmt_step (Switch it (Val v) m bs def) rf σ [] (to_rtstmt rf (default def (i ← m !! n; bs !! i))) σ []
| GotoS rf σ b s :
......
theories/lang/lifting.v
View file @ 62de96aa
......@@ -255,8 +255,8 @@ Lemma wp_cas_fail vl1 vl2 vd vo ve z1 z2 Φ l1 l2 it q E:
val_to_loc vl2 = Some l2 →
l1 `has_layout_loc` it_layout it →
l2 `has_layout_loc` it_layout it →
val_to_Z_weak vo it = Some z1 →
val_to_Z_weak ve it = Some z2 →
val_to_Z vo it = Some z1 →
val_to_Z ve it = Some z2 →
length vd = bytes_per_int it →
(bytes_per_int it ≤ bytes_per_addr)%nat →
z1 ≠ z2 →
......@@ -268,7 +268,7 @@ Proof.
iIntros (σ1) "((%&Hhctx&?)&Hfctx)".
iDestruct (heap_mapsto_has_alloc_id with "Hl1") as %Haid1.
iDestruct (heap_mapsto_has_alloc_id with "Hl2") as %Haid2.
move: (Hvo) (Hve) => /val_to_Z_weak_length ? /val_to_Z_weak_length ?.
move: (Hvo) (Hve) => /val_to_Z_length ? /val_to_Z_length ?.
iDestruct (heap_mapsto_lookup_q (λ st : lock_state, ∃ n : nat, st = RSt n) with "Hhctx Hl1") as %? => //. { naive_solver. }
iDestruct (heap_mapsto_lookup_1 (λ st : lock_state, st = RSt 0%nat) with "Hhctx Hl2") as %? => //.
iModIntro. iSplit; first by eauto 15 using CasFailS.
......@@ -286,8 +286,8 @@ Lemma wp_cas_suc vl1 vl2 vd vo ve z1 z2 Φ l1 l2 it E q:
val_to_loc vl2 = Some l2 →
l1 `has_layout_loc` it_layout it →
l2 `has_layout_loc` it_layout it →
val_to_Z_weak vo it = Some z1 →
val_to_Z_weak ve it = Some z2 →
val_to_Z vo it = Some z1 →
val_to_Z ve it = Some z2 →
length vd = bytes_per_int it →
(bytes_per_int it ≤ bytes_per_addr)%nat →
z1 = z2 →
......@@ -299,7 +299,7 @@ Proof.
iIntros (σ1) "((%&Hhctx&?)&Hfctx)".
iDestruct (heap_mapsto_has_alloc_id with "Hl1") as %Haid1.
iDestruct (heap_mapsto_has_alloc_id with "Hl2") as %Haid2.
move: (Hvo) (Hve) => /val_to_Z_weak_length ? /val_to_Z_weak_length ?.
move: (Hvo) (Hve) => /val_to_Z_length ? /val_to_Z_length ?.
iDestruct (heap_mapsto_lookup_1 (λ st : lock_state, st = RSt 0%nat) with "Hhctx Hl1") as %? => //.
iDestruct (heap_mapsto_lookup_q (λ st : lock_state, ∃ n : nat, st = RSt n) with "Hhctx Hl2") as %? => //. { naive_solver. }
iModIntro. iSplit; first by eauto 15 using CasSucS.
......@@ -313,8 +313,8 @@ Proof.
Qed.
Lemma wp_neg_int Φ v v' n E it:
val_to_Z_weak v it = Some n →
val_of_Z (-n) it = Some v' →
val_to_Z v it = Some n →
val_of_Z (-n) it None = Some v' →
▷ Φ (v') -∗ WP UnOp NegOp (IntOp it) (Val v) @ E {{ Φ }}.
Proof.
iIntros (Hv Hv') "HΦ".
......@@ -325,8 +325,8 @@ Proof.
Qed.
Lemma wp_cast_int Φ v v' i E its itt:
val_to_int_repr v its = Some i →
val_of_int_repr i itt = Some v' →
val_to_Z v its = Some i →
val_of_Z i itt (val_to_byte_prov v) = Some v' →
▷ Φ (v') -∗ WP UnOp (CastOp (IntOp itt)) (IntOp its) (Val v) @ E {{ Φ }}.
Proof.
iIntros (Hv Hv') "HΦ".
......@@ -347,22 +347,23 @@ Proof.
- move => ->. by econstructor.
Qed.
Lemma wp_cast_ptr_int Φ v v' l E it:
Lemma wp_cast_ptr_int Φ v v' l E it p:
val_to_loc v = Some l →
val_of_int_repr (IRLoc l) it = Some v' →
l.1 = ProvAlloc p →
val_of_Z l.2 it p = Some v' →
alloc_alive_loc l ∧ ▷ Φ (v') -∗
WP UnOp (CastOp (IntOp it)) PtrOp (Val v) @ E {{ Φ }}.
Proof.
iIntros (Hv Hv') "HΦ".
iIntros (Hv Hp Hv') "HΦ".
iApply wp_unop_det. iSplit; [iDestruct "HΦ" as "[HΦ _]" | iDestruct "HΦ" as "[_ $]"].
iIntros (σ ?) "Hctx". iDestruct (alloc_alive_loc_to_block_alive with "HΦ Hctx") as %Hb.
iPureIntro. split.
- move: (Hb) => [?[??]]. have ? := val_to_of_loc NULL_loc. inversion 1; unfold NULL in *; by simplify_eq.
- have ? := val_to_of_loc NULL_loc. inversion 1; unfold NULL in *; destruct l; by simplify_eq/=.
- move => ->. by econstructor.
Qed.
Lemma wp_cast_null_int Φ v E it:
val_of_Z 0 it = Some v →
val_of_Z 0 it None = Some v →
▷ Φ v -∗
WP UnOp (CastOp (IntOp it)) PtrOp (Val NULL) @ E {{ Φ }}.
Proof.
......@@ -374,39 +375,42 @@ Proof.
- move => ->. by econstructor.
Qed.
Lemma wp_cast_int_ptr_weak Φ v l E it:
val_to_loc_weak v it = Some l →
(∀ i, ▷ Φ (val_of_loc (i, l.2))) -∗
Lemma wp_cast_int_ptr_weak Φ v a E it:
val_to_Z v it = Some a →
(∀ i, ▷ Φ (val_of_loc (i, a))) -∗
WP UnOp (CastOp PtrOp) (IntOp it) (Val v) @ E {{ Φ }}.
Proof.
iIntros (Hv) "HΦ".
iApply wp_unop.
iIntros (σ) "Hctx". iSplit; [iPureIntro; eexists _; by econstructor |].
iIntros "!>" (v' Hv'). iFrame.
inversion Hv'; simplify_eq. destruct l; simplify_eq/=; case_bool_decide; [ iApply "HΦ"|].
inversion Hv'; simplify_eq.
case_bool_decide; [ iApply "HΦ"|].
case_bool_decide; simplify_eq; iApply "HΦ".
Qed.
Lemma wp_cast_int_ptr_alive Φ v l E it:
val_to_loc_weak v it = Some l →
Lemma wp_cast_int_ptr_alive Φ v a p l E it:
val_to_Z v it = Some a →
val_to_byte_prov v = Some p →
l = (ProvAlloc (Some p), a) →
loc_in_bounds l 0 -∗
alloc_alive_loc l ∧ ▷ Φ (val_of_loc l) -∗
WP UnOp (CastOp PtrOp) (IntOp it) (Val v) @ E {{ Φ }}.
Proof.
iIntros (Hv) "#Hlib HΦ".
iIntros (Hv Hp ->) "#Hlib HΦ".
iApply wp_unop_det. iSplit; [iDestruct "HΦ" as "[HΦ _]" | iDestruct "HΦ" as "[_ $]"].
iIntros (σ ?) "Hctx".
iAssert ⌜valid_ptr l σ.(st_heap)⌝%I as %?. {
iAssert ⌜valid_ptr (ProvAlloc (Some p), a) σ.(st_heap)⌝%I as %?. {
iSplit; [ |iApply (loc_in_bounds_to_heap_loc_in_bounds with "Hlib Hctx")].
by iApply (alloc_alive_loc_to_block_alive with "[HΦ] Hctx").
}
iPureIntro. split.
- by inversion 1; simplify_eq; case_bool_decide.
- move => ->. econstructor; [done..|]. by case_bool_decide.
- inversion 1; simplify_eq; case_bool_decide; by rewrite ->Hp in *.
- move => ->. econstructor; [done..|]. rewrite Hp. by case_bool_decide.
Qed.
Lemma wp_copy_alloc_id Φ it a l v1 v2 E:
val_to_Z_weak v1 it = Some a →
val_to_Z v1 it = Some a →
val_to_loc v2 = Some l →
loc_in_bounds (l.1, a) 0 -∗
alloc_alive_loc l ∧ ▷ Φ (val_of_loc (l.1, a)) -∗
......@@ -425,9 +429,10 @@ Proof.
by iApply wp_value.
Qed.
Lemma wp_ptr_relop Φ op v1 v2 l1 l2 E b:
Lemma wp_ptr_relop Φ op v1 v2 v l1 l2 E b:
val_to_loc v1 = Some l1 →
val_to_loc v2 = Some l2 →
val_of_Z (Z_of_bool b) i32 None = Some v →
match op with
| EqOp => Some (bool_decide (l1.2 = l2.2))
| NeOp => Some (bool_decide (l1.2 ≠ l2.2))
......@@ -438,10 +443,10 @@ Lemma wp_ptr_relop Φ op v1 v2 l1 l2 E b:
| _ => None
end = Some b →
loc_in_bounds l1 0 -∗ loc_in_bounds l2 0 -∗
(alloc_alive_loc l1 ∧ alloc_alive_loc l2 ∧ ▷ Φ (i2v (Z_of_bool b) i32)) -∗
(alloc_alive_loc l1 ∧ alloc_alive_loc l2 ∧ ▷ Φ v) -∗
WP BinOp op PtrOp PtrOp (Val v1) (Val v2) @ E {{ Φ }}.
Proof.
iIntros (Hv1 Hv2 Hop) "#Hl1 #Hl2 HΦ".
iIntros (Hv1 Hv2 Hv Hop) "#Hl1 #Hl2 HΦ".
iDestruct (loc_in_bounds_has_alloc_id with "Hl1") as %[??].
iDestruct (loc_in_bounds_has_alloc_id with "Hl2") as %[??].
iApply wp_binop. iIntros (σ) "Hσ".
......@@ -462,7 +467,7 @@ Qed.
Lemma wp_ptr_offset Φ vl l E it o ly vo:
val_to_loc vl = Some l →
val_to_Z_weak vo it = Some o →
val_to_Z vo it = Some o →
loc_in_bounds (l offset{ly}ₗ o) 0 -∗
▷ Φ (val_of_loc (l offset{ly}ₗ o)) -∗
WP Val vl at_offset{ ly , PtrOp, IntOp it} Val vo @ E {{ Φ }}.
......@@ -478,7 +483,7 @@ Qed.
Lemma wp_ptr_neg_offset Φ vl l E it o ly vo:
val_to_loc vl = Some l →
val_to_Z_weak vo it = Some o →
val_to_Z vo it = Some o →
loc_in_bounds (l offset{ly}ₗ -o) 0 -∗
▷ Φ (val_of_loc (l offset{ly}ₗ -o)) -∗
WP Val vl at_neg_offset{ ly , PtrOp, IntOp it} Val vo @ E {{ Φ }}.
......@@ -501,11 +506,11 @@ Lemma wp_get_member Φ vl l sl n E:
Proof.
iIntros (Hvl [i Hi]) "#Hl HΦ".
rewrite /GetMember/GetMemberLoc/offset_of Hi /=.
have [|v Hv]:= (val_of_Z_is_Some size_t (offset_of_idx sl.(sl_members) i)). {
have [|v Hv]:= (val_of_Z_is_Some None size_t (offset_of_idx sl.(sl_members) i)). {
split; first by rewrite /min_int/=; lia. by apply offset_of_bound.
}
rewrite Hv /=. move: Hv => /val_to_of_Z Hv.
iApply wp_ptr_offset; [done| by apply: val_to_Z_to_int_repr_Z | | ].
iApply wp_ptr_offset; [done| done | | ].
{ have ? := offset_of_idx_le_size sl i. rewrite offset_loc_sz1 //.
iApply (loc_in_bounds_offset with "Hl"); simpl; [done| destruct l => /=; lia | destruct l => /=; lia ]. }
by rewrite offset_loc_sz1.
......@@ -521,11 +526,11 @@ Qed.
Lemma wp_offset_of Φ s m i E:
offset_of s.(sl_members) m = Some i →
(∀ v, ⌜val_of_Z i size_t = Some v⌝ -∗ Φ v) -∗
(∀ v, ⌜val_of_Z i size_t None = Some v⌝ -∗ Φ v) -∗
WP OffsetOf s m @ E {{ Φ }}.
Proof.
rewrite /OffsetOf. iIntros (Ho) "HΦ".
have [|? Hs]:= (val_of_Z_is_Some size_t i). {
have [|? Hs]:= (val_of_Z_is_Some None size_t i). {
split; first by rewrite /min_int/=; lia.
move: Ho => /fmap_Some[?[?->]].
by apply offset_of_bound.
......@@ -539,7 +544,7 @@ Lemma wp_offset_of_union Φ ul m E:
Proof. by iApply @wp_value. Qed.
Lemma wp_if Φ it v e1 e2 n:
val_to_Z_weak v it = Some n →
val_to_Z v it = Some n →
(if decide (n = 0) then WP coerce_rtexpr e2 {{ Φ }} else WP coerce_rtexpr e1 {{ Φ }}) -∗
WP IfE (IntOp it) (Val v) e1 e2 {{ Φ }}.
Proof.
......@@ -837,7 +842,7 @@ Proof.
Qed.
Lemma wps_switch Q Ψ v n ss def m it:
val_to_Z_weak v it = Some n →
val_to_Z v it = Some n →
(∀ i, m !! n = Some i → is_Some (ss !! i)) →
WPs default def (i ← m !! n; ss !! i) {{ Q, Ψ }} -∗ WPs (Switch it (Val v) m ss def) {{ Q , Ψ }}.
Proof.
......@@ -850,7 +855,7 @@ Qed.
(** a version of wps_switch which is directed by ss instead of n *)
Lemma wps_switch' Q Ψ v n ss def m it:
val_to_Z_weak v it = Some n →
val_to_Z v it = Some n →
map_Forall (λ _ i, is_Some (ss !! i)) m →
([∧ list] i↦s∈ss, ⌜m !! n = Some i⌝ -∗ WPs s {{ Q, Ψ }}) ∧
(⌜m !! n = None⌝ -∗ WPs def {{ Q, Ψ }}) -∗
......@@ -865,7 +870,7 @@ Proof.
Qed.
Lemma wps_if Q Ψ v s1 s2 n:
val_to_Z_weak v bool_it = Some n →
val_to_Z v bool_it = Some n →
(if decide (n = 0) then WPs s2 {{ Q, Ψ }} else WPs s1 {{ Q, Ψ }}) -∗
WPs (if: (Val v) then s1 else s2) {{ Q , Ψ }}.
Proof.
......@@ -875,7 +880,7 @@ Proof.
Qed.
Lemma wps_assert Q Ψ v s n:
val_to_Z_weak v bool_it = Some n → n ≠ 0 →
val_to_Z v bool_it = Some n → n ≠ 0 →
WPs s {{ Q, Ψ }} -∗
WPs (assert: Val v; s) {{ Q , Ψ }}.
Proof.
......
theories/lang/notation.v
View file @ 62de96aa
......@@ -321,7 +321,7 @@ Proof.
Qed.
Definition GetMember (e : expr) (s : struct_layout) (m : var_name) : expr :=
(e at_offset{u8, PtrOp, IntOp size_t} Val (default [MPoison] (offset_of s.(sl_members) m ≫= (λ m, val_of_Z (Z.of_nat m) size_t))))%E.
(e at_offset{u8, PtrOp, IntOp size_t} Val (default [MPoison] (offset_of s.(sl_members) m ≫= (λ m, val_of_Z (Z.of_nat m) size_t None))))%E.
Notation "e 'at{' s } m" := (GetMember e%E s m) (at level 10, format "e 'at{' s } m") : expr_scope.
Typeclasses Opaque GetMember.