Changeset 2688 for src


Ignore:
Timestamp:
Feb 21, 2013, 6:03:46 PM (7 years ago)
Author:
tranquil
Message:
  • in Arithmeticcs.ma: commented include that breaks script in latest matita
  • moved COST_LABEL out of joint_seq
Location:
src
Files:
8 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Arithmetic.ma

    r2684 r2688  
    11include "ASM/BitVector.ma".
    22include "ASM/Util.ma".
    3 include "arithmetics/exp.ma".
     3(* include "arithmetics/exp.ma". <-- this does not make it compile on latest matita + Cerco *)
    44
    55definition addr16_of_addr11: Word → Word11 → Word ≝
  • src/ERTLptr/ERTLtoERTLptr.ma

    r2681 r2688  
    2222match s with
    2323[COMMENT s ⇒ COMMENT ERTLptr … s
    24 |COST_LABEL c ⇒ COST_LABEL ERTLptr … c
    2524|MOVE a  ⇒ MOVE ERTLptr … a
    2625|POP a ⇒ POP ERTLptr … a
     
    5453        λ_.CALL ERTLptr ? (inr … dest1) args dest, [ ]〉
    5554    ]
     55|COST_LABEL c ⇒ bret … 〈[ ], λ_.COST_LABEL ERTLptr … c, [ ]〉
    5656| COND reg l ⇒ bret … 〈[ ], λ_.COND ERTLptr ? reg l, [ ]〉
    5757| step_seq x ⇒ bret … [seq_embed … x]
     
    9191| whd %{I I}
    9292| #abs #called #args whd %{I I}
     93| #c %{I} %{I} #l %
    9394| * #called #args #dest whd in match translate_step; normalize nodelta whd
    9495  [ %{I} %{I} #l %
  • src/joint/Joint.ma

    r2681 r2688  
    9494inductive joint_seq (p:unserialized_params) (globals: list ident): Type[0] ≝
    9595  | COMMENT: String → joint_seq p globals
    96   | COST_LABEL: costlabel → joint_seq p globals
    9796  | MOVE: pair_move p → joint_seq p globals
    9897  | POP: acc_a_reg p → joint_seq p globals
     
    136135
    137136inductive joint_step (p : unserialized_params) (globals : list ident) : Type[0] ≝
     137  | COST_LABEL: costlabel → joint_step p globals
    138138  | CALL: (ident + (dpl_arg p × (dph_arg p))) → call_args p → call_dest p → joint_step p globals
    139139  | COND: acc_a_reg p → label → joint_step p globals
     
    152152    ]
    153153  | COND _ l ⇒ [l]
    154   | CALL _ _ _ ⇒ [ ]
     154  | _ ⇒ [ ]
    155155  ].
    156156
  • src/joint/Traces.ma

    r2681 r2688  
    102102  λp,stmt.
    103103  match stmt with
    104   [ step_seq _ ⇒ cl_other
    105   | CALL f args dest ⇒ cl_call
     104  [ CALL f args dest ⇒ cl_call
    106105  | COND _ _ ⇒ cl_jump
     106  | _ ⇒ cl_other
    107107  ].
    108108
     
    124124  | final s ⇒ Some ? (joint_classify_final p s)
    125125  | FCOND _ _ _ _ ⇒ Some ? cl_jump
    126   ].
    127 
    128 definition no_cost_label : ∀p,g.joint_seq p g → Prop ≝
    129   λp,g,s.match s with
    130   [ COST_LABEL _ ⇒ False
    131   | _ ⇒ True
    132126  ].
    133127
     
    145139  >m_return_bind normalize nodelta normalize in ⊢ (%→?); #ABS destruct
    146140]
    147 * [ #f' #args #dest | #a #lbl | #s ] #nxt #fetch >m_return_bind
     141* [ #c | #f' #args #dest | #a #lbl | #s ] #nxt #fetch >m_return_bind
    148142normalize in ⊢ (%→?); #EQ destruct
    149143%[|%[|%[|%[|%[| %]]]]]
     
    266260  [ sequential s _ ⇒
    267261    match s with
    268     [ step_seq s ⇒
    269       match s with
    270       [ COST_LABEL lbl ⇒ Some ? lbl
    271       | _ ⇒ None ?
    272       ]
     262    [  COST_LABEL lbl ⇒ Some ? lbl
    273263    | _ ⇒ None ?
    274264    ]
    275265  | _ ⇒ None ?
    276266  ].
    277 
    278 
    279 lemma no_label_uncosted : ∀p : evaluation_params.∀s,nxt.
    280 no_cost_label p (globals p) s →
    281 cost_label_of_stmt … (sequential … s nxt) = None ?.
    282 #p * // #lbl #next *
    283 qed.
    284267
    285268definition joint_abstract_status :
  • src/joint/TranslateUtils.ma

    r2681 r2688  
    414414    (f_fin l s)
    415415; f_step_on_cost :
    416   ∀l,c.f_step l (COST_LABEL … c) = bret … [ COST_LABEL … c ]
     416  ∀l,c.f_step l (COST_LABEL … c) =
     417    bret ? (step_block ??) 〈[ ], λ_.COST_LABEL dst globals c, [ ]〉
    417418}.
    418419
     
    426427    [ sequential s' nxt ⇒
    427428      match s' return λx.stmt_at ???? = Some ? (sequential … x nxt) → ? with
    428       [ step_seq s'' ⇒
    429         match s'' return λx.stmt_at ???? = Some ? (sequential … (step_seq … x) nxt) → ? with
    430         [ COST_LABEL c ⇒ λ_.〈c, nxt〉
    431         | _ ⇒ λabs.⊥
    432         ]
     429      [ COST_LABEL c ⇒ λ_.〈c, nxt〉
    433430      | _ ⇒ λabs.⊥
    434431      ]
  • src/joint/joint_semantics.ma

    r2655 r2688  
    587587  [ sequential s nxt ⇒
    588588    match s return λ_.IO ??? with
    589     [ step_seq s ⇒ return next … nxt st
    590     | COND a l ⇒
     589    [ COND a l ⇒
    591590      ! v ← acca_retrieve … st a ;
    592591      ! b ← bool_of_beval … v ;
     
    597596    | CALL f args dest ⇒
    598597      eval_call … ge f args dest nxt st
     598    | _ ⇒ return next … nxt st
    599599    ]
    600600  | final s ⇒
  • src/joint/semanticsUtils.ma

    r2687 r2688  
    453453    def_in def_out (f_lbls bl) (f_regs bl).
    454454 
    455 lemma b_graph_transform_program_find_funct_ptr :
     455lemma make_b_graph_transform_program_props :
    456456 ∀src,dst:sem_graph_params.
    457457 ∀data : ∀globals.joint_closed_internal_function src globals →
  • src/joint/semantics_blocks.ma

    r2674 r2688  
    7878  let src ≝ point_of_pc p (pc … st) in
    7979  seq_list_in_code … (joint_if_code … curr_fn) src b l dst →
    80   All ? (no_cost_label …) b →
    8180  repeat_eval_seq_no_pc p curr_id curr_fn b st = return st' →
    8281  Σtaaf : trace_any_any_free (joint_abstract_status p) st
     
    8483  (not_empty … b ↔ bool_to_Prop (taaf_non_empty … taaf)) ≝
    8584  match b
    86   return λb.∀l,dst.?→?→?→?→?→ Σtaaf.(not_empty ? b ↔ bool_to_Prop (taaf_non_empty … taaf))
     85  return λb.∀l,dst.?→?→?→?→ Σtaaf.(not_empty ? b ↔ bool_to_Prop (taaf_non_empty … taaf))
    8786  with
    8887  [ nil ⇒
    89     λl,dst,st',fd_prf,in_code,all_other,EQ1.
     88    λl,dst,st',fd_prf,in_code,EQ1.
    9089    «taaf_base (joint_abstract_status p) st
    9190    ⌈trace_any_any_free ??? ↦ ?⌉,?»
    9291  | cons hd tl ⇒
    9392    λl.
    94     match l return λx.∀dst,st'.?→?→?→?→Σtaaf.(True ↔ bool_to_Prop (taaf_non_empty … taaf)) with
     93    match l return λx.∀dst,st'.?→?→?→Σtaaf.(True ↔ bool_to_Prop (taaf_non_empty … taaf)) with
    9594    [ nil ⇒ λdst,st',fd_prf,in_code.⊥
    9695    | cons _ rest ⇒ λdst.
    9796      let mid ≝ match rest with [ nil ⇒ dst | cons mid _ ⇒ mid ] in
    98       λst',fd_prf,in_code,all_other,EQ1.
     97      λst',fd_prf,in_code,EQ1.
    9998      let mid_pc ≝ pc_of_point p (pc_block (pc … st)) mid in
    10099      match eval_seq_no_pc … (ev_genv p) curr_id curr_fn hd st
     
    106105        let tr_tl ≝ produce_trace_any_any_free_aux ?
    107106            (mk_state_pc ? st_mid mid_pc (last_pop … st))
    108             curr_id curr_fn tl rest dst ????? in
     107            curr_id curr_fn tl rest dst ???? in
    109108        «taaf_cons … tr_tl ?,?»
    110109      | _ ⇒ λEQ2.⊥
     
    118117  >pc_of_point_of_pc cases st // #a #b #c #e >(K ?? e) normalize nodelta *
    119118| cases in_code #a * #b ** #ABS destruct
    120 |12: whd in EQ1 : (??%%); >EQ2 in EQ1; whd in ⊢ (??%?→?); #EQ1 destruct(EQ1)
     119|11: whd in EQ1 : (??%%); >EQ2 in EQ1; whd in ⊢ (??%?→?); #EQ1 destruct(EQ1)
    121120|4: cases tr_tl -tr_tl #tr_tl * #_ #H
    122121  @if_elim [2: #_ % ] #G lapply (H G) -H -G
    123  cases tl in in_code all_other; [ #_ #_ * ]
     122 cases tl in in_code; [ #_ * ]
    124123 #hd' #tl' * #mid' * #rest' ** #EQ * #nxt * #EQstmt_at #EQ_nxt
    125  * #mid'' * #rest'' ** #EQ' * #nxt' * #EQstmt_at' #EQnxt' #_
     124 * #mid'' * #rest'' ** #EQ' * #nxt' * #EQstmt_at' #EQnxt'
    126125 normalize nodelta -mid_pc destruct
    127  * #_ * #H #_ #_ % whd in ⊢ (%→?);
     126 #_ #_ % whd in ⊢ (%→?);
    128127 whd in ⊢ (?(??%?)→?); whd in match (as_pc_of ??);
    129128  >fetch_statement_eq [2: whd in match point_of_pc;
    130129  normalize nodelta >point_of_offset_of_point @EQstmt_at' |3: @fd_prf |*:]
    131   normalize nodelta
    132   >(no_label_uncosted … H) * #ABS @ABS %
     130  normalize nodelta * #ABS @ABS %
    133131|7: % [2: #_ %] #_ @taaf_cons_non_empty
    134132]
     
    138136#nxt * #EQ_stmt_at #EQ_mid' #rest_in_code
    139137normalize nodelta
    140 cases all_other -all_other #hd_no_cost #tl_other
    141138#EQ3 destruct skip (mid_pc)
    142139try assumption
     
    168165  let src ≝ point_of_pc p (pc … st) in
    169166  seq_list_in_code … (joint_if_code … curr_fn) src b l dst →
    170   All ? (no_cost_label …) b →
    171167  repeat_eval_seq_no_pc p curr_id curr_fn b st = return st' →
    172168  trace_any_any_free (joint_abstract_status p) st
    173169    (mk_state_pc ? st' (pc_of_point p (pc_block (pc … st)) dst) (last_pop … st)) ≝
    174   λp,st,curr_id,curr_fn,b,l,dst,st',prf1,prf2,prf3,prf4.
    175   produce_trace_any_any_free_aux p st curr_id curr_fn b l dst st' prf1 prf2 prf3 prf4.
     170  λp,st,curr_id,curr_fn,b,l,dst,st',prf1,prf2,prf3.
     171  produce_trace_any_any_free_aux p st curr_id curr_fn b l dst st' prf1 prf2 prf3.
    176172
    177173(* when a seq_list is coerced to a step_block *)
     
    188184  let src ≝ point_of_pc p (pc … st) in
    189185  src ~❨b, l❩~> dst in joint_if_code … curr_fn →
    190   All ? (no_cost_label …) b →
    191186  repeat_eval_seq_no_pc p curr_id curr_fn b st = return st' →
    192187  trace_any_any_free (joint_abstract_status p) st
     
    196191lapply (coerced_step_list_in_code … prf)
    197192inversion b normalize nodelta
    198 [ #_ #in_code #_ whd in ⊢ (??%%→?); #EQ destruct
     193[ #_ #in_code whd in ⊢ (??%%→?); #EQ destruct
    199194  cases (produce_step_trace … fd_prf … in_code (refl …))
    200195  #H #G
Note: See TracChangeset for help on using the changeset viewer.