Require Import LibLists.
Require Import Relations.
Require Import Tactics.
Load Param.
Require Import Recdef.

Require Import Maps.
Require Import Coqlib.
Require Import Eqdep_dec.
Require Export BuiltinTypes.
Definition ident := positive.
Ltac unfold_ident := unfold ident.
Ltac unfold_ident_in_all := unfold ident in *.
Ltac unfold_ident_in H := unfold ident in H.

C++ notions

 Module Typ.
  Section Typ.
    Variable A : ATOM.t.

    Inductive t : Type :=
    | atom (_ : ATOM.ty A)
    | class (_ : ident)
      .

  Lemma eq_dec : forall a b : t, {a = b} + {a <> b}.
 End Typ.
 Implicit Arguments class [A].

End Typ.

Module WeakTyp.
 Section WeakTyp.
  Variable A : ATOM.t.

  Inductive t : Type :=
  | atom (_ : ATOM.ty A)
  | object
    .

  Fixpoint of_type (u : Typ.t A) : t :=
    match u with
      | Typ.atom a => atom a
      | Typ.class _ => object
    end.

  Fixpoint option_of_type (u : option (Typ.t A)) : option t :=
  match u with
    | None => None
    | Some t' => Some (of_type t')
  end.

  Lemma eq_dec : forall u1 u2 : t, {u1 = u2} + {u1 <> u2}.
End WeakTyp.
Implicit Arguments object [A].
End WeakTyp.


Module MethodSignature.
  Section MS.
  Variable A : ATOM.t.
  Record t : Type := make {
    name : ident;
    params : list (Typ.t A);
    return_type : option (Typ.t A)
  }.
  Lemma eq_dec : forall a b : t, {a = b} + {a <> b}.
End MS.
End MethodSignature.

Module Method.
  Section M.
    Variable A : ATOM.t.


    Inductive method_kind : Set :=
    | abstract
    | concrete (entry : ident)
      .

  Record t : Type := make {
    signature : MethodSignature.t A;
    kind : method_kind;
    virtual : bool
  }.

  Definition find (s : MethodSignature.t A) :=
    find (fun m => if MethodSignature.eq_dec (signature m) s then true else false).

  Lemma find_in : forall s m l, find s l = Some m -> In m l.

End M.

End Method.


Module FieldSignature.
  Section FS.
    Variable A : ATOM.t.


  Inductive field_type : Type :=
  | Scalar (_ : Typ.t A)
  | Struct (struct : ident) (arraysize : positive)
    .

  Record t : Type := make {
    name : ident;
    type : field_type
  }.

  Lemma eq_dec : forall a b : t, {a = b} + {a <> b}.
End FS.

  Implicit Arguments Struct [A].

End FieldSignature.


Module Class.
  Module Inheritance.
    Inductive t : Set :=
    | Repeated | Shared
      .
    Theorem eq_dec : forall a b : t, {a = b} + {a <> b}.
  End Inheritance.
  Section C.
    Variable A : ATOM.t.
  Record t : Type := make {
    super : list (Inheritance.t * ident) ;
    fields : list (FieldSignature.t A);
    methods : list (Method.t A)
  }.
End C.

End Class.


Lemma in_map_bases_intro : forall l c, In (Class.Inheritance.Repeated, c) l -> In c (map (fun hb : Class.Inheritance.t * ident => let (_, b) := hb in b) (filter (fun hb : _ * ident =>
    match hb with
      | (Class.Inheritance.Shared, _) => false
      | _ => true
    end
  ) l)).

Lemma in_map_bases_elim : forall l c, In c (map (fun hb : Class.Inheritance.t * ident => let (_, b) := hb in b) (filter (fun hb : _ * ident =>
    match hb with
      | (Class.Inheritance.Shared, _) => false
      | _ => true
    end
  ) l)) -> In (Class.Inheritance.Repeated, c) l.

Operational semantics

Function is_some (A : Type) (x : option A) : Prop :=
  match x with None => False | Some _ => True end.

Definition is_some_constr {A : Type} (x : option A) (h : is_some x) : {y | x = Some y}.

Lemma is_some_eq : forall (A : Type) (x : _ A) (h1 h2 : is_some x), h1 = h2.

Lemma is_some_last_one_elem : forall (A : Type) (a : A), is_some (last (a :: nil)).

Section Subobjects.
  Variable A : ATOM.t.

Path to a subobject (inheritance) Directly inspired from Wasserrab et al.

Section Paths.

Variable hierarchy : PTree.t (Class.t A).

Lemma super_eq_dec : forall i j : (Class.Inheritance.t * ident),
  {i = j} + {i <> j}.


Function is_valid_repeated_subobject (l : list ident) : bool :=
  match l with
    | nil => false
    | id1 :: l2 =>
      match PTree.get id1 hierarchy with
        | None => false
        | Some cl1 =>
          match l2 with
            | nil => true
            | id2 :: l3 =>
              if In_dec super_eq_dec (Class.Inheritance.Repeated, id2) (Class.super cl1)
                then is_valid_repeated_subobject l2
                else false
          end
      end
  end.

Lemma is_valid_repeated_subobject_join : forall l1 p l2,
  is_valid_repeated_subobject (l1 ++ p :: nil) = true ->
  is_valid_repeated_subobject (p :: l2) = true ->
  is_valid_repeated_subobject (l1 ++ p :: l2) = true.
  
Lemma is_valid_repeated_subobject_split_left : forall l1 p l2,
  is_valid_repeated_subobject (l1 ++ p :: l2) = true ->
  is_valid_repeated_subobject (l1 ++ p :: nil) = true.

Lemma is_valid_repeated_subobject_split_right : forall l1 p l2,
  is_valid_repeated_subobject (l1 ++ p :: l2) = true ->
  is_valid_repeated_subobject (p :: l2) = true.

Lemma is_valid_repeated_subobject_cons_right : forall l1 p,
  is_valid_repeated_subobject (l1 ++ p :: nil) = true ->
  forall c, PTree.get p hierarchy = Some c ->
    forall q, In (Class.Inheritance.Repeated, q) (Class.super c) ->
      PTree.get q hierarchy <> None ->
      is_valid_repeated_subobject (l1 ++ p :: q :: nil) = true.

