# Changeset 1216

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

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

File:
1 edited

Unmodified
Added
Removed
• ## src/Clight/CexecEquiv.ma

 r961 coinductive single_exec_of : execution state io_out io_in → s_execution → Prop ≝ | seo_stop : ∀tr,r,m. single_exec_of (e_stop ??? tr r m) (se_stop tr r m) | seo_stop : ∀tr,r,s. single_exec_of (e_stop ??? tr r s) (se_stop tr r (mem_of_state s)) | seo_step : ∀tr,s,e,se. single_exec_of e se → lemma e_stop_inv: ∀ge,x,tr,r,m. exec_inf_aux ?? clight_exec ge x = e_stop ??? tr r m → x = Value ??? 〈tr,Returnstate (Vint I32 r) Kstop m〉. #ge #x #tr #r #m lemma e_stop_inv: ∀ge,x,tr,r,s. exec_inf_aux ?? clight_exec ge x = e_stop ??? tr r s → x = Value ??? 〈tr,Returnstate (Vint I32 r) Kstop (mem_of_state s)〉. #ge #x #tr #r #s >(exec_inf_aux_unfold …) cases x; [ #o #k #EXEC whd in EXEC:(??%?); destruct; single_exec_of e1 e2 → match e1 with [ e_stop tr r m ⇒ match e2 with [ se_stop tr' r' m' ⇒ tr = tr' ∧ r = r' ∧ m = m' | _ ⇒ False ] [ e_stop tr r s ⇒ match e2 with [ se_stop tr' r' m' ⇒ tr = tr' ∧ r = r' ∧ mem_of_state s = m' | _ ⇒ False ] | e_step tr s e1' ⇒ match e2 with [ se_step tr' s' e2' ⇒ tr = tr' ∧ s = s' ∧ single_exec_of e1' e2' | _ ⇒ False ] | e_wrong _ ⇒ match e2 with [ se_wrong _ ⇒ True | _ ⇒ False ] #e01 #e02 #H cases H; [ #tr #r #m whd; % [ % ] // [ #tr #r #s whd; % [ % ] // | #tr #s #e1' #e2' #H' whd; % [ % ] // | #msg whd; //
Note: See TracChangeset for help on using the changeset viewer.