Changeset 2445
 Timestamp:
 Nov 9, 2012, 11:47:57 AM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/joint/lineariseProof.ma
r2443 r2445 18 18 include "joint/SemanticUtils.ma". 19 19 20 definition graph_prog_params: 21 ∀p:unserialized_params. 22 (∀F.sem_unserialized_params p F) → 23 joint_program (mk_graph_params p) → 24 prog_params 25 ≝ 26 λp,p',prog. 27 (mk_prog_params 28 (make_sem_graph_params (mk_graph_params p) p') 29 prog). 30 31 definition lin_prog_params: 32 ∀p:unserialized_params. 33 (∀F.sem_unserialized_params p F) → 34 joint_program (mk_lin_params p) → 35 prog_params 36 ≝ 37 λp,p',prog. 38 (mk_prog_params 39 (make_sem_lin_params (mk_lin_params p) p') 40 prog). 41 20 42 definition graph_abstract_status: 21 43 ∀p:unserialized_params. … … 25 47 ≝ 26 48 λp,p',prog. 27 joint_abstract_status 28 (mk_prog_params 29 (make_sem_graph_params p p') 30 prog). 49 joint_abstract_status (graph_prog_params p p' prog). 31 50 32 51 definition lin_abstract_status: … … 37 56 ≝ 38 57 λp,p',prog. 39 joint_abstract_status 40 (mk_prog_params 41 (make_sem_lin_params p p') 42 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 → Prop 70 ≝ 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 with 85 [ 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 in 94 ∀s:graph_abstract_status p p' graph_prog. 95 well_formed_status … sigma s → 96 lin_abstract_status p p' lin_prog 97 ≝ 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. 43 105 44 106 definition linearise_status_rel: 45 107 ∀p,p',graph_prog. 108 ∀sigma: identifier LabelTag → option ℕ. 46 109 let lin_prog ≝ linearise ? graph_prog in 47 110 status_rel 48 111 (graph_abstract_status p p' graph_prog) 49 (lin_abstract_status p p' lin_prog). 50 cases daemon 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 120 (*CSC: Paolo, come to the rescue*) 121 axiom choose_sigma: 122 ∀p:unserialized_params. 123 (∀F.sem_unserialized_params p F) → 124 joint_program (mk_graph_params p) → 125 identifier LabelTag → option ℕ. 126 127 (*CSC: Paolo, come to the rescue*) 128 axiom linearise_code_spec: 129 ∀p : unserialized_params. 130 ∀p':(∀F.sem_unserialized_params p F). 131 ∀graph_prog:joint_program (mk_graph_params p). 132 ∀graph_fun:joint_closed_internal_function (mk_graph_params p) 133 (globals (graph_prog_params p p' graph_prog)). 134 let sigma ≝ choose_sigma p p' graph_prog in 135 let lin_fun ≝ linearise_int_fun … graph_fun in 136 let g ≝ joint_if_code ?? (pi1 … graph_fun) in 137 let c ≝ joint_if_code ?? (pi1 … lin_fun) in 138 ∀entry : (Σl.bool_to_Prop (code_has_label … g l)). 139 code_closed … c ∧ 140 sigma entry = Some ? 0 ∧ 141 ∀l,n.sigma l = Some ? n → 142 ∃s. lookup … g l = Some ? s ∧ 143 opt_Exists ? 144 (λls.let 〈lopt, ts〉 ≝ ls in 145 opt_All ? (eq ? l) lopt ∧ 146 ts = graph_to_lin_statement … s ∧ 147 opt_All ? 148 (λnext.Or (sigma next = Some ? (S n)) 149 (nth_opt … (S n) c = Some ? 〈None ?, GOTO … next〉)) 150 (stmt_implicit_label … s)) (nth_opt … n c). 151 152 axiom fetch_function_sigma_commute: 153 ∀p,p',graph_prog,sigma,st1. 154 ∀prf:well_formed_status ??? sigma st1. 155 let lin_prog ≝ linearise ? graph_prog in 156 fetch_function 157 (lin_prog_params p p' lin_prog) 158 (globals (lin_prog_params p p' lin_prog)) 159 (ev_genv (lin_prog_params p p' lin_prog)) 160 (pc (lin_prog_params p p' lin_prog) 161 (linearise_status_fun p p' graph_prog sigma st1 prf)) 162 = 163 m_map … 164 (linearise_int_fun ??) 165 (fetch_function 166 (graph_prog_params p p' graph_prog) 167 (globals (graph_prog_params p p' graph_prog)) 168 (ev_genv (graph_prog_params p p' graph_prog)) 169 (pc (graph_prog_params p p' graph_prog) st1)). 170 171 lemma stm_at_sigma_commute: 172 ∀p,p',graph_prog,graph_fun,s1. 173 let lin_prog ≝ linearise ? graph_prog in 174 let sigma ≝ choose_sigma p p' graph_prog in 175 ∀prf:well_formed_status ??? sigma s1. 176 stmt_at (lin_prog_params p p' (linearise p graph_prog)) 177 (globals (lin_prog_params p p' (linearise p graph_prog))) 178 (joint_if_code (lin_prog_params p p' (linearise p graph_prog)) 179 (globals (lin_prog_params p p' (linearise p graph_prog))) 180 (linearise_int_fun p (globals (graph_prog_params p p' graph_prog)) graph_fun)) 181 (point_of_pointer (lin_prog_params p p' (linearise p graph_prog)) 182 (lin_prog_params p p' (linearise p graph_prog)) 183 (pc (lin_prog_params p p' (linearise p graph_prog)) 184 (linearise_status_fun p p' graph_prog sigma s1 prf))) 185 = 186 option_map … 187 (graph_to_lin_statement …) 188 (stmt_at (graph_prog_params p p' graph_prog) 189 (globals (graph_prog_params p p' graph_prog)) 190 (joint_if_code (graph_prog_params p p' graph_prog) 191 (globals (graph_prog_params p p' graph_prog)) graph_fun) 192 (point_of_pointer (graph_prog_params p p' graph_prog) 193 (graph_prog_params p p' graph_prog) 194 (pc (graph_prog_params p p' graph_prog) s1))). 195 #p #p' #graph_prog #graph_fun #s1 #prf 196 whd in match (stmt_at ????); 197 whd in match (stmt_at ????); 198 199 ================================ 200 normalize nodelta 201 202 lemma fetch_statement_sigma_commute: 203 ∀p,p',graph_prog,sigma,st1. 204 let lin_prog ≝ linearise ? graph_prog in 205 fetch_statement 206 (lin_prog_params p p' lin_prog) 207 (lin_prog_params p p' lin_prog) 208 (globals (lin_prog_params p p' lin_prog)) 209 (ev_genv (lin_prog_params p p' lin_prog)) 210 (pc (lin_prog_params p p' lin_prog) 211 (linearise_status_fun p p' graph_prog sigma st1)) 212 = 213 m_map … 214 (λfun_stm. 215 let 〈fun,stm〉 ≝ fun_stm in 216 〈linearise_int_fun ?? fun, graph_to_lin_statement ?? stm〉) 217 (fetch_statement 218 (graph_prog_params p p' graph_prog) 219 (graph_prog_params p p' graph_prog) 220 (globals (graph_prog_params p p' graph_prog)) 221 (ev_genv (graph_prog_params p p' graph_prog)) 222 (pc (graph_prog_params p p' graph_prog) st1)). 223 #p #p' #graph_prog #sigma #s1 224 whd in match fetch_statement; normalize nodelta 225 >fetch_function_sigma_commute 226 cases (fetch_function ????) [2://] 227 #graph_fun whd in ⊢ (??%%); 228 whd in ⊢ (???(match % with [ _ ⇒ ?  _ ⇒ ?])); 229 >stm_at_sigma_commute 230 cases (stmt_at ????) // 51 231 qed. 52 232 … … 57 237 (graph_abstract_status p p' graph_prog) 58 238 (lin_abstract_status p p' lin_prog) ≝ 59 λp,p',graph_prog. mk_status_simulation … (linearise_status_rel p p' graph_prog) …. 60 cases daemon 61 qed. 239 λp,p',graph_prog. 240 let sigma ≝ choose_sigma p p' graph_prog in 241 mk_status_simulation … (linearise_status_rel p p' graph_prog sigma) …. 242 #st1 #cl #st1' #st2 #move_st1_st1' #rel_st1_st2 #classified_st1_cl 243 cases cl in classified_st1_cl; cl #classified_st1_cl whd 244 [4: 245 whd in rel_st1_st2; >rel_st1_st2 st2 246 whd in move_st1_st1'; 247 letin lin_prog ≝ (linearise ? graph_prog) 248 letin st2' ≝ (eval_state (globals (lin_prog_params p p' lin_prog)) … 249 (ev_genv (lin_prog_params p p' lin_prog)) 250 (linearise_status_fun … sigma st1)) 251 whd in st2'; 252 whd in match (fetch_statement ?????) in st2'; 253 >fetch_function_sigma_commute in st2'; 254 whd in match (fetch_function ????) in st2'; 255 XXX 256 check fetch_statement 257 CSC 258 %{} 259 260 whd in classified_st1_cl; 261 whd in classified_st1_cl:(??%?); 262 inversion (fetch_statement ?????) in classified_st1_cl; 263 264 <classified_st1_cl cl 265 whd in ⊢ (match % with [_ ⇒ ?  _ ⇒ ?  _ ⇒ ?  _ ⇒ ? ] ?); 266 inversion (fetch_statement ?????) 267 268 inversion (fetch_statement ?????) 269 qed.
Note: See TracChangeset
for help on using the changeset viewer.