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