Library correct
Require Export AlgebraType.
Section correct.
Variable P : Program.
Variable R : Ref.Connect P.
Variable N : Num.Connect.
Variable V : Value.Connect (Num.Pos N) (Ref.Pos R).
Variable S : Stack.Connect (Value.Pos V).
Variable L : LocalVar.Connect (Value.Pos V).
Variable O : Object.Connect (Value.Pos V).
Variable H : Heap.Connect (Ref.Pos R) (Object.Pos O).
Record AbMem : Set := st {
Hproj : Heap.t H;
Sproj : Stack.t S;
Lproj : LocalVar.t L
}.
Definition AbState := progCount -> AbMem.
Inductive gammaMem (M:AbMem) : VTrace P -> Prop :=
gammaMem_def : forall (tr:VTrace P) h l s pc,
currentState tr = <<h,pc,l,s>> ->
(Heap.gamma H (Ref.gamma R (Ref.context R tr))
(Object.gamma O P (Value.gamma V (Num.gamma N) (Ref.gamma R (Ref.context R tr))))
(Hproj M) h) ->
(Stack.gamma S (Value.gamma V (Num.gamma N) (Ref.gamma R (Ref.context R tr))) (Sproj M) s) ->
(LocalVar.gamma L (Value.gamma V (Num.gamma N) (Ref.gamma R (Ref.context R tr))) (Lproj M) l) ->
gammaMem M tr.
Inductive gammaSt (ST:AbState) : VTrace P -> Prop :=
gammaSt_def : forall (tr:VTrace P) h l s pc,
currentState tr = <<h,pc,l,s>> ->
gammaMem (ST pc) tr ->
gammaSt ST tr.
Definition AbTransfMem (r:rule) (pc:progCount) : AbMem -> AbMem :=
match r with
| nop1 => fun s => st (Hproj s) (Sproj s) (Lproj s)
| push1 i => fun s => st (Hproj s) (Stack.push_ab S (Value.injN_ab V (Num.const_ab N i)) (Sproj s)) (Lproj s)
| pop1 => fun s => st (Hproj s) (Stack.pop_ab S (Sproj s)) (Lproj s)
| numop1 op => fun s => st (Hproj s) (Stack.push_ab S (Value.injN_ab V (Num.sem_binop_ab N op (Value.getN_ab V (Stack.top_ab S (Sproj s))) (Value.getN_ab V (Stack.top_ab S (Stack.pop_ab S (Sproj s)))))) (Stack.pop_ab S (Stack.pop_ab S (Sproj s)))) (Lproj s)
| load1 x => fun s => st (Hproj s) (Stack.push_ab S (LocalVar.get_ab L x (Lproj s)) (Sproj s)) (Lproj s)
| store1 x => fun s => st (Hproj s) (Stack.pop_ab S (Sproj s)) (LocalVar.store_ab L x (Lproj s) (Stack.top_ab S (Sproj s)))
| If1 pc' => fun s => st (Hproj s) (Stack.pop_ab S (Sproj s)) (Lproj s)
| If2 pc' => fun s => st (Hproj s) (Stack.pop_ab S (Sproj s)) (Lproj s)
| new1 cl => fun s => st (Heap.puto_ab H (Hproj s) (Ref.newLoc_ab R cl pc) (Object.def_ab O P cl (Value.injN_ab V (Num.const_ab N 0)) (Value.null_ab V))) (Stack.push_ab S (Value.injR_ab V (Ref.newLoc_ab R cl pc)) (Sproj s)) (Lproj s)
| putfield1 f => fun s => st (Heap.puto_ab H (Hproj s) (Value.getR_ab V (Stack.top_ab S (Stack.pop_ab S (Sproj s)))) (Object.putf_ab O f (Heap.geto_ab H (Hproj s) (Value.getR_ab V (Stack.top_ab S (Stack.pop_ab S (Sproj s))))) (Stack.top_ab S (Sproj s)))) (Stack.pop_ab S (Stack.pop_ab S (Sproj s))) (Lproj s)
| getfield1 f => fun s => st (Hproj s) (Stack.push_ab S (Object.getf_ab O f (Heap.geto_ab H (Hproj s) (Value.getR_ab V (Stack.top_ab S (Sproj s))))) (Stack.pop_ab S (Sproj s))) (Lproj s)
| goto1 pc' => fun s => st (Hproj s) (Sproj s) (Lproj s)
end.
Definition AbTransPC (r:rule) : progCount -> progCount :=
match r with
| If1 pc' => fun _ => pc'
| goto1 pc' => fun _ => pc'
| _ => fun pc => nextAddress P pc
end.
Lemma gammaHeap_monotone : forall tr1 tr2,
Ref.relC R (Ref.context R tr1) (Ref.context R tr2) ->
Ref.relC R (Ref.context R tr2) (Ref.context R tr1) ->
orderGamma (Heap.gamma H (Ref.gamma R (Ref.context R tr1))
(Object.gamma O P (Value.gamma V (Num.gamma N) (Ref.gamma R (Ref.context R tr1)))))
(Heap.gamma H (Ref.gamma R (Ref.context R tr2))
(Object.gamma O P (Value.gamma V (Num.gamma N) (Ref.gamma R (Ref.context R tr2))))).
Proof.
intros.
apply Heap.gamma_functor_monotone.
apply Ref.gamma_monotone; assumption.
apply Object.gamma_functor_monotone.
apply Value.gamma_functor_monotone.
apply orderGamma_refl.
apply Ref.gamma_monotone; assumption.
Qed.
Lemma gammaHeap_monotone' : forall tr1 tr2,
Ref.relC R (Ref.context R tr1) (Ref.context R tr2) ->
orderGamma (Heap.gamma H (Ref.gamma R (Ref.context R tr1))
(Object.gamma O P (Value.gamma V (Num.gamma N) (Ref.gamma R (Ref.context R tr1)))))
(Heap.gamma H (Ref.gamma R (Ref.context R tr1))
(Object.gamma O P (Value.gamma V (Num.gamma N) (Ref.gamma R (Ref.context R tr2))))).
Proof.
intros.
apply Heap.gamma_functor_monotone.
apply orderGamma_refl.
apply Object.gamma_functor_monotone.
apply Value.gamma_functor_monotone.
apply orderGamma_refl.
apply Ref.gamma_monotone; assumption.
Qed.
Lemma gammaLocalVar_monotone : forall tr1 tr2,
Ref.relC R (Ref.context R tr1) (Ref.context R tr2) ->
orderGamma (LocalVar.gamma L (Value.gamma V (Num.gamma N) (Ref.gamma R (Ref.context R tr1))))
(LocalVar.gamma L (Value.gamma V (Num.gamma N) (Ref.gamma R (Ref.context R tr2)))).
Proof.
intros.
apply LocalVar.gamma_functor_monotone.
apply Value.gamma_functor_monotone.
apply orderGamma_refl.
apply Ref.gamma_monotone; assumption.
Qed.
Lemma gammaStack_monotone : forall tr1 tr2,
Ref.relC R (Ref.context R tr1) (Ref.context R tr2) ->
orderGamma (Stack.gamma S (Value.gamma V (Num.gamma N) (Ref.gamma R (Ref.context R tr1))))
(Stack.gamma S (Value.gamma V (Num.gamma N) (Ref.gamma R (Ref.context R tr2)))).
Proof.
intros.
apply Stack.gamma_functor_monotone.
apply Value.gamma_functor_monotone.
apply orderGamma_refl.
apply Ref.gamma_monotone; assumption.
Qed.
Ltac ApplyGammaMonotone tr :=
(apply gammaHeap_monotone with tr; [assumption|assumption|idtac])
||
(apply gammaStack_monotone with tr; [assumption|idtac])
||
(apply gammaLocalVar_monotone with tr; [assumption|idtac]).
Lemma AbTransfMem_correct_aux : forall M r h1 l1 s1 pc1 h2 l2 s2 pc2 (tr1 tr2:VTrace P),
SmallStepSemTrace P r tr1 tr2 ->
Ref.relC R (Ref.context R tr1) (Ref.context R tr2) ->
(instr_not_new r -> Ref.relC R (Ref.context R tr2) (Ref.context R tr1)) ->
currentState tr1 = <<h1,pc1,l1,s1>> ->
currentState tr2 = <<h2,pc2,l2,s2>> ->
f_h P (sem_func P r) (h1,s1,l1) h2 ->
f_s P (sem_func P r) (h1,s1,l1) s2 ->
f_l P (sem_func P r) (h1,s1,l1) l2 ->
gammaMem M tr1 -> gammaMem (AbTransfMem r pc1 M) tr2.
Proof.
intros (AbH,AbS,AbL) r h1 l1 s1 pc1 h2 l2 s2 pc2 tr1 tr2 HSemTr RelC RelC' Hc1 Hc2.
destruct r; simpl; intros Heq Seq Leq Hgam1;
try (cut (Ref.relC R (Ref.context R tr2) (Ref.context R tr1)); [clear RelC'; intros RelC' |apply RelC'; constructor; fail]);
inversion_clear Hgam1 as [tr' h' l' s' pc' Hcur HgammaH HgammaS HgammaL]; simpl in *;
rewrite Hcur in Hc1; injection Hc1; intros; subst; clear Hc1;
constructor 1 with h2 l2 s2 pc2; subst; simpl in *; subst; auto.
ApplyGammaMonotone tr1; inversion_clear Heq in HgammaH; assumption.
ApplyGammaMonotone tr1; inversion_clear Seq in HgammaS; assumption.
ApplyGammaMonotone tr1; inversion_clear Leq in HgammaL; assumption.
ApplyGammaMonotone tr1; inversion_clear Heq in HgammaH; assumption.
apply Stack.push_ab_correct; inversion_clear Seq as [idSeq1 idSeq2 Seq0 Seq1 Seq2 ]; constructor 1 with idSeq1 idSeq2; [assumption|apply Value.injN_ab_correct; inversion_clear Seq0 as [idSeq01 Seq00 Seq01 ]; constructor 1 with idSeq01; [assumption|apply Num.const_ab_correct; inversion_clear Seq00; reflexivity]|ApplyGammaMonotone tr1; inversion_clear Seq1 in HgammaS; assumption].
ApplyGammaMonotone tr1; inversion_clear Leq in HgammaL; assumption.
ApplyGammaMonotone tr1; inversion_clear Heq in HgammaH; assumption.
apply Stack.pop_ab_correct; inversion_clear Seq as [idSeq1 Seq0 Seq1 ]; constructor 1 with idSeq1; [assumption|ApplyGammaMonotone tr1; inversion_clear Seq0 in HgammaS; assumption].
ApplyGammaMonotone tr1; inversion_clear Leq in HgammaL; assumption.
ApplyGammaMonotone tr1; inversion_clear Heq in HgammaH; assumption.
apply Stack.push_ab_correct; inversion_clear Seq as [idSeq1 idSeq2 Seq0 Seq1 Seq2 ]; constructor 1 with idSeq1 idSeq2; [assumption|apply Value.injN_ab_correct; inversion_clear Seq0 as [idSeq01 Seq00 Seq01 ]; constructor 1 with idSeq01; [assumption|apply Num.sem_binop_ab_correct; inversion_clear Seq00 as [idSeq001 idSeq002 Seq000 Seq001 Seq002 ]; constructor 1 with idSeq001 idSeq002; idtac]|apply Stack.pop_ab_correct; inversion_clear Seq1 as [idSeq11 Seq10 Seq11 ]; constructor 1 with idSeq11; [assumption|apply Stack.pop_ab_correct; inversion_clear Seq10 as [idSeq101 Seq100 Seq101 ]; constructor 1 with idSeq101; [assumption|ApplyGammaMonotone tr1; inversion_clear Seq100 in HgammaS; assumption]]].
assumption.
apply (Value.getN_ab_correct V (Num.gamma N) (Ref.gamma R (Ref.context R tr1)));
inversion_clear Seq000 as [idSeq0001 Seq0000 Seq0001 ]; constructor 1 with idSeq0001; [assumption|apply Stack.top_ab_correct; inversion_clear Seq0000 as [idSeq00001 Seq00000 Seq00001 ]; constructor 1 with idSeq00001; [assumption| inversion_clear Seq00000 in HgammaS; assumption]].
apply (Value.getN_ab_correct V (Num.gamma N) (Ref.gamma R (Ref.context R tr1))); inversion_clear Seq001 as [idSeq0011 Seq0010 Seq0011 ]; constructor 1 with idSeq0011; [assumption|apply Stack.top_ab_correct; inversion_clear Seq0010 as [idSeq00101 Seq00100 Seq00101 ]; constructor 1 with idSeq00101; [assumption|apply Stack.pop_ab_correct; inversion_clear Seq00100 as [idSeq001001 Seq001000 Seq001001 ]; constructor 1 with idSeq001001; [assumption|inversion_clear Seq001000 in HgammaS; assumption]]].
ApplyGammaMonotone tr1; inversion_clear Leq in HgammaL; assumption.
ApplyGammaMonotone tr1; inversion_clear Heq in HgammaH; assumption.
apply Stack.push_ab_correct; inversion_clear Seq as [idSeq1 idSeq2 Seq0 Seq1 Seq2 ]; constructor 1 with idSeq1 idSeq2; [assumption|apply LocalVar.get_ab_correct; inversion_clear Seq0 as [idSeq01 Seq00 Seq01 ]; constructor 1 with idSeq01; [assumption|ApplyGammaMonotone tr1; inversion_clear Seq00 in HgammaL; assumption]|ApplyGammaMonotone tr1; inversion_clear Seq1 in HgammaS; assumption].
ApplyGammaMonotone tr1; inversion_clear Leq in HgammaL; assumption.
ApplyGammaMonotone tr1; inversion_clear Heq in HgammaH; assumption.
apply Stack.pop_ab_correct; inversion_clear Seq as [idSeq1 Seq0 Seq1 ]; constructor 1 with idSeq1; [assumption|ApplyGammaMonotone tr1; inversion_clear Seq0 in HgammaS; assumption].
apply LocalVar.store_ab_correct; inversion_clear Leq as [idLeq1 idLeq2 Leq0 Leq1 Leq2 ]; constructor 1 with idLeq1 idLeq2; [assumption|ApplyGammaMonotone tr1; inversion_clear Leq0 in HgammaL; assumption|apply Stack.top_ab_correct; inversion_clear Leq1 as [idLeq11 Leq10 Leq11 ]; constructor 1 with idLeq11; [assumption|ApplyGammaMonotone tr1; inversion_clear Leq10 in HgammaS; assumption]].
ApplyGammaMonotone tr1; inversion_clear Heq in HgammaH; assumption.
apply Stack.pop_ab_correct; inversion_clear Seq as [idSeq1 Seq0 Seq1 ]; constructor 1 with idSeq1; [assumption|ApplyGammaMonotone tr1; inversion_clear Seq0 in HgammaS; assumption].
ApplyGammaMonotone tr1; inversion_clear Leq in HgammaL; assumption.
ApplyGammaMonotone tr1; inversion_clear Heq in HgammaH; assumption.
apply Stack.pop_ab_correct; inversion_clear Seq as [idSeq1 Seq0 Seq1 ]; constructor 1 with idSeq1; [assumption|ApplyGammaMonotone tr1; inversion_clear Seq0 in HgammaS; assumption].
ApplyGammaMonotone tr1; inversion_clear Leq in HgammaL; assumption.
inversion_clear Heq.
apply (Heap.puto_ab_correct' H (Ref.gamma R (Ref.context R tr1)) (Ref.gamma R (Ref.context R tr2)))
with b c0 d; auto .
apply gammaHeap_monotone'; auto.
inversion_clear H0 in HgammaH; auto.
apply Ref.newLoc_ab_correct with tr1; auto.
rewrite Hcur; reflexivity.
inversion_clear H1.
constructor 1 with b0; auto.
rewrite Hcur; inversion_clear H4; reflexivity.
inversion_clear H2.
apply Object.def_ab_correct.
intro; intros.
apply Value.null_ab_correct; auto.
intro; intros.
apply Value.injN_ab_correct.
exists 0.
subst; constructor.
apply Num.const_ab_correct; auto.
constructor 1 with b0; auto.
intros.
apply Ref.conservation_during_new with c tr2 h1; auto.
rewrite Hcur; auto.
inversion_clear H0; auto.
apply Stack.push_ab_correct; inversion_clear Seq as [idSeq1 idSeq2 Seq0 Seq1 Seq2 ]; constructor 1 with idSeq1 idSeq2.
assumption.
apply Value.injR_ab_correct; inversion_clear Seq0 as [idSeq01 Seq00 Seq01 ]; constructor 1 with idSeq01.
assumption.
apply Ref.newLoc_ab_correct with tr1; auto.
rewrite Hcur; auto.
exists h1.
inversion_clear Seq00.
inversion_clear H0; auto.
rewrite Hcur; reflexivity.
ApplyGammaMonotone tr1.
inversion_clear Seq1 in HgammaS; auto.
ApplyGammaMonotone tr1; inversion_clear Leq in HgammaL; assumption.
apply Heap.puto_ab_correct; inversion_clear Heq as [idHeq1 idHeq2 idHeq3 Heq0 Heq1 Heq2 Heq3 ]; constructor 1 with idHeq1 idHeq2 idHeq3.
assumption.
ApplyGammaMonotone tr1; inversion_clear Heq0 in HgammaH; assumption.
apply (Value.getR_ab_correct V (Num.gamma N) (Ref.gamma R (Ref.context R tr2))).
inversion_clear Heq1 as [idHeq11 Heq10 Heq11 ]; constructor 1 with idHeq11.
assumption.
apply Stack.top_ab_correct; inversion_clear Heq10 as [idHeq101 Heq100 Heq101 ]; constructor 1 with idHeq101; [assumption|apply Stack.pop_ab_correct; inversion_clear Heq100 as [idHeq1001 Heq1000 Heq1001 ]; constructor 1 with idHeq1001; [assumption|ApplyGammaMonotone tr1; inversion_clear Heq1000 in HgammaS; assumption]].
apply Object.putf_ab_correct; inversion_clear Heq2 as [idHeq21 idHeq22 Heq20 Heq21 Heq22 ]; constructor 1 with idHeq21 idHeq22.
assumption.
apply Heap.geto_ab_correct with (Ref.gamma R (Ref.context R tr2)).
inversion_clear Heq20 as [idHeq201 idHeq202 Heq200 Heq201 Heq202 ]; constructor 1 with idHeq201 idHeq202.
assumption.
ApplyGammaMonotone tr1; inversion_clear Heq200 in HgammaH; assumption.
apply (Value.getR_ab_correct V (Num.gamma N) (Ref.gamma R (Ref.context R tr2))).
inversion_clear Heq201 as [idHeq2011 Heq2010 Heq2011 ]; constructor 1 with idHeq2011; [assumption|apply Stack.top_ab_correct; inversion_clear Heq2010 as [idHeq20101 Heq20100 Heq20101 ]; constructor 1 with idHeq20101; [assumption|apply Stack.pop_ab_correct; inversion_clear Heq20100 as [idHeq201001 Heq201000 Heq201001 ]; constructor 1 with idHeq201001; [assumption|ApplyGammaMonotone tr1; inversion_clear Heq201000 in HgammaS; assumption]]].
apply Stack.top_ab_correct; inversion_clear Heq21 as [idHeq211 Heq210 Heq211 ]; constructor 1 with idHeq211; [assumption|ApplyGammaMonotone tr1; inversion_clear Heq210 in HgammaS; assumption].
apply Stack.pop_ab_correct; inversion_clear Seq as [idSeq1 Seq0 Seq1 ]; constructor 1 with idSeq1; [assumption|apply Stack.pop_ab_correct; inversion_clear Seq0 as [idSeq01 Seq00 Seq01 ]; constructor 1 with idSeq01; [assumption|ApplyGammaMonotone tr1; inversion_clear Seq00 in HgammaS; assumption]].
ApplyGammaMonotone tr1; inversion_clear Leq in HgammaL; assumption.
ApplyGammaMonotone tr1; inversion_clear Heq in HgammaH; assumption.
apply Stack.push_ab_correct; inversion_clear Seq as [idSeq1 idSeq2 Seq0 Seq1 Seq2 ]; constructor 1 with idSeq1 idSeq2; [assumption|apply Object.getf_ab_correct with P; inversion_clear Seq0 as [idSeq01 Seq00 Seq01 ]; constructor 1 with idSeq01; [assumption|apply Heap.geto_ab_correct with (Ref.gamma R (Ref.context R tr2)); inversion_clear Seq00 as [idSeq001 idSeq002 Seq000 Seq001 Seq002 ]; constructor 1 with idSeq001 idSeq002; [assumption|ApplyGammaMonotone tr1; inversion_clear Seq000 in HgammaH; assumption|apply Value.getR_ab_correct with (Num.gamma N) ; inversion_clear Seq001 as [idSeq0011 Seq0010 Seq0011 ]; constructor 1 with idSeq0011; [assumption|apply Stack.top_ab_correct; inversion_clear Seq0010 as [idSeq00101 Seq00100 Seq00101 ]; constructor 1 with idSeq00101; [assumption|ApplyGammaMonotone tr1; inversion_clear Seq00100 in HgammaS; assumption]]]]|apply Stack.pop_ab_correct; inversion_clear Seq1 as [idSeq11 Seq10 Seq11 ]; constructor 1 with idSeq11; [assumption|ApplyGammaMonotone tr1; inversion_clear Seq10 in HgammaS; assumption]].
ApplyGammaMonotone tr1; inversion_clear Leq in HgammaL; assumption.
ApplyGammaMonotone tr1; inversion_clear Heq in HgammaH; assumption.
ApplyGammaMonotone tr1; inversion_clear Seq in HgammaS; assumption.
ApplyGammaMonotone tr1; inversion_clear Leq in HgammaL; assumption.
Qed.
Lemma SmallStepSemTrace_SmallStepSem : forall r tr1 tr2,
SmallStepSemTrace P r tr1 tr2 ->
SmallStepSem P r (currentState tr1) (currentState tr2).
Proof.
intros.
inversion_clear H0; auto.
Qed.
Lemma SmallStepSemTrace_instructionAt : forall r tr1 tr2,
SmallStepSemTrace P r tr1 tr2 ->
instructionAt P (pcSt (currentState tr1)) = Some (rule2instr r).
Proof.
intros.
inversion_clear H0.
CaseEq (currentState tr1); intros h1 pc1 l1 s1 Heq.
rewrite Heq in H1; simpl in *; clear Heq.
inversion_clear H1; simpl; try assumption.
Qed.
Definition AbInit : AbMem :=
st (Heap.emptyHeap H) (Stack.nil_ab S) (LocalVar.initLocalVar L (Value.null_ab V)).
Lemma AbInit_correct : forall (tr:VTrace P) (st:State), (vtr P tr) = st ->
initial_State P st -> gammaMem AbInit tr.
Proof.
intros.
destruct st0 as [h pc l s].
constructor 1 with h l s pc; auto;
inversion_clear H1 in H0; unfold AbInit; simpl; subst; auto.
rewrite H0; reflexivity.
apply Heap.emptyHeap_correct; auto.
apply Stack.nil_ab_correct; auto.
apply LocalVar.initLocalVar_correct; auto.
apply Value.null_ab_correct.
Qed.
Inductive AbMemOrder : AbMem -> AbMem -> Prop :=
AbMemOrder_def : forall H1 H2 S1 S2 L1 L2,
order (Heap.Pos H) H1 H2 ->
order (Stack.Pos S) S1 S2 ->
order (LocalVar.Pos L) L1 L2 ->
AbMemOrder (st H1 S1 L1) (st H2 S2 L2).
Definition AbstractSemantic (ST:AbState) : Prop :=
AbMemOrder AbInit (ST Word_1) /\
forall pc r,
instructionAt P pc = Some (rule2instr r) ->
AbMemOrder (AbTransfMem r pc (ST pc))
(ST (AbTransPC r pc)).
Lemma AbTransf_correct : forall M r (tr1 tr2 : VTrace P),
SmallStepSemTrace P r tr1 tr2 ->
gammaMem M tr1 ->
gammaMem (AbTransfMem r (pcSt (currentState tr1)) M) tr2.
Proof.
intros M r tr1 tr2 HSemT.
generalize (SmallStepSemTrace_SmallStepSem r _ _ HSemT).
CaseEq (currentState tr1); intros h1 pc1 l1 s1 Hc1.
CaseEq (currentState tr2); intros h2 pc2 l2 s2 Hc2.
intros.
generalize (sem_func_correct _ _ _ _ H0); intros.
apply AbTransfMem_correct_aux with h1 l1 s1 h2 l2 s2 pc2 tr1; intuition.
apply (Ref.transfert_increase_context R) with r; auto.
apply (Ref.transfert_decrease_context R) with r; auto.
Qed.
Lemma AbTransfPC_correct : forall r tr1 tr2,
SmallStepSemTrace P r tr1 tr2 ->
pcSt (currentState tr2) = AbTransPC r (pcSt (currentState tr1)).
Proof.
intros.
inversion_clear H0.
CaseEq (currentState tr1); intros h1 pc1 l1 s1 Hc1.
rewrite Hc1 in H1; clear Hc1; simpl.
inversion_clear H1; simpl; auto.
Qed.
Lemma gammaMem_monotone : forall M1 M2,
AbMemOrder M1 M2 ->
(gammaMem M1) <=< (gammaMem M2).
Proof.
intros.
inversion_clear H0.
intros tr H6.
inversion_clear H6.
constructor 1 with h l s pc; auto.
apply (Gamma.gamma_monotone
(Heap.gamma H (Ref.gamma R (Ref.context R tr))
(Object.gamma O P
(Value.gamma V (Num.gamma N)
(Ref.gamma R (Ref.context R tr))))))
with (Hproj (st H1 S1 L1)); auto.
apply (Gamma.gamma_monotone
(Stack.gamma S
(Value.gamma V (Num.gamma N)
(Ref.gamma R (Ref.context R tr)))))
with (Sproj (st H1 S1 L1)); auto.
apply (Gamma.gamma_monotone
(LocalVar.gamma L
(Value.gamma V (Num.gamma N)
(Ref.gamma R (Ref.context R tr)))))
with (Lproj (st H1 S1 L1)); auto.
Qed.
Theorem AbstractSemantic_correct : forall ST (tr:VTrace P),
AbstractSemantic ST ->
SemCol P tr -> gammaSt ST tr.
Proof.
intros ST tr (H1,H2).
case tr; clear tr; intros t.
induction t; intros.
inversion_clear H0.
destruct s as [h pc l s].
constructor 1 with h l s pc; auto.
replace (ST pc) with (ST Word_1).
apply gammaMem_monotone with (1:= H1).
apply AbInit_correct with (2:= H3) ;auto.
inversion_clear H3; auto.
destruct s as [h pc l s].
constructor 1 with h l s pc; auto.
inversion_clear H0.
assert (SmallStepSemTrace P i t (t ::: << h, pc, l, s >>)).
constructor; simpl; auto.
generalize (SmallStepSemTrace_instructionAt _ _ _ H0); intros.
generalize (H2 _ _ H5); intros.
generalize (AbTransfPC_correct i _ _ H0); simpl; intros.
subst; apply gammaMem_monotone with (1:= H6).
replace (AbTransfMem i (pcSt (currentState t)) (ST (pcSt (currentState t))))
with (AbTransfMem i (pcSt (currentState (VTR P t H3))) (ST (pcSt (currentState (VTR P t H3))))).
apply AbTransf_correct; auto.
generalize (IHt H3 H3); intros.
unfold VTR.
inversion_clear H7.
rewrite H8; auto.
simpl; auto.
Qed.
End correct.
Index
This page has been generated by coqdoc