Changeset 2938


Ignore:
Timestamp:
Mar 22, 2013, 2:11:59 AM (4 years ago)
Author:
sacerdot
Message:
  1. proof of "all eliminable are eliminable" completed
  2. the notion of state_rel in the helpers file needs to be generalized to accomodate the dependency on the program counter
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ERTLptr/ERTLptrToLTLProof.ma

    r2930 r2938  
    102102
    103103definition state_rel : fixpoint_computer → coloured_graph_computer →
    104 ertlptr_program → (Σb:block.block_region b = Code) → label →
    105  state ERTL_state → state LTL_LIN_state → Prop ≝
     104ertlptr_program →
     105 (Σb:block.block_region b = Code) → label → state ERTL_state → state LTL_LIN_state → Prop ≝
    106106λfix_comp,build,prog,bl,pc,st1,st2.
    107107∃f,fn.fetch_internal_function ? (globalenv_noinit … prog) bl = return 〈f,fn〉 ∧
     
    349349 ∀fix_comp,prog,fn,bv. ∀st: state ERTLptr_semantics. ∀l:label.
    350350 ∀r: register.
    351  let live ≝
    352   analyse_liveness fix_comp (prog_var_names (joint_function ERTLptr) ℕ prog) fn in
     351 let live ≝
     352  analyse_liveness fix_comp (prog_var_names (joint_function ERTLptr) ℕ prog) fn
     353 in
    353354  set_member (identifier RegisterTag) (eq_identifier RegisterTag) r
    354    (\fst  (live l)) = false →
     355   (\fst  (livebefore … fn l live)) = false →
    355356  sigma_fb_state prog
    356357   (to_be_cleared_fb live l)
     
    363364 ∀fix_comp,prog,fn,bv. ∀st: state ERTLptr_semantics. ∀l:label.
    364365 ∀r: Register.
    365  let live ≝
     366 let live ≝ 
    366367  analyse_liveness fix_comp (prog_var_names (joint_function ERTLptr) ℕ prog) fn
    367368 in
    368   set_member Register eq_Register r (\snd  (live l)) = false →
     369  set_member Register eq_Register r (\snd  (livebefore … fn l live)) = false →
    369370  sigma_fb_state prog
    370371   (to_be_cleared_fb live l)
     
    377378axiom sigma_fb_state_insensitive_to_dead_carry:
    378379 ∀fix_comp,prog,fn,bv. ∀st: state ERTLptr_semantics. ∀l:label.
    379  let live ≝
     380 let live ≝ 
    380381  analyse_liveness fix_comp (prog_var_names (joint_function ERTLptr) ℕ prog) fn
    381382 in
    382   set_member Register eq_Register RegisterCarry (\snd (live l)) = false →
     383  set_member Register eq_Register RegisterCarry (\snd (livebefore … fn l live)) = false →
    383384   sigma_fb_state prog (to_be_cleared_fb live l) (set_carry ERTLptr_semantics bv st) =
    384385   sigma_fb_state prog (to_be_cleared_fb live l) st.
     
    386387lemma split_orb_false: ∀a,b:bool. orb a b = false → a = false ∧ b = false.
    387388 ** normalize #abs destruct /2/
     389qed.
     390
     391lemma eta_set_carry:
     392 ∀P,st. set_carry P (carry P st) st = st.
     393#P * //
     394qed.
     395
     396lemma set_carry_set_regs_commute:
     397 ∀P,st,c,v. set_carry P c (set_regs P v st) = set_regs P v (set_carry P c st).
     398 #P * //
     399qed.
     400
     401lemma eliminable_step_to_eq_livebefore_liveafter:
     402 ∀fix_comp,colour,prog,fn.
     403 let p_in ≝
     404   mk_prog_params ERTLptr_semantics prog
     405   (lookup_stack_cost (\snd  (\fst  (ertlptr_to_ltl fix_comp colour prog)))) in
     406 ∀st1: joint_abstract_status p_in.
     407 ∀stms: joint_seq ERTLptr_semantics (prog_var_names … prog). ∀next.
     408 let pt ≝ point_of_pc ERTLptr_semantics (pc ? st1) in
     409 stmt_at p_in ? (joint_if_code p_in … fn) pt = return (sequential … stms next) →
     410 let liveafter ≝ analyse_liveness fix_comp (globals p_in) fn in
     411 eliminable_step (globals p_in) (liveafter (point_of_pc ERTLptr_semantics (pc … st1))) stms = true →
     412  livebefore … fn pt liveafter = liveafter pt.
     413 #fix_comp #colour #prog #fn #st1 #stms #next #stmt_at #Helim
     414 whd in ⊢ (??%?); whd in stmt_at:(??%?); cases (lookup ????) in stmt_at;
     415 normalize nodelta try (#abs whd in abs:(??%%); destruct (abs) @I)
     416 #stms' #EQ whd in EQ:(??%%); destruct (EQ) whd in ⊢ (??%?);
     417 whd in match eliminable; normalize nodelta >Helim %
    388418qed.
    389419
     
    398428 ∀st1 : joint_abstract_status p_in.
    399429 let pt ≝ point_of_pc ERTLptr_semantics (pc ? st1) in
    400  ∀st1_no_pc,stms.
     430 ∀st1_no_pc. ∀stms: joint_seq ERTLptr_semantics (prog_var_names … prog). ∀next.
     431 stmt_at p_in … (joint_if_code p_in … fn) pt = return (sequential … stms next) →
    401432 ∀Heval_seq_no_pc:
    402433   eval_seq_no_pc ERTLptr_semantics
     
    423454   (st_no_pc … st1)).
    424455#fix_comp #colour #prog letin p_in ≝ (mk_prog_params ???) #f #fn
    425 #st1 #st1' *
     456#st1 #st1' #stms #next #stmt_at #Heval #Helim
     457lapply (eliminable_step_to_eq_livebefore_liveafter … stmt_at Helim)
     458#EQ_livebefore_after -next
     459cases stms in Heval Helim;
    426460try (#arg1 #arg2 #arg3 #arg4 #arg5 #Heval #Helim)
    427461try (#arg1 #arg2 #arg3 #arg4 #Heval #Helim)
     
    466500whd in ⊢ (??%% → ?); #X <(injective_OK ??? X) -X
    467501try (cases (split_orb_false … Helim) -Helim #Helim1 #Helim2)
    468 try (@sigma_fb_state_insensitive_to_dead_reg assumption)
    469 try (@sigma_fb_state_insensitive_to_dead_Reg assumption)
    470 try (@sigma_fb_state_insensitive_to_dead_carry assumption)
     502try (@sigma_fb_state_insensitive_to_dead_reg >EQ_livebefore_after assumption)
     503try (@sigma_fb_state_insensitive_to_dead_Reg >EQ_livebefore_after assumption)
     504try (@sigma_fb_state_insensitive_to_dead_carry >EQ_livebefore_after assumption)
    471505[1,2,3,4,5,6,7: <(injective_OK ??? Hst1'') ]
    472506[1,2,3:
    473   >sigma_fb_state_insensitive_to_dead_carry try assumption
    474   @sigma_fb_state_insensitive_to_dead_reg assumption
    475 |4,5,6: (* BUG! *)
    476 |7: >sigma_fb_state_insensitive_to_dead_reg try assumption
     507  >sigma_fb_state_insensitive_to_dead_carry try (>EQ_livebefore_after assumption)
     508  @sigma_fb_state_insensitive_to_dead_reg >EQ_livebefore_after assumption
     509|4: whd in Hvres:(??%%); cases Byte_of_val in Hvres; normalize nodelta
     510    [2: #error #abs destruct (abs) ]
     511    #by #Hvres; cases (bind_inversion ????? Hvres) #by' * #_ #EQ
     512    whd in EQ:(??%%); destruct (EQ) >set_carry_set_regs_commute >eta_set_carry
     513    @sigma_fb_state_insensitive_to_dead_reg >EQ_livebefore_after assumption
     514|5,6: whd in Hvres:(??%%); cases bv in Hvres; normalize nodelta
     515      try (#x1 #x2 #x3 #Hvres) try (#x1 #x2 #Hvres) try (#x1 #Hvres) try #Hvres
     516      try (destruct (Hvres) @I) cases v1 in Hvres; normalize nodelta
     517      try (#x1' #x2' #x3' #Hvres) try (#x1' #x2' #Hvres) try (#x1' #Hvres) try #Hvres
     518      try (destruct (Hvres) @I)
     519      [5: cases orb in Hvres; normalize nodelta try (#Hvres destruct(Hvres) @I)
     520          cases andb normalize nodelta #Hvres
     521      |9,10,11,12: cases cic:/matita/arithmetics/nat/eqb.fix(0,0,1) in Hvres;
     522          normalize nodelta try (#abs destruct(abs) @I) #Hvres ]
     523      whd in Hvres:(??%%); destruct (Hvres) >set_carry_set_regs_commute >eta_set_carry
     524      @sigma_fb_state_insensitive_to_dead_reg >EQ_livebefore_after assumption
     525|7: cases (split_orb_false … Helim1) -Helim1 #Helim1 #Helim3
     526   >sigma_fb_state_insensitive_to_dead_reg try (>EQ_livebefore_after assumption)
     527   @sigma_fb_state_insensitive_to_dead_reg >EQ_livebefore_after assumption
     528|8: >sigma_fb_state_insensitive_to_dead_reg try (>EQ_livebefore_after assumption)
     529    @sigma_fb_state_insensitive_to_dead_reg >EQ_livebefore_after assumption ]
     530qed.
    477531
    478532lemma make_ERTLptr_To_LTL_good_state_relation :
     
    490544good_state_relation ERTLptr_semantics LTL_semantics prog stacksizes
    491545 (λglobals,fn.«translate_data fix_comp colour globals fn,(refl …)»)
    492  init_regs f_lbls f_regs good (state_rel fix_comp colour prog f_lbls f_regs)
     546 init_regs f_lbls f_regs good (state_rel fix_comp colour prog)
    493547 (sem_rel … (ERTLptr_to_LTL_StatusSimulation fix_comp colour prog … good)).
    494548#fix_comp #colour #prog
Note: See TracChangeset for help on using the changeset viewer.