Ignore:
Timestamp:
Jan 23, 2013, 2:38:06 PM (7 years ago)
Author:
garnier
Message:

modified Cexec/Csem? semantics:
. force andbool and orbool types to be Tint sz sg, fail otherwise
. cast result of evaluation to (bitvector sz)
. in lvalue evaluation, field offset for structs is now 16 bit instead of 32
/!\ induction principles modified accordingly
. soundness and correctness adapted

modified label/labelSimulation:
. andbool and orbool are modified so that the true/false constants are

casted to the (integer) type of the enclosing expression, to match
Csem/Cexec?. If the type is not an integer, default on 32 bits.

. labelSimulation proof adapted to match changes.

proof of simulation for expressions Cl to Cm finished
. caveat : eats up all my RAM (8gb) when using matita (not matitac), barely typecheckable
. moved some lemmas from toCminorCorrectness.ma to new file toCminorOps.ma

and frontend_misc.ma to alleviate this, to no avail - more radical splitting required ?

slight modification in SimplifyCasts? to take into account modifications in semantics,
removed some duplicate lemmas and replaced them by wrappers to avoid breaking the
rest of the development.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/labelSimulation.ma

    r2574 r2588  
    22include "Clight/labelSpecification.ma".
    33include "Clight/CexecInd.ma".
     4include "Clight/frontend_misc.ma".
    45
    56(* Useful for breaking up the labeling functions, because we don't care about
     
    4647  trace_with_extra_labels (tr1⧺tr2) (tr1'⧺tr2').
    4748#tr1 #tr2 #tr1' #tr2' #twel1 elim twel1 /3/
    48 qed. 
     49qed.
    4950
    5051
     
    162163  >shift_fst whd in ⊢ (??(λ_.?(??(????(?(???%)?))?)?));
    163164  @label_gen_elim #u2
    164   @label_gen_elim #u3
    165   @add_cost_expr_elim #u4 #l4
    166   @add_cost_expr_elim #u5 #l5
    167   @add_cost_expr_elim #u6 #l6
    168   @add_cost_expr_elim #u7 #l7
     165  @label_gen_elim #u3 normalize nodelta in EX;
    169166  [ cases (bind_inversion ????? EX) -EX * #v2 #tr2 * #EX2 #EX
    170167    cases (bind_inversion ????? EX) -EX * * #EX3 #EX
     168    (* >>> *)
     169    cases (res_inversion ?????? EX) -EX #vres * #Hcast
     170    cases (cast_bool_to_target_inversion … Hcast) #sz * #sg * #Heq_ty #Heq_vres
     171    #Heq destruct normalize nodelta
     172    @add_cost_expr_elim #u4 #l4
     173    @add_cost_expr_elim #u5 #l5
     174    @add_cost_expr_elim #u6 #l6
     175    @add_cost_expr_elim #u7 #l7
     176    (* <<< *)
    171177    cases (IH1 … EX1 u) #tr1' * #EX1' #twel1
    172178    cases (IH2 … EX2 u2) #tr2' * #EX2' #twel2
     
    177183    whd in ⊢ (?(??(match (match % with [_⇒?|_⇒?]) with [_⇒?|_⇒?])?)?); >EX2'
    178184    whd in ⊢ (?(??(match (match % with [_⇒?|_⇒?]) with [_⇒?|_⇒?])?)?); >label_expr_type >EX3
    179     whd in EX:(??%%) ⊢ %; destruct % [ 1,3: normalize @refl | *: @twel_app // @twel_new whd in ⊢ (??%); <(E0_right tr2) @twel_app /2/ ]
     185    whd in EX:(??%%) ⊢ %; destruct %
     186    [ 1,3: normalize nodelta
     187           whd in match (m_bind ?????);
     188           whd in match (exec_expr ????);
     189           whd in match (exec_expr ????);
     190           >eq_intsize_true normalize nodelta
     191           [ >zero_ext_one | >zero_ext_zero ]
     192           @refl           
     193    | *: @twel_app // @twel_new whd in ⊢ (??%); <(E0_right tr2) @twel_app /2/ ]
    180194  | cases (IH1 … EX1 u) #tr1' * #EX1' #twel1
     195    cases (res_inversion ?????? EX) -EX #vres * #Hcast
     196    cases (cast_bool_to_target_inversion … Hcast) #sz * #sg * #Heq_ty #Heq_vres
     197    #Heq destruct normalize nodelta
     198    @add_cost_expr_elim #u4 #l4
     199    @add_cost_expr_elim #u5 #l5
     200    @add_cost_expr_elim #u6 #l6
     201    @add_cost_expr_elim #u7 #l7
    181202    %{(tr1'⧺E0⧺Echarge l7)}
    182203    whd in ⊢ (?(??%?)?); >EX1'
    183204    whd in ⊢ (?(??%?)?); >label_expr_type >EXguard
    184     whd in EX:(??%%); destruct % normalize // <(E0_right tr) @twel_app /2/
     205    whd in EX:(??%%); destruct % normalize nodelta
     206    whd in match (m_bind ?????);
     207    whd in match (exec_expr ????);
     208    whd in match (exec_expr ????);
     209    [ >eq_intsize_true ] normalize nodelta
     210    [ >zero_ext_zero @refl ]   
     211    <(E0_right tr) @twel_app /2/
    185212  ]
    186213| #ty #e1 #e2 #IH1 #IH2 #v #tr #EX #u
     
    190217  @label_gen_elim #u2
    191218  @label_gen_elim #u3
    192   @add_cost_expr_elim #u4 #l4
    193   @add_cost_expr_elim #u5 #l5
    194   @add_cost_expr_elim #u6 #l6
    195   @add_cost_expr_elim #u7 #l7
     219  normalize nodelta in EX;
    196220  [ cases (IH1 … EX1 u) #tr1' * #EX1' #twel1
     221    cases (res_inversion ?????? EX) -EX #vres * #Hcast
     222    cases (cast_bool_to_target_inversion … Hcast) #sz * #sg * #Heq_ty #Heq_vres
     223    #Heq destruct normalize nodelta 
     224    @add_cost_expr_elim #u4 #l4
     225    @add_cost_expr_elim #u5 #l5
     226    @add_cost_expr_elim #u6 #l6
     227    @add_cost_expr_elim #u7 #l7
    197228    %{(tr1'⧺Echarge l7)}
    198229    whd in ⊢ (?(??%?)?); >EX1'
    199     whd in ⊢ (?(??%?)?); >label_expr_type >EXguard
    200     whd in EX:(??%%) ⊢ %; destruct normalize % // <(E0_right tr) /3/
     230    whd in ⊢ (?(??%?)?); >label_expr_type >EXguard normalize nodelta
     231    whd in match (m_bind ?????);
     232    whd in match (exec_expr ????);
     233    whd in match (exec_expr ????);
     234    >eq_intsize_true normalize nodelta
     235    % // <(E0_right tr) /3/
    201236  | cases (bind_inversion ????? EX) -EX * #v2 #tr2 * #EX2 #EX
    202237    cases (bind_inversion ????? EX) -EX * * #EX3 #EX
    203238    cases (IH1 … EX1 u) #tr1' * #EX1' #twel1
    204239    cases (IH2 … EX2 u2) #tr2' * #EX2' #twel2
     240    cases (res_inversion ?????? EX) -EX #vres * #Hcast
     241    cases (cast_bool_to_target_inversion … Hcast) #sz * #sg * #Heq_ty #Heq_vres
     242    #Heq destruct normalize nodelta
     243    @add_cost_expr_elim #u4 #l4
     244    @add_cost_expr_elim #u5 #l5
     245    @add_cost_expr_elim #u6 #l6
     246    @add_cost_expr_elim #u7 #l7   
    205247    [ %{(tr1'⧺Echarge l6⧺tr2'⧺Echarge l4)} | %{(tr1'⧺Echarge l6⧺tr2'⧺Echarge l5)} ]
    206248    whd in ⊢ (?(??%?)?); >EX1'
     
    209251    whd in ⊢ (?(??(match (match % with [_⇒?|_⇒?]) with [_⇒?|_⇒?])?)?); >EX2'
    210252    whd in ⊢ (?(??(match (match % with [_⇒?|_⇒?]) with [_⇒?|_⇒?])?)?); >label_expr_type >EX3
    211     whd in EX:(??%%) ⊢ %; destruct normalize % [1,3: % | *: @twel_app // @twel_new <(E0_right tr2) @twel_app /2/ ]
     253    normalize nodelta
     254    whd in match (m_bind ?????);
     255    whd in match (exec_expr ????);
     256    whd in match (exec_expr ????);
     257    >eq_intsize_true normalize nodelta   
     258    % [ 1,3: [ >zero_ext_one | >zero_ext_zero ] >E0_right @refl
     259      | *: @twel_app // @twel_new >nil_append <(E0_right tr2) @twel_app /2/ ]
    212260  ]
    213261| #ty #ty' #v #tr normalize /3/
Note: See TracChangeset for help on using the changeset viewer.