Changeset 2487


Ignore:
Timestamp:
Nov 23, 2012, 3:47:22 PM (7 years ago)
Author:
campbell
Message:

Set up "after_n_steps" to enforce an invariant on states.

Location:
src
Files:
4 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/labelSimulation.ma

    r2468 r2487  
    642642  state_with_labels_partial s1 s1' →
    643643  exec_step ge s1 = Value … 〈tr,s2〉 →
    644   ∃n. after_n_steps (S n) … clight_exec ge' s1'
     644  ∃n. after_n_steps (S n) … clight_exec ge' s1' (λ_.true)
    645645  (λtr',s2'.
    646646     trace_with_extra_labels tr tr' ∧
     
    960960  state_with_labels s1 s1' →
    961961  exec_step ge s1 = Value … 〈tr,s2〉 →
    962    ∃n. after_n_steps (S n) … clight_exec ge' s1'
     962   ∃n. after_n_steps (S n) … clight_exec ge' s1' (λ_.true)
    963963   (λtr',s2'. trace_with_extra_labels tr tr' ∧
    964964              state_with_labels s2 s2').
     
    11431143  #EX1 #F1
    11441144  cases (step_with_labels … RG … S EX1)
    1145   #n #A cases (after_inv clight_fullexec ???? A) #tr' * #s' * * #TWL #S'
     1145  #n #A cases (after_inv clight_fullexec ????? A) #tr' * #s' * * #TWL #S'
    11461146  lapply F1 whd in ⊢ (??%? → ?); >(final_related … S') #F2
    11471147  whd in match (is_final … s'); >F2 *
     
    11521152  #EX1 #E1'
    11531153  cases (step_with_labels … RG … S EX1)
    1154   #n #AF cases (after_inv clight_fullexec ???? AF) #tr' * #s' * * #TWL #S'
     1154  #n #AF cases (after_inv clight_fullexec ????? AF) #tr' * #s' * * #TWL #S'
    11551155  whd in match (is_final … s'); lapply (refl ? (is_final s'))
    11561156  cases (is_final s') in ⊢ (???% → %);
  • src/Clight/switchRemoval.ma

    r2468 r2487  
    27572757  switch_state_sim ge s1 s1' →
    27582758  exec_step ge s1 = Value … 〈tr,s2〉 → 
    2759   ∃n. after_n_steps (S n) … clight_exec ge' s1'
     2759  ∃n. after_n_steps (S n) … clight_exec ge' s1' (λ_. true)
    27602760  (λtr',s2'. tr = tr' ∧ switch_state_sim ge' s2 s2').
    27612761#ge #ge' #Hrelated #s1 #s1' #tr #s2 #Hsim_state
  • src/common/Executions.ma

    r2338 r2487  
    4646
    4747lemma after_inv : ∀FE:fullexec io_out io_in.
    48  ∀n,g,P,s.
    49   after_n_steps (S n) … FE g s P →
     48 ∀n,g,inv,P,s.
     49  after_n_steps (S n) … FE g s inv P →
    5050  ∃tr,s'.
    5151    P tr s' ∧
     
    5858                 (exec_inf_aux … FE g (step … FE g s'))
    5959    ].
    60 #FE #n #g #P
     60#FE #n #g #inv #P
    6161(* Rather nasty generalisation *)
    6262#s whd in ⊢ (% → ?); cases (is_final … s) [2: #r * ] whd in ⊢ (% → ?); #AW
     
    6666[ #s #tr whd in ⊢ (% → %);
    6767  cases (step … s) [ #o #K * | 3: #m * ]
    68   * #tr' #s' #AW %{tr'} %{s'} %{AW}
     68  * #tr' #s'
     69  whd in ⊢ (% → ?); cases (inv s') [2: *]
     70  #AW %{tr'} %{s'} %{AW}
    6971  lapply (refl ? (is_final … s')) cases (is_final … s') in ⊢ (???% → %);
    7072  [ #NF whd >exec_inf_aux_unfold whd in ⊢ (???%?); >NF @steps_step
     
    7375| #n' #IH #s #tr whd in ⊢ (% → ?);
    7476  cases (step … s) [ #o #K * | 3: #m * ] * #tr1 #s1
     77  whd in ⊢ (% → ?); cases (inv s1) [2: *]
    7578  whd in ⊢ (% → ?); lapply (refl ? (is_final … s1)) cases (is_final … s1) in ⊢ (???% → %);
    7679  [ 2: #r #_ * ] #NF1 whd in ⊢ (% → ?); #AW1
  • src/common/SmallstepExec.ma

    r2459 r2487  
    5959   way whenever the number of steps or the step currently being executed is
    6060   not (reducible to) a value.
     61   
     62   An invariant is also asserted on every state other than the initial one.
    6163
    6264   For example, we state a property to prove by something like
    6365
    64      ∃n. after_n_steps n … clight_exec ge s (λtr,s'. <some property>)
     66     ∃n. after_n_steps n … clight_exec ge s inv (λtr,s'. <some property>)
    6567
    6668   then start reducing by giving the number of steps and reducing the
     
    8789 avs_I : avs_O → Type[0];
    8890 avs_exec : trans_system avs_O avs_I;
    89  avs_g : global ?? avs_exec
     91 avs_g : global ?? avs_exec;
     92 avs_inv : state ?? avs_exec avs_g → bool
    9093}.
    9194
     
    97100| _ ⇒ False
    98101].
     102
     103let rec assert (b:bool) (P:Prop) on b ≝
     104if b then P else False.
    99105
    100106let rec after_aux (avs:await_value_stuff)
     
    108114  [ None ⇒
    109115    await_value avs (step ?? (avs_exec avs) (avs_g avs) s) (λtr',s.
    110       after_aux avs n' s (tr ⧺ tr') P)
     116      assert (avs_inv avs s) (after_aux avs n' s (tr ⧺ tr') P))
    111117  | _ ⇒ False
    112118  ]
     
    116122 ∀O,I. ∀exec:trans_system O I. ∀g:global ?? exec.
    117123 state ?? exec g →
     124 (state ?? exec g → bool) →
    118125 (trace → state ?? exec g → Prop) → Prop ≝
    119 λn,O,I,exec,g,s,P. after_aux (mk_await_value_stuff O I exec g) n s E0 P.
     126λn,O,I,exec,g,s,inv,P. after_aux (mk_await_value_stuff O I exec g inv) n s E0 P.
    120127
    121128lemma after_aux_covariant : ∀avs,P,Q,tr'.
     
    131138  cases (step … s) [1,3: normalize /2/ ]
    132139  * #tr'' #s''
    133   whd in ⊢ (% → %); >Eapp_assoc @IH
    134 ] qed.
    135 
    136 lemma after_n_covariant : ∀n,O,I,exec,g,P,Q.
     140  whd in ⊢ (% → %);
     141  cases (avs_inv avs s'') [ 2: * ]
     142  whd in ⊢ (% → %);
     143  >Eapp_assoc @IH
     144] qed.
     145
     146lemma after_n_covariant : ∀n,O,I,exec,g,P,inv,Q.
    137147  (∀tr,s. P tr s → Q tr s) →
    138148  ∀s.
    139   after_n_steps n O I exec g s P →
    140   after_n_steps n O I exec g s Q.
     149  after_n_steps n O I exec g s inv P →
     150  after_n_steps n O I exec g s inv Q.
    141151normalize /3/
    142152qed.
     
    144154(* for joining a couple of these together *)
    145155
    146 lemma after_n_m : ∀n,m,O,I,exec,g,P,Q,s,s'.
    147   after_n_steps m O I exec g s' Q →
    148   after_n_steps n O I exec g s (λtr1,s1. s' = s1 ∧ (∀tr'',s''. Q tr'' s'' → P (tr1⧺tr'') s'')) →
    149   after_n_steps (n+m) O I exec g s P.
    150 #n #m #O #I #exec #g #P #Q whd in ⊢ (? → ? → ? → % → %); generalize in match E0; elim n
     156lemma after_n_m : ∀n,m,O,I,exec,g,inv,P,Q,s,s'.
     157  after_n_steps m O I exec g s' inv Q →
     158  after_n_steps n O I exec g s inv (λtr1,s1. s' = s1 ∧ (∀tr'',s''. Q tr'' s'' → P (tr1⧺tr'') s'')) →
     159  after_n_steps (n+m) O I exec g s inv P.
     160#n #m #O #I #exec #g #inv #P #Q whd in ⊢ (? → ? → ? → % → %); generalize in match E0; elim n
    151161[ #tr #s #s' #H whd in ⊢ (% → %); * #E destruct #H2
    152162  whd in H; <(E0_right tr) generalize in match E0 in H ⊢ %;
     
    157167    cases (is_final … s) [2: #r * ]
    158168    whd in ⊢ (% → %);
    159     cases (step O I exec g s) [1,3: normalize //] * #tr'' #s'' whd in ⊢ (% → %); >Eapp_assoc @IH ]
     169    cases (step O I exec g s) [1,3: normalize //] * #tr'' #s'' whd in ⊢ (% → %);
     170    cases (inv s'') [2: * ]
     171    >Eapp_assoc @IH ]
    160172| #n' #IH #tr #s #s' #H whd in ⊢ (% → %);
    161173  cases (is_final … s) [2: #r * ]
    162174  whd in ⊢ (% → %);
    163175  cases (step O I exec g s) [1,3: normalize // ]
    164   * #tr1 #s1 whd in ⊢ (% → %); @IH @H
     176  * #tr1 #s1 whd in ⊢ (% → %);
     177  cases (inv s1) [2:*]
     178  @IH @H
    165179] qed.
    166180
    167181(* Inversion lemmas. *)
    168182
    169 lemma after_1_of_n_steps : ∀n,O,I,exec,g,P,s.
    170   after_n_steps (S n) O I exec g s P →
     183lemma after_1_of_n_steps : ∀n,O,I,exec,g,inv,P,s.
     184  after_n_steps (S n) O I exec g s inv P →
    171185  ∃tr,s'. step ?? exec g s = Value … 〈tr,s'〉 ∧
    172   after_n_steps n O I exec g s' (λtr'',s''. P (tr⧺tr'') s'').
    173 #n #O #I #exec #g #P #s
     186  bool_to_Prop (inv s') ∧
     187  after_n_steps n O I exec g s' inv (λtr'',s''. P (tr⧺tr'') s'').
     188#n #O #I #exec #g #inv #P #s
    174189whd in ⊢ (% → ?);
    175190cases (is_final … s)
     
    178193  [ #o #k *
    179194  | * #tr #s' whd in ⊢ (% → ?); >E0_left <(E0_right tr) #AFTER
    180     %{tr} %{s'} % // whd @(after_aux_covariant … AFTER)
    181     #tr' #s'' //
     195    %{tr} %{s'} cases (inv s') in AFTER ⊢ %; #AFTER % /2/ cases AFTER
    182196  | #m *
    183197  ]
     
    185199] qed.
    186200
    187 lemma after_1_step : ∀O,I,exec,g,P,s.
    188   after_n_steps 1 O I exec g s P →
    189   ∃tr,s'. step ?? exec g s = Value … 〈tr,s'〉 ∧ P tr s'.
    190 #O #I #exec #g #P #s #AFTER
     201lemma after_1_step : ∀O,I,exec,g,inv,P,s.
     202  after_n_steps 1 O I exec g s inv P →
     203  ∃tr,s'. step ?? exec g s = Value … 〈tr,s'〉 ∧ bool_to_Prop (inv s') ∧ P tr s'.
     204#O #I #exec #g #inv #P #s #AFTER
    191205cases (after_1_of_n_steps … AFTER)
    192 #tr * #s' * #STEP #FIN %{tr} %{s'} % // whd in FIN; >E0_right in FIN; //
     206#tr * #s' * * #STEP #INV #FIN %{tr} %{s'} % [%] // whd in FIN; >E0_right in FIN; //
    193207qed.
    194208
Note: See TracChangeset for help on using the changeset viewer.