Lemma is_valid_repeated_subobject_defined : forall l,
  is_valid_repeated_subobject l = true ->
  forall a, In a l -> hierarchy ! a <> None.
  
  
Section Virtual_base.

Variable bi : ident.


Inductive is_virtual_base_of : ident -> Prop :=
| is_virtual_base_of_O :
  forall ci c,
    PTree.get ci hierarchy = Some c ->
    In (Class.Inheritance.Shared, bi) (Class.super c) ->
    is_virtual_base_of ci
| is_virtual_base_of_S :
  forall ci c,
    PTree.get ci hierarchy = Some c ->
    forall h' bi',
      In (h', bi') (Class.super c) ->
      is_virtual_base_of bi' ->
      is_virtual_base_of ci
.

Lemma is_virtual_base_of_defined : forall ci,
  is_virtual_base_of ci ->
  PTree.get ci hierarchy <> None.


End Virtual_base.

Lemma is_virtual_base_of_trans : forall b c,
  is_virtual_base_of b c ->
  forall a,
    is_virtual_base_of a b ->
    is_virtual_base_of a c
.

Section Path.

Variable to : ident.

Section path1.

Variable via : list ident.


Inductive path : forall from : ident, Class.Inheritance.t -> Prop :=
| path_repeated :
  forall from lf lt,
    via = from :: lf ->
    via = lt ++ to :: nil ->
    is_valid_repeated_subobject via = true ->
    path from Class.Inheritance.Repeated
| path_shared : forall from base h,
  is_virtual_base_of base from ->
  path base h ->
  path from Class.Inheritance.Shared
.


Inductive path0 : forall from : ident, Class.Inheritance.t -> Prop :=
| path0_repeated :
  forall from lf lt,
    via = from :: lf ->
    via = lt ++ to :: nil ->
    is_valid_repeated_subobject via = true ->
    path0 from Class.Inheritance.Repeated
| path0_shared : forall from base,
  is_virtual_base_of base from ->
  forall lf lt,
    via = base ::lf ->
    via = lt ++ to :: nil ->
    is_valid_repeated_subobject via = true ->
    path0 from Class.Inheritance.Shared
.


Lemma path0_path : forall from h, path0 from h -> path from h.

Lemma path_path0 : forall from h, path from h -> path0 from h.



Inductive path1 : forall from : ident, Class.Inheritance.t -> Prop :=
| path1_repeated :
  forall from lf lt,
    via = from :: lf ->
    via = lt ++ to :: nil ->
    is_valid_repeated_subobject via = true ->
    path1 from Class.Inheritance.Repeated
| path1_shared : forall from base,
  is_virtual_base_of base from ->
  path base Class.Inheritance.Repeated ->
    path1 from Class.Inheritance.Shared
.


Lemma path1_path : forall from h, path1 from h -> path from h.

Lemma path_path1 : forall from h, path from h -> path1 from h.


End path1.


Inductive path2 : forall (via : list ident) (from : ident), Class.Inheritance.t -> Prop :=
| path_O :
  PTree.get to hierarchy <> None ->
  path2 (to :: nil) to Class.Inheritance.Repeated
| path_S_repeated :
  forall from cfrom,
    PTree.get from hierarchy = Some cfrom ->
    forall interm,
      In (Class.Inheritance.Repeated, interm) (Class.super cfrom) ->
      forall l,
        path2 l interm Class.Inheritance.Repeated ->
        path2 (from :: l) from Class.Inheritance.Repeated
| path_S_shared_1 :
  forall from cfrom,
    PTree.get from hierarchy = Some cfrom ->
    forall interm,
      In (Class.Inheritance.Shared, interm) (Class.super cfrom) ->
      forall l h,
        path2 l interm h ->
        path2 l from Class.Inheritance.Shared
| path_S_shared_2 :
  forall from cfrom,
    PTree.get from hierarchy = Some cfrom ->
    forall h interm,
      In (h, interm) (Class.super cfrom) ->
      forall l,
        path2 l interm Class.Inheritance.Shared ->
        path2 l from Class.Inheritance.Shared
.

Lemma path2_path : forall via from h,
  path2 via from h ->
  path via from h.
 
Lemma path_path2_repeated :
  forall l from,
    path l from Class.Inheritance.Repeated ->
    path2 l from Class.Inheritance.Repeated
.

Lemma path_path2 : forall l from h,
  path l from h ->
  path2 l from h
.

Lemma path_repeated_cons : forall i c,
  hierarchy ! i = Some c ->
  forall d, In (Class.Inheritance.Repeated, d) (Class.super c) ->
    forall l, path l d Class.Inheritance.Repeated ->
      path (i :: l) i Class.Inheritance.Repeated.

Lemma path_last : forall l d k,
  path l d k ->
  last l = Some to.

Corollary path_nonempty : forall l d k,
  path l d k ->
  l <> nil.

Lemma path_trivial : hierarchy ! to <> None -> path (to :: nil) to Class.Inheritance.Repeated.
  

Lemma path_cons_repeated : forall from by l h,
  path (by :: l) from h ->
  path (by :: l) by Class.Inheritance.Repeated.


Function plus (a b : list ident) {struct b} : list ident :=
  match b with
    | nil => a
    | hb :: b' =>
      match last a with
        | None => hb :: b'
        | Some la => if peq la hb then a ++ b' else a ++ b
      end
  end.

Lemma plus_nil_left : forall a, plus nil a = a.

Lemma plus_cons : forall b, b <> nil -> forall a c,
  plus (a :: b) c = a :: plus b c.

Transparent last.

Lemma plus_assoc : forall a b c,
  plus (plus a b) c = plus a (plus b c).


Function concat (kp1 kp2 : Class.Inheritance.t * list ident) :
  Class.Inheritance.t * list ident :=
  let (k1, p1) := kp1 in
    let (k2, p2) := kp2 in
      match k2 with
        | Class.Inheritance.Shared => kp2
        | _ => (k1, plus p1 p2)
      end
.

