[2286] | 1 | include "joint/semantics.ma". |
---|
[2422] | 2 | include "common/StructuredTraces.ma". |
---|
[1976] | 3 | |
---|
[2186] | 4 | record evaluation_params : Type[1] ≝ |
---|
| 5 | { globals: list ident |
---|
| 6 | ; sparams:> sem_params |
---|
[2470] | 7 | ; exit: program_counter |
---|
[2286] | 8 | ; ev_genv: genv sparams globals |
---|
[2443] | 9 | (* ; io_env : state sparams → ∀o:io_out.res (io_in o) *) |
---|
[2422] | 10 | }. |
---|
[2470] | 11 | |
---|
[2457] | 12 | |
---|
| 13 | |
---|
[2422] | 14 | record prog_params : Type[1] ≝ |
---|
| 15 | { prog_spars : sem_params |
---|
| 16 | ; prog : joint_program prog_spars |
---|
[2481] | 17 | ; stack_sizes : (Σi.is_internal_function_of_program … prog i) → ℕ |
---|
[2443] | 18 | (* ; prog_io : state prog_spars → ∀o.res (io_in o) *) |
---|
[2422] | 19 | }. |
---|
[1976] | 20 | |
---|
[2473] | 21 | lemma map_Exists : ∀A,B,f,P,l.Exists B P (map A B f l) → Exists ? (λx.P (f x)) l. |
---|
| 22 | #A #B #f #P #l elim l -l [*] |
---|
| 23 | #hd #tl #IH * |
---|
| 24 | [ #Phd %1{Phd} |
---|
| 25 | | #Ptl %2{(IH Ptl)} |
---|
| 26 | ] |
---|
| 27 | qed. |
---|
| 28 | |
---|
| 29 | lemma Exists_In : ∀A,P,l.Exists A P l → ∃x.In A l x ∧ P x. |
---|
| 30 | #A #P #l elim l -l [*] #hd #tl #IH * |
---|
| 31 | [ #Phd %{hd} %{Phd} %1 % |
---|
| 32 | | #Ptl elim (IH Ptl) #x * #H1 #H2 %{x} %{H2} %2{H1} |
---|
| 33 | ] |
---|
| 34 | qed. |
---|
| 35 | |
---|
| 36 | lemma In_Exists : ∀A,P,l,x.In A l x → P x → Exists A P l. |
---|
| 37 | #A #P #l elim l -l [ #x *] #hd #tl #IH #x * |
---|
| 38 | [ #EQ >EQ #H %1{H} |
---|
| 39 | | #Intl #Px %2{(IH … Intl Px)} |
---|
| 40 | ] |
---|
| 41 | qed. |
---|
| 42 | |
---|
[2481] | 43 | lemma Exists_mp : ∀A,P,Q,l.(∀x.P x → Q x) → Exists A P l → Exists A Q l. |
---|
| 44 | #A #P #Q #l #H elim l -l [*] #hd #tl #IH * #G [ %1 | %2 ] /2/ qed. |
---|
| 45 | |
---|
[2422] | 46 | definition make_global : prog_params → evaluation_params |
---|
| 47 | ≝ |
---|
| 48 | λpars. |
---|
| 49 | (* Invariant: a -1 block is unused in common/Globalenvs *) |
---|
| 50 | let b ≝ mk_block Code (-1) in |
---|
[2470] | 51 | let ptr ≝ mk_program_counter «b, refl …» one in |
---|
[2422] | 52 | let p ≝ prog pars in |
---|
| 53 | mk_evaluation_params |
---|
| 54 | (prog_var_names … p) |
---|
| 55 | (prog_spars pars) |
---|
[2470] | 56 | ptr |
---|
[2481] | 57 | (mk_genv_gen ?? (globalenv_noinit ? p) ? (stack_sizes pars)) |
---|
[2443] | 58 | (* (prog_io pars) *). |
---|
[2481] | 59 | #s #H |
---|
| 60 | elim (find_symbol_exists … p s ?) |
---|
| 61 | [ #bl #EQ >EQ % #ABS destruct(ABS)|*:] |
---|
| 62 | @Exists_append_r |
---|
| 63 | @(Exists_mp … H) // |
---|
[2422] | 64 | qed. |
---|
[2186] | 65 | |
---|
[2422] | 66 | coercion prog_params_to_ev_params : ∀p : prog_params.evaluation_params |
---|
| 67 | ≝ make_global on _p : prog_params to evaluation_params. |
---|
[2186] | 68 | |
---|
[2457] | 69 | axiom BadMain : String. |
---|
[2422] | 70 | |
---|
| 71 | definition make_initial_state : |
---|
| 72 | ∀pars: prog_params.res (state_pc pars) ≝ |
---|
| 73 | λpars.let p ≝ prog pars in |
---|
| 74 | let sem_globals : evaluation_params ≝ pars in |
---|
| 75 | let ge ≝ ev_genv sem_globals in |
---|
| 76 | let m ≝ alloc_mem … p in |
---|
| 77 | let 〈m,spb〉 ≝ alloc … m 0 external_ram_size XData in |
---|
| 78 | let 〈m,ispb〉 ≝ alloc … m 0 internal_ram_size XData in |
---|
[2470] | 79 | let dummy_pc ≝ mk_program_counter «mk_block Code (-1), refl …» one in |
---|
[2422] | 80 | let spp : xpointer ≝ mk_pointer spb (mk_offset (bitvector_of_Z ? external_ram_size)) in |
---|
[2443] | 81 | (* let ispp : xpointer ≝ mk_pointer ispb (mk_offset (bitvector_of_nat ? 47)) in *) |
---|
[2422] | 82 | let main ≝ prog_main … p in |
---|
[2443] | 83 | let st0 ≝ mk_state pars (empty_framesT …) empty_is (BBbit false) (empty_regsT … spp) m in |
---|
[2422] | 84 | (* use exit sem_globals as ra and call_dest_for_main as dest *) |
---|
[2484] | 85 | let st0' ≝ mk_state_pc … (set_sp … spp st0) (exit sem_globals) in |
---|
| 86 | ! st0'' ← save_frame ?? sem_globals (call_dest_for_main … pars) st0' ; |
---|
[2443] | 87 | let st_pc0 ≝ mk_state_pc ? st0'' dummy_pc in |
---|
[2457] | 88 | ! main ← opt_to_res … [MSG BadMain; CTX ? main ] (funct_of_ident … ge main) ; |
---|
| 89 | match ? return λx.description_of_function … main = x → ? with |
---|
| 90 | [ Internal fn ⇒ λprf. |
---|
[2473] | 91 | let main : Σi : ident.is_internal_function ??? ≝ «main, ?» in |
---|
[2457] | 92 | ! st' ← eval_internal_call_no_pc ?? ge main (call_args_for_main … pars) st_pc0 ; |
---|
[2470] | 93 | let pc' ≝ eval_internal_call_pc … ge main in |
---|
[2457] | 94 | return mk_state_pc … st' pc' |
---|
| 95 | | External _ ⇒ λ_.Error … [MSG BadMain; CTX ? main] (* External main not supported: why? *) |
---|
| 96 | ] (refl …). |
---|
[2470] | 97 | [ @(description_of_internal_function … prf) |
---|
[2443] | 98 | | cases spb normalize // |
---|
| 99 | ] |
---|
[2422] | 100 | qed. |
---|
| 101 | |
---|
[2477] | 102 | definition joint_classify_seq : |
---|
| 103 | ∀p : evaluation_params.state p → joint_seq p (globals … p) → status_class ≝ |
---|
| 104 | λp,st,stmt. |
---|
| 105 | match stmt with |
---|
| 106 | [ CALL f args dest ⇒ |
---|
| 107 | match function_of_call ?? (ev_genv p) st f with |
---|
| 108 | [ OK fn ⇒ |
---|
| 109 | match description_of_function … fn with |
---|
| 110 | [ Internal _ ⇒ cl_call |
---|
| 111 | | External _ ⇒ cl_other |
---|
| 112 | ] |
---|
| 113 | | Error _ ⇒ cl_other |
---|
| 114 | ] |
---|
| 115 | | _ ⇒ cl_other |
---|
| 116 | ]. |
---|
| 117 | |
---|
| 118 | definition joint_classify_step : |
---|
| 119 | ∀p : evaluation_params.state p → joint_step p (globals … p) → status_class ≝ |
---|
| 120 | λp,st,stmt. |
---|
| 121 | match stmt with |
---|
| 122 | [ step_seq s ⇒ joint_classify_seq p st s |
---|
| 123 | | COND _ _ ⇒ cl_jump |
---|
| 124 | ]. |
---|
| 125 | |
---|
| 126 | definition joint_classify_final : |
---|
| 127 | ∀p : evaluation_params.joint_fin_step p → status_class ≝ |
---|
| 128 | λp,stmt. |
---|
| 129 | match stmt with |
---|
| 130 | [ GOTO _ ⇒ cl_other |
---|
| 131 | | RETURN ⇒ cl_return |
---|
| 132 | | TAILCALL _ _ _ ⇒ cl_other (* this needs tailcalls implemented in structured traces *) |
---|
| 133 | ]. |
---|
| 134 | |
---|
[2457] | 135 | definition joint_classify : |
---|
| 136 | ∀p : evaluation_params.state_pc p → status_class ≝ |
---|
| 137 | λp,st. |
---|
| 138 | match fetch_statement ? p … (ev_genv p) (pc … st) with |
---|
| 139 | [ OK f_s ⇒ |
---|
[2477] | 140 | match \snd f_s with |
---|
| 141 | [ sequential s _ ⇒ joint_classify_step p st s |
---|
| 142 | | final s ⇒ joint_classify_final p s |
---|
[2422] | 143 | ] |
---|
[2457] | 144 | | Error _ ⇒ cl_other |
---|
[2422] | 145 | ]. |
---|
| 146 | |
---|
[2457] | 147 | lemma joint_classify_call : ∀p : evaluation_params.∀st. |
---|
| 148 | joint_classify p st = cl_call → |
---|
| 149 | ∃f,f',args,dest,next,fn,fd. |
---|
| 150 | fetch_statement ? p … (ev_genv p) (pc … st) = |
---|
| 151 | OK ? 〈f, sequential … (CALL … f' args dest) next〉 ∧ |
---|
| 152 | function_of_call … (ev_genv p) st f' = OK ? fn ∧ |
---|
| 153 | description_of_function … (ev_genv p) fn = Internal … fd. |
---|
| 154 | #p #st |
---|
| 155 | whd in match joint_classify; normalize nodelta |
---|
[2477] | 156 | inversion (fetch_statement ? p … (ev_genv p) (pc … st)) normalize nodelta |
---|
[2457] | 157 | [ * #f * [| * [ #lbl || #b #f #args ]] |
---|
| 158 | [ * [| #a #lbl #next ] |
---|
| 159 | [ * |
---|
| 160 | [14: #f' #args #dest | #s | #lbl | #mv | #a | #a | #i #prf #dpl #dph | #op #a #b #a' #b' |
---|
| 161 | | #op #a #a' | #op #a #a' #arg ||| #a #dpl #dph | #dpl #dph #arg |
---|
| 162 | | #ext ] #next |
---|
[2477] | 163 | [ whd in match joint_classify_step; whd in match joint_classify_seq; |
---|
| 164 | normalize nodelta |
---|
| 165 | inversion (function_of_call ?????) normalize nodelta |
---|
| 166 | [ #fn |
---|
| 167 | inversion (description_of_function ?? fn) #fd |
---|
[2457] | 168 | #EQfd |
---|
| 169 | | #e |
---|
| 170 | ] #EQfn |
---|
[2422] | 171 | ] |
---|
| 172 | ] |
---|
[2457] | 173 | ] |
---|
| 174 | | #e |
---|
| 175 | ] #EQfetch |
---|
| 176 | [|*: #ABS normalize in ABS; destruct(ABS) ] |
---|
| 177 | normalize nodelta #_ |
---|
[2477] | 178 | %{f} %{f'} %{args} %{dest} %{next} %{fn} %{fd} |
---|
| 179 | %{EQfd} %{EQfn} % |
---|
[2457] | 180 | qed. |
---|
[2422] | 181 | |
---|
[2473] | 182 | definition joint_after_ret : ∀p:evaluation_params. |
---|
| 183 | (Σs : state_pc p.joint_classify p s = cl_call) → state_pc p → Prop ≝ |
---|
| 184 | λp,s1,s2. |
---|
| 185 | match fetch_statement ? p … (ev_genv p) (pc … s1) with |
---|
| 186 | [ OK x ⇒ |
---|
| 187 | match \snd x with |
---|
| 188 | [ sequential s next ⇒ |
---|
| 189 | pc … s2 = succ_pc p p (pc … s1) next |
---|
| 190 | | _ ⇒ False (* never happens *) |
---|
| 191 | ] |
---|
| 192 | | _ ⇒ False (* never happens *) |
---|
| 193 | ]. |
---|
| 194 | |
---|
[2457] | 195 | definition joint_call_ident : ∀p:evaluation_params. |
---|
| 196 | (Σs : state_pc p.joint_classify p s = cl_call) → ident ≝ |
---|
[2473] | 197 | (* this is a definition without a dummy ident : |
---|
[2457] | 198 | λp,st. |
---|
| 199 | match ? |
---|
| 200 | return λx. |
---|
| 201 | !〈f, s〉 ← fetch_statement ? p … (ev_genv p) (pc … st) ; |
---|
| 202 | match s with |
---|
| 203 | [ sequential s next ⇒ |
---|
| 204 | match s with |
---|
| 205 | [ step_seq s ⇒ |
---|
| 206 | match s with |
---|
| 207 | [ CALL f' args dest ⇒ |
---|
| 208 | function_of_call … (ev_genv p) st f' |
---|
| 209 | | _ ⇒ Error … [ ] |
---|
| 210 | ] |
---|
| 211 | | _ ⇒ Error … [ ] |
---|
| 212 | ] |
---|
| 213 | | _ ⇒ Error … [ ] |
---|
| 214 | ] = x → ? with |
---|
| 215 | [ OK v ⇒ λ_.v |
---|
| 216 | | Error e ⇒ λABS.⊥ |
---|
| 217 | ] (refl …). |
---|
| 218 | @hide_prf |
---|
| 219 | elim (joint_classify_call … (pi2 … st)) |
---|
| 220 | #f *#f' *#args *#dest *#next *#fn *#fd ** #EQ1 #EQ2 #EQ3 |
---|
| 221 | lapply ABS -ABS |
---|
| 222 | >EQ1 >m_return_bind normalize nodelta >EQ2 #ABS destruct(ABS) |
---|
[2473] | 223 | qed. *) |
---|
| 224 | (* with a dummy ident (which is never used as seen above in the commented script) |
---|
| 225 | I think handling of the function is easier *) |
---|
| 226 | λp,st. |
---|
| 227 | let dummy : ident ≝ an_identifier ? one in |
---|
| 228 | match fetch_statement ? p … (ev_genv p) (pc … st) with |
---|
| 229 | [ OK x ⇒ |
---|
| 230 | match \snd x with |
---|
| 231 | [ sequential s next ⇒ |
---|
| 232 | match s with |
---|
| 233 | [ step_seq s ⇒ |
---|
| 234 | match s with |
---|
| 235 | [ CALL f' args dest ⇒ |
---|
| 236 | match function_of_call … (ev_genv p) st f' with |
---|
| 237 | [ OK f ⇒ f |
---|
| 238 | | _ ⇒ dummy |
---|
| 239 | ] |
---|
| 240 | | _ ⇒ dummy |
---|
| 241 | ] |
---|
| 242 | | _ ⇒ dummy |
---|
| 243 | ] |
---|
| 244 | | _ ⇒ dummy |
---|
| 245 | ] |
---|
| 246 | | _ ⇒ dummy |
---|
| 247 | ]. |
---|
[2457] | 248 | |
---|
[2470] | 249 | definition pcDeq ≝ mk_DeqSet program_counter eq_program_counter ?. |
---|
| 250 | *#p1 #EQ1 * #p2 #EQ2 @eq_program_counter_elim |
---|
[1976] | 251 | [ #EQ destruct % #H % |
---|
| 252 | | * #NEQ % #ABS destruct elim (NEQ ?) % |
---|
| 253 | ] |
---|
| 254 | qed. |
---|
[2186] | 255 | |
---|
[2443] | 256 | (* |
---|
[2186] | 257 | let rec io_evaluate O I X (env : ∀o.res (I o)) (c : IO O I X) on c : res X ≝ |
---|
| 258 | match c with |
---|
| 259 | [ Value x ⇒ OK … x |
---|
| 260 | | Interact o f ⇒ |
---|
| 261 | ! i ← env o ; |
---|
| 262 | io_evaluate O I X env (f i) |
---|
| 263 | | Wrong e ⇒ Error … e |
---|
| 264 | ]. |
---|
[2443] | 265 | *) |
---|
[2186] | 266 | |
---|
| 267 | definition cost_label_of_stmt : |
---|
| 268 | ∀p : evaluation_params.joint_statement p (globals p) → option costlabel ≝ |
---|
| 269 | λp,s.match s with |
---|
| 270 | [ sequential s _ ⇒ |
---|
| 271 | match s with |
---|
| 272 | [ step_seq s ⇒ |
---|
| 273 | match s with |
---|
| 274 | [ COST_LABEL lbl ⇒ Some ? lbl |
---|
| 275 | | _ ⇒ None ? |
---|
| 276 | ] |
---|
| 277 | | _ ⇒ None ? |
---|
| 278 | ] |
---|
| 279 | | _ ⇒ None ? |
---|
| 280 | ]. |
---|
| 281 | |
---|
[1976] | 282 | definition joint_abstract_status : |
---|
[2186] | 283 | ∀p : evaluation_params. |
---|
| 284 | abstract_status ≝ |
---|
| 285 | λp. |
---|
[1976] | 286 | mk_abstract_status |
---|
| 287 | (* as_status ≝ *) (state_pc p) |
---|
[2186] | 288 | (* as_execute ≝ *) |
---|
[2481] | 289 | (λs1,s2.(* io_evaluate … (io_env p s1) *) (eval_state … (ev_genv p) s1) = return s2) |
---|
[2470] | 290 | (* as_pc ≝ *) pcDeq |
---|
[1976] | 291 | (* as_pc_of ≝ *) (pc …) |
---|
[2457] | 292 | (* as_classify ≝ *) (joint_classify p) |
---|
[1976] | 293 | (* as_label_of_pc ≝ *) |
---|
| 294 | (λpc. |
---|
[2186] | 295 | match fetch_statement ? p … (ev_genv p) pc with |
---|
[2286] | 296 | [ OK fn_stmt ⇒ cost_label_of_stmt … (\snd fn_stmt) |
---|
[1976] | 297 | | _ ⇒ None ? |
---|
| 298 | ]) |
---|
[2473] | 299 | (* as_after_return ≝ *) (joint_after_ret p) |
---|
[2481] | 300 | (* as_final ≝ *) (λs.is_final p (globals ?) (ev_genv p) (exit p) s ≠ None ?) |
---|
[2457] | 301 | (* as_call_ident ≝ *) (joint_call_ident p). |
---|