Changeset 2668
 Timestamp:
 Feb 15, 2013, 11:27:56 AM (6 years ago)
 Location:
 src
 Files:

 5 edited
Legend:
 Unmodified
 Added
 Removed

src/Clight/test/trivial.test.ma
r2645 r2668 113 113 example ms : 114 114 let 〈p0,init〉 ≝ clight_label myprog in 115 measurable Clight_pcs p0 14 (λfn. 1) 1.115 measurable Clight_pcs p0 0 4 (λfn. 1) 1. 116 116 whd whd in match (state ????); 117 % [2: % [2: % [2: % [2: 117 % [2: % [2: % [2: % [2: % [2: 118 118 @poke 119 119 [ @poke 120 120 [ @poke 121 121 [ @poke 122 [ whd in ⊢ (??%?); % 123  whd in ⊢ (??%? → ??%?); #E destruct % 122 [ @poke 123 [ % 124  whd in ⊢ (??%? → ??%?); #E destruct % 125 ] 126  * #E1 #E2 whd in E1:(??%?); destruct whd in E2:(??%?); destruct % 124 127 ] 125  * #E1 #E2 whd in E1:(??%?); destruct whd in E2:(??%?); destruct128  * * #E1 #E2 #E3 whd in E1:(??%?); destruct whd in E2:(??%?); destruct whd in E3:(??%?); destruct 126 129 whd %[2: % [2: %{[?]} [2: %[2: %[2: %[2: %[ %[ %  whd % ] whd in ⊢ (??%?); % ] 127 130 skip]skip]skip]skip]skip]skip] 128 131 ] 129  * * #E1 #E2 #_ whd in E1:(??%?); destruct whd in E2:(??%?); destruct132  * * * #E1 #E2 #E3 #_ whd in E1:(??%?); destruct whd in E2:(??%?); destruct whd in E3:(??%?); destruct 130 133 whd % 131 134 ] 132  * * * #E1 #E2 #_ #_ whd in E1:(??%?); destruct whd in E2:(??%?); destruct135  * * * * #E1 #E2 #E3 #_ #_ whd in E1:(??%?); destruct whd in E2:(??%?); destruct whd in E3:(??%?); destruct 133 136 whd in ⊢ (?%?); // 134 137 ] qed. 
src/common/ErrorMessages.ma
r2646 r2668 64 64  FinalState : ErrorMessage 65 65  EmptyStack: ErrorMessage 66  OutOfBounds: ErrorMessage. 66  OutOfBounds: ErrorMessage 67  UnexpectedIO : ErrorMessage 68  TerminatedEarly : ErrorMessage. 
src/common/FEMeasurable.ma
r2644 r2668 16 16 ms_stack : ∀g1,g2. ms_inv g1 g2 → (ident → nat); 17 17 ms_rel : ∀g1,g2. ∀INV:ms_inv g1 g2. state … ms_C1 g1 → state … ms_C2 g2 → Prop; 18 ms_rel_normal : ∀g1,g2,INV,s1,s2. ms_rel g1 g2 INV s1 s2 → bool_to_Prop (normal_state ms_C1 g1 s1) ↔ bool_to_Prop (normal_state ms_C2 g2 s2); 19 ms_rel_labelled : ∀g1,g2,INV,s1,s2. ms_rel g1 g2 INV s1 s2 → bool_to_Prop (pcs_labelled ms_C1 g1 s1) ↔ bool_to_Prop (pcs_labelled ms_C2 g2 s2); 18 20 sim_normal : 19 21 ∀g1,g2. … … 129 131 ] qed. 130 132 131 (* WIP commented out 133 lemma stack_labelled_step : ∀C:preclassified_system. ∀g,s1,trace,s2,stack,current. 134 exec_steps 1 io_out io_in C g s1 = OK ? 〈trace,s2〉 → 135 pcs_labelled C g s1 → 136 stack_after (pcs_to_cs C g stack) current trace = current. 137 #C #g #s1 #trace #s2 #stack #current #EXEC 138 cases (exec_steps_S … EXEC) 139 #NF * #tr * #s' * #tl * * #Etr #STEP #EXEC' whd in EXEC':(??%?); destruct 140 #CS 141 whd in ⊢ (??%?); whd in match (cs_classify ??); >CS 142 143 144 (* WIP commented out*) 132 145 lemma prefix_preserved : 133 146 ∀MS:meas_sim. 134 ∀g 1,g2.135 ∀INV:ms_inv MS g 1 g2.147 ∀g,g'. 148 ∀INV:ms_inv MS g g'. 136 149 ∀max_allowed_stack. 137 ∀s1,s1',tr,tr'. 138 ms_rel MS g1 g2 INV s1 s1' → 150 ∀s1,s1'. 151 ms_rel MS g g' INV s1 s1' → 152 153 ∀m,prefix,sf. 154 exec_steps m … (pcs_exec … (ms_C1 MS)) g s1 = OK ? 〈prefix,sf〉 → 155 le (max_stack (pcs_to_cs (ms_C1 MS) ? (ms_stack MS … INV)) 0 prefix) max_allowed_stack → 156 157 ∃m',prefix',sf'. 158 exec_steps m' … (pcs_exec … (ms_C2 MS)) g' s1' = OK ? 〈prefix',sf'〉 ∧ 159 le (max_stack (pcs_to_cs (ms_C2 MS) ? (ms_stack MS … INV)) 0 prefix') max_allowed_stack ∧ 139 160 140 let trace ≝ (exec_inf_aux ?? (pcs_exec … (ms_C1 MS)) g1 (Value … 〈tr,s1〉)) in 141 let trace' ≝ (exec_inf_aux ?? (pcs_exec … (ms_C2 MS)) g2 (Value … 〈tr',s1'〉)) in 142 143 ∀m,prefix,suffix. 144 split_trace … trace m = Some ? 〈prefix,suffix〉 → 145 le (max_stack (pcs_to_cs (ms_C1 MS) ? (ms_stack MS … INV)) prefix) max_allowed_stack → 146 147 ∃m',prefix',suffix'. 148 split_trace … trace' m' = Some ? 〈prefix',suffix'〉 ∧ 149 le (max_stack (pcs_to_cs (ms_C2 MS) ? (ms_stack MS … INV)) prefix') max_allowed_stack ∧ 150 151 ∃s2,s2',tr2,tr2'. 152 suffix = exec_inf_aux ?? (pcs_exec … (ms_C1 MS)) g1 (Value … 〈tr2,s2〉) ∧ 153 suffix' = exec_inf_aux ?? (pcs_exec … (ms_C2 MS)) g2 (Value … 〈tr2',s2'〉) ∧ 154 ms_rel MS g1 g2 INV s2 s2'. 155 * #C1 #C2 #compiled #inv #stack #rel #sim_normal #sim_call_return #sim_cost #sim_init 156 #g1 #g2 #INV #max #s1 #s1' #tr #tr' #REL 157 letin trace ≝ (exec_inf_aux ?????) 158 letin trace' ≝ (exec_inf_aux ?????) 159 #m0 161 ms_rel MS g g' INV sf sf'. 162 * #C1 #C2 #compiled #inv #stack #rel #rel_normal #rel_labelled #sim_normal #sim_call_return #sim_cost #sim_init 163 #g #g' #INV #max #s1 #s1' #REL 164 #m0 generalize in match s1' in REL ⊢ %; generalize in match s1; s1 s1' 165 generalize in match 0; (* current stack level *) 160 166 @(nat_elim1 m0) 161 167 * 162 [ #_ #prefix #suffix #split whd in split:(??%?); destruct 163 #max_ok %{0} %{[]} %{trace'} 164 % [ % //  %{s1} %{s1'} %{tr} %{tr'} /3/ ] 165  * 166 [ (* m = 1; just extracts the current state *) 167 #_ #prefix #suffix #split #max_ok 168 cases (split_trace_1 … split) #E1 #foo 169 %{1} %{[〈tr',s1'〉]} %{(exec_inf_aux … (step … s1'))} 170 % [ % 171 #m #IH #prefix #suffix #split #max_ok 172 (* clean up first step? *) 168 [ #_ #current_stack #s1 #s1' #REL #prefix #sf #exec whd in exec:(??%?); destruct 169 #max_ok %{0} %{[]} %{s1'} 170 % [ % //  // ] 171  #m #IH #current_stack #s1 #s1' #REL #prefix #sf #exec #max_ok 173 172 cases (true_or_false_Prop … (pcs_labelled … s1)) 174 [ #CS cases (split_trace_S … split) #trace1 * #Etrace * 175 [ * #notfinal #split1 176 lapply (sim_cost … REL CS) 173 [ #CS 174 cases (exec_steps_split 1 … exec) #trace1 * #trace2 * #s2 * * #EXEC1 #EXEC2 #E1 175 lapply (sim_cost … s2 ? REL CS ?) 176 [ @(exec_steps_after_n_noinv … EXEC1) %  skip ] 177 #AFTER' 178 cases (after_n_exec_steps … AFTER') 179 #prefix' * #s2' * #EXEC1' * #Etrace #R2 180 cases (IH m ? (stack_after (pcs_to_cs C2 … (stack … INV)) current_stack prefix') … R2 … EXEC2 ?) 181 [ 2: //  3: @(transitive_le … max_ok) >E1 <max_stack_append 182 183 @le_maxr 184 #m'' * #prefix'' * #sf'' * * #EXEC'' #MAX'' #R'' 185 %{(1+m'')} %{(prefix'@prefix'')} %{sf''} 186 % [ % [ @(exec_steps_join … EXEC1') @EXEC''  cases daemon ]  @R2 187  188 %{trace1 } 189 190 cases (exec_steps_S … exec) #notfinal * #tr' * #s' * #tl * * #E #STEP #EXEC' 191 cases (true_or_false_Prop … (pcs_labelled … s1)) 192 [ #CS lapply (sim_cost … s' tr' REL CS ?) 193 [ @(exec_steps_after_n_noinv … whd >notfinal whd >STEP whd % ] 194 #AFTER %{1} 177 195 [ 3: whd in match (after_n_steps ????? s1 ??); 178 196 >(?:is_final ???? s1 = None ?) [ whd in ⊢ ((% → ?) → ?); 
src/common/Measurable.ma
r2618 r2668 25 25 λC,x. ∃tr1,s1,x',tr2,s2,s3. x = 〈tr1,s1〉::(x'@[〈tr2,s2〉;〈E0,s3〉]) ∧ bool_to_Prop (cs_labelled C s1) ∧ cs_classify C s2 = cl_return. 26 26 27 definition measure_stack : ∀C. execution_prefix (cs_state … C) → nat × nat ≝ 28 λC. 29 foldl … (λx, trs. 27 definition measure_stack_aux ≝ 28 λC. (λx. λtrs:trace × (cs_state … C). 30 29 let 〈current,max_stack〉 ≝ x in 31 30 let 〈tr,s〉 ≝ trs in … … 36 35  _ ⇒ λ_. current 37 36 ] (cs_stack C s) in 38 〈new, max max_stack new〉) 〈0,0〉. 39 40 definition stack_after : ∀C. execution_prefix (cs_state … C) → nat ≝ 41 λC,x. \fst (measure_stack C x). 42 43 definition max_stack : ∀C. execution_prefix (cs_state … C) → nat ≝ 44 λC,x. \snd (measure_stack C x). 37 〈new, max max_stack new〉). 38 39 definition measure_stack : ∀C. nat → execution_prefix (cs_state … C) → nat × nat ≝ 40 λC,current. 41 foldl … (measure_stack_aux C) 〈current,0〉. 42 43 definition stack_after : ∀C. nat → execution_prefix (cs_state … C) → nat ≝ 44 λC,current,x. \fst (measure_stack C current x). 45 46 definition max_stack : ∀C. nat → execution_prefix (cs_state … C) → nat ≝ 47 λC,current,x. \snd (measure_stack C current x). 48 49 lemma foldl_inv : ∀A,B. ∀P:A → Prop. ∀f. 50 (∀acc,el. P acc → P (f acc el)) → 51 ∀l,acc. P acc → 52 P (foldl A B f acc l). 53 #A #B #P #f #IH #l elim l 54 [ // 55  #h #t #IH' #acc #H @IH' @IH @H 56 ] qed. 57 58 lemma max_stack_step : ∀C,a,m,a',m',tr,s. 59 measure_stack_aux C 〈a,m〉 〈tr,s〉 = 〈a',m'〉 → 60 m' = max m a'. 61 #C #a #m #a' #m' #tr #s 62 whd in match (measure_stack_aux ???); 63 generalize in match (cs_stack C s); cases (cs_classify C s) #f 64 normalize nodelta #E destruct // 65 qed. 66 67 lemma max_stack_step' : ∀C,a,a1',a2',m1,m1',m2,m2',trs. 68 measure_stack_aux C 〈a,m1〉 trs = 〈a1',m1'〉 → 69 measure_stack_aux C 〈a,m2〉 trs = 〈a2',m2'〉 → 70 a1' = a2'. 71 #C #a #a1' #a2' #m1 #m2 #m1' #m2' * #tr #s 72 whd in match (measure_stack_aux ???); whd in match (measure_stack_aux ???); 73 generalize in match (cs_stack C s); cases (cs_classify C s) #f 74 normalize nodelta 75 #E1 #E2 destruct 76 % 77 qed. 78 79 (* TODO: move*) 80 lemma max_O_n : ∀n. max O n = n. 81 * // 82 qed. 83 84 lemma max_n_O : ∀n. max n O = n. 85 * // 86 qed. 87 88 lemma associative_max : associative nat max. 89 #n #m #o normalize 90 @(leb_elim n m) 91 [ normalize @(leb_elim m o) normalize #H1 #H2 92 [ >(le_to_leb_true n o) /2/ 93  >(le_to_leb_true n m) // 94 ] 95  normalize @(leb_elim m o) normalize #H1 #H2 96 [ % 97  >(not_le_to_leb_false … H2) 98 >(not_le_to_leb_false n o) // @lt_to_not_le @(transitive_lt … m) /2/ 99 ] 100 ] qed. 101 102 103 lemma max_stack_steps : ∀C,trace,a,m. 104 \snd (foldl … (measure_stack_aux C) 〈a,m〉 trace) = 105 max m (\snd (foldl … (measure_stack_aux C) 〈a,0〉 trace)). 106 #C #trace elim trace 107 [ #a #m >max_n_O % 108  * #tr #s #tl #IH #a #m 109 whd in match (foldl ?????); 110 letin x ≝ (measure_stack_aux ???) lapply (refl ? x) cases x in ⊢ (???% → %); #a' #m' #M 111 whd in match (foldl ??? 〈a,O〉 ?); 112 letin y ≝ (measure_stack_aux ? 〈a,O〉 ?) lapply (refl ? y) cases y in ⊢ (???% → %); #a'' #m'' #M' 113 >(IH a'') >IH 114 >(max_stack_step … M) 115 >(max_stack_step … M') >max_O_n >(max_stack_step' … M M') >associative_max % 116 ] qed. 117 118 (* 119 lemma max_stack_step : ∀C,a,m,tr,s. 120 m ≤ \snd (measure_stack_aux C 〈a,m〉 〈tr,s〉). 121 #C #a #m #tr #s 122 whd in match (measure_stack_aux ???); 123 generalize in match (cs_stack C s); cases (cs_classify C s) normalize 124 #f @(leb_elim m) normalize #H /2/ 125 qed. 126 127 lemma max_stack_steps : ∀C. ∀am. ∀trace. 128 \snd am ≤ \snd (foldl … (measure_stack_aux C) am trace). 129 #C * #a #m #trace 130 @foldl_inv 131 [ * #a' #m' * #tr #s #H @(transitive_le … H) @max_stack_step 132  // 133 ] qed. 134 135 lemma max_stack_step' : ∀C,a,m,a',m',tr,s. 136 a ≤ a' → m ≤ m' → 137 \snd (measure_stack_aux C 〈a,m〉 〈tr,s〉) ≤ \snd (measure_stack_aux C 〈a',m'〉 〈tr,s〉). 138 #C #a #m #a' #m' #tr #s #H1 #H2 139 whd in match (measure_stack_aux ???);whd in match (measure_stack_aux ???); 140 generalize in match (cs_stack C s); cases (cs_classify C s) #f 141 whd in ⊢ (?(??%)(??%)); 142 [ @to_max [ @(transitive_le … m') /2/  @(transitive_le … (a'f I)) /2/ ] 143  2,4,5: @to_max /2 by max_r, max_l/ 144  @to_max [ @(transitive_le … m') /2/  @(transitive_le … (a'+f I)) /2/ ] 145 ] qed. 146 147 lemma max_stack_step'' : ∀C,a,m,a',m',tr,s. 148 a ≤ a' → 149 \fst (measure_stack_aux C 〈a,m〉 〈tr,s〉) ≤ \fst (measure_stack_aux C 〈a',m'〉 〈tr,s〉). 150 #C #a #m #a' #m' #tr #s #H1 151 whd in match (measure_stack_aux ???);whd in match (measure_stack_aux ???); 152 generalize in match (cs_stack C s); cases (cs_classify C s) #f 153 whd in ⊢ (?%%); /2/ 154 qed. 155 156 lemma max_stack_steps' : ∀C. ∀trace,am,am'. 157 \fst am ≤ \fst am' → \snd am ≤ \snd am' → 158 \snd (foldl … (measure_stack_aux C) am trace) ≤ \snd (foldl … (measure_stack_aux C) am' trace). 159 #C #trace elim trace 160 [ * #a #m * #a' #m' #H1 #H2 @H2 161  * #tr #s #tl #IH * #a #m * #a' #m' #H1 #H2 @IH [ @max_stack_step'' //  @max_stack_step' // ] 162 ] qed. 163 164 lemma max_stack_append_l : ∀C,ex1,ex2. 165 max_stack C ex1 ≤ max_stack C (ex1@ex2). 166 #C #ex1 #ex2 whd in ⊢ (??%); 167 whd in match (measure_stack ? (ex1@ex2)); 168 >foldl_append 169 @max_stack_steps 170 qed. 171 172 lemma max_stack_append_r : ∀C,ex1,ex2. 173 max_stack C ex2 ≤ max_stack C (ex1@ex2). 174 #C #ex1 #ex2 whd in ⊢ (??%); 175 whd in match (measure_stack ? (ex1@ex2)); 176 >foldl_append 177 @max_stack_steps' // 178 qed. 179 *)(* 180 lemma max_stack_append : ∀C,ex1,ex2. 181 max (max_stack C ex1) (max_stack C ex2) = max_stack C (ex1@ex2). 182 #C #ex1 #ex2 183 whd in match (max_stack ??); whd in match (max_stack ? (ex1@ex2)); 184 whd in match (measure_stack ??); whd in match (measure_stack ? (ex1@ex2)); 185 generalize in match 〈O,O〉; elim ex1 186 [ * #a #m whd in ⊢ (??(?%?)%); >max_stack_steps 187 188 elim ex1 189 [ #ex2 >max_O_n % 190  * #tr #s #tl #IH #ex2 191 whd in match (max_stack ??); whd in match (measure_stack ??); 192 lapply (refl ? (measure_stack_aux C 〈O,O〉 〈tr,s〉)) 193 cases (measure_stack_aux ???) in ⊢ (???% → %); 194 #a #m #M 195 196 #ex2 197 @le_to_le_to_eq 198 [ @to_max // 199  200 whd in ⊢ (???%); 201 202 whd in match (measure_stack ? (ex1@ex2)); 203 >foldl_append 204 @max_stack_steps' // 205 *) 206 lemma max_stack_append : ∀C,c1,ex1,ex2. 207 max (max_stack C c1 ex1) (max_stack C (stack_after C c1 ex1) ex2) = max_stack C c1 (ex1@ex2). 208 #C #c1 #ex1 #ex2 209 whd in match (max_stack ???); whd in match (stack_after ???); 210 whd in match (max_stack ?? (ex1@ex2)); 211 whd in match (measure_stack ???); whd in match (measure_stack ?? (ex1@ex2)); 212 generalize in match O; generalize in match c1; elim ex1 213 [ #c #m whd in ⊢ (??(?%?)%); >max_stack_steps % 214  * #tr #s #tl #IH #c #m 215 whd in match (foldl ?????); whd in ⊢ (???(???%)); 216 lapply (refl ? (measure_stack_aux C 〈c1,m〉 〈tr,s〉)) 217 cases (measure_stack_aux ???) in ⊢ (???% → %); #a' #m' #M 218 >IH % 219 ] qed. 220 45 221 46 222 (* Check that the trace ends with the return from the starting function and one … … 90 266 (ident → nat) (* stack cost *) → 91 267 nat → Prop ≝ 92 λC,p,m,n,stack_cost,max_allowed_stack. ∃prefix,suffix,interesting,remainder. 93 let C' ≝ pcs_to_cs C (make_global … p) stack_cost in 94 let cl_trace ≝ exec_inf … (cs_exec … C') p in 95 split_trace … cl_trace m = Some ? 〈prefix,suffix〉 ∧ 96 split_trace … suffix n = Some ? 〈interesting,remainder〉 ∧ 268 λC,p,m,n,stack_cost,max_allowed_stack. ∃s0,prefix,s1,interesting,s2. 269 let g ≝ make_global … (pcs_exec … C) p in 270 let C' ≝ pcs_to_cs C g stack_cost in 271 make_initial_state … p = OK ? s0 ∧ 272 exec_steps m ?? (cs_exec … C') g s0 = OK ? 〈prefix,s1〉 ∧ 273 exec_steps n ?? (cs_exec … C') g s1 = OK ? 〈interesting,s2〉 ∧ 97 274 trace_is_label_to_return C' interesting ∧ 98 275 bool_to_Prop (will_return' C' interesting) ∧ 99 le (max_stack C' (prefix@interesting)) max_allowed_stack.100 101 (* TODO: probably ought to be elsewhere 276 le (max_stack C' 0 (prefix@interesting)) max_allowed_stack. 277 278 (* TODO: probably ought to be elsewhere; use exec_steps instead 102 279 103 280 Note that this does not include stack space 
src/common/SmallstepExec.ma
r2618 r2668 183 183 lemma after_1_of_n_steps : ∀n,O,I,exec,g,inv,P,s. 184 184 after_n_steps (S n) O I exec g s inv P → 185 ∃tr,s'. step ?? exec g s = Value … 〈tr,s'〉 ∧ 185 ∃tr,s'. 186 is_final … exec g s = None ? ∧ 187 step … exec g s = Value … 〈tr,s'〉 ∧ 186 188 bool_to_Prop (inv s') ∧ 187 189 after_n_steps n O I exec g s' inv (λtr'',s''. P (tr⧺tr'') s''). … … 193 195 [ #o #k * 194 196  * #tr #s' whd in ⊢ (% → ?); >E0_left <(E0_right tr) #AFTER 195 %{tr} %{s'} cases (inv s') in AFTER ⊢ %; #AFTER % / 2/ cases AFTER197 %{tr} %{s'} cases (inv s') in AFTER ⊢ %; #AFTER % /3/ cases AFTER 196 198  #m * 197 199 ] … … 201 203 lemma after_1_step : ∀O,I,exec,g,inv,P,s. 202 204 after_n_steps 1 O I exec g s inv P → 203 ∃tr,s'. step ?? exec g s = Value … 〈tr,s'〉 ∧ bool_to_Prop (inv s') ∧ P tr s'. 205 ∃tr,s'. is_final … exec g s = None ? ∧ 206 step ?? exec g s = Value … 〈tr,s'〉 ∧ 207 bool_to_Prop (inv s') ∧ P tr s'. 204 208 #O #I #exec #g #inv #P #s #AFTER 205 209 cases (after_1_of_n_steps … AFTER) 206 #tr * #s' * * #STEP #INV #FIN %{tr} %{s'} % [%] // whd in FIN; >E0_right in FIN; //210 #tr * #s' * * * #NF #STEP #INV #FIN %{tr} %{s'} % [%[%]] // whd in FIN; >E0_right in FIN; // 207 211 qed. 208 212 … … 377 381 ]. 378 382 379 383 (* For now I'm doing this without I/O, to keep things simple. In the place I 384 intend to use it (the definition of measurable subtraces, and proofs using 385 that) I should allow I/O for the prefix. *) 386 387 let rec exec_steps (n:nat) O I (fx:fullexec O I) (g:global … fx) (s:state … fx g) : res (list (trace × (state … fx g)) × (state … fx g)) ≝ 388 match n with 389 [ O ⇒ return 〈[ ], s〉 390  S m ⇒ 391 match is_final … fx g s with 392 [ Some r ⇒ Error … (msg TerminatedEarly) 393  None ⇒ 394 match step … fx g s with 395 [ Value trs ⇒ 396 ! 〈tl,s'〉 ← exec_steps m O I fx g (\snd trs); 397 return 〈trs::tl, s'〉 398  Interact _ _ ⇒ Error … (msg UnexpectedIO) 399  Wrong m ⇒ Error … m 400 ] 401 ] 402 ]. 403 404 (* Show that it's nice. *) 405 406 lemma exec_steps_S : ∀O,I,fx,g,n,s,trace,s''. 407 exec_steps (S n) O I fx g s = OK … 〈trace,s''〉 → 408 is_final … fx g s = None ? ∧ 409 ∃tr',s',tl. 410 trace = 〈tr',s'〉::tl ∧ 411 step … fx g s = Value … 〈tr',s'〉 ∧ 412 exec_steps n O I fx g s' = OK … 〈tl,s''〉. 413 #O #I #fx #g #n #s #trace #s'' 414 whd in ⊢ (??%? → ?); 415 cases (is_final … s) 416 [ whd in ⊢ (??%? → ?); 417 cases (step … s) 418 [ #o #i #EX whd in EX:(??%?); destruct 419  * #tr' #s' whd in ⊢ (??%? → ?); #EX %{(refl ??)} 420 %{tr'} %{s'} cases (exec_steps … g s') in EX ⊢ %; 421 [ * #tl #s'' #EX whd in EX:(??%?); destruct %{tl} /3/ 422  #m #EX whd in EX:(??%?); destruct 423 ] 424  #m #EX whd in EX:(??%?); destruct 425 ] 426  #r #EX whd in EX:(??%?); destruct 427 ] qed. 428 429 lemma exec_steps_length : ∀O,I,fx,g,n,s,trace,s'. 430 exec_steps n O I fx g s = OK … 〈trace,s'〉 → 431 n = trace. 432 #O #I #fx #g #n elim n 433 [ #s #trace #s' #EX whd in EX:(??%?); destruct % 434  #m #IH #s #trace #s' #EX 435 cases (exec_steps_S … EX) #notfinal * #tr' * #s'' * #tl * * #Etl #Estep #steps 436 >(IH … steps) >Etl % 437 ] qed. 438 439 lemma exec_steps_nonterm : ∀O,I,fx,g,n,s,h,t,s'. 440 exec_steps n O I fx g s = OK … 〈h::t,s'〉 → 441 is_final … s = None ?. 442 #O #I #fx #g #n #s #h #t #s' #EX 443 lapply (exec_steps_length … EX) 444 #Elen destruct whd in EX:(??%?); 445 cases (is_final … s) in EX ⊢ %; 446 [ // 447  #r #EX whd in EX:(??%?); destruct 448 ] qed. 449 450 lemma exec_steps_nonterm' : ∀O,I,fx,g,n,s,h,t,s'. 451 exec_steps n O I fx g s = OK … 〈h@[t], s'〉 → 452 is_final … s = None ?. 453 #O #I #fx #g #n #s * [2: #h1 #h2] #t #s' @exec_steps_nonterm 454 qed. 455 456 let rec gather_trace S (l:list (trace × S)) on l : trace ≝ 457 match l with 458 [ nil ⇒ E0 459  cons h t ⇒ (\fst h)⧺(gather_trace S t) 460 ]. 461 462 lemma exec_steps_after_n_simple : ∀n,O,I,fx,g,s,trace,s'. 463 exec_steps n O I fx g s = OK ? 〈trace,s'〉 → 464 after_n_steps n O I fx g s (λ_. true) (λtr,s''. 〈tr,s''〉 = 〈gather_trace ? trace,s'〉). 465 #n elim n 466 [ #O #I #fx #g #s #trace #s' #EXEC whd in EXEC:(??%?); destruct 467 whd % 468  #m #IH #O #I #fx #g #s #trace #s' #EXEC 469 cases (exec_steps_S … EXEC) #NOTFINAL * #tr1 * #s1 * #tl * * #E1 #STEP #STEPS 470 @(after_n_m 1 … (IH … STEPS)) 471 whd >NOTFINAL whd >STEP whd %{(refl ??)} #tr'' #s'' #E destruct % 472 ] qed. 473 474 lemma exec_steps_after_n : ∀n,O,I,fx,g,s,trace,s',inv,P. 475 exec_steps n O I fx g s = OK ? 〈trace,s'〉 → 476 all … (λts. inv (\snd ts)) trace → 477 P (gather_trace ? trace) s' → 478 after_n_steps n O I fx g s inv P. 479 #n elim n 480 [ #O #I #fx #g #s #trace #s' #inv #P #EXEC whd in EXEC:(??%?); destruct 481 #ALL #p whd @p 482  #m #IH #O #I #fx #g #s #trace #s' #inv #P #EXEC 483 cases (exec_steps_S … EXEC) #NOTFINAL * #tr1 * #s1 * #tl * * #E1 #STEP #STEPS 484 destruct 485 #ALL cut (bool_to_Prop (inv s1) ∧ bool_to_Prop (all … (λts. inv (\snd ts)) tl)) 486 [ whd in ALL:(?%); cases (inv s1) in ALL ⊢ %; /2/ ] * #i1 #itl 487 #p @(after_n_m 1 … (λtr,s. P (tr1⧺tr) s) … (IH … STEPS itl ?)) 488 [ @p 489  whd >NOTFINAL whd >STEP whd >i1 whd %{(refl ??)} #tr'' #s'' #p' @p' 490 ] 491 ] qed. 492 493 lemma exec_steps_after_n_noinv : ∀n,O,I,fx,g,s,trace,s',P. 494 exec_steps n O I fx g s = OK ? 〈trace,s'〉 → 495 P (gather_trace ? trace) s' → 496 after_n_steps n O I fx g s (λ_.true) P. 497 #n #O #I #fx #g #s #trace #s' #P #EXEC #p 498 @(exec_steps_after_n … EXEC) // 499 elim trace /2/ 500 qed. 501 502 lemma after_n_exec_steps : ∀n,O,I. ∀fx:fullexec O I. ∀g,s,inv,P. 503 after_n_steps n O I fx g s inv P → 504 ∃trace,s'. exec_steps n O I fx g s = OK ? 〈trace,s'〉 ∧ P (gather_trace ? trace) s'. 505 #n elim n 506 [ #O #I #fx #g #s #inv #P #AFTER %{[ ]} %{s} %{(refl ??)} @AFTER 507  #m #IH #O #I #fx #g #s #inv #P #AFTER 508 cases (after_1_of_n_steps … AFTER) 509 #tr1 * #s1 * * * #NF #STEP #INV #AFTER' 510 cases (IH … AFTER') 511 #tl * #s' * #STEPS #p 512 %{(〈tr1,s1〉::tl)} %{s'} % 513 [ whd in ⊢ (??%?); >NF whd in ⊢ (??%?); >STEP whd in ⊢ (??%?); >STEPS %  // ] 514 ] qed. 515 516 lemma exec_steps_split : ∀n,m,O,I,fx,g,s,trace,s'. 517 exec_steps (n+m) O I fx g s = OK ? 〈trace,s'〉 → 518 ∃trace1,trace2,s1. 519 exec_steps n O I fx g s = OK ? 〈trace1,s1〉 ∧ 520 exec_steps m O I fx g s1 = OK ? 〈trace2,s'〉 ∧ 521 trace = trace1 @ trace2. 522 #n elim n 523 [ #m #O #I #fx #g #s #trace #s' #EXEC 524 %{[ ]} %{trace} %{s} /3/ 525  #n' #IH #m #O #I #fx #g #s #trace #s' #EXEC 526 cases (exec_steps_S … EXEC) #NF * #tr' * #s' * #tl * * #E1 #STEP #EXEC' 527 cases (IH … EXEC') #trace1 * #trace2 * #s1 * * #EXEC1 #EXEC2 #E2 528 %{(〈tr',s'〉::trace1)} %{trace2} %{s1} 529 % 530 [ % 531 [ whd in ⊢ (??%?); >NF >STEP whd in ⊢ (??%?); >EXEC1 % 532  @EXEC2 533 ] 534  destruct % 535 ] 536 ] qed. 537 538 lemma exec_steps_join : ∀n,m,O,I,fx,g,s1,trace1,s2,trace2,s3. 539 exec_steps n O I fx g s1 = OK ? 〈trace1,s2〉 → 540 exec_steps m O I fx g s2 = OK ? 〈trace2,s3〉 → 541 exec_steps (n+m) O I fx g s1 = OK ? 〈trace1@trace2,s3〉. 542 #n elim n 543 [ #m #O #I #fx #g #s1 #trace1 #s2 #trace2 #s3 #EXEC1 #EXEC2 544 whd in EXEC1:(??%?); destruct @EXEC2 545  #n' #IH #m #O #I #fx #g #s1 #trace1 #s2 #trace2 #s3 #EXEC1 #EXEC2 546 cases (exec_steps_S … EXEC1) #NF * #tr' * #s' * #tl' * * #E1 #STEP #EXEC' 547 whd in ⊢ (??%?); >NF >STEP whd in ⊢ (??%?); >(IH … EXEC' EXEC2) 548 destruct % 549 ] qed. 550 551 (* Show that it corresponds to split_trace … (exec_inf …) *) 552 553 lemma exec_steps_inf_aux : ∀O,I. ∀fx:fullexec O I. ∀g,n,s,trace,s'. 554 exec_steps n O I fx g s = OK ? 〈trace,s'〉 → 555 match is_final … s' with 556 [ None ⇒ split_trace … (exec_inf_aux … fx g (step … fx g s)) n = Some ? 〈trace, exec_inf_aux … fx g (step … s')〉 557  Some r ⇒ n = 0 ∨ ∃tr'. split_trace … (exec_inf_aux … fx g (step … fx g s)) n = Some ? 〈trace, e_stop … tr' r s'〉 558 ]. 559 #O #I #fx #g #n elim n 560 [ #s #trace #s' #EX whd in EX:(??%%); destruct 561 cases (is_final … s') [ %  #r %1 % ] 562  #m #IH #s #trace #s' #EX 563 cases (exec_steps_S … EX) 564 #notfinal * #tr'' * #s'' * #tl * * #Etrace #Estep #Esteps 565 cases tl in Etrace Esteps ⊢ %; 566 [ #E destruct #Esteps 567 lapply (exec_steps_length … Esteps) #Elen normalize in Elen; destruct 568 whd in Esteps:(??%?); destruct 569 >Estep 570 >exec_inf_aux_unfold normalize nodelta 571 cases (is_final … s') 572 [ % 573  #r %2 %{tr''} % 574 ] 575  * #tr1 #s1 #tl1 #E normalize in E; destruct #Esteps 576 lapply (IH … Esteps) cases (is_final … s') 577 [ normalize nodelta #IH' >Estep >exec_inf_aux_unfold whd in ⊢ (??(????%?)?); 578 >(exec_steps_nonterm … Esteps) whd in ⊢ (??%?); >IH' % 579  normalize nodelta #r * 580 [ #E @⊥ >(exec_steps_length … Esteps) in E; #E normalize in E; destruct 581  * #tr'' #IH' %2 %{tr''} >Estep >exec_inf_aux_unfold whd in ⊢ (??(????%?)?); 582 >(exec_steps_nonterm … Esteps) whd in ⊢ (??%?); >IH' % 583 ] 584 ] 585 ] 586 ] qed.
Note: See TracChangeset
for help on using the changeset viewer.