Commit 476fe0a6 authored by Rodolphe Lepigre's avatar Rodolphe Lepigre
Browse files

A couple of renamings for consistency

Obtained with commands:
  sed -i 's/val_of_Z_is_some/val_of_Z_is_Some/g' **/*.v
  sed -i 's/val_to_of_int/val_to_of_Z/g' **/*.v
parent 13acc121
Pipeline #45457 failed with stage
in 28 minutes and 3 seconds
......@@ -22,7 +22,7 @@ Section type.
iIntros (Φ) "HΦ".
iDestruct ("HT" with "[] []" ) as (??) "HT".
1-2: iPureIntro; by apply: val_to_Z_in_range.
have /val_of_Z_is_some[v Hv] : ((n1 + n2) `mod` int_modulus it1) it1 by apply int_modulus_mod_in_range.
have /val_of_Z_is_Some[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.
......@@ -30,7 +30,7 @@ Section type.
by destruct it1 as [? []]; simplify_eq/=.
+ move => ->. econstructor => //.
by destruct it1 as [? []]; simplify_eq/=.
- iIntros "!>". iApply "HΦ"; last done. iPureIntro. by apply val_to_of_int.
- iIntros "!>". iApply "HΦ"; last done. iPureIntro. by apply val_to_of_Z.
Qed.
Global Instance macro_wrapping_add_inst it1 it2 e1 e2 :
......
......@@ -466,8 +466,8 @@ Section proofs.
iSplit. { iPureIntro. by lia. }
iDestruct ((ty_ref (t := (owner + 1) @ int u16)) with "[] Hl []") as "$" => //.
{ iPureIntro. rewrite /i2v.
destruct (val_of_Z (owner + 1)) eqn:Heq => /=; first by apply val_to_of_int.
exfalso. assert (owner + 1 u16) as Hu16%val_of_Z_is_some by (split; lia).
destruct (val_of_Z (owner + 1)) eqn:Heq => /=; first by apply val_to_of_Z.
exfalso. assert (owner + 1 u16) as Hu16%val_of_Z_is_Some by (split; lia).
destruct Hu16 as [??]. by simplify_eq. }
iRight. iFrame "Htok". by iExists _. }
iModIntro.
......
......@@ -444,11 +444,11 @@ Lemma wp_get_member Φ vl l sl n E:
Proof.
iIntros (Hvl [i Hi]) "HΦ".
rewrite /GetMember/GetMemberLoc/offset_of Hi /=.
have [|? Hs]:= (val_of_Z_is_some size_t (offset_of_idx sl.(sl_members) i)). {
have [|? Hs]:= (val_of_Z_is_Some size_t (offset_of_idx sl.(sl_members) i)). {
split; first by rewrite /min_int/=; lia.
by apply offset_of_bound.
}
rewrite Hs /=. move: Hs => /val_to_of_int Hs.
rewrite Hs /=. move: Hs => /val_to_of_Z Hs.
iApply wp_binop_det. iSplit; last done.
iIntros (σ v) "_ !%". split.
- inversion 1; simplify_eq. by rewrite offset_loc_sz1.
......@@ -466,7 +466,7 @@ Lemma wp_offset_of Φ s m i E:
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 size_t i). {
split; first by rewrite /min_int/=; lia.
move: Ho => /fmap_Some[?[?->]].
by apply offset_of_bound.
......
......@@ -107,7 +107,7 @@ Lemma val_of_Z_go_length z sz :
length (val_of_Z_go z sz) = sz.
Proof. elim: sz z => //= ? IH ?. by f_equal. Qed.
Lemma val_to_of_int_go z (sz : nat) :
Lemma val_to_of_Z_go z (sz : nat) :
0 z < 2 ^ (sz * bits_per_byte)
val_to_Z_go (val_of_Z_go z sz) = Some z.
Proof.
......@@ -130,7 +130,7 @@ Lemma val_to_Z_length v it z:
val_to_Z v it = Some z length v = bytes_per_int it.
Proof. rewrite /val_to_Z. by case_decide. Qed.
Lemma val_of_Z_is_some it z:
Lemma val_of_Z_is_Some it z:
z it is_Some (val_of_Z z it).
Proof. rewrite /val_of_Z. case_bool_decide; by eauto. Qed.
......@@ -173,7 +173,7 @@ Proof.
- move => [??] [] ?. lia.
Qed.
Lemma val_to_of_int z it v:
Lemma val_to_of_Z z it v:
val_of_Z z it = Some v val_to_Z v it = Some z.
Proof.
rewrite /val_of_Z /val_to_Z => Ht.
......@@ -181,7 +181,7 @@ Proof.
move: Hr => /bool_decide_eq_true[Hm HM].
have Hlen := bytes_per_int_gt_0 it.
rewrite /max_int in HM. rewrite /min_int in Hm.
rewrite val_of_Z_go_length val_to_of_int_go /=.
rewrite val_of_Z_go_length val_to_of_Z_go /=.
- case_decide as H => //. clear H.
destruct (it_signed it) eqn:Hs => /=.
+ case_decide => /=; last (rewrite bool_decide_false //; lia).
......@@ -202,7 +202,7 @@ Qed.
Lemma val_of_Z_bool b it:
val_of_Z (Z_of_bool b) it = Some (i2v (Z_of_bool b) it).
Proof.
have [|? Hv] := val_of_Z_is_some it (Z_of_bool b); last by rewrite /i2v Hv.
have [|? Hv] := val_of_Z_is_Some it (Z_of_bool b); last by rewrite /i2v Hv.
rewrite /elem_of /int_elem_of_it.
have ? := min_int_le_0 it. have ? := max_int_ge_127 it.
split; destruct b => /=; lia.
......@@ -218,7 +218,7 @@ Proof. by have /val_of_Z_length -> := val_of_Z_bool b it. Qed.
Lemma i2v_bool_Some b it:
val_to_Z (i2v (Z_of_bool b) it) it = Some (Z_of_bool b).
Proof. apply val_to_of_int. apply val_of_Z_bool. Qed.
Proof. apply val_to_of_Z. apply val_of_Z_bool. Qed.
Lemma val_to_Z_go_Some_inj v1 v2 n:
length v1 = length v2
......
......@@ -108,8 +108,8 @@ Section programs.
n it T (t2mt (n @ (int it))) - typed_value (i2v n it) T.
Proof.
iIntros "[%Hn HT]".
move: Hn => /val_of_Z_is_some [v Hv].
move: (Hv) => /val_to_of_int Hn.
move: Hn => /val_of_Z_is_Some [v Hv].
move: (Hv) => /val_to_of_Z Hn.
iExists _. iFrame. iPureIntro. by rewrite /i2v Hv.
Qed.
Global Instance type_val_int_inst n it : TypedValue (i2v n it) :=
......@@ -264,7 +264,7 @@ Section programs.
iIntros "%Hop HT %Hv1 %Hv2 %Φ HΦ".
iDestruct ("HT" with "[] []" ) as (Hsc) "HT".
1-2: iPureIntro; by apply: val_to_Z_in_range.
assert (n it) as [v Hv]%val_of_Z_is_some.
assert (n it) as [v Hv]%val_of_Z_is_Some.
{ apply: arith_op_result_in_range => //; by apply: val_to_Z_in_range. }
move: (Hv) => /val_of_Z_in_range ?. rewrite /i2v Hv /=.
iApply (wp_binop_det v). iSplit.
......@@ -278,7 +278,7 @@ Section programs.
all: try by inversion Hsc; case_bool_decide; naive_solver.
all: destruct it as [? []]; simplify_eq/= => //.
all: try by rewrite it_in_range_mod.
- iIntros "!>". iApply "HΦ"; last done. iPureIntro. by apply val_to_of_int.
- iIntros "!>". iApply "HΦ"; last done. iPureIntro. by apply val_to_of_Z.
Qed.
Global Program Instance type_add_int_int_inst it v1 n1 v2 n2:
TypedBinOpVal v1 (n1 @ int it)%I v2 (n2 @ int it)%I AddOp (IntOp it) (IntOp it) := λ T, i2p (type_arithop_int_int it v1 n1 v2 n2 T (n1 + n2) _ _).
......@@ -357,12 +357,12 @@ Section programs.
iIntros "HT %Hv %Φ HΦ". move: (Hv) => /val_to_Z_in_range ?.
iDestruct ("HT" with "[//]") as (Hs Hn) "HT".
have ? : val_of_Z (- n) it = Some (i2v (- n) it). {
have [|? Hv'] := val_of_Z_is_some it (- n); last by rewrite /i2v Hv'.
have [|? Hv'] := val_of_Z_is_Some it (- n); last by rewrite /i2v Hv'.
unfold elem_of, int_elem_of_it, max_int, min_int in *.
destruct it as [?[]] => //; simpl in *; lia.
}
iApply wp_neg_int => //. iApply ("HΦ" with "[] HT").
iPureIntro. by apply val_to_of_int.
iPureIntro. by apply val_to_of_Z.
Qed.
Global Instance type_neg_int_inst n it v:
TypedUnOpVal v (n @ int it)%I NegOp (IntOp it) :=
......@@ -374,9 +374,9 @@ Section programs.
Proof.
iIntros "HT %Hv %Φ HΦ". iDestruct ("HT" with "[]") as (Hin) "HT".
{ iPureIntro. by apply: val_to_Z_in_range. }
move: Hin => /val_of_Z_is_some [v' Hv']. rewrite /i2v Hv' /=.
move: Hin => /val_of_Z_is_Some [v' Hv']. rewrite /i2v Hv' /=.
iApply wp_cast_int => //. iApply ("HΦ" with "[] HT") => //.
iPureIntro. by apply val_to_of_int.
iPureIntro. by apply val_to_of_Z.
Qed.
Global Instance type_cast_int_inst n it1 it2 v:
TypedUnOpVal v (n @ int it1)%I (CastOp (IntOp it2)) (IntOp it1) :=
......@@ -399,13 +399,13 @@ Section programs.
have -> : a b, a b - 1 a < b by lia.
have ? := bits_per_int_gt_0 it.
apply Z_lunot_range; lia. }
rewrite /n => /val_of_Z_is_some [v Hv]. rewrite /i2v Hv /=.
rewrite /n => /val_of_Z_is_Some [v Hv]. rewrite /i2v Hv /=.
iApply (wp_unop_det v). iSplit.
- iIntros (σ v') "_ !%". split.
+ by inversion 1; simplify_eq.
+ move => ->. by econstructor.
- iIntros "!>". iApply "HΦ"; last done. iPureIntro.
by apply val_to_of_int.
by apply val_to_of_Z.
Qed.
Global Instance type_not_int_inst n it v:
TypedUnOpVal v (n @ int it)%I NotIntOp (IntOp it) :=
......@@ -609,7 +609,7 @@ Section offsetof.
Proof.
iIntros "[%Hin HT] %Φ HΦ". move: Hin => /offset_of_from_in [n Hn].
iApply wp_offset_of => //. iIntros "%v %Hv". iApply "HΦ" => //.
iExists _. iSplit; first done. iPureIntro. by apply val_to_of_int.
iExists _. iSplit; first done. iPureIntro. by apply val_to_of_Z.
Qed.
End offsetof.
......
......@@ -172,7 +172,7 @@ Section optional.
iIntros (σ v) "Hctx". iDestruct "HT" as "[Hpre _]".
iDestruct (opt_bin_op true true with "Hpre Hv1 Hv2 Hctx") as %->.
iPureIntro. rewrite /i2v.
have [|v' ->] := val_of_Z_is_some i32 (Z_of_bool false) => //.
have [|v' ->] := val_of_Z_is_Some i32 (Z_of_bool false) => //.
naive_solver.
}
iDestruct "HT" as "[_ [HT _]]".
......@@ -182,7 +182,7 @@ Section optional.
iIntros (σ v) "Hctx". iDestruct "HT" as "[Hpre _]".
iDestruct (opt_bin_op false true with "Hpre Hv1 Hv2 Hctx") as %->.
iPureIntro. rewrite /i2v.
have [|v' ->] := val_of_Z_is_some i32 (Z_of_bool true) => //.
have [|v' ->] := val_of_Z_is_Some i32 (Z_of_bool true) => //.
naive_solver.
}
iDestruct "HT" as "[_ [_ HT]]".
......@@ -199,14 +199,14 @@ Section optional.
typed_bin_op v1 (v1 ◁ᵥ ty) v2 (v2 ◁ᵥ optty) EqOp ot1 ot2 T.
Proof.
iIntros "HT Hv1 Hv2". iIntros (Φ) "HΦ".
have [|v' Hv] := val_of_Z_is_some i32 (Z_of_bool false) => //.
have [|v' Hv] := val_of_Z_is_Some i32 (Z_of_bool false) => //.
iApply (wp_binop_det v'). iSplit. {
iIntros (σ v) "Hctx". iDestruct "HT" as "[Hpre _]".
iDestruct (opt_bin_op true true with "Hpre Hv1 Hv2 Hctx") as %->.
iPureIntro. by split => ?; simpl in *; simplify_eq.
}
iDestruct ("HT" with "Hv1") as "HT".
iApply "HΦ" => //. iPureIntro. by apply val_to_of_int.
iApply "HΦ" => //. iPureIntro. by apply val_to_of_Z.
Qed.
Global Instance type_eq_optional_neq_inst v1 v2 ty optty ot1 ot2 `{!Movable ty} `{!Movable optty} `{!Optionable ty optty ot1 ot2} :
......@@ -225,7 +225,7 @@ Section optional.
iIntros (σ v) "Hctx". iDestruct "HT" as "[Hpre _]".
iDestruct (opt_bin_op true false with "Hpre Hv1 Hv2 Hctx") as %->.
iPureIntro. rewrite /i2v.
have [|v' ->] := val_of_Z_is_some i32 (Z_of_bool true) => //.
have [|v' ->] := val_of_Z_is_Some i32 (Z_of_bool true) => //.
naive_solver.
}
iDestruct "HT" as "[_ [HT _]]".
......@@ -235,7 +235,7 @@ Section optional.
iIntros (σ v) "Hctx". iDestruct "HT" as "[Hpre _]".
iDestruct (opt_bin_op false false with "Hpre Hv1 Hv2 Hctx") as %->.
iPureIntro. rewrite /i2v.
have [|v' ->] := val_of_Z_is_some i32 (Z_of_bool false) => //.
have [|v' ->] := val_of_Z_is_Some i32 (Z_of_bool false) => //.
naive_solver.
}
iDestruct "HT" as "[_ [_ HT]]".
......@@ -375,22 +375,22 @@ Section optionalO.
Proof.
unfold destruct_hint. iIntros "HT Hv1 Hv2". iIntros (Φ) "HΦ".
destruct b.
- have [|v' Hv] := val_of_Z_is_some i32 (Z_of_bool false) => //.
- have [|v' Hv] := val_of_Z_is_Some i32 (Z_of_bool false) => //.
iApply (wp_binop_det v'). iSplit. {
iIntros (σ v) "Hctx". iDestruct "HT" as "[Hpre _]".
iDestruct (opt_bin_op true true with "Hpre [Hv1] [Hv2] Hctx") as %->.
iFrame. iFrame. iPureIntro. by split => ?; simpl in *; simplify_eq.
}
iDestruct ("HT" with "Hv1") as "HT".
iApply "HΦ" => //. iPureIntro. by apply val_to_of_int.
- have [|v' Hv] := val_of_Z_is_some i32 (Z_of_bool true) => //.
iApply "HΦ" => //. iPureIntro. by apply val_to_of_Z.
- have [|v' Hv] := val_of_Z_is_Some i32 (Z_of_bool true) => //.
iApply (wp_binop_det v'). iSplit. {
iIntros (σ v) "Hctx". iDestruct "HT" as "[Hpre _]".
iDestruct (opt_bin_op false true with "Hpre [Hv1] [Hv2] Hctx") as %->.
iFrame. iFrame. iPureIntro. by split => ?; simpl in *; simplify_eq.
}
iDestruct ("HT" with "Hv1") as "HT".
iApply "HΦ" => //. iPureIntro. by apply val_to_of_int.
iApply "HΦ" => //. iPureIntro. by apply val_to_of_Z.
Qed.
Global Instance type_eq_optionalO_inst A v1 v2 (ty : A type) optty ot1 ot2 `{! x, Movable (ty x)} `{!Movable optty} `{! x, Optionable (ty x) optty ot1 ot2} b `{!Inhabited A} :
......@@ -405,22 +405,22 @@ Section optionalO.
Proof.
unfold destruct_hint. iIntros "HT Hv1 Hv2". iIntros (Φ) "HΦ".
destruct b.
- have [|v' Hv] := val_of_Z_is_some i32 (Z_of_bool true) => //.
- have [|v' Hv] := val_of_Z_is_Some i32 (Z_of_bool true) => //.
iApply (wp_binop_det v'). iSplit. {
iIntros (σ v) "Hctx". iDestruct "HT" as "[Hpre _]".
iDestruct (opt_bin_op true false with "Hpre [Hv1] [Hv2] Hctx") as %->.
iFrame. iFrame. iPureIntro. by split => ?; simpl in *; simplify_eq.
}
iDestruct ("HT" with "Hv1") as "HT".
iApply "HΦ" => //. iPureIntro. by apply val_to_of_int.
- have [|v' Hv] := val_of_Z_is_some i32 (Z_of_bool false) => //.
iApply "HΦ" => //. iPureIntro. by apply val_to_of_Z.
- have [|v' Hv] := val_of_Z_is_Some i32 (Z_of_bool false) => //.
iApply (wp_binop_det v'). iSplit. {
iIntros (σ v) "Hctx". iDestruct "HT" as "[Hpre _]".
iDestruct (opt_bin_op false false with "Hpre [Hv1] [Hv2] Hctx") as %->.
iFrame. iFrame. iPureIntro. by split => ?; simpl in *; simplify_eq.
}
iDestruct ("HT" with "Hv1") as "HT".
iApply "HΦ" => //. iPureIntro. by apply val_to_of_int.
iApply "HΦ" => //. iPureIntro. by apply val_to_of_Z.
Qed.
Global Instance type_neq_optionalO_inst A v1 v2 (ty : A type) optty ot1 ot2 `{! x, Movable (ty x)} `{!Movable optty} `{! x, Optionable (ty x) optty ot1 ot2} b `{!Inhabited A} :
TypedBinOp v1 (v1 ◁ᵥ b @ optionalO ty optty)%I v2 (v2 ◁ᵥ optty) NeOp ot1 ot2 :=
......
......@@ -202,12 +202,12 @@ Section own.
Proof.
iIntros "HT Hp" (Φ) "HΦ".
iDestruct (loc_in_bounds_in_bounds with "Hp") as "#Hlib".
iDestruct (loc_in_bounds_in_range_uintptr_t with "Hlib") as %[? H]%val_of_Z_is_some.
iDestruct (loc_in_bounds_in_range_uintptr_t with "Hlib") as %[? H]%val_of_Z_is_Some.
iDestruct (loc_in_bounds_ptr_in_range with "Hlib") as %?.
iDestruct ("HT" with "[] Hp") as "HT"; first done.
iApply wp_cast_ptr_int => //=; first by rewrite val_to_of_loc.
rewrite /i2v H /=. iApply ("HΦ" with "[] [HT]"); last done.
iPureIntro. by apply val_to_of_int.
iPureIntro. by apply val_to_of_Z.
Qed.
Global Instance type_cast_ptr_int_inst (p : loc) β ty n `{!LocInBounds ty β n}:
TypedUnOp p (p ◁ₗ{β} ty)%I (CastOp (IntOp uintptr_t)) PtrOp :=
......@@ -447,12 +447,12 @@ Section ptr.
Proof.
iIntros "HT Hp" (Φ) "HΦ".
iDestruct "Hp" as "[-> #Hlib]".
iDestruct (loc_in_bounds_in_range_uintptr_t with "Hlib") as %[? H]%val_of_Z_is_some.
iDestruct (loc_in_bounds_in_range_uintptr_t with "Hlib") as %[? H]%val_of_Z_is_Some.
iDestruct (loc_in_bounds_ptr_in_range with "Hlib") as %?.
iDestruct ("HT" with "[] []") as "HT"; first done. { by iFrame "Hlib". }
iApply wp_cast_ptr_int => //=; first by rewrite val_to_of_loc.
rewrite /i2v H /=. iApply ("HΦ" with "[] [HT]"); last done.
iPureIntro. by apply val_to_of_int.
iPureIntro. by apply val_to_of_Z.
Qed.
Global Instance type_cast_ptr_int_val_inst (v : val) (p : loc) n:
TypedUnOp v (v ◁ᵥ p @ ptr n)%I (CastOp (IntOp uintptr_t)) PtrOp :=
......
Supports Markdown
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