Changeset 2666 for src/ERTLptr/ERTLtoERTLptrOK.ma

Timestamp:

Feb 14, 2013, 11:49:48 AM (7 years ago)

Author:

piccolo

Message:

bug fixed in blocks.ma

File:

• src/ERTLptr/ERTLtoERTLptrOK.ma (modified) (9 diffs)

src/ERTLptr/ERTLtoERTLptrOK.ma

@@ -1878 +1878 @@
 qed.
 
+lemma fetch_internal_function_no_minus_one :
+∀F,V,i,p,bl.
+  block_id (pi1 … bl) = -1 →
+  fetch_internal_function ?
+  
+  (globalenv (λvars.fundef (F vars)) V i p) bl = 
+  Error ? [MSG BadFunction].
+#F #V #i #p #bl #EQbl whd in match fetch_internal_function; 
+normalize nodelta >fetch_function_no_minus_one [2: assumption] %
+qed.
+
 lemma fetch_statement_no_zero : 
 ∀pars,prog,stack_size,pc.
@@ -1887 +1898 @@
 >fetch_internal_function_no_zero [2: assumption] %
 qed.
+
+lemma fetch_statement_no_minus_one : 
+∀pars,prog,stack_size,pc.
+block_id(pi1 … (pc_block pc)) = -1 →
+fetch_statement pars (prog_var_names … prog) 
+(ev_genv (mk_prog_params pars prog stack_size)) pc = 
+Error ? [MSG BadFunction].
+#pars #vars #ge #pc #EQpc whd in match fetch_statement; normalize nodelta
+>fetch_internal_function_no_minus_one [2: assumption] %
+qed.
+
+
 
 lemma foo :
@@ -1918 +1941 @@
  luniverse_ok … fn → 
  ∀stmt,nxt.
