Module PreservationAux

Load PreservationHeader.

Lemma stack_objects_sorted :
sorted (fun x y => Plt y x) (stack_objects s2).

Proof.

Lemma unconstructed_scalar_fields : forall obj, (Globals.heap (State.global s2)) ! obj = None -> forall fs ty, FieldSignature.type fs = FieldSignature.Scalar ty -> forall ar i hp, Globals.get_field (Globals.field_values (State.global s2)) (obj, ar, i, hp, fs) = None.

Proof.

Lemma stack_or_deallocated : forall obj, (Globals.heap (State.global s2)) ! obj <> None -> In obj (stack_objects s2) \/ In obj (State.deallocated_objects s2).

Proof.

Lemma deallocated_objects_destructed : forall obj, In obj (State.deallocated_objects s2) -> forall o, (Globals.heap (State.global s2)) ! obj = Some o -> forall i, 0 <= i < Object.arraysize o -> assoc (@pointer_eq_dec _) (obj, (nil, i, (Class.Inheritance.Repeated, Object.class o :: nil))) (State.construction_states s2) = Some Destructed.

Proof.

Lemma deallocated_objects_not_in_stack : forall obj, In obj (stack_objects s2) -> In obj (State.deallocated_objects s2) -> False.

Proof.

Lemma deallocated_objects_exist : forall obj, In obj (State.deallocated_objects s2) -> (Globals.heap (State.global s2)) ! obj <> None.

Proof.

Lemma kind_object_in_construction : forall obj, kind_object (State.kind s2) = Some obj -> exists l', stack_objects s2 = obj :: l'.

Proof.

Lemma stack_objects_in_construction : forall l1 sf l2
  (Hstack : State.stack s2 = l1 ++ sf :: l2)
  obj ar
  (Hframe : frame_array_weak sf = Some (obj, ar)), exists l', stackframe_objects l2 = obj :: l'.

Proof.

Lemma constructed_stack_objects_no_kind : forall obj (Hin : In obj (constructed_stack_objects s2)), kind_object (State.kind s2) = Some obj -> False.

Proof.

Lemma constructed_stack_objects_no_stackframe : forall obj, In obj (constructed_stack_objects s2) -> forall sf, In sf (State.stack s2) -> forall ar, frame_array_weak sf = Some (obj, ar) -> False.

Proof.

Lemma constructed_stack_objects_correct : forall obj, In obj (constructed_stack_objects s2) -> forall o, (Globals.heap (State.global s2)) ! obj = Some o -> forall i, 0 <= i < Object.arraysize o -> assoc (@pointer_eq_dec _) (obj, (nil, i, (Class.Inheritance.Repeated, Object.class o :: nil))) (State.construction_states s2) = Some Constructed.

Proof.

Lemma construction_states_fields_none : forall obj, (Globals.heap (State.global s2)) ! obj = None -> forall ar i hp fs, assoc (aux_constr_state_key_eq_dec ) (obj, ar, i, hp, fs) (State.field_construction_states s2) = None.

Proof.

Lemma stack_objects_no_dup : NoDup (stack_objects s2).

Proof.

Lemma stack_objects_exist :
forall obj, In obj (stack_objects s2) -> (Globals.heap (State.global s2)) ! obj <> None.

Proof.

Lemma valid_global : Globals.valid (State.global s2).

Proof.

Lemma valid_object_classes : forall obj o, (Globals.heap (State.global s2)) ! obj = Some o -> hier ! (Object.class o) <> None.

Proof.

Lemma object_arraysizes_nonnegative : forall obj o, (Globals.heap (State.global s2)) ! obj = Some o -> (0 <= Object.arraysize o)%Z.

Proof.

Lemma stack_state : forall sf l, State.stack s2 = sf :: l -> frame_requires_code sf -> is_code_state (State.kind s2).

Proof.

Lemma construction_states_none : forall obj, (Globals.heap (State.global s2)) ! obj = None -> forall rptr, assoc (@pointer_eq_dec _) (obj, rptr) (State.construction_states s2) = None.

Proof.

End Preservation.