Library IAdd
Require Import Common.
Require Import Semantics.
Require Import ArithOps.
Require Import Relations.
Require Import List.
Require Import ZArith.
Declare Module SEM : SEMANTICS.
Module AllStr := SEM.M_AllStructures.
Module P := AllStr.M_Program.
Module PS := P.M_ProgramStructures.
Module VAT := PS.M_ValuesAndTypes.
Module RS := AllStr.M_RuntimeStructures.
Module SF := SEM.M_Sem_Frame.
Module SSOP := SF.M_Sem_Stackop.
Module ARS := AllStr.M_Arithmetics.
Module RSF := SF.M_AllStructures.M_RuntimeStructuresFacts.
Module H := RS.M_Heap.
Module HF := SF.M_AllStructures.M_HeapFacts.
Import VAT.
Import PS.
Import P.
Import RS.
Import ARS.
Import ArithmeticOperators.
Open Local Scope Z_scope.
Import ListNotations.
Load "Tactics.v".
Definition intArith := ARS.arithmeticForKind KInt.
Module AllStr := SEM.M_AllStructures.
Module P := AllStr.M_Program.
Module PS := P.M_ProgramStructures.
Module VAT := PS.M_ValuesAndTypes.
Module RS := AllStr.M_RuntimeStructures.
Module SF := SEM.M_Sem_Frame.
Module SSOP := SF.M_Sem_Stackop.
Module ARS := AllStr.M_Arithmetics.
Module RSF := SF.M_AllStructures.M_RuntimeStructuresFacts.
Module H := RS.M_Heap.
Module HF := SF.M_AllStructures.M_HeapFacts.
Import VAT.
Import PS.
Import P.
Import RS.
Import ARS.
Import ArithmeticOperators.
Open Local Scope Z_scope.
Import ListNotations.
Load "Tactics.v".
Definition intArith := ARS.arithmeticForKind KInt.
Definitions specific to this example
Most of the things analysed in this example (program or JVM fragments) are defined direclty.Program
The program to be analysed and auxiliary definitionsDefinition ntwo := M_Numeric_Int.const 2.
Definition nfour := M_Numeric_Int.const 4.
Definition vtwo := VInt ntwo.
Definition vfour := VInt nfour.
Definition code: TCode := codeFromList [
I_Frame (FI_Stackop (SI_Const KInt (vtwo)));
I_Frame (FI_Stackop (SI_Generic Op_dup));
I_Frame (FI_Stackop (SI_Binop KInt ArithmeticOperators.BinOp_add))
].
Parameter method_name: TQualifiedMethodName.
Parameter c: TClassName.
Parameter p: TProgram.
Axiom ThisMethod: getMethodBodyFromProgram p method_name = Some code.
States
Subsequent program execution states at different levels of complexity (different JVM runtime structures).- Directly -- we give examples of actual states that may occur as program initial, intermediate, and final states. These definitions are used in proofs in "existential" form (described later).
- By description -- we give specifications of the states. Theoretically, more than one state instance can fulfill a specification. These specifications are used in proofs in "general implication" form (described later).
Parameter heap: H.THeap.
Parameter thid0: H.TThreadId.
Parameter caller_loc: TLoc.
Axiom caller_loc_class_loc: H.getClassObjectLoc heap c = Some caller_loc.
Parameter thid0: H.TThreadId.
Parameter caller_loc: TLoc.
Axiom caller_loc_class_loc: H.getClassObjectLoc heap c = Some caller_loc.
Subsequent program counters.
Definition pc0 := pcFromPosition 0%nat.
Definition pc1 := pcFromPosition 1%nat.
Definition pc2 := pcFromPosition 2%nat.
Definition pc3 := pcFromPosition 3%nat.
Definition pc1 := pcFromPosition 1%nat.
Definition pc2 := pcFromPosition 2%nat.
Definition pc3 := pcFromPosition 3%nat.
Subsequent states at the level of frames.
Definition frame0 := frameMake varsEmpty [] pc0.
Definition frame1 := frameMake varsEmpty [vtwo] pc1.
Definition frame2 := frameMake varsEmpty [vtwo;vtwo] pc2.
Definition frame3 := frameMake varsEmpty [vfour] pc3.
Definition frame1 := frameMake varsEmpty [vtwo] pc1.
Definition frame2 := frameMake varsEmpty [vtwo;vtwo] pc2.
Definition frame3 := frameMake varsEmpty [vfour] pc3.
The same states described generally in specification style.
Definition frame0_props (f: TFrame) :=
frameGetPC f = pc0
∧ frameGetLocalStack f = [].
Definition frame1_props (f: TFrame) :=
∃ x,
frameGetPC f = pc1
∧ frameGetLocalStack f = [VInt x]
∧ M_Numeric_Int.toZ x = 2.
Definition frame2_props (f: TFrame) :=
∃ x y,
frameGetPC f = pc2
∧ frameGetLocalStack f = [VInt y; VInt x]
∧ M_Numeric_Int.toZ x = 2
∧ M_Numeric_Int.toZ y = 2.
Definition frame3_props (f: TFrame) :=
∃ z,
frameGetPC f = pc3
∧ frameGetLocalStack f = [VInt z]
∧ M_Numeric_Int.toZ z = 4.
frameGetPC f = pc0
∧ frameGetLocalStack f = [].
Definition frame1_props (f: TFrame) :=
∃ x,
frameGetPC f = pc1
∧ frameGetLocalStack f = [VInt x]
∧ M_Numeric_Int.toZ x = 2.
Definition frame2_props (f: TFrame) :=
∃ x y,
frameGetPC f = pc2
∧ frameGetLocalStack f = [VInt y; VInt x]
∧ M_Numeric_Int.toZ x = 2
∧ M_Numeric_Int.toZ y = 2.
Definition frame3_props (f: TFrame) :=
∃ z,
frameGetPC f = pc3
∧ frameGetLocalStack f = [VInt z]
∧ M_Numeric_Int.toZ z = 4.
TCurrentMethod structure stored on the call stack.
Subsequent states at the level of threads.
Definition thstate0 := threadMake thid0 null [(cm,frame0)].
Definition thstate1 := threadMake thid0 null [(cm,frame1)].
Definition thstate2 := threadMake thid0 null [(cm,frame2)].
Definition thstate3 := threadMake thid0 null [(cm,frame3)].
Definition thstate1 := threadMake thid0 null [(cm,frame1)].
Definition thstate2 := threadMake thid0 null [(cm,frame2)].
Definition thstate3 := threadMake thid0 null [(cm,frame3)].
The same states described generally in specification style.
Definition thstate0_props (th: TThread) :=
∃ f,
threadGetId th = thid0
∧ threadGetEvalState th = null
∧ threadGetCallStack th = [(cm, f)]
∧ frame0_props f.
Definition thstate1_props (th: TThread) :=
∃ f,
threadGetId th = thid0
∧ threadGetEvalState th = null
∧ threadGetCallStack th = [(cm, f)]
∧ frame1_props f.
Definition thstate2_props (th: TThread) :=
∃ f,
threadGetId th = thid0
∧ threadGetEvalState th = null
∧ threadGetCallStack th = [(cm, f)]
∧ frame2_props f.
Definition thstate3_props (th: TThread) :=
∃ f,
threadGetId th = thid0
∧ threadGetEvalState th = null
∧ threadGetCallStack th = [(cm, f)]
∧ frame3_props f.
∃ f,
threadGetId th = thid0
∧ threadGetEvalState th = null
∧ threadGetCallStack th = [(cm, f)]
∧ frame0_props f.
Definition thstate1_props (th: TThread) :=
∃ f,
threadGetId th = thid0
∧ threadGetEvalState th = null
∧ threadGetCallStack th = [(cm, f)]
∧ frame1_props f.
Definition thstate2_props (th: TThread) :=
∃ f,
threadGetId th = thid0
∧ threadGetEvalState th = null
∧ threadGetCallStack th = [(cm, f)]
∧ frame2_props f.
Definition thstate3_props (th: TThread) :=
∃ f,
threadGetId th = thid0
∧ threadGetEvalState th = null
∧ threadGetCallStack th = [(cm, f)]
∧ frame3_props f.
Subsequent states at the level of whole JVM states.
Definition jvm0 := jvmMake heap [thstate0].
Definition jvm1 := jvmMake heap [thstate1].
Definition jvm2 := jvmMake heap [thstate2].
Definition jvm3 := jvmMake heap [thstate3].
Definition jvm1 := jvmMake heap [thstate1].
Definition jvm2 := jvmMake heap [thstate2].
Definition jvm3 := jvmMake heap [thstate3].
The same states described generally in specification style.
Definition jvm0_props (jvm: TJVM) :=
∃ th,
jvmGetHeap jvm = heap
∧ jvmGetThreads jvm = [th]
∧ thstate0_props th.
Definition jvm1_props (jvm: TJVM) :=
∃ th,
jvmGetHeap jvm = heap
∧ jvmGetThreads jvm = [th]
∧ thstate1_props th.
Definition jvm2_props (jvm: TJVM) :=
∃ th,
jvmGetHeap jvm = heap
∧ jvmGetThreads jvm = [th]
∧ thstate2_props th.
Definition jvm3_props (jvm: TJVM) :=
∃ th,
jvmGetHeap jvm = heap
∧ jvmGetThreads jvm = [th]
∧ thstate3_props th.
∃ th,
jvmGetHeap jvm = heap
∧ jvmGetThreads jvm = [th]
∧ thstate0_props th.
Definition jvm1_props (jvm: TJVM) :=
∃ th,
jvmGetHeap jvm = heap
∧ jvmGetThreads jvm = [th]
∧ thstate1_props th.
Definition jvm2_props (jvm: TJVM) :=
∃ th,
jvmGetHeap jvm = heap
∧ jvmGetThreads jvm = [th]
∧ thstate2_props th.
Definition jvm3_props (jvm: TJVM) :=
∃ th,
jvmGetHeap jvm = heap
∧ jvmGetThreads jvm = [th]
∧ thstate3_props th.
2+2 example -- proofs
Auxiliary lemmas and definitions
Basic arithmetic properties
Lemma small_2: M_Numeric_Int.range 2.
Proof.
prove_range_int.
Qed.
Lemma small_4: M_Numeric_Int.range 4.
Proof.
prove_range_int.
Qed.
Proof.
prove_range_int.
Qed.
Lemma small_4: M_Numeric_Int.range 4.
Proof.
prove_range_int.
Qed.
Z value of our constants available as a single equality.
Lemma toZ2: M_Numeric_Int.toZ ntwo = 2.
Proof.
apply M_Numeric_Int.const_prop.
apply small_2.
Qed.
Lemma toZ4: M_Numeric_Int.toZ nfour = 4.
Proof.
apply M_Numeric_Int.const_prop.
apply small_4.
Qed.
Proof.
apply M_Numeric_Int.const_prop.
apply small_2.
Qed.
Lemma toZ4: M_Numeric_Int.toZ nfour = 4.
Proof.
apply M_Numeric_Int.const_prop.
apply small_4.
Qed.
Result of 2+2 has the desired value - specified in implication style,
using toZ values for comparison.
Lemma num_224_impl_toZ: ∀ arg1 arg2,
M_Numeric_Int.toZ arg1 = 2 →
M_Numeric_Int.toZ arg2 = 2 →
M_Numeric_Int.toZ (M_Numeric_Int.add arg1 arg2) = 4.
Proof.
intros.
rewrite M_Numeric_Int.add_prop.
rewrite H; clear H; rewrite H0; clear H0.
simpl.
auto.
Qed.
M_Numeric_Int.toZ arg1 = 2 →
M_Numeric_Int.toZ arg2 = 2 →
M_Numeric_Int.toZ (M_Numeric_Int.add arg1 arg2) = 4.
Proof.
intros.
rewrite M_Numeric_Int.add_prop.
rewrite H; clear H; rewrite H0; clear H0.
simpl.
auto.
Qed.
Result of 2+2 has the desired value - specified as one equality,
explicitly for our constants.
Lemma num_224_toZ: M_Numeric_Int.toZ (M_Numeric_Int.add ntwo ntwo) = 4.
Proof.
apply num_224_impl_toZ;
apply toZ2.
Qed.
Proof.
apply num_224_impl_toZ;
apply toZ2.
Qed.
Result of 2+2 has the desired value - specified as one equality,
explicitly for our constants. It holds only with PToZDistinct axiom present.
Lemma num_224_const: M_Numeric_Int.add ntwo ntwo = nfour.
Proof.
apply M_Numeric_Int.PToZDistinct.
rewrite toZ4.
apply num_224_toZ.
Qed.
Proof.
apply M_Numeric_Int.PToZDistinct.
rewrite toZ4.
apply num_224_toZ.
Qed.
Note: This is not true in Numeric
M_Numeric_Int.add ntwo ntwo = nfour.
Frame level
Consistency of state definition
Our example state instances fulfill the assumed specification.
Lemma frame0_ok: frame0_props frame0.
Proof.
unfold frame0_props.
unfold frame0.
simpl.
intuition reflexivity.
Qed.
Lemma frame1_ok: frame1_props frame1.
Proof.
unfold frame1_props.
unfold frame1.
∃ ntwo.
simpl.
rewrite toZ2.
intuition reflexivity.
Qed.
Lemma frame2_ok: frame2_props frame2.
Proof.
unfold frame2_props.
unfold frame2.
∃ ntwo.
∃ ntwo.
simpl.
rewrite toZ2.
intuition reflexivity.
Qed.
Lemma frame3_ok: frame3_props frame3.
Proof.
unfold frame3_props.
unfold frame3.
∃ nfour.
simpl.
rewrite toZ4.
intuition reflexivity.
Qed.
Proof.
unfold frame0_props.
unfold frame0.
simpl.
intuition reflexivity.
Qed.
Lemma frame1_ok: frame1_props frame1.
Proof.
unfold frame1_props.
unfold frame1.
∃ ntwo.
simpl.
rewrite toZ2.
intuition reflexivity.
Qed.
Lemma frame2_ok: frame2_props frame2.
Proof.
unfold frame2_props.
unfold frame2.
∃ ntwo.
∃ ntwo.
simpl.
rewrite toZ2.
intuition reflexivity.
Qed.
Lemma frame3_ok: frame3_props frame3.
Proof.
unfold frame3_props.
unfold frame3.
∃ nfour.
simpl.
rewrite toZ4.
intuition reflexivity.
Qed.
Thread level
Lemma thread0_ok: thstate0_props thstate0.
Proof.
unfold thstate0_props.
unfold thstate0.
simpl.
∃ frame0.
auto using frame0_ok.
Qed.
Lemma thread1_ok: thstate1_props thstate1.
Proof.
unfold thstate1_props.
unfold thstate1.
simpl.
∃ frame1.
auto using frame1_ok.
Qed.
Lemma thread2_ok: thstate2_props thstate2.
Proof.
unfold thstate2_props.
unfold thstate2.
simpl.
∃ frame2.
auto using frame2_ok.
Qed.
Lemma thread3_ok: thstate3_props thstate3.
Proof.
unfold thstate3_props.
unfold thstate3.
simpl.
∃ frame3.
auto using frame3_ok.
Qed.
Proof.
unfold thstate0_props.
unfold thstate0.
simpl.
∃ frame0.
auto using frame0_ok.
Qed.
Lemma thread1_ok: thstate1_props thstate1.
Proof.
unfold thstate1_props.
unfold thstate1.
simpl.
∃ frame1.
auto using frame1_ok.
Qed.
Lemma thread2_ok: thstate2_props thstate2.
Proof.
unfold thstate2_props.
unfold thstate2.
simpl.
∃ frame2.
auto using frame2_ok.
Qed.
Lemma thread3_ok: thstate3_props thstate3.
Proof.
unfold thstate3_props.
unfold thstate3.
simpl.
∃ frame3.
auto using frame3_ok.
Qed.
JVM level
Lemma jvm0_ok: jvm0_props jvm0.
Proof.
unfold jvm0_props.
unfold jvm0.
simpl.
∃ thstate0.
auto using thread0_ok.
Qed.
Lemma jvm1_ok: jvm1_props jvm1.
Proof.
unfold jvm1_props.
unfold jvm1.
simpl.
∃ thstate1.
auto using thread1_ok.
Qed.
Lemma jvm2_ok: jvm2_props jvm2.
Proof.
unfold jvm2_props.
unfold jvm2.
simpl.
∃ thstate2.
auto using thread2_ok.
Qed.
Lemma jvm3_ok: jvm3_props jvm3.
Proof.
unfold jvm3_props.
unfold jvm3.
simpl.
∃ thstate3.
auto using thread3_ok.
Qed.
Proof.
unfold jvm0_props.
unfold jvm0.
simpl.
∃ thstate0.
auto using thread0_ok.
Qed.
Lemma jvm1_ok: jvm1_props jvm1.
Proof.
unfold jvm1_props.
unfold jvm1.
simpl.
∃ thstate1.
auto using thread1_ok.
Qed.
Lemma jvm2_ok: jvm2_props jvm2.
Proof.
unfold jvm2_props.
unfold jvm2.
simpl.
∃ thstate2.
auto using thread2_ok.
Qed.
Lemma jvm3_ok: jvm3_props jvm3.
Proof.
unfold jvm3_props.
unfold jvm3.
simpl.
∃ thstate3.
auto using thread3_ok.
Qed.
Lemma pc0_next: next code pc0 = pc1.
Proof.
apply PcodeFromList_next_pc.
Qed.
Lemma pc1_next: next code pc1 = pc2.
Proof.
apply PcodeFromList_next_pc.
Qed.
Lemma pc2_next: next code pc2 = pc3.
Proof.
apply PcodeFromList_next_pc.
Qed.
Proof.
apply PcodeFromList_next_pc.
Qed.
Lemma pc1_next: next code pc1 = pc2.
Proof.
apply PcodeFromList_next_pc.
Qed.
Lemma pc2_next: next code pc2 = pc3.
Proof.
apply PcodeFromList_next_pc.
Qed.
Direct formulation of the PC value in subsequent states.
Lemma getPC_isPC0: ∀ fr,
frame0_props fr → frameGetPC fr = pc0.
Proof.
unfold frame0_props.
tauto.
Qed.
Lemma getPC_isPC1: ∀ fr,
frame1_props fr → frameGetPC fr = pc1.
Proof.
intros.
destruct H as [x H].
tauto.
Qed.
Lemma getPC_isPC2: ∀ fr,
frame2_props fr → frameGetPC fr = pc2.
Proof.
intros.
destruct H as [x H].
destruct H as [y H].
tauto.
Qed.
Lemma getPC_isPC3: ∀ fr,
frame3_props fr → frameGetPC fr = pc3.
Proof.
intros.
destruct H as [x H].
tauto.
Qed.
Lemma pc0_neq_pc3: pc0 ≠ pc3.
Proof.
unfold pc0, pc3.
intro.
f_equal_H H pcToPosition.
rewrite PpositionPc in H0.
rewrite PpositionPc in H0.
discriminate H0.
Qed.
Lemma pc1_neq_pc3: pc1 ≠ pc3.
Proof.
unfold pc1, pc3.
intro.
f_equal_H H pcToPosition.
rewrite PpositionPc in H0.
rewrite PpositionPc in H0.
discriminate H0.
Qed.
Lemma pc2_neq_pc3: pc2 ≠ pc3.
Proof.
unfold pc2, pc3.
intro.
f_equal_H H pcToPosition.
rewrite PpositionPc in H0.
rewrite PpositionPc in H0.
discriminate H0.
Qed.
frame0_props fr → frameGetPC fr = pc0.
Proof.
unfold frame0_props.
tauto.
Qed.
Lemma getPC_isPC1: ∀ fr,
frame1_props fr → frameGetPC fr = pc1.
Proof.
intros.
destruct H as [x H].
tauto.
Qed.
Lemma getPC_isPC2: ∀ fr,
frame2_props fr → frameGetPC fr = pc2.
Proof.
intros.
destruct H as [x H].
destruct H as [y H].
tauto.
Qed.
Lemma getPC_isPC3: ∀ fr,
frame3_props fr → frameGetPC fr = pc3.
Proof.
intros.
destruct H as [x H].
tauto.
Qed.
Lemma pc0_neq_pc3: pc0 ≠ pc3.
Proof.
unfold pc0, pc3.
intro.
f_equal_H H pcToPosition.
rewrite PpositionPc in H0.
rewrite PpositionPc in H0.
discriminate H0.
Qed.
Lemma pc1_neq_pc3: pc1 ≠ pc3.
Proof.
unfold pc1, pc3.
intro.
f_equal_H H pcToPosition.
rewrite PpositionPc in H0.
rewrite PpositionPc in H0.
discriminate H0.
Qed.
Lemma pc2_neq_pc3: pc2 ≠ pc3.
Proof.
unfold pc2, pc3.
intro.
f_equal_H H pcToPosition.
rewrite PpositionPc in H0.
rewrite PpositionPc in H0.
discriminate H0.
Qed.
Method pointed by the given expression is our example method.
Lemma ThisMethodCM: getMethodBodyFromProgram p (cmQName cm) = Some code.
Proof.
unfold cm.
simpl.
exact ThisMethod.
Qed.
Proof.
unfold cm.
simpl.
exact ThisMethod.
Qed.
Lemmas helpful in getting the current instruction in subsequent steps.
Lemma Instruction0: getInstruction code pc0 = Some (I_Frame (FI_Stackop (SI_Const KInt (vtwo)))).
Proof.
unfold code.
unfold pc0.
rewrite PgetInstructionIffNth.
rewrite PpositionPc.
simpl.
reflexivity.
Qed.
Lemma Instruction1: getInstruction code pc1 = Some (I_Frame (FI_Stackop (SI_Generic Op_dup))).
Proof.
unfold code.
unfold pc1.
rewrite PgetInstructionIffNth.
rewrite PpositionPc.
simpl.
reflexivity.
Qed.
Lemma Instruction2: getInstruction code pc2 = Some (I_Frame (FI_Stackop (SI_Binop KInt ArithmeticOperators.BinOp_add))).
Proof.
unfold code.
unfold pc2.
rewrite PgetInstructionIffNth.
rewrite PpositionPc.
simpl.
reflexivity.
Qed.
Lemma Instruction3: getInstruction code pc3 = None.
Proof.
unfold code.
unfold pc3.
rewrite PgetInstructionIffNth.
rewrite PpositionPc.
simpl.
reflexivity.
Qed.
Ltac ThisMethodRewrite :=
match goal with
| Heq: getMethodBodyFromProgram p (cmQName cm) = Some ?code' |- _ ⇒
rewrite ThisMethodCM in Heq;
injection Heq; intros; clear Heq; subst code'
| _ ⇒ idtac
end.
Ltac InstructionRewrite getPC :=
match goal with
| Hprops: frame0_props ?fr,
Heq: getInstruction code (frameGetPC ?fr) = Some ?instr' |- _ ⇒
rewrite (getPC fr Hprops) in Heq;
rewrite Instruction0 in Heq;
simplify_eq Heq; intros; clear Heq; try subst instr'
| _ ⇒ idtac
end.
Ltac Instruction0Rewrite :=
match goal with
| Hprops: frame0_props ?fr,
Heq: getInstruction code (frameGetPC ?fr) = Some ?instr' |- _ ⇒
rewrite (getPC_isPC0 fr Hprops) in Heq;
rewrite Instruction0 in Heq;
simplify_eq Heq; intros; clear Heq; try subst instr'
| _ ⇒ idtac
end.
Ltac Instruction1Rewrite :=
match goal with
| Hprops: frame1_props ?fr,
Heq: getInstruction code (frameGetPC ?fr) = Some ?instr' |- _ ⇒
rewrite (getPC_isPC1 fr Hprops) in Heq;
rewrite Instruction1 in Heq;
simplify_eq Heq; intros; clear Heq; try subst instr'
| _ ⇒ idtac
end.
Ltac Instruction2Rewrite :=
match goal with
| Hprops: frame2_props ?fr,
Heq: getInstruction code (frameGetPC ?fr) = Some ?instr' |- _ ⇒
rewrite (getPC_isPC2 fr Hprops) in Heq;
rewrite Instruction2 in Heq;
simplify_eq Heq; intros; clear Heq; try subst instr'
| _ ⇒ idtac
end.
Ltac Instruction3Rewrite :=
match goal with
| Hprops: frame3_props ?fr,
Heq: getInstruction code (frameGetPC ?fr) = Some ?instr' |- _ ⇒
rewrite (getPC_isPC3 fr Hprops) in Heq;
rewrite Instruction3 in Heq;
simplify_eq Heq; intros; clear Heq; try subst instr'
| _ ⇒ fail
end.
Proof.
unfold code.
unfold pc0.
rewrite PgetInstructionIffNth.
rewrite PpositionPc.
simpl.
reflexivity.
Qed.
Lemma Instruction1: getInstruction code pc1 = Some (I_Frame (FI_Stackop (SI_Generic Op_dup))).
Proof.
unfold code.
unfold pc1.
rewrite PgetInstructionIffNth.
rewrite PpositionPc.
simpl.
reflexivity.
Qed.
Lemma Instruction2: getInstruction code pc2 = Some (I_Frame (FI_Stackop (SI_Binop KInt ArithmeticOperators.BinOp_add))).
Proof.
unfold code.
unfold pc2.
rewrite PgetInstructionIffNth.
rewrite PpositionPc.
simpl.
reflexivity.
Qed.
Lemma Instruction3: getInstruction code pc3 = None.
Proof.
unfold code.
unfold pc3.
rewrite PgetInstructionIffNth.
rewrite PpositionPc.
simpl.
reflexivity.
Qed.
Ltac ThisMethodRewrite :=
match goal with
| Heq: getMethodBodyFromProgram p (cmQName cm) = Some ?code' |- _ ⇒
rewrite ThisMethodCM in Heq;
injection Heq; intros; clear Heq; subst code'
| _ ⇒ idtac
end.
Ltac InstructionRewrite getPC :=
match goal with
| Hprops: frame0_props ?fr,
Heq: getInstruction code (frameGetPC ?fr) = Some ?instr' |- _ ⇒
rewrite (getPC fr Hprops) in Heq;
rewrite Instruction0 in Heq;
simplify_eq Heq; intros; clear Heq; try subst instr'
| _ ⇒ idtac
end.
Ltac Instruction0Rewrite :=
match goal with
| Hprops: frame0_props ?fr,
Heq: getInstruction code (frameGetPC ?fr) = Some ?instr' |- _ ⇒
rewrite (getPC_isPC0 fr Hprops) in Heq;
rewrite Instruction0 in Heq;
simplify_eq Heq; intros; clear Heq; try subst instr'
| _ ⇒ idtac
end.
Ltac Instruction1Rewrite :=
match goal with
| Hprops: frame1_props ?fr,
Heq: getInstruction code (frameGetPC ?fr) = Some ?instr' |- _ ⇒
rewrite (getPC_isPC1 fr Hprops) in Heq;
rewrite Instruction1 in Heq;
simplify_eq Heq; intros; clear Heq; try subst instr'
| _ ⇒ idtac
end.
Ltac Instruction2Rewrite :=
match goal with
| Hprops: frame2_props ?fr,
Heq: getInstruction code (frameGetPC ?fr) = Some ?instr' |- _ ⇒
rewrite (getPC_isPC2 fr Hprops) in Heq;
rewrite Instruction2 in Heq;
simplify_eq Heq; intros; clear Heq; try subst instr'
| _ ⇒ idtac
end.
Ltac Instruction3Rewrite :=
match goal with
| Hprops: frame3_props ?fr,
Heq: getInstruction code (frameGetPC ?fr) = Some ?instr' |- _ ⇒
rewrite (getPC_isPC3 fr Hprops) in Heq;
rewrite Instruction3 in Heq;
simplify_eq Heq; intros; clear Heq; try subst instr'
| _ ⇒ fail
end.
State transitions
Transitions between states descibed at different levels of JVM structures.- "existential" -- we prove that a transition (semantics step) holds between two particular states, our example ones; this kind of property corresponds to total correcntess of program.
- "general" -- we prove that for all states s1 consistent with the specification p1 if a transision is possible that results in state s2, then s2 must fulfill specification p2 (p1 and p2 being appropriate specifications from ..._props introduced above); this kind of properties corresponds to partial correctness of program.
Arithmetic level (binop semantcs)
Properties in existential form
Lemma binop_224: M_ArithmeticTypes.arithBinOp intArith BinOp_add vtwo vtwo (Some vfour).
Proof.
simpl.
unfold vtwo, vfour.
rewrite <- num_224_const.
constructor.
Qed.
Proof.
simpl.
unfold vtwo, vfour.
rewrite <- num_224_const.
constructor.
Qed.
Lemma binop_224_impl_toZ: ∀ arg1 arg2 result,
M_Numeric_Int.toZ arg1 = 2 →
M_Numeric_Int.toZ arg2 = 2 →
M_ArithmeticTypes.arithBinOp intArith BinOp_add (VInt arg1) (VInt arg2) result →
∃ val,
result = Some (VInt val) ∧ M_Numeric_Int.toZ val = 4.
Proof.
intros.
inversion H1; clear H1; subst.
∃ (M_Numeric_Int.add arg1 arg2).
split.
f_equal.
apply num_224_impl_toZ;
assumption.
Qed.
M_Numeric_Int.toZ arg1 = 2 →
M_Numeric_Int.toZ arg2 = 2 →
M_ArithmeticTypes.arithBinOp intArith BinOp_add (VInt arg1) (VInt arg2) result →
∃ val,
result = Some (VInt val) ∧ M_Numeric_Int.toZ val = 4.
Proof.
intros.
inversion H1; clear H1; subst.
∃ (M_Numeric_Int.add arg1 arg2).
split.
f_equal.
apply num_224_impl_toZ;
assumption.
Qed.
Lemma stackop_0_1: SSOP.semStack (SI_Const KInt (vtwo))
[] (Result [vtwo]).
Proof.
constructor.
simpl.
reflexivity.
Qed.
Lemma stackop_1_2: SSOP.semStack (SI_Generic Op_dup)
[vtwo] (Result [vtwo;vtwo]).
Proof.
set (f := fun (i: nat) ⇒ vtwo).
replace [vtwo;vtwo] with (map f [0;0]%nat).
2:simpl; reflexivity.
replace [vtwo] with (map f [0]%nat).
2:simpl; reflexivity.
econstructor.
econstructor.
simpl.
intros.
apply Pnth_error_in in H.
apply in_inv in H.
decompose [or] H.
subst.
constructor.
inversion H0.
Qed.
Lemma stackop_2_3: SSOP.semStack (SI_Binop KInt ArithmeticOperators.BinOp_add)
[vtwo;vtwo] (Result [vfour]).
Proof.
constructor.
apply binop_224.
Qed.
Lemma stackop_0_1_impl: ∀ result,
SSOP.semStack (SI_Const KInt (vtwo)) [] result →
∃ val, result = Result [VInt val]
∧ M_Numeric_Int.toZ val = 2.
Proof.
intros.
inversion H; clear H; subst.
∃ ntwo.
split.
f_equal; f_equal.
exact toZ2.
Qed.
Lemma stackop_1_2_impl: ∀ arg result,
M_Numeric_Int.toZ arg = 2 →
SSOP.semStack (SI_Generic Op_dup) [VInt arg] result →
∃ val1 val2, result = Result [VInt val2;VInt val1]
∧ M_Numeric_Int.toZ val1 = 2
∧ M_Numeric_Int.toZ val2 = 2.
Proof.
intros.
inversion H0; clear H0; subst.
inversion H3; clear H3; subst.
∃ arg.
∃ arg.
simpl in ×.
injection H2; clear H2; intro H2.
rewrite H2; clear H2.
repeat split.
assumption.
assumption.
Qed.
Lemma stackop_2_3_impl: ∀ arg1 arg2 result,
M_Numeric_Int.toZ arg1 = 2 →
M_Numeric_Int.toZ arg2 = 2 →
SSOP.semStack (SI_Binop KInt ArithmeticOperators.BinOp_add) [VInt arg2; VInt arg1] result →
∃ val, result = Result [VInt val]
∧ M_Numeric_Int.toZ val = 4.
Proof.
intros.
inversion H1; clear H1; subst.
destruct (binop_224_impl_toZ _ _ _ H H0 H7) as [val Hbinop].
clear H H0 H7.
decompose [and] Hbinop; clear Hbinop.
injection H; clear H; intro H.
∃ val.
split.
f_equal; f_equal.
assumption.
assumption.
destruct (binop_224_impl_toZ _ _ _ H H0 H7) as [val Hbinop].
clear H H0 H7.
decompose [and] Hbinop; clear Hbinop.
discriminate H.
Qed.
Even more general formalisation of the property.
Lemma stackop_2_3_impl_gen: ∀ arg1 arg2 vs1 result,
vs1 = [VInt arg2; VInt arg1] →
M_Numeric_Int.toZ arg1 = 2 →
M_Numeric_Int.toZ arg2 = 2 →
SSOP.semStack (SI_Binop KInt ArithmeticOperators.BinOp_add) vs1 result →
∃ val, result = Result [VInt val]
∧ M_Numeric_Int.toZ val = 4.
Proof.
intros.
subst vs1.
inversion H2; clear H2; subst.
destruct (binop_224_impl_toZ _ _ _ H0 H1 H7) as [val Hbinop].
clear H0 H1 H7.
decompose [and] Hbinop; clear Hbinop.
injection H; clear H; intro H.
∃ val.
split.
f_equal; f_equal.
assumption.
assumption.
destruct (binop_224_impl_toZ _ _ _ H0 H1 H7) as [val Hbinop].
clear H0 H1 H7.
decompose [and] Hbinop; clear Hbinop.
discriminate H.
Qed.
vs1 = [VInt arg2; VInt arg1] →
M_Numeric_Int.toZ arg1 = 2 →
M_Numeric_Int.toZ arg2 = 2 →
SSOP.semStack (SI_Binop KInt ArithmeticOperators.BinOp_add) vs1 result →
∃ val, result = Result [VInt val]
∧ M_Numeric_Int.toZ val = 4.
Proof.
intros.
subst vs1.
inversion H2; clear H2; subst.
destruct (binop_224_impl_toZ _ _ _ H0 H1 H7) as [val Hbinop].
clear H0 H1 H7.
decompose [and] Hbinop; clear Hbinop.
injection H; clear H; intro H.
∃ val.
split.
f_equal; f_equal.
assumption.
assumption.
destruct (binop_224_impl_toZ _ _ _ H0 H1 H7) as [val Hbinop].
clear H0 H1 H7.
decompose [and] Hbinop; clear Hbinop.
discriminate H.
Qed.
Lemma frame_0_1: SF.semFrame code (FI_Stackop (SI_Const KInt (vtwo)))
frame0 (Result frame1).
Proof.
econstructor.
eapply stackop_0_1.
apply RSF.PstackTopValuesSame.
symmetry.
apply PcodeFromList_next_pc.
Qed.
Lemma frame_1_2: SF.semFrame code (FI_Stackop (SI_Generic Op_dup))
frame1 (Result frame2).
Proof.
econstructor.
eapply stackop_1_2.
apply RSF.PstackTopValuesSame.
symmetry.
apply PcodeFromList_next_pc.
Qed.
Lemma frame_2_3: SF.semFrame code (FI_Stackop (SI_Binop KInt ArithmeticOperators.BinOp_add))
frame2 (Result frame3).
Proof.
econstructor.
eapply stackop_2_3.
apply RSF.PstackTopValuesSame.
symmetry.
apply PcodeFromList_next_pc.
Qed.
Lemma stepFrame_0_1: SF.stepFrame code frame0 frame1.
Proof.
econstructor.
apply Instruction0.
apply frame_0_1.
Qed.
Lemma stepFrame_1_2: SF.stepFrame code frame1 frame2.
Proof.
econstructor.
apply Instruction1.
apply frame_1_2.
Qed.
Lemma stepFrame_2_3: SF.stepFrame code frame2 frame3.
Proof.
econstructor.
apply Instruction2.
apply frame_2_3.
Qed.
Properties in general "implication" form
Lemma stackop_binop_inversion: ∀ k vs1 result,
SSOP.semStack (SI_Binop k ArithmeticOperators.BinOp_add) vs1 result →
∃ arg1 arg2,
vs1 = [arg2; arg1].
Proof.
intros.
inversion H; clear H; subst.
∃ arg1.
∃ arg2.
reflexivity.
∃ arg1.
∃ arg2.
reflexivity.
Qed.
SSOP.semStack (SI_Binop k ArithmeticOperators.BinOp_add) vs1 result →
∃ arg1 arg2,
vs1 = [arg2; arg1].
Proof.
intros.
inversion H; clear H; subst.
∃ arg1.
∃ arg2.
reflexivity.
∃ arg1.
∃ arg2.
reflexivity.
Qed.
The same for dup.
Lemma stackop_dup_inversion: ∀ vs1 result,
SSOP.semStack (SI_Generic Op_dup) vs1 result →
∃ arg,
vs1 = [arg].
Proof.
intros.
inversion H; clear H; subst.
inversion H1; clear H1; subst.
∃ (fv 0%nat).
simpl.
reflexivity.
Qed.
Lemma frame_0_1_impl: ∀ f0 result,
frame0_props f0 →
SF.semFrame code (FI_Stackop (SI_Const KInt (vtwo))) f0 result →
∃ f1, result = Result f1 ∧ frame1_props f1.
Proof.
intros.
unfold frame0_props in H.
decompose [and] H; clear H.
inversion H0; clear H0; subst;
simpl in *;
subst.
set (Hprefix := RSF.PstackTopValues_implies_prefix_l _ _ _ _ H4).
apply RSF.PprefixNilImpliesNil in Hprefix.
subst vs.
RSF.destructStackTopValues H4.
subst.
eapply stackop_0_1_impl in H3.
destruct H3 as [val H3].
decompose [and] H3; clear H3.
injection H; clear H; intro H; subst.
∃ (frameMake vars [VInt val] (next code pc0)).
split.
reflexivity.
∃ val.
simpl.
repeat split.
apply pc0_next.
assumption.
apply RSF.PprefixNilImpliesNil in H4.
subst vs.
eapply stackop_0_1_impl in H3.
destruct H3 as [val H3].
decompose [and] H3; clear H3.
discriminate H.
Qed.
Lemma frame_1_2_impl: ∀ f1 result,
frame1_props f1 →
SF.semFrame code (FI_Stackop (SI_Generic Op_dup)) f1 result →
∃ f2, result = Result f2 ∧ frame2_props f2.
Proof.
intros.
destruct H as [x H].
decompose [and] H; clear H.
inversion H0; clear H0; subst;
simpl in *;
subst.
assert (Hvs1 := stackop_dup_inversion _ _ H2).
destruct Hvs1 as [arg Hvs1].
subst vs.
RSF.destructStackTopValues H5.
subst.
eapply stackop_1_2_impl in H2.
destruct H2 as [val1 H2].
destruct H2 as [val2 H2].
decompose [and] H2; clear H2.
injection H; clear H; intro H; subst.
∃ (frameMake vars [VInt val2; VInt val1] (next code pc1)).
split.
reflexivity.
∃ val1.
∃ val2.
simpl.
repeat split.
apply pc1_next.
assumption.
assumption.
assumption.
assert (Hvs1 := stackop_dup_inversion _ _ H2).
destruct Hvs1 as [arg Hvs1].
subst vs.
RSF.destructPrefix H5.
subst.
eapply stackop_1_2_impl in H2.
destruct H2 as [val1 H2].
destruct H2 as [val2 H2].
decompose [and] H2; clear H2.
discriminate H.
assumption.
Qed.
Lemma frame_2_3_impl: ∀ f2 result,
frame2_props f2 →
SF.semFrame code (FI_Stackop (SI_Binop KInt ArithmeticOperators.BinOp_add)) f2 result →
∃ f3, result = Result f3 ∧ frame3_props f3.
Proof.
intros.
destruct H as [x H].
destruct H as [y H].
decompose [and] H; clear H.
inversion H0; clear H0; subst;
simpl in *;
subst.
assert (Hvs1 := stackop_binop_inversion _ _ _ H4).
destruct Hvs1 as [arg1 Hvs1].
destruct Hvs1 as [arg2 Hvs1].
subst vs.
RSF.destructStackTopValues H6.
subst.
eapply stackop_2_3_impl_gen in H4.
destruct H4 as [val H4].
decompose [and] H4; clear H4.
injection H; clear H; intro H; subst.
∃ (frameMake vars [VInt val] (next code pc2)).
split.
simpl.
reflexivity.
∃ val.
simpl.
repeat split.
apply pc2_next.
assumption.
reflexivity.
assumption.
assumption.
assert (Hvs1 := stackop_binop_inversion _ _ _ H4).
destruct Hvs1 as [arg1 Hvs1].
destruct Hvs1 as [arg2 Hvs1].
subst vs.
RSF.destructPrefix H6.
subst.
eapply stackop_2_3_impl_gen in H4.
destruct H4 as [val H4].
decompose [and] H4; clear H4.
discriminate H.
reflexivity.
assumption.
assumption.
Qed.
Lemma stepFrame_0_1_impl: ∀ f0 f1,
frame0_props f0 →
SF.stepFrame code f0 f1 →
frame1_props f1.
Proof.
intros.
set (H' := H).
destruct H' as [fr0 H'].
decompose [and] H'; clear H'.
inversion H0; clear H0; subst.
InstructionRewrite getPC_isPC0.
subst.
apply frame_0_1_impl in H2.
destruct H2 as [fr' H2].
decompose [and] H2; clear H2.
injection H0; clear H0; intros; subst.
assumption.
assumption.
Qed.
Lemma stepFrame_1_2_impl: ∀ f1 f2,
frame1_props f1 →
SF.stepFrame code f1 f2 →
frame2_props f2.
Proof.
intros.
set (H' := H).
destruct H' as [fr1 H'].
decompose [and] H'; clear H'.
inversion H0; clear H0; subst.
Instruction1Rewrite.
subst.
apply frame_1_2_impl in H5.
destruct H5 as [fr' H5].
decompose [and] H5; clear H5.
injection H0; clear H0; intros; subst.
assumption.
assumption.
Qed.
Lemma stepFrame_2_3_impl: ∀ f2 f3,
frame2_props f2 →
SF.stepFrame code f2 f3 →
frame3_props f3.
Proof.
intros.
set (H' := H).
destruct H' as [fr0 H'].
decompose [and] H'; clear H'.
inversion H0; clear H0; subst.
Instruction2Rewrite.
subst.
apply frame_2_3_impl in H2.
destruct H2 as [fr' H2].
decompose [and] H2; clear H2.
injection H0; clear H0; intros; subst.
assumption.
assumption.
Qed.
Lemma stepFrame_3_impossible: ∀ f3 fx,
frame3_props f3 →
SF.stepFrame code f3 fx →
False.
Proof.
intros.
set (H' := H).
destruct H' as [x H'].
decompose [and] H'; clear H'.
inversion H0; clear H0; subst.
Instruction3Rewrite.
Qed.
SSOP.semStack (SI_Generic Op_dup) vs1 result →
∃ arg,
vs1 = [arg].
Proof.
intros.
inversion H; clear H; subst.
inversion H1; clear H1; subst.
∃ (fv 0%nat).
simpl.
reflexivity.
Qed.
Lemma frame_0_1_impl: ∀ f0 result,
frame0_props f0 →
SF.semFrame code (FI_Stackop (SI_Const KInt (vtwo))) f0 result →
∃ f1, result = Result f1 ∧ frame1_props f1.
Proof.
intros.
unfold frame0_props in H.
decompose [and] H; clear H.
inversion H0; clear H0; subst;
simpl in *;
subst.
set (Hprefix := RSF.PstackTopValues_implies_prefix_l _ _ _ _ H4).
apply RSF.PprefixNilImpliesNil in Hprefix.
subst vs.
RSF.destructStackTopValues H4.
subst.
eapply stackop_0_1_impl in H3.
destruct H3 as [val H3].
decompose [and] H3; clear H3.
injection H; clear H; intro H; subst.
∃ (frameMake vars [VInt val] (next code pc0)).
split.
reflexivity.
∃ val.
simpl.
repeat split.
apply pc0_next.
assumption.
apply RSF.PprefixNilImpliesNil in H4.
subst vs.
eapply stackop_0_1_impl in H3.
destruct H3 as [val H3].
decompose [and] H3; clear H3.
discriminate H.
Qed.
Lemma frame_1_2_impl: ∀ f1 result,
frame1_props f1 →
SF.semFrame code (FI_Stackop (SI_Generic Op_dup)) f1 result →
∃ f2, result = Result f2 ∧ frame2_props f2.
Proof.
intros.
destruct H as [x H].
decompose [and] H; clear H.
inversion H0; clear H0; subst;
simpl in *;
subst.
assert (Hvs1 := stackop_dup_inversion _ _ H2).
destruct Hvs1 as [arg Hvs1].
subst vs.
RSF.destructStackTopValues H5.
subst.
eapply stackop_1_2_impl in H2.
destruct H2 as [val1 H2].
destruct H2 as [val2 H2].
decompose [and] H2; clear H2.
injection H; clear H; intro H; subst.
∃ (frameMake vars [VInt val2; VInt val1] (next code pc1)).
split.
reflexivity.
∃ val1.
∃ val2.
simpl.
repeat split.
apply pc1_next.
assumption.
assumption.
assumption.
assert (Hvs1 := stackop_dup_inversion _ _ H2).
destruct Hvs1 as [arg Hvs1].
subst vs.
RSF.destructPrefix H5.
subst.
eapply stackop_1_2_impl in H2.
destruct H2 as [val1 H2].
destruct H2 as [val2 H2].
decompose [and] H2; clear H2.
discriminate H.
assumption.
Qed.
Lemma frame_2_3_impl: ∀ f2 result,
frame2_props f2 →
SF.semFrame code (FI_Stackop (SI_Binop KInt ArithmeticOperators.BinOp_add)) f2 result →
∃ f3, result = Result f3 ∧ frame3_props f3.
Proof.
intros.
destruct H as [x H].
destruct H as [y H].
decompose [and] H; clear H.
inversion H0; clear H0; subst;
simpl in *;
subst.
assert (Hvs1 := stackop_binop_inversion _ _ _ H4).
destruct Hvs1 as [arg1 Hvs1].
destruct Hvs1 as [arg2 Hvs1].
subst vs.
RSF.destructStackTopValues H6.
subst.
eapply stackop_2_3_impl_gen in H4.
destruct H4 as [val H4].
decompose [and] H4; clear H4.
injection H; clear H; intro H; subst.
∃ (frameMake vars [VInt val] (next code pc2)).
split.
simpl.
reflexivity.
∃ val.
simpl.
repeat split.
apply pc2_next.
assumption.
reflexivity.
assumption.
assumption.
assert (Hvs1 := stackop_binop_inversion _ _ _ H4).
destruct Hvs1 as [arg1 Hvs1].
destruct Hvs1 as [arg2 Hvs1].
subst vs.
RSF.destructPrefix H6.
subst.
eapply stackop_2_3_impl_gen in H4.
destruct H4 as [val H4].
decompose [and] H4; clear H4.
discriminate H.
reflexivity.
assumption.
assumption.
Qed.
Lemma stepFrame_0_1_impl: ∀ f0 f1,
frame0_props f0 →
SF.stepFrame code f0 f1 →
frame1_props f1.
Proof.
intros.
set (H' := H).
destruct H' as [fr0 H'].
decompose [and] H'; clear H'.
inversion H0; clear H0; subst.
InstructionRewrite getPC_isPC0.
subst.
apply frame_0_1_impl in H2.
destruct H2 as [fr' H2].
decompose [and] H2; clear H2.
injection H0; clear H0; intros; subst.
assumption.
assumption.
Qed.
Lemma stepFrame_1_2_impl: ∀ f1 f2,
frame1_props f1 →
SF.stepFrame code f1 f2 →
frame2_props f2.
Proof.
intros.
set (H' := H).
destruct H' as [fr1 H'].
decompose [and] H'; clear H'.
inversion H0; clear H0; subst.
Instruction1Rewrite.
subst.
apply frame_1_2_impl in H5.
destruct H5 as [fr' H5].
decompose [and] H5; clear H5.
injection H0; clear H0; intros; subst.
assumption.
assumption.
Qed.
Lemma stepFrame_2_3_impl: ∀ f2 f3,
frame2_props f2 →
SF.stepFrame code f2 f3 →
frame3_props f3.
Proof.
intros.
set (H' := H).
destruct H' as [fr0 H'].
decompose [and] H'; clear H'.
inversion H0; clear H0; subst.
Instruction2Rewrite.
subst.
apply frame_2_3_impl in H2.
destruct H2 as [fr' H2].
decompose [and] H2; clear H2.
injection H0; clear H0; intros; subst.
assumption.
assumption.
Qed.
Lemma stepFrame_3_impossible: ∀ f3 fx,
frame3_props f3 →
SF.stepFrame code f3 fx →
False.
Proof.
intros.
set (H' := H).
destruct H' as [x H'].
decompose [and] H'; clear H'.
inversion H0; clear H0; subst.
Instruction3Rewrite.
Qed.
Lemma semInstr_0_1:
SEM.semInstr p code (I_Frame (FI_Stackop (SI_Const KInt (vtwo))))
(thstate0, heap) (Result (thstate1, heap)).
Proof.
intros.
econstructor.
reflexivity.
reflexivity.
apply frame_0_1.
Qed.
Lemma semInstr_1_2:
SEM.semInstr p code (I_Frame (FI_Stackop (SI_Generic Op_dup)))
(thstate1, heap) (Result (thstate2, heap)).
Proof.
intros.
econstructor.
reflexivity.
reflexivity.
apply frame_1_2.
Qed.
Lemma semInstr_2_3:
SEM.semInstr p code (I_Frame (FI_Stackop (SI_Binop KInt ArithmeticOperators.BinOp_add)))
(thstate2, heap) (Result (thstate3, heap)).
Proof.
intros.
econstructor.
reflexivity.
reflexivity.
apply frame_2_3.
Qed.
Lemma semInstr_0_1_impl: ∀ h th result,
thstate0_props th →
SEM.semInstr p code (I_Frame (FI_Stackop (SI_Const KInt vtwo)))
(th, h) result →
∃ th',
result = Result (th', h)
∧thstate1_props th'.
Proof.
intros.
destruct H as [fr0 H].
decompose [and] H; clear H.
inversion H0; clear H0; subst;
simpl in ×.
normal result
injection H2; clear H2; intros; subst.
apply frame_0_1_impl in H10.
destruct H10 as [fr1 H].
decompose [and] H; clear H.
injection H0; clear H0; intros; subst.
∃ (threadMake thid0 null [(cm,fr1)]).
split.
reflexivity.
∃ fr1.
simpl.
repeat split.
assumption.
assumption.
apply frame_0_1_impl in H10.
destruct H10 as [fr1 H].
decompose [and] H; clear H.
injection H0; clear H0; intros; subst.
∃ (threadMake thid0 null [(cm,fr1)]).
split.
reflexivity.
∃ fr1.
simpl.
repeat split.
assumption.
assumption.
exception
injection H2; clear H2; intros; subst.
apply frame_0_1_impl in H9.
destruct H9 as [fr1 H].
decompose [and] H; clear H.
discriminate H0.
assumption.
Qed.
Lemma semInstr_1_2_impl: ∀ h th result,
thstate1_props th →
SEM.semInstr p code (I_Frame (FI_Stackop (SI_Generic Op_dup)))
(th, h) result →
∃ th',
result = Result (th', h)
∧thstate2_props th'.
Proof.
intros.
destruct H as [fr1 H].
decompose [and] H; clear H.
inversion H0; clear H0; subst;
simpl in ×.
apply frame_0_1_impl in H9.
destruct H9 as [fr1 H].
decompose [and] H; clear H.
discriminate H0.
assumption.
Qed.
Lemma semInstr_1_2_impl: ∀ h th result,
thstate1_props th →
SEM.semInstr p code (I_Frame (FI_Stackop (SI_Generic Op_dup)))
(th, h) result →
∃ th',
result = Result (th', h)
∧thstate2_props th'.
Proof.
intros.
destruct H as [fr1 H].
decompose [and] H; clear H.
inversion H0; clear H0; subst;
simpl in ×.
normal result
injection H2; clear H2; intros; subst.
apply frame_1_2_impl in H10.
destruct H10 as [f2 H].
decompose [and] H; clear H.
injection H0; clear H0; intros; subst.
∃ (threadMake thid0 null [(cm,f2)]).
split.
reflexivity.
∃ f2.
simpl.
repeat split.
assumption.
assumption.
apply frame_1_2_impl in H10.
destruct H10 as [f2 H].
decompose [and] H; clear H.
injection H0; clear H0; intros; subst.
∃ (threadMake thid0 null [(cm,f2)]).
split.
reflexivity.
∃ f2.
simpl.
repeat split.
assumption.
assumption.
exception
injection H2; clear H2; intros; subst.
apply frame_1_2_impl in H9.
destruct H9 as [fr2 H].
decompose [and] H; clear H.
discriminate H0.
assumption.
Qed.
Lemma semInstr_2_3_impl: ∀ h th result,
thstate2_props th →
SEM.semInstr p code (I_Frame (FI_Stackop (SI_Binop KInt ArithmeticOperators.BinOp_add)))
(th, h) result →
∃ th',
result = Result (th', h)
∧thstate3_props th'.
Proof.
intros.
destruct H as [fr2 H].
decompose [and] H; clear H.
inversion H0; clear H0; subst;
simpl in ×.
apply frame_1_2_impl in H9.
destruct H9 as [fr2 H].
decompose [and] H; clear H.
discriminate H0.
assumption.
Qed.
Lemma semInstr_2_3_impl: ∀ h th result,
thstate2_props th →
SEM.semInstr p code (I_Frame (FI_Stackop (SI_Binop KInt ArithmeticOperators.BinOp_add)))
(th, h) result →
∃ th',
result = Result (th', h)
∧thstate3_props th'.
Proof.
intros.
destruct H as [fr2 H].
decompose [and] H; clear H.
inversion H0; clear H0; subst;
simpl in ×.
normal result
injection H2; clear H2; intros; subst.
apply frame_2_3_impl in H10.
destruct H10 as [fr3 H].
decompose [and] H; clear H.
injection H0; clear H0; intros; subst.
∃ (threadMake thid0 null [(cm,fr3)]).
split.
reflexivity.
∃ fr3.
simpl.
repeat split.
assumption.
assumption.
apply frame_2_3_impl in H10.
destruct H10 as [fr3 H].
decompose [and] H; clear H.
injection H0; clear H0; intros; subst.
∃ (threadMake thid0 null [(cm,fr3)]).
split.
reflexivity.
∃ fr3.
simpl.
repeat split.
assumption.
assumption.
exception
injection H2; clear H2; intros; subst.
apply frame_2_3_impl in H9.
destruct H9 as [fr3 H].
decompose [and] H; clear H.
discriminate H0.
assumption.
Qed.
apply frame_2_3_impl in H9.
destruct H9 as [fr3 H].
decompose [and] H; clear H.
discriminate H0.
assumption.
Qed.
Lemma stepThread_0_1:
SEM.stepInThread p (thstate0, heap) (thstate1, heap).
Proof.
intros.
eapply SEM.StepInThread_instruction_ok. reflexivity.
apply ThisMethodCM.
apply Instruction0.
apply semInstr_0_1.
Qed.
Lemma stepThread_1_2:
SEM.stepInThread p (thstate1, heap) (thstate2, heap).
Proof.
intros.
eapply SEM.StepInThread_instruction_ok. reflexivity.
apply ThisMethodCM.
apply Instruction1.
apply semInstr_1_2.
Qed.
Lemma stepThread_2_3:
SEM.stepInThread p (thstate2, heap) (thstate3, heap).
Proof.
intros.
eapply SEM.StepInThread_instruction_ok. reflexivity.
apply ThisMethodCM.
apply Instruction2.
apply semInstr_2_3.
Qed.
Lemma stepThread_0_1_impl: ∀ h th h' th',
thstate0_props th →
SEM.stepInThread p (th, h) (th', h') →
h' = h ∧ thstate1_props th'.
Proof.
intros.
set (H' := H).
destruct H' as [fr0 H'].
decompose [and] H'; clear H'.
inversion H0; clear H0; subst;
simpl in *;
injection_list;
ThisMethodRewrite;
Instruction0Rewrite.
valid result
apply semInstr_0_1_impl in H12.
destruct H12 as [th0 H12].
decompose [and] H12; clear H12.
injection H0; clear H0; intros; subst th0; subst.
split.
reflexivity.
assumption.
assumption.
destruct H12 as [th0 H12].
decompose [and] H12; clear H12.
injection H0; clear H0; intros; subst th0; subst.
split.
reflexivity.
assumption.
assumption.
invalid cases exception result - not true because of semInstr_224_impl
apply semInstr_0_1_impl in H13.
destruct H13 as [th' H13].
decompose [and] H13; clear H13.
discriminate H0.
assumption.
destruct H13 as [th' H13].
decompose [and] H13; clear H13.
discriminate H0.
assumption.
exceptional state on input - not true (3 times)
apply HF.PRefType_NotNull in H11.
tauto.
apply HF.PRefType_NotNull in H11.
tauto.
apply HF.PRefType_NotNull in H11.
tauto.
Qed.
Lemma stepThread_1_2_impl: ∀ h th h' th',
thstate1_props th →
SEM.stepInThread p (th, h) (th', h') →
h' = h ∧ thstate2_props th'.
Proof.
intros.
set (H' := H).
destruct H' as [fr1 H'].
decompose [and] H'; clear H'.
inversion H0; clear H0; subst;
simpl in *;
injection_list;
ThisMethodRewrite;
Instruction1Rewrite.
tauto.
apply HF.PRefType_NotNull in H11.
tauto.
apply HF.PRefType_NotNull in H11.
tauto.
Qed.
Lemma stepThread_1_2_impl: ∀ h th h' th',
thstate1_props th →
SEM.stepInThread p (th, h) (th', h') →
h' = h ∧ thstate2_props th'.
Proof.
intros.
set (H' := H).
destruct H' as [fr1 H'].
decompose [and] H'; clear H'.
inversion H0; clear H0; subst;
simpl in *;
injection_list;
ThisMethodRewrite;
Instruction1Rewrite.
valid result
apply semInstr_1_2_impl in H12.
destruct H12 as [th0 H12].
decompose [and] H12; clear H12.
injection H0; clear H0; intros; subst th0; subst.
split.
reflexivity.
assumption.
assumption.
destruct H12 as [th0 H12].
decompose [and] H12; clear H12.
injection H0; clear H0; intros; subst th0; subst.
split.
reflexivity.
assumption.
assumption.
invalid cases exception result - not true because of semInstr_224_impl
apply semInstr_1_2_impl in H13.
destruct H13 as [th' H13].
decompose [and] H13; clear H13.
discriminate H0.
assumption.
destruct H13 as [th' H13].
decompose [and] H13; clear H13.
discriminate H0.
assumption.
exceptional state on input - not true (3 times)
apply HF.PRefType_NotNull in H11.
tauto.
apply HF.PRefType_NotNull in H11.
tauto.
apply HF.PRefType_NotNull in H11.
tauto.
Qed.
Lemma stepThread_2_3_impl: ∀ h th h' th',
thstate2_props th →
SEM.stepInThread p (th, h) (th', h') →
h' = h ∧ thstate3_props th'.
Proof.
intros.
set (H' := H).
destruct H' as [fr2 H'].
decompose [and] H'; clear H'.
inversion H0; clear H0; subst;
simpl in *;
injection_list;
ThisMethodRewrite;
Instruction2Rewrite.
tauto.
apply HF.PRefType_NotNull in H11.
tauto.
apply HF.PRefType_NotNull in H11.
tauto.
Qed.
Lemma stepThread_2_3_impl: ∀ h th h' th',
thstate2_props th →
SEM.stepInThread p (th, h) (th', h') →
h' = h ∧ thstate3_props th'.
Proof.
intros.
set (H' := H).
destruct H' as [fr2 H'].
decompose [and] H'; clear H'.
inversion H0; clear H0; subst;
simpl in *;
injection_list;
ThisMethodRewrite;
Instruction2Rewrite.
valid result
apply semInstr_2_3_impl in H12.
destruct H12 as [th0 H12].
decompose [and] H12; clear H12.
injection H0; clear H0; intros; subst th0; subst.
split.
reflexivity.
assumption.
assumption.
destruct H12 as [th0 H12].
decompose [and] H12; clear H12.
injection H0; clear H0; intros; subst th0; subst.
split.
reflexivity.
assumption.
assumption.
invalid cases exception result - not true because of semInstr_224_impl
apply semInstr_2_3_impl in H13.
destruct H13 as [th' H13].
decompose [and] H13; clear H13.
discriminate H0.
assumption.
destruct H13 as [th' H13].
decompose [and] H13; clear H13.
discriminate H0.
assumption.
exceptional state on input - not true (3 times)
apply HF.PRefType_NotNull in H11.
tauto.
apply HF.PRefType_NotNull in H11.
tauto.
apply HF.PRefType_NotNull in H11.
tauto.
Qed.
Lemma stepThread_3_impossible: ∀ h th h' th',
thstate3_props th →
SEM.stepInThread p (th, h) (th', h') →
False.
Proof.
intros.
destruct H as [fr3 H].
decompose [and] H; clear H.
inversion H0; clear H0; subst;
simpl in *;
injection_list;
ThisMethodRewrite.
Instruction3Rewrite.
Instruction3Rewrite.
tauto.
apply HF.PRefType_NotNull in H11.
tauto.
apply HF.PRefType_NotNull in H11.
tauto.
Qed.
Lemma stepThread_3_impossible: ∀ h th h' th',
thstate3_props th →
SEM.stepInThread p (th, h) (th', h') →
False.
Proof.
intros.
destruct H as [fr3 H].
decompose [and] H; clear H.
inversion H0; clear H0; subst;
simpl in *;
injection_list;
ThisMethodRewrite.
Instruction3Rewrite.
Instruction3Rewrite.
exceptional state on input - not true (3 times)
apply HF.PRefType_NotNull in H10.
tauto.
apply HF.PRefType_NotNull in H10.
tauto.
apply HF.PRefType_NotNull in H10.
tauto.
Qed.
tauto.
apply HF.PRefType_NotNull in H10.
tauto.
apply HF.PRefType_NotNull in H10.
tauto.
Qed.
Lemma step_0_1: SEM.step p jvm0 jvm1.
Proof.
econstructor.
3:econstructor 1.
constructor.
apply stepThread_0_1.
Qed.
Lemma step_1_2: SEM.step p jvm1 jvm2.
Proof.
econstructor.
3:econstructor 1.
constructor.
apply stepThread_1_2.
Qed.
Lemma step_2_3: SEM.step p jvm2 jvm3.
Proof.
econstructor.
3:econstructor 1.
constructor.
apply stepThread_2_3.
Qed.
Lemma step_0_1_impl: ∀ jvm jvm',
jvm0_props jvm →
SEM.step p jvm jvm' →
jvm1_props jvm'.
Proof.
intros.
destruct jvm as [heap threads].
destruct jvm' as [heap' threads'].
destruct H as [th H].
decompose [and] H; clear H.
simpl in H1, H3.
inversion H0; clear H0; subst.
apply SEM.oneThreadSelectedAlways in H.
subst th0.
apply SEM.PoneThreadAndHeapChanged_1thread_inv in H5.
decompose [and] H5; clear H5.
simpl in ×.
subst.
apply stepThread_0_1_impl in H2.
decompose [and] H2; clear H2.
subst.
∃ th'.
repeat split.
assumption.
assumption.
Qed.
Lemma step_1_2_impl: ∀ jvm jvm',
jvm1_props jvm →
SEM.step p jvm jvm' →
jvm2_props jvm'.
Proof.
intros.
destruct jvm as [heap threads].
destruct jvm' as [heap' threads'].
destruct H as [th H].
decompose [and] H; clear H.
simpl in H1, H3.
inversion H0; clear H0; subst.
apply SEM.oneThreadSelectedAlways in H.
subst th0.
apply SEM.PoneThreadAndHeapChanged_1thread_inv in H5.
decompose [and] H5; clear H5.
simpl in ×.
subst.
apply stepThread_1_2_impl in H2.
decompose [and] H2; clear H2.
subst.
∃ th'.
repeat split.
assumption.
assumption.
Qed.
Lemma step_2_3_impl: ∀ jvm jvm',
jvm2_props jvm →
SEM.step p jvm jvm' →
jvm3_props jvm'.
Proof.
intros.
destruct jvm as [heap threads].
destruct jvm' as [heap' threads'].
destruct H as [th H].
decompose [and] H; clear H.
simpl in H1, H3.
inversion H0; clear H0; subst.
apply SEM.oneThreadSelectedAlways in H.
subst th0.
apply SEM.PoneThreadAndHeapChanged_1thread_inv in H5.
decompose [and] H5; clear H5.
simpl in ×.
subst.
apply stepThread_2_3_impl in H2.
decompose [and] H2; clear H2.
subst.
∃ th'.
repeat split.
assumption.
assumption.
Qed.
Lemma step_3_impossible: ∀ jvm jvm',
jvm3_props jvm →
SEM.step p jvm jvm' →
False.
Proof.
intros.
destruct jvm as [heap threads].
destruct jvm' as [heap' threads'].
destruct H as [th H].
decompose [and] H; clear H.
simpl in H1, H3.
inversion H0; clear H0; subst.
apply SEM.oneThreadSelectedAlways in H.
subst th0.
apply SEM.PoneThreadAndHeapChanged_1thread_inv in H5.
decompose [and] H5; clear H5.
simpl in ×.
subst.
apply (stepThread_3_impossible _ _ _ _ H4 H2).
Qed.
Theorem StepsFrameConcrete: SF.stepsFrame code frame0 frame3.
Proof.
apply clos_rt1n_rt.
econstructor.
eapply stepFrame_0_1.
econstructor.
eapply stepFrame_1_2.
econstructor.
eapply stepFrame_2_3.
econstructor.
Qed.
Proof.
apply clos_rt1n_rt.
econstructor.
eapply stepFrame_0_1.
econstructor.
eapply stepFrame_1_2.
econstructor.
eapply stepFrame_2_3.
econstructor.
Qed.
stepsFrame in general implication style
Theorem StepsFrameImpl: ∀ fr fr',
frame0_props fr →
frameGetPC fr' = pc3 →
SF.stepsFrame code fr fr' →
frame3_props fr'.
Proof.
intros fr fr' H0 Hpc3 H.
apply clos_rt_rt1n in H.
inversion H; clear H; subst.
apply getPC_isPC0 in H0.
rewrite H0 in Hpc3.
apply pc0_neq_pc3 in Hpc3.
contradiction.
eapply stepFrame_0_1_impl in H1.
2:assumption.
clear H0 fr.
rename H1 into H0.
inversion H2; clear H2; subst.
apply getPC_isPC1 in H0.
rewrite H0 in Hpc3.
apply pc1_neq_pc3 in Hpc3.
contradiction.
eapply stepFrame_1_2_impl in H.
2:assumption.
clear H0 y.
rename H into H0.
inversion H1; clear H1; subst.
apply getPC_isPC2 in H0.
rewrite H0 in Hpc3.
apply pc2_neq_pc3 in Hpc3.
contradiction.
eapply stepFrame_2_3_impl in H.
2:assumption.
clear H0 y0.
rename H into H0.
inversion H2; clear H2; subst.
assumption.
apply stepFrame_3_impossible in H.
2:assumption.
contradiction.
Qed.
frame0_props fr →
frameGetPC fr' = pc3 →
SF.stepsFrame code fr fr' →
frame3_props fr'.
Proof.
intros fr fr' H0 Hpc3 H.
apply clos_rt_rt1n in H.
inversion H; clear H; subst.
apply getPC_isPC0 in H0.
rewrite H0 in Hpc3.
apply pc0_neq_pc3 in Hpc3.
contradiction.
eapply stepFrame_0_1_impl in H1.
2:assumption.
clear H0 fr.
rename H1 into H0.
inversion H2; clear H2; subst.
apply getPC_isPC1 in H0.
rewrite H0 in Hpc3.
apply pc1_neq_pc3 in Hpc3.
contradiction.
eapply stepFrame_1_2_impl in H.
2:assumption.
clear H0 y.
rename H into H0.
inversion H1; clear H1; subst.
apply getPC_isPC2 in H0.
rewrite H0 in Hpc3.
apply pc2_neq_pc3 in Hpc3.
contradiction.
eapply stepFrame_2_3_impl in H.
2:assumption.
clear H0 y0.
rename H into H0.
inversion H2; clear H2; subst.
assumption.
apply stepFrame_3_impossible in H.
2:assumption.
contradiction.
Qed.
steps on actual states
Theorem StepsConcrete: SEM.steps p jvm0 jvm3.
Proof.
apply clos_rt1n_rt.
econstructor.
eapply step_0_1.
econstructor.
eapply step_1_2.
econstructor.
eapply step_2_3.
econstructor.
Qed.
Proof.
apply clos_rt1n_rt.
econstructor.
eapply step_0_1.
econstructor.
eapply step_1_2.
econstructor.
eapply step_2_3.
econstructor.
Qed.
End