Ignore:
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:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/semantics_blocks.ma

    r2529 r2595  
    22include "joint/Traces.ma".
    33include "joint/semanticsUtils.ma".
     4
     5include "common/StatusSimulation.ma". (* for trace_any_any_free *)
    46
    57(* let rec seq_list_labels p g (b : list (joint_step p g)) on b : list label ≝
     
    1315  m_fold … (eval_seq_no_pc … (ev_genv … p) curr_id curr_fn).
    1416
    15 definition list_not_empty ≝ λA.λl : list A.match l with [ nil ⇒ false | _ ⇒ true ].
     17definition taaf_cons : ∀S : abstract_status.∀s1,s2,s3.
     18  as_execute S s1 s2 →
     19  as_classifier … s1 cl_other →
     20  ∀taaf : trace_any_any_free S s2 s3.
     21  (if taaf_non_empty … taaf then ¬as_costed … s2 else True) →
     22  trace_any_any_free S s1 s3 ≝
     23λS,s1,s2,s3,H,I,tl.
     24match tl return λs2,s3,tl.
     25  as_execute … s1 s2 →
     26  if taaf_non_empty … tl then ¬as_costed … s2 else True →
     27  trace_any_any_free S s1 s3
     28with
     29[ taaf_base s2 ⇒ λH.λ_.taaf_step … (taa_base …) H I
     30| taaf_step s2 s3 s4 taa H' I' ⇒
     31  λH,J.taaf_step … (taa_step … H I J taa) H' I'
     32| taaf_step_jump s2 s3 s4 taa H' I' K' ⇒
     33  λH,J.taaf_step_jump … (taa_step ???? H I J taa) H' I' K'
     34] H.
    1635
    17 let rec produce_trace_any_any
     36lemma taaf_cons_non_empty : ∀S,s1,s2,s3,H,I,tl,J.
     37bool_to_Prop (taaf_non_empty … (taaf_cons S s1 s2 s3 H I tl J)).
     38#S #s1 #s2 #s3 #H #I #tl lapply H -H cases tl
     39[ #s #H * % |*: #s2 #s3 #s4 #taa #H' #I' [2: #K'] #H #J % ]
     40qed.
     41
     42let rec produce_trace_any_any_free_aux
    1843  (p : evaluation_params)
    1944  (st : state_pc p)
     
    2651    return 〈curr_id, curr_fn〉 →
    2752  let src ≝ point_of_pc p (pc … st) in
    28   if list_not_empty ? b then
    29     ! x ← stmt_at ?? (joint_if_code … curr_fn) dst ; cost_label_of_stmt … x = None ?
    30   else
    31     True →
     53  (* disambiguation: select 3rd (step list in code) *)
    3254  src ~❨b, l❩~> dst in joint_if_code … curr_fn →
    33   All ? (λx.And (no_call … x) (no_cost_label … x)) b →
     55  All ? (no_cost_label …) b →
    3456  repeat_eval_seq_no_pc p curr_id curr_fn b st = return st' →
    35   trace_any_any (joint_abstract_status p) st
    36     (mk_state_pc ? st' (pc_of_point p (pc_block (pc … st)) dst)) ≝  match b
    37   return λb.∀l,dst.?→?→?→?→?→?→?
     57  Σtaaf : trace_any_any_free (joint_abstract_status p) st
     58    (mk_state_pc ? st' (pc_of_point p (pc_block (pc … st)) dst) (last_pop … st)).
     59  (not_empty … b ↔ bool_to_Prop (taaf_non_empty … taaf)) ≝
     60  match b
     61  return λb.∀l,dst.?→?→?→?→?→ Σtaaf.(not_empty ? b ↔ bool_to_Prop (taaf_non_empty … taaf))
    3862  with
    3963  [ nil ⇒
    40     λl,dst,st',fd_prf,dst_prf,in_code,all_other,EQ1.
    41     (taa_base (joint_abstract_status p) st)
    42     ⌈trace_any_any ??? ↦ ?⌉
     64    λl,dst,st',fd_prf,in_code,all_other,EQ1.
     65    «taaf_base (joint_abstract_status p) st
     66    ⌈trace_any_any_free ??? ↦ ?⌉,?»
    4367  | cons hd tl ⇒
    4468    λl.
    45     match l return λx.∀dst,st'.?→?→?→?→?→? with
    46     [ nil ⇒ λdst,st',fd_prf,dst_prf,in_code.⊥
     69    match l return λx.∀dst,st'.?→?→?→?→Σtaaf.(True ↔ bool_to_Prop (taaf_non_empty … taaf)) with
     70    [ nil ⇒ λdst,st',fd_prf,in_code.⊥
    4771    | cons mid rest ⇒
    48       λdst,st',fd_prf,dst_prf,in_code,all_other,EQ1.
     72      λdst,st',fd_prf,in_code,all_other,EQ1.
    4973      let mid_pc ≝ pc_of_point p (pc_block (pc … st)) mid in
    5074      match eval_seq_no_pc … (ev_genv p) curr_id curr_fn hd st
    5175      return λx.eval_seq_no_pc … (ev_genv p) curr_id curr_fn hd st = x →
    52       trace_any_any (joint_abstract_status p) st
    53         (mk_state_pc ? st' (pc_of_point p (pc_block (pc … st)) dst)) with
    54       [ Value st_mid ⇒ λEQ2.
    55         let tr_tl ≝ produce_trace_any_any ?
    56             (mk_state_pc ? st_mid mid_pc)
    57             curr_id curr_fn tl rest dst ?????? in
    58         taa_step … tr_tl
     76      Σtaaf : trace_any_any_free (joint_abstract_status p) st
     77        (mk_state_pc ? st' (pc_of_point p (pc_block (pc … st)) dst) (last_pop … st)).
     78        (True ↔ bool_to_Prop (taaf_non_empty … taaf)) with
     79      [ OK st_mid ⇒ λEQ2.
     80        let tr_tl ≝ produce_trace_any_any_free_aux ?
     81            (mk_state_pc ? st_mid mid_pc (last_pop … st))
     82            curr_id curr_fn tl rest dst ????? in
     83        «taaf_cons … tr_tl ?,?»
    5984      | _ ⇒ λEQ2.⊥
    6085      ] (refl …)
    6186    ]
    62   ].
    63 [ whd in EQ1 : (??%%);
    64   cases l in in_code; whd in ⊢ (%→?); [2: #hd #tl * ] #EQ destruct
    65   >pc_of_point_of_pc cases st //
     87  ]. @hide_prf
     88[1,2: [2: % [*] generalize in ⊢ (?(???? (match % with [ _ ⇒ ?])) → ?); ]
     89  whd in EQ1 : (??%%);
     90  cases l in in_code; whd in ⊢ (%→?); [2,4: #hd #tl * ] #EQ destruct
     91  >pc_of_point_of_pc cases st // #a #b #c #e >(K ?? e) normalize nodelta *
    6692| @in_code
    67 |3,12: whd in EQ1 : (??%%); >EQ2 in EQ1; whd in ⊢ (??%?→?); #EQ1 destruct(EQ1)
     93|12: whd in EQ1 : (??%%); >EQ2 in EQ1; whd in ⊢ (??%?→?); #EQ1 destruct(EQ1)
     94|4: cases tr_tl -tr_tl #tr_tl cases tl in in_code all_other;
     95  [ #_ #_ * #_ cases (taaf_non_empty ????)
     96    [ #ABS cases (ABS I) | #_ % ]
     97  | #hd' #tl' ** #nxt * #EQstmt_at #EQ_nxt cases rest [*] #mid' #rest' *
     98    * #nxt' * #EQstmt_at' #EQ_nxt' #_ * #hd_other * #hd_other'
     99    #_ * #H #_ >(H I) % whd in ⊢ (%→?);
     100    whd in ⊢ (?(??%?)→?); whd in match (as_pc_of ??);
     101    >fetch_statement_eq [2: whd in match point_of_pc;
     102    normalize nodelta >point_of_offset_of_point @EQstmt_at' |3: @fd_prf |*:]
     103    normalize nodelta
     104    >(no_label_uncosted … hd_other') * #ABS @ABS %
     105  ]
     106|7: % [2: #_ %] * @taaf_cons_non_empty
    68107]
    69108change with (! y ← ? ; repeat_eval_seq_no_pc ????? = ?) in EQ1;
    70109>EQ2 in EQ1; >m_return_bind
    71110cases in_code -in_code * #nxt * #EQ_stmt_at #EQ_mid #rest_in_code
    72 cases all_other -all_other * #hd_no_call #hd_no_cost #tl_other
     111cases all_other -all_other #hd_no_cost #tl_other
    73112#EQ1
    74113try assumption
    75 [ whd whd in match eval_state; normalize nodelta
     114[2: whd whd in match eval_state; normalize nodelta
    76115  >(fetch_statement_eq … fd_prf EQ_stmt_at)
    77116  >m_return_bind
     
    79118  >EQ2 >m_return_bind
    80119  whd in match eval_statement_advance; normalize nodelta
    81   >(no_call_advance … hd_no_call)
    82120  whd in match next; normalize nodelta
    83121  whd in match succ_pc; normalize nodelta
    84122  >EQ_mid %
    85 | whd whd in ⊢ (??%?);
    86   >(fetch_statement_eq … fd_prf EQ_stmt_at) normalize nodelta
    87   @(no_call_other … hd_no_call)
    88 | whd in ⊢ (?%);
    89   whd in match as_label; normalize nodelta
    90   %* #H @H -H whd in ⊢ (??%?);
    91   whd in match (as_pc_of ??);
    92   inversion (fetch_statement ????) normalize nodelta
    93   [2: // ]
    94   ** #i' #f' #stmt' #EQ
    95   elim (fetch_statement_inv … EQ)
    96   >fd_prf
    97   whd in ⊢ (??%?→?); #EQ destruct(EQ)
    98   whd in ⊢ (%→?);
    99   whd in match (point_of_pc ??); >point_of_offset_of_point
    100   #EQ'
    101   cases tl in tl_other rest_in_code;
    102   [ * cases rest [2: #hd' #tl' * ] whd in ⊢ (%→?); #EQ destruct(EQ)
    103     >EQ' in dst_prf; >m_return_bind #H @H
    104   | #hd' #tl' ** #_ #hd_no_cost' #_
    105     cases rest [ * ] #mid' #rest' * * #nxt' * #EQ_stmt_at' #EQ_mid' #_
    106     >EQ_stmt_at' in EQ'; #EQ' destruct(EQ')
    107     @(no_label_uncosted … hd_no_cost')
    108   ]
    109 | >dst_prf cases (list_not_empty ??) %
    110 | normalize nodelta >point_of_pc_of_point assumption
     123|1: whd whd in ⊢ (??%?);
     124  >(fetch_statement_eq … fd_prf EQ_stmt_at) normalize nodelta %
     125|3: normalize nodelta >point_of_pc_of_point assumption
    111126]
    112127qed.
     128
     129definition produce_trace_any_any_free :
     130  ∀p : evaluation_params.
     131  ∀st : state_pc p.
     132  ∀curr_id,curr_fn.
     133  ∀b : list (joint_seq p (globals p)).
     134  ∀l : list (code_point p).
     135  ∀dst : code_point p.
     136  ∀st' : state p.
     137  fetch_internal_function … (ev_genv p) (pc_block (pc … st)) =
     138    return 〈curr_id, curr_fn〉 →
     139  let src ≝ point_of_pc p (pc … st) in
     140  (* disambiguation: select 3rd (step list in code) *)
     141  src ~❨b, l❩~> dst in joint_if_code … curr_fn →
     142  All ? (no_cost_label …) b →
     143  repeat_eval_seq_no_pc p curr_id curr_fn b st = return st' →
     144  trace_any_any_free (joint_abstract_status p) st
     145    (mk_state_pc ? st' (pc_of_point p (pc_block (pc … st)) dst) (last_pop … st)) ≝
     146  λp,st,curr_id,curr_fn,b,l,dst,st',prf1,prf2,prf3,prf4.
     147  produce_trace_any_any_free_aux p st curr_id curr_fn b l dst st' prf1 prf2 prf3 prf4.
Note: See TracChangeset for help on using the changeset viewer.