+ ∀P : (state_pc P2_sem) → Prop.
  (∀pre_Instrs',last_Instrs',dst.
    ∃st''.∃st'''.∃st''''.
@@ -1926 +1950 @@
     st'' = (mk_state_pc (mk_prog_params P2_sem trans_prog stack_size)
      st'''' (pc_of_point P2_sem (pc_block (pc … (sigma_state_pc st))) dst) (last_pop … st)) ∧ 
-    st' = sigma_state_pc st'' ∧
+    P st'' (*st' = sigma_state_pc st''*) ∧
     let P2_prog_params ≝ mk_prog_params P2_sem trans_prog stack_size in
     let P2_globals ≝ globals P2_prog_params in 
@@ -1943 +1967 @@
  (sigma_state_pc st) = return st' → 
  ∃st''. (*CSC: this needs to be linked back again st' = sigma_state_pc ? good st'' ∧*)
+ P st'' ∧
  ∃taf : trace_any_any_free (joint_abstract_status (mk_prog_params P2_sem trans_prog stack_size)) st st''.
- True (* the length of taf is the same of the length of ??? *).
+(if taaf_non_empty … taf then True else 
+(¬as_costed (joint_abstract_status (mk_prog_params P1_sem prog stack_size)) (sigma_state_pc st) ∨ 
+ ¬as_costed (joint_abstract_status (mk_prog_params P1_sem prog stack_size)) st')) 
+ (* the length of taf is the same of the length of ??? *).
 #P1_unser #P2_unser #P1_sem_unser #P2_sem_unser
 letin P1_sem ≝ (make_sem_graph_params P1_unser P1_sem_unser)
@@ -1958 +1986 @@
 #prog
 letin trans_prog ≝ (transform_program ??? prog (λvarnames. transf_fundef ?? (translate_internal varnames)))
-#stack_size #sigma_state_pc #sigma_state_pc_ok #st #st' #f #fn #fn_universe_ok #stmt #nxt #Hpass 
-#EQfetch lapply(fetch_statement_inv … EQfetch) * #EQfn #EQstmt
+#stack_size #sigma_state_pc #sigma_state_pc_ok #st #st' #f #fn #fn_universe_ok #stmt #nxt #P 
+#Hpass #EQfetch lapply(fetch_statement_inv … EQfetch) * #EQfn #EQstmt
 cases
  (b_graph_translate_ok … (init …) (translate_step …) (translate_fin_step …) … fn_universe_ok)
@@ -2025 +2053 @@
                       second one to be taken from somewhere *)
 |4: #x cases daemon (* TO BE DONE, EASY *)
-|5: cases daemon (* to be taken in input *) ]
-[2: cases daemon
-| #st'' * #taaf #_ %{st''}
-  change with ERTL_uns in match (mk_unserialized_params ???????????????);
+|5: cases daemon (* to be taken in input *)
+|6: @(λst''.st' = sigma_state_pc ? good st'')
+|7: cases daemon
+| #st'' * #EQ destruct * change with ERTL_uns in match (mk_unserialized_params ???????????????);
   change with ERTLptr_uns in match (mk_unserialized_params ???????????????);
-  change with ERTL_semantics in match (make_sem_graph_params ??);
-  change with ERTLptr_semantics in match (make_sem_graph_params ??);
-
-
+  (* change with ERTL_semantics in match (make_sem_graph_params ??);
+  change with ERTLptr_semantics in match (make_sem_graph_params ??); *)
+#taaf #Htaaf %{st''}
+ % [%] cases daemon
+ qed.
+
+lemma lookup_opt_none_transf :
+∀prog : ertl_program.
+let trans_prog ≝ ertl_to_ertlptr prog in
+∀x.lookup_opt
+    (fundef
+     (joint_closed_internal_function ERTL
+      (prog_var_names (joint_function ERTL) ℕ prog))) x
+     (functions
+       (fundef
+        (joint_closed_internal_function ERTL
+         (prog_var_names (joint_function ERTL) ℕ prog)))
+       (globalenv_noinit (joint_function ERTL) prog)) =None ? →
+lookup_opt
+    (fundef
+     (joint_closed_internal_function ERTLptr
+      (prog_var_names (joint_function ERTLptr) ℕ trans_prog))) x
+     (functions
+       (fundef
+        (joint_closed_internal_function ERTLptr
+         (prog_var_names (joint_function ERTLptr) ℕ trans_prog)))
+       (globalenv_noinit (joint_function ERTLptr) trans_prog)) =None ?.
+#prog #x #EQlookup 
+whd in match ertl_to_ertlptr in ⊢ (??(???(??%))?); whd in match transform_program; 
+whd in match transf_program; normalize nodelta whd in match globalenv_noinit; 
+whd in match globalenv; whd in match globalenv_allocmem; 
+whd in match add_globals; normalize nodelta
+cases daemon
+qed.
+
+ 
+ 
+lemma fetch_function_none :
+∀prog : ertl_program.
+let trans_prog ≝ ertl_to_ertlptr prog in
+∀bl.
+fetch_function
+        (fundef
+         (joint_closed_internal_function ERTL
+          (prog_var_names (joint_function ERTL) ℕ prog)))
+        (globalenv_noinit (joint_function ERTL) prog) bl = Error ? [MSG BadFunction] → 
+fetch_function
+        (fundef
+         (joint_closed_internal_function ERTLptr
+          (prog_var_names (joint_function ERTLptr) ℕ trans_prog)))
+        (globalenv_noinit (joint_function ERTLptr) trans_prog) bl = Error ? [MSG BadFunction].
+#prog #bl whd in match fetch_function in ⊢ (% → ?); normalize nodelta
+<(symbol_for_block_transf … (λn:ℕ.[Init_space n]) prog … 
+                         (λvars.transf_fundef … (translate_internal …)) bl)
+change with (symbol_for_block 
+              (fundef 
+                (joint_closed_internal_function ERTLptr 
+                  (prog_var_names (joint_function ERTLptr) ℕ (ertl_to_ertlptr prog))))
+               (globalenv_noinit (joint_function ERTLptr) (ertl_to_ertlptr prog)) bl)
+               in match (symbol_for_block ???);
+whd in match fetch_function; normalize nodelta cases(symbol_for_block ???) [#_ %]
+#id >m_return_bind inversion(find_funct_ptr ???) 
+[2: #x #_ whd in ⊢ (??%% → ?); #EQ destruct] whd in match find_funct_ptr;
+normalize nodelta cases(block_region bl) normalize nodelta [ #_ #_ >m_return_bind %]
+cases(block_id bl) normalize nodelta [1,2: [2: #x] #_ #_ >m_return_bind %]
+#x whd in match globalenv_noinit; whd in match globalenv; normalize nodelta 
+whd in match globalenv_allocmem; normalize nodelta #EQlookup
+>(lookup_opt_none_transf … EQlookup) #_ %
+qed.
+
+lemma fetch_function_err :
+∀F,ge,bl,e. fetch_function F ge bl = Error ? e → e = [MSG BadFunction].
+#F #ge #bl #e whd in match fetch_function; normalize nodelta
+cases(symbol_for_block ???) [ normalize #EQ destruct %]
+#id >m_return_bind cases(find_funct_ptr ???) normalize [2: #x] 
+#EQ destruct %
+qed.
+
+ 
+lemma fetch_internal_function_none :
+∀ prog : ertl_program.
+let trans_prog ≝ ertl_to_ertlptr prog in
+∀bl.
+fetch_internal_function
+   (joint_closed_internal_function ERTL
+    (prog_var_names (joint_function ERTL) ℕ prog))
+   (globalenv_noinit (joint_function ERTL) prog) bl = Error ? [MSG BadFunction] →
+fetch_internal_function
+   (joint_closed_internal_function ERTLptr
+    (prog_var_names (joint_function ERTLptr) ℕ trans_prog))
+   (globalenv_noinit (joint_function ERTLptr) trans_prog) bl = Error ? [MSG BadFunction].
+#prog #bl whd in match fetch_internal_function; normalize nodelta
+inversion(fetch_function ???) 
+[2: #err_msg #EQfetch lapply(fetch_function_err … EQfetch) #EQ destruct #_
+    >(fetch_function_none … EQfetch) %] * #f * #fn #EQfetch >m_return_bind
+normalize nodelta whd in ⊢ (??%? → ?); #EQ destruct
+>(fetch_function_transf … (λvars.transf_fundef … (translate_internal …)) … EQfetch)
+>m_return_bind %
+qed.
+ 
+lemma fetch_internal_function_err :
+∀F,ge,bl,e. fetch_internal_function F ge bl = Error ? e → e = [MSG BadFunction].
+#F #ge #bl #e whd in match fetch_internal_function; normalize nodelta
+inversion(fetch_function ???) 
+[2: #e #EQf lapply(fetch_function_err … EQf) #EQ destruct whd in ⊢ (??%? → ?);
+    #EQ destruct %] * #id * #fn #EQf >m_return_bind normalize nodelta 
+whd in ⊢ (??%? → ?); #EQ destruct %
+qed.
+
+ 
+   
+  
+lemma as_label_ok : ∀ prog : ertl_program.
+let trans_prog ≝ ertl_to_ertlptr prog in
+∀ good,stack_sizes,st.
+as_label (ERTLptr_status trans_prog stack_sizes) st = as_label 
+(ERTL_status prog stack_sizes) (sigma_state_pc prog good st).
+#prog #good #stack_size #st whd in match as_label; normalize nodelta
+whd in match (as_pc_of ? ?); whd in match (as_pc_of ? ?);
+whd in match sigma_state_pc; normalize nodelta @if_elim
+[ @eqZb_elim [2: #_ *] #EQbl * whd in match (as_label_of_pc ??);
+  >fetch_statement_no_minus_one [2: assumption] normalize nodelta
+  whd in match (as_label_of_pc ??); >fetch_statement_no_zero [2: %] %]
+#_ inversion(fetch_internal_function ???)
+[2: #e #EQf lapply(fetch_internal_function_err … EQf) #EQ destruct normalize nodelta
+    whd in match (as_label_of_pc ??); whd in match fetch_statement; normalize nodelta
+    >(fetch_internal_function_none … EQf) whd in ⊢ (??%%); 
+    >fetch_statement_no_zero [2: %] % ] * #f #fn #EQf normalize nodelta
+whd in match (as_label_of_pc ??) in ⊢ (???%); whd in match fetch_statement;
+normalize nodelta >EQf >m_return_bind inversion(stmt_at ????) [cases daemon (*to discuss with Paolo*)]
+* [ * [ * [ #id | #addr ] #args #dst | #acc_r #lbl | #seq ] #nxt | #fin | *] 
+#EQstmt_at >m_return_bind normalize nodelta 
+cases(multi_fetch_ok … (good fn) … EQstmt_at) 
+#labs * #regs ** #EQlabs #EQregs normalize nodelta whd in match translate_step;
+normalize nodelta
+[1,3,4: * #step_block * whd in match (bind_new_instantiates ?????); 
+        cases regs in EQregs; [2,4,6: #r #tl #EQ normalize nodelta *]
+        #EQregs normalize nodelta #EQ destruct * #dst * 
+        whd in match (step_list_in_code ???????); cases labs in EQlabs;
+        [2,4,6: #lb #tl #EQ normalize nodelta *] #EQlabs normalize nodelta
+        #EQ destruct * #nxt1 * #EQ_s_stmt #EQ destruct
+        whd in match (as_label_of_pc ??); whd in match fetch_statement;
+        normalize nodelta 
+        >(fetch_internal_function_transf … (λvars.translate_internal …) … EQf)
+        >m_return_bind >EQ_s_stmt >m_return_bind normalize nodelta [1,2: %]
+        cases seq
+        [#str % | #c % | #H1 % | #H3 % | #x % | #H5 #H6 #H7 #H8 % 
+        | #H10 #H11 #H12 #H13 #H14 % | #H16 #H17 #H18 % | #H20 #H21 #H22 #H23 %
+        | % | % | #H25 #H26 #H27 % | #H29 #H30 #H31 % | #H33 %]
+| * #step_block whd in match (bind_new_instantiates ?????);
+  cases regs in EQregs; [ #EQ normalize nodelta **] #reg #tl #EQregs
+  normalize nodelta whd in match (bind_new_instantiates ?????);
+  cases tl in EQregs; [2: #reg1 #tl1 #EQ normalize nodelta **]
+  #EQreg normalize nodelta * #EQ destruct * #dst * 
+  whd in match (step_list_in_code ???????); cases labs in EQlabs;
+  [ #_ normalize nodelta *] #lbl #tl #EQlabs normalize nodelta *
+  * #nxt1 * #EQ_s_stmt #_ #_ #_ whd in match (as_label_of_pc ??); 
+  whd in match fetch_statement; normalize nodelta
+   >(fetch_internal_function_transf … (λvars.translate_internal …) … EQf)
+   >m_return_bind >EQ_s_stmt >m_return_bind normalize nodelta %
+| (whd in match translate_fin_step; normalize nodelta) *
+  #fin_block * whd in match (bind_new_instantiates ?????); cases regs in EQregs;
+  [2: #r #tl #_ normalize nodelta *] #EQregs normalize nodelta #EQ destruct
+  * #list_l * #lbl ** #EQ destruct whd in match (step_list_in_code ???????); 
+  normalize nodelta cases list_l in EQlabs; [2: #lbl1 #tl #_ normalize nodelta *]
+  #EQlabs normalize nodelta #EQ destruct whd in match fin_step_in_code;
+  normalize nodelta #EQ_s_stmt whd in match (as_label_of_pc ??); 
+   whd in match fetch_statement; normalize nodelta
+   >(fetch_internal_function_transf … (λvars.translate_internal …) … EQf)
+   >m_return_bind >EQ_s_stmt >m_return_bind normalize nodelta %
+]
+qed.
+
+(*
 #H1 #H2 #H3 *
 
@@ -2147 +2345 @@
 
 
-qed.
+qed.*)
 
 lemma ertl_to_ertlptr_ok:
@@ -2173 +2371 @@
 | (*seq*) whd in match joint_classify; normalize nodelta >EQfetch >m_return_bind
           normalize nodelta cases (eval_seq_no_call_ok ?????????  EQfetch EQeval)
-  #st3 * #EQ destruct *  #taf #tafne %{st3} %{taf} >tafne normalize nodelta
-  % [% //] whd >as_label_ok [2:assumption] %
+          #st3 * #EQ destruct *  #taf #tafne %{st3} %{taf} >tafne normalize nodelta
+          % [% //] whd >as_label_ok [2:assumption] %