Ignore:
Timestamp:
Feb 15, 2013, 11:27:56 AM (7 years ago)
Author:
campbell
Message:

Intermediate measurable proof check-in before I change its traces again.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/FEMeasurable.ma

    r2644 r2668  
    1616  ms_stack : ∀g1,g2. ms_inv g1 g2 → (ident → nat);
    1717  ms_rel : ∀g1,g2. ∀INV:ms_inv g1 g2. state … ms_C1 g1 → state … ms_C2 g2 → Prop;
     18  ms_rel_normal : ∀g1,g2,INV,s1,s2. ms_rel g1 g2 INV s1 s2 → bool_to_Prop (normal_state ms_C1 g1 s1) ↔ bool_to_Prop (normal_state ms_C2 g2 s2);
     19  ms_rel_labelled : ∀g1,g2,INV,s1,s2. ms_rel g1 g2 INV s1 s2 → bool_to_Prop (pcs_labelled ms_C1 g1 s1) ↔ bool_to_Prop (pcs_labelled ms_C2 g2 s2);
    1820  sim_normal :
    1921    ∀g1,g2.
     
    129131] qed.
    130132
    131 (* WIP commented out
     133lemma stack_labelled_step : ∀C:preclassified_system. ∀g,s1,trace,s2,stack,current.
     134  exec_steps 1 io_out io_in C g s1 = OK ? 〈trace,s2〉 →
     135  pcs_labelled C g s1 →
     136  stack_after (pcs_to_cs C g stack) current trace = current.
     137#C #g #s1 #trace #s2 #stack #current #EXEC
     138cases (exec_steps_S … EXEC)
     139#NF * #tr * #s' * #tl * * #Etr #STEP #EXEC' whd in EXEC':(??%?); destruct
     140#CS
     141whd in ⊢ (??%?); whd in match (cs_classify ??); >CS
     142
     143
     144(* WIP commented out*)
    132145lemma prefix_preserved :
    133146  ∀MS:meas_sim.
    134   ∀g1,g2.
    135   ∀INV:ms_inv MS g1 g2.
     147  ∀g,g'.
     148  ∀INV:ms_inv MS g g'.
    136149  ∀max_allowed_stack.
    137   ∀s1,s1',tr,tr'.
    138   ms_rel MS g1 g2 INV s1 s1' →
     150  ∀s1,s1'.
     151  ms_rel MS g g' INV s1 s1' →
     152
     153  ∀m,prefix,sf.
     154  exec_steps m … (pcs_exec … (ms_C1 MS)) g s1 = OK ? 〈prefix,sf〉 →
     155  le (max_stack (pcs_to_cs (ms_C1 MS) ? (ms_stack MS … INV)) 0 prefix) max_allowed_stack →
     156
     157  ∃m',prefix',sf'.
     158    exec_steps m' … (pcs_exec … (ms_C2 MS)) g' s1' = OK ? 〈prefix',sf'〉 ∧
     159    le (max_stack (pcs_to_cs (ms_C2 MS) ? (ms_stack MS … INV)) 0 prefix') max_allowed_stack ∧
    139160 
    140   let trace ≝ (exec_inf_aux ?? (pcs_exec … (ms_C1 MS)) g1 (Value … 〈tr,s1〉)) in
    141   let trace' ≝ (exec_inf_aux ?? (pcs_exec … (ms_C2 MS)) g2 (Value … 〈tr',s1'〉)) in
    142  
    143   ∀m,prefix,suffix.
    144   split_trace … trace m = Some ? 〈prefix,suffix〉 →
    145   le (max_stack (pcs_to_cs (ms_C1 MS) ? (ms_stack MS … INV)) prefix) max_allowed_stack →
    146 
    147   ∃m',prefix',suffix'.
    148     split_trace … trace' m' = Some ? 〈prefix',suffix'〉 ∧
    149     le (max_stack (pcs_to_cs (ms_C2 MS) ? (ms_stack MS … INV)) prefix') max_allowed_stack ∧
    150  
    151   ∃s2,s2',tr2,tr2'.
    152     suffix = exec_inf_aux ?? (pcs_exec …  (ms_C1 MS)) g1 (Value … 〈tr2,s2〉) ∧
    153     suffix' = exec_inf_aux ?? (pcs_exec … (ms_C2 MS)) g2 (Value … 〈tr2',s2'〉) ∧
    154     ms_rel MS g1 g2 INV s2 s2'.
    155 * #C1 #C2 #compiled #inv #stack #rel #sim_normal #sim_call_return #sim_cost #sim_init
    156 #g1 #g2 #INV #max #s1 #s1' #tr #tr' #REL
    157 letin trace ≝ (exec_inf_aux ?????)
    158 letin trace' ≝ (exec_inf_aux ?????)
    159 #m0
     161    ms_rel MS g g' INV sf sf'.
     162* #C1 #C2 #compiled #inv #stack #rel #rel_normal #rel_labelled #sim_normal #sim_call_return #sim_cost #sim_init
     163#g #g' #INV #max #s1 #s1' #REL
     164#m0 generalize in match s1' in REL ⊢ %; generalize in match s1; -s1 -s1'
     165generalize in match 0; (* current stack level *)
    160166@(nat_elim1 m0)
    161167*
    162 [ #_ #prefix #suffix #split whd in split:(??%?); destruct
    163   #max_ok %{0} %{[]} %{trace'}
    164   % [ % // | %{s1} %{s1'} %{tr} %{tr'} /3/ ]
    165 | *
    166   [ (* m = 1; just extracts the current state *)
    167     #_ #prefix #suffix #split #max_ok
    168     cases (split_trace_1 … split) #E1 #foo
    169     %{1} %{[〈tr',s1'〉]} %{(exec_inf_aux … (step … s1'))}
    170     % [ %
    171  #m #IH #prefix #suffix #split #max_ok
    172   (* clean up first step? *)
     168[ #_ #current_stack #s1 #s1' #REL #prefix #sf #exec whd in exec:(??%?); destruct
     169  #max_ok %{0} %{[]} %{s1'}
     170  % [ % // | // ]
     171| #m #IH #current_stack #s1 #s1' #REL #prefix #sf #exec #max_ok
    173172  cases (true_or_false_Prop … (pcs_labelled … s1))
    174   [ #CS cases (split_trace_S … split) #trace1 * #Etrace *
    175     [ * #notfinal #split1
    176     lapply (sim_cost … REL CS)
     173  [ #CS
     174    cases (exec_steps_split 1 … exec) #trace1 * #trace2 * #s2 * * #EXEC1 #EXEC2 #E1
     175    lapply (sim_cost … s2 ? REL CS ?)
     176    [ @(exec_steps_after_n_noinv … EXEC1) % | skip ]
     177    #AFTER'
     178    cases (after_n_exec_steps … AFTER')
     179    #prefix' * #s2' * #EXEC1' * #Etrace #R2
     180    cases (IH m ? (stack_after (pcs_to_cs C2 … (stack … INV)) current_stack prefix') … R2 … EXEC2 ?)
     181    [ 2: // | 3: @(transitive_le … max_ok) >E1 <max_stack_append
     182
     183     @le_maxr
     184    #m'' * #prefix'' * #sf'' * * #EXEC'' #MAX'' #R''
     185    %{(1+m'')} %{(prefix'@prefix'')} %{sf''}
     186    % [ % [ @(exec_steps_join … EXEC1') @EXEC'' | cases daemon ] | @R2
     187  |
     188    %{trace1 }
     189
     190  cases (exec_steps_S … exec) #notfinal * #tr' * #s' * #tl * * #E #STEP #EXEC'
     191  cases (true_or_false_Prop … (pcs_labelled … s1))
     192  [ #CS lapply (sim_cost … s' tr' REL CS ?)
     193    [ @(exec_steps_after_n_noinv … whd >notfinal whd >STEP whd % ]
     194    #AFTER %{1}
    177195    [ 3: whd in match (after_n_steps ????? s1 ??);
    178196      >(?:is_final ???? s1 = None ?) [ whd in ⊢ ((% → ?) → ?);
Note: See TracChangeset for help on using the changeset viewer.