Lemma concat_assoc : forall kp1 kp2 kp3,
  concat (concat kp1 kp2) kp3 = concat kp1 (concat kp2 kp3).

Lemma concat_other : forall p,
  p <> nil ->
  forall q1 q2, q1 <> q2 ->
    forall h0 p0 h, concat (h0, p0) (h, p ++ q1) <> concat (h0, p0) (h, p ++ q2).


End Path.

Lemma path2_concat : forall (a b : ident) k1 p1,
  path2 b p1 a k1 ->
  forall c k2 p2,
    path2 c p2 b k2 ->
    let (k, p) := concat (k1, p1) (k2, p2) in
      path2 c p a k
.

Corollary path_concat : forall (a b : ident) k1 p1,
  path b p1 a k1 ->
  forall c k2 p2,
    path c p2 b k2 ->
    forall k p,
    (k, p) = concat (k1, p1) (k2, p2) ->
      path c p a k
.

 
Lemma path2_concat_recip : forall (a c : ident) k p,
  path2 c p a k ->
  (a = c /\ k = Class.Inheritance.Repeated) \/
  forall ka, hierarchy ! a = Some ka ->
  exists b, exists k1, exists k2, exists p2,
    In (k1, b) (Class.super ka) /\
    path2 c p2 b k2 /\
    (k, p) = concat (k1, match k1 with
                 | Class.Inheritance.Repeated => a :: b :: nil
                 | Class.Inheritance.Shared => b :: nil
               end) (k2, p2).

Corollary path_concat_recip : forall (a c : ident) k p,
  path c p a k ->
  (a = c /\ k = Class.Inheritance.Repeated) \/
  forall ka, hierarchy ! a = Some ka ->
  exists b, exists k1, exists k2, exists p2,
    In (k1, b) (Class.super ka) /\
    path c p2 b k2 /\
    (k, p) = concat (k1, match k1 with
                 | Class.Inheritance.Repeated => a :: b :: nil
                 | Class.Inheritance.Shared => b :: nil
               end) (k2, p2).


Lemma path_elem : forall b kb,
  hierarchy ! b = Some kb ->
  forall k a, In (k, a) (Class.super kb) ->
    hierarchy ! a <> None ->
    path a (match k with
               | Class.Inheritance.Repeated => (b :: a :: nil)
               | Class.Inheritance.Shared => a :: nil
             end) b k.

Lemma path_defined_from : forall from to via by,
  path to via from by -> hierarchy ! from <> None.

Lemma path_defined_to : forall from to via by,
  path to via from by -> hierarchy ! to <> None.
   
Lemma path_eq_dec : forall p1 p2 : Class.Inheritance.t * list ident,
  {p1 = p2} + {p1 <> p2}.

Lemma concat_trivial_left : forall to via from by,
  path to via from by ->
  concat (Class.Inheritance.Repeated, from :: nil) (by, via) = (by, via).

Lemma concat_trivial_right : forall to via from by,
  path to via from by ->
  concat (by, via) (Class.Inheritance.Repeated, to :: nil) = (by, via).

Lemma last_concat : forall l1 to, last l1 = Some to ->
  forall h l2, (h, l1 ++ l2) = concat (h, l1) (Class.Inheritance.Repeated, to :: l2).

Lemma path_is_virtual_base_of : forall to via from by,
  path to via from by ->
  forall base, is_virtual_base_of base to ->
    is_virtual_base_of base from.


Lemma plus_last : forall p2, p2 <> nil -> forall p1, last (plus p1 p2) = last p2.

Lemma concat_last : forall p2, p2 <> nil -> forall h1 p1 h2 h p, (h, p) = concat (h1, p1) (h2, p2) ->
  last p = last p2.

End Paths.

Array paths (POPL 2011 Section 3.2)

Section Array_path.

Definition array_path := (list (Z * (Class.Inheritance.t * list ident) * (FieldSignature.t A))).

Variable hierarchy : PTree.t (Class.t A).

  Inductive valid_array_path : forall
    (to : ident) (to_n : Z) (from : ident) (from_n : Z) (via : array_path), Prop :=
  | valid_array_path_nil : forall c to_n from_n,
    0 <= to_n ->
    to_n <= from_n ->
    valid_array_path c to_n c from_n nil
  | valid_array_path_cons : forall to to_n by through from from_n p h l fs via by_n,
    0 <= p ->
    p < from_n ->
    path hierarchy through l from h ->
    forall hthrough, hierarchy ! through = Some hthrough ->
      In fs (Class.fields hthrough) ->
      FieldSignature.type fs = FieldSignature.Struct by by_n ->
      valid_array_path to to_n by (Zpos by_n) via ->
      valid_array_path to to_n from from_n ((p, (h, l), fs) :: via)
      .

  Lemma valid_array_path_widening : forall to to_n from from_n via,
    valid_array_path to to_n from from_n via ->
    forall to_n' from_n',
      to_n' <= to_n ->
      from_n <= from_n' ->
      0 <= to_n' ->
      valid_array_path to to_n' from from_n' via.

  Lemma valid_array_path_nonnegative_to : forall by by_n from from_n via1,
    valid_array_path by by_n from from_n via1 ->
    0 <= by_n.

  Lemma valid_array_path_nonnegative_from : forall by by_n from from_n via1,
    valid_array_path by by_n from from_n via1 ->
    0 <= from_n.

  Lemma valid_array_path_concat : forall by by_n from from_n via1,
    valid_array_path by by_n from from_n via1 ->
    forall to to_n via2,
      valid_array_path to to_n by by_n via2 ->
      valid_array_path to to_n from from_n (via1 ++ via2)
      .

  Corollary valid_array_path_concat_widening : forall by by_n from from_n via1,
    valid_array_path by by_n from from_n via1 ->
    forall by_n', by_n' <= by_n ->
      forall to to_n via2,
      valid_array_path to to_n by by_n' via2 ->
      valid_array_path to to_n from from_n (via1 ++ via2)
      .

  Lemma valid_array_path_concat_recip : forall via1 to to_n via2 from from_n,
    valid_array_path to to_n from from_n (via1 ++ via2) ->
    exists by, exists by_n,
      valid_array_path by by_n from from_n via1 /\
      valid_array_path to to_n by by_n via2
      .

  Lemma valid_array_path_last : forall by1 by_n1 from from_n via,
    valid_array_path by1 by_n1 from from_n via ->
    forall by2 by_n2,
      valid_array_path by2 by_n2 from from_n via ->
      by1 = by2.

 Lemma array_path_eq_dec : forall l1 l2 : array_path,
   {l1 = l2} + {l1 <> l2}.

