Require Import Syntax Notations Helpers Typing Subtyping Bigstep ViewpointAdaptation. From Stdlib Require Import List. From Stdlib Require String. Import ListNotations. Ltac solve_q_subtype_wrong := lazymatch goal with | [ H : q_subtype RO Imm |- _ ] => exfalso; inversion H; subst; congruence | [ H : q_subtype RO Mut |- _ ] => exfalso; inversion H; subst; congruence | [ H : q_subtype RO RDM |- _ ] => exfalso; inversion H; subst; congruence | [ H : q_subtype RO Lost |- _ ] => exfalso; inversion H; subst; congruence | [ H : q_subtype RO Bot |- _ ] => exfalso; inversion H; subst; congruence | [ H : q_subtype Imm Mut |- _ ] => exfalso; inversion H; subst; congruence | [ H : q_subtype Imm RDM |- _ ] => exfalso; inversion H; subst; congruence | [ H : q_subtype Imm Lost |- _ ] => exfalso; inversion H; subst; congruence | [ H : q_subtype Imm Bot |- _ ] => exfalso; inversion H; subst; congruence | [ H : q_subtype Mut Imm |- _ ] => exfalso; inversion H; subst; congruence | [ H : q_subtype Mut RDM |- _ ] => exfalso; inversion H; subst; congruence | [ H : q_subtype Mut Lost |- _ ] => exfalso; inversion H; subst; congruence | [ H : q_subtype Mut Bot |- _ ] => exfalso; inversion H; subst; congruence | [ H : q_subtype RDM Imm |- _ ] => exfalso; inversion H; subst; congruence | [ H : q_subtype RDM Mut |- _ ] => exfalso; inversion H; subst; congruence | [ H : q_subtype RDM Lost |- _ ] => exfalso; inversion H; subst; congruence | [ H : q_subtype RDM Bot |- _ ] => exfalso; inversion H; subst; congruence | [ H : q_subtype Lost Lost |- _ ] => exfalso; inversion H; subst; congruence | [ H : q_subtype Lost Imm |- _ ] => exfalso; inversion H; subst; congruence | [ H : q_subtype Lost Mut |- _ ] => exfalso; inversion H; subst; congruence | [ H : q_subtype Lost RDM |- _ ] => exfalso; inversion H; subst; congruence | [ H : q_subtype Lost Bot |- _ ] => exfalso; inversion H; subst; congruence | _ => idtac end. Local Ltac qtypable_contradiction H := exfalso; unfold qualifier_typable_context, vpa_mutability_runtime in H; cbn in H; contradiction H. Ltac solve_qualifier_typable_wrong_concrete := lazymatch goal with | [ H : qualifier_typable_context Imm_r Mut Mut_r |- _ ] => qtypable_contradiction H | [ H : qualifier_typable_context Imm_r RDM Mut_r |- _ ] => qtypable_contradiction H | [ H : qualifier_typable_context Imm_r Bot Mut_r |- _ ] => qtypable_contradiction H | [ H : qualifier_typable_context Imm_r Mut Imm_r |- _ ] => qtypable_contradiction H | [ H : qualifier_typable_context Imm_r Bot Imm_r |- _ ] => qtypable_contradiction H | [ H : qualifier_typable_context Mut_r Imm Mut_r |- _ ] => qtypable_contradiction H | [ H : qualifier_typable_context Mut_r Bot Mut_r |- _ ] => qtypable_contradiction H | [ H : qualifier_typable_context Mut_r Imm Imm_r |- _ ] => qtypable_contradiction H | [ H : qualifier_typable_context Mut_r RDM Imm_r |- _ ] => qtypable_contradiction H | [ H : qualifier_typable_context Mut_r Bot Imm_r |- _ ] => qtypable_contradiction H | [ H : qualifier_typable_context Imm_r Imm Mut_r |- _ ] => clear H | [ H : qualifier_typable_context Imm_r RO Mut_r |- _ ] => clear H | [ H : qualifier_typable_context Imm_r Lost Mut_r |- _ ] => clear H | [ H : qualifier_typable_context Imm_r RO Imm_r |- _ ] => clear H | [ H : qualifier_typable_context Imm_r Imm Imm_r |- _ ] => clear H | [ H : qualifier_typable_context Imm_r Lost Imm_r |- _ ] => clear H | [ H : qualifier_typable_context Imm_r RDM Imm_r |- _ ] => clear H | [ H : qualifier_typable_context Mut_r Mut Mut_r |- _ ] => clear H | [ H : qualifier_typable_context Mut_r RO Mut_r |- _ ] => clear H | [ H : qualifier_typable_context Mut_r Lost Mut_r |- _ ] => clear H | [ H : qualifier_typable_context Mut_r RDM Mut_r |- _ ] => clear H | [ H : qualifier_typable_context Mut_r RO Imm_r |- _ ] => clear H | [ H : qualifier_typable_context Mut_r Mut Imm_r |- _ ] => clear H | [ H : qualifier_typable_context Mut_r Lost Imm_r |- _ ] => clear H | _ => idtac end. Ltac solve_qualifier_typable_correct_concrete := lazymatch goal with | |- qualifier_typable_context Imm_r Imm Mut_r => unfold qualifier_typable_context, vpa_mutability_runtime; cbn; exact I | |- qualifier_typable_context Imm_r RO Mut_r => unfold qualifier_typable_context, vpa_mutability_runtime; cbn; exact I | |- qualifier_typable_context Imm_r Lost Mut_r => unfold qualifier_typable_context, vpa_mutability_runtime; cbn; exact I | |- qualifier_typable_context Imm_r RO Imm_r => unfold qualifier_typable_context, vpa_mutability_runtime; cbn; exact I | |- qualifier_typable_context Imm_r Imm Imm_r => unfold qualifier_typable_context, vpa_mutability_runtime; cbn; exact I | |- qualifier_typable_context Imm_r Lost Imm_r => unfold qualifier_typable_context, vpa_mutability_runtime; cbn; exact I | |- qualifier_typable_context Imm_r RDM Imm_r => unfold qualifier_typable_context, vpa_mutability_runtime; cbn; exact I | |- qualifier_typable_context Mut_r Mut Mut_r => unfold qualifier_typable_context, vpa_mutability_runtime; cbn; exact I | |- qualifier_typable_context Mut_r RO Mut_r => unfold qualifier_typable_context, vpa_mutability_runtime; cbn; exact I | |- qualifier_typable_context Mut_r Lost Mut_r => unfold qualifier_typable_context, vpa_mutability_runtime; cbn; exact I | |- qualifier_typable_context Mut_r RDM Mut_r => unfold qualifier_typable_context, vpa_mutability_runtime; cbn; exact I | |- qualifier_typable_context Mut_r RO Imm_r => unfold qualifier_typable_context, vpa_mutability_runtime; cbn; exact I | |- qualifier_typable_context Mut_r Mut Imm_r => unfold qualifier_typable_context, vpa_mutability_runtime; cbn; exact I | |- qualifier_typable_context Mut_r Lost Imm_r => unfold qualifier_typable_context, vpa_mutability_runtime; cbn; exact I end. Lemma method_body_well_typed_by_find : forall CT C m mdef (Hwf_ct : wf_class_table CT) (Hdom : C < dom CT) (Hlookup : FindMethodWithName CT C m mdef), exists sΓ', stmt_typing CT (mreceiver (msignature mdef) :: mparams (msignature mdef)) mdef.(msignature).(mscope) (mbody_stmt (mbody mdef)) sΓ'. Proof. intros CT C m mdef Hwf_ct Hdom Hlookup. assert (Hexists_class : exists class_def, find_class CT C = Some class_def). { apply find_class_Some. exact Hdom. } destruct Hexists_class as [class_def Hfind_class]. assert (Hwf_class : wf_class CT class_def). { unfold wf_class_table in Hwf_ct. destruct Hwf_ct as [Hforall_wf _]. eapply Forall_nth_error; eauto. } assert (Hcname_eq : cname (signature class_def) = C). { unfold wf_class_table in Hwf_ct. destruct Hwf_ct as [_ [_ Hcname_consistent]]. destruct Hcname_consistent as [_ Hcname_eq]. apply Hcname_eq. exact Hfind_class. } assert (Hwf_inherited : exists D ddef, base_subtype CT C D /\ find_class CT D = Some ddef /\ In mdef (methods (body ddef)) /\ wf_method CT D mdef). { eapply method_lookup_in_wellformed_inherited; eauto. } destruct Hwf_inherited as [D [ddef [Hsub [Hfind_D [Hin_D Hwf_D]]]]]. (* Extract the statement typing from wf_method *) unfold wf_method in Hwf_D; simpl in Hwf_D. destruct Hwf_D as [_ [sΓ' [mbodyrettype [Htyping _]]]]. exists sΓ'. exact Htyping. Qed. Lemma wf_method_sig_types : forall CT C mdef (Hwf_method : wf_method CT C mdef), wf_stypeuse CT (sqtype (mreceiver (msignature mdef))) (sctype (mreceiver (msignature mdef))) /\ Forall (fun T => wf_stypeuse CT (sqtype T) (sctype T)) (mparams (msignature mdef)). Proof. intros CT C mdef Hwf_method. unfold wf_method in Hwf_method; simpl in Hwf_method. destruct Hwf_method as [_ [sΓ' [mbodyrettype [Htyping _]]]]. assert (Hwf_env : wf_senv CT (mreceiver (msignature mdef) :: mparams (msignature mdef))). { eapply stmt_typing_wf_env; eauto. } (* unfold sΓ, msig in Hwf_env. *) inversion Hwf_env; subst. split. - (* Receiver well-formedness *) apply Forall_inv in H0. exact H0. - (* Parameters well-formedness *) apply Forall_inv_tail in H0. exact H0. Qed. Lemma method_sig_wf_receiver_by_find : forall CT C m mdef (Hwf_ct : wf_class_table CT) (Hdom : C < dom CT) (Hlookup : FindMethodWithName CT C m mdef), wf_stypeuse CT (sqtype (mreceiver (msignature mdef))) (sctype (mreceiver (msignature mdef))). Proof. intros CT C m mdef Hwf_ct Hdom Hlookup. assert (Hwf_inherited : exists D ddef, base_subtype CT C D /\ find_class CT D = Some ddef /\ In mdef (methods (body ddef)) /\ wf_method CT D mdef). { eapply method_lookup_in_wellformed_inherited; eauto. } destruct Hwf_inherited as [D [ddef [Hsub [Hfind_D [Hin_D Hwf_D]]]]]. eapply wf_method_sig_types; eauto. Qed. Lemma method_sig_wf_parameters_by_find : forall CT C m mdef (Hwf_ct : wf_class_table CT) (Hdom : C < dom CT) (Hlookup : FindMethodWithName CT C m mdef), Forall (fun T => wf_stypeuse CT (sqtype T) (sctype T)) (mparams (msignature mdef)). Proof. intros CT C m mdef Hwf_ct Hdom Hlookup. assert (Hwf_inherited : exists D ddef, base_subtype CT C D /\ find_class CT D = Some ddef /\ In mdef (methods (body ddef)) /\ wf_method CT D mdef). { eapply method_lookup_in_wellformed_inherited; eauto. } destruct Hwf_inherited as [D [ddef [Hsub [Hfind_D [Hin_D Hwf_D]]]]]. eapply wf_method_sig_types; eauto. Qed. Lemma constructor_params_field_count : forall CT C ctor csig fields (Hwf_ct : wf_class_table CT) (Hdom : C < dom CT) (Hctor_lookup : constructor_def_lookup CT C = Some ctor) (Hcsig : csig = csignature ctor) (Hcollect : CollectFields CT C fields), List.length (cparams csig) = List.length fields. Proof. intros CT C ctor csig fields Hwf_ct Hdom Hctor_lookup Hcsig Hcollect. subst csig. (* Move the quantified variables inside the induction *) revert ctor fields Hctor_lookup Hcollect. (* Strong induction on C *) induction C as [C IH] using lt_wf_ind. intros ctor fields Hctor_lookup Hcollect. (* Get the class definition *) assert (Hclass_exists : exists cdef, find_class CT C = Some cdef). { apply nth_error_Some_exists. exact Hdom. } destruct Hclass_exists as [cdef Hfind_class]. (* Extract well-formedness of the class *) assert (Hwf_class : wf_class CT cdef). { unfold wf_class_table in Hwf_ct. destruct Hwf_ct as [Hforall_wf _]. eapply Forall_nth_error; eauto. } (* Extract constructor well-formedness *) assert (Hctor_eq : constructor (body cdef) = ctor). { unfold constructor_def_lookup in Hctor_lookup. rewrite Hfind_class in Hctor_lookup. injection Hctor_lookup as Hctor_eq. exact Hctor_eq. } (* Case analysis on class structure *) inversion Hwf_class; subst. - (* Object class case *) inversion Hcollect; subst. destruct (find_class CT C). easy. easy. unfold wf_constructor_object in Hwf_ctor. destruct Hwf_ctor as [_ [_ Hcparams]]. destruct Hcparams as [_ [Hcparams _]]. rewrite Hcparams. reflexivity. exfalso. assert (cdef = def) by (rewrite Hfind_class in Hfind; injection Hfind; auto). subst def. rewrite Hsuper in Hno_super. discriminate. - (* Regular class case with superclass *) destruct H as [Hwf_ctor [Hnodup_methods [Hforall_methods Hforall_fields]]]. (* Extract class name consistency *) assert (Hcname_eq : cname sig = C). { apply find_class_cname_consistent in Hfind_class; auto. } unfold wf_constructor in Hwf_ctor. subst C0. destruct Hwf_ctor as [_ [_ [field_defs [Hcollect_field_defs [Hparams_eq _]]]]]. assert (field_defs = fields). { eapply collect_fields_deterministic_rel; eauto. rewrite Hcname_eq. exact Hcollect. } subst field_defs. exact Hparams_eq. Qed. Lemma constructor_lookup_wf : forall CT C ctor (Hwf_ct : wf_class_table CT) (Hdom : C < dom CT) (Hctor_lookup : constructor_sig_lookup CT C = Some ctor), wf_constructor CT C ctor. Proof. intros CT C ctor Hwf_ct Hdom Hctor_lookup. assert (Hexists_class : exists cdef, find_class CT C = Some cdef). { apply find_class_Some. exact Hdom. } destruct Hexists_class as [cdef Hfind_class]. assert (Hwf_class : wf_class CT cdef). { unfold wf_class_table in Hwf_ct. destruct Hwf_ct as [Hforall_wf _]. eapply Forall_nth_error; eauto. } inversion Hwf_class; subst. unfold wf_constructor. unfold wf_constructor. unfold wf_constructor_object in Hwf_ctor. destruct Hwf_ctor as [Hbound [H2314 [Hcparams [Hcollect_fields H2341]]]]. assert (Hcname: cname (signature cdef) = C). { eapply find_class_cname_consistent; eauto. } unfold constructor_sig_lookup in Hctor_lookup. unfold constructor_def_lookup in Hctor_lookup. rewrite Hfind_class in Hctor_lookup. injection Hctor_lookup as Hctor_eq. subst ctor. simpl. repeat split. - rewrite Hcname in Hcparams. symmetry. exact Hcparams. - rewrite Hcollect_fields. constructor. - exists (@nil field_def). split. -- rewrite Hcname in H2341. exact H2341. -- split. + rewrite Hcollect_fields. reflexivity. + rewrite Hcollect_fields. constructor. - destruct H as [Hwf_ctor _]. assert (C0 = C) by (unfold C0; eapply find_class_cname_consistent; eauto). subst C0. unfold constructor_sig_lookup in Hctor_lookup. unfold constructor_def_lookup in Hctor_lookup. rewrite Hfind_class in Hctor_lookup. injection Hctor_lookup as Hctor_eq. rewrite <- Hctor_eq. fold bod. rewrite <- H. exact Hwf_ctor. Qed. Lemma eval_stmt_preserves_heap_domain_simple : forall CT rΓ h stmt rΓ' h' (Heval : eval_stmt CT rΓ h stmt OK rΓ' h'), dom h <= dom h'. Proof. intros CT rΓ h stmt rΓ' h' Heval. remember OK as ok. induction Heval; try reflexivity; try discriminate. - (* FldWrite: h' = update_field h lx f v2 *) rewrite Hupdate. unfold update_field. rewrite Hobj. rewrite update_length. reflexivity. - (* New: h' = h ++ [new_obj] *) rewrite Hheap. rewrite length_app. simpl. lia. - (* Call: use IH *) apply IHHeval. reflexivity. - (* Seq: transitivity *) apply Nat.le_trans with (dom h'). + apply IHHeval1. reflexivity. + apply IHHeval2. reflexivity. Qed. Lemma runtime_getObj_app_left : forall h h_ext loc obj (Hloc_dom : loc < dom h) (Hobj : runtime_getObj h loc = Some obj), runtime_getObj (h ++ [h_ext]) loc = Some obj. Proof. intros h h_ext loc obj Hloc_dom Hobj. unfold runtime_getObj in *. rewrite nth_error_app1. - exact Hloc_dom. - exact Hobj. Qed. (* Not just length, there is no statement can do strong update. *) Lemma eval_stmt_preserves_r_type : forall CT rΓ h stmt rΓ' h' loc rqt (Heval : eval_stmt CT rΓ h stmt OK rΓ' h') (Hrtype : r_type h loc = Some rqt) (Hloc_dom : loc < dom h), r_type h' loc = Some rqt. Proof. intros CT rΓ h stmt rΓ' h' loc rqt Heval Hrtype Hloc_dom. remember OK as ok. induction Heval; try discriminate; try (subst; exact Hrtype). - (* FldWrite: only fields change, not type *) subst h'. unfold r_type in Hrtype |- *. unfold update_field. destruct (runtime_getObj h loc_x) as [ox|] eqn:Hlx; [|exact Hrtype]. destruct (Nat.eq_dec loc loc_x) as [Heq|Hneq]. + (* loc = lx: type preserved *) subst loc. rewrite runtime_getObj_update_same. * apply runtime_getObj_dom in Hlx. exact Hlx. * simpl. unfold r_type in Hrtype. rewrite Hlx in Hrtype. exact Hrtype. + (* loc ≠ lx: unchanged *) rewrite runtime_getObj_update_diff. * symmetry. exact Hneq. * exact Hrtype. - (* New: existing objects unchanged *) subst h'. unfold r_type in Hrtype |- *. destruct (runtime_getObj h loc) as [obj_loc|] eqn:Hobj_loc; [|discriminate]. injection Hrtype as Hrtype_eq. subst rqt. erewrite runtime_getObj_app_left; eauto. - (* Call: use IH *) eapply IHHeval; eauto. - (* Seq: transitivity *) assert (Hloc_dom' : loc < dom h'). { have Hdom_le := eval_stmt_preserves_heap_domain_simple CT rΓ h s1 rΓ' h' Heval1. lia. } assert (Hrtype' : r_type h' loc = Some rqt). { eapply IHHeval1; eauto. } eapply IHHeval2; eauto. Qed. Lemma eval_stmt_preserves_r_muttype : forall CT rΓ h stmt rΓ' h' loc q (Heval : eval_stmt CT rΓ h stmt OK rΓ' h') (Hmut : r_muttype h loc = Some q) (Hloc_dom : loc < dom h), r_muttype h' loc = Some q. Proof. intros CT rΓ h stmt rΓ' h' loc q Heval Hmut Hloc_dom. remember OK as ok. induction Heval; try discriminate; try (subst; exact Hmut). - (* FldWrite: only fields change, not mutability type *) subst h'. unfold update_field. destruct (runtime_getObj h loc_x) as [ox|] eqn:Hlx; [|exact Hmut]. destruct (Nat.eq_dec loc loc_x) as [Heq|Hneq]. + (* loc = lx: mutability type preserved *) subst loc. unfold r_muttype in Hmut |- *. unfold update_field. injection Hobj as H0_eq. subst ox. rewrite runtime_getObj_update_same. * exact Hloc_dom. * simpl. rewrite Hlx in Hmut. exact Hmut. + (* loc ≠ lx: unchanged *) unfold r_muttype in Hmut |- *. unfold update_field. injection Hobj as H0_eq. subst ox. rewrite runtime_getObj_update_diff. * symmetry. exact Hneq. * exact Hmut. - (* New: existing objects unchanged *) subst h'. destruct (runtime_getObj h loc) as [obj_loc|] eqn:Hobj_loc. 2:{ unfold r_muttype in Hmut. rewrite Hobj_loc in Hmut. discriminate Hmut. } unfold r_muttype in Hmut |- *. rewrite Hobj_loc in Hmut. injection Hmut as Hmut_eq. subst q. erewrite runtime_getObj_app_left; eauto. - (* Call: use IH *) eapply IHHeval; eauto. - (* Seq: transitivity *) assert (Hloc_dom' : loc < dom h'). { have Hdom_le := eval_stmt_preserves_heap_domain_simple CT rΓ h s1 rΓ' h' Heval1. lia. } assert (Hmut' : r_muttype h' loc = Some q). { eapply IHHeval1; eauto. } eapply IHHeval2; eauto. Qed. Lemma r_basetype_in_dom : forall CT h loc cy (Hwf_heap : wf_heap CT h) (Hr_basetype : r_basetype h loc = Some cy), cy < dom CT. Proof. intros CT h loc cy Hwf_heap Hr_basetype. unfold r_basetype in Hr_basetype. destruct (runtime_getObj h loc) as [obj|] eqn:Hobj; [|discriminate]. injection Hr_basetype as Heq. subst cy. destruct obj as [rt_obj fields_obj]. destruct rt_obj as [rq_obj rc_obj]. simpl. unfold wf_heap in Hwf_heap. assert (Hloc_dom : loc < dom h) by (apply runtime_getObj_dom in Hobj; exact Hobj). specialize (Hwf_heap loc Hloc_dom). unfold wf_obj in Hwf_heap. rewrite Hobj in Hwf_heap. destruct Hwf_heap as [Hwf_rtypeuse _]. unfold wf_rtypeuse in Hwf_rtypeuse. simpl in Hwf_rtypeuse. destruct (bound CT rc_obj) as [qc|] eqn:Hbound. - destruct Hwf_rtypeuse as [Hwf_rtypeuse _]. exact Hwf_rtypeuse. - contradiction. Qed. Lemma sq_vpa_tt_eq_qq_abstract_state : forall T1 T2, sqtype (vpa_mutability_tt_abstract_state T1 T2) = vpa_mutability_qq_abstract_state (sqtype T1) (sqtype T2). Proof. intros T1 T2. destruct T1 as [q1 c1], T2 as [q2 c2]. unfold vpa_mutability_tt_abstract_state, vpa_mutability_qq_abstract_state. simpl. destruct q1; destruct q2; reflexivity. Qed. Lemma sq_vpa_tt_eq_qq_readonly_state : forall T1 T2, sqtype (vpa_mutability_tt_readonly_state T1 T2) = vpa_mutability_qq_readonly_state (sqtype T1) (sqtype T2). Proof. intros T1 T2. destruct T1 as [q1 c1], T2 as [q2 c2]. unfold vpa_mutability_tt_readonly_state, vpa_mutability_qq_readonly_state. simpl. destruct q1; destruct q2; reflexivity. Qed. Lemma collect_fields_consistent_through_runtime_static : forall CT C D fields1 fields2 f fdef1 fdef2 (Hwf_ct : wf_class_table CT) (Hsub : base_subtype CT C D) (Hcf1 : CollectFields CT C fields1) (Hcf2 : CollectFields CT D fields2) (Hget1 : gget fields1 f = Some fdef1) (Hget2 : gget fields2 f = Some fdef2), fdef1 = fdef2. Proof. intros CT C D fields1 fields2 f fdef1 fdef2 Hwf_ct Hsub Hcf1 Hcf2 Hget1 Hget2. (* Generalize everything that varies *) revert fields1 fields2 f fdef1 fdef2 Hcf1 Hcf2 Hget1 Hget2. (* Now induct on Hsub *) induction Hsub; intros fields1 fields2 f fdef1 fdef2 Hcf1 Hcf2 Hget1 Hget2. - (* Reflexive: C = D *) assert (fields1 = fields2) by (eapply collect_fields_deterministic_rel; eauto). subst fields2. congruence. - (* Transitive: C <: D <: E *) (* Get fields for D *) assert (Hexists_D : exists fields_D, CollectFields CT D fields_D). { (* D must be in CT domain since D <: E *) assert (HD_dom : D < dom CT). { eapply base_subtype_domain; eauto. } (* Use collect_fields_exists *) eapply collect_fields_exists; eauto. } destruct Hexists_D as [fields_D HcfD]. (* Get field at f in D *) assert (Hget_D : exists fdef_D, gget fields_D f = Some fdef_D). { assert (Hlookup_E : FieldLookup CT E f fdef2). { apply FL_Found with fields2; auto. } assert (Hlookup_D : FieldLookup CT D f fdef2). { apply (field_inheritance_subtyping CT D E f fdef2); auto. } inversion Hlookup_D as [? ? fields_D' ? ? HcfD' HgetD']. assert (fields_D = fields_D') by (eapply collect_fields_deterministic_rel; eauto). subst fields_D'. exists fdef2. exact HgetD'. } destruct Hget_D as [fdef_D HgetD]. (* Apply IH1: C <: D *) assert (fdef1 = fdef_D) by (eapply IHHsub1; eauto). (* Apply IH2: D <: E *) assert (fdef_D = fdef2) by (eapply IHHsub2; eauto). congruence. - assert (Hlookup1 : FieldLookup CT C f fdef1). { apply FL_Found with fields1; auto. } assert (Hlookup2 : FieldLookup CT D f fdef2). { apply FL_Found with fields2; auto. } assert (Hlookup_in_C : FieldLookup CT C f fdef2). { unfold parent_lookup in Hparent. destruct (find_class CT C) as [def|] eqn:Hfind; [|discriminate]. eapply field_inheritance_preserves_type; eauto. } eapply field_lookup_deterministic_rel; eauto. Qed. Lemma sf_assignability_consistent_subtype : forall CT C D f a1 a2 (Hwf_ct : wf_class_table CT) (Hsub : base_subtype CT C D) (Ha1 : sf_assignability_rel CT C f a1) (Ha2 : sf_assignability_rel CT D f a2), a1 = a2. Proof. intros CT C D f a1 a2 Hwf_ct Hsub Ha1 Ha2. unfold sf_assignability_rel in *. destruct Ha1 as [fdef1 [Hlookup1 Hassign1]]. destruct Ha2 as [fdef2 [Hlookup2 Hassign2]]. inversion Hlookup1 as [? ? fields1 ? ? Hcf1 Hget1]; subst. inversion Hlookup2 as [? ? fields2 ? ? Hcf2 Hget2]; subst. assert (fdef1 = fdef2) by (eapply collect_fields_consistent_through_runtime_static; eauto). subst. congruence. Qed. Lemma correspondence_to_typable : forall CT sΓ rΓ h i sqt loc ι qcontext (Hreceiveraddr : get_this_var_mapping (vars rΓ) = Some ι) (Hreceiverrmut : (r_muttype h ι) = Some qcontext) (Hcorr : forall i : nat, i < dom sΓ -> forall sqt : qualified_type, nth_error sΓ i = Some sqt -> match runtime_getVal rΓ i with | Some Null_a => True | Some (Iot loc) => wf_r_typable CT h loc sqt qcontext | None => False end) (Hi : i < dom sΓ) (Hnth : nth_error sΓ i = Some sqt) (Hval : runtime_getVal rΓ i = Some (Iot loc)), wf_r_typable CT h loc sqt qcontext. Proof. intros CT sΓ rΓ h i sqt loc ι qcontext Hreceiveraddr Hreceiverrmut Hcorr Hi Hnth Hval. specialize (Hcorr i Hi sqt Hnth). rewrite Hval in Hcorr. exact Hcorr. Qed. Lemma Forall2_from_nth : forall {A B} (P : A -> B -> Prop) l1 l2 (Hlen : List.length l1 = List.length l2) (Hprop : forall i a b, i < List.length l1 -> nth_error l1 i = Some a -> nth_error l2 i = Some b -> P a b), Forall2 P l1 l2. Proof. intros A B P l1 l2 Hlen Hprop. generalize dependent l2. induction l1 as [|a1 l1' IH]; intros l2 Hlen Hprop. - (* Base case: l1 = [] *) destruct l2; [constructor | discriminate]. - (* Inductive case: l1 = a1 :: l1' *) destruct l2 as [|a2 l2']; [discriminate|]. constructor. + (* Show P a1 a2 *) specialize (Hprop 0 a1 a2). apply Hprop. -- simpl. lia. -- reflexivity. -- reflexivity. + (* Show Forall2 P l1' l2' *) apply IH. * simpl in Hlen. lia. * intros i a b Hi Ha Hb. apply Hprop with (S i); [simpl; lia | exact Ha | exact Hb]. Qed. Lemma get_this_var_mapping_update_nonzero : forall vs x v (Hx : x <> 0), get_this_var_mapping (update x v vs) = get_this_var_mapping vs. Proof. intros vs x v Hx. unfold get_this_var_mapping. destruct vs as [|v0 vs']; simpl. - (* vs = [] *) destruct x as [|x']; [contradiction|]. simpl. reflexivity. - (* vs = v0 :: vs' *) destruct x as [|x']; [contradiction|]. simpl. reflexivity. Qed. Lemma get_this_var_mapping_update_vars_nonzero : forall rΓ x v (Hx : x <> 0), get_this_var_mapping (vars (set_vars rΓ (update x v (vars rΓ)))) = get_this_var_mapping (vars rΓ). Proof. intros rΓ x v Hx. simpl. apply get_this_var_mapping_update_nonzero. exact Hx. Qed. Lemma eval_stmt_preserves_receiver_addr_typed : forall CT sΓ mt rΓ h stmt sΓ' rΓ' h' ι (Htyp : stmt_typing CT sΓ mt stmt sΓ') (Heval : eval_stmt CT rΓ h stmt OK rΓ' h') (Hthis : get_this_var_mapping (vars rΓ) = Some ι), get_this_var_mapping (vars rΓ') = Some ι. Proof. intros CT sΓ mt rΓ h stmt sΓ' rΓ' h' ι Htyp Heval Hthis. remember OK as ok eqn:Hok. revert sΓ sΓ' Htyp Hthis. induction Heval; intros sΓ sΓ' Htyp Hthis'; subst; try discriminate; inversion Htyp; subst; simpl in *. - (* Skip *) assumption. - (* Local: vars rΓ' = vars rΓ ++ [Null_a] *) (* Updating rΓ's vars projection just adds at the tail. *) simpl. unfold get_this_var_mapping in *. destruct (vars rΓ) as [|v0 vs]; [discriminate|]. (* head unchanged *) assumption. - (* VarAss x e *) simpl. destruct x as [|x']; simpl in *. + exfalso. (* from the typing rule: x <> 0 *) easy. + (* x = S x' *) destruct (vars rΓ) as [|h0 l'] eqn:Hvars; simpl in *. * (* vars rΓ = [] *) (* Impossible, since Hthis = Some ι *) unfold get_this_var_mapping in Hthis. simpl in Hthis. discriminate. * (* vars rΓ = h0 :: l' *) exact Hthis'. - (* FldWrite *) assumption. - (* FldWrite *) assumption. - (* FldWrite *) assumption. - (* FldWrite — TransitiveState *) assumption. - (* New x q c ys *) simpl. destruct x as [|x']; simpl in *. + (* x = 0 is forbidden by typing (H10 : x <> 0) *) exfalso. easy. + (* non-zero index update does not change 'this' *) destruct (vars rΓ) as [|h0 l'] eqn:Hvars; simpl in *. * (* vars rΓ = [] *) (* Impossible, since Hthis = Some ι *) unfold get_this_var_mapping in Hthis. simpl in Hthis. discriminate. * (* vars rΓ = h0 :: l' *) exact Hthis'. - (* Call x m y zs *) simpl. destruct x as [|x']; simpl in *. + (* x = 0 is forbidden by typing (H10 : x <> 0) *) exfalso. easy. + (* non-zero index update does not change 'this' *) destruct (vars rΓ) as [|h0 l'] eqn:Hvars; simpl in *. * (* vars rΓ = [] *) (* Impossible, since Hthis = Some ι *) unfold get_this_var_mapping in Hthis. simpl in Hthis. discriminate. * (* vars rΓ = h0 :: l' *) exact Hthis'. - (* Call x m y zs *) simpl. destruct x as [|x']; simpl in *. + (* x = 0 is forbidden by typing (H10 : x <> 0) *) exfalso. easy. + (* non-zero index update does not change 'this' *) destruct (vars rΓ) as [|h0 l'] eqn:Hvars; simpl in *. * (* vars rΓ = [] *) (* Impossible, since Hthis = Some ι *) unfold get_this_var_mapping in Hthis. simpl in Hthis. discriminate. * (* vars rΓ = h0 :: l' *) exact Hthis'. - (* Seq s1 s2 *) eapply IHHeval2; eauto. Qed. Lemma eval_stmt_preserves_receiver_addr_typed_backwards : forall CT sΓ mt rΓ h stmt sΓ' rΓ' h' ι (Hwf : wf_r_config CT sΓ rΓ h) (Htyp : stmt_typing CT sΓ mt stmt sΓ') (Heval : eval_stmt CT rΓ h stmt OK rΓ' h') (Hthis' : get_this_var_mapping (vars rΓ') = Some ι), get_this_var_mapping (vars rΓ) = Some ι. Proof. intros CT sΓ mt rΓ h stmt sΓ' rΓ' h' ι Hwf Htyp Heval Hthis'. assert (Hthis : exists ι0, get_this_var_mapping (vars rΓ) = Some ι0). { unfold wf_r_config in Hwf. destruct Hwf as [_ [_ [Hrenv _]]]. destruct Hrenv as [Hlen [Hreceiverval _]]. destruct Hreceiverval as [ι0 Hthis0]. exists ι0. destruct Hthis0 as [Hthis0 Hthisldom]. exact Hthis0. } destruct Hthis as [ι0 Hthis0]. (* forward preservation gives 'ι0' also at the end *) pose proof (eval_stmt_preserves_receiver_addr_typed CT sΓ mt rΓ h stmt sΓ' rΓ' h' ι0 Htyp Heval Hthis0) as Hthis0'. (* uniqueness of Some _ *) rewrite Hthis' in Hthis0'. inversion Hthis0'; subst ι0. assumption. Qed. Lemma eval_stmt_preserves_receiver_addr_mapping_eq : forall CT sΓ mt rΓ h stmt sΓ' rΓ' h' (Hwf : wf_r_config CT sΓ rΓ h) (Htyp : stmt_typing CT sΓ mt stmt sΓ') (Heval : eval_stmt CT rΓ h stmt OK rΓ' h'), get_this_var_mapping (vars rΓ) = get_this_var_mapping (vars rΓ'). Proof. intros CT sΓ mt rΓ h stmt sΓ' rΓ' h' Hwf Htyp Heval. (* get some initial receiver address ι₀ from wf_r_config *) assert (Hthis : exists ι0, get_this_var_mapping (vars rΓ) = Some ι0). { unfold wf_r_config in Hwf. destruct Hwf as [_ [_ [Hrenv _]]]. destruct Hrenv as [Hlen [Hreceiverval _]]. destruct Hreceiverval as [ι0 Hthis0]. exists ι0. destruct Hthis0 as [Hthis0 Hthisldom]. exact Hthis0. } destruct Hthis as [ι0 Hthis0]. pose proof (eval_stmt_preserves_receiver_addr_typed CT sΓ mt rΓ h stmt sΓ' rΓ' h' ι0 Htyp Heval Hthis0) as Hthis0'. rewrite Hthis0. symmetry. exact Hthis0'. Qed. Corollary eval_stmt_preserves_receiver_addr_eq_loc' : forall CT sΓ mt rΓ h stmt sΓ' rΓ' h' ι1 ι2 (Hwf : wf_r_config CT sΓ rΓ h) (Htyp : stmt_typing CT sΓ mt stmt sΓ') (Heval : eval_stmt CT rΓ h stmt OK rΓ' h') (Hthis1 : get_this_var_mapping (vars rΓ) = Some ι1) (Hthis2 : get_this_var_mapping (vars rΓ') = Some ι2), ι1 = ι2. Proof. intros CT sΓ mt rΓ h stmt sΓ' rΓ' h' ι1 ι2 Hwf Htyp Heval Hthis1 Hthis2. pose proof (eval_stmt_preserves_receiver_addr_mapping_eq CT sΓ mt rΓ h stmt sΓ' rΓ' h' Hwf Htyp Heval) as Heq. rewrite Hthis1 in Heq. rewrite Hthis2 in Heq. inversion Heq; reflexivity. Qed. Lemma eval_stmt_preserves_r_muttype_backwards : forall CT rΓ h stmt rΓ' h' loc q (Heval : eval_stmt CT rΓ h stmt OK rΓ' h') (Hmut' : r_muttype h' loc = Some q) (Hloc_dom : loc < dom h), r_muttype h loc = Some q. Proof. intros CT rΓ h stmt rΓ' h' loc q Heval Hmut' Hloc_dom. destruct (r_muttype h loc) as [q0|] eqn:Hmut0. - specialize (eval_stmt_preserves_r_muttype CT rΓ h stmt rΓ' h' loc q0 Heval Hmut0 Hloc_dom) as Hforward. rewrite Hforward in Hmut'. inversion Hmut'; subst q0. assumption. - unfold r_muttype in Hmut0. destruct (runtime_getObj h loc) as [o|] eqn:Hobj; [discriminate|]. exfalso. apply runtime_getObj_not_dom in Hobj. lia. Qed. Lemma preservation_skip : forall CT sΓ mt rΓ h sΓ' (Htyping : stmt_typing CT sΓ mt SSkip sΓ') (Hwf : wf_r_config CT sΓ rΓ h), wf_r_config CT sΓ' rΓ h. Proof. intros CT sΓ mt rΓ h sΓ' Htyping Hwf. inversion Htyping; subst; exact Hwf. Qed. Lemma preservation_local_ok : forall CT sΓ mt rΓ h T x rΓ' h' sΓ' (Hwf : wf_r_config CT sΓ rΓ h) (Htyping : stmt_typing CT sΓ mt (SLocal T x) sΓ') (Heval : eval_stmt CT rΓ h (SLocal T x) OK rΓ' h'), wf_r_config CT sΓ' rΓ' h'. Proof. intros CT sΓ mt rΓ h T x rΓ' h' sΓ' Hwf Htyping Heval. inversion Heval; subst. inversion Htyping; subst. unfold wf_r_config in *. destruct Hwf as [Hclass [Hheap [Hrenv [Hsenv [Hlen Hcorr]]]]]. split; [exact Hclass|]. repeat split. + (* wellformed heap *) exact Hheap. + (* Length of runtime environment greater than 0 *) simpl. rewrite length_app. simpl. lia. + (* The first element of runtime environment is not null *) destruct Hrenv as [HrEnvLen [Hreceiverval Hallvals]]. destruct Hreceiverval as [iot Hiot]. exists iot. simpl. unfold gget in *. destruct (vars rΓ) as [|v0 vs] eqn:Hvars. * (* Case: vars rΓ = [] *) exfalso. (* rewrite Hvars in HrEnvLen. *) simpl in HrEnvLen. lia. * (* Case: vars rΓ = v0 :: vs *) simpl. exact Hiot. + (* wellformed runtime environment *) unfold wf_renv in *. simpl. apply Forall_app. split. * destruct Hrenv as [HrEnvLen [Hreceiverval Hallvals]]. exact Hallvals. * constructor. -- trivial. -- constructor. + (* Length of static environment greater than 0 *) destruct Hsenv as [HsenvLength HsenvWellTyped]. rewrite length_app. simpl. lia. + (* wellformed static environment *) unfold wf_senv in *. apply Forall_app. split. * destruct Hsenv as [HsenvLength HsenvWellTyped]. exact HsenvWellTyped. * constructor. -- exact Hwf_T. (* assuming H is the wellformedness of T *) -- constructor. (* empty tail is well-typed *) + (* length equality *) simpl. rewrite length_app. simpl. rewrite Hlen. rewrite length_app. simpl. lia. + (* correspondence between static and runtime environments *) intros ι qcontext HreceiverAddr Hreceivermut i Hi sqt Hnth. destruct (Nat.eq_dec i (dom sΓ)) as [Heq | Hneq]. * (* Case: i = dom sΓ (new variable) *) subst i. unfold runtime_getVal. simpl. rewrite nth_error_app2. -- rewrite Hlen. trivial. -- rewrite Hlen. assert (Hzero : dom (vars rΓ) - dom (vars rΓ) = 0) by lia. rewrite Hzero. simpl. trivial. * (* Case: i < dom sΓ (existing variable) *) assert (Hi_old : i < dom sΓ). { simpl in Hi. rewrite length_app in Hi. simpl in Hi. lia. } assert (Hnth_old : nth_error sΓ i = Some sqt). { have Happ := nth_error_app1 sΓ [T] Hi_old. rewrite Happ in Hnth. exact Hnth. } rewrite (get_this_var_mapping_update_vars_app_null rΓ) in HreceiverAddr. specialize (Hcorr ι qcontext HreceiverAddr Hreceivermut i Hi_old sqt Hnth_old). unfold runtime_getVal in *. simpl. rewrite nth_error_app1. -- rewrite <- Hlen. exact Hi_old. -- destruct (nth_error (vars rΓ) i) as [v|] eqn:Hgetval. ++ (* Case: nth_error (vars rΓ) i = Some v *) destruct v as [|loc]. ** trivial. ** unfold wf_r_typable in *. simpl. assert (get_this_var_mapping (vars rΓ ++ [Null_a]) = get_this_var_mapping (vars rΓ)). { unfold get_this_var_mapping. destruct (vars rΓ) as [|v0 vs]; reflexivity. } (* rewrite H0. *) exact Hcorr. ++ (* Case: nth_error (vars rΓ) i = None *) exfalso. apply nth_error_None in Hgetval. rewrite <- Hlen in Hgetval. lia. Qed. Lemma preservation_varass_ok : forall CT sΓ mt rΓ h x e rΓ' h' sΓ' (Hwf : wf_r_config CT sΓ rΓ h) (Htyping : stmt_typing CT sΓ mt (SVarAss x e) sΓ') (Heval_stmt : eval_stmt CT rΓ h (SVarAss x e) OK rΓ' h'), wf_r_config CT sΓ' rΓ' h'. Proof. intros CT sΓ mt rΓ h x e rΓ' h' sΓ' Hwf Htyping Heval_stmt. inversion Heval_stmt; subst. rename Hval into Htarget. rename Heval into Heval_expr. inversion Htyping; subst. have Hwfcopy := Hwf. revert Hwfcopy. unfold wf_r_config in Hwf. intros. unfold wf_r_config. destruct Hwf as [Hclass [Hheap [Hrenv [Hsenv [Hlen Hcorr]]]]]. split; [exact Hclass|]. repeat split. + (* wellformed heap *) exact Hheap. + (* Length of runtime environment greater than 0 *) simpl. destruct Hsenv as [HsenvLength HsenvWellTyped]. rewrite update_length. rewrite <- Hlen. exact HsenvLength. + (* The first element of runtime environment is not null *) destruct Hrenv as [HrEnvLen [Hreceiverval Hallvals]]. destruct Hreceiverval as [iot Hiot]. exists iot. simpl. unfold gget in *. destruct (vars rΓ) as [|v0 vs] eqn:Hvars. * (* Case: vars rΓ = [] *) exfalso. (* rewrite Hvars in HrEnvLen. *) simpl in HrEnvLen. lia. * (* Case: vars rΓ = v0 :: vs *) destruct x as [|x']. -- (* x = 0 *) contradiction. -- (* x = S x' *) simpl. (* update (S x') v2 (v0 :: vs) = v0 :: update x' v2 vs *) exact Hiot. + (* wellformed runtime environment *) unfold wf_renv in *. destruct Hrenv as [HrEnvLen [Hreceiverval Hallvals]]. simpl. apply Forall_update. * exact Hallvals. * destruct v2 as [|loc]. -- trivial. -- inversion Heval_expr; subst. (* assert (Hloc_in_vars : exists i, nth_error (vars rΓ) i = Some (Iot loc)). *) ++ assert (Hx0_bound : x0 < dom (vars rΓ)). { apply runtime_getVal_dom in Hval. exact Hval. } unfold runtime_getVal in Hval. assert (Hnth_loc : nth_error (vars rΓ) x0 = Some (Iot loc)) by exact Hval. eapply Forall_nth_error in Hallvals; eauto. simpl in Hallvals. exact Hallvals. ++ pose proof (runtime_getObj_dom v o _ Hobj) as Hv_bound. specialize (Hheap v Hv_bound). unfold wf_obj in Hheap. rewrite Hobj in Hheap. destruct Hheap as [_ [field_defs [Hcollect [Hlen_eq Hforall2]]]]. assert (Hf_bound : f < List.length (fields_map o)). { apply nth_error_Some. unfold getVal in Hfield. rewrite Hfield. discriminate. } rewrite Hlen_eq in Hf_bound. assert (Hfield_def : exists fdef, nth_error field_defs f = Some fdef). { apply nth_error_Some_exists. exact Hf_bound. } destruct Hfield_def as [fdef Hfdef]. unfold getVal in Hfield. eapply Forall2_nth_error in Hforall2; eauto. simpl in Hforall2. destruct (runtime_getObj h' loc) as [obj|] eqn:Hloc_obj. --- (* Case: runtime_getObj h' loc = Some obj *) trivial. --- (* Case: runtime_getObj h' loc = None *) contradiction Hforall2. * assert(Htarget_exists : exists v, nth_error (vars rΓ) x = Some v). { exists v1. exact Htarget. } destruct Htarget_exists as [v Hnth]. apply runtime_getVal_dom in Hnth. exact Hnth. + destruct Hsenv as [HsenvLength HsenvWellTyped]. exact HsenvLength. + (* wellformed static environment *) destruct Hsenv as [HsenvLength HsenvWellTyped]. exact HsenvWellTyped. + (* length equality *) simpl. rewrite update_length. exact Hlen. + (* correspondence between static and runtime environments *) intros ι qcontext HreceiverAddr Hreceivermut i Hi sqt Hnth. destruct (Nat.eq_dec i x) as [Heq | Hneq]. * (* Case: i = x (updated variable) *) subst i. unfold runtime_getVal. simpl. rewrite update_same. rewrite <- Hlen; exact Hi. destruct v2 as [|loc] eqn: Hv2. -- (* Case: v2 = Null_a *) trivial. -- (* Case: v2 = Iot loc *) (* Use subtyping to convert from T to sqt *) assert (Hsubtype_preserved : wf_r_typable CT h' loc sqt qcontext). { assert (Hsqt_eq : sqt = Tx). { unfold static_getType in Hget_x. rewrite Hget_x in Hnth. injection Hnth as Hsqt_eq. symmetry. exact Hsqt_eq. } subst sqt. assert (H_loc_Te : wf_r_typable CT h' loc Te qcontext). { (* Apply expression evaluation preservation lemma *) apply (expr_eval_preservation CT sΓ' mt rΓ h' e (Iot loc) rΓ h' Te ι). auto. - rewrite get_this_var_mapping_update_vars_nonzero in HreceiverAddr. exact Hnot_rcv. exact HreceiverAddr. - exact Hreceivermut. - exact Hwfcopy. - exact Htype_e. - exact Heval_expr. } eapply wf_r_typable_subtype with (T1:=Te)(T2:=Tx); eauto. } unfold wf_r_typable in *. exact Hsubtype_preserved. * (* Case: i ≠ x (unchanged variable) *) { unfold runtime_getVal. simpl. rewrite update_diff. - symmetry. exact Hneq. - rewrite get_this_var_mapping_update_vars_nonzero in HreceiverAddr. exact Hnot_rcv. assert (Hcorr_orig := Hcorr ι qcontext HreceiverAddr Hreceivermut i Hi sqt Hnth). unfold runtime_getVal in Hcorr_orig. destruct (nth_error (vars rΓ) i) as [v|] eqn:Hval. + destruct v as [|loc]. * trivial. * unfold wf_r_typable in Hcorr_orig |- *. destruct (r_type h' loc) as [rqt|] eqn:Hrtype; [|contradiction]. exact Hcorr_orig. + contradiction. } Qed. Lemma get_this_exists_from_wf_r_config : forall CT sΓ rΓ h (Hwf : wf_r_config CT sΓ rΓ h), exists ι, get_this_var_mapping (vars rΓ) = Some ι. Proof. intros CT sΓ rΓ h Hwf. destruct Hwf as [_ [_ [Hrenv _]]]. destruct Hrenv as [_ [Hrecv _]]. destruct Hrecv as [ι [Hthis _]]. now exists ι. Qed. Lemma receiver_mutability_exists_wf_renv : forall CT rΓ h ι (Hrenv : wf_renv CT rΓ h) (Hthis : get_this_var_mapping (vars rΓ) = Some ι), exists qcontext, r_muttype h ι = Some qcontext. Proof. intros CT rΓ h ι [HrLen [Hrecv Hall]] Hthis. unfold get_this_var_mapping in Hthis. destruct (vars rΓ) as [|v vs]; [discriminate|]. destruct v as [|loc]; try discriminate. simpl in Hthis. inversion Hthis; subst loc. apply Forall_inv in Hall. simpl in Hall. destruct (runtime_getObj h ι) as [o|] eqn:Hobj; [|contradiction]. unfold r_muttype. rewrite Hobj. eauto. Qed. Lemma r_muttype_update_field_preserve : forall h locx f v loc, r_muttype (update_field h locx f v) loc = r_muttype h loc. Proof. intros h locx f v loc. unfold r_muttype, update_field. destruct (runtime_getObj h locx) as [o_x|] eqn:Hobjx. - destruct (Nat.eq_dec loc locx) as [Heq|Hneq]. + subst loc. rewrite runtime_getObj_update_same. * f_equal. apply runtime_getObj_dom in Hobjx. exact Hobjx. * rewrite Hobjx. simpl. reflexivity. + rewrite runtime_getObj_update_diff; [symmetry; exact Hneq|]. reflexivity. - reflexivity. Qed. Lemma preservation_fldwrite_ok_abstract_state : forall CT sΓ rΓ h x f y h' sΓ' (Hwf : wf_r_config CT sΓ rΓ h) (Htyping : stmt_typing CT sΓ AbstractState (SFldWrite x f y) sΓ') (Heval : eval_stmt CT rΓ h (SFldWrite x f y) OK rΓ h'), wf_r_config CT sΓ' rΓ h'. Proof. intros CT sΓ rΓ h x f y h' sΓ' Hwf Htyping Heval. inversion Heval; subst. rename Hval_x into Hgetx. rename Hobj into Hgetobj. rename Hfield into Hgetf. rename Hval_y into Hgety. have Hwfcopy := Hwf. inversion Htyping; subst. unfold wf_r_config in Hwf. destruct Hwf as [Hclass [Hheap [Hrenv [Hsenv [Hlen Hcorr]]]]]. split; [exact Hclass|]. repeat split. + (* wellformed heap *) unfold wf_heap in *. intros ι0 Hdom. unfold update_field in *. destruct (runtime_getObj h loc_x) as [o_x|] eqn:Hobj. * (* Case: object exists at lx *) destruct (Nat.eq_dec ι0 loc_x) as [Heq | Hneq]. -- (* Case: ι = lx (the updated object) *) subst ι0. unfold wf_obj. simpl. specialize (Hheap loc_x). rewrite update_length in Hdom. specialize (Hheap Hdom). unfold wf_obj in Hheap. rewrite Hobj in Hheap. destruct Hheap as [Hrtypeuse [Hlen_fields Hwf_fields]]. unfold runtime_getObj. rewrite update_same. ++ exact Hdom. ++ repeat split. ** exact Hrtypeuse. ** simpl. rewrite update_length. exists Hlen_fields. destruct Hwf_fields as [Hcollect [Hlen_eq Hforall2]]. split. --- exact Hcollect. --- split. +++ exact Hlen_eq. +++ { apply Forall2_update. eapply Forall2_impl; [|exact Hforall2]. intros v fdef Hv_fdef. destruct v as [|loc]; [trivial|]. destruct (runtime_getObj h loc) as [obj_at_loc|] eqn:Hobj_at_loc; [|contradiction Hv_fdef]. destruct Hv_fdef as [rqt [Hrtype Hsubtype]]. destruct (Nat.eq_dec loc loc_x) as [Heq_loc | Hneq_loc]. (* Case: loc = lx *) subst loc. unfold update_field. simpl. rewrite update_same. apply runtime_getObj_dom in Hobj_at_loc. exact Hobj_at_loc. exists rqt. split. unfold r_type. simpl. rewrite runtime_getObj_update_same. simpl. apply runtime_getObj_dom in Hobj_at_loc. exact Hobj_at_loc. simpl. unfold r_type in Hrtype. rewrite Hobj_at_loc in Hrtype. injection Hrtype as Hrqt_eq. rewrite Hobj in Hobj_at_loc. injection Hobj_at_loc as Heq_objs. subst obj_at_loc. rewrite Hrqt_eq. reflexivity. exact Hsubtype. (* Case: loc ≠ lx *) rewrite update_diff; [symmetry; exact Hneq_loc |]. unfold runtime_getObj in Hobj_at_loc. rewrite Hobj_at_loc. exists rqt. split. unfold r_type. rewrite runtime_getObj_update_diff; [symmetry; exact Hneq_loc|]. unfold r_type in Hrtype. exact Hrtype. exact Hsubtype. assert (Hf_valid : f < dom (fields_map o_x)). { injection Hgetobj as Ho_eq. subst o_x. apply getVal_dom in Hgetf. exact Hgetf. } rewrite <- Hlen_eq. exact Hf_valid. intros b Hnth_b. destruct val_y as [|loc_y]; [trivial|]. assert (Hx_dom : x < dom sΓ'). { apply static_getType_dom in Hget_x. exact Hget_x. } assert (Hy_dom : y < dom sΓ'). { apply static_getType_dom in Hget_y. exact Hget_y. } have Hcorrcopy := Hcorr. assert (Hthis_exists : exists ι, get_this_var_mapping (vars rΓ) = Some ι). { eapply get_this_exists_from_wf_r_config; eauto. } destruct Hthis_exists as [ι HreceiverAddr]. assert (Hqcontext_exists : exists qcontext, r_muttype h ι = Some qcontext). { eapply receiver_mutability_exists_wf_renv; eauto. } destruct Hqcontext_exists as [qcontext Hreceivermut]. have Hcorropy := Hcorr. specialize (Hcorr ι qcontext HreceiverAddr Hreceivermut x Hx_dom Tx Hget_x). destruct (runtime_getVal rΓ x) as [val_x|] eqn:Hx_val; [|contradiction]. injection Hgetx as H_val_eq. subst val_x. unfold update_field. destruct (runtime_getObj h loc_x) as [o_lx|] eqn:Hobj_lx; [|easy]. destruct (Nat.eq_dec loc_y loc_x) as [Heq_loc2_lx | Hneq_loc2_lx]. specialize (Hcorrcopy ι qcontext HreceiverAddr Hreceivermut y Hy_dom Ty Hget_y). destruct (runtime_getVal rΓ y) as [val_y|] eqn:Hy_val; [|contradiction]. injection Hgety as H_val_eq. subst val_y. unfold update_field. destruct (runtime_getObj h loc_y) as [o_ly|] eqn:Hobj_ly. 2:{ subst loc_y. rewrite Hobj_lx in Hobj_ly. easy. } (* Case: loc_y = loc_x *) subst loc_y. unfold runtime_getObj. rewrite update_same; [exact Hdom|]. unfold wf_r_typable in Hcorr. destruct (r_type h loc_x) as [rqt_x|] eqn:Hrtype_x; [|contradiction Hcorr]. destruct Hcorr as [Hbase_sub Hqual_typable]. exists rqt_x. split. unfold r_type. unfold runtime_getObj. rewrite update_same; [exact Hdom|]. simpl. unfold r_type in Hrtype_x. rewrite Hobj_lx in Hrtype_x. injection Hobj as Ho_eq. injection Hgetobj as Ho_eq2. subst o_lx o_x. exact Hrtype_x. injection Hobj as Ho_lx_eq. injection Hgetobj as Ho_x_eq. subst o_lx o_x. assert (Hrt_type_eq : rt_type o = rqt_x). { unfold r_type in Hrtype_x. rewrite Hobj_lx in Hrtype_x. injection Hrtype_x as Heq. exact Heq. } rewrite Hrt_type_eq in Hcollect. assert (fieldT = b). { unfold sf_def_rel in Hfld_def. inversion Hfld_def; subst. symmetry. eapply collect_fields_consistent_through_runtime_static with (C:=(rctype (rt_type o)))(fields1:=Hlen_fields)(fields2:=fields)(fdef1:=b)(fdef2:=fieldT); eauto. } subst b. (* Case: loc2 ≠ lx *) rewrite Hobj_lx in Hobj_ly. inversion Hobj_ly. subst o_ly. unfold wf_r_typable in Hcorrcopy. rewrite Hrtype_x in Hcorrcopy. destruct Hcorrcopy as [Hxybase Hxyqualifer]. { constructor. (* Base type *) apply qualified_type_subtype_base_subtype in Hsub. simpl in Hsub. eapply base_trans; eauto. (* Qualifier *) apply get_this_qualified_type_nth_error in Hthis. unfold wf_senv in Hsenv; destruct Hsenv as [Hsenvdom _]; apply qualified_type_subtype_q_subtype in Hsub. simpl in Hsub. unfold qualifier_typable_heap. move Hsub at bottom. move Hqual_typable at bottom. unfold vpa_mutability_rec_fld; unfold vpa_mutability_stype_fld_abstract_state in Hsub. subst rqt_x. clear - Hsub Hqual_typable Hxyqualifer. all: destruct (rqtype (rt_type o)) eqn: rq; destruct (mutability (ftype fieldT)) eqn: HfieldMut; simpl; simpl in Hsub; try trivial. all: destruct (sqtype Tx) eqn: qx; destruct (sqtype Ty) eqn: qy; simpl in Hsub; try solve_q_subtype_wrong. all: destruct qcontext eqn: Hqcontext; try solve_qualifier_typable_wrong_concrete. } have H11copy := Hsub. apply qualified_type_subtype_q_subtype in Hsub. destruct (nth_error h loc_y) as [obj_y|] eqn:Hnth_y. - (* loc_y exists in original heap *) assert (Hnth_updated : nth_error (update loc_x (set_fields_map o_x (update f (Iot loc_y) (fields_map o_x))) h) loc_y = Some obj_y). { rewrite nth_error_update_neq; [symmetry; exact Hneq_loc2_lx | exact Hnth_y]. } rewrite Hnth_updated. specialize (Hcorrcopy ι qcontext HreceiverAddr Hreceivermut y Hy_dom Ty Hget_y). rewrite Hgety in Hcorrcopy. unfold wf_r_typable in Hcorrcopy. destruct (r_type h loc_y) as [rqt_y|] eqn:Hrtype_y; [|contradiction]. destruct Hcorrcopy as [Hbase_y Hqual_y]. exists rqt_y. split. unfold r_type. unfold runtime_getObj. rewrite Hnth_updated. unfold r_type in Hrtype_y. unfold runtime_getObj in Hrtype_y. rewrite Hnth_y in Hrtype_y. exact Hrtype_y. assert (fieldT = b). { unfold sf_def_rel in Hfld_def. inversion Hfld_def; subst. symmetry. eapply collect_fields_consistent_through_runtime_static with (C:=(rctype (rt_type o_x)))(fields1:=Hlen_fields)(fields2:=fields)(fdef1:=b)(fdef2:=fieldT); eauto. apply qualified_type_subtype_base_subtype in H11copy. simpl in H11copy. unfold wf_r_typable in Hcorr. unfold r_type in Hcorr. rewrite Hobj_lx in Hcorr. destruct Hcorr as [Hbase_sub Hqual_typable]. inversion Hobj. subst o_lx. exact Hbase_sub. } subst b. split. + (* Base type equality *) apply qualified_type_subtype_base_subtype in H11copy. (* apply vpa_preserve_basetype_subtype in H11copy. *) simpl in H11copy. eapply base_trans; eauto. + (* Qualifier typable *) apply get_this_qualified_type_nth_error in Hthis. unfold wf_senv in Hsenv; destruct Hsenv as [Hsenvdom _]; move Hsub at bottom. inversion Hlen. inversion Hobj. subst. unfold qualifier_typable_heap. unfold qualifier_typable_context in Hqual_y. unfold wf_r_typable in Hcorr. unfold r_type in Hcorr. rewrite Hobj_lx in Hcorr. destruct Hcorr as [_ Hqualifiertypablex]. inversion Hgetobj; subst o. unfold vpa_mutability_stype_fld_abstract_state in Hsub. unfold vpa_mutability_rec_fld. unfold vpa_mutability_runtime in Hqual_y. clear - Hqual_y Hsub Hqualifiertypablex. all: destruct (rqtype rqt_y) eqn: Hrqy; destruct (rqtype (rt_type o_x)) eqn: Hrqx; destruct (mutability (ftype fieldT)) eqn: Hfield; try trivial. all: destruct (sqtype Ty) eqn: Hsqy; destruct qcontext eqn: Hqcontext; simpl in Hqual_y; try solve_q_subtype_wrong. all: destruct (sqtype Tx) eqn: Hsqx; simpl in Hsub; try solve_q_subtype_wrong; try solve_qualifier_typable_wrong_concrete. all: try easy. - (* loc_y doesn't exist - contradiction *) assert (Hnth_updated : nth_error (update loc_x (set_fields_map o_x (update f (Iot loc_y) (fields_map o_x))) h) loc_y = None). { rewrite nth_error_update_neq; [symmetry; exact Hneq_loc2_lx | exact Hnth_y]. } rewrite Hnth_updated. exfalso. specialize (Hcorrcopy ι qcontext HreceiverAddr Hreceivermut y Hy_dom Ty Hget_y). rewrite Hgety in Hcorrcopy. unfold wf_r_typable in Hcorrcopy. unfold r_type in Hcorrcopy. unfold runtime_getObj in Hcorrcopy. rewrite Hnth_y in Hcorrcopy. easy. } -- unfold wf_obj, runtime_getObj. rewrite update_diff. ** rewrite update_length in Hdom. symmetry. exact Hneq. ** rewrite update_length in Hdom. destruct (nth_error h ι0) eqn:Htest. 2:{ exfalso. apply nth_error_None in Htest. lia. } split. specialize (Hheap ι0 Hdom). unfold wf_obj in Hheap. destruct (runtime_getObj h ι0) as [objl|] eqn: Hobjl; [| easy]. destruct Hheap as [Hwfobjtypeuse _]. unfold runtime_getObj in Hobjl. rewrite Htest in Hobjl. inversion Hobjl. subst. exact Hwfobjtypeuse. specialize (Hheap ι0 Hdom). unfold wf_obj in Hheap. destruct (runtime_getObj h ι0) as [objl|] eqn: Hobjl; [| easy]. destruct Hheap as [Hwfobjtypeuse Hwfobjfields]. unfold runtime_getObj in Hobjl. rewrite Htest in Hobjl. inversion Hobjl. subst. destruct Hwfobjfields as [field_defs [Hcollect [Hlen_eq Hforall2]]]. exists field_defs. { split. exact Hcollect. split. exact Hlen_eq. eapply Forall2_impl; [|exact Hforall2]. intros v fdef Hv_fdef. destruct v as [|loc]; [trivial|]. (* First check if the object exists in the updated heap *) unfold update_field. destruct (runtime_getObj h loc_x) as [o_lx|] eqn:Hobj_lx. destruct (Nat.eq_dec loc loc_x) as [Heq | Hneq_loc]. subst loc. rewrite Hobj_lx in Hv_fdef. destruct Hv_fdef as [rqt [Hrtype_loc Hsubtype]]. unfold runtime_getObj. rewrite update_same. unfold r_type in Hrtype_loc. unfold r_type in Hrtype_loc. destruct (runtime_getObj h loc_x) as [oxx|] eqn:Hobj_lxx; [|discriminate Hrtype_loc]. apply runtime_getObj_dom in Hobj_lxx. exact Hobj_lxx. exists rqt. split. unfold r_type. rewrite runtime_getObj_update_same. apply runtime_getObj_dom in Hobj_lx. exact Hobj_lx. simpl. unfold r_type in Hrtype_loc. rewrite Hobj_lx in Hrtype_loc. injection Hobj as Ho_new_eq. subst o_x. injection Hrtype_loc as Hrqt_eq. subst rqt. reflexivity. exact Hsubtype. destruct (runtime_getObj h loc) as [obj_loc|] eqn:Hobj_loc; [|contradiction Hv_fdef]. destruct Hv_fdef as [rqt [Hrtype_loc Hsubtype]]. unfold runtime_getObj. rewrite update_diff. symmetry. exact Hneq_loc. unfold runtime_getObj in Hobj_loc. destruct (nth_error h loc) as [obj|] eqn:Hnth_loc; [|discriminate Hobj_loc]. injection Hobj_loc as Hobj_eq. subst obj. exists rqt. split. unfold r_type. rewrite runtime_getObj_update_diff. symmetry. exact Hneq_loc. exact Hrtype_loc. exact Hsubtype. exfalso. discriminate Hobj. } * exfalso. discriminate Hgetobj. + destruct Hrenv as [HrEnvLen [Hreceiver Hallvals]]. exact HrEnvLen. + destruct Hrenv as [HrEnvLen [Hreceiver Hallvals]]. destruct Hreceiver as [Hreceiverval Hreceivervaldom]. exists Hreceiverval. split. * exact (proj1 Hreceivervaldom). * rewrite update_field_length. exact (proj2 Hreceivervaldom). + destruct Hrenv as [HrEnvLen [Hreceiverval Hallvals]]. eapply Forall_impl; [| exact Hallvals]. intros v Hv. destruct v as [|loc]; [trivial|]. unfold update_field in Hv |- *. destruct (runtime_getObj h loc_x) as [o'|] eqn:Hobj'; [| exact Hv]. destruct (Nat.eq_dec loc loc_x) as [Heq | Hneq]. * subst loc. rewrite runtime_getObj_update_same; [trivial | ]. apply runtime_getObj_dom in Hobj'. exact Hobj'. trivial. * unfold runtime_getObj. rewrite update_diff. -- symmetry. exact Hneq. -- auto. + destruct Hsenv as [HsenvLength HsenvWellTyped]. exact HsenvLength. + destruct Hsenv as [HsenvLength HsenvWellTyped]. exact HsenvWellTyped. + exact Hlen. + intros ι qcontext HreceiverAddr Hreceivermut i Hi sqt Hnth. assert (r_muttype h ι = Some qcontext) as Hreceivermut_orig. { rewrite (r_muttype_update_field_preserve h loc_x f val_y ι) in Hreceivermut. exact Hreceivermut. } assert (Hcorr_orig := Hcorr ι qcontext HreceiverAddr Hreceivermut_orig i Hi sqt Hnth). destruct (runtime_getVal rΓ i) as [v|] eqn:Hval; [|exact Hcorr_orig]. destruct v as [|loc]; [trivial|]. unfold wf_r_typable in Hcorr_orig |- *. destruct (r_type h loc) as [rqt|] eqn:Hrtype; [|contradiction]. assert (Hrtype_preserved : r_type (update_field h loc_x f val_y) loc = Some rqt). { unfold r_type. unfold update_field. remember (runtime_getObj h loc_x) as obj_result eqn:Hobj_eq. destruct obj_result as [o'|]. - destruct (Nat.eq_dec loc loc_x) as [Heq | Hneq]. + subst loc. rewrite runtime_getObj_update_same. * simpl. unfold r_type in Hrtype. destruct (runtime_getObj h loc_x) as [o_lx|] eqn:Hobj_lx; [|discriminate Hrtype]. apply runtime_getObj_dom in Hobj_lx. exact Hobj_lx. * have Hobj_eq_copy := Hobj_eq. symmetry in Hobj_eq. apply runtime_getObj_dom in Hobj_eq. simpl. unfold r_type in Hrtype. destruct (runtime_getObj h loc_x) as [o_lx|] eqn:Hobj_lx; [|discriminate Hrtype]. injection Hrtype as Hrtype_eq. rewrite <- Hrtype_eq. f_equal. injection Hobj_eq_copy as Ho_eq. rewrite Ho_eq. reflexivity. + rewrite runtime_getObj_update_diff. * symmetry. exact Hneq. * exact Hrtype. - exact Hrtype. } rewrite Hrtype_preserved. exact Hcorr_orig. Qed. Lemma preservation_fldwrite_ok_readonly_state : forall CT sΓ rΓ h x f y h' sΓ' (Hwf : wf_r_config CT sΓ rΓ h) (Htyping : stmt_typing CT sΓ ReadonlyState (SFldWrite x f y) sΓ') (Heval : eval_stmt CT rΓ h (SFldWrite x f y) OK rΓ h'), wf_r_config CT sΓ' rΓ h'. Proof. intros CT sΓ rΓ h x f y h' sΓ' Hwf Htyping Heval. inversion Heval; subst. rename Hval_x into Hgetx. rename Hobj into Hgetobj. rename Hfield into Hgetf. rename Hval_y into Hgety. have Hwfcopy := Hwf. inversion Htyping; subst. unfold wf_r_config in Hwf. destruct Hwf as [Hclass [Hheap [Hrenv [Hsenv [Hlen Hcorr]]]]]. split; [exact Hclass|]. repeat split. + (* wellformed heap *) unfold wf_heap in *. intros ι0 Hdom. unfold update_field in *. destruct (runtime_getObj h loc_x) as [o_x|] eqn:Hobj. * (* Case: object exists at lx *) destruct (Nat.eq_dec ι0 loc_x) as [Heq | Hneq]. -- (* Case: ι = lx (the updated object) *) subst ι0. unfold wf_obj. simpl. specialize (Hheap loc_x). rewrite update_length in Hdom. specialize (Hheap Hdom). unfold wf_obj in Hheap. rewrite Hobj in Hheap. destruct Hheap as [Hrtypeuse [Hlen_fields Hwf_fields]]. unfold runtime_getObj. rewrite update_same. ++ exact Hdom. ++ repeat split. ** exact Hrtypeuse. ** simpl. rewrite update_length. exists Hlen_fields. destruct Hwf_fields as [Hcollect [Hlen_eq Hforall2]]. split. --- exact Hcollect. --- split. +++ exact Hlen_eq. +++ { apply Forall2_update. eapply Forall2_impl; [|exact Hforall2]. intros v fdef Hv_fdef. destruct v as [|loc]; [trivial|]. destruct (runtime_getObj h loc) as [obj_at_loc|] eqn:Hobj_at_loc; [|contradiction Hv_fdef]. destruct Hv_fdef as [rqt [Hrtype Hsubtype]]. destruct (Nat.eq_dec loc loc_x) as [Heq_loc | Hneq_loc]. (* Case: loc = lx *) subst loc. unfold update_field. simpl. rewrite update_same. apply runtime_getObj_dom in Hobj_at_loc. exact Hobj_at_loc. exists rqt. split. unfold r_type. simpl. rewrite runtime_getObj_update_same. simpl. apply runtime_getObj_dom in Hobj_at_loc. exact Hobj_at_loc. simpl. unfold r_type in Hrtype. rewrite Hobj_at_loc in Hrtype. injection Hrtype as Hrqt_eq. rewrite Hobj in Hobj_at_loc. injection Hobj_at_loc as Heq_objs. subst obj_at_loc. rewrite Hrqt_eq. reflexivity. exact Hsubtype. (* Case: loc ≠ lx *) rewrite update_diff; [symmetry; exact Hneq_loc |]. unfold runtime_getObj in Hobj_at_loc. rewrite Hobj_at_loc. exists rqt. split. unfold r_type. rewrite runtime_getObj_update_diff; [symmetry; exact Hneq_loc|]. unfold r_type in Hrtype. exact Hrtype. exact Hsubtype. assert (Hf_valid : f < dom (fields_map o_x)). { injection Hgetobj as Ho_eq. subst o_x. apply getVal_dom in Hgetf. exact Hgetf. } rewrite <- Hlen_eq. exact Hf_valid. intros b Hnth_b. destruct val_y as [|loc_y]; [trivial|]. assert (Hx_dom : x < dom sΓ'). { apply static_getType_dom in Hget_x. exact Hget_x. } assert (Hy_dom : y < dom sΓ'). { apply static_getType_dom in Hget_y. exact Hget_y. } have Hcorrcopy := Hcorr. assert (Hthis_exists : exists ι, get_this_var_mapping (vars rΓ) = Some ι). { eapply get_this_exists_from_wf_r_config; eauto. } destruct Hthis_exists as [ι HreceiverAddr]. assert (Hqcontext_exists : exists qcontext, r_muttype h ι = Some qcontext). { eapply receiver_mutability_exists_wf_renv; eauto. } destruct Hqcontext_exists as [qcontext Hreceivermut]. have Hcorropy := Hcorr. specialize (Hcorr ι qcontext HreceiverAddr Hreceivermut x Hx_dom Tx Hget_x). destruct (runtime_getVal rΓ x) as [val_x|] eqn:Hx_val; [|contradiction]. injection Hgetx as H_val_eq. subst val_x. unfold update_field. destruct (runtime_getObj h loc_x) as [o_lx|] eqn:Hobj_lx; [|easy]. destruct (Nat.eq_dec loc_y loc_x) as [Heq_loc2_lx | Hneq_loc2_lx]. specialize (Hcorrcopy ι qcontext HreceiverAddr Hreceivermut y Hy_dom Ty Hget_y). destruct (runtime_getVal rΓ y) as [val_y|] eqn:Hy_val; [|contradiction]. injection Hgety as H_val_eq. subst val_y. unfold update_field. (* subst loc_y. *) destruct (runtime_getObj h loc_y) as [o_ly|] eqn:Hobj_ly. 2:{ subst loc_y. rewrite Hobj_lx in Hobj_ly. easy. } (* Case: loc_y = loc_x *) subst loc_y. unfold runtime_getObj. rewrite update_same; [exact Hdom|]. unfold wf_r_typable in Hcorr. destruct (r_type h loc_x) as [rqt_x|] eqn:Hrtype_x; [|contradiction Hcorr]. destruct Hcorr as [Hbase_sub Hqual_typable]. exists rqt_x. split. unfold r_type. unfold runtime_getObj. rewrite update_same; [exact Hdom|]. simpl. unfold r_type in Hrtype_x. rewrite Hobj_lx in Hrtype_x. injection Hobj as Ho_eq. injection Hgetobj as Ho_eq2. subst o_lx o_x. exact Hrtype_x. injection Hobj as Ho_lx_eq. injection Hgetobj as Ho_x_eq. subst o_lx o_x. assert (Hrt_type_eq : rt_type o = rqt_x). { unfold r_type in Hrtype_x. rewrite Hobj_lx in Hrtype_x. injection Hrtype_x as Heq. exact Heq. } rewrite Hrt_type_eq in Hcollect. assert (fieldT = b). { unfold sf_def_rel in Hfld_def. inversion Hfld_def; subst. symmetry. eapply collect_fields_consistent_through_runtime_static with (C:=(rctype (rt_type o)))(fields1:=Hlen_fields)(fields2:=fields)(fdef1:=b)(fdef2:=fieldT); eauto. } subst b. (* Case: loc2 ≠ lx *) rewrite Hobj_lx in Hobj_ly. inversion Hobj_ly. subst o_ly. unfold wf_r_typable in Hcorrcopy. rewrite Hrtype_x in Hcorrcopy. destruct Hcorrcopy as [Hxybase Hxyqualifer]. { constructor. (* Base type *) apply qualified_type_subtype_base_subtype in Hsub. (* apply vpa_preserve_basetype_subtype in H11. *) simpl in Hsub. eapply base_trans; eauto. (* Qualifier *) apply get_this_qualified_type_nth_error in Hthis. unfold wf_senv in Hsenv; destruct Hsenv as [Hsenvdom _]; apply qualified_type_subtype_q_subtype in Hsub. simpl in Hsub. unfold qualifier_typable_heap. move Hsub at bottom. move Hqual_typable at bottom. unfold vpa_mutability_rec_fld; unfold vpa_mutability_stype_fld_abstract_state in Hsub. subst rqt_x. clear - Hsub Hqual_typable Hxyqualifer. all: destruct (rqtype (rt_type o)) eqn: rq; destruct (mutability (ftype fieldT)) eqn: HfieldMut; simpl; simpl in Hsub; try trivial. all: destruct (sqtype Tx) eqn: qx; destruct (sqtype Ty) eqn: qy; simpl in Hsub; try solve_q_subtype_wrong. all: destruct qcontext eqn: Hqcontext; try solve_qualifier_typable_wrong_concrete. } have H11copy := Hsub. apply qualified_type_subtype_q_subtype in Hsub. destruct (nth_error h loc_y) as [obj_y|] eqn:Hnth_y. - (* loc_y exists in original heap *) assert (Hnth_updated : nth_error (update loc_x (set_fields_map o_x (update f (Iot loc_y) (fields_map o_x))) h) loc_y = Some obj_y). { rewrite nth_error_update_neq; [symmetry; exact Hneq_loc2_lx | exact Hnth_y]. } rewrite Hnth_updated. specialize (Hcorrcopy ι qcontext HreceiverAddr Hreceivermut y Hy_dom Ty Hget_y). rewrite Hgety in Hcorrcopy. unfold wf_r_typable in Hcorrcopy. destruct (r_type h loc_y) as [rqt_y|] eqn:Hrtype_y; [|contradiction]. destruct Hcorrcopy as [Hbase_y Hqual_y]. exists rqt_y. split. unfold r_type. unfold runtime_getObj. rewrite Hnth_updated. unfold r_type in Hrtype_y. unfold runtime_getObj in Hrtype_y. rewrite Hnth_y in Hrtype_y. exact Hrtype_y. assert (fieldT = b). { unfold sf_def_rel in Hfld_def. inversion Hfld_def; subst. symmetry. eapply collect_fields_consistent_through_runtime_static with (C:=(rctype (rt_type o_x)))(fields1:=Hlen_fields)(fields2:=fields)(fdef1:=b)(fdef2:=fieldT); eauto. apply qualified_type_subtype_base_subtype in H11copy. simpl in H11copy. unfold wf_r_typable in Hcorr. unfold r_type in Hcorr. rewrite Hobj_lx in Hcorr. destruct Hcorr as [Hbase_sub Hqual_typable]. inversion Hobj. subst o_lx. exact Hbase_sub. } subst b. split. + (* Base type equality *) apply qualified_type_subtype_base_subtype in H11copy. (* apply vpa_preserve_basetype_subtype in H11copy. *) simpl in H11copy. eapply base_trans; eauto. + (* Qualifier typable *) apply get_this_qualified_type_nth_error in Hthis. unfold wf_senv in Hsenv; destruct Hsenv as [Hsenvdom _]; move Hsub at bottom. inversion Hlen. inversion Hobj. subst. unfold qualifier_typable_heap. unfold qualifier_typable_context in Hqual_y. unfold wf_r_typable in Hcorr. unfold r_type in Hcorr. rewrite Hobj_lx in Hcorr. destruct Hcorr as [_ Hqualifiertypablex]. inversion Hgetobj; subst o. unfold vpa_mutability_stype_fld_abstract_state in Hsub. unfold vpa_mutability_rec_fld. unfold vpa_mutability_runtime in Hqual_y. clear - Hqual_y Hsub Hqualifiertypablex. all: destruct (rqtype rqt_y) eqn: Hrqy; destruct (rqtype (rt_type o_x)) eqn: Hrqx; destruct (mutability (ftype fieldT)) eqn: Hfield; try trivial. all: destruct (sqtype Ty) eqn: Hsqy; destruct qcontext eqn: Hqcontext; simpl in Hqual_y; try solve_q_subtype_wrong. all: destruct (sqtype Tx) eqn: Hsqx; simpl in Hsub; try solve_q_subtype_wrong; try solve_qualifier_typable_wrong_concrete. all: try easy. - (* loc_y doesn't exist - contradiction *) assert (Hnth_updated : nth_error (update loc_x (set_fields_map o_x (update f (Iot loc_y) (fields_map o_x))) h) loc_y = None). { rewrite nth_error_update_neq; [symmetry; exact Hneq_loc2_lx | exact Hnth_y]. } rewrite Hnth_updated. exfalso. specialize (Hcorrcopy ι qcontext HreceiverAddr Hreceivermut y Hy_dom Ty Hget_y). rewrite Hgety in Hcorrcopy. unfold wf_r_typable in Hcorrcopy. unfold r_type in Hcorrcopy. unfold runtime_getObj in Hcorrcopy. rewrite Hnth_y in Hcorrcopy. easy. } -- unfold wf_obj, runtime_getObj. rewrite update_diff. ** rewrite update_length in Hdom. symmetry. exact Hneq. ** rewrite update_length in Hdom. destruct (nth_error h ι0) eqn:Htest. 2:{ exfalso. apply nth_error_None in Htest. lia. } split. specialize (Hheap ι0 Hdom). unfold wf_obj in Hheap. destruct (runtime_getObj h ι0) as [objl|] eqn: Hobjl; [| easy]. destruct Hheap as [Hwfobjtypeuse _]. unfold runtime_getObj in Hobjl. rewrite Htest in Hobjl. inversion Hobjl. subst. exact Hwfobjtypeuse. specialize (Hheap ι0 Hdom). unfold wf_obj in Hheap. destruct (runtime_getObj h ι0) as [objl|] eqn: Hobjl; [| easy]. destruct Hheap as [Hwfobjtypeuse Hwfobjfields]. unfold runtime_getObj in Hobjl. rewrite Htest in Hobjl. inversion Hobjl. subst. destruct Hwfobjfields as [field_defs [Hcollect [Hlen_eq Hforall2]]]. exists field_defs. { split. exact Hcollect. split. exact Hlen_eq. eapply Forall2_impl; [|exact Hforall2]. intros v fdef Hv_fdef. destruct v as [|loc]; [trivial|]. (* First check if the object exists in the updated heap *) unfold update_field. destruct (runtime_getObj h loc_x) as [o_lx|] eqn:Hobj_lx. destruct (Nat.eq_dec loc loc_x) as [Heq | Hneq_loc]. subst loc. rewrite Hobj_lx in Hv_fdef. destruct Hv_fdef as [rqt [Hrtype_loc Hsubtype]]. unfold runtime_getObj. rewrite update_same. unfold r_type in Hrtype_loc. unfold r_type in Hrtype_loc. destruct (runtime_getObj h loc_x) as [oxx|] eqn:Hobj_lxx; [|discriminate Hrtype_loc]. apply runtime_getObj_dom in Hobj_lxx. exact Hobj_lxx. exists rqt. split. unfold r_type. rewrite runtime_getObj_update_same. apply runtime_getObj_dom in Hobj_lx. exact Hobj_lx. simpl. unfold r_type in Hrtype_loc. rewrite Hobj_lx in Hrtype_loc. injection Hobj as Ho_new_eq. subst o_x. injection Hrtype_loc as Hrqt_eq. subst rqt. reflexivity. exact Hsubtype. destruct (runtime_getObj h loc) as [obj_loc|] eqn:Hobj_loc; [|contradiction Hv_fdef]. destruct Hv_fdef as [rqt [Hrtype_loc Hsubtype]]. unfold runtime_getObj. rewrite update_diff. symmetry. exact Hneq_loc. unfold runtime_getObj in Hobj_loc. destruct (nth_error h loc) as [obj|] eqn:Hnth_loc; [|discriminate Hobj_loc]. injection Hobj_loc as Hobj_eq. subst obj. exists rqt. split. unfold r_type. rewrite runtime_getObj_update_diff. symmetry. exact Hneq_loc. exact Hrtype_loc. exact Hsubtype. exfalso. discriminate Hobj. } * exfalso. discriminate Hgetobj. + destruct Hrenv as [HrEnvLen [Hreceiver Hallvals]]. exact HrEnvLen. + destruct Hrenv as [HrEnvLen [Hreceiver Hallvals]]. destruct Hreceiver as [Hreceiverval Hreceivervaldom]. exists Hreceiverval. split. * exact (proj1 Hreceivervaldom). * rewrite update_field_length. exact (proj2 Hreceivervaldom). + destruct Hrenv as [HrEnvLen [Hreceiverval Hallvals]]. eapply Forall_impl; [| exact Hallvals]. intros v Hv. destruct v as [|loc]; [trivial|]. unfold update_field in Hv |- *. destruct (runtime_getObj h loc_x) as [o'|] eqn:Hobj'; [| exact Hv]. destruct (Nat.eq_dec loc loc_x) as [Heq | Hneq]. * subst loc. rewrite runtime_getObj_update_same; [trivial | ]. apply runtime_getObj_dom in Hobj'. exact Hobj'. trivial. * unfold runtime_getObj. rewrite update_diff. -- symmetry. exact Hneq. -- auto. + destruct Hsenv as [HsenvLength HsenvWellTyped]. exact HsenvLength. + destruct Hsenv as [HsenvLength HsenvWellTyped]. exact HsenvWellTyped. + exact Hlen. + intros ι qcontext HreceiverAddr Hreceivermut i Hi sqt Hnth. assert (r_muttype h ι = Some qcontext) as Hreceivermut_orig. { rewrite (r_muttype_update_field_preserve h loc_x f val_y ι) in Hreceivermut. exact Hreceivermut. } assert (Hcorr_orig := Hcorr ι qcontext HreceiverAddr Hreceivermut_orig i Hi sqt Hnth). destruct (runtime_getVal rΓ i) as [v|] eqn:Hval; [|exact Hcorr_orig]. destruct v as [|loc]; [trivial|]. unfold wf_r_typable in Hcorr_orig |- *. destruct (r_type h loc) as [rqt|] eqn:Hrtype; [|contradiction]. assert (Hrtype_preserved : r_type (update_field h loc_x f val_y) loc = Some rqt). { unfold r_type. unfold update_field. remember (runtime_getObj h loc_x) as obj_result eqn:Hobj_eq. destruct obj_result as [o'|]. - destruct (Nat.eq_dec loc loc_x) as [Heq | Hneq]. + subst loc. rewrite runtime_getObj_update_same. * simpl. unfold r_type in Hrtype. destruct (runtime_getObj h loc_x) as [o_lx|] eqn:Hobj_lx; [|discriminate Hrtype]. apply runtime_getObj_dom in Hobj_lx. exact Hobj_lx. * have Hobj_eq_copy := Hobj_eq. symmetry in Hobj_eq. apply runtime_getObj_dom in Hobj_eq. simpl. unfold r_type in Hrtype. destruct (runtime_getObj h loc_x) as [o_lx|] eqn:Hobj_lx; [|discriminate Hrtype]. injection Hrtype as Hrtype_eq. rewrite <- Hrtype_eq. f_equal. injection Hobj_eq_copy as Ho_eq. rewrite Ho_eq. reflexivity. + rewrite runtime_getObj_update_diff. * symmetry. exact Hneq. * exact Hrtype. - exact Hrtype. } rewrite Hrtype_preserved. exact Hcorr_orig. Qed. Lemma preservation_fldwrite_ok : forall CT sΓ mt rΓ h x f y h' sΓ' (Hwf : wf_r_config CT sΓ rΓ h) (Htyping : stmt_typing CT sΓ mt (SFldWrite x f y) sΓ') (Heval : eval_stmt CT rΓ h (SFldWrite x f y) OK rΓ h'), wf_r_config CT sΓ' rΓ h'. Proof. intros. inversion Htyping; subst. - eapply preservation_fldwrite_ok_abstract_state; eauto. - eapply preservation_fldwrite_ok_abstract_state; eauto. econstructor; eauto. eapply concrete_assignable_implies_assignable; eauto. - eapply preservation_fldwrite_ok_readonly_state; eauto. - eapply preservation_fldwrite_ok_readonly_state; eauto. econstructor; eauto. eapply concrete_assignable_implies_assignable; eauto. Qed. Lemma r_muttype_app_preserve_old : forall h h_ext loc (Hlt : loc < dom h), r_muttype (h ++ [h_ext]) loc = r_muttype h loc. Proof. intros h h_ext loc Hlt. unfold r_muttype. destruct (runtime_getObj h loc) as [o|] eqn:Hobj. - rewrite (runtime_getObj_app_left h h_ext loc o Hlt Hobj). reflexivity. - (* impossible under loc < dom h *) exfalso. apply runtime_getObj_not_dom in Hobj. lia. Qed. Lemma r_muttype_app_preserve_old_Some : forall h h_ext loc q (Hlt : loc < dom h) (Hext : r_muttype (h ++ [h_ext]) loc = Some q), r_muttype h loc = Some q. Proof. intros h h_ext loc q Hlt Hext. rewrite (r_muttype_app_preserve_old h h_ext loc Hlt) in Hext. exact Hext. Qed. Lemma preservation_new_ok : forall CT sΓ mt rΓ h x q_c c ys rΓ' h' sΓ' (Hwf : wf_r_config CT sΓ rΓ h) (Htyping : stmt_typing CT sΓ mt (SNew x q_c c ys) sΓ') (Heval : eval_stmt CT rΓ h (SNew x q_c c ys) OK rΓ' h'), wf_r_config CT sΓ' rΓ' h'. Proof. intros CT sΓ mt rΓ h x q_c c ys rΓ' h' sΓ' Hwf Htyping Heval. inversion Heval; subst. rename Hthis into Hgetthis. rename Hargs into Hlookupvals. rename Hmut into HgetthisRuntimeType. inversion Htyping. have Hwf_copy := Hwf. unfold wf_r_config. unfold wf_r_config in Hwf. destruct Hwf as [Hclass [Hheap [Hrenv [Hsenv [Hlen Hcorr]]]]]. split; [exact Hclass|]. repeat split. + (* wellformed heap *) unfold wf_heap. intros ι0 Hι. subst. rewrite length_app in Hι. simpl in Hι. destruct (Nat.eq_dec ι0 (dom h)) as [Heq | Hneq]. * (* ι = dom h (new object) *) subst. unfold wf_obj. rewrite runtime_getObj_last. split. -- (* wf_rtypeuse for new object *) simpl. unfold wf_rtypeuse. destruct (bound CT c) as [q_c_val|] eqn:Hbound. ++ unfold constructor_def_lookup in Hconsig. destruct (find_class CT c) as [def|] eqn:Hfind. ** apply find_class_dom in Hfind. split. exact Hfind. unfold vpa_mutability_runtime_bound_agree. assert (Hwf_ctor : wf_constructor CT c consig). { eapply constructor_lookup_wf; eauto. } unfold wf_constructor in Hwf_ctor. destruct Hwf_ctor as [Hctor_bound [Hparamswf [field_defs [Hcollect_H1 [Hdom_eq Hfieldtypematch]]]]]. rewrite Hbound in Hctor_bound. inversion Hctor_bound; subst. unfold vpa_mutability_object_creation. unfold vpa_mutability_bound in Hqc. destruct q_c eqn:Hnewq; destruct (cqualifier consig) eqn: Hcbound; destruct qthisr eqn: Hqthis; simpl in *; try easy. ** exfalso. unfold bound in Hbound. rewrite Hfind in Hbound. discriminate Hbound. ++ unfold constructor_sig_lookup in Hconsig. destruct (constructor_def_lookup CT c) as [ctor|] eqn:Hctor. ** unfold constructor_def_lookup in Hctor. destruct (find_class CT c) as [def|] eqn:Hfind. --- unfold bound in Hbound. rewrite Hfind in Hbound. discriminate Hbound. --- discriminate Hctor. ** easy. -- { assert (Hc_dom : c < dom CT). { apply constructor_sig_lookup_dom in Hconsig. exact Hconsig. } (* Collect fields for class c *) assert (Hexists_fields : exists field_defs, CollectFields CT c field_defs). { eapply collect_fields_exists; eauto. } destruct Hexists_fields as [field_defs Hcollect_fields]. exists field_defs. split. + (* CollectFields CT c field_defs *) exact Hcollect_fields. + split. * (* Length equality: dom vals = dom field_defs *) simpl. apply Forall2_length in Harg_sub. apply runtime_lookup_list_preserves_length in Hlookupvals. apply static_getType_list_preserves_length in Hget_args. rewrite Hlookupvals. rewrite <- Hget_args. rewrite Harg_sub. rewrite length_map. eapply constructor_sig_lookup_implies_def in Hconsig; eauto. destruct Hconsig as [cdef Hcedflookup]. destruct Hcedflookup as [Hcedflookup Hcdefcsig]. eapply constructor_params_field_count; eauto. * (* Forall2 property *) assert (Hthis_exists : exists ι, get_this_var_mapping (vars rΓ) = Some ι). { eapply get_this_exists_from_wf_r_config; eauto. } destruct Hthis_exists as [ι HreceiverAddr]. assert (Hqcontext_exists : exists qcontext, r_muttype h ι = Some qcontext). { eapply receiver_mutability_exists_wf_renv; eauto. } destruct Hqcontext_exists as [qcontext Hreceivermut]. apply runtime_lookup_list_preserves_typing with (ι:= ι) (qcontext:=qcontext) (CT:= CT) (h := h) (sΓ := sΓ') (args := ys) (argtypes := argtypes) in Hlookupvals; auto. simpl. assert (Hwf_ctor : wf_constructor CT c consig). { eapply constructor_lookup_wf; eauto. } unfold wf_constructor in Hwf_ctor. destruct Hwf_ctor as [Hctor_bound [Hparamswf [field_defs_exists [Hcollect_H1 [Hdom_eq Hfieldtypematch]]]]]. unfold wf_heap in Hheap. unfold wf_obj in Hheap. eapply Forall2_from_nth. - (* Show lengths are equal *) apply Forall2_length in Hlookupvals. rewrite Hlookupvals. apply Forall2_length in Harg_sub. rewrite Harg_sub. rewrite length_map. assert (field_defs_exists = field_defs). { eapply collect_fields_deterministic_rel; eauto. } subst field_defs_exists. exact Hdom_eq. - (* Show pointwise property *) intros i v fdef Hi Hv Hfdef. assert (field_defs_exists = field_defs) as Hfields_eq. { eapply collect_fields_deterministic_rel; eauto. } subst field_defs_exists. destruct v; [easy|]. { assert (Hargtype : exists argtype, nth_error argtypes i = Some argtype). { apply Forall2_length in Hlookupvals. rewrite Hlookupvals in Hi. apply nth_error_Some_exists in Hi. exact Hi. } destruct Hargtype as [argtype Hargtype]. eapply Forall2_nth_error in Hlookupvals; [|exact Hv|exact Hargtype]. simpl in Hlookupvals. unfold wf_r_typable in Hlookupvals. destruct (r_type h l) as [rqt|] eqn:Hrtype; [|contradiction]. assert (Hl_dom : l < dom h). { unfold r_type in Hrtype. destruct (runtime_getObj h l) as [obj|] eqn:Hobj; [|discriminate]. apply runtime_getObj_dom in Hobj. exact Hobj. } rewrite runtime_getObj_last2; auto. destruct (runtime_getObj h l) eqn: Hl. 2:{apply runtime_getObj_not_dom in Hl. lia. } exists rqt. split. - unfold r_type. rewrite runtime_getObj_last2; auto. - split. + destruct Hlookupvals as [Hrctype _]. destruct (nth_error (cparams consig) i) as [paramtype|] eqn: Hparamtype. 2:{ apply nth_error_None in Hparamtype. assert (Hi_fdef : i < dom field_defs). { apply nth_error_Some. rewrite Hfdef. discriminate. } rewrite <- Hdom_eq in Hi_fdef. lia. } eapply Forall2_nth_error with (i:=i) (b:=fdef) (a:=paramtype) in Hfieldtypematch. apply qualified_type_subtype_base_subtype in Hfieldtypematch. simpl in Hfieldtypematch. assert (Hadapted_paramtype : nth_error (map (vpa_mutability_constructor_param q_c) (cparams consig)) i = Some (vpa_mutability_constructor_param q_c paramtype)). { rewrite nth_error_map. rewrite Hparamtype. reflexivity. } eapply Forall2_nth_error with (i:=i) (b:=vpa_mutability_constructor_param q_c paramtype) (a:=argtype) in Harg_sub. apply qualified_type_subtype_base_subtype in Harg_sub. unfold vpa_mutability_constructor_param in Harg_sub. simpl in Harg_sub. eapply base_trans; eauto. eapply base_trans; eauto. exact Hargtype. exact Hadapted_paramtype. exact Hparamtype. exact Hfdef. + destruct Hlookupvals as [Hrctype Hqctype]. destruct (nth_error (cparams consig) i) as [paramtype|] eqn: Hparamtype. 2:{ apply nth_error_None in Hparamtype. assert (Hi_fdef : i < dom field_defs). { apply nth_error_Some. rewrite Hfdef. discriminate. } rewrite <- Hdom_eq in Hi_fdef. lia. } eapply Forall2_nth_error with (i:=i) (b:=fdef) (a:=paramtype) in Hfieldtypematch. apply qualified_type_subtype_q_subtype in Hfieldtypematch. assert (Hadapted_paramtype : nth_error (map (vpa_mutability_constructor_param q_c) (cparams consig)) i = Some (vpa_mutability_constructor_param q_c paramtype)). { rewrite nth_error_map. rewrite Hparamtype. reflexivity. } eapply Forall2_nth_error with (i:=i) (b:=vpa_mutability_constructor_param q_c paramtype) (a:=argtype) in Harg_sub. apply qualified_type_subtype_q_subtype in Harg_sub. apply qualified_type_subtype_q_subtype in Hresult_sub. 2: exact Hargtype. 2: exact Hadapted_paramtype. 2: exact Hparamtype. 2: exact Hfdef. simpl in Hfieldtypematch. unfold vpa_mutability_constructor_param in Harg_sub. simpl in Harg_sub. move Hqctype at bottom. move Hfieldtypematch at bottom. unfold wf_senv in Hsenv; destruct Hsenv as [Hsenvdom _]; destruct (r_type h ι) as [rqt_receiver|] eqn: Hrtype_receiver. assert(H100: qcontext = rqtype rqt_receiver). { unfold r_muttype in Hreceivermut. unfold r_type in Hrtype_receiver. destruct (runtime_getObj h ι) eqn: save; [|easy]. inversion Hreceivermut; subst. inversion Hrtype_receiver; reflexivity. } 2:{ unfold r_type in Hrtype_receiver. unfold r_muttype in Hreceivermut. destruct (runtime_getObj h ι) eqn: save; [|easy]. discriminate Hrtype_receiver. } unfold qualifier_typable_heap. unfold vpa_mutability_rec_fld. unfold vpa_mutability_constructor_fld in Hfieldtypematch. unfold vpa_mutability_object_creation. unfold qc2q in Hresult_sub. simpl in Hresult_sub. assert (l1 = ι). { apply get_this_var_mapping_runtime_getVal in HreceiverAddr. rewrite Hgetthis in HreceiverAddr. injection HreceiverAddr as Heq. exact Heq. } subst l1. assert (qthisr = qcontext). { rewrite Hreceivermut in HgetthisRuntimeType. inversion HgetthisRuntimeType; reflexivity. } subst qthisr. unfold vpa_mutability_bound in Hqc. clear - Hfieldtypematch Hqctype Harg_sub Hqc. destruct (rqtype rqt) eqn: Hrqtq; destruct qcontext eqn: Hqthis; destruct q_c eqn: Hnewq; destruct (cqualifier consig) eqn: Hconstructoreturnq; destruct (mutability (ftype fdef)) eqn: Hfieldq; try easy. all: destruct (sqtype paramtype) eqn: Hparamq; try solve_q_subtype_wrong. all: destruct (sqtype argtype) eqn: Hargq; try solve_q_subtype_wrong; destruct qcontext eqn: Hqcontext; try solve_qualifier_typable_wrong_concrete; try solve_qualifier_typable_correct_concrete; try easy. } } * (* ι < dom h (existing object) *) assert (Hι_old : ι0 < dom h) by lia. unfold wf_obj. rewrite runtime_getObj_last2; auto. { unfold wf_heap in Hheap. specialize (Hheap ι0 Hι_old). unfold wf_obj in Hheap |- *. destruct (runtime_getObj h ι0) as [o|] eqn:Hobj; [|contradiction]. destruct Hheap as [Hrtypeuse [Hfields_len Hforall2]]. repeat split. + exact Hrtypeuse. + { exists Hfields_len. destruct Hforall2 as [Hcollect [Hlen_eq Hforall2_prop]]. split. - exact Hcollect. - split. + exact Hlen_eq. + eapply Forall2_impl; [|exact Hforall2_prop]. intros v fdef Hprop. destruct v as [|loc]; [trivial|]. destruct (runtime_getObj h loc) as [obj_loc|] eqn:Hobj_loc. * (* loc exists in original heap *) destruct Hprop as [rqt [Hrtype_orig Hsubtype_orig]]. assert (loc < dom h). { (apply runtime_getObj_dom in Hobj_loc). exact Hobj_loc. } rewrite runtime_getObj_last2; auto. rewrite Hobj_loc. exists rqt. split. -- unfold r_type in Hrtype_orig |- *. rewrite runtime_getObj_last2; auto. -- exact Hsubtype_orig. * contradiction Hprop. } } + (* Length of runtime environment greater than 0 *) simpl. destruct Hsenv as [HsenvLength HsenvWellTyped]. subst. rewrite update_length. rewrite <- Hlen. exact HsenvLength. + destruct Hrenv as [HrEnvLen [Hreceiverval Hallvals]]. destruct Hreceiverval as [iot Hiot]. destruct Hiot as [Hiot Hiot_dom]. exists iot. simpl. unfold gget in *. destruct (vars rΓ) as [|v0 vs] eqn:Hvars. * (* Case: vars rΓ = [] *) exfalso. simpl in HrEnvLen. lia. * (* Case: vars rΓ = v0 :: vs *) destruct x as [|x']. -- (* x = S x' *) split. --- (* Show update preserves position 0 *) simpl. exfalso. easy. --- (* Show iot is still in extended heap domain *) subst. rewrite length_app. simpl. lia. -- split. subst. exact Hiot. rewrite length_app. simpl. lia. + destruct Hrenv as [HrEnvLen [Hreceiverval Hallvals]]. simpl. subst. apply Forall_update. * eapply Forall_impl; [| exact Hallvals]. intros v Hv. destruct v as [|loc]; [trivial|]. destruct (runtime_getObj h loc) as [obj|] eqn:Hobj; [| contradiction]. assert (Hloc_dom : loc < dom h) by (apply runtime_getObj_dom in Hobj; exact Hobj). rewrite runtime_getObj_last2. -- exact Hloc_dom. -- rewrite Hobj. trivial. * (* Show new object is well-formed *) assert (dom h + 1 = S (dom h)) by lia. unfold runtime_getObj. simpl. assert (Hlen_extended: dom (h ++ [{| rt_type := {| rqtype := vpa_mutability_object_creation qthisr q_c; rctype := c |}; fields_map := vals |}]) = dom h + 1). -- rewrite length_app. simpl. lia. -- rewrite nth_error_app2. ** lia. ** replace (dom h - dom h) with 0 by lia. simpl. reflexivity. * assert (Hx_dom : x < dom sΓ') by (apply static_getType_dom in Hget_x; exact Hget_x). rewrite <- Hlen; exact Hx_dom. + destruct Hsenv as [HsenvLength HsenvWellTyped]. subst. exact HsenvLength. + destruct Hsenv as [HsenvLength HsenvWellTyped]. subst. exact HsenvWellTyped. + subst. rewrite update_length. rewrite <- Hlen. lia. + { intros ι qcontext HreceiverAddr Hreceivermut i Hi sqt Hnth. destruct (Nat.eq_dec i x) as [Heq | Hneq]. - (* Case: i = x (newly assigned variable) *) subst i. simpl. unfold runtime_getVal. subst. rewrite update_same. + assert (Hx_dom : x < dom sΓ') by (apply static_getType_dom in Hget_x; exact Hget_x). rewrite <- Hlen. exact Hx_dom. + (* Show wf_r_typable for the new object *) { unfold wf_r_typable. unfold r_type. rewrite runtime_getObj_last. simpl. unfold get_this_var_mapping. simpl. destruct (vars rΓ) as [|v0 vs] eqn:Hvars. - exfalso. unfold wf_renv in Hrenv. destruct Hrenv as [HrEnvLen _]. rewrite Hvars in HrEnvLen. simpl in HrEnvLen. lia. - unfold r_muttype. destruct x as [|x']. + (* Case: x = 0 *) easy. + (* Case: x = S x' *) simpl. unfold r_muttype. unfold static_getType in Hget_x. rewrite Hget_x in Hnth. inversion Hnth. subst sqt. split. apply qualified_type_subtype_base_subtype in Hresult_sub. unfold qc2q in Hresult_sub. simpl in Hresult_sub. exact Hresult_sub. apply qualified_type_subtype_q_subtype in Hresult_sub. simpl in Hresult_sub. unfold wf_senv in Hsenv; destruct Hsenv as [Hsenvdom _]; destruct (r_type h ι) as [rqt_receiver|] eqn: Hrtype_receiver. assert(H100: qcontext = rqtype rqt_receiver). { unfold r_type in Hrtype_receiver. destruct (runtime_getObj h ι) eqn: save; [|easy]. assert (Hι_dom : ι < dom h). { apply runtime_getObj_dom in save. exact save. } pose proof Hreceivermut as Hreceivermut_old. eapply r_muttype_app_preserve_old_Some in Hreceivermut_old; eauto. unfold r_muttype in Hreceivermut_old. rewrite save in Hreceivermut_old. inversion Hreceivermut_old; subst. inversion Hrtype_receiver; subst. reflexivity. } 2:{ unfold r_type in Hrtype_receiver. unfold r_muttype in Hreceivermut. simpl in HreceiverAddr. destruct v0 as [|]; [easy|]. inversion HreceiverAddr; subst. destruct (runtime_getObj h ι) eqn: save. 2:{ destruct Hrenv as [HrEnvLen [Hrecv Hallvals]]. destruct Hrecv as [ι0 [Hthis' Hι0_dom]]. rewrite Hvars in Hthis'. simpl in Hthis'. inversion Hthis'; subst ι0. exfalso. apply runtime_getObj_not_dom in save. lia. } discriminate Hrtype_receiver. } unfold r_type in Hrtype_receiver. destruct (runtime_getObj h ι) eqn: save; [|easy]. have save_copy := save. apply runtime_getObj_dom in save. apply r_muttype_app_preserve_old_Some in Hreceivermut; auto. rewrite (get_this_var_mapping_update_nonzero (v0 :: vs) (S x') (Iot (dom h))) in HreceiverAddr. discriminate. specialize (Hcorr ι qcontext HreceiverAddr Hreceivermut 0 Hsenvdom Tthis Hthis). rewrite Hgetthis in Hcorr. unfold wf_r_typable in Hcorr. unfold r_type in Hcorr. assert (l1 = ι). { rewrite <- Hvars in HreceiverAddr. pose proof (get_this_var_mapping_runtime_getVal rΓ ι HreceiverAddr) as Hthis_rt. rewrite Hgetthis in Hthis_rt. inversion Hthis_rt; subst; reflexivity. } subst l1. rewrite save_copy in Hcorr. destruct Hcorr as [_ Hqual_receiver]. inversion Hrtype_receiver. subst rqt_receiver. rewrite <- H100 in Hqual_receiver. assert (qcontext = qthisr). { rewrite HgetthisRuntimeType in Hreceivermut. inversion Hreceivermut; reflexivity. } subst qthisr. unfold qualifier_typable_context in *. unfold vpa_mutability_object_creation in *. unfold vpa_mutability_runtime in *; unfold qc2q in *; unfold vpa_mutability_tt_abstract_state in *. unfold vpa_mutability_bound in Hqc. destruct q_c eqn:Hnewq; destruct (cqualifier consig) eqn: Hcbound; destruct qcontext eqn: Hqcontext; destruct (rqtype (rt_type o)) eqn: Hrqtq; destruct (sqtype Tx) eqn: Htxq; try easy. all: destruct (sqtype Tthis) eqn: Hqthisr; try rewrite Htxq in Hresult_sub; simpl in Hresult_sub; try inversion Hresult_sub; try easy. } - (* Case: i ≠ x (existing variable) *) simpl. unfold runtime_getVal. subst. rewrite update_diff; auto. rewrite get_this_var_mapping_update_vars_nonzero in HreceiverAddr; auto. (* Show that the original wf_r_typable holds *) assert (r_muttype h ι = Some qcontext) as Hreceivermut_orig. { eapply r_muttype_app_preserve_old_Some in Hreceivermut; eauto. destruct Hrenv as [HrEnvLen [Hrecv Hallvals]]. destruct Hrecv as [ι0 [Hthis' Hι0_dom]]. rewrite Hthis' in HreceiverAddr. inversion HreceiverAddr; subst ι. exact Hι0_dom. } assert (Hcorr_orig := Hcorr ι qcontext HreceiverAddr Hreceivermut_orig i Hi sqt Hnth). destruct (runtime_getVal rΓ i) as [v|] eqn:Hval. + (* Case: runtime_getVal rΓ i = Some v *) destruct v as [|loc]. * (* Case: v = Null_a *) unfold runtime_getVal in Hval. rewrite Hval. trivial. * (* Case: v = Iot loc *) unfold runtime_getVal in Hval. rewrite Hval. unfold wf_r_typable in Hcorr_orig |- *. destruct (r_type h loc) as [rqt|] eqn:Hrtype; [|contradiction]. assert (Hrtype_ext : r_type (h ++ [{| rt_type := {| rqtype := vpa_mutability_object_creation qthisr q_c; rctype := c |}; fields_map := vals |}]) loc = Some rqt). { unfold r_type in Hrtype |- *. rewrite heap_extension_preserves_objects; auto. destruct (runtime_getObj h loc) as [obj|] eqn:Hobj; [|discriminate]. apply runtime_getObj_dom in Hobj. exact Hobj. } rewrite Hrtype_ext. exact Hcorr_orig. + contradiction Hcorr_orig. } Qed. Lemma receiver_mutability_exists_from_bound : forall h ι (Hlt : ι < dom h), exists q, r_muttype h ι = Some q. Proof. intros h ι Hlt. unfold r_muttype. destruct (runtime_getObj h ι) as [o|] eqn:Hobj. - eexists. reflexivity. - exfalso. apply runtime_getObj_not_dom in Hobj. lia. Qed. Lemma static_getType_list_index_strong : forall sΓ zs argtypes i j argtype (Hmap : mapM (fun x => static_getType sΓ x) zs = Some argtypes) (Hzs : nth_error zs i = Some j) (Hargs : nth_error argtypes i = Some argtype), static_getType sΓ j = Some argtype. Proof. intros sΓ zs. induction zs as [|z zs' IH]; intros argtypes i j argtype Hmap Hzs Hargs. - (* zs = [] *) simpl in Hmap. inversion Hmap; subst argtypes. simpl in Hargs. inversion Hzs. exfalso. rewrite nth_error_nil in Hzs. discriminate Hzs. - (* zs = z :: zs' *) simpl in Hmap. destruct (static_getType sΓ z) as [Tz|] eqn:HTz; try discriminate. destruct (mapM (fun x : Loc => static_getType sΓ x) zs') as [argtypes'|] eqn:Hrec; try discriminate. inversion Hmap; subst argtypes; clear Hmap. destruct i as [|i']. + (* i = 0 *) simpl in Hzs, Hargs. inversion Hzs; subst j. inversion Hargs; subst argtype. exact HTz. + (* i = S i' *) simpl in Hzs, Hargs. eapply IH; eauto. Qed. Lemma static_getType_list_nth_zs : forall sΓ zs argtypes i argtype (Hlist : static_getType_list sΓ zs = Some argtypes) (Hnth : nth_error argtypes i = Some argtype), exists j, nth_error zs i = Some j /\ static_getType sΓ j = Some argtype. Proof. intros sΓ zs. induction zs as [|z zs' IH]; intros argtypes i argtype Hlist Hnth. - (* zs = [] *) simpl in Hlist. inversion Hlist; subst argtypes. simpl in Hnth. rewrite nth_error_nil in Hnth. discriminate. - (* zs = z :: zs' *) simpl in Hlist. destruct (static_getType sΓ z) as [Tz|] eqn:HTz. 2:{ exfalso. unfold static_getType_list in Hlist. simpl in Hlist. rewrite HTz in Hlist. discriminate Hlist. } destruct (mapM (fun x : Loc => static_getType sΓ x) zs') as [argtypes'|] eqn:Hrec. 2:{ unfold static_getType_list in Hlist. simpl in Hlist. rewrite HTz in Hlist. rewrite Hrec in Hlist. discriminate Hlist. } (* inversion Hlist; subst argtypes; clear Hlist. *) destruct i as [|i']. + (* i = 0 *) unfold static_getType_list in Hlist. simpl in Hlist. rewrite HTz in Hlist. rewrite Hrec in Hlist. inversion Hlist; subst argtypes; clear Hlist. simpl in Hnth. inversion Hnth; subst argtype; clear Hnth. exists z. split; [simpl; reflexivity | exact HTz]. + (* i = S i' *) simpl in Hnth. unfold static_getType_list in Hlist. simpl in Hlist. rewrite HTz in Hlist. rewrite Hrec in Hlist. inversion Hlist as [Heq_argtypes]; subst argtypes; clear Hlist. simpl in Hnth. (* nth_error (Tz :: argtypes') (S i') = nth_error argtypes' i' *) destruct (IH argtypes' i' argtype Hrec Hnth) as [j [Hnth_zs Hj]]. exists j. split; simpl; assumption. Qed. Lemma runtime_lookup_list_nth_zs : forall rΓ zs vals i v (Hlist : runtime_lookup_list rΓ zs = Some vals) (Hnth : nth_error vals i = Some v), exists j, nth_error zs i = Some j /\ runtime_getVal rΓ j = Some v. Proof. intros rΓ zs. induction zs as [|z zs' IH]; intros vals i v Hlist Hnth. - (* zs = [] *) simpl in Hlist. inversion Hlist; subst vals. simpl in Hnth. rewrite nth_error_nil in Hnth. discriminate. - (* zs = z :: zs' *) simpl in Hlist. destruct (runtime_getVal rΓ z) as [Vz|] eqn:HVz. 2:{ exfalso. unfold runtime_lookup_list in Hlist. simpl in Hlist. rewrite HVz in Hlist. discriminate Hlist. } destruct (mapM (fun x : Loc => runtime_getVal rΓ x) zs') as [vals'|] eqn:Hrec. 2:{ unfold runtime_lookup_list in Hlist. simpl in Hlist. rewrite HVz in Hlist. rewrite Hrec in Hlist. discriminate Hlist. } destruct i as [|i']. + (* i = 0 *) unfold runtime_lookup_list in Hlist. simpl in Hlist. rewrite HVz in Hlist. rewrite Hrec in Hlist. inversion Hlist; subst vals; clear Hlist. simpl in Hnth. inversion Hnth; subst v; clear Hnth. exists z. split; [simpl; reflexivity | exact HVz]. + (* i = S i' *) simpl in Hnth. unfold runtime_lookup_list in Hlist. simpl in Hlist. rewrite HVz in Hlist. rewrite Hrec in Hlist. inversion Hlist as [Heq_vals]; subst vals; clear Hlist. simpl in Hnth. (* nth_error (Vz :: vals') (S i') = nth_error vals' i' *) destruct (IH vals' i' v Hrec Hnth) as [j [Hnth_zs Hj]]. exists j. split; simpl; assumption. Qed.
A statically typed variable that evaluates to a non-null location has a
runtime class below its static class. This is the caller-side fact needed
to relate static and dynamically selected method signatures.
Lemma runtime_value_base_subtype : forall CT sΓ rΓ h y Ty ly cy (Hwf : wf_r_config CT sΓ rΓ h) (Hget_y : static_getType sΓ y = Some Ty) (Hval_y : runtime_getVal rΓ y = Some (Iot ly)) (Hbase : r_basetype h ly = Some cy), base_subtype CT cy (sctype Ty). Proof. intros CT sΓ rΓ h y Ty ly cy Hwf Hget_y Hval_y Hbase. unfold wf_r_config in Hwf. destruct Hwf as [_ [_ [Hrenv [_ [_ Hcorr]]]]]. unfold wf_renv in Hrenv. destruct Hrenv as [_ [[receiver [Hreceiver Hreceiver_dom]] _]]. destruct (receiver_mutability_exists_from_bound h receiver Hreceiver_dom) as [qcontext Hqcontext]. specialize (Hcorr receiver qcontext Hreceiver Hqcontext). assert (Hy_dom : y < dom sΓ). { apply static_getType_dom in Hget_y. exact Hget_y. } specialize (Hcorr y Hy_dom Ty Hget_y). rewrite Hval_y in Hcorr. unfold wf_r_typable, r_type in Hcorr. unfold r_basetype in Hbase. destruct (runtime_getObj h ly) as [obj|] eqn:Hobj; [|discriminate]. destruct obj as [[rq rc] fields]. simpl in Hbase, Hcorr. injection Hbase as Hcy; subst rc. exact (proj1 Hcorr). Qed.
Class-bound receiver adaptation preserves runtime qualifier typability.
This is the semantic form needed when an override specializes an RDM
formal using the overriding class bound.
Lemma runtime_qualifier_agrees_with_super_bound : forall CT runtime_class declaring_class qr qc, wf_class_table CT -> base_subtype CT runtime_class declaring_class -> wf_rtypeuse CT qr runtime_class -> bound CT declaring_class = Some qc -> vpa_mutability_runtime_bound_agree qr qc = true. Proof. intros CT runtime_class declaring_class qr qc Hwf Hsub. revert qr qc. induction Hsub; intros qr qc Hrt Hbound. - unfold wf_rtypeuse in Hrt. rewrite Hbound in Hrt. tauto. - unfold wf_rtypeuse in Hrt. destruct (bound CT C) as [qC|] eqn:HC; [|contradiction]. destruct Hrt as [HCdom Hagree]. destruct (bound CT D) as [qD|] eqn:HD. + eapply IHHsub2; eauto. unfold wf_rtypeuse. rewrite HD. split. * eapply base_subtype_domain with (C := C); eauto. * eapply IHHsub1; eauto. unfold wf_rtypeuse. rewrite HC. auto. + exfalso. have HDdom : D < dom CT. { eapply base_subtype_domain with (C := C); eauto. } apply find_class_Some in HDdom. destruct HDdom as [ddef HfindD]. unfold bound in HD. rewrite HfindD in HD. discriminate. - unfold wf_rtypeuse in Hrt. destruct (bound CT C) as [qC|] eqn:HC; [|contradiction]. destruct Hrt as [_ Hagree]. unfold parent_lookup in Hparent. destruct (find_class CT C) as [cdef|] eqn:HfindC; [|discriminate]. have Hwf_class : wf_class CT cdef. { unfold wf_class_table in Hwf. destruct Hwf as [Hall _]. eapply Forall_nth_error; eauto. } inversion Hwf_class; subst. + rewrite Hno_super in Hparent. discriminate. + assert (D = superC) by congruence. subst D. unfold bound in HC. rewrite HfindC in HC. simpl in HC. injection HC as <-. destruct H as [_ [_ [_ Hbounds]]]. rewrite Hbound in Hbounds. destruct Hbounds as [fs [_ [[Heq | Heq] _]]]. * rewrite <- Heq. exact Hagree. * subst qc. destruct qr; reflexivity. Qed. Lemma override_parameter_qualifier_typable : forall qr qcontext qc parent_q child_q, vpa_mutability_runtime_bound_agree qcontext qc = true -> qualifier_typable_context qr parent_q qcontext -> q_subtype (vpa_mutability_qq_abstract_state (qc2q qc) parent_q) child_q -> qualifier_typable_context qr child_q qcontext. Proof. intros qr qcontext qc parent_q child_q Hagree Hparent Hsub. destruct qr, qcontext, qc, parent_q, child_q; simpl in *; try discriminate; try contradiction; try solve [inversion Hsub; subst; simpl; auto]. Qed. Lemma wf_r_typable_override_parameter : forall CT h loc parent_type child_type qcontext qc, vpa_mutability_runtime_bound_agree qcontext qc = true -> wf_r_typable CT h loc parent_type qcontext -> qualified_type_subtype CT (vpa_mutability_override qc parent_type) child_type -> wf_r_typable CT h loc child_type qcontext. Proof. intros CT h loc parent_type child_type qcontext qc Hagree Hparent Hsub. unfold wf_r_typable in *. destruct (r_type h loc) as [rt|] eqn:Hrt; [|contradiction]. destruct Hparent as [Hbase Hqual]. split. - eapply base_trans; [exact Hbase|]. apply qualified_type_subtype_base_subtype in Hsub. unfold vpa_mutability_override in Hsub. simpl in Hsub. exact Hsub. - eapply override_parameter_qualifier_typable; eauto. apply qualified_type_subtype_q_subtype in Hsub. unfold vpa_mutability_override in Hsub. simpl in Hsub. exact Hsub. Qed.
Covariant results move in the opposite direction from parameters: a
value valid at the overriding result type is valid at the overridden
result type when the runtime receiver agrees with the overriding class
bound.
Lemma override_return_qualifier_typable : forall qr qcontext qc child_q parent_q, vpa_mutability_runtime_bound_agree qcontext qc = true -> qualifier_typable_context qr child_q qcontext -> q_subtype child_q (vpa_mutability_qq_abstract_state (qc2q qc) parent_q) -> qualifier_typable_context qr parent_q qcontext. Proof. intros qr qcontext qc child_q parent_q Hagree Hchild Hsub. destruct qr, qcontext, qc, child_q, parent_q; simpl in *; try discriminate; try contradiction; try solve [inversion Hsub; subst; simpl; auto]. Qed. Lemma wf_r_typable_override_return : forall CT h loc child_type parent_type qcontext qc, vpa_mutability_runtime_bound_agree qcontext qc = true -> wf_r_typable CT h loc child_type qcontext -> qualified_type_subtype CT child_type (vpa_mutability_override qc parent_type) -> wf_r_typable CT h loc parent_type qcontext. Proof. intros CT h loc child_type parent_type qcontext qc Hagree Hchild Hsub. unfold wf_r_typable in *. destruct (r_type h loc) as [rt|] eqn:Hrt; [|contradiction]. destruct Hchild as [Hbase Hqual]. split. - eapply base_trans; [exact Hbase|]. apply qualified_type_subtype_base_subtype in Hsub. unfold vpa_mutability_override in Hsub. simpl in Hsub. exact Hsub. - eapply override_return_qualifier_typable; eauto. apply qualified_type_subtype_q_subtype in Hsub. unfold vpa_mutability_override in Hsub. simpl in Hsub. exact Hsub. Qed.
The two call-site adaptations preserve runtime result typability across
the target receiver's runtime context and the caller's context.
Lemma call_return_qualifier_typable_abstract : forall qresult qtarget qcaller receiver_q return_q result_q, qualifier_typable_context qtarget receiver_q qcaller -> qualifier_typable_context qresult return_q qtarget -> q_subtype (vpa_mutability_qq_abstract_state receiver_q return_q) result_q -> qualifier_typable_context qresult result_q qcaller. Proof. intros qresult qtarget qcaller receiver_q return_q result_q Htarget Hreturn Hsub. destruct qresult, qtarget, qcaller, receiver_q, return_q, result_q; simpl in *; try contradiction; try solve [inversion Hsub; subst; simpl; auto]. Qed. Lemma call_return_qualifier_typable_readonly : forall qresult qtarget qcaller receiver_q return_q result_q, qualifier_typable_context qtarget receiver_q qcaller -> qualifier_typable_context qresult return_q qtarget -> q_subtype (vpa_mutability_qq_readonly_state receiver_q return_q) result_q -> qualifier_typable_context qresult result_q qcaller. Proof. intros qresult qtarget qcaller receiver_q return_q result_q Htarget Hreturn Hsub. destruct qresult, qtarget, qcaller, receiver_q, return_q, result_q; simpl in *; try contradiction; try solve [inversion Hsub; subst; simpl; auto]. Qed. Lemma wf_r_typable_call_return_abstract : forall CT h target_loc result_loc caller_context target_type return_type result_type target_context, r_muttype h target_loc = Some target_context -> wf_r_typable CT h target_loc target_type caller_context -> wf_r_typable CT h result_loc return_type target_context -> qualified_type_subtype CT (vpa_mutability_tt_abstract_state target_type return_type) result_type -> wf_r_typable CT h result_loc result_type caller_context. Proof. intros CT h target_loc result_loc caller_context target_type return_type result_type target_context Htarget_context Htarget Hreturn Hsub. unfold wf_r_typable in Htarget, Hreturn |- *. destruct (r_type h target_loc) as [target_rt|] eqn:Htarget_rt; [|contradiction]. destruct (r_type h result_loc) as [result_rt|] eqn:Hresult_rt; [|contradiction]. unfold r_muttype, r_type in Htarget_context. destruct (runtime_getObj h target_loc) as [target_obj|] eqn:Htarget_obj; [|discriminate]. unfold r_type in Htarget_rt. rewrite Htarget_obj in Htarget_rt. injection Htarget_rt as <-. simpl in Htarget_context. injection Htarget_context as <-. destruct Htarget as [_ Htarget_qual]. destruct Hreturn as [Hreturn_base Hreturn_qual]. split. - eapply base_trans; [exact Hreturn_base|]. apply qualified_type_subtype_base_subtype in Hsub. unfold vpa_mutability_tt_abstract_state in Hsub. simpl in Hsub. exact Hsub. - eapply call_return_qualifier_typable_abstract; eauto. apply qualified_type_subtype_q_subtype in Hsub. unfold vpa_mutability_tt_abstract_state in Hsub. simpl in Hsub. exact Hsub. Qed. Lemma wf_r_typable_call_return_readonly : forall CT h target_loc result_loc caller_context target_type return_type result_type target_context, r_muttype h target_loc = Some target_context -> wf_r_typable CT h target_loc target_type caller_context -> wf_r_typable CT h result_loc return_type target_context -> qualified_type_subtype CT (vpa_mutability_tt_readonly_state target_type return_type) result_type -> wf_r_typable CT h result_loc result_type caller_context. Proof. intros CT h target_loc result_loc caller_context target_type return_type result_type target_context Htarget_context Htarget Hreturn Hsub. unfold wf_r_typable in Htarget, Hreturn |- *. destruct (r_type h target_loc) as [target_rt|] eqn:Htarget_rt; [|contradiction]. destruct (r_type h result_loc) as [result_rt|] eqn:Hresult_rt; [|contradiction]. unfold r_muttype, r_type in Htarget_context. destruct (runtime_getObj h target_loc) as [target_obj|] eqn:Htarget_obj; [|discriminate]. unfold r_type in Htarget_rt. rewrite Htarget_obj in Htarget_rt. injection Htarget_rt as <-. simpl in Htarget_context. injection Htarget_context as <-. destruct Htarget as [_ Htarget_qual]. destruct Hreturn as [Hreturn_base Hreturn_qual]. split. - eapply base_trans; [exact Hreturn_base|]. apply qualified_type_subtype_base_subtype in Hsub. unfold vpa_mutability_tt_readonly_state in Hsub. simpl in Hsub. exact Hsub. - eapply call_return_qualifier_typable_readonly; eauto. apply qualified_type_subtype_q_subtype in Hsub. unfold vpa_mutability_tt_readonly_state in Hsub. simpl in Hsub. exact Hsub. Qed. Lemma override_preserves_callee_frame : forall CT h ly vals cy qc child parent, wf_r_config CT (mreceiver parent :: mparams parent) (mkr_env (Iot ly :: vals)) h -> r_basetype h ly = Some cy -> base_subtype CT cy (sctype (mreceiver child)) -> bound CT (sctype (mreceiver child)) = Some qc -> base_subtype CT (sctype (mreceiver child)) (sctype (mreceiver parent)) -> wf_senv CT (mreceiver child :: mparams child) -> method_override_compatible CT qc child parent -> wf_r_config CT (mreceiver child :: mparams child) (mkr_env (Iot ly :: vals)) h. Proof. intros CT h ly vals cy qc child parent Hwf Hbase Hruntime_sub Hbound Hreceiver_base Hchild_senv Hoverride. unfold method_override_compatible in Hoverride. destruct Hoverride as [_ [_ [_ [Hparams Hreceiver_qual]]]]. unfold wf_r_config in Hwf. destruct Hwf as [Hclass [Hheap [Hrenv [Hparent_senv [Hlength Hcorr]]]]]. split; [exact Hclass|]. split; [exact Hheap|]. split; [exact Hrenv|]. split; [exact Hchild_senv|]. split. - simpl in Hlength |- *. have Hparams_length := Forall2_length Hparams. simpl. lia. - intros receiver qcontext Hget_receiver Hget_context i Hi child_type Hchild_nth. simpl in Hget_receiver. injection Hget_receiver as <-. have Hly_dom : ly < dom h. { unfold wf_renv in Hrenv. destruct Hrenv as [_ [[receiver [Hget Hdom]] _]]. simpl in Hget. injection Hget as <-. exact Hdom. } have Hwf_obj := Hheap ly Hly_dom. unfold wf_obj in Hwf_obj. unfold r_basetype in Hbase. destruct (runtime_getObj h ly) as [receiver_obj|] eqn:Hobj; [|discriminate]. unfold r_muttype in Hget_context. rewrite Hobj in Hget_context. destruct receiver_obj as [[receiver_q receiver_class] receiver_fields]. simpl in Hget_context, Hbase, Hwf_obj. injection Hget_context as Hqeq. subst receiver_q. have Hcontext : r_muttype h ly = Some qcontext. { unfold r_muttype. rewrite Hobj. reflexivity. } destruct Hwf_obj as [Hruntime_type _]. injection Hbase as Hclass_eq. subst cy. have Hagree : vpa_mutability_runtime_bound_agree qcontext qc = true. { eapply runtime_qualifier_agrees_with_super_bound. - exact Hclass. - exact Hruntime_sub. - exact Hruntime_type. - exact Hbound. } destruct i as [|i']. + simpl in Hchild_nth. injection Hchild_nth as <-. simpl. have Hparent_receiver : wf_r_typable CT h ly (mreceiver parent) qcontext. { specialize (Hcorr ly qcontext eq_refl Hcontext 0). simpl in Hcorr. exact (Hcorr ltac:(lia) (mreceiver parent) eq_refl). } unfold wf_r_typable in Hparent_receiver |- *. unfold r_type in Hparent_receiver |- *. rewrite Hobj in Hparent_receiver |- *. simpl in Hparent_receiver |- *. destruct Hparent_receiver as [_ Hparent_qual]. split; [exact Hruntime_sub|]. eapply override_parameter_qualifier_typable; eauto. + simpl in Hchild_nth, Hi |- *. have Hchild_index : i' < length (mparams child). { apply nth_error_Some. rewrite Hchild_nth. discriminate. } have Hparams_length := Forall2_length Hparams. have Hparent_index : i' < length (mparams parent) by lia. destruct (nth_error (mparams parent) i') as [parent_type|] eqn:Hparent_nth. 2:{ apply nth_error_None in Hparent_nth. lia. } have Hparam_sub : qualified_type_subtype CT (vpa_mutability_override qc parent_type) child_type. { eapply Forall2_nth_error in Hparams; eauto. } specialize (Hcorr ly qcontext eq_refl Hcontext (S i')). simpl in Hcorr. have Hparent_value := Hcorr ltac:(lia) parent_type Hparent_nth. unfold runtime_getVal in Hparent_value |- *. simpl in Hparent_value |- *. destruct (nth_error vals i') as [value|] eqn:Hvalue; [|exact Hparent_value]. destruct value as [|loc]; [trivial|]. eapply wf_r_typable_override_parameter; eauto. Qed. Lemma refinement_preserves_callee_frame : forall CT h ly vals cy child parent, method_signature_refinement CT child parent -> wf_r_config CT (mreceiver parent :: mparams parent) (mkr_env (Iot ly :: vals)) h -> r_basetype h ly = Some cy -> base_subtype CT cy (sctype (mreceiver child)) -> wf_r_config CT (mreceiver child :: mparams child) (mkr_env (Iot ly :: vals)) h. Proof. intros CT h ly vals cy child parent Hrefine. induction Hrefine; intros Hwf Hbase Hruntime_sub. - exact Hwf. - eapply override_preserves_callee_frame; eauto. - have Hchild_dom : sctype (mreceiver child) < dom CT. { eapply base_subtype_domain; exact Hruntime_sub. } have Hchild_middle : base_subtype CT (sctype (mreceiver child)) (sctype (mreceiver middle)). { eapply method_signature_refinement_receiver_base; eauto. } have Hruntime_middle : base_subtype CT cy (sctype (mreceiver middle)). { eapply base_trans; eauto. } have Hmiddle_frame : wf_r_config CT (mreceiver middle :: mparams middle) (mkr_env (Iot ly :: vals)) h. { eapply IHHrefine2; eauto. } eapply IHHrefine1; eauto. Qed. Lemma refinement_preserves_return_typability : forall CT h loc cy qcontext child parent, method_signature_refinement CT child parent -> (forall C qc, base_subtype CT cy C -> bound CT C = Some qc -> vpa_mutability_runtime_bound_agree qcontext qc = true) -> base_subtype CT cy (sctype (mreceiver child)) -> wf_r_typable CT h loc (mret child) qcontext -> wf_r_typable CT h loc (mret parent) qcontext. Proof. intros CT h loc cy qcontext child parent Hrefine. induction Hrefine; intros Hagree Hruntime_sub Hvalue. - exact Hvalue. - match goal with | Hbound : bound CT (sctype (mreceiver overrider)) = Some qc, Hcompat : method_override_compatible CT qc overrider overridden |- _ => unfold method_override_compatible in Hcompat; destruct Hcompat as [_ [_ [Hreturn _]]]; eapply wf_r_typable_override_return; [eapply Hagree; eauto | exact Hvalue | exact Hreturn] end. - have Hchild_dom : sctype (mreceiver child) < dom CT. { eapply base_subtype_domain; exact Hruntime_sub. } have Hchild_middle : base_subtype CT (sctype (mreceiver child)) (sctype (mreceiver middle)). { eapply method_signature_refinement_receiver_base; eauto. } have Hruntime_middle : base_subtype CT cy (sctype (mreceiver middle)). { eapply base_trans; eauto. } have Hmiddle_value : wf_r_typable CT h loc (mret middle) qcontext. { eapply IHHrefine1; eauto. } eapply IHHrefine2; eauto. Qed.
A result produced by the dynamically selected implementation can be
transported back to the statically selected signature, and then through
the call-site viewpoint adaptation. This is the semantic counterpart of
class-bound adapted behavioral subtyping; dispatch itself needs no
compatibility premise.
Lemma refinement_preserves_call_result_abstract : forall CT h target_loc result_loc cy qtarget qcaller target_type result_type child parent, wf_class_table CT -> wf_heap CT h -> r_basetype h target_loc = Some cy -> r_muttype h target_loc = Some qtarget -> wf_r_typable CT h target_loc target_type qcaller -> method_signature_refinement CT child parent -> base_subtype CT cy (sctype (mreceiver child)) -> wf_r_typable CT h result_loc (mret child) qtarget -> qualified_type_subtype CT (vpa_mutability_tt_abstract_state target_type (mret parent)) result_type -> wf_r_typable CT h result_loc result_type qcaller. Proof. intros CT h target_loc result_loc cy qtarget qcaller target_type result_type child parent Hclass Hheap Hbase Htarget_context Htarget Hrefine Hruntime_sub Hresult Hcall_sub. have Htarget_dom : target_loc < dom h. { unfold r_basetype in Hbase. destruct (runtime_getObj h target_loc) as [target_obj|] eqn:Hobj; [eapply runtime_getObj_dom; eauto | discriminate]. } have Hwf_target := Hheap target_loc Htarget_dom. unfold wf_obj in Hwf_target. unfold r_basetype, r_muttype in Hbase, Htarget_context. destruct (runtime_getObj h target_loc) as [[[runtime_q runtime_c] target_fields]|] eqn:Htarget_obj; [|discriminate]. simpl in Hbase, Htarget_context, Hwf_target. injection Hbase as <-. injection Htarget_context as <-. destruct Hwf_target as [Hruntime_type _]. have Hagree : forall C qc, base_subtype CT runtime_c C -> bound CT C = Some qc -> vpa_mutability_runtime_bound_agree runtime_q qc = true. { intros C qc Hsub Hbound. eapply runtime_qualifier_agrees_with_super_bound; eauto. } have Hstatic_result : wf_r_typable CT h result_loc (mret parent) runtime_q. { eapply refinement_preserves_return_typability; eauto. } eapply wf_r_typable_call_return_abstract; eauto. unfold r_muttype. rewrite Htarget_obj. reflexivity. Qed. Lemma refinement_preserves_call_result_readonly : forall CT h target_loc result_loc cy qtarget qcaller target_type result_type child parent, wf_class_table CT -> wf_heap CT h -> r_basetype h target_loc = Some cy -> r_muttype h target_loc = Some qtarget -> wf_r_typable CT h target_loc target_type qcaller -> method_signature_refinement CT child parent -> base_subtype CT cy (sctype (mreceiver child)) -> wf_r_typable CT h result_loc (mret child) qtarget -> qualified_type_subtype CT (vpa_mutability_tt_readonly_state target_type (mret parent)) result_type -> wf_r_typable CT h result_loc result_type qcaller. Proof. intros CT h target_loc result_loc cy qtarget qcaller target_type result_type child parent Hclass Hheap Hbase Htarget_context Htarget Hrefine Hruntime_sub Hresult Hcall_sub. have Htarget_dom : target_loc < dom h. { unfold r_basetype in Hbase. destruct (runtime_getObj h target_loc) as [target_obj|] eqn:Hobj; [eapply runtime_getObj_dom; eauto | discriminate]. } have Hwf_target := Hheap target_loc Htarget_dom. unfold wf_obj in Hwf_target. unfold r_basetype, r_muttype in Hbase, Htarget_context. destruct (runtime_getObj h target_loc) as [[[runtime_q runtime_c] target_fields]|] eqn:Htarget_obj; [|discriminate]. simpl in Hbase, Htarget_context, Hwf_target. injection Hbase as <-. injection Htarget_context as <-. destruct Hwf_target as [Hruntime_type _]. have Hagree : forall C qc, base_subtype CT runtime_c C -> bound CT C = Some qc -> vpa_mutability_runtime_bound_agree runtime_q qc = true. { intros C qc Hsub Hbound. eapply runtime_qualifier_agrees_with_super_bound; eauto. } have Hstatic_result : wf_r_typable CT h result_loc (mret parent) runtime_q. { eapply refinement_preserves_return_typability; eauto. } eapply wf_r_typable_call_return_readonly; eauto. unfold r_muttype. rewrite Htarget_obj. reflexivity. Qed. Lemma runtime_call_signature_refines : forall CT sΓ rΓ h y Ty ly cy m mdef_runtime mdef_static (Hwf : wf_r_config CT sΓ rΓ h) (Hget_y : static_getType sΓ y = Some Ty) (Hval_y : runtime_getVal rΓ y = Some (Iot ly)) (Hbase : r_basetype h ly = Some cy) (Hfind_runtime : FindMethodWithName CT cy m mdef_runtime) (Hfind_static : FindMethodWithName CT (sctype Ty) m mdef_static), method_signature_refinement CT (msignature mdef_runtime) (msignature mdef_static). Proof. intros. eapply method_signature_refines_subtype; eauto. - unfold wf_r_config in Hwf. exact (proj1 Hwf). - eapply runtime_value_base_subtype; eauto. Qed. Lemma runtime_call_scope_eq : forall CT sΓ rΓ h y Ty ly cy m mdef_runtime mdef_static, wf_r_config CT sΓ rΓ h -> static_getType sΓ y = Some Ty -> runtime_getVal rΓ y = Some (Iot ly) -> r_basetype h ly = Some cy -> FindMethodWithName CT cy m mdef_runtime -> FindMethodWithName CT (sctype Ty) m mdef_static -> mscope (msignature mdef_runtime) = mscope (msignature mdef_static). Proof. intros. eapply method_signature_refinement_scope_eq. eapply runtime_call_signature_refines; eauto. Qed.