Changeset 2446
 Timestamp:
 Nov 9, 2012, 1:21:45 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/joint/lineariseProof.ma
r2445 r2446 39 39 (make_sem_lin_params (mk_lin_params p) p') 40 40 prog). 41 42 definition graph_abstract_status:43 ∀p:unserialized_params.44 (∀F.sem_unserialized_params p F) →45 joint_program (mk_graph_params p) →46 abstract_status47 ≝48 λp,p',prog.49 joint_abstract_status (graph_prog_params p p' prog).50 51 definition lin_abstract_status:52 ∀p:unserialized_params.53 (∀F.sem_unserialized_params p F) →54 joint_program (mk_lin_params p) →55 abstract_status56 ≝57 λp,p',prog.58 joint_abstract_status (lin_prog_params p p' prog).59 60 (*CSC: BUG, the natural must be ≤ 2^16! *)61 (*CSC: already defined? *)62 definition pointer_of_block_and_lin_offset :63 ∀b:block. block_region b = Code → nat → cpointer ≝64 λb,p,n. «mk_pointer b (mk_offset (bitvector_of_nat … n)), p».65 66 definition well_formed_status:67 ∀p,p',graph_prog.68 ∀sigma: identifier LabelTag → option ℕ.69 graph_abstract_status p p' graph_prog → Prop70 ≝71 λp,p',graph_prog,sigma,s.72 sigma (point_of_pointer ? (make_sem_graph_params … (mk_graph_params … p) p') (pc ? s))73 ≠ None ….74 75 definition sigma_pc_of_status:76 ∀p,p',graph_prog.77 ∀sigma: identifier LabelTag → option ℕ.78 ∀s:graph_abstract_status p p' graph_prog.79 well_formed_status … sigma s → ℕ80 ≝81 λp,p',prog,sigma,s.82 match sigma (point_of_pointer ? (make_sem_graph_params … (mk_graph_params … p) p') (pc ? s))83 return λx. x ≠ None ? → ℕ84 with85 [ None ⇒ λprf.⊥86  Some n ⇒ λ_.n ].87 @(absurd ?? prf) //88 qed.89 90 definition linearise_status_fun:91 ∀p,p',graph_prog.92 ∀sigma: identifier LabelTag → option ℕ.93 let lin_prog ≝ linearise ? graph_prog in94 ∀s:graph_abstract_status p p' graph_prog.95 well_formed_status … sigma s →96 lin_abstract_status p p' lin_prog97 ≝98 λp,p',graph_prog,sigma,s,prf.99 mk_state_pc ??100 (pointer_of_block_and_lin_offset (pblock (pc ? s)) …101 (sigma_pc_of_status … sigma … prf)).102 [2: cases (pc ??) * normalize //103  cases daemon (* TODO *) ]104 qed.105 106 definition linearise_status_rel:107 ∀p,p',graph_prog.108 ∀sigma: identifier LabelTag → option ℕ.109 let lin_prog ≝ linearise ? graph_prog in110 status_rel111 (graph_abstract_status p p' graph_prog)112 (lin_abstract_status p p' lin_prog)113 ≝ λp,p',graph_prog,sigma.mk_status_rel …114 (λs1,s2.115 ∃prf: well_formed_status … sigma s1.116 s2 = linearise_status_fun p p' graph_prog sigma s1 prf) ….117 cases daemon (* TODO *)118 qed.119 41 120 42 (*CSC: Paolo, come to the rescue*) … … 149 71 (nth_opt … (S n) c = Some ? 〈None ?, GOTO … next〉)) 150 72 (stmt_implicit_label … s)) (nth_opt … n c). 73 74 definition graph_abstract_status: 75 ∀p:unserialized_params. 76 (∀F.sem_unserialized_params p F) → 77 joint_program (mk_graph_params p) → 78 abstract_status 79 ≝ 80 λp,p',prog. 81 joint_abstract_status (graph_prog_params p p' prog). 82 83 definition lin_abstract_status: 84 ∀p:unserialized_params. 85 (∀F.sem_unserialized_params p F) → 86 joint_program (mk_lin_params p) → 87 abstract_status 88 ≝ 89 λp,p',prog. 90 joint_abstract_status (lin_prog_params p p' prog). 91 92 (*CSC: BUG, the natural must be ≤ 2^16! *) 93 (*CSC: already defined? *) 94 definition pointer_of_block_and_lin_offset : 95 ∀b:block. block_region b = Code → nat → cpointer ≝ 96 λb,p,n. «mk_pointer b (mk_offset (bitvector_of_nat … n)), p». 97 98 definition well_formed_status: 99 ∀p,p',graph_prog. 100 ∀sigma: identifier LabelTag → option ℕ. 101 graph_abstract_status p p' graph_prog → Prop 102 ≝ 103 λp,p',graph_prog,sigma,s. 104 sigma (point_of_pointer ? (make_sem_graph_params … (mk_graph_params … p) p') (pc ? s)) 105 ≠ None …. 106 107 definition sigma_pc_of_status: 108 ∀p,p',graph_prog. 109 ∀sigma: identifier LabelTag → option ℕ. 110 ∀s:graph_abstract_status p p' graph_prog. 111 well_formed_status … sigma s → ℕ 112 ≝ 113 λp,p',prog,sigma,s. 114 match sigma (point_of_pointer ? (make_sem_graph_params … (mk_graph_params … p) p') (pc ? s)) 115 return λx. x ≠ None ? → ℕ 116 with 117 [ None ⇒ λprf.⊥ 118  Some n ⇒ λ_.n ]. 119 @(absurd ?? prf) // 120 qed. 121 122 lemma sigma_pc_of_status_ok: 123 ∀p,p',graph_prog. 124 ∀sigma: identifier LabelTag → option ℕ. 125 ∀s:graph_abstract_status p p' graph_prog. 126 ∀prf:well_formed_status … sigma s. 127 sigma (point_of_pointer ? (make_sem_graph_params … (mk_graph_params … p) p') (pc ? s)) 128 = Some … (sigma_pc_of_status … prf). 129 #p #p' #prog #sigma #s whd in ⊢ (% → ?); 130 whd in match sigma_pc_of_status; normalize nodelta cases (sigma ?) // 131 #abs cases (absurd ?? abs) 132 qed. 133 134 definition linearise_status_fun: 135 ∀p,p',graph_prog. 136 ∀sigma: identifier LabelTag → option ℕ. 137 let lin_prog ≝ linearise ? graph_prog in 138 ∀s:graph_abstract_status p p' graph_prog. 139 well_formed_status … sigma s → 140 lin_abstract_status p p' lin_prog 141 ≝ 142 λp,p',graph_prog,sigma,s,prf. 143 mk_state_pc ?? 144 (pointer_of_block_and_lin_offset (pblock (pc ? s)) … 145 (sigma_pc_of_status … sigma … prf)). 146 [2: cases (pc ??) * normalize // 147  cases daemon (* TODO *) ] 148 qed. 149 150 axiom sigma_pc_commute: 151 ∀p,p',graph_prog,s1,prf. 152 sigma_pc_of_status p p' graph_prog (choose_sigma p p' graph_prog) s1 prf = 153 point_of_pointer (lin_prog_params p p' (linearise p graph_prog)) 154 (lin_prog_params p p' (linearise p graph_prog)) 155 (pc (lin_prog_params p p' (linearise p graph_prog)) 156 (linearise_status_fun p p' graph_prog (choose_sigma p p' graph_prog) s1 prf)). 157 158 definition linearise_status_rel: 159 ∀p,p',graph_prog. 160 ∀sigma: identifier LabelTag → option ℕ. 161 let lin_prog ≝ linearise ? graph_prog in 162 status_rel 163 (graph_abstract_status p p' graph_prog) 164 (lin_abstract_status p p' lin_prog) 165 ≝ λp,p',graph_prog,sigma.mk_status_rel … 166 (λs1,s2. 167 ∃prf: well_formed_status … sigma s1. 168 s2 = linearise_status_fun p p' graph_prog sigma s1 prf) …. 169 cases daemon (* TODO *) 170 qed. 151 171 152 172 axiom fetch_function_sigma_commute: … … 196 216 whd in match (stmt_at ????); 197 217 whd in match (stmt_at ????); 198 199 ================================ 200 normalize nodelta 218 cases (linearise_code_spec … p' graph_prog graph_fun 219 (joint_if_entry … graph_fun)) 220 * #lin_code_closed #sigma_entry_is_zero #sigma_spec 221 lapply (sigma_spec 222 (point_of_pointer ? (graph_prog_params … p' graph_prog) (pc … s1))) 223 sigma_spec #sigma_spec cases (sigma_spec ??) [3: @(sigma_pc_of_status_ok … prf) 2: skip ] 224 sigma_spec #graph_stmt * #graph_lookup_ok >graph_lookup_ok graph_lookup_ok 225 whd in ⊢ (? → ???%); #sigma_spec whd in sigma_spec; 226 inversion (nth_opt ???) in sigma_spec; [ #H whd in ⊢ (% → ?); #abs cases abs ] 227 * #optlabel #lin_stm #lin_lookup_ok whd in ⊢ (% → ?); ** #_ 228 #related_lin_stm_graph_stm #_ <related_lin_stm_graph_stm related_lin_stm_graph_stm 229 <sigma_pc_commute >lin_lookup_ok // 230 qed. 201 231 202 232 lemma fetch_statement_sigma_commute: 203 ∀p,p',graph_prog,sigma,st1. 233 ∀p,p',graph_prog,st1. 234 let sigma ≝ choose_sigma p p' graph_prog in 204 235 let lin_prog ≝ linearise ? graph_prog in 236 ∀prf. 205 237 fetch_statement 206 238 (lin_prog_params p p' lin_prog) … … 209 241 (ev_genv (lin_prog_params p p' lin_prog)) 210 242 (pc (lin_prog_params p p' lin_prog) 211 (linearise_status_fun p p' graph_prog sigma st1 ))243 (linearise_status_fun p p' graph_prog sigma st1 prf)) 212 244 = 213 245 m_map … … … 221 253 (ev_genv (graph_prog_params p p' graph_prog)) 222 254 (pc (graph_prog_params p p' graph_prog) st1)). 223 #p #p' #graph_prog #s igma #s1255 #p #p' #graph_prog #s1 #prf 224 256 whd in match fetch_statement; normalize nodelta 225 257 >fetch_function_sigma_commute … … 227 259 #graph_fun whd in ⊢ (??%%); 228 260 whd in ⊢ (???(match % with [ _ ⇒ ?  _ ⇒ ?])); 229 >stm_at_sigma_commute 230 cases (stmt_at ????) // 261 >stm_at_sigma_commute cases (stmt_at ????) // 231 262 qed. 232 263 … … 243 274 cases cl in classified_st1_cl; cl #classified_st1_cl whd 244 275 [4: 245 whd in rel_st1_st2;>rel_st1_st2 st2276 cases rel_st1_st2 rel_st1_st2 #wf_st1 #rel_st1_st2 >rel_st1_st2 st2 246 277 whd in move_st1_st1'; 247 278 letin lin_prog ≝ (linearise ? graph_prog) 248 279 letin st2' ≝ (eval_state (globals (lin_prog_params p p' lin_prog)) … 249 280 (ev_genv (lin_prog_params p p' lin_prog)) 250 (linearise_status_fun … sigma st1 ))281 (linearise_status_fun … sigma st1 wf_st1)) 251 282 whd in st2'; 252 283 whd in match (fetch_statement ?????) in st2';
Note: See TracChangeset
for help on using the changeset viewer.