1(* 2 * Copyright 2018, Data61, CSIRO (ABN 41 687 119 230) 3 * 4 * SPDX-License-Identifier: BSD-2-Clause 5 *) 6 7open preamble MapProgTheory ml_translatorLib ml_progLib basisFunctionsLib ml_translatorTheory 8 charsetTheory regexpTheory regexp_parserTheory regexp_compilerTheory cfTacticsBaseLib 9 camkesStartTheory; 10 11val _ = temp_delsimps ["NORMEQ_CONV"] 12 13val _ = new_theory "filterProg"; 14 15(*---------------------------------------------------------------------------*) 16(* The regexp wrt. which we're filtering *) 17(* Read from the cmakeConstants SML module which is generated by the *) 18(* build system. *) 19(*---------------------------------------------------------------------------*) 20 21val the_regexp = camkesConstants.filter_regex; 22 23val _ = translation_extends "camkesStart"; 24 25(*---------------------------------------------------------------------------*) 26(* Reuse of some code from regexpLib, so that some intermediate lemmas are *) 27(* kept for use in the proofs of side-condition theorems arising from *) 28(* translation. *) 29(*---------------------------------------------------------------------------*) 30 31val regexp_compilation_results as {certificate, aux, ...} 32 = regexpLib.gen_dfa regexpLib.HOL (Regexp_Type.fromString the_regexp); 33 34val matcher_certificate = save_thm 35 ("matcher_certificate", 36 certificate 37 |> valOf 38 |> CONV_RULE(QUANT_CONV(LHS_CONV (REWRITE_CONV [MAP]))) 39); 40 41(*---------------------------------------------------------------------------*) 42(* Define a named matcher function *) 43(*---------------------------------------------------------------------------*) 44 45val matcher_def = 46 Define `matcher ^(matcher_certificate |> concl |> dest_forall |> fst) = 47 ^(matcher_certificate |> concl |> dest_forall |> snd |> lhs)` 48 49val match_string_def = Define `match_string s = matcher(explode s)` 50 51val language_def = 52 Define `language = 53 ^(matcher_certificate |> concl |> dest_forall |> snd |> rhs |> rator)` 54 55val match_string_eq = Q.prove(`match_string = language o explode`, 56 `!s. match_string s = (language o explode) s` suffices_by metis_tac[] 57 >> rw[match_string_def,language_def,matcher_def,matcher_certificate]); 58 59val IMPLODE_pointless = Q.prove(`!s. IMPLODE s = s`, 60 Induct >> simp[]); 61 62val THE_lift = Q.prove(`!f r. 63 IS_SOME r ==> THE(lift f r) = f(THE r)`, 64 Cases_on `r` >> simp[]); 65 66(*---------------------------------------------------------------------------*) 67(* Translator setup boilerplate *) 68(*---------------------------------------------------------------------------*) 69 70fun def_of_const tm = let 71 val res = dest_thy_const tm handle HOL_ERR _ => 72 failwith ("Unable to translate: " ^ term_to_string tm) 73 val name = (#Name res) 74 fun def_from_thy thy name = 75 DB.fetch thy (name ^ "_def") handle HOL_ERR _ => 76 DB.fetch thy (name ^ "_DEF") handle HOL_ERR _ => 77 DB.fetch thy (name ^ "_thm") handle HOL_ERR _ => 78 DB.fetch thy name 79 val def = def_from_thy (#Thy res) name handle HOL_ERR _ => 80 failwith ("Unable to find definition of " ^ name) 81 in def end 82 83val _ = find_def_for_const := def_of_const; 84 85 86(* TODO: translate balanced_map module separately? *) 87 88val _ = ml_translatorLib.pick_name := 89 let val default = !ml_translatorLib.pick_name in 90 fn c => 91 if same_const c ``balanced_map$member`` then "balanced_map_member" else 92 if same_const c ``balanced_map$empty`` then "balanced_map_empty" else 93 default c 94 end 95 96val spec64 = INST_TYPE[alpha|->``:64``] 97 98val _ = translate matcher_def 99 100val mem_tolist = Q.prove(`MEM (toList l) (MAP toList ll) = MEM l ll`, 101 Induct_on `ll` >> fs[]); 102 103val length_tolist_cancel = Q.prove( 104 `!n. n < LENGTH l ==> LENGTH (EL n (MAP mlvector$toList l)) = length (EL n l)`, 105 Induct_on `l` 106 >> fs[] 107 >> rpt strip_tac 108 >> Cases_on `n` 109 >> fs[mlvectorTheory.length_toList]); 110 111val EL_map_toList = Q.prove(`!n. n < LENGTH l ==> EL n' (EL n (MAP toList l)) = sub (EL n l) n'`, 112 Induct_on `l` 113 >> fs[] 114 >> rpt strip_tac 115 >> Cases_on `n` 116 >> fs[mlvectorTheory.EL_toList]); 117 118val exec_dfa_side_imp = Q.prove( 119 `!finals table n s. 120 good_vec (MAP toList (toList table)) (toList finals) 121 /\ EVERY (��c. MEM (ORD c) ALPHABET) (EXPLODE s) 122 /\ n < length finals 123 ==> exec_dfa_side finals table n s`, 124 Induct_on `s` 125 >- fs[fetch "-" "exec_dfa_side_def"] 126 >> PURE_ONCE_REWRITE_TAC [fetch "-" "exec_dfa_side_def"] 127 >> fs[good_vec_def,mlvectorTheory.length_toList] 128 >> rpt GEN_TAC 129 >> Induct_on `table` 130 >> rpt strip_tac 131 >> fs[sub_def,length_def,mlvectorTheory.toList_thm] 132 >> `MEM (toList (EL n l)) (MAP toList l)` 133 by fs[EL_MEM,mem_tolist,mlvectorTheory.toList_thm] 134 >- metis_tac[mlvectorTheory.length_toList] 135 >> first_x_assum(MATCH_MP_TAC o Q.SPECL [`finals`,`Vector l`, `x1`]) 136 >> rpt strip_tac 137 >> fs[mlvectorTheory.toList_thm, length_def, mem_tolist] 138 >- metis_tac[] 139 >> first_x_assum(ASSUME_TAC o Q.SPECL [`toList (EL n l)`,`ORD h`]) 140 >> first_x_assum(MATCH_MP_TAC o Q.SPECL [`n`,`ORD h`,`x1`]) 141 >> rfs[mlvectorTheory.length_toList,mem_tolist,EL_map_toList,length_tolist_cancel]); 142 143val all_ord_string = Q.prove 144(`EVERY (\c. MEM (ORD c) ALPHABET) s 145 <=> 146 EVERY (\c. ORD c < alphabet_size) s`, 147 simp_tac list_ss [mem_alphabet_iff]); 148 149val good_vec_thm = 150 SIMP_RULE std_ss [dom_Brz_alt_equal] 151 regexp_compilerTheory.compile_regexp_good_vec; 152 153val matcher_side_lem = Q.prove( 154 `!s. matcher_side s <=> T`, 155 rw[fetch "-" "matcher_side_def"] 156 >> match_mp_tac exec_dfa_side_imp 157 >> rw_tac list_ss [mlvectorTheory.toList_thm] 158 >- metis_tac [aux |> valOf,good_vec_thm] 159 >- rw_tac list_ss [all_ord_string,ORD_BOUND,alphabet_size_def] 160 >- EVAL_TAC) 161 |> 162 update_precondition; 163 164val _ = translate match_string_def 165 166(* val _ = translate(word_bit_test |> spec64); *) 167 168(* TODO: this is largely copied from the bootstrap translation 169 can it be properly abstracted out? *) 170local 171 val ths = ml_translatorLib.eq_lemmas(); 172in 173 fun find_equality_type_thm tm = 174 first (can (C match_term tm) o rand o snd o strip_imp o concl) ths 175end 176 177val EqualityType_WORD = find_equality_type_thm``WORD`` 178val no_closures_def = ml_translatorTheory.no_closures_def; 179val LIST_TYPE_def = ml_translatorTheory.LIST_TYPE_def; 180val EqualityType_def = ml_translatorTheory.EqualityType_def; 181val types_match_def = ml_translatorTheory.types_match_def; 182val ctor_same_type_def = semanticPrimitivesTheory.ctor_same_type_def; 183 184Theorem tolist_fromlist_map_cancel: 185 MAP mlvector$toList (MAP fromList ll) = ll 186Proof 187 Induct_on `ll` >> fs[] 188QED 189 190(*---------------------------------------------------------------------------*) 191(* Auxiliary functions to deal with null termination. *) 192(*---------------------------------------------------------------------------*) 193 194val null_index_def = tDefine "null_index" 195 `null_index s n = 196 if n >= strlen s then NONE 197 else if strsub s n = CHR 0 then SOME n 198 else null_index s (SUC n)` 199 (wf_rel_tac `inv_image (measure (��(a,b). SUC a - b)) (strlen ## I)`); 200 201val null_index_ind = fetch "-" "null_index_ind"; 202 203Theorem null_index_le_len: 204 !s n m. null_index s n = SOME m ==> m < strlen s 205Proof 206 ho_match_mp_tac null_index_ind 207 >> rpt strip_tac 208 >> qhdtm_x_assum `null_index` (mp_tac o PURE_ONCE_REWRITE_RULE [null_index_def]) 209 >> rw[] 210QED 211 212Theorem null_index_in_bound: 213 !s n m. null_index s n = SOME m ==> n <= m 214Proof 215 ho_match_mp_tac null_index_ind 216 >> rpt strip_tac 217 >> qhdtm_x_assum `null_index` (mp_tac o PURE_ONCE_REWRITE_RULE [null_index_def]) 218 >> rw[] >> fs[] 219QED 220 221Theorem null_index_null: 222 !s n m. null_index s n = SOME m ==> strsub s m = CHR 0 223Proof 224 ho_match_mp_tac null_index_ind 225 >> rpt strip_tac 226 >> qhdtm_x_assum `null_index` (mp_tac o PURE_ONCE_REWRITE_RULE [null_index_def]) 227 >> rw[] >> fs[] 228QED 229 230Theorem null_index_no_null: 231 !s n m. null_index s n = SOME m ==> EVERY ($~ o $= (CHR 0)) (TAKE (m-n) (DROP n (explode s))) 232Proof 233 ho_match_mp_tac null_index_ind 234 >> rpt strip_tac 235 >> qhdtm_x_assum `null_index` (mp_tac o PURE_ONCE_REWRITE_RULE [null_index_def]) 236 >> rw[] 237 >> first_x_assum drule >> rpt(disch_then drule) 238 >> strip_tac 239 >> imp_res_tac null_index_le_len 240 >> imp_res_tac null_index_in_bound 241 >> qmatch_goalsub_abbrev_tac `EVERY _ (TAKE a1 a2)` 242 >> Q.ISPECL_THEN [`a1`,`1`,`a2`] mp_tac take_drop_partition 243 >> unabbrev_all_tac 244 >> impl_tac >- intLib.COOPER_TAC 245 >> disch_then(fn x => rw[GSYM x]) 246 >> fs[ADD1,DROP_DROP] 247 >> `n < LENGTH(explode s)` 248 by(fs[]) 249 >> drule TAKE1_DROP 250 >> Cases_on `s` >> fs[mlstringTheory.strsub_def] 251QED 252 253Theorem null_index_no_null2: 254 !s n. null_index s n = NONE ==> EVERY ($~ o $= (CHR 0)) (DROP n (explode s)) 255Proof 256 ho_match_mp_tac null_index_ind 257 >> rpt strip_tac 258 >> qhdtm_x_assum `null_index` (mp_tac o PURE_ONCE_REWRITE_RULE [null_index_def]) 259 >> rw[] >> Cases_on `n ��� strlen s` 260 >> Cases_on `s` >> fs[GREATER_EQ] 261 >> imp_res_tac DROP_LENGTH_TOO_LONG >> fs[] 262 >> `n < STRLEN s'` by fs[] 263 >> imp_res_tac DROP_CONS_EL >> fs[] 264QED 265 266val cut_at_null_def = Define `cut_at_null s = 267 case null_index s 0 of 268 NONE => strcat s (str(CHR 0)) 269 | SOME n => substring s 0 (SUC n)` 270 271Theorem cut_at_null_SPLITP: 272 !s. cut_at_null s = implode(FST(SPLITP ($= (CHR 0)) (explode s)) ++ [CHR 0]) 273Proof 274 Cases >> rw[cut_at_null_def] >> reverse(PURE_TOP_CASE_TAC >> rw[]) 275 >- (imp_res_tac null_index_le_len >> rw[mlstringTheory.substring_def] 276 >> fs[mlstringTheory.strlen_def,mlstringTheory.implode_def] 277 >> imp_res_tac null_index_no_null >> fs[] 278 >> imp_res_tac null_index_null >> fs[] 279 >> imp_res_tac SPLITP_TAKE_DROP >> rfs[] 280 >> imp_res_tac (GSYM TAKE_SEG) >> fs[] 281 >> fs[ADD1] 282 >> Q.ISPECL_THEN [`s'`,`x`] assume_tac TAKE_EL_SNOC 283 >> rfs[]) 284 >- (imp_res_tac null_index_no_null2 285 >> fs[o_DEF] >> imp_res_tac SPLITP_EVERY 286 >> fs[mlstringTheory.implode_def,mlstringTheory.strcat_thm]) 287QED 288 289val _ = translate cut_at_null_def; 290 291val null_index_side_lem = Q.prove( 292 `!s n. null_index_side s n <=> T`, 293 ho_match_mp_tac null_index_ind 294 >> rw[] 295 >> PURE_ONCE_REWRITE_TAC[fetch "-" "null_index_side_def"] 296 >> fs[ADD1]) 297 |> update_precondition; 298 299val cut_at_null_side_lem = Q.prove(`!s. cut_at_null_side s <=> T`, 300 rw[fetch "-" "cut_at_null_side_def",null_index_side_lem] 301 >> imp_res_tac null_index_le_len >> fs[]) 302 |> update_precondition; 303 304val null_index_w_def = tDefine "null_index_w" 305 `null_index_w s n = 306 if n >= LENGTH s then NONE 307 else if EL n s = 0w then SOME n 308 else null_index_w s (SUC n)` 309 (wf_rel_tac `inv_image (measure (��(a,b). SUC a - b)) (LENGTH ## I)`); 310 311val null_index_w_ind = fetch "-" "null_index_w_ind"; 312 313Theorem null_index_w_le_len: 314 !s n m. null_index_w s n = SOME m ==> m < LENGTH s 315Proof 316 ho_match_mp_tac null_index_w_ind 317 >> rpt strip_tac 318 >> qhdtm_x_assum `null_index_w` (mp_tac o PURE_ONCE_REWRITE_RULE [null_index_w_def]) 319 >> rw[] 320QED 321 322Theorem null_index_w_in_bound: 323 !s n m. null_index_w s n = SOME m ==> n <= m 324Proof 325 ho_match_mp_tac null_index_w_ind 326 >> rpt strip_tac 327 >> qhdtm_x_assum `null_index_w` (mp_tac o PURE_ONCE_REWRITE_RULE [null_index_w_def]) 328 >> rw[] >> fs[] 329QED 330 331Theorem null_index_w_null: 332 !s n m. null_index_w s n = SOME m ==> EL m s = 0w 333Proof 334 ho_match_mp_tac null_index_w_ind 335 >> rpt strip_tac 336 >> qhdtm_x_assum `null_index_w` (mp_tac o PURE_ONCE_REWRITE_RULE [null_index_w_def]) 337 >> rw[] >> fs[] 338QED 339 340Theorem null_index_w_no_null: 341 !s n m. null_index_w s n = SOME m ==> EVERY ($~ o $= 0w) (TAKE (m-n) (DROP n s)) 342Proof 343 ho_match_mp_tac null_index_w_ind 344 >> rpt strip_tac 345 >> qhdtm_x_assum `null_index_w` (mp_tac o PURE_ONCE_REWRITE_RULE [null_index_w_def]) 346 >> rw[] 347 >> first_x_assum drule >> rpt(disch_then drule) 348 >> strip_tac 349 >> imp_res_tac null_index_w_le_len 350 >> imp_res_tac null_index_w_in_bound 351 >> qmatch_goalsub_abbrev_tac `EVERY _ (TAKE a1 a2)` 352 >> Q.ISPECL_THEN [`a1`,`1`,`a2`] mp_tac take_drop_partition 353 >> unabbrev_all_tac 354 >> impl_tac >- intLib.COOPER_TAC 355 >> disch_then(fn x => rw[GSYM x]) 356 >> fs[ADD1,DROP_DROP] 357 >> `n < LENGTH s` 358 by(fs[]) 359 >> drule TAKE1_DROP >> fs[] 360QED 361 362Theorem null_index_w_no_null2: 363 !s n. null_index_w s n = NONE ==> EVERY ($~ o $= 0w) (DROP n s) 364Proof 365 ho_match_mp_tac null_index_w_ind 366 >> rpt strip_tac 367 >> qhdtm_x_assum `null_index_w` (mp_tac o PURE_ONCE_REWRITE_RULE [null_index_w_def]) 368 >> rw[] >> Cases_on `n ��� LENGTH s` 369 >> fs[GREATER_EQ] 370 >> imp_res_tac DROP_LENGTH_TOO_LONG >> fs[] 371 >> `n < LENGTH s` by fs[] 372 >> imp_res_tac DROP_CONS_EL >> fs[] 373QED 374 375val cut_at_null_w_def = Define `cut_at_null_w s = 376 case null_index_w s 0 of 377 NONE => s ++ [0w] 378 | SOME n => SEG (SUC n) 0 s` 379 380Theorem cut_at_null_w_SPLITP: 381 !s. cut_at_null_w s = FST(SPLITP ($= 0w) s) ++ [0w] 382Proof 383 rw[cut_at_null_w_def] >> reverse(PURE_TOP_CASE_TAC >> rw[]) 384 >- (imp_res_tac null_index_w_le_len >> rw[mlstringTheory.substring_def] 385 >> fs[mlstringTheory.strlen_def,mlstringTheory.implode_def] 386 >> imp_res_tac null_index_w_no_null >> fs[] 387 >> imp_res_tac null_index_w_null >> fs[] 388 >> imp_res_tac SPLITP_TAKE_DROP >> rfs[] 389 >> fs[GSYM TAKE_SEG,ADD1] 390 >> Q.ISPECL_THEN [`s`,`x`] assume_tac TAKE_EL_SNOC 391 >> rfs[]) 392 >- (imp_res_tac null_index_w_no_null2 393 >> fs[o_DEF] >> imp_res_tac SPLITP_EVERY >> fs[]) 394QED 395 396Theorem null_index_w_thm: 397 ���s n. null_index_w (s:word8 list) n = null_index (implode (MAP (CHR ��� w2n) s)) n 398Proof 399 ho_match_mp_tac null_index_w_ind 400 >> rpt strip_tac 401 >> MAP_EVERY PURE_ONCE_REWRITE_TAC [[null_index_def],[null_index_w_def]] >> rw[] 402 >> fs[mlstringTheory.implode_def] 403 >> `n < LENGTH s` by fs[] 404 >> rfs[EL_MAP] 405 >> qspecl_then [`[EL n s]`,`[0w]`] assume_tac MAP_CHR_w2n_11 406 >> fs[] 407QED 408 409Theorem cut_at_null_w_thm: 410 ���s. cut_at_null_w (s:word8 list) = MAP (n2w o ORD) (explode (cut_at_null (implode (MAP (CHR ��� w2n) s)))) 411Proof 412 rw[cut_at_null_w_def,cut_at_null_def,null_index_w_thm] 413 >> PURE_TOP_CASE_TAC >> rw[MAP_MAP_o] 414 >> fs[n2w_ORD_CHR_w2n] 415 >> imp_res_tac null_index_le_len 416 >> fs[mlstringTheory.implode_def,mlstringTheory.substring_def] 417 >> MAP_EVERY PURE_ONCE_REWRITE_TAC [[null_index_def],[null_index_w_def]] >> rw[] 418 >> fs[GSYM TAKE_SEG,MAP_TAKE,MAP_MAP_o,n2w_ORD_CHR_w2n] 419QED 420 421Theorem cut_at_null_thm: 422 cut_at_null(strlit (MAP (CHR o w2n) l)) = strlit(MAP (CHR o w2n) (cut_at_null_w(l:word8 list))) 423Proof 424 rw[cut_at_null_w_thm,MAP_MAP_o,implode_def,CHR_w2n_n2w_ORD,REWRITE_RULE[implode_def] implode_explode] 425QED 426 427val null_terminated_def = Define ` 428 null_terminated s = ?m. null_index s 0 = SOME m` 429 430val null_terminated_w_def = Define ` 431 null_terminated_w s = ?m. null_index_w s 0 = SOME m` 432 433Theorem null_terminated_w_thm: 434 !s. null_terminated_w (s:word8 list) = null_terminated(implode(MAP (CHR o w2n) s)) 435Proof 436 rw[null_terminated_def,null_terminated_w_def,null_index_w_thm] 437QED 438 439Theorem null_index_strcat1: 440 !s1 n s2 m. null_index s1 n = SOME m ==> null_index (strcat s1 s2) n = SOME m 441Proof 442 ho_match_mp_tac null_index_ind 443 >> rpt strip_tac 444 >> qhdtm_x_assum `null_index` mp_tac 445 >> PURE_ONCE_REWRITE_TAC [null_index_def] 446 >> rw[] >> fs[] 447 >> MAP_EVERY Cases_on [`s1`,`s2`] 448 >> fs[mlstringTheory.strsub_def,mlstringTheory.strcat_def,mlstringTheory.concat_def,EL_APPEND_EQN] 449QED 450 451Theorem null_terminated_cut_APPEND: 452 !s1 s2. null_terminated s1 ==> cut_at_null(strcat s1 s2) = cut_at_null s1 453Proof 454 rw[null_terminated_def,cut_at_null_def] >> imp_res_tac null_index_strcat1 455 >> fs[] >> imp_res_tac null_index_le_len 456 >> MAP_EVERY Cases_on [`s1`,`s2`] 457 >> fs[mlstringTheory.strsub_def,mlstringTheory.strcat_def,mlstringTheory.concat_def, 458 mlstringTheory.substring_def] 459 >> match_mp_tac SEG_APPEND1 >> fs[] 460QED 461 462Theorem null_terminated_cut_w_APPEND: 463 !s1 s2. null_terminated_w(s1:word8 list) ==> cut_at_null_w(s1 ++ s2) = cut_at_null_w s1 464Proof 465 rw[null_terminated_w_thm,cut_at_null_w_thm] 466 >> drule null_terminated_cut_APPEND 467 >> disch_then(qspec_then `implode(MAP (CHR ��� w2n) s2)` assume_tac) 468 >> simp[mlstringTheory.implode_STRCAT] 469QED 470 471val _ = export_theory (); 472