Lemma maximize_array_path :
  forall from from_n ar to to_n, valid_array_path to to_n from from_n ar ->
      exists to_n', valid_array_path to to_n' from from_n ar /\ to_n <= to_n' /\
        match last ar with
          | Some (pair (pair _ _) fs) =>
            exists n' : positive,
              to_n' = Zpos n' /\
              FieldSignature.type fs = FieldSignature.Struct to n'
          | None => to_n' = from_n /\ to = from
        end.

Generalized subobjects (POPL 2011 Section 3.2) are called "relative pointers" because they are pointers to a suboject relatively to a structure array

   
 Inductive valid_relative_pointer (afrom: ident) (zfrom: Z) (apath: array_path) (ato: ident) (i : Z) (h : Class.Inheritance.t) (p : list ident) (pto : ident) : Prop :=
   | valid_relative_pointer_intro
     (zto : Z) (_ : valid_array_path ato zto afrom zfrom apath)
     (_ : 0 <= i) (_ : i < zto)
     (_ : path hierarchy pto p ato h)
.

Lemma valid_relative_pointer_last : forall afrom zfrom apath ato1 i h p pto1,
  valid_relative_pointer afrom zfrom apath ato1 i h p pto1 ->
  forall ato2 pto2, valid_relative_pointer afrom zfrom apath ato2 i h p pto2 -> ato1 = ato2 /\ pto1 = pto2.
 

 End Array_path.


Section Relative_pointer_alt.

Alternate definition for generalized subobjects (relative to a given structure array) (from POPL 2011)

 Inductive relative_pointer_alt: Type :=
   | relative_pointer_alt_intro
     (i : Z) (p : Class.Inheritance.t * list ident)
     (f : option (FieldSignature.t A * array_path * Z * (Class.Inheritance.t * list ident)))
     .
     
 Function relative_pointer_alt_of_relative_pointer (a : array_path) (i : Z) (p : Class.Inheritance.t * list ident) {struct a} : relative_pointer_alt :=
   match a with
     | nil => relative_pointer_alt_intro i p None
     | (i', p', f') :: a' => relative_pointer_alt_intro i' p' (Some (f', a', i, p))
   end.
 
 Function relative_pointer_of_relative_pointer_alt (rpa : relative_pointer_alt) : (array_path * Z * (Class.Inheritance.t * list ident)) :=
   match rpa with
     | relative_pointer_alt_intro i p None => (nil, i, p)
     | relative_pointer_alt_intro i' p' (Some (f', a, i, p)) => ((i', p', f') :: a, i, p)
   end.

 Fact relative_pointer_alt_to_default_to_alt : forall rpa a i p,
   relative_pointer_of_relative_pointer_alt rpa = (a, i, p) ->
   relative_pointer_alt_of_relative_pointer a i p = rpa.

 Fact relative_pointer_default_to_alt_to_default: forall a i p,
   relative_pointer_of_relative_pointer_alt (relative_pointer_alt_of_relative_pointer a i p) = (a, i, p).

 Function relative_pointer_alt_length (rpa : relative_pointer_alt) : nat :=
   match rpa with
     | relative_pointer_alt_intro _ _ None => O
     | relative_pointer_alt_intro _ _ (Some (_, a, _, _)) => S (length a)
   end.

 Fact relative_pointer_alt_length_correct: forall a i p,
   relative_pointer_alt_length (relative_pointer_alt_of_relative_pointer a i p) = length a.


 Variable hierarchy : PTree.t (Class.t A).

 Inductive valid_relative_pointer_alt (afrom : ident) (zfrom : Z) (ato : ident) (pto : ident) : relative_pointer_alt -> Prop :=
 | valid_relative_pointer_alt_intro : forall i',
   0 <= i' -> i' < zfrom -> forall h' p' through,
     path hierarchy through p' afrom h' ->
     forall f',
       match f' with
         | None => ato = afrom /\ pto = through
         | Some (f, a, i, (h, p)) =>
           exists cthrough, hierarchy ! through = Some cthrough /\
             In f (Class.fields cthrough) /\
             exists bfrom, exists bn,
               FieldSignature.type f = FieldSignature.Struct bfrom bn /\
               valid_relative_pointer hierarchy bfrom (Zpos bn) a ato i h p pto
       end ->
       valid_relative_pointer_alt afrom zfrom ato pto (relative_pointer_alt_intro i' (h', p') f')
.

 Fact valid_relative_pointer_alt_valid_relative_pointer : forall p afrom zfrom ato pto,
   valid_relative_pointer_alt afrom zfrom ato pto p ->
   forall a i h' p', relative_pointer_of_relative_pointer_alt p = (a, i, (h', p')) ->
     valid_relative_pointer hierarchy afrom zfrom a ato i h' p' pto
.

 Fact valid_relative_pointer_valid_relative_pointer_alt : forall afrom zfrom a ato i h' p' pto,
   valid_relative_pointer hierarchy afrom zfrom a ato i h' p' pto ->
   valid_relative_pointer_alt afrom zfrom ato pto (relative_pointer_alt_of_relative_pointer a i (h', p')).

End Relative_pointer_alt.


End Subobjects.

Scalar values

 Module Value.



Section V.
  Variable A : ATOM.t.

  Inductive pointer : Type :=
  | null (_ : ident)
  | subobject (array : ident) (arraypath : array_path A)
    (index : Z) (inhkind : Class.Inheritance.t) (l : list ident) (_ : is_some (last l))
    .
  Implicit Arguments subobject [].

  Lemma pointer_eq_dec : forall p1 p2 : pointer, {p1 = p2} + {p1 <> p2}.

  Inductive t : Type :=
  | atom (ty : ATOM.ty A) (_ : ATOM.val ty)
  | ptr (_ : pointer)
    .

  Lemma eq_dec : forall a b : t, {a = b} + {a <> b}.

   Function type_of (v : t) : Typ.t A :=
     match v with
       | atom a _ => Typ.atom a
       | ptr (null c) => Typ.class c
       | ptr (subobject _ _ _ _ l h) =>
         let (c, _) := is_some_constr h in Typ.class c
  end.

Function weaktype_of (v : t) : WeakTyp.t A :=
  match v with
    | atom a _ => WeakTyp.atom a
    | ptr _ => WeakTyp.object
  end.

Lemma weaktype_of_type_of_value : forall v,
  WeakTyp.of_type (type_of v) = weaktype_of v.

Function weaktype_of_option (v : option t) : option (WeakTyp.t A) :=
  match v with
    | None => None
    | Some v' => Some (weaktype_of v')
  end.

