Changeset 2883 for src/ERTLptr


Ignore:
Timestamp:
Mar 15, 2013, 6:33:18 PM (7 years ago)
Author:
piccolo
Message:

partial commit

Location:
src/ERTLptr
Files:
3 edited

Legend:

Unmodified
Added
Removed
  • src/ERTLptr/ERTLptrToLTL.ma

    r2844 r2883  
    2323  the offset does not need the stack size to be computed *)
    2424
     25check ltl_lin_seq
    2526definition preserve_carry_bit :
    26   ∀globals.bool → list (joint_seq LTL globals) → list (joint_seq LTL globals) ≝
     27 (λglobals:list ident
     28  .λdo_it:bool
     29   .λsteps:step_block LTL globals
     30    .if do_it 
     31     then 〈[λ_:code_point LTL.SAVE_CARRY]@ \fst  (\fst  steps),
     32              \snd  (\fst  steps),
     33              \snd  steps@[RESTORE_CARRY]〉 
     34     else steps ).
     35
     36
     37  ∀globals.bool → step_block LTL globals → step_block LTL globals ≝
    2738  λglobals,do_it,steps.
    28   if do_it then SAVE_CARRY :: steps @ [RESTORE_CARRY] else steps.
     39  if do_it then
     40    〈[?] @ (\fst(\fst steps)),
     41     \snd(\fst steps),
     42      (\snd  steps) @ [RESTORE_CARRY]〉
     43  else steps.
     44#_ @SAVE_CARRY
     45qed.
     46check preserve_carry_bit
    2947
    3048(* for notation *)
  • src/ERTLptr/ERTLptrToLTLProof.ma

    r2863 r2883  
    2525program_counter → program_counter.
    2626
     27
     28definition clear_sb_type ≝ label → decision → bool.
     29 
     30axiom to_be_cleared_sb : 
     31∀after : valuation register_lattice. coloured_graph after → clear_sb_type.
     32
     33definition clear_fb_type ≝ label → vertex → bool.
     34
     35axiom to_be_cleared_fb :
     36∀after : valuation register_lattice.clear_fb_type.
     37
    2738axiom sigma_fb_state: ertlptr_program → (block → label → list label) →
    28  (block → label → list register) → list register →
    29   state ERTLptr_semantics → state ERTLptr_semantics.
    30 
     39 (block → label → list register) →
     40 clear_fb_type → state ERTLptr_semantics → state ERTLptr_semantics.
     41
     42axiom acc_is_dead : ∀fix_comp.∀prog : ertlptr_program.
     43∀fn : joint_closed_internal_function ERTLptr (prog_var_names … prog).
     44∀l.
     45let after ≝ (analyse_liveness fix_comp (prog_var_names … prog) fn) in
     46¬ lives (inr ? ? RegisterA) (livebefore  … fn l after).
     47
     48axiom dead_registers_in_dead :  ∀fix_comp.∀build : coloured_graph_computer.
     49∀prog : ertlptr_program.
     50∀fn : joint_closed_internal_function ERTLptr (prog_var_names … prog).
     51∀l.
     52let after ≝ (analyse_liveness fix_comp (prog_var_names … prog) fn) in
     53let coloured_graph ≝ build … fn after in
     54∀R : Register.
     55¬ lives (inr ? ? R) (livebefore  … fn l after) →
     56to_be_cleared_sb after coloured_graph l R.
     57 
    3158axiom sigma_sb_state: ertlptr_program → (block → label → list label) →
    32  (block → label → list register) → list register →
    33   state LTL_semantics → state ERTLptr_semantics.
     59 (block → label → list register) → clear_sb_type → state LTL_semantics → state ERTLptr_semantics.
    3460
    3561definition dummy_state : state ERTLptr_semantics ≝
     
    4167
    4268
    43 definition sigma_fb_state_pc : ertlptr_program → (block → label → list label) →
    44  (block → label → list register) →
    45  state_pc ERTLptr_semantics → state_pc ERTLptr_semantics ≝
    46 λprog,f_lbls,f_regs,st.
     69definition sigma_fb_state_pc : fixpoint_computer → ertlptr_program →
     70(block → label → list label) → (block → label → list register) →
     71state_pc ERTLptr_semantics → state_pc ERTLptr_semantics ≝
     72λfix_comp,prog,f_lbls,f_regs,st.
    4773let ge ≝ globalenv_noinit … prog in
    4874let globals ≝ prog_var_names … prog in
    4975match fetch_internal_function … ge (pc_block (pc … st)) with
    50   [ OK y ⇒ ?
     76  [ OK y ⇒
     77  let after ≝ (analyse_liveness fix_comp (prog_var_names … prog) (\snd y)) in
     78  mk_state_pc ? (sigma_fb_state prog f_lbls f_regs (to_be_cleared_fb after) st) (pc … st) 
     79                         (last_pop … st)
    5180  | Error e ⇒ dummy_state_pc
    5281  ].
    53 cases daemon qed.
    54 
    55 definition sigma_sb_state_pc : ertlptr_program → (block → label → list label) →
    56  (block → label → list register) → state_pc LTL_semantics → state_pc ERTLptr_semantics ≝
    57 λprog,f_lbls,f_regs,st.
     82
     83definition sigma_sb_state_pc :fixpoint_computer → coloured_graph_computer → 
     84ertlptr_program → (block → label → list label) →
     85(block → label → list register) → state_pc LTL_semantics → state_pc ERTLptr_semantics ≝
     86λfix_comp,build,prog,f_lbls,f_regs,st.
    5887let ge ≝ globalenv_noinit … prog in
    5988let globals ≝ prog_var_names … prog in
    6089match fetch_internal_function … ge (pc_block (pc … st)) with
    61   [ OK y ⇒ ?
     90  [ OK y ⇒ 
     91     let after ≝ (analyse_liveness fix_comp (prog_var_names … prog) (\snd y)) in
     92     let coloured_graph ≝ build … (\snd y) after in
     93     mk_state_pc ? (sigma_sb_state prog f_lbls f_regs
     94                          (to_be_cleared_sb after coloured_graph) st) (pc … st) 
     95                          (sigma_stored_pc prog f_lbls (last_pop … st))
    6296  | Error e ⇒ dummy_state_pc
    6397  ].
    64 cases daemon qed.
     98
     99axiom write_decision : decision → beval → state LTL_LIN_state →
     100state LTL_LIN_state.
     101
     102axiom read_arg_decision : arg_decision → state LTL_LIN_state → beval.
     103
     104axiom insensitive_to_be_cleared_sb : ∀prog. ∀f_lbls : (block → label → list label).
     105∀f_regs : (block → label → list register).∀tb : clear_sb_type.
     106∀st : state LTL_LIN_state.∀lab.
     107∀d : decision.∀bv.tb lab d →
     108sigma_sb_state prog f_lbls f_regs tb st =
     109sigma_sb_state prog f_lbls f_regs tb (write_decision d bv st).
    65110
    66111
     
    82127         (λs1:ERTLptr_status ? ?
    83128          .λs2:LTL_status ? ?
    84            .sigma_fb_state_pc prog f_lbls f_regs s1
    85             =sigma_sb_state_pc prog f_lbls f_regs s2)
     129           .sigma_fb_state_pc fix_comp prog f_lbls f_regs s1
     130            =sigma_sb_state_pc fix_comp colour prog f_lbls f_regs s2)
    86131    (* call_rel ≝ *) 
    87132       (λs1:Σs:ERTLptr_status ??.as_classifier ? s cl_call
     
    121166*)
    122167
    123 lemma set_no_pc_eta:
    124  ∀P.∀st1: state_pc P. set_no_pc P st1 st1 = st1.
    125 #P * //
    126 qed.
    127 
    128 lemma pc_of_label_eq :
    129   ∀p,p'.let pars ≝ mk_sem_graph_params p p' in
    130   ∀globals,ge,bl,i_fn,lbl.
    131   fetch_internal_function ? ge bl = return i_fn →
    132   pc_of_label pars globals ge bl lbl =
    133     OK ? (pc_of_point ERTL_semantics bl lbl).
    134 #p #p' #globals #ge #bl #i_fn #lbl #EQf
    135 whd in match pc_of_label;
    136 normalize nodelta >EQf >m_return_bind %
    137 qed.
    138168
    139169lemma eq_OK_OK_to_eq: ∀T,x,y. OK T x = OK T y → x=y.
     
    151181pc_block (pc … st1) = pc_block (pc … st2).
    152182
     183
    153184axiom pc_eq_sigma_commute : ∀fix_comp,colour.
    154185∀prog.∀ f_lbls,f_regs.∀f_bl_r.
    155186∀ good :b_graph_transform_program_props ERTLptr_semantics LTL_semantics
    156187     (λglobals,fn.«translate_data fix_comp colour globals fn,(refl …)») prog f_bl_r f_lbls f_regs.
    157 ∀st1,st2.
     188∀st1,st2,f,fn,stmt.
     189fetch_statement ERTLptr_semantics (prog_var_names … prog) (globalenv_noinit … prog)
     190                (pc … st1) = return 〈f,fn,stmt〉 →
    158191let R ≝ sem_rel … (ERTLptr_to_LTL_StatusSimulation fix_comp colour prog … good) in
    159192R st1 st2 →
     
    184217include "joint/semantics_blocks.ma".
    185218include "ASM/Util.ma".
     219include "joint/StatusSimulationHelper.ma".
     220
     221
     222axiom hw_reg_retrieve_write_decision_hit : ∀r : Register.∀bv : beval.
     223∀st : state LTL_LIN_state.
     224hw_reg_retrieve (regs … (write_decision r bv st)) r = return bv.
     225
     226axiom move_spec : ∀prog.∀stack_size.∀localss : nat.
     227∀ carry_lives_after : bool.∀dest : decision.∀src : arg_decision.
     228∀f : ident.
     229∀s : state LTL_LIN_state.
     230repeat_eval_seq_no_pc (mk_prog_params LTL_semantics prog stack_size) f
     231   (move (prog_var_names … prog) localss carry_lives_after dest src) s =
     232   return write_decision dest (read_arg_decision src s) s.
     233
     234axiom sigma_beval : ertlptr_program → (block → label → list label) →
     235                    beval → beval.
     236 
     237
     238axiom ps_reg_retrieve_hw_reg_retrieve_commute :
     239∀fix_comp,colour,prog.
     240∀ f_lbls,f_regs.∀f_bl_r.
     241∀ good :b_graph_transform_program_props ERTLptr_semantics LTL_semantics
     242 (λglobals,fn.«translate_data fix_comp colour globals fn,(refl …)») prog f_bl_r f_lbls f_regs.
     243∀fn : joint_closed_internal_function ERTLptr (prog_var_names … prog).
     244let R ≝ sem_rel … (ERTLptr_to_LTL_StatusSimulation fix_comp colour prog … good) in
     245let after ≝ (analyse_liveness fix_comp (prog_var_names … prog) fn) in
     246∀st1 : state_pc ERTL_state.
     247∀st2 : state_pc LTL_LIN_state.
     248∀bv.
     249∀r : register.R st1 st2 →
     250lives (inl ? ? r) (livebefore  … fn (point_of_pc ERTLptr_semantics (pc … st1)) after) →
     251ps_reg_retrieve (regs … st1) r = return bv →
     252∃bv'.bv = sigma_beval prog f_lbls bv' ∧
     253read_arg_decision (colouring after (colour (prog_var_names … prog) fn after)
     254                                            (inl register Register r))
     255                              st2 = bv'.
     256                             
     257axiom set_member_empty :∀A.∀DEC.∀a.¬set_member A DEC a (set_empty …).   
     258axiom set_member_singl : ∀A,DEC,a.set_member A DEC a (set_singleton … a).
     259axiom set_member_union1 : ∀A,DEC,x,y,a.set_member A DEC a x →
     260set_member A DEC a (set_union … x y).
     261axiom set_member_union2 : ∀A,DEC,x,y,a.set_member A DEC a y →
     262set_member A DEC a (set_union … x y).
     263axiom set_member_diff : ∀A,DEC,x,y,a.set_member A DEC a x →
     264¬set_member A DEC a y →
     265set_member A DEC a (set_diff … x y).
     266
     267
     268lemma all_used_are_live_before :
     269∀fix_comp.
     270∀prog : ertlptr_program.
     271∀fn : joint_closed_internal_function ERTLptr (prog_var_names … prog).
     272∀l,stmt.
     273stmt_at … (joint_if_code … fn) l = return stmt →
     274∀r : register. set_member ? (eq_identifier …) r (\fst (used ? stmt)) →
     275let after ≝ (analyse_liveness fix_comp (prog_var_names … prog) fn) in
     276eliminable ? (after l) stmt = None ? →
     277lives (inl ? ? r)  (livebefore  … fn l after).
     278#fix_comp #prog #fn #l *
     279[ * [#c|* [#c_id | #c_ptr] #args #dest | #a #lbl | *
     280[ #str
     281| * * [#r1 | #R1]  * [1,3: * [1,3: #r |2,4: #R] |2,4: #b]
     282| #a
     283| * [ #r | #b]
     284| #i #i_spec #dpl #dph
     285| #op #a #b * [#r | #by]  * [1,3: #r'|2,4: #by']
     286| #op #a #a'
     287| * #a #a' * [1,3,5,7,9,11: #r |2,4,6,8,10,12: #b]
     288|
     289|
     290| #a #dpl #dph
     291| #dpl #dph #a
     292| * [ * [|| #r] | #r #lbl | #r #lbl ]
     293]
     294] #nxt| * [ #lbl | | *] |*]
     295#EQstmt #r #H #H1 whd in match (lives ??); normalize  nodelta
     296whd in match (livebefore ????); whd in EQstmt : (??%?); >EQstmt
     297normalize nodelta -EQstmt whd in match (statement_semantics ???);
     298whd in match(\fst ?); try( @(set_member_union2) assumption) >H1
     299normalize nodelta whd in match(\fst ?); @(set_member_union2) assumption
     300qed.
     301
     302axiom bool_of_beval_sigma_commute :
     303∀prog.∀f_lbls.∀bv,b.
     304bool_of_beval (sigma_beval prog f_lbls bv) = return b →
     305bool_of_beval bv = return b.
     306
     307lemma map_eval_add_dummy_variance_id :
     308∀X,Y.∀l,x.map_eval X Y (add_dummy_variance X Y l) x =l.
     309#X #Y #l elim l [//] #hd #tl normalize #IH #x >IH %
     310qed.
     311
     312lemma state_pc_eq : ∀p.∀st1,st2 : state_pc p.
     313st1 = st2 → st_no_pc … st1 = st_no_pc … st2 ∧
     314pc … st1 = pc … st2 ∧ last_pop … st1 = last_pop … st2.
     315#p * #st1 #pc1 #lp1 * #st2 #pc2 #lp2 #EQ destruct(EQ)
     316%{(refl …)} %{(refl …)} %
     317qed.
     318(*
     319axiom dead_is_to_be_clear :
     320*)
     321
     322(* Cut&paste da un altro file con nome split_on_last_append, unificare*)
     323lemma split_on_last_append_singl : ∀A : Type[0]. ∀pre : list A.
     324∀ last : A. split_on_last ? (pre@[last]) = return 〈pre,last〉.
     325#A #pre elim pre [#last %] #a #tl #IH #last whd in ⊢ (??%?);lapply(IH last)
     326whd in ⊢ (??%? → ?); #EQ >EQ %
     327qed.
     328
     329lemma split_on_last_append : ∀A : Type[0]. ∀l1,l2: list A.
     330 OptPred True (λres.
     331  split_on_last ? (l1@l2) = return 〈l1 @ \fst res, \snd res〉)
     332  (split_on_last … l2).
     333#A #l1 #l2 lapply l1 -l1 @(list_elim_left … l2) //
     334#hd #tl #IH #l1 whd >split_on_last_append_singl whd
     335<associative_append @split_on_last_append_singl
     336qed.
     337
     338lemma make_ERTLptr_To_LTL_good_state_relation :
     339∀fix_comp,colour,prog.
     340let p_out ≝ (\fst (\fst (ertlptr_to_ltl fix_comp colour prog))) in
     341let m ≝ (\snd (\fst (ertlptr_to_ltl fix_comp colour prog))) in
     342let n ≝ \snd (ertlptr_to_ltl fix_comp colour prog) in
     343let stacksizes ≝ lookup_stack_cost … m in
     344∃init_regs : block → list register.
     345∃f_lbls : block → label → list label.
     346∃f_regs : block → label → list register.
     347∃good : b_graph_transform_program_props ERTLptr_semantics LTL_semantics
     348        (λglobals,fn.«translate_data fix_comp colour globals fn,(refl …)»)
     349        prog init_regs f_lbls f_regs.
     350good_state_relation ERTLptr_semantics LTL_semantics prog stacksizes
     351 (λglobals,fn.«translate_data fix_comp colour globals fn,(refl …)»)
     352 (sem_rel … (ERTLptr_to_LTL_StatusSimulation fix_comp colour prog … good)).
     353#fix_comp #colour #prog
     354cases(make_b_graph_transform_program_props ERTLptr_semantics LTL_semantics
     355          (λglobals,fn.«translate_data fix_comp colour globals fn,(refl …)») prog)
     356#init_regs * #f_lbls * #f_regs #good %{init_regs} %{f_lbls} %{f_regs} %{good}
     357%
     358[ #st1 #st2 #f #fn #stmt #Rst1st2 #EQstmt >(pc_eq_sigma_commute … good … EQstmt Rst1st2) %
     359| #st1 #st2 #f #fn #stmt #EQstmt #Rst1St2 >(as_label_ok … good … Rst1St2 EQstmt) %
     360| normalize nodelta whd in ⊢ (% → % → % → ?); #st1 #st1' #st2 #f #fn #a #ltrue #lfalse
     361  #EQfetch whd in match eval_state in ⊢ (% → ?); whd in match eval_statement_no_pc;
     362  normalize nodelta
     363  >EQfetch >m_return_bind normalize nodelta >m_return_bind
     364  whd in match eval_statement_advance; normalize nodelta
     365  change with (ps_reg_retrieve ??) in match (acca_retrieve ?????);
     366  #H lapply(err_eq_from_io ????? H) -H #H @('bind_inversion H) -H
     367  #bv >set_no_pc_eta #EQbv #H @('bind_inversion H) -H * #EQbool normalize nodelta
     368  cases(fetch_statement_inv … EQfetch) #EQfn #EQstmt
     369  [ whd in match goto; normalize nodelta >(pc_of_label_eq … EQfn)
     370    >m_return_bind ] whd in ⊢ (??%% → ?); #EQ destruct(EQ) #Rst1st2
     371  #t_fn1 #EQt_fn1 whd normalize nodelta
     372  letin trans_prog ≝ (b_graph_transform_program ????)
     373  letin stacksizes ≝ (lookup_stack_cost ?)
     374  letin prog_pars_in ≝ (mk_prog_params ERTLptr_semantics ??)
     375  letin prog_pars_out ≝ (mk_prog_params LTL_semantics ??) %{(refl …)}
     376  #mid #EQmid
     377  letin st2_pre_mid_no_pc ≝
     378  (write_decision RegisterA
     379          (read_arg_decision
     380              (colouring
     381                  (analyse_liveness fix_comp (globals prog_pars_in) fn)
     382                  (colour (globals prog_pars_in) fn
     383                  (analyse_liveness fix_comp (globals prog_pars_in) fn))
     384              (inl register Register a)) st2) st2)
     385  %{st2_pre_mid_no_pc}
     386  %
     387  [1,3: >map_eval_add_dummy_variance_id @move_spec]
     388  % [1,3: % %] %{(mk_state_pc ? st2_pre_mid_no_pc
     389                       (pc_of_point LTL_semantics (pc_block (pc … st2)) ?)
     390                        (last_pop … st2))} [@ltrue |3: @lfalse]
     391  change with prog_pars_out in match (mk_prog_params ???); %
     392  [1,3: whd in match eval_state; whd in match eval_statement_no_pc;
     393        whd in match fetch_statement; normalize nodelta
     394       >EQt_fn1 >m_return_bind >point_of_pc_of_point >EQmid >m_return_bind
     395        normalize nodelta >m_return_bind
     396        change with prog_pars_out in match (mk_prog_params ???);
     397        whd in match eval_statement_advance; normalize nodelta
     398        change with (hw_reg_retrieve ??) in match (acca_retrieve ?????);
     399        whd in match set_no_pc; normalize nodelta
     400        >hw_reg_retrieve_write_decision_hit >m_return_bind
     401        cases(ps_reg_retrieve_hw_reg_retrieve_commute fix_comp colour prog … good fn … Rst1st2 … EQbv)
     402        [2,4: @(all_used_are_live_before … EQstmt)
     403            [1,3: @set_member_singl |*: % ] ] #bv' * #EQbv' #EQbv1
     404        change with (prog_var_names … prog) in match (globals ?); >EQbv1
     405        >EQbv' in EQbool; #EQbool
     406        >(bool_of_beval_sigma_commute prog f_lbls … EQbool) >m_return_bind
     407        normalize nodelta [2: %] whd in match goto; normalize nodelta
     408        >(pc_of_label_eq … EQt_fn1) %
     409  |2,4: whd whd in match sigma_fb_state_pc; normalize nodelta
     410        whd in match sigma_sb_state_pc; normalize nodelta
     411        change with (pc_block (pc … st1)) in match (pc_block ?);
     412        cases(fetch_statement_inv … EQfetch) #EQfn #_ >EQfn
     413        normalize nodelta <(pc_eq_sigma_commute … good … EQfetch Rst1st2)
     414        change with (pc_block (pc … st1)) in ⊢ (???match (???%) with [_⇒ ? | _ ⇒ ?]);
     415        >EQfn normalize nodelta
     416        lapply Rst1st2 whd in ⊢ (% → ?); whd in match sigma_fb_state_pc;
     417         whd in match sigma_sb_state_pc; normalize nodelta >EQfn
     418         <(pc_eq_sigma_commute … good … EQfetch Rst1st2) >EQfn normalize nodelta
     419         #EQ cases(state_pc_eq … EQ) * #EQst1st2 #EQpc #EQlp @eq_f3
     420        [3,6:  assumption
     421        |2,5: %
     422        |*: <(insensitive_to_be_cleared_sb … prog f_lbls f_regs … st2 …
     423               (point_of_pc ERTLptr_semantics (pc … st2)))
     424            [2,4: @dead_registers_in_dead @acc_is_dead ]
     425            assumption
     426        ]
     427  ]
     428| letin p_in ≝ (mk_prog_params ERTLptr_semantics ??)
     429  letin p_out ≝ (mk_prog_params LTL_semantics ??)
     430  letin trans_prog ≝ (b_graph_transform_program ????)
     431  #st1 #st1' #st2 #f #fn *
     432  [7: #op1 #dest #src #nxt #EQfetch whd in match eval_state in ⊢ (% → ?);
     433      normalize nodelta >EQfetch >m_return_bind #H @('bind_inversion H) -H
     434      #st1_no_pc whd in match eval_statement_no_pc in ⊢ (% → ?); normalize nodelta
     435      whd in match eval_seq_no_pc; normalize  nodelta
     436      #H lapply(err_eq_from_io ????? H) -H #H @('bind_inversion H) -H
     437      #bv #EQbv #H @('bind_inversion H) -H #bv_op1 #EQbv_op1 #EQst1_no_pc
     438      whd in match eval_statement_advance; normalize nodelta
     439      whd in ⊢ (??%% → ?); #EQ destruct(EQ)
     440      whd in ⊢ (% → ?); #Rst1st2 #t_fn #EQt_fn
     441      whd normalize nodelta whd in match translate_op1;
     442      normalize nodelta
     443      change with p_out in match p_out;
     444      change with p_in in match p_in;
     445      change with trans_prog in match trans_prog;
     446      #mid #mid1 #EQmid % [%]
     447      [ cases (andb ??) whd in match (preserve_carry_bit ???);
     448        whd in match ensure_step_block; normalize nodelta
     449        XXX
     450     
     451     
     452      whd normalize nodelta
     453      change with p_out in match p_out;
     454      change with p_in in match p_in;
     455      change with trans_prog in match trans_prog;
     456      letin coloured_dst ≝ (colouring ???)
     457      letin coloured_src ≝ (colouring ???)
     458      whd in match translate_op1; normalize nodelta
     459
     460
     461
     462      whd in match (translate_op1 ?????);
     463      change with (bind_new_P' ? (? × ?) ?
     464       (f_step ERTLptr_semantics ?????));
     465      whd in match (translate_data ????);
     466      change with (bind_new_P' ??? (f_step ??????));
     467      whd in match (f_step ??????);
     468      @(λH.H)
     469     
     470      whd in match (  #mid whd #
     471 
     472
     473qed.
     474
    186475
    187476lemma eval_cond_ok :
     
    209498bool_to_Prop (taaf_non_empty … taf).
    210499#fix_comp #colour #prog #f_lbls #f_regs #f_bl_r #good #st1 #st2 #st1' #f #fn #a
    211 #ltrue #lfalse #Rst1st2 #EQfetch
     500#ltrue #lfalse #Rst1st2 #EQfetch #EQeval
     501letin R ≝ (sem_rel … (ERTLptr_to_LTL_StatusSimulation fix_comp colour prog … good))
     502@(general_eval_cond_ok … good … Rst1st2 EQfetch EQeval)
     503%
     504[ #st1 #st2 #Rst1St2 >(pc_eq_sigma_commute … good … Rst1St2) %
     505| #st1 #st2 #f #fn #stmt #EQstmt #Rst1St2 >(as_label_ok … good … Rst1St2 EQstmt) %
     506|
     507
     508
     509
    212510whd in match eval_state; normalize nodelta
    213511>EQfetch >m_return_bind
  • src/ERTLptr/liveness.ma

    r2700 r2883  
    2626    〈set_empty …, set_singleton … r〉.
    2727
    28 definition rl_join: register_lattice → register_lattice → register_lattice ≝
    29   λleft.
    30   λright.
    31   let 〈lp, lh〉 ≝ left in
    32   let 〈rp, rh〉 ≝ right in
    33     〈set_union … lp rp, set_union … lh rh〉.
     28definition pairwise : ∀A,B : Type[0]. ∀f : A → A → A. ∀g: B → B → B.
     29A × B → A × B → A × B≝
     30λA,B,f,g,c1,c2.〈f (\fst c1) (\fst c2) , g (\snd c1) (\snd c2)〉.
     31
     32definition rl_join: register_lattice → register_lattice → register_lattice ≝
     33pairwise ?? (set_union …) (set_union …).
    3434
    3535definition rl_diff: register_lattice → register_lattice → register_lattice ≝
    36   λleft.
    37   λright.
    38   let 〈lp, lh〉 ≝ left in
    39   let 〈rp, rh〉 ≝ right in
    40     〈set_diff … lp rp, set_diff … lh rh〉.
     36pairwise ?? (set_diff …) (set_diff …).
    4137
    4238definition defined ≝
Note: See TracChangeset for help on using the changeset viewer.