[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)) |
---|
| 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 |
---|
[708] | 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 |
---|
[702] | 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) ;*) |
---|
| 120 | cases (se_step_eq … E) * #E1 #E2 #E3 >E1 >E2 >E3 |
---|
[487] | 121 | >(exec_e_step_inv … H2) |
---|
| 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 |
---|
[708] | 135 | | #o #k #i #se #H1 #H2 #E 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 |
---|
| 143 | | #tr' #s' #e' #se' #H2 #H3 #E2 destruct (E2); |
---|
[708] | 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 |
---|
[487] | 166 | | #o #k #i #se #H1 #H2 #E destruct (E); |
---|
| 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; |
---|
| 174 | [ #tr #r #m #E1 #E2 lapply (STEP i); destruct; |
---|
| 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:(∀_. ? → ? → ?%); |
---|
| 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; |
---|
| 286 | [ #tr' #r' #m' #EXEC' #E destruct (E); |
---|
| 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 | ] |
---|
| 296 | inversion FINAL; #r''' #m' #E1 #E2 #H destruct (E1 E2); |
---|
| 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; |
---|
| 323 | [ #s #s' #tr #tr' #r #e #m #ESTEPS #E1 #E2 #E3 #E4 #E5 #EXEC |
---|
| 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 | ] |
---|
| 331 | | #s #s' #tr #tr' #r #e #m #o #k #i #ESTEPS #E1 #E2 #E3 #E4 #E5 #EXEC |
---|
| 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; |
---|
| 347 | #tr0 #tr' #s0 #s' #e0 #e' #EREACTS #ESTEPS #REACTED #E1 #E2 #E3 destruct (E2 E3); |
---|
| 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) |
---|
| 373 | | >(exec_inf_aux_unfold …) |
---|
| 374 | cases (exec_step ge s); |
---|
[1344] | 375 | [ #o #k #msg' #EXEC whd in EXEC:(??%??); destruct |
---|
| 376 | | #x cases x; #tr #s' #msg' whd in ⊢ (??%?? → ?) @is_final_elim' |
---|
| 377 | [ #r ] #F #EXEC whd in EXEC:(??%??); destruct |
---|
| 378 | | #msg1 #msg2 #EXEC #E whd in EXEC:(??%??); destruct @refl |
---|
[487] | 379 | ] |
---|
| 380 | | #o #k #i #e #H #EXEC #E destruct |
---|
| 381 | ] qed. |
---|
[399] | 382 | |
---|
[487] | 383 | lemma exec_from_step_notfinal: ∀ge,s,tr,s',e. |
---|
[399] | 384 | exec_from ge s (se_step tr s' e) → |
---|
| 385 | ¬(∃r. final_state s' r). |
---|
[487] | 386 | #ge #s #tr #s' #e #H whd in H; inversion H; |
---|
| 387 | [ #tr' #r #m #EXEC #E destruct |
---|
| 388 | | #tr' #s'' #e' #e'' #H #EXEC #E destruct (E); |
---|
| 389 | >(exec_inf_aux_unfold …) in EXEC; |
---|
| 390 | cases (exec_step ge s); |
---|
[1344] | 391 | [ #o #k #EXEC whd in EXEC:(??%??); destruct |
---|
| 392 | | #x cases x; #tr1 #s1 whd in ⊢ (??%?? → ?) @is_final_elim' |
---|
| 393 | [ #r ] #F #E whd in E:(??%??); destruct @F |
---|
| 394 | | #msg #E whd in E:(??%??); destruct |
---|
[487] | 395 | ] |
---|
[797] | 396 | | #msg #EXEC #E destruct |
---|
[487] | 397 | | #o #k #i #e' #H #EXEC #E destruct |
---|
| 398 | ] qed. |
---|
[399] | 399 | |
---|
[487] | 400 | lemma exec_from_interact_step_notfinal: ∀ge,s,o,k,i,tr,s',e. |
---|
[399] | 401 | exec_from ge s (se_interact o k i (se_step tr s' e)) → |
---|
| 402 | ¬(∃r. final_state s' r). |
---|
[487] | 403 | #ge #s #o #k #i #tr #s' #e #H |
---|
| 404 | % *; #r #F cases F in H; #r' #m #H |
---|
| 405 | inversion H; |
---|
| 406 | [ #tr' #r #m #EXEC #E destruct |
---|
| 407 | | #tr' #s'' #e' #e'' #H #EXEC #E destruct (E); |
---|
[797] | 408 | | #msg #EXEC #E destruct |
---|
[487] | 409 | | #o' #k' #i' #e' #H #EXEC #E destruct; |
---|
| 410 | >(exec_inf_aux_unfold …) in EXEC; |
---|
| 411 | cases (exec_step ge s); |
---|
[1344] | 412 | [ #o1 #k1 #EXEC1 whd in EXEC1:(??%??); destruct (EXEC1); |
---|
[487] | 413 | inversion H; |
---|
| 414 | [ #tr1 #r1 #m1 #EXECK #E destruct (E); |
---|
| 415 | | #tr1 #s1 #e1 #e2 #H1 #EXECK #E destruct (E); |
---|
| 416 | >(exec_inf_aux_unfold …) in EXECK; |
---|
| 417 | cases (k1 i'); |
---|
[1344] | 418 | [ #o2 #k2 #EXECK whd in EXECK:(??%??); destruct |
---|
| 419 | | #x cases x; #tr2 #s2 whd in ⊢ (??%?? → ?); |
---|
[1350] | 420 | lapply (is_final_elim s2) #IFE whd in IFE:(∀_. ? → ? → ?%); |
---|
| 421 | change in match (is_final ?????) with (is_final s2) |
---|
[891] | 422 | @IFE [ #r ] #F #EXECK |
---|
[1344] | 423 | whd in EXECK:(??%??); destruct; |
---|
[487] | 424 | @(absurd ?? F) |
---|
| 425 | %{ r'} //; |
---|
[1344] | 426 | | #msg #E whd in E:(??%??); destruct |
---|
[487] | 427 | ] |
---|
[1344] | 428 | | #msg #EXECK #E whd in E:(??%??); destruct |
---|
[487] | 429 | | #o2 #k2 #i2 #e2 #H2 #EXECK #E destruct |
---|
| 430 | ] |
---|
[1344] | 431 | | #x cases x; #tr1 #s1 whd in ⊢ (??%?? → ?); |
---|
| 432 | @is_final_elim' [ #r ] #F #E whd in E:(??%??); destruct; |
---|
| 433 | | #msg #E whd in E:(??%??); destruct |
---|
[487] | 434 | ] |
---|
| 435 | ] qed. |
---|
[399] | 436 | |
---|
[487] | 437 | lemma wrong_sound: ∀ge,tr,s,s',e. |
---|
[399] | 438 | execution_goes_wrong tr s (se_step E0 s e) s' → |
---|
| 439 | exec_from ge s e → |
---|
| 440 | (¬∃r. final_state s r) → |
---|
| 441 | star (mk_transrel … step) ge s tr s' ∧ |
---|
| 442 | nostep (mk_transrel … step) ge s' ∧ |
---|
| 443 | (¬∃r. final_state s' r). |
---|
[487] | 444 | #ge #tr0 #s0 #s0' #e0 #WRONG inversion WRONG; |
---|
[797] | 445 | #tr #s #s' #e #msg #ESTEPS #E1 #E2 #E3 #E4 #EXEC #NOTFINAL destruct (E1 E2 E3 E4); |
---|
[487] | 446 | cases (several_steps … ESTEPS EXEC); |
---|
| 447 | #STAR #EXEC' % |
---|
| 448 | [ % [ @STAR |
---|
| 449 | | #badtr #bads % #badSTEP |
---|
| 450 | lapply (step_complete … badSTEP); |
---|
| 451 | >(exec_from_wrong … EXEC') |
---|
[399] | 452 | //; |
---|
[487] | 453 | ] |
---|
| 454 | | % |
---|
| 455 | elim ESTEPS in NOTFINAL EXEC ⊢ %; |
---|
| 456 | [ #s1 #e1 #NF #EX #F @(absurd ? F NF) |
---|
| 457 | | #e1 #e2 #tr1 #tr2 #s1 #s2 #s3 #ESTEPS1 #IH #NF #EXEC |
---|
| 458 | cases (exec_from_step … EXEC); #EXEC3 #EXEC1 |
---|
| 459 | @(IH … EXEC1) |
---|
| 460 | @(exec_from_step_notfinal … EXEC) |
---|
| 461 | | #e1 #e2 #o #k #i #s1 #s2 #s3 #tr1 #tr2 #ESTEPS1 #IH #NF #EXEC |
---|
| 462 | @IH |
---|
| 463 | [ @(exec_from_interact_step_notfinal … EXEC) |
---|
[708] | 464 | | cases (exec_from_interact … EXEC) #STEP #EF1 @EF1 |
---|
[487] | 465 | ] |
---|
| 466 | ] |
---|
| 467 | ] qed. |
---|
[399] | 468 | |
---|
[487] | 469 | inductive execution_characterisation : state → s_execution → Prop ≝ |
---|
[399] | 470 | | ec_terminates: ∀s,r,m,e,tr. |
---|
| 471 | execution_terminates tr s e r m → |
---|
| 472 | execution_characterisation s e |
---|
| 473 | | ec_diverges: ∀s,e,tr. |
---|
| 474 | execution_diverges tr s e → |
---|
| 475 | execution_characterisation s e |
---|
| 476 | | ec_reacts: ∀s,e,tr. |
---|
| 477 | execution_reacts tr s e → |
---|
| 478 | execution_characterisation s e |
---|
| 479 | | ec_wrong: ∀e,s,s',tr. |
---|
| 480 | execution_goes_wrong tr s e s' → |
---|
| 481 | execution_characterisation s e. |
---|
| 482 | |
---|
| 483 | (* bit of a hack to avoid inability to reduce term in match *) |
---|
[487] | 484 | 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] | 485 | λA,P,e. match e return λ_.Prop with [ Interact o k ⇒ P o k | _ ⇒ True ]. |
---|
| 486 | |
---|
[487] | 487 | lemma err_does_not_interact: ∀A,B,P,e1,e2. |
---|
[399] | 488 | (∀x:B.interact_prop A P (e2 x)) → |
---|
| 489 | interact_prop A P (bindIO ?? B A (err_to_io ??? e1) e2). |
---|
[487] | 490 | #A #B #P #e1 #e2 #H |
---|
| 491 | cases e1; //; qed. |
---|
[399] | 492 | |
---|
[487] | 493 | lemma err2_does_not_interact: ∀A,B,C,P,e1,e2. |
---|
[399] | 494 | (∀x,y.interact_prop A P (e2 x y)) → |
---|
| 495 | interact_prop A P (bindIO2 ?? B C A (err_to_io ??? e1) e2). |
---|
[487] | 496 | #A #B #C #P #e1 #e2 #H |
---|
| 497 | cases e1; [ #z cases z; ] //; qed. |
---|
[399] | 498 | |
---|
[487] | 499 | lemma err_sig_does_not_interact: ∀A,B,P.∀Q:B→Prop.∀e1,e2. |
---|
[399] | 500 | (∀x.interact_prop A P (e2 x)) → |
---|
[487] | 501 | interact_prop A P (bindIO ?? (Sig B Q) A (err_to_io_sig ??? Q e1) e2). |
---|
| 502 | #A #B #P #Q #e1 #e2 #H |
---|
| 503 | cases e1; //; qed. |
---|
[399] | 504 | |
---|
[797] | 505 | lemma opt_does_not_interact: ∀A,B,P,e1,e2,msg. |
---|
[399] | 506 | (∀x:B.interact_prop A P (e2 x)) → |
---|
[797] | 507 | interact_prop A P (bindIO ?? B A (opt_to_io ??? msg e1) e2). |
---|
| 508 | #A #B #P #e1 #e2 #msg #H |
---|
[487] | 509 | cases e1; //; qed. |
---|
[399] | 510 | |
---|
[487] | 511 | lemma exec_step_interaction: |
---|
[399] | 512 | ∀ge,s. interact_prop ? (λo,k. ∀i.∃tr.∃s'. k i = Value ??? 〈tr,s'〉 ∧ tr ≠ E0) (exec_step ge s). |
---|
[487] | 513 | #ge #s cases s; |
---|
| 514 | [ #f #st #kk #e #m cases st; |
---|
| 515 | [ 11,14: #a | 2,4,6,7,12,13,15: #a #b | 3,5: #a #b #c | 8: #a #b #c #d ] |
---|
| 516 | [ 4,6,8,9: @I ] |
---|
| 517 | whd in ⊢ (???%); |
---|
| 518 | [ cases a; [ cases (fn_return f); //; | #e whd nodelta in ⊢ (???%); |
---|
| 519 | cases (type_eq_dec (fn_return f) Tvoid); #x //; @err2_does_not_interact // ] |
---|
| 520 | | cases (find_label a (fn_body f) (call_cont kk)); [ @I | #z cases z #x #y @I ] |
---|
| 521 | | @err2_does_not_interact #x1 #x2 @err2_does_not_interact #x3 #x4 @opt_does_not_interact #x5 @I |
---|
| 522 | | 4,7: @err2_does_not_interact #x1 #x2 @err_does_not_interact #x3 @I |
---|
| 523 | | @err2_does_not_interact #x1 #x2 cases x1; //; |
---|
| 524 | | @err2_does_not_interact #x1 #x2 @err2_does_not_interact #x3 #x4 @opt_does_not_interact #x5 @err_does_not_interact #x6 cases a; |
---|
| 525 | [ @I | #x7 @err2_does_not_interact #x8 #x9 @I ] |
---|
| 526 | | cases (is_Sskip a); #H [ @err2_does_not_interact #x1 #x2 @err_does_not_interact #x3 @I |
---|
| 527 | | @I ] |
---|
| 528 | | cases kk; [ 1,8: cases (fn_return f); //; | 2,3,5,6,7: //; |
---|
| 529 | | #z1 #z2 #z3 @err2_does_not_interact #x1 #x2 @err_does_not_interact #x3 cases x3; @I ] |
---|
| 530 | | cases kk; //; |
---|
| 531 | | cases kk; [ 4: #z1 #z2 #z3 @err2_does_not_interact #x1 #x2 @err_does_not_interact #x3 cases x3; @I |
---|
| 532 | | *: // ] |
---|
| 533 | ] |
---|
| 534 | | #f #args #kk #m cases f; |
---|
| 535 | [ #f' whd in ⊢ (???%); cases (exec_alloc_variables empty_env m (fn_params f'@fn_vars f')) |
---|
| 536 | #x1 #x2 whd in ⊢ (???%) @err_does_not_interact // |
---|
[399] | 537 | (* This is the only case that actually matters! *) |
---|
[487] | 538 | | #fn #argtys #rty whd in ⊢ (???%); |
---|
| 539 | @err_does_not_interact #x1 |
---|
| 540 | whd; #i % [ 2: % [ 2: % [ % whd in ⊢ (??%?); @refl |
---|
| 541 | | % #E whd in E:(??%%); destruct (E); ] ] ] |
---|
| 542 | ] |
---|
| 543 | | #v #kk #m whd in ⊢ (???%); cases kk; |
---|
| 544 | [ 8: #x1 #x2 #x3 #x4 cases x1; |
---|
| 545 | [ whd in ⊢ (???%); cases v; // | #x5 whd in ⊢ (???%); cases x5; |
---|
| 546 | #x6 #x7 @opt_does_not_interact // ] |
---|
| 547 | | *: // ] |
---|
| 548 | ] qed. |
---|
[399] | 549 | |
---|
| 550 | |
---|
| 551 | (* Some classical logic (roughly like a fragment of Coq's library) *) |
---|
[487] | 552 | lemma classical_doubleneg: |
---|
[399] | 553 | ∀classic:(∀P:Prop.P ∨ ¬P). |
---|
| 554 | ∀P:Prop. ¬ (¬ P) → P. |
---|
[487] | 555 | #classic #P *; #H |
---|
| 556 | cases (classic P); |
---|
| 557 | [ // | #H' @False_ind /2/; ] |
---|
| 558 | qed. |
---|
[399] | 559 | |
---|
[487] | 560 | lemma classical_not_all_not_ex: |
---|
[399] | 561 | ∀classic:(∀P:Prop.P ∨ ¬P). |
---|
[487] | 562 | ∀A:Type[0].∀P:A → Prop. ¬ (∀x. ¬ P x) → ∃x. P x. |
---|
| 563 | #classic #A #P *; #H |
---|
| 564 | @(classical_doubleneg classic) % *; #H' |
---|
| 565 | @H #x % #H'' @H' %{x} @H'' |
---|
| 566 | qed. |
---|
[399] | 567 | |
---|
[487] | 568 | lemma classical_not_all_ex_not: |
---|
[399] | 569 | ∀classic:(∀P:Prop.P ∨ ¬P). |
---|
[487] | 570 | ∀A:Type[0].∀P:A → Prop. ¬ (∀x. P x) → ∃x. ¬ P x. |
---|
| 571 | #classic #A #P *; #H |
---|
| 572 | @(classical_not_all_not_ex classic A (λx.¬ P x)) |
---|
| 573 | % #H' @H #x @(classical_doubleneg classic) |
---|
| 574 | @H' |
---|
| 575 | qed. |
---|
[399] | 576 | |
---|
[487] | 577 | lemma not_ex_all_not: |
---|
| 578 | ∀A:Type[0].∀P:A → Prop. ¬ (∃x. P x) → ∀x. ¬ P x. |
---|
| 579 | #A #P *; #H #x % #H' |
---|
| 580 | @H %{ x} @H' |
---|
| 581 | qed. |
---|
[399] | 582 | |
---|
[487] | 583 | lemma not_imply_elim: |
---|
[399] | 584 | ∀classic:(∀P:Prop.P ∨ ¬P). |
---|
| 585 | ∀P,Q:Prop. ¬ (P → Q) → P. |
---|
[487] | 586 | #classic #P #Q *; #H |
---|
| 587 | @(classical_doubleneg classic) % *; #H' |
---|
| 588 | @H #H'' @False_ind @H' @H'' |
---|
| 589 | qed. |
---|
[399] | 590 | |
---|
[487] | 591 | lemma not_imply_elim2: |
---|
[399] | 592 | ∀P,Q:Prop. ¬ (P → Q) → ¬ Q. |
---|
[487] | 593 | #P #Q *; #H % #H' |
---|
| 594 | @H #_ @H' |
---|
| 595 | qed. |
---|
[399] | 596 | |
---|
[487] | 597 | lemma imply_to_and: |
---|
[399] | 598 | ∀classic:(∀P:Prop.P ∨ ¬P). |
---|
| 599 | ∀P,Q:Prop. ¬ (P → Q) → P ∧ ¬Q. |
---|
[487] | 600 | #classic #P #Q #H % |
---|
| 601 | [ @(not_imply_elim classic P Q H) |
---|
| 602 | | @(not_imply_elim2 P Q H) |
---|
| 603 | ] qed. |
---|
[399] | 604 | |
---|
[487] | 605 | lemma not_and_to_imply: |
---|
[399] | 606 | ∀classic:(∀P:Prop.P ∨ ¬P). |
---|
| 607 | ∀P,Q:Prop. ¬ (P ∧ Q) → P → ¬Q. |
---|
[487] | 608 | #classic #P #Q *; #H #H' |
---|
| 609 | % #H'' @H % //; |
---|
| 610 | qed. |
---|
[399] | 611 | |
---|
[487] | 612 | inductive execution_not_over : s_execution → Prop ≝ |
---|
[399] | 613 | | eno_step: ∀tr,s,e. execution_not_over (se_step tr s e) |
---|
| 614 | | eno_interact: ∀o,k,tr,s,e,i. execution_not_over (se_interact o k i (se_step tr s e)). |
---|
| 615 | |
---|
[487] | 616 | lemma eno_stop: ∀tr,r,m. execution_not_over (se_stop tr r m) → False. |
---|
| 617 | #tr0 #r0 #m0 #H inversion H; |
---|
| 618 | [ #tr #s #e #E destruct |
---|
| 619 | | #o #k #tr #s #e #i #E destruct |
---|
| 620 | ] qed. |
---|
[399] | 621 | |
---|
[797] | 622 | lemma eno_wrong: ∀msg. execution_not_over (se_wrong msg) → False. |
---|
| 623 | #msg #H inversion H; |
---|
[487] | 624 | [ #tr #s #e #E destruct |
---|
| 625 | | #o #k #tr #s #e #i #E destruct |
---|
| 626 | ] qed. |
---|
[399] | 627 | |
---|
[487] | 628 | let corec show_divergence s e |
---|
[399] | 629 | (NONTERMINATING:∀tr1,s1,e1. execution_isteps tr1 s e s1 e1 → |
---|
| 630 | execution_not_over e1) |
---|
| 631 | (UNREACTIVE:∀tr2,s2,e2. execution_isteps tr2 s e s2 e2 → tr2 = E0) |
---|
[487] | 632 | (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] | 633 | : execution_diverging e ≝ ?. |
---|
[487] | 634 | lapply (NONTERMINATING E0 s e ?); //; |
---|
| 635 | cases e in UNREACTIVE NONTERMINATING CONTINUES ⊢ %; |
---|
| 636 | [ #tr #i #m #_ #_ #_ #ENO elim (eno_stop … ENO); |
---|
| 637 | | #tr #s' #e' #UNREACTIVE lapply (UNREACTIVE tr s' e' ?); |
---|
| 638 | [ <(E0_right tr) in ⊢ (?%????) |
---|
| 639 | @isteps_one @isteps_none |
---|
| 640 | | #TR @(match sym_eq ??? TR with [ refl ⇒ ? ]) (* >TR in UNREACTIVE ⊢ % *) |
---|
| 641 | #NONTERMINATING #CONTINUES #_ % |
---|
| 642 | @(show_divergence s') |
---|
| 643 | [ #tr1 #s1 #e1 #S @(NONTERMINATING tr1 s1 e1) |
---|
| 644 | change in ⊢ (?%????) with (Eapp E0 tr1); @isteps_one |
---|
| 645 | @S |
---|
| 646 | | #tr2 #s2 #e2 #S >TR in UNREACTIVE #UNREACTIVE @(UNREACTIVE tr2 s2 e2) |
---|
| 647 | change in ⊢ (?%????) with (Eapp E0 tr2); |
---|
| 648 | @isteps_one @S |
---|
| 649 | | #tr2 #s2 #o #k #i #e2 #S @(CONTINUES tr2 s2 o k i) |
---|
| 650 | change in ⊢ (?%????) with (Eapp E0 tr2); |
---|
| 651 | @(isteps_one … S) |
---|
| 652 | ] |
---|
| 653 | ] |
---|
[797] | 654 | | #msg #_ #_ #_ #ENO elim (eno_wrong … ENO); |
---|
[487] | 655 | | #o #k #i #e' #UNREACTIVE #NONTERMINATING #CONTINUES #_ |
---|
| 656 | lapply (CONTINUES E0 s o k i e' (isteps_none …)); |
---|
| 657 | *; #tr' *; #s' *; #e' *; #EXEC #NOTSILENT |
---|
| 658 | @False_ind @(absurd ?? NOTSILENT) |
---|
| 659 | @(UNREACTIVE … s' e') |
---|
| 660 | <(E0_right tr') in ⊢ (?%????) |
---|
| 661 | >EXEC |
---|
| 662 | @isteps_interact //; |
---|
| 663 | ] qed. |
---|
[399] | 664 | |
---|
[487] | 665 | lemma se_inv: ∀e1,e2. |
---|
[399] | 666 | single_exec_of e1 e2 → |
---|
| 667 | match e1 with |
---|
[1216] | 668 | [ e_stop tr r s ⇒ match e2 with [ se_stop tr' r' m' ⇒ tr = tr' ∧ r = r' ∧ mem_of_state s = m' | _ ⇒ False ] |
---|
[399] | 669 | | e_step tr s e1' ⇒ match e2 with [ se_step tr' s' e2' ⇒ tr = tr' ∧ s = s' ∧ single_exec_of e1' e2' | _ ⇒ False ] |
---|
[797] | 670 | | e_wrong _ ⇒ match e2 with [ se_wrong _ ⇒ True | _ ⇒ False ] |
---|
[399] | 671 | | e_interact o k ⇒ match e2 with [ se_interact o' k' i e ⇒ o' = o ∧ k' ≃ k ∧ single_exec_of (k' i) e | _ ⇒ False ] |
---|
| 672 | ]. |
---|
[487] | 673 | #e01 #e02 #H |
---|
| 674 | cases H; |
---|
[1216] | 675 | [ #tr #r #s whd; % [ % ] // |
---|
[487] | 676 | | #tr #s #e1' #e2' #H' whd; % [ % ] // |
---|
[797] | 677 | | #msg whd; // |
---|
[487] | 678 | | #o #k #i #e #H' whd; % [ % ] // |
---|
| 679 | ] qed. |
---|
[399] | 680 | |
---|
[487] | 681 | lemma interaction_is_not_silent: ∀ge,o,k,i,tr,s,s',e. |
---|
[399] | 682 | exec_from ge s (se_interact o k i (se_step tr s' e)) → |
---|
| 683 | tr ≠ E0. |
---|
[487] | 684 | #ge #o #k #i #tr #s #s' #e whd in ⊢ (% → ?); >(exec_inf_aux_unfold …) |
---|
| 685 | lapply (exec_step_interaction ge s); |
---|
| 686 | cases (exec_step ge s); |
---|
| 687 | [ #o' #k' ; whd in ⊢ (% → ?%? → ?); #H #K cases (se_inv … K); |
---|
| 688 | *; #E1 #E2 #H1 destruct (E1); |
---|
| 689 | lapply (H i); *; #tr' *; #s'' *; #K' #TR |
---|
| 690 | >E2 in H1 #H1 whd in H1:(?%?); >K' in H1 |
---|
| 691 | >(exec_inf_aux_unfold …) whd in ⊢ (?%? → ?); |
---|
[1350] | 692 | change in match (is_final ?????) with (is_final s'') |
---|
[708] | 693 | @is_final_elim |
---|
| 694 | [ #r #F whd in ⊢ (?%? → ?); #S |
---|
[487] | 695 | @False_ind @(absurd ? S) cases (se_inv … S) |
---|
| 696 | | #NF #S whd in S:(?%?); cases (se_inv … S); |
---|
| 697 | *; #E1 #E2 #S' <E1 @TR |
---|
| 698 | ] |
---|
[708] | 699 | | #x cases x; #tr' #s'' #H whd in ⊢ (?%? → ?) |
---|
[891] | 700 | @is_final_elim' [ #r ] #F #E whd in E:(?%?); |
---|
[487] | 701 | inversion E; |
---|
| 702 | [ 1,5: #tr1 #e1 #m1 #E1 #E2 destruct |
---|
| 703 | | 2,6: #tr #s1 #e1 #e2 #H #E1 #E2 destruct |
---|
[797] | 704 | | 3,7: #msg #E destruct |
---|
[487] | 705 | | 4,8: #o1 #k1 #i1 #e1 #H1 #E1 #E2 destruct |
---|
| 706 | ] |
---|
[797] | 707 | | #msg #_ #E whd in E:(?%?); |
---|
[487] | 708 | inversion E; |
---|
| 709 | [ 1,5: #tr1 #e1 #m1 #E1 #E2 destruct |
---|
| 710 | | 2,6: #tr #s1 #e1 #e2 #H #E1 #E2 destruct |
---|
[797] | 711 | | 3,7: #msg #E1 #E2 destruct |
---|
[487] | 712 | | 4,8: #o1 #k1 #i1 #e1 #H1 #E1 #E2 destruct |
---|
| 713 | ] |
---|
| 714 | ] qed. |
---|
[399] | 715 | |
---|
[487] | 716 | let corec reactive_traceinf' ge s e |
---|
[399] | 717 | (EXEC:exec_from ge s e) |
---|
| 718 | (REACTIVE: ∀tr,s1,e1. |
---|
| 719 | execution_isteps tr s e s1 e1 → |
---|
[487] | 720 | (Sig ? (λx.execution_isteps (\fst x) s1 e1 (\fst (\snd x)) (\snd (\snd x)) ∧ (\fst x) ≠ E0))) |
---|
[399] | 721 | : traceinf' ≝ ?. |
---|
[487] | 722 | lapply (REACTIVE E0 s e (isteps_none …)); |
---|
| 723 | *; #x cases x; #tr #y cases y; #s' #e' *; #STEPS #H |
---|
| 724 | %{ tr ? H} |
---|
| 725 | @(reactive_traceinf' ge s' e' ?) |
---|
| 726 | [ cases (several_steps … STEPS EXEC); #_ #H' @H' |
---|
| 727 | | #tr1 #s1 #e1 #STEPS1 |
---|
| 728 | @REACTIVE |
---|
| 729 | [ 2: |
---|
| 730 | @(isteps_trans … STEPS STEPS1) |
---|
| 731 | | skip |
---|
| 732 | ] |
---|
| 733 | ] |
---|
| 734 | qed. |
---|
[399] | 735 | |
---|
| 736 | (* A slightly different version of the above, to work around a problem with the |
---|
| 737 | next result. *) |
---|
[487] | 738 | let corec reactive_traceinf'' ge s e |
---|
[399] | 739 | (EXEC:exec_from ge s e) |
---|
[487] | 740 | (REACTIVE0: Sig ? (λx.execution_isteps (\fst x) s e (\fst (\snd x)) (\snd (\snd x)) ∧ (\fst x) ≠ E0)) |
---|
[399] | 741 | (REACTIVE: ∀tr,s1,e1. |
---|
| 742 | execution_isteps tr s e s1 e1 → |
---|
[487] | 743 | (Sig ? (λx.execution_isteps (\fst x) s1 e1 (\fst (\snd x)) (\snd (\snd x)) ∧ (\fst x) ≠ E0))) |
---|
[399] | 744 | : traceinf' ≝ ?. |
---|
[487] | 745 | cases REACTIVE0; #x cases x; #tr #y cases y; #s' #e' *; #STEPS #H |
---|
| 746 | %{ tr ? H} |
---|
| 747 | @(reactive_traceinf'' ge s' e' ?) |
---|
| 748 | [ cases (several_steps … STEPS EXEC); #_ #H' @H' |
---|
| 749 | | @(REACTIVE … STEPS) |
---|
| 750 | | #tr1 #s1 #e1 #STEPS1 |
---|
| 751 | @REACTIVE |
---|
| 752 | [ 2: |
---|
| 753 | @(isteps_trans … STEPS STEPS1) |
---|
| 754 | | skip |
---|
| 755 | ] |
---|
| 756 | ] qed. |
---|
[399] | 757 | |
---|
| 758 | (* We want to prove |
---|
| 759 | |
---|
[487] | 760 | lemma show_reactive : ∀ge,s. |
---|
[399] | 761 | ∀REACTIVE:∀tr,s1,e1. |
---|
| 762 | execution_isteps tr s (exec_inf_aux ge (exec_step ge s)) s1 e1 → |
---|
| 763 | Σx.execution_isteps (\fst x) s1 e1 (\fst (\snd x)) (\snd (\snd x)) ∧ (\fst x) ≠ E0. |
---|
| 764 | execution_reacting (traceinf_of_traceinf' (reactive_traceinf' ge s REACTIVE)) s (exec_inf_aux ge (exec_step ge s)). |
---|
| 765 | |
---|
| 766 | but the current matita won't unfold reactive_traceinf' so that we can do case |
---|
| 767 | analysis on (REACTIVE …). Instead we take an "applied" version of REACTIVE that |
---|
| 768 | we can do case analysis on, then get it into the desired form afterwards. |
---|
| 769 | *) |
---|
[487] | 770 | let corec show_reactive' ge s e |
---|
[399] | 771 | (EXEC:exec_from ge s e) |
---|
[487] | 772 | (REACTIVE0: Sig ? (λx.execution_isteps (\fst x) s e (\fst (\snd x)) (\snd (\snd x)) ∧ (\fst x) ≠ E0)) |
---|
[399] | 773 | (REACTIVE: ∀tr1,s1,e1. |
---|
| 774 | execution_isteps tr1 s e s1 e1 → |
---|
[487] | 775 | (Sig ? (λx.execution_isteps (\fst x) s1 e1 (\fst (\snd x)) (\snd (\snd x)) ∧ (\fst x) ≠ E0))) |
---|
[399] | 776 | : execution_reacting (traceinf_of_traceinf' (reactive_traceinf'' ge s e EXEC REACTIVE0 REACTIVE)) s e ≝ ?. |
---|
[487] | 777 | (*>(unroll_traceinf' (reactive_traceinf'' …)) *) |
---|
| 778 | @(match sym_eq ??? (unroll_traceinf' (reactive_traceinf'' …)) with [ refl ⇒ ? ]) |
---|
| 779 | cases REACTIVE0; |
---|
| 780 | #x cases x; #tr1 #y cases y; #s1 #e1 #z cases z; #STEPS #NOTSILENT |
---|
| 781 | whd in ⊢ (?(?%)??); |
---|
| 782 | (*>(traceinf_traceinfp_app …) *) |
---|
| 783 | @(match sym_eq ??? (traceinf_traceinfp_app …) with [ refl ⇒ ? ]) |
---|
| 784 | @(reacting … STEPS NOTSILENT) |
---|
| 785 | @show_reactive' |
---|
| 786 | qed. |
---|
[399] | 787 | |
---|
[487] | 788 | lemma show_reactive : ∀ge,s,e. |
---|
[399] | 789 | ∀EXEC:exec_from ge s e. |
---|
| 790 | ∀REACTIVE:∀tr,s1,e1. |
---|
| 791 | execution_isteps tr 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 ? REACTIVE)) s e. |
---|
[487] | 794 | [ #ge #s #e #EXEC #REACTIVE |
---|
| 795 | @show_reactive' |
---|
| 796 | | @(REACTIVE … (isteps_none …)) |
---|
| 797 | ] qed. |
---|
[399] | 798 | |
---|
[487] | 799 | lemma execution_characterisation_complete: |
---|
[399] | 800 | ∀classic:(∀P:Prop.P ∨ ¬P). |
---|
[487] | 801 | ∀constructive_indefinite_description:(∀A:Type[0]. ∀P:A→Prop. (∃x. P x) → Sig A P). |
---|
[399] | 802 | ∀ge,s,e. |
---|
| 803 | exec_from ge s e → |
---|
| 804 | execution_characterisation s (se_step E0 s e). |
---|
[487] | 805 | #classic #constructive_indefinite_description #ge #s #e #EXEC |
---|
| 806 | cases (classic (∀tr1,s1,e1. execution_isteps tr1 s e s1 e1 → |
---|
[399] | 807 | execution_not_over e1)); |
---|
[487] | 808 | [ #NONTERMINATING |
---|
| 809 | cases (classic (∃tr,s1,e1. execution_isteps tr s e s1 e1 ∧ |
---|
[399] | 810 | ∀tr2,s2,e2. execution_isteps tr2 s1 e1 s2 e2 → tr2 = E0)); |
---|
[487] | 811 | [ *; #tr *; #s1 *; #e1 *; #INITIAL #UNREACTIVE |
---|
| 812 | @(ec_diverges … s ? tr) |
---|
| 813 | @(diverges_diverging … INITIAL) |
---|
| 814 | @(show_divergence s1 e1) |
---|
| 815 | [ #tr2 #s2 #e2 #S @(NONTERMINATING (Eapp tr tr2) s2 e2) |
---|
| 816 | @(isteps_trans … INITIAL S) |
---|
| 817 | | #tr2 #s2 #e2 #S @(UNREACTIVE … S) |
---|
| 818 | | #tr2 #s2 #o #k #i #e2 #STEPS |
---|
| 819 | lapply (NONTERMINATING (Eapp tr tr2) s2 (se_interact o k i e2) ?); |
---|
| 820 | [ @(isteps_trans … INITIAL STEPS) ] |
---|
| 821 | #NOTOVER inversion NOTOVER; |
---|
| 822 | [ #tr' #s' #e' #E destruct (E); |
---|
| 823 | | #o' #k' #tr' #s' #e' #i' #E destruct (E); |
---|
| 824 | %{ tr'} %{s'} %{e'} % //; |
---|
| 825 | cases (several_steps … INITIAL EXEC); #_ #EXEC1 |
---|
| 826 | cases (several_steps … STEPS EXEC1); #_ #EXEC2 |
---|
| 827 | @(interaction_is_not_silent … EXEC2) |
---|
| 828 | ] |
---|
| 829 | ] |
---|
[399] | 830 | |
---|
[487] | 831 | | *; #NOTUNREACTIVE |
---|
| 832 | cut (∀tr,s1,e1.execution_isteps tr s e s1 e1 → |
---|
[399] | 833 | ∃x.execution_isteps (\fst x) s1 e1 (\fst (\snd x)) (\snd (\snd x)) ∧ (\fst x) ≠ E0); |
---|
[487] | 834 | [ #tr #s1 #e1 #STEPS |
---|
| 835 | @(classical_doubleneg classic) % #NOREACTION |
---|
| 836 | @NOTUNREACTIVE |
---|
| 837 | %{ tr} %{s1} %{e1} % //; |
---|
| 838 | #tr2 #s2 #e2 #STEPS2 |
---|
| 839 | lapply (not_ex_all_not … NOREACTION); #NR1 |
---|
| 840 | lapply (not_and_to_imply classic … (NR1 〈tr2,〈s2,e2〉〉)); #NR2 |
---|
| 841 | @(classical_doubleneg classic) |
---|
| 842 | @NR2 normalize // |
---|
| 843 | | #REACTIVE |
---|
| 844 | @ec_reacts |
---|
| 845 | [ 2: @reacts |
---|
| 846 | @(show_reactive ge s … EXEC) |
---|
| 847 | #tr #s1 #e1 #STEPS |
---|
| 848 | @constructive_indefinite_description |
---|
| 849 | @(REACTIVE … tr s1 e1 STEPS) |
---|
| 850 | | skip |
---|
| 851 | ] |
---|
| 852 | ] |
---|
| 853 | ] |
---|
[399] | 854 | |
---|
[487] | 855 | | #NOTNONTERMINATING lapply (classical_not_all_ex_not classic … NOTNONTERMINATING); |
---|
| 856 | *; #tr #NNT2 lapply (classical_not_all_ex_not classic … NNT2); |
---|
| 857 | *; #s' #NNT3 lapply (classical_not_all_ex_not classic … NNT3); |
---|
| 858 | *; #e #NNT4 elim (imply_to_and classic … NNT4); |
---|
| 859 | cases e; |
---|
| 860 | [ #tr' #r #m #STEPS #NOSTEP |
---|
| 861 | @(ec_terminates s r m ? (Eapp tr tr')) % |
---|
| 862 | [ @s' |
---|
| 863 | | @STEPS |
---|
| 864 | ] |
---|
| 865 | | #tr' #s'' #e' #STEPS *; #NOSTEP @False_rect_Type0 |
---|
| 866 | @NOSTEP // |
---|
[797] | 867 | | #msg #STEPS #NOSTEP |
---|
[487] | 868 | @(ec_wrong ? s s' tr) % //; |
---|
[399] | 869 | (* The following is stupidly complicated when most of the cases are impossible. |
---|
| 870 | It ought to be simplified. *) |
---|
[487] | 871 | | #o #k #i #e' #STEPS #NOSTEP |
---|
| 872 | cases e' in STEPS NOSTEP; |
---|
| 873 | [ #tr' #r #m #STEPS #NOSTEP |
---|
| 874 | @(ec_terminates s ???) |
---|
| 875 | [ 4: @(annoying_corner_case_terminates … STEPS) ] |
---|
| 876 | | #tr1 #s1 #e1 #STEPS *; #NOSTEP |
---|
| 877 | @False_ind @NOSTEP // |
---|
[797] | 878 | | #msg #STEPS #NOSTEP |
---|
[487] | 879 | lapply (exec_step_interaction ge s'); |
---|
| 880 | cases (several_steps … STEPS EXEC); #_ |
---|
| 881 | whd in ⊢ (% → ?); |
---|
| 882 | >(exec_inf_aux_unfold …) |
---|
| 883 | cases (exec_step ge s'); |
---|
| 884 | [ #o1 #k1 #EXEC' #H whd in EXEC':(?%?) H; |
---|
[1350] | 885 | cases (se_inv … EXEC'); *; #E1 #E2 #H2 destruct (E1 E2); normalize in H2; |
---|
[487] | 886 | cases (H i); #tr1 *; #s1 *; #K #E >K in H2 |
---|
| 887 | >(exec_inf_aux_unfold …) |
---|
[708] | 888 | whd in ⊢ (?%? → ?) @is_final_elim [ #r ] |
---|
[487] | 889 | #F #S whd in S:(?%?); cases (se_inv … S); |
---|
[708] | 890 | | #x cases x; #tr' #s' whd in ⊢ (?%? → ?) |
---|
[891] | 891 | @is_final_elim' [ #r ] #F #S whd in S:(?%?); |
---|
[487] | 892 | cases (se_inv … S); |
---|
[797] | 893 | | #msg #S cases (se_inv … S); |
---|
[487] | 894 | ] |
---|
| 895 | | #o1 #k1 #i1 #e1 #STEPS #NOSTEP |
---|
| 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; |
---|
[1350] | 902 | cases (se_inv … EXEC'); *; #E1 #E2 #H2 destruct (E1 E2); normalize in H2; |
---|
[487] | 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 | ] |
---|
| 913 | ] |
---|
| 914 | ] |
---|
| 915 | qed. |
---|
[399] | 916 | |
---|
[487] | 917 | inductive execution_matches_behavior: s_execution → program_behavior → Prop ≝ |
---|
[399] | 918 | | emb_terminates: ∀s,e,tr,r,m. |
---|
| 919 | execution_terminates tr s e r m → |
---|
| 920 | execution_matches_behavior e (Terminates tr r) |
---|
| 921 | | emb_diverges: ∀s,e,tr. |
---|
| 922 | execution_diverges tr s e → |
---|
| 923 | execution_matches_behavior e (Diverges tr) |
---|
| 924 | | emb_reacts: ∀s,e,tr. |
---|
| 925 | execution_reacts tr s e → |
---|
| 926 | execution_matches_behavior e (Reacts tr) |
---|
| 927 | | emb_wrong: ∀e,s,s',tr. |
---|
| 928 | execution_goes_wrong tr s e s' → |
---|
| 929 | execution_matches_behavior e (Goes_wrong tr) |
---|
[797] | 930 | | emb_initially_wrong: ∀msg. |
---|
| 931 | execution_matches_behavior (se_wrong msg) (Goes_wrong E0). |
---|
[399] | 932 | |
---|
[487] | 933 | lemma exec_state_terminates: ∀tr,tr',s,s',e,r,m. |
---|
[399] | 934 | execution_terminates tr s (se_step tr' s' e) r m → s = s'. |
---|
[487] | 935 | #tr #tr' #s #s' #e #r #m #H inversion H; |
---|
| 936 | [ #s1 #s2 #tr1 #tr2 #r' #e' #m' #H' #E1 #E2 #E3 #E4 #E5 destruct; @refl |
---|
| 937 | | #s1 #s2 #tr1 #tr2 #r' #e' #m' #o #k #i #H' #E1 #E2 #E3 #E4 #E5 destruct; @refl |
---|
| 938 | ] qed. |
---|
[399] | 939 | |
---|
[487] | 940 | lemma exec_state_diverges: ∀tr,tr',s,s',e. |
---|
[399] | 941 | execution_diverges tr s (se_step tr' s' e) → s = s'. |
---|
[487] | 942 | #tr #tr' #s #s' #e #H inversion H; |
---|
| 943 | #tr1 #s1 #s2 #e1 #e2 #H' #E1 #E2 #E3 #E4 destruct; @refl qed. |
---|
[399] | 944 | |
---|
[487] | 945 | lemma exec_state_reacts: ∀tr,tr',s,s',e. |
---|
[399] | 946 | execution_reacts tr s (se_step tr' s' e) → s = s'. |
---|
[487] | 947 | #tr #tr' #s #s' #e #H inversion H; |
---|
| 948 | #tr1 #s1 #e1 #H' #E1 #E2 #E3 destruct; @refl qed. |
---|
[399] | 949 | |
---|
[487] | 950 | lemma exec_state_wrong: ∀tr,tr',s,s',s'',e. |
---|
[399] | 951 | execution_goes_wrong tr s (se_step tr' s' e) s'' → s = s'. |
---|
[487] | 952 | #tr #tr' #s #s' #s'' #e #H inversion H; |
---|
[797] | 953 | #tr1 #s1 #s2 #e1 #msg #H' #E1 #E2 #E3 #E4 destruct; @refl qed. |
---|
[399] | 954 | |
---|
[487] | 955 | lemma behavior_of_execution: ∀s,e. |
---|
[399] | 956 | execution_characterisation s e → |
---|
| 957 | ∃b:program_behavior. execution_matches_behavior e b. |
---|
[487] | 958 | #s0 #e0 #exec |
---|
| 959 | cases exec; |
---|
| 960 | [ #s #r #m #e #tr #TERM |
---|
| 961 | %{ (Terminates tr r)} |
---|
| 962 | @(emb_terminates … TERM) |
---|
| 963 | | #s #e #tr #DIV |
---|
| 964 | %{ (Diverges tr)} |
---|
| 965 | @(emb_diverges … DIV) |
---|
| 966 | | #s #e #tr #REACTS |
---|
| 967 | %{ (Reacts tr)} |
---|
| 968 | @(emb_reacts … REACTS) |
---|
| 969 | | #e #s #s' #tr #WRONG |
---|
| 970 | %{ (Goes_wrong tr)} |
---|
| 971 | @(emb_wrong … WRONG) |
---|
| 972 | ] qed. |
---|
[399] | 973 | |
---|
[487] | 974 | lemma initial_state_not_final: ∀ge,s. |
---|
[399] | 975 | initial_state ge s → |
---|
| 976 | ¬ ∃r.final_state s r. |
---|
[487] | 977 | #ge #s #H cases H; |
---|
| 978 | #b #f #ge #m #E1 #E2 #E3 #E4 % *; #r #H2 |
---|
| 979 | inversion H2; |
---|
| 980 | #r' #m' #E5 #E6 destruct (E5); |
---|
| 981 | qed. |
---|
[399] | 982 | |
---|
[487] | 983 | lemma initial_step: ∀ge,s,e. |
---|
[732] | 984 | exec_inf_aux ?? clight_exec ge (Value ??? 〈E0,s〉) = e → |
---|
[399] | 985 | ¬(∃r.final_state s r) → |
---|
[708] | 986 | ∃e'.e = e_step ??? E0 s e'. |
---|
[487] | 987 | #ge #s #e >(exec_inf_aux_unfold …) |
---|
[891] | 988 | whd in ⊢ (??%? → ?) @is_final_elim' |
---|
[708] | 989 | [ #r #FINAL #EXEC #NOTFINAL |
---|
[487] | 990 | @False_ind @(absurd ?? NOTFINAL) |
---|
[708] | 991 | %{r} @FINAL |
---|
[487] | 992 | | #F1 #EXEC #F2 whd in EXEC:(??%?); % [ 2: <EXEC @refl ] |
---|
| 993 | qed. |
---|
[399] | 994 | |
---|
[487] | 995 | theorem exec_inf_equivalence: |
---|
[399] | 996 | ∀classic:(∀P:Prop.P ∨ ¬P). |
---|
[487] | 997 | ∀constructive_indefinite_description:(∀A:Type[0]. ∀P:A→Prop. (∃x. P x) → Sig A P). |
---|
[732] | 998 | ∀p,e. single_exec_of (exec_inf ?? clight_fullexec p) e → |
---|
[399] | 999 | ∃b.execution_matches_behavior e b ∧ exec_program p b. |
---|
[487] | 1000 | #classic #constructive_indefinite_description #p #e |
---|
| 1001 | whd in ⊢ (?%? → ??(λ_.?(?%?)%)); |
---|
[891] | 1002 | lapply (make_initial_state_sound p) |
---|
| 1003 | lapply (the_initial_state p) |
---|
| 1004 | whd in ⊢ (? → ? → ?(match % with [_ ⇒ ? | _ ⇒ ?])? → ?) |
---|
| 1005 | cases (make_initial_state p) |
---|
[1244] | 1006 | [ #s #INITIAL' #INITIAL whd in INITIAL ⊢ (?%? → ?); |
---|
[891] | 1007 | >exec_inf_aux_unfold |
---|
[708] | 1008 | whd in ⊢ (?%? → ?) |
---|
[891] | 1009 | @is_final_elim' |
---|
[708] | 1010 | [ #r #F @False_ind |
---|
[1244] | 1011 | @(absurd ?? (initial_state_not_final … INITIAL)) |
---|
[708] | 1012 | %{r} @F |
---|
[487] | 1013 | | #NOTFINAL whd in ⊢ (?%? → ?); cases e; |
---|
[797] | 1014 | [ #tr #r #m #EXEC0 | #tr #s' #e0 #EXEC0 | #msg #EXEC0 | #o #k #i #e #EXEC0 ] |
---|
[487] | 1015 | cases (se_inv … EXEC0); *; #E1 #E2 <E1 <E2 #EXEC' |
---|
| 1016 | lapply (behavior_of_execution ?? |
---|
[1244] | 1017 | (execution_characterisation_complete classic constructive_indefinite_description ? s ? EXEC')); |
---|
[891] | 1018 | *; #b #MATCHES %{b} % [ @MATCHES ] |
---|
[1244] | 1019 | #ge #Ege |
---|
[487] | 1020 | inversion MATCHES; |
---|
| 1021 | [ #s0 #e1 #tr1 #r #m #TERM #EXEC #BEHAVES <EXEC in TERM |
---|
| 1022 | #TERM |
---|
| 1023 | lapply (exec_state_terminates … TERM); #E1 |
---|
| 1024 | >E1 in TERM #TERM |
---|
| 1025 | @(program_terminates (mk_transrel … step) ?? ge s) |
---|
[1244] | 1026 | [ 2: @INITIAL |
---|
| 1027 | | 3: <Ege @(terminates_sound … TERM EXEC') |
---|
[487] | 1028 | | skip |
---|
| 1029 | | //; |
---|
| 1030 | ] |
---|
| 1031 | | #s0 #e #tr #DIVERGES #EXEC #E2 <EXEC in DIVERGES #DIVERGES |
---|
| 1032 | lapply (exec_state_diverges … DIVERGES); |
---|
| 1033 | #E1 >E1 in DIVERGES #DIVERGES |
---|
| 1034 | inversion DIVERGES; #tr' #s1 #s2 #e1 #e2 #INITSTEPS #DIVERGING #E4 #E5 #E6 |
---|
| 1035 | <E4 in INITSTEPS ⊢ % <E5 in E6 ⊢ % #E6 #INITSTEPS |
---|
| 1036 | cut (e0 = e1); [ destruct (E6) skip (MATCHES EXEC0 EXEC'); // ] |
---|
| 1037 | #E7 <E7 in INITSTEPS #INITSTEPS |
---|
| 1038 | cases (several_steps … INITSTEPS EXEC'); #INITSTAR #EXECDIV |
---|
[1244] | 1039 | @(program_diverges (mk_transrel … step) ?? ge s … INITIAL) |
---|
| 1040 | [ 2: <Ege @INITSTAR |
---|
| 1041 | | 3: <Ege @(silent_sound … DIVERGING EXECDIV) |
---|
| 1042 | ] |
---|
[487] | 1043 | | #s0 #e #tr #REACTS #EXEC #E2 <EXEC in REACTS #REACTS |
---|
| 1044 | lapply (exec_state_reacts … REACTS); |
---|
| 1045 | #E1 >E1 in REACTS #REACTS |
---|
| 1046 | inversion REACTS; #tr' #s' #e'' #REACTING #E4 #E5 |
---|
| 1047 | <E4 in REACTING ⊢ % <E5 #REACTING #E6 |
---|
| 1048 | cut (e0 = e''); [ destruct (E6) skip (MATCHES EXEC0 EXEC'); // ] |
---|
| 1049 | #E7 <E7 in REACTING #REACTING |
---|
[1244] | 1050 | @(program_reacts (mk_transrel … step) ?? ge s … INITIAL) |
---|
| 1051 | <Ege @(reacts_sound … REACTING EXEC') |
---|
[487] | 1052 | | #e #s1 #s2 #tr #WRONG #EXEC #E2 <EXEC in WRONG #WRONG |
---|
| 1053 | lapply (exec_state_wrong … WRONG); |
---|
| 1054 | #E1 >E1 in WRONG #WRONG |
---|
[797] | 1055 | inversion WRONG; #tr' #s1' #s2' #e'' #msg #GOESWRONG #E4 #E5 #E6 #E7 |
---|
[487] | 1056 | <E4 in GOESWRONG ⊢ % <E5 <E7 #GOESWRONG |
---|
| 1057 | cut (e0 = e''); [ destruct (E6) skip (INITIAL Ege MATCHES EXEC0 EXEC'); // ] |
---|
| 1058 | #E8 <E8 in GOESWRONG #GOESWRONG |
---|
| 1059 | elim (wrong_sound … WRONG EXEC' NOTFINAL); *; #STAR #STOP #FINAL |
---|
[1244] | 1060 | <Ege |
---|
| 1061 | @(program_goes_wrong (mk_transrel … step) ?? ? s … INITIAL STAR STOP) |
---|
[487] | 1062 | #r % #F @(absurd ?? FINAL) %{r} @F |
---|
[797] | 1063 | | #msg #E destruct (E); |
---|
[487] | 1064 | ] |
---|
| 1065 | ] |
---|
[797] | 1066 | | #msg whd in ⊢ ((∀_.? → %) → ?); |
---|
[487] | 1067 | #NOINIT #_ #EXEC |
---|
| 1068 | %{ (Goes_wrong E0)} % |
---|
| 1069 | [ whd in EXEC:(?%?); |
---|
| 1070 | cases e in EXEC; |
---|
[797] | 1071 | [ #tr #r #m #EXEC0 | #tr #s' #e0 #EXEC0 | #msg #EXEC0 | #o #k #i #e #EXEC0 ] |
---|
[487] | 1072 | cases (se_inv … EXEC0); |
---|
| 1073 | @emb_initially_wrong |
---|
| 1074 | | #ge #Ege |
---|
| 1075 | @program_goes_initially_wrong |
---|
| 1076 | #s % #INIT cases (NOINIT s INIT); #ge' #H @H |
---|
| 1077 | ] |
---|
| 1078 | ] qed. |
---|
[399] | 1079 | |
---|