Changeset 1893


Ignore:
Timestamp:
Apr 20, 2012, 11:52:54 AM (7 years ago)
Author:
campbell
Message:

Show stronger result about labelling of expressions.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/labelSimulation.ma

    r1888 r1893  
    3838qed.
    3939
     40inductive trace_with_extra_labels : trace → trace → Prop ≝
     41| twel_0 : trace_with_extra_labels E0 E0
     42| twel_both : ∀h,t1,t2. trace_with_extra_labels t1 t2 → trace_with_extra_labels (h::t1) (h::t2)
     43| twel_new : ∀c,t1,t2. trace_with_extra_labels t1 t2 → trace_with_extra_labels t1 (EVcost c::t2).
     44
     45lemma twel_refl : ∀tr. trace_with_extra_labels tr tr.
     46#tr elim tr /2/
     47qed.
     48
     49lemma twel_app : ∀tr1,tr2,tr1',tr2'.
     50  trace_with_extra_labels tr1 tr1' →
     51  trace_with_extra_labels tr2 tr2' →
     52  trace_with_extra_labels (tr1⧺tr2) (tr1'⧺tr2').
     53#tr1 #tr2 #tr1' #tr2' #twel1 elim twel1 /3/
     54qed. 
     55
    4056lemma label_expr_ok : ∀ge,en,m,e,v,tr.
    4157  exec_expr ge en m e = OK … 〈v,tr〉 →
    42   ∀u. ∃tr'. exec_expr ge en m (\fst (label_expr e u)) = OK … 〈v,tr'〉.
     58  ∀u. ∃tr'. exec_expr ge en m (\fst (label_expr e u)) = OK … 〈v,tr'〉 ∧
     59            trace_with_extra_labels tr tr'.
    4360#ge #en #m #e
    4461@(expr_lvalue_ind ?
    4562  (λe,ty. ∀b,o,tr. exec_lvalue' ge en m e ty = OK … 〈〈b,o〉,tr〉 →
    46           ∀u. ∃tr'. exec_lvalue' ge en m (\fst (label_expr_descr e u ty)) ty = OK … 〈〈b,o〉,tr'〉) … e)
    47 [ 1,2: normalize /2/
     63          ∀u. ∃tr'. exec_lvalue' ge en m (\fst (label_expr_descr e u ty)) ty = OK … 〈〈b,o〉,tr'〉 ∧
     64                    trace_with_extra_labels tr tr') … e)
     65[ 1,2: normalize /3 by ex_intro, conj/
    4866| * //
    49  [ normalize /2 by ex_intro/
     67 [ normalize /3 by ex_intro, conj/
    5068 | #e1 #ty #IH #v #tr #EX #u
    5169   cases (bind_inversion ????? EX) * * #b #o #tr1 * #EX1 #EX1r
    5270   cases (bind_inversion ????? EX1r) #v * #EXl #EXrem
    5371   normalize in EXrem; destruct
    54    cases (IH … EX1 u) #tr1' #EX1'
    55    %{tr1'} >shift_fst in EX1'; >shift_fst >shift_fst #EX1' whd in ⊢ (??%?); >EX1'
    56    whd in ⊢ (??%?); >EXl @refl
     72   cases (IH … EX1 u) #tr1' * #EX1' #twel1
     73   %{tr1'} >shift_fst in EX1'; >shift_fst >shift_fst #EX1' whd in ⊢ (?(??%?)?); >EX1'
     74   whd in ⊢ (?(??%?)?); >EXl /2/
    5775 | #e1 #id #ty #IH #v #tr #EX #u
    5876   cases (bind_inversion ????? EX) * * #b #o #tr1 * #EX1 #EX1r
    5977   cases (bind_inversion ????? EX1r) #v * #EXl #EXrem
    6078   normalize in EXrem; destruct
    61    cases (IH … EX1 u) #tr1' #EX1'
    62    %{tr1'} >shift_fst in EX1'; >shift_fst >shift_fst #EX1' whd in ⊢ (??%?); >EX1'
     79   cases (IH … EX1 u) #tr1' * #EX1' #twel1
     80   %{tr1'} >shift_fst in EX1'; >shift_fst >shift_fst #EX1' % // whd in ⊢ (??%?); >EX1'
    6381   whd in ⊢ (??%?); >EXl @refl
    6482 ]
    65 | #v #ty #b #o #tr #EX #u %{tr} @EX
     83| #v #ty #b #o #tr #EX #u %{tr} % /2/
    6684| #e1 #ty #IH #b #o #tr #EX #u
    6785  cases (bind_inversion ????? EX) * #v1 #tr1 * #EX1 #EX1rem
    68   cases (IH … EX1 u) #tr1' #EX1'
    69   %{tr1'} >shift_fst whd in ⊢ (??%?); >EX1'
    70   whd in ⊢ (??%?);
    71   cases v1 in EX1rem ⊢ %; normalize #A try #B try #C destruct @refl
     86  cases (IH … EX1 u) #tr1' * #EX1' #twel1
     87  %{tr1'} >shift_fst whd in ⊢ (?(??%?)?); >EX1'
     88  whd in ⊢ (?(??%?)?);
     89  cases v1 in EX1rem ⊢ %; normalize #A try #B try #C destruct /2/
    7290| #ty' #e1 #ty #IH #v #tr #EX #u
    7391  cases (bind_inversion ????? EX) * * #b1 #o1 #tr1 * #EX1 #EX1rem
    74   cases (IH … EX1 u) #tr1' #EX1'
    75   %{tr1'} >shift_fst >shift_fst >shift_fst whd in ⊢ (??%?);
    76   whd in ⊢ (??(match % with [_⇒?|_⇒?])?); >EX1'
    77   whd in ⊢ (??%?);
     92  cases (IH … EX1 u) #tr1' * #EX1' #twel1
     93  %{tr1'} >shift_fst >shift_fst >shift_fst whd in ⊢ (?(??%?)?);
     94  whd in ⊢ (?(??(match % with [_⇒?|_⇒?])?)?); >EX1'
     95  whd in ⊢ (?(??%?)?);
    7896  cases ty' in EX1rem ⊢ %;
    79   [ 4: #r #ty' whd in ⊢ (??%? → ??%?); cases (pointer_compat_dec b1 r)
    80        #pc normalize #E destruct @refl
     97  [ 4: #r #ty' whd in ⊢ (??%? → ?(??%?)?); cases (pointer_compat_dec b1 r)
     98       #pc normalize #E destruct /2/
    8199  | *: normalize #A try #B try #C try #D destruct
    82100  ]
     
    85103  cases (bind_inversion ????? EX1rem) #v2 * #EX2 #EXrem
    86104  normalize in EXrem; destruct
    87   cases (IH … EX1 u) #tr1' #EX1'
    88   %{tr1'} >shift_fst
     105  cases (IH … EX1 u) #tr1' * #EX1' #twel1
     106  %{tr1'} % // >shift_fst
    89107  whd in ⊢ (??(????(?(???%)?))?);
    90108  @label_expr_elim #u2
     
    96114  cases (bind_inversion ????? EX2rem) #v' * #EXop #EXop'
    97115  #u
    98   cases (IH1 … EX1 u) #tr1' #EX1'
     116  cases (IH1 … EX1 u) #tr1' * #EX1' #twel1
    99117  >shift_fst
    100   whd in ⊢ (??(λ_.??(????(?(???%)?))?));
    101   @label_expr_elim #u2
    102   cases (IH2 … EX2 u2) #tr2' #EX2'
     118  whd in ⊢ (??(λ_.?(??(????(?(???%)?))?)?));
     119  @label_expr_elim #u2
     120  cases (IH2 … EX2 u2) #tr2' * #EX2' #twel2
    103121  @label_expr_elim #u3 %{(tr1'⧺tr2')}
    104   whd in ⊢ (??%?); >EX1'
    105   whd in ⊢ (??%?); >EX2'
    106   whd in ⊢ (??%?); >label_expr_type >label_expr_type >EXop
    107   normalize in EXop'; destruct @refl
     122  whd in ⊢ (?(??%?)?); >EX1'
     123  whd in ⊢ (?(??%?)?); >EX2'
     124  whd in ⊢ (?(??%?)?); >label_expr_type >label_expr_type >EXop
     125  normalize in EXop'; destruct % /2/
    108126| #ty #ty' #e1 #IH #v #tr #EX #u
    109127  cases (bind_inversion ????? EX) * #v1 #tr1 * #EX1 #EX1rem
    110128  cases (bind_inversion ????? EX1rem) #v2 * #EX2 #EX2rem
    111129  normalize in EX2rem; destruct
    112   cases (IH … EX1 u) #tr1' #EX1'
    113   %{tr1'} >shift_fst >shift_fst
     130  cases (IH … EX1 u) #tr1' * #EX1' #twel1
     131  %{tr1'} % // >shift_fst >shift_fst
    114132  whd in ⊢ (??%?); >EX1'
    115133  whd in ⊢ (??%?); >label_expr_type >EX2 @refl
     
    119137  cases (bind_inversion ????? EXguardrem) * #v2 #tr2 * #EX2 #EX2rem
    120138  normalize in EX2rem; destruct
    121   cases (IH1 … EX1 u) #tr1' #EX1'
    122   >shift_fst whd in ⊢ (??(λ_.??(????(?(???%)?))?));
     139  cases (IH1 … EX1 u) #tr1' * #EX1' #twel1
     140  >shift_fst whd in ⊢ (??(λ_.?(??(????(?(???%)?))?)?));
    123141  @label_expr_elim #u2
    124142  @label_expr_elim #u3
     
    126144  @label_expr_elim #u5
    127145  @add_cost_expr_elim #u6 #l6
    128   [ cases (IH2 … EX2 u2) | cases (IH3 … EX2 u4) ] #trx' #EXx'
     146  [ cases (IH2 … EX2 u2) | cases (IH3 … EX2 u4) ] #trx' * #EXx' #twelx
    129147  [ %{(tr1'⧺trx'⧺(Echarge l4))} | %{(tr1'⧺trx'⧺(Echarge l6))} ]
    130   whd in ⊢ (??%?); >EX1'
    131   whd in ⊢ (??%?); >label_expr_type >EXguard
    132   whd in ⊢ (??%?); whd in ⊢ (??(match % with [_⇒?|_⇒?])?); >EXx'
    133   normalize @refl
     148  whd in ⊢ (?(??%?)?); >EX1'
     149  whd in ⊢ (?(??%?)?); >label_expr_type >EXguard
     150  whd in ⊢ (?(??%?)?); whd in ⊢ (?(??(match % with [_⇒?|_⇒?])?)?); >EXx'
     151  normalize % // @twel_app // <(E0_right tr2) @twel_app /2/
    134152| #ty #e1 #e2 #IH1 #IH2 #v #tr #EX #u
    135153  cases (bind_inversion ????? EX) * #v1 #tr1 * #EX1 #EX1rem
    136154  cases (bind_inversion ????? EX1rem) * * #EXguard #EXguardrem
    137   >shift_fst whd in ⊢ (??(λ_.??(????(?(???%)?))?));
     155  >shift_fst whd in ⊢ (??(λ_.?(??(????(?(???%)?))?)?));
    138156  @label_expr_elim #u2
    139157  @label_expr_elim #u3
     
    142160  [ cases (bind_inversion ????? EXguardrem) * #v2 #tr2 * #EX2 #EX2rem
    143161    cases (bind_inversion ????? EX2rem) * * #EX3 #EX3rem
    144     cases (IH1 … EX1 u) #tr1' #EX1'
    145     cases (IH2 … EX2 u2) #tr2' #EX2'
     162    -EX1rem -EXguardrem -EX2rem
     163    cases (IH1 … EX1 u) #tr1' * #EX1' #twel1
     164    cases (IH2 … EX2 u2) #tr2' * #EX2' #twel2
    146165    %{(tr1'⧺(tr2'⧺E0)⧺Echarge l4)}
    147     whd in ⊢ (??%?); >EX1'
    148     whd in ⊢ (??%?); >label_expr_type >EX2' >EXguard
    149     whd in ⊢ (??%?); whd in ⊢ (??(match % with [_⇒?|_⇒?])?);
    150     whd in ⊢ (??(match (match % with [_⇒?|_⇒?]) with [_⇒?|_⇒?])?); >EX2'
    151     whd in ⊢ (??(match (match % with [_⇒?|_⇒?]) with [_⇒?|_⇒?])?); >label_expr_type >EX3
    152     normalize in EX3rem ⊢ %; destruct @refl
    153   | cases (IH1 … EX1 u) #tr1' #EX1'
     166    whd in ⊢ (?(??%?)?); >EX1'
     167    whd in ⊢ (?(??%?)?); >label_expr_type >EX2' >EXguard
     168    whd in ⊢ (?(??%?)?); whd in ⊢ (?(??(match % with [_⇒?|_⇒?])?)?);
     169    whd in ⊢ (?(??(match (match % with [_⇒?|_⇒?]) with [_⇒?|_⇒?])?)?); >EX2'
     170    whd in ⊢ (?(??(match (match % with [_⇒?|_⇒?]) with [_⇒?|_⇒?])?)?); >label_expr_type >EX3
     171    normalize in EX3rem ⊢ %; destruct % [ 1,3: @refl | *: @twel_app // <(E0_right tr2) @twel_app /2/ ]
     172  | cases (IH1 … EX1 u) #tr1' * #EX1' #twel1
    154173    %{(tr1'⧺E0⧺Echarge l5)}
    155     whd in ⊢ (??%?); >EX1'
    156     whd in ⊢ (??%?); >label_expr_type >EXguard
    157     normalize in EXguardrem; destruct @refl
     174    whd in ⊢ (?(??%?)?); >EX1'
     175    whd in ⊢ (?(??%?)?); >label_expr_type >EXguard
     176    normalize in EXguardrem; destruct % // <(E0_right tr) @twel_app /2/
    158177  ]
    159178| #ty #e1 #e2 #IH1 #IH2 #v #tr #EX #u
    160179  cases (bind_inversion ????? EX) * #v1 #tr1 * #EX1 #EX1rem
    161180  cases (bind_inversion ????? EX1rem) * * #EXguard #EXguardrem
    162   >shift_fst whd in ⊢ (??(λ_.??(????(?(???%)?))?));
     181  >shift_fst whd in ⊢ (??(λ_.?(??(????(?(???%)?))?)?));
    163182  @label_expr_elim #u2
    164183  @add_cost_expr_elim #u4 #l4
    165184  @label_expr_elim #u3
    166185  @add_cost_expr_elim #u5 #l5
    167   [ cases (IH1 … EX1 u) #tr1' #EX1'
     186  [ cases (IH1 … EX1 u) #tr1' * #EX1' #twel1
    168187    %{(tr1'⧺Echarge l4)}
    169     whd in ⊢ (??%?); >EX1'
    170     whd in ⊢ (??%?); >label_expr_type >EXguard
    171     normalize in EXguardrem ⊢ %; destruct @refl
     188    whd in ⊢ (?(??%?)?); >EX1'
     189    whd in ⊢ (?(??%?)?); >label_expr_type >EXguard
     190    normalize in EXguardrem ⊢ %; destruct % // <(E0_right tr) /3/
    172191  | cases (bind_inversion ????? EXguardrem) * #v2 #tr2 * #EX2 #EX2rem
    173192    cases (bind_inversion ????? EX2rem) * * #EX3 #EX3rem
    174     cases (IH1 … EX1 u) #tr1' #EX1'
    175     cases (IH2 … EX2 u4) #tr2' #EX2'
     193    cases (IH1 … EX1 u) #tr1' * #EX1' #twel1
     194    cases (IH2 … EX2 u4) #tr2' * #EX2' #twel2
    176195    %{(tr1'⧺(tr2'⧺E0)⧺Echarge l5)}
    177     whd in ⊢ (??%?); >EX1'
    178     whd in ⊢ (??%?); >label_expr_type >EX2' >EXguard
    179     whd in ⊢ (??%?); whd in ⊢ (??(match % with [_⇒?|_⇒?])?);
    180     whd in ⊢ (??(match (match % with [_⇒?|_⇒?]) with [_⇒?|_⇒?])?); >EX2'
    181     whd in ⊢ (??(match (match % with [_⇒?|_⇒?]) with [_⇒?|_⇒?])?); >label_expr_type >EX3
    182     normalize in EX3rem ⊢ %; destruct @refl
    183   ]
    184 | #ty #ty' #v #tr normalize /2/
     196    whd in ⊢ (?(??%?)?); >EX1'
     197    whd in ⊢ (?(??%?)?); >label_expr_type >EX2' >EXguard
     198    whd in ⊢ (?(??%?)?); whd in ⊢ (?(??(match % with [_⇒?|_⇒?])?)?);
     199    whd in ⊢ (?(??(match (match % with [_⇒?|_⇒?]) with [_⇒?|_⇒?])?)?); >EX2'
     200    whd in ⊢ (?(??(match (match % with [_⇒?|_⇒?]) with [_⇒?|_⇒?])?)?); >label_expr_type >EX3
     201    normalize in EX3rem ⊢ %; destruct % // @twel_app // <(E0_right tr2) @twel_app /2/
     202  ]
     203| #ty #ty' #v #tr normalize /3/
    185204| #ty #e1 #ty' #id #IH #b #o #tr #EX #u cases ty' in IH EX ⊢ %;
    186205  [ 7: #id #fl #IH #EX
     
    188207    cases (bind_inversion ????? EX1rem) #n * #EXoff #EXoffrem
    189208    whd in EXoffrem:(???%); destruct >shift_fst >shift_fst
    190     cases (IH … EX1 u) #tr1' #EX1'
    191     %{tr1'}
     209    cases (IH … EX1 u) #tr1' * #EX1' #twel1
     210    %{tr1'} % //
    192211    whd in ⊢ (??%?); whd in ⊢ (??(match % with [_⇒?|_⇒?])?); >EX1'
    193212    whd in ⊢ (??%?); >EXoff whd in ⊢ (??%?); @refl
     
    195214    cases (bind_inversion ????? EX) * * #b1 #o1 #tr1 * #EX1 #EX1rem
    196215    whd in EX1rem:(???%); destruct >shift_fst >shift_fst
    197     cases (IH … EX1 u) #tr1' #EX1'
    198     %{tr1'}
     216    cases (IH … EX1 u) #tr1' * #EX1' #twel1
     217    %{tr1'} % //
    199218    whd in ⊢ (??%?); whd in ⊢ (??(match % with [_⇒?|_⇒?])?); >EX1'
    200219    whd in ⊢ (??%?); @refl
     
    204223  cases (bind_inversion ????? EX) * #v1 #tr1 * #EX1 #EX1rem
    205224  whd in EX1rem:(???%); destruct
    206   cases (IH … EX1 u) #tr1' #EX1' %{(tr1'@Echarge l)}
    207   >shift_fst >shift_fst whd in ⊢ (??%?); >EX1'
    208   whd in ⊢ (??%?); @refl
     225  cases (IH … EX1 u) #tr1' * #EX1' #twel1 %{(tr1'@Echarge l)}
     226  >shift_fst >shift_fst whd in ⊢ (?(??%?)?); >EX1'
     227  whd in ⊢ (?(??%?)?); /3/
    209228| #e1 #ty #NLV #b #o #tr #EX @⊥
    210229  cases e1 in NLV EX; normalize //
    211230  #A #B #C try #D try #F destruct
    212231] qed.
     232
     233(* Plan:
     234     - extend labelling functions to continuations and hence states
     235       NO - this doesn't work because we don't know *which* cost labels to add
     236       realistically we'll have to define erasure functions
     237     - build a simulation relation linking states to their labelled counterparts
     238     - write a predicate stating that two traces are the same except for some
     239       extra costs
     240     - show some labelling relationship for global environments
     241     - prove that
     242         exec_step ge s1 = = Value … 〈tr,s2〉 →
     243         cost_related s1 s1' →
     244         ∃tr'. equal_up_to_costs tr tr' ∧
     245               plus ge' s1' tr' s2' ∧
     246               cost_related s2 s2'
     247       using some relationship between ge and ge'.
     248
     249WAIT - do I really want functions to erase the labels?  Or a predicate?
     250
     251let rec erase_label_expr (e:expr) : expr ≝
     252match e with
     253[ Expr ed ty ⇒ Expr (erase_label_expr_descr ed) ty
     254]
     255and erase_label_expr_descr (e:expr_descr) : expr_descr ≝
     256match e with
     257[ Ederef e' ⇒ Ederef (erase_label_expr_descr e')
     258| Eaddrof e' ⇒ Eaddrof (erase_label_expr_descr e')
     259| Eunop op e'
     260*)
Note: See TracChangeset for help on using the changeset viewer.