Changeset 2895 for src/RTLabs/MeasurableToStructured.ma

Timestamp:

Mar 16, 2013, 9:08:19 PM (8 years ago)

Author:

campbell

Message:

Match up function id from RTLabs Callstate with shadow stack,
use in observables proof.

File:

• src/RTLabs/MeasurableToStructured.ma (modified) (13 diffs)

src/RTLabs/MeasurableToStructured.ma

@@ -55 +55 @@
   do m ← init_mem … (λx.[Init_space x]) p;
   let main ≝ prog_main ?? p in
-  do b ← opt_to_res ? [MSG MissingSymbol; CTX ? main] (find_symbol … ge main);
+  do b as Eb ← opt_to_res ? [MSG MissingSymbol; CTX ? main] (find_symbol … ge main);
   do f as Ef ← opt_to_res ? [MSG BadFunction; CTX ? main] (find_funct_ptr … ge b);
   let s ≝ Callstate main f (nil ?) (None ?) (nil ?) m in
   return (mk_RTLabs_ext_state (make_global p) s [b] ?).
-% [ @Ef | % ]
+% [ % assumption | % ]
 qed.
 
@@ -67 +67 @@
 #p #s #E
 cases (bind_inversion ????? E) -E #m * #E1 #E
-cases (bind_inversion ????? E) -E #b * #E2 #E
+cases (bind_as_inversion ????? E) -E #b * #Eb #E
 cases (bind_as_inversion ????? E) -E #f * #Ef #E
 whd in ⊢ (??%?); >E1
-whd in ⊢ (??%?); >E2
+whd in ⊢ (??%?); >Eb
 whd in ⊢ (??%?); >Ef
 whd in E:(??%%) ⊢ (??%?); destruct
@@ -81 +81 @@
 #p #s #E
 cases (bind_inversion ????? E) -E #m * #E1 #E
-cases (bind_inversion ????? E) -E #b * #E2 #E
+cases (bind_inversion ????? E) -E #b * #Eb #E
 cases (bind_inversion ????? E) -E #f * #Ef #E
 whd in E:(??%%); destruct
-%{[b]} % [ % [ @Ef | % ] ]
+%{[b]} % [ % [ % assumption | % ] ]
 whd in ⊢ (??%?); >E1
-whd in ⊢ (??%?); >E2
+whd in ⊢ (??%?); generalize in match (refl ??);
+>Eb in ⊢ (???% → ??(match % with [_⇒?|_⇒?]?)?); #Eb' 
 whd in ⊢ (??%?); generalize in match (refl ??);
 >Ef in ⊢ (???% → ??(match % with [_⇒?|_⇒?]?)?); #Ef' %
@@ -140 +141 @@
 lemma will_return_equiv : ∀ge,trace,depth,n,s,s',EX.
   will_return_aux (pcs_to_cs … RTLabs_pcsys ge) depth trace →
