[700] | 1 | include "Clight/CexecComplete.ma". |
---|
| 2 | include "Clight/CexecSound.ma". |
---|
| 3 | include "utilities/extralib.ma". |
---|
[398] | 4 | |
---|
[487] | 5 | include "basics/jmeq.ma". |
---|
[1352] | 6 | include alias "basics/logic.ma". |
---|
[399] | 7 | |
---|
[398] | 8 | (* A "single execution" - where all of the input values are made explicit. *) |
---|
[487] | 9 | coinductive s_execution : Type[0] ≝ |
---|
[1713] | 10 | | se_stop : trace → int → s_execution |
---|
[398] | 11 | | se_step : trace → state → s_execution → s_execution |
---|
[797] | 12 | | se_wrong : errmsg → s_execution |
---|
[700] | 13 | | se_interact : ∀o:io_out. (io_in o → execution state io_out io_in) → io_in o → s_execution → s_execution. |
---|
[398] | 14 | |
---|
[700] | 15 | coinductive single_exec_of : execution state io_out io_in → s_execution → Prop ≝ |
---|
[1713] | 16 | | seo_stop : ∀tr,r,s. single_exec_of (e_stop ??? tr r s) (se_stop tr r) |
---|
[398] | 17 | | seo_step : ∀tr,s,e,se. |
---|
| 18 | single_exec_of e se → |
---|
[700] | 19 | single_exec_of (e_step ??? tr s e) (se_step tr s se) |
---|
[797] | 20 | | seo_wrong : ∀msg:errmsg. single_exec_of (e_wrong ??? msg) (se_wrong msg) |
---|
[398] | 21 | | seo_interact : ∀o,k,i,se. |
---|
| 22 | single_exec_of (k i) se → |
---|
[700] | 23 | single_exec_of (e_interact ??? o k) (se_interact o k i se). |
---|
[398] | 24 | |
---|
| 25 | (* starting after state s, zero or more steps of execution e reach state s' |
---|
| 26 | after which comes e'. *) |
---|
[487] | 27 | inductive execution_isteps : trace → state → s_execution → state → s_execution → Prop ≝ |
---|
[398] | 28 | | isteps_none : ∀s,e. execution_isteps E0 s e s e |
---|
| 29 | | isteps_one : ∀e,e',tr,tr',s,s',s0. |
---|
| 30 | execution_isteps tr' s e s' e' → |
---|
| 31 | execution_isteps (tr⧺tr') s0 (se_step tr s e) s' e' |
---|
| 32 | | isteps_interact : ∀e,e',o,k,i,s,s',s0,tr,tr'. |
---|
| 33 | execution_isteps tr' s e s' e' → |
---|
| 34 | execution_isteps (tr⧺tr') s0 (se_interact o k i (se_step tr s e)) s' e'. |
---|
| 35 | |
---|
[487] | 36 | lemma isteps_trans: ∀tr1,tr2,s1,s2,s3,e1,e2,e3. |
---|
[398] | 37 | execution_isteps tr1 s1 e1 s2 e2 → |
---|
| 38 | execution_isteps tr2 s2 e2 s3 e3 → |
---|
| 39 | execution_isteps (tr1⧺tr2) s1 e1 s3 e3. |
---|
[487] | 40 | #tr1 #tr2 #s1 #s2 #s3 #e1 #e2 #e3 #H1 elim H1; |
---|
| 41 | [ #s #e //; |
---|
| 42 | | #e #e' #tr #tr' #s1' #s2' #s3' #H1 #H2 #H3 |
---|
| 43 | >(Eapp_assoc …) |
---|
| 44 | @isteps_one |
---|
| 45 | @H2 @H3 |
---|
| 46 | | #e #e' #o #k #i #s1' #s2' #s3' #tr #tr' #H1 #H2 #H3 |
---|
| 47 | >(Eapp_assoc …) |
---|
| 48 | @isteps_interact |
---|
[398] | 49 | /2/ |
---|
[487] | 50 | ] qed. |
---|
[398] | 51 | |
---|
[702] | 52 | lemma is_final_elim: ∀s.∀P:option int → Type[0]. |
---|
| 53 | (∀r. final_state s r → P (Some ? r)) → |
---|
| 54 | ((¬∃r.final_state s r) → P (None ?)) → |
---|
[891] | 55 | P (is_final s). |
---|
| 56 | #s #P #F #NF lapply (refl ? (is_final s)) |
---|
[1516] | 57 | cases (is_final s) in ⊢ (???% → %); |
---|
| 58 | [ #E @NF % * #r #H whd in E:(??%?); > (is_final_complete … H) in E; #H destruct |
---|
[708] | 59 | | #r #E @F @is_final_sound @E |
---|
[702] | 60 | ] qed. |
---|
| 61 | |
---|
[1244] | 62 | lemma is_final_elim': ∀ge,s.∀P:option int → Type[0]. |
---|
[891] | 63 | (∀r. final_state s r → P (Some ? r)) → |
---|
| 64 | ((¬∃r.final_state s r) → P (None ?)) → |
---|
[1244] | 65 | P (is_final io_out io_in clight_fullexec ge s). |
---|
| 66 | #ge @is_final_elim qed. |
---|
[891] | 67 | |
---|
[702] | 68 | lemma exec_e_step: ∀ge,x,tr,s,e. |
---|
[732] | 69 | exec_inf_aux ?? clight_exec ge x = e_step ??? tr s e → |
---|
| 70 | exec_inf_aux ?? clight_exec ge (exec_step ge s) = e. |
---|
[702] | 71 | #ge #x #tr #s #e |
---|
[487] | 72 | >(exec_inf_aux_unfold …) cases x; |
---|
| 73 | [ #o #k #EXEC whd in EXEC:(??%?); destruct |
---|
[1516] | 74 | | #y cases y #tr' #s' whd in ⊢ (??%? → ?); |
---|
[891] | 75 | @is_final_elim' |
---|
[702] | 76 | [ #r #FINAL | #FINAL ] |
---|
[708] | 77 | #EXEC whd in EXEC:(??%?); destruct @refl |
---|
[797] | 78 | | #msg #EXEC whd in EXEC:(??%?); destruct |
---|
[487] | 79 | ] qed. |
---|
[398] | 80 | |
---|
[487] | 81 | lemma exec_e_step_inv: ∀ge,x,tr,s,e. |
---|
[732] | 82 | exec_inf_aux ?? clight_exec ge x = e_step ??? tr s e → |
---|
[398] | 83 | x = Value ??? 〈tr,s〉. |
---|
[487] | 84 | #ge #x #tr #s #e |
---|
| 85 | >(exec_inf_aux_unfold …) cases x; |
---|
| 86 | [ #o #k #EXEC whd in EXEC:(??%?); destruct |
---|
| 87 | | #y cases y; #tr' #s' whd in ⊢ (??%? → ?); |
---|
[891] | 88 | @is_final_elim' |
---|
[708] | 89 | [ #r ] #FINAL #EXEC whd in EXEC:(??%?); |
---|
| 90 | destruct @refl |
---|
[797] | 91 | | #msg #EXEC whd in EXEC:(??%?); destruct |
---|
[487] | 92 | ] qed. |
---|
[398] | 93 | |
---|
[487] | 94 | lemma exec_e_step_inv2: ∀ge,x,tr,s,e. |
---|
[732] | 95 | exec_inf_aux ?? clight_exec ge x = e_step ??? tr s e → |
---|
[398] | 96 | ¬∃r.final_state s r. |
---|
[487] | 97 | #ge #x #tr #s #e |
---|
| 98 | >(exec_inf_aux_unfold …) cases x; |
---|
| 99 | [ #o #k #EXEC whd in EXEC:(??%?); destruct |
---|
[1516] | 100 | | #y cases y; #tr' #s' whd in ⊢ (??%? → ?); |
---|
[891] | 101 | @is_final_elim' [ #r ] #F #EXEC whd in EXEC:(??%?); destruct @F |
---|
[797] | 102 | | #msg #EXEC whd in EXEC:(??%?); destruct |
---|
[487] | 103 | ] qed. |
---|
[398] | 104 | |
---|
[487] | 105 | definition exec_from : genv → state → s_execution → Prop ≝ |
---|
[732] | 106 | λge,s,se. single_exec_of (exec_inf_aux ?? clight_exec ge (exec_step ge s)) se. |
---|
[398] | 107 | |
---|
[702] | 108 | lemma se_step_eq : ∀tr,s,e,tr',s',e'. |
---|
| 109 | se_step tr s e = se_step tr' s' e' → |
---|
| 110 | tr = tr' ∧ s = s' ∧ e = e'. |
---|
[708] | 111 | #tr #s #e #tr' #s' #e' #E destruct |
---|
| 112 | % try % @refl qed. |
---|
[702] | 113 | |
---|
[487] | 114 | lemma exec_from_step : ∀ge,s,tr,s',e. |
---|
[398] | 115 | exec_from ge s (se_step tr s' e) → |
---|
| 116 | exec_step ge s = Value ??? 〈tr,s'〉 ∧ exec_from ge s' e. |
---|
[487] | 117 | #ge #s0 #tr0 #s0' #e0 #H inversion H; |
---|
| 118 | [ #tr #r #m #E1 #E2 destruct |
---|
[708] | 119 | | #tr #s #e #se #H1 #H2 #E (* destruct (E) ;*) |
---|
[1510] | 120 | cases (se_step_eq … E) * #E1 #E2 #E3 #E4 >E1 >E2 >E3 |
---|
[487] | 121 | >(exec_e_step_inv … H2) |
---|
[1516] | 122 | <(exec_e_step … H2) in H1; #H1 % // |
---|
[797] | 123 | | #msg #_ #E destruct |
---|
[487] | 124 | | #o #k #i #se #H1 #H2 #E destruct |
---|
| 125 | ] qed. |
---|
[398] | 126 | |
---|
[708] | 127 | lemma exec_from_interact : ∀ge,s,o,k,i,tr,s',e. |
---|
[398] | 128 | exec_from ge s (se_interact o k i (se_step tr s' e)) → |
---|
| 129 | step ge s tr s' ∧ |
---|
| 130 | (*exec_step ge s = Value ??? 〈tr,s'〉 ∧*) exec_from ge s' e. |
---|
[487] | 131 | #ge #s0 #o0 #k0 #i0 #tr0 #s0' #e0 #H inversion H; |
---|
| 132 | [ #tr #r #m #E1 #E2 destruct |
---|
| 133 | | #tr #s #e #se #H1 #H2 #E destruct (E) |
---|
[797] | 134 | | #msg #_ #E destruct |
---|
[1510] | 135 | | #o #k #i #se #H1 #H2 #E #X destruct (E); |
---|
[487] | 136 | lapply (exec_step_sound ge s0); |
---|
| 137 | cases (exec_step ge s0) in H2 ⊢ %; |
---|
| 138 | [ #o' #k' >(exec_inf_aux_unfold …) |
---|
[1344] | 139 | #E' whd in E':(??%??); destruct (E'); |
---|
[487] | 140 | #STEP |
---|
| 141 | inversion H1; |
---|
| 142 | [ #tr #r #m #E1 #E2 destruct |
---|
[1510] | 143 | | #tr' #s' #e' #se' #H2 #H3 #E2 #_ destruct (E2); |
---|
[1516] | 144 | <(exec_e_step … H3) in H2; #H2 % [ 2: @H2 ] |
---|
[487] | 145 | lapply (STEP i); |
---|
| 146 | >(exec_e_step_inv … H3) |
---|
| 147 | #S @S |
---|
[797] | 148 | | #msg #_ #E destruct |
---|
[487] | 149 | | #o #k #i #se #H1 #H2 #E destruct |
---|
| 150 | ] |
---|
| 151 | | #x cases x; #tr' #s' >(exec_inf_aux_unfold …) |
---|
[1344] | 152 | whd in ⊢ (??%?? → ?); @is_final_elim' |
---|
| 153 | [ #r ] #F #E whd in E:(??%??); destruct |
---|
[797] | 154 | | #msg >(exec_inf_aux_unfold …) |
---|
[1344] | 155 | #E' whd in E':(??%??); destruct (E'); |
---|
[487] | 156 | ] |
---|
[708] | 157 | ] qed. |
---|
[398] | 158 | |
---|
[1713] | 159 | lemma exec_from_interact_stop : ∀ge,s,o,k,i,tr,r. |
---|
| 160 | exec_from ge s (se_interact o k i (se_stop tr r)) → |
---|
| 161 | step ge s tr (Finalstate r). |
---|
| 162 | #ge #s0 #o0 #k0 #i0 #tr0 #r0 #H inversion H |
---|
[487] | 163 | [ #tr #r #m #E1 #E2 destruct |
---|
| 164 | | #tr #s #e #se #H1 #H2 #E destruct (E) |
---|
[797] | 165 | | #msg #_ #E destruct |
---|
[1713] | 166 | | #o #k #i #se #H1 #H2 #E #_ destruct (E) |
---|
| 167 | lapply (exec_step_sound ge s0) |
---|
[487] | 168 | >(exec_inf_aux_unfold …) in H2; |
---|
[1713] | 169 | cases (exec_step ge s0) |
---|
[487] | 170 | [ #o' #k' |
---|
[1344] | 171 | #E' whd in E':(??%??); destruct (E'); |
---|
[487] | 172 | #STEP |
---|
| 173 | inversion H1; |
---|
[1510] | 174 | [ #tr #r #m #E1 #E2 #_ lapply (STEP i); destruct; |
---|
[487] | 175 | >(exec_inf_aux_unfold …) in E1; |
---|
| 176 | cases (k' i); |
---|
[1344] | 177 | [ #o2 #k2 #E whd in E:(??%??); destruct (E) |
---|
| 178 | | #x cases x; #tr2 #s2 whd in ⊢ (??%?? → ?); |
---|
[1350] | 179 | lapply (is_final_elim s2) #IFE whd in IFE:(∀_. ? → ? → ?%); |
---|
[1521] | 180 | change with (is_final s2) in match (is_final ?????); |
---|
[891] | 181 | @IFE |
---|
[1344] | 182 | [ #r' #FINAL #E whd in E:(??%??); |
---|
[487] | 183 | destruct (E); |
---|
| 184 | inversion FINAL; |
---|
| 185 | #r'' #m'' #E1 #E2 destruct (E1 E2); //; |
---|
[1344] | 186 | | #NF #E whd in E:(??%??); destruct (E) |
---|
[487] | 187 | ] |
---|
[1344] | 188 | | #msg #E whd in E:(??%??); destruct (E) |
---|
[487] | 189 | ] |
---|
| 190 | | #tr #s #e #e' #H #EXEC #E destruct (E) |
---|
[797] | 191 | | #msg #EXEC #E destruct (E) |
---|
[487] | 192 | | #o2 #k2 #i2 #e2 #H #EXEC #E destruct (E) |
---|
| 193 | ] |
---|
[1344] | 194 | | #x cases x; #tr #s whd in ⊢ (??%?? → ?); |
---|
| 195 | @is_final_elim' [ #r ] #F #E whd in E:(??%??); destruct (E) |
---|
| 196 | | #msg #E whd in E:(??%??); destruct (E) |
---|
[487] | 197 | ] |
---|
[708] | 198 | ] qed. |
---|
[398] | 199 | |
---|
| 200 | (* NB: the E0 in the execs are irrelevant. *) |
---|
[487] | 201 | lemma several_steps: ∀ge,tr,e,e',s,s'. |
---|
[398] | 202 | execution_isteps tr s e s' e' → |
---|
| 203 | exec_from ge s e → |
---|
| 204 | star (mk_transrel … step) ge s tr s' ∧ |
---|
| 205 | exec_from ge s' e'. |
---|
[487] | 206 | #ge #tr0 #e0 #e0' #s0 #s0' #H |
---|
| 207 | elim H; |
---|
| 208 | [ #s #e #EXEC % //; |
---|
| 209 | | #e1 #e2 #tr1 #tr2 #s1 #s2 #s3 #STEPS #IH #EXEC |
---|
| 210 | elim (exec_from_step … EXEC); #EXEC3 #EXEC1 |
---|
| 211 | elim (IH EXEC1); |
---|
| 212 | #STAR12 #EXEC2 % //; |
---|
| 213 | lapply (exec_step_sound ge s3); |
---|
| 214 | >EXEC3 #STEP3 |
---|
| 215 | @(star_step (mk_transrel ?? step) … STEP3 STAR12) |
---|
| 216 | @refl |
---|
| 217 | | #e1 #e2 #o #k #i #s1 #s2 #s3 #tr1 #tr2 #STEPS #IH #EXEC |
---|
| 218 | elim (exec_from_interact … EXEC); |
---|
| 219 | #STEP3 #EXEC1 |
---|
| 220 | elim (IH EXEC1); #STAR #EXEC2 |
---|
| 221 | % |
---|
| 222 | [ @(star_step (mk_transrel ?? step) … STEP3 STAR) |
---|
| 223 | @refl |
---|
| 224 | | // |
---|
| 225 | ] |
---|
| 226 | ] qed. |
---|
[398] | 227 | |
---|
[1713] | 228 | inductive execution_terminates : trace → state → s_execution → int → Prop ≝ |
---|
| 229 | | terminates : ∀s,s',tr,tr',r,e. |
---|
| 230 | execution_isteps tr s e s' (se_stop tr' r) → |
---|
| 231 | execution_terminates (tr⧺tr') s (se_step E0 s e) r |
---|
[398] | 232 | (* We should only be able to get to here if main is an external function, which is silly. *) |
---|
[1713] | 233 | | annoying_corner_case_terminates: ∀s,s',tr,tr',r,e,o,k,i. |
---|
| 234 | execution_isteps tr s e s' (se_interact o k i (se_stop tr' r)) → |
---|
| 235 | execution_terminates (tr⧺tr') s (se_step E0 s e) r. |
---|
[398] | 236 | |
---|
[487] | 237 | coinductive execution_diverging : s_execution → Prop ≝ |
---|
[398] | 238 | | diverging_step : ∀s,e. execution_diverging e → execution_diverging (se_step E0 s e). |
---|
| 239 | |
---|
| 240 | (* Makes a finite number of interactions (including cost labels) before diverging. *) |
---|
[487] | 241 | inductive execution_diverges : trace → state → s_execution → Prop ≝ |
---|
[398] | 242 | | diverges_diverging: ∀tr,s,s',e,e'. |
---|
| 243 | execution_isteps tr s e s' e' → |
---|
| 244 | execution_diverging e' → |
---|
| 245 | execution_diverges tr s (se_step E0 s e). |
---|
| 246 | |
---|
| 247 | (* NB: "reacting" includes hitting a cost label. *) |
---|
[487] | 248 | coinductive execution_reacting : traceinf → state → s_execution → Prop ≝ |
---|
[398] | 249 | | reacting: ∀tr,tr',s,s',e,e'. |
---|
| 250 | execution_reacting tr' s' e' → |
---|
| 251 | execution_isteps tr s e s' e' → |
---|
| 252 | tr ≠ E0 → |
---|
| 253 | execution_reacting (tr⧻tr') s e. |
---|
| 254 | |
---|
[487] | 255 | inductive execution_reacts : traceinf → state → s_execution → Prop ≝ |
---|
[398] | 256 | | reacts: ∀tr,s,e. |
---|
| 257 | execution_reacting tr s e → |
---|
| 258 | execution_reacts tr s (se_step E0 s e). |
---|
| 259 | |
---|
[487] | 260 | inductive execution_goes_wrong: trace → state → s_execution → state → Prop ≝ |
---|
[797] | 261 | | go_wrong: ∀tr,s,s',e,msg. |
---|
| 262 | execution_isteps tr s e s' (se_wrong msg) → |
---|
[398] | 263 | execution_goes_wrong tr s (se_step E0 s e) s'. |
---|
| 264 | |
---|
[487] | 265 | let corec silent_sound ge s e |
---|
[398] | 266 | (H0:execution_diverging e) |
---|
| 267 | (EXEC:exec_from ge s e) |
---|
| 268 | : forever_silent (mk_transrel ?? step) … ge s ≝ ?. |
---|
[487] | 269 | cut (∃s2.∃e2.And (And (execution_diverging e2) (step ge s E0 s2)) (exec_from ge s2 e2)); |
---|
| 270 | [ cases H0 in EXEC ⊢ %; #s1 #e1 #H1 #EXEC |
---|
| 271 | elim (exec_from_step … EXEC); |
---|
| 272 | #EXEC0 #EXEC1 |
---|
| 273 | %{ s1} %{ e1} % //; % //; |
---|
| 274 | lapply (exec_step_sound ge s); >EXEC0 whd in ⊢ (% → ?); #H @H |
---|
| 275 | | *; #s2 *; #e2 *; *; #H2 #STEP2 #EXEC2 |
---|
| 276 | @(forever_silent_intro (mk_transrel ?? step) … ge s s2 ? (silent_sound ge s2 e2 ??)) |
---|
[398] | 277 | //; |
---|
[487] | 278 | ] qed. |
---|
[398] | 279 | |
---|
[1713] | 280 | lemma final_step: ∀ge,tr,r,s. |
---|
| 281 | exec_from ge s (se_stop tr r) → |
---|
| 282 | step ge s tr (Finalstate r). |
---|
| 283 | #ge #tr #r #s #EXEC |
---|
[487] | 284 | whd in EXEC; |
---|
| 285 | inversion EXEC; |
---|
[1713] | 286 | [ #tr' #r' #s' #EXEC' #E #_ destruct (E) |
---|
| 287 | lapply (exec_step_sound ge s) |
---|
[487] | 288 | >(exec_inf_aux_unfold …) in EXEC'; |
---|
[1713] | 289 | cases (exec_step ge s) |
---|
[1344] | 290 | [ #o #k #EXEC' whd in EXEC':(??%??); destruct (EXEC'); |
---|
| 291 | | #x cases x; #tr'' #s' whd in ⊢ (??%?? → ?); |
---|
[891] | 292 | @is_final_elim' [ #r'' #FINAL | #F ] |
---|
[1344] | 293 | #EXEC' whd in EXEC':(??%??); destruct (EXEC'); |
---|
| 294 | | #msg #EXEC' whd in EXEC':(??%??); destruct (EXEC'); |
---|
[487] | 295 | ] |
---|
[1713] | 296 | inversion FINAL #r''' #E1 #E2 #_ #H destruct (E1 E2); |
---|
[487] | 297 | @H |
---|
| 298 | | #tr' #s' #e' #se' #H #EXEC' #E destruct |
---|
[797] | 299 | | #msg #EXEC' #E destruct |
---|
[487] | 300 | | #o #k #i #e #H #EXEC #E destruct |
---|
[708] | 301 | ] qed. |
---|
[398] | 302 | |
---|
| 303 | |
---|
[1216] | 304 | lemma e_stop_inv: ∀ge,x,tr,r,s. |
---|
| 305 | exec_inf_aux ?? clight_exec ge x = e_stop ??? tr r s → |
---|
[1713] | 306 | x = Value ??? 〈tr,Finalstate r〉. |
---|
[1216] | 307 | #ge #x #tr #r #s |
---|
[487] | 308 | >(exec_inf_aux_unfold …) cases x; |
---|
| 309 | [ #o #k #EXEC whd in EXEC:(??%?); destruct; |
---|
[891] | 310 | | #z cases z; #tr' #s' whd in ⊢ (??%? → ?); @is_final_elim' |
---|
[1713] | 311 | [ #r' #FINAL cases FINAL; #r'' #EXEC whd in EXEC:(??%?); |
---|
[487] | 312 | destruct (EXEC); @refl |
---|
| 313 | | #F #EXEC whd in EXEC:(??%?); destruct (EXEC); |
---|
| 314 | ] |
---|
[797] | 315 | | #msg #EXEC whd in EXEC:(??%?); destruct (EXEC); |
---|
[487] | 316 | ] qed. |
---|
[398] | 317 | |
---|
[1713] | 318 | lemma terminates_sound: ∀ge,tr,s,r,e. |
---|
| 319 | execution_terminates tr s (se_step E0 s e) r → |
---|
[398] | 320 | exec_from ge s e → |
---|
[1713] | 321 | star (mk_transrel … step) ge s tr (Finalstate r). |
---|
| 322 | #ge #tr0 #s0 #r #e0 #H inversion H; |
---|
| 323 | [ #s #s' #tr #tr' #r' #e #ESTEPS #E1 #E2 #E3 #E4 #_ #EXEC |
---|
[487] | 324 | destruct (E1 E2 E3 E4 E5); |
---|
| 325 | cases (several_steps … ESTEPS EXEC); #STARs' #EXECs' |
---|
| 326 | @(star_right … STARs') |
---|
[1713] | 327 | [ 2: @(final_step ge tr' r' s' … EXECs') |
---|
[487] | 328 | | skip |
---|
| 329 | | @refl |
---|
| 330 | ] |
---|
[1713] | 331 | | #s #s' #tr #tr' #r' #e #o #k #i #ESTEPS #E1 #E2 #E3 #E4 #_ #EXEC |
---|
| 332 | destruct |
---|
| 333 | cases (several_steps … ESTEPS EXEC) #STARs' #EXECs' |
---|
[487] | 334 | @(star_right … STARs') |
---|
| 335 | [ @tr' |
---|
| 336 | | @(exec_from_interact_stop … EXECs') |
---|
| 337 | | @refl |
---|
| 338 | ] |
---|
| 339 | ] qed. |
---|
[398] | 340 | |
---|
[487] | 341 | let corec reacts_sound ge tr s e |
---|
[398] | 342 | (REACTS:execution_reacting tr s e) |
---|
| 343 | (EXEC:exec_from ge s e) : |
---|
| 344 | forever_reactive (mk_transrel … step) ge s tr ≝ ?. |
---|
[487] | 345 | cut (∃s'.∃e'.∃tr'.∃tr''.(And (And (And (execution_reacting tr'' s' e') (execution_isteps tr' s e s' e')) (tr' ≠ E0)) (tr = tr'⧻tr''))); |
---|
| 346 | [ inversion REACTS; |
---|
[1510] | 347 | #tr0 #tr' #s0 #s' #e0 #e' #EREACTS #ESTEPS #REACTED #E1 #E2 #E3 #_ destruct (E2 E3); |
---|
[487] | 348 | %{ s'} %{ e'} %{ tr0} %{ tr'} % [ % [ % //; | @REACTED ] | @refl ] |
---|
| 349 | | *; #s' *; #e' *; #tr' *; #tr'' |
---|
| 350 | *; *; *; #REACTS' #ESTEPS #REACTED #APPTR |
---|
| 351 | (* >APPTR *) |
---|
| 352 | @(match sym_eq ??? APPTR return λx.λ_.forever_reactive (mk_transrel genv state step) ge s x with [ refl ⇒ ? ]) |
---|
| 353 | % |
---|
| 354 | cases (several_steps … ESTEPS EXEC); #STEPS #EXEC' |
---|
| 355 | [ 2: @STEPS |
---|
| 356 | | skip |
---|
| 357 | | @REACTED |
---|
| 358 | | @reacts_sound |
---|
| 359 | [ 2: @REACTS' |
---|
| 360 | | skip |
---|
| 361 | | @EXEC' |
---|
| 362 | ] |
---|
| 363 | ] |
---|
| 364 | qed. |
---|
[399] | 365 | |
---|
[797] | 366 | lemma exec_from_wrong: ∀ge,s,msg. |
---|
| 367 | exec_from ge s (se_wrong msg) → |
---|
| 368 | exec_step ge s = Wrong ??? msg. |
---|
| 369 | #ge #s #msg #H whd in H; |
---|
[487] | 370 | inversion H; |
---|
| 371 | [ #tr #r #m #EXEC #E destruct (E) |
---|
| 372 | | #tr #s' #e #e' #H #EXEC #E destruct (E) |
---|
[1516] | 373 | | #msg #EXEC #H #_ generalize in match H; -H; generalize in match EXEC; -EXEC; |
---|
| 374 | generalize in match msg; -msg; >(exec_inf_aux_unfold …) |
---|
[487] | 375 | cases (exec_step ge s); |
---|
[1344] | 376 | [ #o #k #msg' #EXEC whd in EXEC:(??%??); destruct |
---|
[1516] | 377 | | #x cases x; #tr #s' #msg' whd in ⊢ (??%?? → ?); @is_final_elim' |
---|
[1344] | 378 | [ #r ] #F #EXEC whd in EXEC:(??%??); destruct |
---|
| 379 | | #msg1 #msg2 #EXEC #E whd in EXEC:(??%??); destruct @refl |
---|
[487] | 380 | ] |
---|
| 381 | | #o #k #i #e #H #EXEC #E destruct |
---|
| 382 | ] qed. |
---|
[399] | 383 | |
---|
[487] | 384 | lemma exec_from_step_notfinal: ∀ge,s,tr,s',e. |
---|
[399] | 385 | exec_from ge s (se_step tr s' e) → |
---|
| 386 | ¬(∃r. final_state s' r). |
---|
[487] | 387 | #ge #s #tr #s' #e #H whd in H; inversion H; |
---|
| 388 | [ #tr' #r #m #EXEC #E destruct |
---|
[1510] | 389 | | #tr' #s'' #e' #e'' #H #EXEC #E #_ destruct (E); |
---|
[487] | 390 | >(exec_inf_aux_unfold …) in EXEC; |
---|
| 391 | cases (exec_step ge s); |
---|
[1344] | 392 | [ #o #k #EXEC whd in EXEC:(??%??); destruct |
---|
[1516] | 393 | | #x cases x; #tr1 #s1 whd in ⊢ (??%?? → ?); @is_final_elim' |
---|
[1344] | 394 | [ #r ] #F #E whd in E:(??%??); destruct @F |
---|
| 395 | | #msg #E whd in E:(??%??); destruct |
---|
[487] | 396 | ] |
---|
[797] | 397 | | #msg #EXEC #E destruct |
---|
[487] | 398 | | #o #k #i #e' #H #EXEC #E destruct |
---|
| 399 | ] qed. |
---|
[399] | 400 | |
---|
[487] | 401 | lemma exec_from_interact_step_notfinal: ∀ge,s,o,k,i,tr,s',e. |
---|
[399] | 402 | exec_from ge s (se_interact o k i (se_step tr s' e)) → |
---|
| 403 | ¬(∃r. final_state s' r). |
---|
[487] | 404 | #ge #s #o #k #i #tr #s' #e #H |
---|
[1713] | 405 | % *; #r #F cases F in H; #r' #H |
---|
[487] | 406 | inversion H; |
---|
| 407 | [ #tr' #r #m #EXEC #E destruct |
---|
| 408 | | #tr' #s'' #e' #e'' #H #EXEC #E destruct (E); |
---|
[797] | 409 | | #msg #EXEC #E destruct |
---|
[1510] | 410 | | #o' #k' #i' #e' #H #EXEC #E #_ destruct; |
---|
[487] | 411 | >(exec_inf_aux_unfold …) in EXEC; |
---|
| 412 | cases (exec_step ge s); |
---|
[1344] | 413 | [ #o1 #k1 #EXEC1 whd in EXEC1:(??%??); destruct (EXEC1); |
---|
[487] | 414 | inversion H; |
---|
| 415 | [ #tr1 #r1 #m1 #EXECK #E destruct (E); |
---|
[1510] | 416 | | #tr1 #s1 #e1 #e2 #H1 #EXECK #E #_ destruct (E); |
---|
[487] | 417 | >(exec_inf_aux_unfold …) in EXECK; |
---|
| 418 | cases (k1 i'); |
---|
[1344] | 419 | [ #o2 #k2 #EXECK whd in EXECK:(??%??); destruct |
---|
| 420 | | #x cases x; #tr2 #s2 whd in ⊢ (??%?? → ?); |
---|
[1350] | 421 | lapply (is_final_elim s2) #IFE whd in IFE:(∀_. ? → ? → ?%); |
---|
[1521] | 422 | change with (is_final s2) in match (is_final ?????); |
---|
[891] | 423 | @IFE [ #r ] #F #EXECK |
---|
[1344] | 424 | whd in EXECK:(??%??); destruct; |
---|
[487] | 425 | @(absurd ?? F) |
---|
| 426 | %{ r'} //; |
---|
[1344] | 427 | | #msg #E whd in E:(??%??); destruct |
---|
[487] | 428 | ] |
---|
[1344] | 429 | | #msg #EXECK #E whd in E:(??%??); destruct |
---|
[487] | 430 | | #o2 #k2 #i2 #e2 #H2 #EXECK #E destruct |
---|
| 431 | ] |
---|
[1344] | 432 | | #x cases x; #tr1 #s1 whd in ⊢ (??%?? → ?); |
---|
| 433 | @is_final_elim' [ #r ] #F #E whd in E:(??%??); destruct; |
---|
| 434 | | #msg #E whd in E:(??%??); destruct |
---|
[487] | 435 | ] |
---|
| 436 | ] qed. |
---|
[399] | 437 | |
---|
[487] | 438 | lemma wrong_sound: ∀ge,tr,s,s',e. |
---|
[399] | 439 | execution_goes_wrong tr s (se_step E0 s e) s' → |
---|
| 440 | exec_from ge s e → |
---|
| 441 | (¬∃r. final_state s r) → |
---|
| 442 | star (mk_transrel … step) ge s tr s' ∧ |
---|
| 443 | nostep (mk_transrel … step) ge s' ∧ |
---|
| 444 | (¬∃r. final_state s' r). |
---|
[487] | 445 | #ge #tr0 #s0 #s0' #e0 #WRONG inversion WRONG; |
---|
[1510] | 446 | #tr #s #s' #e #msg #ESTEPS #E1 #E2 #E3 #E4 #_ #EXEC #NOTFINAL destruct (E1 E2 E3 E4); |
---|
[487] | 447 | cases (several_steps … ESTEPS EXEC); |
---|
| 448 | #STAR #EXEC' % |
---|
| 449 | [ % [ @STAR |
---|
| 450 | | #badtr #bads % #badSTEP |
---|
| 451 | lapply (step_complete … badSTEP); |
---|
| 452 | >(exec_from_wrong … EXEC') |
---|
[399] | 453 | //; |
---|
[487] | 454 | ] |
---|
| 455 | | % |
---|
| 456 | elim ESTEPS in NOTFINAL EXEC ⊢ %; |
---|
| 457 | [ #s1 #e1 #NF #EX #F @(absurd ? F NF) |
---|
| 458 | | #e1 #e2 #tr1 #tr2 #s1 #s2 #s3 #ESTEPS1 #IH #NF #EXEC |
---|
| 459 | cases (exec_from_step … EXEC); #EXEC3 #EXEC1 |
---|
| 460 | @(IH … EXEC1) |
---|
| 461 | @(exec_from_step_notfinal … EXEC) |
---|
| 462 | | #e1 #e2 #o #k #i #s1 #s2 #s3 #tr1 #tr2 #ESTEPS1 #IH #NF #EXEC |
---|
| 463 | @IH |
---|
| 464 | [ @(exec_from_interact_step_notfinal … EXEC) |
---|
[708] | 465 | | cases (exec_from_interact … EXEC) #STEP #EF1 @EF1 |
---|
[487] | 466 | ] |
---|
| 467 | ] |
---|
| 468 | ] qed. |
---|
[399] | 469 | |
---|
[487] | 470 | inductive execution_characterisation : state → s_execution → Prop ≝ |
---|
[1713] | 471 | | ec_terminates: ∀s,r,e,tr. |
---|
| 472 | execution_terminates tr s e r → |
---|
[399] | 473 | execution_characterisation s e |
---|
| 474 | | ec_diverges: ∀s,e,tr. |
---|
| 475 | execution_diverges tr s e → |
---|
| 476 | execution_characterisation s e |
---|
| 477 | | ec_reacts: ∀s,e,tr. |
---|
| 478 | execution_reacts tr s e → |
---|
| 479 | execution_characterisation s e |
---|
| 480 | | ec_wrong: ∀e,s,s',tr. |
---|
| 481 | execution_goes_wrong tr s e s' → |
---|
| 482 | execution_characterisation s e. |
---|
| 483 | |
---|
| 484 | (* bit of a hack to avoid inability to reduce term in match *) |
---|
[487] | 485 | definition interact_prop : ∀A:Type[0].(∀o:io_out. (io_in o → IO io_out io_in A) → Prop) → IO io_out io_in A → Prop ≝ |
---|
[399] | 486 | λA,P,e. match e return λ_.Prop with [ Interact o k ⇒ P o k | _ ⇒ True ]. |
---|
| 487 | |
---|
[487] | 488 | lemma err_does_not_interact: ∀A,B,P,e1,e2. |
---|
[399] | 489 | (∀x:B.interact_prop A P (e2 x)) → |
---|
| 490 | interact_prop A P (bindIO ?? B A (err_to_io ??? e1) e2). |
---|
[487] | 491 | #A #B #P #e1 #e2 #H |
---|
| 492 | cases e1; //; qed. |
---|
[399] | 493 | |
---|
[487] | 494 | lemma err2_does_not_interact: ∀A,B,C,P,e1,e2. |
---|
[399] | 495 | (∀x,y.interact_prop A P (e2 x y)) → |
---|
| 496 | interact_prop A P (bindIO2 ?? B C A (err_to_io ??? e1) e2). |
---|
[487] | 497 | #A #B #C #P #e1 #e2 #H |
---|
| 498 | cases e1; [ #z cases z; ] //; qed. |
---|
[399] | 499 | |
---|
[487] | 500 | lemma err_sig_does_not_interact: ∀A,B,P.∀Q:B→Prop.∀e1,e2. |
---|
[399] | 501 | (∀x.interact_prop A P (e2 x)) → |
---|
[487] | 502 | interact_prop A P (bindIO ?? (Sig B Q) A (err_to_io_sig ??? Q e1) e2). |
---|
| 503 | #A #B #P #Q #e1 #e2 #H |
---|
| 504 | cases e1; //; qed. |
---|
[399] | 505 | |
---|
[797] | 506 | lemma opt_does_not_interact: ∀A,B,P,e1,e2,msg. |
---|
[399] | 507 | (∀x:B.interact_prop A P (e2 x)) → |
---|
[797] | 508 | interact_prop A P (bindIO ?? B A (opt_to_io ??? msg e1) e2). |
---|
| 509 | #A #B #P #e1 #e2 #msg #H |
---|
[487] | 510 | cases e1; //; qed. |
---|
[399] | 511 | |
---|
[487] | 512 | lemma exec_step_interaction: |
---|
[399] | 513 | ∀ge,s. interact_prop ? (λo,k. ∀i.∃tr.∃s'. k i = Value ??? 〈tr,s'〉 ∧ tr ≠ E0) (exec_step ge s). |
---|
[487] | 514 | #ge #s cases s; |
---|
| 515 | [ #f #st #kk #e #m cases st; |
---|
[2391] | 516 | [ 11,14: #a | 2,4,6,7,12,13,15: #a #b | 3,5: #a #b #c | 8: #a #b #c #d ] |
---|
| 517 | [ 4,6,8,9: @I ] |
---|
[487] | 518 | whd in ⊢ (???%); |
---|
| 519 | [ cases a; [ cases (fn_return f); //; | #e whd nodelta in ⊢ (???%); |
---|
| 520 | cases (type_eq_dec (fn_return f) Tvoid); #x //; @err2_does_not_interact // ] |
---|
| 521 | | cases (find_label a (fn_body f) (call_cont kk)); [ @I | #z cases z #x #y @I ] |
---|
| 522 | | @err2_does_not_interact #x1 #x2 @err2_does_not_interact #x3 #x4 @opt_does_not_interact #x5 @I |
---|
[2391] | 523 | | 4,7: @err2_does_not_interact #x1 #x2 @err_does_not_interact #x3 @I |
---|
[2428] | 524 | | @err2_does_not_interact * // #x1 #x2 #x3 cases (typeof a) // #x4 #x5 whd nodelta in ⊢ (???%); cases (sz_eq_dec ??) // #x6 cases (select_switch ???) // |
---|
[487] | 525 | | @err2_does_not_interact #x1 #x2 @err2_does_not_interact #x3 #x4 @opt_does_not_interact #x5 @err_does_not_interact #x6 cases a; |
---|
| 526 | [ @I | #x7 @err2_does_not_interact #x8 #x9 @I ] |
---|
| 527 | | cases (is_Sskip a); #H [ @err2_does_not_interact #x1 #x2 @err_does_not_interact #x3 @I |
---|
| 528 | | @I ] |
---|
| 529 | | cases kk; [ 1,8: cases (fn_return f); //; | 2,3,5,6,7: //; |
---|
| 530 | | #z1 #z2 #z3 @err2_does_not_interact #x1 #x2 @err_does_not_interact #x3 cases x3; @I ] |
---|
| 531 | | cases kk; //; |
---|
| 532 | | cases kk; [ 4: #z1 #z2 #z3 @err2_does_not_interact #x1 #x2 @err_does_not_interact #x3 cases x3; @I |
---|
| 533 | | *: // ] |
---|
| 534 | ] |
---|
| 535 | | #f #args #kk #m cases f; |
---|
| 536 | [ #f' whd in ⊢ (???%); cases (exec_alloc_variables empty_env m (fn_params f'@fn_vars f')) |
---|
[1516] | 537 | #x1 #x2 whd in ⊢ (???%); @err_does_not_interact // |
---|
[399] | 538 | (* This is the only case that actually matters! *) |
---|
[487] | 539 | | #fn #argtys #rty whd in ⊢ (???%); |
---|
| 540 | @err_does_not_interact #x1 |
---|
| 541 | whd; #i % [ 2: % [ 2: % [ % whd in ⊢ (??%?); @refl |
---|
| 542 | | % #E whd in E:(??%%); destruct (E); ] ] ] |
---|
| 543 | ] |
---|
| 544 | | #v #kk #m whd in ⊢ (???%); cases kk; |
---|
[1713] | 545 | [ cases v // * // |
---|
| 546 | | 8: #x1 #x2 #x3 #x4 cases x1; |
---|
[487] | 547 | [ whd in ⊢ (???%); cases v; // | #x5 whd in ⊢ (???%); cases x5; |
---|
| 548 | #x6 #x7 @opt_does_not_interact // ] |
---|
| 549 | | *: // ] |
---|
[1713] | 550 | | #r // |
---|
[487] | 551 | ] qed. |
---|
[399] | 552 | |
---|
| 553 | |
---|
| 554 | (* Some classical logic (roughly like a fragment of Coq's library) *) |
---|
[487] | 555 | lemma classical_doubleneg: |
---|
[399] | 556 | ∀classic:(∀P:Prop.P ∨ ¬P). |
---|
| 557 | ∀P:Prop. ¬ (¬ P) → P. |
---|
[487] | 558 | #classic #P *; #H |
---|
| 559 | cases (classic P); |
---|
| 560 | [ // | #H' @False_ind /2/; ] |
---|
| 561 | qed. |
---|
[399] | 562 | |
---|
[487] | 563 | lemma classical_not_all_not_ex: |
---|
[399] | 564 | ∀classic:(∀P:Prop.P ∨ ¬P). |
---|
[487] | 565 | ∀A:Type[0].∀P:A → Prop. ¬ (∀x. ¬ P x) → ∃x. P x. |
---|
| 566 | #classic #A #P *; #H |
---|
| 567 | @(classical_doubleneg classic) % *; #H' |
---|
| 568 | @H #x % #H'' @H' %{x} @H'' |
---|
| 569 | qed. |
---|
[399] | 570 | |
---|
[487] | 571 | lemma classical_not_all_ex_not: |
---|
[399] | 572 | ∀classic:(∀P:Prop.P ∨ ¬P). |
---|
[487] | 573 | ∀A:Type[0].∀P:A → Prop. ¬ (∀x. P x) → ∃x. ¬ P x. |
---|
| 574 | #classic #A #P *; #H |
---|
| 575 | @(classical_not_all_not_ex classic A (λx.¬ P x)) |
---|
| 576 | % #H' @H #x @(classical_doubleneg classic) |
---|
| 577 | @H' |
---|
| 578 | qed. |
---|
[399] | 579 | |
---|
[487] | 580 | lemma not_ex_all_not: |
---|
| 581 | ∀A:Type[0].∀P:A → Prop. ¬ (∃x. P x) → ∀x. ¬ P x. |
---|
| 582 | #A #P *; #H #x % #H' |
---|
| 583 | @H %{ x} @H' |
---|
| 584 | qed. |
---|
[399] | 585 | |
---|
[487] | 586 | lemma not_imply_elim: |
---|
[399] | 587 | ∀classic:(∀P:Prop.P ∨ ¬P). |
---|
| 588 | ∀P,Q:Prop. ¬ (P → Q) → P. |
---|
[487] | 589 | #classic #P #Q *; #H |
---|
| 590 | @(classical_doubleneg classic) % *; #H' |
---|
| 591 | @H #H'' @False_ind @H' @H'' |
---|
| 592 | qed. |
---|
[399] | 593 | |
---|
[487] | 594 | lemma not_imply_elim2: |
---|
[399] | 595 | ∀P,Q:Prop. ¬ (P → Q) → ¬ Q. |
---|
[487] | 596 | #P #Q *; #H % #H' |
---|
| 597 | @H #_ @H' |
---|
| 598 | qed. |
---|
[399] | 599 | |
---|
[487] | 600 | lemma imply_to_and: |
---|
[399] | 601 | ∀classic:(∀P:Prop.P ∨ ¬P). |
---|
| 602 | ∀P,Q:Prop. ¬ (P → Q) → P ∧ ¬Q. |
---|
[487] | 603 | #classic #P #Q #H % |
---|
| 604 | [ @(not_imply_elim classic P Q H) |
---|
| 605 | | @(not_imply_elim2 P Q H) |
---|
| 606 | ] qed. |
---|
[399] | 607 | |
---|
[487] | 608 | lemma not_and_to_imply: |
---|
[399] | 609 | ∀classic:(∀P:Prop.P ∨ ¬P). |
---|
| 610 | ∀P,Q:Prop. ¬ (P ∧ Q) → P → ¬Q. |
---|
[487] | 611 | #classic #P #Q *; #H #H' |
---|
| 612 | % #H'' @H % //; |
---|
| 613 | qed. |
---|
[399] | 614 | |
---|
[487] | 615 | inductive execution_not_over : s_execution → Prop ≝ |
---|
[399] | 616 | | eno_step: ∀tr,s,e. execution_not_over (se_step tr s e) |
---|
| 617 | | eno_interact: ∀o,k,tr,s,e,i. execution_not_over (se_interact o k i (se_step tr s e)). |
---|
| 618 | |
---|
[1713] | 619 | lemma eno_stop: ∀tr,r. execution_not_over (se_stop tr r) → False. |
---|
| 620 | #tr0 #r0 #H inversion H; |
---|
[487] | 621 | [ #tr #s #e #E destruct |
---|
| 622 | | #o #k #tr #s #e #i #E destruct |
---|
| 623 | ] qed. |
---|
[399] | 624 | |
---|
[797] | 625 | lemma eno_wrong: ∀msg. execution_not_over (se_wrong msg) → False. |
---|
| 626 | #msg #H inversion H; |
---|
[487] | 627 | [ #tr #s #e #E destruct |
---|
| 628 | | #o #k #tr #s #e #i #E destruct |
---|
| 629 | ] qed. |
---|
[399] | 630 | |
---|
[487] | 631 | let corec show_divergence s e |
---|
[399] | 632 | (NONTERMINATING:∀tr1,s1,e1. execution_isteps tr1 s e s1 e1 → |
---|
| 633 | execution_not_over e1) |
---|
| 634 | (UNREACTIVE:∀tr2,s2,e2. execution_isteps tr2 s e s2 e2 → tr2 = E0) |
---|
[487] | 635 | (CONTINUES:∀tr2,s2,o,k,i,e'. execution_isteps tr2 s e s2 (se_interact o k i e') → ∃tr3.∃s3.∃e3. And (e' = se_step tr3 s3 e3) (tr3 ≠ E0)) |
---|
[399] | 636 | : execution_diverging e ≝ ?. |
---|
[487] | 637 | lapply (NONTERMINATING E0 s e ?); //; |
---|
| 638 | cases e in UNREACTIVE NONTERMINATING CONTINUES ⊢ %; |
---|
[1713] | 639 | [ #tr #i #_ #_ #_ #ENO elim (eno_stop … ENO); |
---|
[487] | 640 | | #tr #s' #e' #UNREACTIVE lapply (UNREACTIVE tr s' e' ?); |
---|
[1516] | 641 | [ <(E0_right tr) in ⊢ (?%????); |
---|
[487] | 642 | @isteps_one @isteps_none |
---|
| 643 | | #TR @(match sym_eq ??? TR with [ refl ⇒ ? ]) (* >TR in UNREACTIVE ⊢ % *) |
---|
| 644 | #NONTERMINATING #CONTINUES #_ % |
---|
| 645 | @(show_divergence s') |
---|
| 646 | [ #tr1 #s1 #e1 #S @(NONTERMINATING tr1 s1 e1) |
---|
[1521] | 647 | change with (Eapp E0 tr1) in ⊢ (?%????); @isteps_one |
---|
[487] | 648 | @S |
---|
[1516] | 649 | | #tr2 #s2 #e2 #S >TR in UNREACTIVE; #UNREACTIVE @(UNREACTIVE tr2 s2 e2) |
---|
[1521] | 650 | change with (Eapp E0 tr2) in ⊢ (?%????); |
---|
[487] | 651 | @isteps_one @S |
---|
| 652 | | #tr2 #s2 #o #k #i #e2 #S @(CONTINUES tr2 s2 o k i) |
---|
[1521] | 653 | change with (Eapp E0 tr2) in ⊢ (?%????); |
---|
[487] | 654 | @(isteps_one … S) |
---|
| 655 | ] |
---|
| 656 | ] |
---|
[797] | 657 | | #msg #_ #_ #_ #ENO elim (eno_wrong … ENO); |
---|
[487] | 658 | | #o #k #i #e' #UNREACTIVE #NONTERMINATING #CONTINUES #_ |
---|
| 659 | lapply (CONTINUES E0 s o k i e' (isteps_none …)); |
---|
| 660 | *; #tr' *; #s' *; #e' *; #EXEC #NOTSILENT |
---|
| 661 | @False_ind @(absurd ?? NOTSILENT) |
---|
| 662 | @(UNREACTIVE … s' e') |
---|
[1516] | 663 | <(E0_right tr') in ⊢ (?%????); |
---|
[487] | 664 | >EXEC |
---|
| 665 | @isteps_interact //; |
---|
| 666 | ] qed. |
---|
[399] | 667 | |
---|
[487] | 668 | lemma se_inv: ∀e1,e2. |
---|
[399] | 669 | single_exec_of e1 e2 → |
---|
| 670 | match e1 with |
---|
[1713] | 671 | [ e_stop tr r s ⇒ match e2 with [ se_stop tr' r' ⇒ tr = tr' ∧ r = r' | _ ⇒ False ] |
---|
[399] | 672 | | e_step tr s e1' ⇒ match e2 with [ se_step tr' s' e2' ⇒ tr = tr' ∧ s = s' ∧ single_exec_of e1' e2' | _ ⇒ False ] |
---|
[797] | 673 | | e_wrong _ ⇒ match e2 with [ se_wrong _ ⇒ True | _ ⇒ False ] |
---|
[399] | 674 | | e_interact o k ⇒ match e2 with [ se_interact o' k' i e ⇒ o' = o ∧ k' ≃ k ∧ single_exec_of (k' i) e | _ ⇒ False ] |
---|
| 675 | ]. |
---|
[487] | 676 | #e01 #e02 #H |
---|
| 677 | cases H; |
---|
[1216] | 678 | [ #tr #r #s whd; % [ % ] // |
---|
[487] | 679 | | #tr #s #e1' #e2' #H' whd; % [ % ] // |
---|
[797] | 680 | | #msg whd; // |
---|
[487] | 681 | | #o #k #i #e #H' whd; % [ % ] // |
---|
| 682 | ] qed. |
---|
[399] | 683 | |
---|
[487] | 684 | lemma interaction_is_not_silent: ∀ge,o,k,i,tr,s,s',e. |
---|
[399] | 685 | exec_from ge s (se_interact o k i (se_step tr s' e)) → |
---|
| 686 | tr ≠ E0. |
---|
[487] | 687 | #ge #o #k #i #tr #s #s' #e whd in ⊢ (% → ?); >(exec_inf_aux_unfold …) |
---|
| 688 | lapply (exec_step_interaction ge s); |
---|
| 689 | cases (exec_step ge s); |
---|
| 690 | [ #o' #k' ; whd in ⊢ (% → ?%? → ?); #H #K cases (se_inv … K); |
---|
| 691 | *; #E1 #E2 #H1 destruct (E1); |
---|
| 692 | lapply (H i); *; #tr' *; #s'' *; #K' #TR |
---|
[1516] | 693 | >E2 in H1; #H1 whd in H1:(?%?); >K' in H1; |
---|
[487] | 694 | >(exec_inf_aux_unfold …) whd in ⊢ (?%? → ?); |
---|
[1521] | 695 | change with (is_final s'') in match (is_final ?????); |
---|
[708] | 696 | @is_final_elim |
---|
| 697 | [ #r #F whd in ⊢ (?%? → ?); #S |
---|
[487] | 698 | @False_ind @(absurd ? S) cases (se_inv … S) |
---|
| 699 | | #NF #S whd in S:(?%?); cases (se_inv … S); |
---|
| 700 | *; #E1 #E2 #S' <E1 @TR |
---|
| 701 | ] |
---|
[1516] | 702 | | #x cases x; #tr' #s'' #H whd in ⊢ (?%? → ?); |
---|
[891] | 703 | @is_final_elim' [ #r ] #F #E whd in E:(?%?); |
---|
[487] | 704 | inversion E; |
---|
| 705 | [ 1,5: #tr1 #e1 #m1 #E1 #E2 destruct |
---|
| 706 | | 2,6: #tr #s1 #e1 #e2 #H #E1 #E2 destruct |
---|
[797] | 707 | | 3,7: #msg #E destruct |
---|
[487] | 708 | | 4,8: #o1 #k1 #i1 #e1 #H1 #E1 #E2 destruct |
---|
| 709 | ] |
---|
[797] | 710 | | #msg #_ #E whd in E:(?%?); |
---|
[487] | 711 | inversion E; |
---|
| 712 | [ 1,5: #tr1 #e1 #m1 #E1 #E2 destruct |
---|
| 713 | | 2,6: #tr #s1 #e1 #e2 #H #E1 #E2 destruct |
---|
[797] | 714 | | 3,7: #msg #E1 #E2 destruct |
---|
[487] | 715 | | 4,8: #o1 #k1 #i1 #e1 #H1 #E1 #E2 destruct |
---|
| 716 | ] |
---|
| 717 | ] qed. |
---|
[399] | 718 | |
---|
[487] | 719 | let corec reactive_traceinf' ge s e |
---|
[399] | 720 | (EXEC:exec_from ge s e) |
---|
| 721 | (REACTIVE: ∀tr,s1,e1. |
---|
| 722 | execution_isteps tr s e s1 e1 → |
---|
[1605] | 723 | (Σx.execution_isteps (\fst x) s1 e1 (\fst (\snd x)) (\snd (\snd x)) ∧ (\fst x) ≠ E0)) |
---|
[399] | 724 | : traceinf' ≝ ?. |
---|
[487] | 725 | lapply (REACTIVE E0 s e (isteps_none …)); |
---|
| 726 | *; #x cases x; #tr #y cases y; #s' #e' *; #STEPS #H |
---|
| 727 | %{ tr ? H} |
---|
| 728 | @(reactive_traceinf' ge s' e' ?) |
---|
| 729 | [ cases (several_steps … STEPS EXEC); #_ #H' @H' |
---|
| 730 | | #tr1 #s1 #e1 #STEPS1 |
---|
| 731 | @REACTIVE |
---|
| 732 | [ 2: |
---|
| 733 | @(isteps_trans … STEPS STEPS1) |
---|
| 734 | | skip |
---|
| 735 | ] |
---|
| 736 | ] |
---|
| 737 | qed. |
---|
[399] | 738 | |
---|
| 739 | (* A slightly different version of the above, to work around a problem with the |
---|
| 740 | next result. *) |
---|
[487] | 741 | let corec reactive_traceinf'' ge s e |
---|
[399] | 742 | (EXEC:exec_from ge s e) |
---|
[1605] | 743 | (REACTIVE0: Σx.execution_isteps (\fst x) s e (\fst (\snd x)) (\snd (\snd x)) ∧ (\fst x) ≠ E0) |
---|
[399] | 744 | (REACTIVE: ∀tr,s1,e1. |
---|
| 745 | execution_isteps tr s e s1 e1 → |
---|
[1605] | 746 | (Σx.execution_isteps (\fst x) s1 e1 (\fst (\snd x)) (\snd (\snd x)) ∧ (\fst x) ≠ E0)) |
---|
[399] | 747 | : traceinf' ≝ ?. |
---|
[487] | 748 | cases REACTIVE0; #x cases x; #tr #y cases y; #s' #e' *; #STEPS #H |
---|
| 749 | %{ tr ? H} |
---|
| 750 | @(reactive_traceinf'' ge s' e' ?) |
---|
| 751 | [ cases (several_steps … STEPS EXEC); #_ #H' @H' |
---|
| 752 | | @(REACTIVE … STEPS) |
---|
| 753 | | #tr1 #s1 #e1 #STEPS1 |
---|
| 754 | @REACTIVE |
---|
| 755 | [ 2: |
---|
| 756 | @(isteps_trans … STEPS STEPS1) |
---|
| 757 | | skip |
---|
| 758 | ] |
---|
| 759 | ] qed. |
---|
[399] | 760 | |
---|
| 761 | (* We want to prove |
---|
| 762 | |
---|
[487] | 763 | lemma show_reactive : ∀ge,s. |
---|
[399] | 764 | ∀REACTIVE:∀tr,s1,e1. |
---|
| 765 | execution_isteps tr s (exec_inf_aux ge (exec_step ge s)) s1 e1 → |
---|
| 766 | Σx.execution_isteps (\fst x) s1 e1 (\fst (\snd x)) (\snd (\snd x)) ∧ (\fst x) ≠ E0. |
---|
| 767 | execution_reacting (traceinf_of_traceinf' (reactive_traceinf' ge s REACTIVE)) s (exec_inf_aux ge (exec_step ge s)). |
---|
| 768 | |
---|
| 769 | but the current matita won't unfold reactive_traceinf' so that we can do case |
---|
| 770 | analysis on (REACTIVE …). Instead we take an "applied" version of REACTIVE that |
---|
| 771 | we can do case analysis on, then get it into the desired form afterwards. |
---|
| 772 | *) |
---|
[487] | 773 | let corec show_reactive' ge s e |
---|
[399] | 774 | (EXEC:exec_from ge s e) |
---|
[1605] | 775 | (REACTIVE0: Σx.execution_isteps (\fst x) s e (\fst (\snd x)) (\snd (\snd x)) ∧ (\fst x) ≠ E0) |
---|
[399] | 776 | (REACTIVE: ∀tr1,s1,e1. |
---|
| 777 | execution_isteps tr1 s e s1 e1 → |
---|
[1605] | 778 | (Σx.execution_isteps (\fst x) s1 e1 (\fst (\snd x)) (\snd (\snd x)) ∧ (\fst x) ≠ E0)) |
---|
[399] | 779 | : execution_reacting (traceinf_of_traceinf' (reactive_traceinf'' ge s e EXEC REACTIVE0 REACTIVE)) s e ≝ ?. |
---|
[487] | 780 | (*>(unroll_traceinf' (reactive_traceinf'' …)) *) |
---|
| 781 | @(match sym_eq ??? (unroll_traceinf' (reactive_traceinf'' …)) with [ refl ⇒ ? ]) |
---|
| 782 | cases REACTIVE0; |
---|
| 783 | #x cases x; #tr1 #y cases y; #s1 #e1 #z cases z; #STEPS #NOTSILENT |
---|
| 784 | whd in ⊢ (?(?%)??); |
---|
| 785 | (*>(traceinf_traceinfp_app …) *) |
---|
| 786 | @(match sym_eq ??? (traceinf_traceinfp_app …) with [ refl ⇒ ? ]) |
---|
| 787 | @(reacting … STEPS NOTSILENT) |
---|
| 788 | @show_reactive' |
---|
| 789 | qed. |
---|
[399] | 790 | |
---|
[487] | 791 | lemma show_reactive : ∀ge,s,e. |
---|
[399] | 792 | ∀EXEC:exec_from ge s e. |
---|
| 793 | ∀REACTIVE:∀tr,s1,e1. |
---|
| 794 | execution_isteps tr s e s1 e1 → |
---|
[1605] | 795 | (Σx.execution_isteps (\fst x) s1 e1 (\fst (\snd x)) (\snd (\snd x)) ∧ (\fst x) ≠ E0). |
---|
[399] | 796 | execution_reacting (traceinf_of_traceinf' (reactive_traceinf'' ge s e EXEC ? REACTIVE)) s e. |
---|
[487] | 797 | [ #ge #s #e #EXEC #REACTIVE |
---|
| 798 | @show_reactive' |
---|
| 799 | | @(REACTIVE … (isteps_none …)) |
---|
| 800 | ] qed. |
---|
[399] | 801 | |
---|
[487] | 802 | lemma execution_characterisation_complete: |
---|
[399] | 803 | ∀classic:(∀P:Prop.P ∨ ¬P). |
---|
[487] | 804 | ∀constructive_indefinite_description:(∀A:Type[0]. ∀P:A→Prop. (∃x. P x) → Sig A P). |
---|
[399] | 805 | ∀ge,s,e. |
---|
| 806 | exec_from ge s e → |
---|
| 807 | execution_characterisation s (se_step E0 s e). |
---|
[487] | 808 | #classic #constructive_indefinite_description #ge #s #e #EXEC |
---|
| 809 | cases (classic (∀tr1,s1,e1. execution_isteps tr1 s e s1 e1 → |
---|
[399] | 810 | execution_not_over e1)); |
---|
[487] | 811 | [ #NONTERMINATING |
---|
| 812 | cases (classic (∃tr,s1,e1. execution_isteps tr s e s1 e1 ∧ |
---|
[399] | 813 | ∀tr2,s2,e2. execution_isteps tr2 s1 e1 s2 e2 → tr2 = E0)); |
---|
[487] | 814 | [ *; #tr *; #s1 *; #e1 *; #INITIAL #UNREACTIVE |
---|
| 815 | @(ec_diverges … s ? tr) |
---|
| 816 | @(diverges_diverging … INITIAL) |
---|
| 817 | @(show_divergence s1 e1) |
---|
| 818 | [ #tr2 #s2 #e2 #S @(NONTERMINATING (Eapp tr tr2) s2 e2) |
---|
| 819 | @(isteps_trans … INITIAL S) |
---|
| 820 | | #tr2 #s2 #e2 #S @(UNREACTIVE … S) |
---|
| 821 | | #tr2 #s2 #o #k #i #e2 #STEPS |
---|
| 822 | lapply (NONTERMINATING (Eapp tr tr2) s2 (se_interact o k i e2) ?); |
---|
| 823 | [ @(isteps_trans … INITIAL STEPS) ] |
---|
| 824 | #NOTOVER inversion NOTOVER; |
---|
| 825 | [ #tr' #s' #e' #E destruct (E); |
---|
[1510] | 826 | | #o' #k' #tr' #s' #e' #i' #E #_ destruct (E); |
---|
[487] | 827 | %{ tr'} %{s'} %{e'} % //; |
---|
| 828 | cases (several_steps … INITIAL EXEC); #_ #EXEC1 |
---|
| 829 | cases (several_steps … STEPS EXEC1); #_ #EXEC2 |
---|
| 830 | @(interaction_is_not_silent … EXEC2) |
---|
| 831 | ] |
---|
| 832 | ] |
---|
[399] | 833 | |
---|
[487] | 834 | | *; #NOTUNREACTIVE |
---|
| 835 | cut (∀tr,s1,e1.execution_isteps tr s e s1 e1 → |
---|
[399] | 836 | ∃x.execution_isteps (\fst x) s1 e1 (\fst (\snd x)) (\snd (\snd x)) ∧ (\fst x) ≠ E0); |
---|
[487] | 837 | [ #tr #s1 #e1 #STEPS |
---|
| 838 | @(classical_doubleneg classic) % #NOREACTION |
---|
| 839 | @NOTUNREACTIVE |
---|
| 840 | %{ tr} %{s1} %{e1} % //; |
---|
| 841 | #tr2 #s2 #e2 #STEPS2 |
---|
| 842 | lapply (not_ex_all_not … NOREACTION); #NR1 |
---|
| 843 | lapply (not_and_to_imply classic … (NR1 〈tr2,〈s2,e2〉〉)); #NR2 |
---|
| 844 | @(classical_doubleneg classic) |
---|
| 845 | @NR2 normalize // |
---|
| 846 | | #REACTIVE |
---|
| 847 | @ec_reacts |
---|
| 848 | [ 2: @reacts |
---|
| 849 | @(show_reactive ge s … EXEC) |
---|
| 850 | #tr #s1 #e1 #STEPS |
---|
| 851 | @constructive_indefinite_description |
---|
| 852 | @(REACTIVE … tr s1 e1 STEPS) |
---|
| 853 | | skip |
---|
| 854 | ] |
---|
| 855 | ] |
---|
| 856 | ] |
---|
[399] | 857 | |
---|
[487] | 858 | | #NOTNONTERMINATING lapply (classical_not_all_ex_not classic … NOTNONTERMINATING); |
---|
| 859 | *; #tr #NNT2 lapply (classical_not_all_ex_not classic … NNT2); |
---|
| 860 | *; #s' #NNT3 lapply (classical_not_all_ex_not classic … NNT3); |
---|
| 861 | *; #e #NNT4 elim (imply_to_and classic … NNT4); |
---|
| 862 | cases e; |
---|
[1713] | 863 | [ #tr' #r #STEPS #NOSTEP |
---|
| 864 | @(ec_terminates s r ? (Eapp tr tr')) % |
---|
[487] | 865 | [ @s' |
---|
| 866 | | @STEPS |
---|
| 867 | ] |
---|
| 868 | | #tr' #s'' #e' #STEPS *; #NOSTEP @False_rect_Type0 |
---|
| 869 | @NOSTEP // |
---|
[797] | 870 | | #msg #STEPS #NOSTEP |
---|
[487] | 871 | @(ec_wrong ? s s' tr) % //; |
---|
[399] | 872 | (* The following is stupidly complicated when most of the cases are impossible. |
---|
| 873 | It ought to be simplified. *) |
---|
[487] | 874 | | #o #k #i #e' #STEPS #NOSTEP |
---|
| 875 | cases e' in STEPS NOSTEP; |
---|
[1713] | 876 | [ #tr' #r #STEPS #NOSTEP |
---|
[487] | 877 | @(ec_terminates s ???) |
---|
[1713] | 878 | [ 3: @(annoying_corner_case_terminates … STEPS) ] |
---|
[487] | 879 | | #tr1 #s1 #e1 #STEPS *; #NOSTEP |
---|
| 880 | @False_ind @NOSTEP // |
---|
[797] | 881 | | #msg #STEPS #NOSTEP |
---|
[487] | 882 | lapply (exec_step_interaction ge s'); |
---|
| 883 | cases (several_steps … STEPS EXEC); #_ |
---|
| 884 | whd in ⊢ (% → ?); |
---|
| 885 | >(exec_inf_aux_unfold …) |
---|
| 886 | cases (exec_step ge s'); |
---|
| 887 | [ #o1 #k1 #EXEC' #H whd in EXEC':(?%?) H; |
---|
[1350] | 888 | cases (se_inv … EXEC'); *; #E1 #E2 #H2 destruct (E1 E2); normalize in H2; |
---|
[1516] | 889 | cases (H i); #tr1 *; #s1 *; #K #E >K in H2; |
---|
[487] | 890 | >(exec_inf_aux_unfold …) |
---|
[1516] | 891 | whd in ⊢ (?%? → ?); @is_final_elim [ #r ] |
---|
[487] | 892 | #F #S whd in S:(?%?); cases (se_inv … S); |
---|
[1516] | 893 | | #x cases x; #tr' #s' whd in ⊢ (?%? → ?); |
---|
[891] | 894 | @is_final_elim' [ #r ] #F #S whd in S:(?%?); |
---|
[487] | 895 | cases (se_inv … S); |
---|
[797] | 896 | | #msg #S cases (se_inv … S); |
---|
[487] | 897 | ] |
---|
| 898 | | #o1 #k1 #i1 #e1 #STEPS #NOSTEP |
---|
| 899 | lapply (exec_step_interaction ge s'); |
---|
| 900 | cases (several_steps … STEPS EXEC); #_ |
---|
| 901 | whd in ⊢ (% → ?); |
---|
| 902 | >(exec_inf_aux_unfold …) |
---|
| 903 | cases (exec_step ge s'); |
---|
| 904 | [ #o1 #k1 #EXEC' #H whd in EXEC':(?%?) H; |
---|
[1350] | 905 | cases (se_inv … EXEC'); *; #E1 #E2 #H2 destruct (E1 E2); normalize in H2; |
---|
[1516] | 906 | cases (H i); #tr1 *; #s1 *; #K #E >K in H2; |
---|
[487] | 907 | >(exec_inf_aux_unfold …) |
---|
[1516] | 908 | whd in ⊢ (?%? → ?); @is_final_elim [ #r ] |
---|
[487] | 909 | #F #S whd in S:(?%?); cases (se_inv … S); |
---|
[1516] | 910 | | #x cases x; #tr' #s' whd in ⊢ (?%? → ?); |
---|
[891] | 911 | @is_final_elim' [ #r ] #F #S whd in S:(?%?); |
---|
[487] | 912 | cases (se_inv … S); |
---|
[797] | 913 | | #msg #S cases (se_inv … S); |
---|
[487] | 914 | ] |
---|
| 915 | ] |
---|
| 916 | ] |
---|
| 917 | ] |
---|
| 918 | qed. |
---|
[399] | 919 | |
---|
[487] | 920 | inductive execution_matches_behavior: s_execution → program_behavior → Prop ≝ |
---|
[1713] | 921 | | emb_terminates: ∀s,e,tr,r. |
---|
| 922 | execution_terminates tr s e r → |
---|
[399] | 923 | execution_matches_behavior e (Terminates tr r) |
---|
| 924 | | emb_diverges: ∀s,e,tr. |
---|
| 925 | execution_diverges tr s e → |
---|
| 926 | execution_matches_behavior e (Diverges tr) |
---|
| 927 | | emb_reacts: ∀s,e,tr. |
---|
| 928 | execution_reacts tr s e → |
---|
| 929 | execution_matches_behavior e (Reacts tr) |
---|
| 930 | | emb_wrong: ∀e,s,s',tr. |
---|
| 931 | execution_goes_wrong tr s e s' → |
---|
| 932 | execution_matches_behavior e (Goes_wrong tr) |
---|
[797] | 933 | | emb_initially_wrong: ∀msg. |
---|
| 934 | execution_matches_behavior (se_wrong msg) (Goes_wrong E0). |
---|
[399] | 935 | |
---|
[1713] | 936 | lemma exec_state_terminates: ∀tr,tr',s,s',e,r. |
---|
| 937 | execution_terminates tr s (se_step tr' s' e) r → s = s'. |
---|
| 938 | #tr #tr' #s #s' #e #r #H inversion H; |
---|
| 939 | [ #s1 #s2 #tr1 #tr2 #r' #e' #H' #E1 #E2 #E3 #E4 #_ destruct; @refl |
---|
| 940 | | #s1 #s2 #tr1 #tr2 #r' #e' #o #k #i #H' #E1 #E2 #E3 #E4 #_ destruct; @refl |
---|
[487] | 941 | ] qed. |
---|
[399] | 942 | |
---|
[487] | 943 | lemma exec_state_diverges: ∀tr,tr',s,s',e. |
---|
[399] | 944 | execution_diverges tr s (se_step tr' s' e) → s = s'. |
---|
[487] | 945 | #tr #tr' #s #s' #e #H inversion H; |
---|
[1510] | 946 | #tr1 #s1 #s2 #e1 #e2 #H' #E1 #E2 #E3 #E4 #_ destruct; @refl qed. |
---|
[399] | 947 | |
---|
[487] | 948 | lemma exec_state_reacts: ∀tr,tr',s,s',e. |
---|
[399] | 949 | execution_reacts tr s (se_step tr' s' e) → s = s'. |
---|
[487] | 950 | #tr #tr' #s #s' #e #H inversion H; |
---|
[1510] | 951 | #tr1 #s1 #e1 #H' #E1 #E2 #E3 #_ destruct; @refl qed. |
---|
[399] | 952 | |
---|
[487] | 953 | lemma exec_state_wrong: ∀tr,tr',s,s',s'',e. |
---|
[399] | 954 | execution_goes_wrong tr s (se_step tr' s' e) s'' → s = s'. |
---|
[487] | 955 | #tr #tr' #s #s' #s'' #e #H inversion H; |
---|
[1510] | 956 | #tr1 #s1 #s2 #e1 #msg #H' #E1 #E2 #E3 #E4 #_ destruct; @refl qed. |
---|
[399] | 957 | |
---|
[487] | 958 | lemma behavior_of_execution: ∀s,e. |
---|
[399] | 959 | execution_characterisation s e → |
---|
| 960 | ∃b:program_behavior. execution_matches_behavior e b. |
---|
[487] | 961 | #s0 #e0 #exec |
---|
| 962 | cases exec; |
---|
[1713] | 963 | [ #s #r #e #tr #TERM |
---|
[487] | 964 | %{ (Terminates tr r)} |
---|
| 965 | @(emb_terminates … TERM) |
---|
| 966 | | #s #e #tr #DIV |
---|
| 967 | %{ (Diverges tr)} |
---|
| 968 | @(emb_diverges … DIV) |
---|
| 969 | | #s #e #tr #REACTS |
---|
| 970 | %{ (Reacts tr)} |
---|
| 971 | @(emb_reacts … REACTS) |
---|
| 972 | | #e #s #s' #tr #WRONG |
---|
| 973 | %{ (Goes_wrong tr)} |
---|
| 974 | @(emb_wrong … WRONG) |
---|
| 975 | ] qed. |
---|
[399] | 976 | |
---|
[487] | 977 | lemma initial_state_not_final: ∀ge,s. |
---|
[399] | 978 | initial_state ge s → |
---|
| 979 | ¬ ∃r.final_state s r. |
---|
[487] | 980 | #ge #s #H cases H; |
---|
| 981 | #b #f #ge #m #E1 #E2 #E3 #E4 % *; #r #H2 |
---|
| 982 | inversion H2; |
---|
[1713] | 983 | #r' #E5 #E6 destruct (E5); |
---|
[487] | 984 | qed. |
---|
[399] | 985 | |
---|
[487] | 986 | lemma initial_step: ∀ge,s,e. |
---|
[732] | 987 | exec_inf_aux ?? clight_exec ge (Value ??? 〈E0,s〉) = e → |
---|
[399] | 988 | ¬(∃r.final_state s r) → |
---|
[708] | 989 | ∃e'.e = e_step ??? E0 s e'. |
---|
[487] | 990 | #ge #s #e >(exec_inf_aux_unfold …) |
---|
[1516] | 991 | whd in ⊢ (??%? → ?); @is_final_elim' |
---|
[708] | 992 | [ #r #FINAL #EXEC #NOTFINAL |
---|
[487] | 993 | @False_ind @(absurd ?? NOTFINAL) |
---|
[708] | 994 | %{r} @FINAL |
---|
[487] | 995 | | #F1 #EXEC #F2 whd in EXEC:(??%?); % [ 2: <EXEC @refl ] |
---|
| 996 | qed. |
---|
[399] | 997 | |
---|
[487] | 998 | theorem exec_inf_equivalence: |
---|
[399] | 999 | ∀classic:(∀P:Prop.P ∨ ¬P). |
---|
[487] | 1000 | ∀constructive_indefinite_description:(∀A:Type[0]. ∀P:A→Prop. (∃x. P x) → Sig A P). |
---|
[732] | 1001 | ∀p,e. single_exec_of (exec_inf ?? clight_fullexec p) e → |
---|
[399] | 1002 | ∃b.execution_matches_behavior e b ∧ exec_program p b. |
---|
[487] | 1003 | #classic #constructive_indefinite_description #p #e |
---|
| 1004 | whd in ⊢ (?%? → ??(λ_.?(?%?)%)); |
---|
[891] | 1005 | lapply (make_initial_state_sound p) |
---|
| 1006 | lapply (the_initial_state p) |
---|
[1516] | 1007 | whd in ⊢ (? → ? → ?(match % with [_ ⇒ ? | _ ⇒ ?])? → ?); |
---|
[891] | 1008 | cases (make_initial_state p) |
---|
[1244] | 1009 | [ #s #INITIAL' #INITIAL whd in INITIAL ⊢ (?%? → ?); |
---|
[891] | 1010 | >exec_inf_aux_unfold |
---|
[1516] | 1011 | whd in ⊢ (?%? → ?); |
---|
[891] | 1012 | @is_final_elim' |
---|
[708] | 1013 | [ #r #F @False_ind |
---|
[1244] | 1014 | @(absurd ?? (initial_state_not_final … INITIAL)) |
---|
[708] | 1015 | %{r} @F |
---|
[487] | 1016 | | #NOTFINAL whd in ⊢ (?%? → ?); cases e; |
---|
[1713] | 1017 | [ #tr #r #EXEC0 | #tr #s' #e0 #EXEC0 | #msg #EXEC0 | #o #k #i #e #EXEC0 ] |
---|
[487] | 1018 | cases (se_inv … EXEC0); *; #E1 #E2 <E1 <E2 #EXEC' |
---|
| 1019 | lapply (behavior_of_execution ?? |
---|
[1244] | 1020 | (execution_characterisation_complete classic constructive_indefinite_description ? s ? EXEC')); |
---|
[891] | 1021 | *; #b #MATCHES %{b} % [ @MATCHES ] |
---|
[1244] | 1022 | #ge #Ege |
---|
[487] | 1023 | inversion MATCHES; |
---|
[1713] | 1024 | [ #s0 #e1 #tr1 #r #TERM #EXEC #BEHAVES <EXEC in TERM; |
---|
[487] | 1025 | #TERM |
---|
| 1026 | lapply (exec_state_terminates … TERM); #E1 |
---|
[1516] | 1027 | >E1 in TERM; #TERM #_ |
---|
[487] | 1028 | @(program_terminates (mk_transrel … step) ?? ge s) |
---|
[1244] | 1029 | [ 2: @INITIAL |
---|
| 1030 | | 3: <Ege @(terminates_sound … TERM EXEC') |
---|
[487] | 1031 | | skip |
---|
| 1032 | | //; |
---|
| 1033 | ] |
---|
[1516] | 1034 | | #s0 #e #tr #DIVERGES #EXEC #E2 <EXEC in DIVERGES; #DIVERGES |
---|
[487] | 1035 | lapply (exec_state_diverges … DIVERGES); |
---|
[1516] | 1036 | #E1 >E1 in DIVERGES; #DIVERGES #_ |
---|
[487] | 1037 | inversion DIVERGES; #tr' #s1 #s2 #e1 #e2 #INITSTEPS #DIVERGING #E4 #E5 #E6 |
---|
[1516] | 1038 | <E4 in INITSTEPS ⊢ %; <E5 in E6 ⊢ %; #E6 #INITSTEPS |
---|
[487] | 1039 | cut (e0 = e1); [ destruct (E6) skip (MATCHES EXEC0 EXEC'); // ] |
---|
[1516] | 1040 | #E7 <E7 in INITSTEPS; #INITSTEPS |
---|
[1510] | 1041 | cases (several_steps … INITSTEPS EXEC'); #INITSTAR #EXECDIV #_ |
---|
[1244] | 1042 | @(program_diverges (mk_transrel … step) ?? ge s … INITIAL) |
---|
| 1043 | [ 2: <Ege @INITSTAR |
---|
| 1044 | | 3: <Ege @(silent_sound … DIVERGING EXECDIV) |
---|
| 1045 | ] |
---|
[1516] | 1046 | | #s0 #e #tr #REACTS #EXEC #E2 <EXEC in REACTS; #REACTS |
---|
[487] | 1047 | lapply (exec_state_reacts … REACTS); |
---|
[1516] | 1048 | #E1 >E1 in REACTS; #REACTS #_ |
---|
[487] | 1049 | inversion REACTS; #tr' #s' #e'' #REACTING #E4 #E5 |
---|
[1516] | 1050 | <E4 in REACTING ⊢ %; <E5 #REACTING #E6 |
---|
[487] | 1051 | cut (e0 = e''); [ destruct (E6) skip (MATCHES EXEC0 EXEC'); // ] |
---|
[1516] | 1052 | #E7 <E7 in REACTING; #REACTING #_ |
---|
[1244] | 1053 | @(program_reacts (mk_transrel … step) ?? ge s … INITIAL) |
---|
| 1054 | <Ege @(reacts_sound … REACTING EXEC') |
---|
[1516] | 1055 | | #e #s1 #s2 #tr #WRONG #EXEC #E2 <EXEC in WRONG; #WRONG |
---|
[487] | 1056 | lapply (exec_state_wrong … WRONG); |
---|
[1516] | 1057 | #E1 >E1 in WRONG; #WRONG #_ |
---|
[797] | 1058 | inversion WRONG; #tr' #s1' #s2' #e'' #msg #GOESWRONG #E4 #E5 #E6 #E7 |
---|
[1516] | 1059 | <E4 in GOESWRONG ⊢ %; <E5 <E7 #GOESWRONG |
---|
[487] | 1060 | cut (e0 = e''); [ destruct (E6) skip (INITIAL Ege MATCHES EXEC0 EXEC'); // ] |
---|
[1516] | 1061 | #E8 <E8 in GOESWRONG; #GOESWRONG |
---|
[487] | 1062 | elim (wrong_sound … WRONG EXEC' NOTFINAL); *; #STAR #STOP #FINAL |
---|
[1510] | 1063 | <Ege #_ |
---|
[1244] | 1064 | @(program_goes_wrong (mk_transrel … step) ?? ? s … INITIAL STAR STOP) |
---|
[487] | 1065 | #r % #F @(absurd ?? FINAL) %{r} @F |
---|
[797] | 1066 | | #msg #E destruct (E); |
---|
[487] | 1067 | ] |
---|
| 1068 | ] |
---|
[797] | 1069 | | #msg whd in ⊢ ((∀_.? → %) → ?); |
---|
[487] | 1070 | #NOINIT #_ #EXEC |
---|
| 1071 | %{ (Goes_wrong E0)} % |
---|
| 1072 | [ whd in EXEC:(?%?); |
---|
| 1073 | cases e in EXEC; |
---|
[1713] | 1074 | [ #tr #r #EXEC0 | #tr #s' #e0 #EXEC0 | #msg #EXEC0 | #o #k #i #e #EXEC0 ] |
---|
[487] | 1075 | cases (se_inv … EXEC0); |
---|
| 1076 | @emb_initially_wrong |
---|
| 1077 | | #ge #Ege |
---|
| 1078 | @program_goes_initially_wrong |
---|
| 1079 | #s % #INIT cases (NOINIT s INIT); #ge' #H @H |
---|
| 1080 | ] |
---|
| 1081 | ] qed. |
---|
[399] | 1082 | |
---|