Changeset 3081


Ignore:
Timestamp:
Apr 3, 2013, 5:54:34 PM (4 years ago)
Author:
campbell
Message:

Tidy up recent work a little.

Location:
src
Files:
7 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/SimplifyCastsMeasurable.ma

    r3063 r3081  
    22include "common/FEMeasurable.ma".
    33include "Clight/Clight_classified_system.ma".
    4 
    5 (* TODO: move *)
    6 lemma step_not_final : ∀ge,s,tr,s'.
    7   exec_step ge s = Value … 〈tr,s'〉 →
    8   is_final s = None ?.
    9 #ge * //
    10 #r #tr #s' #ST whd in ST:(??%?); destruct
    11 qed.
    124
    135lemma state_cast_labelled : ∀s,s'.
     
    3527  ]
    3628] qed.
     29
     30(* Put cast simplification simulation into form that FEMeasurable needs.
     31   Note that sim_call_label is just sticking together two normal steps - we
     32   never add extra steps here, so we don't need to worry about moving cost
     33   labels to the start of the function. *)
    3734
    3835definition simplify_measurable_sim : meas_sim ≝
     
    8683  cases (cast_correction … RG … S1 ST)
    8784  #s2' * #ST' #S2 %{1} whd
    88   whd in match (is_final … s1'); >(step_not_final … ST')
     85  whd in match (is_final … s1'); >(cl_step_not_final … ST')
    8986  whd whd in match (step … Clight_pcs ge' s1'); >ST'
    9087  whd % [ % | assumption ]
     
    9390  cases (cast_correction … RG … S1 ST)
    9491  #s2' * #ST' #S2 %{0} whd
    95   whd in match (is_final … s1'); >(step_not_final … ST')
     92  whd in match (is_final … s1'); >(cl_step_not_final … ST')
    9693  whd whd in match (step … Clight_pcs ge' s1'); >ST'
    9794  whd % [ % | assumption ]
     
    103100  #s3' * #ST2' #S3
    104101  %{1} whd
    105   whd in match (is_final … s1'); >(step_not_final … ST1')
     102  whd in match (is_final … s1'); >(cl_step_not_final … ST1')
    106103  whd whd in match (step … Clight_pcs ge' s1'); >ST1'
    107104  whd % [ % [ % | change with (Clight_labelled s2') in ⊢ (?%); <(state_cast_labelled … S2) assumption ] ]
    108   whd whd in match (is_final … s2'); >(step_not_final … ST2')
     105  whd whd in match (is_final … s2'); >(cl_step_not_final … ST2')
    109106  whd whd in match (step … Clight_pcs ge' s2'); >ST2'
    110107  whd % [ % | assumption ]
     
    114111  #s2' * #ST' #S2 %{0} % [ @(return_E0 … ST) assumption ]
    115112  whd
    116   whd in match (is_final … s1'); >(step_not_final … ST')
     113  whd in match (is_final … s1'); >(cl_step_not_final … ST')
    117114  whd whd in match (step … Clight_pcs ge' s1'); >ST'
    118115  whd % [ >(return_E0 … ST) // assumption | assumption ]
     
    121118  cases (cast_correction … RG … S1 ST)
    122119  #s2' * #ST' #S2 whd
    123   whd in match (is_final … s1'); >(step_not_final … ST')
     120  whd in match (is_final … s1'); >(cl_step_not_final … ST')
    124121  whd whd in match (step … Clight_pcs ge' s1'); >ST'
    125122  whd % [ % | assumption ]
  • src/Clight/SwitchAndLabel.ma

    r3047 r3081  
    22include "Clight/labelSimulation.ma".
    33
    4 
    5 lemma after_aux_result : ∀avs,n,s,tr,P.
    6   after_aux avs n s tr P →
    7   ∃tr',s'. P tr' s' ∧ after_aux avs n s tr (λtr'',s''. 〈tr'',s''〉 = 〈tr',s'〉).
    8 #avs #n elim n
    9 [ #s #tr #P #A whd in A; %{tr} %{s} % [ @A | % ]
    10 | #n' #IH #s #tr #P
    11   whd in ⊢ (% → ?);
    12   lapply (refl ? (is_final … s))
    13   cases (is_final … s) in ⊢ (???% → %);
    14   [ #F whd in ⊢ (% → ?);
    15     lapply (refl ? (step … s))
    16     cases (step … s) in ⊢ (???% → %);
    17     [ #o #k #_ *
    18     | * #tr1 #s1 #ST whd in ⊢ (% → ?);
    19       cases n' in IH ⊢ %;
    20       [ #_ whd in ⊢ (% → ?); #p % [2: % [2: %{p} whd >F whd >ST whd % | skip ] | skip ]
    21       | #n'' #IH lapply (refl ? (avs_inv avs s1)) cases (avs_inv avs s1) in ⊢ (???% → %);
    22         [ #INV #AF
    23           cases (IH … AF) #tr' * #s' * #p #AF'
    24          % [2: % [2: %{p} whd >F whd >ST whd >INV @AF' | skip ] | skip ]
    25         | #_ *
    26         ]
    27       ]
    28     | #m #_ *
    29     ]
    30   | #r #F *
    31   ]
    32 ] qed.
    33 
    34 lemma after_n_result : ∀n,O,I,exec,g,s,P,inv.
    35   after_n_steps n O I exec g s inv P →
    36   ∃tr',s'.
    37     P tr' s' ∧
    38     after_n_steps n O I exec g s inv (λtr'',s''. 〈tr'',s''〉 = 〈tr',s'〉).
    39 #n #O #I #exec #g #s #P #inv #A
    40 cases (after_aux_result … A) #tr * #s' * #p #A'
    41 %{tr} %{s'} %{p} @A'
    42 qed.
    43 
    44 
    45 lemma after_1_of_n_steps' : ∀n,O,I,exec,g,tr,s',s.
    46   after_n_steps (S n) O I exec g s (λ_.true) (λtrx,sx. 〈trx,sx〉 = 〈tr,s'〉) →
    47   ∃tr1,tr2,s1.
    48   is_final … exec g s = None ? ∧
    49   step … exec g s = Value … 〈tr1,s1〉 ∧
    50   tr = tr1⧺tr2 ∧
    51   after_n_steps n O I exec g s1 (λ_.true) (λtrx,sx. 〈trx,sx〉 = 〈tr2,s'〉).
    52 #n #O #I #exec #g #tr #s' #s #A
    53 cases (after_1_of_n_steps … A)
    54 #tr1 * #s1 * * * #F #ST #_ #A'
    55 cases (after_n_result … A')
    56 #tr'' * #s'' * #E #A'' destruct
    57 % [2: % [2: % [2: % [ % [% [ @F | @ST ] | % ] | @A'' ] | skip ] | skip ] | skip ]
    58 qed.
    59 
    60 theorem steps_with_labels : ∀ge,ge'.
     4(* Combine the results about switch removal and labelling to provide a single
     5   result linking the input Clight program with the cost labelled Clight
     6   program. *)
     7
     8(* First lift the step result for labelling to a finite run of steps. *)
     9
     10lemma steps_with_labels : ∀ge,ge'.
    6111  related_globals_gen … label_fundef ge ge' →
    6212  ∀n,s1,s1',tr,s2.
     
    13888#tr #s #tr' #s' #E destruct %
    13989qed.
     90
     91(* Now build the coinduction simulation, taking one step to many after switch
     92   removal, then use steps_with_labels to take those to the cost labelled
     93   version. *)
    14094
    14195let corec build_exec
     
    210164] qed.
    211165
     166(* And deal with the start of the program to tie up everything nicely. *)
     167
    212168theorem switch_and_labelling_sim : ∀p.
    213169  let e1 ≝ exec_inf … clight_fullexec p in
  • src/Cminor/toRTLabsCorrectness.ma

    r3063 r3081  
    122122| #r #tr #s' #ST #CL normalize in CL; destruct
    123123] qed.
     124
     125(* Build the simulation record for FEMeasurable.  Note that sim_call_label is
     126   made up of the single step for the call combined with a single step for the
     127   label. *)
    124128
    125129definition cminor_rtlabs_meas_sim : meas_sim ≝
  • src/common/FEMeasurable.ma

    r3063 r3081  
    170170qed.
    171171
    172 
     172(* First show that the trace up to the start of the measurable subtrace (i.e.,
     173   the prefix of the execution) is preserved using the simulation results in
     174   the meas_sim record.  Note that this doesn't end cleanly - the first states
     175   in the measurable subtrace may not be in the simulation relation, see the
     176   comment below. *)
    173177
    174178lemma prefix_preserved :
     
    429433  @IH @Ntl
    430434] qed.
     435
     436(* Now show the preservation of parts of the measurable subtrace from states in
     437   simulation to the end.  (We'll deal with any extra steps at the start from
     438   the prefix lemma in the theorem below.)  The basic idea here is that having
     439   broken up the simulation results into normal, call, return and cost lemmas,
     440   we can match up the structure of the two executions, and in particular
     441   prove the will_return_aux predicate for the target execution. *)
    431442
    432443lemma measurable_subtrace_preserved :
     
    777788] qed.
    778789
    779 (* TODO: move*)
    780 lemma plus_split : ∀x,y:nat. ∃z. x = y + z ∨ y = x + z.
    781 #x0 elim x0
    782 [ #y %{y} %2 %
    783 | #x #IH *
    784   [ %{(S x)} %1 %
    785   | #y cases (IH y) #z *
    786     [ #H %{z} %1 >H //
    787     | #H %{z} %2 >H //
    788     ]
    789   ]
    790 ] qed.
    791 
    792 lemma all_append : ∀A,p,l1,l2.
    793   all A p (l1@l2) →
    794   all A p l1 ∧ all A p l2.
    795 #A #p #l1 elim l1
    796 [ //
    797 | #h #t #IH #l2
    798   whd in ⊢ (?% → ?(?%?));
    799   cases (p h) //
    800   @IH
    801 ] qed.
    802 
    803790
    804791lemma ends_at_return_normal : ∀C,g,t1,t2.
     
    825812
    826813
     814(* Now put the two main lemmas above together to show that the target has a
     815   [measurable] subtrace, and that the observables are the same.
     816
     817   To deal with the extra steps from the prefix lemma, note that they are
     818   "normal" steps, and so cannot interfere with the structure. *)
    827819
    828820theorem measured_subtrace_preserved :
  • src/common/SmallstepExec.ma

    r2685 r3081  
    235235qed.
    236236
     237lemma after_aux_result : ∀avs,n,s,tr,P.
     238  after_aux avs n s tr P →
     239  ∃tr',s'. P tr' s' ∧ after_aux avs n s tr (λtr'',s''. 〈tr'',s''〉 = 〈tr',s'〉).
     240#avs #n elim n
     241[ #s #tr #P #A whd in A; %{tr} %{s} % [ @A | % ]
     242| #n' #IH #s #tr #P
     243  whd in ⊢ (% → ?);
     244  lapply (refl ? (is_final … s))
     245  cases (is_final … s) in ⊢ (???% → %);
     246  [ #F whd in ⊢ (% → ?);
     247    lapply (refl ? (step … s))
     248    cases (step … s) in ⊢ (???% → %);
     249    [ #o #k #_ *
     250    | * #tr1 #s1 #ST whd in ⊢ (% → ?);
     251      cases n' in IH ⊢ %;
     252      [ #_ whd in ⊢ (% → ?); #p % [2: % [2: %{p} whd >F whd >ST whd % | skip ] | skip ]
     253      | #n'' #IH lapply (refl ? (avs_inv avs s1)) cases (avs_inv avs s1) in ⊢ (???% → %);
     254        [ #INV #AF
     255          cases (IH … AF) #tr' * #s' * #p #AF'
     256         % [2: % [2: %{p} whd >F whd >ST whd >INV @AF' | skip ] | skip ]
     257        | #_ *
     258        ]
     259      ]
     260    | #m #_ *
     261    ]
     262  | #r #F *
     263  ]
     264] qed.
     265
     266lemma after_n_result : ∀n,O,I,exec,g,s,P,inv.
     267  after_n_steps n O I exec g s inv P →
     268  ∃tr',s'.
     269    P tr' s' ∧
     270    after_n_steps n O I exec g s inv (λtr'',s''. 〈tr'',s''〉 = 〈tr',s'〉).
     271#n #O #I #exec #g #s #P #inv #A
     272cases (after_aux_result … A) #tr * #s' * #p #A'
     273%{tr} %{s'} %{p} @A'
     274qed.
     275
     276lemma after_1_of_n_steps' : ∀n,O,I,exec,g,tr,s',s.
     277  after_n_steps (S n) O I exec g s (λ_.true) (λtrx,sx. 〈trx,sx〉 = 〈tr,s'〉) →
     278  ∃tr1,tr2,s1.
     279  is_final … exec g s = None ? ∧
     280  step … exec g s = Value … 〈tr1,s1〉 ∧
     281  tr = tr1⧺tr2 ∧
     282  after_n_steps n O I exec g s1 (λ_.true) (λtrx,sx. 〈trx,sx〉 = 〈tr2,s'〉).
     283#n #O #I #exec #g #tr #s' #s #A
     284cases (after_1_of_n_steps … A)
     285#tr1 * #s1 * * * #F #ST #_ #A'
     286cases (after_n_result … A')
     287#tr'' * #s'' * #E #A'' destruct
     288% [2: % [2: % [2: % [ % [% [ @F | @ST ] | % ] | @A'' ] | skip ] | skip ] | skip ]
     289qed.
     290
    237291(* A typical way to use the following:
    238292
  • src/utilities/extranat.ma

    r2824 r3081  
    1313    ]
    1414].
     15
     16lemma plus_split : ∀x,y:nat. ∃z. x = y + z ∨ y = x + z.
     17#x0 elim x0
     18[ #y %{y} %2 %
     19| #x #IH *
     20  [ %{(S x)} %1 %
     21  | #y cases (IH y) #z *
     22    [ #H %{z} %1 >H //
     23    | #H %{z} %2 >H //
     24    ]
     25  ]
     26] qed.
    1527
    1628inductive nat_compared : nat → nat → Type[0] ≝
  • src/utilities/lists.ma

    r2897 r3081  
    7474  | * #p #H whd in ⊢ (?%); >p /2/
    7575  ]
     76] qed.
     77
     78lemma all_append : ∀A,p,l1,l2.
     79  all A p (l1@l2) →
     80  all A p l1 ∧ all A p l2.
     81#A #p #l1 elim l1
     82[ //
     83| #h #t #IH #l2
     84  whd in ⊢ (?% → ?(?%?));
     85  cases (p h) //
     86  @IH
    7687] qed.
    7788
Note: See TracChangeset for help on using the changeset viewer.