Function check_weak (u : WeakTyp.t A) (v : t) {struct v} : option t :=
  match v with
    | atom a _ =>
      match u with
        | WeakTyp.atom a' => if ATOM.ty_eq_dec a a' then Some v else None
        | _ => None
      end
    | ptr _ =>
      match u with
        | WeakTyp.object => Some v
        | _ => None
      end
  end.


Lemma check_weak_some : forall u v v',
  check_weak u v = Some v' -> v' = v.

Lemma weaktype_of_check_weak_2 : forall u v v',
  check_weak u v = Some v' ->
  weaktype_of v = u.

Corollary weaktype_of_check_weak : forall u v v',
  check_weak u v = Some v' ->
  weaktype_of v' = u.
  

Function load_value_weak (v : option t) (ty : WeakTyp.t A) : option t :=
  match v with
    | None => None
    | Some v' => check_weak ty v'
  end.

Lemma weaktype_of_load_value_weak : forall v ty v',
  load_value_weak v ty = Some v' ->
  weaktype_of v' = ty.

Lemma load_value_weak_some : forall v ty v',
  load_value_weak (Some v) ty = Some v' ->
  v = v'.

Function check (u : Typ.t A) (v : t) {struct v} : option t :=
  match v with
    | atom a _ =>
      match u with
        | Typ.atom a' => if ATOM.ty_eq_dec a a' then Some v else None
        | _ => None
      end
    | ptr (null c) =>
      match u with
        | Typ.class c' =>
          if peq c c' then Some v else None
        | _ => None
      end
    | ptr (subobject _ _ _ _ l h) =>
      let (c, _) := is_some_constr h in
        match u with
          | Typ.class c' =>
            if peq c c' then Some v else None
          | _ => None
        end
  end.

Lemma check_some : forall u v v',
  check u v = Some v' -> v' = v.

Lemma type_of_check : forall u v v',
  check u v = Some v' ->
  type_of v' = u.

Corollary type_of_check_2 : forall u v v',
  check u v = Some v' ->
  type_of v = u.

Function load_value (v : option t) (ty : Typ.t A) : option t :=
  match v with
    | None => None
    | Some v' => check ty v'
  end.

Lemma type_of_load_value : forall v ty v',
  load_value v ty = Some v' ->
  type_of v' = ty.

Lemma load_value_some : forall v ty v',
  load_value (Some v) ty = Some v' ->
  v = v'.

End V.
Implicit Arguments atom [A].
Implicit Arguments subobject [A].
End Value.

Object operations (field access, object creation)

Section Find_field.
Variable A : ATOM.t.

Definition field_key := (positive * array_path A * Z * (Class.Inheritance.t * list ident) * FieldSignature.t A)%type.

Lemma cfield_dec : forall a b : field_key,
  {a = b} + {a <> b}.

Definition find_field f := List.find (fun n : field_key * Value.t A => let (a, _) := n in if cfield_dec a f then true else false).

  Function update_field (f : field_key) (v : Value.t A) (l : list (field_key * Value.t A)) {struct l} :
    list (field_key * Value.t A) :=
    match l with
      | nil => (f, v) :: nil
      | a :: q =>
        let (i, _) := a in
          if cfield_dec i f then (i, v) :: q else a :: update_field f v q
    end.

  Lemma find_update_field_same : forall f v l,
    find_field f (update_field f v l) = Some (f, v).

  Lemma find_update_field_other : forall f f',
    f <> f' ->
    forall l v,
      find_field f' (update_field f v l) = find_field f' l.

  Function remove_field (f : field_key) (l : list (field_key * Value.t A)) {struct l} :
    list (field_key * Value.t A) :=
    match l with
      | nil => nil
      | a :: q =>
        let (i, _) := a in
          if cfield_dec i f then remove_field f q else a :: remove_field f q
    end.

  Lemma find_remove_field_same : forall f l,
    find_field f (remove_field f l) = None.

  Lemma find_remove_field_other : forall f f',
    f <> f' ->
    forall l,
      find_field f' (remove_field f l) = find_field f' l.


End Find_field.

Module Object.
  Section O.
     
     Record t : Type := make {
       class : ident;
       arraysize : Z
     }.


     Definition new (ci : ident) (size : Z) :=
       make ci size .

 End O.

End Object.

Section Eq_dec.

Variable A : ATOM.t.

Lemma relative_pointer_eq_dec : forall p q :
  (array_path A * Z * (Class.Inheritance.t * list ident)),
{p = q} + {p <> q}.


Lemma pointer_eq_dec : forall p q :
(ident * (array_path A * Z * (Class.Inheritance.t * list ident))),
{p = q} + {p <> q}.

End Eq_dec.


Section Valid_pointer.

Variable A : ATOM.t.
Variables (hierarchy : PTree.t (Class.t A)).

  Section Valid_ptr.
    Variable (heap : PTree.t Object.t).


  Inductive valid_pointer : Value.pointer A -> Prop :=
  | valud_pointer_null : forall id,
    hierarchy ! id <> None ->
    valid_pointer (Value.null A id)
  | valid_pointer_subobject : forall id o,
    PTree.get id (heap ) = Some o ->
    forall ap through z h p to,
      valid_relative_pointer hierarchy (Object.class o) (Object.arraysize o) ap through z h p to ->
      forall hp,
        valid_pointer (Value.subobject id ap z h p hp)
