Ignore:
Timestamp:
Apr 5, 2013, 6:04:14 PM (7 years ago)
Author:
tranquil
Message:

preliminary work on closing correctness.ma

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTL/RTL_separate_to_overflow.ma

    r2946 r3096  
    22include "joint/Traces.ma".
    33include "common/stacksize.ma".
     4include "common/StatusSimulation.ma".
     5
     6definition extract_call_ud_from_ft ≝
     7  λS : abstract_status.λs1,s2.λft :flat_trace S s1 s2.
     8  extract_call_ud_from_observables … (ft_observables … ft).
     9
     10definition good_stack_usage_ft :
     11  ∀p, stacksizes.
     12  ∀st1,st2 : joint_status RTL_semantics_separate p stacksizes.
     13  flat_trace … st1 st2 → Prop ≝
     14  λp, stacksizes.λst1,st2 : state_pc RTL_semantics_separate.λft.
     15  ∀m : ℕ.m < 2^16 →
     16  let info ≝ mk_stacksize_info (stack_usage … st1) m in
     17  let info' ≝ update_stacksize_info stacksizes info
     18    (extract_call_ud_from_ft … ft) in
     19  maximum info' < 2^16.
    420
    521definition good_stack_usage_tlr :
     
    4157  maximum info' < 2^16.
    4258
     59axiom RTL_separate_to_overflow_produce_ft_and_tlr :
     60∀stacksizes : ident → option ℕ. (* are hypotheses needed here? *)
     61∀p_in : rtl_program.
     62let S1 ≝ joint_status RTL_semantics_separate p_in stacksizes in
     63let S2 ≝ joint_status RTL_semantics_separate_overflow p_in stacksizes in
     64∀fn.∀st1,st1',st1'' : state_pc RTL_semantics_separate.
     65∀ft1 : flat_trace S1 st1 st1'.
     66∀tlr1 : trace_label_return S1 st1' st1''.
     67good_stack_usage_ft … ft1 →
     68good_stack_usage_tlr … fn tlr1 →
     69∃ft2 : flat_trace S2 st1 st1'.
     70∃tlr2 : trace_label_return S2 st1' st1''.
     71ft_observables … ft1 = ft_observables … ft2 ∧
     72tlr_rel … tlr1 tlr2.
     73
     74(*
    4375axiom RTL_separate_to_overflow_produce_tlr :
    4476∀stacksizes : ident → option ℕ. (* are hypotheses needed here? *)
     
    73105good_stack_usage_tal … curr_id tal →
    74106trace_any_label S2 fl s1 s2.
    75 
    76 
    77 
    78 
     107*)
Note: See TracChangeset for help on using the changeset viewer.