# Module ValueDomain

Require Import FunInd.
Require Import Zwf Coqlib Maps Zbits Integers Floats Lattice.
Require Import Compopts AST.
Require Import Values Memory Globalenvs Builtins Events.
Require Import Registers RTL.
Require Import Lia.

The abstract domains for value analysis

Inductive block_class : Type :=
| BCinvalid
| BCglob (id: ident)
| BCstack
| BCother.

Definition block_class_eq: forall (x y: block_class), {x=y} + {x<>y}.
Proof.
decide equality. apply peq. Defined.

Record block_classification : Type := BC {
bc_img :> block -> block_class;
bc_stack: forall b1 b2, bc_img b1 = BCstack -> bc_img b2 = BCstack -> b1 = b2;
bc_glob: forall b1 b2 id, bc_img b1 = BCglob id -> bc_img b2 = BCglob id -> b1 = b2
}.

Definition bc_below (bc: block_classification) (bound: block) : Prop :=
forall b, bc b <> BCinvalid -> Plt b bound.

Lemma bc_below_invalid:
forall b bc bound, ~Plt b bound -> bc_below bc bound -> bc b = BCinvalid.
Proof.
intros. destruct (block_class_eq (bc b) BCinvalid); auto.
elim H. apply H0; auto.
Qed.

Global Hint Extern 2 (_ = _) => congruence : va.
Global Hint Extern 2 (_ <> _) => congruence : va.
Global Hint Extern 2 (_ < _) => extlia : va.
Global Hint Extern 2 (_ <= _) => extlia : va.
Global Hint Extern 2 (_ > _) => extlia : va.
Global Hint Extern 2 (_ >= _) => extlia : va.

Section MATCH.

Variable bc: block_classification.

# Abstracting the result of conditions (type option bool)

Inductive abool :=
| Bnone (* always None (undefined) *)
| Just (b: bool) (* always Some b (defined and known to be b) *)
| Maybe (b: bool) (* either None or Some b (known to be b if defined) *)
| Btop. (* unknown, all results are possible *)

Inductive cmatch: option bool -> abool -> Prop :=
| cmatch_none: cmatch None Bnone
| cmatch_just: forall b, cmatch (Some b) (Just b)
| cmatch_maybe_none: forall b, cmatch None (Maybe b)
| cmatch_maybe_some: forall b, cmatch (Some b) (Maybe b)
| cmatch_top: forall ob, cmatch ob Btop.

Hint Constructors cmatch : va.

Definition club (x y: abool) : abool :=
match x, y with
| Bnone, Bnone => Bnone
| Bnone, (Just b | Maybe b) => Maybe b
| (Just b | Maybe b), Bnone => Maybe b
| Just b1, Just b2 => if eqb b1 b2 then x else Btop
| Maybe b1, Maybe b2 => if eqb b1 b2 then x else Btop
| Maybe b1, Just b2 => if eqb b1 b2 then x else Btop
| Just b1, Maybe b2 => if eqb b1 b2 then y else Btop
| _, _ => Btop
end.

Lemma cmatch_lub_l:
forall ob x y, cmatch ob x -> cmatch ob (club x y).
Proof.
intros. unfold club; inv H; destruct y; try constructor;
destruct (eqb b b0) eqn:EQ; try constructor.
replace b0 with b by (apply eqb_prop; auto). constructor.
Qed.

Lemma cmatch_lub_r:
forall ob x y, cmatch ob y -> cmatch ob (club x y).
Proof.
intros. unfold club; inv H; destruct x; try constructor;
destruct (eqb b0 b) eqn:EQ; try constructor.
replace b with b0 by (apply eqb_prop; auto). constructor.
replace b with b0 by (apply eqb_prop; auto). constructor.
replace b with b0 by (apply eqb_prop; auto). constructor.
Qed.

Definition cnot (x: abool) : abool :=
match x with
| Just b => Just (negb b)
| Maybe b => Maybe (negb b)
| _ => x
end.

Lemma cnot_sound:
forall ob x, cmatch ob x -> cmatch (option_map negb ob) (cnot x).
Proof.
destruct 1; constructor.
Qed.

# Abstracting pointers

Inductive aptr : Type :=
| Pbot (* bottom (empty set of pointers) *)
| Gl (id: ident) (ofs: ptrofs) (* pointer into the block for global variable id at offset ofs *)
| Glo (id: ident) (* pointer anywhere into the block for global id *)
| Glob (* pointer into any global variable *)
| Stk (ofs: ptrofs) (* pointer into the current stack frame at offset ofs *)
| Stack (* pointer anywhere into the current stack frame *)
| Nonstack (* pointer anywhere but into the current stack frame *)
| Ptop. (* any valid pointer *)

Definition eq_aptr: forall (p1 p2: aptr), {p1=p2} + {p1<>p2}.
Proof.
intros. generalize ident_eq, Ptrofs.eq_dec; intros. decide equality.
Defined.

Inductive pmatch (b: block) (ofs: ptrofs): aptr -> Prop :=
| pmatch_gl: forall id,
bc b = BCglob id ->
pmatch b ofs (Gl id ofs)
| pmatch_glo: forall id,
bc b = BCglob id ->
pmatch b ofs (Glo id)
| pmatch_glob: forall id,
bc b = BCglob id ->
pmatch b ofs Glob
| pmatch_stk:
bc b = BCstack ->
pmatch b ofs (Stk ofs)
| pmatch_stack:
bc b = BCstack ->
pmatch b ofs Stack
| pmatch_nonstack:
bc b <> BCstack -> bc b <> BCinvalid ->
pmatch b ofs Nonstack
| pmatch_top:
bc b <> BCinvalid ->
pmatch b ofs Ptop.

Hint Constructors pmatch: va.

Inductive pge: aptr -> aptr -> Prop :=
| pge_top: forall p, pge Ptop p
| pge_bot: forall p, pge p Pbot
| pge_refl: forall p, pge p p
| pge_glo_gl: forall id ofs, pge (Glo id) (Gl id ofs)
| pge_glob_gl: forall id ofs, pge Glob (Gl id ofs)
| pge_glob_glo: forall id, pge Glob (Glo id)
| pge_ns_gl: forall id ofs, pge Nonstack (Gl id ofs)
| pge_ns_glo: forall id, pge Nonstack (Glo id)
| pge_ns_glob: pge Nonstack Glob
| pge_stack_stk: forall ofs, pge Stack (Stk ofs).

Hint Constructors pge: va.

Lemma pge_trans:
forall p q, pge p q -> forall r, pge q r -> pge p r.
Proof.
induction 1; intros r PM; inv PM; auto with va.
Qed.

Lemma pmatch_ge:
forall b ofs p q, pge p q -> pmatch b ofs q -> pmatch b ofs p.
Proof.
induction 1; intros PM; inv PM; eauto with va.
Qed.

Lemma pmatch_top': forall b ofs p, pmatch b ofs p -> pmatch b ofs Ptop.
Proof.
intros. apply pmatch_ge with p; auto with va.
Qed.

Definition plub (p q: aptr) : aptr :=
match p, q with
| Pbot, _ => q
| _, Pbot => p
| Gl id1 ofs1, Gl id2 ofs2 =>
if ident_eq id1 id2 then if Ptrofs.eq_dec ofs1 ofs2 then p else Glo id1 else Glob
| Gl id1 ofs1, Glo id2 =>
if ident_eq id1 id2 then q else Glob
| Glo id1, Gl id2 ofs2 =>
if ident_eq id1 id2 then p else Glob
| Glo id1, Glo id2 =>
if ident_eq id1 id2 then p else Glob
| (Gl _ _ | Glo _ | Glob), Glob => Glob
| Glob, (Gl _ _ | Glo _) => Glob
| (Gl _ _ | Glo _ | Glob | Nonstack), Nonstack =>
Nonstack
| Nonstack, (Gl _ _ | Glo _ | Glob) =>
Nonstack
| Stk ofs1, Stk ofs2 =>
if Ptrofs.eq_dec ofs1 ofs2 then p else Stack
| (Stk _ | Stack), Stack =>
Stack
| Stack, Stk _ =>
Stack
| _, _ => Ptop
end.

Lemma plub_comm:
forall p q, plub p q = plub q p.
Proof.
intros; unfold plub; destruct p; destruct q; auto.
destruct (ident_eq id id0). subst id0.
rewrite dec_eq_true.
destruct (Ptrofs.eq_dec ofs ofs0). subst ofs0. rewrite dec_eq_true. auto.
rewrite dec_eq_false by auto. auto.
rewrite dec_eq_false by auto. auto.
destruct (ident_eq id id0). subst id0.
rewrite dec_eq_true; auto.
rewrite dec_eq_false; auto.
destruct (ident_eq id id0). subst id0.
rewrite dec_eq_true; auto.
rewrite dec_eq_false; auto.
destruct (ident_eq id id0). subst id0.
rewrite dec_eq_true; auto.
rewrite dec_eq_false; auto.
destruct (Ptrofs.eq_dec ofs ofs0). subst ofs0. rewrite dec_eq_true; auto.
rewrite dec_eq_false; auto.
Qed.

Lemma pge_lub_l:
forall p q, pge (plub p q) p.
Proof.
unfold plub; destruct p, q; auto with va.
- destruct (ident_eq id id0).
destruct (Ptrofs.eq_dec ofs ofs0); subst; constructor.
constructor.
- destruct (ident_eq id id0); subst; constructor.
- destruct (ident_eq id id0); subst; constructor.
- destruct (ident_eq id id0); subst; constructor.
- destruct (Ptrofs.eq_dec ofs ofs0); subst; constructor.
Qed.

Lemma pge_lub_r:
forall p q, pge (plub p q) q.
Proof.
intros. rewrite plub_comm. apply pge_lub_l.
Qed.

Lemma pmatch_lub_l:
forall b ofs p q, pmatch b ofs p -> pmatch b ofs (plub p q).
Proof.
intros. eapply pmatch_ge; eauto. apply pge_lub_l.
Qed.

Lemma pmatch_lub_r:
forall b ofs p q, pmatch b ofs q -> pmatch b ofs (plub p q).
Proof.
intros. eapply pmatch_ge; eauto. apply pge_lub_r.
Qed.

Lemma plub_least:
forall r p q, pge r p -> pge r q -> pge r (plub p q).
Proof.
intros. inv H; inv H0; simpl; try constructor.
- destruct p; constructor.
- unfold plub; destruct q; repeat rewrite dec_eq_true; constructor.
- rewrite dec_eq_true; constructor.
- rewrite dec_eq_true; constructor.
- rewrite dec_eq_true. destruct (Ptrofs.eq_dec ofs ofs0); constructor.
- destruct (ident_eq id id0). destruct (Ptrofs.eq_dec ofs ofs0); constructor. constructor.
- destruct (ident_eq id id0); constructor.
- destruct (ident_eq id id0); constructor.
- destruct (ident_eq id id0); constructor.
- destruct (ident_eq id id0). destruct (Ptrofs.eq_dec ofs ofs0); constructor. constructor.
- destruct (ident_eq id id0); constructor.
- destruct (ident_eq id id0); constructor.
- destruct (ident_eq id id0); constructor.
- destruct (Ptrofs.eq_dec ofs ofs0); constructor.
Qed.

Definition pglb (p q: aptr) : aptr :=
match p, q with
| Ptop, _ => q
| _, Ptop => p
| Gl id1 ofs1, Gl id2 ofs2 =>
if ident_eq id1 id2 && Ptrofs.eq_dec ofs1 ofs2
then p
else Pbot
| Gl id1 _, Glo id2 =>
if ident_eq id1 id2 then p else Pbot
| Glo id1, Gl id2 _ =>
if ident_eq id1 id2 then q else Pbot
| Glo id1, Glo id2 =>
if ident_eq id1 id2 then p else Pbot
| (Gl _ _ | Glo _ | Glob), Glob => p
| Glob, (Gl _ _ | Glo _) => q
| (Gl _ _ | Glo _ | Glob | Nonstack), Nonstack => p
| Nonstack, (Gl _ _ | Glo _ | Glob) => q
| Stk ofs1, Stk ofs2 =>
if Ptrofs.eq_dec ofs1 ofs2 then p else Pbot
| (Stk _ | Stack), Stack => p
| Stack, (Stk _) => q
| _, _ => Pbot
end.

Lemma pge_glb_l :
forall p q, pge p (pglb p q).
Proof.
destruct p; destruct q; cbn; try constructor.
- destruct ident_eq; cbn.
+ destruct Ptrofs.eq_dec; cbn; constructor.
+ constructor.
- destruct ident_eq; cbn; constructor.
- destruct ident_eq; cbn.
+ subst id. constructor.
+ constructor.
- destruct ident_eq; cbn; constructor.
- destruct Ptrofs.eq_dec; cbn; constructor.
Qed.

Lemma pge_glb_r :
forall p q, pge q (pglb p q).
Proof.
destruct p; destruct q; cbn; try constructor.
- destruct ident_eq; cbn.
+ subst.
destruct Ptrofs.eq_dec; cbn; subst; constructor.
+ constructor.
- destruct ident_eq; cbn; subst; constructor.
- destruct ident_eq; cbn; subst; constructor.
- destruct ident_eq; cbn; subst; constructor.
- destruct Ptrofs.eq_dec; cbn; subst; constructor.
Qed.

Lemma pglb_greatest:
forall r p q, pge p r -> pge q r -> pge (pglb p q) r.
Proof.
intros. inv H; inv H0; simpl; try constructor.
- destruct r; constructor.
- destruct r; cbn; try constructor.
+ destruct ident_eq; destruct Ptrofs.eq_dec; subst; cbn; try congruence; constructor.
+ destruct ident_eq; subst; cbn; try congruence; constructor.
+ destruct Ptrofs.eq_dec; subst; cbn; try congruence; constructor.
- destruct ident_eq; subst; cbn; try congruence; constructor.
- destruct ident_eq; subst; cbn; try congruence; constructor.
- destruct ident_eq; subst; cbn; try congruence; constructor.
Qed.

Lemma pmatch_glb:
forall b ofs p1 p2
(MATCH1 : pmatch b ofs p1)
(MATCH2 : pmatch b ofs p2),
pmatch b ofs (pglb p1 p2).
Proof.
intros.
inv MATCH1; inv MATCH2; cbn.
all: try (try destruct ident_eq ; try destruct Ptrofs.eq_dec; cbn; subst; try congruence; constructor; auto).
all: econstructor; eassumption.
Qed.

Definition pincl (p q: aptr) : bool :=
match p, q with
| Pbot, _ => true
| Gl id1 ofs1, Gl id2 ofs2 => peq id1 id2 && Ptrofs.eq_dec ofs1 ofs2
| Gl id1 ofs1, Glo id2 => peq id1 id2
| Glo id1, Glo id2 => peq id1 id2
| (Gl _ _ | Glo _ | Glob), Glob => true
| (Gl _ _ | Glo _ | Glob | Nonstack), Nonstack => true
| Stk ofs1, Stk ofs2 => Ptrofs.eq_dec ofs1 ofs2
| Stk ofs1, Stack => true
| Stack, Stack => true
| _, Ptop => true
| _, _ => false
end.

Lemma pincl_ge: forall p q, pincl p q = true -> pge q p.
Proof.
unfold pincl; destruct p, q; intros; try discriminate; auto with va;
InvBooleans; subst; auto with va.
Qed.

Lemma ge_pincl: forall p q, pge p q -> pincl q p = true.
Proof.
destruct 1; simpl; auto.
- destruct p; auto.
- destruct p; simpl; auto; rewrite ! proj_sumbool_is_true; auto.
- rewrite ! proj_sumbool_is_true; auto.
Qed.

Lemma pincl_sound:
forall b ofs p q,
pincl p q = true -> pmatch b ofs p -> pmatch b ofs q.
Proof.
intros. eapply pmatch_ge; eauto. apply pincl_ge; auto.
Qed.

Definition padd (p: aptr) (n: ptrofs) : aptr :=
match p with
| Gl id ofs => Gl id (Ptrofs.add ofs n)
| Stk ofs => Stk (Ptrofs.add ofs n)
| _ => p
end.

forall b ofs p delta,
pmatch b ofs p ->
Proof.
intros. inv H; simpl padd; eauto with va.
Qed.

Definition psub (p: aptr) (n: ptrofs) : aptr :=
match p with
| Gl id ofs => Gl id (Ptrofs.sub ofs n)
| Stk ofs => Stk (Ptrofs.sub ofs n)
| _ => p
end.

Lemma psub_sound:
forall b ofs p delta,
pmatch b ofs p ->
pmatch b (Ptrofs.sub ofs delta) (psub p delta).
Proof.
intros. inv H; simpl psub; eauto with va.
Qed.

Definition poffset (p: aptr) : aptr :=
match p with
| Gl id ofs => Glo id
| Stk ofs => Stack
| _ => p
end.

Lemma poffset_sound:
forall b ofs1 ofs2 p,
pmatch b ofs1 p ->
pmatch b ofs2 (poffset p).
Proof.
intros. inv H; simpl poffset; eauto with va.
Qed.

Definition cmp_different_blocks (c: comparison) : abool :=
match c with
| Ceq => Maybe false
| Cne => Maybe true
| _ => Bnone
end.

Lemma cmp_different_blocks_none:
forall c, cmatch None (cmp_different_blocks c).
Proof.
intros; destruct c; constructor.
Qed.

Lemma cmp_different_blocks_sound:
forall c, cmatch (Val.cmp_different_blocks c) (cmp_different_blocks c).
Proof.
intros; destruct c; constructor.
Qed.

Definition pcmp (c: comparison) (p1 p2: aptr) : abool :=
match p1, p2 with
| Pbot, _ | _, Pbot => Bnone
| Gl id1 ofs1, Gl id2 ofs2 =>
if peq id1 id2 then Maybe (Ptrofs.cmpu c ofs1 ofs2)
else cmp_different_blocks c
| Gl id1 ofs1, Glo id2 =>
if peq id1 id2 then Btop else cmp_different_blocks c
| Glo id1, Gl id2 ofs2 =>
if peq id1 id2 then Btop else cmp_different_blocks c
| Glo id1, Glo id2 =>
if peq id1 id2 then Btop else cmp_different_blocks c
| Stk ofs1, Stk ofs2 => Maybe (Ptrofs.cmpu c ofs1 ofs2)
| (Gl _ _ | Glo _ | Glob | Nonstack), (Stk _ | Stack) => cmp_different_blocks c
| (Stk _ | Stack), (Gl _ _ | Glo _ | Glob | Nonstack) => cmp_different_blocks c
| _, _ => Btop
end.

Lemma pcmp_sound:
forall valid c b1 ofs1 p1 b2 ofs2 p2,
pmatch b1 ofs1 p1 -> pmatch b2 ofs2 p2 ->
cmatch (Val.cmpu_bool valid c (Vptr b1 ofs1) (Vptr b2 ofs2)) (pcmp c p1 p2).
Proof.
intros.
assert (DIFF: b1 <> b2 ->
cmatch (Val.cmpu_bool valid c (Vptr b1 ofs1) (Vptr b2 ofs2))
(cmp_different_blocks c)).
{
intros. simpl. rewrite dec_eq_false by assumption.
destruct Archi.ptr64.
apply cmp_different_blocks_none.
destruct (valid b1 (Ptrofs.unsigned ofs1) && valid b2 (Ptrofs.unsigned ofs2)); simpl.
apply cmp_different_blocks_sound.
apply cmp_different_blocks_none.
}
assert (SAME: b1 = b2 ->
cmatch (Val.cmpu_bool valid c (Vptr b1 ofs1) (Vptr b2 ofs2))
(Maybe (Ptrofs.cmpu c ofs1 ofs2))).
{
intros. subst b2. simpl. destruct Archi.ptr64.
constructor.
rewrite dec_eq_true.
destruct ((valid b1 (Ptrofs.unsigned ofs1) || valid b1 (Ptrofs.unsigned ofs1 - 1)) &&
(valid b1 (Ptrofs.unsigned ofs2) || valid b1 (Ptrofs.unsigned ofs2 - 1))); simpl.
constructor.
constructor.
}
unfold pcmp; inv H; inv H0; (apply cmatch_top || (apply DIFF; congruence) || idtac).
- destruct (peq id id0). subst id0. apply SAME. eapply bc_glob; eauto.
auto with va.
- destruct (peq id id0); auto with va.
- destruct (peq id id0); auto with va.
- destruct (peq id id0); auto with va.
- apply SAME. eapply bc_stack; eauto.
Qed.

Lemma pcmp_sound_64:
forall valid c b1 ofs1 p1 b2 ofs2 p2,
pmatch b1 ofs1 p1 -> pmatch b2 ofs2 p2 ->
cmatch (Val.cmplu_bool valid c (Vptr b1 ofs1) (Vptr b2 ofs2)) (pcmp c p1 p2).
Proof.
intros.
assert (DIFF: b1 <> b2 ->
cmatch (Val.cmplu_bool valid c (Vptr b1 ofs1) (Vptr b2 ofs2))
(cmp_different_blocks c)).
{
intros. simpl. rewrite dec_eq_false by assumption.
destruct Archi.ptr64; simpl.
destruct (valid b1 (Ptrofs.unsigned ofs1) && valid b2 (Ptrofs.unsigned ofs2)); simpl.
apply cmp_different_blocks_sound.
apply cmp_different_blocks_none.
apply cmp_different_blocks_none.
}
assert (SAME: b1 = b2 ->
cmatch (Val.cmplu_bool valid c (Vptr b1 ofs1) (Vptr b2 ofs2))
(Maybe (Ptrofs.cmpu c ofs1 ofs2))).
{
intros. subst b2. simpl. destruct Archi.ptr64.
rewrite dec_eq_true.
destruct ((valid b1 (Ptrofs.unsigned ofs1) || valid b1 (Ptrofs.unsigned ofs1 - 1)) &&
(valid b1 (Ptrofs.unsigned ofs2) || valid b1 (Ptrofs.unsigned ofs2 - 1))); simpl.
constructor.
constructor.
constructor.
}
unfold pcmp; inv H; inv H0; (apply cmatch_top || (apply DIFF; congruence) || idtac).
- destruct (peq id id0). subst id0. apply SAME. eapply bc_glob; eauto.
auto with va.
- destruct (peq id id0); auto with va.
- destruct (peq id id0); auto with va.
- destruct (peq id id0); auto with va.
- apply SAME. eapply bc_stack; eauto.
Qed.

Lemma pcmp_none:
forall c p1 p2, cmatch None (pcmp c p1 p2).
Proof.
intros.
unfold pcmp; destruct p1; try constructor; destruct p2;
try (destruct (peq id id0)); try constructor; try (apply cmp_different_blocks_none).
Qed.

