Require Import Relations.
Require Import Coqlib.
Require Import LibPos.
Require Import Maps.
Require Import LibLists.
Require Import Cppsem.
Require Import Cplusconcepts.
Require Import CplusWf.
Require Import Events.
Require Import Smallstep.
Require Import Wellfounded.
Require Import CplusWf.
Require Import Progress.
Require Import Invariant.
Require Import Preservation.
Require Import Constrorder.
Load Param.
Open Scope Z_scope.

POPL 2012 submission: Theorem 3

Section Progress.

Variable A : ATOM.t.
Variable nativeop : Type.

Variable prog : Program.t A nativeop.
Notation hier := (Program.hierarchy prog).

Hypothesis hierarchy_wf : Well_formed_hierarchy.prop hier.

Variable cppsem : cppsemparam.
Variable sem : semparam A nativeop.

Corollary progress : forall cn,
  has_nearly_trivial_constructor prog cppsem sem cn ->
  forall num, (0 < num)%Z ->
    forall s vlocstruct stm vars stl bl stk gl cs auxcs f,
      s = (State.make (State.codepoint vars (Sblock (Some (vlocstruct, cn, num)) (fun _ => Sconstructor cn nil) stm) stl bl) stk gl cs auxcs f) ->
      invariant prog s ->
      exists hp, exists obj, exists gl1,
        (obj, gl1) = Globals.new gl cn num /\
        exists t, exists vars', exists gl', exists cs', exists auxcs',
          star _ (step prog cppsem (sem := sem)) s t
          (State.make (State.codepoint vars' stm nil (BlockPoint.make stl (Some obj) :: bl)) stk gl' cs' auxcs' f) /\
          vars' = PTree.set vlocstruct (Value.ptr (Value.subobject obj nil 0 Class.Inheritance.Repeated (cn :: nil) hp)) vars /\
            (Globals.heap gl') ! obj = (Globals.heap gl1) ! obj /\
            exists o, (Globals.heap gl1) ! obj = Some o /\
              Object.class o = cn /\
              Object.arraysize o = num
              /\
              forall i, 0 <= i < num ->
                assoc (@pointer_eq_dec _) (obj, (nil, i, (Class.Inheritance.Repeated, cn :: nil))) cs' = Some Constructed.

Corollary progress_destr : forall s,
  invariant prog s -> forall gl obj,
    (forall o, (Globals.heap gl) ! obj = Some o -> has_trivial_destructor prog (Object.class o)) ->
    forall sdestruct sdestruct',
      exit_succ sdestruct = Some sdestruct' ->
      forall vars stl0 stl bl stk cs auxcs f,
        s = (State.make (State.codepoint vars sdestruct stl0 (BlockPoint.make stl (Some obj) :: bl)) stk gl cs auxcs f) ->
        exists gl', exists cs', exists auxcs',
          star _ (step prog cppsem (sem := sem))
          s E0
          (State.make (State.codepoint vars sdestruct' stl bl) stk gl' cs' auxcs' (obj :: f)) /\ (Globals.heap gl') ! obj = (Globals.heap gl) ! obj /\
          exists o,
            (Globals.heap gl) ! obj = Some o /\
            forall i, 0 <= i < Object.arraysize o ->
              assoc (@pointer_eq_dec _) (obj, (nil, i, (Class.Inheritance.Repeated, Object.class o :: nil))) cs' = Some Destructed.
 
End Progress.