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


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

Definition block_class_eq: forall (x y: block_class), {x=y} + {x<>y}.

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.

Hint Extern 2 (_ = _) => congruence : va.
Hint Extern 2 (_ <> _) => congruence : va.
Hint Extern 2 (_ < _) => xomega : va.
Hint Extern 2 (_ <= _) => xomega : va.
Hint Extern 2 (_ > _) => xomega : va.
Hint Extern 2 (_ >= _) => xomega : 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).

Lemma cmatch_lub_r:
  forall ob x y, cmatch ob y -> cmatch ob (club x y).

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).

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}.

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.

Lemma pmatch_ge:
  forall b ofs p q, pge p q -> pmatch b ofs q -> pmatch b ofs p.

Lemma pmatch_top': forall b ofs p, pmatch b ofs p -> pmatch b ofs Ptop.

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.

Lemma pge_lub_l:
  forall p q, pge (plub p q) p.

Lemma pge_lub_r:
  forall p q, pge (plub p q) q.

Lemma pmatch_lub_l:
  forall b ofs p q, pmatch b ofs p -> pmatch b ofs (plub p q).

Lemma pmatch_lub_r:
  forall b ofs p q, pmatch b ofs q -> pmatch b ofs (plub p q).

Lemma plub_least:
  forall r p q, pge r p -> pge r q -> pge r (plub p q).

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.

Lemma pincl_ge_2: forall p q, pge p q -> pincl q p = true.

Lemma pincl_sound:
  forall b ofs p q,
  pincl p q = true -> pmatch b ofs p -> pmatch b ofs q.

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.

Lemma padd_sound:
  forall b ofs p delta,
  pmatch b ofs p ->
  pmatch b (Ptrofs.add ofs delta) (padd p delta).

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).

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).

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).

Lemma cmp_different_blocks_sound:
  forall c, cmatch (Val.cmp_different_blocks c) (cmp_different_blocks c).

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).

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).

Lemma pcmp_none:
  forall c p1 p2, cmatch None (pcmp c p1 p2).

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.

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 *)
  | 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 *)


Definition Vtop := Ifptr Ptop.


Definition eq_aval: forall (v1 v2: aval), {v1=v2} + {v1<>v2}.

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_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).

Lemma vmatch_ifptr:
  forall v p,
  (forall b ofs, v = Vptr b ofs -> pmatch b ofs p) ->
  vmatch v (Ifptr p).

Lemma vmatch_top: forall v x, vmatch v x -> vmatch v Vtop.

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


Lemma is_uns_mon: forall n1 n2 i, is_uns n1 i -> n1 <= n2 -> is_uns n2 i.

Lemma is_sgn_mon: forall n1 n2 i, is_sgn n1 i -> n1 <= n2 -> is_sgn n2 i.

Lemma is_uns_sgn: forall n1 n2 i, is_uns n1 i -> n1 < n2 -> is_sgn n2 i.

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.

Lemma is_sgn_ssize:
  forall i, is_sgn (ssize i) i.

Lemma is_uns_zero_ext:
  forall n i, is_uns n i <-> Int.zero_ext n i = i.

Lemma is_sgn_sign_ext:
  forall n i, 0 < n -> (is_sgn n i <-> Int.sign_ext n i = i).

Lemma is_zero_ext_uns:
  forall i n m,
  is_uns m i \/ n <= m -> is_uns m (Int.zero_ext n i).

Lemma is_zero_ext_sgn:
  forall i n m,
  n < m ->
  is_sgn m (Int.zero_ext n i).

Lemma is_sign_ext_uns:
  forall i n m,
  0 <= m < n ->
  is_uns m i ->
  is_uns m (Int.sign_ext n i).

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).

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.


Definition provenance (x: aval) : aptr :=
  if va_strict tt then Pbot else
    match x with
    | Ptr p | Ifptr p | Uns p _ | Sgn p _ => poffset p
    | _ => Pbot
    end.

Definition ntop : aval := Ifptr Pbot.

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

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


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 Ifptr 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 Ifptr p.

Lemma vmatch_uns':
  forall p i n, is_uns (Z.max 0 n) i -> vmatch (Vint i) (uns p n).

Lemma vmatch_uns:
  forall p i n, is_uns n i -> vmatch (Vint i) (uns p n).

Lemma vmatch_uns_undef: forall p n, vmatch Vundef (uns p n).

Lemma vmatch_sgn':
  forall p i n, is_sgn (Z.max 1 n) i -> vmatch (Vint i) (sgn p n).

Lemma vmatch_sgn:
  forall p i n, is_sgn n i -> vmatch (Vint i) (sgn p n).

Lemma vmatch_sgn_undef: forall p n, vmatch Vundef (sgn p n).

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.


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_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).

