Changeset 1216


Ignore:
Timestamp:
Sep 15, 2011, 3:33:09 PM (8 years ago)
Author:
campbell
Message:

Update Clight semantics equivalence proof to match changes in SmallstepExec?.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/CexecEquiv.ma

    r961 r1216  
    1313
    1414coinductive single_exec_of : execution state io_out io_in → s_execution → Prop ≝
    15 | seo_stop : ∀tr,r,m. single_exec_of (e_stop ??? tr r m) (se_stop tr r m)
     15| seo_stop : ∀tr,r,s. single_exec_of (e_stop ??? tr r s) (se_stop tr r (mem_of_state s))
    1616| seo_step : ∀tr,s,e,se.
    1717    single_exec_of e se →
     
    300300
    301301
    302 lemma e_stop_inv: ∀ge,x,tr,r,m.
    303   exec_inf_aux ?? clight_exec ge x = e_stop ??? tr r m
    304   x = Value ??? 〈tr,Returnstate (Vint I32 r) Kstop m〉.
    305 #ge #x #tr #r #m
     302lemma e_stop_inv: ∀ge,x,tr,r,s.
     303  exec_inf_aux ?? clight_exec ge x = e_stop ??? tr r s
     304  x = Value ??? 〈tr,Returnstate (Vint I32 r) Kstop (mem_of_state s)〉.
     305#ge #x #tr #r #s
    306306>(exec_inf_aux_unfold …) cases x;
    307307[ #o #k #EXEC whd in EXEC:(??%?); destruct;
     
    684684  single_exec_of e1 e2 →
    685685  match e1 with
    686   [ e_stop tr r m ⇒ match e2 with [ se_stop tr' r' m' ⇒ tr = tr' ∧ r = r' ∧ m = m' | _ ⇒ False ]
     686  [ e_stop tr r s ⇒ match e2 with [ se_stop tr' r' m' ⇒ tr = tr' ∧ r = r' ∧ mem_of_state s = m' | _ ⇒ False ]
    687687  | e_step tr s e1' ⇒ match e2 with [ se_step tr' s' e2' ⇒ tr = tr' ∧ s = s' ∧ single_exec_of e1' e2' | _ ⇒ False ]
    688688  | e_wrong _ ⇒ match e2 with [ se_wrong _ ⇒ True | _ ⇒ False ]
     
    691691#e01 #e02 #H
    692692cases H;
    693 [ #tr #r #m whd; % [ % ] //
     693[ #tr #r #s whd; % [ % ] //
    694694| #tr #s #e1' #e2' #H' whd; % [ % ] //
    695695| #msg whd; //
Note: See TracChangeset for help on using the changeset viewer.