Changeset 3493 for LTS/Vm.ma


Ignore:
Timestamp:
Sep 25, 2014, 1:43:19 PM (5 years ago)
Author:
piccolo
Message:
 
File:
1 edited

Legend:

Unmodified
Added
Removed
  • LTS/Vm.ma

    r3492 r3493  
    1 include "costs.ma".
     1 include "costs.ma".
    22include "basics/lists/list.ma".
    33include "../src/utilities/option.ma".
     
    460460definition asm_static_analisys_data ≝ λp,p',prog,abs_t,instr_m.
    461461mk_static_analysis_data (asm_concrete_trans_sys p p' prog) abs_t (option (AssemblerInstr p))
    462  (λs.match s with [ STATE st ⇒ ! x ← fetch_state p p' prog st; Some ? (Some ? x)
     462 (λs.match s with [ STATE st ⇒ if eqb (pc … st) (endmain … prog) then
     463                                   Some ? (None ?)
     464                               else ! x ← fetch_state p p' prog st; Some ? (Some ? x)
    463465                  | INITIAL ⇒ Some ? (None ?)
    464466                  | FINAL  ⇒ None ? ]) instr_m.
     
    856858qed.
    857859
     860definition actionlabel_to_costlabel : ActionLabel → list CostLabel ≝
     861λa.match a with
     862[ call_act f l ⇒ [a_call l]
     863| ret_act opt_l ⇒ match opt_l with [None ⇒ [ ] | Some l ⇒ [a_return_post l]]
     864| cost_act opt_l ⇒ match opt_l with [None ⇒ [ ] | Some l ⇒ [a_non_functional_label l]]
     865].
     866
     867lemma get_cost_label_of_trace_tind : ∀S : abstract_status.
     868∀st1,st2,st3 : S.∀l,prf,t.
     869get_costlabels_of_trace … (t_ind … st1 st2 st3 l prf t) =
     870actionlabel_to_costlabel l @ get_costlabels_of_trace … t.
     871#S #st1 #st2 #st3 * // qed.
     872
     873lemma actionlabel_ok : ∀l : ActionLabel.
     874(is_costlabelled_act l ∨ is_labelled_ret_act l) → ∃c.actionlabel_to_costlabel l = [c].
     875* /2 by refl, ex_intro/
     876[ * /2/ ** #x #EQ destruct | * /2/ ** #x #EQ destruct]
     877qed.
     878
    858879lemma static_dynamic : ∀p,p',prog.
    859880∀abs_t : abstract_transition_sys (m … p').∀instr_m : (AssemblerInstr p) → abs_instr … abs_t.
     
    880901]
    881902#p #p' #prog #abs_t #instr_m #good #mT #map1 #EQmap #st1 #st2 #t * #st3 * #t1 * #l1 * #prf1 * #EQ destruct
    882 lapply prf1 -prf1 lapply l1 -l1 elim t1 -st3
    883 [ * [3: #st] #l #prf * #H1 #H2 #k #_ whd in ⊢ (??%? → ?);
     903* #Hlabelled
     904>(rewrite_in_dependent_map ??? (get_costlabels_of_trace … t1))
     905[2: >get_cost_label_append  >get_cost_label_of_trace_tind >append_nil cases(actionlabel_ok … Hlabelled)
     906   #c #EQc >EQc //
     907]   
     908lapply Hlabelled lapply prf1 -prf1 lapply l1 -l1 elim t1 -st3
     909[ * [3: #st] #l #prf #H1 #H2 #k #_ whd in ⊢ (??%? → ?);
    884910  [3: cases prf
    885   |2: whd in ⊢ (??%% → ?); #EQ destruct #a1 #rel_fin #labels whd in match (get_costlabels_of_trace ????);
    886       whd in match (get_costlabels_of_trace ????);
     911  |2: whd in ⊢ (??%% → ?); #EQ destruct #a1 #rel_fin #labels whd in ⊢ (??%% → ?);
    887912      lapply(instr_map_ok … good … prf … rel_fin) [ %|] cases st2 in prf; -st2 [3: #st2] *
    888       #EQpc #EQ destruct #H whd in ⊢ (??%% → ?); whd in match (dependent_map ????);
    889       #EQ destruct >act_neutral >act_neutral normalize in H;
     913      #EQpc #EQ destruct #H #EQ destruct >act_neutral >act_neutral normalize in H;
    890914      <(act_neutral ?? (act_abs ? abs_t) a1) @H
    891915  | @eqb_elim normalize nodelta
    892     [ #EQpc whd in ⊢(??%% → ?); #EQ destruct #a1 #good_st_a1 #labels
     916    [ #EQpc whd in ⊢(??%% → ?); #EQ destruct #a1 #good_st_a1 #labels whd in ⊢ (??%% → ?);
     917      #EQ destruct >act_neutral >act_neutral whd in prf; cases st2 in prf; -st2 [3: #st2]
     918      normalize nodelta * >EQpc @eqb_elim [2,4: * #ABS @⊥ @ABS %] #_ #EQ destruct
     919      #EQ destruct whd in EQc : (??%%); destruct
     920      lapply(instr_map_ok …  good … good_st_a1)
     921      [5: @(FINAL …)
     922      |2: whd % [ >EQpc @eqb_elim // * #ABS @⊥ @ABS %] %
     923      | whd in ⊢ (??%%); @eqb_elim [2: * #ABS @⊥ @ABS assumption
     924      ]
     925      #_ normalize nodelta % | | | whd in ⊢ (% → ?); >act_neutral //
     926      ]
     927  | #Hpc lapply prf whd in ⊢ (% → ?); cases st2 in prf; -st2 [3: #st2] #prf
     928    normalize nodelta [2:* |3: * #ABS @⊥ lapply ABS -ABS @eqb_elim
     929    [#EQ #_ @(absurd ? EQ Hpc) | #_ #EQ destruct ] ] * #INUTILE #H4
     930    #H cases(bind_inversion ????? H) -H *
     931    [ #seq * [|#lbl1]
     932    | #newpc
     933    | #cond #newpc #ltrue #lfalse
     934    | #lin #io #lout
     935    | #f
     936    |
     937    ]
     938    * #EQfetch  lapply(vm_step_to_eval … H4) whd in match eval_vmstate;
     939    normalize nodelta >EQfetch >m_return_bind normalize nodelta
     940    cases(asm_is_io ??) normalize nodelta
     941    [1,3,5,7,11,13: whd in ⊢ (??%% → ?); #EQ destruct
     942    |2,4,8,9,12,14: #H cases(bind_inversion ????? H) -H #x * #_
     943      [3: cases x normalize nodelta
     944      |6: #H cases(bind_inversion ????? H) -H #y * #_
     945      ]
     946    ]
     947    whd in ⊢ (??%% → ?); #EQ destruct
     948    [4,8: cases H1 [1,3: * |*: * #y #EQ destruct]]
     949    >m_return_bind whd in ⊢ (??%% → ?); #EQ destruct
     950    #a1 #good_st_a1 whd in match (dependent_map ????); #costs #EQ destruct >neutral_r
     951    >act_neutral
     952    lapply(instr_map_ok … good … good_st_a1)
     953    [1,7,13,19,25,31,37: whd in ⊢ (??%%); @eqb_elim normalize nodelta
     954      [1,3,5,7,9,11,13: #EQ cases(absurd ? EQ Hpc) ] #_ whd in match fetch_state;
     955        normalize nodelta
     956        [ >EQfetch in ⊢ (??%?); | >EQfetch in ⊢ (??%?); | >EQfetch in ⊢ (??%?);
     957        | >EQfetch in ⊢ (??%?); | >EQfetch in ⊢ (??%?); | >EQfetch in ⊢ (??%?);
     958        | >EQfetch in ⊢ (??%?); ] %
     959      |3,9,15,21,27,33,39: skip |*: try assumption // ]
     960      ]
     961    ]
     962| -st1 * [3: #st1] #st3 #st4 #l [3: *] cases st3 -st3
     963  [1,2,4,5: * #H1 #H2 #tl #_ #l1 #exe @⊥ lapply tl -tl lapply(refl ? (FINAL p p'))
     964    generalize in match (FINAL ??) in ⊢ (??%? → %); #st5 #EQst5 #tl lapply EQst5
     965    lapply exe lapply st2 -st2 -EQst5 elim tl
     966    [ #st #st5 #ABS #EQ destruct cases ABS
     967    | #s1 #s2 #s3 #l2 #H3 #tl1 #IH #s4 #_ #EQ destruct cases H3
     968    ]
     969  ]
     970  #st3 #exe_st1_st3 #tl #IH #l1 #exe_st4_st2 #l1_lab #l1_lab1 #k #pre_meas whd in ⊢ (??%? → ?);
     971  >rewrite_in_dependent_map [2,5: @get_cost_label_of_trace_tind |3,6: ]
     972  >dependent_map_append
     973  [ @eqb_elim [ #ABS @⊥ cases exe_st1_st3 >ABS @eqb_elim [ #_ #EQ destruct | * #ABS1 @⊥ @ABS1 %] ]
     974    #Hpc normalize nodelta #H cases(bind_inversion ????? H) -H #i * #EQi
     975    inversion(emits_labels ??)
     976    [ #EQemits whd in ⊢ (??%% → ?); #EQ destruct #a1 #good_a1 #labels
     977      cases(step_emit … EQi … EQemits)
     978      [4: cases exe_st1_st3  #EQ #H @(vm_step_to_eval … H) |2,3:] #c * #EQc #Hc
     979      whd in match actionlabel_to_costlabel; normalize nodelta
     980      >rewrite_in_dependent_map [2: @EQc |3:] whd in match (dependent_map ????);
     981      @opt_safe_elim #k_c #EQk_c whd in match (dependent_map ????); letin ih_labels ≝ (dependent_map ????)
     982      #EQ destruct >big_op_associative >act_op @IH
     983    | #f #EQemits normalize nodelta #H cases(bind_inversion ????? H) -H #k' * #EQk' whd in ⊢ (??%% → ?);
     984      #EQ destruct(EQ) #a1 #good_a1 #labels cases(step_non_emit … EQi… EQemits)
     985      [4: cases exe_st1_st3  #EQ #H @(vm_step_to_eval … H) |2,3:] #EQl #EQpc
     986      >(rewrite_in_dependent_map ??? []) [2: assumption] whd in match (dependent_map ????);
     987      #EQlabels >act_op @IH
     988  ]
     989   [2: assumption | | assumption | assumption | cases daemon (*TODO*)|
     990      whd in ⊢ (??%%);
     991  [1,5: inversion H in ⊢ ?;
     992    [1,6: #st #c #EQ1 #EQ2 #EQ3 #EQ4 destruct
     993    |2,7: #s1 #s2 #s3 #lbl #exe #tl1 #s1_noio * #opt_l #EQ destruct #pre_tl1 #_
     994      #EQ1 #EQ2 #EQ3 #EQ4 destruct
     995    |3,8: #s1 #s2 #s3 #lbl #s1_noio #exe #tl1 * #lbl1 #EQ destruct #pre_tl1 #_
     996      #EQ1 #EQ2 #EQ3 #EQ4 destruct
     997    |4,9: #s1 #s2 #s3 #lbl #exe #tl1 #s1_noio * #f * #lbl1 #EQ destruct
     998      * #pre_tl1 #_ #EQ1 #EQ2 #EQ3 #EQ4 destruct
     999    |5,10: #s1 #s2 #s3 #s4 #s5 #l1 #l2 #exe1 #t1 #t2 #exe2 #noio1 #noio2 #H *
     1000    ] //
     1001  | cases(step_emit … EQi (vm_step_to_eval … H4) … EQemits) #x * #EQx #Hx
     1002    >(rewrite_in_dependent_map … EQx)
     1003 
     1004    whd in match (dependent_map ????); whd in match (dependent_map ????); whd in match (big_op ??);
     1005    >neutral_l @opt_safe_elim #elem #EQget
     1006    cases (static_analisys_ok  … x … (pc … st2) … no_dup … EQmap) //
     1007    #EQ #_ <EQ assumption
     1008  | >neutral_r  @(instr_map_ok … good … EQi … good_a1) /2/
     1009  | %
     1010  | >(proj2 … (step_non_emit … EQi (vm_step_to_eval … H4) … EQemits))
     1011    >(monotonicity_of_block_cost … EQk') //
     1012  | @(instr_map_ok … good … EQi … good_a1) /2/
     1013  | lapply (proj1 … (step_non_emit … EQi (vm_step_to_eval … H4) … EQemits))
     1014    #EQ >(rewrite_in_dependent_map … EQ) %
     1015  ]
    8931016    >(rewrite_in_dependent_map ??? [])
    8941017    [ whd in ⊢ (???% → ?); #EQ destruct whd >act_neutral >act_neutral
    8951018      lapply (instr_map_ok … good … prf …)
    8961019   
    897       >(act_neutral ?? (act_abs ? abs_t) a1))
    898       change
    899       with (get_costlabels_of_trace ??? (?@?))
    900       in match (get_costlabels_of_trace ????);
    901       cases l
     1020    >rewrite_in_dependent_map [2: @eq_f [2: @eq_f2 [3: % |4: @get_cost_label_append |*:] |*:] |3:]
     1021    xxxxxx
    9021022   
    903       >(rewrite_in_dependent_map …) [2: @eq_f [2: @get_cost_label_append |skip]|3:skip]
    904       cases daemon
    905     | cases daemon ]]
    906 | -st1 #st1 #st3 #st4 #l whd in ⊢ (% → ?);
     1023    >dependent_map_append
     1024  inversion(emits_labels ??)
     1025  [ #EQemits whd in ⊢ (??%% → ?); #EQ destruct #a1 #good_a1 #labels
     1026    >rewrite_in_dependent_map #EQlabels
     1027    >neutral_r check big_op_associative @IH
     1028    >big_op_associative >act_op @IH
     1029  | #f #EQemits normalize nodelta #H
     1030    cases(bind_inversion ????? H) -H #k' * #EQk' whd in ⊢ (??%% → ?);
     1031    #EQ destruct(EQ) >act_op whd in match (append ???); @IH
     1032  ]
     1033  [1,5: inversion H in ⊢ ?;
     1034    [1,6: #st #c #EQ1 #EQ2 #EQ3 #EQ4 destruct
     1035    |2,7: #s1 #s2 #s3 #lbl #exe #tl1 #s1_noio * #opt_l #EQ destruct #pre_tl1 #_
     1036      #EQ1 #EQ2 #EQ3 #EQ4 destruct
     1037    |3,8: #s1 #s2 #s3 #lbl #s1_noio #exe #tl1 * #lbl1 #EQ destruct #pre_tl1 #_
     1038      #EQ1 #EQ2 #EQ3 #EQ4 destruct
     1039    |4,9: #s1 #s2 #s3 #lbl #exe #tl1 #s1_noio * #f * #lbl1 #EQ destruct
     1040      * #pre_tl1 #_ #EQ1 #EQ2 #EQ3 #EQ4 destruct
     1041    |5,10: #s1 #s2 #s3 #s4 #s5 #l1 #l2 #exe1 #t1 #t2 #exe2 #noio1 #noio2 #H *
     1042    ] //
     1043  | cases(step_emit … EQi (vm_step_to_eval … H4) … EQemits) #x * #EQx #Hx
     1044    >(rewrite_in_dependent_map … EQx)
     1045 
     1046    whd in match (dependent_map ????); whd in match (dependent_map ????); whd in match (big_op ??);
     1047    >neutral_l @opt_safe_elim #elem #EQget
     1048    cases (static_analisys_ok  … x … (pc … st2) … no_dup … EQmap) //
     1049    #EQ #_ <EQ assumption
     1050  | >neutral_r  @(instr_map_ok … good … EQi … good_a1) /2/
     1051  | %
     1052  | >(proj2 … (step_non_emit … EQi (vm_step_to_eval … H4) … EQemits))
     1053    >(monotonicity_of_block_cost … EQk') //
     1054  | @(instr_map_ok … good … EQi … good_a1) /2/
     1055  | lapply (proj1 … (step_non_emit … EQi (vm_step_to_eval … H4) … EQemits))
     1056    #EQ >(rewrite_in_dependent_map … EQ) %
     1057  ]
     1058]
     1059       
     1060  ]
     1061 
     1062 
     1063 
     1064  * #i * #EQi inversion(emits_labels …) normalize nodelta
     1065       
     1066     
     1067       >(act_neutral … a1) in H;
     1068     
     1069     
     1070       #H #H1
     1071      cases st2 in prf; -st2 [3: #st2] #prf
     1072      lapply(instr_map_ok … good … prf … rel_fin)
     1073     
     1074       lapply prf *
     1075      #EQpc_st2 #EQ destruct normalize nodelta whd in ⊢ (??%% → ?); #EQ destruct
     1076      >act_neutral >act_neutral @(instr_map_ok … good … rel_fin)
     1077     
     1078     
     1079       @opt_safe_elim #k_init
     1080      #EQk_init whd in ⊢ (??%% → ?); whd in match (dependent_map ????); #EQ destruct
     1081      >act_neutral whd in match (big_op ??); >act_op >act_neutral
     1082     
     1083     
     1084       #H >act_neutral whd in prf;
     1085       
     1086        cases l in prf H1 H2;
     1087        [1,4: #f #lbl |2,5: * [2,4: #lbl] |*: * [2,4: #lbl] ] #prf
     1088        ** [normalize in ⊢ (% → ?);
     1089         ⊢ (??%% → ?);
    9071090
    9081091 * #H3 #H4
Note: See TracChangeset for help on using the changeset viewer.