Ignore:
Timestamp:
Mar 22, 2013, 7:16:17 PM (8 years ago)
Author:
sacerdot
Message:
  1. StatusSimulationHelper? changed to allow to use status_rel that depends on the pc (necessary for ERTLptrToLTL)
  2. partial repairing of ERTLToERTLptrOK.ma, still in progress
  3. some progress in ERTLptrToLTLProof, but: a) some axioms were wrong, once fixed we now see some proof obligations

related to liveness analysis. Example: the variables live before and
after a COND must be the same. I have put daemons for the time being.

b) I strongly suspect that Interference should be changed to use livebefore,

in the correctness conditions (now it uses liveafter, the two sets
are probably equivalent for correct programs, but one is simpler to use:
which one?)

c) to_be_cleared_* must consult livebefore, but it is now passed liveafter.

Passing liveafter is necessary to typechek the graph, unless we do
b) first. Passing only the set computed by livebefore would be so much
better.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ERTLptr/ERTLptrToLTLProof.ma

    r2938 r2940  
    530530qed.
    531531
     532axiom to_be_cleared_sb_respects_equal_valuations:
     533 ∀live,coloured,l1,l2.
     534  live l1 = live l2 →
     535   to_be_cleared_sb live coloured l1 = to_be_cleared_sb live coloured l2.
     536
     537axiom to_be_cleared_fb_respects_equal_valuations:
     538 ∀live,l1,l2.
     539  live l1 = live l2 →
     540   to_be_cleared_fb live l1 = to_be_cleared_fb live l2.
     541
    532542lemma make_ERTLptr_To_LTL_good_state_relation :
    533543∀fix_comp,colour,prog.
     
    601611                     normalize nodelta #EQ cases(state_pc_eq … EQ) *
    602612                     #EQst1st2 #_ #_ whd %{f} %{fn} %{EQfn}
    603                      <(insensitive_to_be_cleared_sb … prog f_lbls f_regs … st2 …
    604                                           (point_of_pc ERTLptr_semantics (pc … st2)))
     613                     <(insensitive_to_be_cleared_sb prog … st2)
    605614                     [2,4: @dead_registers_in_dead @acc_is_dead ]
    606                      assumption
     615                     whd >point_of_pc_of_point
     616                     [ cut
     617                        (analyse_liveness fix_comp … fn ltrue =
     618                          analyse_liveness fix_comp … fn
     619                          (point_of_pc ERTLptr_semantics (pc … st1)))
     620                       [ cases daemon (*CSC: Genuine proof obligation! *)
     621                       | #Hext ]
     622                     |  cut
     623                        (analyse_liveness fix_comp … fn lfalse =
     624                          analyse_liveness fix_comp … fn
     625                          (point_of_pc ERTLptr_semantics (pc … st1)))
     626                       [ cases daemon (*CSC: Genuine proof obligation! *)
     627                       | #Hext ]]
     628                     >(to_be_cleared_sb_respects_equal_valuations …
     629                        (colour … fn …) … Hext) <EQst1st2
     630                     >(to_be_cleared_fb_respects_equal_valuations … Hext) %
    607631                 ]
    608632            |*: %
Note: See TracChangeset for help on using the changeset viewer.