Ignore:
Timestamp:
Jul 23, 2012, 7:31:11 PM (7 years ago)
Author:
garnier
Message:

Progress on proving semantics preservation under memory injections.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/switchRemoval.ma

    r2227 r2234  
    1  include "Clight/Csyntax.ma".
     1include "Clight/Csyntax.ma".
    22include "Clight/fresh.ma".
    33include "basics/lists/list.ma".
     
    13111311     %{p2} @conj try @refl try assumption
    13121312] qed.
     1313
     1314(* A cleaner version of inversion for [value_eq] *)
     1315lemma value_eq_inversion :
     1316  ∀E,v1,v2. ∀P : val → val → Prop. value_eq E v1 v2 →
     1317  (∀v. P Vundef v) →
     1318  (∀sz,i. P (Vint sz i) (Vint sz i)) →
     1319  (∀f. P (Vfloat f) (Vfloat f)) →
     1320  (P Vnull Vnull) →
     1321  (∀p1,p2. pointer_translation p1 E = Some ? p2 → P (Vptr p1) (Vptr p2)) →
     1322  P v1 v2.
     1323#E #v1 #v2 #P #Heq #H1 #H2 #H3 #H4 #H5
     1324inversion Heq
     1325[ 1: #v #Hv1 #Hv2 #_ destruct @H1
     1326| 2: #sz #i #Hv1 #Hv2 #_ destruct @H2
     1327| 3: #f #Hv1 #Hv2 #_ destruct @H3
     1328| 4: #Hv1 #Hv2 #_ destruct @H4
     1329| 5: #p1 #p2 #Hembed #Hv1 #Hv2 #_ destruct @H5 // ] qed.
    13131330 
    13141331(* If we succeed to load something by value from a 〈b,off〉 location,
     
    13181335    access_mode ty = By_value (typ_of_type ty) →
    13191336    load_value_of_type ty m b off = Some ? v →
    1320     Zltb (block_id b) (nextblock m) = true. (* → valid_block m b *)
    1321 #ty #m * #brg #bid #off #v whd in match (valid_block ??);
     1337    Zltb (block_id b) (nextblock m) = true.
     1338#ty #m * #brg #bid #off #v
    13221339cases ty
    13231340[ 1: | 2: #sz #sg | 3: #fsz | 4: #ptr_ty | 5: #array_ty #array_sz | 6: #domain #codomain
     
    13351352] qed.
    13361353
     1354(* If we succeed in loading some data from a location, then this loc is a valid pointer. *)
     1355lemma load_by_value_success_valid_ptr_aux :
     1356  ∀ty,m,b,off,v.
     1357    access_mode ty = By_value (typ_of_type ty) →
     1358    load_value_of_type ty m b off = Some ? v →
     1359    Zltb (block_id b) (nextblock m) = true ∧
     1360    Zleb (low_bound m b) (offv off) = true ∧
     1361    Zltb (offv off) (high_bound m b) = true.
     1362#ty #m * #brg #bid #off #v
     1363cases ty
     1364[ 1: | 2: #sz #sg | 3: #fsz | 4: #ptr_ty | 5: #array_ty #array_sz | 6: #domain #codomain
     1365| 7: #structname #fieldspec | 8: #unionname #fieldspec | 9: #id ]
     1366whd in match (load_value_of_type ????);
     1367[ 1,7,8: #_ #Habsurd destruct (Habsurd) ]
     1368#Hmode
     1369[ 1,2,3,6: [ 1: elim sz | 2: elim fsz ]
     1370     normalize in match (typesize ?);
     1371     whd in match (loadn ???);
     1372     whd in match (beloadv ??);
     1373     cases (Zltb bid (nextblock m)) normalize nodelta
     1374     cases (Zleb (low (blocks m (mk_block brg bid))) (offv off))
     1375     cases (Zleb (low (blocks m (mk_block brg bid))) (offv off))
     1376     cases (Zltb (offv off) (high (blocks m (mk_block brg bid)))) normalize nodelta
     1377     #Heq destruct (Heq)
     1378     try /3 by conj, refl/
     1379| *: normalize in Hmode; destruct (Hmode)
     1380] qed.
     1381
    13371382
    13381383lemma valid_block_from_bool : ∀b,m. Zltb (block_id b) (nextblock m) = true → valid_block m b.
     
    13511396#ty #m #b #off #v #Haccess_mode #Hload
    13521397@valid_block_from_bool
    1353 @(load_by_value_success_valid_block_aux ty m b off v Haccess_mode Hload)
    1354 qed.
     1398elim (load_by_value_success_valid_ptr_aux ty m b off v Haccess_mode Hload) * //
     1399qed.
     1400
     1401lemma load_by_value_success_valid_pointer :
     1402  ∀ty,m,b,off,v.
     1403    access_mode ty = By_value (typ_of_type ty) →
     1404    load_value_of_type ty m b off = Some ? v →
     1405    valid_pointer m (mk_pointer b off).
     1406#ty #m #b #off #v #Haccess_mode #Hload normalize
     1407elim (load_by_value_success_valid_ptr_aux ty m b off v Haccess_mode Hload)
     1408* #H1 #H2 #H3 >H1 >H2 normalize nodelta
     1409>Zle_to_Zleb_true try //
     1410lapply (Zlt_to_Zle … (Zltb_true_to_Zlt … H3)) /2/
     1411qed.
     1412
    13551413
    13561414(* Making explicit the contents of memory_inj for load_value_of_type *)
     
    21962254qed.
    21972255
    2198 (* A cleaner version of inversion for [value_eq] *)
    2199 lemma value_eq_inversion :
    2200   ∀E,v1,v2. ∀P : val → val → Prop. value_eq E v1 v2 →
    2201   (∀v. P Vundef v) →
    2202   (∀sz,i. P (Vint sz i) (Vint sz i)) →
    2203   (∀f. P (Vfloat f) (Vfloat f)) →
    2204   (P Vnull Vnull) →
    2205   (∀p1,p2. pointer_translation p1 E = Some ? p2 → P (Vptr p1) (Vptr p2)) →
    2206   P v1 v2.
    2207 #E #v1 #v2 #P #Heq #H1 #H2 #H3 #H4 #H5
    2208 inversion Heq
    2209 [ 1: #v #Hv1 #Hv2 #_ destruct @H1
    2210 | 2: #sz #i #Hv1 #Hv2 #_ destruct @H2
    2211 | 3: #f #Hv1 #Hv2 #_ destruct @H3
    2212 | 4: #Hv1 #Hv2 #_ destruct @H4
    2213 | 5: #p1 #p2 #Hembed #Hv1 #Hv2 #_ destruct @H5 // ] qed.
    22142256
    22152257(* value_eq lifts to addition *)
    22162258lemma add_value_eq :
    2217   ∀E,v1,v2,v1',v2',ty1,ty2,m1,m2.
     2259  ∀E,v1,v2,v1',v2',ty1,ty2.
    22182260   value_eq E v1 v2 →
    22192261   value_eq E v1' v2' →
    2220    memory_inj E m1 m2 → (* This injection seems useless TODO *)
     2262   (* memory_inj E m1 m2 → This injection seems useless TODO *)
    22212263   ∀r1. (sem_add v1 ty1 v1' ty2=Some val r1→
    22222264           ∃r2:val.sem_add v2 ty1 v2' ty2=Some val r2∧value_eq E r1 r2).
    2223 #E #v1 #v2 #v1' #v2' #ty1 #ty2 #m1 #m2 #Hvalue_eq1 #Hvalue_eq2 #Hinj #r1
     2265#E #v1 #v2 #v1' #v2' #ty1 #ty2 #Hvalue_eq1 #Hvalue_eq2 #r1
    22242266@(value_eq_inversion E … Hvalue_eq1)
    22252267[ 1: #v | 2: #sz #i | 3: #f | 4: | 5: #p1 #p2 #Hembed ]
     
    22922334     ]
    22932335] qed.
    2294          
    2295 (* TODO all other 10 binary operations. Then wrap this in [binary_operation_value_eq] *)
    2296 
    2297 
     2336
     2337(* Offset subtraction is invariant by translation *)
     2338lemma sub_offset_translation :
     2339 ∀n,x,y,delta. sub_offset n x y = sub_offset n (offset_plus x delta) (offset_plus y delta).
     2340#n #x #y #delta
     2341whd in match (sub_offset ???) in ⊢ (??%%);
     2342elim x #x' elim y #y' elim delta #delta'
     2343normalize in match (offset_plus ??);
     2344normalize in match (offset_plus ??);
     2345cut ((x' - y') = (x'+delta'-(y'+delta')))
     2346[ whd in match (Zminus ??) in ⊢ (??%%);
     2347  >(Zopp_Zplus y' delta') <associative_Zplus /2/ ]
     2348#Heq >Heq @refl
     2349qed.   
     2350
     2351(* value_eq lifts to addition *)
     2352lemma sub_value_eq :
     2353  ∀E,v1,v2,v1',v2',ty1,ty2.
     2354   value_eq E v1 v2 →
     2355   value_eq E v1' v2' →
     2356   ∀r1. (sem_sub v1 ty1 v1' ty2=Some val r1→
     2357           ∃r2:val.sem_sub v2 ty1 v2' ty2=Some val r2∧value_eq E r1 r2).
     2358#E #v1 #v2 #v1' #v2' #ty1 #ty2 #Hvalue_eq1 #Hvalue_eq2 #r1
     2359@(value_eq_inversion E … Hvalue_eq1)
     2360[ 1: #v | 2: #sz #i | 3: #f | 4: | 5: #p1 #p2 #Hembed ]
     2361[ 1: whd in match (sem_sub ????); normalize nodelta
     2362     cases (classify_sub ty1 ty2) normalize nodelta
     2363     [ 1: #sz #sg | 2: #fsz | 3: #n #ty #sz #sg | 4: #n #sz #sg #ty | 5: #ty1' #ty2' ]
     2364     #Habsurd destruct (Habsurd)
     2365| 2: whd in match (sem_sub ????); whd in match (sem_sub ????); normalize nodelta
     2366     cases (classify_sub ty1 ty2) normalize nodelta     
     2367     [ 1: #tsz #tsg | 2: #tfsz | 3: #tn #ty #tsz #tsg | 4: #tn #tsz #tsg #ty | 5: #ty1' #ty2' ]
     2368     [ 2,3,5: #Habsurd destruct (Habsurd) ]
     2369     @(value_eq_inversion E … Hvalue_eq2) normalize nodelta
     2370     [ 1,6: #v' | 2,7: #sz' #i' | 3,8: #f' | 4,9: | 5,10: #p1' #p2' #Hembed' ]
     2371     [ 1,2,4,5,6,7,8,9,10: #Habsurd destruct (Habsurd) ]
     2372     @intsize_eq_elim_elim
     2373      [ 1: #_ #Habsurd destruct (Habsurd)
     2374      | 2: #Heq destruct (Heq) normalize nodelta
     2375           #Heq destruct (Heq)
     2376          /3 by ex_intro, conj, vint_eq/           
     2377      ]
     2378| 3: whd in match (sem_sub ????); whd in match (sem_sub ????); normalize nodelta
     2379     cases (classify_sub ty1 ty2) normalize nodelta     
     2380     [ 1: #tsz #tsg | 2: #tfsz | 3: #tn #ty #tsz #tsg | 4: #tn #tsz #tsg #ty | 5: #ty1' #ty2' ]
     2381     [ 1,3,4,5: #Habsurd destruct (Habsurd) ]
     2382     @(value_eq_inversion E … Hvalue_eq2) normalize nodelta
     2383     [ 1: #v' | 2: #sz' #i' | 3: #f' | 4: | 5: #p1' #p2' #Hembed' ]
     2384     [ 1,2,4,5: #Habsurd destruct (Habsurd) ]
     2385     #Heq destruct (Heq)
     2386     /3 by ex_intro, conj, vfloat_eq/
     2387| 4: whd in match (sem_sub ????); whd in match (sem_sub ????); normalize nodelta
     2388     cases (classify_sub ty1 ty2) normalize nodelta
     2389     [ 1: #tsz #tsg | 2: #tfsz | 3: #tn #ty #tsz #tsg | 4: #tn #tsz #tsg #ty | 5: #ty1' #ty2' ]
     2390     [ 1,2,5: #Habsurd destruct (Habsurd) ]
     2391     @(value_eq_inversion E … Hvalue_eq2) normalize nodelta
     2392     [ 1,6: #v' | 2,7: #sz' #i' | 3,8: #f' | 4,9: | 5,10: #p1' #p2' #Hembed' ]
     2393     [ 1,2,4,5,6,7,9,10: #Habsurd destruct (Habsurd) ]         
     2394     [ 1: @eq_bv_elim [ 1: normalize nodelta #Heq1 #Heq2 destruct /3 by ex_intro, conj, vnull_eq/
     2395                      | 2: #_ normalize nodelta #Habsurd destruct (Habsurd) ]
     2396     | 2: #Heq destruct (Heq) /3 by ex_intro, conj, vnull_eq/ ]
     2397| 5: whd in match (sem_sub ????); whd in match (sem_sub ????); normalize nodelta
     2398     cases (classify_sub ty1 ty2) normalize nodelta
     2399     [ 1: #tsz #tsg | 2: #tfsz | 3: #tn #ty #tsz #tsg | 4: #tn #tsz #tsg #ty | 5: #ty1' #ty2' ]
     2400     [ 1,2,5: #Habsurd destruct (Habsurd) ]
     2401     @(value_eq_inversion E … Hvalue_eq2) normalize nodelta
     2402     [ 1,6: #v' | 2,7: #sz' #i' | 3,8: #f' | 4,9: | 5,10: #p1' #p2' #Hembed' ]
     2403     [ 1,2,4,5,6,7,8,9: #Habsurd destruct (Habsurd) ]
     2404     #Heq destruct (Heq)
     2405     [ 1: %{(Vptr (neg_shift_pointer_n (bitsize_of_intsize sz') p2 (sizeof ty) i'))} @conj try @refl
     2406          @vptr_eq whd in match (pointer_translation ??) in Hembed ⊢ %;
     2407          elim p1 in Hembed; #b1 #o1 normalize nodelta
     2408          cases (E b1)
     2409          [ 1: normalize in ⊢ (% → ?); #Habsurd destruct (Habsurd)
     2410          | 2: * #block #offset normalize nodelta #Heq destruct (Heq)
     2411               normalize >(sym_Zplus ? (offv offset)) <associative_Zplus >(sym_Zplus ? (offv offset))
     2412               @refl
     2413          ]
     2414     | 2: lapply Heq @eq_block_elim
     2415          [ 2: #_ normalize nodelta #Habsurd destruct (Habsurd)
     2416          | 1: #Hpblock1_eq normalize nodelta
     2417               elim p1 in Hpblock1_eq Hembed Hembed'; #b1 #off1
     2418               elim p1' #b1' #off1' whd in ⊢ (% → % → ?); #Hpblock1_eq destruct (Hpblock1_eq)
     2419               whd in ⊢ ((??%?) → (??%?) → ?);
     2420               cases (E b1') normalize nodelta
     2421               [ 1: #Habsurd destruct (Habsurd) ]
     2422               * #dest_block #dest_off normalize nodelta
     2423               #Heq_ptr1 #Heq_ptr2 destruct >eq_block_identity normalize nodelta
     2424               cases (eqb (sizeof tsg) O) normalize nodelta
     2425               [ 1: #Habsurd destruct (Habsurd)
     2426               | 2: >(sub_offset_translation 32 off1 off1' dest_off)
     2427                    cases (division_u 31
     2428                            (sub_offset 32 (offset_plus off1 dest_off) (offset_plus off1' dest_off))
     2429                            (repr (sizeof tsg)))
     2430                    [ 1: normalize nodelta #Habsurd destruct (Habsurd)
     2431                    | 2: #r1' normalize nodelta #Heq2 destruct (Heq2)
     2432                         /3 by ex_intro, conj, vint_eq/ ]
     2433    ] ] ]
     2434] qed.
     2435
     2436
     2437lemma mul_value_eq :
     2438  ∀E,v1,v2,v1',v2',ty1,ty2.
     2439   value_eq E v1 v2 →
     2440   value_eq E v1' v2' →
     2441   ∀r1. (sem_mul v1 ty1 v1' ty2=Some val r1→
     2442           ∃r2:val.sem_mul v2 ty1 v2' ty2=Some val r2∧value_eq E r1 r2).
     2443#E #v1 #v2 #v1' #v2' #ty1 #ty2 #Hvalue_eq1 #Hvalue_eq2 #r1
     2444@(value_eq_inversion E … Hvalue_eq1)
     2445[ 1: #v | 2: #sz #i | 3: #f | 4: | 5: #p1 #p2 #Hembed ]
     2446[ 1: whd in match (sem_mul ????); normalize nodelta
     2447     cases (classify_aop ty1 ty2) normalize nodelta
     2448     [ 1: #sz #sg | 2: #fsz | 3: #ty1' #ty2' ]
     2449     #Habsurd destruct (Habsurd)
     2450| 2: whd in match (sem_mul ????); whd in match (sem_mul ????); normalize nodelta
     2451     cases (classify_aop ty1 ty2) normalize nodelta
     2452     [ 1: #sz #sg | 2: #fsz | 3: #ty1' #ty2' ]
     2453     [ 2,3: #Habsurd destruct (Habsurd) ]
     2454     @(value_eq_inversion E … Hvalue_eq2) normalize nodelta
     2455     [ 1: #v' | 2: #sz' #i' | 3: #f' | 4: | 5: #p1' #p2' #Hembed' ]
     2456     [ 1,3,4,5: #Habsurd destruct (Habsurd) ]
     2457     @intsize_eq_elim_elim
     2458      [ 1: #_ #Habsurd destruct (Habsurd)
     2459      | 2: #Heq destruct (Heq) normalize nodelta
     2460           #Heq destruct (Heq)
     2461          /3 by ex_intro, conj, vint_eq/           
     2462      ]
     2463| 3: whd in match (sem_mul ????); whd in match (sem_mul ????); normalize nodelta
     2464     cases (classify_aop ty1 ty2) normalize nodelta
     2465     [ 1: #sz #sg | 2: #fsz | 3: #ty1' #ty2' ]
     2466     [ 1,3: #Habsurd destruct (Habsurd) ]
     2467     @(value_eq_inversion E … Hvalue_eq2) normalize nodelta     
     2468     [ 1: #v' | 2: #sz' #i' | 3: #f' | 4: | 5: #p1' #p2' #Hembed' ]
     2469     [ 1,2,4,5: #Habsurd destruct (Habsurd) ]
     2470     #Heq destruct (Heq)
     2471     /3 by ex_intro, conj, vfloat_eq/
     2472| 4: whd in match (sem_mul ????); whd in match (sem_mul ????); normalize nodelta
     2473     cases (classify_aop ty1 ty2) normalize nodelta
     2474     [ 1: #sz #sg | 2: #fsz | 3: #ty1' #ty2' ]
     2475     #Habsurd destruct (Habsurd)
     2476| 5: whd in match (sem_mul ????); whd in match (sem_mul ????); normalize nodelta
     2477     cases (classify_aop ty1 ty2) normalize nodelta
     2478     [ 1: #sz #sg | 2: #fsz | 3: #ty1' #ty2' ]     
     2479     #Habsurd destruct (Habsurd)
     2480] qed.
     2481
     2482lemma div_value_eq :
     2483  ∀E,v1,v2,v1',v2',ty1,ty2.
     2484   value_eq E v1 v2 →
     2485   value_eq E v1' v2' →
     2486   ∀r1. (sem_div v1 ty1 v1' ty2=Some val r1→
     2487           ∃r2:val.sem_div v2 ty1 v2' ty2=Some val r2∧value_eq E r1 r2).
     2488#E #v1 #v2 #v1' #v2' #ty1 #ty2 #Hvalue_eq1 #Hvalue_eq2 #r1
     2489@(value_eq_inversion E … Hvalue_eq1)
     2490[ 1: #v | 2: #sz #i | 3: #f | 4: | 5: #p1 #p2 #Hembed ]
     2491[ 1: whd in match (sem_div ????); normalize nodelta
     2492     cases (classify_aop ty1 ty2) normalize nodelta
     2493     [ 1: #sz #sg | 2: #fsz | 3: #ty1' #ty2' ]
     2494     #Habsurd destruct (Habsurd)
     2495| 2: whd in match (sem_div ????); whd in match (sem_div ????); normalize nodelta
     2496     cases (classify_aop ty1 ty2) normalize nodelta
     2497     [ 1: #sz #sg | 2: #fsz | 3: #ty1' #ty2' ]
     2498     [ 2,3: #Habsurd destruct (Habsurd) ]
     2499     @(value_eq_inversion E … Hvalue_eq2) normalize nodelta
     2500     [ 1: #v' | 2: #sz' #i' | 3: #f' | 4: | 5: #p1' #p2' #Hembed' ]
     2501     [ 1,3,4,5: #Habsurd destruct (Habsurd) ]
     2502     elim sg normalize nodelta
     2503     @intsize_eq_elim_elim
     2504     [ 1,3: #_ #Habsurd destruct (Habsurd)
     2505     | 2,4: #Heq destruct (Heq) normalize nodelta
     2506            @(match (division_s (bitsize_of_intsize sz') i i') with
     2507              [ None ⇒ ?
     2508              | Some bv' ⇒ ? ])
     2509            [ 1: normalize  #Habsurd destruct (Habsurd)
     2510            | 2: normalize #Heq destruct (Heq)
     2511                 /3 by ex_intro, conj, vint_eq/
     2512            | 3,4: elim sz' in i' i; #i' #i
     2513                   normalize in match (pred_size_intsize ?);
     2514                   generalize in match division_u; #division_u normalize
     2515                   @(match (division_u ???) with
     2516                    [ None ⇒ ?
     2517                    | Some bv ⇒ ?]) normalize nodelta
     2518                   #H destruct (H)
     2519                  /3 by ex_intro, conj, vint_eq/ ]
     2520     ]
     2521| 3: whd in match (sem_div ????); whd in match (sem_div ????); normalize nodelta
     2522     cases (classify_aop ty1 ty2) normalize nodelta
     2523     [ 1: #sz #sg | 2: #fsz | 3: #ty1' #ty2' ]
     2524     [ 1,3: #Habsurd destruct (Habsurd) ]
     2525     @(value_eq_inversion E … Hvalue_eq2) normalize nodelta     
     2526     [ 1: #v' | 2: #sz' #i' | 3: #f' | 4: | 5: #p1' #p2' #Hembed' ]
     2527     [ 1,2,4,5: #Habsurd destruct (Habsurd) ]
     2528     #Heq destruct (Heq)
     2529     /3 by ex_intro, conj, vfloat_eq/
     2530| 4: whd in match (sem_div ????); whd in match (sem_div ????); normalize nodelta
     2531     cases (classify_aop ty1 ty2) normalize nodelta
     2532     [ 1: #sz #sg | 2: #fsz | 3: #ty1' #ty2' ]
     2533     #Habsurd destruct (Habsurd)
     2534| 5: whd in match (sem_div ????); whd in match (sem_div ????); normalize nodelta
     2535     cases (classify_aop ty1 ty2) normalize nodelta
     2536     [ 1: #sz #sg | 2: #fsz | 3: #ty1' #ty2' ]     
     2537     #Habsurd destruct (Habsurd)
     2538] qed.
     2539
     2540lemma mod_value_eq :
     2541  ∀E,v1,v2,v1',v2',ty1,ty2.
     2542   value_eq E v1 v2 →
     2543   value_eq E v1' v2' →
     2544   ∀r1. (sem_mod v1 ty1 v1' ty2=Some val r1→
     2545           ∃r2:val.sem_mod v2 ty1 v2' ty2=Some val r2∧value_eq E r1 r2).
     2546#E #v1 #v2 #v1' #v2' #ty1 #ty2 #Hvalue_eq1 #Hvalue_eq2 #r1
     2547@(value_eq_inversion E … Hvalue_eq1)
     2548[ 1: #v | 2: #sz #i | 3: #f | 4: | 5: #p1 #p2 #Hembed ]
     2549[ 1: whd in match (sem_mod ????); normalize nodelta
     2550     cases (classify_aop ty1 ty2) normalize nodelta
     2551     [ 1: #sz #sg | 2: #fsz | 3: #ty1' #ty2' ]
     2552     #Habsurd destruct (Habsurd)
     2553| 2: whd in match (sem_mod ????); whd in match (sem_mod ????); normalize nodelta
     2554     cases (classify_aop ty1 ty2) normalize nodelta
     2555     [ 1: #sz #sg | 2: #fsz | 3: #ty1' #ty2' ]
     2556     [ 2,3: #Habsurd destruct (Habsurd) ]
     2557     @(value_eq_inversion E … Hvalue_eq2) normalize nodelta
     2558     [ 1: #v' | 2: #sz' #i' | 3: #f' | 4: | 5: #p1' #p2' #Hembed' ]
     2559     [ 1,3,4,5: #Habsurd destruct (Habsurd) ]
     2560     elim sg normalize nodelta
     2561     @intsize_eq_elim_elim
     2562     [ 1,3: #_ #Habsurd destruct (Habsurd)
     2563     | 2,4: #Heq destruct (Heq) normalize nodelta
     2564            @(match (modulus_s (bitsize_of_intsize sz') i i') with
     2565              [ None ⇒ ?
     2566              | Some bv' ⇒ ? ])
     2567            [ 1: normalize  #Habsurd destruct (Habsurd)
     2568            | 2: normalize #Heq destruct (Heq)
     2569                 /3 by ex_intro, conj, vint_eq/
     2570            | 3,4: elim sz' in i' i; #i' #i
     2571                   generalize in match modulus_u; #modulus_u normalize
     2572                   @(match (modulus_u ???) with
     2573                    [ None ⇒ ?
     2574                    | Some bv ⇒ ?]) normalize nodelta
     2575                   #H destruct (H)
     2576                  /3 by ex_intro, conj, vint_eq/ ]
     2577     ]
     2578| 3: whd in match (sem_mod ????); whd in match (sem_mod ????); normalize nodelta
     2579     cases (classify_aop ty1 ty2) normalize nodelta
     2580     [ 1: #sz #sg | 2: #fsz | 3: #ty1' #ty2' ]
     2581     #Habsurd destruct (Habsurd)
     2582| 4: whd in match (sem_mod ????); whd in match (sem_mod ????); normalize nodelta
     2583     cases (classify_aop ty1 ty2) normalize nodelta
     2584     [ 1: #sz #sg | 2: #fsz | 3: #ty1' #ty2' ]
     2585     #Habsurd destruct (Habsurd)
     2586| 5: whd in match (sem_mod ????); whd in match (sem_mod ????); normalize nodelta
     2587     cases (classify_aop ty1 ty2) normalize nodelta
     2588     [ 1: #sz #sg | 2: #fsz | 3: #ty1' #ty2' ]     
     2589     #Habsurd destruct (Habsurd)
     2590] qed.
     2591
     2592(* boolean ops *)
     2593lemma and_value_eq :
     2594  ∀E,v1,v2,v1',v2'.
     2595   value_eq E v1 v2 →
     2596   value_eq E v1' v2' →
     2597   ∀r1. (sem_and v1 v1'=Some val r1→
     2598           ∃r2:val.sem_and v2 v2'=Some val r2∧value_eq E r1 r2).
     2599#E #v1 #v2 #v1' #v2' #Hvalue_eq1 #Hvalue_eq2 #r1
     2600@(value_eq_inversion E … Hvalue_eq1)
     2601[ 2: #sz #i
     2602     @(value_eq_inversion E … Hvalue_eq2)
     2603     [ 2: #sz' #i' whd in match (sem_and ??);
     2604          @intsize_eq_elim_elim
     2605          [ 1: #_ #Habsurd destruct (Habsurd)
     2606          | 2: #Heq destruct (Heq) normalize nodelta
     2607               #Heq destruct (Heq) /3 by ex_intro,conj,vint_eq/ ]
     2608] ]
     2609normalize in match (sem_and ??); #arg1 destruct
     2610normalize in match (sem_and ??); #arg2 destruct
     2611normalize in match (sem_and ??); #arg3 destruct
     2612normalize in match (sem_and ??); #arg4 destruct
     2613qed.
     2614
     2615lemma or_value_eq :
     2616  ∀E,v1,v2,v1',v2'.
     2617   value_eq E v1 v2 →
     2618   value_eq E v1' v2' →
     2619   ∀r1. (sem_or v1 v1'=Some val r1→
     2620           ∃r2:val.sem_or v2 v2'=Some val r2∧value_eq E r1 r2).
     2621#E #v1 #v2 #v1' #v2' #Hvalue_eq1 #Hvalue_eq2 #r1
     2622@(value_eq_inversion E … Hvalue_eq1)
     2623[ 2: #sz #i
     2624     @(value_eq_inversion E … Hvalue_eq2)
     2625     [ 2: #sz' #i' whd in match (sem_or ??);
     2626          @intsize_eq_elim_elim
     2627          [ 1: #_ #Habsurd destruct (Habsurd)
     2628          | 2: #Heq destruct (Heq) normalize nodelta
     2629               #Heq destruct (Heq) /3 by ex_intro,conj,vint_eq/ ]
     2630] ]
     2631normalize in match (sem_or ??); #arg1 destruct
     2632normalize in match (sem_or ??); #arg2 destruct
     2633normalize in match (sem_or ??); #arg3 destruct
     2634normalize in match (sem_or ??); #arg4 destruct
     2635qed.
     2636
     2637lemma xor_value_eq :
     2638  ∀E,v1,v2,v1',v2'.
     2639   value_eq E v1 v2 →
     2640   value_eq E v1' v2' →
     2641   ∀r1. (sem_xor v1 v1'=Some val r1→
     2642           ∃r2:val.sem_xor v2 v2'=Some val r2∧value_eq E r1 r2).
     2643#E #v1 #v2 #v1' #v2' #Hvalue_eq1 #Hvalue_eq2 #r1
     2644@(value_eq_inversion E … Hvalue_eq1)
     2645[ 2: #sz #i
     2646     @(value_eq_inversion E … Hvalue_eq2)
     2647     [ 2: #sz' #i' whd in match (sem_xor ??);
     2648          @intsize_eq_elim_elim
     2649          [ 1: #_ #Habsurd destruct (Habsurd)
     2650          | 2: #Heq destruct (Heq) normalize nodelta
     2651               #Heq destruct (Heq) /3 by ex_intro,conj,vint_eq/ ]
     2652] ]
     2653normalize in match (sem_xor ??); #arg1 destruct
     2654normalize in match (sem_xor ??); #arg2 destruct
     2655normalize in match (sem_xor ??); #arg3 destruct
     2656normalize in match (sem_xor ??); #arg4 destruct
     2657qed.
     2658
     2659lemma shl_value_eq :
     2660  ∀E,v1,v2,v1',v2'.
     2661   value_eq E v1 v2 →
     2662   value_eq E v1' v2' →
     2663   ∀r1. (sem_shl v1 v1'=Some val r1→
     2664           ∃r2:val.sem_shl v2 v2'=Some val r2∧value_eq E r1 r2).
     2665#E #v1 #v2 #v1' #v2' #Hvalue_eq1 #Hvalue_eq2 #r1
     2666@(value_eq_inversion E … Hvalue_eq1)
     2667[ 1: #v | 2: #sz #i | 3: #f | 4: | 5: #p1 #p2 #Hembed ]
     2668[ 2:
     2669     @(value_eq_inversion E … Hvalue_eq2)
     2670     [ 1: #v' | 2: #sz' #i' | 3: #f' | 4: | 5: #p1' #p2' #Hembed' ]
     2671     [ 2: whd in match (sem_shl ??);
     2672          cases (lt_u ???) normalize nodelta
     2673          [ 1: #Heq destruct (Heq) /3 by ex_intro,conj,vint_eq/
     2674          | 2: #Habsurd destruct (Habsurd)
     2675          ]
     2676     | *: whd in match (sem_shl ??); #Habsurd destruct (Habsurd) ]
     2677| *: whd in match (sem_shl ??); #Habsurd destruct (Habsurd) ]
     2678qed.
     2679
     2680lemma shr_value_eq :
     2681  ∀E,v1,v2,v1',v2',ty,ty'.
     2682   value_eq E v1 v2 →
     2683   value_eq E v1' v2' →
     2684   ∀r1. (sem_shr v1 ty v1' ty'=Some val r1→
     2685           ∃r2:val.sem_shr v2 ty v2' ty'=Some val r2∧value_eq E r1 r2).
     2686#E #v1 #v2 #v1' #v2' #ty #ty' #Hvalue_eq1 #Hvalue_eq2 #r1
     2687@(value_eq_inversion E … Hvalue_eq1)
     2688[ 1: #v | 2: #sz #i | 3: #f | 4: | 5: #p1 #p2 #Hembed ]
     2689whd in match (sem_shr ????); whd in match (sem_shr ????);
     2690[ 1: cases (classify_aop ty ty') normalize nodelta
     2691     [ 1: #sz #sg | 2: #fsz | 3: #ty1' #ty2' ]
     2692     #Habsurd destruct (Habsurd)
     2693| 2: cases (classify_aop ty ty') normalize nodelta
     2694     [ 1: #sz #sg | 2: #fsz | 3: #ty1' #ty2' ]
     2695     [ 2,3: #Habsurd destruct (Habsurd) ]
     2696     @(value_eq_inversion E … Hvalue_eq2) normalize nodelta
     2697     [ 1: #v' | 2: #sz' #i' | 3: #f' | 4: | 5: #p1' #p2' #Hembed' ]
     2698     [ 1,3,4,5: #Habsurd destruct (Habsurd) ]
     2699     elim sg normalize nodelta
     2700     cases (lt_u ???) normalize nodelta #Heq destruct (Heq)
     2701     /3 by ex_intro, conj, refl, vint_eq/
     2702| 3: cases (classify_aop ty ty') normalize nodelta
     2703     [ 1: #sz #sg | 2: #fsz | 3: #ty1' #ty2' ]
     2704     #Habsurd destruct (Habsurd)
     2705| 4: cases (classify_aop ty ty') normalize nodelta
     2706     [ 1: #sz #sg | 2: #fsz | 3: #ty1' #ty2' ]
     2707     #Habsurd destruct (Habsurd)
     2708| 5: cases (classify_aop ty ty') normalize nodelta
     2709     [ 1: #sz #sg | 2: #fsz | 3: #ty1' #ty2' ]
     2710     #Habsurd destruct (Habsurd)
     2711] qed.
     2712
     2713(* We want to prove that, but we can't since valid_pointers can in fact be one off outside the block,
     2714   and [memory_inj] handles only stuff that is loadable (i.e. inside a block). TODO *)
     2715lemma pointer_eq_valid :
     2716∀E,m,m',p,p'.
     2717 memory_inj E m m' →
     2718 pointer_translation p E = Some ? p' →
     2719 valid_pointer m p →
     2720 valid_pointer m' p'.
     2721@cthulhu qed.
     2722
     2723
     2724lemma sem_cmp_value_eq :
     2725  ∀E,v1,v2,v1',v2',ty,ty',m1,m2.
     2726   value_eq E v1 v2 →
     2727   value_eq E v1' v2' →
     2728   memory_inj E m1 m2 →   
     2729   ∀op,r1. (sem_cmp op v1 ty v1' ty' m1 = Some val r1→
     2730           ∃r2:val.sem_cmp op v2 ty v2' ty' m2 = Some val r2∧value_eq E r1 r2).
     2731#E #v1 #v2 #v1' #v2' #ty #ty' #m1 #m2 #Hvalue_eq1 #Hvalue_eq2 #Hinj #op #r1
     2732cases op whd in match (sem_cmp ??????); whd in match (sem_cmp ??????);
     2733[ 1:
     2734  cases (classify_cmp ty ty') normalize nodelta
     2735  [ 1: #sz #sg | 2: #n #ty0 | 3: #fsz | 4: #ty0 #ty0' #Habsurd destruct (Habsurd) ]
     2736  @(value_eq_inversion E … Hvalue_eq1)
     2737  [ 1,6,11: #v | 2,7,12: #sz #i | 3,8,13: #f | 4,9,14: | 5,10,15: #p1 #p2 #Hembed ]
     2738  normalize nodelta
     2739  [ 1,2,3,5,6,7,8,10,12,13,15: #Habsurd destruct (Habsurd) ]
     2740  @(value_eq_inversion E … Hvalue_eq2) normalize nodelta
     2741  [ 1,6,11,16: #v' | 2,7,12,17: #sz' #i' | 3,8,13,18: #f' | 4,9,14,19: | 5,10,15,20: #p1' #p2' #Hembed' ]
     2742  [ 5: elim sg normalize nodelta
     2743       @intsize_eq_elim_elim
     2744       [ 1,3: #_ #Habsurd destruct (Habsurd)
     2745       | 2,4: #Heq destruct (Heq) normalize nodelta
     2746              [ 1: cases (cmp_int ????) whd in match (of_bool ?); #Heq destruct (Heq)
     2747              | 2: cases (cmpu_int ????) whd in match (of_bool ?); #Heq destruct (Heq) ]
     2748              /3 by ex_intro, conj, vint_eq/ ]
     2749  | 10: #Heq destruct (Heq) cases (Fcmp Ceq f f') /3 by ex_intro, conj, vint_eq/
     2750  | 15: whd in match (sem_cmp_match ?); #Heq destruct (Heq)
     2751        /3 by ex_intro, conj, vint_eq/
     2752  | 16,19: whd in match (sem_cmp_mismatch ?); #Heq destruct (Heq)
     2753        /3 by ex_intro, conj, vint_eq/
     2754  | 20: @cthulhu (* relies on [pointer_eq_valid] TODO *)   
     2755  | *: #Habsurd destruct (Habsurd) ]
     2756| *: @cthulhu ]
     2757qed.
     2758 
    22982759(* Commutation result for binary operators. *)
    22992760lemma binary_operation_value_eq :
Note: See TracChangeset for help on using the changeset viewer.