Changeset 3505

Timestamp:

Sep 26, 2014, 4:58:21 PM (6 years ago)

Author:

piccolo

Message:

 

File:

• LTS/Vm.ma (modified) (2 diffs)

LTS/Vm.ma

@@ -1126 +1126 @@
  mem … 〈c1,pc p p' st1〉
   (labels_pc … (instructions … prog) (call_label_fun … prog)
-   (return_label_fun … prog) (in_act … prog) O).
+   (return_label_fun … prog) (in_act … prog) O). 
+#p #p' #prog #st0 #st1 #l1 #c1 #EQc1 #H lapply(vm_step_to_eval … H) -H
+#H cases(bind_inversion ????? H); #i * #EQi #Hi cases(step_emit … EQi H)
+[ #c2 whd in match actionlabel_to_costlabel in EQc1; normalize nodelta in EQc1;
+  >EQc1 * #EQ destruct // ]
+cases i in Hi;        
+[ #seq * [|#lbl1]
+| #newpc
+| #cond #newpc #ltrue #lfalse
+| #lin #io #lout
+| #f
+|
+]
+normalize nodelta cases(asm_is_io ??) normalize nodelta 
+[1,3,5,7,11,13: whd in ⊢ (??%% → ?); #EQ destruct
+|2,4,8,9,12,14: #H cases(bind_inversion ????? H) -H #x * #_
+  [3: cases x normalize nodelta
+  |6: #H cases(bind_inversion ????? H) -H #y *  #_
+  ]
+]
+whd in ⊢ (??%% → ?); #EQ destruct try % normalize in EQc1; destruct
+qed.
+
 theorem static_dynamic :
 (* Given an assembly program *)
@@ -1190 +1212 @@
       [ normalize in ⊢ (??%%); >neutral_l @EQact
       |
-      | check nth_opt
-  
-  cases daemon
+      | @execute_mem_label_pc //
+      ]
+    | #H #EQ destruct #_ whd in match get_pc; normalize nodelta 
+      <(proj1 ?? (static_analisys_ok … EQmap …))
+      [ normalize in ⊢ (??%%); >neutral_l @EQact
+      |
+      |  whd in EQc1 : (??%%); destruct lapply H @eqb_elim [2: #_ #EQ destruct] #EQ >EQ #_ @i_act_in_map
+      ]
+    ]
   | >rewrite_in_dependent_map
-     [2: >get_cost_label_append in ⊢ (??%?); >get_cost_label_of_trace_tind in ⊢ (??%?);
-         >append_nil in ⊢ (??%?); % |3:]
-     %
+       [2: >get_cost_label_append in ⊢ (??%?); >get_cost_label_of_trace_tind in ⊢ (??%?);
+       >append_nil in ⊢ (??%?); % |3:]
+       %
    ]
 qed.