Definition pdisjoint (p1: aptr) (sz1: Z) (p2: aptr) (sz2: Z) : bool :=
match p1, p2 with
| Pbot, _ => true
| _, Pbot => true
| Gl id1 ofs1, Gl id2 ofs2 =>
if peq id1 id2
then zle (Ptrofs.unsigned ofs1 + sz1) (Ptrofs.unsigned ofs2)
|| zle (Ptrofs.unsigned ofs2 + sz2) (Ptrofs.unsigned ofs1)
else true
| Gl id1 ofs1, Glo id2 => negb(peq id1 id2)
| Glo id1, Gl id2 ofs2 => negb(peq id1 id2)
| Glo id1, Glo id2 => negb(peq id1 id2)
| Stk ofs1, Stk ofs2 =>
zle (Ptrofs.unsigned ofs1 + sz1) (Ptrofs.unsigned ofs2)
|| zle (Ptrofs.unsigned ofs2 + sz2) (Ptrofs.unsigned ofs1)
| (Gl _ _ | Glo _ | Glob | Nonstack), (Stk _ | Stack) => true
| (Stk _ | Stack), (Gl _ _ | Glo _ | Glob | Nonstack) => true
| _, _ => false
end.

Lemma pdisjoint_sound:
forall sz1 b1 ofs1 p1 sz2 b2 ofs2 p2,
pdisjoint p1 sz1 p2 sz2 = true ->
pmatch b1 ofs1 p1 -> pmatch b2 ofs2 p2 ->
b1 <> b2 \/ Ptrofs.unsigned ofs1 + sz1 <= Ptrofs.unsigned ofs2 \/ Ptrofs.unsigned ofs2 + sz2 <= Ptrofs.unsigned ofs1.
Proof.
intros. inv H0; inv H1; simpl in H; try discriminate; try (left; congruence).
- destruct (peq id id0). subst id0. destruct (orb_true_elim _ _ H); InvBooleans; auto.
left; congruence.
- destruct (peq id id0); try discriminate. left; congruence.
- destruct (peq id id0); try discriminate. left; congruence.
- destruct (peq id id0); try discriminate. left; congruence.
- destruct (orb_true_elim _ _ H); InvBooleans; auto.
Qed.

# Abstracting values

Inductive aval : Type :=
| Vbot (* bottom (empty set of values) *)
| I (n: int) (* exactly Vint n *)
| Uns (p: aptr) (n: Z) (* a n-bit unsigned integer, or Vundef *)
| Sgn (p: aptr) (n: Z) (* a n-bit signed integer, or Vundef *)
| L (n: int64) (* exactly Vlong n *)
| F (f: float) (* exactly Vfloat f *)
| FS (f: float32) (* exactly Vsingle f *)
| Num (p: aptr) (* any number, or Vundef *)
| Ptr (p: aptr) (* a pointer from the set p, or Vundef *)
| Ifptr (p: aptr). (* a pointer from the set p, or a number, or Vundef *)

The "top" of the value domain is defined as any pointer, or any number, or Vundef.

Definition Vtop := Ifptr Ptop.

The p parameter (an abstract pointer) to Uns, Sgn and Num helps keeping track of pointers that leak through arithmetic operations such as shifts. See the section "Tracking leakage of pointers" below.

Definition eq_aval: forall (v1 v2: aval), {v1=v2} + {v1<>v2}.
Proof.
intros. generalize zeq Int.eq_dec Int64.eq_dec Float.eq_dec Float32.eq_dec eq_aptr; intros.
decide equality.
Defined.

Definition is_uns (n: Z) (i: int) : Prop :=
forall m, 0 <= m < Int.zwordsize -> m >= n -> Int.testbit i m = false.
Definition is_sgn (n: Z) (i: int) : Prop :=
forall m, 0 <= m < Int.zwordsize -> m >= n - 1 -> Int.testbit i m = Int.testbit i (Int.zwordsize - 1).

Inductive vmatch : val -> aval -> Prop :=
| vmatch_i: forall i, vmatch (Vint i) (I i)
| vmatch_Uns: forall p i n, 0 <= n -> is_uns n i -> vmatch (Vint i) (Uns p n)
| vmatch_Uns_undef: forall p n, vmatch Vundef (Uns p n)
| vmatch_Sgn: forall p i n, 0 < n -> is_sgn n i -> vmatch (Vint i) (Sgn p n)
| vmatch_Sgn_undef: forall p n, vmatch Vundef (Sgn p n)
| vmatch_l: forall i, vmatch (Vlong i) (L i)
| vmatch_f: forall f, vmatch (Vfloat f) (F f)
| vmatch_s: forall f, vmatch (Vsingle f) (FS f)
| vmatch_num_undef: forall p, vmatch Vundef (Num p)
| vmatch_num_i: forall i p, vmatch (Vint i) (Num p)
| vmatch_num_l: forall i p, vmatch (Vlong i) (Num p)
| vmatch_num_f: forall f p, vmatch (Vfloat f) (Num p)
| vmatch_num_s: forall f p, vmatch (Vsingle f) (Num p)
| vmatch_ptr: forall b ofs p, pmatch b ofs p -> vmatch (Vptr b ofs) (Ptr p)
| vmatch_ptr_undef: forall p, vmatch Vundef (Ptr p)
| vmatch_ifptr_undef: forall p, vmatch Vundef (Ifptr p)
| vmatch_ifptr_i: forall i p, vmatch (Vint i) (Ifptr p)
| vmatch_ifptr_l: forall i p, vmatch (Vlong i) (Ifptr p)
| vmatch_ifptr_f: forall f p, vmatch (Vfloat f) (Ifptr p)
| vmatch_ifptr_s: forall f p, vmatch (Vsingle f) (Ifptr p)
| vmatch_ifptr_p: forall b ofs p, pmatch b ofs p -> vmatch (Vptr b ofs) (Ifptr p).

Hint Extern 1 (vmatch _ _) => constructor : va.

Lemma vmatch_num:
forall v p,
match v with Vptr _ _ => False | _ => True end ->
vmatch v (Num p).
Proof.
intros. destruct v; auto with va; contradiction.
Qed.

Lemma vmatch_ifptr:
forall v p,
(forall b ofs, v = Vptr b ofs -> pmatch b ofs p) ->
vmatch v (Ifptr p).
Proof.
intros. destruct v; constructor; auto.
Qed.

Lemma vmatch_top: forall v x, vmatch v x -> vmatch v Vtop.
Proof.
intros. apply vmatch_ifptr. intros. subst v. inv H; eapply pmatch_top'; eauto.
Qed.

Some properties about is_uns and is_sgn.

Lemma is_uns_mon: forall n1 n2 i, is_uns n1 i -> n1 <= n2 -> is_uns n2 i.
Proof.
intros; red; intros. apply H; lia.
Qed.

Lemma is_sgn_mon: forall n1 n2 i, is_sgn n1 i -> n1 <= n2 -> is_sgn n2 i.
Proof.
intros; red; intros. apply H; lia.
Qed.

Lemma is_uns_sgn: forall n1 n2 i, is_uns n1 i -> n1 < n2 -> is_sgn n2 i.
Proof.
intros; red; intros. rewrite ! H by lia. auto.
Qed.

Definition usize := Int.size.

Definition ssize (i: int) := Int.size (if Int.lt i Int.zero then Int.not i else i) + 1.

Lemma is_uns_usize:
forall i, is_uns (usize i) i.
Proof.
unfold usize; intros; red; intros.
apply Int.bits_size_2. lia.
Qed.

Lemma is_sgn_ssize:
forall i, is_sgn (ssize i) i.
Proof.
unfold ssize; intros; red; intros.
destruct (Int.lt i Int.zero) eqn:LT.
- rewrite <- (negb_involutive (Int.testbit i m)).
rewrite <- (negb_involutive (Int.testbit i (Int.zwordsize - 1))).
f_equal.
generalize (Int.size_range (Int.not i)); intros RANGE.
rewrite <- ! Int.bits_not by lia.
rewrite ! Int.bits_size_2 by lia.
auto.
- rewrite ! Int.bits_size_2 by lia.
auto.
Qed.

Lemma is_uns_zero_ext:
forall n i, is_uns n i <-> Int.zero_ext n i = i.
Proof.
intros; split; intros.
Int.bit_solve. destruct (zlt i0 n); auto. symmetry; apply H; auto. lia.
rewrite <- H. red; intros. rewrite Int.bits_zero_ext by lia. rewrite zlt_false by lia. auto.
Qed.

Lemma is_sgn_sign_ext:
forall n i, 0 < n -> (is_sgn n i <-> Int.sign_ext n i = i).
Proof.
intros; split; intros.
Int.bit_solve. destruct (zlt i0 n); auto.
transitivity (Int.testbit i (Int.zwordsize - 1)).
apply H0; lia. symmetry; apply H0; lia.
rewrite <- H0. red; intros. rewrite ! Int.bits_sign_ext by lia.
f_equal. transitivity (n-1). destruct (zlt m n); lia.
destruct (zlt (Int.zwordsize - 1) n); lia.
Qed.

Lemma is_zero_ext_uns:
forall i n m,
is_uns m i \/ n <= m -> is_uns m (Int.zero_ext n i).
Proof.
intros. red; intros. rewrite Int.bits_zero_ext by lia.
destruct (zlt m0 n); auto. destruct H. apply H; lia. extlia.
Qed.

Lemma is_zero_ext_sgn:
forall i n m,
n < m ->
is_sgn m (Int.zero_ext n i).
Proof.
intros. red; intros. rewrite ! Int.bits_zero_ext by lia.
transitivity false. apply zlt_false; lia.
symmetry; apply zlt_false; lia.
Qed.

Lemma is_sign_ext_uns:
forall i n m,
0 <= m < n ->
is_uns m i ->
is_uns m (Int.sign_ext n i).
Proof.
intros; red; intros. rewrite Int.bits_sign_ext by lia.
apply H0. destruct (zlt m0 n); lia. destruct (zlt m0 n); lia.
Qed.

Lemma is_sign_ext_sgn:
forall i n m,
0 < n -> 0 < m ->
is_sgn m i \/ n <= m -> is_sgn m (Int.sign_ext n i).
Proof.
intros. apply is_sgn_sign_ext; auto.
destruct (zlt m n). destruct H1. apply is_sgn_sign_ext in H1; auto.
rewrite <- H1. rewrite (Int.sign_ext_widen i) by lia. apply Int.sign_ext_idem; auto.
extlia.
apply Int.sign_ext_widen; lia.
Qed.

Hint Resolve is_uns_mon is_sgn_mon is_uns_sgn is_uns_usize is_sgn_ssize : va.

Lemma is_uns_1:
forall n, is_uns 1 n -> n = Int.zero \/ n = Int.one.
Proof.
intros. destruct (Int.testbit n 0) eqn:B0; [right|left]; apply Int.same_bits_eq; intros.
rewrite Int.bits_one. destruct (zeq i 0). subst i; auto. apply H; lia.
rewrite Int.bits_zero. destruct (zeq i 0). subst i; auto. apply H; lia.
Qed.

Tracking leakage of pointers through arithmetic operations. In the CompCert semantics, arithmetic operations (e.g. "xor") applied to pointer values are undefined or produce the Vundef result. If we later use the result as the address of a memory access, the memory access will fail. Hence, in strict mode, the alias analysis can ignore these pointers that were transformed by arithmetic operations. In real code, arithmetic over pointers occurs, and can produce valid pointers. For example, a bitwise "and" can be used to realign a pointer. Hence, in conservative mode, the alias analysis must track these pointers that were transformed by arithmetic operations. This is the purpose of the "provenance" argument p to the abstract values Num p, Uns p n, and Sgn p n. p is an abstract pointer that over-approximates all the pointer values that may have been used as integers to produce this numerical value. If a memory access is performed at an address that matches Num p, Uns p n, or Sgn p n, the value analysis considers that the abstract pointer p is accessed. Likewise, if one of these abstract values is joined with a pointer abstract value Ptr q or Ifptr q, the pointer abstract value Ifptr (plub p q) is produced. To define the provenance p of the result of an arithmetic operation, we follow the same policy as GCC: "undefined" arithmetic operations involving pointer arguments can produce a pointer, but not any pointer, just a pointer to the same block but possibly with a different offset. Hence, if the operation has a pointer to abstract region p as argument, the result value can be a pointer to abstract region poffset p. We encapsulate this reasoning in the following ntop1 and ntop2 functions ("numerical top").

Definition provenance (x: aval) : aptr :=
match x with
| Ptr p | Ifptr p => poffset p
| Uns p _ | Sgn p _ | Num p => p
| _ => Pbot
end.

Definition ntop : aval := Num Pbot.

Definition ntop1 (x: aval) : aval := Num (provenance x).

Definition ntop2 (x y: aval) : aval := Num (plub (provenance x) (provenance y)).

Lemma vundef_ntop1: forall p, vmatch Vundef (ntop1 p).
Proof.
unfold ntop1. constructor.
Qed.

Lemma vundef_ntop2: forall p1 p2, vmatch Vundef (ntop2 p1 p2).
Proof.
unfold ntop2. constructor.
Qed.

Embedded C code often uses integer literals as absolute addresses for loads and stores, e.g. int * device = (int * ) 0x1000; *device = 12; . In conservative mode, we analyze these loads and stores as potentially accessing any memory location except stack blocks, i.e. as a Nonstack access. The following functions determine the provenance to use for integer literals when they are used in a pointer context. The null pointer (literal 0) is treated specially: even in conservative mode, accesses to address 0 are considered illegal.

Definition int_provenance (i: int) : aptr :=
if va_strict tt || Int.eq i Int.zero then Pbot else Nonstack.

Definition long_provenance (i: int64) : aptr :=
if va_strict tt || Int64.eq i Int64.zero then Pbot else Nonstack.

Smart constructors for Uns and Sgn.

Definition uns (p: aptr) (n: Z) : aval :=
if zle n 1 then Uns p 1
else if zle n 7 then Uns p 7
else if zle n 8 then Uns p 8
else if zle n 15 then Uns p 15
else if zle n 16 then Uns p 16
else Num p.

Definition sgn (p: aptr) (n: Z) : aval :=
if zle n 8 then Sgn p 8 else if zle n 16 then Sgn p 16 else Num p.

Lemma vmatch_uns':
forall p i n, is_uns (Z.max 0 n) i -> vmatch (Vint i) (uns p n).
Proof.
intros.
assert (A: forall n', n' >= 0 -> n' >= n -> is_uns n' i) by (eauto with va).
unfold uns. repeat destruct zle; auto with va.
Qed.

Lemma vmatch_uns:
forall p i n, is_uns n i -> vmatch (Vint i) (uns p n).
Proof.
intros. apply vmatch_uns'. eauto with va.
Qed.

Lemma vmatch_uns_undef: forall p n, vmatch Vundef (uns p n).
Proof.
intros. unfold uns. repeat destruct zle; auto with va.
Qed.

Lemma vmatch_sgn':
forall p i n, is_sgn (Z.max 1 n) i -> vmatch (Vint i) (sgn p n).
Proof.
intros.
assert (A: forall n', n' >= 1 -> n' >= n -> is_sgn n' i) by (eauto with va).
unfold sgn. repeat destruct zle; auto with va.
Qed.

Lemma vmatch_sgn:
forall p i n, is_sgn n i -> vmatch (Vint i) (sgn p n).
Proof.
intros. apply vmatch_sgn'. eauto with va.
Qed.

Lemma vmatch_sgn_undef: forall p n, vmatch Vundef (sgn p n).
Proof.
intros. unfold sgn. repeat destruct zle; auto with va.
Qed.

Hint Resolve vmatch_uns vmatch_uns_undef vmatch_sgn vmatch_sgn_undef : va.

Lemma vmatch_Uns_1:
forall p v, vmatch v (Uns p 1) -> v = Vundef \/ v = Vint Int.zero \/ v = Vint Int.one.
Proof.
intros. inv H; auto. right. exploit is_uns_1; eauto. intuition congruence.
Qed.

Ordering

Inductive vge: aval -> aval -> Prop :=
| vge_bot: forall v, vge v Vbot
| vge_i: forall i, vge (I i) (I i)
| vge_l: forall i, vge (L i) (L i)
| vge_f: forall f, vge (F f) (F f)
| vge_s: forall f, vge (FS f) (FS f)
| vge_uns_i: forall p n i, 0 <= n -> is_uns n i -> vge (Uns p n) (I i)
| vge_uns_uns: forall p1 n1 p2 n2, n1 >= n2 -> pge p1 p2 -> vge (Uns p1 n1) (Uns p2 n2)
| vge_sgn_i: forall p n i, 0 < n -> is_sgn n i -> vge (Sgn p n) (I i)
| vge_sgn_sgn: forall p1 n1 p2 n2, n1 >= n2 -> pge p1 p2 -> vge (Sgn p1 n1) (Sgn p2 n2)
| vge_sgn_uns: forall p1 n1 p2 n2, n1 > n2 -> pge p1 p2 -> vge (Sgn p1 n1) (Uns p2 n2)
| vge_num_i: forall p i, vge (Num p) (I i)
| vge_num_l: forall p i, vge (Num p) (L i)
| vge_num_f: forall p f, vge (Num p) (F f)
| vge_num_s: forall p f, vge (Num p) (FS f)
| vge_num_uns: forall p q n, pge p q -> vge (Num p) (Uns q n)
| vge_num_sgn: forall p q n, pge p q -> vge (Num p) (Sgn q n)
| vge_num_num: forall p q, pge p q -> vge (Num p) (Num q)
| vge_p_p: forall p q, pge p q -> vge (Ptr p) (Ptr q)
| vge_ip_p: forall p q, pge p q -> vge (Ifptr p) (Ptr q)
| vge_ip_ip: forall p q, pge p q -> vge (Ifptr p) (Ifptr q)
| vge_ip_i: forall p i, vge (Ifptr p) (I i)
| vge_ip_l: forall p i, vge (Ifptr p) (L i)
| vge_ip_f: forall p f, vge (Ifptr p) (F f)
| vge_ip_s: forall p f, vge (Ifptr p) (FS f)
| vge_ip_uns: forall p q n, pge p q -> vge (Ifptr p) (Uns q n)
| vge_ip_sgn: forall p q n, pge p q -> vge (Ifptr p) (Sgn q n)
| vge_ip_num: forall p q, pge p q -> vge (Ifptr p) (Num q).

Hint Constructors vge : va.

Lemma vge_top: forall x, vge Vtop x.
Proof.
unfold Vtop; destruct x; auto with va.
Qed.

Lemma vge_refl: forall x, vge x x.
Proof.
destruct x; auto with va.
Qed.

Hint Resolve vge_top vge_refl : va.

Lemma vge_trans: forall x y z, vge x y -> vge y z -> vge x z.
Proof.
intros x y z XY YZ; revert y z YZ x XY.
destruct 1; intros x V; auto with va; inv V; eauto using pge_trans with va.
Qed.

Lemma vmatch_ge:
forall v x y, vge x y -> vmatch v y -> vmatch v x.
Proof.
induction 1; intros V; inv V; eauto using pmatch_ge with va.
Qed.

Least upper bound

Definition vlub (v w: aval) : aval :=
match v, w with
| Vbot, _ => w
| _, Vbot => v
| I i1, I i2 =>
if Int.eq i1 i2 then v else
if Int.lt i1 Int.zero || Int.lt i2 Int.zero
then sgn Pbot (Z.max (ssize i1) (ssize i2))
else uns Pbot (Z.max (usize i1) (usize i2))
| I i, Uns p n | Uns p n, I i =>
if Int.lt i Int.zero
then sgn p (Z.max (ssize i) (n + 1))
else uns p (Z.max (usize i) n)
| I i, Sgn p n | Sgn p n, I i =>
sgn p (Z.max (ssize i) n)
| I i, Num p | Num p, I i => Num p
| I i, (Ptr p | Ifptr p) | (Ptr p | Ifptr p), I i => Ifptr (plub p (int_provenance i))
| I _, (L _ | F _ | FS _) | (L _ | F _ | FS _), I _ => ntop
| Uns p1 n1, Uns p2 n2 => Uns (plub p1 p2) (Z.max n1 n2)
| Uns p1 n1, Sgn p2 n2 => sgn (plub p1 p2) (Z.max (n1 + 1) n2)
| Sgn p1 n1, Uns p2 n2 => sgn (plub p1 p2) (Z.max n1 (n2 + 1))
| Sgn p1 n1, Sgn p2 n2 => sgn (plub p1 p2) (Z.max n1 n2)
| (Uns p1 _ | Sgn p1 _), Num p2 | Num p1, (Uns p2 _ | Sgn p2 _) => Num (plub p1 p2)
| (Uns p1 _ | Sgn p1 _), (Ptr p2 | Ifptr p2) | (Ptr p1 | Ifptr p1), (Uns p2 _ | Sgn p2 _) => Ifptr (plub p1 p2)
| (Uns p _ | Sgn p _), (L _ | F _ | FS _) | (L _ | F _ | FS _), (Uns p _ | Sgn p _) => Num p
| L i1, L i2 => if Int64.eq i1 i2 then v else ntop
| L i, Num p | Num p, L i => Num p
| L i, (Ptr p | Ifptr p) | (Ptr p | Ifptr p), L i => Ifptr (plub p (long_provenance i))
| L _, (F _ | FS _) | (F _ | FS _), L _ => ntop
| F f1, F f2 => if Float.eq_dec f1 f2 then v else ntop
| F _, Num p | Num p, F _ => Num p
| F _, (Ptr p | Ifptr p) | (Ptr p | Ifptr p), F _ => Ifptr p
| F _, FS _ | FS _, F _ => ntop
| FS f1, FS f2 => if Float32.eq_dec f1 f2 then v else ntop
| FS _, Num p | Num p, FS _ => Num p
| FS _, (Ptr p | Ifptr p) | (Ptr p | Ifptr p), FS _ => Ifptr p
| Num p1, Num p2 => Num (plub p1 p2)
| Num p1, (Ptr p2 | Ifptr p2) | (Ifptr p1 | Ptr p1), Num p2 => Ifptr (plub p1 p2)
| Ptr p1, Ptr p2 => Ptr(plub p1 p2)
| Ptr p1, Ifptr p2 | Ifptr p1, Ptr p2 | Ifptr p1, Ifptr p2 => Ifptr(plub p1 p2)
end.