Hint Constructors vge : va.

Lemma vge_top: forall v, vge Vtop v.

Hint Resolve vge_top : va.

Lemma vge_refl: forall v, vge v v.

Lemma vge_trans: forall u v, vge u v -> forall w, vge v w -> vge u w.

Lemma vmatch_ge:
  forall v x y, vge x y -> vmatch v y -> vmatch v x.


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, (Ptr p | Ifptr p) | (Ptr p | Ifptr p), I i =>
      if va_strict tt || Int.eq i Int.zero then Ifptr p else Vtop
  | 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)
  | F f1, F f2 =>
      if Float.eq_dec f1 f2 then v else ntop
  | FS f1, FS f2 =>
      if Float32.eq_dec f1 f2 then v else ntop
  | L i1, L i2 =>
      if Int64.eq i1 i2 then v else ntop
  | Ptr p1, Ptr p2 => Ptr(plub p1 p2)
  | Ptr p1, Ifptr p2 => Ifptr(plub p1 p2)
  | Ifptr p1, Ptr p2 => Ifptr(plub p1 p2)
  | Ifptr p1, Ifptr p2 => Ifptr(plub p1 p2)
  | (Ptr p1 | Ifptr p1), (Uns p2 _ | Sgn p2 _) => Ifptr(plub p1 p2)
  | (Uns p1 _ | Sgn p1 _), (Ptr p2 | Ifptr p2) => Ifptr(plub p1 p2)
  | _, (Ptr p | Ifptr p) | (Ptr p | Ifptr p), _ => if va_strict tt then Ifptr p else Vtop
  | _, _ => Vtop
  end.

Lemma vlub_comm:
  forall v w, vlub v w = vlub w v.

Lemma vge_uns_uns': forall p n, vge (uns p n) (Uns p n).

Lemma vge_uns_i': forall p n i, 0 <= n -> is_uns n i -> vge (uns p n) (I i).

Lemma vge_sgn_sgn': forall p n, vge (sgn p n) (Sgn p n).

Lemma vge_sgn_i': forall p n i, 0 < n -> is_sgn n i -> vge (sgn p n) (I i).

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

Lemma usize_pos: forall n, 0 <= usize n.

Lemma ssize_pos: forall n, 0 < ssize n.

Lemma vge_lub_l:
  forall x y, vge (vlub x y) x.

Lemma vge_lub_r:
  forall x y, vge (vlub x y) y.

Lemma vmatch_lub_l:
  forall v x y, vmatch v x -> vmatch v (vlub x y).

Lemma vmatch_lub_r:
  forall v x y, vmatch v y -> vmatch v (vlub x y).


Definition aptr_of_aval (v: aval) : aptr :=
  match v with
  | Ptr p => p
  | Ifptr p => p
  | _ => if va_strict tt then Pbot else Nonstack
  end.

Lemma match_aptr_of_aval:
  forall b ofs av,
  vmatch (Vptr b ofs) av -> pmatch b ofs (aptr_of_aval av).

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)).

Lemma pmatch_vplub:
  forall b ofs x p, pmatch b ofs p -> pmatch b ofs (vplub x p).

Lemma vmatch_vplub_r:
  forall v x p, vmatch v (Ifptr p) -> vmatch v (Ifptr (vplub x p)).


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

Lemma vpincl_ge:
  forall x p, vpincl x p = true -> vge (Ifptr p) x.

Lemma vpincl_sound:
  forall v x p, vpincl x p = true -> vmatch v x -> vmatch v (Ifptr p).

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
  | Ptr p, Ptr q => pincl p q
  | (Ptr p | Ifptr p | Uns p _ | Sgn p _), Ifptr q => pincl p q
  | _, Ifptr _ => true
  | _, _ => false
  end.

Lemma vincl_ge: forall v w, vincl v w = true -> vge w v.


Definition genv_match (ge: 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).

Lemma symbol_address_sound:
  forall ge id ofs,
  genv_match ge ->
  vmatch (Genv.symbol_address ge id ofs) (Ptr (Gl id ofs)).

Lemma vmatch_ptr_gl:
  forall ge v id ofs,
  genv_match ge ->
  vmatch v (Ptr (Gl id ofs)) ->
  Val.lessdef v (Genv.symbol_address ge id ofs).

Lemma vmatch_ptr_stk:
  forall v ofs sp,
  vmatch v (Ptr(Stk ofs)) ->
  bc sp = BCstack ->
  Val.lessdef v (Vptr sp ofs).


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).

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).

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).

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).

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).

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).

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).

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).


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).

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).

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).

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).

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).

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).

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).

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).

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).

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

Lemma rolm_sound:
  forall v x amount mask,
  vmatch v x -> vmatch (Val.rolm v amount mask) (rolm x amount mask).


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.

