Ignore:
Timestamp:
Mar 21, 2011, 6:27:22 PM (9 years ago)
Author:
campbell
Message:

Refine small-step executable semantics abstraction a little.
Some progress on using the new definition in CexecEquiv?, but only partial
because of over-eager normalisation by the destruct tactic.
Whole program semantics for RTLabs using it.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/CexecEquiv.ma

    r700 r702  
    4949] qed.
    5050
    51 lemma exec_e_step: ∀p,ge,x,tr,s,e.
    52   exec_inf_aux (clight_exec p) ge x = e_step ??? tr s e →
    53   exec_inf_aux (clight_exec p) ge (exec_step ge s) = e.
    54 #p #ge #x #tr #s #e
     51lemma is_final_elim: ∀s.∀P:option int → Type[0].
     52 (∀r. final_state s r → P (Some ? r)) →
     53 ((¬∃r.final_state s r) → P (None ?)) →
     54P (is_final clight_exec s).
     55#s #P #F #NF whd in ⊢ (?%) cases (is_final_state s)
     56[ * #r #FINAL @F @FINAL
     57| #NOTFINAL @NF @NOTFINAL
     58] qed.
     59
     60lemma exec_e_step: ∀ge,x,tr,s,e.
     61  exec_inf_aux clight_exec ge x = e_step ??? tr s e →
     62  exec_inf_aux clight_exec ge (exec_step ge s) = e.
     63#ge #x #tr #s #e
    5564>(exec_inf_aux_unfold …) cases x;
    5665[ #o #k #EXEC whd in EXEC:(??%?); destruct
    57 | #y cases y; #tr' #s' whd in ⊢ (??%? → ?); >(?:? (clight_exec p) s' = is_final s'); whd in match (? (clight_exec) s') in ⊢ %; whd in ⊢ (??%? → ?);
    58     cases (is_final_state s'); #FINAL #EXEC whd in EXEC:(??%?); destruct;
    59     @refl
     66| #y cases y; #tr' #s' whd in ⊢ (??%? → ?)
     67  @is_final_elim
     68  [ #r #FINAL | #FINAL ]
     69  (* Some trickery to prevent destruct normalizing clight_exec *)
     70  #EXEC whd in EXEC:(??%?); [ @False_ind destruct |
     71  cut (s = s') [ generalize in EXEC:(??(??????%)?) ⊢ ? #e0 #E destruct @refl ]
     72  #Es <Es in EXEC #EXEC
     73  generalize in EXEC:(??(??????%)?) ⊢ (??%?)
     74  #e0 #E destruct @refl
     75  ]
    6076| #EXEC whd in EXEC:(??%?); destruct
    6177] qed.
    6278
    6379lemma exec_e_step_inv: ∀ge,x,tr,s,e.
    64   exec_inf_aux ge x = e_step tr s e →
     80  exec_inf_aux clight_exec ge x = e_step ??? tr s e →
    6581  x = Value ??? 〈tr,s〉.
    6682#ge #x #tr #s #e
     
    6884[ #o #k #EXEC whd in EXEC:(??%?); destruct
    6985| #y cases y; #tr' #s' whd in ⊢ (??%? → ?);
    70     cases (is_final_state s'); #FINAL #EXEC whd in EXEC:(??%?); destruct;
     86  @is_final_elim
     87  [ #r ] #FINAL #EXEC whd in EXEC:(??%?)
     88  (* Again, prevent destruct blowing up *)
     89  [ 2: generalize in EXEC:(??(??????%)?) ⊢ ? #e0 #EXEC ]
     90  destruct;
    7191    @refl
    7292| #EXEC whd in EXEC:(??%?); destruct
     
    7494
    7595lemma exec_e_step_inv2: ∀ge,x,tr,s,e.
    76   exec_inf_aux ge x = e_step tr s e →
     96  exec_inf_aux clight_exec ge x = e_step ??? tr s e →
    7797  ¬∃r.final_state s r.
    7898#ge #x #tr #s #e
    7999>(exec_inf_aux_unfold …) cases x;
    80100[ #o #k #EXEC whd in EXEC:(??%?); destruct
    81 | #y cases y; #tr' #s' whd in ⊢ (??%? → ?);
    82     cases (is_final_state s'); #FINAL #EXEC whd in EXEC:(??%?); destruct;
    83     @FINAL
     101| #y cases y; #tr' #s' whd in ⊢ (??%? → ?)
     102  @is_final_elim [ #r #F #EXEC whd in EXEC:(??%?); destruct
     103  | #F whd in ⊢ (??%? → ?) generalize in ⊢ (??(??????%)? → ?) #e0 #EXEC destruct  @F ]
    84104| #EXEC whd in EXEC:(??%?); destruct
    85105] qed.
    86106
    87107definition exec_from : genv → state → s_execution → Prop ≝
    88 λge,s,se. single_exec_of (exec_inf_aux ge (exec_step ge s)) se.
     108λge,s,se. single_exec_of (exec_inf_aux clight_exec ge (exec_step ge s)) se.
     109
     110lemma se_step_eq : ∀tr,s,e,tr',s',e'.
     111 se_step tr s e = se_step tr' s' e' →
     112 tr = tr' ∧ s = s' ∧ e = e'.
     113#tr #s #e #tr' #s' #e' #E
     114(* destruct  This takes a hideous amount of time, not sure why. *)
     115@(match E return λl.λ_. match l with [ se_step tr0 s0 e0 ⇒ tr = tr0 ∧ s = s0 ∧ e = e0 | _ ⇒ False ] with [ refl ⇒ ? ])
     116whd % try % @refl qed.
    89117
    90118lemma exec_from_step : ∀ge,s,tr,s',e.
     
    93121#ge #s0 #tr0 #s0' #e0 #H inversion H;
    94122[ #tr #r #m #E1 #E2 destruct
    95 | #tr #s #e #se #H1 #H2 #E destruct (E);
     123| #tr #s #e #se #H1 #H2 #E (*destruct (E);*)
     124  lapply (se_step_eq … E) * * #E1 #E2 #E3 >E1 >E2 >E3
    96125    >(exec_e_step_inv … H2)
    97126    <(exec_e_step … H2) in H1 #H1 % //
     
    100129] qed.
    101130
    102 lemma exec_from_interact : ∀ge,s,o,k,i,tr,s',e.
     131axiom exec_from_interact : ∀ge,s,o,k,i,tr,s',e.
    103132exec_from ge s (se_interact o k i (se_step tr s' e)) →
    104133step ge s tr s' ∧
    105134(*exec_step ge s = Value ??? 〈tr,s'〉 ∧*) exec_from ge s' e.
     135(*
    106136#ge #s0 #o0 #k0 #i0 #tr0 #s0' #e0 #H inversion H;
    107137[ #tr #r #m #E1 #E2 destruct
    108138| #tr #s #e #se #H1 #H2 #E destruct (E)
    109139| #_ #E destruct
    110 | #o #k #i #se #H1 #H2 #E destruct (E);
     140| #o #k #i #se #H1 #H2 #E (*destruct (E);*)
    111141    lapply (exec_step_sound ge s0);
    112142    cases (exec_step ge s0) in H2 ⊢ %;
     
    130160        #E' whd in E':(??%?); destruct (E');
    131161    ]
    132 ] qed.
    133 
    134 lemma exec_from_interact_stop : ∀ge,s,o,k,i,tr,r,m.
     162] qed.*)
     163
     164axiom exec_from_interact_stop : ∀ge,s,o,k,i,tr,r,m.
    135165exec_from ge s (se_interact o k i (se_stop tr r m)) →
    136166step ge s tr (Returnstate (Vint r) Kstop m).
     167(*
    137168#ge #s0 #o0 #k0 #i0 #tr0 #s0' #e0 #H inversion H;
    138169[ #tr #r #m #E1 #E2 destruct
     
    169200   | #E whd in E:(??%?); destruct (E)
    170201   ]
    171 ] qed.
     202] qed.*)
    172203
    173204(* NB: the E0 in the execs are irrelevant. *)
     
    251282] qed.
    252283
    253 lemma final_step: ∀ge,tr,r,m,s.
     284axiom final_step: ∀ge,tr,r,m,s.
    254285  exec_from ge s (se_stop tr r m) →
    255286  step ge s tr (Returnstate (Vint r) Kstop m).
     287  (*
    256288#ge #tr #r #m #s #EXEC
    257289whd in EXEC;
     
    272304| #EXEC' #E destruct
    273305| #o #k #i #e #H #EXEC #E destruct
    274 ] qed.
     306] qed.*)
    275307
    276308
    277309lemma e_stop_inv: ∀ge,x,tr,r,m.
    278   exec_inf_aux ge x = e_stop tr r m →
     310  exec_inf_aux clight_exec ge x = e_stop ??? tr r m →
    279311  x = Value ??? 〈tr,Returnstate (Vint r) Kstop m〉.
    280312#ge #x #tr #r #m
    281313>(exec_inf_aux_unfold …) cases x;
    282314[ #o #k #EXEC whd in EXEC:(??%?); destruct;
    283 | #z cases z; #tr' #s' whd in ⊢ (??%? → ?); cases (is_final_state s');
    284   [ #F cases F; #r' #FINAL cases FINAL; #r'' #m' #EXEC whd in EXEC:(??%?);
     315| #z cases z; #tr' #s' whd in ⊢ (??%? → ?); @is_final_elim
     316  [ #r' #FINAL cases FINAL; #r'' #m' #EXEC whd in EXEC:(??%?);
    285317      destruct (EXEC); @refl
    286318  | #F #EXEC whd in EXEC:(??%?); destruct (EXEC);
     
    347379    cases (exec_step ge s);
    348380  [ #o #k #EXEC whd in EXEC:(??%?); destruct
    349   | #x cases x; #tr #s' whd in ⊢ (??%? → ?); cases (is_final_state s');
    350       #F #EXEC whd in EXEC:(??%?); destruct
     381  | #x cases x; #tr #s' whd in ⊢ (??%? → ?) @is_final_elim
     382      [ #r ] #F #EXEC whd in EXEC:(??%?); destruct
    351383  | //
    352384  ]
     
    363395    cases (exec_step ge s);
    364396    [ #o #k #EXEC whd in EXEC:(??%?); destruct
    365     | #x cases x; #tr1 #s1 whd in ⊢ (??%? → ?); cases (is_final_state s1);
    366         #F #E whd in E:(??%?); destruct; @F
     397    | #x cases x; #tr1 #s1 whd in ⊢ (??%? → ?) @is_final_elim
     398        [ #r ] #F #E whd in E:(??%?); [ destruct | generalize in E:(??(??????%)?) ⊢ ? #e0 #E destruct; @F ]
    367399    | #E whd in E:(??%?); destruct
    368400    ]
Note: See TracChangeset for help on using the changeset viewer.