Changeset 2666


Ignore:
Timestamp:
Feb 14, 2013, 11:49:48 AM (6 years ago)
Author:
piccolo
Message:

bug fixed in blocks.ma

Location:
src
Files:
4 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/ERTL_semantics.ma

    r2604 r2666  
    114114   | ertl_frame_size dst ⇒ ps_reg_store_status dst (BVByte framesize) st
    115115   ]. @hide_prf whd in match newsp; cases sp #ptr #EQ <EQ % qed. 
    116          
    117 definition ERTL_semantics ≝
    118   make_sem_graph_params ERTL
    119   (λF. mk_sem_unserialized_params ??
     116
     117definition ERTL_sem_uns ≝ 
     118λF. mk_sem_unserialized_params ERTL ?
    120119  (* st_pars            ≝ *) ERTL_state
    121120  (* acca_store_        ≝ *) ps_reg_store
     
    142141     λst.return map ?? (hwreg_retrieve (\snd (regs … st))) RegisterRets)
    143142  (* eval_ext_seq       ≝ *) (λgl,ge,stm,id.λ_.eval_ertl_seq F gl ge stm id)
    144   (* pop_frame          ≝ *) (λ_.λ_.λ_.λ_.pop_ra …)).
     143  (* pop_frame          ≝ *) (λ_.λ_.λ_.λ_.pop_ra …).
     144         
     145definition ERTL_semantics ≝
     146  make_sem_graph_params ERTL ERTL_sem_uns.
  • src/ERTLptr/ERTLptr_semantics.ma

    r2604 r2666  
    2626                        ps_reg_store_status r addrh st
    2727   ].
    28    
    29 definition ERTLptr_semantics ≝
    30   make_sem_graph_params ERTLptr
    31   (λF. mk_sem_unserialized_params ??
     28
     29definition ERTLptr_sem_uns ≝
     30λF. mk_sem_unserialized_params ERTLptr ?
    3231  (* st_pars            ≝ *) ERTL_state
    3332  (* acca_store_        ≝ *) ps_reg_store
     
    5453     λst.return map ?? (hwreg_retrieve (\snd (regs … st))) RegisterRets)
    5554  (* eval_ext_seq       ≝ *) (λgl,ge,stm,id.λ_.eval_ertlptr_seq F gl ge stm id)
    56   (* pop_frame          ≝ *) (λ_.λ_.λ_.λ_.pop_ra …)).
     55  (* pop_frame          ≝ *) (λ_.λ_.λ_.λ_.pop_ra …).
     56definition ERTLptr_semantics ≝
     57  make_sem_graph_params ERTLptr ERTLptr_sem_uns.
  • src/ERTLptr/ERTLtoERTLptrOK.ma

    r2663 r2666  
    18781878qed.
    18791879
     1880lemma fetch_internal_function_no_minus_one :
     1881∀F,V,i,p,bl.
     1882  block_id (pi1 … bl) = -1 →
     1883  fetch_internal_function ?
     1884 
     1885  (globalenv (λvars.fundef (F vars)) V i p) bl =
     1886  Error ? [MSG BadFunction].
     1887#F #V #i #p #bl #EQbl whd in match fetch_internal_function;
     1888normalize nodelta >fetch_function_no_minus_one [2: assumption] %
     1889qed.
     1890
    18801891lemma fetch_statement_no_zero :
    18811892∀pars,prog,stack_size,pc.
     
    18871898>fetch_internal_function_no_zero [2: assumption] %
    18881899qed.
     1900
     1901lemma fetch_statement_no_minus_one :
     1902∀pars,prog,stack_size,pc.
     1903block_id(pi1 … (pc_block pc)) = -1 →
     1904fetch_statement pars (prog_var_names … prog)
     1905(ev_genv (mk_prog_params pars prog stack_size)) pc =
     1906Error ? [MSG BadFunction].
     1907#pars #vars #ge #pc #EQpc whd in match fetch_statement; normalize nodelta
     1908>fetch_internal_function_no_minus_one [2: assumption] %
     1909qed.
     1910
     1911
    18891912
    18901913lemma foo :
     
    19181941 luniverse_ok … fn →
    19191942 ∀stmt,nxt.
     1943 ∀P : (state_pc P2_sem) → Prop.
    19201944 (∀pre_Instrs',last_Instrs',dst.
    19211945   ∃st''.∃st'''.∃st''''.
     
    19261950    st'' = (mk_state_pc (mk_prog_params P2_sem trans_prog stack_size)
    19271951     st'''' (pc_of_point P2_sem (pc_block (pc … (sigma_state_pc st))) dst) (last_pop … st)) ∧
    1928     st' = sigma_state_pc st''
     1952    P st'' (*st' = sigma_state_pc st''*)
    19291953    let P2_prog_params ≝ mk_prog_params P2_sem trans_prog stack_size in
    19301954    let P2_globals ≝ globals P2_prog_params in
     
    19431967 (sigma_state_pc st) = return st' →
    19441968 ∃st''. (*CSC: this needs to be linked back again st' = sigma_state_pc ? good st'' ∧*)
     1969 P st'' ∧
    19451970 ∃taf : trace_any_any_free (joint_abstract_status (mk_prog_params P2_sem trans_prog stack_size)) st st''.
    1946  True (* the length of taf is the same of the length of ??? *).
     1971(if taaf_non_empty … taf then True else
     1972(¬as_costed (joint_abstract_status (mk_prog_params P1_sem prog stack_size)) (sigma_state_pc st) ∨
     1973 ¬as_costed (joint_abstract_status (mk_prog_params P1_sem prog stack_size)) st'))
     1974 (* the length of taf is the same of the length of ??? *).
    19471975#P1_unser #P2_unser #P1_sem_unser #P2_sem_unser
    19481976letin P1_sem ≝ (make_sem_graph_params P1_unser P1_sem_unser)
     
    19581986#prog
    19591987letin trans_prog ≝ (transform_program ??? prog (λvarnames. transf_fundef ?? (translate_internal varnames)))
    1960 #stack_size #sigma_state_pc #sigma_state_pc_ok #st #st' #f #fn #fn_universe_ok #stmt #nxt #Hpass
    1961 #EQfetch lapply(fetch_statement_inv … EQfetch) * #EQfn #EQstmt
     1988#stack_size #sigma_state_pc #sigma_state_pc_ok #st #st' #f #fn #fn_universe_ok #stmt #nxt #P
     1989#Hpass #EQfetch lapply(fetch_statement_inv … EQfetch) * #EQfn #EQstmt
    19621990cases
    19631991 (b_graph_translate_ok … (init …) (translate_step …) (translate_fin_step …) … fn_universe_ok)
     
    20252053                      second one to be taken from somewhere *)
    20262054|4: #x cases daemon (* TO BE DONE, EASY *)
    2027 |5: cases daemon (* to be taken in input *) ]
    2028 [2: cases daemon
    2029 | #st'' * #taaf #_ %{st''}
    2030   change with ERTL_uns in match (mk_unserialized_params ???????????????);
     2055|5: cases daemon (* to be taken in input *)
     2056|6: @(λst''.st' = sigma_state_pc ? good st'')
     2057|7: cases daemon
     2058| #st'' * #EQ destruct * change with ERTL_uns in match (mk_unserialized_params ???????????????);
    20312059  change with ERTLptr_uns in match (mk_unserialized_params ???????????????);
    2032   change with ERTL_semantics in match (make_sem_graph_params ??);
    2033   change with ERTLptr_semantics in match (make_sem_graph_params ??);
    2034 
    2035 
     2060  (* change with ERTL_semantics in match (make_sem_graph_params ??);
     2061  change with ERTLptr_semantics in match (make_sem_graph_params ??); *)
     2062#taaf #Htaaf %{st''}
     2063 % [%] cases daemon
     2064 qed.
     2065
     2066lemma lookup_opt_none_transf :
     2067∀prog : ertl_program.
     2068let trans_prog ≝ ertl_to_ertlptr prog in
     2069∀x.lookup_opt
     2070    (fundef
     2071     (joint_closed_internal_function ERTL
     2072      (prog_var_names (joint_function ERTL) ℕ prog))) x
     2073     (functions
     2074       (fundef
     2075        (joint_closed_internal_function ERTL
     2076         (prog_var_names (joint_function ERTL) ℕ prog)))
     2077       (globalenv_noinit (joint_function ERTL) prog)) =None ? →
     2078lookup_opt
     2079    (fundef
     2080     (joint_closed_internal_function ERTLptr
     2081      (prog_var_names (joint_function ERTLptr) ℕ trans_prog))) x
     2082     (functions
     2083       (fundef
     2084        (joint_closed_internal_function ERTLptr
     2085         (prog_var_names (joint_function ERTLptr) ℕ trans_prog)))
     2086       (globalenv_noinit (joint_function ERTLptr) trans_prog)) =None ?.
     2087#prog #x #EQlookup
     2088whd in match ertl_to_ertlptr in ⊢ (??(???(??%))?); whd in match transform_program;
     2089whd in match transf_program; normalize nodelta whd in match globalenv_noinit;
     2090whd in match globalenv; whd in match globalenv_allocmem;
     2091whd in match add_globals; normalize nodelta
     2092cases daemon
     2093qed.
     2094
     2095 
     2096 
     2097lemma fetch_function_none :
     2098∀prog : ertl_program.
     2099let trans_prog ≝ ertl_to_ertlptr prog in
     2100∀bl.
     2101fetch_function
     2102        (fundef
     2103         (joint_closed_internal_function ERTL
     2104          (prog_var_names (joint_function ERTL) ℕ prog)))
     2105        (globalenv_noinit (joint_function ERTL) prog) bl = Error ? [MSG BadFunction] →
     2106fetch_function
     2107        (fundef
     2108         (joint_closed_internal_function ERTLptr
     2109          (prog_var_names (joint_function ERTLptr) ℕ trans_prog)))
     2110        (globalenv_noinit (joint_function ERTLptr) trans_prog) bl = Error ? [MSG BadFunction].
     2111#prog #bl whd in match fetch_function in ⊢ (% → ?); normalize nodelta
     2112<(symbol_for_block_transf … (λn:ℕ.[Init_space n]) prog …
     2113                         (λvars.transf_fundef … (translate_internal …)) bl)
     2114change with (symbol_for_block
     2115              (fundef
     2116                (joint_closed_internal_function ERTLptr
     2117                  (prog_var_names (joint_function ERTLptr) ℕ (ertl_to_ertlptr prog))))
     2118               (globalenv_noinit (joint_function ERTLptr) (ertl_to_ertlptr prog)) bl)
     2119               in match (symbol_for_block ???);
     2120whd in match fetch_function; normalize nodelta cases(symbol_for_block ???) [#_ %]
     2121#id >m_return_bind inversion(find_funct_ptr ???)
     2122[2: #x #_ whd in ⊢ (??%% → ?); #EQ destruct] whd in match find_funct_ptr;
     2123normalize nodelta cases(block_region bl) normalize nodelta [ #_ #_ >m_return_bind %]
     2124cases(block_id bl) normalize nodelta [1,2: [2: #x] #_ #_ >m_return_bind %]
     2125#x whd in match globalenv_noinit; whd in match globalenv; normalize nodelta
     2126whd in match globalenv_allocmem; normalize nodelta #EQlookup
     2127>(lookup_opt_none_transf … EQlookup) #_ %
     2128qed.
     2129
     2130lemma fetch_function_err :
     2131∀F,ge,bl,e. fetch_function F ge bl = Error ? e → e = [MSG BadFunction].
     2132#F #ge #bl #e whd in match fetch_function; normalize nodelta
     2133cases(symbol_for_block ???) [ normalize #EQ destruct %]
     2134#id >m_return_bind cases(find_funct_ptr ???) normalize [2: #x]
     2135#EQ destruct %
     2136qed.
     2137
     2138 
     2139lemma fetch_internal_function_none :
     2140∀ prog : ertl_program.
     2141let trans_prog ≝ ertl_to_ertlptr prog in
     2142∀bl.
     2143fetch_internal_function
     2144   (joint_closed_internal_function ERTL
     2145    (prog_var_names (joint_function ERTL) ℕ prog))
     2146   (globalenv_noinit (joint_function ERTL) prog) bl = Error ? [MSG BadFunction] →
     2147fetch_internal_function
     2148   (joint_closed_internal_function ERTLptr
     2149    (prog_var_names (joint_function ERTLptr) ℕ trans_prog))
     2150   (globalenv_noinit (joint_function ERTLptr) trans_prog) bl = Error ? [MSG BadFunction].
     2151#prog #bl whd in match fetch_internal_function; normalize nodelta
     2152inversion(fetch_function ???)
     2153[2: #err_msg #EQfetch lapply(fetch_function_err … EQfetch) #EQ destruct #_
     2154    >(fetch_function_none … EQfetch) %] * #f * #fn #EQfetch >m_return_bind
     2155normalize nodelta whd in ⊢ (??%? → ?); #EQ destruct
     2156>(fetch_function_transf … (λvars.transf_fundef … (translate_internal …)) … EQfetch)
     2157>m_return_bind %
     2158qed.
     2159 
     2160lemma fetch_internal_function_err :
     2161∀F,ge,bl,e. fetch_internal_function F ge bl = Error ? e → e = [MSG BadFunction].
     2162#F #ge #bl #e whd in match fetch_internal_function; normalize nodelta
     2163inversion(fetch_function ???)
     2164[2: #e #EQf lapply(fetch_function_err … EQf) #EQ destruct whd in ⊢ (??%? → ?);
     2165    #EQ destruct %] * #id * #fn #EQf >m_return_bind normalize nodelta
     2166whd in ⊢ (??%? → ?); #EQ destruct %
     2167qed.
     2168
     2169 
     2170   
     2171 
     2172lemma as_label_ok : ∀ prog : ertl_program.
     2173let trans_prog ≝ ertl_to_ertlptr prog in
     2174∀ good,stack_sizes,st.
     2175as_label (ERTLptr_status trans_prog stack_sizes) st = as_label
     2176(ERTL_status prog stack_sizes) (sigma_state_pc prog good st).
     2177#prog #good #stack_size #st whd in match as_label; normalize nodelta
     2178whd in match (as_pc_of ? ?); whd in match (as_pc_of ? ?);
     2179whd in match sigma_state_pc; normalize nodelta @if_elim
     2180[ @eqZb_elim [2: #_ *] #EQbl * whd in match (as_label_of_pc ??);
     2181  >fetch_statement_no_minus_one [2: assumption] normalize nodelta
     2182  whd in match (as_label_of_pc ??); >fetch_statement_no_zero [2: %] %]
     2183#_ inversion(fetch_internal_function ???)
     2184[2: #e #EQf lapply(fetch_internal_function_err … EQf) #EQ destruct normalize nodelta
     2185    whd in match (as_label_of_pc ??); whd in match fetch_statement; normalize nodelta
     2186    >(fetch_internal_function_none … EQf) whd in ⊢ (??%%);
     2187    >fetch_statement_no_zero [2: %] % ] * #f #fn #EQf normalize nodelta
     2188whd in match (as_label_of_pc ??) in ⊢ (???%); whd in match fetch_statement;
     2189normalize nodelta >EQf >m_return_bind inversion(stmt_at ????) [cases daemon (*to discuss with Paolo*)]
     2190* [ * [ * [ #id | #addr ] #args #dst | #acc_r #lbl | #seq ] #nxt | #fin | *]
     2191#EQstmt_at >m_return_bind normalize nodelta
     2192cases(multi_fetch_ok … (good fn) … EQstmt_at)
     2193#labs * #regs ** #EQlabs #EQregs normalize nodelta whd in match translate_step;
     2194normalize nodelta
     2195[1,3,4: * #step_block * whd in match (bind_new_instantiates ?????);
     2196        cases regs in EQregs; [2,4,6: #r #tl #EQ normalize nodelta *]
     2197        #EQregs normalize nodelta #EQ destruct * #dst *
     2198        whd in match (step_list_in_code ???????); cases labs in EQlabs;
     2199        [2,4,6: #lb #tl #EQ normalize nodelta *] #EQlabs normalize nodelta
     2200        #EQ destruct * #nxt1 * #EQ_s_stmt #EQ destruct
     2201        whd in match (as_label_of_pc ??); whd in match fetch_statement;
     2202        normalize nodelta
     2203        >(fetch_internal_function_transf … (λvars.translate_internal …) … EQf)
     2204        >m_return_bind >EQ_s_stmt >m_return_bind normalize nodelta [1,2: %]
     2205        cases seq
     2206        [#str % | #c % | #H1 % | #H3 % | #x % | #H5 #H6 #H7 #H8 %
     2207        | #H10 #H11 #H12 #H13 #H14 % | #H16 #H17 #H18 % | #H20 #H21 #H22 #H23 %
     2208        | % | % | #H25 #H26 #H27 % | #H29 #H30 #H31 % | #H33 %]
     2209| * #step_block whd in match (bind_new_instantiates ?????);
     2210  cases regs in EQregs; [ #EQ normalize nodelta **] #reg #tl #EQregs
     2211  normalize nodelta whd in match (bind_new_instantiates ?????);
     2212  cases tl in EQregs; [2: #reg1 #tl1 #EQ normalize nodelta **]
     2213  #EQreg normalize nodelta * #EQ destruct * #dst *
     2214  whd in match (step_list_in_code ???????); cases labs in EQlabs;
     2215  [ #_ normalize nodelta *] #lbl #tl #EQlabs normalize nodelta *
     2216  * #nxt1 * #EQ_s_stmt #_ #_ #_ whd in match (as_label_of_pc ??);
     2217  whd in match fetch_statement; normalize nodelta
     2218   >(fetch_internal_function_transf … (λvars.translate_internal …) … EQf)
     2219   >m_return_bind >EQ_s_stmt >m_return_bind normalize nodelta %
     2220| (whd in match translate_fin_step; normalize nodelta) *
     2221  #fin_block * whd in match (bind_new_instantiates ?????); cases regs in EQregs;
     2222  [2: #r #tl #_ normalize nodelta *] #EQregs normalize nodelta #EQ destruct
     2223  * #list_l * #lbl ** #EQ destruct whd in match (step_list_in_code ???????);
     2224  normalize nodelta cases list_l in EQlabs; [2: #lbl1 #tl #_ normalize nodelta *]
     2225  #EQlabs normalize nodelta #EQ destruct whd in match fin_step_in_code;
     2226  normalize nodelta #EQ_s_stmt whd in match (as_label_of_pc ??);
     2227   whd in match fetch_statement; normalize nodelta
     2228   >(fetch_internal_function_transf … (λvars.translate_internal …) … EQf)
     2229   >m_return_bind >EQ_s_stmt >m_return_bind normalize nodelta %
     2230]
     2231qed.
     2232
     2233(*
    20362234#H1 #H2 #H3 *
    20372235
     
    21472345
    21482346
    2149 qed.
     2347qed.*)
    21502348
    21512349lemma ertl_to_ertlptr_ok:
     
    21732371| (*seq*) whd in match joint_classify; normalize nodelta >EQfetch >m_return_bind
    21742372          normalize nodelta cases (eval_seq_no_call_ok ?????????  EQfetch EQeval)
    2175   #st3 * #EQ destruct *  #taf #tafne %{st3} %{taf} >tafne normalize nodelta
    2176   % [% //] whd >as_label_ok [2:assumption] %
     2373          #st3 * #EQ destruct *  #taf #tafne %{st3} %{taf} >tafne normalize nodelta
     2374          % [% //] whd >as_label_ok [2:assumption] %
    21772375
    21782376
  • src/joint/blocks.ma

    r2599 r2666  
    381381  λp,g.λc:codeT p g.λsrc.λB : fin_block p g.λl.λdst : unit.
    382382  ∃hd,tl.l = hd @ [tl] ∧
    383   src ~❨\fst B, l❩~> tl in c ∧ fin_step_in_code … c tl (\snd B).
     383  src ~❨\fst B, hd❩~> tl in c ∧ fin_step_in_code … c tl (\snd B).
    384384
    385385interpretation "step block in code" 'block_in_code c x B l y = (step_block_in_code ?? c x B l y).
Note: See TracChangeset for help on using the changeset viewer.