Changeset 3499


Ignore:
Timestamp:
Sep 25, 2014, 4:13:03 PM (5 years ago)
Author:
sacerdot
Message:

Nicer statement.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • LTS/Vm.ma

    r3498 r3499  
    907907 terminated_trace … t → pre_measurable_trace … t →
    908908
     909(* Let labels be the costlabels observed in the trace, excluding the last one *)
     910let labels ≝ chop … (get_costlabels_of_trace …  t) in
     911
    909912(* Let k be the statically computed abstract action of the prefix of the trace
    910913   up to the first label *)
    911914∀k.block_cost p prog … instr_m (get_pc … st1 (endmain … prog)) (S (|(instructions … prog)|)) = return k →
    912 
    913 (* Given an abstract state in relation with the first state of the trace *)
    914 ∀a1.R st1 a1 →
    915 
    916 (* Let labels be the costlabels observed in the trace, excluding the last one *)
    917 let labels ≝ chop … (get_costlabels_of_trace …  t) in
    918915
    919916(* Let abs_actions be the list of statically computed abstract actions
     
    923920  dependent_map … labels (λlbl,prf.(opt_safe … (get_map … map1 lbl) …)) →
    924921
     922(* Given an abstract state in relation with the first state of the trace *)
     923∀a1.R st1 a1 →
     924
    925925(* The final state of the trace is in relation with the one obtained by
    926926   first applying k to a1, and then applying every semantics in abs_trace. *)
     
    933933    @(proj2 … (static_analisys_ok … EQmap … Hmem))
    934934]
    935 #p #p' #prog #abs_t #instr_m #good #mT #map1 #EQmap #st1 #st2 #t * #st3 * #t1 * #l1 * #prf1 * #EQ destruct
    936 #Hlabelled >(rewrite_in_dependent_map ??? (get_costlabels_of_trace … t1))
     935#p #p' #prog #abs_t #instr_m #good #mT #map1 #EQmap #st1 #st2 #t * #st3 * #t1 *
     936#l1 * #prf1 * #EQ destruct #Hlabelled
     937>(rewrite_in_dependent_map ??? (get_costlabels_of_trace … t1))
    937938[2: >get_cost_label_append  >get_cost_label_of_trace_tind >append_nil cases(actionlabel_ok … Hlabelled)
    938    #c #EQc >EQc //
    939 ]   
     939   #c #EQc >EQc // ]
    940940lapply Hlabelled lapply prf1 -prf1 lapply l1 -l1 elim t1 -st3
    941941[ * [3: #st] #l #prf #H1 #_ #k whd in ⊢ (??%? → ?);
    942942  [3: cases prf
    943   |2: whd in ⊢ (??%% → ?); #EQ destruct #a1 #rel_fin #labels whd in ⊢ (??%% → ?);
     943  |2: whd in ⊢ (??%% → ?); #EQ destruct #labels whd in ⊢ (??%% → ?); #EQlabels
     944      #a1 #rel_fin
    944945      lapply(instr_map_ok … good … prf … rel_fin) [ %|] cases st2 in prf; -st2 [3: #st2] *
    945       #EQpc #EQ destruct #H #EQ destruct >act_neutral >act_neutral normalize in H;
     946      #EQpc #EQ destruct #H >act_neutral >act_neutral normalize in H;
    946947      <(act_neutral … (act_abs …) a1) @H
    947948  | @eqb_elim normalize nodelta
    948     [ #EQpc whd in ⊢(??%% → ?); #EQ destruct #a1 #good_st_a1 #labels whd in ⊢ (??%% → ?);
    949       #EQ destruct >act_neutral >act_neutral whd in prf; cases st2 in prf; -st2 [3: #st2]
     949    [ #EQpc whd in ⊢(??%% → ?); #EQ destruct #labels whd in ⊢ (??%% → ?);
     950      #EQ destruct #a1 #good_st_a1>act_neutral >act_neutral whd in prf; cases st2 in prf; -st2 [3: #st2]
    950951      normalize nodelta * >EQpc @eqb_elim [2,4: * #ABS @⊥ @ABS %] #_ #EQ destruct
    951952      #EQ destruct whd in EQc : (??%%); destruct
     
    968969    |
    969970    ]
    970     * #EQfetch  lapply(vm_step_to_eval … H4) whd in match eval_vmstate;
     971    * #EQfetch  lapply(vm_step_to_eval … H4) whd in match eval_vmstate in ⊢ (% → ?);
    971972    normalize nodelta >EQfetch >m_return_bind normalize nodelta
    972973    cases(asm_is_io ??) normalize nodelta
     
    979980    whd in ⊢ (??%% → ?); #EQ destruct [4,8: cases H1 ]
    980981    >m_return_bind whd in ⊢ (??%% → ?); #EQ destruct
    981     #a1 #good_st_a1 whd in match (dependent_map ????); #costs #EQ destruct >neutral_r
    982     >act_neutral
     982    whd in match (dependent_map ????); #costs #EQ destruct #a1 #good_st_a1
     983    >neutral_r >act_neutral
    983984    lapply(instr_map_ok … good … good_st_a1)
    984985    [1,7,13,19,25,31,37: whd in ⊢ (??%%); @eqb_elim normalize nodelta
     
    10051006    #Hpc normalize nodelta #H cases(bind_inversion ????? H) -H #i * #EQi
    10061007    inversion(emits_labels ??)
    1007     [ #EQemits whd in ⊢ (??%% → ?); #EQ destruct #a1 #good_a1 #labels
     1008    [ #EQemits whd in ⊢ (??%% → ?); #EQ destruct #labels
    10081009      cases(step_emit … EQi … EQemits)
    10091010      [4: cases exe_st1_st3  #EQ #H @(vm_step_to_eval … H) |2,3:] #c * #EQc #Hc
     
    10111012      >rewrite_in_dependent_map [2: @EQc |3:] whd in match (dependent_map ????);
    10121013      @opt_safe_elim #k_c #EQk_c whd in match (dependent_map ????); letin ih_labels ≝ (dependent_map ????)
    1013       #EQ destruct >big_op_associative >act_op @IH
     1014      #EQ destruct #a1 #good_a1 >big_op_associative >act_op @IH
    10141015    | #f #EQemits normalize nodelta #H cases(bind_inversion ????? H) -H #k' * #EQk' whd in ⊢ (??%% → ?);
    1015       #EQ destruct(EQ) #a1 #good_a1 #labels cases(step_non_emit … EQi… EQemits)
     1016      #EQ destruct(EQ) #labels cases(step_non_emit … EQi… EQemits)
    10161017      [4: cases exe_st1_st3  #EQ #H @(vm_step_to_eval … H) |2,3:] #EQl #EQpc
    10171018      >(rewrite_in_dependent_map ??? []) [2: assumption] whd in match (dependent_map ????);
    1018       #EQlabels >act_op @IH
     1019      #EQlabels #a1 #good_a1 >act_op @IH
    10191020  ]
    10201021  try //
     
    10411042    ] //
    10421043  ]
    1043  | whd in ⊢ (??%% → ?); #EQ destruct #a1 #good_a1 cases exe_st1_st3 #EQpc_st3 #EQ destruct
     1044 | whd in ⊢ (??%% → ?); #EQ destruct cases exe_st1_st3 #EQpc_st3 #EQ destruct
    10441045   #labels whd in match actionlabel_to_costlabel; normalize nodelta
    10451046   whd in match (dependent_map ????); @opt_safe_elim #k_c #EQk_c letin ih_labels ≝ (dependent_map ????)
    1046    change with ([?]@?) in match ([?]@?); #EQ destruct >big_op_associative >act_op @IH try //
     1047   change with ([?]@?) in match ([?]@?); #EQ #a1 #good_a1 destruct
     1048   >big_op_associative >act_op @IH try //
    10471049   [  inversion pre_meas in ⊢ ?;
    10481050     [1,6: #st #c #EQ1 #EQ2 #EQ3 #EQ4 destruct whd in EQ3 : (??%??); destruct
     
    10551057     |5,10: #s1 #s2 #s3 #s4 #s5 #l1 #l2 #exe1 #t1 #t2 #exe2 #noio1 #noio2 #H *
    10561058     ] //
    1057    |  cases(static_analisys_ok … (in_act … prog) … (pc … st3) … EQmap) 
     1059   |  cases(static_analisys_ok … (in_act … prog) … (pc … st3) … EQmap)
    10581060      [2: lapply EQpc_st3 @eqb_elim [2: #_ #EQ destruct] #EQ #_ >EQ @i_act_in_map ]
    10591061      #EQ #_ <EQ whd in match (big_op ??); >neutral_l assumption
Note: See TracChangeset for help on using the changeset viewer.