Lemma add_sound:
  forall v w x y, vmatch v x -> vmatch w y -> vmatch (Val.add v w) (add x y).

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).

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).

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).

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).

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).

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).


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).

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).

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.

Lemma addl_sound:
  forall v w x y, vmatch v x -> vmatch w y -> vmatch (Val.addl v w) (addl x y).

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).

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).

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).

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).

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).

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).

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

Lemma rolml_sound:
  forall v x amount mask,
  vmatch v x -> vmatch (Val.rolml v amount mask) (rolml x amount mask).


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).


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).

Definition addf := binop_float Float.add.

Lemma addf_sound:
  forall v x w y, vmatch v x -> vmatch w y -> vmatch (Val.addf v w) (addf x y).
Proof (binop_float_sound Float.add).

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 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).

Definition addfs := binop_single Float32.add.

Lemma addfs_sound:
  forall v x w y, vmatch v x -> vmatch w y -> vmatch (Val.addfs v w) (addfs x y).
Proof (binop_single_sound Float32.add).

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 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).

Definition sign_ext (nbits: Z) (v: aval) :=
  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, 0 < nbits -> vmatch v x -> vmatch (Val.sign_ext nbits v) (sign_ext nbits x).

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).

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).

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).

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).

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).

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).

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).

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).

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).

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).

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).

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).

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).

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).

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).

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).

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).

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).

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).

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).

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).

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).

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).

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).


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).

Lemma cmp_intv_None:
  forall c i n, cmatch None (cmp_intv c i n).

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).

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)).

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)).

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).

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)).

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)).


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).

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).

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).

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).

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).

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).

Definition maskzero (x: aval) (mask: int) : abool :=
  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.

Lemma maskzero_sound:
  forall mask v x,
  vmatch v x ->
  cmatch (Val.maskzero_bool v mask) (maskzero x mask).

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).

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.


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 _ _ | Ifptr _) => v
  | Mint32, Ptr p => if Archi.ptr64 then Ifptr p else v
  | Mint64, (L _ | Ifptr _) => v
  | Mint64, (Uns p _ | Sgn p _) => Ifptr p
  | Mint64, Ptr p => if Archi.ptr64 then v else Ifptr p
  | Mfloat32, FS f => v
  | Mfloat64, F f => v
  | Many32, (I _ | Uns _ _ | Sgn _ _ | FS _ | Ifptr _) => v
  | Many32, Ptr p => if Archi.ptr64 then Ifptr p else v
  | Many64, _ => v
  | _, _ => Ifptr (provenance v)
  end.

Lemma vnormalize_sound:
  forall chunk v x, vmatch v x -> vmatch (Val.load_result chunk v) (vnormalize chunk x).

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)).

Remark poffset_monotone:
  forall p q, pge p q -> pge (poffset p) (poffset q).

Remark provenance_monotone:
  forall x y, vge x y -> pge (provenance x) (provenance y).

Lemma vnormalize_monotone:
  forall chunk x y,
  vge x y -> vge (vnormalize chunk x) (vnormalize chunk y).


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

Definition eq_acontent : forall (c1 c2: acontent), {c1=c2} + {c1<>c2}.

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.

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.

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).

Remark loadbytes_load_ext:
  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.

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.

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.

Lemma smatch_ge:
  forall m b p q, smatch m b p -> pge q p -> smatch m b q.

Lemma In_loadbytes:
  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).

Lemma smatch_loadbytes:
  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.

Lemma loadbytes_provenance:
  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.

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).

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).

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).

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).

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.

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.

Lemma ablock_load_sound:
  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).

Lemma ablock_load_anywhere_sound:
  forall chunk m b ofs v ab,
  Mem.load chunk m b ofs = Some v ->
  bmatch m b ab ->
  vmatch v (ablock_load_anywhere chunk ab).

Lemma ablock_init_sound:
  forall m b p, smatch m b p -> bmatch m b (ablock_init p).

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).

Remark inval_after_outside:
  forall i lo hi c, i < lo \/ i > hi -> (inval_after lo hi c)##i = c##i.

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).

Remark inval_before_outside:
  forall i hi lo c, i < lo \/ i >= hi -> (inval_before hi lo c)##i = c##i.

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.

Lemma max_size_chunk: forall chunk, size_chunk chunk <= 8.

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).

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)).

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'.

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).

Lemma ablock_loadbytes_sound:
  forall m b ab b' ofs' q i n ofs bytes,
  Mem.loadbytes m b ofs n = Some bytes ->
  bmatch m b ab ->
  In (Fragment (Vptr b' ofs') q i) bytes ->
  pmatch b' ofs' (ablock_loadbytes ab).

