Move no-assumptions related definitions and theorems to bir-support

:robot: Results of: scripts/ci/static-analysis.sh

Grep-cheat analysis:

Found 23 occurences of cheat in src/ and 0 in examples/.

- [src/theory/tools/wp/bir_wp_simpScript.sml, line 397](https://github.com/kth-step/HolBA/blob/05e86baaccda36f35ae1b03a4acfaf72dcc68c45/src/theory/tools/wp/bir_wp_simpScript.sml#L397) - [src/theory/tools/wp/bir_wp_simpScript.sml, line 422](https://github.com/kth-step/HolBA/blob/05e86baaccda36f35ae1b03a4acfaf72dcc68c45/src/theory/tools/wp/bir_wp_simpScript.sml#L422) - [src/theory/tools/wp/bir_wp_simpScript.sml, line 429](https://github.com/kth-step/HolBA/blob/05e86baaccda36f35ae1b03a4acfaf72dcc68c45/src/theory/tools/wp/bir_wp_simpScript.sml#L429) - [src/theory/tools/wp/bir_wp_simpScript.sml, line 442](https://github.com/kth-step/HolBA/blob/05e86baaccda36f35ae1b03a4acfaf72dcc68c45/src/theory/tools/wp/bir_wp_simpScript.sml#L442) - [src/theory/tools/wp/bir_wp_simpScript.sml, line 541](https://github.com/kth-step/HolBA/blob/05e86baaccda36f35ae1b03a4acfaf72dcc68c45/src/theory/tools/wp/bir_wp_simpScript.sml#L541) - [src/theory/tools/wp/bir_wp_simpScript.sml, line 913](https://github.com/kth-step/HolBA/blob/05e86baaccda36f35ae1b03a4acfaf72dcc68c45/src/theory/tools/wp/bir_wp_simpScript.sml#L913) - [src/theory/tools/wp/bir_wp_simpScript.sml, line 987](https://github.com/kth-step/HolBA/blob/05e86baaccda36f35ae1b03a4acfaf72dcc68c45/src/theory/tools/wp/bir_wp_simpScript.sml#L987) - [src/theory/tools/wp/bir_wp_simpScript.sml, line 1075](https://github.com/kth-step/HolBA/blob/05e86baaccda36f35ae1b03a4acfaf72dcc68c45/src/theory/tools/wp/bir_wp_simpScript.sml#L1075) - [src/theory/tools/wp/bir_wp_simpScript.sml, line 1085](https://github.com/kth-step/HolBA/blob/05e86baaccda36f35ae1b03a4acfaf72dcc68c45/src/theory/tools/wp/bir_wp_simpScript.sml#L1085) - [src/theory/tools/wp/bir_wp_simpScript.sml, line 1192](https://github.com/kth-step/HolBA/blob/05e86baaccda36f35ae1b03a4acfaf72dcc68c45/src/theory/tools/wp/bir_wp_simpScript.sml#L1192) - [src/theory/tools/wp/bir_wp_simpScript.sml, line 2898](https://github.com/kth-step/HolBA/blob/05e86baaccda36f35ae1b03a4acfaf72dcc68c45/src/theory/tools/wp/bir_wp_simpScript.sml#L2898) - [src/theory/tools/wp/bir_wp_simpScript.sml, line 2906](https://github.com/kth-step/HolBA/blob/05e86baaccda36f35ae1b03a4acfaf72dcc68c45/src/theory/tools/wp/bir_wp_simpScript.sml#L2906) - [src/theory/tools/wp/bir_wp_simpScript.sml, line 2916](https://github.com/kth-step/HolBA/blob/05e86baaccda36f35ae1b03a4acfaf72dcc68c45/src/theory/tools/wp/bir_wp_simpScript.sml#L2916) - [src/theory/tools/wp/bir_wp_simpScript.sml, line 2925](https://github.com/kth-step/HolBA/blob/05e86baaccda36f35ae1b03a4acfaf72dcc68c45/src/theory/tools/wp/bir_wp_simpScript.sml#L2925) - [src/theory/tools/wp/bir_wp_simpScript.sml, line 3167](https://github.com/kth-step/HolBA/blob/05e86baaccda36f35ae1b03a4acfaf72dcc68c45/src/theory/tools/wp/bir_wp_simpScript.sml#L3167) - [src/theory/tools/wp/bir_wp_simpScript.sml, line 3373](https://github.com/kth-step/HolBA/blob/05e86baaccda36f35ae1b03a4acfaf72dcc68c45/src/theory/tools/wp/bir_wp_simpScript.sml#L3373) - [src/theory/tools/wp/bir_wp_simpScript.sml, line 3456](https://github.com/kth-step/HolBA/blob/05e86baaccda36f35ae1b03a4acfaf72dcc68c45/src/theory/tools/wp/bir_wp_simpScript.sml#L3456) - [src/theory/tools/wp/bir_wp_simpScript.sml, line 3672](https://github.com/kth-step/HolBA/blob/05e86baaccda36f35ae1b03a4acfaf72dcc68c45/src/theory/tools/wp/bir_wp_simpScript.sml#L3672) - [src/theory/tools/wp/bir_wp_simpScript.sml, line 4065](https://github.com/kth-step/HolBA/blob/05e86baaccda36f35ae1b03a4acfaf72dcc68c45/src/theory/tools/wp/bir_wp_simpScript.sml#L4065) - [src/theory/tools/wp/bir_wp_simpScript.sml, line 4101](https://github.com/kth-step/HolBA/blob/05e86baaccda36f35ae1b03a4acfaf72dcc68c45/src/theory/tools/wp/bir_wp_simpScript.sml#L4101) - [src/theory/tools/wp/bir_wp_simpScript.sml, line 4509](https://github.com/kth-step/HolBA/blob/05e86baaccda36f35ae1b03a4acfaf72dcc68c45/src/theory/tools/wp/bir_wp_simpScript.sml#L4509) - [src/theory/tools/wp/bir_wp_simpScript.sml, line 4544](https://github.com/kth-step/HolBA/blob/05e86baaccda36f35ae1b03a4acfaf72dcc68c45/src/theory/tools/wp/bir_wp_simpScript.sml#L4544) - [src/theory/tools/lifter/bir_arm8_extrasScript.sml, line 825](https://github.com/kth-step/HolBA/blob/05e86baaccda36f35ae1b03a4acfaf72dcc68c45/src/theory/tools/lifter/bir_arm8_extrasScript.sml#L825)

Click here for details

``` src/theory/tools/wp/bir_wp_simpScript.sml-391- [ src/theory/tools/wp/bir_wp_simpScript.sml-392- ALL_TAC src/theory/tools/wp/bir_wp_simpScript.sml-393- , src/theory/tools/wp/bir_wp_simpScript.sml-394- ALL_TAC src/theory/tools/wp/bir_wp_simpScript.sml-395- , src/theory/tools/wp/bir_wp_simpScript.sml-396- FULL_SIMP_TAC std_ss [bir_exp_tautologiesTheory.bir_exp_is_taut_def] >> src/theory/tools/wp/bir_wp_simpScript.sml:397: cheat (* extend environment by uninitialized variables of e2, and then use the theorems for bir_and and bir_imp *) src/theory/tools/wp/bir_wp_simpScript.sml-398- ] >> ( src/theory/tools/wp/bir_wp_simpScript.sml-399- FULL_SIMP_TAC std_ss [bir_exp_imp_def, bir_exp_and_def, bir_exp_tautologiesTheory.bir_exp_is_taut_def] >> src/theory/tools/wp/bir_wp_simpScript.sml-400- FULL_SIMP_TAC (std_ss++pred_setSimps.PRED_SET_ss) [bir_is_bool_exp_REWRS, bir_vars_of_exp_def, bir_var_set_is_well_typed_UNION] src/theory/tools/wp/bir_wp_simpScript.sml-401- ) src/theory/tools/wp/bir_wp_simpScript.sml-402- ) src/theory/tools/wp/bir_wp_simpScript.sml-403- ) >> -- src/theory/tools/wp/bir_wp_simpScript.sml-416- subgoal `(bir_var_set_is_well_typed (bir_vars_of_exp e1)) /\ (bir_var_set_is_well_typed (bir_vars_of_exp e2)) /\ (bir_var_set_is_well_typed (bir_vars_of_exp prem))` >- ( src/theory/tools/wp/bir_wp_simpScript.sml-417- FULL_SIMP_TAC (std_ss++pred_setSimps.PRED_SET_ss) [bir_var_set_is_well_typed_UNION] src/theory/tools/wp/bir_wp_simpScript.sml-418- ) >> src/theory/tools/wp/bir_wp_simpScript.sml-419- src/theory/tools/wp/bir_wp_simpScript.sml-420- FULL_SIMP_TAC std_ss [bir_var_set_is_well_typed_UNION_initialised_thm] src/theory/tools/wp/bir_wp_simpScript.sml-421-*) src/theory/tools/wp/bir_wp_simpScript.sml:422: cheat src/theory/tools/wp/bir_wp_simpScript.sml-423- , src/theory/tools/wp/bir_wp_simpScript.sml-424- subgoal `(bir_eval_exp (bir_exp_imp prem e1) env = bir_val_true) /\ (bir_eval_exp (bir_exp_imp prem e2) env = bir_val_true)` >- ( src/theory/tools/wp/bir_wp_simpScript.sml-425- FULL_SIMP_TAC std_ss [bir_exp_imp_def, bir_exp_and_def, bir_vars_of_exp_def, bir_env_vars_are_initialised_UNION] src/theory/tools/wp/bir_wp_simpScript.sml-426- ) >> src/theory/tools/wp/bir_wp_simpScript.sml-427- src/theory/tools/wp/bir_wp_simpScript.sml-428- src/theory/tools/wp/bir_wp_simpScript.sml:429: cheat src/theory/tools/wp/bir_wp_simpScript.sml-430- ] src/theory/tools/wp/bir_wp_simpScript.sml-431-); src/theory/tools/wp/bir_wp_simpScript.sml-432- src/theory/tools/wp/bir_wp_simpScript.sml-433-val bir_wp_simp_taut_imp_thm = store_thm("bir_wp_simp_taut_imp_thm", `` src/theory/tools/wp/bir_wp_simpScript.sml-434- !prem e1 e2. src/theory/tools/wp/bir_wp_simpScript.sml-435- (bir_exp_is_taut (bir_exp_imp prem (bir_exp_imp e1 e2))) src/theory/tools/wp/bir_wp_simpScript.sml-436- <=> src/theory/tools/wp/bir_wp_simpScript.sml-437- (bir_exp_is_taut (bir_exp_imp (bir_exp_and prem e1) e2) src/theory/tools/wp/bir_wp_simpScript.sml-438-``, src/theory/tools/wp/bir_wp_simpScript.sml-439- src/theory/tools/wp/bir_wp_simpScript.sml-440- REWRITE_TAC [bir_exp_imp_def, bir_exp_and_def] >> src/theory/tools/wp/bir_wp_simpScript.sml-441- REPEAT STRIP_TAC >> src/theory/tools/wp/bir_wp_simpScript.sml:442:cheat src/theory/tools/wp/bir_wp_simpScript.sml-443-); src/theory/tools/wp/bir_wp_simpScript.sml-444-*) src/theory/tools/wp/bir_wp_simpScript.sml-445- src/theory/tools/wp/bir_wp_simpScript.sml-446- src/theory/tools/wp/bir_wp_simpScript.sml-447- src/theory/tools/wp/bir_wp_simpScript.sml-448- -- src/theory/tools/wp/bir_wp_simpScript.sml-535-(* src/theory/tools/wp/bir_wp_simpScript.sml-536-val bir_exp_and_bool_thm = store_thm ("bir_exp_and_bool_thm", `` src/theory/tools/wp/bir_wp_simpScript.sml-537- bir_eval_exp (bir_exp_and e1 e2) s) src/theory/tools/wp/bir_wp_simpScript.sml-538-``, src/theory/tools/wp/bir_wp_simpScript.sml-539- src/theory/tools/wp/bir_wp_simpScript.sml-540-bir_wp_simp_eval_bin_is_Imm_s_thm src/theory/tools/wp/bir_wp_simpScript.sml:541: cheat src/theory/tools/wp/bir_wp_simpScript.sml-542-); src/theory/tools/wp/bir_wp_simpScript.sml-543-*) src/theory/tools/wp/bir_wp_simpScript.sml-544- src/theory/tools/wp/bir_wp_simpScript.sml-545- src/theory/tools/wp/bir_wp_simpScript.sml-546-val bir_wp_simp_eval_imp_thm = store_thm("bir_wp_simp_eval_imp_thm", `` src/theory/tools/wp/bir_wp_simpScript.sml-547- !prem e1 e2. -- src/theory/tools/wp/bir_wp_simpScript.sml-907- src/theory/tools/wp/bir_wp_simpScript.sml-908-val bir_env_initialise_vars_ORDER_thm = store_thm("bir_env_initialise_vars_ORDER_thm", `` src/theory/tools/wp/bir_wp_simpScript.sml-909- !vs env. src/theory/tools/wp/bir_wp_simpScript.sml-910- (bir_env_order env (bir_env_initialise_vars env vs)) src/theory/tools/wp/bir_wp_simpScript.sml-911-``, src/theory/tools/wp/bir_wp_simpScript.sml-912- src/theory/tools/wp/bir_wp_simpScript.sml:913: cheat src/theory/tools/wp/bir_wp_simpScript.sml-914-(* src/theory/tools/wp/bir_wp_simpScript.sml-915-bir_env_order_def src/theory/tools/wp/bir_wp_simpScript.sml-916-*) src/theory/tools/wp/bir_wp_simpScript.sml-917-); src/theory/tools/wp/bir_wp_simpScript.sml-918- src/theory/tools/wp/bir_wp_simpScript.sml-919- -- src/theory/tools/wp/bir_wp_simpScript.sml-981- !vs env. src/theory/tools/wp/bir_wp_simpScript.sml-982- (bir_var_set_is_well_typed vs) ==> src/theory/tools/wp/bir_wp_simpScript.sml-983- (FINITE vs) ==> src/theory/tools/wp/bir_wp_simpScript.sml-984- (bir_env_vars_are_initialised (bir_env_initialise_vars env vs) vs) src/theory/tools/wp/bir_wp_simpScript.sml-985-``, src/theory/tools/wp/bir_wp_simpScript.sml-986- src/theory/tools/wp/bir_wp_simpScript.sml:987: cheat src/theory/tools/wp/bir_wp_simpScript.sml-988-); src/theory/tools/wp/bir_wp_simpScript.sml-989-*) src/theory/tools/wp/bir_wp_simpScript.sml-990- src/theory/tools/wp/bir_wp_simpScript.sml-991-(* src/theory/tools/wp/bir_wp_simpScript.sml-992-this is a special case as well src/theory/tools/wp/bir_wp_simpScript.sml-993-*) -- src/theory/tools/wp/bir_wp_simpScript.sml-1069- ( src/theory/tools/wp/bir_wp_simpScript.sml-1070- (!v. (v IN vs1) ==> (bir_env_lookup (bir_var_name v) env' = bir_env_lookup (bir_var_name v) env)) /\ src/theory/tools/wp/bir_wp_simpScript.sml-1071- (!v. (v IN (vs2 DIFF vs1)) ==> (bir_env_lookup (bir_var_name v) env' = SOME (bir_var_type v, SOME (bir_default_value_of_type (bir_var_type v))))) src/theory/tools/wp/bir_wp_simpScript.sml-1072- ) src/theory/tools/wp/bir_wp_simpScript.sml-1073-``, src/theory/tools/wp/bir_wp_simpScript.sml-1074- src/theory/tools/wp/bir_wp_simpScript.sml:1075: cheat src/theory/tools/wp/bir_wp_simpScript.sml-1076-); src/theory/tools/wp/bir_wp_simpScript.sml-1077-*) src/theory/tools/wp/bir_wp_simpScript.sml-1078- src/theory/tools/wp/bir_wp_simpScript.sml-1079-val bir_env_initialise_vars_DIFF_eval_exp_thm = store_thm("bir_env_initialise_vars_DIFF_eval_exp_thm", `` src/theory/tools/wp/bir_wp_simpScript.sml-1080- !e vs1 e2 env. src/theory/tools/wp/bir_wp_simpScript.sml-1081- ((bir_vars_of_exp e) SUBSET vs1) ==> src/theory/tools/wp/bir_wp_simpScript.sml-1082- (bir_eval_exp e (bir_env_initialise_vars env ((bir_vars_of_exp e2) DIFF vs1)) = bir_eval_exp e env) src/theory/tools/wp/bir_wp_simpScript.sml-1083-``, src/theory/tools/wp/bir_wp_simpScript.sml-1084- src/theory/tools/wp/bir_wp_simpScript.sml:1085: cheat src/theory/tools/wp/bir_wp_simpScript.sml-1086-); src/theory/tools/wp/bir_wp_simpScript.sml-1087-*) src/theory/tools/wp/bir_wp_simpScript.sml-1088- src/theory/tools/wp/bir_wp_simpScript.sml-1089- src/theory/tools/wp/bir_wp_simpScript.sml-1090-val bir_wp_simp_taut_and_thm = store_thm("bir_wp_simp_taut_and_thm", `` src/theory/tools/wp/bir_wp_simpScript.sml-1091- !prem e1 e2. -- src/theory/tools/wp/bir_wp_simpScript.sml-1186- METIS_TAC [Abbr `env'`, bir_env_initialise_vars_inited_DIFF_exp_thm, bir_env_vars_are_initialised_UNION, pred_setTheory.UNION_ASSOC] src/theory/tools/wp/bir_wp_simpScript.sml-1187-(*, pred_setTheory.UNION_COMM*) src/theory/tools/wp/bir_wp_simpScript.sml-1188-(*bir_env_initialise_vars_init_exp_thm*) src/theory/tools/wp/bir_wp_simpScript.sml-1189-(*bir_env_initialise_vars_inited_thm, *) src/theory/tools/wp/bir_wp_simpScript.sml-1190- src/theory/tools/wp/bir_wp_simpScript.sml-1191-(* uncheat *) src/theory/tools/wp/bir_wp_simpScript.sml:1192:(*cheat*) src/theory/tools/wp/bir_wp_simpScript.sml-1193-(* src/theory/tools/wp/bir_wp_simpScript.sml-1194-FULL_SIMP_TAC std_ss [bir_env_initialise_vars_init_exp_thm] src/theory/tools/wp/bir_wp_simpScript.sml-1195-*) src/theory/tools/wp/bir_wp_simpScript.sml-1196- ) >> src/theory/tools/wp/bir_wp_simpScript.sml-1197-*) src/theory/tools/wp/bir_wp_simpScript.sml-1198- -- src/theory/tools/wp/bir_wp_simpScript.sml-2892-(* src/theory/tools/wp/bir_wp_simpScript.sml-2893-val bir_eval_memeq_REFL = store_thm("bir_eval_memeq_REFL", `` src/theory/tools/wp/bir_wp_simpScript.sml-2894- !m. src/theory/tools/wp/bir_wp_simpScript.sml-2895- (bir_eval_memeq m m = bir_val_true) src/theory/tools/wp/bir_wp_simpScript.sml-2896-``, src/theory/tools/wp/bir_wp_simpScript.sml-2897- src/theory/tools/wp/bir_wp_simpScript.sml:2898: cheat src/theory/tools/wp/bir_wp_simpScript.sml-2899-); src/theory/tools/wp/bir_wp_simpScript.sml-2900- src/theory/tools/wp/bir_wp_simpScript.sml-2901-val bir_eval_memeq_SYMM = store_thm("bir_eval_memeq_SYMM", `` src/theory/tools/wp/bir_wp_simpScript.sml-2902- !m1 m2. src/theory/tools/wp/bir_wp_simpScript.sml-2903- (bir_eval_memeq m1 m2) = (bir_eval_memeq m2 m1) src/theory/tools/wp/bir_wp_simpScript.sml-2904-``, src/theory/tools/wp/bir_wp_simpScript.sml-2905- src/theory/tools/wp/bir_wp_simpScript.sml:2906: cheat src/theory/tools/wp/bir_wp_simpScript.sml-2907-); src/theory/tools/wp/bir_wp_simpScript.sml-2908- src/theory/tools/wp/bir_wp_simpScript.sml-2909-val bir_eval_memeq_TRANS = store_thm("bir_eval_memeq_TRANS", `` src/theory/tools/wp/bir_wp_simpScript.sml-2910- !m1 m2 m3. src/theory/tools/wp/bir_wp_simpScript.sml-2911- (bir_eval_memeq m1 m2 = bir_val_true) ==> src/theory/tools/wp/bir_wp_simpScript.sml-2912- (bir_eval_memeq m2 m3 = bir_val_true) ==> src/theory/tools/wp/bir_wp_simpScript.sml-2913- (bir_eval_memeq m1 m3 = bir_val_true) src/theory/tools/wp/bir_wp_simpScript.sml-2914-``, src/theory/tools/wp/bir_wp_simpScript.sml-2915- src/theory/tools/wp/bir_wp_simpScript.sml:2916: cheat src/theory/tools/wp/bir_wp_simpScript.sml-2917-); src/theory/tools/wp/bir_wp_simpScript.sml-2918- src/theory/tools/wp/bir_wp_simpScript.sml-2919-val bir_eval_memeq_trans = store_thm("bir_eval_memeq_trans", `` src/theory/tools/wp/bir_wp_simpScript.sml-2920- !m1 m2 m3. src/theory/tools/wp/bir_wp_simpScript.sml-2921- (bir_eval_memeq m1 m2) ==> src/theory/tools/wp/bir_wp_simpScript.sml-2922- (bir_eval_memeq m1 m3 = bir_eval_memeq m2 m3) src/theory/tools/wp/bir_wp_simpScript.sml-2923-``, src/theory/tools/wp/bir_wp_simpScript.sml-2924- src/theory/tools/wp/bir_wp_simpScript.sml:2925: cheat src/theory/tools/wp/bir_wp_simpScript.sml-2926-); src/theory/tools/wp/bir_wp_simpScript.sml-2927-*) src/theory/tools/wp/bir_wp_simpScript.sml-2928- src/theory/tools/wp/bir_wp_simpScript.sml-2929- src/theory/tools/wp/bir_wp_simpScript.sml-2930-val bir_eval_exp_eq_def = Define ` src/theory/tools/wp/bir_wp_simpScript.sml-2931- bir_eval_exp_eq e1 e2 env = -- src/theory/tools/wp/bir_wp_simpScript.sml-3161- ``!. src/theory/tools/wp/bir_wp_simpScript.sml-3162- () ==> src/theory/tools/wp/bir_wp_simpScript.sml-3163- () ==> src/theory/tools/wp/bir_wp_simpScript.sml-3164- (bir_update_mmap aty mmap a vs) src/theory/tools/wp/bir_wp_simpScript.sml-3165-``, src/theory/tools/wp/bir_wp_simpScript.sml-3166- src/theory/tools/wp/bir_wp_simpScript.sml:3167:cheat src/theory/tools/wp/bir_wp_simpScript.sml-3168-); src/theory/tools/wp/bir_wp_simpScript.sml-3169-*) src/theory/tools/wp/bir_wp_simpScript.sml-3170- src/theory/tools/wp/bir_wp_simpScript.sml-3171- src/theory/tools/wp/bir_wp_simpScript.sml-3172-(* src/theory/tools/wp/bir_wp_simpScript.sml-3173-bir_exp_memTheory.bir_update_mmap_UNCHANGED -- src/theory/tools/wp/bir_wp_simpScript.sml-3367- ASSUME_TAC (Q.SPECL [`aty`, `((bir_mem_addr aty a =+ v2n h) mmap)`, `(SUC a)`, `vs`, `(bir_mem_addr aty a)`] bir_exp_memTheory.bir_update_mmap_UNCHANGED) >> src/theory/tools/wp/bir_wp_simpScript.sml-3368-*) src/theory/tools/wp/bir_wp_simpScript.sml-3369-(* src/theory/tools/wp/bir_wp_simpScript.sml-3370- ASSUME_TAC (prove(``(!n. src/theory/tools/wp/bir_wp_simpScript.sml-3371- n < LENGTH (vs:bitstring list) ==> src/theory/tools/wp/bir_wp_simpScript.sml-3372- bir_mem_addr aty a <> bir_mem_addr aty (SUC a + n))``, src/theory/tools/wp/bir_wp_simpScript.sml:3373:cheat)) >> src/theory/tools/wp/bir_wp_simpScript.sml-3374- src/theory/tools/wp/bir_wp_simpScript.sml-3375- FULL_SIMP_TAC list_ss [combinTheory.UPDATE_APPLY] src/theory/tools/wp/bir_wp_simpScript.sml-3376-*) src/theory/tools/wp/bir_wp_simpScript.sml-3377- src/theory/tools/wp/bir_wp_simpScript.sml-3378- FULL_SIMP_TAC arith_ss [bir_exp_memTheory.bir_mem_addr_def, bitTheory.MOD_2EXP_def] >> src/theory/tools/wp/bir_wp_simpScript.sml-3379- FULL_SIMP_TAC list_ss [] >> -- src/theory/tools/wp/bir_wp_simpScript.sml-3450- Cases_on `addr = bir_mem_addr at a` >> src/theory/tools/wp/bir_wp_simpScript.sml-3451- METIS_TAC [bir_exp_memTheory.bir_update_mmap_UNCHANGED, combinTheory.UPDATE_APPLY] src/theory/tools/wp/bir_wp_simpScript.sml-3452- ) src/theory/tools/wp/bir_wp_simpScript.sml-3453- src/theory/tools/wp/bir_wp_simpScript.sml-3454-bir_exp_memTheory.bir_update_mmap_UNCHANGED src/theory/tools/wp/bir_wp_simpScript.sml-3455-bir_update_mmap_EQUAL_FOR src/theory/tools/wp/bir_wp_simpScript.sml:3456: cheat src/theory/tools/wp/bir_wp_simpScript.sml-3457-); src/theory/tools/wp/bir_wp_simpScript.sml-3458-*) src/theory/tools/wp/bir_wp_simpScript.sml-3459- src/theory/tools/wp/bir_wp_simpScript.sml-3460-(* src/theory/tools/wp/bir_wp_simpScript.sml-3461-bir_update_mmap_EQUAL_FOR src/theory/tools/wp/bir_wp_simpScript.sml-3462-bir_exp_memTheory.bir_update_mmap_UNCHANGED -- src/theory/tools/wp/bir_wp_simpScript.sml-3666- GEN_TAC >> src/theory/tools/wp/bir_wp_simpScript.sml-3667-(* Q.PAT_X_ASSUM `!a. P` (fn thm => ASSUME_TAC (((Q.SPECL [`a`])) thm) >> src/theory/tools/wp/bir_wp_simpScript.sml-3668- ASSUME_TAC (((Q.SPECL [`a`])) thm)) >> src/theory/tools/wp/bir_wp_simpScript.sml-3669-*) src/theory/tools/wp/bir_wp_simpScript.sml-3670- Q.PAT_X_ASSUM `!a. P` (ASSUME_TAC o (Q.SPEC `a`)) >> src/theory/tools/wp/bir_wp_simpScript.sml-3671-(* FULL_SIMP_TAC std_ss [] >>*) src/theory/tools/wp/bir_wp_simpScript.sml:3672: cheat >> src/theory/tools/wp/bir_wp_simpScript.sml-3673- METIS_TAC [n2bs_bir_update_mmap_REVERSE_thm, n2bs_bir_update_mmap_thm] src/theory/tools/wp/bir_wp_simpScript.sml-3674-*) src/theory/tools/wp/bir_wp_simpScript.sml-3675- src/theory/tools/wp/bir_wp_simpScript.sml-3676- src/theory/tools/wp/bir_wp_simpScript.sml-3677- src/theory/tools/wp/bir_wp_simpScript.sml-3678- -- src/theory/tools/wp/bir_wp_simpScript.sml-4059- src/theory/tools/wp/bir_wp_simpScript.sml-4060- ) >> src/theory/tools/wp/bir_wp_simpScript.sml-4061- src/theory/tools/wp/bir_wp_simpScript.sml-4062-*) src/theory/tools/wp/bir_wp_simpScript.sml-4063- src/theory/tools/wp/bir_wp_simpScript.sml-4064-(* src/theory/tools/wp/bir_wp_simpScript.sml:4065: cheat src/theory/tools/wp/bir_wp_simpScript.sml-4066- Cases_on `b2` >> ( src/theory/tools/wp/bir_wp_simpScript.sml-4067- ) src/theory/tools/wp/bir_wp_simpScript.sml-4068- src/theory/tools/wp/bir_wp_simpScript.sml-4069- src/theory/tools/wp/bir_wp_simpScript.sml-4070- src/theory/tools/wp/bir_wp_simpScript.sml-4071- -- src/theory/tools/wp/bir_wp_simpScript.sml-4095- GEN_TAC >> src/theory/tools/wp/bir_wp_simpScript.sml-4096-(* Q.PAT_X_ASSUM `!a. P` (fn thm => ASSUME_TAC (((Q.SPECL [`a`])) thm) >> src/theory/tools/wp/bir_wp_simpScript.sml-4097- ASSUME_TAC (((Q.SPECL [`a`])) thm)) >> src/theory/tools/wp/bir_wp_simpScript.sml-4098-*) src/theory/tools/wp/bir_wp_simpScript.sml-4099- Q.PAT_X_ASSUM `!a. P` (ASSUME_TAC o (Q.SPEC `a`)) >> src/theory/tools/wp/bir_wp_simpScript.sml-4100-(* FULL_SIMP_TAC std_ss [] >>*) src/theory/tools/wp/bir_wp_simpScript.sml:4101: cheat >> src/theory/tools/wp/bir_wp_simpScript.sml-4102- METIS_TAC [n2bs_bir_update_mmap_REVERSE_thm, n2bs_bir_update_mmap_thm] src/theory/tools/wp/bir_wp_simpScript.sml-4103-*) src/theory/tools/wp/bir_wp_simpScript.sml-4104- ) src/theory/tools/wp/bir_wp_simpScript.sml-4105-); src/theory/tools/wp/bir_wp_simpScript.sml-4106- src/theory/tools/wp/bir_wp_simpScript.sml-4107- -- src/theory/tools/wp/bir_wp_simpScript.sml-4503-``, src/theory/tools/wp/bir_wp_simpScript.sml-4504- src/theory/tools/wp/bir_wp_simpScript.sml-4505-(* src/theory/tools/wp/bir_wp_simpScript.sml-4506- REPEAT STRIP_TAC >> src/theory/tools/wp/bir_wp_simpScript.sml-4507-*) src/theory/tools/wp/bir_wp_simpScript.sml-4508- src/theory/tools/wp/bir_wp_simpScript.sml:4509: cheat src/theory/tools/wp/bir_wp_simpScript.sml-4510-); src/theory/tools/wp/bir_wp_simpScript.sml-4511- src/theory/tools/wp/bir_wp_simpScript.sml-4512- src/theory/tools/wp/bir_wp_simpScript.sml-4513-(* TODO: should probably be somewhere else *) src/theory/tools/wp/bir_wp_simpScript.sml-4514-val bir_exp_conj_from_list_def = Define ` src/theory/tools/wp/bir_wp_simpScript.sml-4515- bir_exp_conj_from_list = FOLDL (\expa. \exp. BExp_BinExp BIExp_And expa exp) (BExp_Const (Imm1 1w)) -- src/theory/tools/wp/bir_wp_simpScript.sml-4538- REPEAT STRIP_TAC >> src/theory/tools/wp/bir_wp_simpScript.sml-4539- EQ_TAC >- ( src/theory/tools/wp/bir_wp_simpScript.sml-4540- REPEAT STRIP_TAC >> src/theory/tools/wp/bir_wp_simpScript.sml-4541- src/theory/tools/wp/bir_wp_simpScript.sml-4542- ) >> src/theory/tools/wp/bir_wp_simpScript.sml-4543-*) src/theory/tools/wp/bir_wp_simpScript.sml:4544: cheat src/theory/tools/wp/bir_wp_simpScript.sml-4545-); src/theory/tools/wp/bir_wp_simpScript.sml-4546-*) src/theory/tools/wp/bir_wp_simpScript.sml-4547- src/theory/tools/wp/bir_wp_simpScript.sml-4548- src/theory/tools/wp/bir_wp_simpScript.sml-4549- src/theory/tools/wp/bir_wp_simpScript.sml-4550- -- src/theory/tools/lifter/bir_arm8_extrasScript.sml-819- g_low(g_low(w1) * g_high(w2)) src/theory/tools/lifter/bir_arm8_extrasScript.sml-820- ) + src/theory/tools/lifter/bir_arm8_extrasScript.sml-821- g_high(g_high(w1) * g_low(w2)) + src/theory/tools/lifter/bir_arm8_extrasScript.sml-822- g_high(g_low(w1) * g_high(w2)) + src/theory/tools/lifter/bir_arm8_extrasScript.sml-823-(g_high(w1) * g_high(w2)) src/theory/tools/lifter/bir_arm8_extrasScript.sml-824-``, src/theory/tools/lifter/bir_arm8_extrasScript.sml:825: cheat); src/theory/tools/lifter/bir_arm8_extrasScript.sml-826-val arm8_high_u_mul = REWRITE_RULE [g_low_def, g_high_def] arm8_high_u_mul_internal; src/theory/tools/lifter/bir_arm8_extrasScript.sml-827-*) src/theory/tools/lifter/bir_arm8_extrasScript.sml-828- src/theory/tools/lifter/bir_arm8_extrasScript.sml-829- src/theory/tools/lifter/bir_arm8_extrasScript.sml-830-val arm8_ngc64_fold = store_thm ("arm8_ngc64_fold", src/theory/tools/lifter/bir_arm8_extrasScript.sml-831- ``!w:word64 c. ```

Grep-todo analysis:

Found 54 occurences of TODO/FIXME in src/ and 0 in examples/.

- [src/shared/bir_exp_to_wordsLib.sml, line 514](https://github.com/kth-step/HolBA/blob/05e86baaccda36f35ae1b03a4acfaf72dcc68c45/src/shared/bir_exp_to_wordsLib.sml#L514) - [src/theory/bir-support/bir_program_no_assumeScript.sml, line 379](https://github.com/kth-step/HolBA/blob/05e86baaccda36f35ae1b03a4acfaf72dcc68c45/src/theory/bir-support/bir_program_no_assumeScript.sml#L379) - [src/theory/bir-support/bir_exp_congruencesScript.sml, line 167](https://github.com/kth-step/HolBA/blob/05e86baaccda36f35ae1b03a4acfaf72dcc68c45/src/theory/bir-support/bir_exp_congruencesScript.sml#L167) - [src/theory/bir-support/bir_exp_congruencesScript.sml, line 362](https://github.com/kth-step/HolBA/blob/05e86baaccda36f35ae1b03a4acfaf72dcc68c45/src/theory/bir-support/bir_exp_congruencesScript.sml#L362) - [src/theory/tools/wp/bir_wp_simpScript.sml, line 29](https://github.com/kth-step/HolBA/blob/05e86baaccda36f35ae1b03a4acfaf72dcc68c45/src/theory/tools/wp/bir_wp_simpScript.sml#L29) - [src/theory/tools/wp/bir_wp_simpScript.sml, line 220](https://github.com/kth-step/HolBA/blob/05e86baaccda36f35ae1b03a4acfaf72dcc68c45/src/theory/tools/wp/bir_wp_simpScript.sml#L220) - [src/theory/tools/wp/bir_wp_simpScript.sml, line 726](https://github.com/kth-step/HolBA/blob/05e86baaccda36f35ae1b03a4acfaf72dcc68c45/src/theory/tools/wp/bir_wp_simpScript.sml#L726) - [src/theory/tools/wp/bir_wp_simpScript.sml, line 1293](https://github.com/kth-step/HolBA/blob/05e86baaccda36f35ae1b03a4acfaf72dcc68c45/src/theory/tools/wp/bir_wp_simpScript.sml#L1293) - [src/theory/tools/wp/bir_wp_simpScript.sml, line 4513](https://github.com/kth-step/HolBA/blob/05e86baaccda36f35ae1b03a4acfaf72dcc68c45/src/theory/tools/wp/bir_wp_simpScript.sml#L4513) - [src/theory/tools/wp/bir_wpScript.sml, line 171](https://github.com/kth-step/HolBA/blob/05e86baaccda36f35ae1b03a4acfaf72dcc68c45/src/theory/tools/wp/bir_wpScript.sml#L171) - [src/theory/tools/wp/bir_wpScript.sml, line 227](https://github.com/kth-step/HolBA/blob/05e86baaccda36f35ae1b03a4acfaf72dcc68c45/src/theory/tools/wp/bir_wpScript.sml#L227) - [src/theory/tools/lifter/bir_inst_liftingScript.sml, line 31](https://github.com/kth-step/HolBA/blob/05e86baaccda36f35ae1b03a4acfaf72dcc68c45/src/theory/tools/lifter/bir_inst_liftingScript.sml#L31) - [src/theory/tools/lifter/bir_inst_liftingScript.sml, line 42](https://github.com/kth-step/HolBA/blob/05e86baaccda36f35ae1b03a4acfaf72dcc68c45/src/theory/tools/lifter/bir_inst_liftingScript.sml#L42) - [src/tools/wp/bir_wp_simpLib.sml, line 134](https://github.com/kth-step/HolBA/blob/05e86baaccda36f35ae1b03a4acfaf72dcc68c45/src/tools/wp/bir_wp_simpLib.sml#L134) - [src/tools/wp/bir_wp_simpLib.sml, line 386](https://github.com/kth-step/HolBA/blob/05e86baaccda36f35ae1b03a4acfaf72dcc68c45/src/tools/wp/bir_wp_simpLib.sml#L386) - [src/tools/wp/bir_wp_simpLib.sml, line 534](https://github.com/kth-step/HolBA/blob/05e86baaccda36f35ae1b03a4acfaf72dcc68c45/src/tools/wp/bir_wp_simpLib.sml#L534) - [src/tools/wp/bir_wp_simpLib.sml, line 538](https://github.com/kth-step/HolBA/blob/05e86baaccda36f35ae1b03a4acfaf72dcc68c45/src/tools/wp/bir_wp_simpLib.sml#L538) - [src/tools/wp/bir_wp_simpLib.sml, line 568](https://github.com/kth-step/HolBA/blob/05e86baaccda36f35ae1b03a4acfaf72dcc68c45/src/tools/wp/bir_wp_simpLib.sml#L568) - [src/tools/wp/bir_wp_simpLib.sml, line 644](https://github.com/kth-step/HolBA/blob/05e86baaccda36f35ae1b03a4acfaf72dcc68c45/src/tools/wp/bir_wp_simpLib.sml#L644) - [src/tools/wp/bir_wpLib.sml, line 40](https://github.com/kth-step/HolBA/blob/05e86baaccda36f35ae1b03a4acfaf72dcc68c45/src/tools/wp/bir_wpLib.sml#L40) - [src/tools/wp/bir_wpLib.sml, line 95](https://github.com/kth-step/HolBA/blob/05e86baaccda36f35ae1b03a4acfaf72dcc68c45/src/tools/wp/bir_wpLib.sml#L95) - [src/tools/wp/bir_wpLib.sml, line 136](https://github.com/kth-step/HolBA/blob/05e86baaccda36f35ae1b03a4acfaf72dcc68c45/src/tools/wp/bir_wpLib.sml#L136) - [src/tools/wp/bir_wpLib.sml, line 142](https://github.com/kth-step/HolBA/blob/05e86baaccda36f35ae1b03a4acfaf72dcc68c45/src/tools/wp/bir_wpLib.sml#L142) - [src/tools/wp/bir_wpLib.sml, line 149](https://github.com/kth-step/HolBA/blob/05e86baaccda36f35ae1b03a4acfaf72dcc68c45/src/tools/wp/bir_wpLib.sml#L149) - [src/tools/wp/bir_wpLib.sml, line 154](https://github.com/kth-step/HolBA/blob/05e86baaccda36f35ae1b03a4acfaf72dcc68c45/src/tools/wp/bir_wpLib.sml#L154) - [src/tools/wp/bir_wpLib.sml, line 192](https://github.com/kth-step/HolBA/blob/05e86baaccda36f35ae1b03a4acfaf72dcc68c45/src/tools/wp/bir_wpLib.sml#L192) - [src/tools/wp/bir_wpLib.sml, line 206](https://github.com/kth-step/HolBA/blob/05e86baaccda36f35ae1b03a4acfaf72dcc68c45/src/tools/wp/bir_wpLib.sml#L206) - [src/tools/wp/bir_wpLib.sml, line 255](https://github.com/kth-step/HolBA/blob/05e86baaccda36f35ae1b03a4acfaf72dcc68c45/src/tools/wp/bir_wpLib.sml#L255) - [src/tools/wp/bir_wpLib.sml, line 262](https://github.com/kth-step/HolBA/blob/05e86baaccda36f35ae1b03a4acfaf72dcc68c45/src/tools/wp/bir_wpLib.sml#L262) - [src/tools/wp/bir_wpLib.sml, line 265](https://github.com/kth-step/HolBA/blob/05e86baaccda36f35ae1b03a4acfaf72dcc68c45/src/tools/wp/bir_wpLib.sml#L265) - [src/tools/wp/bir_wpLib.sml, line 271](https://github.com/kth-step/HolBA/blob/05e86baaccda36f35ae1b03a4acfaf72dcc68c45/src/tools/wp/bir_wpLib.sml#L271) - [src/tools/pass/bir_passificationLib.sml, line 62](https://github.com/kth-step/HolBA/blob/05e86baaccda36f35ae1b03a4acfaf72dcc68c45/src/tools/pass/bir_passificationLib.sml#L62) - [src/tools/pass/bir_passificationLib.sml, line 306](https://github.com/kth-step/HolBA/blob/05e86baaccda36f35ae1b03a4acfaf72dcc68c45/src/tools/pass/bir_passificationLib.sml#L306) - [src/tools/cfg/bir_cfgLib.sml, line 169](https://github.com/kth-step/HolBA/blob/05e86baaccda36f35ae1b03a4acfaf72dcc68c45/src/tools/cfg/bir_cfgLib.sml#L169) - [src/tools/cfg/bir_cfgLib.sml, line 188](https://github.com/kth-step/HolBA/blob/05e86baaccda36f35ae1b03a4acfaf72dcc68c45/src/tools/cfg/bir_cfgLib.sml#L188) - [src/tools/cfg/bir_cfgLib.sml, line 191](https://github.com/kth-step/HolBA/blob/05e86baaccda36f35ae1b03a4acfaf72dcc68c45/src/tools/cfg/bir_cfgLib.sml#L191) - [src/tools/cfg/bir_cfgLib.sml, line 193](https://github.com/kth-step/HolBA/blob/05e86baaccda36f35ae1b03a4acfaf72dcc68c45/src/tools/cfg/bir_cfgLib.sml#L193) - [src/tools/cfg/bir_cfgLib.sml, line 381](https://github.com/kth-step/HolBA/blob/05e86baaccda36f35ae1b03a4acfaf72dcc68c45/src/tools/cfg/bir_cfgLib.sml#L381) - [src/tools/cfg/bir_cfgLib.sml, line 386](https://github.com/kth-step/HolBA/blob/05e86baaccda36f35ae1b03a4acfaf72dcc68c45/src/tools/cfg/bir_cfgLib.sml#L386) - [src/tools/cfg/bir_cfgLib.sml, line 388](https://github.com/kth-step/HolBA/blob/05e86baaccda36f35ae1b03a4acfaf72dcc68c45/src/tools/cfg/bir_cfgLib.sml#L388) - [src/tools/lifter/selftest.sml, line 511](https://github.com/kth-step/HolBA/blob/05e86baaccda36f35ae1b03a4acfaf72dcc68c45/src/tools/lifter/selftest.sml#L511) - [src/tools/lifter/bir_inst_liftingLib.sml, line 419](https://github.com/kth-step/HolBA/blob/05e86baaccda36f35ae1b03a4acfaf72dcc68c45/src/tools/lifter/bir_inst_liftingLib.sml#L419) - [src/tools/lifter/bir_inst_liftingLib.sml, line 1207](https://github.com/kth-step/HolBA/blob/05e86baaccda36f35ae1b03a4acfaf72dcc68c45/src/tools/lifter/bir_inst_liftingLib.sml#L1207) - [src/tools/exec/examples/example-toy.sml, line 52](https://github.com/kth-step/HolBA/blob/05e86baaccda36f35ae1b03a4acfaf72dcc68c45/src/tools/exec/examples/example-toy.sml#L52) - [src/tools/exec/examples/example-toy.sml, line 62](https://github.com/kth-step/HolBA/blob/05e86baaccda36f35ae1b03a4acfaf72dcc68c45/src/tools/exec/examples/example-toy.sml#L62) - [src/tools/exec/bir_exec_typingLib.sml, line 64](https://github.com/kth-step/HolBA/blob/05e86baaccda36f35ae1b03a4acfaf72dcc68c45/src/tools/exec/bir_exec_typingLib.sml#L64) - [src/tools/exec/bir_exec_typingLib.sml, line 80](https://github.com/kth-step/HolBA/blob/05e86baaccda36f35ae1b03a4acfaf72dcc68c45/src/tools/exec/bir_exec_typingLib.sml#L80) - [src/tools/exec/bir_exec_envLib.sml, line 55](https://github.com/kth-step/HolBA/blob/05e86baaccda36f35ae1b03a4acfaf72dcc68c45/src/tools/exec/bir_exec_envLib.sml#L55) - [src/tools/exec/bir_exec_envLib.sml, line 63](https://github.com/kth-step/HolBA/blob/05e86baaccda36f35ae1b03a4acfaf72dcc68c45/src/tools/exec/bir_exec_envLib.sml#L63) - [src/tools/exec/bir_exec_expLib.sml, line 147](https://github.com/kth-step/HolBA/blob/05e86baaccda36f35ae1b03a4acfaf72dcc68c45/src/tools/exec/bir_exec_expLib.sml#L147) - [src/tools/exec/bir_exec_expLib.sml, line 148](https://github.com/kth-step/HolBA/blob/05e86baaccda36f35ae1b03a4acfaf72dcc68c45/src/tools/exec/bir_exec_expLib.sml#L148) - [src/tools/scamv/examples/driver-test.sml, line 25](https://github.com/kth-step/HolBA/blob/05e86baaccda36f35ae1b03a4acfaf72dcc68c45/src/tools/scamv/examples/driver-test.sml#L25) - [src/tools/scamv/examples/run-test.sml, line 77](https://github.com/kth-step/HolBA/blob/05e86baaccda36f35ae1b03a4acfaf72dcc68c45/src/tools/scamv/examples/run-test.sml#L77) - [src/tools/scamv/bir_symb_execLib.sml, line 140](https://github.com/kth-step/HolBA/blob/05e86baaccda36f35ae1b03a4acfaf72dcc68c45/src/tools/scamv/bir_symb_execLib.sml#L140)

Click here for details

``` src/shared/bir_exp_to_wordsLib.sml-508- (BExp_BinPred BIExp_LessThan (BExp_Const (Imm64 112w)) (BExp_Const (Imm64 11w))) src/shared/bir_exp_to_wordsLib.sml-509- (BExp_Const (Imm64 200w)) src/shared/bir_exp_to_wordsLib.sml-510- (BExp_Const (Imm64 404w))`` src/shared/bir_exp_to_wordsLib.sml-511- ``if (112w :word64) <₊ (11w :word64) src/shared/bir_exp_to_wordsLib.sml-512- then (200w :word64) src/shared/bir_exp_to_wordsLib.sml-513- else (404w :word64)``; src/shared/bir_exp_to_wordsLib.sml:514: (* TODO: Write tests for store and loads *) src/shared/bir_exp_to_wordsLib.sml-515- in () end; src/shared/bir_exp_to_wordsLib.sml-516- src/shared/bir_exp_to_wordsLib.sml-517- end (* local *) src/shared/bir_exp_to_wordsLib.sml-518- src/shared/bir_exp_to_wordsLib.sml-519-end (* bir_exp_to_wordsLib *) src/shared/bir_exp_to_wordsLib.sml-520- -- src/theory/bir-support/bir_program_no_assumeScript.sml-373- FULL_SIMP_TAC std_ss [optionTheory.IS_SOME_EXISTS] >> src/theory/bir-support/bir_program_no_assumeScript.sml-374- FULL_SIMP_TAC (std_ss++holBACore_ss) [] >> src/theory/bir-support/bir_program_no_assumeScript.sml-375- PAT_X_ASSUM ``(ol,nstep,npc,st'') = _`` src/theory/bir-support/bir_program_no_assumeScript.sml-376- (fn thm => ASSUME_TAC src/theory/bir-support/bir_program_no_assumeScript.sml-377- (GSYM thm) src/theory/bir-support/bir_program_no_assumeScript.sml-378- ) >> src/theory/bir-support/bir_program_no_assumeScript.sml:379: (* TODO: The below finish is ugly... *) src/theory/bir-support/bir_program_no_assumeScript.sml-380- Cases_on `(bir_exec_block_n prog st' n)` >> src/theory/bir-support/bir_program_no_assumeScript.sml-381- Cases_on `r` >> src/theory/bir-support/bir_program_no_assumeScript.sml-382- Cases_on `r'` >> src/theory/bir-support/bir_program_no_assumeScript.sml-383- FULL_SIMP_TAC (std_ss++holBACore_ss) [], src/theory/bir-support/bir_program_no_assumeScript.sml-384- src/theory/bir-support/bir_program_no_assumeScript.sml-385- FULL_SIMP_TAC (std_ss++holBACore_ss) [] >> -- src/theory/bir-support/bir_exp_congruencesScript.sml-161-SIMP_TAC (std_ss++holBACore_ss) [bir_exp_CONG_def, src/theory/bir-support/bir_exp_congruencesScript.sml-162- bir_env_vars_are_initialised_UNION, type_of_bir_exp_def] >> src/theory/bir-support/bir_exp_congruencesScript.sml-163-REPEAT STRIP_TAC >> ASM_SIMP_TAC std_ss []); src/theory/bir-support/bir_exp_congruencesScript.sml-164- src/theory/bir-support/bir_exp_congruencesScript.sml-165- src/theory/bir-support/bir_exp_congruencesScript.sml-166-(* Now real simplifications. src/theory/bir-support/bir_exp_congruencesScript.sml:167: TODO: Add Many more! *) src/theory/bir-support/bir_exp_congruencesScript.sml-168- src/theory/bir-support/bir_exp_congruencesScript.sml-169-val bir_exp_CONG_simp_IDEMPOTENT_AND = store_thm ("bir_exp_CONG_simp_IDEMPOTENT_AND", src/theory/bir-support/bir_exp_congruencesScript.sml-170- ``!e. src/theory/bir-support/bir_exp_congruencesScript.sml-171- (?ty. bir_type_is_Imm ty /\ (type_of_bir_exp e = SOME ty)) ==> src/theory/bir-support/bir_exp_congruencesScript.sml-172- bir_exp_CONG (BExp_BinExp BIExp_And e e) e``, src/theory/bir-support/bir_exp_congruencesScript.sml-173- -- src/theory/bir-support/bir_exp_congruencesScript.sml-356- METIS_TAC[type_of_bir_exp_THM_with_init_vars] >> src/theory/bir-support/bir_exp_congruencesScript.sml-357-Cases_on `bir_eval_exp c env` >> ( src/theory/bir-support/bir_exp_congruencesScript.sml-358- FULL_SIMP_TAC (std_ss++holBACore_ss) [bir_eval_bin_exp_def, BType_Bool_def] src/theory/bir-support/bir_exp_congruencesScript.sml-359-)); src/theory/bir-support/bir_exp_congruencesScript.sml-360- src/theory/bir-support/bir_exp_congruencesScript.sml-361- src/theory/bir-support/bir_exp_congruencesScript.sml:362:(* TODO: ADD MANY MORE! *) src/theory/bir-support/bir_exp_congruencesScript.sml-363- src/theory/bir-support/bir_exp_congruencesScript.sml-364- src/theory/bir-support/bir_exp_congruencesScript.sml-365-val _ = export_theory(); -- src/theory/tools/wp/bir_wp_simpScript.sml-23- src/theory/tools/wp/bir_wp_simpScript.sml-24-val bir_var_ss = rewrites (type_rws ``:bir_var_t``); src/theory/tools/wp/bir_wp_simpScript.sml-25-val string_t_ss = rewrites (type_rws ``:string``); src/theory/tools/wp/bir_wp_simpScript.sml-26- src/theory/tools/wp/bir_wp_simpScript.sml-27- src/theory/tools/wp/bir_wp_simpScript.sml-28- src/theory/tools/wp/bir_wp_simpScript.sml:29:(* TODO: memory load store updates *) src/theory/tools/wp/bir_wp_simpScript.sml-30- src/theory/tools/wp/bir_wp_simpScript.sml-31-(* Definitions moved to theories/bir_bool_expScript.sml: src/theory/tools/wp/bir_wp_simpScript.sml-32- * - bir_exp_and src/theory/tools/wp/bir_wp_simpScript.sml-33- * - bir_exp_or src/theory/tools/wp/bir_wp_simpScript.sml-34- * - bir_exp_not src/theory/tools/wp/bir_wp_simpScript.sml-35- * - bir_exp_imp -- src/theory/tools/wp/bir_wp_simpScript.sml-214-); src/theory/tools/wp/bir_wp_simpScript.sml-215- src/theory/tools/wp/bir_wp_simpScript.sml-216- src/theory/tools/wp/bir_wp_simpScript.sml-217-val bir_var_set_is_well_typed_UNION_initialised_thm = store_thm("bir_var_set_is_well_typed_UNION_initialised_thm", `` src/theory/tools/wp/bir_wp_simpScript.sml-218- !e1vs e2vs env. src/theory/tools/wp/bir_wp_simpScript.sml-219-(* src/theory/tools/wp/bir_wp_simpScript.sml:220:TODO: the first two assumptions are not neccessary i believe src/theory/tools/wp/bir_wp_simpScript.sml-221-*) src/theory/tools/wp/bir_wp_simpScript.sml-222- (bir_var_set_is_well_typed e1vs) ==> src/theory/tools/wp/bir_wp_simpScript.sml-223- (bir_var_set_is_well_typed e2vs) ==> src/theory/tools/wp/bir_wp_simpScript.sml-224- (bir_env_vars_are_initialised env (e1vs UNION e2vs)) ==> src/theory/tools/wp/bir_wp_simpScript.sml-225- (bir_var_set_is_well_typed (e1vs UNION e2vs)) src/theory/tools/wp/bir_wp_simpScript.sml-226-``, -- src/theory/tools/wp/bir_wp_simpScript.sml-720- FULL_SIMP_TAC (std_ss) [bir_typing_expTheory.type_of_bir_exp_EQ_SOME_REWRS, type_of_bir_val_def, type_of_bir_imm_def] >> src/theory/tools/wp/bir_wp_simpScript.sml-721- PAT_X_ASSUM ``(A:bir_immtype_t) = (s:bir_immtype_t)`` (ASSUME_TAC o GSYM) >> src/theory/tools/wp/bir_wp_simpScript.sml-722- FULL_SIMP_TAC (std_ss++bir_immtype_ss) [] src/theory/tools/wp/bir_wp_simpScript.sml-723- ) src/theory/tools/wp/bir_wp_simpScript.sml-724-); src/theory/tools/wp/bir_wp_simpScript.sml-725- src/theory/tools/wp/bir_wp_simpScript.sml:726:(* TODO: simplify the following congruence proofs by introducing theorems to enable use of automation *) src/theory/tools/wp/bir_wp_simpScript.sml-727-val bir_exp_CONG_de_morgan_or_thm = store_thm("bir_exp_CONG_de_morgan_or_thm", `` src/theory/tools/wp/bir_wp_simpScript.sml-728- !e1 e2. src/theory/tools/wp/bir_wp_simpScript.sml-729- (bir_exp_CONG (bir_exp_not (bir_exp_or e1 e2)) (bir_exp_and (bir_exp_not e1) (bir_exp_not e2))) src/theory/tools/wp/bir_wp_simpScript.sml-730-``, src/theory/tools/wp/bir_wp_simpScript.sml-731- src/theory/tools/wp/bir_wp_simpScript.sml-732- REPEAT STRIP_TAC >> -- src/theory/tools/wp/bir_wp_simpScript.sml-1287- ) src/theory/tools/wp/bir_wp_simpScript.sml-1288-); src/theory/tools/wp/bir_wp_simpScript.sml-1289- src/theory/tools/wp/bir_wp_simpScript.sml-1290- src/theory/tools/wp/bir_wp_simpScript.sml-1291-(* --------------------------------------------- more ------------------------------------------------ *) src/theory/tools/wp/bir_wp_simpScript.sml-1292- src/theory/tools/wp/bir_wp_simpScript.sml:1293:(* TODO: should be in bir_exp_substitutionsTheory *) src/theory/tools/wp/bir_wp_simpScript.sml-1294- src/theory/tools/wp/bir_wp_simpScript.sml-1295-(* src/theory/tools/wp/bir_wp_simpScript.sml-1296- src/theory/tools/wp/bir_wp_simpScript.sml-1297-val thm = SIMP_CONV (std_ss) [bir_exp_subst_update_REWRS] ``bir_exp_subst_update (FUPDATE (FUPDATE FEMPTY (BVar "h" (BType_Imm Bit8),BExp_Den (BVar "h1" (BType_Imm Bit8)))) (BVar "k" (BType_Imm Bit8),BExp_Den (BVar "k1" (BType_Imm Bit8)))) (FUPDATE FEMPTY (BVar "h1" (BType_Imm Bit8),BExp_Den (BVar "h1" (BType_Imm Bit16))))``; src/theory/tools/wp/bir_wp_simpScript.sml-1298-val thm = TRANS thm ((EVAL o snd o dest_eq o concl) thm); src/theory/tools/wp/bir_wp_simpScript.sml-1299- -- src/theory/tools/wp/bir_wp_simpScript.sml-4507-*) src/theory/tools/wp/bir_wp_simpScript.sml-4508- src/theory/tools/wp/bir_wp_simpScript.sml-4509- cheat src/theory/tools/wp/bir_wp_simpScript.sml-4510-); src/theory/tools/wp/bir_wp_simpScript.sml-4511- src/theory/tools/wp/bir_wp_simpScript.sml-4512- src/theory/tools/wp/bir_wp_simpScript.sml:4513:(* TODO: should probably be somewhere else *) src/theory/tools/wp/bir_wp_simpScript.sml-4514-val bir_exp_conj_from_list_def = Define ` src/theory/tools/wp/bir_wp_simpScript.sml-4515- bir_exp_conj_from_list = FOLDL (\expa. \exp. BExp_BinExp BIExp_And expa exp) (BExp_Const (Imm1 1w)) src/theory/tools/wp/bir_wp_simpScript.sml-4516-`; src/theory/tools/wp/bir_wp_simpScript.sml-4517- src/theory/tools/wp/bir_wp_simpScript.sml-4518- src/theory/tools/wp/bir_wp_simpScript.sml-4519-val bir_wp_simp_eval_subst_thm = store_thm("bir_wp_simp_eval_subst_thm", `` -- src/theory/tools/wp/bir_wpScript.sml-165- src/theory/tools/wp/bir_wpScript.sml-166-(* Preservation of valid status for the Assume statement *) src/theory/tools/wp/bir_wpScript.sml-167-val bir_assume_valid_status = src/theory/tools/wp/bir_wpScript.sml-168- store_thm("bir_assume_valid_status", src/theory/tools/wp/bir_wpScript.sml-169- ``!s s' ex post obs. src/theory/tools/wp/bir_wpScript.sml-170- bir_is_valid_status s ==> src/theory/tools/wp/bir_wpScript.sml:171: (* TODO: We need some type of antecedent to guarantee Failed src/theory/tools/wp/bir_wpScript.sml-172- * does not occur. This could be either Booleanity+var.init. src/theory/tools/wp/bir_wpScript.sml-173- * or the Assume precondition. *) src/theory/tools/wp/bir_wpScript.sml-174- bir_is_bool_exp_env s.bst_environ src/theory/tools/wp/bir_wpScript.sml-175- (BExp_BinExp BIExp_Or (BExp_UnaryExp BIExp_Not ex) post) ==> src/theory/tools/wp/bir_wpScript.sml-176- (bir_exec_stmtB (BStmt_Assume ex) s = (obs,s')) ==> src/theory/tools/wp/bir_wpScript.sml-177- bir_is_valid_status s'``, -- src/theory/tools/wp/bir_wpScript.sml-221- bir_exec_stmt_assume_def, src/theory/tools/wp/bir_wpScript.sml-222- bir_dest_bool_val_TF] src/theory/tools/wp/bir_wpScript.sml-223-); src/theory/tools/wp/bir_wpScript.sml-224- src/theory/tools/wp/bir_wpScript.sml-225-(* Given the Assumed expression not holding in the initial src/theory/tools/wp/bir_wpScript.sml-226- * state, the final state will have status AssumptionViolated. *) src/theory/tools/wp/bir_wpScript.sml:227:(* TODO: This theorem could also be stated with the precondition src/theory/tools/wp/bir_wpScript.sml-228- * holding instead of Booleanity holding. This antecedent is src/theory/tools/wp/bir_wpScript.sml-229- * needed to translate "not equal to True" to "equal to False". *) src/theory/tools/wp/bir_wpScript.sml-230-val bir_assume_assumviol = src/theory/tools/wp/bir_wpScript.sml-231- store_thm("bir_assume_assumviol", src/theory/tools/wp/bir_wpScript.sml-232- ``!s s' ex post obs. src/theory/tools/wp/bir_wpScript.sml-233- bir_is_bool_exp_env s.bst_environ -- src/theory/tools/lifter/bir_inst_liftingScript.sml-25- to be corresponding to a machine instruction *) src/theory/tools/lifter/bir_inst_liftingScript.sml-26- src/theory/tools/lifter/bir_inst_liftingScript.sml-27-val _ = new_theory "bir_inst_lifting"; src/theory/tools/lifter/bir_inst_liftingScript.sml-28- src/theory/tools/lifter/bir_inst_liftingScript.sml-29- src/theory/tools/lifter/bir_inst_liftingScript.sml-30- src/theory/tools/lifter/bir_inst_liftingScript.sml:31:(* TODO: find a better place for this. bmr_ss is now created in 3 src/theory/tools/lifter/bir_inst_liftingScript.sml-32- places and there are probably more like this in the lifter *) src/theory/tools/lifter/bir_inst_liftingScript.sml-33-val bmr_REWRS = ( src/theory/tools/lifter/bir_inst_liftingScript.sml-34- (type_rws ``:('a, 'b, 'c) bir_lifting_machine_rec_t``) @ src/theory/tools/lifter/bir_inst_liftingScript.sml-35- (type_rws ``:'a bir_machine_lifted_pc_t``) @ src/theory/tools/lifter/bir_inst_liftingScript.sml-36- (type_rws ``:'a bir_machine_lifted_imm_t``) @ src/theory/tools/lifter/bir_inst_liftingScript.sml-37- (type_rws ``:('a, 'b, 'c) bir_machine_lifted_mem_t``) src/theory/tools/lifter/bir_inst_liftingScript.sml-38-) src/theory/tools/lifter/bir_inst_liftingScript.sml-39-; src/theory/tools/lifter/bir_inst_liftingScript.sml-40- src/theory/tools/lifter/bir_inst_liftingScript.sml-41-val bmr_ss = rewrites bmr_REWRS src/theory/tools/lifter/bir_inst_liftingScript.sml:42:(* TODO: end of TODO todo above*) src/theory/tools/lifter/bir_inst_liftingScript.sml-43- src/theory/tools/lifter/bir_inst_liftingScript.sml-44- src/theory/tools/lifter/bir_inst_liftingScript.sml-45-(*****************************) src/theory/tools/lifter/bir_inst_liftingScript.sml-46-(* Unchanged memory interval *) src/theory/tools/lifter/bir_inst_liftingScript.sml-47-(*****************************) src/theory/tools/lifter/bir_inst_liftingScript.sml-48- -- src/tools/wp/bir_wp_simpLib.sml-128- bir_exp_varsubst_introduced_vars_REWRS, src/tools/wp/bir_wp_simpLib.sml-129- finite_mapTheory.FDOM_FEMPTY, src/tools/wp/bir_wp_simpLib.sml-130- finite_mapTheory.FDOM_FUPDATE, src/tools/wp/bir_wp_simpLib.sml-131- bir_exp_varsubst1_def src/tools/wp/bir_wp_simpLib.sml-132- ]@varexps_thms); src/tools/wp/bir_wp_simpLib.sml-133- src/tools/wp/bir_wp_simpLib.sml:134: (* TODO: this has to be touched again, new expressions may contain varsubst *) src/tools/wp/bir_wp_simpLib.sml-135- val simp_conv_for_bir_var_set_is_well_typed1 = SIMP_CONV src/tools/wp/bir_wp_simpLib.sml-136- (std_ss++stringSimps.STRING_ss++string_ss++char_ss) []; src/tools/wp/bir_wp_simpLib.sml-137- val simp_conv_for_bir_var_set_is_well_typed2 = computeLib.RESTR_EVAL_CONV [``bir_var_set_is_well_typed``]; src/tools/wp/bir_wp_simpLib.sml-138- val simp_conv_for_bir_var_set_is_well_typed3 = SIMP_CONV pure_ss [GSYM listTheory.LIST_TO_SET, src/tools/wp/bir_wp_simpLib.sml-139- bir_var_set_is_well_typed_REWRS]; src/tools/wp/bir_wp_simpLib.sml-140- -- src/tools/wp/bir_wp_simpLib.sml-380- fun bir_wp_simp_step_CONV_conv_2_impl recStepFun rec_step_CONV prem term varexps_thms (goalterm:term) (extra_wt_varset:term option) wt0_thm = src/tools/wp/bir_wp_simpLib.sml-381- let src/tools/wp/bir_wp_simpLib.sml-382- val rulename = "2 impl"; src/tools/wp/bir_wp_simpLib.sml-383- val _ = enterRule rulename; src/tools/wp/bir_wp_simpLib.sml-384- src/tools/wp/bir_wp_simpLib.sml-385- val (e1, e2) = dest_bir_exp_imp term; src/tools/wp/bir_wp_simpLib.sml:386: val thm_gen = (Q.GENL [`prem`, `e1`, `e2`]) (MATCH_MP bir_exp_tautologiesTheory.bir_exp_is_taut_WEAK_CONG_IFF (Q.SPECL [`prem`, `e1`, `e2`, `fixme`] bir_exp_CONG_imp_imp_thm)); src/tools/wp/bir_wp_simpLib.sml-387- val thm_1 = SPECL [prem, e1, e2] thm_gen; src/tools/wp/bir_wp_simpLib.sml-388- val wt_thm_gen = case extra_wt_varset of src/tools/wp/bir_wp_simpLib.sml-389- NONE => ((REWRITE_RULE [pred_setTheory.UNION_EMPTY]) o (Q.GENL [`prem`, `e1`, `e2`]) o (SPEC emptyvarset) o (Q.SPECL [`prem`, `e1`, `e2`])) bir_wp_simp_varset_imp_wunions_thm src/tools/wp/bir_wp_simpLib.sml-390- | SOME x => bir_wp_simp_varset_imp_wunions_thm; src/tools/wp/bir_wp_simpLib.sml-391- val wt_thm_1 = case extra_wt_varset of src/tools/wp/bir_wp_simpLib.sml-392- NONE => SPECL [prem, e1, e2] wt_thm_gen -- src/tools/wp/bir_wp_simpLib.sml-528- val _ = enterRule rulename; src/tools/wp/bir_wp_simpLib.sml-529- src/tools/wp/bir_wp_simpLib.sml-530- val (term_vs, term_e) = dest_bir_exp_varsubst term; src/tools/wp/bir_wp_simpLib.sml-531- val (term_v, term_ve, term_e2) = dest_bir_exp_subst1 term_e; src/tools/wp/bir_wp_simpLib.sml-532- val thm_1 = SPECL [term_vs, term_v, term_ve, term_e2] bir_exp_varsubst_subst1_swap_thm; src/tools/wp/bir_wp_simpLib.sml-533- val assum = (fst o dest_imp o concl) thm_1; src/tools/wp/bir_wp_simpLib.sml:534: val feveryvarneq_conv = SIMP_CONV (std_ss++pred_setSimps.PRED_SET_ss++HolBACoreSimps.holBACore_ss++stringSimps.STRING_ss++string_ss++char_ss) [finite_mapTheory.FEVERY_FEMPTY, finite_mapTheory.FEVERY_FUPDATE, finite_mapTheory.DRESTRICT_FUPDATE, finite_mapTheory.DRESTRICT_FEMPTY]; (* TODO: this has to be touched again *) src/tools/wp/bir_wp_simpLib.sml-535- val assum_thm = REWRITE_RULE [boolTheory.EQ_CLAUSES] (feveryvarneq_conv assum); src/tools/wp/bir_wp_simpLib.sml-536- val thm_2 = MP thm_1 assum_thm; src/tools/wp/bir_wp_simpLib.sml-537- val restrict1_conv = SIMP_CONV (std_ss++HolBACoreSimps.holBACore_ss++stringSimps.STRING_ss++string_ss++char_ss) [bir_exp_subst_restrict1_REWRS, bir_exp_varsubst_REWRS, bir_exp_varsubst_REWRS_ALT, bir_exp_varsubst_var_REWR, finite_mapTheory.FLOOKUP_UPDATE, finite_mapTheory.FLOOKUP_EMPTY, LET_DEF]; src/tools/wp/bir_wp_simpLib.sml:538: val thm_2 = TRANS thm_2 ((restrict1_conv o get_concl_rhs) thm_2); (* TODO: this as well, add holbasimps *) src/tools/wp/bir_wp_simpLib.sml-539- val thm_3 = REWRITE_CONV [thm_2] goalterm; src/tools/wp/bir_wp_simpLib.sml-540- val thm_in = thm_3; (* val goalterm = get_concl_rhs thm_in; *) src/tools/wp/bir_wp_simpLib.sml-541- val wt_thm_in = REWRITE_CONV [thm_2] (simp_construct_wt (prem, term) extra_wt_varset); src/tools/wp/bir_wp_simpLib.sml-542- val _ = exitRule rulename; src/tools/wp/bir_wp_simpLib.sml-543- in src/tools/wp/bir_wp_simpLib.sml-544- recStepFun (thm_in, wt_thm_in) extra_wt_varset (EQ_MP wt_thm_in wt0_thm) -- src/tools/wp/bir_wp_simpLib.sml-562- val term_v_is_Imm_thm = REWRITE_CONV [bir_var_type_def, bir_type_checker_REWRS] ``bir_type_is_Imm (bir_var_type ^term_v)``; src/tools/wp/bir_wp_simpLib.sml-563- val term_v_is_Imm_thm = REWRITE_RULE [boolTheory.EQ_CLAUSES] term_v_is_Imm_thm; src/tools/wp/bir_wp_simpLib.sml-564- val term_v_is_Mem_thm = REWRITE_CONV [bir_var_type_def, bir_type_checker_REWRS] ``bir_type_is_Mem (bir_var_type ^term_v)``; src/tools/wp/bir_wp_simpLib.sml-565- val term_v_is_Mem_thm = REWRITE_RULE [boolTheory.EQ_CLAUSES] term_v_is_Mem_thm; src/tools/wp/bir_wp_simpLib.sml-566- src/tools/wp/bir_wp_simpLib.sml-567-(* well_typed_conv varexps_thms ``^term_v IN (bir_vars_of_exp ^term_e)``*) src/tools/wp/bir_wp_simpLib.sml:568: val varused_thm = SIMP_CONV (std_ss++pred_setSimps.PRED_SET_ss++HolBACoreSimps.holBACore_ss++stringSimps.STRING_ss++string_ss++char_ss) ([bir_exp_varsubst_USED_VARS, bir_exp_subst1_USED_VARS, bir_exp_varsubst_introduced_vars_REWRS, finite_mapTheory.FDOM_FEMPTY, finite_mapTheory.FDOM_FUPDATE]@varexps_thms) ``^term_v IN (bir_vars_of_exp ^term_e)``; (* TODO: has to be touched again *) src/tools/wp/bir_wp_simpLib.sml-569- val varused_thm = REWRITE_RULE [boolTheory.EQ_CLAUSES] varused_thm; src/tools/wp/bir_wp_simpLib.sml-570- in src/tools/wp/bir_wp_simpLib.sml-571- if ((is_neg o concl) varused_thm) then src/tools/wp/bir_wp_simpLib.sml-572- (* raise ERR "bir_wp_simp_CONV" "rule 6 missing" *) src/tools/wp/bir_wp_simpLib.sml-573- let src/tools/wp/bir_wp_simpLib.sml-574- val thm_1 = SPECL [term_v, term_ve, term_e] bir_exp_subst1_UNUSED_VAR; -- src/tools/wp/bir_wp_simpLib.sml-638- (REWRITE_CONV [pred_setTheory.NOT_IN_EMPTY]) THENC src/tools/wp/bir_wp_simpLib.sml-639- (SIMP_CONV (std_ss++HolBACoreSimps.holBACore_ss++stringSimps.STRING_ss++string_ss++char_ss) []); src/tools/wp/bir_wp_simpLib.sml-640-(* val v2_in_set_thm = varname_in_set_conv ``(bir_var_name ^term_v2) IN ("A2" INSERT "B5" INSERT ^(get_concl_rhs varnameset_exp_thm))``;*) src/tools/wp/bir_wp_simpLib.sml-641- src/tools/wp/bir_wp_simpLib.sml-642- val varnameset_exp_thm = varnameset_conv ``IMAGE bir_var_name (bir_vars_of_exp ^term_exp)`` handle UNCHANGED => raise ERR "bir_wp_simp_CONV" ("varnameset "^varname^" not resolvable"); src/tools/wp/bir_wp_simpLib.sml-643- val v2_in_set_thm = varname_in_set_conv ``(bir_var_name ^term_v2) IN (^(get_concl_rhs varnameset_exp_thm))``; src/tools/wp/bir_wp_simpLib.sml:644: val assum_thm = REWRITE_RULE [boolTheory.EQ_CLAUSES] v2_in_set_thm; (* TODO: add neg conclusion check for debug error messages *) src/tools/wp/bir_wp_simpLib.sml-645- val thm_1 = MP (REWRITE_RULE [varnameset_exp_thm] thm_1) assum_thm; src/tools/wp/bir_wp_simpLib.sml-646- in src/tools/wp/bir_wp_simpLib.sml-647- thm_1 src/tools/wp/bir_wp_simpLib.sml-648- end; src/tools/wp/bir_wp_simpLib.sml-649- src/tools/wp/bir_wp_simpLib.sml-650- fun varnameset_discharge_cheat thm_1 varname term_exp term_v2 = -- src/tools/wp/bir_wpLib.sml-34- val wrap_exn = Feedback.wrap_exn "bir_wpLib"; src/tools/wp/bir_wpLib.sml-35- src/tools/wp/bir_wpLib.sml-36- in (* local *) src/tools/wp/bir_wpLib.sml-37- src/tools/wp/bir_wpLib.sml-38- val wps_id_prefix = "bir_wp_comp_wps_iter_step2_wp_" src/tools/wp/bir_wpLib.sml-39- src/tools/wp/bir_wpLib.sml:40: (* TODO: Replace all expressions in double hyphens by syntactic src/tools/wp/bir_wpLib.sml-41- * functions. src/tools/wp/bir_wpLib.sml-42- * src/tools/wp/bir_wpLib.sml-43- * Local syntax function library should contain: src/tools/wp/bir_wpLib.sml-44- * bir_bool_wps_map, bir_sound_wps_map, *) src/tools/wp/bir_wpLib.sml-45- (* Establish wps_bool_sound_thm for an initial analysis context *) src/tools/wp/bir_wpLib.sml-46- fun bir_wp_init_wps_bool_sound_thm (program, post, ls) wps defs = -- src/tools/wp/bir_wpLib.sml-89- val var_wps1 = mk_var ("wps'", finite_mapSyntax.mk_fmap_ty (bir_label_t_ty, bir_exp_t_ty)) src/tools/wp/bir_wpLib.sml-90- val thm = SPECL [program, var_l, ls, post, var_wps, var_wps1] reusable_thm src/tools/wp/bir_wpLib.sml-91- handle e => raise wrap_exn ("Failed to specialize the reusable thm " src/tools/wp/bir_wpLib.sml-92- ^ "(you may need to instantiate the reusable_thm's " src/tools/wp/bir_wpLib.sml-93- ^ "observation type to the one you're using)") e src/tools/wp/bir_wpLib.sml-94- src/tools/wp/bir_wpLib.sml:95: (* TODO: Redefining these convs every call is not part of src/tools/wp/bir_wpLib.sml-96- * computation, so these should be placed externally... *) src/tools/wp/bir_wpLib.sml-97- val post_bool_conv = [bir_is_bool_exp_def, type_of_bir_exp_def, src/tools/wp/bir_wpLib.sml-98- bir_var_type_def, type_of_bir_imm_def, src/tools/wp/bir_wpLib.sml-99- bir_type_is_Imm_def, BType_Bool_def, src/tools/wp/bir_wpLib.sml-100- bir_number_of_mem_splits_def, src/tools/wp/bir_wpLib.sml-101- size_of_bir_immtype_def] -- src/tools/wp/bir_wpLib.sml-130- bir_isnot_declare_stmt_def] src/tools/wp/bir_wpLib.sml-131- src/tools/wp/bir_wpLib.sml-132- fun wrap_exn_ exn term message = wrap_exn src/tools/wp/bir_wpLib.sml-133- (message ^ ": \n" ^ (Hol_pp.term_to_string term) ^ "\n") exn src/tools/wp/bir_wpLib.sml-134- val concl_tm = (snd o dest_eq o concl) src/tools/wp/bir_wpLib.sml-135- src/tools/wp/bir_wpLib.sml:136: (* TODO: Create bir_is_bool_expSyntax for the below *) src/tools/wp/bir_wpLib.sml-137- val post_bool_thm = SIMP_CONV (srw_ss()) (post_bool_conv@defs) src/tools/wp/bir_wpLib.sml-138- ``bir_is_bool_exp ^post`` src/tools/wp/bir_wpLib.sml-139- val thm = MP thm (SIMP_RULE std_ss [] post_bool_thm) src/tools/wp/bir_wpLib.sml-140- handle e => raise wrap_exn_ e (concl_tm post_bool_thm) "The postcondition isn't a bool"; src/tools/wp/bir_wpLib.sml-141- src/tools/wp/bir_wpLib.sml:142: (* TODO: Make bir_typing_progSyntax *) src/tools/wp/bir_wpLib.sml-143- val prog_typed_thm = SIMP_CONV (srw_ss()) (prog_typed_conv@defs) src/tools/wp/bir_wpLib.sml-144- ``bir_is_well_typed_program ^program`` src/tools/wp/bir_wpLib.sml-145- val thm = MP thm (SIMP_RULE std_ss [] prog_typed_thm) src/tools/wp/bir_wpLib.sml-146- handle e => raise wrap_exn_ e (concl_tm prog_typed_thm) "The program isn't well-typed"; src/tools/wp/bir_wpLib.sml-147- src/tools/wp/bir_wpLib.sml-148- (*val prog_valid_thm = SIMP_CONV (srw_ss()) (prog_valid_conv@defs) ``bir_is_valid_program ^program``;*) src/tools/wp/bir_wpLib.sml:149: (* TODO: Make bir_program_valid_stateSyntax *) src/tools/wp/bir_wpLib.sml-150- val prog_valid_thm = EVAL ``bir_is_valid_program ^program`` src/tools/wp/bir_wpLib.sml-151- val thm = MP thm (SIMP_RULE std_ss [] prog_valid_thm) src/tools/wp/bir_wpLib.sml-152- handle e => raise wrap_exn_ e (concl_tm prog_valid_thm) "The program isn't valid"; src/tools/wp/bir_wpLib.sml-153- src/tools/wp/bir_wpLib.sml:154: (* TODO: Make bir_wpSyntax *) src/tools/wp/bir_wpLib.sml-155- val no_declare_thm = SIMP_CONV (srw_ss()) (no_declare_conv@defs) src/tools/wp/bir_wpLib.sml-156- ``bir_declare_free_prog_exec ^program`` src/tools/wp/bir_wpLib.sml-157- val thm = MP thm (SIMP_RULE std_ss [] no_declare_thm) src/tools/wp/bir_wpLib.sml-158- handle e => raise wrap_exn_ e (concl_tm no_declare_thm) "The program isn't BStmt_Declare-free"; src/tools/wp/bir_wpLib.sml-159- src/tools/wp/bir_wpLib.sml-160- val thm = GENL [var_l, var_wps, var_wps1] thm; -- src/tools/wp/bir_wpLib.sml-186- listTheory.INDEX_FIND_def, BL_Address_HC_def] src/tools/wp/bir_wpLib.sml-187- val l_not_in_ls_conv = [BL_Address_HC_def] src/tools/wp/bir_wpLib.sml-188- src/tools/wp/bir_wpLib.sml-189- (* val label_in_prog_thm = src/tools/wp/bir_wpLib.sml-190- * SIMP_CONV (srw_ss()) (label_in_prog_conv@defs) src/tools/wp/bir_wpLib.sml-191- * ``MEM ^label (bir_labels_of_program ^program)``; *) src/tools/wp/bir_wpLib.sml:192: (* TODO: Use mk_mem in listSyntax, and add src/tools/wp/bir_wpLib.sml-193- * bir_labels_of_program to syntax functions in src/tools/wp/bir_wpLib.sml-194- * bir_programSyntax (bir_exec_blockLib has some redundant src/tools/wp/bir_wpLib.sml-195- * functions which should be moved) *) src/tools/wp/bir_wpLib.sml-196- val label_in_prog_thm = src/tools/wp/bir_wpLib.sml-197- EVAL ( src/tools/wp/bir_wpLib.sml-198- listSyntax.mk_mem (label, -- src/tools/wp/bir_wpLib.sml-200- ) src/tools/wp/bir_wpLib.sml-201- ) src/tools/wp/bir_wpLib.sml-202- val thm = MP thm (SIMP_RULE std_ss [] label_in_prog_thm) src/tools/wp/bir_wpLib.sml-203- (* val edges_blocks_in_prog_thm = src/tools/wp/bir_wpLib.sml-204- * SIMP_CONV (srw_ss()) (edges_blocks_in_prog_conv@defs) src/tools/wp/bir_wpLib.sml-205- * ``bir_edges_blocks_in_prog_exec ^program ^label``; *) src/tools/wp/bir_wpLib.sml:206: (* TODO: Add to bir_wpSyntax. *) src/tools/wp/bir_wpLib.sml-207- val edges_blocks_in_prog_thm = src/tools/wp/bir_wpLib.sml-208- EVAL ``bir_edges_blocks_in_prog_exec ^program ^label`` src/tools/wp/bir_wpLib.sml-209- val thm = MP thm (SIMP_RULE std_ss [] edges_blocks_in_prog_thm) src/tools/wp/bir_wpLib.sml-210- val l_not_in_ls_thm = src/tools/wp/bir_wpLib.sml-211- SIMP_CONV (srw_ss()) (l_not_in_ls_conv@defs) src/tools/wp/bir_wpLib.sml-212- (mk_neg (mk_IN (label, ls))) -- src/tools/wp/bir_wpLib.sml-249- (* produce wps1 and reestablish bool_sound_thm for this one *) src/tools/wp/bir_wpLib.sml-250- fun bir_wp_comp_wps_iter_step2 (wps, wps_bool_sound_thm) prog_l_thm src/tools/wp/bir_wpLib.sml-251- ((program, post, ls), (label)) defs = src/tools/wp/bir_wpLib.sml-252- let src/tools/wp/bir_wpLib.sml-253- val wps_id_suffix = label_to_wps_id_suffix label src/tools/wp/bir_wpLib.sml-254- src/tools/wp/bir_wpLib.sml:255: (* TODO: Constant, move out of function. *) src/tools/wp/bir_wpLib.sml-256- val var_wps1 = src/tools/wp/bir_wpLib.sml-257- mk_var("wps'", finite_mapSyntax.mk_fmap_ty(bir_label_t_ty, src/tools/wp/bir_wpLib.sml-258- bir_exp_t_ty) src/tools/wp/bir_wpLib.sml-259- ) src/tools/wp/bir_wpLib.sml-260- val thm = SPECL [wps, var_wps1] prog_l_thm src/tools/wp/bir_wpLib.sml-261- src/tools/wp/bir_wpLib.sml:262: (* FIXME: This seems to take some time, is that normal? *) src/tools/wp/bir_wpLib.sml-263- val thm = MP thm wps_bool_sound_thm src/tools/wp/bir_wpLib.sml-264- src/tools/wp/bir_wpLib.sml:265: (* FIXME: This seems to take some time, is that normal? *) src/tools/wp/bir_wpLib.sml-266- val wps_eval_restrict_consts = !bir_wp_comp_wps_iter_step2_consts; src/tools/wp/bir_wpLib.sml-267- val obs_ty = (hd o snd o dest_type o type_of) program src/tools/wp/bir_wpLib.sml-268- val wps1_thm = src/tools/wp/bir_wpLib.sml-269- computeLib.RESTR_EVAL_CONV wps_eval_restrict_consts src/tools/wp/bir_wpLib.sml-270- (list_mk_comb src/tools/wp/bir_wpLib.sml:271: (* TODO: Add to bir_wpSyntax *) src/tools/wp/bir_wpLib.sml-272- (inst [Type `:'obs_ty` |-> obs_ty] src/tools/wp/bir_wpLib.sml-273- ``bir_wp_exec_of_block:'obs_ty bir_program_t -> src/tools/wp/bir_wpLib.sml-274- bir_label_t -> src/tools/wp/bir_wpLib.sml-275- (bir_label_t -> bool) -> src/tools/wp/bir_wpLib.sml-276- bir_exp_t -> src/tools/wp/bir_wpLib.sml-277- (bir_label_t |-> bir_exp_t) -> -- src/tools/pass/bir_passificationLib.sml-56- prog src/tools/pass/bir_passificationLib.sml-57- end src/tools/pass/bir_passificationLib.sml-58-; src/tools/pass/bir_passificationLib.sml-59- src/tools/pass/bir_passificationLib.sml-60-(* Passification procedure *) src/tools/pass/bir_passificationLib.sml-61-local src/tools/pass/bir_passificationLib.sml:62: (* TODO: Map with string instead of bir_var term? *) src/tools/pass/bir_passificationLib.sml-63- val vmap = ref (Redblackmap.mkDict bir_var_compare : src/tools/pass/bir_passificationLib.sml-64- (term, int) Redblackmap.dict src/tools/pass/bir_passificationLib.sml-65- ) src/tools/pass/bir_passificationLib.sml-66- val underscore = "_" src/tools/pass/bir_passificationLib.sml-67- src/tools/pass/bir_passificationLib.sml-68- fun rename_var var version = -- src/tools/pass/bir_passificationLib.sml-300- src/tools/pass/bir_passificationLib.sml-301-fun passify_block_list_ssa [] = [] src/tools/pass/bir_passificationLib.sml-302- | passify_block_list_ssa (h::t) = src/tools/pass/bir_passificationLib.sml-303- let src/tools/pass/bir_passificationLib.sml-304- val (obs, label, bstmts, estmt) = dest_bir_block_list h src/tools/pass/bir_passificationLib.sml-305- val passified_bstmts = src/tools/pass/bir_passificationLib.sml:306: map (inst [(* TODO: make this "alpha" again *) (Type `:'a`) |-> obs]) (passify_bstmts_ssa bstmts) src/tools/pass/bir_passificationLib.sml-307- val passified_estmt = passify_estmt_ssa estmt src/tools/pass/bir_passificationLib.sml-308- val passified_block = src/tools/pass/bir_passificationLib.sml-309- mk_bir_block_list (obs, label, passified_bstmts, src/tools/pass/bir_passificationLib.sml-310- passified_estmt) src/tools/pass/bir_passificationLib.sml-311- in src/tools/pass/bir_passificationLib.sml-312- (passified_block::passify_block_list_ssa t) -- src/tools/cfg/bir_cfgLib.sml-163- reachability src/tools/cfg/bir_cfgLib.sml-164-================================================================= src/tools/cfg/bir_cfgLib.sml-165- *) src/tools/cfg/bir_cfgLib.sml-166- src/tools/cfg/bir_cfgLib.sml-167-(* src/tools/cfg/bir_cfgLib.sml-168- fun is_reachable_ nodes outs (done, []) = false src/tools/cfg/bir_cfgLib.sml:169: | is_reachable_ nodes outs (done, n::todo) = src/tools/cfg/bir_cfgLib.sml-170- if List.exists (fn x => x = n) outs then true else src/tools/cfg/bir_cfgLib.sml-171- let src/tools/cfg/bir_cfgLib.sml-172- val outs = List.nth(out_idxs,n; src/tools/cfg/bir_cfgLib.sml-173- val n_outs = List.filter (fn x => List.exists (fn y => x = y) nodes) outs); src/tools/cfg/bir_cfgLib.sml-174- val todo_outs = List.filter (fn x => List.exists (fn y => x = y) done) n_outs); src/tools/cfg/bir_cfgLib.sml-175- in -- src/tools/cfg/bir_cfgLib.sml-182- val n_outs = List.filter (fn x => List.exists (fn y => x = y) nodes) (List.nth(out_idxs,n)); src/tools/cfg/bir_cfgLib.sml-183- in src/tools/cfg/bir_cfgLib.sml-184- List.exists (fn x => is_reachable_chk out_idxs nodes outs x) n_outs src/tools/cfg/bir_cfgLib.sml-185- end; src/tools/cfg/bir_cfgLib.sml-186- src/tools/cfg/bir_cfgLib.sml-187-fun reachable_nodes_ out_idxs nodes (acc,[]) = acc src/tools/cfg/bir_cfgLib.sml:188: | reachable_nodes_ out_idxs nodes (acc,n::todo) = src/tools/cfg/bir_cfgLib.sml-189- let src/tools/cfg/bir_cfgLib.sml-190- val n_outs = List.filter (fn x => List.exists (fn y => x = y) nodes) (List.nth(out_idxs,n)); src/tools/cfg/bir_cfgLib.sml:191: val n_outs_filtered = List.filter (fn x => not (List.exists (fn y => x = y) (todo@acc))) n_outs; src/tools/cfg/bir_cfgLib.sml-192- in src/tools/cfg/bir_cfgLib.sml:193: reachable_nodes_ out_idxs nodes (n::acc,n_outs_filtered@todo) src/tools/cfg/bir_cfgLib.sml-194- end; src/tools/cfg/bir_cfgLib.sml-195- src/tools/cfg/bir_cfgLib.sml-196-fun reachable_nodes out_idxs nodes n = src/tools/cfg/bir_cfgLib.sml-197- let src/tools/cfg/bir_cfgLib.sml-198- val outs = List.filter (fn x => List.exists (fn y => x = y) nodes) (List.nth(out_idxs,n)); src/tools/cfg/bir_cfgLib.sml-199- in -- src/tools/cfg/bir_cfgLib.sml-375- src/tools/cfg/bir_cfgLib.sml-376-(* src/tools/cfg/bir_cfgLib.sml-377-val conn_comps = tl conn_comps; src/tools/cfg/bir_cfgLib.sml-378-val frags = divide_loopfree_fragments (blocks, in_idxs, out_idxs) conn_comps; src/tools/cfg/bir_cfgLib.sml-379- src/tools/cfg/bir_cfgLib.sml-380-val c = hd conn_comps; src/tools/cfg/bir_cfgLib.sml:381:val todo = prep_frag_todo_for_compnent c; src/tools/cfg/bir_cfgLib.sml-382-(divide_linear_fragments (blocks, in_idxs, out_idxs) [c]) src/tools/cfg/bir_cfgLib.sml-383-val frags = process_comp_frags [] []; src/tools/cfg/bir_cfgLib.sml-384- src/tools/cfg/bir_cfgLib.sml-385-val frags =[([0,1,3],[0],[3])] src/tools/cfg/bir_cfgLib.sml:386:val ((ns,en,ex)::todo) = [([2],2,2)] src/tools/cfg/bir_cfgLib.sml-387-val (nodes,entries,exits) = hd frags src/tools/cfg/bir_cfgLib.sml:388:process_comp_frags frags ((ns,en,ex)::todo) src/tools/cfg/bir_cfgLib.sml-389- src/tools/cfg/bir_cfgLib.sml-390- src/tools/cfg/bir_cfgLib.sml-391- src/tools/cfg/bir_cfgLib.sml-392- src/tools/cfg/bir_cfgLib.sml-393-fun find_component conn_comp target_label = find_idx (fn (n,_,_) => List.exists (fn i => src/tools/cfg/bir_cfgLib.sml-394- let -- src/tools/lifter/selftest.sml-505- src/tools/lifter/selftest.sml-506- src/tools/lifter/selftest.sml-507-val res = m0_test_asm "adds r0, r1, #0"; src/tools/lifter/selftest.sml-508-val res = m0_test_asm "adds r0, r1, #2"; src/tools/lifter/selftest.sml-509-val res = m0_test_asm "adds r0, r1, r2"; src/tools/lifter/selftest.sml-510-val res = m0_test_asm "add r0, r1"; src/tools/lifter/selftest.sml:511:val res = m0_test_asm "add pc, r1"; (* TODO: improve result *) src/tools/lifter/selftest.sml-512-val res = m0_test_asm "adds r0, #128"; src/tools/lifter/selftest.sml-513-val res = m0_test_asm "adcs r0, r1"; src/tools/lifter/selftest.sml-514-val res = m0_test_asm "add sp, #128"; src/tools/lifter/selftest.sml-515-val res = m0_test_asm "add r0, sp, #128"; src/tools/lifter/selftest.sml-516- src/tools/lifter/selftest.sml-517- -- src/tools/lifter/bir_inst_liftingLib.sml-413- src/tools/lifter/bir_inst_liftingLib.sml-414- fun preprocess_next_thms (lb:term) ([]:thm list) = src/tools/lifter/bir_inst_liftingLib.sml-415- raise bir_inst_liftingAuxExn (BILED_msg ("empty list of step theorems produced")) src/tools/lifter/bir_inst_liftingLib.sml-416- | preprocess_next_thms lb [thm] = [(lb, T, thm)] src/tools/lifter/bir_inst_liftingLib.sml-417- | preprocess_next_thms lb thms = src/tools/lifter/bir_inst_liftingLib.sml-418- [(lb, T, preprocess_next_thms_simple_merge (el 1 thms) (el 2 thms))] handle HOL_ERR _ => src/tools/lifter/bir_inst_liftingLib.sml:419: raise bir_inst_liftingAuxExn (BILED_msg ("more than 2 next-theorems cannot be merged currently: TODO")); src/tools/lifter/bir_inst_liftingLib.sml-420- src/tools/lifter/bir_inst_liftingLib.sml-421- src/tools/lifter/bir_inst_liftingLib.sml-422- src/tools/lifter/bir_inst_liftingLib.sml-423- (***********************************************) src/tools/lifter/bir_inst_liftingLib.sml-424- (* Lifting a single thm *) src/tools/lifter/bir_inst_liftingLib.sml-425- (***********************************************) -- src/tools/lifter/bir_inst_liftingLib.sml-1201- val thm1 = MP thm0 block_thm src/tools/lifter/bir_inst_liftingLib.sml-1202- val (pre, _) = dest_imp_only (concl thm1) src/tools/lifter/bir_inst_liftingLib.sml-1203- val pre_thm = EQT_ELIM (pre_conv pre) src/tools/lifter/bir_inst_liftingLib.sml-1204- val thm2 = MP thm1 pre_thm src/tools/lifter/bir_inst_liftingLib.sml-1205- in thm2 end src/tools/lifter/bir_inst_liftingLib.sml-1206- | _ => src/tools/lifter/bir_inst_liftingLib.sml:1207: raise (bir_inst_liftingAuxExn (BILED_msg "TODO: multiblock instructions are not supported yet")); src/tools/lifter/bir_inst_liftingLib.sml-1208- src/tools/lifter/bir_inst_liftingLib.sml-1209- end; src/tools/lifter/bir_inst_liftingLib.sml-1210- src/tools/lifter/bir_inst_liftingLib.sml-1211- src/tools/lifter/bir_inst_liftingLib.sml-1212- (**************************) src/tools/lifter/bir_inst_liftingLib.sml-1213- (* Lifting an instruction *) -- src/tools/exec/examples/example-toy.sml-46- bb_statements := []; src/tools/exec/examples/example-toy.sml-47- bb_last_statement := BStmt_Jmp (BLE_Label (BL_Label "scheduler")) src/tools/exec/examples/example-toy.sml-48- |>; src/tools/exec/examples/example-toy.sml-49- (* Bus arrived *) src/tools/exec/examples/example-toy.sml-50- <|bb_label := BL_Label "entrypoints.bus_arrived"; src/tools/exec/examples/example-toy.sml-51- bb_statements := [ src/tools/exec/examples/example-toy.sml:52: (* TODO: Assert that Alice is waiting the bus? *) src/tools/exec/examples/example-toy.sml-53- (* state.alice.step := 3 *) src/tools/exec/examples/example-toy.sml-54- BStmt_Assign (BVar "state.alice.step" (BType_Imm Bit32)) src/tools/exec/examples/example-toy.sml-55- (BExp_Const (Imm32 0x3w)) src/tools/exec/examples/example-toy.sml-56- ]; src/tools/exec/examples/example-toy.sml-57- bb_last_statement := BStmt_Halt (BExp_Const (Imm32 0x000000w)) src/tools/exec/examples/example-toy.sml-58- |>; src/tools/exec/examples/example-toy.sml-59- (* Taxi arrived *) src/tools/exec/examples/example-toy.sml-60- <|bb_label := BL_Label "entrypoints.taxi_arrived"; src/tools/exec/examples/example-toy.sml-61- bb_statements := [ src/tools/exec/examples/example-toy.sml:62: (* TODO: Assert that Bob is waiting a taxi? *) src/tools/exec/examples/example-toy.sml-63- (* state.bob.step := 5 *) src/tools/exec/examples/example-toy.sml-64- BStmt_Assign (BVar "state.bob.step" (BType_Imm Bit32)) src/tools/exec/examples/example-toy.sml-65- (BExp_Const (Imm32 0x5w)) src/tools/exec/examples/example-toy.sml-66- ]; src/tools/exec/examples/example-toy.sml-67- bb_last_statement := BStmt_Halt (BExp_Const (Imm32 0x000000w)) src/tools/exec/examples/example-toy.sml-68- |>; -- src/tools/exec/bir_exec_typingLib.sml-58- let src/tools/exec/bir_exec_typingLib.sml-59- val var_usage_list = GEN_find_all_subterm is_BVar prog; src/tools/exec/bir_exec_typingLib.sml-60- src/tools/exec/bir_exec_typingLib.sml-61- fun filter_doubles [] acc = acc src/tools/exec/bir_exec_typingLib.sml-62- | filter_doubles (x::xs) acc = filter_doubles (List.filter (fn y => y <> x) xs) (x::acc); src/tools/exec/bir_exec_typingLib.sml-63- in src/tools/exec/bir_exec_typingLib.sml:64: filter_doubles var_usage_list [] (* TODO: double check that these are all variables? *) src/tools/exec/bir_exec_typingLib.sml-65- end; src/tools/exec/bir_exec_typingLib.sml-66- src/tools/exec/bir_exec_typingLib.sml-67- src/tools/exec/bir_exec_typingLib.sml-68- fun gen_labels_of_prog prog = src/tools/exec/bir_exec_typingLib.sml-69- let src/tools/exec/bir_exec_typingLib.sml-70- val rep_gen_set_and_eval_conv = -- src/tools/exec/bir_exec_typingLib.sml-74- )); src/tools/exec/bir_exec_typingLib.sml-75- val label_set = (snd o dest_eq o concl o rep_gen_set_and_eval_conv) ``bir_labels_of_program ^prog``; src/tools/exec/bir_exec_typingLib.sml-76- in src/tools/exec/bir_exec_typingLib.sml-77- (fst o dest_list) label_set src/tools/exec/bir_exec_typingLib.sml-78- end; src/tools/exec/bir_exec_typingLib.sml-79- src/tools/exec/bir_exec_typingLib.sml:80:(* TODO: *) src/tools/exec/bir_exec_typingLib.sml-81-(* src/tools/exec/bir_exec_typingLib.sml-82-type_of_bir_exp src/tools/exec/bir_exec_typingLib.sml-83-(bir_vars_of_exp) src/tools/exec/bir_exec_typingLib.sml-84-(bir_var_set_is_well_typed vs) src/tools/exec/bir_exec_typingLib.sml-85-((bir_exp_is_well_typed)) src/tools/exec/bir_exec_typingLib.sml-86-bir_is_well_typed_program -- src/tools/exec/bir_exec_envLib.sml-49- bir_programTheory.bir_declare_initial_value_def src/tools/exec/bir_exec_envLib.sml-50- *) src/tools/exec/bir_exec_envLib.sml-51- val var_assigns = List.map (fn (n,t) => src/tools/exec/bir_exec_envLib.sml-52- mk_pair (n, (mk_pair (t, (snd o dest_eq o concl o EVAL) ``SOME (bir_default_value_of_type ^t)``)))) var_pairs; src/tools/exec/bir_exec_envLib.sml-53- src/tools/exec/bir_exec_envLib.sml-54- val env = mk_BEnv (list_mk_fupdate (fempty_env_tm, var_assigns)); src/tools/exec/bir_exec_envLib.sml:55: (* TODO: check that "bir_env_vars_are_initialised ^env (bir_vars_of_prog ^prog)" *) src/tools/exec/bir_exec_envLib.sml-56-(* bir_envTheory.bir_env_vars_are_initialised_def *) src/tools/exec/bir_exec_envLib.sml-57- in src/tools/exec/bir_exec_envLib.sml-58- env src/tools/exec/bir_exec_envLib.sml-59- end; src/tools/exec/bir_exec_envLib.sml-60- src/tools/exec/bir_exec_envLib.sml-61- src/tools/exec/bir_exec_envLib.sml-62- src/tools/exec/bir_exec_envLib.sml:63: (* TODO: organize these and other theorem lists in simpsets if suitable *) src/tools/exec/bir_exec_envLib.sml-64- (* list of theorems to evaluate environment lookups *) src/tools/exec/bir_exec_envLib.sml-65- val env_lookup_thms = src/tools/exec/bir_exec_envLib.sml-66- [bir_var_name_def, src/tools/exec/bir_exec_envLib.sml-67- bir_var_type_def, src/tools/exec/bir_exec_envLib.sml-68- FLOOKUP_EMPTY, src/tools/exec/bir_exec_envLib.sml-69- FLOOKUP_UPDATE, -- src/tools/exec/bir_exec_expLib.sml-141- thm2 src/tools/exec/bir_exec_expLib.sml-142- end; src/tools/exec/bir_exec_expLib.sml-143- in src/tools/exec/bir_exec_expLib.sml-144- GEN_selective_conv is_tm_fun check_tm_fun conv src/tools/exec/bir_exec_expLib.sml-145- end; src/tools/exec/bir_exec_expLib.sml-146- src/tools/exec/bir_exec_expLib.sml:147:(* TODO: improve evaluation completion checks and generalize these functions everywhere *) src/tools/exec/bir_exec_expLib.sml:148:(* TODO: generally: improve rewriting, select proper theorems and organize reusably in separate lists according to respective goals *) src/tools/exec/bir_exec_expLib.sml-149- fun bir_exec_exp_conv var_eq_thms = src/tools/exec/bir_exec_expLib.sml-150- let src/tools/exec/bir_exec_expLib.sml-151- val is_tm_fun = is_bir_eval_exp; src/tools/exec/bir_exec_expLib.sml-152- val check_tm_fun = (fn t => is_BVal_Imm t orelse is_BVal_Mem t); src/tools/exec/bir_exec_expLib.sml-153- fun conv t = src/tools/exec/bir_exec_expLib.sml-154- let -- src/tools/scamv/examples/driver-test.sml-19-val word_relation = make_word_relation relation all_exps; src/tools/scamv/examples/driver-test.sml-20-print_term (word_relation); src/tools/scamv/examples/driver-test.sml-21- src/tools/scamv/examples/driver-test.sml-22-val model = Z3_SAT_modelLib.Z3_GET_SAT_MODEL word_relation; src/tools/scamv/examples/driver-test.sml-23-*) src/tools/scamv/examples/driver-test.sml-24- src/tools/scamv/examples/driver-test.sml:25:(*TODO try to make 'complement' relation that doesn't include the invalid paths, src/tools/scamv/examples/driver-test.sml-26- since the paths will be selected by the driver anyway src/tools/scamv/examples/driver-test.sml-27- *) -- src/tools/scamv/examples/run-test.sml-71- src/tools/scamv/examples/run-test.sml-72-val _ = scamv_test_mock (); src/tools/scamv/examples/run-test.sml-73-(*val _ = scamv_test_asmf asm_file;*) src/tools/scamv/examples/run-test.sml-74- src/tools/scamv/examples/run-test.sml-75- src/tools/scamv/examples/run-test.sml-76-(* src/tools/scamv/examples/run-test.sml:77: TODO: move the following somewhere else src/tools/scamv/examples/run-test.sml-78- >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> src/tools/scamv/examples/run-test.sml-79- *) src/tools/scamv/examples/run-test.sml-80- src/tools/scamv/examples/run-test.sml-81- src/tools/scamv/examples/run-test.sml-82-open gcc_supportLib; src/tools/scamv/examples/run-test.sml-83- -- src/tools/scamv/bir_symb_execLib.sml-134- src/tools/scamv/bir_symb_execLib.sml-135-fun symb_exec_leaflist (Symb_Node (s, [])) = [s] src/tools/scamv/bir_symb_execLib.sml-136- | symb_exec_leaflist (Symb_Node (_, l )) = List.concat (List.map symb_exec_leaflist l) src/tools/scamv/bir_symb_execLib.sml-137-(* | symb_exec_leaflist _ = raise ERR "symb_exec_leaflist" "this should not happen"*) src/tools/scamv/bir_symb_execLib.sml-138- ; src/tools/scamv/bir_symb_execLib.sml-139- src/tools/scamv/bir_symb_execLib.sml:140:(* TODO: move this to lib and possibly merge to bir_expLib *) src/tools/scamv/bir_symb_execLib.sml-141- fun bir_exp_rewrite rwf exp = src/tools/scamv/bir_symb_execLib.sml-142- if is_BExp_Const exp then src/tools/scamv/bir_symb_execLib.sml-143- rwf exp src/tools/scamv/bir_symb_execLib.sml-144- src/tools/scamv/bir_symb_execLib.sml-145- else if is_BExp_Den exp then src/tools/scamv/bir_symb_execLib.sml-146- rwf exp ```

Note: I'm a script, and I'm simple, so I may be missing something or show false positives. You can review the script here.

kth-step / HolBA

Move no-assumptions related definitions and theorems to bir-support #94