Changeset 3578

Timestamp:

Jul 1, 2015, 11:45:08 PM (4 years ago)

Author:

piccolo

Message:

baco

Location:

LTS

Files:

• imp.ma (modified) (1 diff)
• monostack_to_asm_pass.ma (modified) (5 diffs)
• variable_stack_pass.ma (modified) (1 diff)

LTS/imp.ma

@@ -60 +60 @@
     expr ≡ carr X.
 
-(* ambigous input? why?
+(*
 unification hint  0 ≔ p1,p2; 
     X ≟ DeqExpr

LTS/monostack_to_asm_pass.ma

@@ -94 +94 @@
 qed.
 
-
-
 let rec mono_asm_state_rel_aux (s_stack : list ((ActionLabel flat_labels) × mono_stack_Instructions)) (stack_t : stackT)
 (post_t : list asm_instructions) (t_code : list asm_instructions) (post_t_pc : ℕ) on s_stack : 
@@ -114 +112 @@
                          mono_asm_state_rel_aux tl stack_t post_pc t_code (post_t_pc + |ts_code|) (proj2 … prf)) 
                      ∨
-                     (∃new_pc.option_hd … post_t = return (Ijmp … new_pc) ∧
+                     (∃new_pc.nth_opt … O post_t = return (Ijmp … new_pc) ∧
                       ∃pre_pc,post_pc.t_code = pre_pc @ ts_code @post_pc ∧ (|pre_pc|) = new_pc ∧
                       mono_asm_state_rel_aux tl stack_t post_pc t_code (new_pc + |ts_code|) (proj2 … prf))
@@ -124 +122 @@
 definition mono_asm_state_rel : ∀s_code : mono_stack_Instructions.
 ∀s_stack : list ((ActionLabel flat_labels) × mono_stack_Instructions). 
-ℕ → stackT → list asm_instructions → post_labelled_return_instr … s_code → 
+ℕ → stackT → list asm_instructions → ? → post_labelled_return_instr … s_code → 
 All … (λx.post_labelled_return_instr … (\snd x)) s_stack → Prop ≝  
-λs_code,s_stack,pc,t_stack,t_code,prf1,prf2.
+λs_code,s_stack,pc,t_stack,t_code,init_act,prf1,prf2.
 let 〈ts_code,ret_label〉 ≝ trans_mono_stack_instr s_code pc prf1 in
 ∃pre_pc,post_t.t_code = pre_pc @ ts_code @ post_t ∧ (|pre_pc|) = pc ∧ 
- (All … (λx.let 〈act,code〉 ≝ x in is_cost_label … act → (bool_to_Prop (is_silent_cost_act_b … act))) s_stack) ∧
+∃chop_stack.s_stack = chop_stack @ [〈init_act,EMPTY …〉] ∧
+ (All … (λx.let 〈act,code〉 ≝ x in is_cost_label … act → (bool_to_Prop (is_silent_cost_act_b … act))) chop_stack) ∧
  mono_asm_state_rel_aux s_stack t_stack post_t t_code (pc + |ts_code|) prf2.
- 
+
 definition monostack_asm_pass_rel : 
 ∀prog : Program stack_env_params stack_instr_params flat_labels.
@@ -144 +143 @@
 (mk_relations flat_labels (operational_semantics mono_stack_state_params (mono_stack_sem_state_params bound) prog)
  (asm_operational_semantics … (asm_sem_params) t_prog)
- (λs1,s2.∃s2'.s2 = STATE … s2' ∧ store … s1 = (\fst (asm_store … s2')) ∧ ∃prf1 : post_labelled_return_instr … (code … s1).
-   ∃prf2 : All … (λx.post_labelled_return_instr … (\snd x)) (cont … s1).
-   mono_asm_state_rel (code … s1) (cont … s1) (pc … s2') (asm_stack … s2') (instructions … t_prog) prf1 prf2
+ (λs1,s2.
+   match s2 with
+   [ INITIAL ⇒ bool_to_Prop (lang_initial … (mono_stack_sem_state_params bound) prog s1)
+   | FINAL ⇒ bool_to_Prop (lang_final … s1)
+   | STATE s2' ⇒ store … s1 = (\fst (asm_store … s2')) ∧ ∃prf1 : post_labelled_return_instr … (code … s1).
+                 ∃prf2 : All … (λx.post_labelled_return_instr … (\snd x)) (cont … s1).
+                 mono_asm_state_rel (code … s1) (cont … s1) (pc … s2') (asm_stack … s2') (instructions … t_prog) 
+                   (cost_act … (Some ? (initial_act … prog))) prf1 prf2
+   ]
   )
  (λ_.λ_.True)).
@@ -158 +163 @@
 [4: #s1 #s1' #s2 #H inversion H
   [ #st1 #st2 * #act #instr #tl #EQcode_st1 #EQcont_st1 #EQ1 #EQ2 destruct #EQstore #Hio1 #Hio2
-    #no_ret #EQ1 #EQ2 #EQ3 #EQ4 destruct whd in ⊢ (% → ?); * #st2' ** #EQ destruct #EQstore1
-    * #post_label1 * #post_label2 whd in match mono_asm_state_rel; normalize nodelta lapply post_label1 >EQcode_st1
-    * whd in match (trans_mono_stack_instr ???); normalize nodelta
-    * #pre_pc * #post_t *** #EQinstructions #EQpc lapply post_label2 
-    -post_label2 >EQcont_st1 * #post_code_st2 #post_tail * #_ #Hcont_cost
-    whd in match (mono_asm_state_rel_aux ??????); @pair_elim #t_code_st2 #t_ret_st2 whd in match (length ??);
-    <plus_n_O #EQt_code_st2
+    #no_ret #EQ1 #EQ2 #EQ3 #EQ4 destruct whd in ⊢ (% → ?); cases s1' -s1' normalize nodelta
+    [ whd in match lang_initial; normalize nodelta #H cases(andb_Prop_true … H) -H 
+      #H cases(andb_Prop_true … H) -H #H cases(andb_Prop_true … H) -H #_ inversion(eqb_list ???) [2: #_ *]
+      #ABS @⊥ >EQcont_st1 in ABS; normalize #EQ destruct
+    | whd in match lang_final; normalize nodelta #H cases(andb_Prop_true … H) -H #_ >EQcont_st1 *
+    ]
+    #st2' * #EQstore1 * #post_label1 * #post_label2 whd in match mono_asm_state_rel; normalize nodelta lapply post_label1 
+    >EQcode_st1 * whd in match (trans_mono_stack_instr ???); normalize nodelta
+    * #pre_pc * #post_t ** #EQinstructions #EQpc ** [|#chop_hd #chop_tail] ** 
+    [ >EQcont_st1 in ⊢ (% → ?); | >EQcont_st1 in ⊢ (% → ?); ] whd in ⊢ (??%% → ?); #EQ destruct -EQ
+    * #_ #Hchop_tail >EQcont_st1 in post_label2; * #post_code_st2 #post_tail 
+    whd in match (mono_asm_state_rel_aux ??????); @pair_elim #t_code_st2 #t_ret_st2 
+    whd in match (length ??); <plus_n_O #EQt_code_st2
     * 
     [ * #post_pc1 * #EQ destruct #Haux #class1 #class2 %{(STATE … st2')} %{(t_base …)} % [2: %2 normalize % *]
-      whd %{st2'} % [ %{(refl …)} <EQstore1 //] %{post_code_st2} %{post_tail} whd >EQt_code_st2
-      normalize nodelta %{pre_pc} %{post_pc1} % [ % // % // >EQinstructions %] assumption
-    | cases daemon
-    ]
+      whd  % [ <EQstore1 //] %{post_code_st2} %{post_tail} whd >EQt_code_st2
+      normalize nodelta %{pre_pc} %{post_pc1} % [ % // >EQinstructions %] %{chop_tail} % 
+      [ % //] assumption
+    | * #new_pc * #EQnew_pc * #pre_pc * #post_pc ** #EQinstructions1 #EQ destruct #Hcont #class1 #class2
+      %{(STATE … (mk_vm_state … (|pre_pc|) (asm_stack … st2') (asm_store … st2') (asm_is_io … st2')))}
+      %{(t_ind … (cost_act … (None ?)) … (t_base …))}
+      [ whd <EQpc % [ cases daemon (* BOH!!! *) ] @(vm_ijump … (|pre_pc|)) // [2: cases daemon (* TODO ???*) ]
+      whd in match fetch; normalize nodelta >EQinstructions >nth_second <EQpc [2: //] <minus_n_n assumption ]      
+      % [2: %1 %2 cases daemon ] whd % [ <EQstore //] %{post_code_st2} %{post_tail} whd @pair_elim #p1 #p2 
+      <EQpc in EQt_code_st2; #EQt_code_st2
+      cut (∀a,b,c,c'. trans_mono_stack_instr a b c = trans_mono_stack_instr a b c')
+      [ #a #b #c #d % ] #KK >KK [ <EQt_code_st2
+      
+       #K lapply (trans_eq ???? (sym_eq … EQt_code_st2) K)
+      
+       >EQt_code_st2 in ⊢ (% → ?);
+      normalize nodelta
   |*: cases daemon
   ]

LTS/variable_stack_pass.ma

@@ -203 +203 @@
 qed.
 
-(*
-let rec create_silent_trace_from_eval_combinators (st : (l : list guard_combinators)
-(prf: m_fold Option … eval_combinators l st = return st')
-*)
+definition safe_cast : ∀A,B : Type[0].A = B → A → B ≝ 
+λA,B,prf.match prf with [refl ⇒ λx : A.x]. 
+
+let rec create_silent_trace_from_eval_combinators (prog : Program stack_env_params stack_instr_params flat_labels)
+(bound : ℕ) (st,st' : state stack_state_params) (l : list guard_combinators)  
+on l : 
+ m_fold Option … eval_combinators l (store … st) = return (store … st') → 
+  code … st = list_combinators_to_instructions l (code … st') → 
+  cont … st = cont … st' → io_info … st = io_info … st' → 
+  raw_trace … (operational_semantics stack_state_params (stack_sem_state_params bound) prog) st st' ≝ 
+match l return λx.(m_fold Option … eval_combinators x ? = ? → ? = list_combinators_to_instructions x ? → ?) with
+[ nil ⇒ λprf1,prf2,prf3,prf4.safe_cast (raw_trace … (operational_semantics stack_state_params (stack_sem_state_params bound) prog) st st) 
+     (raw_trace … (operational_semantics stack_state_params (stack_sem_state_params bound) prog) st st') ? (t_base ?? st)
+| cons x xs ⇒ λprf1,prf2,prf3,prf4.
+   let next_store ≝ (opt_safe … (eval_combinators x (store … st)) ?) in
+   let next_st ≝ mk_state stack_state_params (list_combinators_to_instructions xs (code … st')) (cont … st') 
+                   next_store (io_info … st') in 
+   let tail ≝ create_silent_trace_from_eval_combinators prog bound next_st st' xs ? (refl …) (refl …) (refl …) in 
+   t_ind … (cost_act … (None ?)) … tail
+].
+@hide_prf
+[ cases st in prf1 prf2 prf3 prf4; cases st' #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 whd in H9 : (??%%);
+  whd in H10 : (??%%); destruct %
+|4: change with (m_bind ?????) in prf1 :(??%?); cases(bind_inversion ????? prf1) -prf1 #w * #EQw #_ >EQw % 
+   whd in ⊢ (??%% → ?); #EQ destruct
+| whd @seq_sil
+  [4: >prf2 in ⊢ (??%?); % 
+  |8: %
+  |5: change with (eval_combinators ??) in ⊢ (??%?); normalize nodelta @opt_safe_elim #w #H assumption
+  |6: %
+  |7: assumption
+  |9,10: cases daemon (*io*)
+  |*:
+  ]
+| normalize nodelta @opt_safe_elim #w #EQw change with (m_bind ?????) in prf1 :(??%?); >EQw in prf1;
+  >m_return_bind //
+]
+qed.
+
+lemma create_silent_trace_from_eval_combinators_ok : ∀prog,bound,st,st',l,prf1,prf2,prf3,prf4,t.
+create_silent_trace_from_eval_combinators prog bound st st' l prf1 prf2 prf3 prf4 = t → 
+pre_silent_trace … t.
+#prog #bound #st #st' #l lapply st -st lapply st' -st' elim l
+[ * #code' #cont' #store' #io' * #code #cont #store #io whd in ⊢ (??%% → ??%% → ?); #EQ destruct #EQ1 #EQ2 #EQ3 destruct 
+  #t whd in ⊢ (??%% → ?); #EQ destruct % cases daemon (*io*) 
+| #x #xs #IH #st' #st #H cases(bind_inversion ????? H) #w * #EQw #EQstore_st'
+  whd in ⊢ (???% → ?); change with (list_combinators_to_instructions ??) in match (foldr ?????);
+  #prf2 #EQcont #EQio #t whd in ⊢ (??%? → ?); #EQ destruct %2 [cases daemon (* io *)] @IH [|*: %]
+]
+qed.
+
+(*  [ @opt_safe_elim #w' >EQw whd in ⊢ (??%% → ?); #EQ destruct assumption
+  | %
+  | % c'e' un baco????*)
 
 definition simulation_imp_frame :