Changeset 1922

Ignore:
Timestamp:
May 8, 2012, 3:41:43 PM (9 years ago)
Message:

Main labelling simulation proof complete.

File:
1 edited

Unmodified
Removed
• src/Clight/labelSimulation.ma

 r1920 qed. inductive state_with_labels : state → state → Prop ≝ | swl_state : ∀f,us,s,k,k',e,m. cont_with_labels k k' → state_with_labels (State f s k e m) (State (label_function f) (\fst (label_statement s us)) k' e m) inductive state_with_labels_partial : state → state → Prop ≝ | swl_state : ∀f,us,s,k,k',e,m. cont_with_labels k k' → state_with_labels_partial (State f s k e m) (State (label_function f) (\fst (label_statement s us)) k' e m) (* Extra matching states that we can reach that don't quite correspond to the labelling function *) | swl_whilestate : ∀f,ua,a,us,s,cs,cpost,k,k',e,m. cont_with_labels k k' → state_with_labels (State f (Swhile a s) k e m) (State (label_function f) (Swhile (\fst (label_expr a ua)) (Scost cs (\fst (label_statement s us)))) (Kseq (Scost cpost Sskip) k') e m) state_with_labels_partial (State f (Swhile a s) k e m) (State (label_function f) (Swhile (\fst (label_expr a ua)) (Scost cs (\fst (label_statement s us)))) (Kseq (Scost cpost Sskip) k') e m) | swl_dowhilestate : ∀f,ua,a,us,s,cs,cpost,k,k',e,m. cont_with_labels k k' → state_with_labels (State f (Sdowhile a s) k e m) (State (label_function f) (Sdowhile (\fst (label_expr a ua)) (Scost cs (\fst (label_statement s us)))) (Kseq (Scost cpost Sskip) k') e m) state_with_labels_partial (State f (Sdowhile a s) k e m) (State (label_function f) (Sdowhile (\fst (label_expr a ua)) (Scost cs (\fst (label_statement s us)))) (Kseq (Scost cpost Sskip) k') e m) | swl_forstate : ∀f,ua2,a2,us3,s3,us,s,cs,cpost,k,k',e,m. cont_with_labels k k' → state_with_labels (State f (Sfor Sskip a2 s3 s) k e m) (State (label_function f) (Sfor Sskip (\fst (label_expr a2 ua2)) (\fst (label_statement s3 us3)) (Scost cs (\fst (label_statement s us)))) (Kseq (Scost cpost Sskip) k') e m) state_with_labels_partial (State f (Sfor Sskip a2 s3 s) k e m) (State (label_function f) (Sfor Sskip (\fst (label_expr a2 ua2)) (\fst (label_statement s3 us3)) (Scost cs (\fst (label_statement s us)))) (Kseq (Scost cpost Sskip) k') e m) (* and the rest *) | swl_callstate : ∀fd,args,k,k',m. cont_with_labels k k' → state_with_labels_partial (Callstate fd args k m) (Callstate (label_fundef fd) args k' m) | swl_returnstate : ∀res,k,k',m. cont_with_labels k k' → state_with_labels_partial (Returnstate res k m) (Returnstate res k' m) | swl_finalstate : ∀r. state_with_labels_partial (Finalstate r) (Finalstate r) . (* We handle the switch states after the rest so that we can reuse the partial result. *) inductive state_with_labels : state → state → Prop ≝ | swl_partial : ∀s,s'. state_with_labels_partial s s' → state_with_labels s s' | swl_switchstate : ∀f,u,ls,k,k',e,m. cont_with_labels k k' → state_with_labels (State f (seq_of_labeled_statement ls) k e m) (State (label_function f) (seq_of_labeled_statement (\fst  (label_lstatements ls u))) k' e m) (* and the rest *) | swl_callstate : ∀fd,args,k,k',m. cont_with_labels k k' → state_with_labels (Callstate fd args k m) (Callstate (label_fundef fd) args k' m) | swl_returnstate : ∀res,k,k',m. cont_with_labels k k' → state_with_labels (Returnstate res k m) (Returnstate res k' m) | swl_finalstate : ∀r. state_with_labels (Finalstate r) (Finalstate r) . ] ] qed. lemma label_fn_params : ∀f. fn_params (label_function f) = fn_params f. * #rty #params #vars #s whd in ⊢ (??(?%)?); @breakup_pair @breakup_pair // qed. lemma label_fn_vars : ∀f. fn_vars (label_function f) = fn_vars f. * #rty #params #vars #s whd in ⊢ (??(?%)?); @breakup_pair @breakup_pair // qed. (* Apply induction hypothesis while getting Matita to infer the continuations qed. lemma step_with_labels : ∀ge,ge'. (* We show the main simulation in two stages.  First, we show it for all states in the relation *except* those for labeled_statements, then we'll show the whole thing.  This is so that we can appeal to the other cases in the proof for labeled_statements. *) lemma step_with_labels_partial : ∀ge,ge'. related_globals ge ge' → ∀s1,s1',tr,s2. state_with_labels s1 s1' → state_with_labels_partial s1 s1' → exec_step ge s1 = Value … 〈tr,s2〉 → ∃tr',s2'. plus ge' s1' tr' s2' ∧ trace_with_extra_labels tr tr' ∧ state_with_labels s2 s2'. ∃tr',s2'. plus ge' s1' tr' s2' ∧ trace_with_extra_labels tr tr' ∧ state_with_labels s2 s2'. #ge #ge' #RG #Xs1 #Xs1' #tr #s2 * [ #f #us #s #k #k' #e #m #KL cases s [ #E >E in EX; whd in ⊢ (??%% → ?); #EX' destruct %{(Returnstate Vundef Kstop (free_list ? m (blocks_of_env e)))} % [ % [ @plus_one whd in ⊢ (??%?); >label_function_return >E @refl | // ] | /2/ ] | // ] | /3/ ] | *: #A [ 1,3,5,6,7,8: #B | 4: #B #C ] #E >E in EX; #EX whd in EX:(??%%); destruct ] %{(State (label_function f) (\fst (label_statement s0 u)) k0' e m)} whd in EX:(??%%); destruct % [ % [ @plus_one @refl | // ] | /2/ ] % [ % [ @plus_one @refl | // ] | /3/ ] | #ue #e0 #us0 #s0 #cs #cpost #k0 #k0' #K #_ #E1 #E2 #E3 destruct %{tr} whd in EX:(??%%); destruct % [ 2: % [ % [ @plus_one @refl | // ] | @swl_whilestate // ] | skip ] % [ 2: % [ % [ @plus_one @refl | // ] | @swl_partial @swl_whilestate // ] | skip ] | #ue #e0 #us0 #s0 #cs #cpost #k0 #k0' #K #_ #E1 #E2 #E3 destruct cases (bindIO_inversion ??????? EX) * #ve #tre * #EXe #EXrem whd in ⊢ (??%?); @refl | // ] | @swl_dowhilestate // ] | skip ] | skip ] | @swl_partial @swl_dowhilestate // ] | skip ] | skip ] | % [ 2: % [ 2: % [ % [ @plus_succ [ 4: whd in ⊢ (??%?); >EXe' in ⊢ (??%?); | 5: @plus_one @refl | skip ] | skip ] | <(E0_right tr) @twel_app /2/ ] | /2/ ] | skip ] | skip ] | /3/ ] | skip ] | skip ] ] | #ue #e0 #us1 #st1 #us2 #st2 #cs #cpost #k0 #k0' #K #_ #E1 #E2 #E3 destruct | #ue #e0 #us1 #st1 #us2 #st2 #cs #cpost #k0 #k0' #K #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct %{E0} % [2: % [ % [ @plus_one @refl | // ] | /3/ ] | skip ] %{E0} % [2: % [ % [ @plus_one @refl | // ] | /4/ ] | skip ] | #ue #e0 #us1 #st1 #us2 #st2 #cs #cpost #k0 #k0' #K #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct %{E0} % [2: % [ % [ @plus_one @refl | // ] | /3/ ] | skip ] %{E0} % [2: % [ % [ @plus_one @refl | // ] | /4/ ] | skip ] | #k0 #k0' #K #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct %{E0} % [2: % [ % [ @plus_one @refl | // ] | /3/ ] | skip ] %{E0} % [2: % [ % [ @plus_one @refl | // ] | /4/ ] | skip ] | #r #f0 #en #k0 #k0' #K #_ #E1 #E2 #E3 destruct whd in EX:(??%?); [ #E >E in EX; whd in ⊢ (??%? → ?); #EX destruct %{E0} % [2: % [ % [ @plus_one whd in ⊢ (??%?); >label_function_return >E in ⊢ (??%?); @refl | // ] | /3/ ] | skip ] @refl | // ] | /4/ ] | skip ] | *: #A [ 1,3,5,6,7,8: #B | 4: #B #C ] #E >E in EX; #EX whd in EX:(??%%); destruct ] | #ls #u #k0 #k0' #K #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct % [2: % [2: % [ % [ @plus_one @refl | // ] | /2/ ]| skip ]| skip ] % [2: % [2: % [ % [ @plus_one @refl | // ] | /3/ ]| skip ]| skip ] ] | * #a1 #ty1 #a2 #EX whd in ⊢ (??%?); >label_expr_type >EX3 in ⊢ (??%?); @refl | @twel_app // ] | /2/ ] | skip ] | skip ] | @twel_app // ] | /3/ ] | skip ] | skip ] | * [2: * #er #tyr ] #ef #args #EX cases (bindIO_inversion ??????? EX) -EX * #v1 #tr1 * #EX1 #EX whd in ⊢ (??%?); >label_fundef_typeof_fundef >label_expr_fun_typeof [ >EX4 in ⊢ (??%?); | >EX4 in ⊢ (??%?); ] whd in ⊢ (??%?); [ >exec_lvalue_labelled >EX5' in ⊢ (??%?); ] @refl | *: @twel_app /2/ ] | *: @swl_callstate /2/ ] | *: skip ] | *: skip ] @refl | *: @twel_app /2/ ] | *: @swl_partial @swl_callstate /2/ ] | *: skip ] | *: skip ] | #st1 #st2 #EX whd in EX:(??%%); destruct whd in match (label_statement ??); @label_gen_elim #u1 @label_gen_elim #u2 %{E0} % [2: % [ % [ @plus_one @refl | // ] | @swl_state /2/ ] | skip ] %{E0} % [2: % [ % [ @plus_one @refl | // ] | @swl_partial @swl_state /2/ ] | skip ] | #a #st1 #st2 #EX cases (bindIO_inversion ??????? EX) -EX * #v1 #tr1 * #EX1 #EX ] | 2,4: <(E0_right tr) @twel_app /2/ ]| 2,4: /2/ ] | *: skip ] | *: skip ] ]| 2,4: /3/ ] | *: skip ] | *: skip ] | #a #st #EX cases (bindIO_inversion ??????? EX) -EX * #v1 #tr1 * #EX1 #EX ] | 2,4: <(E0_left tr) @twel_app // <(E0_right tr) @twel_app /2/ ]| 2,4: /3/ ] | *: skip ] | *: skip ] ]| 2,4: /4/ ] | *: skip ] | *: skip ] | #a #st #EX normalize in EX; destruct % [2: % [2: % [ % [ @plus_succ [ 4: @refl | 1,2: skip | 5: @plus_succ [ 4: @refl | 1,2: skip | 5: @plus_one // | skip ] | skip ] | /2/ ] | /3/ ] | skip ] | skip ] | /2/ ] | /4/ ] | skip ] | skip ] | #st1 #a #st2 #st #EX lapply (refl ? (is_Sskip st1)) cases (is_Sskip st1) in ⊢ (???% → ?); #Esk #Eskip ] | 2,4: <(E0_left tr) @twel_app // <(E0_right tr) @twel_app /2/ ]| 2,4: /3/ ] | *: skip ] | *: skip ] ]| 2,4: /4/ ] | *: skip ] | *: skip ] | whd in EX:(??%%); destruct % [2: % [2: %[ %[ @plus_succ [ 4: @refl | 5: @plus_one whd in ⊢ (??%?); cases (labelled_is_not_skip ? u1 Esk) #Esk' #Eskip' >Eskip' whd in ⊢ (??%?); @refl | *: skip ]| // ] | @swl_state /2/ ] >Eskip' whd in ⊢ (??%?); @refl | *: skip ]| // ] | @swl_partial @swl_state /2/ ] | skip ] | skip ] ] | @plus_succ [ 4: @refl | 5: @plus_one @refl |*:skip] | /2/ | @plus_succ [ 4: @refl | 5: @plus_succ [ 4: @refl | 5: @plus_one @refl |*:skip]|*:skip] | /2/ ]| *: /2/ ]|*: skip]|*: skip ] ]| *: /3/ ]|*: skip]|*: skip ] | #EX inversion KL [ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct [ 1,2,4,5,6,7: % [2,4,6,8,10,12: % [2,4,6,8,10,12: % [1,3,5,7,9,11: % [1,3,7,9,11: @plus_one @refl | 5: @plus_succ [4:@refl | 5:@plus_one @refl | *: skip ] | *: // ] | *: /3 by cwl_for3, swl_state, swl_whilestate/ ]| *:skip ]| *: skip ] | *: // ] | *: @swl_partial /3 by cwl_for3, swl_state, swl_whilestate/ ]| *:skip ]| *: skip ] | cases (bindIO_inversion ??????? EX) -EX * #v1 #tr1 * #EX1 #EX cases (bindIO_inversion ??????? EX) -EX * * #EX2 #EX | // | <(E0_right tr) @twel_app /2/ ] | /3/ | /2/ ] | *: skip ] | *: skip ] | /3/ | /3/ ] | *: skip ] | *: skip ] ] | * [2: #a ] #EX | >label_function_return >Ety in ⊢ (??%?); ] whd in ⊢ (??%?); @refl | *: // ]| *: @swl_returnstate /2/ ]|*:skip]|*:skip] | *: // ]| *: @swl_partial @swl_returnstate /2/ ]|*:skip]|*:skip] | #a #ls #EX cases (bindIO_inversion ??????? EX) -EX * #v1 #tr1 * #EX1 #EX %[2: %[2: %[ %[ @plus_succ [ 4: @refl | 5: @plus_one @refl | *: skip ] | /2/ ] | /2/ ] |skip ]| skip ] | /2/ ] | /3/ ] |skip ]| skip ] | #l #EX whd in EX:(??%?); % [2: %[2: %[ %[ @plus_succ [ 4: whd in ⊢ (??%?); >F' in ⊢ (??%?); @refl | 5: @plus_one @refl | *: skip ] | /2/ ] | /2/ ] | skip ] | skip ] | /2/ ] | /3/ ] | skip ] | skip ] ] | #c #st #EX whd in EX:(??%?); destruct @blindly_label #u1 % [2: % [2: % [ % [ @plus_one @refl | // ] | /2/ ] | skip ]| skip ] % [2: % [2: % [ % [ @plus_one @refl | // ] | /3/ ] | skip ]| skip ] ] | #f #ua #a #us #s #cs #cpost #k #k' #e #m #K #EX whd in ⊢ (??%?); >label_expr_type >EX2 in ⊢ (??%?); @refl |5: @plus_one @refl | *: skip ] | <(E0_right tr) /3/ ]| /3/ ]| skip ]| skip ] | <(E0_right tr) /3/ ]| /4/ ]| skip ]| skip ] | % [2: % [2: % [ % [ @plus_succ [4: whd in ⊢ (??%?); >EX1' in ⊢ (??%?); | 5: @plus_succ [4: @refl | 5: @plus_one @refl | *: skip ] | *: skip ] | <(E0_right tr) /3/ ]| /2/ ]| skip ]| skip ] | <(E0_right tr) /3/ ]| /3/ ]| skip ]| skip ] ] | #f #ua #a #us #s #cs #cpost #k #k' #e #m #K #EX % [2: % [2: % [ % [ @plus_succ [4: % | 5: @plus_one % | *: skip ] | /2/ ]| /3/ ]| skip ]| skip ] | /2/ ]| /4/ ]| skip ]| skip ] | #f #ua2 #a2 #us3 #s3 #us #s #cs #cpost #k #k' #e #m #K #EX cases (bindIO_inversion ??????? EX) -EX * #v1 #tr1 * #EX1 #EX whd in ⊢ (??%?); >label_expr_type >EX2 in ⊢ (??%?); @refl | 5: whd in ⊢ (??(??%%??)??); @plus_one @refl | *: skip ]| <(E0_right tr) /3/ ] | /3/ ]| skip ]| skip ] | *: skip ]| <(E0_right tr) /3/ ] | /4/ ]| skip ]| skip ] | % [2: % [2: % [ % [ @plus_succ [ 4: whd in ⊢ (??%?); >EX1' in ⊢ (??%?); whd in ⊢ (??%?); >label_expr_type >EX2 in ⊢ (??%?); @refl | 5: whd in ⊢ (??(??%%??)??); @plus_succ [4: @refl | 5: @plus_one @refl ]| *: skip ]| <(E0_right tr) /3/ ]| /2/ ]| skip ]| skip ] ] | #f #u * [ #s | #sz #i #s #ls ] #k #k' #e #m #K #EX whd in EX:(??(??(??%???))?); | 5: @plus_one @refl ]| *: skip ]| <(E0_right tr) /3/ ]| /3/ ]| skip ]| skip ] ] | * [ #f #args #k #k' #m #K whd in ⊢ (??%? → ?); @pair_elim #e #m1 #EX1 #EX cases (bindIO_inversion ??????? EX) -EX #m2 * #EX2 #EX whd in EX:(??%%); destruct whd in match (label_fundef ?); whd in match (label_function ?); lapply (refl ? (label_function f)) whd in ⊢ (???% → ?); @label_gen_elim #u1 @label_gen_elim #u2 >shift_fst #Ef % [2: % [2: % [ % [ @plus_succ [4: whd in ⊢ (??%?); >EX1 in ⊢ (??%?); whd in ⊢ (??%?); >EX2 in ⊢ (??%?); @refl | 5: @plus_one @refl | *: skip ] | /2/ ]| EX1 in ⊢ (??%?); @refl | // ]| /3/ ]| skip ]| skip ] ] | *: #A #B #C #D #E #F #G try #H try #I try #J try #L try #M try #N try #O destruct whd in EX:(??%?); destruct ] | #r #EX whd in EX:(??%%); destruct ] qed. lemma step_with_labels : ∀ge,ge'. related_globals ge ge' → ∀s1,s1',tr,s2. state_with_labels s1 s1' → (exec_step ge s1 = Value … 〈tr,s2〉 → ∃tr',s2'. plus ge' s1' tr' s2' ∧ trace_with_extra_labels tr tr' ∧ state_with_labels s2 s2'). #ge #ge' #RG #Xs1 #Xs1' #tr #s2 * [ #s1 #s1' @step_with_labels_partial // | #f #u * (* If we have LSdefault we need to smuggle the execution of the cost label in before the actual statement. *) [ #s #k #k' #e #m #K #EX whd in EX:(??(??(??%???))?); whd in match (label_lstatements ??); @label_gen_elim #u1 @label_gen_elim #u2 >shift_fst whd in match (seq_of_labeled_statement ?); cases (step_with_labels_partial … RG (State f s k e m) (State (label_function f) (\fst (label_statement s u)) k' e m) tr s2 (swl_state … K) EX) #tr' * #s2' * * #P #T #S % [2: % [2: % [ % [ @plus_succ [4: @refl | 5: @P | *: skip ] | /2/ ]| @S ]| skip ]| skip ] (* but for LScase it's just like the cases in step_with_labels_partial *) | #sz #i #s #ls #k #k' #e #m #K #EX whd in EX:(??(??(??%???))?); whd in match (label_lstatements ??); @label_gen_elim #u1 @label_gen_elim #u2 @label_gen_elim #u3 >shift_fst whd in match (seq_of_labeled_statement ?); whd in EX:(??%?); destruct % [2: % [2: % [ % [ @plus_succ [4: @refl | 5: @plus_one @refl | *: skip ] | /2/ ]| /4/ ]| skip ]| skip ] ] ] qed.
Note: See TracChangeset for help on using the changeset viewer.