Ignore:
Timestamp:
Dec 4, 2012, 6:16:25 PM (7 years ago)
Author:
tranquil
Message:

rewritten function handling in joint
swapped call_rel with ret_rel in the definition of status_rel, and parameterised status_simulation on status_rel
renamed SemanticUtils?

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/semantics_blocks.ma

    r2422 r2529  
    11include "joint/blocks.ma".
    22include "joint/Traces.ma".
     3include "joint/semanticsUtils.ma".
    34
    45(* let rec seq_list_labels p g (b : list (joint_step p g)) on b : list label ≝
     
    89  ].*)
    910
    10 lemma fetch_statement_eq : ∀p:sem_params.∀g.∀ge : genv p g.∀ptr : cpointer.
    11   ∀fn,pt,s.
    12   fetch_function … ge ptr = OK … fn →
    13   point_of_pointer ? p … ptr = pt →
    14   stmt_at … (joint_if_code … fn) pt = Some ? s →
    15   fetch_statement ? p … ge ptr = OK … 〈fn, s〉.
    16 #p #g #ge #ptr #fn #pt #s #EQ1 #EQ2 #EQ3
    17 whd in match fetch_statement; normalize nodelta >EQ1 >m_return_bind
    18 >EQ2 >EQ3 >m_return_bind %
    19 qed.
    20 
    21 include alias "basics/logic.ma".
    22 lemma io_evaluate_bind : ∀O,I,X,Y,env.
    23 ∀m : IO O I X.∀f : X → IO O I Y.
    24 io_evaluate O I Y env (! x ← m ; f x) =
    25 ! x ← io_evaluate O I X env m ;
    26 io_evaluate O I Y env (f x).
    27 #O #I #X #Y #env #m elim m
    28 [ #o #g #IH #f whd in match (! x ← Interact ????? ; ?);
    29   change with (! y ← ? ; ?) in ⊢ (??%(????%?));
    30   >m_bind_bind @m_bind_ext_eq #i @IH
    31 | #x #f %
    32 | #e #f %
    33 ]
    34 qed.
    35 
    36 lemma fetch_function_from_block_eq :
    37   ∀p,g,ge.
    38   ∀ptr1,ptr2 : cpointer. pblock ptr1 = pblock ptr2 →
    39   fetch_function p g ge ptr1 = fetch_function p g ge ptr2.
    40 #p #g #ge #ptr1 #ptr2 #EQ
    41 whd in match fetch_function; normalize nodelta >EQ
    42 @m_bind_ext_eq // qed.
    43 
    44 let rec repeat_eval_seq_no_pc
    45   (p : evaluation_params) env curr_fn
    46   (l : list (joint_seq p (globals p))) on l :
    47   state p → res (state p) ≝
    48   λst.match l with
    49   [ nil ⇒ return st
    50   | cons hd tl ⇒
    51     ! st' ← io_evaluate … (env st) (eval_seq_no_pc p (globals p) (ev_genv p) curr_fn st hd) ;
    52     repeat_eval_seq_no_pc p env curr_fn tl st'
    53   ].
    54 
    55 lemma err_to_io_evaluate : ∀O,I,X,env,m.
    56   io_evaluate O I X env (err_to_io … m) = m.
    57 #O#I#X#env * // qed.
     11definition repeat_eval_seq_no_pc ≝
     12  λp : evaluation_params.λcurr_id,curr_fn.
     13  m_fold … (eval_seq_no_pc … (ev_genv … p) curr_id curr_fn).
    5814
    5915definition list_not_empty ≝ λA.λl : list A.match l with [ nil ⇒ false | _ ⇒ true ].
    6016
    61 definition no_call_nor_label : ∀p,g.joint_seq p g → bool ≝
    62   λp,g,s.match s with
    63   [ COST_LABEL _ ⇒ false
    64   | CALL_ID _ _ _ ⇒ false
    65   | extension_call _ ⇒ false
    66   | _ ⇒ true
    67   ].
    68 
    69 lemma no_call_nor_label_proceed : ∀p : evaluation_params.
    70 ∀st : state p. ∀s.
    71 no_call_nor_label p (globals p) s →
    72 eval_seq_pc p (globals p) (ev_genv p) st s = return Proceed ???.
    73 #p #st * // [ #f #args #dest | #c ] *
    74 qed.
    75 
    76 lemma no_call_nor_label_other : ∀p : evaluation_params.∀s.
    77 no_call_nor_label p (globals p) s →
    78 step_classifier … s = cl_other.
    79 #p * // [ #f #args #dest | #c ] *
    80 qed.
    81 
    82 lemma no_call_nor_label_uncosted : ∀p : evaluation_params.∀s,nxt.
    83 no_call_nor_label p (globals p) s →
    84 cost_label_of_stmt … (sequential … s nxt) = None ?.
    85 #p * // #lbl#next *
    86 qed.
    87 
    88 definition code_compact : ∀p:sem_params.∀g.codeT p g → Prop ≝
    89   λp,g,c.code_closed … c∧
    90     ∀pt,ptr.code_has_point … c pt → ∃ptr'.pointer_of_point p p ptr pt = return ptr'.
    91 
    92 definition pointer_of_point_step_in_code : ∀p:sem_params.∀g.
    93   ∀c,pc,step,dst.
    94   code_compact p g c → step_in_code … c (point_of_pointer p p pc) step dst →
    95   Σpc'.pointer_of_point p p pc dst = return pc' ≝
    96   λp,g,c,pc,step,dst,c_compact,step_in.
    97   match pointer_of_point p p pc dst
    98   return λx.pointer_of_point p p pc dst = x → ?
    99   with
    100   [ OK pc' ⇒ mk_Sig ?? pc'
    101   | Error e ⇒ λEQ.⊥
    102   ] (refl …).
    103 cases step_in #nxt * #EQ1 #EQ2
    104 cases c_compact -c_compact #c_closed #c_compact
    105 elim (c_compact dst pc ?)
    106 [ >EQ #pc' normalize #ABS destruct(ABS)
    107 | elim (c_closed … EQ1) #_ whd in ⊢ (%→?);
    108   >EQ2 #H @H
    109 ]
    110 qed.
    111 
    112 let rec pointer_of_point_in_code
    113   p g c pc dst b on b :
    114   ∀l.code_compact p g c → point_of_pointer p p pc ~❨b,l❩~> dst in c →
    115   Σpc'.pointer_of_point p p pc dst = return pc' ≝
    116 match b
    117 return λb.? → ? → ? ~❨b,?❩~> ? in ? → Σptr'.pointer_of_point p p pc dst = return ptr'
    118 with
    119 [ nil ⇒
    120   λl,c_compact,in_code.
    121   match pointer_of_point p p pc dst
    122   return λx.pointer_of_point p p pc dst = x → ? with
    123   [ OK ptr' ⇒ mk_Sig ?? ptr'
    124   | Error e ⇒ λEQ.⊥
    125   ] (refl …)
    126 | cons hd tl ⇒
    127   λl.match l return λl.? → ? → Σptr'.? with
    128   [ nil ⇒ λc_compact,in_code.⊥
    129   | cons mid rest ⇒ λc_compact,in_code.
    130     let mid_pc ≝ pointer_of_point_step_in_code … c pc hd mid c_compact ? in
    131     pi1 … (pointer_of_point_in_code ?? c mid_pc dst tl rest c_compact ?)
    132   ]
    133 ].
    134 [ cases l in in_code; [2: #mid #rest * ]
    135   whd in ⊢ (%→?); #EQ' <EQ' in EQ; >pointer_of_point_of_pointer [2: %]
    136   normalize #ABS destruct(ABS)
    137 | cases (pointer_of_point_in_code ?????????)
    138   #ptr' >pointer_of_point_uses_block
    139   [ #H @H |*:]
    140   cases mid_pc -mid_pc #mid_pc @pointer_of_point_block
    141 | elim in_code
    142 | cases mid_pc -mid_pc #mid_pc #EQ
    143   >(point_of_pointer_of_point … EQ)
    144   cases in_code #_ #H @H
    145 | cases in_code #H #_ @H
    146 ]
    147 qed.
    148 
    14917let rec produce_trace_any_any
    15018  (p : evaluation_params)
    151   (st : state_pc p) fd
     19  (st : state_pc p)
     20  curr_id curr_fn
    15221  (b : list (joint_seq p (globals p))) on b :
    15322  ∀l : list (code_point p).
    15423  ∀dst : code_point p.
    15524  ∀st' : state p.
    156   fetch_function p ? (ev_genv p) (pc … st) = return fd →
    157   ∀prf1 : code_compact p (globals p) (joint_if_code … fd).
    158   let src ≝ point_of_pointer p p (pc … st) in
     25  fetch_internal_function … (ev_genv p) (pc_block (pc … st)) =
     26    return 〈curr_id, curr_fn〉 →
     27  let src ≝ point_of_pc p (pc … st) in
    15928  if list_not_empty ? b then
    160     ! x ← stmt_at ?? (joint_if_code … fd) dst ; cost_label_of_stmt … x = None ?
     29    ! x ← stmt_at ?? (joint_if_code … curr_fn) dst ; cost_label_of_stmt … x = None ?
    16130  else
    16231    True →
    163   ∀prf2 : src ~❨b, l❩~> dst in joint_if_code … fd.
    164   All ? (λx.bool_to_Prop (no_call_nor_label … x)) b →
    165   repeat_eval_seq_no_pc p (io_env p) fd b st = return st' →
     32  src ~❨b, l❩~> dst in joint_if_code … curr_fn →
     33  All ? (λx.And (no_call … x) (no_cost_label … x)) b →
     34  repeat_eval_seq_no_pc p curr_id curr_fn b st = return st' →
    16635  trace_any_any (joint_abstract_status p) st
    167     (mk_state_pc ? st' (pointer_of_point_in_code … prf1 prf2)) ≝
    168   match b
    169   return λx.∀l,dst.?→?→?→?→?→?→?→?
     36    (mk_state_pc ? st' (pc_of_point p (pc_block (pc … st)) dst)) ≝  match b
     37  return λb.∀l,dst.?→?→?→?→?→?→?
    17038  with
    17139  [ nil ⇒
    172     λl,dst,st',fd_prf,c_compact,dst_prf,in_code,all_other,EQ1.
     40    λl,dst,st',fd_prf,dst_prf,in_code,all_other,EQ1.
    17341    (taa_base (joint_abstract_status p) st)
    174       ⌈trace_any_any (joint_abstract_status p) st st ↦ ?⌉
     42    ⌈trace_any_any ??? ↦ ?⌉
    17543  | cons hd tl ⇒
    17644    λl.
    177     match l return λx.?→?→?→?→?→?→?→?→? with
    178     [ nil ⇒ λdst_pc,st',fd_prf,src_prf,dst_prf,in_code.⊥
     45    match l return λx.∀dst,st'.?→?→?→?→?→? with
     46    [ nil ⇒ λdst,st',fd_prf,dst_prf,in_code.⊥
    17947    | cons mid rest ⇒
    180       λdst,st',fd_prf,c_compact,dst_prf,in_code,all_other,EQ1.
    181       let mid_pc ≝
    182         pointer_of_point_step_in_code p ? (joint_if_code … fd) (pc … st)
    183           hd mid c_compact ? in
    184       match io_evaluate ??? (io_env p st) (eval_seq_no_pc … (ev_genv p) fd st hd)
    185       return λx.io_evaluate ??? (io_env p st) (eval_seq_no_pc … (ev_genv p) fd st hd) = x → ?
    186       with
    187       [ OK st_mid ⇒ λEQ2.
     48      λdst,st',fd_prf,dst_prf,in_code,all_other,EQ1.
     49      let mid_pc ≝ pc_of_point p (pc_block (pc … st)) mid in
     50      match eval_seq_no_pc … (ev_genv p) curr_id curr_fn hd st
     51      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.
    18855        let tr_tl ≝ produce_trace_any_any ?
    18956            (mk_state_pc ? st_mid mid_pc)
    190             fd tl rest dst ??????? in
    191         (* works fast only in interactive mode:
    192         taa_step … tr_tl *) ?
    193       | Error _ ⇒ λEQ2.⊥
     57            curr_id curr_fn tl rest dst ?????? in
     58        taa_step … tr_tl
     59      | _ ⇒ λEQ2.⊥
    19460      ] (refl …)
    19561    ]
    196   ].[3: @(taa_step … tr_tl) |*:]
    197 try (cases mid_pc -mid_pc #mid_pc #EQ_mid_pc)
    198 try (cases in_code * #nxt * #EQ_stmt_at #EQ_mid #rest_in_code)
    199 try (cases all_other #hd_other #tl_other)
     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 //
     66| @in_code
     67|3,12: whd in EQ1 : (??%%); >EQ2 in EQ1; whd in ⊢ (??%?→?); #EQ1 destruct(EQ1)
     68]
     69change with (! y ← ? ; repeat_eval_seq_no_pc ????? = ?) in EQ1;
     70>EQ2 in EQ1; >m_return_bind
     71cases in_code -in_code * #nxt * #EQ_stmt_at #EQ_mid #rest_in_code
     72cases all_other -all_other * #hd_no_call #hd_no_cost #tl_other
     73#EQ1
     74try assumption
    20075[ whd whd in match eval_state; normalize nodelta
    201   >(fetch_statement_eq … fd_prf (refl …) EQ_stmt_at)
     76  >(fetch_statement_eq … fd_prf EQ_stmt_at)
    20277  >m_return_bind
    203   whd in match eval_statement; normalize nodelta
    204   whd in match eval_step; normalize nodelta
    205   >m_bind_bind
    206   >(no_call_nor_label_proceed … hd_other) >m_return_bind
    207   >m_bind_bind
    208   >io_evaluate_bind >EQ2 >m_return_bind
    209   >m_return_bind
     78  whd in match eval_statement_no_pc; normalize nodelta
     79  >EQ2 >m_return_bind
     80  whd in match eval_statement_advance; normalize nodelta
     81  >(no_call_advance … hd_no_call)
     82  whd in match next; normalize nodelta
    21083  whd in match succ_pc; normalize nodelta
    211   >EQ_mid >EQ_mid_pc >m_return_bind %
    212 | whd %{fd} %{(sequential … hd nxt)}
    213   %{(no_call_nor_label_other … hd_other)}
    214   @(fetch_statement_eq … fd_prf (refl …) EQ_stmt_at)
    215 |4: cases (pointer_of_point_in_code ?????????)
    216   #dst_pc
    217   cases l in in_code; [2: #mid #rest * ]
    218   whd in ⊢ (%→?); #EQ' <EQ'
    219   >pointer_of_point_of_pointer [2: %] lapply EQ1 -EQ1
    220   normalize in ⊢ (%→%→?);
    221   #EQ1 #EQ'' destruct cases st //
    222 |5: >fetch_function_from_block_eq [ @fd_prf |*: ]
    223   @(pointer_of_point_block … EQ_mid_pc)
    224 |6: cases tl [ % ] #hd' #tl' @dst_prf
    225 |7: assumption
    226 |8,9:
    227   lapply EQ1 whd in ⊢ (??%?→?); >EQ2 normalize nodelta
    228   [ #H @H
    229   | normalize #ABS destruct(ABS)
     84  >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')
    230108  ]
    231 |3:
    232   %* #H @H -H
    233   lapply tl_other lapply rest_in_code
    234   cases tl [2: #hd' #tl' ]
    235   cases rest [2,4: #mid' #rest']
    236   [2,3: * ]
    237   [2: whd in ⊢ (%→?); #EQ' destruct(EQ') *
    238   | ** #nxt' * #at_mid #_ #_ * #mid_other #_
    239   ]
    240   whd in ⊢ (??%?);
    241   [ lapply dst_prf ]
    242   whd in match as_label;
    243   whd in match (as_pc_of ??);
    244   whd in match fetch_statement;
    245   normalize nodelta
    246   >(point_of_pointer_of_point … EQ_mid_pc)
    247   >(fetch_function_from_block_eq … (pointer_of_point_block … EQ_mid_pc))
    248   >fd_prf >m_return_bind
    249   [ cases (stmt_at ????) [ #_ % ]
    250     #stmt #H @H
    251   | >at_mid >m_return_bind normalize nodelta
    252     @(no_call_nor_label_uncosted … mid_other)
    253   ]
     109| >dst_prf cases (list_not_empty ??) %
     110| normalize nodelta >point_of_pc_of_point assumption
    254111]
    255112qed.
Note: See TracChangeset for help on using the changeset viewer.