Changeset 2555

Timestamp:

Dec 14, 2012, 12:40:37 AM (8 years ago)

Author:

piccolo

Message:

lemma eval_call_ok finished

File:

• src/joint/lineariseProof.ma (modified) (2 diffs)

src/joint/lineariseProof.ma

@@ -2147 +2147 @@
 qed.
 
+lemma block_of_call_sigma_commute : 
+∀p,p',graph_prog,sigma.
+∀gss : good_state_sigma p p' graph_prog sigma.∀cl.
+ preserving … res_preserve …
+   (sigma_state p p' graph_prog sigma gss)
+   (λx.λ_ : True .x)
+   (block_of_call (make_sem_graph_params p p') … 
+      (globalenv_noinit ? graph_prog) cl)   
+   (block_of_call (make_sem_lin_params p p') … 
+      (globalenv_noinit ? (linearise ? graph_prog)) cl).
+#p #p' #graph_prog #sigma #gss #cl #st #prf 
+@mfr_bind
+[3: cases cl
+  [ #id normalize nodelta @opt_to_res_preserve
+    >(find_symbol_transf …
+          (λvars.transf_fundef … (λfn.\fst (linearise_int_fun … fn))) graph_prog id)
+   #s #EQs %{I} >EQs in ⊢ (??%?); %
+  | * #dpl #dph normalize nodelta
+    @mfr_bind [3: @dpl_arg_retrieve_commute |*:]
+    #bv1 #bv1_prf
+    @mfr_bind [3: @dph_arg_retrieve_commute |*:]
+    #bv2 #bv2_prf
+    @(mfr_bind … (λptr.λ_:True.ptr))
+    [ lapply bv2_prf lapply bv2 lapply bv1_prf lapply bv1
+      @bv_pc_other
+      [ #pc1 #p #bv1_prf #bv2 #bv2_prf @res_preserve_error ]
+      #bv1 #bv1_no_pc #bv1_prf
+      @bv_pc_other
+      [ cases bv1 in bv1_prf;
+        [||#a #b #c| #a | #a | #a #b | #a #b ] #bv1_prf
+        #pc2 #p #bv2_prf @res_preserve_error ]
+      #bv2 #bv2_no_pc #bv2_prf
+      >sigma_bv_no_pc try assumption
+      >sigma_bv_no_pc try assumption
+      whd #ptr #EQ %{I EQ}
+   ] #ptr *
+   @if_elim #_ [ @mfr_return | @res_preserve_error ] %
+ ]
+|4: #bl * @opt_to_res_preserve #x #EQ %{I} @EQ
+|*:
+]
+qed.
+
+    
 lemma eval_call_ok :
  ∀p,p',graph_prog.
  let lin_prog ≝ linearise p graph_prog in
  ∀stack_sizes.
- ∀sigma.∀gss : good_state_sigma p p' graph_prog sigma.
+ ∀sigma. good_sigma p graph_prog sigma → 
+ ∀gss : good_state_sigma p p' graph_prog sigma.
  ∀st,st',f,fn,called,args,dest,nxt.
  ∀prf : well_formed_state_pc … gss st.
-  fetch_statement (make_sem_lin_params p p') …
-    (globalenv_noinit ? lin_prog) (pc … (sigma_state_pc … st prf)) =
-      return 〈f, \fst (linearise_int_fun … fn),
-        sequential … (CALL (mk_lin_params p) … called args dest ) it〉 →
+  fetch_statement (make_sem_graph_params p p') …
+    (globalenv_noinit ? graph_prog) (pc … st) =
+      return 〈f, fn,
+        sequential … (CALL (mk_graph_params p) … called args dest ) nxt〉 →
    eval_seq_advance ?? (ev_genv … (graph_prog_params … graph_prog stack_sizes))
       (CALL … called args dest) nxt st = return st' →
@@ -2181 +2226 @@
   eval_state … (ev_genv … (lin_prog_params … (linearise … graph_prog) stack_sizes))
     st2_pre_call = return st2_after_call.
-cases daemon
-qed.
-
+#p #p' #graph_prog #stack_sizes #sigma #good #gss #st #st1 #f #fn 
+#called #args #dest #nxt #prf #fetch_spec 
+cases(fetch_statement_sigma_commute … good (proj1 … prf) … fetch_spec) #_
+normalize nodelta * #lin_fetch_spec #_
+whd in match eval_seq_advance; whd in match eval_seq_call; normalize nodelta
+@('bind_inversion) #bl #H lapply (err_eq_from_io ????? H) -H #bl_spec
+@('bind_inversion) * #id #int_f #H lapply (err_eq_from_io ????? H) -H
+cases int_f -int_f [ #fn | #ext_f] #int_f_spec normalize nodelta 
+[2:#H @('bind_inversion H) -H #st' #H #_ @('bind_inversion H) -H #vals #_
+  @'bind_inversion #vals' #_ whd in ⊢ (??%%→?); #ABS destruct(ABS) ]
+#H %
+[  @hide_prf 
+  whd in match joint_classify; normalize nodelta >fetch_spec >m_return_bind
+  normalize nodelta whd in match joint_classify_step; 
+  whd in match joint_classify_seq; normalize nodelta
+  >bl_spec >m_return_bind >int_f_spec normalize nodelta %
+| %
+  [ @hide_prf whd in match joint_classify; normalize nodelta >lin_fetch_spec
+    >m_return_bind normalize nodelta whd in match joint_classify_step; 
+    whd in match joint_classify_seq; normalize nodelta
+    cases bl in bl_spec int_f_spec; #reg #reg_prf -bl #reg_spec #int_f_spec 
+    cases(block_of_call_sigma_commute p p' graph_prog sigma gss ?? (proj2 … prf) ? 
+            reg_spec)
+    * #EQ >EQ -EQ >m_return_bind
+    lapply(fetch_function_transf ?????
+      (λvars.transf_fundef … (λf_in.\fst(linearise_int_fun ?? f_in))) ????) 
+        [ 
+        | @(Internal ? fn)
+        | @id 
+        | assumption assumption 
+        | 
+        |
+        | % 
+          [@(prog_vars … graph_prog)  
+          |@(prog_funct … graph_prog) 
+          |@(prog_main … graph_prog) 
+          ]
+        ]
+      [>int_f_spec % | | |] #EQ >EQ normalize nodelta % 
+   | %
+     [2: %
+         [  change with ((λx.joint_call_ident (lin_prog_params p p' (linearise p graph_prog) stack_sizes)
+              (mk_Sig ? ? ? x)) ? = (λx.joint_call_ident ? (mk_Sig ? ? ? x)) ?)
+            whd in match joint_call_ident in ⊢ (??(%?)?); normalize nodelta in ⊢ (??(%?)?); 
+            whd in match (pc ?); >lin_fetch_spec in ⊢ (??(%?)?); normalize nodelta in ⊢ (??%?);
+            whd in match joint_call_ident in ⊢ (???(%?)); normalize nodelta in ⊢ (???(%?)); 
+            >fetch_spec in ⊢ (???(%?)); normalize nodelta >bl_spec in ⊢ (???%);
+            >m_return_bind in ⊢ (???%);
+         |  whd in match eval_state; normalize nodelta 
+            >lin_fetch_spec in ⊢ (??%?); >m_return_bind in ⊢ (??%?);
+             whd in match eval_statement_no_pc; normalize nodelta 
+             whd in match eval_seq_no_pc; normalize nodelta 
+             >m_return_bind in ⊢ (??%?);
+             whd in match eval_statement_advance; whd in match eval_seq_advance; 
+             whd in match eval_seq_call; normalize nodelta
+         ]
+         cases(block_of_call_sigma_commute p p' graph_prog sigma gss ?? (proj2 … prf) ? 
+             bl_spec) * #EQ >EQ in ⊢ (??%?); >m_return_bind in ⊢ (??%?); -EQ 
+         [ whd in match fetch_internal_function; normalize nodelta >int_f_spec in ⊢ (???%);
+           >m_return_bind in ⊢ (???%); normalize nodelta ]
+         lapply(fetch_function_transf ?????
+                (λvars.transf_fundef … (λf_in.\fst(linearise_int_fun ?? f_in))) ????)
+            [ 
+            | 2,12: @(Internal ? fn)
+            | 3,13: @id 
+            | 4,14: assumption assumption 
+            | 5,15:
+            | 6,16:
+            |7,17: % 
+               [1,4: @(prog_vars … graph_prog)  
+               |2,5: @(prog_funct … graph_prog) 
+               |3,6: @(prog_main … graph_prog) 
+               ]
+            ]
+         [1,5: >int_f_spec % |*:] #EQ >EQ in ⊢ (??%?); -EQ 
+          >m_return_bind in ⊢ (??%?); normalize nodelta [ %]
+      ]
+  ]
+]
+[2: @hide_prf] 
+lapply (err_eq_from_io ????? H) -H #H @('bind_inversion H)
+#st' #st_spec' #H @('bind_inversion H) -H #st'' #st_spec'' 
+whd in ⊢ (??%% → ?); #EQ destruct(EQ) [ % ]
+[2,3: elim(save_frame_commute p p' graph_prog sigma gss … prf … st_spec')
+      #wf_st' #sigma_st_spec' [2: >sigma_st_spec' in ⊢ (??%?); >m_return_bind in ⊢ (??%?);]
+      lapply st_spec'' -st_spec''  whd in match eval_internal_call; normalize nodelta 
+      #H @('bind_inversion H) -H #dim_s #dim_s_spec #H 
+      [ >dim_s_spec in ⊢ (??%?); >m_return_bind in ⊢ (??%?);]
+      elim(bind_inversion ????? H) -H #st''' * #st_spec'''
+      elim(setup_call_commute p p' graph_prog sigma gss … wf_st' … st_spec''')
+      #wf_st''' #sigma_st_spec''' whd in ⊢ (??%% → ?); 
+      whd in match allocate_locals; whd in match set_regs; normalize nodelta 
+      #EQ destruct(EQ)
+]
+[  >sigma_st_spec''' in ⊢ (??%?); >m_return_bind in ⊢ (??%?);
+   whd in match sigma_state_pc; normalize nodelta
+   change with (return mk_state_pc (make_sem_lin_params p p') ? ? = ?)
+   cut(∀A,semp,pc,pc',st,st'.∀ f : ? → A.pc = pc' ∧ st = st' → 
+          f(mk_state_pc semp st pc) = f(mk_state_pc semp st' pc'))
+   [#A #H1 #H2 #H3 #H4 #H5 #f * #H8 #H9 //]
+   #APP @APP %
+]
+[1,4: [whd in match sigma_pc; normalize nodelta @opt_safe_elim #lin_pc | whd in match well_formed_pc;]
+      whd in match sigma_pc_opt; normalize nodelta @if_elim 
+      [1,3: @eqZb_elim [2,4: #_ *] #EQbl cases bl in EQbl int_f_spec; *
+            #reg #pos #reg_prf normalize in ⊢ (% → ?);
+            #EQbl whd in match fetch_function; normalize nodelta
+            >EQbl cases(symbol_for_block ???) 
+            [1,3: whd in ⊢ (??%% → ?); #ABS destruct(ABS)]
+            #id1 >m_return_bind inversion(find_funct_ptr ???) 
+            [1,3:#_ whd in ⊢ (??%% → ?); #ABS destruct(ABS)]
+            #z lapply(globalenv_no_minus_one ??? graph_prog) [1,3: @(λn.[Init_space n])]
+            #EQ  
+            change with ((find_funct_ptr ? (globalenv_noinit ? graph_prog) ? = ?) → ?)
+            change with ((find_funct_ptr ? (globalenv_noinit ? graph_prog) ? = ?)) in EQ;
+            cases reg in ⊢ (% → ?); 
+            [1,3: whd in match find_funct_ptr; normalize nodelta #ABS destruct(ABS)
+            |2,4: >EQ #ABS destruct(ABS)
+            ]
+      |2,4: #_ whd in match fetch_internal_function; normalize nodelta
+            whd in match (pc_block ?); >int_f_spec >m_return_bind
+             >point_of_pc_of_point lapply(good fn) ** #EQ #_ #_ >EQ -EQ 
+              >m_return_bind [2:%] whd in ⊢ (??%? → ?); #EQ destruct(EQ)
+              %
+      ]
+| whd in match sigma_state; normalize nodelta 
+  cut(∀A,semp,fr,fr',is,is',c,c',r,r',m,m'.∀ f : ? → A.
+      fr = fr' ∧ is = is' ∧ c = c' ∧ r = r' ∧ m = m'→ 
+          f(mk_state semp fr is c r m) = f(mk_state semp fr' is' c' r' m'))
+  [#A #semp #fr #fr' #is #is' #c #c' #r #r' #m #m' #f **** //]
+  #APP @APP % [% [% [% [%]]]] // [whd in match sigma_is; normalize nodelta % |3:
+  whd in match sigma_mem; normalize nodelta %]
+|  % [2:  @(proj2 … wf_st')] % [  %  [ @(proj1 … (proj1 … (proj1 … wf_st'))) | 
+          @(proj2 … (proj1 … (proj1 … wf_st')))] ]
+]
+[ change with (? = (λx.sigma_regs ? ? ? ? ? (foldr ? ? ? ? x) ?)?)
+  [ cut((joint_if_locals (lin_prog_params p p' (linearise p graph_prog) stack_sizes)
+   (globals (lin_prog_params p p' (linearise p graph_prog) stack_sizes))
+   (\fst  (linearise_int_fun p
+                (globals (graph_prog_params p p' graph_prog stack_sizes)) fn))) = (joint_if_locals (graph_prog_params p p' graph_prog stack_sizes)
+   (globals (graph_prog_params p p' graph_prog stack_sizes)) fn))
+   [%] #EQ >EQ 
+    elim(joint_if_locals (graph_prog_params p p' graph_prog stack_sizes)
+     (globals (graph_prog_params p p' graph_prog stack_sizes)) fn) in ⊢ (??%(?%));
+  | @hide_prf elim x
+  ]
+| @hide_prf elim(joint_if_locals (graph_prog_params p p' graph_prog stack_sizes)
+     (globals (graph_prog_params p p' graph_prog stack_sizes)) fn)
+]
+[3,5: whd in match (foldr ? ? ???); @(proj2 … (proj1 … wf_st'))
+|4,6: #locs_t #tl_list #wf_regs_tail whd in match (foldr ? ? ???);
+      elim(allocate_locals_commute p p' graph_prog sigma gss locs_t 
+               ? wf_regs_tail) #wf_regs_locs_t #_ assumption
+|*: normalize nodelta
+    [  whd in match (foldr ? ? ???) in ⊢ (??%%); %
+    | #locs_t #tl_list #EQtl whd in match (foldr ?????) in ⊢ (??%%);
+      >EQtl
+      lapply(allocate_locals_commute p p' graph_prog sigma gss locs_t 
+        (foldr (localsT ?) (regsT ?) (allocate_locals_ ???) (regs ? st') tl_list) ?)
+      [2: * #x #H >H % |]
+    ]
+]
+qed.          
+                
 lemma eval_goto_ok :
-lemma eval_tailcall_ok :
+lemma eval_tailcall_ok 
+ :
 lemma eval_cond_cond_ok :
 lemma eval_cond_fcond_ok :