Changeset 2922


Ignore:
Timestamp:
Mar 21, 2013, 2:12:59 AM (4 years ago)
Author:
sacerdot
Message:

Progress: proof of "eliminable statements can be eliminated" almost completed.
Bug there is a bug in the interface of sigma_fb_state: it should take the
current pc, otherwise it does not make sense. Alternatively, it can take
the liveness map already instantiated on the current pc.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ERTLptr/ERTLptrToLTLProof.ma

    r2898 r2922  
    340340<associative_append @split_on_last_append_singl
    341341qed.
     342
     343lemma injective_OK: ∀A:Type[0].∀a,b:A. OK … a = OK … b → a=b.
     344 #A #a #b #EQ destruct %
     345qed.
     346
     347lemma eq_notb_true_to_eq_false:
     348 ∀b. (¬b) = true → b = false.
     349* // #abs normalize in abs; destruct
     350qed.
     351
     352axiom sigma_fb_state_insensitive_to_dead_reg:
     353 ∀fix_comp,colour,prog.
     354 let p_in ≝
     355   mk_prog_params ERTLptr_semantics prog
     356   (lookup_stack_cost (\snd  (\fst  (ertlptr_to_ltl fix_comp colour prog)))) in
     357 ∀fn,f_lbls,f_regs,bv.
     358 ∀st: joint_abstract_status p_in.
     359 ∀r: register.
     360 let live ≝
     361  analyse_liveness fix_comp (prog_var_names (joint_function ERTLptr) ℕ prog) fn
     362 in
     363  set_member (identifier RegisterTag) (eq_identifier RegisterTag) r
     364   (\fst  (live (point_of_pc ERTLptr_semantics (pc p_in st)))) = false →
     365  sigma_fb_state prog f_lbls f_regs
     366   (to_be_cleared_fb live)
     367   (set_regs ERTLptr_semantics
     368    〈reg_store r bv (\fst  (regs ERTLptr_semantics (st_no_pc … st))),
     369    \snd  (regs ERTLptr_semantics (st_no_pc … st))〉 (st_no_pc … st))
     370  = sigma_fb_state prog f_lbls f_regs (to_be_cleared_fb live) (st_no_pc … st).
     371
     372axiom sigma_fb_state_insensitive_to_dead_Reg:
     373 ∀fix_comp,colour,prog.
     374 let p_in ≝
     375   mk_prog_params ERTLptr_semantics prog
     376   (lookup_stack_cost (\snd  (\fst  (ertlptr_to_ltl fix_comp colour prog)))) in
     377 ∀fn,f_lbls,f_regs,bv.
     378 ∀st: joint_abstract_status p_in.
     379 ∀r: Register.
     380 let live ≝
     381  analyse_liveness fix_comp (prog_var_names (joint_function ERTLptr) ℕ prog) fn
     382 in
     383  set_member Register eq_Register r
     384   (\snd  (live (point_of_pc ERTLptr_semantics (pc p_in st)))) = false →
     385  sigma_fb_state prog f_lbls f_regs
     386   (to_be_cleared_fb live)
     387   (set_regs ERTLptr_semantics
     388     〈\fst  (regs ERTLptr_semantics (st_no_pc … st)),
     389      hwreg_store r bv (\snd  (regs ERTLptr_semantics (st_no_pc … st)))〉
     390      (st_no_pc … st))
     391  = sigma_fb_state prog f_lbls f_regs
     392   (to_be_cleared_fb live) (st_no_pc … st).
     393
     394axiom sigma_fb_state_insensitive_to_dead_carry:
     395 ∀fix_comp,colour,prog.
     396 let p_in ≝
     397   mk_prog_params ERTLptr_semantics prog
     398   (lookup_stack_cost (\snd  (\fst  (ertlptr_to_ltl fix_comp colour prog)))) in
     399 ∀fn,f_lbls,f_regs,bv.
     400 ∀st: joint_abstract_status p_in.
     401 let live ≝
     402  analyse_liveness fix_comp (prog_var_names (joint_function ERTLptr) ℕ prog) fn
     403 in
     404  set_member Register eq_Register RegisterCarry
     405   (\snd  (live (point_of_pc ERTLptr_semantics (pc p_in st)))) = false →
     406  sigma_fb_state prog f_lbls f_regs
     407  (to_be_cleared_fb live)
     408  (set_carry ERTLptr_semantics bv (st_no_pc … st))
     409  = sigma_fb_state prog f_lbls f_regs (to_be_cleared_fb live) (st_no_pc … st).
     410
     411lemma split_orb_false: ∀a,b:bool. orb a b = false → a = false ∧ b = false.
     412 ** normalize #abs destruct /2/
     413qed.
     414
     415lemma sigma_fb_state_insensitive_to_eliminable:
     416 ∀fix_comp: fixpoint_computer.
     417 ∀colour: coloured_graph_computer.
     418 ∀prog: ertlptr_program.
     419 let p_in ≝
     420   mk_prog_params ERTLptr_semantics prog
     421   (lookup_stack_cost (\snd  (\fst  (ertlptr_to_ltl fix_comp colour prog)))) in
     422 ∀f,fn,f_lbls,f_regs.
     423 ∀st1 : joint_abstract_status p_in.
     424 ∀st1_no_pc,stms.
     425 ∀Heval_seq_no_pc:
     426   eval_seq_no_pc ERTLptr_semantics
     427   (prog_var_names (joint_function ERTLptr_semantics) ℕ prog)
     428   (ev_genv
     429    (mk_prog_params ERTLptr_semantics prog
     430     (lookup_stack_cost (\snd  (\fst  (ertlptr_to_ltl fix_comp colour prog))))))
     431   f stms (st_no_pc … st1)
     432   =return st1_no_pc.
     433 ∀Heliminable:
     434   eliminable_step (globals p_in)
     435   (analyse_liveness fix_comp (globals p_in) fn
     436    (point_of_pc ERTLptr_semantics (pc p_in st1))) stms
     437   =true.
     438 (sigma_fb_state prog f_lbls f_regs
     439  (to_be_cleared_fb
     440   (analyse_liveness fix_comp (prog_var_names (joint_function ERTLptr) ℕ prog)
     441    fn))
     442  st1_no_pc
     443  =sigma_fb_state prog f_lbls f_regs
     444   (to_be_cleared_fb
     445    (analyse_liveness fix_comp (prog_var_names (joint_function ERTLptr) ℕ prog)
     446     fn))
     447   (st_no_pc … st1)).
     448#fix_comp #colour #prog letin p_in ≝ (mk_prog_params ???) #f #fn #f_lbls #f_regs
     449#st1 #st1' *
     450try (#arg1 #arg2 #arg3 #arg4 #arg5 #Heval #Helim)
     451try (#arg1 #arg2 #arg3 #arg4 #Heval #Helim)
     452try (#arg1 #arg2 #arg3 #Heval #Helim) try (#arg1 #arg2 #Heval #Helim)
     453try (#arg1 #Heval #Helim) try (#Heval #Helim)
     454whd in Heval:(??%?);
     455whd in Helim:(??%?); try (change with (false=true) in Helim; destruct (Helim))
     456[7: inversion arg1 in Heval Helim; [ * [3: #arg2 ] |*: #arg2 #arg3 ] #Harg1
     457    normalize nodelta ] try #Heval try #Helim whd in Heval:(??%?);
     458    try (change with (false=true) in Helim; destruct (Helim))
     459    [4,8: cases arg1 in Heval Helim; normalize nodelta
     460      [ * normalize nodelta #arg10 #arg11] #Heval #Helim]
     461lapply (eq_notb_true_to_eq_false ? Helim) -Helim #Helim
     462[1,2: cases arg11 in Heval; [1,3: *] #arg12 whd in ⊢ (??%? → ?);
     463  [1,3: whd in match (pair_reg_move_ ?????); normalize nodelta
     464        inversion ps_reg_retrieve normalize nodelta
     465        [2,4: #error #_ #abs whd in abs:(???%); destruct (abs) ]
     466        #bv #EQbv ]
     467|3,4,5,6,7,8,13: inversion (acca_arg_retrieve ERTLptr_semantics) in Heval;
     468    [2,4,6,8,10,12,14: #error #_ #abs whd in abs:(??%%); destruct (abs) ]
     469    #bv normalize nodelta #EQbv #X cases (bind_inversion ????? X) -X
     470    #v1 * #Hv1 #X cases (bind_inversion ????? X) -X
     471    #vres * #Hvres #X cases (bind_inversion ????? X) -X
     472    #st1'' * #Hst1''
     473|9: inversion (opt_to_res ???) in Heval;
     474    [2: #error #_ #abs whd in abs:(??%%); destruct (abs) ]
     475    #bv normalize nodelta #EQbv
     476|10,11: inversion (get_pc_from_label ?????) in Heval;
     477     [2,4: #error #_ #abs whd in abs:(??%%); destruct (abs) ]
     478     #bv normalize nodelta #EQbv
     479|12: lapply Heval -Heval
     480|14: inversion (acca_retrieve ???) in Heval;
     481    [2: #error #_ #abs whd in abs:(??%%); destruct (abs) ]
     482    #bv normalize nodelta #EQbv #X cases (bind_inversion ????? X) -X
     483    #v1 * #Hv1
     484|15: inversion (dph_arg_retrieve ???) in Heval;
     485    [2: #error #_ #abs whd in abs:(??%%); destruct (abs) ]
     486    #bv normalize nodelta #EQbv #X cases (bind_inversion ????? X) -X
     487    #v1 * #Hv1 #X cases (bind_inversion ????? X) -X
     488    #vres * #Hvres #X cases (bind_inversion ????? X) -X
     489    #v1 * #Hv2 ]
     490whd in ⊢ (??%% → ?); #X <(injective_OK ??? X) -X
     491try (cases (split_orb_false … Helim) -Helim #Helim1 #Helim2)
     492try (@sigma_fb_state_insensitive_to_dead_reg assumption)
     493try (@sigma_fb_state_insensitive_to_dead_Reg assumption)
     494try (@sigma_fb_state_insensitive_to_dead_carry assumption)
     495[ <(injective_OK ??? Hst1'') XXX
     496  >sigma_fb_state_insensitive_to_dead_carry assumption
     497 @sigma_fb_state_insensitive_to_dead_carry
    342498
    343499lemma make_ERTLptr_To_LTL_good_state_relation :
     
    435591        >(pc_of_label_eq … EQt_fn1) <(pc_eq_sigma_commute … good … EQfn Rst1st2) %
    436592  ]
    437 | xxxxxxxxxxxx
    438  letin p_in ≝ (mk_prog_params ERTLptr_semantics ??)
    439   letin p_out ≝ (mk_prog_params LTL_semantics ??)
     593| letin p_in ≝ (mk_prog_params ERTLptr_semantics ??)
     594  letin p_out ≝ (mk_prog_params LTL_semantics ??)
    440595  letin trans_prog ≝ (b_graph_transform_program ????)
    441   #st1 #st1' #st2 #f #fn *
     596  #st1 #st1' #st2 #f #fn
     597  #stms #nxt #EQfetch whd in match eval_state in ⊢ (% → ?);
     598  normalize nodelta >EQfetch >m_return_bind #H @('bind_inversion H) -H
     599  #st1_no_pc whd in match eval_statement_no_pc in ⊢ (% → ?); normalize nodelta
     600  #Heval_seq_no_pc
     601  whd in match eval_statement_advance; normalize nodelta
     602  whd in ⊢ (??%% → ?); #EQ destruct(EQ)
     603  whd in ⊢ (% → ?); #Rst1st2 #t_fn #EQt_fn
     604  whd normalize nodelta
     605  change with p_out in match p_out;
     606  change with p_in in match p_in;
     607  change with trans_prog in match trans_prog;
     608  inversion eliminable_step #Heliminable normalize nodelta %
     609  [ @([ ])
     610  | % [%] % [2: % [%] | skip] whd
     611    cases(fetch_statement_inv … EQfetch) #EQfn #EQstmt >EQfn
     612    % [2: % [2: % [%] | skip] | skip]
     613    (* CSC: BEGIN cut&paste from previous case: make lemma? *)
     614    lapply Rst1st2 whd in ⊢ (% → ?); whd in match sigma_fb_state_pc;
     615    whd in match sigma_sb_state_pc; normalize nodelta >EQfn
     616    <(pc_eq_sigma_commute … good … EQfn Rst1st2) >EQfn
     617    normalize nodelta #EQ cases(state_pc_eq … EQ) *
     618    #EQst1st2 #_ #_
     619    (* CSC: END *)
     620    <EQst1st2 whd in EQst1_no_pc:(??%%); whd in match (st_no_pc ??);
     621
     622
     623       
     624       
     625       
     626        <(injective_OK ??? EQst1_no_pc)
     627        change with (set_regs ???) in match (st_no_pc ??);
     628 
     629 
     630  *
    442631  [7: #op1 #dest #src #nxt #EQfetch whd in match eval_state in ⊢ (% → ?);
    443632      normalize nodelta >EQfetch >m_return_bind #H @('bind_inversion H) -H
     
    454643      change with p_in in match p_in;
    455644      change with trans_prog in match trans_prog;
     645      inversion eliminable_step #Heliminable normalize nodelta %
     646      [ @([ ])
     647      | % [%] % [2: % [%] | skip] whd
     648        cases(fetch_statement_inv … EQfetch) #EQfn #EQstmt >EQfn
     649        % [2: % [2: % [%] | skip] | skip]
     650        (* CSC: BEGIN cut&paste from previous case: make lemma? *)
     651        lapply Rst1st2 whd in ⊢ (% → ?); whd in match sigma_fb_state_pc;
     652        whd in match sigma_sb_state_pc; normalize nodelta >EQfn
     653        <(pc_eq_sigma_commute … good … EQfn Rst1st2) >EQfn
     654        normalize nodelta #EQ cases(state_pc_eq … EQ) *
     655        #EQst1st2 #_ #_
     656        (* CSC: END *)
     657        <EQst1st2 whd in EQst1_no_pc:(??%%); <(injective_OK ??? EQst1_no_pc)
     658        change with (set_regs ???) in match (st_no_pc ??);
     659
     660       
     661       
     662       
     663       
     664       
     665       
     666       
     667         destruct (EQst1_no_pc)
     668       
     669        <(insensitive_to_be_cleared_sb … prog f_lbls f_regs … st2 …
     670          (point_of_pc ERTLptr_semantics (pc … st2)))
     671                     [2,4: @dead_registers_in_dead @acc_is_dead ]
     672                     assumption
     673     
     674      Rst1st2
     675     
    456676      % [2: % [ % | ] | skip]
    457677qed.
Note: See TracChangeset for help on using the changeset viewer.