Changeset 2666
 Timestamp:
 Feb 14, 2013, 11:49:48 AM (7 years ago)
 Location:
 src
 Files:

 4 edited
Legend:
 Unmodified
 Added
 Removed

src/ERTL/ERTL_semantics.ma
r2604 r2666 114 114  ertl_frame_size dst ⇒ ps_reg_store_status dst (BVByte framesize) st 115 115 ]. @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 117 definition ERTL_sem_uns ≝ 118 λF. mk_sem_unserialized_params ERTL ? 120 119 (* st_pars ≝ *) ERTL_state 121 120 (* acca_store_ ≝ *) ps_reg_store … … 142 141 λst.return map ?? (hwreg_retrieve (\snd (regs … st))) RegisterRets) 143 142 (* 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 145 definition ERTL_semantics ≝ 146 make_sem_graph_params ERTL ERTL_sem_uns. 
src/ERTLptr/ERTLptr_semantics.ma
r2604 r2666 26 26 ps_reg_store_status r addrh st 27 27 ]. 28 29 definition ERTLptr_semantics ≝ 30 make_sem_graph_params ERTLptr 31 (λF. mk_sem_unserialized_params ?? 28 29 definition ERTLptr_sem_uns ≝ 30 λF. mk_sem_unserialized_params ERTLptr ? 32 31 (* st_pars ≝ *) ERTL_state 33 32 (* acca_store_ ≝ *) ps_reg_store … … 54 53 λst.return map ?? (hwreg_retrieve (\snd (regs … st))) RegisterRets) 55 54 (* 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 …). 56 definition ERTLptr_semantics ≝ 57 make_sem_graph_params ERTLptr ERTLptr_sem_uns. 
src/ERTLptr/ERTLtoERTLptrOK.ma
r2663 r2666 1878 1878 qed. 1879 1879 1880 lemma 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; 1888 normalize nodelta >fetch_function_no_minus_one [2: assumption] % 1889 qed. 1890 1880 1891 lemma fetch_statement_no_zero : 1881 1892 ∀pars,prog,stack_size,pc. … … 1887 1898 >fetch_internal_function_no_zero [2: assumption] % 1888 1899 qed. 1900 1901 lemma fetch_statement_no_minus_one : 1902 ∀pars,prog,stack_size,pc. 1903 block_id(pi1 … (pc_block pc)) = 1 → 1904 fetch_statement pars (prog_var_names … prog) 1905 (ev_genv (mk_prog_params pars prog stack_size)) pc = 1906 Error ? [MSG BadFunction]. 1907 #pars #vars #ge #pc #EQpc whd in match fetch_statement; normalize nodelta 1908 >fetch_internal_function_no_minus_one [2: assumption] % 1909 qed. 1910 1911 1889 1912 1890 1913 lemma foo : … … 1918 1941 luniverse_ok … fn → 1919 1942 ∀stmt,nxt. 1943 ∀P : (state_pc P2_sem) → Prop. 1920 1944 (∀pre_Instrs',last_Instrs',dst. 1921 1945 ∃st''.∃st'''.∃st''''. … … 1926 1950 st'' = (mk_state_pc (mk_prog_params P2_sem trans_prog stack_size) 1927 1951 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''*) ∧ 1929 1953 let P2_prog_params ≝ mk_prog_params P2_sem trans_prog stack_size in 1930 1954 let P2_globals ≝ globals P2_prog_params in … … 1943 1967 (sigma_state_pc st) = return st' → 1944 1968 ∃st''. (*CSC: this needs to be linked back again st' = sigma_state_pc ? good st'' ∧*) 1969 P st'' ∧ 1945 1970 ∃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 ??? *). 1947 1975 #P1_unser #P2_unser #P1_sem_unser #P2_sem_unser 1948 1976 letin P1_sem ≝ (make_sem_graph_params P1_unser P1_sem_unser) … … 1958 1986 #prog 1959 1987 letin 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 # Hpass1961 # EQfetch lapply(fetch_statement_inv … EQfetch) * #EQfn #EQstmt1988 #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 1962 1990 cases 1963 1991 (b_graph_translate_ok … (init …) (translate_step …) (translate_fin_step …) … fn_universe_ok) … … 2025 2053 second one to be taken from somewhere *) 2026 2054 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 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 ???????????????); 2031 2059 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 2066 lemma lookup_opt_none_transf : 2067 ∀prog : ertl_program. 2068 let 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 ? → 2078 lookup_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 2088 whd in match ertl_to_ertlptr in ⊢ (??(???(??%))?); whd in match transform_program; 2089 whd in match transf_program; normalize nodelta whd in match globalenv_noinit; 2090 whd in match globalenv; whd in match globalenv_allocmem; 2091 whd in match add_globals; normalize nodelta 2092 cases daemon 2093 qed. 2094 2095 2096 2097 lemma fetch_function_none : 2098 ∀prog : ertl_program. 2099 let trans_prog ≝ ertl_to_ertlptr prog in 2100 ∀bl. 2101 fetch_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] → 2106 fetch_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) 2114 change 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 ???); 2120 whd 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; 2123 normalize nodelta cases(block_region bl) normalize nodelta [ #_ #_ >m_return_bind %] 2124 cases(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 2126 whd in match globalenv_allocmem; normalize nodelta #EQlookup 2127 >(lookup_opt_none_transf … EQlookup) #_ % 2128 qed. 2129 2130 lemma 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 2133 cases(symbol_for_block ???) [ normalize #EQ destruct %] 2134 #id >m_return_bind cases(find_funct_ptr ???) normalize [2: #x] 2135 #EQ destruct % 2136 qed. 2137 2138 2139 lemma fetch_internal_function_none : 2140 ∀ prog : ertl_program. 2141 let trans_prog ≝ ertl_to_ertlptr prog in 2142 ∀bl. 2143 fetch_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] → 2147 fetch_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 2152 inversion(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 2155 normalize nodelta whd in ⊢ (??%? → ?); #EQ destruct 2156 >(fetch_function_transf … (λvars.transf_fundef … (translate_internal …)) … EQfetch) 2157 >m_return_bind % 2158 qed. 2159 2160 lemma 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 2163 inversion(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 2166 whd in ⊢ (??%? → ?); #EQ destruct % 2167 qed. 2168 2169 2170 2171 2172 lemma as_label_ok : ∀ prog : ertl_program. 2173 let trans_prog ≝ ertl_to_ertlptr prog in 2174 ∀ good,stack_sizes,st. 2175 as_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 2178 whd in match (as_pc_of ? ?); whd in match (as_pc_of ? ?); 2179 whd 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 2188 whd in match (as_label_of_pc ??) in ⊢ (???%); whd in match fetch_statement; 2189 normalize 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 2192 cases(multi_fetch_ok … (good fn) … EQstmt_at) 2193 #labs * #regs ** #EQlabs #EQregs normalize nodelta whd in match translate_step; 2194 normalize 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 ] 2231 qed. 2232 2233 (* 2036 2234 #H1 #H2 #H3 * 2037 2235 … … 2147 2345 2148 2346 2149 qed. 2347 qed.*) 2150 2348 2151 2349 lemma ertl_to_ertlptr_ok: … … 2173 2371  (*seq*) whd in match joint_classify; normalize nodelta >EQfetch >m_return_bind 2174 2372 normalize nodelta cases (eval_seq_no_call_ok ????????? EQfetch EQeval) 2175 #st3 * #EQ destruct * #taf #tafne %{st3} %{taf} >tafne normalize nodelta2176 % [% //] whd >as_label_ok [2:assumption] %2373 #st3 * #EQ destruct * #taf #tafne %{st3} %{taf} >tafne normalize nodelta 2374 % [% //] whd >as_label_ok [2:assumption] % 2177 2375 2178 2376 
src/joint/blocks.ma
r2599 r2666 381 381 λp,g.λc:codeT p g.λsrc.λB : fin_block p g.λl.λdst : unit. 382 382 ∃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). 384 384 385 385 interpretation "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.