Changeset 2682
 Timestamp:
 Feb 19, 2013, 7:24:20 PM (8 years ago)
 Location:
 src
 Files:

 3 edited
Legend:
 Unmodified
 Added
 Removed

src/Clight/labelSimulation.ma
r2677 r2682 1021 1021 >shift_fst whd in match (seq_of_labeled_statement ?); 1022 1022 cases (step_with_labels_partial … RG (State f s k e m) (State (\fst (label_function u0 f)) (\fst (label_statement s u)) k' e m) tr s2 (swl_state … K) EX) 1023 #n #H %{(S n)} @(after_n_m 1 (S n) … H) % /2/1023 #n #H %{(S n)} @(after_n_m 1 (S n) … H) // % /2/ 1024 1024 #trx #sx * /3/ 1025 1025 (* but for LScase it's just like the cases in step_with_labels_partial *) 
src/common/Executions.ma
r2487 r2682 67 67 cases (step … s) [ #o #K *  3: #m * ] 68 68 * #tr' #s' 69 whd in ⊢ (% → ?); cases (inv s') [2: *]69 whd in ⊢ (% → ?); 70 70 #AW %{tr'} %{s'} %{AW} 71 71 lapply (refl ? (is_final … s')) cases (is_final … s') in ⊢ (???% → %); 
src/common/SmallstepExec.ma
r2669 r2682 60 60 not (reducible to) a value. 61 61 62 An invariant is also asserted on every state other than the initial one. 62 An invariant is also asserted on every intermediate state (i.e., everything 63 other than the first and last states). 63 64 64 65 For example, we state a property to prove by something like … … 103 104 let rec assert (b:bool) (P:Prop) on b ≝ 104 105 if b then P else False. 106 107 let rec assert_nz (n:nat) (b:bool) (P:Prop) on n ≝ 108 match n with 109 [ O ⇒ P 110  _ ⇒ assert b P 111 ]. 105 112 106 113 let rec after_aux (avs:await_value_stuff) … … 114 121 [ None ⇒ 115 122 await_value avs (step ?? (avs_exec avs) (avs_g avs) s) (λtr',s. 116 assert (avs_inv avs s) (after_aux avs n' s (tr ⧺ tr') P))123 assert_nz n' (avs_inv avs s) (after_aux avs n' s (tr ⧺ tr') P)) 117 124  _ ⇒ False 118 125 ] 119 126 ]. 127 128 lemma assert_nz_lift : ∀n,b,P,Q. 129 (P → Q) → 130 assert_nz n b P → 131 assert_nz n b Q. 132 * [ /2/  #n * [ normalize /2/  #P #Q #_ * ] ] 133 qed. 120 134 121 135 definition after_n_steps : nat → … … 139 153 * #tr'' #s'' 140 154 whd in ⊢ (% → %); 141 cases (avs_inv avs s'') [ 2: * ] 142 whd in ⊢ (% → %); 155 @assert_nz_lift 143 156 >Eapp_assoc @IH 144 157 ] qed. … … 156 169 lemma after_n_m : ∀n,m,O,I,exec,g,inv,P,Q,s,s'. 157 170 after_n_steps m O I exec g s' inv Q → 171 (notb (eqb m 0) → inv s') → 158 172 after_n_steps n O I exec g s inv (λtr1,s1. s' = s1 ∧ (∀tr'',s''. Q tr'' s'' → P (tr1⧺tr'') s'')) → 159 173 after_n_steps (n+m) O I exec g s inv P. 160 #n #m #O #I #exec #g #inv #P #Q whd in ⊢ (? → ? → ? → % → %); generalize in match E0; elim n161 [ #tr #s #s' #H whd in ⊢ (% → %); * #E destruct #H2174 #n #m #O #I #exec #g #inv #P #Q whd in ⊢ (? → ? → ? → ? → % → %); generalize in match E0; elim n 175 [ #tr #s #s' #H #INVs' whd in ⊢ (% → %); * #E destruct #H2 162 176 whd in H; <(E0_right tr) generalize in match E0 in H ⊢ %; 163 177 generalize in match s; s … … 168 182 whd in ⊢ (% → %); 169 183 cases (step O I exec g s) [1,3: normalize //] * #tr'' #s'' whd in ⊢ (% → %); 170 cases (inv s'') [2: * ]184 @assert_nz_lift 171 185 >Eapp_assoc @IH ] 172  #n' #IH #tr #s #s' #H whd in ⊢ (% → %);186  #n' #IH #tr #s #s' #H #INVs' whd in ⊢ (% → %); 173 187 cases (is_final … s) [2: #r * ] 174 188 whd in ⊢ (% → %); 175 189 cases (step O I exec g s) [1,3: normalize // ] 176 190 * #tr1 #s1 whd in ⊢ (% → %); 191 cases n' in IH H ⊢ %; [ cases m in INVs' ⊢ %; 192 [ #Is' #IH #H @IH [ //  * #H cases (H (refl ??)) ] 193  #m' #Is' #IH #H * #E destruct >Is' [ #X @(IH … H) [ @Is'  % // @X ]  % #E destruct ] ] ] 194 #n'' #IH #H 177 195 cases (inv s1) [2:*] 178 @IH @H196 @IH assumption 179 197 ] qed. 180 198 181 199 (* Inversion lemmas. *) 200 201 lemma assert_nz_inv : ∀n,b,P. 202 assert_nz n b P → 203 (n = 0 ∨ bool_to_Prop b) ∧ P. 204 * [ /3/  #n * [ #P #p % /2/ @p  #P * ] ] 205 qed. 182 206 183 207 lemma after_1_of_n_steps : ∀n,O,I,exec,g,inv,P,s. … … 186 210 is_final … exec g s = None ? ∧ 187 211 step … exec g s = Value … 〈tr,s'〉 ∧ 188 bool_to_Prop (inv s') ∧212 (notb (eqb n 0) → bool_to_Prop (inv s')) ∧ 189 213 after_n_steps n O I exec g s' inv (λtr'',s''. P (tr⧺tr'') s''). 190 214 #n #O #I #exec #g #inv #P #s … … 194 218 cases (step … s) 195 219 [ #o #k * 196  * #tr #s' whd in ⊢ (% → ?); >E0_left <(E0_right tr)#AFTER197 %{tr} %{s'} cases (inv s') in AFTER ⊢ %; #AFTER % /3/ cases AFTER220  * #tr #s' whd in ⊢ (% → ?); #ASSERT cases (assert_nz_inv … ASSERT) * #H #AFTER 221 %{tr} %{s'} % [1,3: % [1,3: /2/  *: >H /4 by notb_Prop, absurd, nmk, I/ ] *: /2/ ] 198 222  #m * 199 223 ] … … 205 229 ∃tr,s'. is_final … exec g s = None ? ∧ 206 230 step ?? exec g s = Value … 〈tr,s'〉 ∧ 207 bool_to_Prop (inv s') ∧P tr s'.231 P tr s'. 208 232 #O #I #exec #g #inv #P #s #AFTER 209 233 cases (after_1_of_n_steps … AFTER) 210 #tr * #s' * * * #NF #STEP #INV #FIN %{tr} %{s'} % [% [%]] // whd in FIN; >E0_right in FIN; //234 #tr * #s' * * * #NF #STEP #INV #FIN %{tr} %{s'} % [%] // whd in FIN; >E0_right in FIN; // 211 235 qed. 212 236 … … 477 501  #m #IH #O #I #fx #g #s #trace #s' #EXEC 478 502 cases (exec_steps_S … EXEC) #NOTFINAL * #tr1 * #s1 * #tl * * #E1 #STEP #STEPS 479 @(after_n_m 1 … (IH … STEPS)) 503 @(after_n_m 1 … (IH … STEPS)) // 480 504 whd >NOTFINAL whd >STEP whd %{(refl ??)} #tr'' #s'' #E destruct % 481 505 ] qed. … … 484 508 exec_steps n O I fx g s = OK ? 〈trace,s'〉 → 485 509 all ? (λstr. inv (\fst str)) (tail … trace) → 486 inv s' →487 510 P (gather_trace ? trace) s' → 488 511 after_n_steps n O I fx g s inv P. 489 512 #n elim n 490 513 [ #O #I #fx #g #s #trace #s' #inv #P #EXEC whd in EXEC:(??%?); destruct 491 #ALL # FI #p whd @p514 #ALL #p whd @p 492 515  #m #IH #O #I #fx #g #s #trace #s' #inv #P #EXEC 493 516 cases (exec_steps_S … EXEC) #NOTFINAL * #tr1 * #s1 * #tl * * #E1 #STEP #STEPS 494 517 destruct 495 #ALL #FALL cut (bool_to_Prop (inv s1) ∧ bool_to_Prop (all ? (λst. inv (\fst st)) (tail … tl)))518 #ALL cut ((notb (eqb m 0) → bool_to_Prop (inv s1)) ∧ bool_to_Prop (all ? (λst. inv (\fst st)) (tail … tl))) 496 519 [ cases m in STEPS; 497 [ whd in ⊢ (??%? → ?); #E destruct /2/520 [ whd in ⊢ (??%? → ?); #E destruct % [ * #H cases (H (refl ??))  /2/ ] 498 521  #m' #STEPS cases (exec_steps_S … STEPS) #_ * #tr'' * #s'' * #tl'' * * #E #_ #_ destruct 499 whd in ALL:(?%); cases (inv s1) in ALL ⊢ %; /2/522 whd in ALL:(?%); cases (inv s1) in ALL ⊢ %; [ /2/  * ] 500 523 ] 501 524 ] * #i1 #itl 502 #p @(after_n_m 1 … (λtr,s. P (tr1⧺tr) s) … (IH … STEPS itl ? ?))525 #p @(after_n_m 1 … (λtr,s. P (tr1⧺tr) s) … (IH … STEPS itl ?)) 503 526 [ @p 504  @ FALL505  whd >NOTFINAL whd >STEP whd >i1 whd%{(refl ??)} #tr'' #s'' #p' @p'527  @i1 528  whd >NOTFINAL whd >STEP whd %{(refl ??)} #tr'' #s'' #p' @p' 506 529 ] 507 530 ] qed.
Note: See TracChangeset
for help on using the changeset viewer.