Require syntax.
Require Lattice.
Require SumLattice.
Require func.
Require StackLattice.
Require AbVal.
Require FiniteSet.
Require semantic.
Require analysis.
Require invariant.
Require rel_correct.
Require aux_lemmas.
Require Omega.
Require Wf_nat.
Inductive Adr_CallStack : Address -> CallStack -> Prop :=
| Adr_CallStack_cons_rec :
(m:MethodName;pc:progCount;cf:Frame;SF:CallStack)
(Adr_CallStack (add m pc) SF) ->
(Adr_CallStack (add m pc) cf::SF)
| Adr_CallStack_cons_eq :
(m:MethodName;pc:progCount;L:LocalVar;S:OperandStack;SF:CallStack)
(Adr_CallStack (add m pc) <m,pc,L,S>::SF).
Lemma Adr_CallStack_inv :(m:MethodName;pc:progCount;
L:LocalVar;S:OperandStack;SF:CallStack)
(Adr_CallStack (add m pc) (frame m pc L S)::SF).
Intros; Constructor 2.
Qed.
Recursive Tactic Definition ElimVerifConstr P H L S HvF listC :=
Match listC With
[(cons ?1 ?2)] -> Cut (verifyContraint P (H,(L,S)) ?1);
[Intros Hid1|Apply HvF; Auto with datatypes];
Inversion_clear Hid1; ElimVerifConstr P H L S HvF ?2
| _ -> Idtac.
Tactic Definition InvVerifyFlow P H L S HvF :=
Unfold verifyFlow in HvF;
Cbv Beta Iota Delta [Flow] in HvF;
Match Context With
[id:(c:?)(In c ?1)->?|-?] -> ElimVerifConstr P H L S HvF ?1;
Clear HvF.
Tactic Definition Apply_R_LocalVar_monotonicity :=
Match Context With
[id:(order ? ?2 ?1)|-(R_LocalVar ? ? ? ?1)] ->
Apply R_LocalVar_monotonicity with ?2; [Idtac|Exact id].
Tactic Definition Apply_R_Stack_monotonicity :=
Match Context With
[id:(order ? ?2 ?1)|-(R_Stack ? ? ? ?1)] ->
Apply R_Stack_monotonicity with ?2; [Idtac|Exact id].
Theorem SubjectReduction_nop :
(P:Program;s2:State;h:Heap;m:MethodName;pc:progCount;
S:OperandStack;L:LocalVar;sf:CallStack;
St:(AbState P))
(SmallStepSem P (config h <m,pc,L,S>::sf) s2) ->
(instructionAt P m pc)=(Some nop) ->
(verifyFlow P m pc nop St) ->
(R_State P (config h <m,pc,L,S>::sf) St) ->
(R_State P s2 St).
Intros P (h2,sf2) h m pc s l sf (H,(L,S)) Hsem.
Inversion_clear Hsem; Try (Rewrite H1; Intros H'; Discriminate H'); Intros H'; Clear H'.
Intros HvF; InvVerifyFlow P H L S HvF.
Intros (Hheap,Hsf).
Inversion_clear Hsf.
Split.
Exact Hheap.
Constructor.
Apply_R_LocalVar_monotonicity; Auto.
Apply_R_Stack_monotonicity ; Auto.
EApply R_PopCallStack_monotonicity2 ; EAuto.
Qed.
Theorem SubjectReduction_pop :
(P:Program;s2:State;h:Heap;m:MethodName;pc:progCount;
S:OperandStack;L:LocalVar;sf:CallStack;
St:(AbState P))
(SmallStepSem P (config h <m,pc,L,S>::sf) s2) ->
(instructionAt P m pc)=(Some pop) ->
(verifyFlow P m pc pop St) ->
(R_State P (config h <m,pc,L,S>::sf) St) ->
(R_State P s2 St).
Intros P (h2,sf2) h m pc s l sf (H,(L,S)) Hsem.
Inversion_clear Hsem; Try (Rewrite H1; Intros H'; Discriminate H'); Intros H'; Clear H'.
Intros HvF; InvVerifyFlow P H L S HvF.
Intros (Hheap,Hsf).
Inversion_clear Hsf.
Split.
Exact Hheap.
Constructor.
Apply_R_LocalVar_monotonicity ; Auto.
Apply_R_Stack_monotonicity ; Auto.
EApply R_Stack_AbPop ; EAuto.
EApply R_PopCallStack_monotonicity2 ; EAuto.
Inversion H5.
Constructor.
Trivial.
Subst.
EApply R_PopCallStack_2 ; EAuto.
Qed.
Theorem SubjectReduction_push :
(P:Program;s2:State;h:Heap;m:MethodName;pc:progCount;
S:OperandStack;L:LocalVar;sf:CallStack;
St:(AbState P); c:integer)
(SmallStepSem P (config h <m,pc,L,S>::sf) s2) ->
(instructionAt P m pc)=(Some (push c)) ->
(verifyFlow P m pc (push c) St) ->
(R_State P (config h <m,pc,L,S>::sf) St) ->
(R_State P s2 St).
Intros P (h2,sf2) h m pc s l sf (H,(L,S)) c Hsem.
Inversion_clear Hsem; Try (Rewrite H1; Intros H'; Discriminate H'); Intros H'.
Rewrite H1 in H' ; Injection H' ; Intros; Injection H' ; Intros ; Subst.
Clear H4.
InvVerifyFlow P H L S H2.
Inversion_clear H3 ; Subst.
Split.
Assumption.
Constructor.
Apply_R_LocalVar_monotonicity ; Auto.
Inversion_clear H2 ; Auto.
Inversion_clear H2.
Apply_R_Stack_monotonicity ; EAuto.
Unfold R_Stack betaStack.
Replace (some (AbVal P) (PolyList.map (betaVal P h2) (num c)::s))
with (AbPush (betaVal P h2 (num c))
(some (AbVal P) (PolyList.map (betaVal P h2) s))).
Apply (AbPush_monotone (LatAbVal P)).
Unfold betaVal; Auto.
Generalize H6; Unfold R_Stack betaStack; Auto.
Simpl; Auto.
EApply R_PopCallStack_monotonicity2 ; EAuto.
Inversion H2.
Subst.
Inversion H14.
Subst.
Constructor.
EApply R_PopCallStack_2 ; EAuto.
Qed.
Theorem SubjectReduction_dup :
(P:Program;s2:State;h:Heap;m:MethodName;pc:progCount;
S:OperandStack;L:LocalVar;sf:CallStack;
St:(AbState P))
(SmallStepSem P (config h <m,pc,L,S>::sf) s2) ->
(instructionAt P m pc)=(Some dup) ->
(verifyFlow P m pc dup St) ->
(R_State P (config h <m,pc,L,S>::sf) St) ->
(R_State P s2 St).
Intros P (h2,sf2) h m pc s l sf (H,(L,S)) Hsem.
Inversion_clear Hsem; Try (Rewrite H1; Intros H'; Discriminate H'); Intros H'.
Clear H'.
Intros.
InvVerifyFlow P H L S H0.
Inversion_clear H2 ; Subst.
Split.
Assumption.
Constructor.
Inversion_clear H3 ; Subst.
Apply R_LocalVar_monotonicity with (L (add m pc)) ; Auto.
Unfold R_Stack.
Apply order_trans with (AbPush (AbTop (LatAbVal P) (S (add m pc))) (S (add m pc))) ;
Auto.
Inversion H3 ; Subst.
CaseEq '(S (add m pc)) ; Intros.
Rewrite H2 in H13 ; Inversion H13.
Simpl ; Apply order_top.
CaseEq l0 ; Intros.
Subst.
Rewrite H2 in H13 ; Inversion H13.
Subst.
CaseEq a ; Simpl ; Intros ; Subst.
Rewrite H2 in H13 ; Inversion_clear H13 ;Subst.
Inversion H6 ; Subst.
Generalize H10 ; Clear H10.
CaseEq v ; Intros ; Subst ; Try Inversion H6.
Unfold betaStack ; Simpl ; Do 2 Constructor ; Auto.
Unfold betaStack ; Simpl; Do 2 Constructor ; Simpl ; Auto.
Constructor.
Rewrite H2 in H13 ; Inversion_clear H13 ; Auto.
Rewrite H2 in H13 ; Inversion_clear H13 ; Auto.
Unfold betaStack ; Simpl; Constructor ; Simpl ; Auto.
Constructor ; Auto.
EApply R_PopCallStack_monotonicity2 ; EAuto.
Inversion H3 ;Subst ; Auto.
Inversion H14 ;Subst.
Constructor.
EApply R_PopCallStack_2 ; EAuto.
Qed.
Theorem SubjectReduction_goto :
(P:Program;s2:State;h:Heap;m:MethodName;pc:progCount;
S:OperandStack;L:LocalVar;sf:CallStack;
St:(AbState P) ; pc' : progCount)
(SmallStepSem P (config h <m,pc,L,S>::sf) s2) ->
(instructionAt P m pc)=(Some (goto pc')) ->
(verifyFlow P m pc (goto pc') St) ->
(R_State P (config h <m,pc,L,S>::sf) St) ->
(R_State P s2 St).
Intros P (h2,sf2) h m pc s l sf (H,(L,S)) pc' Hsem.
Inversion_clear Hsem; Try (Rewrite H1; Intros H'; Discriminate H'); Intros H'.
Rewrite H1 in H' ; Injection H' ; Intros ; Subst ; Clear H'.
Intros.
InvVerifyFlow P H L S H2.
Inversion_clear H3 ; Subst.
Split.
Assumption.
Constructor.
Inversion_clear H2 ; Subst.
Apply R_LocalVar_monotonicity with (L (add m pc)) ; Auto.
Unfold R_Stack.
Inversion_clear H2 ; Subst.
Unfold R_Stack in H6.
Apply R_Stack_monotonicity with (S (add m pc)) ; Auto.
EApply R_PopCallStack_monotonicity2 ; EAuto.
Inversion_clear H2 ; Subst ; Auto.
Qed.
Theorem SubjectReduction_swap :
(P:Program;s2:State;h:Heap;m:MethodName;pc:progCount;
S:OperandStack;L:LocalVar;sf:CallStack;
St:(AbState P))
(SmallStepSem P (config h <m,pc,L,S>::sf) s2) ->
(instructionAt P m pc)=(Some swap) ->
(verifyFlow P m pc swap St) ->
(R_State P (config h <m,pc,L,S>::sf) St) ->
(R_State P s2 St).
Intros P (h2,sf2) h m pc s l sf (H,(L,S)) Hsem.
Inversion_clear Hsem; Try (Rewrite H1; Intros H'; Discriminate H'); Intros H'.
Clear H'.
Intros.
InvVerifyFlow P H L S H0.
Inversion_clear H2 ; Subst.
Split.
Assumption.
Constructor.
Inversion_clear H3 ; Subst.
Apply R_LocalVar_monotonicity with (L (add m pc)) ; Auto.
Unfold R_Stack.
Apply order_trans with (AbPush (AbTop (LatAbVal P) (AbPop (S (add m pc))))
(AbPush (AbTop (LatAbVal P) (S (add m pc)))
(AbPop (AbPop (S (add m pc)))))) ; Auto.
Inversion_clear H3 ; Subst.
Unfold R_Stack in H6.
CaseEq '(S (add m pc)) ; Intros.
Rewrite H3 in H6; Inversion H6.
Simpl ; Apply order_top.
CaseEq l0 ; Intros.
Subst.
Rewrite H3 in H6 ; Inversion H6.
Subst.
CaseEq l1 ; Intros ; Subst.
Rewrite H3 in H6 ; Inversion_clear H6.
Inversion_clear H9.
Simpl.
Rewrite H3 in H6 ; Inversion_clear H6.
Inversion_clear H9.
CaseEq a0 ; Intros ; Subst.
CaseEq v2 ; Intros ; Subst ; Try Inversion H6.
Unfold betaStack ; Simpl ; Constructor ; Auto.
CaseEq a; Intros ; Subst.
CaseEq v1 ; Intros ; Subst ; Try Inversion H8.
Unfold betaStack ; Simpl ; Constructor ; Auto.
Constructor.
Constructor.
Assumption.
Constructor ; Auto.
Unfold betaStack.
Simpl.
Constructor ; Auto.
Constructor ; Auto.
Unfold betaStack.
Simpl.
Constructor ; Auto.
Constructor ; Auto.
EApply R_PopCallStack_monotonicity2 ; EAuto.
Inversion H3 ;Subst ; Auto.
Inversion H14 ;Subst.
Constructor.
EApply R_PopCallStack_2 ; EAuto.
Qed.
Theorem SubjectReduction_dup2 :
(P:Program;s2:State;h:Heap;m:MethodName;pc:progCount;
S:OperandStack;L:LocalVar;sf:CallStack;
St:(AbState P))
(SmallStepSem P (config h <m,pc,L,S>::sf) s2) ->
(instructionAt P m pc)=(Some dup2) ->
(verifyFlow P m pc dup2 St) ->
(R_State P (config h <m,pc,L,S>::sf) St) ->
(R_State P s2 St).
Intros P (h2,sf2) h m pc s l sf (H,(L,S)) Hsem.
Inversion_clear Hsem; Try (Rewrite H1; Intros H'; Discriminate H'); Intros H'.
Clear H'.
Intros.
InvVerifyFlow P H L S H0.
Inversion_clear H2 ; Subst.
Split.
Assumption.
Constructor.
Inversion_clear H3 ; Subst.
Apply R_LocalVar_monotonicity with (L (add m pc)) ; Auto.
Unfold R_Stack.
Apply order_trans with (AbPush (AbTop (LatAbVal P) (S (add m pc)))
(AbPush (AbTop (LatAbVal P) (AbPop (S (add m pc))))
(S (add m pc)))) ; Auto.
Inversion_clear H3 ; Subst.
Unfold R_Stack in H6.
CaseEq '(S (add m pc)) ; Intros.
Rewrite H3 in H6; Inversion H6.
Simpl ; Apply order_top.
CaseEq l0 ; Intros.
Subst.
Rewrite H3 in H6 ; Inversion H6.
Subst.
CaseEq l1 ; Intros ; Subst.
Rewrite H3 in H6 ; Inversion_clear H6.
Inversion_clear H9.
Simpl.
Rewrite H3 in H6 ; Inversion_clear H6.
Inversion_clear H9.
CaseEq a0 ; Intros ; Subst.
CaseEq v2 ; Intros ; Subst ; Try Inversion H6.
Unfold betaStack ; Simpl ; Constructor ; Auto.
CaseEq a; Intros ; Subst.
CaseEq v1 ; Intros ; Subst ; Try Inversion H8.
Unfold betaStack ; Simpl ; Constructor ; Auto.
Constructor.
Constructor.
Constructor ; Auto.
Constructor ; Auto.
Constructor ; Auto.
Constructor ; Auto.
Constructor ; Auto.
Constructor ; Auto.
Constructor ; Auto.
Unfold betaStack.
Simpl.
Constructor ; Auto.
Constructor ; Auto.
Constructor ; Auto.
Constructor ; Auto.
Unfold betaStack.
Simpl.
Constructor ; Auto.
Constructor ; Auto.
Constructor ; Auto.
Constructor ; Auto.
EApply R_PopCallStack_monotonicity2 ; EAuto.
Inversion H3 ;Subst ; Auto.
Inversion H14 ;Subst.
Constructor.
EApply R_PopCallStack_2 ; EAuto.
Qed.
Theorem SubjectReduction_numop:
(P:Program;s2:State;h:Heap;m:MethodName;pc:progCount;
S:OperandStack;L:LocalVar;sf:CallStack;
St:(AbState P) ; op: Operator)
(SmallStepSem P (config h <m,pc,L,S>::sf) s2) ->
(instructionAt P m pc)=(Some (numop op)) ->
(verifyFlow P m pc (numop op) St) ->
(R_State P (config h <m,pc,L,S>::sf) St) ->
(R_State P s2 St).
Intros P (h2,sf2) h m pc s l sf (H,(L,S)) op Hsem.
Inversion_clear Hsem;
Try (Rewrite H1; Intros H'; Discriminate H').
Intros H'.
Rewrite H1 in H' ; Injection H'.
Intros H'' ; Subst.
Intros HvF ; InvVerifyFlow P H L S HvF.
Intros (Hheap,Hsf).
Inversion_clear Hsf.
Split.
Exact Hheap.
Constructor.
Apply_R_LocalVar_monotonicity ; Auto.
Apply_R_Stack_monotonicity ; Auto.
EApply R_Stack_AbBinop ; EAuto.
EApply R_PopCallStack_monotonicity2 ; EAuto.
Inversion H5 ; Try Constructor ; Auto.
EApply R_PopCallStack_2 ; EAuto.
Qed.
Theorem SubjectReduction_load:
(P:Program;s2:State;h:Heap;m:MethodName;pc:progCount;
S:OperandStack;L:LocalVar;sf:CallStack;
St:(AbState P); i : Var)
(SmallStepSem P (config h <m,pc,L,S>::sf) s2) ->
(instructionAt P m pc)=(Some (load i)) ->
(verifyFlow P m pc (load i) St) ->
(R_State P (config h <m,pc,L,S>::sf) St) ->
(R_State P s2 St).
Intros P (h2,sf2) h m pc s l sf (H,(L,S)) i Hsem.
Inversion_clear Hsem;
Try (Rewrite H1; Intros H'; Discriminate H').
Intros H'.
Rewrite H1 in H' ; Injection H'.
Intros H'' ; Subst.
Clear H'.
Intros HvF ; InvVerifyFlow P H L S HvF.
Intros (Hheap,Hsf).
Inversion_clear Hsf.
Split.
Exact Hheap.
Constructor.
Apply_R_LocalVar_monotonicity ; Auto.
Apply_R_Stack_monotonicity ; Auto.
Apply (R_Stack_AbPush P) ; Auto.
EApply R_PopCallStack_monotonicity2 ; EAuto.
Inversion H5 ; Try Constructor ; Auto.
Subst.
EApply R_PopCallStack_2 ; EAuto.
Qed.
Theorem SubjectReduction_store:
(P:Program;s2:State;h:Heap;m:MethodName;pc:progCount;
S:OperandStack;L:LocalVar;sf:CallStack;
St:(AbState P); i : Var)
(SmallStepSem P (config h <m,pc,L,S>::sf) s2) ->
(instructionAt P m pc)=(Some (store i)) ->
(verifyFlow P m pc (store i) St) ->
(R_State P (config h <m,pc,L,S>::sf) St) ->
(R_State P s2 St).
Intros P (h2,sf2) h m pc s l sf (H,(L,S)) i Hsem.
Inversion_clear Hsem;
Try (Rewrite H1; Intros H'; Discriminate H').
Intros H'.
Rewrite H1 in H' ; Injection H'.
Intros H'' ; Subst.
Intros HvF ; InvVerifyFlow P H L S HvF.
Intros (Hheap,Hsf).
Inversion_clear Hsf;
(Split; [Try Exact Hheap
|Constructor; [Idtac
|Idtac
|Try Assumption]]).
Apply_R_LocalVar_monotonicity ; Auto.
Unfold R_LocalVar ; Intros.
Case (positive_dec i x) ; Intros.
Subst.
Rewrite apply_subst1 ; Auto.
Unfold substLocalVar.
Case positive_dec ; Intros.
EApply (R_Stack_AbTop P) ; EAuto.
Elim n ; Trivial.
Elim (instructionAt_some ? ? ? ? H1); Intros M (H6,(H7,(H8,H9))).
Apply valid_store with M; Auto.
Rewrite apply_subst2 ; Auto.
Unfold substLocalVar.
Case positive_dec ; Intros.
Elim n ; Auto.
Apply H0 ; Trivial.
Elim (instructionAt_some ? ? ? ? H1); Intros M (H6,(H7,(H8,H9))).
EApply valid_store_instructionAt ; EAuto.
Apply_R_Stack_monotonicity ; Auto.
EApply (R_Stack_AbPop P) ; EAuto.
Inversion H5 ; Try Constructor ; Auto.
Subst.
EApply R_PopCallStack_2 ; EAuto.
Qed.
Theorem SubjectReduction_if:
(P:Program;s2:State;h:Heap;m:MethodName;pc:progCount;
S:OperandStack;L:LocalVar;sf:CallStack;
St:(AbState P); pc': progCount)
(SmallStepSem P (config h <m,pc,L,S>::sf) s2) ->
(instructionAt P m pc)=(Some (If pc')) ->
(verifyFlow P m pc (If pc') St) ->
(R_State P (config h <m,pc,L,S>::sf) St) ->
(R_State P s2 St).
Intros P (h2,sf2) h m pc s l sf (H,(L,S)) pc' Hsem.
Inversion_clear Hsem;
Try (Rewrite H1; Intros H'; Discriminate H').
Intros H'.
Rewrite H1 in H' ; Injection H'.
Intros H'' ; Subst.
Intros HvF ; InvVerifyFlow P H L S HvF.
Intros (Hheap,Hsf).
Inversion_clear Hsf;
(Split; [Try Exact Hheap
|Constructor; [Idtac
|Idtac
|Try Assumption]]).
Apply_R_LocalVar_monotonicity.
Apply R_LocalVar_monotonicity with (L (add m pc)); Auto.
Generalize
[H](lift_right_unop_keep_monotone ? ? (LatAbRef P) LatAbNum ? (LatAbLocalVar P)
(AbIf_NZ (LatAbLocalVar P) (L (add m pc))) (AbIf_NZ (LatAbLocalVar P) (L (add m pc)))
H (some_sum ? (inr ? ? (betaNum n)))(AbTop (LatAbVal P) (S (add m pc))) ).
Unfold 1 lift_right_unop.
Rewrite AbIf_NZ_prop; Auto.
Intros.
Apply H9; Auto.
Intros; Apply AbIf_NZ_monotone; Auto.
Unfold R_Stack betaStack in H7.
Replace (some_sum (AbRef P)+AbNum (inr (AbRef P) AbNum (betaNum n)))
with (AbTop (LatAbVal P) (some (AbVal P) (PolyList.map (betaVal P h2) (num n)::S0))).
Apply AbTop_monotone; Auto.
Auto.
Apply_R_Stack_monotonicity.
Apply R_Stack_monotonicity with (AbPop (S (add m pc))); Auto.
Unfold R_Stack; Unfold R_Stack betaStack in H7.
Replace (betaStack P h2 S0) with
(AbPop (some (AbVal P) (PolyList.map (betaVal P h2) (num n)::S0))).
Apply (AbPop_monotone (LatAbVal P)); Auto.
Auto.
Generalize
[H](lift_right_unop_keep_monotone ? ? (LatAbRef P) LatAbNum ? (LatAbStack P)
(AbIf_NZ (LatAbStack P) (AbPop (S (add m pc)))) (AbIf_NZ (LatAbStack P) (AbPop (S (add m pc))))
H (some_sum ? (inr ? ? (betaNum n)))(AbTop (LatAbVal P) (S (add m pc))) ).
Unfold 1 lift_right_unop.
Rewrite AbIf_NZ_prop; Auto.
Intros.
Apply H9; Auto.
Intros; Apply AbIf_NZ_monotone; Auto.
Unfold R_Stack betaStack in H7.
Replace (some_sum (AbRef P)+AbNum (inr (AbRef P) AbNum (betaNum n)))
with (AbTop (LatAbVal P) (some (AbVal P) (PolyList.map (betaVal P h2) (num n)::S0))).
Apply AbTop_monotone; Auto.
Auto.
Inversion_clear H8; Try Constructor.
EApply R_PopCallStack_2; EAuto.
Intros H'.
Rewrite H1 in H' ; Injection H'.
Intros H'' ; Subst.
Clear H'.
Intros HvF ; InvVerifyFlow P H L S HvF.
Intros (Hheap,Hsf).
Inversion_clear Hsf;
(Split; [Try Exact Hheap
|Constructor; [Idtac
|Idtac
|Try Assumption]]).
Apply_R_LocalVar_monotonicity.
Apply R_LocalVar_monotonicity with (L (add m pc)); Auto.
Generalize
[H](lift_right_unop_keep_monotone ? ? (LatAbRef P) LatAbNum ? (LatAbLocalVar P)
(AbIf_Z (LatAbLocalVar P) (L (add m pc))) (AbIf_Z (LatAbLocalVar P) (L (add m pc)))
H (some_sum ? (inr ? ? (betaNum (0))))(AbTop (LatAbVal P) (S (add m pc))) ).
Unfold 1 lift_right_unop.
Rewrite AbIf_Z_prop; Auto.
Intros.
Apply H8; Auto.
Intros; Apply AbIf_Z_monotone; Auto.
Unfold R_Stack betaStack in H6.
Replace (some_sum (AbRef P)+AbNum (inr (AbRef P) AbNum (betaNum (0))))
with (AbTop (LatAbVal P) (some (AbVal P) (PolyList.map (betaVal P h2) (num (0))::S0))).
Apply AbTop_monotone; Auto.
Auto.
Unfold R_Num; Auto.
Apply_R_Stack_monotonicity.
Apply R_Stack_monotonicity with (AbPop (S (add m pc))); Auto.
Unfold R_Stack; Unfold R_Stack betaStack in H7.
Replace (betaStack P h2 S0) with
(AbPop (some (AbVal P) (PolyList.map (betaVal P h2) (num (0))::S0))).
Apply (AbPop_monotone (LatAbVal P)); Auto.
Auto.
Generalize
[H](lift_right_unop_keep_monotone ? ? (LatAbRef P) LatAbNum ? (LatAbStack P)
(AbIf_Z (LatAbStack P) (AbPop (S (add m pc)))) (AbIf_Z (LatAbStack P) (AbPop (S (add m pc))))
H (some_sum ? (inr ? ? (betaNum (0))))(AbTop (LatAbVal P) (S (add m pc))) ).
Unfold 1 lift_right_unop.
Rewrite AbIf_Z_prop; Auto.
Intros.
Apply H8; Auto.
Intros; Apply AbIf_Z_monotone; Auto.
Unfold R_Stack betaStack in H6.
Replace (some_sum (AbRef P)+AbNum (inr (AbRef P) AbNum (betaNum (0))))
with (AbTop (LatAbVal P) (some (AbVal P) (PolyList.map (betaVal P h2) (num (0))::S0))).
Apply AbTop_monotone; Auto.
Auto.
Unfold R_Num; Auto.
Inversion_clear H7; Try Constructor.
EApply R_PopCallStack_2; EAuto.
Qed.
Theorem SubjectReduction_putfield:
(P:Program;s2:State;h:Heap;m:MethodName;pc:progCount;
S:OperandStack;L:LocalVar;sf:CallStack;
St:(AbState P); f : FieldName)
(SmallStepSem P (config h <m,pc,L,S>::sf) s2) ->
(instructionAt P m pc)=(Some (putfield f)) ->
(verifyFlow P m pc (putfield f) St) ->
(R_State P (config h <m,pc,L,S>::sf) St) ->
(R_State P s2 St).
Intros P (h2,sf2) h m pc s l sf (H,(L,S)) f Hsem.
Inversion_clear Hsem;
Try (Rewrite H1; Intros H'; Discriminate H').
Intros H'.
Rewrite H1 in H' ; Injection H'.
Intros H'' ; Subst.
Opaque LatAbObject.
Intros HvF ; InvVerifyFlow P H L S HvF.
Intros (Hheap,Hsf).
Inversion_clear Hsf;
(Split; [Try Exact Hheap
|Constructor; [Idtac
|Idtac
|Try Assumption]]).
Clear H'.
Unfold R_Heap ; Intros.
CaseEq '(substHeap h loc (substField o f v) loc0) ; Intros ; Trivial.
Unfold R_Object R_Val; Intros.
Case (Location_dec loc loc0) ; Intros.
Subst.
Case (Field_dec f f0) ; Intros.
Inversion H7.
Rewrite <- H12 in H6.
Simpl in H6.
Apply order_trans with
(apply (LatAbVal P) (apply (LatAbObject P) (Lattice.top (LatAbHeap P)) (class c)) f0).
Case (inf_log_dec (class c) (max_log_ClassName P)) ; Intros ; Trivial.
Rewrite (apply_on_top (AbObject P) (LatAbObject P) (max_log_ClassName P)) ; Auto.
Rewrite (apply_on_top (AbVal P) (LatAbVal P) (max_log_Field P)) ; Auto.
Subst.
Apply (valid_putfield_instructionAt ? ? ? ? H1); Intuition.
Cut (fieldValue c f0) = null.
Intros.
Rewrite H11.
Clear H11.
Unfold betaVal.
Apply bottom_is_a_bottom.
Cut (class o) = (class c).
Intros.
Elim n; Apply valid_ClassName.
Elim H3; Intros; Rewrite <- H11.
Exists x0; Intuition.
Generalize H9 ; Unfold substHeap.
Case Location_dec; Intros.
Injection H11 ; Clear H11 ; Intros.
Rewrite <-H11 ; Trivial.
Elim n0 ; Auto.
Apply apply_monotone.
Apply apply_monotone.
Auto.
Rewrite <- H12 in H6.
CaseEq l2; Intros; Rewrite H15 in H6.
Apply order_trans with (apply (LatAbVal P) (apply (LatAbObject P) (Lattice.top (LatAbHeap P)) (class c)) f0).
Case (inf_log_dec (class c) (max_log_ClassName P)) ; Intros ; Trivial.
Rewrite (apply_on_top (AbObject P) (LatAbObject P) (max_log_ClassName P)) ; Auto.
Rewrite (apply_on_top (AbVal P) (LatAbVal P) (max_log_Field P)) ; Auto.
Subst.
Apply (valid_putfield_instructionAt ? ? ? ? H1); Intuition.
Cut (fieldValue c f0) = null.
Intros.
Rewrite H16.
Clear H16.
Unfold betaVal.
Apply bottom_is_a_bottom.
Cut (class o) = (class c).
Intros.
Elim n; Apply valid_ClassName.
Elim H3; Intros; Rewrite <- H16.
Exists x; Intuition.
Generalize H9 ; Unfold substHeap.
Case Location_dec; Intros.
Injection H16 ; Clear H16 ; Intros.
Rewrite <-H16 ; Trivial.
Elim n0 ; Auto.
Apply apply_monotone.
Apply apply_monotone.
Auto.
Rewrite H15 in H14.
Inversion_clear H14.
Inversion H16.
Rewrite <- H18 in H6; Simpl in H6.
Apply order_trans with
(apply (LatAbVal P) (apply (LatAbObject P) (Lattice.top (LatAbHeap P)) (class c)) f0).
Case (inf_log_dec (class c) (max_log_ClassName P)) ; Intros ; Trivial.
Rewrite (apply_on_top (AbObject P) (LatAbObject P) (max_log_ClassName P)) ; Auto.
Rewrite (apply_on_top (AbVal P) (LatAbVal P) (max_log_Field P)) ; Auto.
Subst.
Apply (valid_putfield_instructionAt ? ? ? ? H1); Intuition.
Cut (fieldValue c f0) = null.
Intros.
Rewrite H19.
Clear H19.
Unfold betaVal.
Apply bottom_is_a_bottom.
Cut (class o) = (class c).
Intros.
Elim n; Apply valid_ClassName.
Elim H3; Intros; Rewrite <- H19.
Exists x0; Intuition.
Generalize H9 ; Unfold substHeap.
Case Location_dec; Intros.
Injection H19 ; Clear H19 ; Intros.
Rewrite <-H19 ; Trivial.
Elim n0 ; Auto.
Apply apply_monotone.
Apply apply_monotone.
Auto.
Rewrite <- H19 in H6.
Cbv Beta Iota Delta [AbTop AbPop] in H6.
Unfold lift_left_unop in H6.
Apply order_trans with (apply (LatAbVal P) (apply (LatAbObject P) (map (LatAbObject P)
[_:ClassName]
(subst (LatAbVal P) (bottom (LatAbObject P)) f x2) a2) (class c)) f0).
Rewrite map_in_finite ; Auto.
Subst.
Rewrite apply_subst1 ; Auto.
Unfold substHeap in H9.
Generalize H9; Clear H9;
Case Location_dec; Intros.
Injection H9; Clear H9; Intros.
Rewrite <- H9.
Rewrite <-substfield_equal.
Rewrite <-betaVal_subst ; Trivial.
Elim n ; Auto.
Subst.
Apply (valid_putfield_instructionAt ? ? ? ? H1); Intuition.
Subst.
Cut (class c) = (class o) ; Intros.
Rewrite H10.
Generalize H18 ; Clear H18 ; Unfold betaRef ; Rewrite H2 ; Intros H18.
Apply singleton_in_finite.
Apply valid_ClassName.
Elim H3 ; Intros ; Intuition.
Exists x ; Intros.
Intuition.
Exact H18.
Generalize H9 ; Unfold substHeap ; Case Location_dec ; Intros ; Try (Elim n ; Auto).
Injection H10 ; Intros H' ; Rewrite <-H' ; Auto.
Subst.
Apply apply_monotone.
Apply apply_monotone.
Exact H6.
Unfold R_Heap R_Object R_Val in Hheap.
Generalize (Hheap loc0) ; Rewrite H2 ; Intros H11.
Generalize (H11 f0) ; Intros ; Clear H11.
Cut (betaVal P h (fieldValue o f0)) =
(betaVal P (substHeap h loc0 (substField o f v)) (fieldValue c f0)) ; Intros.
Rewrite <-H11 ; Auto.
Cut (class c) = (class o) ; Intros. Rewrite H12; Auto.
Generalize H9 ; Unfold substHeap ; Case Location_dec ; Intros ; Try (Elim n0; Auto).
Injection H12 ; Intros H' ; Rewrite <-H' ; Auto.
Generalize H9 ; Unfold substHeap ; Case Location_dec ; Intros ; Try (Elim n0; Auto).
Injection H11 ; Intros H' ; Rewrite <-H' ; Auto.
Simpl.
Case Field_dec ; Intros.
Elim n ; Auto.
Unfold betaVal.
CaseEq '(fieldValue o f0).
Intros ; Trivial.
Intros.
Simpl.
Unfold betaRef.
CaseEq '(h r).
Intros.
Case (Location_dec r loc0).
Intros.
Rewrite e0 in H13.
Rewrite H2 in H13 ; Injection H13 ; Intros H'' ; Rewrite H''.
Simpl ; Auto.
Intros ; Auto.
Intros.
Case (Location_dec r loc0) ; Intros.
Rewrite e0 in H13.
Rewrite H2 in H13 ; Discriminate H13.
Trivial.
Auto.
Unfold R_Heap R_Object R_Val in Hheap.
Unfold substHeap in H9 ; Generalize H9; Case Location_dec ; Intros.
Subst; Elim n ; Auto.
Generalize (Hheap loc0); Rewrite H10 ; Intros H11.
Generalize (H11 f0) ; Intros ; Clear H11.
Cut (betaVal P h (fieldValue c f0)) =
(betaVal P (substHeap h loc (substField o f v)) (fieldValue c f0)) ; Intros.
Rewrite <-H11 ; Auto.
Unfold betaVal.
CaseEq '(fieldValue c f0) ; Intros.
Trivial.
Unfold betaRef.
CaseEq '(h r).
Intros.
Unfold substHeap.
Case Location_dec ; Intros.
Subst.
Rewrite H2 in H13 ; Injection H13 ; Intros H'' ; Rewrite <- H'' ; Auto.
Rewrite H13; Trivial.
Intros.
Unfold substHeap.
Case Location_dec ; Intros.
Subst.
Rewrite H2 in H13 ; Discriminate H13.
Rewrite H13 ; Auto.
Trivial.
Apply R_LocalVar_subst ; Auto.
Apply_R_LocalVar_monotonicity ; Auto.
Apply R_Stack_subst ; Auto.
Apply R_Stack_monotonicity with (AbPop (AbPop (S (add m pc)))) ; Auto.
EApply R_Stack_AbPop ; EAuto.
EApply R_Stack_AbPop ; EAuto.
Apply R_PopCallStack_monotonicity2 with pc ; Auto.
Apply R_PopCallStack_subst ; Auto.
Inversion H8; Try Constructor ; Auto.
Subst.
EApply R_PopCallStack_2 ; EAuto.
Qed.
Theorem SubjectReduction_getfield:
(P:Program;s2:State;h:Heap;m:MethodName;pc:progCount;
S:OperandStack;L:LocalVar;sf:CallStack;
St:(AbState P); f : FieldName)
(SmallStepSem P (config h <m,pc,L,S>::sf) s2) ->
(instructionAt P m pc)=(Some (getfield f)) ->
(verifyFlow P m pc (getfield f) St) ->
(R_State P (config h <m,pc,L,S>::sf) St) ->
(R_State P s2 St).
Intros P (h2,sf2) h m pc s l sf (H,(L,S)) f Hsem.
Inversion_clear Hsem;
Try (Rewrite H1; Intros H'; Discriminate H').
Intros H'.
Rewrite H1 in H' ; Injection H'.
Intros H'' ; Subst.
Opaque LatAbObject.
Intros HvF ; InvVerifyFlow P H L S HvF.
Intros (Hheap,Hsf).
Inversion_clear Hsf;
(Split; [Try Exact Hheap
|Constructor; [Idtac
|Idtac
|Try Assumption]]).
Apply_R_LocalVar_monotonicity ; Auto.
Apply_R_Stack_monotonicity ; Auto.
EApply R_Stack_AbPush ; EAuto.
Unfold R_Val.
Inversion H6.
Simpl.
Constructor.
CaseEq x2 ; Intros.
Rewrite H13 in H11.
Clear H'.
Inversion H11.
Simpl ;
Constructor.
CaseEq s0 ; Intros.
Cbv Beta Iota Delta [AbTop lift_left_unop].
Rewrite H13 in H11 ; Rewrite H14 in H11 ; Simpl in H11.
Inversion H11.
Subst.
Unfold R_Heap R_Object R_Val in Hheap.
Generalize (Hheap loc); Rewrite H2 ; Intro Hheap' ; Generalize (Hheap' f) ; Clear
Hheap'; Intro Hheap'.
Apply order_trans with
(apply (LatAbVal P) (apply (LatAbObject P) H (class o)) f) ; Trivial.
Apply join_on_set_prop with f:= ([cl:positive](apply (LatAbVal P) (apply (LatAbObject P) H cl) f)).
Apply singleton_in_finite.
Apply valid_ClassName.
Elim H3 ; Intros x H'' ; Exists x ; Intuition.
Inversion H11.
Unfold betaRef in H13.
Generalize H13 ; Rewrite H2 ; Intros.
Exact H14.
Rewrite H13 in H11 ; Rewrite H14 in H11 ; Inversion H11.
EApply R_Stack_AbPop ; EAuto.
Apply R_PopCallStack_monotonicity2 with pc ; Auto.
Inversion H7; Try Constructor ; Auto.
Subst.
EApply R_PopCallStack_2 ; EAuto.
Qed.
Lemma AbObject_bottom : (P:Program;h:Heap;c:ClassInst)
(R_Object P h c (bottom (LatAbObject P))) ->
(f:FieldName) (fieldValue c f)=null.
Unfold R_Object; Intros.
Generalize (H f); Clear H.
Rewrite (apply_on_bottom (AbVal P) (LatAbVal P) (max_log_Field P)).
Unfold R_Val.
Case (fieldValue c f); Simpl; Intros.
Inversion H.
Inversion H.
Auto.
Qed.
Lemma R_PopCallStack_subst_def' :
(P : Program ; h: Heap ; loc : Location ;
sf : CallStack ; L : (AbFuncLocalVar P) ; S: (AbFuncStack P) ; c : Class;
m : MethodName ; pc : progCount ; l : LocalVar ; s : OperandStack)
(h loc)=(None ClassInst) ->
((f:Frame)
(In f sf)
->(let (_, _, l', s') = f
in ((x:Var; loc1:Location)
(l' x)=(ref loc1)->~(h loc1)=(None ClassInst))
/\((loc2:Location)
(In (ref loc2) s')->~(h loc2)=(None ClassInst))))
-> (R_PopCallStack P h sf (L,S)) ->
(R_PopCallStack P (substHeap h loc (def c)) sf
(L,S)).
Intros.
NewInduction H1.
Constructor.
Constructor.
Apply R_PopCallStack_2 with M' ; Auto.
Generalize H1 ; Unfold R_LocalVar ; Intros.
Generalize (H5 x) ; Intros.
CaseEq '(l0 x) ; Intros.
Rewrite H7 in H6.
Apply R_Val_subst_def_num ; Trivial.
Rewrite H7 in H6.
Apply R_Val_subst_def_ref ; Trivial.
Red ; Intros.
Generalize (H0 (frame m0 pc0 l0 s0)) ; Clear H0 ; Intros.
Simpl in H0 ;
Intuition.
EApply H0 ; EAuto.
Unfold R_Val betaVal ; Simpl ; Auto.
Constructor.
Generalize (H0 (frame m0 pc0 l0 s0)) ; Clear H0 ; Intros.
Simpl in H0 ;
Intuition.
Apply R_Stack_subst_def ; Auto.
Apply IHR_PopCallStack.
Intros.
Generalize (H0 f) ; Clear H0 ; Intros.
Simpl in H0.
Intuition.
Qed.
Lemma R_PopCallStack_subst_def : (P : Program ; h: Heap ; loc : Location ;
sf : CallStack ; L : (AbFuncLocalVar P) ; S: (AbFuncStack P) ; c : Class;
m : MethodName ; pc : progCount ; l : LocalVar ; s : OperandStack)
(h loc)=(None ClassInst) ->
((f:Frame)
(In f ((frame m pc l s))::sf)
->(let (_, _, l', s') = f
in ((x:Var; loc1:Location)
(l' x)=(ref loc1)->~(h loc1)=(None ClassInst))
/\((loc2:Location)
(In (ref loc2) s')->~(h loc2)=(None ClassInst))))->
(R_PopCallStack P h ((frame m pc l s))::sf (L,S)) ->
(R_PopCallStack P (substHeap h loc (def c))
((frame m pc l ((ref loc))::s))::sf (L,S)).
NewInduction sf.
Intros.
Constructor.
Intros.
Subst.
Inversion H1.
Subst.
EApply R_PopCallStack_2 ; EAuto.
Generalize H6 ; Clear H6 ; Unfold R_LocalVar; Intros.
Generalize (H6 x) ; Clear H6 ;Intros.
CaseEq '(l0 x) ; Intros.
Rewrite H3 in H2.
Apply R_Val_subst_def_num ; Auto.
Rewrite H3 in H2.
Apply R_Val_subst_def_ref ; Auto.
Generalize (H0 a) ; Intros H0'; Simpl in H0' ; Intuition.
Rewrite <- H7 in H6 ; Simpl in H6.
Elim H6 ; Intros.
EApply H8 ; EAuto.
Unfold R_Val betaVal ; Simpl ; Auto.
Constructor.
Apply R_Stack_subst_def ; Auto.
Generalize (H0 a) ; Intros H0'; Simpl in H0' ; Intuition.
Rewrite <- H7 in H3 ; Simpl in H3.
Elim H3 ; Intros.
EApply H10 ; EAuto.
EApply R_PopCallStack_subst_def' ; Auto.
Intros.
Generalize (H0 f) ; Clear H0 ; Intros H0 ; Simpl in H0 ;
Intuition.
Subst.
Simpl in H2 ; Elim H2 ; Intros.
Rewrite H7 in H4.
Apply (H0 H4) ; Auto.
Apply (H5 H4) ; Auto.
Qed.
Lemma SubjectReduction_new_valid:
(P:Program;s2:State;h:Heap;m:MethodName;pc:progCount;
S:OperandStack;L:LocalVar;sf:CallStack;
St:(AbState P); cl : ClassName)
(SmallStepSem P (config h <m,pc,L,S>::sf) s2) ->
(instructionAt P m pc)=(Some (new cl)) ->
(valid_State (config h <m,pc,L,S>::sf)) ->
(verifyFlow P m pc (new cl) St) ->
(R_State P (config h <m,pc,L,S>::sf) St) ->
(R_State P s2 St).
Intros P (h2,sf2) h m pc s l sf (H,(L,S)) f Hsem.
Inversion_clear Hsem;
Try (Rewrite H1; Intros H'; Discriminate H').
Intros H' Hvalid.
Rewrite H1 in H' ; Injection H'.
Intros H'' ; Subst.
Opaque LatAbObject.
Intros HvF ; InvVerifyFlow P H L S HvF.
Intros (Hheap,Hsf).
Unfold valid_State in Hvalid.
Elim Hvalid; Clear Hvalid; Intros HvalidH Hvalid.
Cut (In (frame m pc l s) (frame m pc l s)::sf); [Intros Inf|Simpl; Left; Auto].
Generalize (Hvalid (frame m pc l s) Inf); Clear Inf; Intros (HvalidL,HvalidS).
Inversion_clear Hsf;
(Split; [Try Exact Hheap
|Constructor; [Idtac
|Idtac
|Try Assumption]]).
Clear H'.
Elim H2 ; Intros x H'.
Generalize (newObject_specif P x h h2 loc); Intro newObject_specif.
Elim newObject_specif ; Intros.
Unfold R_Heap.
Unfold R_Heap in Hheap.
Intros.
Case (Location_dec loc loc0) ; Intros.
Subst.
CaseEq '(substHeap h loc0 (def x) loc0) ; Intros ; Trivial.
Generalize H10; Unfold 1 substHeap; Case Location_dec ; Intros.
Injection H11 ; Intros H'' ; Rewrite H''.
Generalize (AbDef_correct P (substHeap h loc0 c) x f H'); Intros.
Rewrite H'' in H12.
Apply R_Object_monotonicity with (AbDef P f); Auto.
Elim (searchClass_some ? ? ? H'); Intros.
Cut (nameClass x)=(class c); Intros.
Rewrite <- H15; Rewrite <- H14.
Replace (AbDef P f) with (apply (LatAbObject P) (subst (LatAbObject P)
(Fbottom (AbObject P) (LatAbObject P) (max_log_ClassName P))
f (AbDef P f)) f).
Apply apply_monotone.
Exact H7.
Rewrite apply_subst1; Auto.
Rewrite H14; Rewrite H15.
Apply valid_ClassName.
Elim H2 ; Intros.
Elim (searchClass_some ? ? ? H16); Intros.
Exists x0 ; Intuition.
Rewrite H14 in H18.
Rewrite H15 in H18; Auto.
Rewrite <- H''.
Unfold def; Simpl; Reflexivity.
Elim n ; Auto.
CaseEq '(h2 loc0) ;Intros ; Trivial.
Rewrite H10 in H11 ; Generalize H11 ; Unfold substHeap ; Case Location_dec ; Intros ; Subst.
Elim n ; Auto.
Generalize (Hheap loc0) ; Rewrite H12.
Elim (searchClass_some ? ? ? H'); Do 2 Intro.
Unfold R_Object; Intros.
Generalize (H14 f0); Clear H14.
CaseEq '(fieldValue c f0); Intros.
Apply R_Val_subst_def_num; Auto.
Apply R_Val_subst_def_ref; Auto.
Apply (HvalidH ? ? ? ? H12 H14).
Auto.
Elim (searchClass_some ? ? ? H'); Auto.
Elim (searchClass_some ? ? ? H'); Intros.
Subst; Auto.
Apply_R_LocalVar_monotonicity; Auto.
Elim H2; Clear H2; Intros c H2.
Elim (searchClass_some ? ? ? H2); Do 2 Intro.
Generalize (newObject_specif P c h h2 loc); Intro newObject_specif.
Elim (newObject_specif H9) ; Intros.
Rewrite H12.
Unfold R_LocalVar; Intros.
CaseEq '(l x) ; Intros.
Apply R_Val_subst_def_num; Auto.
Unfold R_LocalVar in H0 ; Rewrite <- H13 ; Apply (H0 x); Auto.
Apply R_Val_subst_def_ref; Auto.
Unfold R_LocalVar in H0 ; Rewrite <- H13 ; Apply (H0 x); Auto.
Apply (HvalidL x r) ; Trivial.
Unfold R_Val betaVal.
Apply bottom_is_a_bottom.
Rewrite <- H10 ; Assumption.
Apply_R_Stack_monotonicity; Auto.
Elim H2; Clear H2; Intros c H2.
Elim (searchClass_some ? ? ? H2); Do 2 Intro.
Generalize (newObject_specif P c h h2 loc); Intro newObject_specif.
Elim (newObject_specif H9) ; Intros.
Rewrite H12.
Apply (R_Stack_AbPush P (substHeap h loc (def c)) (ref loc) s
(some_sum (FiniteSet (max_log_ClassName P))+AbNum
(inl (FiniteSet (max_log_ClassName P)) AbNum (singleton f)))
(S (add m pc)) ).
Unfold R_Val betaVal.
Unfold betaRef.
Rewrite substHeap_equal.
Opaque bottom.
Simpl; Apply sum_order_left.
Rewrite <-H10 ; Auto.
Apply R_Stack_subst_def ; Auto.
Rewrite <-H10 ; Auto.
Apply R_PopCallStack_monotonicity2 with pc ; Auto.
Elim H2; Clear H2; Intros c H2.
Elim (searchClass_some ? ? ? H2); Do 2 Intro.
Generalize (newObject_specif P c h h2 loc); Intro newObject_specif.
Elim (newObject_specif H9) ; Intros.
Rewrite H12.
EApply R_PopCallStack_subst_def ; EAuto.
Subst ; Auto.
Qed.
Theorem SubjectReduction_new:
(P:Program;s2:State;h:Heap;m:MethodName;pc:progCount;
S:OperandStack;L:LocalVar;sf:CallStack;
St:(AbState P); cl : ClassName)
(SmallStepSem P (config h <m,pc,L,S>::sf) s2) ->
(instructionAt P m pc)=(Some (new cl)) ->
(reachable_State P (config h <m,pc,L,S>::sf)) ->
(verifyFlow P m pc (new cl) St) ->
(R_State P (config h <m,pc,L,S>::sf) St) ->
(R_State P s2 St).
Intros ; EApply SubjectReduction_new_valid ; EAuto.
EApply reachable_is_Valid ; EAuto.
Qed.
Lemma SubjectReduction_return:
(P:Program; n : nat ; St2:State;h:Heap;m, m':MethodName;pc,pc':progCount;
s,s' :OperandStack; l,l':LocalVar;sf:CallStack; AbS:(AbState P))
(SmallStepSem P (config h <m,pc,l, s>::<m',pc',l',s'>::sf) St2) ->
(instructionAt P m pc)=(Some return) ->
(reachable_in P (config h <m,pc,l, s>::<m',pc',l',s'>::sf) n) ->
(verifyFlow P m pc return AbS) ->
(
(j : nat ; h'' : Heap ; m'': MethodName ; pc'' : progCount; l'': LocalVar ;
s'': OperandStack; sf'' : CallStack; mID : MethodID)
(lt j n)->
(reachable_in P (config h'' <m'',pc'',l'',s''>::sf'') j)->
(instructionAt P m'' pc'')=(Some (invokevirtual mID )) ->
((verifyFlow P m'' pc'' (invokevirtual mID) AbS) /\
(R_State P (config h'' <m'',pc'',l'',s''>::sf'') AbS))
) ->
(R_State P (config h <m,pc,l, s>::<m',pc',l',s'>::sf) AbS) ->
(R_State P St2 AbS).
Intros P n (h2,sf2) h m m' pc pc' s s' l l' sf (H,(L,AbS)) Hsem.
Inversion_clear Hsem; Try (Rewrite H1; Intro H' ; Discriminate H').
Intros H' Hreach HvF H_wf.
Clear H'.
Intros (Hheap,Hsf).
Inversion_clear Hsf.
Split.
Exact Hheap.
Elim (return_inv ? ? ? ? ? ? ? ? ? ? ? ? Hreach); Clear Hreach;
Intros m0 (H7,(h',(s'',(H8,(mID,(H9,(loc,(A,(B,(o,(M,H10))))))))))).
Decompose [and] H10; Clear H10.
Subst.
Elim (H_wf ? ? ? ? ? ? ? ? H7 H8 H9); Clear H_wf; Intros.
Inversion_clear H10.
Inversion_clear H14.
InvVerifyFlow P H L AbS H4.
Clear H18 H19.
Generalize HvF; Clear HvF.
Unfold verifyFlow.
Cbv Beta Iota Delta [Flow].
CaseEq '(searchMethod P m); Intros.
Match Context With
[id:(c:?)(In c ?1)->?|-?] -> ElimVerifConstr P H L AbS HvF ?1;
Clear HvF.
Rewrite H4 in H11; Injection H11; Intros; Subst; Clear H11.
Inversion_clear H3.
Rewrite H4 in H14; Injection H14; Intros; Subst; Clear H14.
Constructor.
Apply_R_LocalVar_monotonicity ; Auto.
Apply_R_Stack_monotonicity ; Auto.
CaseEq '(AbS (add m' pc')); Intros.
Generalize H15; Rewrite H3; Unfold R_Stack; Simpl.
Intros H'; Inversion_clear H'.
Simpl; Unfold R_Stack.
Generalize (top_is_top (LatAbStack P)); Simpl; Auto.
Generalize H15; Rewrite H3; Unfold R_Stack betaStack.
Intros.
Inversion H14.
Subst.
Inversion H25; Subst.
Simpl.
Generalize (top_is_top (LatAbStack P)); Simpl; Auto.
Opaque LatAbStack.
Simpl.
Elim (searchMethod_some ? ? ? H4).
Intros _ H'.
Generalize (sym_equal ? ? ? H'); Clear H'; Intros H'; Subst.
Apply order_trans with
([cl:positive]
Cases (methodLookup P mID cl) of
(Some M'0) =>
(AbPush
(AbTop (LatAbVal P) (AbS (add (nameMethod M'0) (END M'0))))
(AbPop
(AbPop_n P
(some (AbVal P)
(some_sum (AbRef P)+AbNum (inl (AbRef P) AbNum a2))::
l2) (nbArguments M'0))))
| None => (bottom (LatAbStack P))
end (class o)).
Rewrite H5.
Generalize (AbPush_monotone (LatAbVal P)
(betaVal P h2 v)
(AbTop (LatAbVal P) (AbS (add (nameMethod M') (END M'))))
(some ? (PolyList.map (betaVal P h2) s'))
); Intros.
Apply H22.
Apply order_trans with
(AbTop (LatAbVal P) (AbS (add (nameMethod M') pc))).
Unfold R_Stack betaStack in H2.
Replace (betaVal P h2 v)
with (AbTop (LatAbVal P) (some (AbVal P) (PolyList.map (betaVal P h2) v::S'))).
Apply AbTop_monotone; Auto.
Auto.
Apply AbTop_monotone; Auto.
Clear H22.
Apply order_trans with
(AbPop_n P (AbS (add m' pc')) (S (nbArguments M'))).
Unfold R_Stack betaStack in H19; Auto.
Rewrite H3.
Rewrite <- H24.
Rewrite <- H27; Auto.
Apply join_on_set_prop
with f:= [cl:positive]
Cases (methodLookup P mID cl) of
(Some M'0) =>
(AbPush
(AbTop (LatAbVal P) (AbS (add (nameMethod M'0) (END M'0))))
(AbPop
(AbPop_n P
(some (AbVal P)
(some_sum (AbRef P)+AbNum (inl (AbRef P) AbNum a2))::
l2) (nbArguments M'0))))
| None => (bottom (LatAbStack P))
end.
Generalize H25; Rewrite <- H27.
Intros.
Inversion_clear H22.
Generalize H28.
Unfold betaRef.
Rewrite H6.
Intros.
Apply singleton_in_finite; Auto.
Apply referred_class with h' m' pc' l' ((ref loc)::(app A B)) sf loc; Auto.
Apply reachable_in_reachable with m0 ; Auto.
Apply R_PopCallStack_monotonicity2 with pc' ; Auto.
Inversion_clear H21 ; Subst.
Constructor.
EApply R_PopCallStack_2 ; EAuto.
Rewrite H11 in H4; Discriminate H4.
Qed.
Theorem SubjectReduction_invokevirtual:
(P:Program;s2:State;h:Heap;m:MethodName;pc:progCount;
S:OperandStack;L:LocalVar;sf:CallStack;
St:(AbState P); mID : MethodID)
(SmallStepSem P (config h <m,pc,L,S>::sf) s2) ->
(instructionAt P m pc)=(Some (invokevirtual mID))->
(verifyFlow P m pc (invokevirtual mID) St) ->
(R_State P (config h <m,pc,L,S>::sf) St) ->
(R_State P s2 St).
Intros P (h2,sf2) h m pc s l sf (H,(L,S)) mID Hsem.
Inversion_clear Hsem; Try (Rewrite H1; Intros H'; Discriminate H'); Intros H'.
Rewrite H1 in H'.
Injection H' ; Clear H' ; Intro H'.
Rewrite H' in H1 ; Rewrite H' in H4.
Clear H'.
Intros HvF; InvVerifyFlow P H L S HvF.
Intros (Hheap,Hsf).
Inversion_clear Hsf.
Split.
Exact Hheap.
Constructor.
Unfold R_LocalVar R_Val.
Intros.
Case (inf_log_dec x (max_log_Var P)); Intros H14.
Generalize (H9 (nameMethod M') xH x).
Intro H9' ; Clear H9.
Unfold apply.
Apply order_trans with (apply_tree (AbVal P) (bottom (LatAbVal P))
(tr (AbVal P) (max_log_Var P)
(apply_tree (AbLocalVar P) (bottom (LatAbLocalVar P))
(tr (AbLocalVar P) (max_log_pc P)
(apply_tree (AbFuncPcLocalVar P)
(bottom (LatAbFuncPcLocalVar P))
(tr (AbFuncPcLocalVar P) (max_log_MethodName P)
(lift_left_unop (LatAbFuncLocalVar P)
(join_on_set (LatAbFuncLocalVar P)
[cl:positive]
Cases (methodLookup P mID cl) of
(Some M') =>
(subst (LatAbFuncPcLocalVar P)
(Fbottom (AbFuncPcLocalVar P)
(LatAbFuncPcLocalVar P)
(max_log_MethodName P))
(nameMethod M')
(subst (LatAbLocalVar P)
(Fbottom (AbLocalVar P)
(LatAbLocalVar P) (max_log_pc P))
xH
(subst_n P
(some_sum
(FiniteSet (max_log_ClassName P))
+AbNum
(inl
(FiniteSet
(max_log_ClassName P)) AbNum
(singleton cl)))::
(AbTop_n P (AbPop (S (add m pc)))
(nbArguments M')))))
| None =>
(Fbottom (AbFuncPcLocalVar P)
(LatAbFuncPcLocalVar P)
(max_log_MethodName P))
end) (AbTop (LatAbVal P) (S (add m pc)))))
(nameMethod M'))) xH)) x) ; Auto.
Inversion H12.
Clear H9'.
Simpl.
Generalize apply_on_top ; Unfold apply ; Intros.
Generalize (H15 (AbFuncPcLocalVar P) (LatAbFuncPcLocalVar P) (max_log_MethodName P)
(nameMethod M')) ; Intros.
Simpl in H17.
Rewrite H17 ; Clear H17.
Simpl in H15.
Simpl.
Generalize (H15 (AbLocalVar P) (LatAbLocalVar P) (max_log_pc P) xH) ; Intros.
Simpl in H17.
Rewrite H17 ; Clear H17.
Simpl.
Generalize (H15 (AbVal P) (LatAbVal P) (max_log_Var P) x) ; Intros.
Simpl.
Simpl in H17.
Rewrite H17 ; Auto.
Unfold betaVal ; Simpl.
Case (Cases (pred (convert x)) of
(0) => (ref loc)
| ((S m0)) => (nth m0 A null)
end) ; Intros.
Simpl ; Apply sum_order_top.
Simpl ; Apply sum_order_top.
Simpl ; Apply sum_order_top.
Constructor.
EApply methodLookUp_prop ; EAuto.
Opaque order apply_tree bottom nth.
Simpl.
Clear H9'.
Do 3 Rewrite apply_apply_tree.
Generalize (orderS_length (AbVal P) (LatAbVal P) ? ? H18) ; Intros.
Rewrite map_length in H19.
Generalize (length_app ? A S0) ; Intros.
Rewrite H19 in H20 ; Rewrite <-H6 in H20 ; Rewrite H5 in H20.
Clear H19.
LetTac theJoinfunc := [cl0:positive]
Cases (methodLookup P mID cl0) of
(Some M'0) =>
(subst (LatAbFuncPcLocalVar P)
(Fbottom (AbFuncPcLocalVar P)
(LatAbFuncPcLocalVar P) (max_log_MethodName P))
(nameMethod M'0)
(subst (LatAbLocalVar P)
(Fbottom (AbLocalVar P) (LatAbLocalVar P)
(max_log_pc P)) xH
(subst_n P
(some_sum
(FiniteSet (max_log_ClassName P))+AbNum
(inl (FiniteSet (max_log_ClassName P))
AbNum (singleton cl0)))::
(AbTop_n P (some (AbVal P) l2)
(nbArguments M'0)))))
| None =>
(Fbottom (AbFuncPcLocalVar P)
(LatAbFuncPcLocalVar P) (max_log_MethodName P))
end.
Generalize (join_on_set_prop (max_log_ClassName P) (AbFuncLocalVar P) (LatAbFuncLocalVar P)
theJoinfunc) ; Intros.
CaseEq x2 ; Intros.
Rewrite H21 in H17.
Transparent order apply_tree bottom nth.
Simpl in H17.
Inversion H17.
Unfold lift_left_unop.
Unfold LatAbFuncLocalVar.
Generalize
(apply_on_top (AbFuncPcLocalVar P) (LatAbFuncPcLocalVar P) (max_log_MethodName P) (nameMethod M') ) ;
Intros.
Opaque nth order.
Simpl in H22 ; Simpl.
Rewrite H22.
Generalize
(apply_on_top (AbLocalVar P) (LatAbLocalVar P) (max_log_pc P) xH) ;
Intros.
Simpl in H23 ; Simpl.
Rewrite H23.
Generalize
(apply_on_top (AbVal P) (LatAbVal P) (max_log_Var P) x) ;
Intros.
Simpl in H24 ; Simpl.
Rewrite H24.
Transparent order.
Simpl.
Constructor.
Trivial.
Constructor.
EApply methodLookUp_prop ; EAuto.
CaseEq s0 ; Intros.
Opaque order nth.
Simpl.
Generalize (join_on_set_prop (max_log_ClassName P) (AbFuncLocalVar P) (LatAbFuncLocalVar P)
theJoinfunc a (class o)) ; Intros.
Transparent order.
Rewrite H22 in H21 ; Rewrite H21 in H17 ; Simpl in H17.
Inversion_clear H17.
Generalize H24 ; Clear H24 ; Unfold betaRef; Rewrite H2 ; Intro H24.
Cut (in_finite (max_log_ClassName P) (class o) a) ; Intros.
Generalize (H23 H17) ; Clear H23 H17 ; Intro H23.
Generalize (H23 (nameMethod M') xH x).
Intro H19' ; Clear H23.
Unfold apply.
Apply order_trans with (apply_tree (AbVal P) (bottom (LatAbVal P))
(tr (AbVal P) (max_log_Var P)
(apply_tree (AbLocalVar P) (bottom (LatAbLocalVar P))
(tr (AbLocalVar P) (max_log_pc P)
(apply_tree (AbFuncPcLocalVar P)
(bottom (LatAbFuncPcLocalVar P))
(tr (AbFuncPcLocalVar P) (max_log_MethodName P)
(theJoinfunc (class o))) (nameMethod M'))) xH))
x); Auto.
Clear H19'.
Replace theJoinfunc with [cl0:positive]
Cases (methodLookup P mID cl0) of
(Some M'0) =>
(subst (LatAbFuncPcLocalVar P)
(Fbottom (AbFuncPcLocalVar P)
(LatAbFuncPcLocalVar P) (max_log_MethodName P))
(nameMethod M'0)
(subst (LatAbLocalVar P)
(Fbottom (AbLocalVar P) (LatAbLocalVar P)
(max_log_pc P)) xH
(subst_n P
(some_sum
(FiniteSet (max_log_ClassName P))+AbNum
(inl (FiniteSet (max_log_ClassName P))
AbNum (singleton cl0)))::
(AbTop_n P (some (AbVal P) l2)
(nbArguments M'0)))))
| None =>
(Fbottom (AbFuncPcLocalVar P)
(LatAbFuncPcLocalVar P) (max_log_MethodName P))
end ; Auto.
Rewrite H4.
Do 3 Rewrite apply_apply_tree.
Rewrite H7.
Rewrite apply_subst1 ; [Idtac | EApply methodLookUp_prop ; EAuto].
Rewrite apply_subst1 ; [Idtac | Constructor].
Cut
(P: Program ; x: positive ; l : (list (AbVal P)))
(inf_log x (max_log_Var P)) -> (apply (LatAbVal P) (subst_n P l) x) =
(nth (pred (convert x)) l(bottom (LatAbVal P))).
Intros.
Generalize (H17 P x
(some_sum (FiniteSet (max_log_ClassName P))+AbNum
(inl (FiniteSet (max_log_ClassName P)) AbNum
(singleton (class o))))::
(AbTop_n P (some (AbVal P) l2) (nbArguments M')) H14) ;
Clear H17; Intros ; Auto.
Transparent order.
Rewrite H17.
LetTac N := (pred (convert x)).
CaseEq N ; Intros.
Transparent nth.
Simpl.
Constructor.
Unfold betaRef.
Rewrite H2 ; Auto.
Opaque order bottom.
Simpl.
Case (le_gt_dec (nbArguments M') n0 ) ; Intros.
Rewrite <- H5 in l0 ; Rewrite H6 in l0.
Rewrite nth_notIn ; Auto.
Unfold betaVal betaRef.
Apply bottom_is_a_bottom.
Cut (P: Program ; n,m : nat ; l : (list (AbVal P)))
(lt n m) -> (le m (length l))->
(nth n (AbTop_n P (some (AbVal P) l) m)
(bottom (LatAbVal P))) =
(nth n l (bottom (LatAbVal P))).
Intros.
Rewrite (H25 P) ; Auto with arith.
Transparent bottom.
Simpl.
Cut
(P: Program ; A, A' : (OperandStack) ; h : Heap ; l : (list (AbVal P)))
(orderS (AbVal P) (LatAbVal P)
(some (AbVal P) (PolyList.map (betaVal P h) (app A A')))
(some (AbVal P) l))
-> (n : nat) (order (LatAbVal P) (betaVal P h (nth n A null))
(nth n l (bot_sum (AbRef P)+AbNum))).
Intro.
EApply H26 ; EAuto.
Apply orderS_order.
Intros.
Apply nth_AbTop_n ; Auto.
Intros ; Apply nth_subst_n ; Auto.
Elim H3 ; Intros ; Intuition.
Rewrite <- H26 ; Rewrite <- H26 in H24.
Apply singleton_in_finite ; Auto.
Unfold max_log_ClassName ; EApply in_inf_log ; EAuto.
Rewrite H22 in H21 ; Rewrite H21 in H17.
Transparent order.
Inversion H17.
Rewrite H7.
Rewrite nth_notIn.
Simpl.
Generalize (bottom_is_a_bottom (LatAbVal P)).
Simpl; Auto.
Apply not_gt.
Red; Intros; Elim H14; Clear H14.
Rename S into AbS.
Apply inf_log_trans with (anti_convert (S (nbArguments M'))).
Apply valid_nbArguments; Auto.
Generalize H4.
Unfold methodLookup.
CaseEq '(searchClass P (class o)); Do 2 Intro.
CaseEq '(searchWithMethodID (list_methods_lookup c) mID); Do 2 Intro.
CaseEq '(searchMethod P m0); Intros.
Injection H18; Intros; Subst.
Elim (searchMethod_some ? ? ? H17); Auto.
Discriminate H18.
Discriminate H17.
Discriminate H16.
Rewrite <- H5.
Rewrite H6.
Simpl in H15.
Apply convert_compare_INFERIEUR.
Rewrite bij1.
Omega.
Clear H9.
Opaque bottom.
Generalize (H10 (nameMethod M') xH) ; Intros.
Do 4 Rewrite apply_apply_tree in H9.
Clear H10.
Unfold R_Stack.
Apply order_trans with (apply (LatAbStack P)
(apply (LatAbFuncPcStack P)
(lift_left_unop (LatAbFuncStack P)
(join_on_set (LatAbFuncStack P)
[cl:positive]
Cases (methodLookup P mID cl) of
(Some M') =>
(subst (LatAbFuncPcStack P)
(Fbottom (AbFuncPcStack P) (LatAbFuncPcStack P)
(max_log_MethodName P)) (nameMethod M')
(subst (LatAbStack P)
(Fbottom (AbStack P) (LatAbStack P)
(max_log_pc P)) xH
(some (AbVal P) (nil (AbVal P)))))
| None =>
(Fbottom (AbFuncPcStack P) (LatAbFuncPcStack P)
(max_log_MethodName P))
end) (AbTop (LatAbVal P) (S (add m pc))))
(nameMethod M')) xH) ; Auto.
Clear H9.
Inversion H12.
Simpl.
Generalize apply_on_top ; Intros.
Simpl in H10.
Rewrite H10 ; Auto.
Simpl.
Rewrite H10 ; Auto.
Constructor.
EApply methodLookUp_prop ; EAuto.
CaseEq x2 ; Intros.
Rewrite H17 in H15.
Inversion H15.
Simpl.
Generalize apply_on_top ; Intros.
Simpl in H18.
Rewrite H18 ; Auto.
Simpl.
Rewrite H18 ; Auto.
Constructor.
EApply methodLookUp_prop ; EAuto.
CaseEq s0 ; Intros.
Rewrite H18 in H17 ; Rewrite H17 in H15 ; Simpl in H15.
Inversion_clear H15.
Subst.
Simpl.
LetTac thejoinfunc := [cl0:positive]
Cases (methodLookup P mID cl0) of
(Some M'0) =>
(subst (LatAbFuncPcStack P)
(Fbottom (AbFuncPcStack P) (LatAbFuncPcStack P)
(max_log_MethodName P)) (nameMethod M'0)
(subst (LatAbStack P)
(Fbottom (AbStack P) (LatAbStack P) (max_log_pc P))
xH (some (AbVal P) (nil (AbVal P)))))
| None =>
(Fbottom (AbFuncPcStack P) (LatAbFuncPcStack P)
(max_log_MethodName P))
end.
Unfold betaStack; Simpl.
Cut (order (LatAbStack P) (some (AbVal P) (nil (AbVal P)))
(apply (LatAbStack P)
(apply (LatAbFuncPcStack P)
(join_on_set (LatAbFuncStack P) thejoinfunc a) (nameMethod M'))
xH)) ; Intros ; Auto.
Generalize join_on_set_prop ; Intros.
Simpl in H5.
Generalize (H5 (max_log_ClassName P) (AbFuncStack P)(LatAbFuncStack P)) ; Clear H5;
Intros.
Generalize (H5 thejoinfunc a (class o)) ; Clear H5 ; Intros.
Cut (in_finite (max_log_ClassName P) (class o) a) ; Intros.
Generalize (H5 H7) ; Clear H5 H7 ; Intros.
Generalize (H5 (class o) xH) ; Clear H5 ; Intros.
Do 4 Rewrite apply_apply_tree in H5.
Apply order_trans with (apply (LatAbStack P)
(apply (LatAbFuncPcStack P) (thejoinfunc (class o))
(nameMethod M') ) xH).
Clear H5.
Replace thejoinfunc with [cl0:positive]
Cases (methodLookup P mID cl0) of
(Some M'0) =>
(subst (LatAbFuncPcStack P)
(Fbottom (AbFuncPcStack P) (LatAbFuncPcStack P)
(max_log_MethodName P)) (nameMethod M'0)
(subst (LatAbStack P)
(Fbottom (AbStack P) (LatAbStack P)
(max_log_pc P)) xH
(some (AbVal P) (nil (AbVal P)))))
| None =>
(Fbottom (AbFuncPcStack P) (LatAbFuncPcStack P)
(max_log_MethodName P))
end ; Auto.
Rewrite H4 ; Simpl.
Generalize apply_subst1 ; Intros.
Transparent order.
Rewrite apply_subst1.
Rewrite apply_subst1.
Constructor.
Constructor.
EApply methodLookUp_prop ; EAuto.
Do 2 Apply apply_monotone.
EApply join_on_set_prop ; EAuto.
Elim H3 ; Intros ; Intuition.
Apply singleton_in_finite ; Auto.
Rewrite <- H10.
Unfold max_log_ClassName ; EApply in_inf_log ; EAuto.
Generalize H19 ; Unfold betaRef ; Clear H19 ; Rewrite H2 ; Intro H19 ; Apply H19.
Elim H3 ; Intros ; Intuition.
Apply singleton_in_finite ; Auto.
Rewrite <- H10.
Unfold max_log_ClassName ; EApply in_inf_log ; EAuto.
Generalize H19 ; Unfold betaRef ; Clear H19 ; Rewrite H2 ; Intro H19 ; Apply H19.
Rewrite H18 in H17 ; Rewrite H17 in H15 ; Inversion H15.
Generalize (searchMethod_some_inv P M') ; Intros.
Apply R_PopCallStack_2 with M' ; Auto.
Apply H14.
Generalize H4 ; Unfold methodLookup.
CaseEq '(searchClass P (class o)) ; Do 2 Intro.
CaseEq '(searchWithMethodID (list_methods_lookup c) mID) ; Do 2 Intro.
CaseEq '(searchMethod P m0) ; Intros.
Injection H18 ; Intros ; Subst.
Generalize (searchMethod_some P m0 M') ; Intros; Intuition.
Discriminate H18.
Discriminate H17.
Discriminate H16.
Generalize H12 ; Replace ((ref loc))::(app A S0) with (app ((ref loc))::A S0) ;
Intros ; Auto.
LetTac S_add := (S (add m pc)).
Generalize (plus_Snm_nSm (0)) ; Intros.
Unfold 2 plus in H16.
Generalize (H16 (nbArguments M')) ; Clear H16 ; Intro H16.
Rewrite <- H16.
Replace (plus (1) (nbArguments M')) with (length ((ref loc)::A)) ; Auto.
EApply R_Stack_AbPop_n ; EAuto.
Simpl ; Omega.
Inversion H13.
Constructor.
EApply R_PopCallStack_2 ; EAuto.
Qed.
Theorem SubjectReduction_wf:
(P : Program ; n : nat ; St : State ; h : Heap ; m: MethodName ; pc: progCount;
l: LocalVar ;s: OperandStack;sf: CallStack ; I: Instruction ; AbS : (AbState P))
(reachable_in P (config h <m,pc,l,s>::sf) n) ->
(instructionAt P m pc)= (Some I) ->
(verifyFlow P m pc I AbS) ->
(R_State P (config h <m,pc,l,s>::sf) AbS)->
(
(j : nat) (h' : Heap ; m': MethodName ; pc': progCount;
l': LocalVar ;s': OperandStack;sf': CallStack ; I': Instruction)
(lt j n) ->
(reachable_in P (config h' <m',pc',l',s'>::sf') j) ->
(instructionAt P m' pc')= (Some I') ->
((verifyFlow P m' pc' I' AbS) /\
(R_State P (config h' <m',pc',l',s'>::sf') AbS))
)->
(SmallStepSem P (config h <m,pc,l,s>::sf) St) ->
(R_State P St AbS).
Intros.
CaseEq I ; Intros.
Subst.
Generalize (SubjectReduction_nop P St h m pc s l sf AbS H4 H0 H1 H2) ;
Intros ; Auto.
Subst.
Generalize (SubjectReduction_push P St h m pc s l sf AbS i H4 H0 H1 H2) ;
Intros ; Auto.
Subst.
Generalize (SubjectReduction_pop P St h m pc s l sf AbS H4 H0 H1 H2) ;
Intros ; Auto.
Subst.
Generalize (SubjectReduction_numop P St h m pc s l sf AbS o H4 H0 H1 H2) ;
Intros ; Auto.
Subst.
Generalize (SubjectReduction_load P St h m pc s l sf AbS v H4 H0 H1 H2) ;
Intros ; Auto.
Subst.
Generalize (SubjectReduction_store P St h m pc s l sf AbS v H4 H0 H1 H2) ;
Intros ; Auto.
Subst.
Generalize (SubjectReduction_if P St h m pc s l sf AbS p H4 H0 H1 H2) ;
Intros ; Auto.
Subst.
Generalize (reachable_in_reachable ? ? ?H) ; Intros.
Generalize (SubjectReduction_new P St h m pc s l sf AbS c H4 H0 H5 H1 H2) ;
Intros ; Auto.
Subst.
Generalize (SubjectReduction_putfield P St h m pc s l sf AbS f H4 H0 H1 H2);
Intros ; Auto.
Subst.
Generalize (SubjectReduction_getfield P St h m pc s l sf AbS f H4 H0 H1 H2);
Intros ; Auto.
Subst.
Generalize (SubjectReduction_invokevirtual P St h m pc s l sf AbS m0 H4 H0 H1 H2);
Intros ; Auto.
Subst.
Generalize (return_inv2 ? ? ? ? ? ? ? ? H H0) ; Intros.
Do 5 (Elim H5 ; Clear H5 ; Intros).
Generalize (SubjectReduction_return P n St h m x pc x0 s x2 l x1 x3 AbS) ; Intros.
Subst.
Generalize (H6 H4 H0 H H1) ; Clear H6 ; Intros.
Apply H5 ; Clear H5.
Intros.
Generalize (H3 ? ? ? ? ? ? ? ? H5 H6 H7) ; Clear H3 ; Intros; Auto.
Assumption.
Subst.
Generalize (SubjectReduction_dup P St h m pc s l sf AbS H4 H0 H1 H2);
Intros ; Auto.
Subst.
Generalize (SubjectReduction_goto P St h m pc s l sf AbS p H4 H0 H1 H2) ; Intros;
Auto.
Subst.
Generalize (SubjectReduction_swap P St h m pc s l sf AbS H4 H0 H1 H2) ; Intros;
Auto.
Subst.
Generalize (SubjectReduction_dup2 P St h m pc s l sf AbS H4 H0 H1 H2) ; Intros;
Auto.
Qed.
Theorem SubjectReduction :
(P : Program ; st : State ; AbS : (AbState P))
(verifyAllFlow P AbS)->
(reachable_State P st) ->
(R_State P st AbS).
Intros P st AbS Hvf Hsem.
Elim (reachable_reachable_in P st); Auto; Intros.
Generalize st H Hsem; Clear H Hsem st.
Apply (lt_wf_ind x [x] (st:State)(reachable_in P st x)->(reachable_State P st)->(R_State P st AbS)); Intros.
Generalize H; Clear H.
Inversion_clear H0; Intros HP.
Apply verifyAllFlow_hyp2; Auto.
CaseEq st0; Intros; Subst.
CaseEq c; Intros; Subst.
Elim (Nonempty_reachable_frame P h (nil ?)); Intros; Auto.
Apply reachable_in_reachable with n0; Auto.
CaseEq f; Intros; Subst.
Elim (smallstep_instruction_only P h m p l0 o l st H2); Intros I HI.
Apply (SubjectReduction_wf P n0 st h m p l0 o l I AbS H HI); Auto.
Apply verifyAllFlow_hyp1; Auto.
Apply HP with n0; Auto.
Apply reachable_in_reachable with n0; Auto.
Intros.
Split.
Apply verifyAllFlow_hyp1; Auto.
Apply HP with j; Auto.
Apply reachable_in_reachable with j; Auto.
Qed.