Changeset 3449 for LTS

Timestamp:

Feb 20, 2014, 10:59:25 AM (6 years ago)

Author:

piccolo

Message:

clean up

Location:

LTS

Files:

• Common.ma (deleted)
• Imp.ma (deleted)
• Language.ma (modified) (8 diffs)
• Simulation.ma (modified) (1 diff)
• StaticAnalysis.ma (deleted)
• Vm.ma (modified) (4 diffs)

LTS/Language.ma

@@ -85 +85 @@
 ].
 
+
 (*
 lemma eq_instructions_elim : ∀ P : bool → Prop.∀p,i1,i2.(i1 = i2 → P true) → 
@@ -95 +96 @@
   [|*: #x #y #z [2,3: #w1 #w2 [#w3] |4,5: #w1]] #_ #H2 @H2 % #EQ
   lapply (eq_to_jmeq ??? EQ) #EQ' destruct(EQ')
-| cases daemon (*TODO*)
-qed.
+| #seq * [| #lbl] #i #IH * normalize
+  [1,8: |2,9: #t_t |3,10: #seq1 #opt_l #i2 |4,11: #cond #ltrue #i_t #lfalse #i_f #i_c
+  |5,12: #cond #ltrue #i_t #lfalse #i_f |6,13: #f #act_p #ret #i3 |*: #lin #io #lout #i3]
+  #H1 #H2 try(@H2 % #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct)
+  inversion(?==?) normalize nodelta
+  [2,4: #ABS @H2 % #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct
+        >(\b (refl …)) in ABS; #EQ destruct]
+  #EQseq inversion(eq_instructions ???) normalize nodelta #Heq_i2
+  [2,4: @H2 % #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct
 *)
 
@@ -150 +158 @@
 ].
 
-definition is_ret_act : ActionLabel → Prop ≝ 
-λa.match a with [ret_act _ ⇒ True | _ ⇒ False ].
+definition is_ret_call_act : ActionLabel → Prop ≝ 
+λa.match a with [ret_act _ ⇒ True | call_act _ _ ⇒ True | _ ⇒ False ].
 
 inductive execute_l (p : state_params) (p' : sem_state_params p) (env : list (env_item p p)) : 
@@ -157 +165 @@
 | empty : ∀st,st',hd,tl.(code ? st) = (EMPTY p)→ (cont ? st) = hd :: tl → 
            (code ? st') = \snd hd → (cont … st') = tl → (store … st) = (store … st') → 
-           (io_info … st = true → is_non_silent_cost_act (\fst hd)) →  (io_info … st') = false → ¬ is_ret_act (\fst hd) →  execute_l … (\fst hd) st st'
+           (io_info … st = true → is_non_silent_cost_act (\fst hd)) →  (io_info … st') = false → ¬ is_ret_call_act (\fst hd) →  execute_l … (\fst hd) st st'
 | seq_sil : ∀st,st',i,cd,s,opt_l.(code ? st) = SEQ … i opt_l cd → 
              eval_seq … p' i (store … st) = return s → (code ? st') = cd → 
@@ -2428 +2436 @@
   ]
 | #st1 #st2 #st3 #st4 #st5 #l1 #l2 #H inversion H in ⊢ ?;
-  [1,2,3,4,5,6,7,9: cases daemon (*assurdi*) ]
+  [1,2,3,4,5,6,7,9: 
+    [ #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 #x15 #x16
+    | #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 #x15 #x16 #x17
+    | #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 #x15 #x16 #x17 #x18 #x19 #x20
+    | #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 #x15 #x16 #x17 #x18 #x19 #x20   
+    | #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 #x15 #x16 #x17 #x18 #x19
+    | #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 #x15 #x16 #x17 #x18 #x19
+    | #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 #x15 #x16 #x18
+    | #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 #x15 #x16 #x18 #x19 #x20
+    ]
+    destruct #t1 #t2 #prf #_ #_ * #y1 * #y2 #EQ destruct(EQ) @⊥ >EQ in x12; * #H @H %
+  ]
   #st11 #st12 #f #act_p #opt_l #i #mem #env_it #EQcode11 #EQenv_it #EQmem
   #EQ destruct(EQ) #EQcode12 #EQcont12 #EQio11 #EQio12 #EQ1 #EQ2 #EQ3 
   destruct(EQ1 EQ2 EQ3) #EQ destruct(EQ) #t1 #t2 #H inversion H in ⊢ ?;
-  [1,2,3,4,5,6,7,8: cases daemon (*assurdi*) ]
+  [1,2,3,4,5,6,7,8: 
+    [ #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 #x15 #x16
+    | #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 #x15 #x16 #x17
+    | #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 #x15 #x16 #x17 #x18 #x19 #x20
+    | #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 #x15 #x16 #x17 #x18 #x19 #x20   
+    | #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 #x15 #x16 #x17 #x18 #x19
+    | #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 #x15 #x16 #x17 #x18 #x19
+    | #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 #x15 #x16 #x18
+    | #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 #x15 #x16 #x18 #x19 #x20 #x21
+    ]
+    destruct #_ #_ #_ #_ #_ #_ #_ whd in ⊢ (% → ?); #EQ destruct(EQ)
+    @⊥ >EQ in x12; * #H @H %
+  ]
    #st41 #st42 #r_t #mem1 #new_cont #opt_l1 #cd #EQcode41 #EQcont41 #EQ destruct(EQ)
    #EQio41 #EQio42 #EQmem1 #EQ1 #EQ2 #EQ3 #EQ4 #EQ5 #EQ6 destruct #st11_noio 
@@ -2443 +2474 @@
     #abs_top_cont #abs_tail_cont #EQcheck
     normalize nodelta **** #HH1 >EQcode11 in ⊢ (% → ?); inversion(code … st1')
-    [1,2,3,4,5,7: (*assurdi da fare*) cases daemon] #f' #act_p' #opt_l' #i' #_
+    [1,2,3,4,5,7:
+     [ #_ whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
+     | #r_t #_ whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) 
+     | #seq #lbl #i #_ #_ whd in ⊢ (??%% → ?); cases(call_post_clean ?????)
+       normalize nodelta [2: * #z1 #z2 cases lbl normalize nodelta 
+       [2: #l1 cases(?==?) normalize nodelta]]
+       whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
+     | #cond #ltrue #i1 #lfalse #i2 #i3 #_ #_ #_ #_
+            whd in ⊢ (??%% → ?); cases(call_post_clean ?????)
+            [2,4: * #z1 #z2 normalize nodelta cases (call_post_clean ?????)
+                [2,4: * #z3 #z4 >m_return_bind cases(call_post_clean ?????)
+                     [2,4: * #z5 #z6 >m_return_bind cases(?∧?) normalize nodelta ]]] 
+            whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
+     | #cond #ltrue #i1 #lfalse #i2 #_ #_ #_
+       whd in ⊢ (??%% → ?); cases(call_post_clean ?????)
+       [2,4: * #z1 #z2 normalize nodelta cases (call_post_clean ?????)
+       [2,4: * #z3 #z4 >m_return_bind cases(?∧?) normalize nodelta ]] 
+       whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
+     | #lin #io #lout #i #_ #_ whd in ⊢ (??%% → ?); cases(call_post_clean ?????)
+             normalize nodelta
+             [2,4: * #z1 #z2 cases(?∧?) normalize nodelta]
+             whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
+     ]
+    ] #f' #act_p' #opt_l' #i' #_
     #EQcode_st1' #EQclean #EQstore #EQio #EQ destruct(EQ)
     lapply(trans_env_ok … no_dup) >EQtrans normalize nodelta #H
@@ -2488 +2542 @@
      normalize nodelta inversion(call_post_clean ?????) normalize nodelta
      [ #_ whd in ⊢ (??%% → ?); #EQ destruct ***** ] * #abs_top'''' #i'''
-     #EQ_clean_i'' inversion(act_lbl) normalize nodelta [1,3,4: cases daemon (*assurdi*)]
+     #EQ_clean_i'' inversion(act_lbl) normalize nodelta 
+     [1,3,4:
+       [ #x1 #x2 #EQ whd in ⊢ (??%% → ?); #EQ1 destruct *****
+       | * [|#x1] #EQ destruct normalize nodelta whd in ⊢ (??%% → ?);
+         #EQ destruct ****** [2: *] #EQ destruct
+       | #EQ whd in ⊢ (??%% → ?); #EQ1 destruct *****
+       ]
+     ]
      cut(act_lbl = ret_act (Some ? lbl') ∧ cont_st42' = cont … st1' ∧ i'' = i') 
      [ cases(stack_safety1 [ ] …)
@@ -2499 +2560 @@
      whd in ⊢ (??%% → ?); #EQ destruct ****** #_ #HH3 #EQ destruct(EQ)
      >EQcode41 in ⊢ (% → ?); inversion(code … st41') 
-     [1,3,4,5,6,7: cases daemon (*ASSURDI*) ] #r_t' #EQcode_st41' whd in ⊢ (??%% → ?);
+     [1,3,4,5,6,7:
+       [ #_ whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) 
+       | #seq #lbl #i #_ #_ whd in ⊢ (??%% → ?); cases(call_post_clean ?????)
+         normalize nodelta [2: * #z1 #z2 cases lbl normalize nodelta 
+         [2: #l1 cases(?==?) normalize nodelta]]
+         whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
+       | #cond #ltrue #i1 #lfalse #i2 #i3 #_ #_ #_ #_
+            whd in ⊢ (??%% → ?); cases(call_post_clean ?????)
+            [2,4: * #z1 #z2 normalize nodelta cases (call_post_clean ?????)
+                [2,4: * #z3 #z4 >m_return_bind cases(call_post_clean ?????)
+                     [2,4: * #z5 #z6 >m_return_bind cases(?∧?) normalize nodelta ]]] 
+            whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
+       | #cond #ltrue #i1 #lfalse #i2 #_ #_ #_
+         whd in ⊢ (??%% → ?); cases(call_post_clean ?????)
+         [2,4: * #z1 #z2 normalize nodelta cases (call_post_clean ?????)
+         [2,4: * #z3 #z4 >m_return_bind cases(?∧?) normalize nodelta ]] 
+         whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
+       | #f #act_p #lbl #i #_ #_ whd in ⊢ (??%% → ?); cases(call_post_clean ?????)
+             normalize nodelta 
+             [2,4: * #z1 #z2 cases lbl normalize nodelta
+               [2,4: #l1 cases(memb ???) normalize nodelta
+                 [1,3: cases(?==?) normalize nodelta ]]]
+            whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
+       | #lin #io #lout #i #_ #_ whd in ⊢ (??%% → ?); cases(call_post_clean ?????)
+             normalize nodelta
+             [2,4: * #z1 #z2 cases(?∧?) normalize nodelta]
+             whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
+       ]   
+     ] #r_t' #EQcode_st41' whd in ⊢ (??%% → ?);
      #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) #EQstore_st41' #EQinfo_st41'
      #EQ destruct(EQ) >EQcont11_42 in EQcheck; >EQ_contst42 in ⊢ (% → ?);

LTS/Simulation.ma

@@ -1 @@
-include "Common.ma".
 include "Traces.ma".
 

LTS/Vm.ma

@@ -3 +3 @@
 include "../src/utilities/option.ma".
 include "basics/jmeq.ma".
+
+lemma bind_inversion : ∀A,B : Type[0].∀m : option A.
+∀f : A → option B.∀y : B.
+! x ← m; f x = return y → 
+∃ x.(m = return x) ∧ (f x = return y).
+#A #B * [| #a] #f #y normalize #EQ [destruct]
+%{a} %{(refl …)} //
+qed.
 
 record monoid: Type[1] ≝
@@ -56 +64 @@
 definition label_of_pc ≝ λL.λl.λpc.find … 
    (λp.let 〈x,y〉 ≝ p in if eqb x pc then Some L y else None ? ) l.
+   
+definition option_pop ≝ 
+  λA.λl:list A. match l with
+  [ nil ⇒ None ?
+  | cons a tl ⇒ Some ? (〈a,tl〉) ].
 
 
@@ -143 +156 @@
            op … (cost … st1) (cost_of p p' (Iret p)) = cost … st2 → 
            vmstep … (ret_act (Some ? lbl)) st1 st2.
-           
+
+definition eval_vmstate : ∀p : assembler_params.∀p' : sem_params p. 
+AssemblerProgram p → vm_state p p' → option (ActionLabel × (vm_state p p')) ≝ 
+λp,p',prog,st.
+! i ← fetch … prog (pc … st);
+match i with
+[ Seq x opt_l ⇒ 
+   if asm_is_io … st then
+     None ?
+   else 
+     ! new_store ← eval_asm_seq p p' x (asm_store … st);
+     return 〈cost_act opt_l,
+             mk_vm_state ?? (S (pc … st)) (asm_stack … st) new_store false
+                (op … (cost … st) (cost_of p p' (Seq p x opt_l)))〉
+| Ijmp newpc ⇒ 
+   if asm_is_io … st then
+     None ?
+   else
+     return 〈cost_act (None ?),
+             mk_vm_state ?? newpc (asm_stack … st) (asm_store … st) false
+                (op … (cost … st) (cost_of p p' (Ijmp … newpc)))〉
+| CJump cond newpc ltrue lfalse ⇒ 
+   if asm_is_io … st then
+     None ?
+   else
+     ! b ← eval_asm_cond p p' cond (asm_store … st);
+     if b then
+       return 〈cost_act (Some ? ltrue),
+               mk_vm_state ?? newpc (asm_stack … st) (asm_store … st) false
+                (op … (cost … st) (cost_of p p' (CJump … cond newpc ltrue lfalse)))〉
+     else
+       return 〈cost_act (Some ? lfalse),
+               mk_vm_state ?? (S (pc … st)) (asm_stack … st) (asm_store … st) false
+                (op … (cost … st) (cost_of p p' (CJump … cond newpc ltrue lfalse)))〉
+| Iio lin io lout ⇒ 
+              if asm_is_io … st then 
+                 ! new_store ← eval_asm_io … io (asm_store … st);
+                 return 〈cost_act (Some ? lout),
+                         mk_vm_state ?? (S (pc … st)) (asm_stack … st) 
+                         new_store false
+                         (op … (cost … st) 
+                               (cost_of_io p p' io (asm_store … st)))〉    
+              else 
+                return 〈cost_act (Some ? lin),
+                        mk_vm_state ?? (pc … st) (asm_stack … st) (asm_store … st)
+                                    true (cost … st)〉
+| Icall f ⇒ 
+    if asm_is_io … st then
+      None ?
+    else
+      ! lbl ← label_of_pc ? (call_label_fun p) (entry_of_function p f);
+      return 〈call_act f lbl,
+              mk_vm_state ?? (entry_of_function p f) 
+                             ((S (pc … st)) :: (asm_stack … st))
+                             (asm_store … st) false
+                             (op … (cost … st) (cost_of p p' (Icall p f)))〉
+| Iret ⇒ if asm_is_io … st then
+            None ?
+         else
+            ! 〈newpc,tl〉 ← option_pop … (asm_stack … st);
+            ! lbl ← label_of_pc ? (return_label_fun p) newpc;
+            return 〈ret_act (Some ? lbl),
+                    mk_vm_state ?? newpc tl (asm_store … st) false   
+                     (op … (cost … st) (cost_of p p' (Iret p)))〉
+].
+
+lemma eval_vmstate_to_Prop : ∀p,p',prog,st1,st2,l.
+eval_vmstate p p' prog st1 = return 〈l,st2〉 → vmstep … prog l st1 st2.
+#p #p' #prog #st1 #st2 #l whd in match eval_vmstate; normalize nodelta
+#H cases(bind_inversion ????? H) -H * normalize nodelta
+[ #seq #opt_l * #EQfetch inversion(asm_is_io ???) normalize nodelta
+  [ #_ whd in ⊢ (??%% → ?); #EQ destruct] #EQio #H cases(bind_inversion ????? H)
+  #newstore * #EQnewstore whd in ⊢ (??%% → ?); #EQ destruct
+  @vm_seq //
+| #newpc * #EQfetch inversion(asm_is_io ???) normalize nodelta #EQio
+  [ whd in ⊢ (??%% → ?); #EQ destruct] whd in ⊢ (??%% → ?); #EQ destruct
+  @vm_ijump //
+| #cond #new_pc #ltrue #lfase * #EQfetch inversion(asm_is_io ???) normalize nodelta
+  [ #_ whd in ⊢ (??%% → ?); #EQ destruct] #EQio #H cases(bind_inversion ????? H) -H
+  * normalize nodelta * #EQcond whd in ⊢ (??%% → ?); #EQ destruct
+  [ @(vm_cjump_true … EQfetch) // | @(vm_cjump_false … EQfetch) //]
+| #lin #io #lout * #EQfetch inversion(asm_is_io ???) normalize nodelta #EQio
+  [ #H cases(bind_inversion ????? H) -H #newstore * #EQnewstore ]
+  whd in ⊢ (??%% → ?); #EQ destruct
+  [ @(vm_io_out … EQfetch) // | @(vm_io_in … EQfetch) // ]
+| #f * #EQfetch inversion(asm_is_io ???) #EQio normalize nodelta
+  [ whd in ⊢ (??%% → ?); #EQ destruct ] #H cases (bind_inversion ????? H) -H
+  #lbl * #EQlb whd in ⊢ (??%% → ?); #EQ destruct @(vm_call … EQfetch) //
+| * #EQfetch inversion(asm_is_io ???) normalize nodelta #EQio
+  [ whd in ⊢ (??%% → ?); #EQ destruct] #H cases(bind_inversion ????? H) -H
+  * #newpc #tl * whd in match option_pop; normalize nodelta inversion(asm_stack ???)
+  normalize nodelta [#_ whd in ⊢ (??%% → ?); #EQ destruct] #newpc1 #tl1 #_
+  #EQstack whd in ⊢ (??%% → ?); #EQ destruct #H cases(bind_inversion ????? H) #lbl
+  * #EQlbl whd in ⊢ (??%% → ?); #EQ destruct @vm_ret //
+]
+qed.
+
 include "../src/utilities/hide.ma".
 
@@ -325 +434 @@
  }.
  
-lemma bind_inversion : ∀A,B : Type[0].∀m : option A.
-∀f : A → option B.∀y : B.
-! x ← m; f x = return y → 
-∃ x.(m = return x) ∧ (f x = return y).
-#A #B * [| #a] #f #y normalize #EQ [destruct]
-%{a} %{(refl …)} //
-qed.
-
 lemma static_dynamic : ∀p,p',prog,k,mT,map.
 static_analisys p p' mT prog = return map →