Changeset 2595 for src/joint/semantics_blocks.ma

Timestamp:

Jan 30, 2013, 7:25:39 PM (7 years ago)

Author:

tranquil

Message:

• dropped locals and exit from definition of joint_if_function
• new definition of blocks to accomodate ERTLptr pass
• stated properties of translation as axioms

File:

• src/joint/semantics_blocks.ma (modified) (4 diffs)

src/joint/semantics_blocks.ma

@@ -2 +2 @@
 include "joint/Traces.ma".
 include "joint/semanticsUtils.ma".
+
+include "common/StatusSimulation.ma". (* for trace_any_any_free *)
 
 (* let rec seq_list_labels p g (b : list (joint_step p g)) on b : list label ≝
@@ -13 +15 @@
   m_fold … (eval_seq_no_pc … (ev_genv … p) curr_id curr_fn).
 
-definition list_not_empty ≝ λA.λl : list A.match l with [ nil ⇒ false | _ ⇒ true ].
+definition taaf_cons : ∀S : abstract_status.∀s1,s2,s3.
+  as_execute S s1 s2 →
+  as_classifier … s1 cl_other →
+  ∀taaf : trace_any_any_free S s2 s3.
+  (if taaf_non_empty … taaf then ¬as_costed … s2 else True) →
+  trace_any_any_free S s1 s3 ≝
+λS,s1,s2,s3,H,I,tl.
+match tl return λs2,s3,tl.
+  as_execute … s1 s2 →
+  if taaf_non_empty … tl then ¬as_costed … s2 else True →
+  trace_any_any_free S s1 s3 
+with
+[ taaf_base s2 ⇒ λH.λ_.taaf_step … (taa_base …) H I
+| taaf_step s2 s3 s4 taa H' I' ⇒
+  λH,J.taaf_step … (taa_step … H I J taa) H' I'
+| taaf_step_jump s2 s3 s4 taa H' I' K' ⇒
+  λH,J.taaf_step_jump … (taa_step ???? H I J taa) H' I' K'
+] H.
 
-let rec produce_trace_any_any
+lemma taaf_cons_non_empty : ∀S,s1,s2,s3,H,I,tl,J.
+bool_to_Prop (taaf_non_empty … (taaf_cons S s1 s2 s3 H I tl J)).
+#S #s1 #s2 #s3 #H #I #tl lapply H -H cases tl
+[ #s #H * % |*: #s2 #s3 #s4 #taa #H' #I' [2: #K'] #H #J % ]
+qed.
+
+let rec produce_trace_any_any_free_aux
   (p : evaluation_params)
   (st : state_pc p)
@@ -26 +51 @@
     return 〈curr_id, curr_fn〉 →
   let src ≝ point_of_pc p (pc … st) in
-  if list_not_empty ? b then
-    ! x ← stmt_at ?? (joint_if_code … curr_fn) dst ; cost_label_of_stmt … x = None ?
-  else
-    True →
+  (* disambiguation: select 3rd (step list in code) *)
   src ~❨b, l❩~> dst in joint_if_code … curr_fn →
-  All ? (λx.And (no_call … x) (no_cost_label … x)) b →
+  All ? (no_cost_label …) b →
   repeat_eval_seq_no_pc p curr_id curr_fn b st = return st' →
-  trace_any_any (joint_abstract_status p) st
-    (mk_state_pc ? st' (pc_of_point p (pc_block (pc … st)) dst)) ≝  match b
-  return λb.∀l,dst.?→?→?→?→?→?→?
+  Σtaaf : trace_any_any_free (joint_abstract_status p) st
+    (mk_state_pc ? st' (pc_of_point p (pc_block (pc … st)) dst) (last_pop … st)).
+  (not_empty … b ↔ bool_to_Prop (taaf_non_empty … taaf)) ≝
+  match b
+  return λb.∀l,dst.?→?→?→?→?→ Σtaaf.(not_empty ? b ↔ bool_to_Prop (taaf_non_empty … taaf))
   with
   [ nil ⇒
-    λl,dst,st',fd_prf,dst_prf,in_code,all_other,EQ1.
-    (taa_base (joint_abstract_status p) st)
-    ⌈trace_any_any ??? ↦ ?⌉
+    λl,dst,st',fd_prf,in_code,all_other,EQ1.
+    «taaf_base (joint_abstract_status p) st
+    ⌈trace_any_any_free ??? ↦ ?⌉,?»
   | cons hd tl ⇒
     λl.
-    match l return λx.∀dst,st'.?→?→?→?→?→? with
-    [ nil ⇒ λdst,st',fd_prf,dst_prf,in_code.⊥
+    match l return λx.∀dst,st'.?→?→?→?→Σtaaf.(True ↔ bool_to_Prop (taaf_non_empty … taaf)) with
+    [ nil ⇒ λdst,st',fd_prf,in_code.⊥
     | cons mid rest ⇒
-      λdst,st',fd_prf,dst_prf,in_code,all_other,EQ1.
+      λdst,st',fd_prf,in_code,all_other,EQ1.
       let mid_pc ≝ pc_of_point p (pc_block (pc … st)) mid in
       match eval_seq_no_pc … (ev_genv p) curr_id curr_fn hd st
       return λx.eval_seq_no_pc … (ev_genv p) curr_id curr_fn hd st = x →
-      trace_any_any (joint_abstract_status p) st
-        (mk_state_pc ? st' (pc_of_point p (pc_block (pc … st)) dst)) with
-      [ Value st_mid ⇒ λEQ2.
-        let tr_tl ≝ produce_trace_any_any ?
-            (mk_state_pc ? st_mid mid_pc)
-            curr_id curr_fn tl rest dst ?????? in
-        taa_step … tr_tl
+      Σtaaf : trace_any_any_free (joint_abstract_status p) st
+        (mk_state_pc ? st' (pc_of_point p (pc_block (pc … st)) dst) (last_pop … st)).
+        (True ↔ bool_to_Prop (taaf_non_empty … taaf)) with
+      [ OK st_mid ⇒ λEQ2.
+        let tr_tl ≝ produce_trace_any_any_free_aux ?
+            (mk_state_pc ? st_mid mid_pc (last_pop … st))
+            curr_id curr_fn tl rest dst ????? in
+        «taaf_cons … tr_tl ?,?»
       | _ ⇒ λEQ2.⊥
       ] (refl …)
     ]
-  ].
-[ whd in EQ1 : (??%%);
-  cases l in in_code; whd in ⊢ (%→?); [2: #hd #tl * ] #EQ destruct
-  >pc_of_point_of_pc cases st //
+  ]. @hide_prf
+[1,2: [2: % [*] generalize in ⊢ (?(???? (match % with [ _ ⇒ ?])) → ?); ]
+  whd in EQ1 : (??%%);
+  cases l in in_code; whd in ⊢ (%→?); [2,4: #hd #tl * ] #EQ destruct
+  >pc_of_point_of_pc cases st // #a #b #c #e >(K ?? e) normalize nodelta *
 | @in_code
-|3,12: whd in EQ1 : (??%%); >EQ2 in EQ1; whd in ⊢ (??%?→?); #EQ1 destruct(EQ1)
+|12: whd in EQ1 : (??%%); >EQ2 in EQ1; whd in ⊢ (??%?→?); #EQ1 destruct(EQ1)
+|4: cases tr_tl -tr_tl #tr_tl cases tl in in_code all_other;
+  [ #_ #_ * #_ cases (taaf_non_empty ????)
+    [ #ABS cases (ABS I) | #_ % ]
+  | #hd' #tl' ** #nxt * #EQstmt_at #EQ_nxt cases rest [*] #mid' #rest' *
+    * #nxt' * #EQstmt_at' #EQ_nxt' #_ * #hd_other * #hd_other'
+    #_ * #H #_ >(H I) % whd in ⊢ (%→?);
+    whd in ⊢ (?(??%?)→?); whd in match (as_pc_of ??);
+    >fetch_statement_eq [2: whd in match point_of_pc;
+    normalize nodelta >point_of_offset_of_point @EQstmt_at' |3: @fd_prf |*:]
+    normalize nodelta
+    >(no_label_uncosted … hd_other') * #ABS @ABS %
+  ]
+|7: % [2: #_ %] * @taaf_cons_non_empty
 ]
 change with (! y ← ? ; repeat_eval_seq_no_pc ????? = ?) in EQ1;
 >EQ2 in EQ1; >m_return_bind
 cases in_code -in_code * #nxt * #EQ_stmt_at #EQ_mid #rest_in_code
-cases all_other -all_other * #hd_no_call #hd_no_cost #tl_other
+cases all_other -all_other #hd_no_cost #tl_other
 #EQ1
 try assumption
-[ whd whd in match eval_state; normalize nodelta
+[2: whd whd in match eval_state; normalize nodelta
   >(fetch_statement_eq … fd_prf EQ_stmt_at)
   >m_return_bind
@@ -79 +118 @@
   >EQ2 >m_return_bind
   whd in match eval_statement_advance; normalize nodelta
-  >(no_call_advance … hd_no_call)
   whd in match next; normalize nodelta 
   whd in match succ_pc; normalize nodelta
   >EQ_mid %
-| whd whd in ⊢ (??%?);
-  >(fetch_statement_eq … fd_prf EQ_stmt_at) normalize nodelta
-  @(no_call_other … hd_no_call)
-| whd in ⊢ (?%);
-  whd in match as_label; normalize nodelta
-  %* #H @H -H whd in ⊢ (??%?);
-  whd in match (as_pc_of ??);
-  inversion (fetch_statement ????) normalize nodelta
-  [2: // ]
-  ** #i' #f' #stmt' #EQ
-  elim (fetch_statement_inv … EQ)
-  >fd_prf
-  whd in ⊢ (??%?→?); #EQ destruct(EQ)
-  whd in ⊢ (%→?);
-  whd in match (point_of_pc ??); >point_of_offset_of_point
-  #EQ'
-  cases tl in tl_other rest_in_code;
-  [ * cases rest [2: #hd' #tl' * ] whd in ⊢ (%→?); #EQ destruct(EQ)
-    >EQ' in dst_prf; >m_return_bind #H @H
-  | #hd' #tl' ** #_ #hd_no_cost' #_
-    cases rest [ * ] #mid' #rest' * * #nxt' * #EQ_stmt_at' #EQ_mid' #_
-    >EQ_stmt_at' in EQ'; #EQ' destruct(EQ')
-    @(no_label_uncosted … hd_no_cost')
-  ]
-| >dst_prf cases (list_not_empty ??) %
-| normalize nodelta >point_of_pc_of_point assumption
+|1: whd whd in ⊢ (??%?);
+  >(fetch_statement_eq … fd_prf EQ_stmt_at) normalize nodelta %
+|3: normalize nodelta >point_of_pc_of_point assumption
 ]
 qed.
+
+definition produce_trace_any_any_free :
+  ∀p : evaluation_params.
+  ∀st : state_pc p.
+  ∀curr_id,curr_fn.
+  ∀b : list (joint_seq p (globals p)).
+  ∀l : list (code_point p).
+  ∀dst : code_point p.
+  ∀st' : state p.
+  fetch_internal_function … (ev_genv p) (pc_block (pc … st)) =
+    return 〈curr_id, curr_fn〉 →
+  let src ≝ point_of_pc p (pc … st) in
+  (* disambiguation: select 3rd (step list in code) *)
+  src ~❨b, l❩~> dst in joint_if_code … curr_fn →
+  All ? (no_cost_label …) b →
+  repeat_eval_seq_no_pc p curr_id curr_fn b st = return st' →
+  trace_any_any_free (joint_abstract_status p) st
+    (mk_state_pc ? st' (pc_of_point p (pc_block (pc … st)) dst) (last_pop … st)) ≝
+  λp,st,curr_id,curr_fn,b,l,dst,st',prf1,prf2,prf3,prf4.
+  produce_trace_any_any_free_aux p st curr_id curr_fn b l dst st' prf1 prf2 prf3 prf4.