# Changeset 1244

Ignore:
Timestamp:
Sep 21, 2011, 6:08:50 PM (8 years ago)
Message:

Sort out Clight semantics equivalence proof for new SmallstepExec?.

Location:
src/Clight
Files:
4 edited

Unmodified
Removed
• ## src/Clight/Cexec.ma

 r1231 axiom MainMissing : String. let rec make_global (p:clight_program) : genv ≝ globalenv Genv ?? (fst ??) p. definition make_global : clight_program → genv ≝ λp. globalenv Genv ?? (fst ??) p. let rec make_initial_state (p:clight_program) : res state ≝
• ## src/Clight/CexecComplete.ma

 r1058 theorem the_initial_state: ∀p,s. initial_state p s → ∃ge. yields ? (make_initial_state p) 〈ge,s〉. #p #s cases p; #fns #main #globs #H ∀p,s. initial_state p s → yields ? (make_initial_state p) s. #p #s cases p; #globs #fns #main #H inversion H; #b #f #ge #m #e1 #e2 #e3 #e4 #e5 %{ge} whd in ⊢ (??%?); >e1 #b #f #ge #m #e1 #e2 #e3 #e4 #e5 whd in ⊢ (??%?); >e2 whd in ⊢ (??%?); change in e1:(??%?) with (make_global (mk_program ?? globs fns main)) >e1 >e3 whd in ⊢ (??%?);
• ## src/Clight/CexecEquiv.ma

 r1216 ] qed. lemma is_final_elim': ∀s.∀P:option int → Type[0]. lemma is_final_elim': ∀ge,s.∀P:option int → Type[0]. (∀r. final_state s r → P (Some ? r)) → ((¬∃r.final_state s r) → P (None ?)) → P (is_final io_out io_in clight_fullexec s). @is_final_elim qed. P (is_final io_out io_in clight_fullexec ge s). #ge @is_final_elim qed. lemma exec_e_step: ∀ge,x,tr,s,e. whd in ⊢ (? → ? → ?(match % with [_ ⇒ ? | _ ⇒ ?])? → ?) cases (make_initial_state p) [ #gs cases gs; #ge #s #INITIAL' #INITIAL whd in INITIAL ⊢ (?%? → ?); cases INITIAL; #Ege #INITIAL'' [ #s #INITIAL' #INITIAL whd in INITIAL ⊢ (?%? → ?); >exec_inf_aux_unfold whd in ⊢ (?%? → ?) @is_final_elim' [ #r #F @False_ind @(absurd ?? (initial_state_not_final … INITIAL'')) @(absurd ?? (initial_state_not_final … INITIAL)) %{r} @F | #NOTFINAL whd in ⊢ (?%? → ?); cases e; cases (se_inv … EXEC0); *; #E1 #E2 Ege #Ege' >(?:ge' = ge) [ 2: destruct (Ege') skip (INITIAL Ege EXEC0 EXEC'); // ] #ge #Ege inversion MATCHES; [ #s0 #e1 #tr1 #r #m #TERM #EXEC #BEHAVES E1 in TERM #TERM @(program_terminates (mk_transrel … step) ?? ge s) [ 2: @INITIAL'' | 3: @(terminates_sound … TERM EXEC') [ 2: @INITIAL | 3:
• ## src/Clight/CexecSound.ma

 r1224 qed. lemma make_initial_state_sound : ∀p. P_res ? (λgs.globalenv Genv ?? (fst ??) p = OK ? (\fst gs) ∧ initial_state p (\snd gs)) (make_initial_state p). lemma make_initial_state_sound : ∀p. P_res ? (initial_state p) (make_initial_state p). #p cases p; #fns #main #vars whd in ⊢ (???%); @bind_OK #ge #Ege @bind_OK #m #Em @opt_bind_OK #x cases x; #sp #b #esb @opt_bind_OK #f #ef whd; % [ whd in ⊢ (???(??%)) @Ege | @(initial_state_intro … Ege Em esb ef) ] @(initial_state_intro … Em esb ef) @refl qed.
Note: See TracChangeset for help on using the changeset viewer.