(* Show that measurable subtraces are preserved in the front-end. *) include "common/Measurable.ma". definition pnormal_state : ∀C:preclassified_system. ∀g. state … C g → bool ≝ λC,g,s. match pcs_classify C g s with [ cl_other ⇒ true | cl_jump ⇒ true | _ ⇒ false ]. lemma pnormal_state_inv : ∀C,g,s. pnormal_state C g s → pcs_classify C g s = cl_other ∨ pcs_classify C g s = cl_jump. #C #g #s whd in ⊢ (?% → ?); cases (pcs_classify C g s) /2/ * qed. lemma normal_state_p : ∀C,g,s. pnormal_state C g s = normal_state (pcs_to_cs C g) s. // qed. (* A record giving the languages and simulation results necessary to show that measurability is preserved. Note: as we're interested in measurable subtraces, we don't have to worry about the execution "going wrong." *) record meas_sim : Type[2] ≝ { ms_C1 : preclassified_system; ms_C2 : preclassified_system; ms_compiled : program … ms_C1 → program … ms_C2 → Prop; ms_inv : ? → ? → Type[0]; ms_stack : ∀g1,g2. ms_inv g1 g2 → (ident → nat); ms_rel : ∀g1,g2. ∀INV:ms_inv g1 g2. state … ms_C1 g1 → state … ms_C2 g2 → Prop; ms_rel_normal : ∀g1,g2,INV,s1,s2. ms_rel g1 g2 INV s1 s2 → pnormal_state ms_C1 g1 s1 = pnormal_state ms_C2 g2 s2; ms_rel_labelled : ∀g1,g2,INV,s1,s2. ms_rel g1 g2 INV s1 s2 → pcs_labelled ms_C1 g1 s1 = pcs_labelled ms_C2 g2 s2; (* FIXME: this is almost certainly too strong if the step from s1 "disappears" in s2. *) ms_rel_classify : ∀g1,g2,INV,s1,s2. ms_rel g1 g2 INV s1 s2 → pcs_classify ms_C1 g1 s1 = pcs_classify ms_C2 g2 s2; ms_rel_callee : ∀g1,g2,INV,s1,s2. ms_rel g1 g2 INV s1 s2 → ∀H,H'. pcs_callee ms_C1 g1 s1 H = pcs_callee ms_C2 g2 s2 H'; (* These hold in (at least) the languages of interest for measurable subtraces *) ms_labelled_normal_1 : ∀g1,s1. pcs_labelled ms_C1 g1 s1 → pnormal_state ms_C1 g1 s1; ms_labelled_normal_2 : ∀g2,s2. pcs_labelled ms_C2 g2 s2 → pnormal_state ms_C2 g2 s2; ms_notailcalls : ∀g1,s1. pcs_classify ms_C1 g1 s1 ≠ cl_tailcall; (* Measure on source states; only needed for showing preservation of non-termination. Should not be necessary for showing that the measurable traces are preserved. *) ms_measure1 : ∀g1. state … ms_C1 g1 → nat; sim_normal : ∀g1,g2. ∀INV:ms_inv g1 g2. ∀s1,s1'. ms_rel g1 g2 INV s1 s1' → pnormal_state ms_C1 g1 s1 → ¬ pcs_labelled ms_C1 g1 s1 → ∀s2,tr. step … (pcs_exec ms_C1) g1 s1 = Value … 〈tr,s2〉 → ∃m. after_n_steps m … (pcs_exec ms_C2) g2 s1' (λs.pnormal_state ms_C2 g2 s) (λtr',s2'. tr = tr' ∧ ms_rel g1 g2 INV s2 s2' ∧ (m = 0 → lt (ms_measure1 g1 s2) (ms_measure1 g1 s1)) ); (* Naughty code without a cost label will end up being rejected, but we don't have local information about that. *) sim_call_nolabel : ∀g1,g2. ∀INV:ms_inv g1 g2. ∀s1,s1'. ms_rel g1 g2 INV s1 s1' → pcs_classify ms_C1 g1 s1 = cl_call → ¬ pcs_labelled ms_C1 g1 s1 → ∀s2,tr. step … (pcs_exec ms_C1) g1 s1 = Value … 〈tr,s2〉 → ¬ pcs_labelled ms_C1 g1 s2 → ∃m. after_n_steps (S m) … (pcs_exec ms_C2) g2 s1' (λs.pnormal_state ms_C2 g2 s) (λtr',s2'. tr = tr' ∧ ms_rel g1 g2 INV s2 s2' ); (* Note that extra steps are introduced in the front-end to perform variable saves on entry. If there's a cost label (and there ought to be!) then we move it forward, so have to include it in the simulation. Unfortunately that's a little messy. *) sim_call_label : ∀g1,g2. ∀INV:ms_inv g1 g2. ∀s1,s1'. ms_rel g1 g2 INV s1 s1' → pcs_classify ms_C1 g1 s1 = cl_call → ¬ pcs_labelled ms_C1 g1 s1 → ∀s2,tr2,s3,tr3. step … (pcs_exec ms_C1) g1 s1 = Value … 〈tr2,s2〉 → pcs_labelled ms_C1 g1 s2 → step … (pcs_exec ms_C1) g1 s2 = Value … 〈tr3,s3〉 → ∃m. after_n_steps 1 … (pcs_exec ms_C2) g2 s1' (λs.pnormal_state ms_C2 g2 s) (λtr',s2'. tr2 = tr' ∧ bool_to_Prop (pcs_labelled ms_C2 g2 s2') ∧ (after_n_steps m … (pcs_exec ms_C2) g2 s2' (λs.pnormal_state ms_C2 g2 s) (λtr'',s3'. tr'' = tr3 ∧ ms_rel g1 g2 INV s3 s3')) ); sim_return : ∀g1,g2. ∀INV:ms_inv g1 g2. ∀s1,s1'. ms_rel g1 g2 INV s1 s1' → pcs_classify ms_C1 g1 s1 = cl_return → ¬ pcs_labelled ms_C1 g1 s1 → (* NB: calls and returns don't emit timing cost labels; otherwise we would have to worry about whether the cost labels seen at the final return of the measured trace might appear in the target in subsequent steps that are *after* the new measurable subtrace. Also note that extra steps are introduced in the front-end: to perform variable saves on entry and to write back the result *after* exit. The latter do not get included in the measurable subtrace because it stops at the return, and they are the caller's responsibility. *) ∀s2,tr. step … (pcs_exec ms_C1) g1 s1 = Value … 〈tr,s2〉 → ∃m. tr = E0 ∧ after_n_steps (S m) … (pcs_exec ms_C2) g2 s1' (λs.pnormal_state ms_C2 g2 s) (λtr',s2'. E0 = tr' ∧ ms_rel g1 g2 INV s2 s2' ); sim_cost : ∀g1,g2. ∀INV:ms_inv g1 g2. ∀s1,s1',s2,tr. ms_rel g1 g2 INV s1 s1' → pcs_labelled ms_C1 g1 s1 → step … (pcs_exec ms_C1) g1 s1 = Value … 〈tr,s2〉 → after_n_steps 1 … (pcs_exec ms_C2) g2 s1' (λs.true) (λtr',s2'. tr = tr' ∧ ms_rel g1 g2 INV s2 s2' ); sim_init : ∀p1,p2,s. ms_compiled p1 p2 → make_initial_state ?? ms_C1 p1 = OK ? s → ∃s'. make_initial_state ?? ms_C2 p2 = OK ? s' ∧ ∃INV. ms_rel ?? INV s s' }. (* lemma stack_normal_step : ∀C:preclassified_system. ∀g,s1,trace,s2,stack,current. exec_steps 1 io_out io_in C g s1 = OK ? 〈trace,s2〉 → pnormal_state C g s1 → stack_after (pcs_to_cs C g stack) current trace = current. #C #g #s1 #trace #s2 #stack #current #EXEC cases (exec_steps_S … EXEC) #NF * #tr * #s' * #tl * * #Etr #STEP #EXEC' whd in EXEC':(??%?); destruct #N whd in ⊢ (??%?); generalize in match (cs_stack ??); whd in match (cs_classify ??); cases (pnormal_state_inv … N) #CL >CL #f % qed. lemma max_stack_normal_step : ∀C:preclassified_system. ∀g,s1,trace,s2,stack,current. exec_steps 1 io_out io_in C g s1 = OK ? 〈trace,s2〉 → pnormal_state C g s1 → max_stack (pcs_to_cs C g stack) current trace = current. #C #g #s1 #trace #s2 #stack #current #EXEC cases (exec_steps_S … EXEC) #NF * #tr * #s' * #tl * * #Etr #STEP #EXEC' whd in EXEC':(??%?); destruct #N whd in ⊢ (??%?); generalize in match (cs_stack ??); whd in match (cs_classify ??); cases (pnormal_state_inv … N) #CL >CL #f % qed. lemma exec_split : ∀C:preclassified_system.∀g,m,s1,trace,sf. exec_steps m io_out io_in (pcs_exec … C) g s1 = OK ? 〈trace,sf〉 → ¬pcs_labelled C g s1 → pcs_labelled C g sf → ∀inv. (∀s. bool_to_Prop (inv s) → ¬pcs_labelled C g s) → ∀n,P. after_n_steps n io_out io_in (pcs_exec … C) g s1 inv P → ∃p,trace1,s2,trace2. exec_steps n io_out io_in (pcs_exec … C) g s1 = OK ? 〈trace1,s2〉 ∧ P (gather_trace … trace1) s2 ∧ exec_steps p io_out io_in (pcs_exec … C) g s2 = OK ? 〈trace2,sf〉 ∧ m = n + p. #C #g #m elim m -m [ #s1 #trace #sf #EXEC whd in EXEC:(??%?); destruct #NCS #CS @⊥ @(absurd … CS) @Prop_notb @NCS | #m #IH #s1 #trace #sf #EXEC1 #NCS1 #CS2 #inv #H * [ #P #AFTER %{(S m)} %{[ ]} %{s1} %{trace} % [ % [ % [ % | @AFTER ] | @EXEC1 ]| % ] | #n #P #AFTER cases (exec_steps_S … EXEC1) #NF1 * #tr1 * #s2 * #tl * * #Etrace #STEP #EXEC2 cases (after_1_of_n_steps … AFTER) #tr1' * #s2' * * * #NF1' #STEP' #INV2 #AFTER2 >STEP in STEP'; #E destruct cases (IH … EXEC2 … AFTER2) [ #p * #trace1 * #s2 * #trace2 * * * #EXEC2' #P2 #EXEC2 #E %{p} % [2: %{s2} %{trace2} % [ % [ % [ @(exec_steps_join 1 … EXEC2') [2: whd in ⊢ (??%?); >NF1 in ⊢ (??%?); >STEP in ⊢ (??%?); % | skip ] | @P2 ]| @EXEC2 ]| >E % ] | skip ] | @H assumption | assumption | assumption ] ] ] qed. lemma exec_split1 : ∀C:preclassified_system.∀g,m,s1,trace,sf. exec_steps (S m) io_out io_in (pcs_exec … C) g s1 = OK ? 〈trace,sf〉 → ∀P,inv. after_n_steps 1 io_out io_in (pcs_exec … C) g s1 inv P → ∃trace1,s2,trace2. exec_steps 1 io_out io_in (pcs_exec … C) g s1 = OK ? 〈trace1,s2〉 ∧ P (gather_trace … trace1) s2 ∧ exec_steps m io_out io_in (pcs_exec … C) g s2 = OK ? 〈trace2,sf〉. #C #g #m #s1 #trace #sf #EXEC1 #P #inv #AFTER1 cases (exec_steps_S … EXEC1) #NF1 * #tr * #s2 * #tl * * #E1 destruct #STEP #EXEC2 %{[〈s1,tr〉]} %{s2} %{tl} % [ % [ whd in ⊢ (??%?); >NF1 >STEP % | whd in AFTER1; >NF1 in AFTER1; >STEP normalize cases (inv s2) // * ]| // ] qed. *) (* XXX do I need to do the max_stack reasoning here? perhaps just by preserving observables? *) lemma exec_steps_1_trace : ∀O,I,fx,g,s,trace,s'. exec_steps 1 O I fx g s = OK ? 〈trace,s'〉 → ∃tr. trace = [〈s,tr〉]. #O #I #fx #g #s #trace #s' #EXEC cases (exec_steps_S … EXEC) #nf * #tr * #s'' * #tl * * #E1 #STEP #EXEC' whd in EXEC':(??%%); destruct %{tr} % qed. lemma all_1 : ∀A.∀P:A → bool.∀x. P x = all A P [x]. #A #P #x whd in ⊢ (???%); cases (P x) // qed. lemma prefix_preserved : ∀MS:meas_sim. ∀g,g'. ∀INV:ms_inv MS g g'. ∀s1,s1'. ms_rel MS g g' INV s1 s1' → ∀m,prefix,sf. exec_steps m … (pcs_exec … (ms_C1 MS)) g s1 = OK ? 〈prefix,sf〉 → pcs_labelled (ms_C1 MS) g sf → (* Needed to ensure we can get back into the relation after a call *) (∃ex,sx. exec_steps 1 … (pcs_exec … (ms_C1 MS)) g sf = OK ? 〈ex,sx〉) → ∃m',prefix',sf'. exec_steps m' … (pcs_exec … (ms_C2 MS)) g' s1' = OK ? 〈prefix',sf'〉 ∧ bool_to_Prop (pcs_labelled (ms_C2 MS) g' sf') ∧ intensional_trace_of_trace (pcs_to_cs (ms_C1 MS) g) [ ] prefix = intensional_trace_of_trace (pcs_to_cs (ms_C2 MS) g') [ ] prefix' ∧ (* We may need to make extra steps to get back into the relation. In particular, the Clight to Cminor stage adds stores to the stack after the function call, but must preserve the position of the cost label at the head of the function, so we may need to move past these stores. *) ∃r,r',ex,ex',sr,sr'. exec_steps r … (pcs_exec … (ms_C1 MS)) g sf = OK … 〈ex,sr〉 ∧ bool_to_Prop (all … (λst.pnormal_state (ms_C1 MS) g (\fst st)) ex) ∧ exec_steps r' … (pcs_exec … (ms_C2 MS)) g' sf' = OK … 〈ex',sr'〉 ∧ bool_to_Prop (all … (λst.pnormal_state (ms_C2 MS) g' (\fst st)) ex') ∧ (∀cs. intensional_trace_of_trace (pcs_to_cs (ms_C1 MS) g) cs ex = intensional_trace_of_trace (pcs_to_cs (ms_C2 MS) g') cs ex') ∧ ms_rel MS g g' INV sr sr'. * #C1 #C2 #compiled #inv #stack #rel #rel_normal #rel_labelled #rel_classify #rel_callee #labelled_normal1 #labelled_normal2 #no_tailcalls #measure1 #sim_normal #sim_call_nolabel #sim_call_label #sim_return #sim_cost #sim_init #g #g' #INV #s1 #s1' #REL #m0 generalize in match s1' in REL ⊢ %; generalize in match s1; -s1 -s1' generalize in match [ ]; (* current call stack *) @(nat_elim1 m0) * [ #_ #current_stack #s1 #s1' #REL #prefix #sf #EXEC whd in EXEC:(??%?); destruct #CSf #_ %{0} %{[]} %{s1'} % [ % [ % [ // | <(rel_labelled … REL) // ] | // ] | %{0} %{0} %{[ ]} %{[ ]} %{sf} %{s1'} /6/ ] | #m #IH #current_stack #s1 #s1' #REL #prefix #sf #EXEC #CSf #EXTRA_STEP cases (exec_steps_S … EXEC) #NF1 * #tr1 * #s2 * #trace2 * * #E1 #STEP1 #EXEC2 cases (true_or_false_Prop … (pcs_labelled … s1)) [ #CS lapply (sim_cost … REL CS STEP1) #AFTER1' cases (after_n_exec_steps … AFTER1') #prefix' * #s2' * * #EXEC1' #_ * #Etrace #R2 cut (pnormal_state C1 g s1) [ @labelled_normal1 assumption ] #N1 cut (pnormal_state C2 g' s1') [ @labelled_normal2 <(rel_labelled … REL) assumption ] #N1' cases (IH m ? current_stack … R2 … EXEC2 CSf EXTRA_STEP) [2: // ] #m'' * #prefix'' * #sf'' * * * #EXEC'' #CS'' #OBS'' #R'' %{(1+m'')} %{(prefix'@prefix'')} %{sf''} % [ % [ % [ @(exec_steps_join … EXEC1') @EXEC'' | @CS'' ]| destruct @(build_eq_trace (pcs_to_cs C1 g) (pcs_to_cs C2 g')) // cases (exec_steps_1_trace … EXEC1') #tr1' #E destruct NORMAL @INV ] | @OBS'' ] ]| @R'' ] | #CALLRET cut (pcs_classify C1 g s1 = cl_call ∨ pcs_classify C1 g s1 = cl_return) [ whd in CALLRET:(?%); whd in match (pnormal_state ???) in CALLRET; lapply (no_tailcalls … s1) cases (pcs_classify … s1) in CALLRET ⊢ %; [ 1,3: #_ #_ /2/ | *: normalize * #H #H' try cases (H I) cases H' #H'' cases (H'' (refl ??)) ] ] * #CL [ cases (true_or_false_Prop … (pcs_labelled … s2)) [ #CS2 (* Can we execute another step now, or shall we wait for later? *) cases m in IH EXEC2; [ #_ (* Nope, use extra step to get back into relation *) #EXEC2 whd in EXEC2:(??%%); destruct cases EXTRA_STEP #trx * #sx #EXTRA -EXTRA_STEP cases (exec_steps_S … EXTRA) #NFf * #trx' * #sx' * #tlx * * #Ex #EXTRA_STEP #EX' whd in EX':(??%?); destruct cases (sim_call_label … REL … CL (notb_Prop … NCS) … STEP1 CS2 EXTRA_STEP) #m' #AFTER1' cases (after_n_exec_steps … AFTER1') #prefix1' * #s2' * * #EXEC1' #INV1 * * #Etrace #CS2' #AFTER2' cases (after_n_exec_steps … AFTER2') #prefix2' * #s3' * * #EXEC2' #INV2 * #Etrace2 #R3 %{1} %{prefix1'} %{s2'} % [ % [ % [ @EXEC1' | @CS2' ]| destruct cases (exec_steps_S … EXEC1') #NF1' * #tr1' * #s2' * #prefix2 * * #E #STEP1' #EXEC2' destruct <(append_nil … (?::prefix2)) in ⊢ (???%); @(build_call_trace (pcs_to_cs C1 g) (pcs_to_cs C2 g')) [ whd in match (cs_classify ??); >CL % | whd in match (cs_classify ??); <(rel_classify … REL) >CL % | @INV1 | % | @(rel_callee … REL) ] ]| %{1} %{m'} %{[〈sf,trx'〉]} %{prefix2'} %{sx} %{s3'} cut (all ? (λst.pnormal_state C2 g' (\fst st)) prefix2') [ cases prefix2' in EXEC2' INV2 ⊢ %; [ // | * #sp #trp #tlp #EXEC2' #INV2 whd in ⊢ (?%); <(exec_steps_first … EXEC2') >labelled_normal2 // ] ] #Np2' % [ % [ % [ % [ % [ @EXTRA | whd in ⊢ (?%); >labelled_normal1 // ]| @EXEC2' ]| @Np2' ]| #cs <(append_nil … prefix2') CL %] cases (IH m1 ? next_stack … R3 … EXEC3 CSf EXTRA_STEP) [2: // ] #m'' * #prefix'' * #sf'' * * * #EXEC'' #CSf'' #OBS'' #R'' %{(S m' + m'')} %{(prefix1'@prefix2'@prefix'')} %{sf''} % [ % [ % [ @(exec_steps_join … EXEC1') @(exec_steps_join … EXEC2') @EXEC'' | @CSf'' ]| destruct cases (exec_steps_S … EXEC1') #NF1' * #tr1' * #s2'' * #prefix2'' * * #E #STEP1' #EXEC2'' whd in EXEC2'':(??%%); destruct @(build_call_trace (pcs_to_cs C1 g) (pcs_to_cs C2 g')) [ whd in match (cs_classify ??); >CL % | whd in match (cs_classify ??); <(rel_classify … REL) >CL % | % | @(build_eq_trace (pcs_to_cs C1 g) (pcs_to_cs C2 g')) [ labelled_normal2 // ] | assumption ] | @(rel_callee … REL) ] ]| @R'' ] ] | #NCS2 cases (sim_call_nolabel … REL … (notb_Prop … NCS) … STEP1) [2: >CL % | 3: @notb_Prop @NCS2 ] #m' #AFTER1' cases (after_n_exec_steps … AFTER1') #prefix' * #s2' * * #EXEC1' #INV * #Etrace #R2 letin next_stack ≝ ((pcs_callee C1 g s1 ?)::current_stack) [2: >CL %] cases (IH m ? next_stack … R2 … EXEC2 CSf EXTRA_STEP) [2: // ] #m'' * #prefix'' * #sf'' * * * #EXEC'' #CSf'' #OBS'' #R'' %{(S m' + m'')} %{(prefix'@prefix'')} %{sf''} % [ % [ % [ @(exec_steps_join … EXEC1') @EXEC'' | @CSf'' ]| destruct cases (exec_steps_S … EXEC1') #NF1' * #tr1' * #s2' * #prefix2 * * #E #STEP1' #EXEC2' destruct @(build_call_trace (pcs_to_cs C1 g) (pcs_to_cs C2 g')) [ whd in match (cs_classify ??); >CL % | whd in match (cs_classify ??); <(rel_classify … REL) >CL % | @INV | assumption | @(rel_callee … REL) ] ]| @R'' ] ] | cases (sim_return … REL … (notb_Prop … NCS) … STEP1) [2: >CL %] #m' * #Etr #AFTER1' cases (after_n_exec_steps … AFTER1') #prefix' * #s2' * * #EXEC1' #INV * #Etrace #R2 letin next_stack ≝ (tail … current_stack) cases (IH m ? next_stack … R2 … EXEC2 CSf EXTRA_STEP) [2: //] #m'' * #prefix'' * #sf'' * * * #EXEC'' #CSf'' #OBS'' #R'' %{(S m' + m'')} %{(prefix'@prefix'')} %{sf''} % [ % [ % [ @(exec_steps_join … EXEC1') @EXEC'' | @CSf'' ]| destruct cases (exec_steps_S … EXEC1') #NF1' * #tr1' * #s2' * #prefix2 * * #E #STEP1' #EXEC2' destruct >Etrace @(build_return_trace (pcs_to_cs C1 g) (pcs_to_cs C2 g')) [ whd in match (cs_classify ??); >CL % | whd in match (cs_classify ??); <(rel_classify … REL) >CL % | @INV | assumption ] ]| @R'' ] ] ] ] ] qed. definition ends_at_return : ∀C:preclassified_system. ∀g. list (state … C g × trace) → Prop ≝ λC,g,x. ∃x',tr2,s2. x = x'@[〈s2,tr2〉] ∧ pcs_classify C g s2 = cl_return. lemma ends_at_return_append : ∀C,g,t1,t2. ends_at_return C g t2 → ends_at_return C g (t1@t2). #C #g #t1 #t2 * #x * #tr * #s * #E >E #CL %{(t1@x)} %{tr} %{s} % /2/ qed. lemma will_return_aux_normal : ∀C,depth,t1,t2. all … (λstr. normal_state C (\fst str)) t1 → will_return_aux C depth (t1@t2) = will_return_aux C depth t2. #C #depth #t1 #t2 elim t1 [ #_ % | * #s #tr #tl #IH #N cases (andb_Prop_true … N) #N1 #Ntl whd in ⊢ (??%?); cases (normal_state_inv … N1) #CL >CL @IH @Ntl ] qed. lemma measurable_subtrace_preserved : ∀MS:meas_sim. ∀g,g'. ∀INV:ms_inv MS g g'. ∀s1,s1',depth,callstack. ms_rel MS g g' INV s1 s1' → let C ≝ pcs_to_cs (ms_C1 MS) g in let C' ≝ pcs_to_cs (ms_C2 MS) g' in ∀m,interesting,sf. exec_steps m … (pcs_exec … (ms_C1 MS)) g s1 = OK ? 〈interesting,sf〉 → ends_at_return (ms_C1 MS) g interesting → will_return_aux C depth interesting → ∃m',interesting',sf'. exec_steps m' … (pcs_exec … (ms_C2 MS)) g' s1' = OK ? 〈interesting',sf'〉 ∧ (* The obs trace equality almost gives this, but doesn't ensure the cost/return are exactly at the ends *) ends_at_return (ms_C2 MS) g' interesting' ∧ bool_to_Prop (will_return_aux C' depth interesting') ∧ intensional_trace_of_trace C callstack interesting = intensional_trace_of_trace C' callstack interesting'. (* Seems a shame to leave this out "∧ ms_rel MS g g' INV sf sf'", but it isn't true if the final return step is expanded into the caller, e.g., in Clight → Cminor we added an instruction to callers if they need to store the result in memory. This extra step doesn't form part of the measurable trace, so the end is no longer in the relation. ☹ *) * #C1 #C2 #compiled #inv #stack #rel #rel_normal #rel_labelled #rel_classify #rel_callee #labelled_normal1 #labelled_normal2 #no_tailcalls #measure1 #sim_normal #sim_call_nolabel #sim_call_label #sim_return #sim_cost #sim_init #g #g' #INV #s1 #s1' #depth #callstack #REL #m0 generalize in match s1' in REL ⊢ %; generalize in match s1; -s1 -s1' generalize in match callstack; generalize in match depth; -callstack -depth @(nat_elim1 m0) * [ #_ (* "fake" base case - we can never have zero steps *) #depth #current_stack #s1 #s1' #REL #interesting #sf #EXEC whd in EXEC:(??%?); destruct * * [2: #x1 #x2] * #x3 * #x4 * #x5 normalize in x5; destruct | #m #IH #depth #current_stack #s1 #s1' #REL #prefix #sf #EXEC #END #RETURNS cases (exec_steps_S … EXEC) #NF1 * #tr1 * #s2 * #trace2 * * #E1 #STEP1 #EXEC2 cases (true_or_false_Prop … (pcs_labelled … s1)) [ #CS lapply (sim_cost … REL CS STEP1) #AFTER1' cases (after_n_exec_steps … AFTER1') #interesting' * #s2' * * #EXEC1' #_ * #Etrace #R2 cut (pnormal_state C1 g s1) [ @labelled_normal1 assumption ] #N1 cut (pnormal_state C2 g' s1') [ @labelled_normal2 <(rel_labelled … REL) assumption ] #N1' cases (IH m ? depth current_stack … R2 … EXEC2 ??) [ 2: // | (* End must be later, and still a return *) 3: destruct cases END * [ * #trE * #sE * #E whd in E:(???%); destruct #CL cases (pnormal_state_inv … N1) >CL #E destruct | #h #t * #trE * #sE * #E whd in E:(???%); destruct #CL %{t} %{trE} %{sE} /2/ ] | 4: destruct whd in RETURNS:(?%); whd in match (cs_classify ??) in RETURNS; cases (pnormal_state_inv … N1) #CL >CL in RETURNS; #RETURNS @RETURNS ] #m'' * #interesting'' * #sf'' * * * #EXEC'' #ENDS'' #RETURNS'' #OBS'' %{(1+m'')} %{(interesting'@interesting'')} %{sf''} % [ % [ % [ @(exec_steps_join … EXEC1') @EXEC'' | @ends_at_return_append assumption ]| cases (exec_steps_1_trace … EXEC1') #tr1' #E destruct whd in ⊢ (?%); whd in match (cs_classify ??); <(rel_classify … REL) cases (pnormal_state_inv … N1) #CL >CL @RETURNS'' ]| destruct @(build_eq_trace (pcs_to_cs C1 g) (pcs_to_cs C2 g')) // cases (exec_steps_1_trace … EXEC1') #tr1' #E destruct CL #E destruct | #h #t * #trE * #sE * #E whd in E:(???%); destruct #CL %{t} %{trE} %{sE} /2/ ] | 4: destruct whd in RETURNS:(?%); whd in match (cs_classify ??) in RETURNS; cases (pnormal_state_inv … NORMAL) #CL >CL in RETURNS; #RETURNS @RETURNS ] #m'' * #interesting'' * #sf'' * * * #EXEC'' #ENDS'' #RETURNS'' #OBS'' %{(n'+m'')} %{(interesting'@interesting'')} %{sf''} % [ % [ % [ @(exec_steps_join … EXEC1') @EXEC'' | @ends_at_return_append assumption ]| >will_return_aux_normal [ @RETURNS'' | cases n' in EXEC1'; [ #EXEC >(lenght_to_nil (*sic*) … interesting') // >(exec_steps_length … EXEC) % | #n'' #EXEC cases (exec_steps_S … EXEC) #_ * #tr1' * #s2' * #tl * * #E #STEP1' #EXEC2' destruct @andb_Prop [ NORMAL @INV ] | @OBS'' ] ] | #CALLRET cases trace2 in E1 EXEC2; (* For a return we might hit the end - this is the real base case. *) [ #E1 #EXEC2 destruct cases END #tl * #tr * #s1x * #E1 #CL cases tl in E1; [2: #h * [2: #h2 #t] #E normalize in E; destruct ] #E1 normalize in E1; destruct cases (sim_return … REL … (notb_Prop … NCS) … STEP1) [2: >CL %] #m' * #Etr #AFTER1' destruct cases (after_1_of_n_steps … AFTER1') #tr1' * #s2' * * * #NF1' #STEP1' #_ #AFTER2' cut (tr1' = E0) [ cases (after_n_exec_steps … AFTER2') #trace * #sf' * * #_ #_ * #H #_ cases (Eapp_E0_inv … (sym_eq … H)) // ] #E1 destruct %{1} %{[〈s1',E0〉]} %{s2'} % [ % [ % [ whd in ⊢ (??%?); >NF1' >STEP1' whd in ⊢ (??%?); % | %{[ ]} %{E0} %{s1'} %{(refl ??)} <(rel_classify … REL) assumption ]| whd in RETURNS:(?%) ⊢ (?%); whd in match (cs_classify ??) in RETURNS; whd in match (cs_classify ??); <(rel_classify … REL) >CL in RETURNS ⊢ %; whd in ⊢ (?% → ?%); cases depth [ // | #d * ] ]| <(append_nil … [〈s1',E0〉]) change with (gather_trace … [〈s1',E0〉]) in match E0 in ⊢ (??%?); @(build_return_trace (pcs_to_cs C1 g) (pcs_to_cs C2 g')) [ @CL | whd in ⊢ (??%?); <(rel_classify … REL) @CL | % | % ] ] ] (* Not at the end *) * #s2x #tr2 #trace3 #E1 #EXEC2 cut (pcs_classify C1 g s1 = cl_call ∨ pcs_classify C1 g s1 = cl_return) [ whd in CALLRET:(?%); whd in match (pnormal_state ???) in CALLRET; lapply (no_tailcalls … s1) cases (pcs_classify … s1) in CALLRET ⊢ %; [ 1,3: #_ #_ /2/ | *: normalize * #H #H' try cases (H I) cases H' #H'' cases (H'' (refl ??)) ] ] * #CL [ cases (true_or_false_Prop … (pcs_labelled … s2)) [ #CS2 (* We can't stop here *) cases m in IH EXEC2; [ #_ #EXEC2 whd in EXEC2:(??%%); destruct ] #m1 #IH #EXEC2 cases (exec_steps_S … EXEC2) #NF2 * #tr3 * #s3 * #tl3 * * #Etrace2 #STEP2 #EXEC3 cases (sim_call_label … REL … CL (notb_Prop … NCS) … STEP1 CS2 STEP2) #m' #AFTER1' cases (after_n_exec_steps … AFTER1') #interesting1' * #s2' * * #EXEC1' #INV1 * * #Etrace' #CS2' #AFTER2' cases (after_n_exec_steps … AFTER2') #interesting2' * #s3' * * #EXEC2' #INV2 * #Etrace2' #R3 letin next_stack ≝ ((pcs_callee C1 g s1 ?)::current_stack) [2: >CL %] letin next_depth ≝ (S depth) cut (pnormal_state C1 g s2) [ @labelled_normal1 assumption ] #N2 cases (IH m1 ? next_depth next_stack … R3 … EXEC3 ??) [ 2: // | (* End must be later, and still a return *) 3: destruct cases END * [ * #trE * #sE * #E whd in E:(???%); destruct | *: #h1 * [ * #trE * #sE * #E normalize in E:(???%); destruct #CL cases (pnormal_state_inv … N2) >CL #E destruct | #h2 #t * #trE * #sE * #E normalize in E:(???%); destruct #CL %{t} %{trE} %{sE} /2/ ] ] | 4: destruct whd in RETURNS:(?%); whd in match (cs_classify ??) in RETURNS; >CL in RETURNS; whd in ⊢ (?% → ?); cases (pnormal_state_inv … N2) #CL2 whd in match (cs_classify ??); >CL2 // ] #m'' * #interesting'' * #sf'' * * * #EXEC'' #ENDS'' #RETURNS'' #OBS'' %{(S m' + m'')} %{(interesting1'@interesting2'@interesting'')} %{sf''} % [ % [ % [ @(exec_steps_join … EXEC1') @(exec_steps_join … EXEC2') @EXEC'' | @ends_at_return_append @ends_at_return_append assumption ]| cases (exec_steps_S … EXEC1') #NF1' * #tr1' * #s2' * #trace2' * * #E2 #STEP1' #EXEC2'' destruct whd in ⊢ (?%); whd in match (cs_classify ??); <(rel_classify … REL) >CL whd in ⊢ (?%); whd in INV1:(?(???%)); >will_return_aux_normal [2: @INV1 ] >will_return_aux_normal [ // | cases interesting2' in EXEC2' INV2 ⊢ %; [ // | * #s2'' #tr2'' #tl2'' #E2'' <(exec_steps_first … E2'') #TL whd in ⊢ (?%); (labelled_normal2 … CS2') @TL ] ] ]| destruct cases (exec_steps_S … EXEC1') #NF1' * #tr1' * #s2' * #prefix2 * * #E #STEP1' #EXEC2'' destruct @(build_call_trace (pcs_to_cs C1 g) (pcs_to_cs C2 g')) [ whd in match (cs_classify ??); >CL % | whd in match (cs_classify ??); <(rel_classify … REL) >CL % | @INV1 | @(build_eq_trace (pcs_to_cs C1 g) (pcs_to_cs C2 g')) (* Repeats bits of proof above, could compress *) [ labelled_normal2 // ] | assumption ] | @(rel_callee … REL) ] ] | #NCS2 cases (sim_call_nolabel … REL … (notb_Prop … NCS) … STEP1) [2: >CL % | 3: @notb_Prop @NCS2 ] #m' #AFTER1' cases (after_n_exec_steps … AFTER1') #interesting' * #s2' * * #EXEC1' #INV * #Etrace #R2 letin next_stack ≝ ((pcs_callee C1 g s1 ?)::current_stack) [2: >CL %] letin next_depth ≝ (S depth) cases (IH m ? next_depth next_stack … R2 … EXEC2 ??) [ 2: // | (* End must be later, and still a return *) 3: destruct cases END * [ * #trE * #sE * #E whd in E:(???%); destruct | *: #h #t * #trE * #sE * #E whd in E:(???%); destruct #CL %{t} %{trE} %{sE} /2/ ] | 4: destruct whd in RETURNS:(?%); whd in match (cs_classify ??) in RETURNS; >CL in RETURNS; // ] #m'' * #interesting'' * #sf'' * * * #EXEC'' #ENDS'' #RETURNS'' #OBS'' %{(S m' + m'')} %{(interesting'@interesting'')} %{sf''} % [ % [ % [ @(exec_steps_join … EXEC1') @EXEC'' | @ends_at_return_append assumption ]| cases (exec_steps_S … EXEC1') #NF1' * #tr1' * #s2' * #trace2' * * #E2 #STEP1' #EXEC2' destruct whd in ⊢ (?%); whd in match (cs_classify ??); <(rel_classify … REL) >CL whd in ⊢ (?%); >will_return_aux_normal // ]| destruct cases (exec_steps_S … EXEC1') #NF1' * #tr1' * #s2' * #prefix2 * * #E #STEP1' #EXEC2' destruct @(build_call_trace (pcs_to_cs C1 g) (pcs_to_cs C2 g')) [ whd in match (cs_classify ??); >CL % | whd in match (cs_classify ??); <(rel_classify … REL) >CL % | @INV | assumption | @(rel_callee … REL) ] ] ] | cases (sim_return … REL … (notb_Prop … NCS) … STEP1) [2: >CL %] #m' * #Etr #AFTER1' cases (after_n_exec_steps … AFTER1') #interesting' * #s2' * * #EXEC1' #INV * #Etrace #R2 letin next_stack ≝ (tail … current_stack) letin next_depth ≝ (pred depth) cases (IH m ? next_depth next_stack … R2 … EXEC2 ??) [ 2: // | (* End must be later, and still a return *) 3: destruct cases END * [ * #trE * #sE * #E whd in E:(???%); destruct | *: #h #t * #trE * #sE * #E whd in E:(???%); destruct #CL %{t} %{trE} %{sE} /2/ ] | 4: destruct whd in RETURNS:(?%); whd in match (cs_classify ??) in RETURNS; >CL in RETURNS; whd in ⊢ (?% → ?); whd in match next_depth; cases depth [ * | #d' // ] ] #m'' * #interesting'' * #sf'' * * * #EXEC'' #ENDS'' #RETURNS'' #OBS'' %{(S m' + m'')} %{(interesting'@interesting'')} %{sf''} % [ % [ % [ @(exec_steps_join … EXEC1') @EXEC'' | @ends_at_return_append assumption ]| cases (exec_steps_S … EXEC1') #NF1' * #tr1' * #s2' * #trace2' * * #E2 #STEP1' #EXEC2' destruct whd in RETURNS:(?%) ⊢ (?%); whd in match (cs_classify ??) in RETURNS ⊢ %; <(rel_classify … REL) in RETURNS ⊢ %; >CL whd in ⊢ (?% → ?%); whd in match next_depth in RETURNS''; cases depth in RETURNS'' ⊢ %; [ #_ * ] #depth' #RETURNS'' #_ whd in ⊢ (?%); >will_return_aux_normal [ @RETURNS'' | @INV ] ]| destruct cases (exec_steps_S … EXEC1') #NF1' * #tr1' * #s2' * #prefix2 * * #E #STEP1' #EXEC2' destruct >Etrace @(build_return_trace (pcs_to_cs C1 g) (pcs_to_cs C2 g')) [ whd in match (cs_classify ??); >CL % | whd in match (cs_classify ??); <(rel_classify … REL) >CL % | @INV | assumption ] ] ] ] qed. lemma label_to_ret_inv : ∀C,m,g,s,trace,s'. exec_steps m … (pcs_exec … C) g s = OK ? 〈trace,s'〉 → trace_is_label_to_return (pcs_to_cs … C g) trace → bool_to_Prop (pcs_labelled C g s) ∧ ends_at_return C g trace. #C #m #g #s #trace #s' #EXEC * #tr * #s1 * #tl * #tr2 * #s2 * * #E #CS #CL destruct >(exec_steps_first … EXEC) % [ @CS | %{(〈s1,tr〉::tl)} %{tr2} %{s2} %{(refl ??)} @CL ] qed. lemma build_label_to_ret : ∀C,m,g,s,trace,s'. (∀s. pcs_labelled C g s → pnormal_state C g s) → exec_steps m … (pcs_exec … C) g s = OK ? 〈trace,s'〉 → pcs_labelled C g s → ends_at_return C g trace → trace_is_label_to_return (pcs_to_cs … C g) trace. #C #m #g #s #trace #s' #LABELLED_NORMAL #EXEC #CS * #trace' * #tr2 * #s2 * #E #CL destruct cases trace' in EXEC ⊢ %; [ #EXEC >(exec_steps_first … EXEC) in CS; #CS cases (pnormal_state_inv … (LABELLED_NORMAL … CS)) >CL #E destruct | * #s1 #tr1 #trace1 #EXEC %{tr1} %{s1} %{trace1} %{tr2} %{s2} % [ % [ % | <(exec_steps_first … EXEC) @CS ] | @CL ] ] qed. (* TODO: move*) lemma plus_split : ∀x,y:nat. ∃z. x = y + z ∨ y = x + z. #x0 elim x0 [ #y %{y} %2 % | #x #IH * [ %{(S x)} %1 % | #y cases (IH y) #z * [ #H %{z} %1 >H // | #H %{z} %2 >H // ] ] ] qed. lemma all_append : ∀A,p,l1,l2. all A p (l1@l2) → all A p l1 ∧ all A p l2. #A #p #l1 elim l1 [ // | #h #t #IH #l2 whd in ⊢ (?% → ?(?%?)); cases (p h) // @IH ] qed. lemma ends_at_return_normal : ∀C,g,t1,t2. ends_at_return C g (t1@t2) → all … (λst. pnormal_state C g (\fst st)) t1 → ends_at_return C g t2. #C #g #t1 elim t1 [ // | * #s #tr #tl #IH #t2 * #tr1 * #tr2 * #s2 * cases tr1 [ #E normalize in E; destruct #CL whd in ⊢ (?% → ?); lapply (pnormal_state_inv … s2) cases (pnormal_state … s2) [ #H cases (H I) >CL #E' destruct | #_ * ] | * #s' #tr' #tl' #E whd in E:(??%%); destruct #CL #ALL @IH [ %{tl'} %{tr2} %{s2} >e0 % // | whd in ALL:(?%); cases (pnormal_state … s') in ALL; [ // | * ] ] ] ] qed. theorem measured_subtrace_preserved : ∀MS:meas_sim. ∀p1,p2,m,n,stack_cost,max. ms_compiled MS p1 p2 → measurable (ms_C1 MS) p1 m n stack_cost max → ∃m',n'. measurable (ms_C2 MS) p2 m' n' stack_cost max ∧ observables (ms_C1 MS) p1 m n = observables (ms_C2 MS) p2 m' n'. #MS #p1 #p2 #m #n #stack_cost #max #compiled * #s0 * #prefix * #s1 * #interesting * #s2 whd in ⊢ (? → ??(λ_.??(λ_.(?%(??%%))))); letin g ≝ (make_global … (pcs_exec … ) p1) letin g' ≝ (make_global … (pcs_exec … ) p2) letin C ≝ (pcs_to_cs ? g) letin C' ≝ (pcs_to_cs ? g') * * * * * #INIT #EXEC0 #EXEC1 #TLR #RETURNS #MAX cases (sim_init … compiled INIT) #s0' * #INIT' * #INV #R0 cases (label_to_ret_inv … EXEC1 TLR) #CS1 #ENDS cases (prefix_preserved MS g g' INV … R0 … EXEC0 CS1) (* Need an extra step from the source in case we end up at a label after a function call. *) [2: cases n in EXEC1; [ #E whd in E:(??%?); destruct cases RETURNS | #n1 #EXEC1 cases (exec_steps_split 1 … EXEC1) #ex * #ex2 * #sx * * #EX1 #_ #_ %{ex} %{sx} @EX1 ] ] #m' * #prefix' * #s1' * * * #EXEC0' #CS1' #OBS0 * #r * #r' * #interesting1 * #interesting1' * #sr * #sr' * * * * * #EXECr #Nr #EXECr' #Nr' #OBS1 #R1 (* Show that the extra r steps we need to get back into the relation are a prefix of the measurable subtrace. *) cut (∃nr,interesting2. n = r + nr ∧ exec_steps nr … C g sr = OK … 〈interesting2,s2〉 ∧ interesting = interesting1 @ interesting2) [ cases (plus_split n r) #nr * [ #En %{nr} >En in EXEC1; #EXEC1 cases (exec_steps_split … EXEC1) #interesting1x * #interesting2 * #srx * * #EXEC1x #EXECrx #E >EXECr in EXEC1x; #E1x destruct %{interesting2} % [ % [ % | assumption ] | % ] | #En @⊥ >En in EXECr; #EXECr cases (exec_steps_split … EXECr) #ex1 * #ex2 * #sx * * #EX1 #EXx #E >E in Nr; >EXEC1 in EX1; #E' destruct #Nr cases (andb_Prop_true … (all_append … Nr)) #N1 #N2 cases ENDS #le * #tre * #se * #Ee #CLe destruct cases (andb_Prop_true … (all_append … N1)) #_ whd in ⊢ (?% → ?); lapply (pnormal_state_inv … se) cases (pnormal_state … se) [ #H cases (H I) >CLe #E destruct | #_ * ] ] ] * #nr * #interesting2 * * #En #EXECr2 #Ei destruct whd in RETURNS:(?%); >will_return_aux_normal in RETURNS; [2: @Nr] #RETURNS lapply (ends_at_return_normal … ENDS Nr) #ENDS2 cases (measurable_subtrace_preserved MS … INV … (\fst (intensional_trace_of_trace C [ ] (prefix@interesting1))) R1 … EXECr2 ENDS2 RETURNS) #n' * #interesting' * #s2' * * * #EXEC1' #ENDS' #RETURNS' #OBS' cut (intensional_trace_of_trace C [ ] (prefix@interesting1) = intensional_trace_of_trace C' [ ] (prefix'@interesting1')) [ >int_trace_append' >(int_trace_append' C') int_trace_append' >(int_trace_append' C') will_return_aux_normal [2: @Nr'] @RETURNS' ]| INIT >INIT' whd in ⊢ (??%%); >EXEC0 >EXEC0' whd in ⊢ (??%%); >EXEC1 >EXECr'' whd in ⊢ (??%%); >int_trace_append' in OBS'; int_trace_append' >int_trace_append'