.


   Inductive pointer_array_size : Value.pointer A -> Z -> Prop :=
   | pointer_array_size_nil : forall r o sz z h p hp,
     (heap) ! r = Some o ->
     sz = Object.arraysize o ->
     pointer_array_size (Value.subobject r nil z h p hp) sz
   | pointer_array_size_cons : forall r ap apf kf cf f z h p hp psz,
     ap = apf ++ (kf, f) :: nil ->
     FieldSignature.type f = FieldSignature.Struct cf psz ->
     pointer_array_size (Value.subobject r ap z h p hp) (Zpos psz)
     .


   Function array_index (p : Value.pointer A) (i : Z) : Value.pointer A :=
     match p with
       | Value.subobject ide ap z h p0 hp =>
         (Value.subobject ide ap (z + i) h p0 hp)
       | _ => p
     end.


   Inductive complete_pointer : Value.pointer A -> Prop :=
   | complete_pointer_intro : forall r ap z ci hp,
     complete_pointer (Value.subobject r ap z Class.Inheritance.Repeated (ci :: nil) hp)
       .

   Lemma array_index_complete : forall p,
     complete_pointer p ->
     forall i, complete_pointer (array_index p i).



   Lemma array_index_valid : forall r ap z h p sp,
     valid_pointer (Value.subobject r ap z h p sp) ->
     complete_pointer (Value.subobject r ap z h p sp) ->
     forall sz, pointer_array_size (Value.subobject r ap z h p sp) sz ->
       forall j, 0 <= (z + j) -> z + j < sz ->
       valid_pointer (array_index (Value.subobject r ap z h p sp) j)
       .

End Valid_ptr.

Lemma valid_pointer_preserve : forall obj heap heap', heap' ! obj = heap ! obj -> forall ar i h p hp, valid_pointer heap (Value.subobject obj ar i h p hp) -> valid_pointer heap' (Value.subobject obj ar i h p hp).


End Valid_pointer.


