Changeset 3505 for LTS


Ignore:
Timestamp:
Sep 26, 2014, 4:58:21 PM (5 years ago)
Author:
piccolo
Message:
 
File:
1 edited

Legend:

Unmodified
Added
Removed
  • LTS/Vm.ma

    r3503 r3505  
    11261126 mem … 〈c1,pc p p' st1〉
    11271127  (labels_pc … (instructions … prog) (call_label_fun … prog)
    1128    (return_label_fun … prog) (in_act … prog) O).
     1128   (return_label_fun … prog) (in_act … prog) O).
     1129#p #p' #prog #st0 #st1 #l1 #c1 #EQc1 #H lapply(vm_step_to_eval … H) -H
     1130#H cases(bind_inversion ????? H); #i * #EQi #Hi cases(step_emit … EQi H)
     1131[ #c2 whd in match actionlabel_to_costlabel in EQc1; normalize nodelta in EQc1;
     1132  >EQc1 * #EQ destruct // ]
     1133cases i in Hi;       
     1134[ #seq * [|#lbl1]
     1135| #newpc
     1136| #cond #newpc #ltrue #lfalse
     1137| #lin #io #lout
     1138| #f
     1139|
     1140]
     1141normalize nodelta cases(asm_is_io ??) normalize nodelta
     1142[1,3,5,7,11,13: whd in ⊢ (??%% → ?); #EQ destruct
     1143|2,4,8,9,12,14: #H cases(bind_inversion ????? H) -H #x * #_
     1144  [3: cases x normalize nodelta
     1145  |6: #H cases(bind_inversion ????? H) -H #y *  #_
     1146  ]
     1147]
     1148whd in ⊢ (??%% → ?); #EQ destruct try % normalize in EQc1; destruct
     1149qed.
     1150
    11291151theorem static_dynamic :
    11301152(* Given an assembly program *)
     
    11901212      [ normalize in ⊢ (??%%); >neutral_l @EQact
    11911213      |
    1192       | check nth_opt
    1193  
    1194   cases daemon
     1214      | @execute_mem_label_pc //
     1215      ]
     1216    | #H #EQ destruct #_ whd in match get_pc; normalize nodelta
     1217      <(proj1 ?? (static_analisys_ok … EQmap …))
     1218      [ normalize in ⊢ (??%%); >neutral_l @EQact
     1219      |
     1220      |  whd in EQc1 : (??%%); destruct lapply H @eqb_elim [2: #_ #EQ destruct] #EQ >EQ #_ @i_act_in_map
     1221      ]
     1222    ]
    11951223  | >rewrite_in_dependent_map
    1196      [2: >get_cost_label_append in ⊢ (??%?); >get_cost_label_of_trace_tind in ⊢ (??%?);
    1197          >append_nil in ⊢ (??%?); % |3:]
    1198      %
     1224       [2: >get_cost_label_append in ⊢ (??%?); >get_cost_label_of_trace_tind in ⊢ (??%?);
     1225       >append_nil in ⊢ (??%?); % |3:]
     1226       %
    11991227   ]
    12001228qed.
Note: See TracChangeset for help on using the changeset viewer.