-  will_return ge depth s (make_flat_trace ge n s trace s' EX).
+  ΣWR:will_return ge depth s (make_flat_trace ge n s trace s' EX).
+    will_return_end … WR = ?.
+[2: %{s'} @ft_stop ] (* XXX replace ? above? *)
 #ge #trace0 elim trace0
 [ #depth #n #s #s' #EX *
@@ -169 +172 @@
       [ #EX #_ 
         lapply (cons_flat_trace … EX) #CFT >(cft_E … CFT)
-        @wr_base
-        destruct @CL
+        %{(wr_base …)}
+        [ destruct @CL
+        | cases CFT #ctr #cs #cEV #cEX #cmake whd in ⊢ (??%?);
+          whd in cEX:(??%%); destruct %
+        ]
       | * #s3 #tr3 #tl3 #EX *
       ]
     | #depth' whd in ⊢ (?% → ?); #H
       lapply (cons_flat_trace … EX) #CFT >(cft_E … CFT)
-      @wr_ret
-      [ destruct @CL
-      | @IH @H
+      cases (IH ???? (cft_EX … CFT) H) #WR' #WRe
+      %{(wr_ret …)}
+      [ @WR'
+      | destruct @CL
+      | @WRe
       ]
     ]
   | #H lapply (cons_flat_trace … EX) #CFT >(cft_E … CFT)
-    @wr_step [ %2 destruct @CL | @IH @H ]
+    cases (IH ???? (cft_EX … CFT) H) #WR' #WRe
+    %{(wr_step …)} [ @WR' | %2 destruct @CL | @WRe ]
   | #H lapply (cons_flat_trace … EX) #CFT >(cft_E … CFT)
-    @wr_call [ destruct @CL | @IH @H ]
+    cases (IH ???? (cft_EX … CFT) H) #WR' #WRe
+    %{(wr_call …)} [ @WR' | destruct @CL | @WRe ]
   | cases (RTLabs_notail … CL)
   | #H lapply (cons_flat_trace … EX) #CFT >(cft_E … CFT)
-    @wr_step [ %1 destruct @CL | @IH @H ]
-  ]
-] qed.
+    cases (IH ???? (cft_EX … CFT) H) #WR' #WRe
+    %{(wr_step …)} [ @WR' | %1 destruct @CL | @WRe ]
+  ]
+] qed.
+
 
 lemma extend_RTLabs_eval_statement : ∀ge. ∀s:RTLabs_ext_state ge. ∀tr,s'.
@@ -446 +458 @@
 ] qed.
 
+lemma really_no_label : ∀ge,s,obs.
+  ¬as_costed (RTLabs_status ge) s →
+  maybe_label ge s obs = obs.
+#ge #s #obs
+whd in ⊢ (?% → ??%?);
+cases (as_label ??)
+[ //
+| #l * #H @⊥ @H % #E destruct
+] qed.
+
+
 lemma call_ret_event : ∀ge,s,tr,s',obs.
   step … RTLabs_ext_fullexec ge s = Value ??? 〈tr,s'〉 →
@@ -478 +501 @@
 ] qed.
 
+lemma as_call_cs_callee : ∀ge,s,CL,CL'.
+  as_call_ident (RTLabs_status ge) «s,CL» = cs_callee (pcs_to_cs RTLabs_ext_pcsys ge) s CL'.
+#ge * #s #S #M #CL #CL' cases (rtlabs_call_inv … CL) #fn * #fd * #args * #dst * #stk * #m #E
+destruct %
+qed.
+
 lemma itot_call : ∀C,cs,s,rem,cs',trace.
   ∀CL:match cs_classify C s with [ cl_call ⇒ True | _ ⇒ False ].
@@ -491 +520 @@
 qed.
 
-(* WIP
-lemma as_call_cs_callee : ∀ge,s,CL,CL'.
-  as_call_ident (RTLabs_status ge) «s,CL» = cs_callee (pcs_to_cs RTLabs_ext_pcsys ge) s CL'.
-#ge * #s #S #M #CL #CL' cases (rtlabs_call_inv … CL) #fn * #fd * #args * #dst * #stk * #m #E
-destruct cases S in M CL' ⊢ %; [ * ] #fn' #S' * #M1 #M' #CL'
-whd in ⊢ (??%%); cases (symbol_for_block ??)
-
+lemma itot_step : ∀ge,cs,s,tr,s',rem,cs',obs.
+  as_classifier (RTLabs_status ge) s cl_other →
+  step … RTLabs_ext_pcsys ge s = Value ??? 〈tr,s'〉 →
+  intensional_trace_of_trace (pcs_to_cs … RTLabs_ext_pcsys ge) cs (〈s,tr〉::rem) = 〈cs',obs〉 →
+  ∃obs'.
+    obs = (intensional_events_of_events tr) @ obs' ∧
+    intensional_trace_of_trace (pcs_to_cs … RTLabs_ext_pcsys ge) cs rem = 〈cs',obs'〉.
+#ge #cs #s #tr #s' #rem #cs #obs #CL #EX
+whd in ⊢ (??%? → ?); generalize in match (cs_callee ??) in ⊢ (% → ?);
+whd in CL; change with (cs_classify (pcs_to_cs … RTLabs_ext_pcsys ge) ?) in CL:(??%?);
+>CL #name whd in ⊢ (??%? → ?);
+cases (intensional_trace_of_trace ???) #cs'' #trace'' #E whd in E:(??%?); destruct
+%{trace''} /2/
+qed.
 
 (* observables_trace_label_label emits the cost label for the first step of the
@@ -527 +563 @@
   @(eq_obs_tal … EX ITOT)
 | cases tal
-  [ #s1 #s2 #ST * #CL #CS #EX
+  [ #s1 #s2 #ST #CL0 #CS #EX cases CL0 #CL
     cases (exec_steps_S … EX) #_ * #tr * #s2' * #trace2 * * #E1 #ST' #EX
     whd in EX:(??%?); destruct
@@ -555 +591 @@
     cases (eq_obs_tlr … EX ITOT')
     #OBS' #E4 <E4 %
-    [ >E3 <OBS' whd in ⊢ (??%?);
-
-    
-    
-
-] qed.
-*)
-
+    [ >E3 <OBS' whd in ⊢ (??%?); <(as_call_cs_callee … CL) %
+    | %
+    ]
+  | #s1 #s2 #s3 #ST #CL #tlr #EX #ITOT @⊥ @(RTLabs_notail … CL)
+  | #ends #s1 #s2 #s3 #s4 #ST #CL #AF #tlr #CS #tal' #EX
+    cases (exec_steps_S … EX) #_ * #tr * #s2' * #trace0 * * #E1 >E1 #ST' #EX
+    cases (call_ret_event … ST')
+    [ #E2 #E3 >E2 >E3 | skip | %1 @CL ] #ITOT
+    cases (itot_call … ITOT) [2: change with (cs_classify (pcs_to_cs RTLabs_ext_pcsys ge) ? = ?) in CL; >CL % ]
+    #obs' * #E4 #ITOT'
+    <(as_exec_eq_step … ST ST') in EX; #EX
+    cases (exec_steps_split … EX) #trace1 * #trace2 * #s2'' * * #EX1 #EX2 #E
+    >E in ITOT'; #ITOT' cases (int_trace_split … ITOT') #cs1 * #t1' * #t2' * * #ITOT1 #ITOT2 #Eobs
+    lapply (eq_end_tlr … EX1) #E5 <E5 in EX1; #EX1
+    cases (eq_obs_tlr … EX1 ITOT1) #ITOT1' #CS_CH <CS_CH in ITOT2 EX2; <E5 #ITOT2 #EX2
+    cases (eq_obs_tal … EX2 ITOT2) #ITOT2' #CS_CH' %
+    [ >E4 whd in ⊢ (??%?);
+      <(as_call_cs_callee … CL) in ITOT1' ⊢ %; #ITOT1' >ITOT1'
+      >(really_no_label … CS) in ITOT2'; #ITOT2' >ITOT2'
+      <Eobs %
+    | @CS_CH'
+    ]
+  | #ends #s1 #s2 #s3 #ST #tal' #CL #CS #EX
+    cases (exec_steps_S … EX) #_ * #tr * #s2' * #trace0 * * #E1 >E1 #ST' #EX
+    #ITOT  cases (itot_step … CL ST' ITOT) #obs' * #E >E #ITOT'
+    <(as_exec_eq_step … ST ST') in EX; #EX
+    cases (eq_obs_tal … EX ITOT')
+    >(really_no_label … CS) #OBS' #CS_CH
+    >(step_cost_event … ST') <OBS'
+    % [ % | @CS_CH ]
+  ]
+] qed.
+
+
+(* TODO move *)
+lemma make_flat_trace_length : ∀ge,n,s1,trace,s2,EX.
+  length_flat_trace io_out io_in ge s1 (make_flat_trace ge n s1 trace s2 EX) = n.
+#ge #n0 elim n0
+[ #s1 #trace #s2 #EX %
+| #n #IH #s1 #trace #s2 #EX
+  cases (exec_steps_S … EX) #_ * #tr * #s' * #tl * * #E1 #E2 #E3 destruct
+  cases (cons_flat_trace ?????? EX)
+  #tr'' #s'' #ST'' #EX'' #E >E whd in ⊢ (??%?); @eq_f @IH
+] qed.
+
+
+lemma cost_state_is_in_function : ∀ge,s,S,M.
+  RTLabs_cost (mk_RTLabs_ext_state ge s S M) →
+  ∃fn,S',id. S = fn::S' ∧ symbol_for_block ? ge fn = Some ? id.
+#ge *
+[ #f #fs #m * [*] #fn #S' * #FFP #M #_
+  %{fn} %{S'} %{(symbol_of_function_block' … FFP)}
+  % [ % | @symbol_of_function_block_ok [ >FFP % #E destruct | % ] ]
+| #fid #fn #args #ret #fs #m #S #M *
+| #rv #rr #fs #m #S #M *
+| #r #S #M *
+] qed.
 
 
@@ -594 +679 @@
 cases (initial_states_OK' … INIT) #S * #M #INIT'
 cases (extend_RTLabs_exec_steps ?? (mk_RTLabs_ext_state (make_global p) s0 S M) … EXEC1)
-#prefix'' * #S1 * #M1 letin s1' ≝ (mk_RTLabs_ext_state ? s1 S1 M1) #EXEC1'
+#prefix'' * #S1 * #M1
+lapply (label_to_return_state_labelled … LABEL_TO_RETURN EXEC2) #CS1
+lapply (cost_state_is_in_function ge s1 S1 M1 CS1) * #fnb * #S1' * #fn * #ES1 #FN destruct
+letin s1' ≝ (mk_RTLabs_ext_state ? s1 (fnb::S1') M1) #EXEC1'
+cases (will_return_equiv … EXEC2 RETURNS) #RETURNS' #RETURNS_END
 lapply (make_label_return' ge 0 s1' (make_flat_trace ????? EXEC2) ????)
-[ @will_return_equiv assumption
-| @(label_to_return_state_labelled … LABEL_TO_RETURN EXEC2)
+[ @RETURNS'
+| @CS1
 | @(well_cost_labelled_exec_steps … EXEC1)
   [ assumption
@@ -603 +692 @@
   ]
 | @WCLge
-| * #s2' #rem #_ #tlr #LEN #STACK #_
-%{s1'} %{s2'} % [2: %{tlr}
+| * #s2' #rem #_ #tlr #LEN #STACK whd in ⊢ (% → ?); whd in ⊢ (??%? → ?);
+>RETURNS_END #E destruct
+%{s1'} %{s2'} %{fn} %{tlr}
 % [ % [ %
   [ whd in ⊢ (??%?);
@@ -618 +708 @@
     ]
  ]|
- ]|
+ ]| cut (length_tlr … tlr = n)
+    [ lapply (make_flat_trace_length ????? EXEC2) <LEN
+      <plus_n_O @(λx.x) ]
+    #LEN' <LEN' in EXEC2; #EXEC2
+    cases (extend_RTLabs_exec_steps ?? s1' … EXEC2) #interesting'''
+    lapply (eq_obs_tlr ????????? EXEC2)
   ]
 ]]
 
-