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.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • 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.