Ignore:
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:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/MeasurableToStructured.ma

    r2894 r2895  
    5555  do m ← init_mem … (λx.[Init_space x]) p;
    5656  let main ≝ prog_main ?? p in
    57   do b ← opt_to_res ? [MSG MissingSymbol; CTX ? main] (find_symbol … ge main);
     57  do b as Eb ← opt_to_res ? [MSG MissingSymbol; CTX ? main] (find_symbol … ge main);
    5858  do f as Ef ← opt_to_res ? [MSG BadFunction; CTX ? main] (find_funct_ptr … ge b);
    5959  let s ≝ Callstate main f (nil ?) (None ?) (nil ?) m in
    6060  return (mk_RTLabs_ext_state (make_global p) s [b] ?).
    61 % [ @Ef | % ]
     61% [ % assumption | % ]
    6262qed.
    6363
     
    6767#p #s #E
    6868cases (bind_inversion ????? E) -E #m * #E1 #E
    69 cases (bind_inversion ????? E) -E #b * #E2 #E
     69cases (bind_as_inversion ????? E) -E #b * #Eb #E
    7070cases (bind_as_inversion ????? E) -E #f * #Ef #E
    7171whd in ⊢ (??%?); >E1
    72 whd in ⊢ (??%?); >E2
     72whd in ⊢ (??%?); >Eb
    7373whd in ⊢ (??%?); >Ef
    7474whd in E:(??%%) ⊢ (??%?); destruct
     
    8181#p #s #E
    8282cases (bind_inversion ????? E) -E #m * #E1 #E
    83 cases (bind_inversion ????? E) -E #b * #E2 #E
     83cases (bind_inversion ????? E) -E #b * #Eb #E
    8484cases (bind_inversion ????? E) -E #f * #Ef #E
    8585whd in E:(??%%); destruct
    86 %{[b]} % [ % [ @Ef | % ] ]
     86%{[b]} % [ % [ % assumption | % ] ]
    8787whd in ⊢ (??%?); >E1
    88 whd in ⊢ (??%?); >E2
     88whd in ⊢ (??%?); generalize in match (refl ??);
     89>Eb in ⊢ (???% → ??(match % with [_⇒?|_⇒?]?)?); #Eb'
    8990whd in ⊢ (??%?); generalize in match (refl ??);
    9091>Ef in ⊢ (???% → ??(match % with [_⇒?|_⇒?]?)?); #Ef' %
     
    140141lemma will_return_equiv : ∀ge,trace,depth,n,s,s',EX.
    141142  will_return_aux (pcs_to_cs … RTLabs_pcsys ge) depth trace →
    142   will_return ge depth s (make_flat_trace ge n s trace s' EX).
     143  ΣWR:will_return ge depth s (make_flat_trace ge n s trace s' EX).
     144    will_return_end … WR = ?.
     145[2: %{s'} @ft_stop ] (* XXX replace ? above? *)
    143146#ge #trace0 elim trace0
    144147[ #depth #n #s #s' #EX *
     
    169172      [ #EX #_
    170173        lapply (cons_flat_trace … EX) #CFT >(cft_E … CFT)
    171         @wr_base
    172         destruct @CL
     174        %{(wr_base …)}
     175        [ destruct @CL
     176        | cases CFT #ctr #cs #cEV #cEX #cmake whd in ⊢ (??%?);
     177          whd in cEX:(??%%); destruct %
     178        ]
    173179      | * #s3 #tr3 #tl3 #EX *
    174180      ]
    175181    | #depth' whd in ⊢ (?% → ?); #H
    176182      lapply (cons_flat_trace … EX) #CFT >(cft_E … CFT)
    177       @wr_ret
    178       [ destruct @CL
    179       | @IH @H
     183      cases (IH ???? (cft_EX … CFT) H) #WR' #WRe
     184      %{(wr_ret …)}
     185      [ @WR'
     186      | destruct @CL
     187      | @WRe
    180188      ]
    181189    ]
    182190  | #H lapply (cons_flat_trace … EX) #CFT >(cft_E … CFT)
    183     @wr_step [ %2 destruct @CL | @IH @H ]
     191    cases (IH ???? (cft_EX … CFT) H) #WR' #WRe
     192    %{(wr_step …)} [ @WR' | %2 destruct @CL | @WRe ]
    184193  | #H lapply (cons_flat_trace … EX) #CFT >(cft_E … CFT)
    185     @wr_call [ destruct @CL | @IH @H ]
     194    cases (IH ???? (cft_EX … CFT) H) #WR' #WRe
     195    %{(wr_call …)} [ @WR' | destruct @CL | @WRe ]
    186196  | cases (RTLabs_notail … CL)
    187197  | #H lapply (cons_flat_trace … EX) #CFT >(cft_E … CFT)
    188     @wr_step [ %1 destruct @CL | @IH @H ]
    189   ]
    190 ] qed.
     198    cases (IH ???? (cft_EX … CFT) H) #WR' #WRe
     199    %{(wr_step …)} [ @WR' | %1 destruct @CL | @WRe ]
     200  ]
     201] qed.
     202
    191203
    192204lemma extend_RTLabs_eval_statement : ∀ge. ∀s:RTLabs_ext_state ge. ∀tr,s'.
     
    446458] qed.
    447459
     460lemma really_no_label : ∀ge,s,obs.
     461  ¬as_costed (RTLabs_status ge) s →
     462  maybe_label ge s obs = obs.
     463#ge #s #obs
     464whd in ⊢ (?% → ??%?);
     465cases (as_label ??)
     466[ //
     467| #l * #H @⊥ @H % #E destruct
     468] qed.
     469
     470
    448471lemma call_ret_event : ∀ge,s,tr,s',obs.
    449472  step … RTLabs_ext_fullexec ge s = Value ??? 〈tr,s'〉 →
     
    478501] qed.
    479502
     503lemma as_call_cs_callee : ∀ge,s,CL,CL'.
     504  as_call_ident (RTLabs_status ge) «s,CL» = cs_callee (pcs_to_cs RTLabs_ext_pcsys ge) s CL'.
     505#ge * #s #S #M #CL #CL' cases (rtlabs_call_inv … CL) #fn * #fd * #args * #dst * #stk * #m #E
     506destruct %
     507qed.
     508
    480509lemma itot_call : ∀C,cs,s,rem,cs',trace.
    481510  ∀CL:match cs_classify C s with [ cl_call ⇒ True | _ ⇒ False ].
     
    491520qed.
    492521
    493 (* WIP
    494 lemma as_call_cs_callee : ∀ge,s,CL,CL'.
    495   as_call_ident (RTLabs_status ge) «s,CL» = cs_callee (pcs_to_cs RTLabs_ext_pcsys ge) s CL'.
    496 #ge * #s #S #M #CL #CL' cases (rtlabs_call_inv … CL) #fn * #fd * #args * #dst * #stk * #m #E
    497 destruct cases S in M CL' ⊢ %; [ * ] #fn' #S' * #M1 #M' #CL'
    498 whd in ⊢ (??%%); cases (symbol_for_block ??)
    499 
     522lemma itot_step : ∀ge,cs,s,tr,s',rem,cs',obs.
     523  as_classifier (RTLabs_status ge) s cl_other →
     524  step … RTLabs_ext_pcsys ge s = Value ??? 〈tr,s'〉 →
     525  intensional_trace_of_trace (pcs_to_cs … RTLabs_ext_pcsys ge) cs (〈s,tr〉::rem) = 〈cs',obs〉 →
     526  ∃obs'.
     527    obs = (intensional_events_of_events tr) @ obs' ∧
     528    intensional_trace_of_trace (pcs_to_cs … RTLabs_ext_pcsys ge) cs rem = 〈cs',obs'〉.
     529#ge #cs #s #tr #s' #rem #cs #obs #CL #EX
     530whd in ⊢ (??%? → ?); generalize in match (cs_callee ??) in ⊢ (% → ?);
     531whd in CL; change with (cs_classify (pcs_to_cs … RTLabs_ext_pcsys ge) ?) in CL:(??%?);
     532>CL #name whd in ⊢ (??%? → ?);
     533cases (intensional_trace_of_trace ???) #cs'' #trace'' #E whd in E:(??%?); destruct
     534%{trace''} /2/
     535qed.
    500536
    501537(* observables_trace_label_label emits the cost label for the first step of the
     
    527563  @(eq_obs_tal … EX ITOT)
    528564| cases tal
    529   [ #s1 #s2 #ST * #CL #CS #EX
     565  [ #s1 #s2 #ST #CL0 #CS #EX cases CL0 #CL
    530566    cases (exec_steps_S … EX) #_ * #tr * #s2' * #trace2 * * #E1 #ST' #EX
    531567    whd in EX:(??%?); destruct
     
    555591    cases (eq_obs_tlr … EX ITOT')
    556592    #OBS' #E4 <E4 %
    557     [ >E3 <OBS' whd in ⊢ (??%?);
    558 
    559    
    560    
    561 
    562 ] qed.
    563 *)
    564 
     593    [ >E3 <OBS' whd in ⊢ (??%?); <(as_call_cs_callee … CL) %
     594    | %
     595    ]
     596  | #s1 #s2 #s3 #ST #CL #tlr #EX #ITOT @⊥ @(RTLabs_notail … CL)
     597  | #ends #s1 #s2 #s3 #s4 #ST #CL #AF #tlr #CS #tal' #EX
     598    cases (exec_steps_S … EX) #_ * #tr * #s2' * #trace0 * * #E1 >E1 #ST' #EX
     599    cases (call_ret_event … ST')
     600    [ #E2 #E3 >E2 >E3 | skip | %1 @CL ] #ITOT
     601    cases (itot_call … ITOT) [2: change with (cs_classify (pcs_to_cs RTLabs_ext_pcsys ge) ? = ?) in CL; >CL % ]
     602    #obs' * #E4 #ITOT'
     603    <(as_exec_eq_step … ST ST') in EX; #EX
     604    cases (exec_steps_split … EX) #trace1 * #trace2 * #s2'' * * #EX1 #EX2 #E
     605    >E in ITOT'; #ITOT' cases (int_trace_split … ITOT') #cs1 * #t1' * #t2' * * #ITOT1 #ITOT2 #Eobs
     606    lapply (eq_end_tlr … EX1) #E5 <E5 in EX1; #EX1
     607    cases (eq_obs_tlr … EX1 ITOT1) #ITOT1' #CS_CH <CS_CH in ITOT2 EX2; <E5 #ITOT2 #EX2
     608    cases (eq_obs_tal … EX2 ITOT2) #ITOT2' #CS_CH' %
     609    [ >E4 whd in ⊢ (??%?);
     610      <(as_call_cs_callee … CL) in ITOT1' ⊢ %; #ITOT1' >ITOT1'
     611      >(really_no_label … CS) in ITOT2'; #ITOT2' >ITOT2'
     612      <Eobs %
     613    | @CS_CH'
     614    ]
     615  | #ends #s1 #s2 #s3 #ST #tal' #CL #CS #EX
     616    cases (exec_steps_S … EX) #_ * #tr * #s2' * #trace0 * * #E1 >E1 #ST' #EX
     617    #ITOT  cases (itot_step … CL ST' ITOT) #obs' * #E >E #ITOT'
     618    <(as_exec_eq_step … ST ST') in EX; #EX
     619    cases (eq_obs_tal … EX ITOT')
     620    >(really_no_label … CS) #OBS' #CS_CH
     621    >(step_cost_event … ST') <OBS'
     622    % [ % | @CS_CH ]
     623  ]
     624] qed.
     625
     626
     627(* TODO move *)
     628lemma make_flat_trace_length : ∀ge,n,s1,trace,s2,EX.
     629  length_flat_trace io_out io_in ge s1 (make_flat_trace ge n s1 trace s2 EX) = n.
     630#ge #n0 elim n0
     631[ #s1 #trace #s2 #EX %
     632| #n #IH #s1 #trace #s2 #EX
     633  cases (exec_steps_S … EX) #_ * #tr * #s' * #tl * * #E1 #E2 #E3 destruct
     634  cases (cons_flat_trace ?????? EX)
     635  #tr'' #s'' #ST'' #EX'' #E >E whd in ⊢ (??%?); @eq_f @IH
     636] qed.
     637
     638
     639lemma cost_state_is_in_function : ∀ge,s,S,M.
     640  RTLabs_cost (mk_RTLabs_ext_state ge s S M) →
     641  ∃fn,S',id. S = fn::S' ∧ symbol_for_block ? ge fn = Some ? id.
     642#ge *
     643[ #f #fs #m * [*] #fn #S' * #FFP #M #_
     644  %{fn} %{S'} %{(symbol_of_function_block' … FFP)}
     645  % [ % | @symbol_of_function_block_ok [ >FFP % #E destruct | % ] ]
     646| #fid #fn #args #ret #fs #m #S #M *
     647| #rv #rr #fs #m #S #M *
     648| #r #S #M *
     649] qed.
    565650
    566651
     
    594679cases (initial_states_OK' … INIT) #S * #M #INIT'
    595680cases (extend_RTLabs_exec_steps ?? (mk_RTLabs_ext_state (make_global p) s0 S M) … EXEC1)
    596 #prefix'' * #S1 * #M1 letin s1' ≝ (mk_RTLabs_ext_state ? s1 S1 M1) #EXEC1'
     681#prefix'' * #S1 * #M1
     682lapply (label_to_return_state_labelled … LABEL_TO_RETURN EXEC2) #CS1
     683lapply (cost_state_is_in_function ge s1 S1 M1 CS1) * #fnb * #S1' * #fn * #ES1 #FN destruct
     684letin s1' ≝ (mk_RTLabs_ext_state ? s1 (fnb::S1') M1) #EXEC1'
     685cases (will_return_equiv … EXEC2 RETURNS) #RETURNS' #RETURNS_END
    597686lapply (make_label_return' ge 0 s1' (make_flat_trace ????? EXEC2) ????)
    598 [ @will_return_equiv assumption
    599 | @(label_to_return_state_labelled … LABEL_TO_RETURN EXEC2)
     687[ @RETURNS'
     688| @CS1
    600689| @(well_cost_labelled_exec_steps … EXEC1)
    601690  [ assumption
     
    603692  ]
    604693| @WCLge
    605 | * #s2' #rem #_ #tlr #LEN #STACK #_
    606 %{s1'} %{s2'} % [2: %{tlr}
     694| * #s2' #rem #_ #tlr #LEN #STACK whd in ⊢ (% → ?); whd in ⊢ (??%? → ?);
     695>RETURNS_END #E destruct
     696%{s1'} %{s2'} %{fn} %{tlr}
    607697% [ % [ %
    608698  [ whd in ⊢ (??%?);
     
    618708    ]
    619709 ]|
    620  ]|
     710 ]| cut (length_tlr … tlr = n)
     711    [ lapply (make_flat_trace_length ????? EXEC2) <LEN
     712      <plus_n_O @(λx.x) ]
     713    #LEN' <LEN' in EXEC2; #EXEC2
     714    cases (extend_RTLabs_exec_steps ?? s1' … EXEC2) #interesting'''
     715    lapply (eq_obs_tlr ????????? EXEC2)
    621716  ]
    622717]]
    623718
    624 
Note: See TracChangeset for help on using the changeset viewer.