Lemma ablock_storebytes_anywhere_sound:
  forall m b ofs bytes p m' b' ab,
  Mem.storebytes m b ofs bytes = Some m' ->
  (forall b' ofs' q i, In (Fragment (Vptr b' ofs') q i) bytes -> pmatch b' ofs' p) ->
  bmatch m b' ab ->
  bmatch m' b' (ablock_storebytes_anywhere ab p).

Lemma ablock_storebytes_contents:
  forall ab p i sz j chunk' av',
  (ablock_storebytes ab p i sz).(ab_contents)##j = Some(ACval chunk' av') ->
  ab.(ab_contents)##j = Some (ACval chunk' av')
  /\ (j + size_chunk chunk' <= i \/ i + Z.max sz 0 <= j).

Lemma ablock_storebytes_sound:
  forall m b ofs bytes m' p ab sz,
  Mem.storebytes m b ofs bytes = Some m' ->
  length bytes = nat_of_Z sz ->
  (forall b' ofs' q i, In (Fragment (Vptr b' ofs') q i) bytes -> pmatch b' ofs' p) ->
  bmatch m b ab ->
  bmatch m' b (ablock_storebytes ab p ofs sz).


Definition bbeq (ab1 ab2: ablock) : bool :=
  eq_aptr ab1.(ab_summary) ab2.(ab_summary) &&
  ZTree.beq (fun c1 c2 => proj_sumbool (eq_acontent c1 c2)) ab1.(ab_contents) ab2.(ab_contents).

Lemma bbeq_load:
  forall ab1 ab2,
  bbeq ab1 ab2 = true ->
  ab1.(ab_summary) = ab2.(ab_summary)
  /\ (forall chunk i, ablock_load chunk ab1 i = ablock_load chunk ab2 i).

Lemma bbeq_sound:
  forall ab1 ab2,
  bbeq ab1 ab2 = true ->
  forall m b, bmatch m b ab1 <-> bmatch m b ab2.


Definition combine_acontents (c1 c2: option acontent) : option acontent :=
  match c1, c2 with
  | Some (ACval chunk1 v1), Some (ACval chunk2 v2) =>
      if chunk_eq chunk1 chunk2 then Some(ACval chunk1 (vlub v1 v2)) else None
  | _, _ =>
      None
  end.

Definition blub (ab1 ab2: ablock) : ablock :=
  {| ab_contents := ZTree.combine_inter combine_acontents ab1.(ab_contents) ab2.(ab_contents);
     ab_summary := plub ab1.(ab_summary) ab2.(ab_summary) |}.

Lemma smatch_lub_l:
  forall m b p q, smatch m b p -> smatch m b (plub p q).

Lemma smatch_lub_r:
  forall m b p q, smatch m b q -> smatch m b (plub p q).

Lemma bmatch_lub_l:
  forall m b x y, bmatch m b x -> bmatch m b (blub x y).

Lemma bmatch_lub_r:
  forall m b x y, bmatch m b y -> bmatch m b (blub x y).

Abstracting read-only global variables

Definition romem := PTree.t ablock.

Definition romatch (m: mem) (rm: romem) : Prop :=
  forall b id ab,
  bc b = BCglob id ->
  rm!id = Some ab ->
  pge Glob ab.(ab_summary)
  /\ bmatch m b ab
  /\ forall ofs, ~Mem.perm m b ofs Max Writable.

Lemma romatch_store:
  forall chunk m b ofs v m' rm,
  Mem.store chunk m b ofs v = Some m' ->
  romatch m rm ->
  romatch m' rm.

Lemma romatch_storebytes:
  forall m b ofs bytes m' rm,
  Mem.storebytes m b ofs bytes = Some m' ->
  romatch m rm ->
  romatch m' rm.

Lemma romatch_ext:
  forall m rm m',
  romatch m rm ->
  (forall b id ofs n bytes, bc b = BCglob id -> Mem.loadbytes m' b ofs n = Some bytes -> Mem.loadbytes m b ofs n = Some bytes) ->
  (forall b id ofs p, bc b = BCglob id -> Mem.perm m' b ofs Max p -> Mem.perm m b ofs Max p) ->
  romatch m' rm.

Lemma romatch_free:
  forall m b lo hi m' rm,
  Mem.free m b lo hi = Some m' ->
  romatch m rm ->
  romatch m' rm.

Lemma romatch_alloc:
  forall m b lo hi m' rm,
  Mem.alloc m lo hi = (m', b) ->
  bc_below bc (Mem.nextblock m) ->
  romatch m rm ->
  romatch m' rm.

Abstracting memory states

Record amem : Type := AMem {
  am_stack: ablock;
  am_glob: PTree.t ablock;
  am_nonstack: aptr;
  am_top: aptr
}.

Record mmatch (m: mem) (am: amem) : Prop := mk_mem_match {
  mmatch_stack: forall b,
    bc b = BCstack ->
    bmatch m b am.(am_stack);
  mmatch_glob: forall id ab b,
    bc b = BCglob id ->
    am.(am_glob)!id = Some ab ->
    bmatch m b ab;
  mmatch_nonstack: forall b,
    bc b <> BCstack -> bc b <> BCinvalid ->
    smatch m b am.(am_nonstack);
  mmatch_top: forall b,
    bc b <> BCinvalid ->
    smatch m b am.(am_top);
  mmatch_below:
    bc_below bc (Mem.nextblock m)
}.

Definition minit (p: aptr) :=
  {| am_stack := ablock_init p;
     am_glob := PTree.empty _;
     am_nonstack := p;
     am_top := p |}.

Definition mbot := minit Pbot.
Definition mtop := minit Ptop.

Definition load (chunk: memory_chunk) (rm: romem) (m: amem) (p: aptr) : aval :=
  match p with
  | Pbot => if va_strict tt then Vbot else Vtop
  | Gl id ofs =>
      match rm!id with
      | Some ab => ablock_load chunk ab (Ptrofs.unsigned ofs)
      | None =>
          match m.(am_glob)!id with
          | Some ab => ablock_load chunk ab (Ptrofs.unsigned ofs)
          | None => vnormalize chunk (Ifptr m.(am_nonstack))
          end
      end
  | Glo id =>
      match rm!id with
      | Some ab => ablock_load_anywhere chunk ab
      | None =>
          match m.(am_glob)!id with
          | Some ab => ablock_load_anywhere chunk ab
          | None => vnormalize chunk (Ifptr m.(am_nonstack))
          end
      end
  | Stk ofs => ablock_load chunk m.(am_stack) (Ptrofs.unsigned ofs)
  | Stack => ablock_load_anywhere chunk m.(am_stack)
  | Glob | Nonstack => vnormalize chunk (Ifptr m.(am_nonstack))
  | Ptop => vnormalize chunk (Ifptr m.(am_top))
  end.

Definition loadv (chunk: memory_chunk) (rm: romem) (m: amem) (addr: aval) : aval :=
  load chunk rm m (aptr_of_aval addr).

Definition store (chunk: memory_chunk) (m: amem) (p: aptr) (av: aval) : amem :=
  {| am_stack :=
       match p with
       | Stk ofs => ablock_store chunk m.(am_stack) (Ptrofs.unsigned ofs) av
       | Stack | Ptop => ablock_store_anywhere chunk m.(am_stack) av
       | _ => m.(am_stack)
       end;
     am_glob :=
       match p with
       | Gl id ofs =>
           let ab := match m.(am_glob)!id with Some ab => ab | None => ablock_init m.(am_nonstack) end in
           PTree.set id (ablock_store chunk ab (Ptrofs.unsigned ofs) av) m.(am_glob)
       | Glo id =>
           let ab := match m.(am_glob)!id with Some ab => ab | None => ablock_init m.(am_nonstack) end in
           PTree.set id (ablock_store_anywhere chunk ab av) m.(am_glob)
       | Glob | Nonstack | Ptop => PTree.empty _
       | _ => m.(am_glob)
       end;
     am_nonstack :=
       match p with
       | Gl _ _ | Glo _ | Glob | Nonstack | Ptop => vplub av m.(am_nonstack)
       | _ => m.(am_nonstack)
       end;
     am_top := vplub av m.(am_top)
  |}.

Definition storev (chunk: memory_chunk) (m: amem) (addr: aval) (v: aval): amem :=
  store chunk m (aptr_of_aval addr) v.

Definition loadbytes (m: amem) (rm: romem) (p: aptr) : aptr :=
  match p with
  | Pbot => if va_strict tt then Pbot else Ptop
  | Gl id _ | Glo id =>
      match rm!id with
      | Some ab => ablock_loadbytes ab
      | None =>
          match m.(am_glob)!id with
          | Some ab => ablock_loadbytes ab
          | None => m.(am_nonstack)
          end
      end
  | Stk _ | Stack => ablock_loadbytes m.(am_stack)
  | Glob | Nonstack => m.(am_nonstack)
  | Ptop => m.(am_top)
  end.

Definition storebytes (m: amem) (dst: aptr) (sz: Z) (p: aptr) : amem :=
  {| am_stack :=
       match dst with
       | Stk ofs => ablock_storebytes m.(am_stack) p (Ptrofs.unsigned ofs) sz
       | Stack | Ptop => ablock_storebytes_anywhere m.(am_stack) p
       | _ => m.(am_stack)
       end;
     am_glob :=
       match dst with
       | Gl id ofs =>
           let ab := match m.(am_glob)!id with Some ab => ab | None => ablock_init m.(am_nonstack) end in
           PTree.set id (ablock_storebytes ab p (Ptrofs.unsigned ofs) sz) m.(am_glob)
       | Glo id =>
           let ab := match m.(am_glob)!id with Some ab => ab | None => ablock_init m.(am_nonstack) end in
           PTree.set id (ablock_storebytes_anywhere ab p) m.(am_glob)
       | Glob | Nonstack | Ptop => PTree.empty _
       | _ => m.(am_glob)
       end;
     am_nonstack :=
       match dst with
       | Gl _ _ | Glo _ | Glob | Nonstack | Ptop => plub p m.(am_nonstack)
       | _ => m.(am_nonstack)
       end;
     am_top := plub p m.(am_top)
  |}.

Theorem load_sound:
  forall chunk m b ofs v rm am p,
  Mem.load chunk m b (Ptrofs.unsigned ofs) = Some v ->
  romatch m rm ->
  mmatch m am ->
  pmatch b ofs p ->
  vmatch v (load chunk rm am p).

Theorem loadv_sound:
  forall chunk m addr v rm am aaddr,
  Mem.loadv chunk m addr = Some v ->
  romatch m rm ->
  mmatch m am ->
  vmatch addr aaddr ->
  vmatch v (loadv chunk rm am aaddr).

Theorem store_sound:
  forall chunk m b ofs v m' am p av,
  Mem.store chunk m b (Ptrofs.unsigned ofs) v = Some m' ->
  mmatch m am ->
  pmatch b ofs p ->
  vmatch v av ->
  mmatch m' (store chunk am p av).

Theorem storev_sound:
  forall chunk m addr v m' am aaddr av,
  Mem.storev chunk m addr v = Some m' ->
  mmatch m am ->
  vmatch addr aaddr ->
  vmatch v av ->
  mmatch m' (storev chunk am aaddr av).

Theorem loadbytes_sound:
  forall m b ofs sz bytes am rm p,
  Mem.loadbytes m b (Ptrofs.unsigned ofs) sz = Some bytes ->
  romatch m rm ->
  mmatch m am ->
  pmatch b ofs p ->
  forall b' ofs' q i, In (Fragment (Vptr b' ofs') q i) bytes -> pmatch b' ofs' (loadbytes am rm p).

Theorem storebytes_sound:
  forall m b ofs bytes m' am p sz q,
  Mem.storebytes m b (Ptrofs.unsigned ofs) bytes = Some m' ->
  mmatch m am ->
  pmatch b ofs p ->
  length bytes = nat_of_Z sz ->
  (forall b' ofs' qt i, In (Fragment (Vptr b' ofs') qt i) bytes -> pmatch b' ofs' q) ->
  mmatch m' (storebytes am p sz q).

Lemma mmatch_ext:
  forall m am m',
  mmatch m am ->
  (forall b ofs n bytes, bc b <> BCinvalid -> n >= 0 -> Mem.loadbytes m' b ofs n = Some bytes -> Mem.loadbytes m b ofs n = Some bytes) ->
  Ple (Mem.nextblock m) (Mem.nextblock m') ->
  mmatch m' am.

Lemma mmatch_free:
  forall m b lo hi m' am,
  Mem.free m b lo hi = Some m' ->
  mmatch m am ->
  mmatch m' am.

Lemma mmatch_top':
  forall m am, mmatch m am -> mmatch m mtop.


Definition mbeq (m1 m2: amem) : bool :=
  eq_aptr m1.(am_top) m2.(am_top)
  && eq_aptr m1.(am_nonstack) m2.(am_nonstack)
  && bbeq m1.(am_stack) m2.(am_stack)
  && PTree.beq bbeq m1.(am_glob) m2.(am_glob).

Lemma mbeq_sound:
  forall m1 m2, mbeq m1 m2 = true -> forall m, mmatch m m1 <-> mmatch m m2.


Definition combine_ablock (ob1 ob2: option ablock) : option ablock :=
  match ob1, ob2 with
  | Some b1, Some b2 => Some (blub b1 b2)
  | _, _ => None
  end.

Definition mlub (m1 m2: amem) : amem :=
{| am_stack := blub m1.(am_stack) m2.(am_stack);
   am_glob := PTree.combine_inter combine_ablock m1.(am_glob) m2.(am_glob);
   am_nonstack := plub m1.(am_nonstack) m2.(am_nonstack);
   am_top := plub m1.(am_top) m2.(am_top) |}.

Lemma mmatch_lub_l:
  forall m x y, mmatch m x -> mmatch m (mlub x y).

Lemma mmatch_lub_r:
  forall m x y, mmatch m y -> mmatch m (mlub x y).

End MATCH.

Monotonicity properties when the block classification changes.

Lemma genv_match_exten:
  forall ge (bc1 bc2: block_classification),
  genv_match bc1 ge ->
  (forall b id, bc1 b = BCglob id <-> bc2 b = BCglob id) ->
  (forall b, bc1 b = BCother -> bc2 b = BCother) ->
  genv_match bc2 ge.

Lemma romatch_exten:
  forall (bc1 bc2: block_classification) m rm,
  romatch bc1 m rm ->
  (forall b id, bc2 b = BCglob id <-> bc1 b = BCglob id) ->
  romatch bc2 m rm.

Definition bc_incr (bc1 bc2: block_classification) : Prop :=
  forall b, bc1 b <> BCinvalid -> bc2 b = bc1 b.

Section MATCH_INCR.

Variables bc1 bc2: block_classification.
Hypothesis INCR: bc_incr bc1 bc2.

Lemma pmatch_incr: forall b ofs p, pmatch bc1 b ofs p -> pmatch bc2 b ofs p.

Lemma vmatch_incr: forall v x, vmatch bc1 v x -> vmatch bc2 v x.

Lemma smatch_incr: forall m b p, smatch bc1 m b p -> smatch bc2 m b p.

Lemma bmatch_incr: forall m b ab, bmatch bc1 m b ab -> bmatch bc2 m b ab.

End MATCH_INCR.

Matching and memory injections.

Definition inj_of_bc (bc: block_classification) : meminj :=
  fun b => match bc b with BCinvalid => None | _ => Some(b, 0) end.

Lemma inj_of_bc_valid:
  forall (bc: block_classification) b, bc b <> BCinvalid -> inj_of_bc bc b = Some(b, 0).

Lemma inj_of_bc_inv:
  forall (bc: block_classification) b b' delta,
  inj_of_bc bc b = Some(b', delta) -> bc b <> BCinvalid /\ b' = b /\ delta = 0.

Lemma pmatch_inj:
  forall bc b ofs p, pmatch bc b ofs p -> inj_of_bc bc b = Some(b, 0).

Lemma vmatch_inj:
  forall bc v x, vmatch bc v x -> Val.inject (inj_of_bc bc) v v.

Lemma vmatch_list_inj:
  forall bc vl xl, list_forall2 (vmatch bc) vl xl -> Val.inject_list (inj_of_bc bc) vl vl.

Lemma mmatch_inj:
  forall bc m am, mmatch bc m am -> bc_below bc (Mem.nextblock m) -> Mem.inject (inj_of_bc bc) m m.

Lemma inj_of_bc_preserves_globals:
  forall bc ge, genv_match bc ge -> meminj_preserves_globals ge (inj_of_bc bc).

Lemma pmatch_inj_top:
  forall bc b b' delta ofs, inj_of_bc bc b = Some(b', delta) -> pmatch bc b ofs Ptop.

Lemma vmatch_inj_top:
  forall bc v v', Val.inject (inj_of_bc bc) v v' -> vmatch bc v Vtop.

Lemma mmatch_inj_top:
  forall bc m m', Mem.inject (inj_of_bc bc) m m' -> mmatch bc m mtop.

Abstracting RTL register environments

Module AVal <: SEMILATTICE_WITH_TOP.

  Definition t := aval.
  Definition eq (x y: t) := (x = y).
  Definition eq_refl: forall x, eq x x := (@eq_refl t).
  Definition eq_sym: forall x y, eq x y -> eq y x := (@eq_sym t).
  Definition eq_trans: forall x y z, eq x y -> eq y z -> eq x z := (@eq_trans t).
  Definition beq (x y: t) : bool := proj_sumbool (eq_aval x y).
  Lemma beq_correct: forall x y, beq x y = true -> eq x y.
  Definition ge := vge.
  Lemma ge_refl: forall x y, eq x y -> ge x y.
  Lemma ge_trans: forall x y z, ge x y -> ge y z -> ge x z.
  Definition bot : t := Vbot.
  Lemma ge_bot: forall x, ge x bot.
  Definition top : t := Vtop.
  Lemma ge_top: forall x, ge top x.
  Definition lub := vlub.
  Lemma ge_lub_left: forall x y, ge (lub x y) x.
  Proof vge_lub_l.
  Lemma ge_lub_right: forall x y, ge (lub x y) y.
  Proof vge_lub_r.
End AVal.

Module AE := LPMap(AVal).

Definition aenv := AE.t.

Section MATCHENV.

Variable bc: block_classification.

Definition ematch (e: regset) (ae: aenv) : Prop :=
  forall r, vmatch bc e#r (AE.get r ae).

Lemma ematch_ge:
  forall e ae1 ae2,
  ematch e ae1 -> AE.ge ae2 ae1 -> ematch e ae2.

Lemma ematch_update:
  forall e ae v av r,
  ematch e ae -> vmatch bc v av -> ematch (e#r <- v) (AE.set r av ae).

Fixpoint einit_regs (rl: list reg) : aenv :=
  match rl with
  | r1 :: rs => AE.set r1 (Ifptr Nonstack) (einit_regs rs)
  | nil => AE.top
  end.

Lemma ematch_init:
  forall rl vl,
  (forall v, In v vl -> vmatch bc v (Ifptr Nonstack)) ->
  ematch (init_regs vl rl) (einit_regs rl).

Fixpoint eforget (rl: list reg) (ae: aenv) {struct rl} : aenv :=
  match rl with
  | nil => ae
  | r1 :: rs => eforget rs (AE.set r1 Vtop ae)
  end.

Lemma eforget_ge:
  forall rl ae, AE.ge (eforget rl ae) ae.

Lemma ematch_forget:
  forall e rl ae, ematch e ae -> ematch e (eforget rl ae).

End MATCHENV.

Lemma ematch_incr:
  forall bc bc' e ae, ematch bc e ae -> bc_incr bc bc' -> ematch bc' e ae.

Lattice for dataflow analysis

Module VA <: SEMILATTICE.

  Inductive t' := Bot | State (ae: aenv) (am: amem).
  Definition t := t'.

  Definition eq (x y: t) :=
    match x, y with
    | Bot, Bot => True
    | State ae1 am1, State ae2 am2 =>
        AE.eq ae1 ae2 /\ forall bc m, mmatch bc m am1 <-> mmatch bc m am2
    | _, _ => False
    end.

  Lemma eq_refl: forall x, eq x x.
  Lemma eq_sym: forall x y, eq x y -> eq y x.
  Lemma eq_trans: forall x y z, eq x y -> eq y z -> eq x z.

  Definition beq (x y: t) : bool :=
    match x, y with
    | Bot, Bot => true
    | State ae1 am1, State ae2 am2 => AE.beq ae1 ae2 && mbeq am1 am2
    | _, _ => false
    end.

  Lemma beq_correct: forall x y, beq x y = true -> eq x y.

  Definition ge (x y: t) : Prop :=
    match x, y with
    | _, Bot => True
    | Bot, _ => False
    | State ae1 am1, State ae2 am2 => AE.ge ae1 ae2 /\ forall bc m, mmatch bc m am2 -> mmatch bc m am1
    end.

  Lemma ge_refl: forall x y, eq x y -> ge x y.
  Lemma ge_trans: forall x y z, ge x y -> ge y z -> ge x z.

  Definition bot : t := Bot.
  Lemma ge_bot: forall x, ge x bot.

  Definition lub (x y: t) : t :=
    match x, y with
    | Bot, _ => y
    | _, Bot => x
    | State ae1 am1, State ae2 am2 => State (AE.lub ae1 ae2) (mlub am1 am2)
    end.

  Lemma ge_lub_left: forall x y, ge (lub x y) x.
  Lemma ge_lub_right: forall x y, ge (lub x y) y.

End VA.

Hint Constructors cmatch : va.
Hint Constructors pmatch: va.
Hint Constructors vmatch: va.
Hint Resolve cnot_sound symbol_address_sound
       shl_sound shru_sound shr_sound
       and_sound or_sound xor_sound notint_sound
       ror_sound rolm_sound
       neg_sound add_sound sub_sound
       mul_sound mulhs_sound mulhu_sound
       divs_sound divu_sound mods_sound modu_sound shrx_sound
       shll_sound shrl_sound shrlu_sound
       andl_sound orl_sound xorl_sound notl_sound roll_sound rorl_sound
       negl_sound addl_sound subl_sound
       mull_sound mullhs_sound mullhu_sound
       divls_sound divlu_sound modls_sound modlu_sound shrxl_sound
       offset_ptr_sound
       negf_sound absf_sound
       addf_sound subf_sound mulf_sound divf_sound
       negfs_sound absfs_sound
       addfs_sound subfs_sound mulfs_sound divfs_sound
       zero_ext_sound sign_ext_sound longofint_sound longofintu_sound
       singleoffloat_sound floatofsingle_sound
       intoffloat_sound intuoffloat_sound floatofint_sound floatofintu_sound
       intofsingle_sound intuofsingle_sound singleofint_sound singleofintu_sound
       longoffloat_sound longuoffloat_sound floatoflong_sound floatoflongu_sound
       longofsingle_sound longuofsingle_sound singleoflong_sound singleoflongu_sound
       longofwords_sound loword_sound hiword_sound
       cmpu_bool_sound cmp_bool_sound cmplu_bool_sound cmpl_bool_sound
       cmpf_bool_sound cmpfs_bool_sound
       maskzero_sound : va.