Lemma vlub_comm:
forall v w, vlub v w = vlub w v.
Proof.
intros. unfold vlub; destruct v; destruct w; auto; f_equal; auto using Z.max_comm, plub_comm.
- rewrite Int.eq_sym. predSpec Int.eq Int.eq_spec n0 n. congruence.
rewrite orb_comm. destruct orb; f_equal; apply Z.max_comm.
- rewrite Int64.eq_sym. predSpec Int64.eq Int64.eq_spec n0 n; congruence.
- rewrite dec_eq_sym. destruct (Float.eq_dec f0 f); congruence.
- rewrite dec_eq_sym. destruct (Float32.eq_dec f0 f); congruence.
Qed.

Lemma vge_uns_uns': forall p n, vge (uns p n) (Uns p n).
Proof.
unfold uns; intros. repeat (destruct zle); eauto with va.
Qed.

Lemma vge_uns_i': forall p n i, 0 <= n -> is_uns n i -> vge (uns p n) (I i).
Proof.
intros. apply vge_trans with (Uns p n). apply vge_uns_uns'. auto with va.
Qed.

Lemma vge_sgn_sgn': forall p n, vge (sgn p n) (Sgn p n).
Proof.
unfold sgn; intros. repeat (destruct zle); eauto with va.
Qed.

Lemma vge_sgn_i': forall p n i, 0 < n -> is_sgn n i -> vge (sgn p n) (I i).
Proof.
intros. apply vge_trans with (Sgn p n). apply vge_sgn_sgn'. auto with va.
Qed.

Hint Resolve vge_uns_uns' vge_uns_i' vge_sgn_sgn' vge_sgn_i' : va.

Lemma usize_pos: forall n, 0 <= usize n.
Proof.
unfold usize; intros. generalize (Int.size_range n); lia.
Qed.

Lemma ssize_pos: forall n, 0 < ssize n.
Proof.
unfold ssize; intros.
generalize (Int.size_range (if Int.lt n Int.zero then Int.not n else n)); lia.
Qed.

Lemma vge_lub_l:
forall x y, vge (vlub x y) x.
Proof.
unfold vlub, ntop; destruct x, y; eauto using vge_trans, pge_lub_l with va.
- predSpec Int.eq Int.eq_spec n n0. auto with va. destruct orb.
apply vge_sgn_i'. generalize (ssize_pos n); lia. eauto with va.
apply vge_uns_i'. generalize (usize_pos n); lia. eauto with va.
- destruct (Int.lt n Int.zero).
apply vge_sgn_i'. generalize (ssize_pos n); lia. eauto with va.
apply vge_uns_i'. generalize (usize_pos n); lia. eauto with va.
- apply vge_sgn_i'. generalize (ssize_pos n); lia. eauto with va.
- destruct (Int.lt n0 Int.zero).
eapply vge_trans. apply vge_sgn_sgn'.
apply vge_trans with (Sgn p (n + 1)); eauto with va.
eapply vge_trans. apply vge_uns_uns'. eauto with va.
- destruct (Int64.eq n n0); constructor.
- destruct (Float.eq_dec f f0); constructor.
- destruct (Float32.eq_dec f f0); constructor.
Qed.

Lemma vge_lub_r:
forall x y, vge (vlub x y) y.
Proof.
intros. rewrite vlub_comm. apply vge_lub_l.
Qed.

Lemma vmatch_lub_l:
forall v x y, vmatch v x -> vmatch v (vlub x y).
Proof.
intros. eapply vmatch_ge; eauto. apply vge_lub_l.
Qed.

Lemma vmatch_lub_r:
forall v x y, vmatch v y -> vmatch v (vlub x y).
Proof.
intros. rewrite vlub_comm. apply vmatch_lub_l; auto.
Qed.

In the CompCert semantics, a memory load or store succeeds only if the address is a pointer value. Hence, in strict mode, aptr_of_aval x returns Pbot (no pointer value) if x denotes a number or Vundef. However, in real code, memory addresses are sometimes synthesized from integers, e.g. an absolute address for a hardware device. It is a reasonable assumption that these absolute addresses do not point within the stack block, however. Therefore, in relaxed mode, aptr_of_aval x returns Nonstack (any pointer outside the stack) when x denotes a number.

Definition aptr_of_aval (v: aval) : aptr :=
match v with
| Ptr p | Ifptr p => p
| Num p | Uns p _ | Sgn p _ => if va_strict tt then Pbot else p
| I i => int_provenance i
| L i => long_provenance i
| _ => Pbot
end.

Lemma match_aptr_of_aval:
forall b ofs av,
vmatch (Vptr b ofs) av -> pmatch b ofs (aptr_of_aval av).
Proof.
unfold aptr_of_aval; intros. inv H; auto.
Qed.

Definition vplub (v: aval) (p: aptr) : aptr :=
match v with
| Ptr q => plub q p
| Ifptr q => plub q p
| _ => p
end.

Lemma vmatch_vplub_l:
forall v x p, vmatch v x -> vmatch v (Ifptr (vplub x p)).
Proof.
intros. unfold vplub; inv H; auto with va; constructor; eapply pmatch_lub_l; eauto.
Qed.

