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/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 ⊢ (???% → %);
Note: See TracChangeset for help on using the changeset viewer.