Changeset 3388


Ignore:
Timestamp:
Aug 27, 2013, 6:11:57 PM (6 years ago)
Author:
piccolo
Message:

partial commit

Files:
3 edited

Legend:

Unmodified
Added
Removed

  • LTS/Simulation.ma

    r3387 r3388  
    1010 ∀s1,s1'. as_syntactical_succ S s1 s → Crel … rel s1 s1' → as_syntactical_succ S s1' s'.
    1111
    12 record simulation_conditions (S : abstract_status) (rel : relations S) : Type[0] ≝
     12record simulation_conditions (S : abstract_status) (rel : relations S) : Prop ≝
    1313 { simulate_tau:
    1414     ∀s1,s2,s1' : S.
    … …  
    1616      Srel … rel s1 s2 →
    1717      ∃s2'. ∃t: raw_trace S s2 s2'.
    18         Srel … rel s2 s2' ∧ silent_trace … t
     18        Srel … rel s1' s2' ∧ silent_trace … t
    1919 ; simulate_label:
    2020     ∀s1,s2,l,s1'.
    2121      as_execute S (cost_act (Some ? l)) s1 s1' →
     22      as_classify … s1' ≠ cl_io →
    2223      Srel … rel s1 s2 →
    2324      ∃s2',s2'',s2'''.
    2425       ∃t1: raw_trace S s2 s2'.
    25        as_execute … (cost_act (Some ? l)) s2' s2'' ∧
     26       as_execute … (cost_act (Some ? l)) s2' s2'' ∧ as_classify … s2'' ≠ cl_io ∧
    2627       ∃t3: raw_trace S s2'' s2'''.
    2728        Srel … rel  s1' s2''' ∧ silent_trace … t1 ∧ silent_trace … t3
    … …  
    3031      is_call_post_label … s1 →
    3132      as_execute … (call_act f l) s1 s1' →
     33      as_classify … s1' ≠ cl_io →
    3234      Srel … rel s1 s2 →
    3335      ∃s2',s2'',s2'''.
    3436       ∃t1: raw_trace S s2 s2'.
     37       as_classify … s2' ≠ cl_jump ∧
    3538       as_execute … (call_act f l) s2' s2'' ∧
     39       bool_to_Prop(is_call_post_label … s2') ∧
     40       as_classify … s2'' ≠ cl_io ∧
    3641       ∃t3: raw_trace S s2'' s2'''.
    3742        Srel … rel s1' s2''' ∧ silent_trace … t1 ∧ silent_trace … t3
    … …  
    3944     ∀s1,s2,s1' : S.∀l.
    4045      as_execute S (ret_act (Some ? l)) s1 s1' →
     46      as_classify … s1' ≠ cl_io →
    4147      Srel  … rel s1 s2 →
    4248      ∃s2',s2'',s2'''.
    4349       ∃t1: raw_trace S s2 s2'.
     50       as_classify … s2' ≠ cl_jump ∧
    4451       as_execute … (ret_act (Some ? l)) s2' s2'' ∧
     52       as_classify … s2'' ≠ cl_io ∧
    4553       ∃t3: raw_trace S s2'' s2'''.
    46         Srel … rel s2 s2''' ∧ silent_trace … t1 ∧ silent_trace … t3
     54        Srel … rel s1' s2''' ∧ silent_trace … t1 ∧ silent_trace … t3
    4755 ; simulate_call_n:
    4856     ∀s1,s2,s1' : S.∀f,l.
    … …  
    8997
    9098
     99lemma append_premeasurable_silent : ∀S : abstract_status.
     100∀st1',st1,st2 : S.∀t : raw_trace S st1 st2.∀t' : raw_trace S st1' st1.
     101pre_measurable_trace … t → pre_silent_trace … t' → as_classify … st1' ≠ cl_io →
     102pre_measurable_trace … (t' @ t).
     103#S #st1' #st1 #st2 #t #t' lapply t -t elim t'
     104[ #st #t #Hpre #_ #_ whd in ⊢ (????%); assumption]
     105#s1 #s2 #s3 #l #prf #tl #IH #t #Hpre #H inversion H in ⊢ ?;
     106[ #s #EQ1 #EQ2 destruct #EQ destruct]
     107#s1' #s2' #s3' #prf' #tl' #Hclass #silent_tl' #_ #EQ1 #EQ2 #EQ3
     108destruct #_ #Hs1' whd in ⊢ (????%); %2
     109[ assumption
     110| %{(None ?)} %
     111| @IH try assumption >Hclass % #EQ destruct
     112]
     113qed.
     114
     115definition is_trace_non_empty : ∀S : abstract_status.∀st1,st2.
     116raw_trace S st1 st2 → bool ≝
     117λS,st1,st2,t.match t with [ t_base _ ⇒ false | _ ⇒ true ].
     118
     119lemma append_well_formed_silent : ∀S : abstract_status.
     120∀st1',st1,st2 : S.∀t : raw_trace S st1 st2.∀t' : raw_trace S st1' st1.
     121well_formed_trace … t → pre_silent_trace … t' →
     122(is_trace_non_empty … t' → as_classify … st1' = cl_other) →
     123well_formed_trace … (t' @ t).
     124#S #st1' #st1 #st2 #t #t' lapply t -t elim t'
     125[ #st #t #H #_ #_ assumption ]
     126#s1' #s2' #s3' #l #prf #tl #IH #t #well_formed_t #H
     127inversion H in ⊢ ?;
     128[ #st #EQ1 #EQ2 #EQ3 destruct]
     129#st1'' #st2' #st3' #prf' #tl' #Hclass #silent_tl #_
     130#EQ1 destruct #EQ #EQ1 destruct #_ #Hclass1 %2
     131[2: >(Hclass1 I) % #EQ destruct]
     132@IH try assumption #_ assumption
     133qed.
     134
     135lemma get_cost_label_invariant_for_append_silent_trace_l :∀S : abstract_status.
     136∀st1,st2,st3 : S.∀t1 : raw_trace S st1 st2.∀t2 : raw_trace S st2 st3.
     137pre_silent_trace … t1 →
     138get_costlabels_of_trace … (t1 @ t2) = get_costlabels_of_trace … t2.
     139#S #st1 #st2 #st3 #t1 elim t1
     140[#st #t2 #_ %] #st1' #st2' #st3' #l' #prf #tl #IH #t2 #H
     141inversion H in ⊢ ?; [ #st #EQ1 #EQ2 #EQ3 destruct]
     142#st1'' #st2'' #st3'' #prf'' #tl'' #Hclass #Htl'' #_ #EQ1 #EQ2 #EQ3 destruct
     143#_ whd in ⊢ (??%?); >IH [%] assumption
     144qed.
     145
     146(*
     147lemma raw_trace_ind_r : ∀S : abstract_status.
     148∀P : (∀st1,st2.raw_trace S st1 st2 → Prop).
     149(∀st : S.P … (t_base … st)) →
     150(∀st1,st2,st3,l.
     151 ∀prf : as_execute S l st2 st3.
     152 ∀tl : raw_trace S st1 st2. P … tl → P … (tl @ (t_ind … prf … (t_base … st3)))) →
     153∀st1,st2 : S.∀t : raw_trace S st1 st2.P … t.
     154#S #P #base #ind #st1 #st2 #t elim t [ assumption]
     155#st1 #st2 #st3 #l #prf #raw #IH
     156*)
     157
     158
    91159theorem simulates_pre_mesurable:
    92160 ∀S : abstract_status.∀rel : relations S.
    93161 ∀s1,s1' : S. ∀t1: raw_trace S s1 s1'.
     162  simulation_conditions S rel →
    94163  pre_measurable_trace … t1 →
    95   well_formed_trace … t1 → ∀s2.Srel … rel s1 s2 →
    96   ∃s2'. ∃t2: raw_trace … s1' s2'.
     164  well_formed_trace … t1 → ∀s2 : S.
     165  as_classify … s2 ≠ cl_io → Srel … rel s1 s2 →
     166  ∃s2'. ∃t2: raw_trace … s2 s2'.
    97167    pre_measurable_trace … t2 ∧
    98168    well_formed_trace … t2 ∧
    99169    get_costlabels_of_trace … t1 = get_costlabels_of_trace … t2 ∧
    100     Srel … rel s2 s2'.
    101 cases daemon (*TODO*)
    102 qed.
     170    Srel … rel s1' s2'.
     171#S #rel #s1 #s1' #t1 #good #pre_measurable elim pre_measurable
     172[ #st #H1 #well_formed #s2 #H2 #REL %{s2} %{(t_base …)}
     173  /8 by refl, pm_empty, wf_empty, conj/
     174| #st1 #st2 #st3 #l #execute #tl #ClASS ** [|#c] #EQ destruct
     175  #pre_measurable_tl #IH #well_formed #s2 #classify_s2 #REL
     176  [ cases(simulate_tau … good … execute … REL) #s2'' * #t_s2'' * #RELst2s2''
     177    * #silent_ts2'' #Hclass_s2 cases(IH … RELst2s2'')
     178    [2: cases(well_formed_trace_inv … well_formed)
     179         [2: * #st2''' * #l''' * #prf''' * #tl''' ** #H #_
     180             #EQ destruct(EQ) assumption
     181         | *
     182            [2: * #st2''' * #l''' * #prf''' * #tl''' ** #H #_ #EQ destruct
     183                assumption
     184            | * #EQ1 #EQ2 destruct
     185            ]
     186         ]
     187    |3: @(silent_io … silent_ts2'')  assumption   
     188    ]
     189    #s3 * #ts3 *** #pre_meas_ts3 #well_formed_ts3 #EQcost #RELst3s3
     190    %{s3} %{(t_s2'' @ ts3)} % [2: assumption] %
     191    [ %
     192      [ @append_premeasurable_silent assumption
     193      | @append_well_formed_silent assumption
     194      ]
     195    | whd in ⊢ (??%?); >EQcost >get_cost_label_invariant_for_append_silent_trace_l
     196      [% | assumption]
     197    ]
     198  | cases(simulate_label … good … execute … REL)
     199    [2: cases pre_measurable_tl
     200        [ #st #H @H
     201        | #st1 #st2 #st3 #l #prf #tl #H #_ #_ @H
     202        | #st1 #st2 #st3 #l #H #_ #tl #_ #_ @H
     203        | #st1 #st2 #st3 #l #_ #tl #H #_ #_ #_ @H
     204        | #st1 #st2 #st3 #st4 #st5 #l1 #l2 #_ #t1 #t2 #_ #H #_ #_ #_ #_ #_ #_ #_ @H
     205        ]
     206    ]
     207    #s2'' * #s2''' * #s2'''' * #t_s2'' ** #exe_s2''' #CLASS' * #t_s2'''' ** #RELst2_s2''''
     208    * #sil_ts2'' #Hclass_s2 * #sil_t_s2'''' #Hclass_s2''' cases(IH … RELst2_s2'''')
     209    [2: cases(well_formed_trace_inv … well_formed)
     210         [2: * #st2''' * #l''' * #prf''' * #tl''' ** #H #_
     211             #EQ destruct(EQ) assumption
     212         | *
     213            [2: * #st2''' * #l''' * #prf''' * #tl''' ** #H #_ #EQ destruct
     214                assumption
     215            | * #EQ1 #EQ2 destruct
     216            ]
     217         ]
     218    |3: @(silent_io … sil_t_s2'''') assumption
     219    ]
     220    #s3 * #t_s3 *** #pre_s3 #well_s3 #EQcost #RElst3s3 %{s3}
     221    %{(t_s2'' @ (t_ind … exe_s2''' …))}  [ @(t_s2'''' @ t_s3) ] % [2: assumption]
     222    %
     223    [ %
     224      [ @append_premeasurable_silent try assumption %2
     225        [ @(silent_io … t_s2'') assumption
     226        | %{(Some ? c)} %
     227        ]
     228        @append_premeasurable_silent assumption
     229      | @append_well_formed_silent try assumption inversion(as_classify … s2'')
     230        #Hclass
     231        [ %3 [2: %{c} %]
     232        |*: %2 [2,4: >Hclass % #EQ destruct]
     233        ]
     234        @append_well_formed_silent assumption
     235      ]
     236    | whd in ⊢ (??%?); >EQcost >get_cost_label_invariant_for_append_silent_trace_l
     237      [2: assumption] whd in ⊢ (???%);
     238      >get_cost_label_invariant_for_append_silent_trace_l
     239      [ % | assumption]
     240    ]
     241  ]
     242| #s2 #s2' #s2'' #l #class_s2 #exe_s2_s2' #tl whd in ⊢ (% → ?); * #ret_lab #EQ destruct(EQ)
     243  #pre_meas_tl #IH #H inversion H
     244  [ #s3 #EQ1 #EQ2 destruct #ABS destruct(ABS) ]
     245  #st1 #st2 #st3 #l #exe_st1_st2 #tl' #wf_tl'
     246  [ #class_no_jump | whd in ⊢ (% → ?); * #nf #EQ destruct(EQ) ]
     247  #_ #EQ1 #EQ2 #EQ3 destruct #_ -H #s2 #class_s2 #RELst1s2
     248  cases(simulate_ret_l … good … exe_st1_st2 … RELst1s2)
     249  [2: inversion pre_meas_tl
     250      try #x1 try #x2 try #x3 try #x4 try #x5 try #x6
     251      try #x11 try #x12 try #x13 try #x14 try #x15 try #x16
     252      try #x17 try #x18 try #x19 try #x20 try #x21 try #x22
     253      try #x37 try #x38 try #x39 try #x30 try #x31 try #x32 try #x33
     254      destruct assumption ]
     255  #s2' * #s2'' * #s2''' * #t1 *** #j_s2' #exe_s2'' #class_s2'' * #t2 ** #rel_s2_s2'''
     256  #sil_t1 #sil_t2
     257  cases(IH … wf_tl' … rel_s2_s2''')
     258  [2: @(silent_io … (proj1 … sil_t2)) assumption]
     259  #s2_fin * #t_fin *** #pre_t_fin #wf_t_fin #EQcost #REL
     260  %{s2_fin} %{(t1 @ (t_ind … exe_s2'' … t2) @ t_fin)} % [2: assumption]
     261  % [2: whd in ⊢ (??%?);
     262        >(get_cost_label_invariant_for_append_silent_trace_l … (proj1 … sil_t1))
     263        whd in ⊢ (???%);
     264        >(get_cost_label_invariant_for_append_silent_trace_l … (proj1 … sil_t2))
     265        @eq_f assumption ]
     266  %
     267  [ @append_premeasurable_silent try assumption [2: @(proj1 … sil_t1)]
     268    %3
     269    [ @(silent_io … (proj1 … sil_t1)) assumption
     270    | whd %{ret_lab} %
     271    | @append_premeasurable_silent try assumption @(proj1 … sil_t2)
     272    ]
     273  | @append_well_formed_silent
     274    [ %2 try assumption @append_well_formed_silent try assumption
     275      [ @(proj1 … sil_t2)
     276      | @(proj2 … sil_t2)
     277      ]
     278    | @(proj1 … sil_t1)
     279    | @(proj2 … sil_t1)
     280    ]
     281  ]
     282| #s2 #s2' #s2'' #l #exe_s2_s2' #tl #class_s2 whd in ⊢ (% → ?); * #f * #lab #EQ destruct
     283  #post #pre_tl #IH #H inversion H [ #s3 #EQ1 #EQ2 destruct #ABS destruct(ABS) ]
     284  #st1 #st2 #st3 #l #exe_st1_st2 #tl' #wf_tl'
     285  [#class_no_jump | whd in ⊢ (% → ?); * #nf #EQ destruct(EQ) ]
     286   #_ #EQ1 #EQ2 #EQ3 destruct #_ -H #s2 #io_s2 #REL_st1_s2
     287   cases(simulate_call_pl … good … post … exe_st1_st2 … REL_st1_s2)
     288   [2: inversion pre_tl
     289      try #x1 try #x2 try #x3 try #x4 try #x5 try #x6
     290      try #x11 try #x12 try #x13 try #x14 try #x15 try #x16
     291      try #x17 try #x18 try #x19 try #x20 try #x21 try #x22
     292      try #x37 try #x38 try #x39 try #x30 try #x31 try #x32 try #x33
     293      destruct assumption ]
     294   #s2' * #s2'' * #s2''' * #t1 **** #j_s2' #exe_s2'' #post' #io_s2'' * #t2 ** #REL #sil_t1 #sil_t2
     295   cases(IH … wf_tl' … REL)
     296   [2: @(silent_io … (proj1 … sil_t2)) assumption ]
     297   #s2_fin * #t_fin *** #pre_t_fin #wf_t_fin #EQcost #REL1 %{s2_fin}
     298   %{(t1 @ (t_ind … exe_s2'' … t2) @ t_fin)} % [2: assumption] %
     299   [2: whd in ⊢ (??%?);
     300        >(get_cost_label_invariant_for_append_silent_trace_l … (proj1 … sil_t1))
     301        whd in ⊢ (???%);
     302        >(get_cost_label_invariant_for_append_silent_trace_l … (proj1 … sil_t2))
     303        @eq_f assumption ]
     304   %
     305   [ @append_premeasurable_silent try assumption [2: @(proj1 … sil_t1)]
     306     %4 try assumption
     307     [ @(silent_io … (proj1 … sil_t1)) assumption
     308     | whd %{f} %{lab} %
     309     | @append_premeasurable_silent try assumption @(proj1 … sil_t2)
     310     ]
     311   | @append_well_formed_silent
     312     [ %2 try assumption @append_well_formed_silent try assumption
     313        [ @(proj1 … sil_t2)
     314        | @(proj2 … sil_t2)
     315        ]
     316     | @(proj1 …  sil_t1)
     317     | @(proj2 … sil_t1)
     318     ]
     319   ]
     320| cases daemon (*TODO*)
     321]
     322qed.
     323
     324 
     325 
     326   #st3 #l #class_st1 #exe #tl * #x #EQ destruct(EQ) #pre_tl #IH
     327  #well_formed #s2 #class_s2 #REL cases(simulate_ret_l … good … exe … REL)
     328  #s2'' * #s2''' * #s2'''' * #t1 * #exe' * #t2 ** #Rs2s2'''' #t1_sil #t2_sil
     329  xxxxxxxxx
     330
     331
     332 #st4 #st5 #l1 #l2 * #x #EQ whd in ⊢ (% → ?);   
     333      @append_premeasurable_silent
     334   
     335    xxxxxxxxxxxxxx
     336  ]
     337|*: cases daemon (*TODO*)
     338]
     339qed.*)
    103340
    104341(* IDEA: aggiungere stati di I/O e cambiare la semantica del linguaggio

  • LTS/Traces.ma

    r3387 r3388  
    139139                  well_formed_trace … tl → is_non_silent_cost_act l →
    140140                  well_formed_trace … (t_ind … prf … tl).
     141(*  | wf_cons_io : ∀st1,st2,st3 : S.∀l : ActionLabel.
     142                 ∀prf : as_execute S l st1 st2.∀tl : raw_trace S st2 st3.
     143                 well_formed_trace … tl → as_classify … st1 = cl_io →
     144                 is_non_silent_cost_act l → well_formed_trace … (t_ind … prf … tl).*)
     145
     146lemma well_formed_trace_inv :
     147∀S : abstract_status.∀st1,st2 : S.∀t : raw_trace S st1 st2.
     148well_formed_trace … t →
     149(st1 = st2 ∧ t ≃ t_base S st1) ∨
     150(∃st1'.∃l.∃prf : as_execute S l st1 st1'.∃tl : raw_trace S st1' st2.
     151well_formed_trace … tl ∧ as_classify … st1 ≠ cl_jump ∧
     152t ≃ t_ind … prf … tl) ∨
     153(∃st1'.∃l.∃ prf : as_execute S l st1 st1'.∃ tl : raw_trace S st1' st2.
     154 well_formed_trace … tl ∧ is_non_silent_cost_act l ∧ t ≃ t_ind … prf … tl). (* ∨
     155(∃st1'.∃l.∃prf : as_execute S l st1 st1'.∃tl : raw_trace S st1' st2.
     156 well_formed_trace … tl ∧ as_classify … st1 = cl_io ∧
     157 is_non_silent_cost_act l ∧ t ≃ t_ind … prf … tl).*)
     158#S #st1 #st2 #t #H inversion H
     159[ #st #EQ1 #EQ2 destruct(EQ1 EQ2) #EQ destruct(EQ) #_ /5 by refl_jmeq, or_introl, conj/
     160| #st1' #st2' #st3' #l #prf' #tl' #Htl #Hclass #_ #EQ2 #EQ3 #EQ4 destruct #_
     161  %  %2 %{st2'} %{l} %{prf'} %{tl'} /4 by conj/
     162| #st1' #st2' #st3' #l #prf #tl #Htl #Hl #_ #EQ2 #EQ3 #EQ4 destruct #_ %2 %{st2'}
     163  %{l} %{prf} %{tl} % // % //
     164(*| #st1' #st2' #st3' #l #prf #tl #Htl #Hclass #is_non_silent #_ #EQ1 #EQ2 #EQ3
     165  destruct #_ %2 %{st2'} %{l} %{prf} %{tl} /5 by conj/ *)
     166]
     167qed.
     168
    141169
    142170let rec append_on_trace (S : abstract_status) (st1 : S) (st2 : S) (st3 : S)
    … …  
    166194λS,st1,st2,st3,t1,t2.∃t3 : raw_trace … st1 st2.t2 = t3 @ t1.
    167195
    168 inductive silent_trace (S : abstract_status) :
     196inductive pre_silent_trace (S : abstract_status) :
    169197∀st1,st2 : S.raw_trace S st1 st2 → Prop ≝
    170 | silent_empty : ∀st : S.silent_trace … (t_base S st)
     198| silent_empty : ∀st : S.pre_silent_trace … (t_base S st)
    171199| silent_cons : ∀st1,st2,st3 : S.∀prf : as_execute S (cost_act (None ?)) st1 st2.
    172                 ∀tl : raw_trace S st2 st3. silent_trace … tl →
    173                 silent_trace … (t_ind … prf … tl).
     200                ∀tl : raw_trace S st2 st3. as_classify … st2 = cl_other → pre_silent_trace … tl →
     201                pre_silent_trace … (t_ind … prf … tl).
     202
     203lemma silent_io : ∀S : abstract_status.
     204∀s1,s2 : S. ∀t : raw_trace … s1 s2. pre_silent_trace … t → as_classify … s1 ≠ cl_io →
     205as_classify … s2 ≠ cl_io.
     206#S #s1 #s2 #t elim t [ #st #_ #Hclass @Hclass]
     207#st1 #st2 #st3 #l #prf #tl #IH #H inversion H
     208[ #st' #EQ1 #EQ2 destruct #EQ destruct]
     209#st1' #st2' #st3' #prf' #tl' #Hclass #silent_tl' #_ #EQ1 #EQ2 destruct
     210#EQ destruct #_ #Hclass' @IH [ assumption ] >Hclass % #EQ destruct
     211qed.
     212
     213definition is_trace_non_empty : ∀S : abstract_status.∀st1,st2.
     214raw_trace S st1 st2 → bool ≝
     215λS,st1,st2,t.match t with [ t_base _ ⇒ false | _ ⇒ true ].
     216
     217definition silent_trace : ∀S : abstract_status.∀st1,st2 : S.
     218raw_trace S st1 st2 → Prop ≝ λS,st1,st2,t.pre_silent_trace … t ∧
     219(is_trace_non_empty … t → as_classify … st1 = cl_other).
     220
     221lemma silent_is_well_formed : ∀S : abstract_status.∀st1,st2 : S.
     222∀t : raw_trace S st1 st2. silent_trace … t → well_formed_trace … t.
     223#S #st1 #st2 #t elim t -t
     224[ #st #_ %]
     225#st1' #st2' #st3' #l #prf #tl #IH * #H #cl %2
     226[2: >cl % #EQ destruct]
     227@IH inversion H in ⊢ ?; [ #st #EQ1 #EQ2 #EQ3 destruct]
     228#st1'' #st2'' #st3'' #prf' #tl' #H1 #Htl' #_ #EQ1 #EQ2 #EQ3 destruct #_
     229% [ assumption | #_ assumption]
     230qed.
    174231
    175232inductive pre_measurable_trace (S : abstract_status) :
    … …  
    199256                      is_unlabelled_ret_act l2 →
    200257                      pre_measurable_trace … (t_ind … prf … (t1 @ (t_ind … prf' … t2))).
     258                     
     259lemma pre_measurable_trace_inv : ∀S : abstract_status.
     260∀st1,st2 : S.∀t : raw_trace … st1 st2. pre_measurable_trace … t →
     261(st1 = st2 ∧ as_classify … st1 ≠ cl_io ∧ t ≃ t_base … st1) ∨
     262(∃st1' : S.∃l.∃prf : as_execute S l st1 st1'.∃tl.
     263 t = t_ind … prf … tl ∧ as_classify … st1 ≠ cl_io ∧ is_cost_act l ∧
     264 pre_measurable_trace … tl) ∨
     265(∃st1' : S.∃l.∃prf : as_execute S l st1 st1'.∃tl.
     266 t = t_ind … prf … tl ∧
     267 as_classify … st1 ≠ cl_io ∧ is_labelled_ret_act l ∧ pre_measurable_trace … tl) ∨
     268(∃st1' : S .∃l.∃prf : as_execute S l st1 st1'.∃tl.
     269 t = t_ind … prf … tl ∧ as_classify … st1 ≠ cl_io ∧ is_call_act l ∧
     270 (bool_to_Prop (is_call_post_label … st1)) ∧ pre_measurable_trace … tl) ∨
     271(∃st1',st1'',st1''' : S.∃l1,l2.∃prf : as_execute S l1 st1 st1'.
     272 ∃t1 : raw_trace S st1' st1''.∃t2 : raw_trace S st1''' st2.
     273 ∃prf' : as_execute S l2 st1'' st1'''.
     274 t = t_ind … prf … (t1 @ (t_ind … prf' … t2)) ∧ as_classify … st1 ≠cl_io ∧
     275 as_classify … st1'' ≠ cl_io ∧ is_call_act l1 ∧
     276 bool_to_Prop (¬ is_call_post_label … st1) ∧
     277 pre_measurable_trace … t1 ∧ pre_measurable_trace … t2 ∧
     278 as_syntactical_succ S st1 st1''' ∧ is_unlabelled_ret_act l2).
     279#S #st1 #st2 #t #H inversion H
     280[ #st #Hclass #EQ1 #EQ2 destruct #EQ destruct #_ %%%%% // % //
     281| #st1' #st2' #st3' #l #prf #tl #Hst1' #Hl #Htl #_ #EQ1 #EQ2 #EQ3 destruct #_
     282  %%%%2 %{st2'} %{l} %{prf} %{tl} % // % // % //
     283| #st1' #st2' #st3' #l #Hst1 #prf #tl #Hl #Htl #_ #EQ1 #EQ2 #EQ3 destruct #_
     284  %%%2 %{st2'} %{l} %{prf} %{tl} % // % // % //
     285| #st1' #st2' #st3' #l #prf #tl #Hst1 #Hl #H1st1 #Htl #_ #EQ1 #EQ2 #EQ3 destruct #_
     286  % %2 %{st2'} %{l} %{prf} %{tl} % // % // % // % //
     287| #st1' #st2' #st3' #st4' #st5' #l1 #l2 #prf #t1 #t2 #prf' #Hst1' #Hst3' #Hl1
     288  #H1st1'  #Ht1 #Ht2 #succ #Hl2 #_ #_ #EQ1 #EQ2 #EQ3 destruct #_ %2
     289  %{st2'} %{st3'} %{st4'} %{l1} %{(ret_act (None ?))} %{prf} %{t1} %{t2}
     290  %{prf'} /12 by conj/
     291]
     292qed.
     293                     

  • src/ERTL/ERTLToLTLProof.ma

    r3372 r3388  
    4242λlocalss,live_fun,color_fun,R,hw1,hw2,mem.
    4343hwreg_retrieve_sp hw1 = hwreg_retrieve_sp hw2 ∧
    44 ∀r : Register.live_fun (inr ?? r) → hwreg_retrieve hw1 r ≠ BVundef →
     44∀r : Register.r ≠ RegisterCarry → live_fun (inr ?? r) → hwreg_retrieve hw1 r ≠ BVundef →
    4545match color_fun (inr ?? r) with
    4646[ decision_colour r' ⇒ R (hwreg_retrieve hw1 r) (hwreg_retrieve hw2 r')
    … …  
    129129].
    130130
    131 xxxxxxxxxxxxx
    132 
     131(*
    133132let rec frames_relation_aux (prog : ertl_program) (stacksize : ident → option ℕ)
    134133(color_f : (Σb:block.block_region b=Code) →  option (list register → vertex → decision))
    … …  
    163162      (λd.acc (callee_saved_remap (pc_block (funct_pc hd)) init_regs color_f d))
    164163      init_regs
    165 ].
    166 
    167 (*
     164].*)
     165
    168166let rec frames_relation_aux (fix_comp : fixpoint_computer)
    169167(build : coloured_graph_computer) (prog : ertl_program) (R : beval → beval → Prop)
    … …  
    200198      (λd.acc (callee_saved_remap fix_comp build prog (pc_block (funct_pc hd)) init_regs d))
    201199      init_regs
    202 ].*)
     200].
    203201
    204202definition frames_relation :
     203(*
    205204∀prog : ertl_program.(ident → option ℕ) → (beval → beval → Prop) →
    206205((Σb:block.block_region b=Code) →  option(list register → vertex → decision)) →
    … …  
    209208λprog,stacksize,R,color_fun,live_fun,frames,regs,m,init_regs.
    210209frames_relation_aux prog stacksize color_fun live_fun R frames regs m (λx.x) init_regs.
    211 
    212 (*
     210*)
    213211fixpoint_computer → coloured_graph_computer → 
    214212ertl_program → (beval → beval → Prop) → list ERTL_frame →
    … …  
    217215 frames_relation_aux fix_comp build prog R frames regs m (λx.x) init_regs.
    218216
    219 
     217(*
    220218definition register_of_bitvector :  BitVector 6 → option Register≝
    221219λvect.
    … …  
    334332 
    335333definition gen_state_rel :
    336 ∀prog : ertl_program.(ident → option ℕ) → ? →
    337 ((Σb:block.block_region b=Code) → option (list register → vertex → decision)) →
    338 ((Σb:block.block_region b=Code)→ option (list register → live_type)) →
    339 ? → ? →
    340 (block → list register) →
    341 lbl_funct_type → regs_funct_type →
    342 joint_state_relation ERTL_semantics LTL_semantics ≝
    343 λprog,stacksizes,init,color_f,live_f,color_fun,live_fun,init_regs,f_lbls,f_regs,pc,st1,st2.
     334fixpoint_computer → coloured_graph_computer →
     335ertl_program →  (block → list register) → lbl_funct_type → regs_funct_type →
     336local_live_type →  (vertex → decision) →
     337joint_state_relation ERTL_semantics LTL_semantics ≝
     338λfix_comp,colour,prog,init_regs,f_lbls,f_regs,live_fun,color_fun,pc,st1,st2.
     339let m1 ≝ (\snd (\fst (ertl_to_ltl fix_comp colour prog))) in
     340let stacksizes ≝ lookup_stack_cost … m1 in
    344341let ge ≝ joint_globalenv ERTL_semantics prog stacksizes in
     342let init ≝ translate_data fix_comp colour in
    345343∃f,fn,ssize.
    346344fetch_internal_function … ge (pc_block pc) = return 〈f,fn〉 ∧
    … …  
    351349| Some frames ⇒
    352350   mem_relation prog stacksizes R f st1 (m … st1) (m … st2) ∧
    353    frames_relation prog stacksizes R color_f live_f frames (regs … st2) (m … st2) init_regs ∧
    354    hw_relation (joint_if_local_stacksize … fn) (live_fun fn (point_of_pc ERTL_semantics pc))
    355     (color_fun fn) R (\snd (regs … st1)) (regs … st2) (m … st2) ∧
     351   frames_relation fix_comp colour prog R frames (regs … st2) (m … st2) init_regs ∧
     352   hw_relation (joint_if_local_stacksize … fn) live_fun
     353    color_fun R (\snd (regs … st1)) (regs … st2) (m … st2) ∧
    356354   make_is_relation_from_beval R (istack … st1) (istack … st2) ∧
    357    (live_fun fn (point_of_pc ERTL_semantics pc)
    358     (inr ?? RegisterCarry) → carry … st1 = carry … st2) ∧
     355   ((live_fun (inr ?? RegisterCarry)) → carry … st1 ≠ BBundef → carry … st1 = carry … st2) ∧
    359356   stack_usage … st1 = stack_usage … st2 ∧
    360357   ∃ptr.sp … st2 = return ptr ∧
    361358    le ((nat_of_bitvector … (offv (poff … ptr))) + ssize) (2^16 -1) ∧
    362359    plus (nat_of_bitvector … (offv (poff … ptr))) (stack_usage … st2) = 2^16 ∧
    363     ps_relation (joint_if_local_stacksize … fn)
    364      (live_fun fn (point_of_pc ERTL_semantics pc))
    365      (color_fun fn)
    366      R ptr (\fst (regs … st1)) 〈regs … st2,m … st2〉
     360    ps_relation (joint_if_local_stacksize … fn) live_fun
     361     color_fun R ptr (\fst (regs … st1)) 〈regs … st2,m … st2〉
    367362].
    368363
    … …  
    374369ertl_program →  (block → list register) → lbl_funct_type → regs_funct_type →
    375370joint_state_relation ERTL_semantics LTL_semantics ≝
    376 λfix_comp,build,prog,init_regs,f_lbls,f_regs,pc.
    377 let after ≝ λfn,callee.analyse_liveness fix_comp (prog_names … prog) fn callee in
    378 let before ≝ λfn,callee.livebefore … fn callee (after fn callee) in
    379 let coloured_graph ≝ λfn,callee.build … fn (after fn callee) callee in
     371λfix_comp,build,prog,init_regs,f_lbls,f_regs,pc,st1,st2.
    380372let m1 ≝ (\snd (\fst (ertl_to_ltl fix_comp build prog))) in
    381373let stacksizes ≝ lookup_stack_cost … m1 in
    382 let init ≝ translate_data fix_comp build in
    383 gen_state_rel prog stacksizes init
    384  (λbl.
    385    match fetch_internal_function …
    386           (joint_globalenv ERTL_semantics prog stacksizes) bl with
    387    [ OK x ⇒ Some ? (λcallee.colouring … (coloured_graph (\snd x) callee))
    388    | Error e ⇒ None ?
    389    ])
    390  (λbl.
    391    match fetch_internal_function …
    392           (joint_globalenv ERTL_semantics prog stacksizes) bl with
    393    [ OK x ⇒ Some ? (λcallee,l,v.
    394                      in_lattice v ((before (\snd x) callee) l) ∧
    395                      match v with
    396                      [ inl r ⇒ true
    397                      | inr R ⇒ all … (λR'.¬ eq_Register R' R) RegisterAlwaysDead
    398                      ])
    399    | Error e ⇒ None ?
    400    ]) (λfn.colouring … (coloured_graph fn (init_regs (pc_block pc))))
    401    (λfn,l,v. in_lattice v (before fn (init_regs (pc_block pc)) l) ∧
    402              match v with
     374let ge ≝ joint_globalenv ERTL_semantics prog stacksizes in
     375∃f,fn.
     376fetch_internal_function … ge (pc_block pc) = return 〈f,fn〉 ∧
     377let after ≝ analyse_liveness fix_comp (prog_names … prog) fn (init_regs (pc_block pc)) in
     378let before ≝ livebefore … fn (init_regs (pc_block pc)) after in
     379let coloured_graph ≝ build … fn after (init_regs (pc_block pc)) in
     380gen_state_rel fix_comp build prog init_regs f_lbls f_regs
     381(λv.in_lattice v (before (point_of_pc ERTL_semantics pc)) ∧
     382       match v with
    403383             [ inl r ⇒ true
    404384             | inr R ⇒ all … (λR'.¬ eq_Register R' R) RegisterAlwaysDead
    405385             ])
    406     init_regs f_lbls f_regs pc.
     386(colouring … coloured_graph) pc st1 st2.
     387
    407388(*
    408389definition state_rel : fixpoint_computer → coloured_graph_computer →
    … …  
    526507
    527508lemma ps_reg_retrieve_hw_reg_retrieve_commute :
    528 ∀prog,stacksize,init,color_f,live_f,color_fun,live_fun.
     509∀fix_comp,colour,prog,color_fun,live_fun.
    529510∀init_regs : (block → list register).∀f_lbls,f_regs.∀f : ident.
    530511∀fn : joint_closed_internal_function ERTL (prog_names … prog).
    531512∀pc.
     513let m1 ≝ (\snd (\fst (ertl_to_ltl fix_comp colour prog))) in
     514let stacksize ≝ lookup_stack_cost … m1 in 
    532515fetch_internal_function … (joint_globalenv ERTL_semantics prog stacksize)
    533516 (pc_block pc) = return 〈f,fn〉→
     517 let init ≝ translate_data fix_comp colour in
    534518gen_preserving2 ?? gen_res_preserve ??????
    535      (gen_state_rel prog stacksize init color_f live_f color_fun live_fun init_regs f_lbls f_regs pc)
     519     (gen_state_rel fix_comp colour prog init_regs f_lbls f_regs live_fun color_fun pc)
    536520     (λr,d.
    537       bool_to_Prop
    538         (live_fun fn (point_of_pc ERTL_semantics pc)
    539           (inl ?? r)) ∧
    540       d =
    541       (color_fun fn (inl register Register r)))
     521      bool_to_Prop (live_fun (inl ?? r)) ∧
     522      d = (color_fun (inl register Register r)))
    542523     (λbv,bv'.bv = sigma_beval prog stacksize init init_regs f_lbls f_regs bv') …
    543524     (λst1.ps_reg_retrieve (regs … st1))
    544525     (λst,d.m_map Res ?? (\fst …)
    545526      (read_arg_decision (joint_if_local_stacksize ?? fn) st d)).
    546 #prog #stacksize #init #color_f #live_f #color_fun #live_fun #init_regs #f_lbls
     527#fix_comp #colour #prog #color_fun #live_fun #init_regs #f_lbls
    547528#f_regs #f #fn #pc #EQfn #st1 #st2 #r #d
    548529whd in match gen_state_rel; normalize nodelta * #f1 * #fn1 * #ssize
    … …  
    10631044qed.
    10641045
    1065 lemma vertex_retrieve_read_arg_decision_commute :
    1066 ∀prog,stacksize,init,color_f,live_f,color_fun,live_fun.
    1067 ∀init_regs : (block → list register).∀f_lbls,f_regs.∀f : ident.
    1068 ∀fn : joint_closed_internal_function ERTL (prog_names … prog).
    1069 ∀pc.
    1070 fetch_internal_function … (joint_globalenv ERTL_semantics prog stacksize)
    1071  (pc_block pc) = return 〈f,fn〉→
    1072 gen_preserving2 ?? gen_res_preserve ??????
    1073      (gen_state_rel prog stacksize init color_f live_f color_fun live_fun init_regs f_lbls f_regs pc)
    1074      (λv,d.
    1075       bool_to_Prop
    1076         (live_fun fn (point_of_pc ERTL_semantics pc) v) ∧
    1077       d =
    1078       (color_fun fn v))
    1079      (λx,y.\fst x = sigma_beval prog stacksize init init_regs f_lbls f_regs (\fst y) ∧
    1080             gen_state_rel prog stacksize init color_f live_f color_fun
    1081             live_fun init_regs f_lbls f_regs pc (\snd x) (\snd y)) …
    1082      (λst1,v.! bv ← ertl_vertex_retrieve (regs … st1) v;
    1083               return〈bv,st1〉)
    1084      (λst,d.(read_arg_decision (joint_if_local_stacksize ?? fn) st d)).
    1085 #prog #stacksize #init #color_f #live_f #color_fun #live_fun #init_regs #f_lbls #f_regs
    1086 #f #fn #pc #EQfn #st1 #st2 *
    1087 [ @ps_reg_retrieve_hw_reg_retrieve_commute assumption] #R #d * #f1 * #fn1 * #ssize
    1088 ** >EQfn whd in ⊢ (??%% → ?); #EQ1 destruct(EQ1) #_ cases(st_frms ??) [*] #frames
    1089 normalize nodelta ***** #_ #H1 #_ #_ #_ #_ * #live_R #EQ destruct(EQ) #bv #EQbv
    1090 lapply((proj2 ?? H1 …) R live_R ?)
    1091 [ % #ABS whd in match ertl_vertex_retrieve in EQbv; normalize nodelta in EQbv;
    1092   >ABS in EQbv; normalize nodelta whd in ⊢ (???% → ?); #EQ destruct(EQ) ]
    1093  cases(color_fun ??) normalize nodelta [#n1 | #R1 ] lapply(ertl_vertex_retrieve_ok_on_hw_regs … EQbv)
    1094  #EQ destruct(EQ)
    1095 [ inversion (hwreg_retrieve_sp ?) normalize nodelta [2: #e #_ *] #sp #EQsp
    1096   inversion(beloadv ??) normalize nodelta [ #_ *] #bv1 #EQbv1 #Hbv1 %{bv1}
    1097   % [2: assumption] whd in match m_map; whd in match read_arg_decision; normalize nodelta
    1098   @pair_elim #off_h #off_l #EQoff >m_return_bind >m_return_bind @('bind_inversion EQsp)
    1099   #ptr1 #EQptr1 @match_reg_elim
    1100    [2: #_ whd in ⊢ (??%% → ?); #EQ destruct] #prf whd in ⊢ (??%% → ?); #EQ destruct
    1101    cases(shift_pointer_commute
    1102          (bitvector_of_nat 16 (joint_if_local_stacksize … fn1 +n1)) (carry … st2) … 
    1103          〈hwreg_retrieve (regs LTL_semantics st2) RegisterSPL,
    1104           hwreg_retrieve (regs LTL_semantics st2) RegisterSPH〉 …)
    1105    [3: %
    1106    |5: >EQptr1 in ⊢ (??%?); >m_return_bind whd in match xpointer_of_pointer; normalize nodelta
    1107        @match_reg_elim [2: >prf in ⊢ (% → ?); #EQ destruct] #prf1 >m_return_bind %
    1108    |*:
    1109    ]
    1110    #x * >EQoff normalize nodelta #H @('bind_inversion H) -H #val1 #EQval1
    1111    #H @('bind_inversion H) -H #val2 #EQval2 #EQx #EQ destruct(EQ)
    1112    >EQval1 >m_return_bind >EQval2 >m_return_bind >EQx >m_return_bind >EQbv1 >m_return_bind %
    1113 | #EQ %{(hwreg_retrieve (regs … st2) R1)} %{(refl …)} assumption
    1114 ]
    1115 qed.
    1116 
    11171046lemma hwreg_retrieve_sp_insensitive_to_set_other : ∀b,rgs.
    11181047hwreg_retrieve_sp (hwreg_set_other b rgs) = hwreg_retrieve_sp rgs.
    … …  
    11291058qed.
    11301059
    1131 lemma shift_pointer_inj : ∀n,ptr.∀b1,b2 : BitVector n.
    1132 nat_of_bitvector … (offv (poff … ptr)) + nat_of_bitvector … b1 ≤ 2^16 - 1 →
    1133 nat_of_bitvector … (offv (poff … ptr)) + nat_of_bitvector … b2 ≤ 2^16 - 1 →
    1134 shift_pointer n ptr b1 = shift_pointer n ptr b2 →
    1135 b1 = b2.
     1060lemma vertex_retrieve_read_arg_decision_commute :
     1061∀fix_comp,colour,prog,color_fun,live_fun.
     1062∀init_regs : (block → list register).∀f_lbls,f_regs.∀f : ident.
     1063∀fn : joint_closed_internal_function ERTL (prog_names … prog).
     1064∀pc.
     1065let m1 ≝ (\snd (\fst (ertl_to_ltl fix_comp colour prog))) in
     1066let stacksize ≝ lookup_stack_cost … m1 in 
     1067fetch_internal_function … (joint_globalenv ERTL_semantics prog stacksize)
     1068 (pc_block pc) = return 〈f,fn〉→
     1069 let init ≝ translate_data fix_comp colour in
     1070(∀v.∀R. color_fun v = decision_colour R → R = RegisterDPL ∨ R = RegisterDPH → ¬ live_fun v) →
     1071bool_to_Prop (¬ live_fun (inr ?? RegisterDPL)) →
     1072bool_to_Prop (¬ live_fun (inr ?? RegisterDPH)) →
     1073gen_preserving2 ?? gen_res_preserve ??????
     1074     (gen_state_rel fix_comp colour prog init_regs f_lbls f_regs live_fun color_fun pc)
     1075     (λv,d.v ≠ (inr ?? RegisterCarry) ∧ bool_to_Prop(live_fun v) ∧ d = (color_fun v))
     1076     (λx,y.\fst x = sigma_beval prog stacksize init init_regs f_lbls f_regs (\fst y) ∧
     1077          gen_state_rel fix_comp colour prog init_regs f_lbls f_regs
     1078           (update_fun … eq_vertex live_fun (inr ?? RegisterCarry) false)
     1079           color_fun pc (\snd x) (\snd y)) …
     1080     (λst1,v.! bv ← ertl_vertex_retrieve (regs … st1) v;
     1081              return〈bv,st1〉)
     1082     (λst,d.(read_arg_decision (joint_if_local_stacksize ?? fn) st d)).
     1083#fix_comp #colour #prog #color_fun #live_fun #init_regs #f_lbls #f_regs
     1084#f #fn #pc #EQfn #Hvert #Hdpl #Hdph #st1 #st2 *
     1085[ #r #d #Rst1st2 ** #_ #live_r #colour_d * #bv #st #H @('bind_inversion H) -H
     1086  #bv1 whd in match ertl_vertex_retrieve; normalize nodelta #EQbv1
     1087  whd in ⊢ (??%% → ?); #EQ destruct(EQ)
     1088  cases (ps_reg_retrieve_hw_reg_retrieve_commute … EQfn … Rst1st2 … EQbv1)
     1089  [3: % assumption |2:] #fbv * whd in match m_map; normalize nodelta
     1090  #H @('bind_inversion H) -H * #fbv1 #st2' #EQfbv1 whd in ⊢ (??%% → ?);
     1091  #EQ destruct(EQ) #EQ destruct(EQ) %{〈fbv,st2'〉} %{EQfbv1} % [%]
     1092  whd in match read_arg_decision in EQfbv1; normalize nodelta in EQfbv1;
     1093  destruct cases (color_fun ?) in EQfbv1; [#n | #R] normalize nodelta
     1094  [2: whd in ⊢ (??%% → ?); #EQ destruct(EQ)
     1095  | @pair_elim #high #low #EQhl >m_return_bind >m_return_bind #H @('bind_inversion H) -H
     1096    #val1 #EQval1 #H @('bind_inversion H) -H #val2 #EQval2 #H @('bind_inversion H)
     1097    -H #ptr #EQptr #H @('bind_inversion H) -H #fbv1 #H lapply(opt_eq_from_res ???? H)
     1098    -H #EQfbv1 whd in ⊢ (??%% → ?); #EQ destruct(EQ) whd in match set_carry;
     1099    normalize nodelta
     1100  ]
     1101  cases Rst1st2 #f1 * #fn1 * #ssize ** >EQfn whd in ⊢ (??%% → ?);
     1102  #EQ destruct(EQ) #EQssize inversion(st_frms ??) [1,3: #_ *] #frames #EQframes
     1103  normalize nodelta ****** #Hmem #Hframes #Hhw #His #Hcarry #Hstack #Hpsregs
     1104  %{f1} %{fn1} %{ssize} % [1,3: % assumption] >EQframes normalize nodelta %
     1105  [2,4: cases Hpsregs -Hpsregs #ptr *** #EQptr #H1 #H2 #H3 %{ptr} %
     1106    [1,3: % [2,4: assumption] % [1,2,4: assumption]
     1107         change with (hwreg_retrieve_sp ?) in ⊢ (??%?);
     1108         >hwreg_retrieve_sp_insensitive_to_regstore
     1109         [ >hwreg_retrieve_sp_insensitive_to_regstore [ assumption]]
     1110         normalize % #EQ destruct
     1111    |*: #r1 #d1 * whd in match update_fun; normalize nodelta #r1_live #EQ destruct(EQ)
     1112        #bv1 #EQbv1 [ @(H3 … EQbv1) % //] cases(H3 … EQbv1) [3: % [ assumption | % ] |2:]
     1113        #bv1' inversion(color_fun ?) [ #n | #R ] #EQcol normalize nodelta *
     1114        [ #H lapply(opt_eq_from_res ???? H) -H #EQbv1'
     1115        | whd in ⊢ (??%% → ?); #EQ destruct(EQ)
     1116        ]
     1117        #EQ destruct(EQ) [ %{bv1'} % [ >EQbv1' % | %]]
     1118        %{(hwreg_retrieve (regs … st2) R)} % [2: %] >hwreg_retrieve_hwregstore_miss
     1119        [ >hwreg_retrieve_hwregstore_miss [%]] % #H lapply(Hvert … EQcol ?)
     1120        [1,3: [%2|%] assumption] >r1_live *
     1121    ]
     1122  |*: % [2,4: assumption] % [2,4: *] % [2,4: assumption] %
     1123      [2,4: [2: whd >hwreg_retrieve_sp_insensitive_to_regstore
     1124               [ >hwreg_retrieve_sp_insensitive_to_regstore ] ]
     1125            [2,3,4,5: normalize % #EQ destruct(EQ) |*: %{(proj1 ?? Hhw)} ]
     1126            #r1 * #r1_no_c whd in match update_fun; normalize nodelta
     1127            @eq_vertex_elim [1,3: #EQ destruct(EQ) @⊥ @r1_no_c % ] #_
     1128            normalize nodelta #r1_live #r1_no_undef [2: @(proj2 … Hhw) [%] assumption]
     1129            lapply(proj2 ?? Hhw … r1_live r1_no_undef) [% assumption]
     1130            inversion(color_fun ?) normalize nodelta [ #n #_ #H @H]
     1131            #R1 #HR1 #H >hwreg_retrieve_hwregstore_miss
     1132            [ >hwreg_retrieve_hwregstore_miss [ @H ] ] % #H1
     1133            lapply(Hvert … HR1 ?) [1,3: [%2|%] assumption] >r1_live *
     1134            #H1 #H2 assumption
     1135      |*: % [1,2,3: assumption ] cases daemon (*TODO in a separate lemma *)
     1136      ]
     1137  ]
     1138]
     1139#Reg #dec #Rst1st2 *** #Reg_nocarry #Reg_live #EQ destruct(EQ) * #bv #st1'
     1140#H @('bind_inversion H) -H #bv1 #EQbv1 whd in ⊢ (??%% → ?); #EQ destruct(EQ)
     1141cases Rst1st2 #f1 * #fn1 * #ssize ** >EQfn whd in ⊢ (??%% → ?); #EQ destruct(EQ)
     1142#EQsszie inversion(st_frms ??) [ #_ *] #frames #EQframes normalize nodelta ******
     1143#Hmem #Hframes #Hhw #His #Hcarry #Hstack #Hps cut(? : Prop)
     1144[3: #H_nocarry lapply(proj2 ?? Hhw … Reg_live H_nocarry)
     1145    [% #EQ destruct(EQ) @Reg_nocarry %] cases(color_fun ?) normalize nodelta
     1146    [ #n inversion(hwreg_retrieve_sp ?) normalize nodelta [2: #e #_ *]
     1147      #ptr #EQptr inversion(beloadv ??) [#_ *] #bv2 #EQbv2 normalize nodelta
     1148      #Hbv2 @('bind_inversion EQptr) #ptr1 #EQptr1 @match_reg_elim
     1149      [2: #_ whd in ⊢ (??%% → ?); #EQ destruct(EQ)] #prf whd in ⊢ (??%% → ?);
     1150      #EQ destruct(EQ)
     1151      cases(shift_pointer_commute (bitvector_of_nat 16 (joint_if_local_stacksize … fn1 +n))
     1152                (carry … st2) … 
     1153                〈hwreg_retrieve (regs LTL_semantics st2) RegisterSPL,
     1154                 hwreg_retrieve (regs LTL_semantics st2) RegisterSPH〉 …)
     1155     [5: >EQptr1 in ⊢ (??(????%?)?); >m_return_bind whd in match xpointer_of_pointer;
     1156         normalize nodelta @match_reg_elim [2: >prf in ⊢ (% → ?); #EQ destruct(EQ)]
     1157         #prf1 >m_return_bind %
     1158      |3: %
     1159      |*:
     1160      ]
     1161      @pair_elim #ptr_h #ptr_l #EQvsplit #ptr2 * #H @('bind_inversion H) -H #val1
     1162      #EQval1 #H @('bind_inversion H) -H #val2 #EQval2 #EQptr2 #EQ destruct(EQ)
     1163      %
     1164      [ % [ @bv2]
     1165      | %
     1166        [ whd in match read_arg_decision; normalize nodelta >EQvsplit in ⊢ (??%?);
     1167          normalize nodelta >m_return_bind >m_return_bind >EQval1 in ⊢ (??%?);
     1168          >m_return_bind >EQval2 in ⊢ (??%?); >m_return_bind >EQptr2 in ⊢ (??%?);
     1169          >m_return_bind >EQbv2 in ⊢ (??%?); %
     1170        | % [ <Hbv2 whd in match ertl_vertex_retrieve in EQbv1; normalize nodelta in EQbv1;
     1171              cases(hwreg_retrieve ??) in EQbv1; normalize nodelta
     1172              try (whd in ⊢ (??%% → ?); #EQ destruct(EQ) %)
     1173              try (#x1 whd in ⊢ (??%% → ?); #EQ destruct(EQ) %)
     1174              try (#x1 #x2 whd in ⊢ (??%% → ?); #EQ destruct(EQ) %)
     1175              #x1 #x2 #x3 whd in ⊢ (??%% → ?); #EQ destruct(EQ) % ]
     1176          %{f1} %{fn1} %{ssize} % [ %{EQfn} assumption ] >EQframes normalize nodelta
     1177          %
     1178          [2: cases Hps #ptr3 *** change with (hwreg_retrieve_sp ?) in ⊢ (??%? → ?);
     1179           >EQptr in ⊢ (% → ?); whd in ⊢ (??%% → ?); #EQ destruct(EQ) #H1 #H2 #H3
     1180           %{(«ptr1,prf»)} whd in match set_regs; normalize nodelta
     1181           %
     1182           [ %
     1183             [ % [2: assumption] change with (hwreg_retrieve_sp ?) in ⊢ (??%?);
     1184               >hwreg_retrieve_sp_insensitive_to_regstore
     1185               [ >hwreg_retrieve_sp_insensitive_to_regstore [ assumption] ]
     1186               % normalize #EQ destruct
     1187             | assumption
     1188             ]
     1189           ]
     1190           #r1 #d1 * whd in match update_fun; normalize nodelta #live_r1 #EQ destruct(EQ)
     1191           #bev #EQbev cases(H3 … (color_fun (inl ?? r1)) … EQbev) [2: %{live_r1} %]
     1192           #bev1 inversion(color_fun ?) normalize nodelta [#n #_ #H1 %{bev1} assumption]
     1193           #R1 #EQR1 * whd in ⊢ (??%% → ?); #EQ1 #EQ2 destruct %{(hwreg_retrieve (regs … st2) R1)}
     1194           % [2: %] >hwreg_retrieve_hwregstore_miss [ >hwreg_retrieve_hwregstore_miss [%]]
     1195           % #H lapply(Hvert … EQR1 ?) [1,3: [%2|%] assumption ] >live_r1 *
     1196          | % [2: assumption] % [2: *] % [2: assumption ] % cases daemon (*TODO*)
     1197          ]
     1198        ]
     1199      ]
     1200    | cases daemon (*TODO*)
     1201    ]
     1202|
     1203| whd in match ertl_vertex_retrieve in EQbv1; normalize nodelta in EQbv1;
     1204  cases(hwreg_retrieve ??) in EQbv1; normalize nodelta
     1205  [ whd in ⊢ (??%% → ?); #EQ destruct(EQ)
     1206  |*: try( #H1 #H2 #H3 #H4) try( #H1 #H2 #H3) try( #H1 #H2) try( #H1) % #EQ destruct
     1207  ]
     1208]
     1209qed.
     1210
     1211definition ertl_vertex_store : vertex → beval → state ERTL_state → state ERTL_state ≝
     1212λv,bv,st.match v with
     1213[ inl r ⇒ set_regs ERTL_state 〈reg_store r bv (\fst (regs … st)),\snd (regs … st)〉 st
     1214| inr r ⇒ set_regs ERTL_state 〈\fst (regs … st),hwreg_store r bv (\snd (regs … st))〉 st
     1215].
     1216
     1217lemma state_rel_insensitive_to_dead_write_decision :
     1218∀fix_comp,colour,prog,color_fun,live_fun.
     1219∀init_regs : (block → list register).∀f_lbls,f_regs.∀f : ident.
     1220∀fn : joint_closed_internal_function ERTL (prog_names … prog).
     1221∀pc.
     1222let m1 ≝ (\snd (\fst (ertl_to_ltl fix_comp colour prog))) in
     1223let stacksize ≝ lookup_stack_cost … m1 in 
     1224fetch_internal_function … (joint_globalenv ERTL_semantics prog stacksize)
     1225 (pc_block pc) = return 〈f,fn〉→
     1226∀r : Register.
     1227In … RegisterAlwaysDead r →
     1228∀bv.(∀v.color_fun v = (decision_colour r) → ¬ live_fun v) →
     1229gen_preserving ?? gen_res_preserve ????
     1230   (gen_state_rel fix_comp colour prog init_regs f_lbls f_regs live_fun color_fun pc)
     1231   (gen_state_rel fix_comp colour prog init_regs f_lbls f_regs live_fun color_fun pc)
     1232   (m_return …)
     1233   (λst.write_decision (joint_if_local_stacksize ?? fn) (decision_colour r) bv st).
     1234#fix_comp #colour #prog #color_fun #live_fun #init_regs #f_lbls #f_regs #f #fn #pc
     1235#EQfn #r #r_forb #bv #Hr #st1 #st2 #Rst1st2 #st1' whd in ⊢ (??%% → ?);
     1236#EQ destruct(EQ) %
     1237[2: % [ whd in match write_decision; normalize nodelta >m_return_bind %] |]
     1238cases Rst1st2 #f1 * #fn1 * #ssize ** >EQfn whd in ⊢ (??%% → ?); #EQ destruct(EQ)
     1239#EQssize inversion(st_frms ??); [ #_ * ] #frames #EQframes normalize nodelta
     1240****** #Hmem #Hframes #Hhw #His #Hcarry #Hstack * #sp *** #EQsp #H1 #H2 #Hps
     1241%{f1} %{fn1} %{ssize} % [ %{EQfn} assumption ] >EQframes normalize nodelta
     1242%
     1243[2: %{sp} %
     1244   [ % [2: assumption ] % [2: assumption ]
     1245     change with (hwreg_retrieve_sp ?) in ⊢ (??%?); whd in match set_regs;
     1246     normalize nodelta >hwreg_retrieve_sp_insensitive_to_regstore
     1247     [ assumption ] % #EQ destruct(EQ) cases r_forb
     1248     [1,3: normalize #EQ destruct(EQ) ] *
     1249     [1,3: normalize #EQ destruct(EQ) ] *
     1250     [1,3: normalize #EQ destruct(EQ) ] *
     1251     [1,3: normalize #EQ destruct(EQ) ] *
     1252     [1,3: normalize #EQ destruct(EQ) ] *
     1253   | whd #r1 #d1 * #live_r1 #EQ destruct(EQ) #bv1 #EQbv1
     1254     cases(Hps … (color_fun (inl ?? r1)) …  EQbv1) [2: % // ]
     1255     #bv2 inversion(color_fun ?) normalize nodelta
     1256     [#n #_ * #EQ1 #EQ2 destruct %{bv2} %{EQ1} % ]
     1257     #R #EQR * whd in ⊢ (??%% → ?); #EQ1 #EQ2 destruct
     1258     %{(hwreg_retrieve (regs … st2) R)} % [2: %]
     1259     whd in match set_regs; normalize nodelta
     1260     >hwreg_retrieve_hwregstore_miss [%] % #EQ destruct
     1261     lapply(Hr … EQR) >live_r1 *
     1262   ]
     1263]
     1264% [2: assumption] % [2: assumption ] % [2: assumption] cases daemon (*TODO*)
     1265qed.
     1266
     1267lemma beloadv_ok_bestorev_ok :
     1268∀m,ptr,bv,bv'.beloadv m ptr = return bv →
     1269∃m'.bestorev m ptr bv' = return m'.
    11361270cases daemon (*TODO*)
    11371271qed.
     1272
     1273include alias "arithmetics/nat.ma".
     1274
     1275lemma vertex_retrieve_write_decision_commute :
     1276∀fix_comp,colour,prog,color_fun,live_fun.
     1277∀init_regs : (block → list register).∀f_lbls,f_regs.∀f : ident.
     1278∀fn : joint_closed_internal_function ERTL (prog_names … prog).
     1279∀pc.
     1280let m1 ≝ (\snd (\fst (ertl_to_ltl fix_comp colour prog))) in
     1281let stacksize ≝ lookup_stack_cost … m1 in 
     1282fetch_internal_function … (joint_globalenv ERTL_semantics prog stacksize)
     1283 (pc_block pc) = return 〈f,fn〉→
     1284 let init ≝ translate_data fix_comp colour in
     1285(∀v.∀R. color_fun v = decision_colour R → R = RegisterDPL ∨ R = RegisterDPH → ¬ live_fun v) →
     1286bool_to_Prop (¬ live_fun (inr ?? RegisterDPL)) →
     1287bool_to_Prop (¬ live_fun (inr ?? RegisterDPH)) →
     1288(∀v.∀n : ℕ.color_fun v = decision_spill n → le n (joint_if_stacksize … fn)) →
     1289gen_preserving ?? gen_res_preserve ????
     1290     (λx,y.gen_state_rel fix_comp colour prog init_regs f_lbls f_regs live_fun
     1291             color_fun pc (\snd (\fst x)) (\snd (\fst y)) ∧
     1292           (\fst (\fst x)) = sigma_beval prog stacksize init init_regs f_lbls f_regs (\fst (\fst y)) ∧
     1293           (\snd x) ≠ (inr ?? RegisterCarry) ∧ bool_to_Prop(live_fun (\snd x)) ∧
     1294           (\snd y) = (color_fun (\snd x)) ∧
     1295           (∃bv'.ertl_vertex_retrieve (regs … (\snd (\fst x))) (\snd x) = return bv') ∧
     1296           (∀v'.v' ≠ (\snd x) → bool_to_Prop (live_fun v') → color_fun v' = (\snd y) → 
     1297                False))
     1298     (gen_state_rel fix_comp colour prog init_regs f_lbls f_regs
     1299         (update_fun … eq_vertex live_fun (inr ?? RegisterCarry) false)
     1300         color_fun pc) …
     1301     (λx.return ertl_vertex_store (\snd x) (\fst (\fst x)) (\snd (\fst x)))
     1302     (λx.write_decision (joint_if_local_stacksize ?? fn) (\snd x) (\fst (\fst x)) (\snd (\fst x))).
     1303#fix_comp #colour #prog #color_fun #live_fun #init_regs #f_lbls #f_regs #f #fn #pc
     1304#EQfn #Hdpl_dph #dpl_dead #dph_dead #Hspill ** #bv1 #st1 * #r ** #bv2 #st2 #d ******* #f1 * #fn1 * #sszie **
     1305>EQfn whd in ⊢ (??%% → ?); #EQ destruct(EQ) #EQsszie inversion(st_frms …) [1,3: #_ *]
     1306#frames #EQframes normalize nodelta ****** #Hmem #Hframes #Hhw #His #Hcarry #Hstack
     1307* #sp *** change with (hwreg_retrieve_sp ?) in ⊢ (??%? → ?); #EQsp #H1 #H2 #Hps #EQ destruct(EQ)
     1308[ #_ | * #r_nocarry ] #live_r #EQ destruct(EQ) * #bv' #EQbv' #Hinterf #st1' whd in ⊢ (??%% → ?);
     1309whd in match ertl_vertex_store; normalize nodelta #EQ destruct(EQ)
     1310[ cases(Hps … EQbv') [3: % [ assumption | %] |*:] #bv'' inversion(color_fun …)
     1311  [ #n | #R ] #EQcol normalize nodelta *
     1312  [ #H lapply(opt_eq_from_res ???? H) -H #EQbv''
     1313  | whd in ⊢ (??%% → ?); #EQ1
     1314  ]
     1315  #EQ2 destruct
     1316  [ @('bind_inversion EQsp) #ptr #EQptr @match_reg_elim #prf whd in ⊢ (??%% → ?); #EQ destruct
     1317    cases(shift_pointer_commute (bitvector_of_nat 16 (joint_if_local_stacksize … fn1 +n))
     1318                (carry … st2) … 
     1319                〈hwreg_retrieve (regs LTL_semantics st2) RegisterSPL,
     1320                 hwreg_retrieve (regs LTL_semantics st2) RegisterSPH〉 …)
     1321    [3: %
     1322    |5: >EQptr in ⊢ (??%?); >m_return_bind whd in match xpointer_of_pointer; normalize nodelta
     1323        @match_reg_elim [2: >prf in ⊢ (% → ?); #EQ destruct] #prf' >m_return_bind %
     1324    |*:
     1325    ]
     1326    #ptr1 @pair_elim #x1 #x2 #EQx1x2 * #H @('bind_inversion H) -H #x1' #EQx1'
     1327    #H @('bind_inversion H) -H #x2' #EQx2' #EQptr1 #EQ destruct(EQ)
     1328    cases(beloadv_ok_bestorev_ok … bv2 … EQbv'') #m' #EQm'
     1329    % [2: %
     1330          [ whd in match write_decision; normalize nodelta
     1331            >EQx1x2 in ⊢ (??%?); normalize nodelta >m_return_bind
     1332            >m_return_bind >EQx1' in ⊢ (??%?); >m_return_bind
     1333            >EQx2' in ⊢ (??%?); >m_return_bind >EQptr1 in ⊢ (??%?);
     1334            >m_return_bind >EQm' in ⊢ (??%?); >m_return_bind %
     1335          | whd %{f1} %{fn1} %{sszie} % [ % assumption ] >EQframes normalize nodelta
     1336            %
     1337            [2: %{(«ptr,prf»)} %
     1338                [ % [2: assumption] % [2: assumption]
     1339                change with (hwreg_retrieve_sp ?) in ⊢ (??%?); whd in match set_m;
     1340                whd in match set_regs; normalize nodelta
     1341                >hwreg_retrieve_sp_insensitive_to_regstore
     1342                [ >hwreg_retrieve_sp_insensitive_to_regstore [assumption]]
     1343                % normalize #EQ destruct ] #r1 #d1 * whd in match update_fun;
     1344                normalize nodelta #liv_r1 #EQ destruct(EQ) #val1
     1345                cut(eq_identifier … r r1 ∨ ¬ eq_identifier … r r1)
     1346                [ @eq_identifier_elim #_ // ] @eq_identifier_elim
     1347                [ #EQ destruct(EQ) #_ whd in match reg_retrieve; whd in match reg_store;
     1348                  normalize nodelta >lookup_add_hit whd in ⊢ (??%% → ?); #EQ destruct
     1349                  %{bv2} >EQcol normalize nodelta % [2: %] whd in match set_m; whd in match set_regs;
     1350                  normalize nodelta >beloadv_bestorev_hit [% | @EQm' |*:]
     1351                | #r_neq_r1 #_ whd in match reg_retrieve; whd in match reg_store;
     1352                  normalize nodelta >lookup_add_miss
     1353                  [2: % #EQ destruct cases r_neq_r1 #H @H %]
     1354                  change with (ps_reg_retrieve ??) in ⊢ (??%? → ?);
     1355                  #EQval1 cases(Hps … EQval1) [3: % [ assumption | %] |*:]
     1356                  #val2 inversion(color_fun ?) [ #n1 | #R1 ] #col_r1 normalize nodelta *
     1357                  [ #H lapply(opt_eq_from_res ???? H) -H #EQval2 | whd in ⊢ (??%% → ?); #EQ1 ]
     1358                  #EQ2 %{val2} destruct %
     1359                  [2,4: % |3: >hwreg_retrieve_hwregstore_miss [ >hwreg_retrieve_hwregstore_miss [%]]
     1360                  % #EQ destruct(EQ) lapply(Hdpl_dph … col_r1 ?) [1,3: [ %2 | %] %]
     1361                  >liv_r1 * ]
     1362                  whd in match set_m; whd in match set_regs; normalize nodelta
     1363                  cut(eqb … n n1 ∨ ¬ eqb … n n1) [ @eqb_elim #_ //]
     1364                  @eqb_elim
     1365                  [ #EQ destruct(EQ) #_ >(beloadv_bestorev_hit …  EQm')
     1366                    whd in ⊢ (??%%); @eq_f
     1367                    cases(Hinterf (inl ?? r1) ? liv_r1 ?)
     1368                    [ % #EQ destruct cases r_neq_r1 #H @H %
     1369                    | >EQcol >col_r1 %
     1370                    ]
     1371                  | * #n_no_n1 #_ >(beloadv_bestorev_miss … EQm')
     1372                    [ >EQval2 % ]
     1373                    % #ABS @n_no_n1
     1374                    @(injective_plus_r (joint_if_local_stacksize … fn1))
     1375                    @(eq_bitvector_of_nat_to_eq … (shift_pointer_injective … ABS))
     1376                    whd change with (plus 1 ?) in ⊢ (?%?);
     1377                    @monotonic_le_plus_r @(transitive_le … H1)
     1378                    [ cut (joint_if_local_stacksize … fn1 + n ≤ sszie)
     1379                      [ cases daemon (*TODO an invariant to be added*) ]
     1380                      | cut (joint_if_local_stacksize … fn1 + n1 ≤ sszie)
     1381                      [ cases daemon (*TODO an invariant to be added*) ]
     1382                    ]
     1383                    #H2 @(transitive_le … H2) @le_plus_n   
     1384                  ]
     1385                ]
     1386            | % [2: assumption ] % [2: *] % [2: assumption] %
     1387              [2: % [ >(proj1 … Hhw) >hwreg_retrieve_sp_insensitive_to_regstore
     1388                      [ >hwreg_retrieve_sp_insensitive_to_regstore [%]] normalize % #EQ destruct]
     1389                    #r1 * #r1_nocarry whd in match update_fun; normalize nodelta @eq_vertex_elim
     1390                    [ #EQ @⊥ destruct(EQ) @r1_nocarry %] #_ normalize nodelta
     1391                    #live_r1 #r1_noundef inversion(color_fun ?)
     1392                    [ #n1 | #r1'] #col_r1 normalize nodelta
     1393                    [ >hwreg_retrieve_sp_insensitive_to_regstore
     1394                      [ >hwreg_retrieve_sp_insensitive_to_regstore ]
     1395                      [2,3,4,5: normalize % #EQ destruct]
     1396                      >EQsp normalize nodelta whd in match set_m; normalize nodelta
     1397                      cases daemon (*TODO*)
     1398                    | >hwreg_retrieve_hwregstore_miss
     1399                      [ >hwreg_retrieve_hwregstore_miss ] [2,3: % #EQ destruct(EQ)
     1400                      lapply(Hdpl_dph … col_r1 ?) [1,3: [ %2 | % ] %] >live_r1 * ]
     1401                      lapply(proj2 … Hhw r1 … live_r1 r1_noundef) [% assumption]
     1402                      >col_r1 normalize nodelta #H @H
     1403                    ]
     1404              | cases daemon (*TODO*)
     1405              ]
     1406            ]
     1407       ]
     1408    |
     1409    ]
     1410  |  cases daemon (*TODO*)   
     1411  ]
     1412| cases daemon (*TODO*)
     1413]
     1414qed.
     1415
     1416xxxxxxx     
     1417                         @transitive_le\
     1418                       
     1419                       
     1420                         check plus lapply injective_S whd in match injective;
     1421                        normalize nodelta change with(plus ? 1 ≤ 2 ^16); check injective_plus_l
     1422                 
     1423               
     1424           
     1425 
     1426 
     1427
     1428   %
     1429  [2,4: %
     1430        [1,3: whd in match write_decision; normalize nodelta [2: %] @pair_elim
     1431              #h_l #h_h #EQh >m_return_bind >m_return_bind
     1432              @('bind_inversion EQsp) #ptr #EQptr @match_reg_elim #prf whd in ⊢ (??%% → ?);
     1433              #EQ destruct(EQ)
     1434              cases(shift_pointer_commute (bitvector_of_nat 16 (joint_if_local_stacksize … fn1 +n))
     1435                (carry … st2) … 
     1436                〈hwreg_retrieve (regs LTL_semantics st2) RegisterSPL,
     1437                 hwreg_retrieve (regs LTL_semantics st2) RegisterSPH〉 …)
     1438              [
     1439         
     1440 inversion(color_fun …) [1,3: #n |*: #R ] #EQcol %
     1441[2: %
     1442    [ whd in match write_decision; normalize nodelta
     1443
     1444
     1445[ cases(Hps … EQbv')
     1446
     1447
     1448
     1449#Rst1st2 ****
     1450#EQ destruct(EQ) [ #_ | * #r_nocarry] #live_r #EQ destruct(EQ) #Hinterf #st1'
     1451whd in ⊢ (??%% → ?); #EQ destruct(EQ) cases Rst1st2
     1452[ cases(Hps … r)
     1453
     1454
     1455
     1456
     1457
     1458
    11381459
    11391460(*
    … …  
    12061527cases daemon qed.  *)
    12071528
    1208 lemma move_preserve :
    1209 ∀fix_comp,colour,prog,init.
    1210 ∀color_f : ((Σb:block.block_region b=Code) → option (list register → vertex → decision)).
    1211 ∀live_f : ((Σb:block.block_region b=Code)→ option (list register → live_type)).
    1212 ∀color_fun : (joint_closed_internal_function ERTL (prog_names … prog) → vertex → decision).
    1213 ∀live_fun : (joint_closed_internal_function ERTL (prog_names … prog) → label → vertex → bool).
    1214 let p_out ≝ (\fst (\fst (ertl_to_ltl fix_comp colour prog))) in
    1215 let m1 ≝ (\snd (\fst (ertl_to_ltl fix_comp colour prog))) in
    1216 let stacksizes ≝ lookup_stack_cost … m1 in
    1217  ∀init_regs : block → list register.∀f_lbls,f_regs. ∀pc,carry_lives_after.
    1218  ∀src,dest : decision.
    1219  ∀f.∀fn : joint_closed_internal_function ? (prog_names … prog).
    1220  fetch_internal_function … (joint_globalenv ERTL_semantics prog stacksizes)
    1221  (pc_block pc) = return 〈f,fn〉 → 
    1222 ∀v1,v2. color_fun fn v1 = src →
    1223 color_fun fn v2 = dest →
    1224 v2 ≠ (inr ?? RegisterCarry) →
    1225 live_fun fn (point_of_pc ERTL_semantics pc) v1 →
    1226 invariant_for_move src →
    1227 (∀v. live_fun fn (point_of_pc ERTL_semantics pc) v →
    1228      color_fun fn v ≠ decision_colour RegisterDPL ∧
    1229      color_fun fn v ≠ decision_colour RegisterDPH ∧
    1230      color_fun fn v ≠ decision_colour RegisterST1) →
    1231 live_fun fn (point_of_pc ERTL_semantics pc)
    1232  (inr ?? RegisterCarry) = carry_lives_after →
    1233 gen_preserving ?? gen_res_preserve ????
    1234 (λst1,st2.
    1235  gen_state_rel prog stacksizes init color_f live_f color_fun live_fun init_regs
    1236   f_lbls f_regs pc st1 st2 ∧
    1237  ∃bv.ertl_vertex_retrieve (regs … st1) v1 = return bv ∧
    1238  (∀v.live_fun fn (point_of_pc ERTL_semantics pc) v → v ≠ v1 → v ≠ v2 →
    1239      color_fun fn v = dest →
    1240      ertl_vertex_retrieve (regs … st1) v = return bv) ∧
    1241  (∀ptr.
    1242   sp … st2 = return ptr → 
    1243   match dest with
    1244   [ decision_spill n ⇒ 
    1245         ∀bv.bestorev (m … st2)
    1246          (shift_pointer ? ptr (bitvector_of_nat 16 ((joint_if_local_stacksize … fn) + n)))
    1247          bv ≠ None ?
    1248  | _ ⇒ True
    1249  ]))
    1250 (gen_state_rel prog stacksizes init color_f live_f
    1251  (λfn.update_fun ?? eq_vertex (color_fun fn) v1 dest)
    1252  (λfn.update_fun ?? (eq_identifier …) (live_fun fn) (point_of_pc ERTL_semantics pc)
    1253    (update_fun ?? eq_vertex (live_fun fn (point_of_pc ERTL_semantics pc)) v2
    1254     (eq_decision src dest)))
    1255  init_regs f_lbls f_regs pc)
    1256 (m_return ??)
    1257 (repeat_eval_seq_no_pc LTL_semantics (mk_prog_params LTL_semantics p_out stacksizes) f
    1258    (move (prog_names … prog) (joint_if_local_stacksize … fn) carry_lives_after dest src)).
    1259 #fix_comp #colour #prog #init #color_f #live_f #color_fun #live_fun #init_regs #f_lbls
    1260 #f_regs #pc #carry_live #src #dst #f #fn #EQfn #v1 #v2 #EQsrc
    1261 #EQdst * #v2_noCarry #v1_live #Hsrc #dst_spec #EQcarry_live #st1 #st2 * #Rst1st2 * #bv ** #EQbv
    1262 #Hv1v2 #Hdst >move_spec [2: assumption]
    1263 cases(vertex_retrieve_read_arg_decision_commute … init … EQfn … Rst1st2 … EQbv)
    1264 [3: %{v1_live} % |2: ] #bv1 * whd in match m_map; normalize nodelta
    1265 #H @('bind_inversion H) -H * #bv2 #st2' #EQread_arg whd in ⊢ (??%% → ?); #EQ1 #EQ2
    1266 destruct(EQ1 EQ2) cases src in EQsrc Hsrc; normalize nodelta -src
    1267 [ #n1 | #R1 ] #EQcol_src * [2: #R1_noDPL #R1_noDPH ] cases dst in EQdst Hdst Hv1v2 dst_spec;
    1268 [1,3: #n2 |*: #R2 ] #EQcol_dst normalize nodelta [1,2: #Hn2 |*: #_] #Hv1v2 #dst_spec
    1269 >EQcol_src in EQread_arg; #EQread_arg >EQread_arg whd in EQread_arg : (??%%);
    1270 [2,4: lapply EQread_arg -EQread_arg @pair_elim #off_h_src #off_l_src #EQoff_src
    1271       >m_return_bind >m_return_bind #H @('bind_inversion H) -H #val1_src #EQval1_src
    1272       #H @('bind_inversion H) -H #val2_src #EQval2_src #H @('bind_inversion H) -H
    1273       #ptr_shift_src #EQptr_shift_src #H @('bind_inversion H) -H #bv_src #H
    1274       lapply(opt_eq_from_res ???? H) -H #EQbv_src whd in ⊢ (??%% → ?); #EQread_arg ]
    1275 destruct(EQread_arg) >m_return_bind #st1' whd in ⊢ (??%% → ?); #EQ destruct(EQ)
    1276 cases Rst1st2 #f1 * #fn1 * #ssize ** >EQfn whd in ⊢ (??%% → ?); #EQ1 destruct(EQ1)
    1277 #EQssize inversion(st_frms ??) normalize nodelta [1,3,5,7: #_ *] #frames #EQframes ******
    1278 #Hmem #Hframes #Hhw_reg #His #Hcarry #Hsu * #sp ***
    1279 change with (hwreg_retrieve_sp ?) in ⊢ (??%? → ?); #EQsp #Hssize #Hstack_usage #Hps_reg
    1280 [ @eqb_elim normalize nodelta [ #EQ destruct(EQ) %{st2} %{(refl …)} | * #src_dest_spec ]
    1281 | @eq_Register_elim normalize nodelta [ #EQ destruct(EQ) | * #R2_noA ]
    1282 | @eq_Register_elim normalize nodelta [ #EQ destruct(EQ) | * #R1_noA ]
    1283 | @eq_Register_elim normalize nodelta
    1284    [ #EQ destruct(EQ) %{st2'} %{(refl …)}
    1285    | * #src_dest_spec @eq_Register_elim normalize nodelta [#EQ destruct(EQ) | * #R2_noA >m_return_bind ]
    1286    ]
    1287 ]
    1288 [1,7: @(update_color_lemma … EQfn)
    1289   [1,3: @(update_live_fun_lemma … EQfn) [1,3: assumption] @eq_decision_elim
    1290     [2,4: * #H @⊥ @H %] #_ normalize nodelta inversion(live_fun ??)
    1291     [1,3: #_ @I] normalize nodelta >EQcol_dst normalize nodelta cases v2 in EQcol_dst; [1,3: #r |*: #R ] #EQcol_dst #v2_dead
    1292     normalize nodelta #bv1 whd in match ertl_vertex_retrieve; normalize nodelta #EQbv1
    1293     >EQcol_dst normalize nodelta
    1294     [1,3: %{sp} %{EQsp} cases v1 in EQcol_src v1_live EQbv; [1,3: #r1 |*: #R1] #EQcol_src
    1295           #v1_live whd in match ertl_vertex_retrieve; normalize nodelta
    1296           [1,2: #EQbv cases(Hps_reg r1 (decision_spill n2) … EQbv) [2,4: % assumption] #bv2
    1297           normalize nodelta
    1298    
    1299 
    1300  
    1301  
    1302  
    1303    @(update_color_lemma … EQfn)
    1304     cases daemon (*TODO: it follows by extensionality:
    1305                           maybe to be merged with other proof obbligations *)
    1306   ]
    1307   * #src_dest_spec
    1308  
    1309 
    1310 [2,4:
    1311 
    1312 
    1313 [1,3: whd in EQread_arg : (??%%); destruct(EQread_arg) @eq_Register_elim normalize nodelta
    1314  [ #EQ destruct(EQ) @('bind_inversion EQsp) #ptr #EQptr @match_reg_elim
    1315    [2: #_ whd in ⊢ (??%% → ?); #EQ destruct] #prf whd in ⊢ (??%% → ?);
    1316    #EQ destruct(EQ)
    1317    cases(shift_pointer_commute
    1318          (bitvector_of_nat 16 (joint_if_local_stacksize … fn1 +n2)) (carry … st2') … 
    1319          〈hwreg_retrieve (regs LTL_semantics st2') RegisterSPL,
    1320           hwreg_retrieve (regs LTL_semantics st2') RegisterSPH〉 …)
    1321    [3: %
    1322    |5: >EQptr in ⊢ (??%?); >m_return_bind whd in match xpointer_of_pointer; normalize nodelta
    1323        @match_reg_elim [2: >prf in ⊢ (% → ?); #EQ destruct] #prf1 >m_return_bind %
    1324    |*:
    1325    ]
    1326    #x * @pair_elim #offh #offl #EQoff #H @('bind_inversion H) -H #val1 #EQval1
    1327    #H @('bind_inversion H) -H #val2 #EQval2 #EQx #EQ destruct(EQ) %
    1328    [2: %
    1329        [ whd in match write_decision; whd in match set_regs; whd in match set_carry;
    1330          normalize nodelta > EQoff in ⊢ (??%?); normalize nodelta
    1331          >m_return_bind >m_return_bind >hwreg_retrieve_hwregstore_miss
    1332          [ >EQval1 in ⊢ (??%?); >m_return_bind >hwreg_retrieve_hwregstore_miss
    1333            [ >EQval2 in ⊢ (??%?); >m_return_bind >EQx in ⊢ (??%?); >m_return_bind
    1334              >(opt_to_opt_safe … (Hn2 … EQsp …)) >m_return_bind <commute_if
    1335              whd in match set_m; normalize nodelta %
    1336            ]
    1337          ]
    1338          normalize % #EQ destruct
    1339        | %{f1} %{fn1} %{ssize} % [ %{EQfn EQssize} ]
    1340          >EQframes normalize nodelta %
    1341          [ % [2: cases carry_live normalize nodelta assumption ]
    1342            % [2: whd in match update_fun; normalize nodelta @eq_identifier_elim
    1343                  [2: * #H @⊥ @H %] #_ normalize nodelta
    1344                  @eq_vertex_elim [ #EQ destruct @⊥ @v2_noCarry %] #_
    1345                  @eq_decision_elim [ #EQ destruct] #_ normalize nodelta
    1346                  destruct #H >H normalize nodelta @Hcarry assumption ]
    1347            % [2: @if_elim #_ assumption ] %
    1348            [2: whd in match update_fun; normalize nodelta @eq_identifier_elim
    1349                [2: * #H @⊥ @H %] #_ normalize nodelta %
    1350                [ cases carry_live normalize nodelta
    1351                  [ >hwreg_retrieve_sp_insensitive_to_set_other]
    1352                  >hwreg_retrieve_sp_insensitive_to_regstore
    1353                  [1,4: >hwreg_retrieve_sp_insensitive_to_regstore
    1354                    [1,4: >hwreg_retrieve_sp_insensitive_to_regstore
    1355                       [1,4:  @(proj1 … Hhw_reg) ] ] ]
    1356                  % normalize #EQ destruct
    1357                | #R' @eq_vertex_elim normalize nodelta [ #_ @eq_decision_elim [#EQ destruct] #_ *]
    1358                  #v2_noR' #live_R' @eq_vertex_elim
    1359                  [ #EQ destruct(EQ) normalize nodelta cases carry_live in EQcarry_live;
    1360                    #EQcarry_live normalize nodelta
    1361                    [ >hwreg_retrieve_sp_insensitive_to_set_other]
    1362                    >hwreg_retrieve_sp_insensitive_to_regstore
    1363                    [1,4: >hwreg_retrieve_sp_insensitive_to_regstore
    1364                      [1,4: >hwreg_retrieve_sp_insensitive_to_regstore ]]
    1365                    [1,4: |*: % normalize #EQ destruct]
    1366                    try >EQsp in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ?]); normalize nodelta
    1367                    @opt_safe_elim #m' #EQm' >(beloadv_bestorev_hit … EQm')
    1368                    normalize nodelta whd in EQbv : (??%%);
    1369                    cut(∀A,a1,a2. OK A a1 = OK A a2 → a1 = a2)
    1370                    [1,3: #H1 #H2 #H3 #H4 destruct %] #AUX
    1371                    @(AUX … EQbv)
    1372                  | #v1_noR' normalize nodelta
    1373                    cut(bool_to_Prop(eq_decision (decision_spill n2) (color_fun fn1 (inr ?? R'))) ∨
    1374                        bool_to_Prop(¬ eq_decision (decision_spill n2) (color_fun fn1 (inr ?? R'))))
    1375                    [ @eq_decision_elim #_ [%%|%2%]] *
    1376                    [ @eq_decision_elim [2: #_ *] #EQ lapply(sym_eq ??? EQ) -EQ #EQcolR'
    1377                      #_ >EQcolR' normalize nodelta cases carry_live
    1378                      [ >hwreg_retrieve_sp_insensitive_to_set_other]
    1379                      >hwreg_retrieve_sp_insensitive_to_regstore
    1380                      [1,4: >hwreg_retrieve_sp_insensitive_to_regstore
    1381                      [1,4: >hwreg_retrieve_sp_insensitive_to_regstore ]]
    1382                      [1,4: |*: % normalize #EQ destruct]
    1383                      try >EQsp in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ]); normalize nodelta
    1384                      @opt_safe_elim #m' #EQm' >(beloadv_bestorev_hit … EQm') normalize nodelta
    1385                      lapply(Hv1v2 (inr ?? R') live_R' v1_noR' v2_noR' EQcolR')
    1386                      whd in match ertl_vertex_retrieve;  normalize nodelta
    1387                      whd in ⊢ (??%% → ?); cut(∀A,a1,a2. OK A a1 = OK A a2 → a1 = a2)
    1388                      [1,3: #H1 #H2 #H3 #H4 destruct %] #AUX #EQ
    1389                      >(AUX ??? EQ) %
    1390                    | @eq_decision_elim [ #_ *] #Hnodet_R' #_ inversion(color_fun ??)
    1391                      [ #n3 #EQn3 normalize nodelta cases carry_live
    1392                        [ >hwreg_retrieve_sp_insensitive_to_set_other]
    1393                        >hwreg_retrieve_sp_insensitive_to_regstore
    1394                        [1,4: >hwreg_retrieve_sp_insensitive_to_regstore
    1395                        [1,4: >hwreg_retrieve_sp_insensitive_to_regstore ]]
    1396                        [1,4: |*: % normalize #EQ destruct]
    1397                        try >EQsp in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ]); normalize nodelta
    1398                        @opt_safe_elim #m' #EQm' >(beloadv_bestorev_miss … EQm')
    1399                        [1,3: lapply(proj2 ?? Hhw_reg R' live_R') >EQn3 normalize nodelta
    1400                              >EQsp normalize nodelta #H @H ]
    1401                        % #ABS >EQn3 in Hnodet_R'; * #H @H @eq_f -H
    1402                        @(injective_plus_r … (joint_if_local_stacksize … fn1))
    1403                        cut(? : Prop)
    1404                        [3,6: cut(? : Prop)
    1405                          [3,6: #H1 #H2 @(eq_bitvector_of_nat_to_eq 16)
    1406                                [1,4: @H1 |2,5: @H2 ]
    1407                                @(shift_pointer_inj … ABS) >nat_of_bitvector_bitvector_of_nat_inverse
    1408                                try assumption @(transitive_le … Hssize)
    1409                                @monotonic_le_plus_r cases daemon (*TODO*)
    1410                          |1,4:
    1411                          |*: cases daemon (*TODO*)
    1412                          ]
    1413                        |1,4:
    1414                        |*: cases daemon (*TODO*)
    1415                        ]     
    1416                      | #R'' #EQR'' normalize nodelta cases carry_live normalize nodelta
    1417                        [ >hwreg_retrieve_insensitive_to_set_other ]
    1418                        >hwreg_retrieve_hwregstore_miss
    1419                        [1,3: >hwreg_retrieve_hwregstore_miss 
    1420                              [1,3: >hwreg_retrieve_hwregstore_miss
    1421                                  [1,3: lapply(proj2 ?? Hhw_reg R' live_R') > EQR''
    1422                                        normalize nodelta #H @H ] ] ]
    1423                         cases(dst_spec … live_R') * >EQR'' * #H1 * #H2 * #H3 % #EQ destruct(EQ)
    1424                         try(@H1 %) try(@H2 %) try(@H3 %)
    1425                        
    1426                        
    1427                          [@H3 try @H1 try @H2 try assumption
    1428                        cases daemon (*hypothesis on colouring function to be added TODO *)
    1429                      ] 
    1430                        
    1431                                    
    1432                               lapply EQssize whd in ⊢ (??%% → ?);
    1433                              whd in match ertl_to_ltl; normalize nodelta whd in match (stack_cost ??);
    1434                              whd in ⊢ (??%% → ?);
    1435                  xxxxxxxx
    1436                    
    1437                    
    1438                     <EQbv destruct(EQbv)
    1439                    
    1440                    
    1441                     whd in match hwreg_retrieve_sp;
    1442                    normalize nodelta                                                                 
    1443           @eq_vertex_elim
    1444      
    1445        
    1446          
    1447                
    1448                 | normalize nodelta
    1449        
    1450        
    1451        
    1452        %{live_fun1} %{color_fun1} %
    1453          [%
    1454            [ %{EQfn}
    1455 
    1456 
    1457  
    1458 cases src in EQsrc Hsrc; -src normalize nodelta
    1459 [ #n1 | #R1 ] #EQcol_src * [2: #R1_noDPL #R1_noDPH] cases dst in EQdst Hdst;
    1460 [1,3: #n2 |*: #R2 ] #EQcol_dst normalize nodelta [1,2: #Hn2 |*: #_]
    1461 #st1' whd in ⊢ (??%% → ?); #EQ destruct(EQ)
    1462 cases daemon (*TODO*)
    1463 qed.
    1464 
    1465 
    1466 
    1467 
    1468 
    1469 
    1470 
    1471 
    1472 
     1529
     1530
     1531
     1532
     1533
     1534
     1535
     1536(*
    14731537lemma state_rel_insensitive_to_forbidden_Reg :
    14741538 ∀fix_comp,colour,prog,init_regs,f_lbls,f_regs,pc.
    … …  
    15611625]
    15621626qed.
    1563 
     1627*)
    15641628
    15651629
    … …  
    17071771whd in match acca_retrieve; normalize nodelta
    17081772change with (ps_reg_retrieve ??) in ⊢ (??%? → ?);
    1709 #EQbv #EQb whd in match state_pc_rel; normalize nodelta ** #Rst1st2 #_ #_
    1710 #t_fn #_ #z1 #z2 #z3 #z4 #z5 #z6 #z7 #z8 whd #EQinit_regs
     1773#EQbv #EQb whd in match state_pc_rel; normalize nodelta **
     1774whd in match state_rel; normalize nodelta * #f1 * #fn1 *
     1775>(proj1 … (fetch_statement_inv … EQfetch)) whd in ⊢ (???% → ?); #EQ destruct(EQ)
     1776#Rst1st2 #_ #_ #t_fn #_ #z1 #z2 #z3 #z4 #z5 #z6 #z7 #z8 whd #EQinit_regs
    17111777whd normalize nodelta %{(refl …)} #mid #_ <EQinit_regs
     1778>map_eval_add_dummy_variance_id >move_spec normalize nodelta
     1779[2: whd inversion(colouring …) normalize nodelta [#n #_ @I] #R
     1780    #EQR
     1781    cases(colouring_is_never_forbidden … (proj1 … (fetch_statement_inv … EQfetch)) … EQR)
     1782    #_ * #_ * #H1 * #H2 #_ %{H1 H2} ]
     1783cases(vertex_retrieve_read_arg_decision_commute … (proj1 … (fetch_statement_inv … EQfetch)) … (inl ?? r) … Rst1st2 …)
     1784[2: *
     1785   [ #r1 #R #EQR * #EQ destruct
     1786     cases(colouring_is_never_forbidden … (proj1 … (fetch_statement_inv … EQfetch)) … EQR)
     1787     #_ * #_ * * #H1 * * #H2 #_ @⊥ try( @H1 %) @H2 %
     1788   | #R1 #R2 >hdw_same_colouring #EQ destruct * #EQ destruct cases(in_lattice …) %
     1789   ]
     1790|3,4: cases(in_lattice …) %
     1791|6: % [2: %] % [ % #EQ destruct]
     1792    >(all_used_are_live_before fix_comp … (proj2 … (fetch_statement_inv … EQfetch)))
     1793    [% | % | @set_member_singl]
     1794|8: whd in match ertl_vertex_retrieve; normalize nodelta >EQbv in ⊢ (??%?); %
     1795|*:
     1796]
     1797* #bv' #st2' * #EQst2' * #EQ destruct(EQ) #Rst1st2' >EQst2' >m_return_bind >m_return_bind
     1798>m_return_bind >m_return_bind
     1799cases(state_rel_insensitive_to_dead_write_decision … (proj1 … (fetch_statement_inv … EQfetch)) … RegisterA … bv' … Rst1st2' … (refl …))
     1800[2: %%
     1801|3: * [#r #EQr cases(colouring_is_never_forbidden … (proj1 … (fetch_statement_inv … EQfetch)) … EQr) * #H @⊥ @H %
     1802      | #R >hdw_same_colouring #EQ destruct(EQ) whd in match update_fun; normalize nodelta
     1803        cases(in_lattice …) %
     1804      ]
     1805]
     1806#st2'' * #EQst2'' #Rst1st2'' >EQst2'' inversion(colouring …) normalize nodelta
     1807[ #n | #R] #EQcol <commute_if % [2,4: %{(refl …)} |*:] %
     1808[1,3: %{f1} %{fn1} % [1,3: @if_elim #_ @(proj1 ?? (fetch_statement_inv … EQfetch)) ]
     1809  cases Rst1st2'' #f2 * #fn2 * #ssize ** >(proj1 ?? (fetch_statement_inv … EQfetch))
     1810  whd in ⊢ (??%% → ?); #EQ destruct #EQssize inversion(st_frms …) [1,3: #_ *]
     1811  #frames #EQframes ****** #Hmem #Hframes #Hhw #His #_ #Hstack * #sp *** #EQsp
     1812  #H1 #H2 #Hps %{f2} %{fn2} %{ssize} %
     1813  [1,3: @if_elim #_ %{(proj1 … (fetch_statement_inv … EQfetch))} assumption]
     1814  >EQframes normalize nodelta %
     1815  [2,4: %{sp}
     1816      [| @eq_Register_elim
     1817         [ #EQ destruct(EQ)
     1818           cases(colouring_is_never_forbidden …
     1819                         (proj1 … (fetch_statement_inv … EQfetch)) … EQcol)
     1820           * #ABS #_ @⊥ @ABS % ]
     1821         #RnoA normalize nodelta ] %
     1822      [2,4: #r1 #d1 * @andb_elim @if_elim <commute_if in ⊢ (% → ?);
     1823            whd in match (pc_block ?); >point_of_pc_of_point #r1_live *
     1824            [ <commute_if in ⊢ (% → ?); ] whd in match (pc_block ?); #EQ
     1825            destruct(EQ) #v1 #EQv1 cases(Hps … EQv1)
     1826            [3,6: % [2,4: %] whd in match update_fun; normalize nodelta
     1827                  whd in match (livebefore ?????);
     1828                  change with (stmt_at ??? (point_of_pc ERTL_semantics ?)) in
     1829                           ⊢ (?(?(??match % with [_ ⇒ ? | _ ⇒ ? ])?));
     1830                  >(proj2 … (fetch_statement_inv … EQfetch)) normalize nodelta
     1831                  whd in match statement_semantics; normalize nodelta
     1832                  @andb_Prop [2,4: @I]
     1833                  @set_member_union1 @set_member_diff [2,4: @set_member_empty]
     1834                  @(set_member_subset_if … r1_live)
     1835                  lapply(included_livebefore_livebeafter_stmt_labels
     1836                                 fix_comp … (init_regs (pc_block (pc … st1))) …
     1837                                 (proj2 ?? (fetch_statement_inv … EQfetch))
     1838                                 (if b then ltrue else lfalse) ?)
     1839                   [1,3: cases b normalize nodelta
     1840                          whd in match stmt_labels; whd in match stmt_explicit_labels;
     1841                          whd in match step_labels; normalize nodelta
     1842                          [1,3: >memb_cons [1,3: @I |*: @memb_hd] |*: >memb_hd @I ] ]
     1843                   whd in match (l_included ???); cases(set_subset (identifier ?) ??)
     1844                   [1,3: #_ @I] @if_elim **
     1845            |*:
     1846            ]
     1847            #v1' inversion(colouring …) normalize nodelta
     1848            [1,3: #n #EQn * #H1 #EQ destruct(EQ) %{v1'} % [2,4: %]
     1849                  [ >(commute_if ????? (λx.m LTL_semantics x))
     1850                    whd in match (m ??); @if_elim #_ ]
     1851                  whd in match write_decision in EQst2''; normalize nodelta in EQst2'';
     1852                  >m_return_bind in EQst2''; whd in ⊢ (??%% → ?); #EQ destruct(EQ)
     1853                  assumption
     1854            |*: #R #EQR * whd in ⊢ (??%% → ?); #EQ1 #EQ2 destruct(EQ1 EQ2)   
     1855                %{(hwreg_retrieve (regs … st2'') R)} % [2,3,4: % ] 
     1856                @if_elim #_ whd in match set_regs; normalize nodelta
     1857                [ >hwreg_retrieve_insensitive_to_set_other ]
     1858                >hwreg_retrieve_hwregstore_miss
     1859                [1,3: whd in match write_decision in EQst2''; normalize nodelta in EQst2'';
     1860                      >m_return_bind in EQst2''; whd in ⊢ (??%% → ?); #EQ destruct(EQ)
     1861                      >hwreg_retrieve_hwregstore_miss [1,3: %] ]
     1862                % #EQ destruct(EQ)
     1863                cases(colouring_is_never_forbidden …
     1864                         (proj1 … (fetch_statement_inv … EQfetch)) … EQR)
     1865                * #ABS #_ @ABS %
     1866            ]
     1867      |*: % try % try assumption
     1868          [1,3: change with (hwreg_retrieve_sp ?) in ⊢ (??%?);
     1869                [ @if_elim #_ whd in match set_regs; normalize nodelta
     1870                  [ >hwreg_retrieve_sp_insensitive_to_set_other ]
     1871                  >hwreg_retrieve_sp_insensitive_to_regstore
     1872                  [1,4: whd in match write_decision in EQst2'';
     1873                        normalize nodelta in EQst2''; >m_return_bind in EQst2'';
     1874                        whd in ⊢ (??%% → ?); #EQ destruct(EQ)
     1875                        change with (hwreg_retrieve_sp ?) in EQsp : (??%?);
     1876                        >hwreg_retrieve_sp_insensitive_to_regstore in EQsp;
     1877                        [1,4: //]
     1878                  ]
     1879                  % normalize #EQ destruct
     1880               | @eq_Register_elim [2: #_ assumption ] #EQ destruct(EQ)
     1881                 cases(colouring_is_never_forbidden …
     1882                         (proj1 … (fetch_statement_inv … EQfetch)) … EQcol)
     1883                 * #ABS #_ @⊥ @ABS %
     1884               ]
     1885          |*:     
     1886         
     1887         
     1888         
     1889                         
    17121890cases(ps_reg_retrieve_hw_reg_retrieve_commute prog ???? init_regs f_lbls
    17131891f_regs f fn (pc … st1) ?????????)
Note: See TracChangeset for help on using the changeset viewer.