Commit 8a6281e3 authored by Rodolphe Lepigre's avatar Rodolphe Lepigre
Browse files

Renaming of val_[to|of]int into val_[to|of]_Z.

This was done using the following sed commands (with ZSH ** pattern):
> sed -i 's/val_of_int/val_of_Z/g' **/*.v
> sed -i 's/val_to_int/val_to_Z/g' **/*.v
parent f463b946
Pipeline #44950 passed with stage
in 31 minutes and 14 seconds
......@@ -21,8 +21,8 @@ Section type.
iDestruct ("HT" with "Hty2") as (Hv2) "HT".
iIntros (Φ) "HΦ".
iDestruct ("HT" with "[] []" ) as (??) "HT".
1-2: iPureIntro; by apply: val_of_int_in_range.
have /val_of_int_is_some[v Hv] : ((n1 + n2) `mod` int_modulus it1) it1 by apply int_modulus_mod_in_range.
1-2: iPureIntro; by apply: val_of_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.
move: Hv1 Hv2 => /val_to_of_int Hv1 /val_to_of_int Hv2. subst it2.
iApply (wp_binop_det v). iSplit.
- iIntros (σ v') "_ !%". split.
......
......@@ -382,7 +382,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_of_int_in_range. }
{ rewrite /ty_own_val /=. by iDestruct "Hv" as %Hv%val_of_Z_in_range. }
iAssert (owner < next)%I as %?.
{ destruct (decide (owner < next)); first done. iExFalso.
iDestruct (ty_size_eq with "Hv") as %?.
......@@ -484,7 +484,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_of_int_in_range in Hnext as [??]. lia. }
iPureIntro. apply val_of_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]".
......@@ -511,7 +511,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_of_int_in_range. destruct Howner as [Howner ?].
iDestruct "Hv" as %Howner%val_of_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.
split => //. rewrite /min_int /= in Howner. lia. }
......@@ -558,7 +558,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_of_int_in_range.
iDestruct "Hv" as %?%val_of_Z_in_range.
iSplitL "Hl". { iExists _. by iFrame "Hl". }
iIntros "!> Hl".
iMod "Hclose" as "_". iMod ("Hclose_inv" with "[Htok H● H◯ Hticket Hnext Hl Htk1 Htk2]") as "_".
......@@ -568,8 +568,8 @@ Section proofs.
iSplit. { iPureIntro. by lia. }
iDestruct ((ty_ref (t := (owner + 1) @ int u16)) with "[] Hl []") as "$" => //.
{ iPureIntro. rewrite /i2v.
destruct (val_of_int (owner + 1) u16) eqn:Heq => //. exfalso.
assert (owner + 1 u16) as Hu16%val_of_int_is_some by (split; lia).
destruct (val_of_Z (owner + 1) u16) eqn:Heq => //. 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.
......
......@@ -227,37 +227,37 @@ 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_int 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? *)
0 o
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_int 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? *)
eval_bin_op (PtrNegOffsetOp ly) (IntOp it) PtrOp σ v1 v2 (val_of_loc (l offset{ly} -o))
| EqOpPNull v1 v2 σ l v:
heap_state_loc_in_bounds l 0%nat σ.(st_heap)
val_to_loc v1 = Some l
val_to_int v2 size_t = Some 0
val_to_Z v2 size_t = Some 0
(* TODO ( see below ): Should we really hard code i32 here because of C? *)
i2v (Z_of_bool false) i32 = 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
val_to_int v2 size_t = Some 0
val_to_Z v2 size_t = Some 0
i2v (Z_of_bool true) i32 = v
eval_bin_op NeOp PtrOp PtrOp σ v1 v2 v
| EqOpNullNull v1 v2 σ v:
val_to_int v1 size_t = Some 0
val_to_int v2 size_t = Some 0
val_to_Z v1 size_t = Some 0
val_to_Z v2 size_t = Some 0
i2v (Z_of_bool true) i32 = v
eval_bin_op EqOp PtrOp PtrOp σ v1 v2 v
| NeOpNullNull v1 v2 σ v:
val_to_int v1 size_t = Some 0
val_to_int v2 size_t = Some 0
val_to_Z v1 size_t = Some 0
val_to_Z v2 size_t = Some 0
i2v (Z_of_bool false) i32 = v
eval_bin_op NeOp PtrOp PtrOp σ v1 v2 v
| RelOpPP v1 v2 σ l1 l2 v b op:
......@@ -285,8 +285,8 @@ 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_int v1 it = Some n1
val_to_int 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)
......@@ -314,16 +314,16 @@ 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_int v1 it = Some n1
val_to_int v2 it = Some n2
val_of_int (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 = Some v
eval_bin_op op (IntOp it) (IntOp it) σ v1 v2 v
.
Inductive eval_un_op : un_op op_type state val val Prop :=
| CastOpII itt its σ vs vt n:
val_to_int vs its = Some n
val_of_int n itt = Some vt
val_to_Z vs its = Some n
val_of_Z n itt = Some vt
eval_un_op (CastOp (IntOp itt)) (IntOp its) σ vs vt
| CastOpPP σ vs vt l:
val_to_loc vs = Some l
......@@ -331,19 +331,19 @@ Inductive eval_un_op : un_op → op_type → state → val → val → Prop :=
eval_un_op (CastOp PtrOp) PtrOp σ vs vt
| CastOpPI it σ vs vt l:
val_to_loc vs = Some l
val_of_int l.2 it = Some vt
val_of_Z l.2 it = Some vt
eval_un_op (CastOp (IntOp it)) PtrOp σ vs vt
| CastOpIP it σ vs vt n:
val_to_int vs it = Some n
val_to_Z vs it = Some n
val_of_loc (None, n) = vt
eval_un_op (CastOp PtrOp) (IntOp it) σ vs vt
| NegOpI it σ vs vt n:
val_to_int vs it = Some n
val_of_int (-n) it = Some vt
val_to_Z vs it = Some n
val_of_Z (-n) it = Some vt
eval_un_op NegOp (IntOp it) σ vs vt
| NotIntOpI it σ vs vt n:
val_to_int vs it = Some n
val_of_int (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 = Some vt
eval_un_op NotIntOp (IntOp it) σ vs vt
.
......@@ -380,8 +380,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_int vo it = Some z1
val_to_int 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
......@@ -392,8 +392,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_int vo it = Some z1
val_to_int 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
......@@ -430,7 +430,7 @@ comparing pointers? (see lambda rust) *)
val_to_loc v2 = Some l2
expr_step (CopyAllocId (Val v1) (Val v2)) σ [] (Val (val_of_loc (l2.1, l1.2))) σ []
| IfES v it e1 e2 n σ:
val_to_int 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 *)
.
......@@ -447,7 +447,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_int 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 :
......
......@@ -240,7 +240,7 @@ Qed.
val_to_loc vl2 = Some l2 →
(bytes_per_int it ≤ bytes_per_addr)%nat →
(|={E, ∅}=> ∃ (q1 q2 : Qp) vo ve z1 z2,
⌜val_to_int vo it = Some z1⌝ ∗ ⌜val_to_int ve it = Some z2⌝ ∗
⌜val_to_Z vo it = Some z1⌝ ∗ ⌜val_to_Z ve it = Some z2⌝ ∗
⌜l1 `has_layout_loc` it_layout it⌝ ∗ ⌜l2 `has_layout_loc` it_layout it⌝ ∗
⌜length vd = bytes_per_int it⌝ ∗ ⌜if bool_decide (z1 = z2) then q1 = 1%Qp else q2 = 1%Qp⌝ ∗
l1↦{q1}vo ∗ l2↦{q2}ve ∗ ▷ (
......@@ -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_int vo it = Some z1
val_to_int 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_int_length ? /val_to_int_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_int vo it = Some z1
val_to_int 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_int_length ? /val_to_int_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_int v it = Some n
val_of_int (-n) it = Some v'
val_to_Z v it = Some n
val_of_Z (-n) it = 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' n E its itt:
val_to_int v its = Some n
val_of_int n itt = Some v'
val_to_Z v its = Some n
val_of_Z n itt = Some v'
Φ (v') - WP UnOp (CastOp (IntOp itt)) (IntOp its) (Val v) @ E {{ Φ }}.
Proof.
iIntros (Hv Hv') "HΦ".
......@@ -349,7 +349,7 @@ Qed.
Lemma wp_cast_ptr_int Φ v v' l E it:
val_to_loc v = Some l
val_of_int l.2 it = Some v'
val_of_Z l.2 it = Some v'
Φ (v') - WP UnOp (CastOp (IntOp it)) PtrOp (Val v) @ E {{ Φ }}.
Proof.
iIntros (Hv Hv') "HΦ".
......@@ -360,7 +360,7 @@ Proof.
Qed.
Lemma wp_cast_int_ptr Φ v n E it:
val_to_int v it = Some n
val_to_Z v it = Some n
Φ (val_of_loc (None, n)) - WP UnOp (CastOp PtrOp) (IntOp it) (Val v) @ E {{ Φ }}.
Proof.
iIntros (Hv) "HΦ".
......@@ -414,7 +414,7 @@ Qed.
Lemma wp_ptr_offset Φ vl l E it o ly vo:
val_to_loc vl = Some l
val_to_int vo it = Some o
val_to_Z vo it = Some o
0 o
Φ (val_of_loc (l offset{ly} o)) - WP Val vl at_offset{ ly , PtrOp, IntOp it} Val vo @ E {{ Φ }}.
Proof.
......@@ -427,7 +427,7 @@ Qed.
Lemma wp_ptr_neg_offset Φ vl l E it o ly vo:
val_to_loc vl = Some l
val_to_int vo it = Some o
val_to_Z vo it = Some o
Φ (val_of_loc (l offset{ly} -o)) - WP Val vl at_neg_offset{ ly , PtrOp, IntOp it} Val vo @ E {{ Φ }}.
Proof.
iIntros (Hvl Hvo) "HΦ".
......@@ -444,7 +444,7 @@ 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_int_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.
}
......@@ -462,11 +462,11 @@ Proof. iIntros (->%val_of_to_loc) "?". rewrite /GetMemberUnion/GetMemberUnionLoc
Lemma wp_offset_of Φ s m i E:
offset_of s.(sl_members) m = Some i
( v, val_of_int i size_t = Some v - Φ v) -
( v, val_of_Z i size_t = Some v - Φ v) -
WP OffsetOf s m @ E {{ Φ }}.
Proof.
rewrite /OffsetOf. iIntros (Ho) "HΦ".
have [|? Hs]:= (val_of_int_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.
......@@ -480,7 +480,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_int 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.
......@@ -778,7 +778,7 @@ Proof.
Qed.
Lemma wps_switch Q Ψ v n ss def m it:
val_to_int 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.
......@@ -791,7 +791,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_int v it = Some n
val_to_Z v it = Some n
map_Forall (λ _ i, is_Some (ss !! i)) m
([ list] isss, m !! n = Some i - WPs s {{ Q, Ψ }})
(m !! n = None - WPs def {{ Q, Ψ }}) -
......@@ -806,7 +806,7 @@ Proof.
Qed.
Lemma wps_if Q Ψ v s1 s2 n:
val_to_int 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.
......@@ -816,7 +816,7 @@ Proof.
Qed.
Lemma wps_assert Q Ψ v s n:
val_to_int 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.
......
......@@ -316,7 +316,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_int (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))))%E.
Notation "e 'at{' s } m" := (GetMember e%E s m) (at level 10, format "e 'at{' s } m") : expr_scope.
Typeclasses Opaque GetMember.
Arguments GetMember : simpl never.
......@@ -328,7 +328,7 @@ Typeclasses Opaque GetMemberLoc.
Arguments GetMemberLoc : simpl never.
Definition OffsetOf (s : struct_layout) (m : var_name) : expr :=
(default StuckE (Val <$> (offset_of s.(sl_members) m) = (λ m, val_of_int (Z.of_nat m) size_t)))%E.
(default StuckE (Val <$> (offset_of s.(sl_members) m) = (λ m, val_of_Z (Z.of_nat m) size_t)))%E.
Typeclasses Opaque OffsetOf.
Arguments OffsetOf : simpl never.
......
......@@ -548,7 +548,7 @@ Proof.
end; done.
- rewrite /notation.OffsetOf/=.
match goal with | |- context [offset_of ?s ?m] => destruct (offset_of s m) end => //=.
by match goal with | |- context [val_of_int ?o ?it] => destruct (val_of_int o it) end.
by match goal with | |- context [val_of_Z ?o ?it] => destruct (val_of_Z o it) end.
- (** AnnotExpr *)
match goal with
| |- notation.AnnotExpr ?n _ _ = _ => generalize dependent n
......
......@@ -66,50 +66,50 @@ Arguments val_to_loc : simpl never.
(* TODO: we currently assume little-endian, make this more generic. *)
Fixpoint val_to_int_go v : option Z :=
Fixpoint val_to_Z_go v : option Z :=
match v with
| [] => Some 0
| MByte b :: v => z val_to_int_go v; Some (byte_modulus * z + b.(byte_val))
| MByte b :: v => z val_to_Z_go v; Some (byte_modulus * z + b.(byte_val))
| _ => None
end.
Definition val_to_int (v : val) (it : int_type) : option Z :=
Definition val_to_Z (v : val) (it : int_type) : option Z :=
if decide (length v = bytes_per_int it) then
z val_to_int_go v;
z val_to_Z_go v;
if it.(it_signed) && bool_decide (int_half_modulus it z) then
Some (z - int_modulus it)
else
Some z
else None.
Program Fixpoint val_of_int_go (n : Z) (sz : nat) : val :=
Program Fixpoint val_of_Z_go (n : Z) (sz : nat) : val :=
match sz return _ with
| O => []
| S sz => MByte {| byte_val := (n `mod` byte_modulus) |}
:: val_of_int_go (n / byte_modulus) sz
:: val_of_Z_go (n / byte_modulus) sz
end.
Next Obligation. move => n. have [] := Z_mod_lt n byte_modulus => //*. lia. Qed.
Definition val_of_int (z : Z) (it : int_type) : option val :=
Definition val_of_Z (z : Z) (it : int_type) : option val :=
if bool_decide (z it) then
let p := if bool_decide (z < 0) then z + int_modulus it else z in
Some (val_of_int_go p (bytes_per_int it))
Some (val_of_Z_go p (bytes_per_int it))
else
None.
Definition i2v (n : Z) (it : int_type) : val :=
default [MPoison] (val_of_int n it).
default [MPoison] (val_of_Z n it).
Definition val_of_bool (b : bool) : val :=
i2v (Z_of_bool b) bool_it.
Lemma val_of_int_go_length z sz :
length (val_of_int_go z sz) = sz.
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) :
0 z < 2 ^ (sz * bits_per_byte)
val_to_int_go (val_of_int_go z sz) = Some z.
val_to_Z_go (val_of_Z_go z sz) = Some z.
Proof.
rewrite /bits_per_byte.
elim: sz z => /=. 1: rewrite /Z.of_nat; move => ??; f_equal; lia.
......@@ -119,34 +119,34 @@ Proof.
lia.
Qed.
Lemma val_of_int_length z it v:
val_of_int z it = Some v length v = bytes_per_int it.
Lemma val_of_Z_length z it v:
val_of_Z z it = Some v length v = bytes_per_int it.
Proof.
rewrite /val_of_int => Hv. case_bool_decide => //. simplify_eq.
by rewrite val_of_int_go_length.
rewrite /val_of_Z => Hv. case_bool_decide => //. simplify_eq.
by rewrite val_of_Z_go_length.
Qed.
Lemma val_to_int_length v it z:
val_to_int v it = Some z length v = bytes_per_int it.
Proof. rewrite /val_to_int. by case_decide. Qed.
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_int_is_some it z:
z it is_Some (val_of_int z it).
Proof. rewrite /val_of_int. case_bool_decide; by eauto. Qed.
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.
Lemma val_of_int_in_range it z v:
val_of_int z it = Some v z it.
Proof. rewrite /val_of_int. case_bool_decide; by eauto. Qed.
Lemma val_of_Z_in_range it z v:
val_of_Z z it = Some v z it.
Proof. rewrite /val_of_Z. case_bool_decide; by eauto. Qed.
Lemma val_to_of_int z it v:
val_of_int z it = Some v val_to_int v it = Some z.
val_of_Z z it = Some v val_to_Z v it = Some z.
Proof.
rewrite /val_of_int /val_to_int => Ht.
rewrite /val_of_Z /val_to_Z => Ht.
destruct (bool_decide (z it)) eqn: Hr => //. simplify_eq.
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_int_go_length val_to_of_int_go /=.
rewrite val_of_Z_go_length val_to_of_int_go /=.
- case_decide as H => //. clear H.
destruct (it_signed it) eqn:Hs => /=.
+ case_decide => /=; last (rewrite bool_decide_false //; lia).
......@@ -164,27 +164,27 @@ Proof.
+ rewrite /int_modulus /bits_per_int in HM. lia.
Qed.
Lemma val_of_int_bool b it:
val_of_int (Z_of_bool b) it = Some (i2v (Z_of_bool b) it).
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_int_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.
Qed.
Lemma val_to_int_bool b :
val_to_int (val_of_bool b) bool_it = Some (Z_of_bool b).
Lemma val_to_Z_bool b :
val_to_Z (val_of_bool b) bool_it = Some (Z_of_bool b).
Proof. by destruct b.