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/SmallstepExec.ma

    r2618 r2668  
    183183lemma after_1_of_n_steps : ∀n,O,I,exec,g,inv,P,s.
    184184  after_n_steps (S n) O I exec g s inv P →
    185   ∃tr,s'. step ?? exec g s = Value … 〈tr,s'〉 ∧
     185  ∃tr,s'.
     186  is_final … exec g s = None ? ∧
     187  step … exec g s = Value … 〈tr,s'〉 ∧
    186188  bool_to_Prop (inv s') ∧
    187189  after_n_steps n O I exec g s' inv (λtr'',s''. P (tr⧺tr'') s'').
     
    193195  [ #o #k *
    194196  | * #tr #s' whd in ⊢ (% → ?); >E0_left <(E0_right tr) #AFTER
    195     %{tr} %{s'} cases (inv s') in AFTER ⊢ %; #AFTER % /2/ cases AFTER
     197    %{tr} %{s'} cases (inv s') in AFTER ⊢ %; #AFTER % /3/ cases AFTER
    196198  | #m *
    197199  ]
     
    201203lemma after_1_step : ∀O,I,exec,g,inv,P,s.
    202204  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'.
     205  ∃tr,s'. is_final … exec g s = None ? ∧
     206    step ?? exec g s = Value … 〈tr,s'〉 ∧
     207    bool_to_Prop (inv s') ∧ P tr s'.
    204208#O #I #exec #g #inv #P #s #AFTER
    205209cases (after_1_of_n_steps … AFTER)
    206 #tr * #s' * * #STEP #INV #FIN %{tr} %{s'} % [%] // whd in FIN; >E0_right in FIN; //
     210#tr * #s' * * * #NF #STEP #INV #FIN %{tr} %{s'} % [%[%]] // whd in FIN; >E0_right in FIN; //
    207211qed.
    208212
     
    377381].
    378382
    379 
     383(* For now I'm doing this without I/O, to keep things simple.  In the place I
     384   intend to use it (the definition of measurable subtraces, and proofs using
     385   that) I should allow I/O for the prefix. *)
     386
     387let 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)) ≝
     388match n with
     389[ O ⇒ return 〈[ ], s〉
     390| S m ⇒
     391  match is_final … fx g s with
     392  [ Some r ⇒ Error … (msg TerminatedEarly)
     393  | None ⇒
     394    match step … fx g s with
     395    [ Value trs ⇒
     396        ! 〈tl,s'〉 ← exec_steps m O I fx g (\snd trs);
     397        return 〈trs::tl, s'〉
     398    | Interact _ _ ⇒ Error … (msg UnexpectedIO)
     399    | Wrong m ⇒ Error … m
     400    ]
     401  ]
     402].
     403
     404(* Show that it's nice. *)
     405
     406lemma exec_steps_S : ∀O,I,fx,g,n,s,trace,s''.
     407  exec_steps (S n) O I fx g s = OK … 〈trace,s''〉 →
     408  is_final … fx g s = None ? ∧
     409  ∃tr',s',tl.
     410    trace = 〈tr',s'〉::tl ∧
     411    step … fx g s = Value … 〈tr',s'〉 ∧
     412    exec_steps n O I fx g s' = OK … 〈tl,s''〉.
     413#O #I #fx #g #n #s #trace #s''
     414whd in ⊢ (??%? → ?);
     415cases (is_final … s)
     416[ whd in ⊢ (??%? → ?);
     417  cases (step … s)
     418  [ #o #i #EX whd in EX:(??%?); destruct
     419  | * #tr' #s' whd in ⊢ (??%? → ?); #EX %{(refl ??)}
     420    %{tr'} %{s'} cases (exec_steps … g s') in EX ⊢ %;
     421    [ * #tl #s'' #EX whd in EX:(??%?); destruct %{tl} /3/
     422    | #m #EX whd in EX:(??%?); destruct
     423    ]
     424  | #m #EX whd in EX:(??%?); destruct
     425  ]
     426| #r #EX whd in EX:(??%?); destruct
     427] qed.
     428
     429lemma exec_steps_length : ∀O,I,fx,g,n,s,trace,s'.
     430  exec_steps n O I fx g s = OK … 〈trace,s'〉 →
     431  n = |trace|.
     432#O #I #fx #g #n elim n
     433[ #s #trace #s' #EX whd in EX:(??%?); destruct %
     434| #m #IH #s #trace #s' #EX
     435  cases (exec_steps_S … EX) #notfinal * #tr' * #s'' * #tl * * #Etl #Estep #steps
     436  >(IH … steps) >Etl %
     437] qed.
     438
     439lemma exec_steps_nonterm : ∀O,I,fx,g,n,s,h,t,s'.
     440  exec_steps n O I fx g s = OK … 〈h::t,s'〉 →
     441  is_final … s = None ?.
     442#O #I #fx #g #n #s #h #t #s' #EX
     443lapply (exec_steps_length … EX)
     444#Elen destruct whd in EX:(??%?);
     445cases (is_final … s) in EX ⊢ %;
     446[ //
     447| #r #EX whd in EX:(??%?); destruct
     448] qed.
     449
     450lemma exec_steps_nonterm' : ∀O,I,fx,g,n,s,h,t,s'.
     451  exec_steps n O I fx g s = OK … 〈h@[t], s'〉 →
     452  is_final … s = None ?.
     453#O #I #fx #g #n #s * [2: #h1 #h2] #t #s' @exec_steps_nonterm
     454qed.
     455
     456let rec gather_trace S (l:list (trace × S)) on l : trace ≝
     457match l with
     458[ nil ⇒ E0
     459| cons h t ⇒ (\fst h)⧺(gather_trace S t)
     460].
     461
     462lemma exec_steps_after_n_simple : ∀n,O,I,fx,g,s,trace,s'.
     463  exec_steps n O I fx g s = OK ? 〈trace,s'〉 →
     464  after_n_steps n O I fx g s (λ_. true) (λtr,s''. 〈tr,s''〉 = 〈gather_trace ? trace,s'〉).
     465#n elim n
     466[ #O #I #fx #g #s #trace #s' #EXEC whd in EXEC:(??%?); destruct
     467  whd %
     468| #m #IH #O #I #fx #g #s #trace #s' #EXEC
     469  cases (exec_steps_S … EXEC) #NOTFINAL * #tr1 * #s1 * #tl * * #E1 #STEP #STEPS
     470  @(after_n_m 1 … (IH … STEPS))
     471  whd >NOTFINAL whd >STEP whd %{(refl ??)} #tr'' #s'' #E destruct %
     472] qed.
     473
     474lemma exec_steps_after_n : ∀n,O,I,fx,g,s,trace,s',inv,P.
     475  exec_steps n O I fx g s = OK ? 〈trace,s'〉 →
     476  all … (λts. inv (\snd ts)) trace →
     477  P (gather_trace ? trace) s' →
     478  after_n_steps n O I fx g s inv P.
     479#n elim n
     480[ #O #I #fx #g #s #trace #s' #inv #P #EXEC whd in EXEC:(??%?); destruct
     481  #ALL #p whd @p
     482| #m #IH #O #I #fx #g #s #trace #s' #inv #P #EXEC
     483  cases (exec_steps_S … EXEC) #NOTFINAL * #tr1 * #s1 * #tl * * #E1 #STEP #STEPS
     484  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 ?))
     488  [ @p
     489  | whd >NOTFINAL whd >STEP whd >i1 whd %{(refl ??)} #tr'' #s'' #p' @p'
     490  ]
     491] qed.
     492
     493lemma exec_steps_after_n_noinv : ∀n,O,I,fx,g,s,trace,s',P.
     494  exec_steps n O I fx g s = OK ? 〈trace,s'〉 →
     495  P (gather_trace ? trace) s' →
     496  after_n_steps n O I fx g s (λ_.true) P.
     497#n #O #I #fx #g #s #trace #s' #P #EXEC #p
     498@(exec_steps_after_n … EXEC) //
     499elim trace /2/
     500qed.
     501
     502lemma after_n_exec_steps : ∀n,O,I. ∀fx:fullexec O I. ∀g,s,inv,P.
     503  after_n_steps n O I fx g s inv P →
     504  ∃trace,s'. exec_steps n O I fx g s = OK ? 〈trace,s'〉 ∧ P (gather_trace ? trace) s'.
     505#n elim n
     506[ #O #I #fx #g #s #inv #P #AFTER %{[ ]} %{s} %{(refl ??)} @AFTER
     507| #m #IH #O #I #fx #g #s #inv #P #AFTER
     508  cases (after_1_of_n_steps … AFTER)
     509  #tr1 * #s1 * * * #NF #STEP #INV #AFTER'
     510  cases (IH … AFTER')
     511  #tl * #s' * #STEPS #p
     512  %{(〈tr1,s1〉::tl)} %{s'} %
     513  [ whd in ⊢ (??%?); >NF whd in ⊢ (??%?); >STEP whd in ⊢ (??%?); >STEPS % | // ]
     514] qed.
     515
     516lemma exec_steps_split : ∀n,m,O,I,fx,g,s,trace,s'.
     517  exec_steps (n+m) O I fx g s = OK ? 〈trace,s'〉 →
     518  ∃trace1,trace2,s1.
     519    exec_steps n O I fx g s = OK ? 〈trace1,s1〉 ∧
     520    exec_steps m O I fx g s1 = OK ? 〈trace2,s'〉 ∧   
     521    trace = trace1 @ trace2.
     522#n elim n
     523[ #m #O #I #fx #g #s #trace #s' #EXEC
     524  %{[ ]} %{trace} %{s} /3/
     525| #n' #IH #m #O #I #fx #g #s #trace #s' #EXEC
     526  cases (exec_steps_S … EXEC) #NF * #tr' * #s' * #tl * * #E1 #STEP #EXEC'
     527  cases (IH … EXEC') #trace1 * #trace2 * #s1 * * #EXEC1 #EXEC2 #E2
     528  %{(〈tr',s'〉::trace1)} %{trace2} %{s1}
     529  %
     530  [ %
     531    [ whd in ⊢ (??%?); >NF >STEP whd in ⊢ (??%?); >EXEC1 %
     532    | @EXEC2
     533    ]
     534  | destruct %
     535  ]
     536] qed.
     537
     538lemma exec_steps_join : ∀n,m,O,I,fx,g,s1,trace1,s2,trace2,s3.
     539  exec_steps n O I fx g s1 = OK ? 〈trace1,s2〉 →
     540  exec_steps m O I fx g s2 = OK ? 〈trace2,s3〉 →
     541  exec_steps (n+m) O I fx g s1 = OK ? 〈trace1@trace2,s3〉.
     542#n elim n
     543[ #m #O #I #fx #g #s1 #trace1 #s2 #trace2 #s3 #EXEC1 #EXEC2
     544  whd in EXEC1:(??%?); destruct @EXEC2
     545| #n' #IH #m #O #I #fx #g #s1 #trace1 #s2 #trace2 #s3 #EXEC1 #EXEC2
     546  cases (exec_steps_S … EXEC1) #NF * #tr' * #s' * #tl' * * #E1 #STEP #EXEC'
     547  whd in ⊢ (??%?); >NF >STEP whd in ⊢ (??%?); >(IH … EXEC' EXEC2)
     548  destruct %
     549] qed.
     550
     551(* Show that it corresponds to split_trace … (exec_inf …) *)
     552
     553lemma exec_steps_inf_aux : ∀O,I. ∀fx:fullexec O I. ∀g,n,s,trace,s'.
     554  exec_steps n O I fx g s = OK ? 〈trace,s'〉 →
     555  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'〉
     558  ].
     559#O #I #fx #g #n elim n
     560[ #s #trace #s' #EX whd in EX:(??%%); destruct
     561  cases (is_final … s') [ % | #r %1 % ]
     562| #m #IH #s #trace #s' #EX
     563  cases (exec_steps_S … EX)
     564  #notfinal * #tr'' * #s'' * #tl * * #Etrace #Estep #Esteps
     565  cases tl in Etrace Esteps ⊢ %;
     566  [ #E destruct #Esteps
     567    lapply (exec_steps_length … Esteps) #Elen normalize in Elen; destruct
     568    whd in Esteps:(??%?); destruct
     569    >Estep
     570    >exec_inf_aux_unfold normalize nodelta
     571    cases (is_final … s')
     572    [ %
     573    | #r %2 %{tr''} %
     574    ]
     575  | * #tr1 #s1 #tl1 #E normalize in E; destruct #Esteps
     576    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' %
     579    | normalize nodelta #r *
     580      [ #E @⊥ >(exec_steps_length … Esteps) in E; #E normalize in E; destruct
     581      | * #tr'' #IH' %2 %{tr''} >Estep >exec_inf_aux_unfold whd in ⊢ (??(????%?)?);
     582        >(exec_steps_nonterm … Esteps) whd in ⊢ (??%?); >IH' %
     583      ]
     584    ]
     585  ]
     586] qed.
Note: See TracChangeset for help on using the changeset viewer.