This file can be downloaded in Coq format (.v) via this link: kayrebt.v.

Library kayrebt

Require Import ZArith.
Require Import List.
Require Import Lists.ListSet.
Require Import ProofIrrelevance.

Section Kayrebt.

Syntax

Vars is the type of variables taken into account in our semantics while IgnoredVars is the type of the variables we ignore. Equality is decidable on the type of variables.
Variable Vars : Type.
Variable IgnoredVars : Type.
Hypothesis Vars_eq_dec : x y:Vars, {x = y}+{x y}.

pointer and addressable are properties on variables. It is always possible to decide whether a variable is a pointer or an integer and whether it is addressable (its address is taken in the program) or not.
Variable pointer : Vars Prop.
Variable addressable : Vars Prop.
Hypothesis Addressable_dec : x:Vars, {addressable x}+{¬ addressable x}.
Hypothesis Pointer_dec : x:Vars, {pointer x}+{¬ pointer x}.

OtherExprs is the type of expressions of unknown values. This actually includes all arithmetic operations.
Variable OtherExprs : Type.

Exprs is the type of expressions. Dereferenciation and address-taking operations are not represented as expressions but are distinguished below, in the definition of nodes.
Inductive Exprs : Type :=
| int (z:Z)
| var (v:Vars)
| other (o: OtherExprs)
.

We suppose there exists a points-to oracle ptoracle, able to decide for each pair (pointer,addressable variable) whether the pointer may point on the variable. We are provided with this oracle by the compiler.
Variable ptoracle :
   (x:Vars) (Hptr: pointer x) (a:Vars) (Haddr: addressable a), Prop.
Hypothesis pt_or_not_pt :
   p Hptr x Haddr, {ptoracle p Hptr x Haddr}+{¬ ptoracle p Hptr x Haddr}.

Helpful lemma to perform case analysis on variables.
Lemma may_point_to p Hptr x: { (Hx: addressable x), ptoracle p Hptr x Hx}+
  {¬ addressable x}+{ (Hx: addressable x), ¬ ptoracle p Hptr x Hx}.
Proof.
  destruct (Addressable_dec x) as [Haddr | Hnaddr].
  - destruct (pt_or_not_pt p Hptr x Haddr) as [Hpt | Hnpt].
    + left; left.
       Haddr.
      exact Hpt.
    + right.
      intros.
      assert (Haddr = Hx) by (apply proof_irrelevance); subst.
      exact Hnpt.
  - left; right.
    exact Hnaddr.
Qed.

Some pointers point to numeric variables while some others point to pointers. It is always possible to decide whether a pointer may point to numeric variables or pointers because this is part of the typing done by the compiler.
Definition pointers_to_pointers p Hptr : Prop :=
   q Haddr, ptoracle p Hptr q Haddr pointer q.
Definition pointers_to_non_pointers p Hptr : Prop :=
   q Haddr, ptoracle p Hptr q Haddr ¬ pointer q.
Hypothesis cannot_point_to_both :
   v Hptr, {pointers_to_pointers v Hptr}+{pointers_to_non_pointers v Hptr}.

Nodes is the type of all nodes in the control flow graph, i.e. the type of all possible GIMPLE instructions.
Inductive Nodes : Type :=
| assignZ_to_Varz (x:Vars) (Hnptr_x: ¬ pointer x) (e:Z)
| assignVarz_to_Varz (x:Vars) (Hnptr_x: ¬ pointer x) (e:Vars) (Hnptr_e: ¬ pointer e)
| assignPtr_to_Varz (x:Vars) (Hnptr_x: ¬ pointer x) (p:Vars) (Hptr_p: pointer p)
| assignOther_to_Varz (x:Vars) (Hnptr_x: ¬ pointer x) (e:OtherExprs)
| assignDeref_to_Varz (x:Vars) (Hnptr_x: ¬ pointer x) (e:Vars) (Hptr_e: pointer e) (He: pointers_to_non_pointers e Hptr_e)
| assignZ_to_Ptr (p:Vars) (Hptr_p: pointer p) (e:Z)
| assignVarz_to_Ptr (p:Vars) (Hptr_p: pointer p) (x:Vars) (Hnptr_x: ¬ pointer x)
| assignPtr_to_Ptr (p:Vars) (Hptr_p: pointer p) (q:Vars) (Hptr_q: pointer q) (Hconsistency: (v:Vars) (Haddr_v: addressable v), ptoracle q Hptr_q v Haddr_v ptoracle p Hptr_p v Haddr_v)
| assignDeref_to_Ptr (p:Vars) (Hptr_p: pointer p) (q:Vars) (Hptr_q: pointer q)
    (Hq: pointers_to_pointers q Hptr_q)
    (Hconsistency: v Haddr_v Hptr_v, ptoracle q Hptr_q v Haddr_v
      ( x Haddr_x, ptoracle v Hptr_v x Haddr_x ptoracle p Hptr_p x Haddr_x))
| assignAddr_to_Ptr (p:Vars) (Hptr_p: pointer p) (a:Vars)
    (Haddr_a: addressable a) (Hconsistency: ptoracle p Hptr_p a Haddr_a)
| assignOther_to_Ptr (p:Vars) (Hptr_p: pointer p) (e:OtherExprs)
| assign_to_IgnoredVar (w:IgnoredVars) (e:Exprs)
| memZ_to_Ptr (p:Vars) (Hptr_p: pointer p) (e:Z)
    (Hp: pointers_to_non_pointers p Hptr_p)
| memVarz_to_Ptr (p:Vars) (Hptr_p: pointer p) (x:Vars) (Hnptr_x: ¬ pointer x)
    (Hp: pointers_to_non_pointers p Hptr_p)
| memPtr_to_Ptr (p:Vars) (Hptr_p: pointer p) (q:Vars) (Hptr_q: pointer q)
    (Hp: pointers_to_pointers p Hptr_p)
    (Hconsistency: v Haddr_v Hptr_v, ptoracle p Hptr_p v Haddr_v
        ( x Haddr_x, ptoracle q Hptr_q x Haddr_x ptoracle v Hptr_v x Haddr_x))
| memOther_to_Ptr (p:Vars) (Hptr_p: pointer p) (e:OtherExprs)
| mem_to_IgnoredVar (w:IgnoredVars) (e:Exprs)
| phiZ_to_Varz (x:Vars) (Hnptr_x: ¬ pointer x) (Hnaddr_x: ¬ addressable x) (e:Z)
| phiVarz_to_Varz (x:Vars) (Hnptr_x: ¬ pointer x) (Hnaddr_x: ¬ addressable x)
    (e:Vars) (Hnptr_e: ¬ pointer e)
| phiOther_to_Varz (x:Vars) (Hnptr_x: ¬ pointer x) (Hnaddr_x: ¬ addressable x)
    (e:OtherExprs)
| phiPtr_to_Ptr (p:Vars) (Hptr_p: pointer p) (Hnaddr_p: ¬ addressable p)
    (e:Vars) (Hptr_e: pointer e)
    (Hconsistency: v Haddr_v, ptoracle e Hptr_e v Haddr_v
      ptoracle p Hptr_p v Haddr_v)
| phiAddr_to_Ptr (p:Vars) (Hptr_p: pointer p) (Hnaddr_p: ¬ addressable p)
    (y:Vars) (Haddr_y: addressable y)
    (Hconsistency: ptoracle p Hptr_p y Haddr_y)
| phiOther_to_Ptr (p:Vars) (Hptr_p: pointer p) (Hnaddr_p: ¬ addressable p)
    (e:OtherExprs)
| callVars (x:Vars)
| callOther (x:IgnoredVars)
| call
| join
.