Lemma pmatch_vplub:
forall b ofs x p, pmatch b ofs p -> pmatch b ofs (vplub x p).
Proof.
intros.
assert (DFL: pmatch b ofs (if va_strict tt then p else Ptop)).
{ destruct (va_strict tt); auto. eapply pmatch_top'; eauto. }
unfold vplub; destruct x; auto; apply pmatch_lub_r; auto.
Qed.

Lemma vmatch_vplub_r:
forall v x p, vmatch v (Ifptr p) -> vmatch v (Ifptr (vplub x p)).
Proof.
intros. apply vmatch_ifptr; intros; subst v. inv H. apply pmatch_vplub; auto.
Qed.

Inclusion

Definition vpincl (v: aval) (p: aptr) : bool :=
match v with
| Ptr q | Ifptr q | Num q | Uns q _ | Sgn q _ => pincl q p
| _ => true
end.

Lemma vpincl_ge:
forall x p, vpincl x p = true -> vge (Ifptr p) x.
Proof.
unfold vpincl; intros. destruct x; eauto using pincl_ge with va.
Qed.

Lemma vpincl_sound:
forall v x p, vpincl x p = true -> vmatch v x -> vmatch v (Ifptr p).
Proof.
intros. apply vmatch_ge with x; auto. apply vpincl_ge; auto.
Qed.

Definition vincl (v w: aval) : bool :=
match v, w with
| Vbot, _ => true
| I i, I j => Int.eq_dec i j
| I i, Uns p n => Int.eq_dec (Int.zero_ext n i) i && zle 0 n
| I i, Sgn p n => Int.eq_dec (Int.sign_ext n i) i && zlt 0 n
| Uns p n, Uns q m => zle n m && pincl p q
| Uns p n, Sgn q m => zlt n m && pincl p q
| Sgn p n, Sgn q m => zle n m && pincl p q
| L i, L j => Int64.eq_dec i j
| F i, F j => Float.eq_dec i j
| FS i, FS j => Float32.eq_dec i j
| (I _ | L _ | F _ | FS _), (Num _ | Ifptr _) => true
| (Uns p _ | Sgn p _ | Num p), Num q => pincl p q
| Ptr p, Ptr q => pincl p q
| (Ptr p | Ifptr p | Num p | Uns p _ | Sgn p _), Ifptr q => pincl p q
| _, _ => false
end.

Lemma vincl_ge: forall v w, vincl v w = true -> vge w v.
Proof.
unfold vincl; destruct v; destruct w;
intros; try discriminate; try InvBooleans; try subst; eauto using pincl_ge with va.
- constructor; auto. rewrite is_uns_zero_ext; auto.
- constructor; auto. rewrite is_sgn_sign_ext; auto.
Qed.

Lemma ge_vincl: forall v w, vge v w -> vincl w v = true.
Proof.
induction 1; simpl; try (apply andb_true_intro; split); auto using ge_pincl, proj_sumbool_is_true.
all: try ( unfold proj_sumbool; rewrite zlt_true by lia; auto; fail).
all: try ( unfold proj_sumbool; rewrite zle_true by lia; auto; fail).
- apply is_uns_zero_ext in H0; rewrite H0. auto using proj_sumbool_is_true.
- apply is_sgn_sign_ext in H0; auto. rewrite H0. auto using proj_sumbool_is_true.
Qed.

Definition vglb (v w: aval) : aval :=
match v, w with
| I i1, I i2 =>
if Int.eq_dec i1 i2 then v else Vbot
| (Uns p1 n1), (Uns p2 n2) =>
Uns (pglb p1 p2) (Z.min n1 n2)
| (Sgn p1 n1), (Sgn p2 n2) =>
Sgn (pglb p1 p2) (Z.min n1 n2)
| (Uns p n), (I i) | (I i), (Uns p n) =>
if Int.eq_dec (Int.zero_ext n i) i && zle 0 n
then I i
else Vbot
| (Sgn p n), (I i) | (I i), (Sgn p n) =>
if Int.eq_dec (Int.sign_ext n i) i && zlt 0 n
then I i
else Vbot
| F f1, F f2 =>
if Float.eq_dec f1 f2 then v else Vbot
| FS f1, FS f2 =>
if Float32.eq_dec f1 f2 then v else Vbot
| L i1, L i2 =>
if Int64.eq_dec i1 i2 then v else Vbot
| ((I _) | (L _) | (F _) | (FS _)), (Ifptr _ | Num _) => v
| (Ifptr _ | Num _), ((I _) | (L _) | (F _) | (FS _)) => w
| (Ifptr p1 | Num p1), (Uns p2 n2) => Uns (pglb p1 p2) n2
| (Uns p1 n1), (Ifptr p2 | Num p2) => Uns (pglb p1 p2) n1
| (Uns p1 n1), (Sgn p2 n2)
| (Sgn p2 n2), (Uns p1 n1) => Uns (pglb p1 p2) n1
| (Ifptr p1 | Num p1), (Sgn p2 n2) => Sgn (pglb p1 p2) n2
| (Sgn p1 n1), (Ifptr p2 | Num p2) => Sgn (pglb p1 p2) n1
| (Ptr p1 | Ifptr p1 | Uns p1 _ |Sgn p1 _ | Num p1), Ptr p2
| Ptr p1, (Ifptr p2 | Sgn p2 _ | Uns p2 _ | Num p2) => Ptr(pglb p1 p2)
| Num p1, Ifptr p2 | Ifptr p1, Num p2
| Num p1, Num p2 => Num(pglb p1 p2)
| Ifptr p1, Ifptr p2 => Ifptr(pglb p1 p2)
| _, _ => Vbot
end.

Lemma if_eq_dec:
forall {T U: Type}
(eq_dec : forall (x y : T), {x = y} + {x <> y})
(a : T)
(x y : U),
(if eq_dec a a then x else y) = x.
Proof.
intros.
destruct eq_dec; congruence.
Qed.

Lemma is_not_uns_usize:
forall (i : int) sz
(SIZE : 0 <= sz < usize i),
~ is_uns sz i.
Proof.
intros.
unfold is_uns, usize in *.
intro BITS.
pose proof (Int.size_range i) as RANGE.
destruct (Int.bits_size_1 i) as [ZERO | NZ].
{ subst i.
change (Int.size Int.zero) with 0 in SIZE.
lia.
}
rewrite BITS in NZ.
discriminate.
lia.
lia.
Qed.

Lemma is_uns_glb:
forall a b x
(UNS_A : is_uns a x)
(UNS_B : is_uns b x),
(is_uns (Z.min a b) x).
Proof.
intros.
unfold is_uns in *.
intro.
destruct (Zmin_irreducible a b) as [RE | RE]; rewrite RE; auto.
Qed.

Lemma is_sgn_glb:
forall a b x
(UNS_A : is_sgn a x)
(UNS_B : is_sgn b x),
(is_sgn (Z.min a b) x).
Proof.
intros.
unfold is_sgn in *.
intro.
destruct (Zmin_irreducible a b) as [RE | RE]; rewrite RE; auto.
Qed.

Lemma vmatch_glb:
forall v a1 a2
(MATCH1 : vmatch v a1)
(MATCH2 : vmatch v a2),
vmatch v (vglb a1 a2).
Proof.
intros.
inv MATCH1; inv MATCH2; cbn; try rewrite if_eq_dec; try constructor; try lia; auto using pmatch_glb, is_uns_glb, is_sgn_glb.

- pose proof (is_uns_zero_ext n i) as EQV.
destruct Int.eq_dec; cbn; cycle 1.
rewrite <- EQV in n0. contradiction.
destruct zle; cbn; cycle 1.
lia.
constructor.
- pose proof (is_sgn_sign_ext n i) as EQV.
destruct Int.eq_dec; cbn; cycle 1.
rewrite <- EQV in n0. contradiction.
assumption.
destruct zlt; cbn; cycle 1.
lia.
constructor.
- pose proof (is_uns_zero_ext n i) as EQV.
destruct Int.eq_dec; cbn; cycle 1.
rewrite <- EQV in n0. contradiction.
destruct zle; cbn; cycle 1.
lia.
constructor.
- pose proof (is_sgn_sign_ext n i) as EQV.
destruct Int.eq_dec; cbn; cycle 1.
rewrite <- EQV in n0. contradiction.
assumption.
destruct zlt; cbn; cycle 1.
lia.
constructor.
Qed.

Lemma vge_glb_r :
forall p q, vge q (vglb p q).
Proof.
destruct p; destruct q; cbn; try (constructor; apply pge_glb_r).
all: try (destruct Int.eq_dec; subst; cbn; constructor).
- destruct Int.eq_dec; cbn; cycle 1. constructor.
destruct zle; cbn; cycle 1. constructor.
constructor. assumption.
apply is_uns_zero_ext. assumption.

- destruct Int.eq_dec; cbn; cycle 1. constructor.
destruct zlt; cbn; cycle 1. constructor.
constructor. assumption.
apply is_sgn_sign_ext; assumption.
- destruct Int.eq_dec; cbn; cycle 1. constructor.
destruct zle; cbn; cycle 1. constructor.
constructor.

- constructor. lia. apply pge_glb_r.
Abort.

Definition genv_match {genF genV: Type} (ge: Genv.t genF genV) : Prop :=
(forall id b, Genv.find_symbol ge id = Some b <-> bc b = BCglob id)
/\(forall b, Plt b (Genv.genv_next ge) -> bc b <> BCinvalid /\ bc b <> BCstack).

forall {genF genV : Type} (ge : Genv.t genF genV) id ofs,
genv_match ge ->
vmatch (Genv.symbol_address ge id ofs) (Ptr (Gl id ofs)).
Proof.
intros. unfold Genv.symbol_address. destruct (Genv.find_symbol ge id) as [b|] eqn:F.
constructor. constructor. apply H; auto.
constructor.
Qed.

Lemma vmatch_ptr_gl:
forall {genF genV : Type} (ge : Genv.t genF genV) v id ofs,
genv_match ge ->
vmatch v (Ptr (Gl id ofs)) ->
Val.lessdef v (Genv.symbol_address ge id ofs).
Proof.
- inv H3. replace (Genv.find_symbol ge id) with (Some b). constructor.
symmetry. apply H; auto.
- constructor.
Qed.

Lemma vmatch_ptr_stk:
forall v ofs sp,
vmatch v (Ptr(Stk ofs)) ->
bc sp = BCstack ->
Val.lessdef v (Vptr sp ofs).
Proof.
intros. inv H.
- inv H3. replace b with sp by (eapply bc_stack; eauto). constructor.
- constructor.
Qed.

Generic operations that just do constant propagation.

Definition unop_int (sem: int -> int) (x: aval) :=
match x with I n => I (sem n) | _ => ntop1 x end.

Lemma unop_int_sound:
forall sem v x,
vmatch v x ->
vmatch (match v with Vint i => Vint(sem i) | _ => Vundef end) (unop_int sem x).
Proof.
intros. unfold unop_int; inv H; auto with va.
Qed.

Definition binop_int (sem: int -> int -> int) (x y: aval) :=
match x, y with I n, I m => I (sem n m) | _, _ => ntop2 x y end.

Lemma binop_int_sound:
forall sem v x w y,
vmatch v x -> vmatch w y ->
vmatch (match v, w with Vint i, Vint j => Vint(sem i j) | _, _ => Vundef end) (binop_int sem x y).
Proof.
intros. unfold binop_int; inv H; auto with va; inv H0; auto with va.
Qed.

Definition unop_long (sem: int64 -> int64) (x: aval) :=
match x with L n => L (sem n) | _ => ntop1 x end.

Lemma unop_long_sound:
forall sem v x,
vmatch v x ->
vmatch (match v with Vlong i => Vlong(sem i) | _ => Vundef end) (unop_long sem x).
Proof.
intros. unfold unop_long; inv H; auto with va.
Qed.

Definition binop_long (sem: int64 -> int64 -> int64) (x y: aval) :=
match x, y with L n, L m => L (sem n m) | _, _ => ntop2 x y end.

Lemma binop_long_sound:
forall sem v x w y,
vmatch v x -> vmatch w y ->
vmatch (match v, w with Vlong i, Vlong j => Vlong(sem i j) | _, _ => Vundef end) (binop_long sem x y).
Proof.
intros. unfold binop_long; inv H; auto with va; inv H0; auto with va.
Qed.

Definition unop_float (sem: float -> float) (x: aval) :=
match x with F n => F (sem n) | _ => ntop1 x end.

Lemma unop_float_sound:
forall sem v x,
vmatch v x ->
vmatch (match v with Vfloat i => Vfloat(sem i) | _ => Vundef end) (unop_float sem x).
Proof.
intros. unfold unop_float; inv H; auto with va.
Qed.

Definition binop_float (sem: float -> float -> float) (x y: aval) :=
match x, y with F n, F m => F (sem n m) | _, _ => ntop2 x y end.

Lemma binop_float_sound:
forall sem v x w y,
vmatch v x -> vmatch w y ->
vmatch (match v, w with Vfloat i, Vfloat j => Vfloat(sem i j) | _, _ => Vundef end) (binop_float sem x y).
Proof.
intros. unfold binop_float; inv H; auto with va; inv H0; auto with va.
Qed.

Definition unop_single (sem: float32 -> float32) (x: aval) :=
match x with FS n => FS (sem n) | _ => ntop1 x end.

Lemma unop_single_sound:
forall sem v x,
vmatch v x ->
vmatch (match v with Vsingle i => Vsingle(sem i) | _ => Vundef end) (unop_single sem x).
Proof.
intros. unfold unop_single; inv H; auto with va.
Qed.

Definition binop_single (sem: float32 -> float32 -> float32) (x y: aval) :=
match x, y with FS n, FS m => FS (sem n m) | _, _ => ntop2 x y end.

Lemma binop_single_sound:
forall sem v x w y,
vmatch v x -> vmatch w y ->
vmatch (match v, w with Vsingle i, Vsingle j => Vsingle(sem i j) | _, _ => Vundef end) (binop_single sem x y).
Proof.
intros. unfold binop_single; inv H; auto with va; inv H0; auto with va.
Qed.

Logical operations

Definition shl (v w: aval) :=
match w with
| I amount =>
if Int.ltu amount Int.iwordsize then
match v with
| I i => I (Int.shl i amount)
| Uns p n => uns p (n + Int.unsigned amount)
| Sgn p n => sgn p (n + Int.unsigned amount)
| _ => ntop1 v
end
else ntop1 v
| _ => ntop1 v
end.

Lemma shl_sound:
forall v w x y, vmatch v x -> vmatch w y -> vmatch (Val.shl v w) (shl x y).
Proof.
intros.
assert (DEFAULT: vmatch (Val.shl v w) (ntop1 x)).
{
destruct v; destruct w; simpl; try constructor.
destruct (Int.ltu i0 Int.iwordsize); constructor.
}
destruct y; auto. simpl. inv H0. unfold Val.shl.
destruct (Int.ltu n Int.iwordsize) eqn:LTU; auto.
exploit Int.ltu_inv; eauto. intros RANGE.
inv H; auto with va.
- apply vmatch_uns'. red; intros. rewrite Int.bits_shl by lia.
destruct (zlt m (Int.unsigned n)). auto. apply H1; extlia.
- apply vmatch_sgn'. red; intros. zify.
rewrite ! Int.bits_shl by lia.
rewrite ! zlt_false by lia.
rewrite H1 by lia. symmetry. rewrite H1 by lia. auto.
- destruct v; constructor.
Qed.

Definition shru (v w: aval) :=
match w with
| I amount =>
if Int.ltu amount Int.iwordsize then
match v with
| I i => I (Int.shru i amount)
| Uns p n => uns p (n - Int.unsigned amount)
| _ => uns (provenance v) (Int.zwordsize - Int.unsigned amount)
end
else ntop1 v
| _ => ntop1 v
end.

Lemma shru_sound:
forall v w x y, vmatch v x -> vmatch w y -> vmatch (Val.shru v w) (shru x y).
Proof.
intros.
assert (DEFAULT: vmatch (Val.shru v w) (ntop1 x)).
{
destruct v; destruct w; simpl; try constructor.
destruct (Int.ltu i0 Int.iwordsize); constructor.
}
destruct y; auto. inv H0. unfold shru, Val.shru.
destruct (Int.ltu n Int.iwordsize) eqn:LTU; auto.
exploit Int.ltu_inv; eauto. intros RANGE. change (Int.unsigned Int.iwordsize) with Int.zwordsize in RANGE.
assert (DEFAULT2: forall i, vmatch (Vint (Int.shru i n)) (uns (provenance x) (Int.zwordsize - Int.unsigned n))).
{
intros. apply vmatch_uns. red; intros.
rewrite Int.bits_shru by lia. apply zlt_false. lia.
}
inv H; auto with va.
- apply vmatch_uns'. red; intros. zify.
rewrite Int.bits_shru by lia.
destruct (zlt (m + Int.unsigned n) Int.zwordsize); auto.
apply H1; lia.
- destruct v; constructor.
Qed.

Definition shr (v w: aval) :=
match w with
| I amount =>
if Int.ltu amount Int.iwordsize then
match v with
| I i => I (Int.shr i amount)
| Uns p n => sgn p (n + 1 - Int.unsigned amount)
| Sgn p n => sgn p (n - Int.unsigned amount)
| _ => sgn (provenance v) (Int.zwordsize - Int.unsigned amount)
end
else ntop1 v
| _ => ntop1 v
end.

Lemma shr_sound:
forall v w x y, vmatch v x -> vmatch w y -> vmatch (Val.shr v w) (shr x y).
Proof.
intros.
assert (DEFAULT: vmatch (Val.shr v w) (ntop1 x)).
{
destruct v; destruct w; simpl; try constructor.
destruct (Int.ltu i0 Int.iwordsize); constructor.
}
destruct y; auto. inv H0. unfold shr, Val.shr.
destruct (Int.ltu n Int.iwordsize) eqn:LTU; auto.
exploit Int.ltu_inv; eauto. intros RANGE. change (Int.unsigned Int.iwordsize) with Int.zwordsize in RANGE.
assert (DEFAULT2: forall i, vmatch (Vint (Int.shr i n)) (sgn (provenance x) (Int.zwordsize - Int.unsigned n))).
{
intros. apply vmatch_sgn. red; intros.
rewrite ! Int.bits_shr by lia. f_equal.
destruct (zlt (m + Int.unsigned n) Int.zwordsize);
destruct (zlt (Int.zwordsize - 1 + Int.unsigned n) Int.zwordsize);
lia.
}
assert (SGN: forall q i p, is_sgn p i -> 0 < p -> vmatch (Vint (Int.shr i n)) (sgn q (p - Int.unsigned n))).
{
intros. apply vmatch_sgn'. red; intros. zify.
rewrite ! Int.bits_shr by lia.
transitivity (Int.testbit i (Int.zwordsize - 1)).
destruct (zlt (m + Int.unsigned n) Int.zwordsize).
apply H0; lia.
auto.
symmetry.
destruct (zlt (Int.zwordsize - 1 + Int.unsigned n) Int.zwordsize).
apply H0; lia.
auto.
}
inv H; eauto with va.
- destruct v; constructor.
Qed.

Definition and (v w: aval) :=
match v, w with
| I i1, I i2 => I (Int.and i1 i2)
| I i, Uns p n | Uns p n, I i => uns p (Z.min n (usize i))
| I i, x | x, I i => uns (provenance x) (usize i)
| Uns p1 n1, Uns p2 n2 => uns (plub p1 p2) (Z.min n1 n2)
| Uns p n, _ => uns (plub p (provenance w)) n
| _, Uns p n => uns (plub (provenance v) p) n
| Sgn p1 n1, Sgn p2 n2 => sgn (plub p1 p2) (Z.max n1 n2)
| _, _ => ntop2 v w
end.

Lemma and_sound:
forall v w x y, vmatch v x -> vmatch w y -> vmatch (Val.and v w) (and x y).
Proof.
assert (UNS_l: forall i j n, is_uns n i -> is_uns n (Int.and i j)).
{
intros; red; intros. rewrite Int.bits_and by auto. rewrite (H m) by auto.
apply andb_false_l.
}
assert (UNS_r: forall i j n, is_uns n i -> is_uns n (Int.and j i)).
{
intros. rewrite Int.and_commut. eauto.
}
assert (UNS: forall i j n m, is_uns n i -> is_uns m j -> is_uns (Z.min n m) (Int.and i j)).
{
intros. apply Z.min_case; auto.
}
assert (SGN: forall i j n m, is_sgn n i -> is_sgn m j -> is_sgn (Z.max n m) (Int.and i j)).
{
intros; red; intros. rewrite ! Int.bits_and by auto with va.
rewrite H by auto with va. rewrite H0 by auto with va. auto.
}
intros. unfold and, Val.and; inv H; eauto with va; inv H0; eauto with va.
Qed.

Definition or (v w: aval) :=
match v, w with
| I i1, I i2 => I (Int.or i1 i2)
| I i, Uns p n | Uns p n, I i => uns p (Z.max n (usize i))
| Uns p1 n1, Uns p2 n2 => uns (plub p1 p2) (Z.max n1 n2)
| Sgn p1 n1, Sgn p2 n2 => sgn (plub p1 p2) (Z.max n1 n2)
| _, _ => ntop2 v w
end.

Lemma or_sound:
forall v w x y, vmatch v x -> vmatch w y -> vmatch (Val.or v w) (or x y).
Proof.
assert (UNS: forall i j n m, is_uns n i -> is_uns m j -> is_uns (Z.max n m) (Int.or i j)).
{
intros; red; intros. rewrite Int.bits_or by auto.
rewrite H by extlia. rewrite H0 by extlia. auto.
}
assert (SGN: forall i j n m, is_sgn n i -> is_sgn m j -> is_sgn (Z.max n m) (Int.or i j)).
{
intros; red; intros. rewrite ! Int.bits_or by extlia.
rewrite H by extlia. rewrite H0 by extlia. auto.
}
intros. unfold or, Val.or; inv H; eauto with va; inv H0; eauto with va.
Qed.

Definition xor (v w: aval) :=
match v, w with
| I i1, I i2 => I (Int.xor i1 i2)
| I i, Uns p n | Uns p n, I i => uns p (Z.max n (usize i))
| Uns p1 n1, Uns p2 n2 => uns (plub p1 p2) (Z.max n1 n2)
| Sgn p1 n1, Sgn p2 n2 => sgn (plub p1 p2) (Z.max n1 n2)
| _, _ => ntop2 v w
end.

Lemma xor_sound:
forall v w x y, vmatch v x -> vmatch w y -> vmatch (Val.xor v w) (xor x y).
Proof.
assert (UNS: forall i j n m, is_uns n i -> is_uns m j -> is_uns (Z.max n m) (Int.xor i j)).
{
intros; red; intros. rewrite Int.bits_xor by auto.
rewrite H by extlia. rewrite H0 by extlia. auto.
}
assert (SGN: forall i j n m, is_sgn n i -> is_sgn m j -> is_sgn (Z.max n m) (Int.xor i j)).
{
intros; red; intros. rewrite ! Int.bits_xor by extlia.
rewrite H by extlia. rewrite H0 by extlia. auto.
}
intros. unfold xor, Val.xor; inv H; eauto with va; inv H0; eauto with va.
Qed.

Definition notint (v: aval) :=
match v with
| I i => I (Int.not i)
| Uns p n => sgn p (n + 1)
| Sgn p n => Sgn p n
| _ => ntop1 v
end.

Lemma notint_sound:
forall v x, vmatch v x -> vmatch (Val.notint v) (notint x).
Proof.
assert (SGN: forall n i, is_sgn n i -> is_sgn n (Int.not i)).
{
intros; red; intros. rewrite ! Int.bits_not by lia.
f_equal. apply H; auto.
}
intros. unfold Val.notint, notint; inv H; eauto with va.
Qed.

Definition rol (x y: aval) :=
match y, x with
| I j, I i => I(Int.rol i j)
| I j, Uns p n => uns p (n + Int.unsigned j)
| I j, Sgn p n => if zlt n Int.zwordsize then sgn p (n + Int.unsigned j) else ntop1 x
| _, _ => ntop1 x
end.

Lemma rol_sound:
forall v w x y, vmatch v x -> vmatch w y -> vmatch (Val.rol v w) (rol x y).
Proof.
intros.
assert (DEFAULT: forall p, vmatch (Val.rol v w) (Num p)).
{
destruct v; destruct w; simpl; constructor.
}
unfold rol; destruct y; try apply DEFAULT; auto. inv H0. unfold Val.rol.
inv H; auto with va.
- apply vmatch_uns. red; intros. rewrite Int.bits_rol by auto.
generalize (Int.unsigned_range n); intros.
rewrite Z.mod_small by lia.
apply H1. lia. lia.
- destruct (zlt n0 Int.zwordsize); auto with va.
apply vmatch_sgn. red; intros. rewrite ! Int.bits_rol by lia.
generalize (Int.unsigned_range n); intros.
rewrite ! Z.mod_small by lia.
rewrite H1 by lia. symmetry. rewrite H1 by lia. auto.
- destruct (zlt n0 Int.zwordsize); auto with va.
Qed.

Definition ror (x y: aval) :=
match y, x with
| I j, I i => I(Int.ror i j)
| _, _ => ntop1 x
end.

Lemma ror_sound:
forall v w x y, vmatch v x -> vmatch w y -> vmatch (Val.ror v w) (ror x y).
Proof.
intros.
assert (DEFAULT: forall p, vmatch (Val.ror v w) (Num p)).
{
destruct v; destruct w; simpl; constructor.
}
unfold ror; destruct y; try apply DEFAULT; auto. inv H0. unfold Val.ror.
inv H; auto with va.
Qed.

Definition rolm (x: aval) (amount mask: int) :=
and (rol x (I amount)) (I mask).

Lemma rolm_sound:
vmatch v x -> vmatch (Val.rolm v amount mask) (rolm x amount mask).
Proof.
intros.
replace (Val.rolm v amount mask) with (Val.and (Val.rol v (Vint amount)) (Vint mask)).
apply and_sound. apply rol_sound. auto. constructor. constructor.
destruct v; auto.
Qed.

Integer arithmetic operations

Definition neg := unop_int Int.neg.

Lemma neg_sound:
forall v x, vmatch v x -> vmatch (Val.neg v) (neg x).
Proof (unop_int_sound Int.neg).

Definition add (x y: aval) :=
match x, y with
| I i, I j => I (Int.add i j)
| Ptr p, I i | I i, Ptr p => Ptr (if Archi.ptr64 then poffset p else padd p (Ptrofs.of_int i))
| Ptr p, _ | _, Ptr p => Ptr (poffset p)
| Ifptr p, I i | I i, Ifptr p => Ifptr (if Archi.ptr64 then poffset p else padd p (Ptrofs.of_int i))
| Ifptr p, Ifptr q => Ifptr (plub (poffset p) (poffset q))
| Ifptr p, _ | _, Ifptr p => Ifptr (poffset p)
| _, _ => ntop2 x y
end.

forall v w x y, vmatch v x -> vmatch w y -> vmatch (Val.add v w) (add x y).
Proof.
- inv H; inv H0; constructor.
- inv H; inv H0; constructor;
((apply padd_sound; assumption) || (eapply poffset_sound; eassumption) || idtac).
apply pmatch_lub_r. eapply poffset_sound; eauto.
apply pmatch_lub_l. eapply poffset_sound; eauto.
Qed.

Definition sub (v w: aval) :=
match v, w with
| I i1, I i2 => I (Int.sub i1 i2)
| Ptr p, I i => if Archi.ptr64 then Ifptr (poffset p) else Ptr (psub p (Ptrofs.of_int i))
| Ptr p, _ => Ifptr (poffset p)
| Ifptr p, I i => if Archi.ptr64 then Ifptr (plub (poffset p) (provenance w)) else Ifptr (psub p (Ptrofs.of_int i))
| Ifptr p, _ => Ifptr (plub (poffset p) (provenance w))
| _, _ => ntop2 v w
end.

Lemma sub_sound:
forall v w x y, vmatch v x -> vmatch w y -> vmatch (Val.sub v w) (sub x y).
Proof.
intros. unfold Val.sub, sub. destruct Archi.ptr64.
- inv H; inv H0; eauto with va.
- inv H; inv H0; try (destruct (eq_block b b0)); eauto using psub_sound, poffset_sound, pmatch_lub_l with va.
Qed.

Definition mul := binop_int Int.mul.

Lemma mul_sound:
forall v x w y, vmatch v x -> vmatch w y -> vmatch (Val.mul v w) (mul x y).
Proof (binop_int_sound Int.mul).

Definition mulhs := binop_int Int.mulhs.

Lemma mulhs_sound:
forall v x w y, vmatch v x -> vmatch w y -> vmatch (Val.mulhs v w) (mulhs x y).
Proof (binop_int_sound Int.mulhs).

Definition mulhu := binop_int Int.mulhu.

Lemma mulhu_sound:
forall v x w y, vmatch v x -> vmatch w y -> vmatch (Val.mulhu v w) (mulhu x y).
Proof (binop_int_sound Int.mulhu).

Definition divs (v w: aval) :=
match w, v with
| I i2, I i1 =>
if Int.eq i2 Int.zero
|| Int.eq i1 (Int.repr Int.min_signed) && Int.eq i2 Int.mone
then if va_strict tt then Vbot else ntop
else I (Int.divs i1 i2)
| _, _ => ntop2 v w
end.

Lemma divs_sound:
forall v w u x y, vmatch v x -> vmatch w y -> Val.divs v w = Some u -> vmatch u (divs x y).
Proof.
intros. destruct v; destruct w; try discriminate; simpl in H1.
destruct (Int.eq i0 Int.zero
|| Int.eq i (Int.repr Int.min_signed) && Int.eq i0 Int.mone) eqn:E; inv H1.
inv H; inv H0; auto with va. simpl. rewrite E. constructor.
Qed.

Definition divu (v w: aval) :=
match w, v with
| I i2, I i1 =>
if Int.eq i2 Int.zero
then if va_strict tt then Vbot else ntop
else I (Int.divu i1 i2)
| _, _ => ntop2 v w
end.

Lemma divu_sound:
forall v w u x y, vmatch v x -> vmatch w y -> Val.divu v w = Some u -> vmatch u (divu x y).
Proof.
intros. destruct v; destruct w; try discriminate; simpl in H1.
destruct (Int.eq i0 Int.zero) eqn:E; inv H1.
inv H; inv H0; auto with va. simpl. rewrite E. constructor.
Qed.

Definition mods (v w: aval) :=
match w, v with
| I i2, I i1 =>
if Int.eq i2 Int.zero
|| Int.eq i1 (Int.repr Int.min_signed) && Int.eq i2 Int.mone
then if va_strict tt then Vbot else ntop
else I (Int.mods i1 i2)
| _, _ => ntop2 v w
end.

Lemma mods_sound:
forall v w u x y, vmatch v x -> vmatch w y -> Val.mods v w = Some u -> vmatch u (mods x y).
Proof.
intros. destruct v; destruct w; try discriminate; simpl in H1.
destruct (Int.eq i0 Int.zero
|| Int.eq i (Int.repr Int.min_signed) && Int.eq i0 Int.mone) eqn:E; inv H1.
inv H; inv H0; auto with va. simpl. rewrite E. constructor.
Qed.

Definition modu (v w: aval) :=
match w, v with
| I i2, I i1 =>
if Int.eq i2 Int.zero
then if va_strict tt then Vbot else ntop
else I (Int.modu i1 i2)
| I i2, _ => uns (provenance v) (usize i2)
| _, _ => ntop2 v w
end.

Lemma modu_sound:
forall v w u x y, vmatch v x -> vmatch w y -> Val.modu v w = Some u -> vmatch u (modu x y).
Proof.
assert (UNS: forall i j, j <> Int.zero -> is_uns (usize j) (Int.modu i j)).
{
intros. apply is_uns_mon with (usize (Int.modu i j)); auto with va.
unfold usize, Int.size. apply Zsize_monotone.
generalize (Int.unsigned_range_2 j); intros RANGE.
assert (Int.unsigned j <> 0).
{ red; intros; elim H. rewrite <- (Int.repr_unsigned j). rewrite H0. auto. }
exploit (Z_mod_lt (Int.unsigned i) (Int.unsigned j)). lia. intros MOD.
unfold Int.modu. rewrite Int.unsigned_repr. lia. lia.
}
intros. destruct v; destruct w; try discriminate; simpl in H1.
destruct (Int.eq i0 Int.zero) eqn:Z; inv H1.
assert (i0 <> Int.zero) by (generalize (Int.eq_spec i0 Int.zero); rewrite Z; auto).
unfold modu. inv H; inv H0; auto with va. rewrite Z. constructor.
Qed.

Definition shrx (v w: aval) :=
match v, w with
| I i, I j => if Int.ltu j (Int.repr 31) then I(Int.shrx i j) else ntop
| _, _ => ntop1 v
end.

Lemma shrx_sound:
forall v w u x y, vmatch v x -> vmatch w y -> Val.shrx v w = Some u -> vmatch u (shrx x y).
Proof.
intros.
destruct v; destruct w; try discriminate; simpl in H1.
destruct (Int.ltu i0 (Int.repr 31)) eqn:LTU; inv H1.
unfold shrx; inv H; auto with va; inv H0; auto with va.
rewrite LTU; auto with va.
Qed.

64-bit integer operations

Definition shift_long (sem: int64 -> int -> int64) (v w: aval) :=
match w with
| I amount =>
if Int.ltu amount Int64.iwordsize' then
match v with
| L i => L (sem i amount)
| _ => ntop1 v
end
else ntop1 v
| _ => ntop1 v
end.

Lemma shift_long_sound:
forall sem v w x y,
vmatch v x -> vmatch w y ->
vmatch (match v, w with
| Vlong i, Vint j => if Int.ltu j Int64.iwordsize'
then Vlong (sem i j) else Vundef
| _, _ => Vundef end)
(shift_long sem x y).
Proof.
intros.
assert (DEFAULT:
vmatch (match v, w with
| Vlong i, Vint j => if Int.ltu j Int64.iwordsize'
then Vlong (sem i j) else Vundef
| _, _ => Vundef end)
(ntop1 x)).
{ destruct v; try constructor; destruct w; try constructor.
destruct (Int.ltu i0 Int64.iwordsize'); constructor. }
unfold shift_long. destruct y; auto.
destruct (Int.ltu n Int64.iwordsize') eqn:LT; auto.
destruct x; auto.
inv H; inv H0. rewrite LT. constructor.
Qed.

Definition shll := shift_long Int64.shl'.

Lemma shll_sound:
forall v w x y, vmatch v x -> vmatch w y -> vmatch (Val.shll v w) (shll x y).
Proof (shift_long_sound Int64.shl').

Definition shrl := shift_long Int64.shr'.

Lemma shrl_sound:
forall v w x y, vmatch v x -> vmatch w y -> vmatch (Val.shrl v w) (shrl x y).
Proof (shift_long_sound Int64.shr').

Definition shrlu := shift_long Int64.shru'.

Lemma shrlu_sound:
forall v w x y, vmatch v x -> vmatch w y -> vmatch (Val.shrlu v w) (shrlu x y).
Proof (shift_long_sound Int64.shru').

Definition andl := binop_long Int64.and.

Lemma andl_sound:
forall v x w y, vmatch v x -> vmatch w y -> vmatch (Val.andl v w) (andl x y).
Proof (binop_long_sound Int64.and).

Definition orl := binop_long Int64.or.

Lemma orl_sound:
forall v x w y, vmatch v x -> vmatch w y -> vmatch (Val.orl v w) (orl x y).
Proof (binop_long_sound Int64.or).

Definition xorl := binop_long Int64.xor.

Lemma xorl_sound:
forall v x w y, vmatch v x -> vmatch w y -> vmatch (Val.xorl v w) (xorl x y).
Proof (binop_long_sound Int64.xor).

Definition notl := unop_long Int64.not.

Lemma notl_sound:
forall v x, vmatch v x -> vmatch (Val.notl v) (notl x).
Proof (unop_long_sound Int64.not).

Definition rotate_long (sem: int64 -> int64 -> int64) (v w: aval) :=
match v, w with
| L i, I amount => L (sem i (Int64.repr (Int.unsigned amount)))
| _, _ => ntop1 v
end.

Lemma rotate_long_sound:
forall sem v w x y,
vmatch v x -> vmatch w y ->
vmatch (match v, w with
| Vlong i, Vint j => Vlong (sem i (Int64.repr (Int.unsigned j)))
| _, _ => Vundef end)
(rotate_long sem x y).
Proof.
intros.
assert (DEFAULT:
vmatch (match v, w with
| Vlong i, Vint j => Vlong (sem i (Int64.repr (Int.unsigned j)))
| _, _ => Vundef end)
(ntop1 x)).
{ destruct v; try constructor. destruct w; constructor. }
unfold rotate_long. destruct x; auto. destruct y; auto. inv H; inv H0. constructor.
Qed.

Definition roll := rotate_long Int64.rol.

Lemma roll_sound:
forall v w x y, vmatch v x -> vmatch w y -> vmatch (Val.roll v w) (roll x y).
Proof (rotate_long_sound Int64.rol).

Definition rorl := rotate_long Int64.ror.

Lemma rorl_sound:
forall v w x y, vmatch v x -> vmatch w y -> vmatch (Val.rorl v w) (rorl x y).
Proof (rotate_long_sound Int64.ror).

Definition negl := unop_long Int64.neg.

Lemma negl_sound:
forall v x, vmatch v x -> vmatch (Val.negl v) (negl x).
Proof (unop_long_sound Int64.neg).

Definition addl (x y: aval) :=
match x, y with
| L i, L j => L (Int64.add i j)
| Ptr p, L i | L i, Ptr p => Ptr (if Archi.ptr64 then padd p (Ptrofs.of_int64 i) else poffset p)
| Ptr p, _ | _, Ptr p => Ptr (poffset p)
| Ifptr p, L i | L i, Ifptr p => Ifptr (if Archi.ptr64 then padd p (Ptrofs.of_int64 i) else poffset p)
| Ifptr p, Ifptr q => Ifptr (plub (poffset p) (poffset q))
| Ifptr p, _ | _, Ifptr p => Ifptr (poffset p)
| _, _ => ntop2 x y
end.

forall v w x y, vmatch v x -> vmatch w y -> vmatch (Val.addl v w) (addl x y).
Proof.
- inv H; inv H0; constructor;
((apply padd_sound; assumption) || (eapply poffset_sound; eassumption) || idtac).
apply pmatch_lub_r. eapply poffset_sound; eauto.
apply pmatch_lub_l. eapply poffset_sound; eauto.
- inv H; inv H0; constructor.
Qed.

Definition subl (v w: aval) :=
match v, w with
| L i1, L i2 => L (Int64.sub i1 i2)
| Ptr p, L i => if Archi.ptr64 then Ptr (psub p (Ptrofs.of_int64 i)) else Ifptr (poffset p)
| Ptr p, _ => Ifptr (poffset p)
| Ifptr p, L i => if Archi.ptr64 then Ifptr (psub p (Ptrofs.of_int64 i)) else Ifptr (plub (poffset p) (provenance w))
| Ifptr p, _ => Ifptr (plub (poffset p) (provenance w))
| _, _ => ntop2 v w
end.

Lemma subl_sound:
forall v w x y, vmatch v x -> vmatch w y -> vmatch (Val.subl v w) (subl x y).
Proof.
intros. unfold Val.subl, subl. destruct Archi.ptr64.
- inv H; inv H0; try (destruct (eq_block b b0)); eauto using psub_sound, poffset_sound, pmatch_lub_l with va.
- inv H; inv H0; eauto with va.
Qed.

Definition mull := binop_long Int64.mul.

Lemma mull_sound:
forall v x w y, vmatch v x -> vmatch w y -> vmatch (Val.mull v w) (mull x y).
Proof (binop_long_sound Int64.mul).

Definition mullhs := binop_long Int64.mulhs.

Lemma mullhs_sound:
forall v x w y, vmatch v x -> vmatch w y -> vmatch (Val.mullhs v w) (mullhs x y).
Proof (binop_long_sound Int64.mulhs).

Definition mullhu := binop_long Int64.mulhu.

Lemma mullhu_sound:
forall v x w y, vmatch v x -> vmatch w y -> vmatch (Val.mullhu v w) (mullhu x y).
Proof (binop_long_sound Int64.mulhu).

Definition divls (v w: aval) :=
match w, v with
| L i2, L i1 =>
if Int64.eq i2 Int64.zero
|| Int64.eq i1 (Int64.repr Int64.min_signed) && Int64.eq i2 Int64.mone
then if va_strict tt then Vbot else ntop
else L (Int64.divs i1 i2)
| _, _ => ntop2 v w
end.

Lemma divls_sound:
forall v w u x y, vmatch v x -> vmatch w y -> Val.divls v w = Some u -> vmatch u (divls x y).
Proof.
intros. destruct v; destruct w; try discriminate; simpl in H1.
destruct (Int64.eq i0 Int64.zero
|| Int64.eq i (Int64.repr Int64.min_signed) && Int64.eq i0 Int64.mone) eqn:E; inv H1.
inv H; inv H0; auto with va. simpl. rewrite E. constructor.
Qed.

Definition divlu (v w: aval) :=
match w, v with
| L i2, L i1 =>
if Int64.eq i2 Int64.zero
then if va_strict tt then Vbot else ntop
else L (Int64.divu i1 i2)
| _, _ => ntop2 v w
end.

Lemma divlu_sound:
forall v w u x y, vmatch v x -> vmatch w y -> Val.divlu v w = Some u -> vmatch u (divlu x y).
Proof.
intros. destruct v; destruct w; try discriminate; simpl in H1.
destruct (Int64.eq i0 Int64.zero) eqn:E; inv H1.
inv H; inv H0; auto with va. simpl. rewrite E. constructor.
Qed.

Definition modls (v w: aval) :=
match w, v with
| L i2, L i1 =>
if Int64.eq i2 Int64.zero
|| Int64.eq i1 (Int64.repr Int64.min_signed) && Int64.eq i2 Int64.mone
then if va_strict tt then Vbot else ntop
else L (Int64.mods i1 i2)
| _, _ => ntop2 v w
end.

Lemma modls_sound:
forall v w u x y, vmatch v x -> vmatch w y -> Val.modls v w = Some u -> vmatch u (modls x y).
Proof.
intros. destruct v; destruct w; try discriminate; simpl in H1.
destruct (Int64.eq i0 Int64.zero
|| Int64.eq i (Int64.repr Int64.min_signed) && Int64.eq i0 Int64.mone) eqn:E; inv H1.
inv H; inv H0; auto with va. simpl. rewrite E. constructor.
Qed.

Definition modlu (v w: aval) :=
match w, v with
| L i2, L i1 =>
if Int64.eq i2 Int64.zero
then if va_strict tt then Vbot else ntop
else L (Int64.modu i1 i2)
| _, _ => ntop2 v w
end.

Lemma modlu_sound:
forall v w u x y, vmatch v x -> vmatch w y -> Val.modlu v w = Some u -> vmatch u (modlu x y).
Proof.
intros. destruct v; destruct w; try discriminate; simpl in H1.
destruct (Int64.eq i0 Int64.zero) eqn:E; inv H1.
inv H; inv H0; auto with va. simpl. rewrite E. constructor.
Qed.

Definition shrxl (v w: aval) :=
match v, w with
| L i, I j => if Int.ltu j (Int.repr 63) then L(Int64.shrx' i j) else ntop
| _, _ => ntop1 v
end.

Lemma shrxl_sound:
forall v w u x y, vmatch v x -> vmatch w y -> Val.shrxl v w = Some u -> vmatch u (shrxl x y).
Proof.
intros.
destruct v; destruct w; try discriminate; simpl in H1.
destruct (Int.ltu i0 (Int.repr 63)) eqn:LTU; inv H1.
unfold shrxl; inv H; auto with va; inv H0; auto with va.
rewrite LTU; auto with va.
Qed.

Definition rolml (x: aval) (amount: int) (mask: int64) :=
andl (roll x (I amount)) (L mask).

Lemma rolml_sound:
vmatch v x -> vmatch (Val.rolml v amount mask) (rolml x amount mask).
Proof.
intros.
replace (Val.rolml v amount mask) with (Val.andl (Val.roll v (Vint amount)) (Vlong mask)).
apply andl_sound. apply roll_sound. auto. constructor. constructor.
destruct v; auto.
Qed.

Pointer operations

Definition offset_ptr (v: aval) (n: ptrofs) :=
match v with
| Ptr p => Ptr (padd p n)
| Ifptr p => Ifptr (padd p n)
| _ => ntop1 v
end.

Lemma offset_ptr_sound:
forall v x n, vmatch v x -> vmatch (Val.offset_ptr v n) (offset_ptr x n).
Proof.
intros. unfold Val.offset_ptr, offset_ptr.
inv H; constructor; apply padd_sound; assumption.
Qed.

Floating-point arithmetic operations

Definition negf := unop_float Float.neg.

Lemma negf_sound:
forall v x, vmatch v x -> vmatch (Val.negf v) (negf x).
Proof (unop_float_sound Float.neg).

Definition absf := unop_float Float.abs.

Lemma absf_sound:
forall v x, vmatch v x -> vmatch (Val.absf v) (absf x).
Proof (unop_float_sound Float.abs).

forall v x w y, vmatch v x -> vmatch w y -> vmatch (Val.addf v w) (addf x y).

Definition subf := binop_float Float.sub.

Lemma subf_sound:
forall v x w y, vmatch v x -> vmatch w y -> vmatch (Val.subf v w) (subf x y).
Proof (binop_float_sound Float.sub).

Definition mulf := binop_float Float.mul.

Lemma mulf_sound:
forall v x w y, vmatch v x -> vmatch w y -> vmatch (Val.mulf v w) (mulf x y).
Proof (binop_float_sound Float.mul).

Definition divf := binop_float Float.div.

Lemma divf_sound:
forall v x w y, vmatch v x -> vmatch w y -> vmatch (Val.divf v w) (divf x y).
Proof (binop_float_sound Float.div).

Definition sqrtf := unop_float Float.sqrt.

Lemma sqrtf_sound:
forall v x, vmatch v x -> vmatch (Val.sqrtf v) (sqrtf x).
Proof (unop_float_sound Float.sqrt).

Definition negfs := unop_single Float32.neg.

Lemma negfs_sound:
forall v x, vmatch v x -> vmatch (Val.negfs v) (negfs x).
Proof (unop_single_sound Float32.neg).

Definition absfs := unop_single Float32.abs.

Lemma absfs_sound:
forall v x, vmatch v x -> vmatch (Val.absfs v) (absfs x).
Proof (unop_single_sound Float32.abs).

forall v x w y, vmatch v x -> vmatch w y -> vmatch (Val.addfs v w) (addfs x y).

Definition subfs := binop_single Float32.sub.

Lemma subfs_sound:
forall v x w y, vmatch v x -> vmatch w y -> vmatch (Val.subfs v w) (subfs x y).
Proof (binop_single_sound Float32.sub).

Definition mulfs := binop_single Float32.mul.

Lemma mulfs_sound:
forall v x w y, vmatch v x -> vmatch w y -> vmatch (Val.mulfs v w) (mulfs x y).
Proof (binop_single_sound Float32.mul).

Definition divfs := binop_single Float32.div.

Lemma divfs_sound:
forall v x w y, vmatch v x -> vmatch w y -> vmatch (Val.divfs v w) (divfs x y).
Proof (binop_single_sound Float32.div).

Definition sqrtfs := unop_single Float32.sqrt.

Lemma sqrtfs_sound:
forall v x, vmatch v x -> vmatch (Val.sqrtfs v) (sqrtfs x).
Proof (unop_single_sound Float32.sqrt).

Conversions

Definition zero_ext (nbits: Z) (v: aval) :=
match v with
| I i => I (Int.zero_ext nbits i)
| Uns p n => uns p (Z.min n nbits)
| _ => uns (provenance v) nbits
end.

Lemma zero_ext_sound:
forall nbits v x, vmatch v x -> vmatch (Val.zero_ext nbits v) (zero_ext nbits x).
Proof.
assert (DFL: forall nbits i, is_uns nbits (Int.zero_ext nbits i)).
{
intros; red; intros. rewrite Int.bits_zero_ext by lia. apply zlt_false; auto.
}
intros. inv H; simpl; auto with va. apply vmatch_uns.
red; intros. zify.
rewrite Int.bits_zero_ext by lia.
destruct (zlt m nbits); auto. apply H1; lia.
Qed.

Definition sign_ext (nbits: Z) (v: aval) :=
if zle nbits 0 then Uns (provenance v) 0 else
match v with
| I i => I (Int.sign_ext nbits i)
| Uns p n => if zlt n nbits then Uns p n else sgn p nbits
| Sgn p n => sgn p (Z.min n nbits)
| _ => sgn (provenance v) nbits
end.

Lemma sign_ext_sound:
forall nbits v x, vmatch v x -> vmatch (Val.sign_ext nbits v) (sign_ext nbits x).
Proof.
assert (DFL: forall p nbits i, 0 < nbits -> vmatch (Vint (Int.sign_ext nbits i)) (sgn p nbits)).
{
intros. apply vmatch_sgn. apply is_sign_ext_sgn; auto with va.
}
intros. unfold sign_ext. destruct (zle nbits 0).
- destruct v; simpl; auto with va. constructor. lia.
rewrite Int.sign_ext_below by auto. red; intros; apply Int.bits_zero.
- inv H; simpl; auto with va.
+ destruct (zlt n nbits); eauto with va.
constructor; auto. eapply is_sign_ext_uns; eauto with va.
+ destruct (zlt n nbits); auto with va.
+ apply vmatch_sgn. apply is_sign_ext_sgn; auto with va.
apply Z.min_case; auto with va.
Qed.

Definition zero_ext_l (s: Z) := unop_long (Int64.zero_ext s).

Lemma zero_ext_l_sound:
forall s v x, vmatch v x -> vmatch (Val.zero_ext_l s v) (zero_ext_l s x).
Proof.
intros s. exact (unop_long_sound (Int64.zero_ext s)).
Qed.

Definition sign_ext_l (s: Z) := unop_long (Int64.sign_ext s).

Lemma sign_ext_l_sound:
forall s v x, vmatch v x -> vmatch (Val.sign_ext_l s v) (sign_ext_l s x).
Proof.
intros s. exact (unop_long_sound (Int64.sign_ext s)).
Qed.

Definition longofint (v: aval) :=
match v with
| I i => L (Int64.repr (Int.signed i))
| _ => ntop1 v
end.

Lemma longofint_sound:
forall v x, vmatch v x -> vmatch (Val.longofint v) (longofint x).
Proof.
unfold Val.longofint, longofint; intros; inv H; auto with va.
Qed.

Definition longofintu (v: aval) :=
match v with
| I i => L (Int64.repr (Int.unsigned i))
| _ => ntop1 v
end.

Lemma longofintu_sound:
forall v x, vmatch v x -> vmatch (Val.longofintu v) (longofintu x).
Proof.
unfold Val.longofintu, longofintu; intros; inv H; auto with va.
Qed.

Definition singleoffloat (v: aval) :=
match v with
| F f => FS (Float.to_single f)
| _ => ntop1 v
end.

Lemma singleoffloat_sound:
forall v x, vmatch v x -> vmatch (Val.singleoffloat v) (singleoffloat x).
Proof.
intros.
assert (DEFAULT: vmatch (Val.singleoffloat v) (ntop1 x)).
{ destruct v; constructor. }
destruct x; auto. inv H. constructor.
Qed.

Definition floatofsingle (v: aval) :=
match v with
| FS f => F (Float.of_single f)
| _ => ntop1 v
end.

Lemma floatofsingle_sound:
forall v x, vmatch v x -> vmatch (Val.floatofsingle v) (floatofsingle x).
Proof.
intros.
assert (DEFAULT: vmatch (Val.floatofsingle v) (ntop1 x)).
{ destruct v; constructor. }
destruct x; auto. inv H. constructor.
Qed.

Definition intoffloat (x: aval) :=
match x with
| F f =>
match Float.to_int f with
| Some i => I i
| None => if va_strict tt then Vbot else ntop
end
| _ => ntop1 x
end.

Lemma intoffloat_sound:
forall v x w, vmatch v x -> Val.intoffloat v = Some w -> vmatch w (intoffloat x).
Proof.
unfold Val.intoffloat; intros. destruct v; try discriminate.
destruct (Float.to_int f) as [i|] eqn:E; simpl in H0; inv H0.
inv H; simpl; auto with va. rewrite E; constructor.
Qed.

Definition intuoffloat (x: aval) :=
match x with
| F f =>
match Float.to_intu f with
| Some i => I i
| None => if va_strict tt then Vbot else ntop
end
| _ => ntop1 x
end.

Lemma intuoffloat_sound:
forall v x w, vmatch v x -> Val.intuoffloat v = Some w -> vmatch w (intuoffloat x).
Proof.
unfold Val.intuoffloat; intros. destruct v; try discriminate.
destruct (Float.to_intu f) as [i|] eqn:E; simpl in H0; inv H0.
inv H; simpl; auto with va. rewrite E; constructor.
Qed.

Definition floatofint (x: aval) :=
match x with
| I i => F(Float.of_int i)
| _ => ntop1 x
end.

Lemma floatofint_sound:
forall v x w, vmatch v x -> Val.floatofint v = Some w -> vmatch w (floatofint x).
Proof.
unfold Val.floatofint; intros. destruct v; inv H0.
inv H; simpl; auto with va.
Qed.

Definition floatofintu (x: aval) :=
match x with
| I i => F(Float.of_intu i)
| _ => ntop1 x
end.

Lemma floatofintu_sound:
forall v x w, vmatch v x -> Val.floatofintu v = Some w -> vmatch w (floatofintu x).
Proof.
unfold Val.floatofintu; intros. destruct v; inv H0.
inv H; simpl; auto with va.
Qed.

Definition intofsingle (x: aval) :=
match x with
| FS f =>
match Float32.to_int f with
| Some i => I i
| None => if va_strict tt then Vbot else ntop
end
| _ => ntop1 x
end.

Lemma intofsingle_sound:
forall v x w, vmatch v x -> Val.intofsingle v = Some w -> vmatch w (intofsingle x).
Proof.
unfold Val.intofsingle; intros. destruct v; try discriminate.
destruct (Float32.to_int f) as [i|] eqn:E; simpl in H0; inv H0.
inv H; simpl; auto with va. rewrite E; constructor.
Qed.

Definition intofsingle_ne (x: aval) :=
match x with
| FS f =>
match Float32.to_int_ne f with
| Some i => I i
| None => if va_strict tt then Vbot else ntop
end
| _ => ntop1 x
end.

Lemma intofsingle_ne_sound:
forall v x w, vmatch v x -> Val.intofsingle_ne v = Some w -> vmatch w (intofsingle_ne x).
Proof.
unfold Val.intofsingle_ne; intros. destruct v; try discriminate.
destruct (Float32.to_int_ne f) as [i|] eqn:E; simpl in H0; inv H0.
inv H; simpl; auto with va. rewrite E; constructor.
Qed.

Definition intuofsingle (x: aval) :=
match x with
| FS f =>
match Float32.to_intu f with
| Some i => I i
| None => if va_strict tt then Vbot else ntop
end
| _ => ntop1 x
end.

Lemma intuofsingle_sound:
forall v x w, vmatch v x -> Val.intuofsingle v = Some w -> vmatch w (intuofsingle x).
Proof.
unfold Val.intuofsingle; intros. destruct v; try discriminate.
destruct (Float32.to_intu f) as [i|] eqn:E; simpl in H0; inv H0.
inv H; simpl; auto with va. rewrite E; constructor.
Qed.

Definition intuofsingle_ne (x: aval) :=
match x with
| FS f =>
match Float32.to_intu_ne f with
| Some i => I i
| None => if va_strict tt then Vbot else ntop
end
| _ => ntop1 x
end.

Lemma intuofsingle_ne_sound:
forall v x w, vmatch v x -> Val.intuofsingle_ne v = Some w -> vmatch w (intuofsingle_ne x).
Proof.
unfold Val.intuofsingle_ne; intros. destruct v; try discriminate.
destruct (Float32.to_intu_ne f) as [i|] eqn:E; simpl in H0; inv H0.
inv H; simpl; auto with va. rewrite E; constructor.
Qed.

Definition singleofint (x: aval) :=
match x with
| I i => FS(Float32.of_int i)
| _ => ntop1 x
end.

Lemma singleofint_sound:
forall v x w, vmatch v x -> Val.singleofint v = Some w -> vmatch w (singleofint x).
Proof.
unfold Val.singleofint; intros. destruct v; inv H0.
inv H; simpl; auto with va.
Qed.

Definition singleofintu (x: aval) :=
match x with
| I i => FS(Float32.of_intu i)
| _ => ntop1 x
end.

Lemma singleofintu_sound:
forall v x w, vmatch v x -> Val.singleofintu v = Some w -> vmatch w (singleofintu x).
Proof.
unfold Val.singleofintu; intros. destruct v; inv H0.
inv H; simpl; auto with va.
Qed.

Definition longoffloat (x: aval) :=
match x with
| F f =>
match Float.to_long f with
| Some i => L i
| None => if va_strict tt then Vbot else ntop
end
| _ => ntop1 x
end.

Lemma longoffloat_sound:
forall v x w, vmatch v x -> Val.longoffloat v = Some w -> vmatch w (longoffloat x).
Proof.
unfold Val.longoffloat; intros. destruct v; try discriminate.
destruct (Float.to_long f) as [i|] eqn:E; simpl in H0; inv H0.
inv H; simpl; auto with va. rewrite E; constructor.
Qed.

Definition longuoffloat (x: aval) :=
match x with
| F f =>
match Float.to_longu f with
| Some i => L i
| None => if va_strict tt then Vbot else ntop
end
| _ => ntop1 x
end.

Lemma longuoffloat_sound:
forall v x w, vmatch v x -> Val.longuoffloat v = Some w -> vmatch w (longuoffloat x).
Proof.
unfold Val.longuoffloat; intros. destruct v; try discriminate.
destruct (Float.to_longu f) as [i|] eqn:E; simpl in H0; inv H0.
inv H; simpl; auto with va. rewrite E; constructor.
Qed.

Definition longoffloat_ne (x: aval) :=
match x with
| F f =>
match Float.to_long_ne f with
| Some i => L i
| None => if va_strict tt then Vbot else ntop
end
| _ => ntop1 x
end.

Lemma longoffloat_ne_sound:
forall v x w, vmatch v x -> Val.longoffloat_ne v = Some w -> vmatch w (longoffloat_ne x).
Proof.
unfold Val.longoffloat_ne; intros. destruct v; try discriminate.
destruct (Float.to_long_ne f) as [i|] eqn:E; simpl in H0; inv H0.
inv H; simpl; auto with va. rewrite E; constructor.
Qed.

Definition longuoffloat_ne (x: aval) :=
match x with
| F f =>
match Float.to_longu_ne f with
| Some i => L i
| None => if va_strict tt then Vbot else ntop
end
| _ => ntop1 x
end.

Lemma longuoffloat_ne_sound:
forall v x w, vmatch v x -> Val.longuoffloat_ne v = Some w -> vmatch w (longuoffloat_ne x).
Proof.
unfold Val.longuoffloat_ne; intros. destruct v; try discriminate.
destruct (Float.to_longu_ne f) as [i|] eqn:E; simpl in H0; inv H0.
inv H; simpl; auto with va. rewrite E; constructor.
Qed.

Definition floatoflong (x: aval) :=
match x with
| L i => F(Float.of_long i)
| _ => ntop1 x
end.

Lemma floatoflong_sound:
forall v x w, vmatch v x -> Val.floatoflong v = Some w -> vmatch w (floatoflong x).
Proof.
unfold Val.floatoflong; intros. destruct v; inv H0.
inv H; simpl; auto with va.
Qed.

Definition floatoflongu (x: aval) :=
match x with
| L i => F(Float.of_longu i)
| _ => ntop1 x
end.

Lemma floatoflongu_sound:
forall v x w, vmatch v x -> Val.floatoflongu v = Some w -> vmatch w (floatoflongu x).
Proof.
unfold Val.floatoflongu; intros. destruct v; inv H0.
inv H; simpl; auto with va.
Qed.

Definition longofsingle (x: aval) :=
match x with
| FS f =>
match Float32.to_long f with
| Some i => L i
| None => if va_strict tt then Vbot else ntop
end
| _ => ntop1 x
end.

Lemma longofsingle_sound:
forall v x w, vmatch v x -> Val.longofsingle v = Some w -> vmatch w (longofsingle x).
Proof.
unfold Val.longofsingle; intros. destruct v; try discriminate.
destruct (Float32.to_long f) as [i|] eqn:E; simpl in H0; inv H0.
inv H; simpl; auto with va. rewrite E; constructor.
Qed.

Definition longuofsingle (x: aval) :=
match x with
| FS f =>
match Float32.to_longu f with
| Some i => L i
| None => if va_strict tt then Vbot else ntop
end
| _ => ntop1 x
end.

Lemma longuofsingle_sound:
forall v x w, vmatch v x -> Val.longuofsingle v = Some w -> vmatch w (longuofsingle x).
Proof.
unfold Val.longuofsingle; intros. destruct v; try discriminate.
destruct (Float32.to_longu f) as [i|] eqn:E; simpl in H0; inv H0.
inv H; simpl; auto with va. rewrite E; constructor.
Qed.

Definition singleoflong (x: aval) :=
match x with
| L i => FS(Float32.of_long i)
| _ => ntop1 x
end.

Lemma singleoflong_sound:
forall v x w, vmatch v x -> Val.singleoflong v = Some w -> vmatch w (singleoflong x).
Proof.
unfold Val.singleoflong; intros. destruct v; inv H0.
inv H; simpl; auto with va.
Qed.

Definition singleoflongu (x: aval) :=
match x with
| L i => FS(Float32.of_longu i)
| _ => ntop1 x
end.

Lemma singleoflongu_sound:
forall v x w, vmatch v x -> Val.singleoflongu v = Some w -> vmatch w (singleoflongu x).
Proof.
unfold Val.singleoflongu; intros. destruct v; inv H0.
inv H; simpl; auto with va.
Qed.

Definition floatofwords (x y: aval) :=
match x, y with
| I i, I j => F(Float.from_words i j)
| _, _ => ntop2 x y
end.

Lemma floatofwords_sound:
forall v w x y, vmatch v x -> vmatch w y -> vmatch (Val.floatofwords v w) (floatofwords x y).
Proof.
intros. unfold floatofwords; inv H; simpl; auto with va; inv H0; auto with va.
Qed.

Definition longofwords (x y: aval) :=
match y, x with
| I j, I i => L(Int64.ofwords i j)
| _, _ => ntop2 x y
end.

Lemma longofwords_sound:
forall v w x y, vmatch v x -> vmatch w y -> vmatch (Val.longofwords v w) (longofwords x y).
Proof.
intros. unfold longofwords; inv H0; inv H; simpl; auto with va.
Qed.

Definition loword (x: aval) :=
match x with
| L i => I(Int64.loword i)
| _ => ntop1 x
end.

Lemma loword_sound: forall v x, vmatch v x -> vmatch (Val.loword v) (loword x).
Proof.
destruct 1; simpl; auto with va.
Qed.

Definition hiword (x: aval) :=
match x with
| L i => I(Int64.hiword i)
| _ => ntop1 x
end.

Lemma hiword_sound: forall v x, vmatch v x -> vmatch (Val.hiword v) (hiword x).
Proof.
destruct 1; simpl; auto with va.
Qed.

Definition intoffloat_total (x: aval) :=
match x with
| F f =>
match Float.to_int f with
| Some i => I i
| None => ntop
end
| _ => ntop1 x
end.

Definition intuoffloat_total (x: aval) :=
match x with
| F f =>
match Float.to_intu f with
| Some i => I i
| None => ntop
end
| _ => ntop1 x
end.

Definition intofsingle_total (x: aval) :=
match x with
| FS f =>
match Float32.to_int f with
| Some i => I i
| None => ntop
end
| _ => ntop1 x
end.

Definition intuofsingle_total (x: aval) :=
match x with
| FS f =>
match Float32.to_intu f with
| Some i => I i
| None => ntop
end
| _ => ntop1 x
end.

Definition longoffloat_total (x: aval) :=
match x with
| F f =>
match Float.to_long f with
| Some i => L i
| None => ntop
end
| _ => ntop1 x
end.

Definition longuoffloat_total (x: aval) :=
match x with
| F f =>
match Float.to_longu f with
| Some i => L i
| None => ntop
end
| _ => ntop1 x
end.

Definition longofsingle_total (x: aval) :=
match x with
| FS f =>
match Float32.to_long f with
| Some i => L i
| None => ntop
end
| _ => ntop1 x
end.

Definition longuofsingle_total (x: aval) :=
match x with
| FS f =>
match Float32.to_longu f with
| Some i => L i
| None => ntop
end
| _ => ntop1 x
end.

Definition intofsingle_ne_total (x: aval) :=
match x with
| FS f =>
match Float32.to_int_ne f with
| Some i => I i
| None => ntop
end
| _ => ntop1 x
end.

Definition intuofsingle_ne_total (x: aval) :=
match x with
| FS f =>
match Float32.to_intu_ne f with
| Some i => I i
| None => ntop
end
| _ => ntop1 x
end.

Definition longoffloat_ne_total (x: aval) :=
match x with
| F f =>
match Float.to_long_ne f with
| Some i => L i
| None => ntop
end
| _ => ntop1 x
end.

Definition longuoffloat_ne_total (x: aval) :=
match x with
| F f =>
match Float.to_longu_ne f with
| Some i => L i
| None => ntop
end
| _ => ntop1 x
end.

Lemma intoffloat_total_sound:
forall v x
(MATCH : vmatch v x),
vmatch (Val.maketotal (Val.intoffloat v)) (intoffloat_total x).
Proof.
unfold Val.intoffloat, intoffloat_total. intros.
inv MATCH; simpl in *; try constructor.
all: destruct (Float.to_int f) as [i|] eqn:E; simpl; [auto with va | constructor].
Qed.

Lemma intuoffloat_total_sound:
forall v x
(MATCH : vmatch v x),
vmatch (Val.maketotal (Val.intuoffloat v)) (intuoffloat_total x).
Proof.
unfold Val.intoffloat, intoffloat_total. intros.
inv MATCH; simpl in *; try constructor.
all: destruct (Float.to_intu f) as [i|] eqn:E; simpl; [auto with va | constructor].
Qed.

Lemma intofsingle_total_sound:
forall v x
(MATCH : vmatch v x),
vmatch (Val.maketotal (Val.intofsingle v)) (intofsingle_total x).
Proof.
unfold Val.intofsingle, intofsingle_total. intros.
inv MATCH; simpl in *; try constructor.
all: destruct (Float32.to_int f) as [i|] eqn:E; simpl; [auto with va | constructor].
Qed.

Lemma intuofsingle_total_sound:
forall v x
(MATCH : vmatch v x),
vmatch (Val.maketotal (Val.intuofsingle v)) (intuofsingle_total x).
Proof.
unfold Val.intofsingle, intofsingle_total. intros.
inv MATCH; simpl in *; try constructor.
all: destruct (Float32.to_intu f) as [i|] eqn:E; simpl; [auto with va | constructor].
Qed.

Lemma intofsingle_ne_total_sound:
forall v x
(MATCH : vmatch v x),
vmatch (Val.maketotal (Val.intofsingle_ne v)) (intofsingle_ne_total x).
Proof.
unfold Val.intofsingle_ne, intofsingle_ne_total. intros.
inv MATCH; simpl in *; try constructor.
all: destruct (Float32.to_int_ne f) as [i|] eqn:E; simpl; [auto with va | constructor].
Qed.

Lemma intuofsingle_ne_total_sound:
forall v x
(MATCH : vmatch v x),
vmatch (Val.maketotal (Val.intuofsingle_ne v)) (intuofsingle_ne_total x).
Proof.
unfold Val.intofsingle, intofsingle_total. intros.
inv MATCH; simpl in *; try constructor.
all: destruct (Float32.to_intu_ne f) as [i|] eqn:E; simpl; [auto with va | constructor].
Qed.

Lemma singleofint_total_sound:
forall v x, vmatch v x ->
vmatch (Val.maketotal (Val.singleofint v)) (singleofint x).
Proof.
unfold Val.singleofint, singleofint; intros.
inv H; simpl.
all: auto with va.
all: unfold ntop1, provenance.
all: try constructor.
Qed.

Lemma singleofintu_total_sound:
forall v x, vmatch v x ->
vmatch (Val.maketotal (Val.singleofintu v)) (singleofintu x).
Proof.
unfold Val.singleofintu, singleofintu; intros.
inv H; simpl.
all: auto with va.
all: unfold ntop1, provenance.
all: try constructor.
Qed.

Lemma longoffloat_total_sound:
forall v x
(MATCH : vmatch v x),
vmatch (Val.maketotal (Val.longoffloat v)) (longoffloat_total x).
Proof.
unfold Val.longoffloat, longoffloat_total. intros.
inv MATCH; simpl in *; try constructor.
all: destruct (Float.to_long f) as [i|] eqn:E; simpl; [auto with va | constructor].
Qed.

Lemma longuoffloat_total_sound:
forall v x
(MATCH : vmatch v x),
vmatch (Val.maketotal (Val.longuoffloat v)) (longuoffloat_total x).
Proof.
unfold Val.longoffloat, longoffloat_total. intros.
inv MATCH; simpl in *; try constructor.
all: destruct (Float.to_longu f) as [i|] eqn:E; simpl; [auto with va | constructor].
Qed.

Lemma longoffloat_ne_total_sound:
forall v x
(MATCH : vmatch v x),
vmatch (Val.maketotal (Val.longoffloat_ne v)) (longoffloat_ne_total x).
Proof.
unfold Val.longoffloat_ne, longoffloat_ne_total. intros.
inv MATCH; simpl in *; try constructor.
all: destruct (Float.to_long_ne f) as [i|] eqn:E; simpl; [auto with va | constructor].
Qed.

Lemma longuoffloat_ne_total_sound:
forall v x
(MATCH : vmatch v x),
vmatch (Val.maketotal (Val.longuoffloat_ne v)) (longuoffloat_ne_total x).
Proof.
unfold Val.longoffloat_ne, longoffloat_ne_total. intros.
inv MATCH; simpl in *; try constructor.
all: destruct (Float.to_longu_ne f) as [i|] eqn:E; simpl; [auto with va | constructor].
Qed.

Lemma longofsingle_total_sound:
forall v x
(MATCH : vmatch v x),
vmatch (Val.maketotal (Val.longofsingle v)) (longofsingle_total x).
Proof.
unfold Val.longofsingle, longofsingle_total. intros.
inv MATCH; simpl in *; try constructor.
all: destruct (Float32.to_long f) as [i|] eqn:E; simpl; [auto with va | constructor].
Qed.

Lemma longuofsingle_total_sound:
forall v x
(MATCH : vmatch v x),
vmatch (Val.maketotal (Val.longuofsingle v)) (longuofsingle_total x).
Proof.
unfold Val.longofsingle, longofsingle_total. intros.
inv MATCH; simpl in *; try constructor.
all: destruct (Float32.to_longu f) as [i|] eqn:E; simpl; [auto with va | constructor].
Qed.

Lemma singleoflong_total_sound:
forall v x, vmatch v x ->
vmatch (Val.maketotal (Val.singleoflong v)) (singleoflong x).
Proof.
unfold Val.singleoflong, singleoflong; intros.
inv H; simpl.
all: auto with va.
all: unfold ntop1, provenance.
all: try constructor.
Qed.

Lemma singleoflongu_total_sound:
forall v x, vmatch v x ->
vmatch (Val.maketotal (Val.singleoflongu v)) (singleoflongu x).
Proof.
unfold Val.singleoflongu, singleoflongu; intros.
inv H; simpl.
all: auto with va.
all: unfold ntop1, provenance.
all: try constructor.
Qed.

Lemma floatoflong_total_sound:
forall v x, vmatch v x ->
vmatch (Val.maketotal (Val.floatoflong v)) (floatoflong x).
Proof.
unfold Val.floatoflong, floatoflong; intros.
inv H; simpl.
all: auto with va.
all: unfold ntop1, provenance.
all: try constructor.
Qed.

Lemma floatoflongu_total_sound:
forall v x, vmatch v x ->
vmatch (Val.maketotal (Val.floatoflongu v)) (floatoflongu x).
Proof.
unfold Val.floatoflongu, floatoflongu; intros.
inv H; simpl.
all: auto with va.
all: unfold ntop1, provenance.
all: try constructor.
Qed.

Lemma floatofint_total_sound:
forall v x, vmatch v x ->
vmatch (Val.maketotal (Val.floatofint v)) (floatofint x).
Proof.
unfold Val.floatofint, floatofint; intros.
inv H; simpl.
all: auto with va.
all: unfold ntop1, provenance.
all: try constructor.
Qed.

Lemma floatofintu_total_sound:
forall v x, vmatch v x ->
vmatch (Val.maketotal (Val.floatofintu v)) (floatofintu x).
Proof.
unfold Val.floatofintu, floatofintu; intros.
inv H; simpl.
all: auto with va.
all: unfold ntop1, provenance.
all: try constructor.
Qed.

Definition divs_total (v w: aval) :=
match w, v with
| I i2, I i1 =>
if Int.eq i2 Int.zero
|| Int.eq i1 (Int.repr Int.min_signed) && Int.eq i2 Int.mone
then ntop
else I (Int.divs i1 i2)
| _, _ => ntop2 v w
end.

Lemma divs_total_sound:
forall v w x y, vmatch v x -> vmatch w y -> vmatch (Val.maketotal (Val.divs v w)) (divs_total x y).
Proof.
intros until y.
intros HX HY.
inv HX; inv HY; cbn in *.
{ destruct (_ || _) eqn:E; cbn; unfold ntop; auto with va.
}
all: unfold ntop2; auto with va.
all: destruct (_ || _) eqn:E; unfold ntop2; cbn; auto with va.
Qed.

Definition divu_total (v w: aval) :=
match w, v with
| I i2, I i1 =>
if Int.eq i2 Int.zero
then ntop
else I (Int.divu i1 i2)
| _, _ => ntop2 v w
end.

Lemma divu_total_sound:
forall v w x y, vmatch v x -> vmatch w y -> vmatch (Val.maketotal (Val.divu v w)) (divu_total x y).
Proof.
intros until y.
intros HX HY.
inv HX; inv HY; cbn in *.
{ destruct Int.eq eqn:E; cbn; unfold ntop; auto with va.
}
all: unfold ntop2; auto with va.
all: destruct Int.eq eqn:E; unfold ntop2; cbn; auto with va.
Qed.

Definition mods_total (v w: aval) :=
match w, v with
| I i2, I i1 =>
if Int.eq i2 Int.zero
|| Int.eq i1 (Int.repr Int.min_signed) && Int.eq i2 Int.mone
then ntop
else I (Int.mods i1 i2)
| _, _ => ntop2 v w
end.

Lemma mods_total_sound:
forall v w x y, vmatch v x -> vmatch w y -> vmatch (Val.maketotal (Val.mods v w)) (mods_total x y).
Proof.
intros until y.
intros HX HY.
inv HX; inv HY; cbn in *.
{ destruct (_ || _) eqn:E; cbn; unfold ntop; auto with va.
}
all: unfold ntop2; auto with va.
all: destruct (_ || _) eqn:E; unfold ntop2; cbn; auto with va.
Qed.

Definition modu_total (v w: aval) :=
match w, v with
| I i2, I i1 =>
if Int.eq i2 Int.zero
then ntop
else I (Int.modu i1 i2)
| I i2, _ => uns (provenance v) (usize i2)
| _, _ => ntop2 v w
end.

Lemma modu_total_sound:
forall v w x y, vmatch v x -> vmatch w y -> vmatch (Val.maketotal (Val.modu v w)) (modu_total x y).
Proof.
assert (UNS: forall i j, j <> Int.zero -> is_uns (usize j) (Int.modu i j)).
{
intros. apply is_uns_mon with (usize (Int.modu i j)).
{ apply is_uns_usize.
}
unfold usize, Int.size.
apply Zsize_monotone.
generalize (Int.unsigned_range_2 j); intros RANGE.
assert (Int.unsigned j <> 0).
{ red; intros; elim H. rewrite <- (Int.repr_unsigned j). rewrite H0. auto. }
exploit (Z_mod_lt (Int.unsigned i) (Int.unsigned j)). lia. intros MOD.
unfold Int.modu. rewrite Int.unsigned_repr. lia. lia.
}
intros until y.
intros HX HY.
inv HX; inv HY; cbn in *.
{ destruct Int.eq eqn:E; unfold ntop; cbn; auto with va.
}
all: try discriminate.
all: unfold ntop2; auto with va.
all: try (destruct Int.eq eqn:E; cbn; unfold ntop2; auto with va; fail).
all: try apply vmatch_uns_undef.

all:
generalize (Int.eq_spec i0 Int.zero);
destruct (Int.eq i0 Int.zero);
cbn;
intro.
all: try apply vmatch_uns_undef.
all: apply vmatch_uns; auto.
Qed.

Lemma shrx_total_sound:
forall v w x y, vmatch v x -> vmatch w y -> vmatch (Val.maketotal (Val.shrx v w)) (shrx x y).
Proof.
intros until y. intros HX HY.
inv HX; inv HY; cbn.
all: unfold ntop1; auto with va.
all: destruct Int.ltu eqn:LTU; cbn; unfold ntop; auto with va.
Qed.

Definition divls_total (v w: aval) :=
match w, v with
| L i2, L i1 =>
if Int64.eq i2 Int64.zero
|| Int64.eq i1 (Int64.repr Int64.min_signed) && Int64.eq i2 Int64.mone
then ntop
else L (Int64.divs i1 i2)
| _, _ => ntop2 v w
end.

Lemma divls_total_sound:
forall v w x y, vmatch v x -> vmatch w y -> vmatch (Val.maketotal (Val.divls v w)) (divls_total x y).
Proof.
intros until y.
intros HX HY.
inv HX; inv HY; cbn in *.
all: unfold ntop2; auto with va.
all: destruct (_ || _) eqn:E; unfold ntop2, ntop; cbn; auto with va.
Qed.

Definition divlu_total (v w: aval) :=
match w, v with
| L i2, L i1 =>
if Int64.eq i2 Int64.zero
then ntop
else L (Int64.divu i1 i2)
| _, _ => ntop2 v w
end.

Lemma divlu_total_sound:
forall v w x y, vmatch v x -> vmatch w y -> vmatch (Val.maketotal (Val.divlu v w)) (divlu_total x y).
Proof.
intros until y.
intros HX HY.
inv HX; inv HY; cbn in *.
all: unfold ntop2; auto with va.
all: destruct Int64.eq eqn:E; unfold ntop2, ntop; cbn; auto with va.
Qed.

Definition modls_total (v w: aval) :=
match w, v with
| L i2, L i1 =>
if Int64.eq i2 Int64.zero
|| Int64.eq i1 (Int64.repr Int64.min_signed) && Int64.eq i2 Int64.mone
then ntop
else L (Int64.mods i1 i2)
| _, _ => ntop2 v w
end.

Lemma modls_total_sound:
forall v w x y, vmatch v x -> vmatch w y -> vmatch (Val.maketotal (Val.modls v w)) (modls_total x y).
Proof.
intros until y.
intros HX HY.
inv HX; inv HY; cbn in *.
all: unfold ntop2; auto with va.
all: destruct (_ || _) eqn:E; unfold ntop2, ntop; cbn; auto with va.
Qed.

Definition modlu_total (v w: aval) :=
match w, v with
| L i2, L i1 =>
if Int64.eq i2 Int64.zero
then ntop
else L (Int64.modu i1 i2)
| _, _ => ntop2 v w
end.

Lemma modlu_total_sound:
forall v w x y, vmatch v x -> vmatch w y -> vmatch (Val.maketotal (Val.modlu v w)) (modlu_total x y).
Proof.
intros until y.
intros HX HY.
inv HX; inv HY; cbn in *.
all: unfold ntop2; auto with va.
all: destruct Int64.eq eqn:E; cbn; unfold ntop2, ntop; auto with va.
Qed.

Lemma shrxl_total_sound:
forall v w x y, vmatch v x -> vmatch w y -> vmatch (Val.maketotal (Val.shrxl v w)) (shrxl x y).
Proof.
intros until y. intros HX HY.
inv HX; inv HY; cbn.
all: unfold ntop1; auto with va.
all: destruct Int.ltu eqn:LTU; cbn; unfold ntop; auto with va.
Qed.

Comparisons and variation intervals

Definition cmp_intv (c: comparison) (i: Z * Z) (n: Z) : abool :=
let (lo, hi) := i in
match c with
| Ceq => if zlt n lo || zlt hi n then Maybe false else Btop
| Cne => Btop
| Clt => if zlt hi n then Maybe true else if zle n lo then Maybe false else Btop
| Cle => if zle hi n then Maybe true else if zlt n lo then Maybe false else Btop
| Cgt => if zlt n lo then Maybe true else if zle hi n then Maybe false else Btop
| Cge => if zle n lo then Maybe true else if zlt hi n then Maybe false else Btop
end.

Definition zcmp (c: comparison) (n1 n2: Z) : bool :=
match c with
| Ceq => zeq n1 n2
| Cne => negb (zeq n1 n2)
| Clt => zlt n1 n2
| Cle => zle n1 n2
| Cgt => zlt n2 n1
| Cge => zle n2 n1
end.

Lemma zcmp_intv_sound:
forall c i x n,
fst i <= x <= snd i ->
cmatch (Some (zcmp c x n)) (cmp_intv c i n).
Proof.
intros c [lo hi] x n; simpl; intros R.
destruct c; unfold zcmp, proj_sumbool.
- (* eq *)
destruct (zlt n lo). rewrite zeq_false by lia. constructor.
destruct (zlt hi n). rewrite zeq_false by lia. constructor.
constructor.
- (* ne *)
constructor.
- (* lt *)
destruct (zlt hi n). rewrite zlt_true by lia. constructor.
destruct (zle n lo). rewrite zlt_false by lia. constructor.
constructor.
- (* le *)
destruct (zle hi n). rewrite zle_true by lia. constructor.
destruct (zlt n lo). rewrite zle_false by lia. constructor.
constructor.
- (* gt *)
destruct (zlt n lo). rewrite zlt_true by lia. constructor.
destruct (zle hi n). rewrite zlt_false by lia. constructor.
constructor.
- (* ge *)
destruct (zle n lo). rewrite zle_true by lia. constructor.
destruct (zlt hi n). rewrite zle_false by lia. constructor.
constructor.
Qed.

Lemma cmp_intv_None:
forall c i n, cmatch None (cmp_intv c i n).
Proof.
unfold cmp_intv; intros. destruct i as [lo hi].
destruct c.
- (* eq *)
destruct (zlt n lo). constructor. destruct (zlt hi n); constructor.
- (* ne *)
constructor.
- (* lt *)
destruct (zlt hi n). constructor. destruct (zle n lo); constructor.
- (* le *)
destruct (zle hi n). constructor. destruct (zlt n lo); constructor.
- (* gt *)
destruct (zlt n lo). constructor. destruct (zle hi n); constructor.
- (* ge *)
destruct (zle n lo). constructor. destruct (zlt hi n); constructor.
Qed.

Definition uintv (v: aval) : Z * Z :=
match v with
| I n => (Int.unsigned n, Int.unsigned n)
| Uns _ n => if zlt n Int.zwordsize then (0, two_p n - 1) else (0, Int.max_unsigned)
| _ => (0, Int.max_unsigned)
end.

Lemma uintv_sound:
forall n v, vmatch (Vint n) v -> fst (uintv v) <= Int.unsigned n <= snd (uintv v).
Proof.
intros. inv H; simpl; try (apply Int.unsigned_range_2).
- lia.
- destruct (zlt n0 Int.zwordsize); simpl.
+ rewrite is_uns_zero_ext in H2. rewrite <- H2. rewrite Int.zero_ext_mod by lia.
exploit (Z_mod_lt (Int.unsigned n) (two_p n0)). apply two_p_gt_ZERO; auto. lia.
+ apply Int.unsigned_range_2.
Qed.

Lemma cmpu_intv_sound:
forall valid c n1 v1 n2,
vmatch (Vint n1) v1 ->
cmatch (Val.cmpu_bool valid c (Vint n1) (Vint n2)) (cmp_intv c (uintv v1) (Int.unsigned n2)).
Proof.
intros. simpl. replace (Int.cmpu c n1 n2) with (zcmp c (Int.unsigned n1) (Int.unsigned n2)).
apply zcmp_intv_sound; apply uintv_sound; auto.
destruct c; simpl; auto.
unfold Int.ltu. destruct (zle (Int.unsigned n1) (Int.unsigned n2)); [rewrite zlt_false|rewrite zlt_true]; auto; lia.
unfold Int.ltu. destruct (zle (Int.unsigned n2) (Int.unsigned n1)); [rewrite zlt_false|rewrite zlt_true]; auto; lia.
Qed.

Lemma cmpu_intv_sound_2:
forall valid c n1 v1 n2,
vmatch (Vint n1) v1 ->
cmatch (Val.cmpu_bool valid c (Vint n2) (Vint n1)) (cmp_intv (swap_comparison c) (uintv v1) (Int.unsigned n2)).
Proof.
intros. rewrite <- Val.swap_cmpu_bool. apply cmpu_intv_sound; auto.
Qed.

Definition sintv (v: aval) : Z * Z :=
match v with
| I n => (Int.signed n, Int.signed n)
| Uns _ n =>
if zlt n Int.zwordsize then (0, two_p n - 1) else (Int.min_signed, Int.max_signed)
| Sgn _ n =>
if zlt n Int.zwordsize
then (let x := two_p (n-1) in (-x, x-1))
else (Int.min_signed, Int.max_signed)
| _ => (Int.min_signed, Int.max_signed)
end.

Lemma sintv_sound:
forall n v, vmatch (Vint n) v -> fst (sintv v) <= Int.signed n <= snd (sintv v).
Proof.
intros. inv H; simpl; try (apply Int.signed_range).
- lia.
- destruct (zlt n0 Int.zwordsize); simpl.
+ rewrite is_uns_zero_ext in H2. rewrite <- H2.
assert (Int.unsigned (Int.zero_ext n0 n) = Int.unsigned n mod two_p n0) by (apply Int.zero_ext_mod; lia).
exploit (Z_mod_lt (Int.unsigned n) (two_p n0)). apply two_p_gt_ZERO; auto. intros.
replace (Int.signed (Int.zero_ext n0 n)) with (Int.unsigned (Int.zero_ext n0 n)).
rewrite H. lia.
unfold Int.signed. rewrite zlt_true. auto.
assert (two_p n0 <= Int.half_modulus).
{ change Int.half_modulus with (two_p (Int.zwordsize - 1)).
apply two_p_monotone. lia. }
lia.
+ apply Int.signed_range.
- destruct (zlt n0 (Int.zwordsize)); simpl.
+ rewrite is_sgn_sign_ext in H2 by auto. rewrite <- H2.
exploit (Int.sign_ext_range n0 n). lia. lia.
+ apply Int.signed_range.
Qed.

Lemma cmp_intv_sound:
forall c n1 v1 n2,
vmatch (Vint n1) v1 ->
cmatch (Val.cmp_bool c (Vint n1) (Vint n2)) (cmp_intv c (sintv v1) (Int.signed n2)).
Proof.
intros. simpl. replace (Int.cmp c n1 n2) with (zcmp c (Int.signed n1) (Int.signed n2)).
apply zcmp_intv_sound; apply sintv_sound; auto.
destruct c; simpl; rewrite ? Int.eq_signed; auto.
unfold Int.lt. destruct (zle (Int.signed n1) (Int.signed n2)); [rewrite zlt_false|rewrite zlt_true]; auto; lia.
unfold Int.lt. destruct (zle (Int.signed n2) (Int.signed n1)); [rewrite zlt_false|rewrite zlt_true]; auto; lia.
Qed.

Lemma cmp_intv_sound_2:
forall c n1 v1 n2,
vmatch (Vint n1) v1 ->
cmatch (Val.cmp_bool c (Vint n2) (Vint n1)) (cmp_intv (swap_comparison c) (sintv v1) (Int.signed n2)).
Proof.
intros. rewrite <- Val.swap_cmp_bool. apply cmp_intv_sound; auto.
Qed.

Comparisons

Definition cmpu_bool (c: comparison) (v w: aval) : abool :=
match v, w with
| I i1, I i2 => Just (Int.cmpu c i1 i2)
| Ptr _, I i => if Int.eq i Int.zero then cmp_different_blocks c else Btop
| I i, Ptr _ => if Int.eq i Int.zero then cmp_different_blocks c else Btop
| Ptr p1, Ptr p2 => pcmp c p1 p2
| _, I i => club (cmp_intv c (uintv v) (Int.unsigned i)) (cmp_different_blocks c)
| I i, _ => club (cmp_intv (swap_comparison c) (uintv w) (Int.unsigned i)) (cmp_different_blocks c)
| _, _ => Btop
end.

Lemma cmpu_bool_sound:
forall valid c v w x y, vmatch v x -> vmatch w y -> cmatch (Val.cmpu_bool valid c v w) (cmpu_bool c x y).
Proof.
intros.
assert (IP: forall i b ofs,
cmatch (Val.cmpu_bool valid c (Vint i) (Vptr b ofs)) (cmp_different_blocks c)).
{
intros. simpl. destruct Archi.ptr64.
apply cmp_different_blocks_none.
destruct (Int.eq i Int.zero && (valid b (Ptrofs.unsigned ofs) || valid b (Ptrofs.unsigned ofs - 1))).
apply cmp_different_blocks_sound. apply cmp_different_blocks_none.
}
assert (PI: forall i b ofs,
cmatch (Val.cmpu_bool valid c (Vptr b ofs) (Vint i)) (cmp_different_blocks c)).
{
intros. simpl. destruct Archi.ptr64.
apply cmp_different_blocks_none.
destruct (Int.eq i Int.zero && (valid b (Ptrofs.unsigned ofs) || valid b (Ptrofs.unsigned ofs - 1))).
apply cmp_different_blocks_sound. apply cmp_different_blocks_none.
}
unfold cmpu_bool; inversion H; subst; inversion H0; subst;
auto using cmatch_top, cmp_different_blocks_none, pcmp_none,
cmatch_lub_l, cmatch_lub_r, pcmp_sound,
cmpu_intv_sound, cmpu_intv_sound_2, cmp_intv_None.
- constructor.
- destruct (Int.eq i Int.zero); auto using cmatch_top.
- simpl; destruct (Int.eq i Int.zero); auto using cmatch_top, cmp_different_blocks_none.
- destruct (Int.eq i Int.zero); auto using cmatch_top.
- simpl; destruct (Int.eq i Int.zero); auto using cmatch_top, cmp_different_blocks_none.
Qed.

Definition cmp_bool (c: comparison) (v w: aval) : abool :=
match v, w with
| I i1, I i2 => Just (Int.cmp c i1 i2)
| _, I i => cmp_intv c (sintv v) (Int.signed i)
| I i, _ => cmp_intv (swap_comparison c) (sintv w) (Int.signed i)
| _, _ => Btop
end.

Lemma cmp_bool_sound:
forall c v w x y, vmatch v x -> vmatch w y -> cmatch (Val.cmp_bool c v w) (cmp_bool c x y).
Proof.
intros.
unfold cmp_bool; inversion H; subst; inversion H0; subst;
auto using cmatch_top, cmp_intv_sound, cmp_intv_sound_2, cmp_intv_None.
- constructor.
Qed.

Definition cmplu_bool (c: comparison) (v w: aval) : abool :=
match v, w with
| L i1, L i2 => Just (Int64.cmpu c i1 i2)
| Ptr _, L i => if Int64.eq i Int64.zero then cmp_different_blocks c else Btop
| L i, Ptr _ => if Int64.eq i Int64.zero then cmp_different_blocks c else Btop
| Ptr p1, Ptr p2 => pcmp c p1 p2
| _, _ => Btop
end.

Lemma cmplu_bool_sound:
forall valid c v w x y, vmatch v x -> vmatch w y -> cmatch (Val.cmplu_bool valid c v w) (cmplu_bool c x y).
Proof.
intros.
assert (IP: forall i b ofs,
cmatch (Val.cmplu_bool valid c (Vlong i) (Vptr b ofs)) (cmp_different_blocks c)).
{
intros. simpl. destruct Archi.ptr64; simpl.
destruct (Int64.eq i Int64.zero && (valid b (Ptrofs.unsigned ofs) || valid b (Ptrofs.unsigned ofs - 1))).
apply cmp_different_blocks_sound. apply cmp_different_blocks_none.
apply cmp_different_blocks_none.
}
assert (PI: forall i b ofs,
cmatch (Val.cmplu_bool valid c (Vptr b ofs) (Vlong i)) (cmp_different_blocks c)).
{
intros. simpl. destruct Archi.ptr64; simpl.
destruct (Int64.eq i Int64.zero && (valid b (Ptrofs.unsigned ofs) || valid b (Ptrofs.unsigned ofs - 1))).
apply cmp_different_blocks_sound. apply cmp_different_blocks_none.
apply cmp_different_blocks_none.
}
unfold cmplu_bool; inversion H; subst; inversion H0; subst;
auto using cmatch_top, cmp_different_blocks_none, pcmp_none,
cmatch_lub_l, cmatch_lub_r, pcmp_sound_64.
- constructor.
- destruct (Int64.eq i Int64.zero); auto using cmatch_top.
- simpl; destruct (Int64.eq i Int64.zero); auto using cmatch_top, cmp_different_blocks_none.
- destruct (Int64.eq i Int64.zero); auto using cmatch_top.
- simpl; destruct (Int64.eq i Int64.zero); auto using cmatch_top, cmp_different_blocks_none.
Qed.

Definition cmpl_bool (c: comparison) (v w: aval) : abool :=
match v, w with
| L i1, L i2 => Just (Int64.cmp c i1 i2)
| _, _ => Btop
end.

Lemma cmpl_bool_sound:
forall c v w x y, vmatch v x -> vmatch w y -> cmatch (Val.cmpl_bool c v w) (cmpl_bool c x y).
Proof.
intros.
unfold cmpl_bool; inversion H; subst; inversion H0; subst;
auto using cmatch_top.
- constructor.
Qed.

Definition cmpf_bool (c: comparison) (v w: aval) : abool :=
match v, w with
| F f1, F f2 => Just (Float.cmp c f1 f2)
| _, _ => Btop
end.

Lemma cmpf_bool_sound:
forall c v w x y, vmatch v x -> vmatch w y -> cmatch (Val.cmpf_bool c v w) (cmpf_bool c x y).
Proof.
intros. inv H; try constructor; inv H0; constructor.
Qed.

Definition cmpfs_bool (c: comparison) (v w: aval) : abool :=
match v, w with
| FS f1, FS f2 => Just (Float32.cmp c f1 f2)
| _, _ => Btop
end.

Lemma cmpfs_bool_sound:
forall c v w x y, vmatch v x -> vmatch w y -> cmatch (Val.cmpfs_bool c v w) (cmpfs_bool c x y).
Proof.
intros. inv H; try constructor; inv H0; constructor.
Qed.

match x with
| I i => Just (Int.eq (Int.and i mask) Int.zero)
| Uns p n => if Int.eq (Int.zero_ext n mask) Int.zero then Maybe true else Btop
| _ => Btop
end.

vmatch v x ->
Proof.
intros. inv H; simpl; auto with va.
predSpec Int.eq Int.eq_spec (Int.zero_ext n mask) Int.zero; auto with va.
replace (Int.and i mask) with Int.zero.
rewrite Int.eq_true. constructor.
rewrite is_uns_zero_ext in H1. rewrite Int.zero_ext_and in * by auto.
rewrite <- H1. rewrite Int.and_assoc. rewrite Int.and_commut in H. rewrite H.
rewrite Int.and_zero; auto.
destruct (Int.eq (Int.zero_ext n mask) Int.zero); constructor.
Qed.

Definition of_optbool (ab: abool) : aval :=
match ab with
| Just b => I (if b then Int.one else Int.zero)
| _ => Uns Pbot 1
end.

Lemma of_optbool_sound:
forall ob ab, cmatch ob ab -> vmatch (Val.of_optbool ob) (of_optbool ab).
Proof.
intros.
assert (DEFAULT: vmatch (Val.of_optbool ob) (Uns Pbot 1)).
{
destruct ob; simpl; auto with va.
destruct b; constructor; try lia.
change 1 with (usize Int.one). apply is_uns_usize.
red; intros. apply Int.bits_zero.
}
inv H; auto. simpl. destruct b; constructor.
Qed.

Definition resolve_branch (ab: abool) : option bool :=
match ab with
| Just b => Some b
| Maybe b => Some b
| _ => None
end.

Lemma resolve_branch_sound:
forall b ab b',
cmatch (Some b) ab -> resolve_branch ab = Some b' -> b' = b.
Proof.
intros. inv H; simpl in H0; congruence.
Qed.

Select either returns one of its arguments, or Vundef.

match x with
| Vbot => ntop
| I i =>
if Int.lt i Int.zero
then sgn Pbot (ssize i)
else uns Pbot (usize i)
| L _ | F _ | FS _ => ntop
| _ => x
end.

forall v x, vmatch v x -> vmatch v (add_undef x).
Proof.
destruct 1; simpl; auto with va.
destruct (Int.lt i Int.zero).
apply vmatch_sgn; apply is_sgn_ssize.
apply vmatch_uns; apply is_uns_usize.
Qed.

forall x, vmatch Vundef (add_undef x).
Proof.
destruct x; simpl; auto with va.
destruct (Int.lt n Int.zero); auto with va.
Qed.

forall v x ty, vmatch v x -> vmatch (Val.normalize v ty) (add_undef x).
Proof.
intros. destruct (Val.lessdef_normalize v ty);
Qed.

Definition select (ab: abool) (x y: aval) :=
match ab with
| Bnone => ntop
| Just b | Maybe b => add_undef (if b then x else y)
| Btop => add_undef (vlub x y)
end.

Lemma select_sound:
forall ob v w ab x y ty,
cmatch ob ab -> vmatch v x -> vmatch w y ->
vmatch (Val.select ob v w ty) (select ab x y).
Proof.
unfold Val.select, select; intros. inv H.
- auto with va.
- apply add_undef_normalize; destruct b; auto.
- apply add_undef_normalize; destruct b; auto.
- destruct ob as [b|].
+ apply add_undef_normalize. destruct b; [apply vmatch_lub_l|apply vmatch_lub_r]; auto.
Qed.

Copy
Definition copy (ty : typ) (av : aval) := Vtop.

Lemma copy_sound :
forall ty v av (MATCH : vmatch v av),
(vmatch v (copy ty av)).
Proof.
intros.
inv MATCH; unfold copy; cbn; try constructor.
all: inv H; constructor; congruence.
Qed.

Lemma normalize_copy_sound :
forall ty v av (MATCH : vmatch v av),
(vmatch (Val.normalize v ty) (copy ty av)).
Proof.
intros.
inv MATCH; unfold copy; destruct ty; cbn; try constructor.
all: inv H; try destruct Archi.ptr64;
repeat constructor; congruence.
Qed.

Bitwise conversion between floating-point values and integers

Definition bits_of_single (v : aval) : aval :=
match v with
| FS f => I (Float32.to_bits f)
| _ => ntop1 v
end.

Definition bits_of_float (v : aval) : aval :=
match v with
| F f => L (Float.to_bits f)
| _ => ntop1 v
end.

Definition single_of_bits (v : aval) : aval :=
match v with
| I f => FS (Float32.of_bits f)
| _ => ntop1 v
end.

Definition float_of_bits (v : aval) : aval :=
match v with
| L f => F (Float.of_bits f)
| _ => ntop1 v
end.

Lemma bits_of_single_sound:
forall v x, vmatch v x -> vmatch (Val.bits_of_single v) (bits_of_single x).
Proof.
unfold Val.bits_of_single; intros. inv H; cbn; constructor.
Qed.

Lemma bits_of_float_sound:
forall v x, vmatch v x -> vmatch (Val.bits_of_float v) (bits_of_float x).
Proof.
unfold Val.bits_of_float; intros. inv H; cbn; constructor.
Qed.

Lemma single_of_bits_sound:
forall v x, vmatch v x -> vmatch (Val.single_of_bits v) (single_of_bits x).
Proof.
unfold Val.bits_of_single; intros. inv H; cbn; constructor.
Qed.

Lemma float_of_bits_sound:
forall v x, vmatch v x -> vmatch (Val.float_of_bits v) (float_of_bits x).
Proof.
unfold Val.bits_of_float; intros. inv H; cbn; constructor.
Qed.

Canary
Definition canary_aval := Num Pbot.

Lemma canary_aval_sound : vmatch (canary_val tt) canary_aval.
Proof.
unfold canary_val, canary_aval.
destruct Archi.canary64; constructor.
Qed.

Definition vnormalize (chunk: memory_chunk) (v: aval) :=
match chunk, v with
| _, Vbot => Vbot
| Mint8signed, I i => I (Int.sign_ext 8 i)
| Mint8signed, Uns p n => if zlt n 8 then Uns (provenance v) n else Sgn (provenance v) 8
| Mint8signed, Sgn p n => Sgn (provenance v) (Z.min n 8)
| Mint8signed, _ => Sgn (provenance v) 8
| Mint8unsigned, I i => I (Int.zero_ext 8 i)
| Mint8unsigned, Uns p n => Uns (provenance v) (Z.min n 8)
| Mint8unsigned, _ => Uns (provenance v) 8
| Mint16signed, I i => I (Int.sign_ext 16 i)
| Mint16signed, Uns p n => if zlt n 16 then Uns (provenance v) n else Sgn (provenance v) 16
| Mint16signed, Sgn p n => Sgn (provenance v) (Z.min n 16)
| Mint16signed, _ => Sgn (provenance v) 16
| Mint16unsigned, I i => I (Int.zero_ext 16 i)
| Mint16unsigned, Uns p n => Uns (provenance v) (Z.min n 16)
| Mint16unsigned, _ => Uns (provenance v) 16
| Mint32, (I _ | Uns _ _ | Sgn _ _ | Num _) => v
| Mint32, (Ptr p | Ifptr p) => if Archi.ptr64 then Num (provenance v) else v
| Mint32, _ => Num (provenance v)
| Mint64, L _ => v
| Mint64, (Ptr p | Ifptr p) => if Archi.ptr64 then v else Num (provenance v)
| Mint64, _ => Num (provenance v)
| Mfloat32, FS f => v
| Mfloat32, _ => Num (provenance v)
| Mfloat64, F f => v
| Mfloat64, _ => Num (provenance v)
| Many32, (I _ | Uns _ _ | Sgn _ _ | FS _) => v
| Many32, (Ptr p | Ifptr p) => if Archi.ptr64 then Num (provenance v) else v
| Many32, _ => Num (provenance v)
| Many64, _ => v
end.

Lemma vnormalize_sound:
forall chunk v x, vmatch v x -> vmatch (Val.load_result chunk v) (vnormalize chunk x).
Proof.
unfold Val.load_result, vnormalize; generalize Archi.ptr64; intros ptr64;
induction 1; destruct chunk; eauto using is_zero_ext_uns, is_sign_ext_sgn with va;
try (destruct ptr64; auto with va; fail).
- destruct (zlt n 8); constructor; auto with va.
apply is_sign_ext_uns; auto.
apply is_sign_ext_sgn; auto with va.
- constructor. lia. apply is_zero_ext_uns. apply Z.min_case; auto with va.
- destruct (zlt n 16); constructor; auto with va.
apply is_sign_ext_uns; auto.
apply is_sign_ext_sgn; auto with va.
- constructor. extlia. apply is_zero_ext_uns. apply Z.min_case; auto with va.
- destruct (zlt n 8); auto with va.
- destruct (zlt n 16); auto with va.
- constructor. lia. apply is_sign_ext_sgn; auto with va. apply Z.min_case; auto with va.
- constructor. lia. apply is_sign_ext_sgn; auto with va. apply Z.min_case; auto with va.
Qed.

Lemma vnormalize_cast:
forall chunk m b ofs v p,
Mem.load chunk m b ofs = Some v ->
vmatch v (Ifptr p) ->
vmatch v (vnormalize chunk (Ifptr p)).
Proof.
destruct chunk; simpl; intros.
- (* int8signed *)
rewrite H2. destruct v; simpl; constructor. lia. apply is_sign_ext_sgn; auto with va.
- (* int8unsigned *)
rewrite H2. destruct v; simpl; constructor. lia. apply is_zero_ext_uns; auto with va.
- (* int16signed *)
rewrite H2. destruct v; simpl; constructor. lia. apply is_sign_ext_sgn; auto with va.
- (* int16unsigned *)
rewrite H2. destruct v; simpl; constructor. lia. apply is_zero_ext_uns; auto with va.
- (* int32 *)
red in H1. destruct Archi.ptr64; auto. destruct v; constructor || discriminate.
- (* int64 *)
red in H1. destruct Archi.ptr64; auto. destruct v; constructor || discriminate.
- (* float32 *)
- (* float64 *)
- (* any32 *)
red in H1. destruct Archi.ptr64; auto. destruct v; constructor || discriminate.
- (* any64 *)
auto.
Qed.

Remark poffset_ge: forall p, pge (poffset p) p.
Proof.
destruct p; constructor.
Qed.

Remark poffset_monotone:
forall p q, pge p q -> pge (poffset p) (poffset q).
Proof.
destruct 1; simpl; auto with va.
Qed.

Remark provenance_monotone:
forall x y, vge x y -> pge (provenance x) (provenance y).
Proof.
induction 1; simpl; eauto using poffset_ge, poffset_monotone, pge_trans with va.
Qed.

Remark provenance_ifptr_ge:
forall p q, pge p q -> pge (provenance (Ifptr p)) q.
Proof.
intros. simpl. apply pge_trans with p; auto. apply poffset_ge.
Qed.

Lemma vnormalize_monotone:
forall chunk x y,
vge x y -> vge (vnormalize chunk x) (vnormalize chunk y).
Proof with
(auto using provenance_monotone, provenance_ifptr_ge with va).
Local Opaque provenance.
induction 1;
unfold vnormalize; generalize Archi.ptr64; intro ptr64; subst;
destruct chunk eqn:C; simpl;
repeat match goal with |- vge (if ?x then _ else _) _ => destruct x end...
- constructor... apply is_sign_ext_uns...
- constructor... apply is_sign_ext_sgn...
- constructor... apply is_zero_ext_uns... apply Z.min_case...
- constructor... apply is_sign_ext_uns...
- constructor... apply is_sign_ext_sgn...
- constructor... apply is_zero_ext_uns... apply Z.min_case...
- rewrite zlt_true by lia...
- destruct (zlt n2 8)...
- rewrite zlt_true by lia...
- destruct (zlt n2 16)...
- constructor... apply is_sign_ext_sgn... apply Z.min_case...
- constructor... apply is_zero_ext_uns...
- constructor... apply is_sign_ext_sgn... apply Z.min_case...
- constructor... apply is_zero_ext_uns...
- destruct (zlt n2 8); constructor...
- destruct (zlt n2 16); constructor...
- constructor... apply is_sign_ext_sgn...
- constructor... apply is_zero_ext_uns...
- constructor... apply is_sign_ext_sgn...
- constructor... apply is_zero_ext_uns...
- destruct (zlt n 8); constructor...
- destruct (zlt n 16); constructor...
- constructor... apply is_sign_ext_sgn...
- constructor... apply is_zero_ext_uns...
- constructor... apply is_sign_ext_sgn...
- constructor... apply is_zero_ext_uns...
- destruct (zlt n 8); constructor...
- destruct (zlt n 16); constructor...
Qed.

Remark vlub_bot_l: forall a, vlub Vbot a = a.
Proof.
reflexivity.
Qed.

Remark vlub_bot_r: forall a, vlub a Vbot = a.
Proof.
intros. rewrite vlub_comm. apply vlub_bot_l.
Qed.

Remark plub_idem: forall p, plub p p = p.
Proof.
destruct p; cbn; try reflexivity.
all: try destruct Ptrofs.eq_dec.
all: try destruct ident_eq.
all: reflexivity.
Qed.

Remark vlub_idem: forall a, vlub a a = a.
Proof.
destruct a; cbn; try reflexivity.
all: try rewrite Int.eq_true.
all: try rewrite Int64.eq_true.
all: try rewrite plub_idem.
all: try rewrite Z.max_id.
all: try reflexivity.
Abort.

Remark plub_monotone_l: forall p1 p2 q (GE : pge p1 p2),
pge (plub p1 q) (plub p2 q).
Proof.
intros. apply plub_least.
- apply pge_trans with (q := p1).
+ apply pge_lub_l.
+ assumption.
- apply pge_lub_r.
Qed.

Hint Resolve plub_monotone_l : va.

Analysis of known builtin functions. All we have is a dynamic semantics as a function list val -> option val, but we can still perform some constant propagation.

Definition val_of_aval (a: aval) : val :=
match a with
| I n => Vint n
| L n => Vlong n
| F f => Vfloat f
| FS f => Vsingle f
| _ => Vundef
end.

Definition aval_of_val (v: val) : option aval :=
match v with
| Vint n => Some (I n)
| Vlong n => Some (L n)
| Vfloat f => Some (F f)
| Vsingle f => Some (FS f)
| _ => None
end.

Lemma val_of_aval_sound:
forall v a, vmatch v a -> Val.lessdef (val_of_aval a) v.
Proof.
destruct 1; simpl; auto.
Qed.

Corollary list_val_of_aval_sound:
forall vl al, list_forall2 vmatch vl al -> Val.lessdef_list (map val_of_aval al) vl.
Proof.
induction 1; simpl; constructor; auto using val_of_aval_sound.
Qed.

Lemma aval_of_val_sound:
forall v a, aval_of_val v = Some a -> vmatch v a.
Proof.
intros v a E; destruct v; simpl in E; inv E; constructor.
Qed.

Lemma Uns_PBot_1_is_01:
forall v (MATCH : vmatch v (Uns Pbot 1%Z)),
v = Vint Int.zero \/ v = Vint Int.one \/ v = Vundef.
Proof.
intros.
inv MATCH.
2: tauto.
destruct (is_uns_1 i); intuition congruence.
Qed.

# Abstracting memory blocks

Inductive acontent : Type :=
| ACval (chunk: memory_chunk) (av: aval).

Definition eq_acontent : forall (c1 c2: acontent), {c1=c2} + {c1<>c2}.
Proof.
intros. generalize chunk_eq eq_aval. decide equality.
Defined.

Record ablock : Type := ABlock {
ab_contents: ZTree.t acontent;
ab_summary: aptr
}.

Local Notation "a ## b" := (ZTree.get b a) (at level 1).

Definition ablock_init (p: aptr) : ablock :=
{| ab_contents := ZTree.empty _; ab_summary := p |}.

Definition chunk_compat (chunk chunk': memory_chunk) : bool :=
match chunk, chunk' with
| (Mint8signed | Mint8unsigned), (Mint8signed | Mint8unsigned) => true
| (Mint16signed | Mint16unsigned), (Mint16signed | Mint16unsigned) => true
| Mint32, Mint32 => true
| Mfloat32, Mfloat32 => true
| Mint64, Mint64 => true
| Mfloat64, Mfloat64 => true
| Many32, Many32 => true
| Many64, Many64 => true
| _, _ => false
end.

Definition ablock_load (chunk: memory_chunk) (ab: ablock) (i: Z) : aval :=
match ab.(ab_contents)##i with
| None => vnormalize chunk (Ifptr ab.(ab_summary))
| Some (ACval chunk' av) =>
if chunk_compat chunk chunk'
then vnormalize chunk av
else vnormalize chunk (Ifptr ab.(ab_summary))
end.

Definition ablock_load_anywhere (chunk: memory_chunk) (ab: ablock) : aval :=
vnormalize chunk (Ifptr ab.(ab_summary)).

Function inval_after (lo: Z) (hi: Z) (c: ZTree.t acontent) { wf (Zwf lo) hi } : ZTree.t acontent :=
if zle lo hi
then inval_after lo (hi - 1) (ZTree.remove hi c)
else c.
Proof.
intros; red; lia.
apply Zwf_well_founded.
Qed.

Definition inval_if (hi: Z) (lo: Z) (c: ZTree.t acontent) :=
match c##lo with
| None => c
| Some (ACval chunk av) => if zle (lo + size_chunk chunk) hi then c else ZTree.remove lo c
end.

Function inval_before (hi: Z) (lo: Z) (c: ZTree.t acontent) { wf (Zwf_up hi) lo } : ZTree.t acontent :=
if zlt lo hi
then inval_before hi (lo + 1) (inval_if hi lo c)
else c.
Proof.
intros; red; lia.
apply Zwf_up_well_founded.
Qed.

Definition ablock_store (chunk: memory_chunk) (ab: ablock) (i: Z) (av: aval) : ablock :=
{| ab_contents :=
ZTree.set i (ACval chunk av)
(inval_before i (i - 7)
(inval_after (i + 1) (i + size_chunk chunk - 1) ab.(ab_contents)));
ab_summary :=
vplub av ab.(ab_summary) |}.

Definition ablock_store_anywhere (chunk: memory_chunk) (ab: ablock) (av: aval) : ablock :=
ablock_init (vplub av ab.(ab_summary)).

Definition ablock_loadbytes (ab: ablock) : aptr := ab.(ab_summary).

Definition ablock_storebytes (ab: ablock) (p: aptr) (ofs: Z) (sz: Z) :=
{| ab_contents :=
inval_before ofs (ofs - 7)
(inval_after ofs (ofs + sz - 1) ab.(ab_contents));
ab_summary :=
plub p ab.(ab_summary) |}.

Definition ablock_storebytes_anywhere (ab: ablock) (p: aptr) :=
ablock_init (plub p ab.(ab_summary)).

Definition smatch (m: mem) (b: block) (p: aptr) : Prop :=
(forall chunk ofs v, Mem.load chunk m b ofs = Some v -> vmatch v (Ifptr p))
/\(forall ofs b' ofs' q i, Mem.loadbytes m b ofs 1 = Some (Fragment (Vptr b' ofs') q i :: nil) -> pmatch b' ofs' p).

forall b m m',
(forall ofs n bytes, Mem.loadbytes m' b ofs n = Some bytes -> n >= 0 -> Mem.loadbytes m b ofs n = Some bytes) ->
forall chunk ofs v, Mem.load chunk m' b ofs = Some v -> Mem.load chunk m b ofs = Some v.
Proof.
exploit Mem.load_valid_access; eauto. intros [C D].
subst v. apply Mem.loadbytes_load; auto. apply H; auto. generalize (size_chunk_pos chunk); lia.
Qed.

Lemma smatch_ext:
forall m b p m',
smatch m b p ->
(forall ofs n bytes, Mem.loadbytes m' b ofs n = Some bytes -> n >= 0 -> Mem.loadbytes m b ofs n = Some bytes) ->
smatch m' b p.
Proof.
intros. destruct H. split; intros.
eapply H1; eauto. apply H0; eauto. lia.
Qed.

Lemma smatch_inv:
forall m b p m',
smatch m b p ->
(forall ofs n, n >= 0 -> Mem.loadbytes m' b ofs n = Mem.loadbytes m b ofs n) ->
smatch m' b p.
Proof.
intros. eapply smatch_ext; eauto.
intros. rewrite <- H0; eauto.
Qed.

Lemma smatch_ge:
forall m b p q, smatch m b p -> pge q p -> smatch m b q.
Proof.
intros. destruct H as [A B]. split; intros.
apply vmatch_ge with (Ifptr p); eauto with va.
apply pmatch_ge with p; eauto with va.
Qed.

forall m b byte n ofs bytes,
Mem.loadbytes m b ofs n = Some bytes ->
In byte bytes ->
exists ofs', ofs <= ofs' < ofs + n /\ Mem.loadbytes m b ofs' 1 = Some(byte :: nil).
Proof.
intros until n. pattern n.
apply well_founded_ind with (R := Zwf 0).
- apply Zwf_well_founded.
- intros sz REC ofs bytes LOAD IN.
destruct (zle sz 0).
+ exploit (Mem.loadbytes_split m b ofs 1 (sz - 1) bytes).
replace (1 + (sz - 1)) with sz by lia. auto.
lia.
lia.
subst bytes.
rewrite in_app_iff in IN. destruct IN.
* destruct bytes1; try discriminate. destruct bytes1; try discriminate.
simpl in H. destruct H; try contradiction. subst m0.
exists ofs; split. lia. auto.
* exploit (REC (sz - 1)). red; lia. eexact LOAD2. auto.
intros (ofs' & A & B).
exists ofs'; split. lia. auto.
Qed.

forall m b p b' ofs' q i n ofs bytes,
Mem.loadbytes m b ofs n = Some bytes ->
smatch m b p ->
In (Fragment (Vptr b' ofs') q i) bytes ->
pmatch b' ofs' p.
Proof.
intros. exploit In_loadbytes; eauto. intros (ofs1 & A & B).
eapply H0; eauto.
Qed.

forall m b ofs' byte n ofs bytes,
Mem.loadbytes m b ofs n = Some bytes ->
Mem.loadbytes m b ofs' 1 = Some (byte :: nil) ->
ofs <= ofs' < ofs + n ->
In byte bytes.
Proof.
intros until n. pattern n.
apply well_founded_ind with (R := Zwf 0).
- apply Zwf_well_founded.
exploit (Mem.loadbytes_split m b ofs 1 (sz - 1) bytes).
replace (1 + (sz - 1)) with sz by lia. auto.
lia.
lia.
intros (bytes1 & bytes2 & LOAD3 & LOAD4 & CONCAT). subst bytes. rewrite in_app_iff.
destruct (zeq ofs ofs').
+ right. eapply (REC (sz - 1)). red; lia. eexact LOAD4. auto. lia.
Qed.

Lemma storebytes_provenance:
forall m b ofs bytes m' b' ofs' b'' ofs'' q i,
Mem.storebytes m b ofs bytes = Some m' ->
Mem.loadbytes m' b' ofs' 1 = Some (Fragment (Vptr b'' ofs'') q i :: nil) ->
In (Fragment (Vptr b'' ofs'') q i) bytes
\/ Mem.loadbytes m b' ofs' 1 = Some (Fragment (Vptr b'' ofs'') q i :: nil).
Proof.
intros.
assert (EITHER:
(b' <> b \/ ofs' + 1 <= ofs \/ ofs + Z.of_nat (length bytes) <= ofs')
\/ (b' = b /\ ofs <= ofs' < ofs + Z.of_nat (length bytes))).
{
destruct (eq_block b' b); auto.
destruct (zle (ofs' + 1) ofs); auto.
destruct (zle (ofs + Z.of_nat (length bytes)) ofs'); auto.
right. split. auto. lia.
}
destruct EITHER as [A | (A & B)].
- right. rewrite <- H0. symmetry. eapply Mem.loadbytes_storebytes_other; eauto. lia.
- subst b'. left.
Qed.

Lemma store_provenance:
forall chunk m b ofs v m' b' ofs' b'' ofs'' q i,
Mem.store chunk m b ofs v = Some m' ->
Mem.loadbytes m' b' ofs' 1 = Some (Fragment (Vptr b'' ofs'') q i :: nil) ->
v = Vptr b'' ofs'' /\ (chunk = Mint32 \/ chunk = Many32 \/ chunk = Mint64 \/ chunk = Many64)
\/ Mem.loadbytes m b' ofs' 1 = Some (Fragment (Vptr b'' ofs'') q i :: nil).
Proof.
intros. exploit storebytes_provenance; eauto. eapply Mem.store_storebytes; eauto.
intros [A|A]; auto. left.
generalize (encode_val_shape chunk v). intros ENC; inv ENC.
- split; auto. rewrite <- H1 in A; destruct A.
+ congruence.
+ exploit H5; eauto. intros (j & P & Q); congruence.
- rewrite <- H1 in A; destruct A.
+ congruence.
+ exploit H3; eauto. intros [byte P]; congruence.
- rewrite <- H1 in A; destruct A.
+ congruence.
+ exploit H2; eauto. congruence.
Qed.

Lemma smatch_store:
forall chunk m b ofs v m' b' p av,
Mem.store chunk m b ofs v = Some m' ->
smatch m b' p ->
vmatch v av ->
smatch m' b' (vplub av p).
Proof.
intros. destruct H0 as [A B]. split.
- intros chunk' ofs' v' LOAD. destruct v'; auto with va.
intros [(P & Q & R & S) | DISJ].
+ subst. apply vmatch_vplub_l. auto.
+ apply vmatch_vplub_r. apply A with (chunk := chunk') (ofs := ofs').
- intros. exploit store_provenance; eauto. intros [[P Q] | P].
+ subst.
assert (V: vmatch (Vptr b'0 ofs') (Ifptr (vplub av p))).
{
apply vmatch_vplub_l. auto.
}
inv V; auto.
+ apply pmatch_vplub. eapply B; eauto.
Qed.

Lemma smatch_storebytes:
forall m b ofs bytes m' b' p p',
Mem.storebytes m b ofs bytes = Some m' ->
smatch m b' p ->
(forall b' ofs' q i, In (Fragment (Vptr b' ofs') q i) bytes -> pmatch b' ofs' p') ->
smatch m' b' (plub p' p).
Proof.
intros. destruct H0 as [A B]. split.
- intros. apply vmatch_ifptr. intros bx ofsx EQ; subst v.
destruct bytes' as [ | byte1' bytes'].
exploit Mem.loadbytes_length; eauto. intros. destruct chunk; discriminate.
generalize (decode_val_shape chunk byte1' bytes'). rewrite <- Q.
intros DEC; inv DEC; try contradiction.
assert (v = Vptr bx ofsx).
{ destruct H5 as [E|[E|[E|E]]]; rewrite E in H4; destruct v; simpl in H4;
try congruence; destruct Archi.ptr64; congruence. }
exploit In_loadbytes; eauto. eauto with coqlib.
intros (ofs' & X & Y). subst v.
exploit storebytes_provenance; eauto. intros [Z | Z].
apply pmatch_lub_l. eauto.
apply pmatch_lub_r. eauto.
- intros. exploit storebytes_provenance; eauto. intros [Z | Z].
apply pmatch_lub_l. eauto.
apply pmatch_lub_r. eauto.
Qed.

Definition bmatch (m: mem) (b: block) (ab: ablock) : Prop :=
smatch m b ab.(ab_summary) /\
forall chunk ofs v, Mem.load chunk m b ofs = Some v -> vmatch v (ablock_load chunk ab ofs).

Lemma bmatch_ext:
forall m b ab m',
bmatch m b ab ->
(forall ofs n bytes, Mem.loadbytes m' b ofs n = Some bytes -> n >= 0 -> Mem.loadbytes m b ofs n = Some bytes) ->
bmatch m' b ab.
Proof.
intros. destruct H as [A B]. split; intros.
apply smatch_ext with m; auto.
Qed.

Lemma bmatch_inv:
forall m b ab m',
bmatch m b ab ->
(forall ofs n, n >= 0 -> Mem.loadbytes m' b ofs n = Mem.loadbytes m b ofs n) ->
bmatch m' b ab.
Proof.
intros. eapply bmatch_ext; eauto.
intros. rewrite <- H0; eauto.
Qed.

forall chunk m b ofs v ab,
Mem.load chunk m b ofs = Some v ->
bmatch m b ab ->
vmatch v (ablock_load chunk ab ofs).
Proof.
intros. destruct H0. eauto.
Qed.

forall chunk m b ofs v ab,
Mem.load chunk m b ofs = Some v ->
bmatch m b ab ->
Proof.
intros. destruct H0. destruct H0. unfold ablock_load_anywhere.
eapply vnormalize_cast; eauto.
Qed.

Lemma ablock_init_sound:
forall m b p, smatch m b p -> bmatch m b (ablock_init p).
Proof.
intros; split; auto; intros.
eapply vnormalize_cast; eauto. eapply H; eauto.
Qed.

Lemma ablock_store_anywhere_sound:
forall chunk m b ofs v m' b' ab av,
Mem.store chunk m b ofs v = Some m' ->
bmatch m b' ab ->
vmatch v av ->
bmatch m' b' (ablock_store_anywhere chunk ab av).
Proof.
intros. destruct H0 as [A B]. unfold ablock_store_anywhere.
apply ablock_init_sound. eapply smatch_store; eauto.
Qed.

Remark inval_after_outside:
forall i lo hi c, i < lo \/ i > hi -> (inval_after lo hi c)##i = c##i.
Proof.
intros until c. functional induction (inval_after lo hi c); intros.
rewrite IHt by lia. apply ZTree.gro. unfold ZTree.elt, ZIndexed.t; lia.
auto.
Qed.

Remark inval_after_contents:
forall chunk av i lo hi c,
(inval_after lo hi c)##i = Some (ACval chunk av) ->
c##i = Some (ACval chunk av) /\ (i < lo \/ i > hi).
Proof.
intros until c. functional induction (inval_after lo hi c); intros.
destruct (zeq i hi).
subst i. rewrite inval_after_outside in H by lia. rewrite ZTree.grs in H. discriminate.
exploit IHt; eauto. intros [A B]. rewrite ZTree.gro in A by auto. split. auto. lia.
split. auto. lia.
Qed.

Remark inval_before_outside:
forall i hi lo c, i < lo \/ i >= hi -> (inval_before hi lo c)##i = c##i.
Proof.
intros until c. functional induction (inval_before hi lo c); intros.
rewrite IHt by lia. unfold inval_if. destruct (c##lo) as [[chunk av]|]; auto.
destruct (zle (lo + size_chunk chunk) hi); auto.
apply ZTree.gro. unfold ZTree.elt, ZIndexed.t; lia.
auto.
Qed.

Remark inval_before_contents_1:
forall i chunk av lo hi c,
lo <= i < hi -> (inval_before hi lo c)##i = Some(ACval chunk av) ->
c##i = Some(ACval chunk av) /\ i + size_chunk chunk <= hi.
Proof.
intros until c. functional induction (inval_before hi lo c); intros.
- destruct (zeq lo i).
+ subst i. rewrite inval_before_outside in H0 by lia.
unfold inval_if in H0. destruct (c##lo) as [[chunk0 v0]|] eqn:C; try congruence.
destruct (zle (lo + size_chunk chunk0) hi).
rewrite C in H0; inv H0. auto.
rewrite ZTree.grs in H0. congruence.
+ exploit IHt. lia. auto. intros [A B]; split; auto.
unfold inval_if in A. destruct (c##lo) as [[chunk0 v0]|] eqn:C; auto.
destruct (zle (lo + size_chunk chunk0) hi); auto.
rewrite ZTree.gro in A; auto.
- extlia.
Qed.

Lemma max_size_chunk: forall chunk, size_chunk chunk <= 8.
Proof.
destruct chunk; simpl; lia.
Qed.

Remark inval_before_contents:
forall i c chunk' av' j,
(inval_before i (i - 7) c)##j = Some (ACval chunk' av') ->
c##j = Some (ACval chunk' av') /\ (j + size_chunk chunk' <= i \/ i <= j).
Proof.
intros. destruct (zlt j (i - 7)).
rewrite inval_before_outside in H by lia.
split. auto. left. generalize (max_size_chunk chunk'); lia.
destruct (zlt j i).
exploit inval_before_contents_1; eauto. lia. tauto.
rewrite inval_before_outside in H by lia.
split. auto. lia.
Qed.

Lemma ablock_store_contents:
forall chunk ab i av j chunk' av',
(ablock_store chunk ab i av).(ab_contents)##j = Some(ACval chunk' av') ->
(i = j /\ chunk' = chunk /\ av' = av)
\/ (ab.(ab_contents)##j = Some(ACval chunk' av')
/\ (j + size_chunk chunk' <= i \/ i + size_chunk chunk <= j)).
Proof.
unfold ablock_store; simpl; intros.
destruct (zeq i j).
subst j. rewrite ZTree.gss in H. inv H; auto.
right. rewrite ZTree.gso in H by auto.
exploit inval_before_contents; eauto. intros [A B].
exploit inval_after_contents; eauto. intros [C D].
split. auto. lia.
Qed.

Lemma chunk_compat_true:
forall c c',
chunk_compat c c' = true ->
size_chunk c = size_chunk c' /\ align_chunk c <= align_chunk c' /\ type_of_chunk c = type_of_chunk c'.
Proof.
destruct c, c'; intros; try discriminate; simpl; auto with va.
Qed.

Lemma ablock_store_sound:
forall chunk m b ofs v m' ab av,
Mem.store chunk m b ofs v = Some m' ->
bmatch m b ab ->
vmatch v av ->
bmatch m' b (ablock_store chunk ab ofs av).
Proof.
intros until av; intros STORE BIN VIN. destruct BIN as [BIN1 BIN2]. split.
eapply smatch_store; eauto.
assert (SUMMARY: vmatch v' (vnormalize chunk' (Ifptr (vplub av ab.(ab_summary))))).
{ exploit smatch_store; eauto. intros [A B]. eapply vnormalize_cast; eauto. }
destruct ((ab_contents (ablock_store chunk ab ofs av)) ## ofs') as [[chunk1 av1]|] eqn:C; auto.
destruct (chunk_compat chunk' chunk1) eqn:COMPAT; auto.
exploit chunk_compat_true; eauto. intros (U & V & W).
exploit ablock_store_contents; eauto. intros [(P & Q & R) | (P & Q)].
- (* same offset and compatible chunks *)
subst.
assert (v' = Val.load_result chunk' v).
{ exploit Mem.load_store_similar_2; eauto. congruence. }
subst v'. apply vnormalize_sound; auto.
assert (Mem.load chunk' m b ofs' = Some v').
rewrite U. auto. }
exploit BIN2; eauto. unfold ablock_load. rewrite P. rewrite COMPAT. auto.
Qed.