Changeset 2548
 Timestamp:
 Dec 10, 2012, 2:33:40 PM (7 years ago)
 Location:
 src
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

src/common/BackEndOps.ma
r2462 r2548 221 221 ] 222 222  BVnull p1 ⇒ 223 match opwith224 [ Xor⇒225 match a2with226 [ BVptr ptr2 p2⇒223 match a2 with 224 [ BVptr ptr2 p2 ⇒ 225 match op with 226 [ Xor ⇒ 227 227 if eqb p1 p2 then 228 228 return 〈BVXor (None ?) (Some ? ptr2) p1, carry〉 229 229 else 230 230 Error … [MSG UnsupportedOp] 231  BVnull p2 ⇒ 231  _ ⇒ Error … [MSG UnsupportedOp] 232 ] 233  BVnull p2 ⇒ 234 match op with 235 [ Xor ⇒ 232 236 if eqb p1 p2 then 233 237 return 〈BVXor (None ?) (None ?) p1, carry〉 … … 239 243 ] 240 244  BVXor ptr1_opt ptr1_opt' p1 ⇒ 241 match opwith242 [ Or⇒243 match a2with244 [ BVByte b2⇒245 match a2 with 246 [ BVByte b2 ⇒ 247 match op with 248 [ Or ⇒ 245 249 if eq_bv … (bv_zero …) b2 then return 〈a1, carry〉 246 250 else Error … [MSG UnsupportedOp] 247  BVnonzero ⇒ return 〈BVnonzero, carry〉 248  BVXor ptr2_opt ptr2_opt' p2 ⇒ 251  _ ⇒ Error … [MSG UnsupportedOp] 252 ] 253  BVnonzero ⇒ 254 match op with 255 [ Or ⇒ 256 return 〈BVnonzero, carry〉 257  _ ⇒ Error … [MSG UnsupportedOp] 258 ] 259  BVXor ptr2_opt ptr2_opt' p2 ⇒ 260 match op with 261 [ Or ⇒ 249 262 if ((eqb p1 0 ∧ eqb p2 1) ∨ (eqb p1 1 ∧ eqb p2 0)) then 250 263 let eq_at ≝ λp,ptr1,ptr2. … … 262 275 ] 263 276  BVnonzero ⇒ 264 match op with 265 [ Or ⇒ 266 match a2 with 267 [ BVByte _ ⇒ return 〈BVnonzero, carry〉 268  BVnonzero ⇒ return 〈BVnonzero, carry〉 269  BVXor _ _ _ ⇒ return 〈BVnonzero, carry〉 277 match a2 with 278 [ BVByte _ ⇒ 279 match op with 280 [ Or ⇒ return 〈BVnonzero, carry〉 281  _ ⇒ Error … [MSG UnsupportedOp] 282 ] 283  BVnonzero ⇒ 284 match op with 285 [ Or ⇒ return 〈BVnonzero, carry〉 286  _ ⇒ Error … [MSG UnsupportedOp] 287 ] 288  BVXor _ _ _ ⇒ 289 match op with 290 [ Or ⇒ return 〈BVnonzero, carry〉 270 291  _ ⇒ Error … [MSG UnsupportedOp] 271 292 ] 
src/joint/lineariseProof.ma
r2547 r2548 1221 1221 normalize // 1222 1222 qed. 1223 1223 check pc_of_label 1224 1224 lemma fetch_statement_sigma_commute: 1225 1225 ∀p,p',graph_prog,pc,f,fn,stmt. … … 1229 1229 fetch_statement (make_sem_graph_params p p') … 1230 1230 (globalenv_noinit ? graph_prog) pc = return 〈f, fn,stmt〉 → 1231 All ? (λlbl.well_formed_pc p p' graph_prog sigma 1232 (pc_of_point (make_sem_graph_params p p') (pc_block pc) lbl)) 1233 (stmt_labels … stmt) ∧ 1231 All ? (λlbl.∃prf:well_formed_pc p p' graph_prog sigma 1232 (pc_of_point (make_sem_graph_params p p') (pc_block pc) lbl). 1233 pc_of_label (make_sem_lin_params p p') … 1234 (globalenv_noinit … lin_prog) 1235 (pc_block pc) 1236 lbl = return sigma_pc … prf) 1237 (stmt_explicit_labels … stmt) ∧ 1234 1238 match stmt with 1235 1239 [ sequential s nxt ⇒ … … 1241 1245 sequential (mk_lin_params p) … (step_seq … x ) it〉 ∧ 1242 1246 ∃prf'. 1247 let sigma_nxt ≝ sigma_pc p p' graph_prog sigma (succ_pc (make_sem_graph_params p p') pc nxt) prf' in 1243 1248 let nxt_pc ≝ succ_pc (make_sem_lin_params p p') (sigma_pc … pc prf) it in 1249 (nxt_pc = sigma_nxt ∨ 1250 (fetch_statement (make_sem_lin_params p p') … 1251 (globalenv_noinit … lin_prog) nxt_pc = 1252 return 〈f, \fst (linearise_int_fun … fn), 1253 final (mk_lin_params p) … (GOTO … nxt)〉 ∧ 1254 (pc_of_label (make_sem_lin_params p p') … 1255 (globalenv_noinit … lin_prog) 1256 (pc_block pc) 1257 nxt = return sigma_nxt))) 1258  COND a ltrue ⇒ 1259 ∃prf'. 1244 1260 let sigma_nxt ≝ sigma_pc p p' graph_prog sigma (succ_pc (make_sem_graph_params p p') pc nxt) prf' in 1245 (nxt_pc = sigma_nxt ∨ fetch_statement (make_sem_lin_params p p') … 1246 (globalenv_noinit … lin_prog) nxt_pc = 1247 return 〈f, \fst (linearise_int_fun … fn), final (mk_lin_params p) … (GOTO … nxt)〉) 1248  COND a ltrue ⇒ 1249 (∃ prf'. 1250 let nxt_pc ≝ succ_pc (make_sem_lin_params p p') (sigma_pc … pc prf) it in 1251 let sigma_nxt ≝ sigma_pc p p' graph_prog sigma (succ_pc (make_sem_graph_params p p') pc nxt) prf' in 1261 (let nxt_pc ≝ succ_pc (make_sem_lin_params p p') (sigma_pc … pc prf) it in 1252 1262 (fetch_statement (make_sem_lin_params p p') … 1253 1263 (globalenv_noinit … lin_prog) (sigma_pc … pc prf) = 1254 1264 return 〈f, \fst (linearise_int_fun … fn), 1255 1265 sequential (mk_lin_params p) … (COND … a ltrue) it〉 ∧ 1256 nxt_pc = sigma_nxt)) ∨ 1257 1266 nxt_pc = sigma_nxt)) ∨ 1267 (fetch_statement (make_sem_lin_params p p') … (globalenv_noinit … lin_prog) (sigma_pc … pc prf) 1258 1268 = 1259 return 〈f, \fst (linearise_int_fun … fn), FCOND (mk_lin_params p) … I a ltrue nxt〉 1269 return 〈f, \fst (linearise_int_fun … fn), FCOND (mk_lin_params p) … I a ltrue nxt〉 ∧ 1270 pc_of_label (make_sem_lin_params p p') … 1271 (globalenv_noinit … lin_prog) 1272 (pc_block pc) 1273 nxt = return sigma_nxt) 1260 1274 ] 1261 1275  final z ⇒ fetch_statement (make_sem_lin_params p p') … … … 1277 1291 lapply(stmt_at_sigma_commute ???????? (good graph_fun) ?? graph_stmt) 1278 1292 [@lin_pt_spec] * #H1 #H2 % 1279 [ H2 @(All_mp … H1) #lab #lab_spec1293 [ H2 @(All_mp … (All_append_r H1) #lab #lab_spec 1280 1294 whd in match well_formed_pc; normalize nodelta 1281 1295 whd in match sigma_pc_opt; normalize nodelta >fetchfn … … 1409 1423 @opt_safe_elim H 1410 1424 #res #_ 1411 #H 1425 #H cases daemon (* 1412 1426 #H @('bind_inversion H) H 1413 1427 * #f #stmt … … 1461 1475 1462 1476 xxxxxxxxxxxxxx 1463 1477 *) 1464 1478 qed. 1465 1479 … … 1899 1913 qed. 1900 1914 1915 lemma eval_seq_no_call_no_goto : 1916 ∀p,p',graph_prog. 1917 let lin_prog ≝ linearise p graph_prog in 1918 ∀stack_sizes. 1919 ∀sigma.∀gss : good_state_sigma p p' graph_prog sigma. 1920 ∀st,st',f,fn,stmt,nxt.no_call ?? stmt → 1921 ∀prf : well_formed_state_pc … gss st. 1922 fetch_statement (make_sem_lin_params p p') … 1923 (globalenv_noinit ? lin_prog) (pc … (sigma_state_pc … st prf)) = 1924 return 〈f, \fst (linearise_int_fun … fn), 1925 sequential … (step_seq (mk_lin_params p) … stmt) it〉 → 1926 eval_seq_no_pc … (ev_genv … (graph_prog_params … graph_prog stack_sizes)) 1927 f fn stmt st = return st' → 1928 let st_pc' ≝ mk_state_pc ? st' 1929 (succ_pc (make_sem_graph_params p p') … 1930 (pc … st) nxt) in 1931 ∀prf'. 1932 succ_pc (make_sem_lin_params p p') (sigma_pc … (pc … st) (proj1 … prf)) it = 1933 sigma_pc p p' graph_prog sigma 1934 (succ_pc (make_sem_graph_params p p') (pc … st) nxt) prf' → 1935 ∃prf''. 1936 ∃taf : trace_any_any_free (lin_abstract_status p p' lin_prog stack_sizes) 1937 (sigma_state_pc … gss st prf) 1938 (sigma_state_pc … gss st_pc' prf''). 1939 bool_to_Prop (taaf_non_empty … taf). 1940 #p #p' #graph_prog #stack_sizes #sigma #gss #st #st' #f #fn #stmt #nxt #stmt_no_call 1941 #prf #EQfetch' #EQeval #prf' #EQsucc_pc 1942 cases (eval_seq_no_pc_sigma_commute … gss … EQeval) [2: @(proj2 … prf)] 1943 #prf'' #EQeval' 1944 % [ @hide_prf % assumption ] 1945 %{(taaf_step … (taa_base …) …)} [3: % ] 1946 [ whd whd in ⊢ (??%?); >EQfetch' normalize nodelta 1947 whd in match joint_classify_step; normalize nodelta 1948 @no_call_other assumption 1949  whd whd in match eval_state; normalize nodelta >EQfetch' >m_return_bind 1950 whd in match eval_statement_no_pc; normalize nodelta 1951 >EQeval' >m_return_bind 1952 whd in match eval_statement_advance; normalize nodelta 1953 >no_call_advance [2: assumption ] 1954 whd in match (next ???); 1955 >EQsucc_pc % 1956 ] 1957 qed. 1958 1959 lemma eval_seq_no_call_goto : 1960 ∀p,p',graph_prog. 1961 let lin_prog ≝ linearise p graph_prog in 1962 ∀stack_sizes. 1963 ∀sigma.∀gss : good_state_sigma p p' graph_prog sigma. 1964 ∀st,st',f,fn,stmt,nxt.no_call ?? stmt → 1965 ∀prf : well_formed_state_pc … gss st. 1966 fetch_statement (make_sem_lin_params p p') … 1967 (globalenv_noinit ? lin_prog) (pc … (sigma_state_pc … st prf)) = 1968 return 〈f, \fst (linearise_int_fun … fn), 1969 sequential … (step_seq (mk_lin_params p) … stmt) it〉 → 1970 eval_seq_no_pc … (ev_genv … (graph_prog_params … graph_prog stack_sizes)) 1971 f fn stmt st = return st' → 1972 let st_pc' ≝ mk_state_pc ? st' 1973 (succ_pc (make_sem_graph_params p p') … 1974 (pc … st) nxt) in 1975 (? : Prop) → 1976 fetch_statement (make_sem_lin_params p p') … 1977 (globalenv_noinit … lin_prog) 1978 (succ_pc (make_sem_lin_params p p') (sigma_pc … (pc … st) (proj1 … prf)) it) = 1979 return 〈f, \fst (linearise_int_fun … fn), final (mk_lin_params p) … (GOTO … nxt)〉 → 1980 ∃prf''. 1981 ∃taf : trace_any_any_free (lin_abstract_status p p' lin_prog stack_sizes) 1982 (sigma_state_pc … gss st prf) 1983 (sigma_state_pc … gss st_pc' prf''). 1984 bool_to_Prop (taaf_non_empty … taf). 1985 #p #p' #graph_prog #stack_sizes #sigma #gss #st #st' #f #fn #stmt #nxt #stmt_no_call 1986 #prf #EQfetch' #EQeval #prf' #EQsucc_pc 1987 cases (eval_seq_no_pc_sigma_commute … gss … EQeval) [2: @(proj2 … prf)] 1988 #prf'' #EQeval' 1989 % [ @hide_prf % assumption ] 1990 %{(taaf_step … (taa_base …) …)} [3: % ] 1991 [ whd whd in ⊢ (??%?); >EQfetch' normalize nodelta 1992 whd in match joint_classify_step; normalize nodelta 1993 @no_call_other assumption 1994  whd whd in match eval_state; normalize nodelta >EQfetch' >m_return_bind 1995 whd in match eval_statement_no_pc; normalize nodelta 1996 >EQeval' >m_return_bind 1997 whd in match eval_statement_advance; normalize nodelta 1998 >no_call_advance [2: assumption ] 1999 whd in match (next ???); 2000 >EQsucc_pc % 2001 ] 2002 qed. 2003 2004 2005 2006 2007 [ assumption 2008  assu 2009 2010 fetch_statement (make_sem_lin_params p p') … 2011 (globalenv_noinit … lin_prog) (sigma_pc … pc prf) = 2012 return 〈f, \fst (linearise_int_fun … fn), 2013 sequential (mk_lin_params p) … (step_seq … x ) it〉 ∧ 2014 ∃prf'. 2015 let nxt_pc ≝ in 2016 let sigma_nxt ≝ in 2017 (nxt_pc = sigma_nxt ∨ fetch_statement (make_sem_lin_params p p') … 2018 (globalenv_noinit … lin_prog) nxt_pc = 2019 return 〈f, \fst (linearise_int_fun … fn), final (mk_lin_params p) … (GOTO … nxt)〉) 2020 1901 2021 inductive ex_Type1 (A:Type[1]) (P:A → Prop) : Prop ≝ 1902 2022 ex1_intro: ∀ x:A. P x → ex_Type1 A P.
Note: See TracChangeset
for help on using the changeset viewer.