Constraint is the type of the constraints about variables. Each edge is labelled by a constraint. Forced transitions are labelled by the special constraint true while conditional edges bear a predicate on the value of variables.
Inductive Ops : Type :=
| Eq
| Neq
| Leq
| Lt
| Geq
| Gt
.
Inductive Constraint : Type :=
| constraint1 (v:Vars) (o:Ops) (z:Z)
| constraint2 (v:Vars) (o:Ops) (v':Vars)
| true
.
Definition ConstraintSet : Type := set Constraint.

Equality is decidable on the type of constraints, because it is so on the type of variables.
Lemma Constraint_eq_dec : c c':Constraint, {c = c'}+{c c'}.
Proof.
  repeat decide equality; apply Vars_eq_dec.
Qed.

Abstract semantics

A pointer map is a refinement of the points-to oracle. It associates to each pointer either a variable, meaning that we know for sure that the pointer points to the variable, or the special value ptunknown meaning that the destination of the pointer cannot be statically known.
Inductive Target : Type :=
| ptvar (v:Vars) (Haddr: addressable v)
| ptunknown
.
Definition PointerMap : Type := (x:Vars) (Hptr: pointer x), Target.

A pointer map is said to be consistent if it does not contradict the points to oracle.
Definition PointerMap_is_consistent P : Prop :=
(x:Vars) (Hptr: pointer x) (v:Vars) (Haddr: addressable v),
   P x Hptr = ptvar v Haddr ptoracle x Hptr v Haddr.


An abstract configuration is a pair (ConstraintSet,PointerMap) equipped with the proof that the pointer map is consistent.
We define a few manipulation functions on abstract configurations.
reset removes from a constraint set all constraints about some variable.
reset_all_pt removes all constraints about variables to which a given pointer might point.
reset_addr removes all constraints about addressable variables.
update_with_existing_element and update_with_addr modify a pointer map to record the new value of a pointer.
update_with_top modifies a pointer map to record that the destination of some pointer is now unknown.
update_all_pt_with_top modifies a pointer map to record that the destination of all pointers which might be pointed to by a pointer is now unknown.
update_all_addr_with_top modifies a pointer map to record that the destination of all addressable pointers is now unknown.
All update functions also redo the consistency proof.
Fixpoint reset (C:ConstraintSet) (v:Vars) : ConstraintSet :=
  match C with
  | nilnil
  | c1 :: C1
      match c1 with
      | constraint1 v1 _ _
          match Vars_eq_dec v1 v with
          | left _reset C1 v
          | right _c1 :: (reset C1 v)
          end
      | constraint2 v1 _ v2
          match Vars_eq_dec v1 v with
          | left _reset C1 v
          | right _
              match Vars_eq_dec v2 v with
              | left _reset C1 v
              | right _c1 :: (reset C1 v)
              end
          end
      | truec1 :: (reset C1 v)
      end
  end.

Fixpoint reset_all_pt (C:ConstraintSet) (p:Vars) (Hptr: pointer p) : ConstraintSet:=
  match C with
  | nilnil
  | c1 :: C1
      match c1 with
      | constraint1 v1 _ _
        match (may_point_to p Hptr v1) with
        | inleft Hmaybematch Hmaybe with
                         | left _reset_all_pt C1 p Hptr
                         | right _c1 :: (reset_all_pt C1 p Hptr)
                         end
        | inright _c1 :: (reset_all_pt C1 p Hptr)
        end
      | constraint2 v1 _ v2
        match (may_point_to p Hptr v1) with
        | inleft Hmaybematch Hmaybe with
                         | left _reset_all_pt C1 p Hptr
                         | right _
                            match (may_point_to p Hptr v2) with
                            | inleft Hmaybematch Hmaybe with
                                          | left _reset_all_pt C1 p Hptr
                                          | right _c1 :: (reset_all_pt C1 p Hptr)
                                          end
                            | inright _c1 :: (reset_all_pt C1 p Hptr)
                            end
                        end
        | inright _match (may_point_to p Hptr v2) with
                     | inleft Hmaybematch Hmaybe with
                                      | left _reset_all_pt C1 p Hptr
                                      | right _c1 :: (reset_all_pt C1 p Hptr)
                                      end
                     | inright _c1 :: (reset_all_pt C1 p Hptr)
                     end
        end
      | truec1 :: (reset_all_pt C1 p Hptr)
      end
  end.

Fixpoint reset_addr (C:ConstraintSet) : ConstraintSet :=
  match C with
  | nilnil
  | c1 :: C1
      match c1 with
      | constraint1 v1 _ _
          match Addressable_dec v1 with
          | left _reset_addr C1
          | right _c1 :: (reset_addr C1)
          end
      | constraint2 v1 _ v2
          match Addressable_dec v1 with
          | left _reset_addr C1
          | right _
              match Addressable_dec v2 with
              | left _reset_addr C1
              | right _c1 :: (reset_addr C1)
              end
          end
      | truec1 :: (reset_addr C1)
      end
  end.

Definition update_with_existing_element (P:sig PointerMap_is_consistent)
  (p: Vars) (Hptr_p: pointer p) (e:Vars) (Hptr_e: pointer e)
  (Hconsistency: v Haddr_v (Hinner: ptoracle e Hptr_e v Haddr_v),
    ptoracle p Hptr_p v Haddr_v)
  : sig PointerMap_is_consistent.
destruct P as [P HPconsistent].
refine (exist PointerMap_is_consistent
  (fun p' Hptr_p'match Vars_eq_dec p p' with
                    | left _P e Hptr_e
                    | right _P p' Hptr_p'
                    end) _).
  unfold PointerMap_is_consistent.
  intros p' Hptr_p' v Haddr_v.
  destruct (Vars_eq_dec p p') as [H | H]; [subst p'|].
  - intro Hptvar.
    assert (Hptr_p = Hptr_p') by (apply proof_irrelevance); subst.
    apply Hconsistency.
    apply HPconsistent.
    exact Hptvar.
  - apply HPconsistent.
Defined.

Definition update_with_top (P:sig PointerMap_is_consistent)
  (p:Vars) (Hptr_p: pointer p)
  : sig PointerMap_is_consistent.
destruct P as [P HPconsistent].
refine (exist PointerMap_is_consistent
  (fun p' Hptr_p'match Vars_eq_dec p p' with
                    | left _ptunknown
                    | right _P p' Hptr_p'
                    end) _).
  unfold PointerMap_is_consistent.
  intros p' Hptr_p' v Haddr_v.
  destruct (Vars_eq_dec p p'); [subst p'|].
  - intro Himpossible.
    discriminate Himpossible.
  - apply HPconsistent.
Defined.

Definition update_all_pt_with_top (P:sig PointerMap_is_consistent)
  (p:Vars) (Hptr_p: pointer p)
  : sig PointerMap_is_consistent.
destruct P as [P HPconsistent].
refine (exist PointerMap_is_consistent
 (fun p' Hptr_p'match (may_point_to p Hptr_p p') with
                    | inleft Hmatchmatch Hmatch with
                                        | left _ptunknown
                                        | right _P p' Hptr_p'
                                        end
                    | inright _P p' Hptr_p'
                      end) _).
  unfold PointerMap_is_consistent.
  intros p' Hptr_p' v Haddr_v.
  destruct (may_point_to p Hptr_p p') as [Hp_p' | Hp_p'].
  - destruct Hp_p'.
    × intros.
      discriminate.
    × apply HPconsistent.
  - apply HPconsistent.
Defined.

Definition update_with_address (P:sig PointerMap_is_consistent)
  (p:Vars) (Hptr_p: pointer p) (y: Vars) (Haddr_y: addressable y)
  (Hconsistency: ptoracle p Hptr_p y Haddr_y)
  : sig PointerMap_is_consistent.
destruct P as [P HPconsistent].
refine (exist PointerMap_is_consistent
    (fun p' Hptr_p'match Vars_eq_dec p p' with
                      | left _ptvar y Haddr_y
                      | right _P p' Hptr_p'
                      end) _).
  unfold PointerMap_is_consistent.
  intros p' Hptr_p' v Haddr_v.
  destruct (Vars_eq_dec p p') as [H | H]; [subst p|].
  - intros Hy_eq_v.
    inversion Hy_eq_v; subst.
    assert (Hptr_p = Hptr_p') by (apply proof_irrelevance); subst.
    assert (Haddr_v = Haddr_y) by (apply proof_irrelevance); subst.
    exact Hconsistency.
  - apply HPconsistent.
Defined.

Definition update_all_addr_with_top (P:sig PointerMap_is_consistent) :
  sig PointerMap_is_consistent.
destruct P as [P HPconsistent].
refine (exist PointerMap_is_consistent
    (fun p' Hptr_p'match (Addressable_dec p') with
                       | left _ptunknown
                       | right _P p' Hptr_p'
                       end) _).
  unfold PointerMap_is_consistent in ×.
  intros p' Hptr_p' v Haddr_v.
  destruct (Addressable_dec p').
  - discriminate.
  - apply HPconsistent.
Defined.

The abstract semantics is defined as a relation AbstractSemantics between abstract configurations, labelled by a node and a constraint (born by the edge following the node in the current path).
Inductive AbstractSemantics : AbstractConfiguration Nodes Constraint AbstractConfiguration Prop :=
| asem_assignZ_to_Varz C P (x:Vars) (Hnptr_x: ¬pointer x) (z:Z) c:
  
    AbstractSemantics (C,P) (assignZ_to_Varz x Hnptr_x z) c
      (set_add Constraint_eq_dec (constraint1 x Eq z)
        (set_add Constraint_eq_dec c (reset C x)), P)
| asem_assignVarz_to_Varz C P (x:Vars) (Hnptr_x: ¬pointer x)
    (v:Vars) (Hnptr_v: ¬pointer v) c:
  
    AbstractSemantics (C,P) (assignVarz_to_Varz x Hnptr_x v Hnptr_v) c
      (set_add Constraint_eq_dec (constraint2 x Eq v)
        (set_add Constraint_eq_dec c (reset C x)), P)
| asem_assignPtr_to_Ptr C P (x:Vars) (Hptr_x: pointer x)
    (e:Vars) (Hptr_e: pointer e) c Hconsistency:
  
    AbstractSemantics (C,P) (assignPtr_to_Ptr x Hptr_x e Hptr_e Hconsistency) c
      (set_add Constraint_eq_dec (constraint2 x Eq e)
        (set_add Constraint_eq_dec c (reset C x)),
        (update_with_existing_element P x Hptr_x e Hptr_e Hconsistency))
| asem_assignAddr_to_Ptr C P (x:Vars) (Hptr_x: pointer x)
    (y:Vars) (Haddr_y: addressable y) c Hconsistency:
  
    AbstractSemantics (C,P) (assignAddr_to_Ptr x Hptr_x y Haddr_y Hconsistency) c
      (set_add Constraint_eq_dec c (reset C x),
        (update_with_address P x Hptr_x y Haddr_y Hconsistency))
| asem_assignDerefPtr_to_Varz C P
    (x:Vars) (Hnptr_x: ¬pointer x) (p:Vars) (Hptr_p: pointer p) c
    (v:Vars) (Haddr_v: addressable v)
    (Hp: (proj1_sig P) p Hptr_p = ptvar v Haddr_v) Hptp:
  
    AbstractSemantics (C,P) (assignDeref_to_Varz x Hnptr_x p Hptr_p Hptp) c
      (set_add Constraint_eq_dec (constraint2 x Eq v)
        (set_add Constraint_eq_dec c (reset C x)), P)
| asem_assignDerefUnknown_to_Varz C P
    (x:Vars) (Hnptr_x: ¬pointer x)
    (p:Vars) (Hptr_p: pointer p) c
    (Hp: (proj1_sig P) p Hptr_p = ptunknown) Horacle:
  
    AbstractSemantics (C,P) (assignDeref_to_Varz x Hnptr_x p Hptr_p Horacle) c
      (set_add Constraint_eq_dec c (reset C x), P)
| asem_assignDeref_to_Ptr C P (x:Vars) (Hptr_x: pointer x)
    (p:Vars) (Hptr_p: pointer p) c (v:Vars) (Haddr_v: addressable v)
    (Hp: (proj1_sig P) p Hptr_p = ptvar v Haddr_v)
    Hptp Hconsistency:
  
    AbstractSemantics (C,P) (assignDeref_to_Ptr x Hptr_x p Hptr_p Hptp Hconsistency) c
      (set_add Constraint_eq_dec (constraint2 x Eq v)
        (set_add Constraint_eq_dec c (reset C x)),
          (update_with_existing_element P x Hptr_x v
            (Hptp _ _ ((proj2_sig P) _ _ _ _ Hp))
            (Hconsistency _ _ _ ((proj2_sig P) _ _ _ _ Hp))))
| asem_assignOther_to_Varz C P (x:Vars) (Hnptr_x: ¬pointer x) (e:OtherExprs) c:
  
    AbstractSemantics (C,P) (assignOther_to_Varz x Hnptr_x e) c
      (set_add Constraint_eq_dec c (reset C x), P)
| asem_assignPtr_to_Varz C P (x:Vars) (Hnptr_x: ¬pointer x)
    (e:Vars) (Hptr_e: pointer e) c:
  
    AbstractSemantics (C,P) (assignPtr_to_Varz x Hnptr_x e Hptr_e) c
      (set_add Constraint_eq_dec c (reset C x), P)
| asem_assignDerefUnknown_to_Ptr C P (x:Vars) (Hptr_x: pointer x)
    (p:Vars) (Hptr_p: pointer p) c (Hp: (proj1_sig P) p Hptr_p = ptunknown)
    Hptp Hconsistency:
  
    AbstractSemantics (C,P)
      (assignDeref_to_Ptr x Hptr_x p Hptr_p Hptp Hconsistency) c
        (set_add Constraint_eq_dec c (reset C x),
          (update_with_top P x Hptr_x))
| asem_assignOther_to_Ptr C P (x:Vars) (Hptr_x: pointer x) (e:OtherExprs) c:
  
    AbstractSemantics (C,P) (assignOther_to_Ptr x Hptr_x e) c
      (set_add Constraint_eq_dec c (reset C x),
        (update_with_top P x Hptr_x))
| asem_assignZ_to_Ptr C P (x:Vars) (Hptr_x: pointer x) (e:Z) c:
  
    AbstractSemantics (C,P) (assignZ_to_Ptr x Hptr_x e) c
      (set_add Constraint_eq_dec c (reset C x),
        (update_with_top P x Hptr_x))
| asem_assignVarz_to_Ptr C P (x:Vars) (Hptr_x: pointer x)
    (e:Vars) (Hnptr_e: ¬pointer e) c:
  
    AbstractSemantics (C,P) (assignVarz_to_Ptr x Hptr_x e Hnptr_e) c
      (set_add Constraint_eq_dec c (reset C x),
        (update_with_top P x Hptr_x))
| asem_assign_to_IgnoredVar C P (x:IgnoredVars) (e:Exprs) c:
  
    AbstractSemantics (C,P) (assign_to_IgnoredVar x e) c (set_add Constraint_eq_dec c C,P)

| asem_memZ_to_Ptr C P (p:Vars) (Hptr_p: pointer p) (z:Z) c
    (v:Vars) (Haddr_v: addressable v)
    (Hptp: (proj1_sig P) p Hptr_p = ptvar v Haddr_v) Hnonpointers:
  
    AbstractSemantics (C,P) (memZ_to_Ptr p Hptr_p z Hnonpointers) c
        (set_add Constraint_eq_dec (constraint1 v Eq z)
          (set_add Constraint_eq_dec c (reset C v)), P)
| asem_memVarz_to_Ptr C P (p:Vars) (Hptr_p: pointer p)
    (e:Vars) (Hnptr_e: ¬ pointer e) c (v:Vars) (Haddr_v: addressable v)
    (Hptp: (proj1_sig P) p Hptr_p = ptvar v Haddr_v) Hnonpointers:
  
    AbstractSemantics (C,P) (memVarz_to_Ptr p Hptr_p e Hnptr_e Hnonpointers) c
        (set_add Constraint_eq_dec (constraint2 v Eq e)
          (set_add Constraint_eq_dec c (reset C v)), P)
| asem_memZ_to_Unknown C P (p:Vars) (Hptr_p: pointer p) (z:Z) c
    (Hptp: (proj1_sig P) p Hptr_p = ptunknown) Hnonpointers:
  
    AbstractSemantics (C,P) (memZ_to_Ptr p Hptr_p z Hnonpointers) c
        (set_add Constraint_eq_dec c (reset_all_pt C p Hptr_p), P)
| asem_memVarz_to_Unknown C P (p:Vars) (Hptr_p: pointer p)
    (e:Vars) (Hnptr_e: ¬ pointer e) c
    (Hptp: (proj1_sig P) p Hptr_p = ptunknown) Hnonpointers:
  
    AbstractSemantics (C,P) (memVarz_to_Ptr p Hptr_p e Hnptr_e Hnonpointers) c
      (set_add Constraint_eq_dec c (reset_all_pt C p Hptr_p), P)
| asem_memPtr_to_Ptr C P
    (p:Vars) (Hptr_p: pointer p) (e:Vars) (Hptr_e: pointer e) c
    (v:Vars) (Haddr_v: addressable v)
    (Hptp: (proj1_sig P) p Hptr_p = ptvar v Haddr_v)
    (Hpointers: pointers_to_pointers p Hptr_p) Hconsistency:
  
    AbstractSemantics (C,P)
    (memPtr_to_Ptr p Hptr_p e Hptr_e Hpointers Hconsistency) c
       (set_add Constraint_eq_dec (constraint2 v Eq e)
         (set_add Constraint_eq_dec c (reset C v)),
           (update_with_existing_element P
            v (Hpointers _ _ ((proj2_sig P) _ _ _ _ Hptp))
            e Hptr_e
            (Hconsistency _ _ _ ((proj2_sig P) _ _ _ _ Hptp))))
| asem_memPtr_to_Unknown C P (p:Vars) (Hptr_p: pointer p)
    (e:Vars) (Hptr_e: pointer e) c
    (Hptp: (proj1_sig P) p Hptr_p = ptunknown)
    (Hpointers: pointers_to_pointers p Hptr_p) Hconsistency:
  
    AbstractSemantics (C,P)
    (memPtr_to_Ptr p Hptr_p e Hptr_e Hpointers Hconsistency) c
       (set_add Constraint_eq_dec c (reset_all_pt C p Hptr_p),
         (update_all_pt_with_top P p Hptr_p))

| asem_memUnknownVarz_to_Ptr C P (p:Vars) (Hptr_p: pointer p)
  (e:OtherExprs) c
  (v:Vars) (Haddr_v: addressable v) (Hnptr_v: ¬pointer v)
  (Hptp: (proj1_sig P) p Hptr_p = ptvar v Haddr_v) :
  
    AbstractSemantics (C,P)
     (memOther_to_Ptr p Hptr_p e) c
        (set_add Constraint_eq_dec c (reset C v), P)
| asem_memUnknownVarz_to_Unknown C P (p:Vars) (Hptr_p: pointer p)
  (e:OtherExprs) c
  (Hptp: (proj1_sig P) p Hptr_p = ptunknown)
  (Hpointers: pointers_to_non_pointers p Hptr_p) :
  
    AbstractSemantics (C,P)
      (memOther_to_Ptr p Hptr_p e) c
        (set_add Constraint_eq_dec c (reset_all_pt C p Hptr_p), P)

| asem_memUnknownPtr_to_Ptr C P (p:Vars) (Hptr_p: pointer p)
  (e:OtherExprs) c
  (q:Vars) (Haddr_q: addressable q) (Hptr_q: pointer q)
  (Hptp: (proj1_sig P) p Hptr_p = ptvar q Haddr_q) :
  
    AbstractSemantics (C,P)
      (memOther_to_Ptr p Hptr_p e) c
        (set_add Constraint_eq_dec c (reset C q),
         update_with_top P q Hptr_q)
| asem_memUnknownPtr_to_Unknown C P (p:Vars) (Hptr_p: pointer p)
  (e:OtherExprs) c
  (Hptp: (proj1_sig P) p Hptr_p = ptunknown) :
  
    AbstractSemantics (C,P)
      (memOther_to_Ptr p Hptr_p e) c
        (set_add Constraint_eq_dec c (reset_all_pt C p Hptr_p),
         update_all_pt_with_top P p Hptr_p)

| asem_mem_to_IgnoredVars C P (w:IgnoredVars) (e:Exprs) c :
  
    AbstractSemantics (C,P)
      (mem_to_IgnoredVar w e) c (set_add Constraint_eq_dec c C,P)

| asem_phiZ_to_Varz C P (x:Vars) (Hnptr_x: ¬pointer x) (Hnaddr_x: ¬addressable x)
    (z:Z) c:
  
    AbstractSemantics (C,P) (phiZ_to_Varz x Hnptr_x Hnaddr_x z) c
        (set_add Constraint_eq_dec (constraint1 x Eq z)
          (set_add Constraint_eq_dec c (reset C x)), P)
| asem_phiVarz_to_Varz C P
    (x:Vars) (Hnptr_x: ¬pointer x) (Hnaddr_x: ¬addressable x)
    (v:Vars) (Hnptr_v: ¬pointer v) c:
  
    AbstractSemantics (C,P) (phiVarz_to_Varz x Hnptr_x Hnaddr_x v Hnptr_v) c
        (set_add Constraint_eq_dec (constraint2 x Eq v)
          (set_add Constraint_eq_dec c (reset C x)), P)
| asem_phiOther_to_Varz C P
    (x:Vars) (Hnptr_x: ¬pointer x) (Hnaddr_x: ¬addressable x)
    (e:OtherExprs) c:
  
    AbstractSemantics (C,P) (phiOther_to_Varz x Hnptr_x Hnaddr_x e) c
        (set_add Constraint_eq_dec c (reset C x), P)
| asem_phiPtr_to_Ptr C P
    (p:Vars) (Hptr_p: pointer p) (Hnaddr_p : ¬addressable p)
    (v:Vars) (Hptr_v: pointer v) c Hconsistency:
  
    AbstractSemantics (C,P)
      (phiPtr_to_Ptr p Hptr_p Hnaddr_p v Hptr_v Hconsistency) c
        (set_add Constraint_eq_dec (constraint2 p Eq v)
          (set_add Constraint_eq_dec c (reset C p)),
          (update_with_existing_element P p Hptr_p v Hptr_v Hconsistency))
| asem_phiAddr_to_Ptr C P
    (p:Vars) (Hptr_p: pointer p) (Hnaddr_p: ¬ addressable p)
    (y:Vars) (Haddr_y: addressable y) c Hconsistency:
  
    AbstractSemantics (C,P)
      (phiAddr_to_Ptr p Hptr_p Hnaddr_p y Haddr_y Hconsistency) c
        (set_add Constraint_eq_dec c (reset C p),
          (update_with_address P p Hptr_p y Haddr_y Hconsistency))
| asem_phiOther_to_Ptr C P
    (p:Vars) (Hptr_p: pointer p) (Hnaddr_p: ¬addressable p)
    (e:OtherExprs) c:
  
    AbstractSemantics (C,P) (phiOther_to_Ptr p Hptr_p Hnaddr_p e) c
      (set_add Constraint_eq_dec c (reset C p),
        (update_with_top P p Hptr_p))

| asem_callVarz C P (x: Vars) (Hnptr_x: ¬pointer x) c:
   
    AbstractSemantics (C,P) (callVars x) c
      (set_add Constraint_eq_dec c (reset (reset_addr C) x),
        update_all_addr_with_top P)
| asem_callPtr C P (p: Vars) (Hptr_p: pointer p) c:
  
    AbstractSemantics (C,P) (callVars p) c
      (set_add Constraint_eq_dec c (reset (reset_addr C) p),
        update_all_addr_with_top (update_with_top P p Hptr_p))
| asem_callIgnoredVars C P (x:IgnoredVars) c:
  
    AbstractSemantics (C,P) (callOther x) c
      (set_add Constraint_eq_dec c (reset_addr C),
        update_all_addr_with_top P)
| asem_callNoVars C P c:
  
    AbstractSemantics (C,P) call c
      (set_add Constraint_eq_dec c (reset_addr C),
        update_all_addr_with_top P)
| asem_join C P c:
  
    AbstractSemantics (C,P) join c
        (set_add Constraint_eq_dec c C, P)
.

We want the abstract semantics to be defined for each kind of node.
Theorem abstract_semantics_is_left_total :
   C P n c, C' P', AbstractSemantics (C,P) n c (C',P').
Proof.
  intros.
  destruct n.
  - (set_add Constraint_eq_dec (constraint1 x Eq e) (set_add Constraint_eq_dec c (reset C x))).
     P.
    apply asem_assignZ_to_Varz.
  - (set_add Constraint_eq_dec (constraint2 x Eq e) (set_add Constraint_eq_dec c (reset C x))).
     P.
    apply asem_assignVarz_to_Varz.
  - (set_add Constraint_eq_dec c (reset C x)).
     P.
    apply asem_assignPtr_to_Varz.
  - (set_add Constraint_eq_dec c (reset C x)).
     P.
    apply asem_assignOther_to_Varz.
  - destruct ((proj1_sig P) e Hptr_e) eqn:HPe.
    + (set_add Constraint_eq_dec (constraint2 x Eq v) (set_add Constraint_eq_dec c (reset C x))).
       P.
      apply asem_assignDerefPtr_to_Varz with (Haddr_v:=Haddr).
      exact HPe.
    + (set_add Constraint_eq_dec c (reset C x)).
       P.
      apply asem_assignDerefUnknown_to_Varz.
      exact HPe.
  - (set_add Constraint_eq_dec c (reset C p)).
     (update_with_top P p Hptr_p).
    apply asem_assignZ_to_Ptr.
  - (set_add Constraint_eq_dec c (reset C p)).
     (update_with_top P p Hptr_p).
    apply asem_assignVarz_to_Ptr.
  - (set_add Constraint_eq_dec (constraint2 p Eq q) (set_add Constraint_eq_dec c (reset C p))).
     (update_with_existing_element P p Hptr_p q Hptr_q Hconsistency).
    apply asem_assignPtr_to_Ptr.
  - destruct ((proj1_sig P) q Hptr_q) eqn:HPe.
    + (set_add Constraint_eq_dec (constraint2 p Eq v) (set_add Constraint_eq_dec c (reset C p))).
      eexists (update_with_existing_element P p Hptr_p v _ _).
      eapply asem_assignDeref_to_Ptr.
    + (set_add Constraint_eq_dec c (reset C p)).
       (update_with_top P p Hptr_p).
      apply asem_assignDerefUnknown_to_Ptr.
      exact HPe.
  - (set_add Constraint_eq_dec c (reset C p)).
     (update_with_address P p Hptr_p a Haddr_a Hconsistency).
    apply asem_assignAddr_to_Ptr.
  - (set_add Constraint_eq_dec c (reset C p)).
     (update_with_top P p Hptr_p).
    apply asem_assignOther_to_Ptr.
  - (set_add Constraint_eq_dec c C).
     P.
    apply asem_assign_to_IgnoredVar.
  - destruct ((proj1_sig P) p Hptr_p) eqn:Hptp.
    + (set_add Constraint_eq_dec (constraint1 v Eq e)
          (set_add Constraint_eq_dec c (reset C v))).
       P.
      apply asem_memZ_to_Ptr with (Haddr_v:=Haddr).
      exact Hptp.
    + (set_add Constraint_eq_dec c (reset_all_pt C p Hptr_p)).
       P.
      apply asem_memZ_to_Unknown.
      exact Hptp.
  - destruct ((proj1_sig P) p Hptr_p) eqn:Hptp.
    + (set_add Constraint_eq_dec (constraint2 v Eq x)
          (set_add Constraint_eq_dec c (reset C v))).
       P.
      apply asem_memVarz_to_Ptr with (Haddr_v:=Haddr).
      exact Hptp.
    + (set_add Constraint_eq_dec c (reset_all_pt C p Hptr_p)).
       P.
      apply asem_memVarz_to_Unknown.
      exact Hptp.
  - destruct ((proj1_sig P) p Hptr_p) eqn:Hpt.
    + (set_add Constraint_eq_dec (constraint2 v Eq q) (set_add Constraint_eq_dec c (reset C v))).
      eexists (update_with_existing_element P v _ q Hptr_q _).
      apply asem_memPtr_to_Ptr.
    + (set_add Constraint_eq_dec c (reset_all_pt C p Hptr_p)).
       (update_all_pt_with_top P p Hptr_p).
      apply asem_memPtr_to_Unknown.
      exact Hpt.
  - destruct (cannot_point_to_both p Hptr_p) as [Hpointers | Hpointers];
    destruct ((proj1_sig P) p Hptr_p) eqn:Hpt.
    + (set_add Constraint_eq_dec c (reset C v)).
      eexists (update_with_top P v _).
      apply asem_memUnknownPtr_to_Ptr with (Haddr_q:=Haddr).
      exact Hpt.
    + (set_add Constraint_eq_dec c (reset_all_pt C p Hptr_p)).
       (update_all_pt_with_top P p Hptr_p).
      apply asem_memUnknownPtr_to_Unknown.
      exact Hpt.
    + (set_add Constraint_eq_dec c (reset C v)).
       P.
      apply asem_memUnknownVarz_to_Ptr with (Haddr_v:=Haddr).
      × apply (Hpointers v Haddr).
        apply (proj2_sig P).
        exact Hpt.
      × exact Hpt.
    + (set_add Constraint_eq_dec c (reset_all_pt C p Hptr_p)).
       P.
      apply asem_memUnknownVarz_to_Unknown.
      × exact Hpt.
      × exact Hpointers.
  - (set_add Constraint_eq_dec c C).
     P.
    apply asem_mem_to_IgnoredVars.
  - (set_add Constraint_eq_dec (constraint1 x Eq e)
              (set_add Constraint_eq_dec c (reset C x))).
     P.
    apply asem_phiZ_to_Varz.
  - (set_add Constraint_eq_dec (constraint2 x Eq e)
              (set_add Constraint_eq_dec c (reset C x))).
     P.
    apply asem_phiVarz_to_Varz.
  - (set_add Constraint_eq_dec c (reset C x)).
     P.
    apply asem_phiOther_to_Varz.
  - (set_add Constraint_eq_dec (constraint2 p Eq e)
              (set_add Constraint_eq_dec c (reset C p))).
     (update_with_existing_element P p Hptr_p e Hptr_e Hconsistency).
    apply asem_phiPtr_to_Ptr.
  - (set_add Constraint_eq_dec c (reset C p)).
     (update_with_address P p Hptr_p y Haddr_y Hconsistency).
    apply asem_phiAddr_to_Ptr.
  - (set_add Constraint_eq_dec c (reset C p)).
     (update_with_top P p Hptr_p).
    apply asem_phiOther_to_Ptr.
  - (set_add Constraint_eq_dec c (reset (reset_addr C) x)).
    destruct (Pointer_dec x) as [Hp_ptr | Hp_nptr].
    + (update_all_addr_with_top (update_with_top P x Hp_ptr)).
      apply asem_callPtr.
    + (update_all_addr_with_top P).
      apply asem_callVarz.
      exact Hp_nptr.
  - (set_add Constraint_eq_dec c (reset_addr C)).
     (update_all_addr_with_top P).
    apply asem_callIgnoredVars.
  - (set_add Constraint_eq_dec c (reset_addr C)).
     (update_all_addr_with_top P).
    apply asem_callNoVars.
  - (set_add Constraint_eq_dec c C).
     P.
    apply asem_join.

  Unshelve.   + exact Haddr.
  + exact HPe.
  + exact Haddr.
  + exact Hpt.
  + apply (Hpointers v Haddr).
    apply ((proj2_sig P) p).
    exact Hpt.
Qed.

Concrete semantics

MemoryLocation is the type of "addresses", we consider that each variable lives in its own, independent, location in memory and that it is not possible for two variables to live at the same place. The memory location of a variable never changed and can be known with function alpha.
Variable MemoryLocation : Type.
Hypothesis MemoryLocation_eq_dec : l l':MemoryLocation, {l = l'}+{l l'}.
Variable alpha : (v:Vars) (Haddr_v: addressable v), MemoryLocation.
Hypothesis location_is_unique : x Haddr_x y Haddr_y,
  alpha x Haddr_x = alpha y Haddr_y x = y.

The value of a variable depends on whether it is a pointer or a numeric variable, and whether it is addressable or not.
GammaZ is the function giving its value to all non addressable numeric variables.
GammaLoc gives the value of all non addressable pointers.
SigmaZ gives the memory location of all addressable numeric variables.
SigmaLoc gives the location of all addressable pointers.
Definition GammaZ : Type := (v:Vars) (Haddr_v: ¬addressable v), Z.
Definition GammaLoc : Type := (v:Vars) (Haddr_v: ¬addressable v), MemoryLocation.
Definition SigmaZ : Type := (l:MemoryLocation), Z.
Definition SigmaLoc : Type := (l:MemoryLocation), MemoryLocation.

MemoryState is the type of all concrete configurations, composed of an item of each function above. gz,sz,gloc and sloc are used to access the individual components of the concrete configuration. update_gz, update_gloc, update_sz and update_sloc make a new configuration by modifying one mapping in the corresponding component.
Definition MemoryState : Type := (GammaZ × SigmaZ × GammaLoc × SigmaLoc)%type.
Definition gz (m:MemoryState) : GammaZ := fst (fst (fst m)).
Definition sz (m:MemoryState) : SigmaZ := snd (fst (fst m)).
Definition gloc (m:MemoryState) : GammaLoc := snd (fst m).
Definition sloc (m:MemoryState) : SigmaLoc := snd m.

Definition update_gz (theta:MemoryState)
  (x:Vars) (Hnptr_x: ¬pointer x) (Hnaddr_x: ¬addressable x)
  (z:Z) : MemoryState :=
  (fun y Hnaddr_ymatch Vars_eq_dec x y with
                    | left _z
                    | right _gz theta y Hnaddr_y
                    end, sz theta, gloc theta, sloc theta).

Definition update_gloc (theta:MemoryState)
  (x: Vars) (Hptr_x: pointer x) (Hnaddr_x: ¬addressable x)
  (l:MemoryLocation) : MemoryState :=
  (gz theta, sz theta,
   fun y Hnaddr_ymatch Vars_eq_dec x y with
                     | left _l
                     | right _gloc theta y Hnaddr_y
                     end, sloc theta).

Definition update_sz (theta:MemoryState) (l:MemoryLocation)
  (z:Z) : MemoryState :=
  (gz theta,
  fun l'match MemoryLocation_eq_dec l l' with
            | left _z
            | right _sz theta l'
            end, gloc theta, sloc theta).

Definition update_sloc (theta:MemoryState) (l val:MemoryLocation) :
  MemoryState :=
  (gz theta, sz theta, gloc theta,
  fun l'match MemoryLocation_eq_dec l l' with
            | left _val
            | right _sloc theta l'
            end).

Function Valuation yields the value of any variable for any concrete configuration. It does no more than querying the appropriate function in the configuration. ValuationZ and ValuationLoc are other avatars of the same function provided for typing purposes.
Definition Valuation (theta:MemoryState) (v:Vars) : Z + MemoryLocation.
destruct (Addressable_dec v).
- destruct (Pointer_dec v).
  + exact (inr (sloc theta (alpha v a))).
  + exact (inl (sz theta (alpha v a))).
- destruct (Pointer_dec v).
  + exact (inr (gloc theta v n)).
  + exact (inl (gz theta v n)).
Defined.

Definition ValuationZ (theta:MemoryState) (v:Vars) (Hptr_v: ¬pointer v) : Z.
refine ((match (Valuation theta v) as val
        return (Valuation theta v = val) Z with
        | inl zfun Heqz
        | inr afun Heq_
        end) (eq_refl (Valuation theta v))).
        compute in Heq.
        destruct (Addressable_dec v); destruct (Pointer_dec v); subst; simpl; congruence.
Defined.

Definition ValuationLoc (theta:MemoryState) (p:Vars) (Hptr_p: pointer p) : MemoryLocation.
refine ((match (Valuation theta p) as val
        return (Valuation theta p = val) MemoryLocation with
        | inl zfun Heq_
        | inr afun Heqa
        end) (eq_refl (Valuation theta p))).
        compute in Heq.
        destruct (Addressable_dec p); destruct (Pointer_dec p); subst; simpl; congruence.
Defined.

We suppose that concrete configurations are consistent, i.e. that the points-to oracle is conservative. This must be true otherwise many optimizations would make the compiler miscompiles.
Hypothesis Valuation_is_consistent :
   (theta:MemoryState) (p:Vars) (Hptr_p: pointer p)
    (y:Vars) (Haddr_y: addressable y),
  Valuation theta p = inr (alpha y Haddr_y) ptoracle p Hptr_p y Haddr_y.

Open Scope Z_scope.

A concrete configuration satisfies a constraint if the valuation of the involved variables verifies the predicate expressed by the constraint.
Inductive satisfiability : MemoryState Constraint Prop :=
| satisfy_true theta:
  
    satisfiability theta true
| satisfy_constraint_Eq_Z theta x k (Hval: Valuation theta x = inl k):
  
    satisfiability theta (constraint1 x Eq k)
| satisfy_constraint_Neq_Z theta x k1 k2 (Hval: Valuation theta x = inl k2)
    (Hneq: k1 k2):
  
    satisfiability theta (constraint1 x Neq k2)
| satisfy_constraint_Leq_Z theta x k1 k2 (Hval: Valuation theta x = inl k2)
    (Hneq: k1 k2):
  
    satisfiability theta (constraint1 x Leq k2)
| satisfy_constraint_Lt_Z theta x k1 k2 (Hval: Valuation theta x = inl k2)
    (Hneq: k1 < k2):
  
    satisfiability theta (constraint1 x Lt k2)
| satisfy_constraint_Geq_Z theta x k1 k2 (Hval: Valuation theta x = inl k2)
    (Hneq: k1 k2):
  
    satisfiability theta (constraint1 x Geq k2)
| satisfy_constraint_Gt_Z theta x k1 k2 (Hval: Valuation theta x = inl k2)
    (Hneq: k1 > k2):
  
    satisfiability theta (constraint1 x Gt k2)
| satisfy_constraint_Eq_Var theta x y
    (Hval: Valuation theta x = Valuation theta y):
  
    satisfiability theta (constraint2 x Eq y)
| satisfy_constraint_Neq_Var theta x y k1 k2
    (Hvalx: Valuation theta x = inl k1) (Hvaly: Valuation theta y = inl k2)
    (Hneq: k1 k2):
  
    satisfiability theta (constraint2 x Neq y)
| satisfy_constraint_Leq_Var theta x y k1 k2
    (Hvalx: Valuation theta x = inl k1) (Hvaly: Valuation theta y = inl k2)
    (Hneq: k1 k2):
  
    satisfiability theta (constraint2 x Leq y)
| satisfy_constraint_Lt_Var theta x y k1 k2
    (Hvalx: Valuation theta x = inl k1) (Hvaly: Valuation theta y = inl k2)
    (Hneq: k1 < k2):
  
    satisfiability theta (constraint2 x Lt y)
| satisfy_constraint_Geq_Var theta x y k1 k2
    (Hvalx: Valuation theta x = inl k1) (Hvaly: Valuation theta y = inl k2)
    (Hneq: k1 k2):
  
    satisfiability theta (constraint2 x Geq y)
| satisfy_constraint_Gt_Var theta x y k1 k2
    (Hvalx: Valuation theta x = inl k1) (Hvaly: Valuation theta y = inl k2)
    (Hneq: k1 > k2):
  
    satisfiability theta (constraint2 x Gt y)
.

For a concrete configuration to satisfy an abstract one, it must satisfy each constraint in its constraint set and also agree with the pointer map.
We suppose there exist a concrete semantics. First of all, ConcreteSemantics' is a function updating a concrete configuration by going through a node.
Then, the actual concrete semantics is a relation between concrete configurations, labelled by a node and a constraint. But, unlike the abstract semantics, the relation is not verified if the constraint is not satisfied by the updated configuration. This models the fact that an execution can take a conditional jump only if the condition is verified.
We cannot know for sure the semantics given by the compiler to the code but we can make hypothesis on it. For example, instruction "x = 3" modifies the memory state in such a way that variable x is equal to 3 afterwards.
Hypothesis csem_assignZ_addr :
   theta (x: Vars) (Hnptr_x: ¬pointer x) (Haddr_x: addressable x) z,
  ConcreteSemantics' theta (assignZ_to_Varz x Hnptr_x z) =
    update_sz theta (alpha x Haddr_x) z.

Hypothesis csem_assignZ_naddr :
   theta (x: Vars) (Hnptr_x: ¬pointer x) (Hnaddr_x: ¬addressable x) z,
  ConcreteSemantics' theta (assignZ_to_Varz x Hnptr_x z) =
    update_gz theta x Hnptr_x Hnaddr_x z.

Hypothesis csem_assignVarz_addr :
   theta (x: Vars) (Hnptr_x: ¬pointer x) (Haddr_x: addressable x)
    (e: Vars) (Hnptr_e: ¬pointer e),
  ConcreteSemantics' theta (assignVarz_to_Varz x Hnptr_x e Hnptr_e) =
   update_sz theta (alpha x Haddr_x) (ValuationZ theta e Hnptr_e).

Hypothesis csem_assignVarz_naddr :
   theta (x: Vars) (Hnptr_x: ¬pointer x) (Hnaddr_x: ¬addressable x)
    (e: Vars) (Hnptr_e: ¬pointer e),
  ConcreteSemantics' theta (assignVarz_to_Varz x Hnptr_x e Hnptr_e) =
    update_gz theta x Hnptr_x Hnaddr_x (ValuationZ theta e Hnptr_e).

Hypothesis csem_assignPtr_to_Varz :
   theta (x:Vars) (Hnptr_x: ¬pointer x) (e: Vars) (Hptr_e: pointer e),
   theta2,
  ConcreteSemantics' theta (assignPtr_to_Varz x Hnptr_x e Hptr_e) = theta2
  ( (y:Vars), x y Valuation theta y = Valuation theta2 y).

Hypothesis csem_assignOther_to_Varz :
   theta (x:Vars) (Hptr_x: ¬pointer x) (e: OtherExprs),
   theta2,
  ConcreteSemantics' theta (assignOther_to_Varz x Hptr_x e) = theta2
  ( (y:Vars), x y Valuation theta y = Valuation theta2 y).

Hypothesis csem_assignDeref_to_Varz_addr :
   theta (x:Vars) (Hnptr_x: ¬pointer x) (Haddr_x: addressable x)
    (e:Vars) (Hptr_e: pointer e)
    (He: pointers_to_non_pointers e Hptr_e),
  ConcreteSemantics' theta (assignDeref_to_Varz x Hnptr_x e Hptr_e He) =
    update_sz theta (alpha x Haddr_x) ((sz theta) (ValuationLoc theta e Hptr_e)).

Hypothesis csem_assignDeref_to_Varz_naddr :
   theta (x:Vars) (Hnptr_x: ¬pointer x) (Hnaddr_x: ¬addressable x)
    (e:Vars) (Hptr_e: pointer e)
    (He: pointers_to_non_pointers e Hptr_e),
  ConcreteSemantics' theta (assignDeref_to_Varz x Hnptr_x e Hptr_e He) =
    update_gz theta x Hnptr_x Hnaddr_x ((sz theta) (ValuationLoc theta e Hptr_e)).

Hypothesis csem_assignZ_to_Ptr :
   theta (x:Vars) (Hptr_x: pointer x) (z:Z),
   theta2,
  ConcreteSemantics' theta (assignZ_to_Ptr x Hptr_x z) = theta2
     (y:Vars), x y Valuation theta y = Valuation theta2 y.

Hypothesis csem_assignVarz_to_Ptr :
   theta (x:Vars) (Hptr_x: pointer x) (e:Vars) (Hnptr_e: ¬pointer e),
   theta2,
  ConcreteSemantics' theta (assignVarz_to_Ptr x Hptr_x e Hnptr_e) = theta2
     (y:Vars), x y Valuation theta y = Valuation theta2 y.

Hypothesis csem_assignPtr_to_Ptr_addr :
   theta (p:Vars) (Hptr_p: pointer p) (Haddr_p: addressable p)
    (q:Vars) (Hptr_q: pointer q) Hconsistency,
  ConcreteSemantics' theta (assignPtr_to_Ptr p Hptr_p q Hptr_q Hconsistency) =
    update_sloc theta (alpha p Haddr_p) (ValuationLoc theta q Hptr_q).

Hypothesis csem_assignPtr_to_Ptr_naddr :
   theta (p:Vars) (Hptr_p: pointer p) (Hnaddr_p: ¬addressable p)
    (q:Vars) (Hptr_q: pointer q) Hconsistency,
  ConcreteSemantics' theta (assignPtr_to_Ptr p Hptr_p q Hptr_q Hconsistency) =
    update_gloc theta p Hptr_p Hnaddr_p (ValuationLoc theta q Hptr_q).

Hypothesis csem_assignDeref_to_Ptr_addr :
   theta (p: Vars) (Hptr_p: pointer p) (Haddr_p: addressable p)
    (q:Vars) (Hptr_q: pointer q) Hpointers_q Hconsistency,
  ConcreteSemantics' theta (assignDeref_to_Ptr p Hptr_p q Hptr_q Hpointers_q Hconsistency) =
    update_sloc theta (alpha p Haddr_p) ((sloc theta) (ValuationLoc theta q Hptr_q)).

Hypothesis csem_assignDeref_to_Ptr_naddr :
   theta (p: Vars) (Hptr_p: pointer p) (Hnaddr_p: ¬addressable p)
    (q:Vars) (Hptr_q: pointer q) Hpointers_q Hconsistency,
  ConcreteSemantics' theta (assignDeref_to_Ptr p Hptr_p q Hptr_q Hpointers_q Hconsistency) =
    update_gloc theta p Hptr_p Hnaddr_p ((sloc theta) (ValuationLoc theta q Hptr_q)).

Hypothesis csem_assignAddr_to_Ptr_addr :
   theta (p:Vars) (Hptr_p: pointer p) (Haddr_p: addressable p)
    (a:Vars) (Haddr_a: addressable a) Hconsistency,
  ConcreteSemantics' theta (assignAddr_to_Ptr p Hptr_p a Haddr_a Hconsistency) =
    update_sloc theta (alpha p Haddr_p) (alpha a Haddr_a).

Hypothesis csem_assignAddr_to_Ptr_naddr :
   theta (p:Vars) (Hptr_p: pointer p) (Hnaddr_p: ¬addressable p)
    (a:Vars) (Haddr_a: addressable a) Hconsistency,
  ConcreteSemantics' theta (assignAddr_to_Ptr p Hptr_p a Haddr_a Hconsistency) =
    update_gloc theta p Hptr_p Hnaddr_p (alpha a Haddr_a).

Hypothesis csem_assignOther_to_Ptr :
   theta (p:Vars) (Hptr_p: pointer p) (e: OtherExprs),
   theta2,
  ConcreteSemantics' theta (assignOther_to_Ptr p Hptr_p e) = theta2
     y, p y Valuation theta y = Valuation theta2 y.

Hypothesis csem_assign_to_IgnoredVar :
   theta (w:IgnoredVars) (e:Exprs),
  ConcreteSemantics' theta (assign_to_IgnoredVar w e) = theta.

Hypothesis csem_memZ_to_Ptr :
   theta (p:Vars) (Hptr_p: pointer p) (e:Z) Hpointers_p,
  ConcreteSemantics' theta (memZ_to_Ptr p Hptr_p e Hpointers_p) =
    update_sz theta (ValuationLoc theta p Hptr_p) e.

Hypothesis csem_memVarz_to_Ptr :
   theta (p:Vars) (Hptr_p: pointer p) (e:Vars) (Hnptr_e: ¬pointer e)
   Hpointers_p,
  ConcreteSemantics' theta (memVarz_to_Ptr p Hptr_p e Hnptr_e Hpointers_p) =
    update_sz theta (ValuationLoc theta p Hptr_p) (ValuationZ theta e Hnptr_e).

Hypothesis csem_memPtr_to_Ptr :
   theta (p:Vars) (Hptr_p: pointer p) (q:Vars) (Hptr_q: pointer q)
    Hpointers_p Hconsistency,
  ConcreteSemantics' theta (memPtr_to_Ptr p Hptr_p q Hptr_q Hpointers_p Hconsistency) =
    update_sloc theta (ValuationLoc theta p Hptr_p) (ValuationLoc theta q Hptr_q).

Hypothesis csem_memOther_to_Ptr :
   theta (p:Vars) (Hptr_p: pointer p) (e:OtherExprs),
   theta2,
  ConcreteSemantics' theta (memOther_to_Ptr p Hptr_p e) = theta2
     (y:Vars),
    (¬ addressable y ( (Haddr_y: addressable y),
      alpha y Haddr_y ValuationLoc theta p Hptr_p))
        Valuation theta y = Valuation theta2 y.

Hypothesis csem_mem_to_IgnoredVar :
   theta (w:IgnoredVars) (e:Exprs),
  ConcreteSemantics' theta (mem_to_IgnoredVar w e) = theta.

Hypothesis csem_phiZ_naddr :
   theta (x: Vars) (Hnptr_x: ¬pointer x) (Hnaddr_x: ¬addressable x) z,
  ConcreteSemantics' theta (phiZ_to_Varz x Hnptr_x Hnaddr_x z) =
    update_gz theta x Hnptr_x Hnaddr_x z.

Hypothesis csem_phiVarz_naddr :
   theta (x: Vars) (Hnptr_x: ¬pointer x) (Hnaddr_x: ¬addressable x)
    (e: Vars) (Hnptr_e: ¬pointer e),
  ConcreteSemantics' theta (phiVarz_to_Varz x Hnptr_x Hnaddr_x e Hnptr_e) =
   update_gz theta x Hnptr_x Hnaddr_x (ValuationZ theta e Hnptr_e).

Hypothesis csem_phiOther_to_Varz :
   theta (x: Vars) (Hnptr_x: ¬pointer x) (Hnaddr_x: ¬addressable x)
    (e: OtherExprs),
   theta2,
  ConcreteSemantics' theta (phiOther_to_Varz x Hnptr_x Hnaddr_x e) = theta2
     (y:Vars), x y Valuation theta y = Valuation theta2 y.

Hypothesis csem_phiPtr_to_Ptr_naddr :
   theta (p: Vars) (Hptr_p: pointer p) (Hnaddr_p: ¬addressable p)
    (q:Vars) (Hptr_q: pointer q) Hconsistency,
  ConcreteSemantics' theta (phiPtr_to_Ptr p Hptr_p Hnaddr_p q Hptr_q Hconsistency) =
    update_gloc theta p Hptr_p Hnaddr_p (ValuationLoc theta q Hptr_q).

Hypothesis csem_phiAddr_to_Ptr_naddr :
   theta (p: Vars) (Hptr_p: pointer p) (Hnaddr_p: ¬addressable p)
    (a:Vars) (Haddr_a: addressable a) Hconsistency,
  ConcreteSemantics' theta (phiAddr_to_Ptr p Hptr_p Hnaddr_p a Haddr_a Hconsistency) =
    update_gloc theta p Hptr_p Hnaddr_p (alpha a Haddr_a).

Hypothesis csem_phiOther_to_Ptr :
   theta (p: Vars) (Hptr_p: pointer p) (Hnaddr_p: ¬addressable p)
    (e: OtherExprs),
   theta2,
  ConcreteSemantics' theta (phiOther_to_Ptr p Hptr_p Hnaddr_p e) = theta2
     y, p y Valuation theta y = Valuation theta2 y.

Hypothesis csem_callVars :
   theta (ret: Vars),
   theta2,
  ConcreteSemantics' theta (callVars ret) = theta2
     y (Hnaddr_y: ¬addressable y), y ret Valuation theta y = Valuation theta2 y.

Hypothesis csem_callOther :
   theta (ret: IgnoredVars),
   theta2,
  ConcreteSemantics' theta (callOther ret) = theta2
     y (Hnaddr_y: ¬addressable y), Valuation theta y = Valuation theta2 y.

Hypothesis csem_call :
   theta,
   theta2,
  ConcreteSemantics' theta call = theta2
     y (Hnaddr_y: ¬addressable y), Valuation theta y = Valuation theta2 y.

Hypothesis csem_join :
   theta,
  ConcreteSemantics' theta join = theta.

Satisfiability and soundness

Some straightforward and helpful lemmas.
Lemma reset_subset : C x c, set_In c (reset C x) set_In c C.
Proof.
  intros.
  unfold set_In in ×.
  induction C; auto.
  destruct (Constraint_eq_dec a c); try (left; assumption).
  right.
  apply IHC.
  unfold reset in H.
  destruct a.
  - destruct (Vars_eq_dec v x); subst.
    + exact H.
    + apply in_inv in H; destruct H; [contradiction | exact H].
  - destruct (Vars_eq_dec v x); subst.
    + exact H.
    + destruct (Vars_eq_dec v' x); subst.
      × exact H.
      × apply in_inv in H; destruct H; [contradiction | exact H].
  - apply in_inv in H; destruct H; [contradiction | exact H].
Qed.

Lemma reset_ind : C c x, {reset (c::C) x = reset C x}+{reset (c::C) x = c :: (reset C x)}.
Proof.
  intros.
  destruct c.
  - destruct (Vars_eq_dec v x); subst.
    + left.
      compute.
      destruct (Vars_eq_dec x x); [reflexivity | congruence].
    + right.
      compute.
      destruct (Vars_eq_dec v x); [congruence | reflexivity].
  - destruct (Vars_eq_dec v x); destruct (Vars_eq_dec v' x); subst.
    + left; compute; destruct (Vars_eq_dec x x); [reflexivity | congruence].
    + left; compute; destruct (Vars_eq_dec x x); [reflexivity | congruence].
    + left; compute; destruct (Vars_eq_dec v x); destruct (Vars_eq_dec x x); try reflexivity; try congruence.
    + right; compute; destruct (Vars_eq_dec v x); destruct (Vars_eq_dec v' x); try reflexivity; try congruence.
  - right.
    unfold reset.
    reflexivity.
Qed.

Lemma reset_subset_all_pt : C p Hptr_p c, set_In c (reset_all_pt C p Hptr_p) set_In c C.
Proof.
  intros.
  unfold set_In in ×.
  induction C; auto.
  destruct (Constraint_eq_dec a c); try (left; assumption).
  right.
  apply IHC.
  destruct a.
  - simpl in H.
    destruct (may_point_to p Hptr_p v) as [[Hpoints_to | Hnaddr_v] |Hnpoints_to]; subst.
    + exact H.
    + inversion H; congruence.
    + inversion H; congruence.
  - simpl in H.
    destruct (may_point_to p Hptr_p v) as [[Hpoints_to | Hnaddr_v] |Hnpoints_to]; subst.
    + exact H.
    + destruct (may_point_to p Hptr_p v') as [[Hpoints_to' | Hnaddr_v'] |Hnpoints_to']; subst.
      × exact H.
      × inversion H; congruence.
      × inversion H; congruence.
    + destruct (may_point_to p Hptr_p v') as [[Hpoints_to' | Hnaddr_v'] |Hnpoints_to']; subst.
      × exact H.
      × inversion H; congruence.
      × inversion H; congruence.
  - inversion H; congruence.
Qed.

Lemma reset_subset_addr : C c, set_In c (reset_addr C) set_In c C.
Proof.
  intros.
  unfold set_In in ×.
  induction C; auto.
  destruct (Constraint_eq_dec a c); try (left; assumption).
  right.
  apply IHC.
  destruct a.
  × simpl in H.
    destruct (Addressable_dec v) as [Haddr_v | Hnaddr_v].
    { assumption. }
    { inversion H; [congruence | assumption]. }
  × simpl in H.
    destruct (Addressable_dec v) as [Haddr_v | Hnaddr_v];
      destruct (Addressable_dec v') as [Haddr_v' | Hnaddr_v'].
    { assumption. }
    { assumption. }
    { assumption. }
    { inversion H; [congruence | assumption]. }
  × inversion H.
    { congruence. }
    { assumption. }
Qed.

Lemma a_cons_l_neq_l : {A} l (a:A), l a :: l.
Proof.
  intros A l a.
  assert (length l length (a::l)).
  - unfold length.
    apply n_Sn.
  - assert (Hlength: (l l':list A), l = l' length l = length l').
    + intros l1 l2 Hl1l2.
      rewrite Hl1l2.
      reflexivity.
    + red.
      intro Habsurd.
      apply Hlength in Habsurd.
      contradiction.
Qed.

Lemma x_not_In_reset_x_1 : C x o z, ¬ set_In (constraint1 x o z) (reset C x).
Proof.
  intros.
  unfold set_In.
  induction C.
  - auto.
  - destruct (reset_ind C a x).
    + rewrite e.
      apply IHC.
    + rewrite e.
      red.
      intro Habsurd.
      inversion Habsurd; subst.
      × inversion e as [Hreset].
        destruct (Vars_eq_dec x x) in Hreset; [|congruence].
        assert (reset C x constraint1 x o z :: reset C x) by
          (apply a_cons_l_neq_l); contradiction.
      × apply IHC.
        assumption.
Qed.

Lemma x_not_In_reset_x_2 : C x o v, ¬ set_In (constraint2 x o v) (reset C x).
Proof.
  intros.
  unfold set_In.
  induction C.
  - auto.
  - destruct (reset_ind C a x).
    + rewrite e.
      apply IHC.
    + rewrite e.
      red.
      intro Habsurd.
      inversion Habsurd as [ Heq | Hneq ].
      × inversion e as [ Hreset ]; subst.
        destruct (Vars_eq_dec x x); [|congruence].
        assert (reset C x constraint2 x o v :: reset C x) by (apply a_cons_l_neq_l).
        contradiction.
      × apply IHC; apply Hneq.
Qed.

Lemma x_not_In_reset_x_2' : C x o v, ¬ set_In (constraint2 v o x) (reset C x).
Proof.
  intros.
  unfold set_In.
  induction C.
  - auto.
  - destruct (reset_ind C a x).
    + rewrite e.
      apply IHC.
    + rewrite e.
      red.
      intro Habsurd.
      inversion Habsurd as [ Heq | Hneq ].
      × inversion e as [ Hreset ]; subst.
        destruct (Vars_eq_dec v x); subst.
        { assert (reset C x constraint2 x o x :: reset C x) by (apply a_cons_l_neq_l).
          contradiction. }
        { destruct (Vars_eq_dec x x); [|congruence].
          assert (reset C x constraint2 v o x :: reset C x) by (apply a_cons_l_neq_l).
          contradiction. }
      × apply IHC; apply Hneq.
Qed.

Some lemmas to express the fact that the satisfiability depends on no more than the valuation of the involved variables. If the valuation has not changed, then the satisfiability of the constraint has not changed either.
Lemma satisfiability_maintained : theta1 theta2 v o z,
  Valuation theta1 v = Valuation theta2 v
  satisfiability theta1 (constraint1 v o z)
  satisfiability theta2 (constraint1 v o z).
Proof.
  intros theta1 theta2 v o z Hval Hsatis_theta1.
  destruct o;
  inversion Hsatis_theta1; subst;
  [apply satisfy_constraint_Eq_Z |
   apply satisfy_constraint_Neq_Z with (k1:=k1); try assumption |
   apply satisfy_constraint_Leq_Z with (k1:=k1); try assumption |
   apply satisfy_constraint_Lt_Z with (k1:=k1); try assumption |
   apply satisfy_constraint_Geq_Z with (k1:=k1); try assumption |
   apply satisfy_constraint_Gt_Z with (k1:=k1); try assumption ];
   rewrite <- Hval;
   assumption.
Qed.

Lemma satisfiability_maintained_2 : theta1 theta2 v o v',
  Valuation theta1 v = Valuation theta2 v
  Valuation theta1 v' = Valuation theta2 v'
  satisfiability theta1 (constraint2 v o v')
  satisfiability theta2 (constraint2 v o v').
Proof.
  intros theta1 theta2 v o v' Hval_theta1 Hval_theta2 Hsatis_theta1.
  destruct o;
  inversion Hsatis_theta1; subst.
  - apply satisfy_constraint_Eq_Var.
    congruence.
  - apply satisfy_constraint_Neq_Var with (k1:=k1) (k2:=k2); congruence.
  - apply satisfy_constraint_Leq_Var with (k1:=k1) (k2:=k2); congruence.
  - apply satisfy_constraint_Lt_Var with (k1:=k1) (k2:=k2); congruence.
  - apply satisfy_constraint_Geq_Var with (k1:=k1) (k2:=k2); congruence.
  - apply satisfy_constraint_Gt_Var with (k1:=k1) (k2:=k2); congruence.
Qed.

Lemma constraint_untouched: C theta1 theta2 x c',
  set_In c' (reset C x)
  ( c, set_In c C satisfiability theta1 c)
  ( y, y x Valuation theta1 y = Valuation theta2 y)
  satisfiability theta2 c'.
Proof.
  intros C theta1 theta2 x c' Hin Hsatis Hval.
  destruct c'.
  - destruct (Vars_eq_dec v x); subst.
    + assert (¬ set_In (constraint1 x o z) (reset C x)) by
            (apply x_not_In_reset_x_1).
      contradiction.
    + apply satisfiability_maintained with (theta1:=theta1) (theta2:=theta2).
      × auto.
      × apply Hsatis.
        apply reset_subset with (x:=x).
        apply Hin.
  - destruct (Vars_eq_dec v x); destruct (Vars_eq_dec v' x); subst.
    + assert (¬ set_In (constraint2 x o x) (reset C x)) by
            (apply x_not_In_reset_x_2).
      contradiction.
    + assert (¬ set_In (constraint2 x o v') (reset C x)) by
            (apply x_not_In_reset_x_2).
      contradiction.
    + assert (¬ set_In (constraint2 v o x) (reset C x)) by
            (apply x_not_In_reset_x_2').
      contradiction.
    + apply satisfiability_maintained_2 with (theta1:=theta1) (theta2:=theta2).
      × auto.
      × auto.
      × apply Hsatis.
        apply reset_subset with (x:=x).
        apply Hin.
  - apply satisfy_true.
Qed.

Lemma x_not_In_reset_x_1_all_pt : C x o z p Hptr_p Haddr_x, set_In (constraint1 x o z) (reset_all_pt C p Hptr_p) ¬ ptoracle p Hptr_p x Haddr_x.
Proof.
  induction C.
  - intros x o z p Hptr_p Haddr_x Hin; simpl in Hin.
    congruence.
  - intros x o z p Hptr_p Haddr_x Hin; simpl in Hin.
    destruct a.
    + destruct (may_point_to p Hptr_p v) as [[Hpoints_to | Hnaddr_v] | Hnpoints_to].
      × apply IHC with (o:=o) (z:=z).
        apply Hin.
      × inversion Hin.
        { inversion H; subst.
          congruence. }
        { apply IHC with (o:=o) (z:=z).
          apply H. }
      × inversion Hin.
        { inversion H; subst.
          apply Hnpoints_to. }
        { apply IHC with (o:=o) (z:=z).
          apply H. }
    + destruct (may_point_to p Hptr_p v) as [[Hpoints_to | Hnaddr_v] | Hnpoints_to].
      × apply IHC with (o:=o) (z:=z).
        apply Hin.
      × destruct (may_point_to p Hptr_p v') as [[Hpoints_to' | Hnaddr_v'] | Hnpoints_to'].
        { apply IHC with (o:=o) (z:=z).
          apply Hin. }
        { inversion Hin; [discriminate|].
          apply IHC with (o:=o) (z:=z).
          apply H. }
        { inversion Hin; [discriminate|].
          apply IHC with (o:=o) (z:=z).
          apply H. }
      × destruct (may_point_to p Hptr_p v') as [[Hpoints_to' | Hnaddr_v'] | Hnpoints_to'].
        { apply IHC with (o:=o) (z:=z).
          apply Hin. }
        { inversion Hin; [discriminate|].
          apply IHC with (o:=o) (z:=z).
          apply H. }
        { inversion Hin; [discriminate|].
          apply IHC with (o:=o) (z:=z).
          apply H. }
    + inversion Hin; [discriminate|].
      apply IHC with (o:=o) (z:=z).
      apply H.
Qed.

Lemma x_not_In_reset_x_2_all_pt : C v o v' p Hptr_p Haddr_v, set_In (constraint2 v o v') (reset_all_pt C p Hptr_p) ¬ ptoracle p Hptr_p v Haddr_v.
Proof.
  induction C.
  - intros v o v' p Hptr_p Haddr_v Hin; simpl in Hin.
    congruence.
  - intros v o v' p Hptr_p Haddr_v Hin; simpl in Hin.
    destruct a.
    + apply IHC with (o:=o) (v':=v').
      destruct (may_point_to p Hptr_p v0) as [[Hpoints_to' | Hnaddr_v'] | Hnpoints_to'].
      × exact Hin.
      × inversion Hin; [discriminate | assumption].
      × inversion Hin; [discriminate | assumption].
    + destruct (may_point_to p Hptr_p v0) as [[Hpoints_to' | Hnaddr_v'] | Hnpoints_to'].
      × exact (IHC _ _ _ _ _ _ Hin).
      × destruct (may_point_to p Hptr_p v'0) as [[Hpoints_to'' | Hnaddr_v''] | Hnpoints_to''].
        { exact (IHC _ _ _ _ _ _ Hin). }
        { inversion Hin; [subst | exact (IHC _ _ _ _ _ _ H)].
          inversion H; subst.
          congruence. }
        { inversion Hin; [subst | exact (IHC _ _ _ _ _ _ H)].
          inversion H; subst.
          congruence. }
      × destruct (may_point_to p Hptr_p v'0) as [[Hpoints_to'' | Hnaddr_v''] | Hnpoints_to''].
        { exact (IHC _ _ _ _ _ _ Hin). }
        { inversion Hin; [inversion H; subst | exact (IHC _ _ _ _ _ _ H)].
          exact (Hnpoints_to' Haddr_v). }
        { inversion Hin; [inversion H; subst | exact (IHC _ _ _ _ _ _ H)].
          exact (Hnpoints_to' Haddr_v). }
    + inversion Hin; [discriminate | exact (IHC _ _ _ _ _ _ H)].
Qed.

Lemma x_not_In_reset_x_2_all_pt' : C v o v' p Hptr_p Haddr_v', set_In (constraint2 v o v') (reset_all_pt C p Hptr_p) ¬ ptoracle p Hptr_p v' Haddr_v'.
Proof.
  induction C.
  - intros v o v' p Hptr_p Haddr_v Hin; simpl in Hin.
    congruence.
  - intros v o v' p Hptr_p Haddr_v Hin; simpl in Hin.
    destruct a.
    + apply IHC with (o:=o) (v:=v).
      destruct (may_point_to p Hptr_p v0) as [[Hpoints_to' | Hnaddr_v'] | Hnpoints_to'].
      × exact Hin.
      × inversion Hin; [discriminate | assumption].
      × inversion Hin; [discriminate | assumption].
    + destruct (may_point_to p Hptr_p v0) as [[Hpoints_to' | Hnaddr_v'] | Hnpoints_to'].
      × exact (IHC _ _ _ _ _ _ Hin).
      × destruct (may_point_to p Hptr_p v'0) as [[Hpoints_to'' | Hnaddr_v''] | Hnpoints_to''].
        { exact (IHC _ _ _ _ _ _ Hin). }
        { inversion Hin; [subst | exact (IHC _ _ _ _ _ _ H)].
          inversion H; subst.
          congruence. }
        { inversion Hin; [subst | exact (IHC _ _ _ _ _ _ H)].
          inversion H; subst.
          exact (Hnpoints_to'' Haddr_v). }
      × destruct (may_point_to p Hptr_p v'0) as [[Hpoints_to'' | Hnaddr_v''] | Hnpoints_to''].
        { exact (IHC _ _ _ _ _ _ Hin). }
        { inversion Hin; [inversion H; subst | exact (IHC _ _ _ _ _ _ H)].
          congruence. }
        { inversion Hin; [inversion H; subst | exact (IHC _ _ _ _ _ _ H)].
          exact (Hnpoints_to'' Haddr_v). }
    + inversion Hin; [discriminate | exact (IHC _ _ _ _ _ _ H)].
Qed.

Lemma constraint_untouched_all_pt: C theta1 theta2 p Hptr_p c',
  set_In c' (reset_all_pt C p Hptr_p)
  ( c, set_In c C satisfiability theta1 c)
  ( y, (( Haddr_y, ¬ ptoracle p Hptr_p y Haddr_y) ¬ addressable y) Valuation theta1 y = Valuation theta2 y)
  satisfiability theta2 c'.
Proof.
  intros C theta1 theta2 p Hptr_p c' Hin Hsatis Heq.
  destruct c'.
  - apply satisfiability_maintained with (theta1:=theta1) (theta2:=theta2).
    + apply Heq.
      destruct (Addressable_dec v) as [Haddr_v | Hnaddr_v].
      × left; Haddr_v.
        apply (x_not_In_reset_x_1_all_pt _ _ _ _ _ _ _ Hin).
      × right.
        assumption.
    + apply Hsatis.
      apply (reset_subset_all_pt _ _ _ _ Hin).
  - apply satisfiability_maintained_2 with (theta1:=theta1) (theta2:=theta2).
    + apply Heq.
      destruct (Addressable_dec v) as [Haddr_v | Hnaddr_v].
      × left; Haddr_v.
        apply (x_not_In_reset_x_2_all_pt _ _ _ _ _ _ _ Hin).
      × right; assumption.
    + apply Heq.
      destruct (Addressable_dec v') as [Haddr_v' | Hnaddr_v'].
      × left; Haddr_v'.
        apply (x_not_In_reset_x_2_all_pt' _ _ _ _ _ _ _ Hin).
      × right; assumption.
    + apply Hsatis.
      apply (reset_subset_all_pt _ _ _ _ Hin).
  - apply satisfy_true.
Qed.

Lemma pointer_dest_unchanged : P x Hptr_x p Hptr_p v Hnaddr_v,
  p x proj1_sig (update_with_top P x Hptr_x) p Hptr_p = ptvar v Hnaddr_v
  proj1_sig P p Hptr_p = ptvar v Hnaddr_v.
Proof.
  intros P x Hptr_x p Hptr_p v Hnaddr_v Hneq Hvar.
  rewrite <- Hvar.
  unfold update_with_top.
  destruct P as [P HP_consistent]; subst.
  simpl.
  destruct (Vars_eq_dec x p).
  - congruence.
  - reflexivity.
Qed.

Lemma previous_valuation: P x Hptr_x e Hptr_e v Hnaddr_v Hupdate,
  proj1_sig (update_with_existing_element P x Hptr_x e Hptr_e Hupdate) x Hptr_x =
    ptvar v Hnaddr_v
  proj1_sig P e Hptr_e = ptvar v Hnaddr_v.
Proof.
  intros.
  rewrite <- H.
  unfold update_with_existing_element.
  destruct P as [P HP]; subst.
  simpl.
  destruct (Vars_eq_dec x x); [| congruence].
  reflexivity.
Qed.

A new tactic to automate the proofs somewhat.
Ltac compute_val :=
    compute;
    repeat match goal with
      | [ H1:pointer ?x, H2:pointer ?x |- _ ] ⇒ (assert (H1=H2) by (apply proof_irrelevance); subst H2)
      | [ H1:¬pointer ?x, H2:¬pointer ?x |- _ ] ⇒ (assert (H1=H2) by (apply proof_irrelevance); subst H2)
      | [ H1:addressable ?x, H2:addressable ?x |- _ ] ⇒ (assert (H1=H2) by (apply proof_irrelevance); subst H2)
      | [ H1:¬addressable ?x, H2:¬addressable ?x |- _ ] ⇒ (assert (H1=H2) by (apply proof_irrelevance); subst H2)
      | [ H: alpha ?x _ = alpha ?y _ |- _ ] ⇒ (assert (x=y) by (apply (location_is_unique _ _ _ _ H)); clear H)
      | |- context[match ?x with | left __ | right __ end] ⇒ destruct x
      | |- context[match ?x with | __ end] ⇒ (let E := fresh "Eq" in destruct x eqn:E; try congruence)
    end; try congruence.

Big and reusable lemmas, helpful to clear some cases.
Lemma update_with_existing_element_preserves_satisfiability_gloc :
   (P: sig PointerMap_is_consistent) theta (x: Vars) (Hptr_x: pointer x) (Hnaddr_x: ¬addressable x)
    (e: Vars) (Hptr_e: pointer e) Hconsistency
    (Hptr: (p : Vars) (Hptr_p : pointer p) (v : Vars) (Haddr_v : addressable v),
  proj1_sig P p Hptr_p = ptvar v Haddr_v Valuation theta p = inr (alpha v Haddr_v)),
   (p : Vars) (Hptr_p : pointer p) (v : Vars) (Haddr_v : addressable v),
    proj1_sig (update_with_existing_element P x Hptr_x e Hptr_e Hconsistency) p Hptr_p = ptvar v Haddr_v
      Valuation (update_gloc theta x Hptr_x Hnaddr_x (ValuationLoc theta e Hptr_e)) p =
        inr (alpha v Haddr_v).
Proof.
  intros.
  assert (Hsame: p, p x Valuation (update_gloc theta x Hptr_x Hnaddr_x (ValuationLoc theta e Hptr_e)) p = Valuation theta p).
  { intros Hpx.
    compute_val. }
  assert (Hsame': Valuation (update_gloc theta x Hptr_x Hnaddr_x (ValuationLoc theta e Hptr_e)) x = Valuation theta e).
  { compute_val. }
  assert (Hpx: p x proj1_sig P p Hptr_p = proj1_sig (update_with_existing_element P x Hptr_x e Hptr_e Hconsistency) p Hptr_p).
  { compute_val. }
  assert (He: proj1_sig P e Hptr_e = proj1_sig (update_with_existing_element P x Hptr_x e Hptr_e Hconsistency) x Hptr_x).
  { compute_val. }
  destruct (Vars_eq_dec p x) as [Hp_eq_x | Hp_neq_x]; [subst p|].
  - rewrite Hsame'.
    apply Hptr with (Hptr_p:=Hptr_e).
    rewrite He.
    rewrite (proof_irrelevance _ Hptr_p Hptr_x) in H.
    apply H.
  - rewrite (Hsame p Hp_neq_x).
    apply Hptr with (Hptr_p:=Hptr_p).
    rewrite (Hpx Hp_neq_x).
    exact H.
Qed.

Lemma update_with_existing_element_preserves_satisfiability_sloc :
   (P: sig PointerMap_is_consistent) theta (x: Vars) (Hptr_x: pointer x) (Haddr_x: addressable x)
    (e: Vars) (Hptr_e: pointer e) Hconsistency
    (Hptr: (p : Vars) (Hptr_p : pointer p) (v : Vars) (Haddr_v : addressable v),
  proj1_sig P p Hptr_p = ptvar v Haddr_v Valuation theta p = inr (alpha v Haddr_v)),
   (p : Vars) (Hptr_p : pointer p) (v : Vars) (Haddr_v : addressable v),
    proj1_sig (update_with_existing_element P x Hptr_x e Hptr_e Hconsistency) p Hptr_p = ptvar v Haddr_v
      Valuation (update_sloc theta (alpha x Haddr_x) (ValuationLoc theta e Hptr_e)) p =
        inr (alpha v Haddr_v).
Proof.
  intros.
  assert (Hsame: p, p x Valuation (update_sloc theta (alpha x Haddr_x) (ValuationLoc theta e Hptr_e)) p = Valuation theta p).
  { intros Hpx.
    compute_val. }
  assert (Hsame': Valuation (update_sloc theta (alpha x Haddr_x) (ValuationLoc theta e Hptr_e)) x = Valuation theta e).
  { compute_val. }
  assert (Hpx: p x proj1_sig P p Hptr_p = proj1_sig (update_with_existing_element P x Hptr_x e Hptr_e Hconsistency) p Hptr_p).
  { compute_val. }
  assert (He: proj1_sig P e Hptr_e = proj1_sig (update_with_existing_element P x Hptr_x e Hptr_e Hconsistency) x Hptr_x).
  { compute_val. }
  destruct (Vars_eq_dec p x) as [Hp_eq_x | Hp_neq_x]; [subst p|].
  - rewrite Hsame'.
    apply Hptr with (Hptr_p:=Hptr_e).
    rewrite He.
    rewrite (proof_irrelevance _ Hptr_p Hptr_x) in H.
    apply H.
  - rewrite (Hsame p Hp_neq_x).
    apply Hptr with (Hptr_p:=Hptr_p).
    rewrite (Hpx Hp_neq_x).
    exact H.
Qed.

A rewriting lemma.
Lemma ValuationLoc_vs_Valuation :
   theta p Hptr a Haddr,
  ValuationLoc theta p Hptr = alpha a Haddr Valuation theta p = inr (alpha a Haddr).
Proof.
  split.
  - compute_val.
  - compute_val.
Qed.

Some inversion lemmas to help rule out impossible cases.
Lemma only_constraints_on_naddr :
   C v o z,
  set_In (constraint1 v o z) (reset_addr C) ¬ addressable v.
Proof.
  intros C v o z H.
  induction C.
  - simpl in H.
    elim H.
  - simpl in H.
    destruct a.
    + destruct (Addressable_dec v0); auto.
      inversion H; subst; try auto; try congruence.
    + destruct (Addressable_dec v0); destruct (Addressable_dec v'); auto.
      inversion H; subst; try auto; try congruence.
    + apply IHC; auto.
      inversion H; auto; discriminate.
Qed.

Lemma only_constraints_on_naddr' :
   C v o v',
  set_In (constraint2 v o v') (reset_addr C) ¬ addressable v ¬ addressable v'.
Proof.
  intros C v o v' H.
  induction C.
  - simpl in H.
    elim H.
  - simpl in H.
    destruct a.
    + destruct (Addressable_dec v0); auto.
      inversion H; subst; try auto; try congruence.
    + destruct (Addressable_dec v0); destruct (Addressable_dec v'0); auto.
      inversion H; subst; auto.
      inversion H0; subst; auto.
    + apply IHC; auto.
      inversion H; auto; discriminate.
Qed.

Lemma only_constraints_neq_x :
   C v o z x,
  set_In (constraint1 v o z) (reset C x) v x.
Proof.
  intros C v o z x Hin.
  induction C.
  - simpl in Hin.
    elim Hin.
  - simpl in Hin.
    destruct a.
    + destruct (Vars_eq_dec v0 x); auto.
      inversion Hin; auto.
      inversion H; subst; auto.
    + destruct (Vars_eq_dec v0 x); destruct (Vars_eq_dec v' x); auto.
      inversion Hin; auto.
      discriminate.
    + inversion Hin; auto.
      discriminate.
Qed.

Lemma only_constraints_neq_x' :
   C v o v' x,
  set_In (constraint2 v o v') (reset C x) v x v' x.
Proof.
  intros C v o v' x Hin.
  induction C.
  - simpl in Hin.
    elim Hin.
  - simpl in Hin.
    destruct a.
    + destruct (Vars_eq_dec v0 x); auto.
      inversion Hin; auto.
      discriminate.
    + destruct (Vars_eq_dec v0 x); destruct (Vars_eq_dec v'0 x); auto.
      inversion Hin; auto.
      inversion H; subst; auto.
    + inversion Hin; auto.
      discriminate.
Qed.

The base case of our soundness proposition. Here we prove that the abstract semantics is sound with respect with the concrete semantics by induction on the type of nodes.
Lemma restricted_soundness : (v:Nodes) (c:Constraint)
  (k k':AbstractConfiguration) (theta theta':MemoryState),
  (AbstractSemantics k v c k') (ConcreteSemantics theta v c theta')
  satisfiability_abstract_configuration theta k
  satisfiability_abstract_configuration theta' k'.
Proof.
  intros v c k k' theta theta' Habstract Hconc Hsatis.
  inversion Hconc; subst.
  inversion Hsatis as [Hval Hptr]; subst.
  unfold satisfiability_set_constraints in Hval.
  unfold satisfiability_pointer_map in Hptr.
  destruct k as [C P]; destruct k' as [C' P']; subst; simpl in ×.
  inversion Habstract;
    unfold satisfiability_abstract_configuration;
    unfold satisfiability_set_constraints;
    unfold satisfiability_pointer_map;
    simpl in *; subst.
  - split.
    + intros c1 Hin.
      apply set_add_elim in Hin; inversion Hin; subst.
      × apply satisfy_constraint_Eq_Z.
        destruct (Addressable_dec x) as [Haddr_x | Hnaddr_x].
        { rewrite csem_assignZ_addr with (Haddr_x:=Haddr_x).
          compute_val. }
        { rewrite csem_assignZ_naddr with (Hnaddr_x:=Hnaddr_x).
          compute_val. }
      × apply set_add_elim in H; inversion H; subst.
        { exact Hsatis_c. }
        { apply constraint_untouched with (C:=C) (theta1:=theta) (x:=x); auto.
          destruct (Addressable_dec x) as [Haddr | Hnaddr].
          - rewrite csem_assignZ_addr with (Haddr_x:=Haddr).
            intros y Hxy.
            compute_val.
          - rewrite csem_assignZ_naddr with (Hnaddr_x:=Hnaddr).
            intros y Hxy.
            compute_val. }
    + intros.
      destruct (Addressable_dec x) as [Haddr_x | Hnaddr_x].
      × rewrite csem_assignZ_addr with (Haddr_x:=Haddr_x).
        assert (Hsame: Valuation (update_sz theta (alpha x Haddr_x) z) p = Valuation theta p) by compute_val.
        rewrite Hsame.
        exact (Hptr p Hptr_p v Haddr_v Hptv).
      × rewrite csem_assignZ_naddr with (Hnaddr_x:=Hnaddr_x).
        assert (Hsame: Valuation (update_gz theta x Hnptr_x Hnaddr_x z) p = Valuation theta p) by compute_val.
        rewrite Hsame.
        exact (Hptr p Hptr_p v Haddr_v Hptv).

  - split.
    + intros c1 Hin.
      apply set_add_elim in Hin; inversion Hin; subst.
      × apply satisfy_constraint_Eq_Var.
        destruct (Addressable_dec x) as [Haddr_x | Hnaddr_x]; destruct (Addressable_dec v0) as [Haddr_v | Hnaddr_v].
        { rewrite csem_assignVarz_addr with (Haddr_x:=Haddr_x).
          compute_val. }
        { rewrite csem_assignVarz_addr with (Haddr_x:=Haddr_x).
          compute_val. }
        { rewrite csem_assignVarz_naddr with (Hnaddr_x:=Hnaddr_x).
          compute_val. }
        { rewrite csem_assignVarz_naddr with (Hnaddr_x:=Hnaddr_x).
          compute_val. }
      × apply set_add_elim in H; inversion H; subst.
        { exact Hsatis_c. }
        { apply constraint_untouched with (C:=C) (theta1:=theta) (x:=x); auto.
          destruct (Addressable_dec x) as [Haddr | Hnaddr].
          - rewrite csem_assignVarz_addr with (Haddr_x:=Haddr).
            intros y Hxy.
            compute_val.
          - rewrite csem_assignVarz_naddr with (Hnaddr_x:=Hnaddr).
            intros y Hxy.
            compute_val. }
    + intros.
      destruct (Addressable_dec x) as [Haddr_x | Hnaddr_x].
      × rewrite csem_assignVarz_addr with (Haddr_x:=Haddr_x).
        assert (Hsame: Valuation (update_sz theta (alpha x Haddr_x) (ValuationZ theta v0 Hnptr_v)) p = Valuation theta p) by compute_val.
        rewrite Hsame.
        exact (Hptr p Hptr_p v Haddr_v Hptv).
      × rewrite csem_assignVarz_naddr with (Hnaddr_x:=Hnaddr_x).
        assert (Hsame: Valuation (update_gz theta x Hnptr_x Hnaddr_x (ValuationZ theta v0 Hnptr_v)) p = Valuation theta p) by compute_val.
        rewrite Hsame.
        exact (Hptr p Hptr_p v Haddr_v Hptv).

  - split.
    + intros c1 Hin.
      apply set_add_elim in Hin; inversion Hin; subst.
      × apply satisfy_constraint_Eq_Var.
        destruct (Addressable_dec x) as [Haddr_x | Hnaddr_x]; destruct (Addressable_dec e) as [Haddr_e | Hnaddr_e].
        { rewrite csem_assignPtr_to_Ptr_addr with (Haddr_p:=Haddr_x) ; compute_val. }
        { rewrite csem_assignPtr_to_Ptr_addr with (Haddr_p:=Haddr_x); compute_val. }
        { rewrite csem_assignPtr_to_Ptr_naddr with (Hnaddr_p:=Hnaddr_x); compute_val. }
        { rewrite csem_assignPtr_to_Ptr_naddr with (Hnaddr_p:=Hnaddr_x); compute_val. }
     × apply set_add_elim in H; inversion H; subst.
        { exact Hsatis_c. }
        { apply constraint_untouched with (C:=C) (theta1:=theta) (x:=x); auto.
          destruct (Addressable_dec x) as [Haddr | Hnaddr].
          - rewrite csem_assignPtr_to_Ptr_addr with (Haddr_p:=Haddr).
            intros y Hxy.
            compute_val.
          - rewrite csem_assignPtr_to_Ptr_naddr with (Hnaddr_p:=Hnaddr).
            intros y Hxy.
            compute_val. }
    + intros.
      destruct (Addressable_dec x) as [Haddr_x | Hnaddr_x].
      × rewrite csem_assignPtr_to_Ptr_addr with (Haddr_p:=Haddr_x).
        eapply update_with_existing_element_preserves_satisfiability_sloc; [exact Hptr | exact Hptv].
      × rewrite csem_assignPtr_to_Ptr_naddr with (Hnaddr_p:=Hnaddr_x).
        eapply update_with_existing_element_preserves_satisfiability_gloc; [exact Hptr | exact Hptv].

  - split.
    + intros c1 Hin.
      apply set_add_elim in Hin; inversion Hin; subst.
      × exact Hsatis_c.
      × apply constraint_untouched with (C:=C) (theta1:=theta) (x:=x); auto.
        intros y' Hy'.
        destruct (Addressable_dec x) as [Haddr_x | Hnaddr_x].
        { rewrite csem_assignAddr_to_Ptr_addr with (Haddr_p:=Haddr_x).
          compute_val. }
        { rewrite csem_assignAddr_to_Ptr_naddr with (Hnaddr_p:=Hnaddr_x).
          compute_val. }
    + intros p Hptr_p v Haddr_v H.
      destruct (Addressable_dec x) as [Haddr_x | Hnaddr_x].
      × rewrite csem_assignAddr_to_Ptr_addr with (Haddr_p:=Haddr_x).
        assert (Hpx: p x Valuation (update_sloc theta (alpha x Haddr_x) (alpha y Haddr_y)) p = Valuation theta p)
          by compute_val.
        destruct (Vars_eq_dec p x) as [Hp_eq_x | Hp_neq_x] ; [subst p|].
        { compute_val.
          assert (proj1_sig (update_with_address P x Hptr_x y Haddr_y Hconsistency) x Hptr_x = ptvar y Haddr_y).
          - unfold update_with_address.
            destruct P as [P HP].
            simpl.
            destruct (Vars_eq_dec x x); [reflexivity | congruence].
          - assert (Hequal: ptvar v Haddr_v = ptvar y Haddr_y) by congruence.
            inversion Hequal; subst y.
            rewrite (proof_irrelevance _ Haddr_y Haddr_v).
            reflexivity. }
        { rewrite (Hpx Hp_neq_x).
          apply Hptr with (Hptr_p:=Hptr_p).
          assert (Hnot_changed: proj1_sig (update_with_address P x Hptr_x y Haddr_y Hconsistency) p Hptr_p = proj1_sig P p Hptr_p).
          - unfold update_with_address.
            destruct P as [P HP].
            simpl.
            destruct (Vars_eq_dec x p); [congruence | reflexivity].
          - rewrite <- Hnot_changed.
            assumption. }
      × rewrite csem_assignAddr_to_Ptr_naddr with (Hnaddr_p:=Hnaddr_x).
        assert (Hpx: p x Valuation (update_gloc theta x Hptr_x Hnaddr_x (alpha y Haddr_y)) p = Valuation theta p)
          by compute_val.
        destruct (Vars_eq_dec p x) as [Hp_eq_x | Hp_neq_x] ; [subst p|].
        { compute_val.
          assert (proj1_sig (update_with_address P x Hptr_x y Haddr_y Hconsistency) x Hptr_x = ptvar y Haddr_y).
          - unfold update_with_address.
            destruct P as [P HP].
            simpl.
            destruct (Vars_eq_dec x x); [reflexivity | congruence].
          - assert (Hequal: ptvar v Haddr_v = ptvar y Haddr_y) by congruence.
            inversion Hequal; subst y.
            rewrite (proof_irrelevance _ Haddr_y Haddr_v).
            reflexivity. }
        { rewrite (Hpx Hp_neq_x).
          apply Hptr with (Hptr_p:=Hptr_p).
          assert (Hnot_changed: proj1_sig (update_with_address P x Hptr_x y Haddr_y Hconsistency) p Hptr_p = proj1_sig P p Hptr_p).
          - unfold update_with_address.
            destruct P as [P HP].
            simpl.
            destruct (Vars_eq_dec x p); [congruence | reflexivity].
          - rewrite <- Hnot_changed.
            assumption. }

  - split.
    + intros c1 Hin.
      apply set_add_elim in Hin; inversion Hin; subst.
      apply satisfy_constraint_Eq_Var.
      × pose proof (Hptr _ _ _ _ Hp) as Hpt_p_v0.
        rewrite <- ValuationLoc_vs_Valuation in Hpt_p_v0.
        destruct (Addressable_dec x) as [Haddr_x | Hnaddr_x].
        { rewrite csem_assignDeref_to_Varz_addr with (Haddr_x:=Haddr_x).
          rewrite Hpt_p_v0.
          compute_val.
          enough (¬ pointer v0) by congruence.
          apply (Hptp v0 Haddr_v).
          apply (proj2_sig P').
          assumption. }
        { rewrite csem_assignDeref_to_Varz_naddr with (Hnaddr_x:=Hnaddr_x).
          rewrite Hpt_p_v0.
          compute_val.
          enough (¬ pointer v0) by congruence.
          apply (Hptp v0 Haddr_v).
          apply (proj2_sig P').
          assumption. }
      × apply set_add_elim in H; inversion H; subst.
        { exact Hsatis_c. }
        { apply constraint_untouched with (C:=C) (theta1:=theta) (x:=x); auto.
          destruct (Addressable_dec x) as [Haddr | Hnaddr].
          - rewrite csem_assignDeref_to_Varz_addr with (Haddr_x:=Haddr).
            intros y Hxy.
            compute_val.
          - rewrite csem_assignDeref_to_Varz_naddr with (Hnaddr_x:=Hnaddr).
            intros y Hxy.
            compute_val. }
    + intros p' Hptr_p' v' Haddr_v' H.
      destruct (Addressable_dec x) as [Haddr_x | Hnaddr_x].
      × rewrite csem_assignDeref_to_Varz_addr with (Haddr_x:=Haddr_x).
        assert (Hsame: Valuation (update_sz theta (alpha x Haddr_x) (sz theta (ValuationLoc theta p Hptr_p))) p' = Valuation theta p') by compute_val.
        rewrite Hsame.
        exact (Hptr p' Hptr_p' v' Haddr_v' H).
      × rewrite csem_assignDeref_to_Varz_naddr with (Hnaddr_x:=Hnaddr_x).
        assert (Hsame: Valuation (update_gz theta x Hnptr_x Hnaddr_x (sz theta (ValuationLoc theta p Hptr_p))) p' = Valuation theta p') by compute_val.
        rewrite Hsame.
        exact (Hptr p' Hptr_p' v' Haddr_v' H).

  - split.
    + intros c1 Hin.
      apply set_add_elim in Hin; inversion Hin; subst.
      × exact Hsatis_c.
      × apply constraint_untouched with (C:=C) (theta1:=theta) (x:=x); auto.
        intros y' Hy'.
        destruct (Addressable_dec x) as [Haddr_x | Hnaddr_x].
        { rewrite csem_assignDeref_to_Varz_addr with (Haddr_x:=Haddr_x).
          compute_val. }
        { rewrite csem_assignDeref_to_Varz_naddr with (Hnaddr_x:=Hnaddr_x).
          compute_val. }
    + intros p' Hptr_p' v' Haddr_v' H.
      destruct (Addressable_dec x) as [Haddr_x | Hnaddr_x].
      × rewrite csem_assignDeref_to_Varz_addr with (Haddr_x:=Haddr_x).
        assert (Hsame: Valuation (update_sz theta (alpha x Haddr_x) (sz theta (ValuationLoc theta p Hptr_p))) p' = Valuation theta p') by compute_val.
        rewrite Hsame.
        exact (Hptr p' Hptr_p' v' Haddr_v' H).
      × rewrite csem_assignDeref_to_Varz_naddr with (Hnaddr_x:=Hnaddr_x).
        assert (Hsame: Valuation (update_gz theta x Hnptr_x Hnaddr_x (sz theta (ValuationLoc theta p Hptr_p))) p' = Valuation theta p') by compute_val.
        rewrite Hsame.
        exact (Hptr p' Hptr_p' v' Haddr_v' H).

  - split.
    + intros c1 Hin.
      apply set_add_elim in Hin; inversion Hin; subst.
      × apply satisfy_constraint_Eq_Var.
        pose proof (Hptr _ _ _ _ Hp) as Hpt_p_v0.
        rewrite <- ValuationLoc_vs_Valuation in Hpt_p_v0.
        destruct (Addressable_dec x) as [Haddr_x | Hnaddr_x].
        { rewrite csem_assignDeref_to_Ptr_addr with (Haddr_p:=Haddr_x).
          rewrite Hpt_p_v0.
          compute_val.
          enough (pointer v0) by congruence.
          apply (Hptp v0 Haddr_v).
          apply (proj2_sig P).
          assumption. }
        { rewrite csem_assignDeref_to_Ptr_naddr with (Hnaddr_p:=Hnaddr_x).
          rewrite Hpt_p_v0.
          compute_val.
          enough (pointer v0) by congruence.
          apply (Hptp v0 Haddr_v).
          apply (proj2_sig P).
          assumption. }
      × apply set_add_elim in H; inversion H; subst.
        { exact Hsatis_c. }
        { apply constraint_untouched with (C:=C) (theta1:=theta) (x:=x); auto.
          intros y' Hy'.
          destruct (Addressable_dec x) as [Haddr_x | Hnaddr_x].
          - rewrite csem_assignDeref_to_Ptr_addr with (Haddr_p:=Haddr_x); compute_val.
          - rewrite csem_assignDeref_to_Ptr_naddr with (Hnaddr_p:=Hnaddr_x); compute_val. }
    + destruct (Addressable_dec x) as [Haddr_x | Hnaddr_x].
      × rewrite csem_assignDeref_to_Ptr_addr with (Haddr_p:=Haddr_x).
        assert (Heq: ValuationLoc theta p Hptr_p = alpha v0 Haddr_v).
        { rewrite ValuationLoc_vs_Valuation.
          apply Hptr with (Hptr_p:=Hptr_p).
          assumption. }
        rewrite Heq.
        assert (Hval_loc: sloc theta (alpha v0 Haddr_v) = ValuationLoc theta v0 (Hptp v0 Haddr_v (proj2_sig P p Hptr_p v0 Haddr_v Hp))) by compute_val.
        rewrite Hval_loc.
        eapply update_with_existing_element_preserves_satisfiability_sloc.
        apply Hptr.
      × rewrite csem_assignDeref_to_Ptr_naddr with (Hnaddr_p:=Hnaddr_x).
        assert (Heq: ValuationLoc theta p Hptr_p = alpha v0 Haddr_v).
        { rewrite ValuationLoc_vs_Valuation.
          apply Hptr with (Hptr_p:=Hptr_p).
          assumption. }
        rewrite Heq.
        assert (Hval_loc: sloc theta (alpha v0 Haddr_v) = ValuationLoc theta v0 (Hptp v0 Haddr_v (proj2_sig P p Hptr_p v0 Haddr_v Hp))) by compute_val.
        rewrite Hval_loc.
        eapply update_with_existing_element_preserves_satisfiability_gloc.
        apply Hptr.

  - split.
    + intros c1 Hin.
      apply set_add_elim in Hin; inversion Hin; subst.
      × exact Hsatis_c.
      × apply constraint_untouched with (C:=C) (theta1:=theta) (x:=x); auto.
        intros y Hyx.
        destruct (csem_assignOther_to_Varz theta x Hnptr_x e) as [theta2 [Htheta2 Htheta']].
        rewrite Htheta2.
        apply Htheta'.
        congruence.
    + intros p' Hptr_p' v' Haddr_v'.
      destruct (csem_assignOther_to_Varz theta x Hnptr_x e) as [theta2 [Htheta2 Htheta']].
      rewrite Htheta2.
      destruct (Vars_eq_dec x p') as [Himpossible | Hneq].
      × subst p'.
        congruence.
      × rewrite <- (Htheta' p' Hneq).
        apply Hptr.

  - split.
    + intros c1 Hin.
      apply set_add_elim in Hin; inversion Hin; subst.
      × exact Hsatis_c.
      × apply constraint_untouched with (C:=C) (theta1:=theta) (x:=x); auto.
        intros y Hyx.
        destruct (csem_assignPtr_to_Varz theta x Hnptr_x e Hptr_e) as [theta2 [Htheta2 Htheta']].
        rewrite Htheta2.
        apply Htheta'.
        congruence.
    + intros p' Hptr_p' v' Haddr_v'.
      destruct (csem_assignPtr_to_Varz theta x Hnptr_x e Hptr_e) as [theta2 [Htheta2 Htheta']].
      rewrite Htheta2.
      destruct (Vars_eq_dec x p') as [Himpossible | Hneq].
      × subst p'.
        congruence.
      × rewrite <- (Htheta' p' Hneq).
        apply Hptr.

  - split.
    + intros c1 Hin.
      apply set_add_elim in Hin; inversion Hin; subst.
      × exact Hsatis_c.
      × apply constraint_untouched with (C:=C) (theta1:=theta) (x:=x); auto.
        intros y Hyx.
        destruct (Addressable_dec x) as [Haddr_x | Hnaddr_x].
        { rewrite csem_assignDeref_to_Ptr_addr with (Haddr_p:=Haddr_x).
          compute_val. }
        { rewrite csem_assignDeref_to_Ptr_naddr with (Hnaddr_p:=Hnaddr_x).
          compute_val. }
    + intros p' Hptr_p' v' Haddr_v' Htop.
      destruct (Vars_eq_dec x p') as [Heq | Hneq].
      × subst x.
        unfold update_with_top in Htop.
        destruct P as [P HP]; simpl in Htop.
        destruct (Vars_eq_dec p' p'); [discriminate | congruence].
      × destruct (Addressable_dec x) as [Haddr_x | Hnaddr_x].
        { rewrite csem_assignDeref_to_Ptr_addr with (Haddr_p:=Haddr_x).
          assert (H: Valuation (update_sloc theta (alpha x Haddr_x) (sloc theta (ValuationLoc theta p Hptr_p))) p' =
            Valuation theta p') by compute_val.
          rewrite H.
          apply Hptr with (Hptr_p:=Hptr_p').
          rewrite <- Htop.
          compute_val. }
        { rewrite csem_assignDeref_to_Ptr_naddr with (Hnaddr_p:=Hnaddr_x).
          assert (H: Valuation (update_gloc theta x Hptr_x Hnaddr_x (sloc theta (ValuationLoc theta p Hptr_p))) p' =
            Valuation theta p') by compute_val.
          rewrite H.
          apply Hptr with (Hptr_p:=Hptr_p').
          rewrite <- Htop.
          compute_val. }

  - split.
    + intros c1 Hin.
      apply set_add_elim in Hin; inversion Hin; subst.
      × exact Hsatis_c.
      × apply constraint_untouched with (C:=C) (theta1:=theta) (x:=x); auto.
        intros y Hyx.
        destruct (csem_assignOther_to_Ptr theta x Hptr_x e) as [theta2 [Htheta2 Htheta']].
        rewrite Htheta2.
        apply Htheta'.
        congruence.
    + intros p' Hptr_p' v' Haddr_v' Htop.
      destruct (csem_assignOther_to_Ptr theta x Hptr_x e) as [theta2 [Htheta2 Htheta']].
      rewrite Htheta2.
      destruct (Vars_eq_dec x p') as [Heq | Hneq].
      × subst x.
        unfold update_with_top in Htop.
        destruct P as [P HP]; simpl in Htop.
        destruct (Vars_eq_dec p' p'); [discriminate | congruence].
      × rewrite <- (Htheta' p' Hneq).
        apply Hptr with (Hptr_p:=Hptr_p').
        rewrite <- Htop.
        compute_val.

  - split.
    + intros c1 Hin.
      apply set_add_elim in Hin; inversion Hin; subst.
      × exact Hsatis_c.
      × apply constraint_untouched with (C:=C) (theta1:=theta) (x:=x); auto.
        intros y Hyx.
        destruct (csem_assignZ_to_Ptr theta x Hptr_x e) as [theta2 [Htheta2 Htheta']].
        rewrite Htheta2.
        apply Htheta'.
        congruence.
    + intros p' Hptr_p' v' Haddr_v' Htop.
      destruct (csem_assignZ_to_Ptr theta x Hptr_x e) as [theta2 [Htheta2 Htheta']].
      rewrite Htheta2.
      destruct (Vars_eq_dec x p') as [Heq | Hneq].
      × subst x.
        unfold update_with_top in Htop.
        destruct P as [P HP]; simpl in Htop.
        destruct (Vars_eq_dec p' p'); [discriminate | congruence].
      × rewrite <- (Htheta' p' Hneq).
        apply Hptr with (Hptr_p:=Hptr_p').
        rewrite <- Htop.
        compute_val.

  - split.
    + intros c1 Hin.
      apply set_add_elim in Hin; inversion Hin; subst.
      × exact Hsatis_c.
      × apply constraint_untouched with (C:=C) (theta1:=theta) (x:=x); auto.
        intros y Hyx.
        destruct (csem_assignVarz_to_Ptr theta x Hptr_x e Hnptr_e) as [theta2 [Htheta2 Htheta']].
        rewrite Htheta2.
        apply Htheta'.
        congruence.
    + intros p' Hptr_p' v' Haddr_v' Htop.
      destruct (csem_assignVarz_to_Ptr theta x Hptr_x e Hnptr_e) as [theta2 [Htheta2 Htheta']].
      rewrite Htheta2.
      destruct (Vars_eq_dec x p') as [Heq | Hneq].
      × subst x.
        unfold update_with_top in Htop.
        destruct P as [P HP]; simpl in Htop.
        destruct (Vars_eq_dec p' p'); [discriminate | congruence].
      × rewrite <- (Htheta' p' Hneq).
        apply Hptr with (Hptr_p:=Hptr_p').
        rewrite <- Htop.
        compute_val.

  - split.
    + intros c1 Hin.
      apply set_add_elim in Hin; inversion Hin; subst.
      × exact Hsatis_c.
      × rewrite csem_assign_to_IgnoredVar.
        exact (Hval c1 H).
    + rewrite csem_assign_to_IgnoredVar.
      exact Hptr.

  - split.
    + intros c1 Hin.
      apply set_add_elim in Hin; inversion Hin; subst.
      × apply satisfy_constraint_Eq_Z.
        rewrite csem_memZ_to_Ptr with (Hptr_p:=Hptr_p).
        assert (H:ValuationLoc theta p Hptr_p = alpha v0 Haddr_v).
        { rewrite ValuationLoc_vs_Valuation.
          apply Hptr with (Hptr_p:=Hptr_p).
          assumption. }
        rewrite H.
        unfold Valuation.
        assert (¬ pointer v0).
        { apply (Hnonpointers v0 Haddr_v).
          apply ((proj2_sig P') p Hptr_p).
          exact Hptp. }
        { compute_val. }
     × apply set_add_elim in H; inversion H; subst.
       { exact Hsatis_c. }
       { apply constraint_untouched with (C:=C) (theta1:=theta) (x:=v0); auto.
         intros y Hyx.
         rewrite csem_memZ_to_Ptr.
         assert (Heq_val:ValuationLoc theta p Hptr_p = alpha v0 Haddr_v).
         { rewrite ValuationLoc_vs_Valuation.
          apply Hptr with (Hptr_p:=Hptr_p).
          assumption. }
         rewrite Heq_val.
         compute_val. }
    + intros p' Hptr_p' v' Haddr_p' Heq_proj.
      rewrite csem_memZ_to_Ptr.
      assert (Hsame: Valuation (update_sz theta (ValuationLoc theta p Hptr_p) z) p' = Valuation theta p').
      { compute_val. }
      rewrite Hsame.
      apply Hptr with (Hptr_p:=Hptr_p').
      apply Heq_proj.

  - split.
    + intros c1 Hin.
      apply set_add_elim in Hin; inversion Hin; subst.
      × apply satisfy_constraint_Eq_Var.
        rewrite csem_memVarz_to_Ptr with (Hptr_p:=Hptr_p).
        assert (H:ValuationLoc theta p Hptr_p = alpha v0 Haddr_v).
        { rewrite ValuationLoc_vs_Valuation.
          apply Hptr with (Hptr_p:=Hptr_p).
          assumption. }
        rewrite H.
        unfold Valuation.
        assert (¬ pointer v0).
        { apply (Hnonpointers v0 Haddr_v).
          apply ((proj2_sig P') p Hptr_p).
          exact Hptp. }
        { compute_val. }
     × apply set_add_elim in H; inversion H; subst.
       { exact Hsatis_c. }
       { apply constraint_untouched with (C:=C) (theta1:=theta) (x:=v0); auto.
         intros y Hyx.
         rewrite csem_memVarz_to_Ptr.
         assert (Heq_val:ValuationLoc theta p Hptr_p = alpha v0 Haddr_v).
         { rewrite ValuationLoc_vs_Valuation.
          apply Hptr with (Hptr_p:=Hptr_p).
          assumption. }
         rewrite Heq_val.
         compute_val. }
    + intros p' Hptr_p' v' Haddr_p' Heq_proj.
      rewrite csem_memVarz_to_Ptr.
      assert (Hsame: Valuation (update_sz theta (ValuationLoc theta p Hptr_p) (ValuationZ theta e Hnptr_e)) p' = Valuation theta p').
      { compute_val. }
      rewrite Hsame.
      apply Hptr with (Hptr_p:=Hptr_p').
      apply Heq_proj.

  - split.
    + intros c1 Hin.
      apply set_add_elim in Hin; inversion Hin; subst.
      × exact Hsatis_c.
      × apply constraint_untouched_all_pt with (C:=C) (theta1:=theta) (p:=p) (Hptr_p:=Hptr_p); try assumption.
        intros y Hnpt.
        rewrite csem_memZ_to_Ptr.
        destruct Hnpt as [[Haddr_y Hnpt_y] | Hnaddr_y].
        { cut (ValuationLoc theta p Hptr_p alpha y Haddr_y).
          - unfold update_sz.
            unfold Valuation.
            destruct (Addressable_dec y); [|congruence].
            destruct (Pointer_dec y) as [Hptr_y | Hnptr_y].
            + simpl.
              reflexivity.
            + intro Hnpt.
              f_equal; unfold sz; simpl.
              destruct (MemoryLocation_eq_dec (ValuationLoc theta p Hptr_p) (alpha y a)) as [Himpossible | Hok].
              × rewrite (proof_irrelevance _ a Haddr_y) in Himpossible; congruence.
              × reflexivity.
          - red.
            intro Himpossible.
            apply Hnpt_y.
            apply (Valuation_is_consistent) with (theta:=theta).
            rewrite <- ValuationLoc_vs_Valuation.
            exact Himpossible. }
        { compute_val. }
    + intros p' Hptr_p' v' Haddr_p' Heq_proj.
      rewrite csem_memZ_to_Ptr.
      assert (Hsame: Valuation (update_sz theta (ValuationLoc theta p Hptr_p) z) p' = Valuation theta p').
      { compute_val. }
      rewrite Hsame.
      apply Hptr with (Hptr_p:=Hptr_p').
      apply Heq_proj.

  - split.
    + intros c1 Hin.
      apply set_add_elim in Hin; inversion Hin; subst.
      × exact Hsatis_c.
      × apply constraint_untouched_all_pt with (C:=C) (theta1:=theta) (p:=p) (Hptr_p:=Hptr_p); try assumption.
        intros y Hnpt.
        rewrite csem_memVarz_to_Ptr.
        destruct Hnpt as [[Haddr_y Hnpt_y] | Hnaddr_y].
        { cut (ValuationLoc theta p Hptr_p alpha y Haddr_y).
          - unfold update_sz.
            unfold Valuation.
            destruct (Addressable_dec y); [|congruence].
            destruct (Pointer_dec y) as [Hptr_y | Hnptr_y].
            + simpl.
              reflexivity.
            + intro Hnpt.
              f_equal; unfold sz; simpl.
              destruct (MemoryLocation_eq_dec (ValuationLoc theta p Hptr_p) (alpha y a)) as [Himpossible | Hok].
              × rewrite (proof_irrelevance _ a Haddr_y) in Himpossible; congruence.
              × reflexivity.
          - red.
            intro Himpossible.
            apply Hnpt_y.
            apply (Valuation_is_consistent) with (theta:=theta).
            rewrite <- ValuationLoc_vs_Valuation.
            exact Himpossible. }
        { compute_val. }
   + intros p' Hptr_p' v' Haddr_p' Heq_proj.
      rewrite csem_memVarz_to_Ptr.
      assert (Hsame: Valuation (update_sz theta (ValuationLoc theta p Hptr_p) (ValuationZ theta e Hnptr_e)) p' = Valuation theta p').
      { compute_val. }
      rewrite Hsame.
      apply Hptr with (Hptr_p:=Hptr_p').
      apply Heq_proj.

  - split.
    + intros c1 Hin.
      apply set_add_elim in Hin; inversion Hin; subst.
      × apply satisfy_constraint_Eq_Var.
        rewrite csem_memPtr_to_Ptr with (Hptr_p:=Hptr_p).
        assert (H:ValuationLoc theta p Hptr_p = alpha v0 Haddr_v).
        { rewrite ValuationLoc_vs_Valuation.
          apply Hptr with (Hptr_p:=Hptr_p).
          assumption. }
        rewrite H.
        unfold Valuation.
        assert (pointer v0).
        { apply (Hpointers v0 Haddr_v).
          apply ((proj2_sig P) p Hptr_p).
          exact Hptp. }
        { compute_val. }
     × apply set_add_elim in H; inversion H; subst.
       { exact Hsatis_c. }
       { apply constraint_untouched with (C:=C) (theta1:=theta) (x:=v0); auto.
         intros y Hyx.
         rewrite csem_memPtr_to_Ptr.
         assert (Heq_val:ValuationLoc theta p Hptr_p = alpha v0 Haddr_v).
         { rewrite ValuationLoc_vs_Valuation.
          apply Hptr with (Hptr_p:=Hptr_p).
          assumption. }
         rewrite Heq_val.
         compute_val. }
    + intros p' Hptr_p' v' Haddr_v' Hpt_p'_v'.
      rewrite csem_memPtr_to_Ptr.
      assert (H:ValuationLoc theta p Hptr_p = alpha v0 Haddr_v).
      { rewrite ValuationLoc_vs_Valuation.
        apply Hptr with (Hptr_p:=Hptr_p).
        assumption. }
      rewrite H.
      eapply update_with_existing_element_preserves_satisfiability_sloc.
      × exact Hptr.
      × exact Hpt_p'_v'.

  - split.
    + intros c1 Hin.
      apply set_add_elim in Hin; inversion Hin; subst.
      × exact Hsatis_c.
      × apply constraint_untouched_all_pt with (C:=C) (theta1:=theta) (p:=p) (Hptr_p:=Hptr_p); try assumption.
        intros y Hnpt.
        rewrite csem_memPtr_to_Ptr.
        destruct Hnpt as [[Haddr_y Hnpt_y] | Hnaddr_y].
        { cut (ValuationLoc theta p Hptr_p alpha y Haddr_y).
          - unfold update_sloc.
            unfold Valuation.
            destruct (Addressable_dec y); [|congruence].
            destruct (Pointer_dec y) as [Hptr_y | Hnptr_y].
            + intro Hnpt.
              f_equal; unfold sz; simpl.
              destruct (MemoryLocation_eq_dec (ValuationLoc theta p Hptr_p) (alpha y a)) as [Himpossible | Hok].
              × rewrite (proof_irrelevance _ a Haddr_y) in Himpossible; congruence.
              × reflexivity.
            + simpl.
              reflexivity.
          - red.
            intro Himpossible.
            apply Hnpt_y.
            apply (Valuation_is_consistent) with (theta:=theta).
            rewrite <- ValuationLoc_vs_Valuation.
            exact Himpossible. }
        { compute_val. }
   + intros p' Hptr_p' v' Haddr_v' Heq_proj.
     rewrite csem_memPtr_to_Ptr.
     unfold update_all_pt_with_top in Heq_proj.
     destruct P as [P HPconsistent]; simpl in × |- ×.
     destruct (may_point_to p Hptr_p p') as [[Himpossible | Hnaddr_p'] | Hnpt_p'].
     × discriminate.
     × unfold update_sloc.
       unfold Valuation.
       destruct (Addressable_dec p'); destruct (Pointer_dec p'); try congruence.
       f_equal.
       unfold gloc; simpl.
       assert (Hsame:snd (fst theta) p' n = ValuationLoc theta p' Hptr_p').
       { compute_val. }
       { rewrite Hsame; rewrite ValuationLoc_vs_Valuation.
         apply Hptr with (Hptr_p:=Hptr_p').
         exact Heq_proj. }
     × unfold update_sloc.
       unfold Valuation.
       destruct (Addressable_dec p') as [Haddr_p' | Hnaddr_p']; destruct (Pointer_dec p'); try congruence.
       { f_equal; simpl.
         destruct (MemoryLocation_eq_dec (ValuationLoc theta p Hptr_p) (alpha p' Haddr_p')) as [Himpossible | Hok].
         - exfalso.
           apply (Hnpt_p' Haddr_p').
           apply Valuation_is_consistent with (theta:=theta).
           rewrite <- ValuationLoc_vs_Valuation.
           exact Himpossible.
         - (assert (Hsame: sloc theta (alpha p' Haddr_p') = ValuationLoc theta p' Hptr_p')).
           + compute_val.
           + rewrite Hsame.
             rewrite ValuationLoc_vs_Valuation.
             apply Hptr with (Hptr_p:=Hptr_p').
             exact Heq_proj. }
       { f_equal; unfold gloc; simpl.
         (assert (Hsame: snd (fst theta) p' Hnaddr_p' = ValuationLoc theta p' Hptr_p')).
         + compute_val.
         + rewrite Hsame.
           rewrite ValuationLoc_vs_Valuation.
           apply Hptr with (Hptr_p:=Hptr_p').
           exact Heq_proj. }

  - split.
    + intros c1 Hin.
      apply set_add_elim in Hin; inversion Hin; subst.
      × exact Hsatis_c.
      × apply constraint_untouched with (C:=C) (theta1:=theta) (x:=v0); auto.
        intros y Hneq.
        destruct (Addressable_dec y) as [Haddr_y | Hnaddr_y].
        { destruct (csem_memOther_to_Ptr theta p Hptr_p e) as [theta2 [Htheta2 Htheta']].
          rewrite Htheta2.
          apply Htheta'; right.
          enough (Hnot_same: ValuationLoc theta p Hptr_p = alpha v0 Haddr_v).
          - rewrite Hnot_same.
            intro Haddr_y_already.
            red; intro Hfalse; apply Hneq.
            eapply location_is_unique; exact Hfalse.
          - rewrite ValuationLoc_vs_Valuation.
            eapply Hptr.
            exact Hptp. }
        { destruct (csem_memOther_to_Ptr theta p Hptr_p e) as [theta2 [Htheta2 Htheta']].
          rewrite Htheta2.
          apply Htheta'; left.
          exact Hnaddr_y. }
    + intros p' Hptr_p' v' Haddr_v' Hpt'.
      destruct (csem_memOther_to_Ptr theta p Hptr_p e) as [theta2 [Htheta2 Htheta']].
      destruct (Addressable_dec p') as [Haddr_p' | Hnaddr_p'].
      × assert (Hsame: Valuation theta p' = Valuation theta2 p').
        { apply Htheta'; right.
          intro Haddr_p'_already; rewrite (proof_irrelevance _ Haddr_p'_already Haddr_p') in × |- ×.
          red; intro Himpossible.
          pose proof (Hptr p Hptr_p v0 Haddr_v Hptp) as Hreal.
          rewrite <- ValuationLoc_vs_Valuation in Hreal.
          rewrite Hreal in Himpossible.
          assert (Himpossible_eq:p' = v0) by (eapply location_is_unique; apply Himpossible).
          congruence. }
        { rewrite Htheta2; rewrite <- Hsame.
          eapply Hptr.
          apply Hpt'. }
      × assert (Hsame: Valuation theta p' = Valuation theta2 p').
        { apply Htheta'; left.
          exact Hnaddr_p'. }
        { rewrite Htheta2; rewrite <- Hsame.
          eapply Hptr.
          apply Hpt'. }

  - split.
    + intros c1 Hin.
      apply set_add_elim in Hin; inversion Hin; subst.
      × exact Hsatis_c.
      × apply constraint_untouched_all_pt with (C:=C) (theta1:=theta) (p:=p) (Hptr_p:=Hptr_p); auto.
        intros y [[Haddr_y Hnpointers] | Hnaddr_y].
        { destruct (csem_memOther_to_Ptr theta p Hptr_p e) as [theta2 [Htheta2 Htheta']].
          rewrite Htheta2.
          apply Htheta'.
          right.
          intro Haddr_y'; red; intro Himpossible; apply Hnpointers.
          apply Valuation_is_consistent with (theta:=theta).
          rewrite <- ValuationLoc_vs_Valuation.
          rewrite (proof_irrelevance _ Haddr_y' Haddr_y) in Himpossible.
          rewrite Himpossible; reflexivity. }
        { destruct (csem_memOther_to_Ptr theta p Hptr_p e) as [theta2 [Htheta2 Htheta']].
          rewrite Htheta2.
          apply Htheta'.
          left.
          exact Hnaddr_y. }
    + intros p' Hptr_p' v' Haddr_v' Hpt'.
      destruct (csem_memOther_to_Ptr theta p Hptr_p e) as [theta2 [Htheta2 Htheta']].
      destruct (Addressable_dec p') as [Haddr_p' | Hnaddr_p'].
      × assert (Hsame: Valuation theta p' = Valuation theta2 p').
        { apply Htheta'; right.
          intro Haddr_p'_already; rewrite (proof_irrelevance _ Haddr_p'_already Haddr_p') in × |- ×.
          red; intro Himpossible.
          symmetry in Himpossible;
            rewrite ValuationLoc_vs_Valuation in Himpossible.
          pose proof (Hpointers _ _ (Valuation_is_consistent _ _ Hptr_p _ _ Himpossible)) as Himpossible'.
          congruence. }
        { rewrite Htheta2; rewrite <- Hsame.
          eapply Hptr.
          apply Hpt'. }
      × assert (Hsame: Valuation theta p' = Valuation theta2 p').
        { apply Htheta'; left.
          exact Hnaddr_p'. }
        { rewrite Htheta2; rewrite <- Hsame.
          eapply Hptr.
          apply Hpt'. }

  - split.
    + intros c1 Hin.
      apply set_add_elim in Hin; inversion Hin; subst.
      × exact Hsatis_c.
      × apply constraint_untouched with (C:=C) (theta1:=theta) (x:=q); auto.
        intros y Hneq.
        destruct (Addressable_dec y) as [Haddr_y | Hnaddr_y].
        { destruct (csem_memOther_to_Ptr theta p Hptr_p e) as [theta2 [Htheta2 Htheta']].
          rewrite Htheta2.
          apply Htheta'; right.
          enough (Hnot_same: ValuationLoc theta p Hptr_p = alpha q Haddr_q).
          - rewrite Hnot_same.
            intro Haddr_q_already.
            red; intro Hfalse; apply Hneq.
            eapply location_is_unique; exact Hfalse.
          - rewrite ValuationLoc_vs_Valuation.
            eapply Hptr.
            exact Hptp. }
        { destruct (csem_memOther_to_Ptr theta p Hptr_p e) as [theta2 [Htheta2 Htheta']].
          rewrite Htheta2.
          apply Htheta'; left.
          exact Hnaddr_y. }
    + intros p' Hptr_p' v' Haddr_v' Hpt'.
      destruct (csem_memOther_to_Ptr theta p Hptr_p e) as [theta2 [Htheta2 Htheta']].
      destruct (Addressable_dec p') as [Haddr_p' | Hnaddr_p'].
      × assert (Hsame: Valuation theta p' = Valuation theta2 p').
        { apply Htheta'; right.
          intro Haddr_p'_already; rewrite (proof_irrelevance _ Haddr_p'_already Haddr_p') in × |- ×.
          red; intro Himpossible.
          pose proof (Hptr p Hptr_p q Haddr_q Hptp) as Hreal.
          rewrite <- ValuationLoc_vs_Valuation in Hreal.
          rewrite Hreal in Himpossible.
          assert (Himpossible_eq:p' = q) by (eapply location_is_unique; apply Himpossible); subst.
          rewrite (proof_irrelevance _ Hptr_p' Hptr_q) in × |- ×.
          assert (proj1_sig (update_with_top P q Hptr_q) q Hptr_q = ptunknown).
          - unfold update_with_top.
            destruct P as [P HPconsistent]; simpl.
            destruct (Vars_eq_dec q q); [reflexivity | congruence].
          - congruence. }
        { rewrite Htheta2; rewrite <- Hsame.
          eapply Hptr.
          rewrite <- Hpt'.
          unfold update_with_top in Hpt' |- ×.
          destruct P as [P HPconsistent].
          simpl in Hpt' |- ×.
          destruct (Vars_eq_dec q p') as [Himpossible | Hok].
          - discriminate.
          - reflexivity. }
      × assert (Hsame: Valuation theta p' = Valuation theta2 p').
        { apply Htheta'; left.
          exact Hnaddr_p'. }
        { rewrite Htheta2; rewrite <- Hsame.
          eapply Hptr.
          rewrite <- Hpt'.
          unfold update_with_top in Hpt' |- ×.
          destruct P as [P HPconsistent].
          simpl in Hpt' |- ×.
          destruct (Vars_eq_dec q p') as [Himpossible | Hok].
          - discriminate.
          - reflexivity. }

  - split.
    + intros c1 Hin.
      apply set_add_elim in Hin; inversion Hin; subst.
      × exact Hsatis_c.
      × apply constraint_untouched_all_pt with (C:=C) (theta1:=theta) (p:=p) (Hptr_p:=Hptr_p); auto.
        intros y [[Haddr_y Hnpointers] | Hnaddr_y].
        { destruct (csem_memOther_to_Ptr theta p Hptr_p e) as [theta2 [Htheta2 Htheta']].
          rewrite Htheta2.
          apply Htheta'.
          right.
          intro Haddr_y'; red; intro Himpossible; apply Hnpointers.
          apply Valuation_is_consistent with (theta:=theta).
          rewrite <- ValuationLoc_vs_Valuation.
          rewrite (proof_irrelevance _ Haddr_y' Haddr_y) in Himpossible.
          rewrite Himpossible; reflexivity. }
        { destruct (csem_memOther_to_Ptr theta p Hptr_p e) as [theta2 [Htheta2 Htheta']].
          rewrite Htheta2.
          apply Htheta'.
          left.
          exact Hnaddr_y. }
    + intros p' Hptr_p' v' Haddr_v' Hpt'.
      destruct (csem_memOther_to_Ptr theta p Hptr_p e) as [theta2 [Htheta2 Htheta']].
      unfold update_all_pt_with_top in Hpt'.
      destruct P as [P HPconsistent].
      simpl in × |- ×.
      destruct (may_point_to p Hptr_p p') as [[[Haddr_p' Hpointers] | Hnaddr_p'] | Hnpointers].
      × discriminate.
      × rewrite Htheta2.
        pose proof (Hptr _ _ _ _ Hpt') as Hval_theta1.
        rewrite <- Hval_theta1; symmetry.
        apply Htheta'.
        left; exact Hnaddr_p'.
      × rewrite Htheta2.
        pose proof (Hptr _ _ _ _ Hpt') as Hval_theta1.
        rewrite <- Hval_theta1; symmetry.
        apply Htheta'.
        right.
        intro Haddr_p'.
        red; intro Himpossible.
        apply (Hnpointers Haddr_p').
        apply Valuation_is_consistent with (theta:=theta).
        rewrite <- ValuationLoc_vs_Valuation; symmetry.
        exact Himpossible.

  - split.
    + intros c1 Hin.
      apply set_add_elim in Hin; inversion Hin; subst.
      × exact Hsatis_c.
      × rewrite csem_mem_to_IgnoredVar.
        exact (Hval c1 H).
    + rewrite csem_mem_to_IgnoredVar.
      exact Hptr.

  - split.
    + intros c1 Hin.
      apply set_add_elim in Hin; inversion Hin; subst.
      × apply satisfy_constraint_Eq_Z.
        rewrite csem_phiZ_naddr with (Hnaddr_x:=Hnaddr_x).
        compute_val.
      × apply set_add_elim in H; inversion H; subst.
        { exact Hsatis_c. }
        { apply constraint_untouched with (C:=C) (theta1:=theta) (x:=x); auto.
          rewrite csem_phiZ_naddr with (Hnaddr_x:=Hnaddr_x).
          intros y Hxy.
          compute_val. }
    + intros.
      rewrite csem_phiZ_naddr with (Hnaddr_x:=Hnaddr_x).
      assert (Hsame: Valuation (update_gz theta x Hnptr_x Hnaddr_x z) p = Valuation theta p) by compute_val.
      rewrite Hsame.
      exact (Hptr p Hptr_p v Haddr_v Hptv).

  - split.
    + intros c1 Hin.
      apply set_add_elim in Hin; inversion Hin; subst.
      × apply satisfy_constraint_Eq_Var.
        destruct (Addressable_dec v0) as [Haddr_v | Hnaddr_v].
        { rewrite csem_phiVarz_naddr with (Hnaddr_x:=Hnaddr_x).
          compute_val. }
        { rewrite csem_phiVarz_naddr with (Hnaddr_x:=Hnaddr_x).
          compute_val. }
      × apply set_add_elim in H; inversion H; subst.
        { exact Hsatis_c. }
        { apply constraint_untouched with (C:=C) (theta1:=theta) (x:=x); auto.
          rewrite csem_phiVarz_naddr with (Hnaddr_x:=Hnaddr_x).
          intros y Hxy.
          compute_val. }
    + intros.
      rewrite csem_phiVarz_naddr with (Hnaddr_x:=Hnaddr_x).
      assert (Hsame: Valuation (update_gz theta x Hnptr_x Hnaddr_x (ValuationZ theta v0 Hnptr_v)) p = Valuation theta p) by compute_val.
      rewrite Hsame.
      exact (Hptr p Hptr_p v Haddr_v Hptv).

  - split.
    + intros c1 Hin.
      apply set_add_elim in Hin; inversion Hin; subst.
      × exact Hsatis_c.
      × apply constraint_untouched with (C:=C) (theta1:=theta) (x:=x); auto.
        intros y Hyx.
        destruct (csem_phiOther_to_Varz theta x Hnptr_x Hnaddr_x e) as [theta2 [Htheta2 Htheta']].
        rewrite Htheta2.
        apply Htheta'.
        congruence.
    + intros p' Hptr_p' v' Haddr_v'.
      destruct (csem_phiOther_to_Varz theta x Hnptr_x Hnaddr_x e) as [theta2 [Htheta2 Htheta']].
      rewrite Htheta2.
      destruct (Vars_eq_dec x p') as [Himpossible | Hneq].
      × subst p'.
        congruence.
      × rewrite <- (Htheta' p' Hneq).
        apply Hptr.

  - split.
    + intros c1 Hin.
      apply set_add_elim in Hin; inversion Hin; subst.
      × apply satisfy_constraint_Eq_Var.
        destruct (Addressable_dec v0) as [Haddr_v0 | Hnaddr_v0].
        { rewrite csem_phiPtr_to_Ptr_naddr with (Hnaddr_p:=Hnaddr_p); compute_val. }
        { rewrite csem_phiPtr_to_Ptr_naddr with (Hnaddr_p:=Hnaddr_p); compute_val. }
     × apply set_add_elim in H; inversion H; subst.
        { exact Hsatis_c. }
        { apply constraint_untouched with (C:=C) (theta1:=theta) (x:=p); auto.
          rewrite csem_phiPtr_to_Ptr_naddr with (Hnaddr_p:=Hnaddr_p).
          intros y Hxy.
          compute_val. }
    + intros.
      rewrite csem_phiPtr_to_Ptr_naddr with (Hnaddr_p:=Hnaddr_p).
      eapply update_with_existing_element_preserves_satisfiability_gloc; [exact Hptr | exact Hptv].

  - split.
    + intros c1 Hin.
      apply set_add_elim in Hin; inversion Hin; subst.
      × exact Hsatis_c.
      × apply constraint_untouched with (C:=C) (theta1:=theta) (x:=p); auto.
        intros y' Hy'.
        rewrite csem_phiAddr_to_Ptr_naddr with (Hnaddr_p:=Hnaddr_p).
        compute_val.
    + intros p' Hptr_p' v Haddr_v H.
      rewrite csem_phiAddr_to_Ptr_naddr with (Hnaddr_p:=Hnaddr_p).
      assert (Hpx: p' p Valuation (update_gloc theta p Hptr_p Hnaddr_p (alpha y Haddr_y)) p' = Valuation theta p')
        by compute_val.
      destruct (Vars_eq_dec p' p) as [Hp_eq_p | Hp_neq_p] ; [subst p'|].
      { compute_val.
        assert (proj1_sig (update_with_address P p Hptr_p y Haddr_y Hconsistency) p Hptr_p = ptvar y Haddr_y).
        - unfold update_with_address.
          destruct P as [P HP].
          simpl.
          destruct (Vars_eq_dec p p); [reflexivity | congruence].
        - assert (Hequal: ptvar v Haddr_v = ptvar y Haddr_y) by congruence.
          inversion Hequal; subst y.
          rewrite (proof_irrelevance _ Haddr_y Haddr_v).
          reflexivity. }
      { rewrite (Hpx Hp_neq_p).
        apply Hptr with (Hptr_p:=Hptr_p').
        assert (Hnot_changed: proj1_sig (update_with_address P p Hptr_p y Haddr_y Hconsistency) p' Hptr_p' = proj1_sig P p' Hptr_p').
        - unfold update_with_address.
          destruct P as [P HP].
          simpl.
          destruct (Vars_eq_dec p p'); [congruence | reflexivity].
        - rewrite <- Hnot_changed.
          assumption. }

  - split.
    + intros c1 Hin.
      apply set_add_elim in Hin; inversion Hin; subst.
      × exact Hsatis_c.
      × apply constraint_untouched with (C:=C) (theta1:=theta) (x:=p); auto.
        intros y Hyx.
        destruct (csem_phiOther_to_Ptr theta p Hptr_p Hnaddr_p e) as [theta2 [Htheta2 Hthe