Module Globals.
  Section G.
    Variable A : ATOM.t.


  Record t : Type := make {
    heap : PTree.t (Object.t);
    next_object : positive;
    field_values: list (field_key A * Value.t A)
  }.

  Definition new (h : t) (ci : ident) (arraysize : Z) :=
    ((next_object h), make (PTree.set (next_object h) (Object.new ci arraysize) (heap h)) (Psucc (next_object h)) (field_values h)).

  Definition remove (h : t) (obj : positive) : t :=
    make (PTree.remove obj (heap h)) (next_object h) (field_values h).

  Definition empty :=
    make (PTree.empty (Object.t )) xH nil.

  Definition update (h : t) (l : list (field_key A * Value.t A)) :=
    make (heap h) (next_object h) l
    .


  Record valid (h : t) : Prop := valid_intro {
    valid_none : forall i,
      Ple (next_object h) i -> (heap h) ! i = None
      
  }.


  Lemma valid_new : forall h,
    valid h ->
    forall ci sz r h',
      new h ci sz = (r, h') ->
      valid h'
      .

  Lemma valid_empty : valid empty.

 
  Lemma valid_pointer_new : forall hierarchy he,
    valid he ->
    forall p,
    valid_pointer (A := A) hierarchy (heap he) p ->
    forall ci sz r h',
      new he ci sz = (r, h') ->
      valid_pointer hierarchy (heap h') p
      .

   Lemma valid_pointer_new_recip : forall he,
     valid he ->
     forall ci sz r h',
       new he ci sz = (r, h') ->
       forall hierarchy (p : _ A) ,
       valid_pointer hierarchy (heap h') p ->
       (forall ap' z' h' p' hp', p <> Value.subobject r ap' z' h' p' hp') ->
       valid_pointer hierarchy (heap he) p
       .






   
  Function get_field (fields : list (field_key A * Value.t A)) (f : field_key A) : option (Value.t A) :=
    match f with
      (obj, ap, n, (h, l), fs) =>
      match FieldSignature.type fs with
        | FieldSignature.Scalar ty =>
          match find_field f (fields) with
            | Some (_, v) => Value.check ty v
            | None => None
          end
        | FieldSignature.Struct cl _ => Some (Value.ptr (Value.subobject (obj) (ap ++ (n, (h, l), fs) :: nil) 0 Class.Inheritance.Repeated _ (is_some_last_one_elem cl)))
      end
    end.


  Lemma get_field_type_scalar : forall o ci fs v,
    get_field o (ci, fs) = Some v ->
    forall t,
      FieldSignature.type fs = FieldSignature.Scalar t ->
      t = (Value.type_of v).

  Lemma get_field_type_struct : forall o ci fs v,
    get_field o (ci, fs) = Some v ->
    forall cl n, FieldSignature.type fs = FieldSignature.Struct cl n ->
      Value.type_of v = Typ.class cl.

  Function put_field (fields : list (field_key A * Value.t A)) (cifs : field_key A) (v : Value.t A) : option (list (field_key A * Value.t A)) :=
    let (_, fs) := cifs in
      match FieldSignature.type fs with
        | FieldSignature.Scalar ty =>
          match Value.check ty v with
            | Some v' => Some (update_field cifs v' (fields ))
            | None => None
          end
        | _ => None
      end
      .

  Lemma put_field_type : forall o ci fs v o',
    put_field o (ci, fs) v = Some o' ->
    FieldSignature.type fs = FieldSignature.Scalar (Value.type_of v).

  Lemma get_put_field_other : forall o cifs' v o', put_field o cifs' v = Some o' ->
    forall cifs,
    cifs' <> cifs ->
    get_field o' cifs = get_field o cifs.

  Lemma get_put_field_same : forall o ci0fs0 v o', put_field o ci0fs0 v = Some o' ->
    get_field o' ci0fs0 = Some v.





  End G.
End Globals.

Cast (inspired from Wasserrab et al.)

Section Wasserrab.
  Variable A : ATOM.t.

Domination

Section Domination.

Variable hierarchy : PTree.t (Class.t A).

Inductive dominates (from : ident) (kp1 kp2 : Class.Inheritance.t * list ident) : Prop :=
| dominates_intro : forall k1 p1,
  kp1 = (k1, p1) ->
  forall to1,
    path hierarchy to1 p1 from k1 ->
    forall to2 k p,
      path hierarchy to2 p to1 k ->
      kp2 = concat kp1 (k, p) ->
      dominates from kp1 kp2
      .

Lemma dominates_trans : forall from kp1 kp2,
  dominates from kp1 kp2 ->
  forall kp3,
    dominates from kp2 kp3 ->
    dominates from kp1 kp3
    .

Lemma dominates_refl_weak : forall from to k p,
  path hierarchy to p from k ->
  dominates from (k, p) (k, p).

Lemma dominates_concat_left_0 : forall from from' k' p',
    path hierarchy from p' from' k' ->
    forall k1 p1 k2 p2,
      dominates from (k1, p1) (k2, p2) ->
      forall k'1 p'1,
        (k'1, p'1) = concat (k', p') (k1, p1) ->
        forall k'2 p'2,
          (k'2, p'2) = concat (k', p') (k2, p2) ->
          dominates from' (k'1, p'1) (k'2, p'2)
          .

Lemma dominates_concat_left : forall from from' k' p',
    path hierarchy from p' from' k' ->
    forall k1 p1 k2 p2,
      forall k'1 p'1,
        (k'1, p'1) = concat (k', p') (k1, p1) ->
        forall k'2 p'2,
          (k'2, p'2) = concat (k', p') (k2, p2) ->
          dominates from (k1, p1) (k2, p2) ->
          dominates from' (k'1, p'1) (k'2, p'2)
          .

End Domination.

Dynamic cast

Section Dynamic_cast.


Variable hierarchy : PTree.t (Class.t A).

Variable real : ident.

Variable real_inheritance : Class.Inheritance.t.

Variable real_path : list ident.

Variable from : ident.

Variable cast : ident.

Section Dyncast.

Variable cast_inheritance : Class.Inheritance.t.

Variable cast_path : list ident.

Inductive dynamic_cast : Prop :=
| dynamic_cast_upcast
  (_ : path hierarchy from real_path real real_inheritance)
  k p
  (_ : path hierarchy cast p from k)
  (_ : forall k' p', path hierarchy cast p' from k' -> (k, p) = (k', p'))
  (_ : (cast_inheritance, cast_path) = concat (real_inheritance, real_path) (k, p))
| dynamic_cast_downcast
  (_ : path hierarchy cast cast_path real cast_inheritance)
  p
  (_ : path hierarchy from p cast Class.Inheritance.Repeated)
  (_ : (real_inheritance, real_path) = concat (cast_inheritance, cast_path) (Class.Inheritance.Repeated, p))
| dynamic_cast_crosscast
  (_ : path hierarchy from real_path real real_inheritance)
  (_ : path hierarchy cast cast_path real cast_inheritance)
  (_ : forall k p, path hierarchy cast p real k -> (k, p) = (cast_inheritance, cast_path))
.

Inductive dynamic_cast_aux : nat -> Prop :=
| dynamic_cast_aux_upcast : forall
  (_ : path hierarchy from real_path real real_inheritance)
  k p
  (_ : path hierarchy cast p from k)
  (_ : forall k' p', path hierarchy cast p' from k' -> (k, p) = (k', p'))
  (_ : (cast_inheritance, cast_path) = concat (real_inheritance, real_path) (k, p)),
  dynamic_cast_aux O
| dynamic_cast_aux_downcast : forall
  (_ : path hierarchy cast cast_path real cast_inheritance)
  p
  (_ : path hierarchy from p cast Class.Inheritance.Repeated)
  (_ : (real_inheritance, real_path) = concat (cast_inheritance, cast_path) (Class.Inheritance.Repeated, p)),
  dynamic_cast_aux (S O)
| dynamic_cast_aux_crosscast : forall
  (_ : path hierarchy from real_path real real_inheritance)
  (_ : path hierarchy cast cast_path real cast_inheritance)
  (_ : forall k p, path hierarchy cast p real k -> (k, p) = (cast_inheritance, cast_path)),
  dynamic_cast_aux (S (S O))
.

Lemma dynamic_cast_dynamic_cast_aux :
  dynamic_cast -> exists n,
    dynamic_cast_aux n.


End Dyncast.

End Dynamic_cast.

Static cast

Section Static_cast.

Variable hierarchy : PTree.t (Class.t A).

Variable real : ident.

Variable real_inheritance : Class.Inheritance.t.

Variable real_path : list ident.

Variables from cast : ident.

Section Statcast.

Variable cast_inheritance : Class.Inheritance.t.

Variable cast_path : list ident.

Inductive static_cast : Prop :=
| static_cast_upcast
  (_ : path hierarchy from real_path real real_inheritance)
  k p
  (_ : path hierarchy cast p from k)
  (_ : forall k' p', path hierarchy cast p' from k' -> (k, p) = (k', p'))
  (_ : (cast_inheritance, cast_path) = concat (real_inheritance, real_path) (k, p))
| static_cast_downcast
  (_ : path hierarchy cast cast_path real cast_inheritance)
  p
  (_ : path hierarchy from p cast Class.Inheritance.Repeated)
  (_ : forall p', path hierarchy from p' cast Class.Inheritance.Repeated -> p' = p)
  (_ : (real_inheritance, real_path) = concat (cast_inheritance, cast_path) (Class.Inheritance.Repeated, p))
.

End Statcast.

End Static_cast.

Lemma static_cast_dynamic_cast : forall hierarchy real rh rp from cast ch cp,
  static_cast hierarchy real rh rp from cast ch cp ->
  dynamic_cast hierarchy real rh rp from cast ch cp.
 

Method dispatch (inspired from Wasserrab et al.)

Section Method_dispatch.

Variable hierarchy : PTree.t (Class.t A).

Inductive final_overrider
  (ms : MethodSignature.t A )
  (apparent_class : ident )
  (most_derived : ident )
  (apparent_inheritance : Class.Inheritance.t)
  (apparent_path : list ident )
  (dispatched_inheritance: Class.Inheritance.t)
  (dispatched_path : list ident ) : Prop :=
| final_overrider_intro
    (_ : path hierarchy apparent_class apparent_path most_derived apparent_inheritance)
   apparent_method_class apparent_method_inheritance apparent_method_path
    (_ : path hierarchy apparent_method_class apparent_method_path apparent_class apparent_method_inheritance)
    apparent_method_class_body
    (_ : hierarchy ! apparent_method_class = Some apparent_method_class_body)
    (_ : Method.find ms (Class.methods apparent_method_class_body) <> None)
    (_ : forall to k p,
        path hierarchy to p apparent_class k ->
        forall c, hierarchy ! to = Some c ->
          Method.find ms (Class.methods c) <> None ->
          dominates hierarchy apparent_class (apparent_method_inheritance, apparent_method_path) (k, p))
    k0 p0
    (_ : (k0, p0) = concat (apparent_inheritance, apparent_path) (apparent_method_inheritance, apparent_method_path) )
    dispatched
    (_ : path hierarchy dispatched dispatched_path most_derived dispatched_inheritance)
    (_ : dominates hierarchy most_derived (dispatched_inheritance, dispatched_path) (k0, p0))
    dispatched_body
    (_ : hierarchy ! dispatched = Some dispatched_body)
    (_ : Method.find ms (Class.methods dispatched_body) <> None)
    (_ : forall to k p,
      path hierarchy to p most_derived k ->
      forall c, hierarchy ! to = Some c ->
        Method.find ms (Class.methods c) <> None ->
        dominates hierarchy most_derived (k, p) (dispatched_inheritance, dispatched_path) ->
        (k, p) = (dispatched_inheritance, dispatched_path)
    )
.

Inductive method_dispatch
  (ms : MethodSignature.t A )
  (apparent_class : ident )
  (most_derived : ident )
  (apparent_inheritance : Class.Inheritance.t)
  (apparent_path : list ident )
  (dispatched_inheritance: Class.Inheritance.t)
  (dispatched_path : list ident ) : Prop :=
  method_dispatch_intro
  h p tom
  (_ : path hierarchy tom p apparent_class h)
  tomc
  (_ : hierarchy ! tom = Some tomc)
  m
  (_ : Method.find ms (Class.methods tomc) = Some m)
  (_ : Method.virtual m = true)
  (_ : final_overrider ms apparent_class most_derived apparent_inheritance apparent_path dispatched_inheritance dispatched_path)
  (_ : forall di dp, final_overrider ms apparent_class most_derived apparent_inheritance apparent_path di dp -> (dispatched_inheritance, dispatched_path) = (di, dp))
.



End Method_dispatch.

End Wasserrab.




Section VBorder.

  Variable A : ATOM.t.

  Function vborder_f (l : list ident) (b : ident) : bool :=
    if In_dec peq b l then false else true.

  Function pne (a b : ident) : bool :=
    if peq a b then false else true.

  Variable hier : PTree.t (Class.t A).

  Inductive vborder_list : list (Class.Inheritance.t * ident) -> list ident -> Prop :=
  | vborder_list_nil : vborder_list nil nil
  | vborder_list_cons : forall a c,
    hier ! a = Some c ->
    forall la, vborder_list (Class.super c) la ->
      forall l y, vborder_list l y ->
      forall h y',
        y' = match h with
               | Class.Inheritance.Repeated => y
               | Class.Inheritance.Shared => a :: (filter (pne a) y)
             end ->
        forall z,
          z = la ++ filter (vborder_f la) y' ->
          vborder_list ((h, a) :: l) z
.

  Lemma vborder_list_func : forall l l1,
    vborder_list l l1 ->
    forall l2, vborder_list l l2 ->
      l1 = l2.



   Lemma vborder_no_dup : forall l y,
     vborder_list l y -> NoDup y.

   Definition vborder_list_no_dup := vborder_no_dup.

   Lemma filter_vborder_f_nil : forall y2, (filter (vborder_f nil) y2 = y2).

    Lemma filter_vborder_app : forall l1 l2 l,
      filter (vborder_f (l1 ++ l2)) l = filter (vborder_f l1) (filter (vborder_f l2) l).

    Lemma filter_vborder_compo : forall l1 l2 l,
      filter (vborder_f l1) (filter (vborder_f (filter (vborder_f l1) l2)) l) = filter (vborder_f l1) (filter (vborder_f l2) l).


      Lemma filter_pne_vborder : forall a l,
        filter (pne a) l = filter (vborder_f (a::nil)) l.

  Lemma vborder_list_app_intro : forall l1 y1,
    vborder_list l1 y1 ->
    forall l2 y2,
      vborder_list l2 y2 ->
      vborder_list (l1 ++ l2) (
        y1 ++ filter (vborder_f y1) y2
      ).

  Lemma vborder_list_app_elim : forall l1 l2 y,
    vborder_list (l1 ++ l2) y ->
    (exists y1, vborder_list l1 y1) /\
    (exists y2, vborder_list l2 y2).
  
  Lemma vborder_list_In : forall l y,
    vborder_list l y ->
    forall b, In b y ->
      In (Class.Inheritance.Shared, b) l \/ (
        exists h', exists b', In (h', b') l /\
          exists c', hier ! b' = Some c' /\
            exists y', vborder_list (Class.super c') y' /\
              In b y'
      ).


  Lemma virtual_base_vborder_list : forall a b,
    is_virtual_base_of hier b a ->
    forall c, hier ! a = Some c ->
      forall y, vborder_list (Class.super c) y ->
        In b y.

  Lemma vborder_list_virtual_base : forall a c,
    hier ! a = Some c ->
    forall y,
      vborder_list (Class.super c) y ->
      forall b, In b y ->
        is_virtual_base_of hier b a.
          
   Lemma vborder_list_bases_first : forall l y,
     vborder_list l y ->
     forall b, In b y ->
       forall a, is_virtual_base_of hier a b ->
         list_lt y a b.
      
End VBorder.