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

Tweak exec_steps output; show that simulations extend to measurable
subtrace prefixes.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/SmallstepExec.ma

    r2668 r2669  
    383383(* For now I'm doing this without I/O, to keep things simple.  In the place I
    384384   intend to use it (the definition of measurable subtraces, and proofs using
    385    that) I should allow I/O for the prefix. *)
    386 
    387 let rec exec_steps (n:nat) O I (fx:fullexec O I) (g:global … fx) (s:state … fx g) : res (list (trace × (state … fx g)) × (state … fx g)) ≝
     385   that) I should allow I/O for the prefix.
     386   
     387   If the execution has the form
     388   
     389     s1 -tr1→ s2 -tr2→ … sn -trn→ s'
     390   
     391   then the function returns
     392   
     393     〈[〈s1,tr1〉; 〈s2,tr2〉; …; 〈sn,trn〉], s'〉
     394   *)
     395
     396let rec exec_steps (n:nat) O I (fx:fullexec O I) (g:global … fx) (s:state … fx g) : res (list (state … fx g × trace) × (state … fx g)) ≝
    388397match n with
    389398[ O ⇒ return 〈[ ], s〉
     
    395404    [ Value trs ⇒
    396405        ! 〈tl,s'〉 ← exec_steps m O I fx g (\snd trs);
    397         return 〈trs::tl, s'〉
     406        return 〈〈s, \fst trs〉::tl, s'〉
    398407    | Interact _ _ ⇒ Error … (msg UnexpectedIO)
    399408    | Wrong m ⇒ Error … m
     
    408417  is_final … fx g s = None ? ∧
    409418  ∃tr',s',tl.
    410     trace = 〈tr',s'〉::tl ∧
     419    trace = 〈s,tr'〉::tl ∧
    411420    step … fx g s = Value … 〈tr',s'〉 ∧
    412421    exec_steps n O I fx g s' = OK … 〈tl,s''〉.
     
    454463qed.
    455464
    456 let rec gather_trace S (l:list (trace × S)) on l : trace ≝
     465let rec gather_trace S (l:list (S × trace)) on l : trace ≝
    457466match l with
    458467[ nil ⇒ E0
    459 | cons h t ⇒ (\fst h)⧺(gather_trace S t)
     468| cons h t ⇒ (\snd h)⧺(gather_trace S t)
    460469].
    461470
     
    474483lemma exec_steps_after_n : ∀n,O,I,fx,g,s,trace,s',inv,P.
    475484  exec_steps n O I fx g s = OK ? 〈trace,s'〉 →
    476   all … (λts. inv (\snd ts)) trace →
     485  all ? (λstr. inv (\fst str)) (tail … trace) →
     486  inv s' →
    477487  P (gather_trace ? trace) s' →
    478488  after_n_steps n O I fx g s inv P.
    479489#n elim n
    480490[ #O #I #fx #g #s #trace #s' #inv #P #EXEC whd in EXEC:(??%?); destruct
    481   #ALL #p whd @p
     491  #ALL #FI #p whd @p
    482492| #m #IH #O #I #fx #g #s #trace #s' #inv #P #EXEC
    483493  cases (exec_steps_S … EXEC) #NOTFINAL * #tr1 * #s1 * #tl * * #E1 #STEP #STEPS
    484494  destruct
    485   #ALL cut (bool_to_Prop (inv s1) ∧ bool_to_Prop (all … (λts. inv (\snd ts)) tl))
    486   [ whd in ALL:(?%); cases (inv s1) in ALL ⊢ %; /2/ ] * #i1 #itl
    487   #p @(after_n_m 1 … (λtr,s. P (tr1⧺tr) s) … (IH … STEPS itl ?))
     495  #ALL #FALL cut (bool_to_Prop (inv s1) ∧ bool_to_Prop (all ? (λst. inv (\fst st)) (tail … tl)))
     496  [ cases m in STEPS;
     497    [ whd in ⊢ (??%? → ?); #E destruct /2/
     498    | #m' #STEPS cases (exec_steps_S … STEPS) #_ * #tr'' * #s'' * #tl'' * * #E #_ #_ destruct
     499      whd in ALL:(?%); cases (inv s1) in ALL ⊢ %; /2/
     500    ]
     501  ] * #i1 #itl
     502  #p @(after_n_m 1 … (λtr,s. P (tr1⧺tr) s) … (IH … STEPS itl ??))
    488503  [ @p
     504  | @FALL
    489505  | whd >NOTFINAL whd >STEP whd >i1 whd %{(refl ??)} #tr'' #s'' #p' @p'
    490506  ]
     
    497513#n #O #I #fx #g #s #trace #s' #P #EXEC #p
    498514@(exec_steps_after_n … EXEC) //
    499 elim trace /2/
     515cases trace // #x #trace'
     516elim trace' /2/
    500517qed.
    501518
     
    510527  cases (IH … AFTER')
    511528  #tl * #s' * #STEPS #p
    512   %{(〈tr1,s1〉::tl)} %{s'} %
     529  %{(〈s,tr1〉::tl)} %{s'} %
    513530  [ whd in ⊢ (??%?); >NF whd in ⊢ (??%?); >STEP whd in ⊢ (??%?); >STEPS % | // ]
    514531] qed.
     
    526543  cases (exec_steps_S … EXEC) #NF * #tr' * #s' * #tl * * #E1 #STEP #EXEC'
    527544  cases (IH … EXEC') #trace1 * #trace2 * #s1 * * #EXEC1 #EXEC2 #E2
    528   %{(〈tr',s'〉::trace1)} %{trace2} %{s1}
     545  %{(〈s,tr'〉::trace1)} %{trace2} %{s1}
    529546  %
    530547  [ %
     
    549566] qed.
    550567
    551 (* Show that it corresponds to split_trace … (exec_inf …) *)
     568lemma exec_steps_first : ∀n,O,I,fx,g,s,s1,tr1,tl,s'.
     569  exec_steps n O I fx g s = OK ? 〈〈s1,tr1〉::tl,s'〉 →
     570  s = s1.
     571#n #O #I #fx #g #s #s1 #tr1 #tl #s' #EXEC
     572lapply (exec_steps_length … EXEC) #E normalize in E; destruct
     573cases (exec_steps_S … EXEC) #_ * #tr2 * #s2 * #tl2 * * #E #_ #_ destruct
     574%
     575qed.
     576
     577(* Show that it corresponds to split_trace … (exec_inf …).
     578   We need to adjust the form of trace. *)
     579
     580let rec switch_trace_aux S tr (l:list (S × trace)) (s':S) on l : list (trace × S) ≝
     581match l with
     582[ nil ⇒ [〈tr,s'〉]
     583| cons h t ⇒ 〈tr,\fst h〉::(switch_trace_aux S (\snd h) t s')
     584].
     585
     586definition switch_trace ≝
     587λS,l,s'. match l with
     588[ nil ⇒ nil ?
     589| cons h t ⇒ switch_trace_aux S (\snd h) t s'
     590].
    552591
    553592lemma exec_steps_inf_aux : ∀O,I. ∀fx:fullexec O I. ∀g,n,s,trace,s'.
    554593  exec_steps n O I fx g s = OK ? 〈trace,s'〉 →
    555594  match is_final … s' with
    556   [ None ⇒ split_trace … (exec_inf_aux … fx g (step … fx g s)) n = Some ? 〈trace, exec_inf_aux … fx g (step … s')〉
    557   | Some r ⇒ n = 0 ∨ ∃tr'. split_trace … (exec_inf_aux … fx g (step … fx g s)) n = Some ? 〈trace, e_stop … tr' r s'〉
     595  [ None ⇒ split_trace … (exec_inf_aux … fx g (step … fx g s)) n = Some ? 〈switch_trace ? trace s', exec_inf_aux … fx g (step … s')〉
     596  | Some r ⇒ n = 0 ∨ ∃tr'. split_trace … (exec_inf_aux … fx g (step … fx g s)) n = Some ? 〈switch_trace ? trace s', e_stop … tr' r s'〉
    558597  ].
    559598#O #I #fx #g #n elim n
     
    570609    >exec_inf_aux_unfold normalize nodelta
    571610    cases (is_final … s')
    572     [ %
     611    [ whd %
    573612    | #r %2 %{tr''} %
    574613    ]
    575   | * #tr1 #s1 #tl1 #E normalize in E; destruct #Esteps
     614  | * #s1 #tr1 #tl1 #E normalize in E; destruct #Esteps
    576615    lapply (IH … Esteps) cases (is_final … s')
    577     [ normalize nodelta #IH' >Estep >exec_inf_aux_unfold whd in ⊢ (??(????%?)?);
    578       >(exec_steps_nonterm … Esteps) whd in ⊢ (??%?); >IH' %
     616    [ normalize nodelta #IH' >Estep <(exec_steps_first … Esteps)
     617      >exec_inf_aux_unfold whd in ⊢ (??(????%?)?);
     618      >(exec_steps_nonterm … Esteps) whd in ⊢ (??%?); >IH' normalize nodelta %
    579619    | normalize nodelta #r *
    580620      [ #E @⊥ >(exec_steps_length … Esteps) in E; #E normalize in E; destruct
    581       | * #tr'' #IH' %2 %{tr''} >Estep >exec_inf_aux_unfold whd in ⊢ (??(????%?)?);
     621      | * #tr'' #IH' %2 %{tr''} >Estep <(exec_steps_first … Esteps)
     622        >exec_inf_aux_unfold whd in ⊢ (??(????%?)?);
    582623        >(exec_steps_nonterm … Esteps) whd in ⊢ (??%?); >IH' %
    583624      ]
Note: See TracChangeset for help on using the changeset viewer.