Ignore:
Timestamp:
Mar 8, 2013, 12:48:20 PM (7 years ago)
Author:
garnier
Message:

A consitent proof state for Clight to Cminor, with some progress (and some temporary regressions)

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/memoryInjections.ma

    r2698 r2822  
    20202020(* Lift the above result to memory_inj
    20212021 * This is Lemma 40 of Leroy & Blazy *)
    2022 lemma bestorev_memory_inj_to_memory_inj :
     2022lemma store_value_of_type_memory_inj_to_memory_inj :
    20232023  ∀E,mA,mB,mC.
    20242024  ∀Hext:memory_inj E mA mB.
     
    22112211  ∀b1,b2,delta. E b1 = Some ? 〈b2, delta〉 →
    22122212  ∀ty,i,m1'.
    2213   ast_typ_consistent_with_value ty v1 →
     2213  (* ast_typ_consistent_with_value ty v1 → *)
    22142214  storen m1 (mk_pointer b1 i) (fe_to_be_values ty v1) = Some ? m1' →
    22152215  ∃m2'. storen m2 (mk_pointer b2 (offset_plus i delta)) (fe_to_be_values ty v2) = Some ? m2' ∧
     
    22992299  ∀b1,b2,delta. E b1 = Some ? 〈b2, delta〉 →
    23002300  ∀ty,i,m1'.
    2301   type_consistent_with_value ty v1 →
     2301  (* type_consistent_with_value ty v1 → *)
    23022302  store_value_of_type ty m1 b1 i v1 = Some ? m1' →
    23032303  ∃m2'. store_value_of_type ty m2 b2 (offset_plus i delta) v2 = Some ? m2' ∧
     
    23072307[ | #sz' #sg' | #ptr_ty' | #array_ty' #array_sz' | #domain' #codomain'
    23082308| #structname' #fieldspec' | #unionname' #fieldspec' | #id' ]
    2309 #Hconsistent whd in ⊢ ((??%?) → ?);
     2309whd in ⊢ ((??%?) → ?);
    23102310[ 1,4,5,6,7: #Habsurd destruct ]
    23112311whd in match (store_value_of_type ?????);
    2312 @(storen_parallel_aux … Hinj … Hembed … Hconsistent) //
     2312@(storen_parallel_aux … Hinj … Hembed) //
    23132313qed.
    23142314
Note: See TracChangeset for help on using the changeset viewer.