[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] ≝ |
---|
[398] | 10 | | se_stop : trace → int → mem → s_execution |
---|
| 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 ≝ |
---|
[1216] | 16 | | seo_stop : ∀tr,r,s. single_exec_of (e_stop ??? tr r s) (se_stop tr r (mem_of_state s)) |
---|
[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 | |
---|
[708] | 159 | lemma exec_from_interact_stop : ∀ge,s,o,k,i,tr,r,m. |
---|
[398] | 160 | exec_from ge s (se_interact o k i (se_stop tr r m)) → |
---|
[961] | 161 | step ge s tr (Returnstate (Vint I32 r) Kstop m). |
---|
[487] | 162 | #ge #s0 #o0 #k0 #i0 #tr0 #s0' #e0 #H inversion H; |
---|
| 163 | [ #tr #r #m #E1 #E2 destruct |
---|
| 164 | | #tr #s #e #se #H1 #H2 #E destruct (E) |
---|
[797] | 165 | | #msg #_ #E destruct |
---|
[1510] | 166 | | #o #k #i #se #H1 #H2 #E #_ destruct (E); |
---|
[487] | 167 | lapply (exec_step_sound ge s0); |
---|
| 168 | >(exec_inf_aux_unfold …) in H2; |
---|
| 169 | cases (exec_step ge s0); |
---|
| 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:(∀_. ? → ? → ?%); |
---|
[1516] | 180 | change in match (is_final ?????); with (is_final s2) |
---|
[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 | |
---|
[487] | 228 | inductive execution_terminates : trace → state → s_execution → int → mem → Prop ≝ |
---|
[398] | 229 | | terminates : ∀s,s',tr,tr',r,e,m. |
---|
| 230 | execution_isteps tr s e s' (se_stop tr' r m) → |
---|
| 231 | execution_terminates (tr⧺tr') s (se_step E0 s e) r m |
---|
| 232 | (* We should only be able to get to here if main is an external function, which is silly. *) |
---|
| 233 | | annoying_corner_case_terminates: ∀s,s',tr,tr',r,e,m,o,k,i. |
---|
| 234 | execution_isteps tr s e s' (se_interact o k i (se_stop tr' r m)) → |
---|
| 235 | execution_terminates (tr⧺tr') s (se_step E0 s e) r m. |
---|
| 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 | |
---|
[708] | 280 | lemma final_step: ∀ge,tr,r,m,s. |
---|
[398] | 281 | exec_from ge s (se_stop tr r m) → |
---|
[961] | 282 | step ge s tr (Returnstate (Vint I32 r) Kstop m). |
---|
[487] | 283 | #ge #tr #r #m #s #EXEC |
---|
| 284 | whd in EXEC; |
---|
| 285 | inversion EXEC; |
---|
[1510] | 286 | [ #tr' #r' #m' #EXEC' #E #_ destruct (E); |
---|
[487] | 287 | lapply (exec_step_sound ge s); |
---|
| 288 | >(exec_inf_aux_unfold …) in EXEC'; |
---|
| 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 | ] |
---|
[1510] | 296 | inversion FINAL; #r''' #m' #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 → |
---|
| 306 | x = Value ??? 〈tr,Returnstate (Vint I32 r) Kstop (mem_of_state s)〉. |
---|
| 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' |
---|
[702] | 311 | [ #r' #FINAL cases FINAL; #r'' #m' #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 | |
---|
[487] | 318 | lemma terminates_sound: ∀ge,tr,s,r,m,e. |
---|
[398] | 319 | execution_terminates tr s (se_step E0 s e) r m → |
---|
| 320 | exec_from ge s e → |
---|
[961] | 321 | star (mk_transrel … step) ge s tr (Returnstate (Vint I32 r) Kstop m). |
---|
[487] | 322 | #ge #tr0 #s0 #r #m #e0 #H inversion H; |
---|
[1510] | 323 | [ #s #s' #tr #tr' #r #e #m #ESTEPS #E1 #E2 #E3 #E4 #E5 #_ #EXEC |
---|
[487] | 324 | destruct (E1 E2 E3 E4 E5); |
---|
| 325 | cases (several_steps … ESTEPS EXEC); #STARs' #EXECs' |
---|
| 326 | @(star_right … STARs') |
---|
| 327 | [ 2: @(final_step ge tr' r m s' … EXECs') |
---|
| 328 | | skip |
---|
| 329 | | @refl |
---|
| 330 | ] |
---|
[1510] | 331 | | #s #s' #tr #tr' #r #e #m #o #k #i #ESTEPS #E1 #E2 #E3 #E4 #E5 #_ #EXEC |
---|
[487] | 332 | destruct; |
---|
| 333 | cases (several_steps … ESTEPS EXEC); #STARs' #EXECs' |
---|
| 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 |
---|
| 405 | % *; #r #F cases F in H; #r' #m #H |
---|
| 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:(∀_. ? → ? → ?%); |
---|
[1516] | 422 | change in match (is_final ?????); with (is_final s2) |
---|
[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 ≝ |
---|
[399] | 471 | | ec_terminates: ∀s,r,m,e,tr. |
---|
| 472 | execution_terminates tr s e r m → |
---|
| 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; |
---|
| 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 ] |
---|
| 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 |
---|
| 523 | | 4,7: @err2_does_not_interact #x1 #x2 @err_does_not_interact #x3 @I |
---|
| 524 | | @err2_does_not_interact #x1 #x2 cases x1; //; |
---|
| 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; |
---|
| 545 | [ 8: #x1 #x2 #x3 #x4 cases x1; |
---|
| 546 | [ whd in ⊢ (???%); cases v; // | #x5 whd in ⊢ (???%); cases x5; |
---|
| 547 | #x6 #x7 @opt_does_not_interact // ] |
---|
| 548 | | *: // ] |
---|
| 549 | ] qed. |
---|
[399] | 550 | |
---|
| 551 | |
---|
| 552 | (* Some classical logic (roughly like a fragment of Coq's library) *) |
---|
[487] | 553 | lemma classical_doubleneg: |
---|
[399] | 554 | ∀classic:(∀P:Prop.P ∨ ¬P). |
---|
| 555 | ∀P:Prop. ¬ (¬ P) → P. |
---|
[487] | 556 | #classic #P *; #H |
---|
| 557 | cases (classic P); |
---|
| 558 | [ // | #H' @False_ind /2/; ] |
---|
| 559 | qed. |
---|
[399] | 560 | |
---|
[487] | 561 | lemma classical_not_all_not_ex: |
---|
[399] | 562 | ∀classic:(∀P:Prop.P ∨ ¬P). |
---|
[487] | 563 | ∀A:Type[0].∀P:A → Prop. ¬ (∀x. ¬ P x) → ∃x. P x. |
---|
| 564 | #classic #A #P *; #H |
---|
| 565 | @(classical_doubleneg classic) % *; #H' |
---|
| 566 | @H #x % #H'' @H' %{x} @H'' |
---|
| 567 | qed. |
---|
[399] | 568 | |
---|
[487] | 569 | lemma classical_not_all_ex_not: |
---|
[399] | 570 | ∀classic:(∀P:Prop.P ∨ ¬P). |
---|
[487] | 571 | ∀A:Type[0].∀P:A → Prop. ¬ (∀x. P x) → ∃x. ¬ P x. |
---|
| 572 | #classic #A #P *; #H |
---|
| 573 | @(classical_not_all_not_ex classic A (λx.¬ P x)) |
---|
| 574 | % #H' @H #x @(classical_doubleneg classic) |
---|
| 575 | @H' |
---|
| 576 | qed. |
---|
[399] | 577 | |
---|
[487] | 578 | lemma not_ex_all_not: |
---|
| 579 | ∀A:Type[0].∀P:A → Prop. ¬ (∃x. P x) → ∀x. ¬ P x. |
---|
| 580 | #A #P *; #H #x % #H' |
---|
| 581 | @H %{ x} @H' |
---|
| 582 | qed. |
---|
[399] | 583 | |
---|
[487] | 584 | lemma not_imply_elim: |
---|
[399] | 585 | ∀classic:(∀P:Prop.P ∨ ¬P). |
---|
| 586 | ∀P,Q:Prop. ¬ (P → Q) → P. |
---|
[487] | 587 | #classic #P #Q *; #H |
---|
| 588 | @(classical_doubleneg classic) % *; #H' |
---|
| 589 | @H #H'' @False_ind @H' @H'' |
---|
| 590 | qed. |
---|
[399] | 591 | |
---|
[487] | 592 | lemma not_imply_elim2: |
---|
[399] | 593 | ∀P,Q:Prop. ¬ (P → Q) → ¬ Q. |
---|
[487] | 594 | #P #Q *; #H % #H' |
---|
| 595 | @H #_ @H' |
---|
| 596 | qed. |
---|
[399] | 597 | |
---|
[487] | 598 | lemma imply_to_and: |
---|
[399] | 599 | ∀classic:(∀P:Prop.P ∨ ¬P). |
---|
| 600 | ∀P,Q:Prop. ¬ (P → Q) → P ∧ ¬Q. |
---|
[487] | 601 | #classic #P #Q #H % |
---|
| 602 | [ @(not_imply_elim classic P Q H) |
---|
| 603 | | @(not_imply_elim2 P Q H) |
---|
| 604 | ] qed. |
---|
[399] | 605 | |
---|
[487] | 606 | lemma not_and_to_imply: |
---|
[399] | 607 | ∀classic:(∀P:Prop.P ∨ ¬P). |
---|
| 608 | ∀P,Q:Prop. ¬ (P ∧ Q) → P → ¬Q. |
---|
[487] | 609 | #classic #P #Q *; #H #H' |
---|
| 610 | % #H'' @H % //; |
---|
| 611 | qed. |
---|
[399] | 612 | |
---|
[487] | 613 | inductive execution_not_over : s_execution → Prop ≝ |
---|
[399] | 614 | | eno_step: ∀tr,s,e. execution_not_over (se_step tr s e) |
---|
| 615 | | eno_interact: ∀o,k,tr,s,e,i. execution_not_over (se_interact o k i (se_step tr s e)). |
---|
| 616 | |
---|
[487] | 617 | lemma eno_stop: ∀tr,r,m. execution_not_over (se_stop tr r m) → False. |
---|
| 618 | #tr0 #r0 #m0 #H inversion H; |
---|
| 619 | [ #tr #s #e #E destruct |
---|
| 620 | | #o #k #tr #s #e #i #E destruct |
---|
| 621 | ] qed. |
---|
[399] | 622 | |
---|
[797] | 623 | lemma eno_wrong: ∀msg. execution_not_over (se_wrong msg) → False. |
---|
| 624 | #msg #H inversion H; |
---|
[487] | 625 | [ #tr #s #e #E destruct |
---|
| 626 | | #o #k #tr #s #e #i #E destruct |
---|
| 627 | ] qed. |
---|
[399] | 628 | |
---|
[487] | 629 | let corec show_divergence s e |
---|
[399] | 630 | (NONTERMINATING:∀tr1,s1,e1. execution_isteps tr1 s e s1 e1 → |
---|
| 631 | execution_not_over e1) |
---|
| 632 | (UNREACTIVE:∀tr2,s2,e2. execution_isteps tr2 s e s2 e2 → tr2 = E0) |
---|
[487] | 633 | (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] | 634 | : execution_diverging e ≝ ?. |
---|
[487] | 635 | lapply (NONTERMINATING E0 s e ?); //; |
---|
| 636 | cases e in UNREACTIVE NONTERMINATING CONTINUES ⊢ %; |
---|
| 637 | [ #tr #i #m #_ #_ #_ #ENO elim (eno_stop … ENO); |
---|
| 638 | | #tr #s' #e' #UNREACTIVE lapply (UNREACTIVE tr s' e' ?); |
---|
[1516] | 639 | [ <(E0_right tr) in ⊢ (?%????); |
---|
[487] | 640 | @isteps_one @isteps_none |
---|
| 641 | | #TR @(match sym_eq ??? TR with [ refl ⇒ ? ]) (* >TR in UNREACTIVE ⊢ % *) |
---|
| 642 | #NONTERMINATING #CONTINUES #_ % |
---|
| 643 | @(show_divergence s') |
---|
| 644 | [ #tr1 #s1 #e1 #S @(NONTERMINATING tr1 s1 e1) |
---|
[1516] | 645 | change in ⊢ (?%????); with (Eapp E0 tr1); @isteps_one |
---|
[487] | 646 | @S |
---|
[1516] | 647 | | #tr2 #s2 #e2 #S >TR in UNREACTIVE; #UNREACTIVE @(UNREACTIVE tr2 s2 e2) |
---|
| 648 | change in ⊢ (?%????); with (Eapp E0 tr2); |
---|
[487] | 649 | @isteps_one @S |
---|
| 650 | | #tr2 #s2 #o #k #i #e2 #S @(CONTINUES tr2 s2 o k i) |
---|
[1516] | 651 | change in ⊢ (?%????); with (Eapp E0 tr2); |
---|
[487] | 652 | @(isteps_one … S) |
---|
| 653 | ] |
---|
| 654 | ] |
---|
[797] | 655 | | #msg #_ #_ #_ #ENO elim (eno_wrong … ENO); |
---|
[487] | 656 | | #o #k #i #e' #UNREACTIVE #NONTERMINATING #CONTINUES #_ |
---|
| 657 | lapply (CONTINUES E0 s o k i e' (isteps_none …)); |
---|
| 658 | *; #tr' *; #s' *; #e' *; #EXEC #NOTSILENT |
---|
| 659 | @False_ind @(absurd ?? NOTSILENT) |
---|
| 660 | @(UNREACTIVE … s' e') |
---|
[1516] | 661 | <(E0_right tr') in ⊢ (?%????); |
---|
[487] | 662 | >EXEC |
---|
| 663 | @isteps_interact //; |
---|
| 664 | ] qed. |
---|
[399] | 665 | |
---|
[487] | 666 | lemma se_inv: ∀e1,e2. |
---|
[399] | 667 | single_exec_of e1 e2 → |
---|
| 668 | match e1 with |
---|
[1216] | 669 | [ e_stop tr r s ⇒ match e2 with [ se_stop tr' r' m' ⇒ tr = tr' ∧ r = r' ∧ mem_of_state s = m' | _ ⇒ False ] |
---|
[399] | 670 | | e_step tr s e1' ⇒ match e2 with [ se_step tr' s' e2' ⇒ tr = tr' ∧ s = s' ∧ single_exec_of e1' e2' | _ ⇒ False ] |
---|
[797] | 671 | | e_wrong _ ⇒ match e2 with [ se_wrong _ ⇒ True | _ ⇒ False ] |
---|
[399] | 672 | | e_interact o k ⇒ match e2 with [ se_interact o' k' i e ⇒ o' = o ∧ k' ≃ k ∧ single_exec_of (k' i) e | _ ⇒ False ] |
---|
| 673 | ]. |
---|
[487] | 674 | #e01 #e02 #H |
---|
| 675 | cases H; |
---|
[1216] | 676 | [ #tr #r #s whd; % [ % ] // |
---|
[487] | 677 | | #tr #s #e1' #e2' #H' whd; % [ % ] // |
---|
[797] | 678 | | #msg whd; // |
---|
[487] | 679 | | #o #k #i #e #H' whd; % [ % ] // |
---|
| 680 | ] qed. |
---|
[399] | 681 | |
---|
[487] | 682 | lemma interaction_is_not_silent: ∀ge,o,k,i,tr,s,s',e. |
---|
[399] | 683 | exec_from ge s (se_interact o k i (se_step tr s' e)) → |
---|
| 684 | tr ≠ E0. |
---|
[487] | 685 | #ge #o #k #i #tr #s #s' #e whd in ⊢ (% → ?); >(exec_inf_aux_unfold …) |
---|
| 686 | lapply (exec_step_interaction ge s); |
---|
| 687 | cases (exec_step ge s); |
---|
| 688 | [ #o' #k' ; whd in ⊢ (% → ?%? → ?); #H #K cases (se_inv … K); |
---|
| 689 | *; #E1 #E2 #H1 destruct (E1); |
---|
| 690 | lapply (H i); *; #tr' *; #s'' *; #K' #TR |
---|
[1516] | 691 | >E2 in H1; #H1 whd in H1:(?%?); >K' in H1; |
---|
[487] | 692 | >(exec_inf_aux_unfold …) whd in ⊢ (?%? → ?); |
---|
[1516] | 693 | change in match (is_final ?????); with (is_final s'') |
---|
[708] | 694 | @is_final_elim |
---|
| 695 | [ #r #F whd in ⊢ (?%? → ?); #S |
---|
[487] | 696 | @False_ind @(absurd ? S) cases (se_inv … S) |
---|
| 697 | | #NF #S whd in S:(?%?); cases (se_inv … S); |
---|
| 698 | *; #E1 #E2 #S' <E1 @TR |
---|
| 699 | ] |
---|
[1516] | 700 | | #x cases x; #tr' #s'' #H whd in ⊢ (?%? → ?); |
---|
[891] | 701 | @is_final_elim' [ #r ] #F #E whd in E:(?%?); |
---|
[487] | 702 | inversion E; |
---|
| 703 | [ 1,5: #tr1 #e1 #m1 #E1 #E2 destruct |
---|
| 704 | | 2,6: #tr #s1 #e1 #e2 #H #E1 #E2 destruct |
---|
[797] | 705 | | 3,7: #msg #E destruct |
---|
[487] | 706 | | 4,8: #o1 #k1 #i1 #e1 #H1 #E1 #E2 destruct |
---|
| 707 | ] |
---|
[797] | 708 | | #msg #_ #E whd in E:(?%?); |
---|
[487] | 709 | inversion E; |
---|
| 710 | [ 1,5: #tr1 #e1 #m1 #E1 #E2 destruct |
---|
| 711 | | 2,6: #tr #s1 #e1 #e2 #H #E1 #E2 destruct |
---|
[797] | 712 | | 3,7: #msg #E1 #E2 destruct |
---|
[487] | 713 | | 4,8: #o1 #k1 #i1 #e1 #H1 #E1 #E2 destruct |
---|
| 714 | ] |
---|
| 715 | ] qed. |
---|
[399] | 716 | |
---|
[487] | 717 | let corec reactive_traceinf' ge s e |
---|
[399] | 718 | (EXEC:exec_from ge s e) |
---|
| 719 | (REACTIVE: ∀tr,s1,e1. |
---|
| 720 | execution_isteps tr s e s1 e1 → |
---|
[487] | 721 | (Sig ? (λx.execution_isteps (\fst x) s1 e1 (\fst (\snd x)) (\snd (\snd x)) ∧ (\fst x) ≠ E0))) |
---|
[399] | 722 | : traceinf' ≝ ?. |
---|
[487] | 723 | lapply (REACTIVE E0 s e (isteps_none …)); |
---|
| 724 | *; #x cases x; #tr #y cases y; #s' #e' *; #STEPS #H |
---|
| 725 | %{ tr ? H} |
---|
| 726 | @(reactive_traceinf' ge s' e' ?) |
---|
| 727 | [ cases (several_steps … STEPS EXEC); #_ #H' @H' |
---|
| 728 | | #tr1 #s1 #e1 #STEPS1 |
---|
| 729 | @REACTIVE |
---|
| 730 | [ 2: |
---|
| 731 | @(isteps_trans … STEPS STEPS1) |
---|
| 732 | | skip |
---|
| 733 | ] |
---|
| 734 | ] |
---|
| 735 | qed. |
---|
[399] | 736 | |
---|
| 737 | (* A slightly different version of the above, to work around a problem with the |
---|
| 738 | next result. *) |
---|
[487] | 739 | let corec reactive_traceinf'' ge s e |
---|
[399] | 740 | (EXEC:exec_from ge s e) |
---|
[487] | 741 | (REACTIVE0: Sig ? (λx.execution_isteps (\fst x) s e (\fst (\snd x)) (\snd (\snd x)) ∧ (\fst x) ≠ E0)) |
---|
[399] | 742 | (REACTIVE: ∀tr,s1,e1. |
---|
| 743 | execution_isteps tr s e s1 e1 → |
---|
[487] | 744 | (Sig ? (λx.execution_isteps (\fst x) s1 e1 (\fst (\snd x)) (\snd (\snd x)) ∧ (\fst x) ≠ E0))) |
---|
[399] | 745 | : traceinf' ≝ ?. |
---|
[487] | 746 | cases REACTIVE0; #x cases x; #tr #y cases y; #s' #e' *; #STEPS #H |
---|
| 747 | %{ tr ? H} |
---|
| 748 | @(reactive_traceinf'' ge s' e' ?) |
---|
| 749 | [ cases (several_steps … STEPS EXEC); #_ #H' @H' |
---|
| 750 | | @(REACTIVE … STEPS) |
---|
| 751 | | #tr1 #s1 #e1 #STEPS1 |
---|
| 752 | @REACTIVE |
---|
| 753 | [ 2: |
---|
| 754 | @(isteps_trans … STEPS STEPS1) |
---|
| 755 | | skip |
---|
| 756 | ] |
---|
| 757 | ] qed. |
---|
[399] | 758 | |
---|
| 759 | (* We want to prove |
---|
| 760 | |
---|
[487] | 761 | lemma show_reactive : ∀ge,s. |
---|
[399] | 762 | ∀REACTIVE:∀tr,s1,e1. |
---|
| 763 | execution_isteps tr s (exec_inf_aux ge (exec_step ge s)) s1 e1 → |
---|
| 764 | Σx.execution_isteps (\fst x) s1 e1 (\fst (\snd x)) (\snd (\snd x)) ∧ (\fst x) ≠ E0. |
---|
| 765 | execution_reacting (traceinf_of_traceinf' (reactive_traceinf' ge s REACTIVE)) s (exec_inf_aux ge (exec_step ge s)). |
---|
| 766 | |
---|
| 767 | but the current matita won't unfold reactive_traceinf' so that we can do case |
---|
| 768 | analysis on (REACTIVE …). Instead we take an "applied" version of REACTIVE that |
---|
| 769 | we can do case analysis on, then get it into the desired form afterwards. |
---|
| 770 | *) |
---|
[487] | 771 | let corec show_reactive' ge s e |
---|
[399] | 772 | (EXEC:exec_from ge s e) |
---|
[487] | 773 | (REACTIVE0: Sig ? (λx.execution_isteps (\fst x) s e (\fst (\snd x)) (\snd (\snd x)) ∧ (\fst x) ≠ E0)) |
---|
[399] | 774 | (REACTIVE: ∀tr1,s1,e1. |
---|
| 775 | execution_isteps tr1 s e s1 e1 → |
---|
[487] | 776 | (Sig ? (λx.execution_isteps (\fst x) s1 e1 (\fst (\snd x)) (\snd (\snd x)) ∧ (\fst x) ≠ E0))) |
---|
[399] | 777 | : execution_reacting (traceinf_of_traceinf' (reactive_traceinf'' ge s e EXEC REACTIVE0 REACTIVE)) s e ≝ ?. |
---|
[487] | 778 | (*>(unroll_traceinf' (reactive_traceinf'' …)) *) |
---|
| 779 | @(match sym_eq ??? (unroll_traceinf' (reactive_traceinf'' …)) with [ refl ⇒ ? ]) |
---|
| 780 | cases REACTIVE0; |
---|
| 781 | #x cases x; #tr1 #y cases y; #s1 #e1 #z cases z; #STEPS #NOTSILENT |
---|
| 782 | whd in ⊢ (?(?%)??); |
---|
| 783 | (*>(traceinf_traceinfp_app …) *) |
---|
| 784 | @(match sym_eq ??? (traceinf_traceinfp_app …) with [ refl ⇒ ? ]) |
---|
| 785 | @(reacting … STEPS NOTSILENT) |
---|
| 786 | @show_reactive' |
---|
| 787 | qed. |
---|
[399] | 788 | |
---|
[487] | 789 | lemma show_reactive : ∀ge,s,e. |
---|
[399] | 790 | ∀EXEC:exec_from ge s e. |
---|
| 791 | ∀REACTIVE:∀tr,s1,e1. |
---|
| 792 | execution_isteps tr s e s1 e1 → |
---|
[487] | 793 | (Sig ? (λx.execution_isteps (\fst x) s1 e1 (\fst (\snd x)) (\snd (\snd x)) ∧ (\fst x) ≠ E0)). |
---|
[399] | 794 | execution_reacting (traceinf_of_traceinf' (reactive_traceinf'' ge s e EXEC ? REACTIVE)) s e. |
---|
[487] | 795 | [ #ge #s #e #EXEC #REACTIVE |
---|
| 796 | @show_reactive' |
---|
| 797 | | @(REACTIVE … (isteps_none …)) |
---|
| 798 | ] qed. |
---|
[399] | 799 | |
---|
[487] | 800 | lemma execution_characterisation_complete: |
---|
[399] | 801 | ∀classic:(∀P:Prop.P ∨ ¬P). |
---|
[487] | 802 | ∀constructive_indefinite_description:(∀A:Type[0]. ∀P:A→Prop. (∃x. P x) → Sig A P). |
---|
[399] | 803 | ∀ge,s,e. |
---|
| 804 | exec_from ge s e → |
---|
| 805 | execution_characterisation s (se_step E0 s e). |
---|
[487] | 806 | #classic #constructive_indefinite_description #ge #s #e #EXEC |
---|
| 807 | cases (classic (∀tr1,s1,e1. execution_isteps tr1 s e s1 e1 → |
---|
[399] | 808 | execution_not_over e1)); |
---|
[487] | 809 | [ #NONTERMINATING |
---|
| 810 | cases (classic (∃tr,s1,e1. execution_isteps tr s e s1 e1 ∧ |
---|
[399] | 811 | ∀tr2,s2,e2. execution_isteps tr2 s1 e1 s2 e2 → tr2 = E0)); |
---|
[487] | 812 | [ *; #tr *; #s1 *; #e1 *; #INITIAL #UNREACTIVE |
---|
| 813 | @(ec_diverges … s ? tr) |
---|
| 814 | @(diverges_diverging … INITIAL) |
---|
| 815 | @(show_divergence s1 e1) |
---|
| 816 | [ #tr2 #s2 #e2 #S @(NONTERMINATING (Eapp tr tr2) s2 e2) |
---|
| 817 | @(isteps_trans … INITIAL S) |
---|
| 818 | | #tr2 #s2 #e2 #S @(UNREACTIVE … S) |
---|
| 819 | | #tr2 #s2 #o #k #i #e2 #STEPS |
---|
| 820 | lapply (NONTERMINATING (Eapp tr tr2) s2 (se_interact o k i e2) ?); |
---|
| 821 | [ @(isteps_trans … INITIAL STEPS) ] |
---|
| 822 | #NOTOVER inversion NOTOVER; |
---|
| 823 | [ #tr' #s' #e' #E destruct (E); |
---|
[1510] | 824 | | #o' #k' #tr' #s' #e' #i' #E #_ destruct (E); |
---|
[487] | 825 | %{ tr'} %{s'} %{e'} % //; |
---|
| 826 | cases (several_steps … INITIAL EXEC); #_ #EXEC1 |
---|
| 827 | cases (several_steps … STEPS EXEC1); #_ #EXEC2 |
---|
| 828 | @(interaction_is_not_silent … EXEC2) |
---|
| 829 | ] |
---|
| 830 | ] |
---|
[399] | 831 | |
---|
[487] | 832 | | *; #NOTUNREACTIVE |
---|
| 833 | cut (∀tr,s1,e1.execution_isteps tr s e s1 e1 → |
---|
[399] | 834 | ∃x.execution_isteps (\fst x) s1 e1 (\fst (\snd x)) (\snd (\snd x)) ∧ (\fst x) ≠ E0); |
---|
[487] | 835 | [ #tr #s1 #e1 #STEPS |
---|
| 836 | @(classical_doubleneg classic) % #NOREACTION |
---|
| 837 | @NOTUNREACTIVE |
---|
| 838 | %{ tr} %{s1} %{e1} % //; |
---|
| 839 | #tr2 #s2 #e2 #STEPS2 |
---|
| 840 | lapply (not_ex_all_not … NOREACTION); #NR1 |
---|
| 841 | lapply (not_and_to_imply classic … (NR1 〈tr2,〈s2,e2〉〉)); #NR2 |
---|
| 842 | @(classical_doubleneg classic) |
---|
| 843 | @NR2 normalize // |
---|
| 844 | | #REACTIVE |
---|
| 845 | @ec_reacts |
---|
| 846 | [ 2: @reacts |
---|
| 847 | @(show_reactive ge s … EXEC) |
---|
| 848 | #tr #s1 #e1 #STEPS |
---|
| 849 | @constructive_indefinite_description |
---|
| 850 | @(REACTIVE … tr s1 e1 STEPS) |
---|
| 851 | | skip |
---|
| 852 | ] |
---|
| 853 | ] |
---|
| 854 | ] |
---|
[399] | 855 | |
---|
[487] | 856 | | #NOTNONTERMINATING lapply (classical_not_all_ex_not classic … NOTNONTERMINATING); |
---|
| 857 | *; #tr #NNT2 lapply (classical_not_all_ex_not classic … NNT2); |
---|
| 858 | *; #s' #NNT3 lapply (classical_not_all_ex_not classic … NNT3); |
---|
| 859 | *; #e #NNT4 elim (imply_to_and classic … NNT4); |
---|
| 860 | cases e; |
---|
| 861 | [ #tr' #r #m #STEPS #NOSTEP |
---|
| 862 | @(ec_terminates s r m ? (Eapp tr tr')) % |
---|
| 863 | [ @s' |
---|
| 864 | | @STEPS |
---|
| 865 | ] |
---|
| 866 | | #tr' #s'' #e' #STEPS *; #NOSTEP @False_rect_Type0 |
---|
| 867 | @NOSTEP // |
---|
[797] | 868 | | #msg #STEPS #NOSTEP |
---|
[487] | 869 | @(ec_wrong ? s s' tr) % //; |
---|
[399] | 870 | (* The following is stupidly complicated when most of the cases are impossible. |
---|
| 871 | It ought to be simplified. *) |
---|
[487] | 872 | | #o #k #i #e' #STEPS #NOSTEP |
---|
| 873 | cases e' in STEPS NOSTEP; |
---|
| 874 | [ #tr' #r #m #STEPS #NOSTEP |
---|
| 875 | @(ec_terminates s ???) |
---|
| 876 | [ 4: @(annoying_corner_case_terminates … STEPS) ] |
---|
| 877 | | #tr1 #s1 #e1 #STEPS *; #NOSTEP |
---|
| 878 | @False_ind @NOSTEP // |
---|
[797] | 879 | | #msg #STEPS #NOSTEP |
---|
[487] | 880 | lapply (exec_step_interaction ge s'); |
---|
| 881 | cases (several_steps … STEPS EXEC); #_ |
---|
| 882 | whd in ⊢ (% → ?); |
---|
| 883 | >(exec_inf_aux_unfold …) |
---|
| 884 | cases (exec_step ge s'); |
---|
| 885 | [ #o1 #k1 #EXEC' #H whd in EXEC':(?%?) H; |
---|
[1350] | 886 | cases (se_inv … EXEC'); *; #E1 #E2 #H2 destruct (E1 E2); normalize in H2; |
---|
[1516] | 887 | cases (H i); #tr1 *; #s1 *; #K #E >K in H2; |
---|
[487] | 888 | >(exec_inf_aux_unfold …) |
---|
[1516] | 889 | whd in ⊢ (?%? → ?); @is_final_elim [ #r ] |
---|
[487] | 890 | #F #S whd in S:(?%?); cases (se_inv … S); |
---|
[1516] | 891 | | #x cases x; #tr' #s' whd in ⊢ (?%? → ?); |
---|
[891] | 892 | @is_final_elim' [ #r ] #F #S whd in S:(?%?); |
---|
[487] | 893 | cases (se_inv … S); |
---|
[797] | 894 | | #msg #S cases (se_inv … S); |
---|
[487] | 895 | ] |
---|
| 896 | | #o1 #k1 #i1 #e1 #STEPS #NOSTEP |
---|
| 897 | lapply (exec_step_interaction ge s'); |
---|
| 898 | cases (several_steps … STEPS EXEC); #_ |
---|
| 899 | whd in ⊢ (% → ?); |
---|
| 900 | >(exec_inf_aux_unfold …) |
---|
| 901 | cases (exec_step ge s'); |
---|
| 902 | [ #o1 #k1 #EXEC' #H whd in EXEC':(?%?) H; |
---|
[1350] | 903 | cases (se_inv … EXEC'); *; #E1 #E2 #H2 destruct (E1 E2); normalize in H2; |
---|
[1516] | 904 | cases (H i); #tr1 *; #s1 *; #K #E >K in H2; |
---|
[487] | 905 | >(exec_inf_aux_unfold …) |
---|
[1516] | 906 | whd in ⊢ (?%? → ?); @is_final_elim [ #r ] |
---|
[487] | 907 | #F #S whd in S:(?%?); cases (se_inv … S); |
---|
[1516] | 908 | | #x cases x; #tr' #s' whd in ⊢ (?%? → ?); |
---|
[891] | 909 | @is_final_elim' [ #r ] #F #S whd in S:(?%?); |
---|
[487] | 910 | cases (se_inv … S); |
---|
[797] | 911 | | #msg #S cases (se_inv … S); |
---|
[487] | 912 | ] |
---|
| 913 | ] |
---|
| 914 | ] |
---|
| 915 | ] |
---|
| 916 | qed. |
---|
[399] | 917 | |
---|
[487] | 918 | inductive execution_matches_behavior: s_execution → program_behavior → Prop ≝ |
---|
[399] | 919 | | emb_terminates: ∀s,e,tr,r,m. |
---|
| 920 | execution_terminates tr s e r m → |
---|
| 921 | execution_matches_behavior e (Terminates tr r) |
---|
| 922 | | emb_diverges: ∀s,e,tr. |
---|
| 923 | execution_diverges tr s e → |
---|
| 924 | execution_matches_behavior e (Diverges tr) |
---|
| 925 | | emb_reacts: ∀s,e,tr. |
---|
| 926 | execution_reacts tr s e → |
---|
| 927 | execution_matches_behavior e (Reacts tr) |
---|
| 928 | | emb_wrong: ∀e,s,s',tr. |
---|
| 929 | execution_goes_wrong tr s e s' → |
---|
| 930 | execution_matches_behavior e (Goes_wrong tr) |
---|
[797] | 931 | | emb_initially_wrong: ∀msg. |
---|
| 932 | execution_matches_behavior (se_wrong msg) (Goes_wrong E0). |
---|
[399] | 933 | |
---|
[487] | 934 | lemma exec_state_terminates: ∀tr,tr',s,s',e,r,m. |
---|
[399] | 935 | execution_terminates tr s (se_step tr' s' e) r m → s = s'. |
---|
[487] | 936 | #tr #tr' #s #s' #e #r #m #H inversion H; |
---|
[1510] | 937 | [ #s1 #s2 #tr1 #tr2 #r' #e' #m' #H' #E1 #E2 #E3 #E4 #E5 #_ destruct; @refl |
---|
| 938 | | #s1 #s2 #tr1 #tr2 #r' #e' #m' #o #k #i #H' #E1 #E2 #E3 #E4 #E5 #_ destruct; @refl |
---|
[487] | 939 | ] qed. |
---|
[399] | 940 | |
---|
[487] | 941 | lemma exec_state_diverges: ∀tr,tr',s,s',e. |
---|
[399] | 942 | execution_diverges tr s (se_step tr' s' e) → s = s'. |
---|
[487] | 943 | #tr #tr' #s #s' #e #H inversion H; |
---|
[1510] | 944 | #tr1 #s1 #s2 #e1 #e2 #H' #E1 #E2 #E3 #E4 #_ destruct; @refl qed. |
---|
[399] | 945 | |
---|
[487] | 946 | lemma exec_state_reacts: ∀tr,tr',s,s',e. |
---|
[399] | 947 | execution_reacts tr s (se_step tr' s' e) → s = s'. |
---|
[487] | 948 | #tr #tr' #s #s' #e #H inversion H; |
---|
[1510] | 949 | #tr1 #s1 #e1 #H' #E1 #E2 #E3 #_ destruct; @refl qed. |
---|
[399] | 950 | |
---|
[487] | 951 | lemma exec_state_wrong: ∀tr,tr',s,s',s'',e. |
---|
[399] | 952 | execution_goes_wrong tr s (se_step tr' s' e) s'' → s = s'. |
---|
[487] | 953 | #tr #tr' #s #s' #s'' #e #H inversion H; |
---|
[1510] | 954 | #tr1 #s1 #s2 #e1 #msg #H' #E1 #E2 #E3 #E4 #_ destruct; @refl qed. |
---|
[399] | 955 | |
---|
[487] | 956 | lemma behavior_of_execution: ∀s,e. |
---|
[399] | 957 | execution_characterisation s e → |
---|
| 958 | ∃b:program_behavior. execution_matches_behavior e b. |
---|
[487] | 959 | #s0 #e0 #exec |
---|
| 960 | cases exec; |
---|
| 961 | [ #s #r #m #e #tr #TERM |
---|
| 962 | %{ (Terminates tr r)} |
---|
| 963 | @(emb_terminates … TERM) |
---|
| 964 | | #s #e #tr #DIV |
---|
| 965 | %{ (Diverges tr)} |
---|
| 966 | @(emb_diverges … DIV) |
---|
| 967 | | #s #e #tr #REACTS |
---|
| 968 | %{ (Reacts tr)} |
---|
| 969 | @(emb_reacts … REACTS) |
---|
| 970 | | #e #s #s' #tr #WRONG |
---|
| 971 | %{ (Goes_wrong tr)} |
---|
| 972 | @(emb_wrong … WRONG) |
---|
| 973 | ] qed. |
---|
[399] | 974 | |
---|
[487] | 975 | lemma initial_state_not_final: ∀ge,s. |
---|
[399] | 976 | initial_state ge s → |
---|
| 977 | ¬ ∃r.final_state s r. |
---|
[487] | 978 | #ge #s #H cases H; |
---|
| 979 | #b #f #ge #m #E1 #E2 #E3 #E4 % *; #r #H2 |
---|
| 980 | inversion H2; |
---|
| 981 | #r' #m' #E5 #E6 destruct (E5); |
---|
| 982 | qed. |
---|
[399] | 983 | |
---|
[487] | 984 | lemma initial_step: ∀ge,s,e. |
---|
[732] | 985 | exec_inf_aux ?? clight_exec ge (Value ??? 〈E0,s〉) = e → |
---|
[399] | 986 | ¬(∃r.final_state s r) → |
---|
[708] | 987 | ∃e'.e = e_step ??? E0 s e'. |
---|
[487] | 988 | #ge #s #e >(exec_inf_aux_unfold …) |
---|
[1516] | 989 | whd in ⊢ (??%? → ?); @is_final_elim' |
---|
[708] | 990 | [ #r #FINAL #EXEC #NOTFINAL |
---|
[487] | 991 | @False_ind @(absurd ?? NOTFINAL) |
---|
[708] | 992 | %{r} @FINAL |
---|
[487] | 993 | | #F1 #EXEC #F2 whd in EXEC:(??%?); % [ 2: <EXEC @refl ] |
---|
| 994 | qed. |
---|
[399] | 995 | |
---|
[487] | 996 | theorem exec_inf_equivalence: |
---|
[399] | 997 | ∀classic:(∀P:Prop.P ∨ ¬P). |
---|
[487] | 998 | ∀constructive_indefinite_description:(∀A:Type[0]. ∀P:A→Prop. (∃x. P x) → Sig A P). |
---|
[732] | 999 | ∀p,e. single_exec_of (exec_inf ?? clight_fullexec p) e → |
---|
[399] | 1000 | ∃b.execution_matches_behavior e b ∧ exec_program p b. |
---|
[487] | 1001 | #classic #constructive_indefinite_description #p #e |
---|
| 1002 | whd in ⊢ (?%? → ??(λ_.?(?%?)%)); |
---|
[891] | 1003 | lapply (make_initial_state_sound p) |
---|
| 1004 | lapply (the_initial_state p) |
---|
[1516] | 1005 | whd in ⊢ (? → ? → ?(match % with [_ ⇒ ? | _ ⇒ ?])? → ?); |
---|
[891] | 1006 | cases (make_initial_state p) |
---|
[1244] | 1007 | [ #s #INITIAL' #INITIAL whd in INITIAL ⊢ (?%? → ?); |
---|
[891] | 1008 | >exec_inf_aux_unfold |
---|
[1516] | 1009 | whd in ⊢ (?%? → ?); |
---|
[891] | 1010 | @is_final_elim' |
---|
[708] | 1011 | [ #r #F @False_ind |
---|
[1244] | 1012 | @(absurd ?? (initial_state_not_final … INITIAL)) |
---|
[708] | 1013 | %{r} @F |
---|
[487] | 1014 | | #NOTFINAL whd in ⊢ (?%? → ?); cases e; |
---|
[797] | 1015 | [ #tr #r #m #EXEC0 | #tr #s' #e0 #EXEC0 | #msg #EXEC0 | #o #k #i #e #EXEC0 ] |
---|
[487] | 1016 | cases (se_inv … EXEC0); *; #E1 #E2 <E1 <E2 #EXEC' |
---|
| 1017 | lapply (behavior_of_execution ?? |
---|
[1244] | 1018 | (execution_characterisation_complete classic constructive_indefinite_description ? s ? EXEC')); |
---|
[891] | 1019 | *; #b #MATCHES %{b} % [ @MATCHES ] |
---|
[1244] | 1020 | #ge #Ege |
---|
[487] | 1021 | inversion MATCHES; |
---|
[1516] | 1022 | [ #s0 #e1 #tr1 #r #m #TERM #EXEC #BEHAVES <EXEC in TERM; |
---|
[487] | 1023 | #TERM |
---|
| 1024 | lapply (exec_state_terminates … TERM); #E1 |
---|
[1516] | 1025 | >E1 in TERM; #TERM #_ |
---|
[487] | 1026 | @(program_terminates (mk_transrel … step) ?? ge s) |
---|
[1244] | 1027 | [ 2: @INITIAL |
---|
| 1028 | | 3: <Ege @(terminates_sound … TERM EXEC') |
---|
[487] | 1029 | | skip |
---|
| 1030 | | //; |
---|
| 1031 | ] |
---|
[1516] | 1032 | | #s0 #e #tr #DIVERGES #EXEC #E2 <EXEC in DIVERGES; #DIVERGES |
---|
[487] | 1033 | lapply (exec_state_diverges … DIVERGES); |
---|
[1516] | 1034 | #E1 >E1 in DIVERGES; #DIVERGES #_ |
---|
[487] | 1035 | inversion DIVERGES; #tr' #s1 #s2 #e1 #e2 #INITSTEPS #DIVERGING #E4 #E5 #E6 |
---|
[1516] | 1036 | <E4 in INITSTEPS ⊢ %; <E5 in E6 ⊢ %; #E6 #INITSTEPS |
---|
[487] | 1037 | cut (e0 = e1); [ destruct (E6) skip (MATCHES EXEC0 EXEC'); // ] |
---|
[1516] | 1038 | #E7 <E7 in INITSTEPS; #INITSTEPS |
---|
[1510] | 1039 | cases (several_steps … INITSTEPS EXEC'); #INITSTAR #EXECDIV #_ |
---|
[1244] | 1040 | @(program_diverges (mk_transrel … step) ?? ge s … INITIAL) |
---|
| 1041 | [ 2: <Ege @INITSTAR |
---|
| 1042 | | 3: <Ege @(silent_sound … DIVERGING EXECDIV) |
---|
| 1043 | ] |
---|
[1516] | 1044 | | #s0 #e #tr #REACTS #EXEC #E2 <EXEC in REACTS; #REACTS |
---|
[487] | 1045 | lapply (exec_state_reacts … REACTS); |
---|
[1516] | 1046 | #E1 >E1 in REACTS; #REACTS #_ |
---|
[487] | 1047 | inversion REACTS; #tr' #s' #e'' #REACTING #E4 #E5 |
---|
[1516] | 1048 | <E4 in REACTING ⊢ %; <E5 #REACTING #E6 |
---|
[487] | 1049 | cut (e0 = e''); [ destruct (E6) skip (MATCHES EXEC0 EXEC'); // ] |
---|
[1516] | 1050 | #E7 <E7 in REACTING; #REACTING #_ |
---|
[1244] | 1051 | @(program_reacts (mk_transrel … step) ?? ge s … INITIAL) |
---|
| 1052 | <Ege @(reacts_sound … REACTING EXEC') |
---|
[1516] | 1053 | | #e #s1 #s2 #tr #WRONG #EXEC #E2 <EXEC in WRONG; #WRONG |
---|
[487] | 1054 | lapply (exec_state_wrong … WRONG); |
---|
[1516] | 1055 | #E1 >E1 in WRONG; #WRONG #_ |
---|
[797] | 1056 | inversion WRONG; #tr' #s1' #s2' #e'' #msg #GOESWRONG #E4 #E5 #E6 #E7 |
---|
[1516] | 1057 | <E4 in GOESWRONG ⊢ %; <E5 <E7 #GOESWRONG |
---|
[487] | 1058 | cut (e0 = e''); [ destruct (E6) skip (INITIAL Ege MATCHES EXEC0 EXEC'); // ] |
---|
[1516] | 1059 | #E8 <E8 in GOESWRONG; #GOESWRONG |
---|
[487] | 1060 | elim (wrong_sound … WRONG EXEC' NOTFINAL); *; #STAR #STOP #FINAL |
---|
[1510] | 1061 | <Ege #_ |
---|
[1244] | 1062 | @(program_goes_wrong (mk_transrel … step) ?? ? s … INITIAL STAR STOP) |
---|
[487] | 1063 | #r % #F @(absurd ?? FINAL) %{r} @F |
---|
[797] | 1064 | | #msg #E destruct (E); |
---|
[487] | 1065 | ] |
---|
| 1066 | ] |
---|
[797] | 1067 | | #msg whd in ⊢ ((∀_.? → %) → ?); |
---|
[487] | 1068 | #NOINIT #_ #EXEC |
---|
| 1069 | %{ (Goes_wrong E0)} % |
---|
| 1070 | [ whd in EXEC:(?%?); |
---|
| 1071 | cases e in EXEC; |
---|
[797] | 1072 | [ #tr #r #m #EXEC0 | #tr #s' #e0 #EXEC0 | #msg #EXEC0 | #o #k #i #e #EXEC0 ] |
---|
[487] | 1073 | cases (se_inv … EXEC0); |
---|
| 1074 | @emb_initially_wrong |
---|
| 1075 | | #ge #Ege |
---|
| 1076 | @program_goes_initially_wrong |
---|
| 1077 | #s % #INIT cases (NOINIT s INIT); #ge' #H @H |
---|
| 1078 | ] |
---|
| 1079 | ] qed. |
---|
[399] | 1080 | |
---|