1structure ARM_prover_toolsLib :> ARM_prover_toolsLib = 2struct 3 4open Abbrev HolKernel boolLib bossLib Parse proofManagerLib; 5open arm_seq_monadTheory ; 6open tacticsLib inference_rulesTheory ARM_proverLib; 7open switching_lemma_helperTheory user_lemma_basicsTheory; 8 9(***************************************************) 10(* Tools to interact with ARM prover *) 11(* (and some tactics for mode mixes) *) 12(* Oliver Schwarz *) 13(***************************************************) 14 15 16exception not_matched_pattern; 17 18val _ = temp_overload_on("priv_mode_constraints", ``priv_mode_constraints_v1``); 19val priv_mode_constraints_def = priv_mode_constraints_v1_def; 20 21 22fun add_to_simplist thm = simp_thms_list := (thm::(!simp_thms_list)); 23 24 25fun update_mode_changing_comp_list opr = mode_changing_comp_list := (opr::(! mode_changing_comp_list)); 26 27 28fun save_comb_thm (name, th, listelement) = 29 let val () = update_mode_changing_comp_list listelement 30 in 31 save_thm(name, th) 32 end; 33 34 35fun get_trans_thm uf = 36 if (uf = ``priv_mode_constraints``) then 37 trans_priv_mode_constraints_thm 38 else if (uf = ``strict_unt``) then 39 trans_strict_unt_thm 40 else 41 trans_empty_unt_thm; 42 43 44fun get_reflex_thm uf = 45 if (uf = ``priv_mode_constraints``) then 46 reflex_priv_mode_constraints_thm 47 else if (uf = ``strict_unt``) then 48 reflex_strict_unt_thm 49 else 50 reflex_empty_unt_thm; 51 52fun get_sim_reflex_thm uy = 53 if (uy = ``priv_mode_similar``) then 54 reflex_priv_mode_similar_thm 55 else 56 reflex_empty_sim_thm; 57 58 59fun get_unt_def uf = 60 if (uf = ``priv_mode_constraints``) then 61 priv_mode_constraints_def 62 else if (uf = ``strict_unt``) then 63 strict_unt_def 64 else 65 empty_unt_def; 66 67 68fun get_sim_def uy = 69 if (uy = ``priv_mode_similar``) then 70 priv_mode_similar_def 71 else if (uy = ``empty_similar_def``) then 72 empty_sim_def 73 else 74 CONJ fixed_flags_def (CONJ fix_flags_def (CONJ empty_sim_def priv_mode_similar_def)) ; 75 76 77fun prove_it a src_inv trg_inv uf uy = 78 let val () = global_mode := ``16w:bool[5]`` 79 in 80 prove a src_inv trg_inv ([uf, uy, ``27w:word5``, ``_thm``]) ([(get_trans_thm uf), (get_reflex_thm uf), (get_unt_def uf), (get_sim_def uy), errorT_thm, (get_sim_reflex_thm uy)]) 81 end; 82 83fun obtain_proofs() = 84 case top_goals() of 85 [] => trivial_true 86 | (_, to_show)::_ => 87 let 88 val (rcstu, simp) = dest_comb to_show 89 val (rcst, unt) = dest_comb rcstu 90 val (rcs, i2) = dest_comb rcst 91 val (rc, i1) = dest_comb rcs 92 val (rel, comp) = dest_comb rc 93 val (thm, _) = prove_it comp i1 i2 unt simp 94 in 95 thm 96 end handle HOL_ERR _ => trivial_true 97 98fun GO_ON_TAC () = 99 let val thm = obtain_proofs () 100 in 101 ASSUME_TAC thm THEN FULL_SIMP_TAC (srw_ss()) [] 102 end; 103 104fun go_on cnt = case cnt of 105 0 => e(GO_ON_TAC()) 106 |1 => e(GO_ON_TAC()) 107 |_ => let val _= e(GO_ON_TAC()) in go_on (cnt-1) end; 108 109fun go_on_p cnt = go_on cnt; 110 111 112fun thm_prove a = 113 let val (cplx_thm, _) = (prove_it a ``assert_mode 16w`` ``assert_mode 16w`` ``empty_unt`` ``empty_sim``) 114 in 115 cplx_thm 116 end; 117 118fun thm_proveP a = 119 let val (cplx_thm, _) = (prove_it a ``assert_mode 16w`` ``comb_mode 16w 27w`` ``priv_mode_constraints`` ``priv_mode_similar``) 120 in 121 cplx_thm 122 end; 123 124 125fun thm_proveS a = 126 let val (cplx_thm, _) = (prove_it a ``assert_mode 16w`` ``assert_mode 16w`` ``strict_unt`` ``empty_sim``) 127 in 128 cplx_thm 129 end; 130 131 132fun prove_and_save (a, name) = 133 let val th = thm_prove a 134 in 135 save_thm(name, th) 136 end; 137 138 139fun prove_and_save_e (a, name) = 140 let val th = thm_prove a 141 in 142 save_thm(name, (MATCH_MP extras_lem2 th)) 143 end; 144 145fun prove_and_save_s (a, name) = 146 let val th = thm_proveS a 147 in 148 save_thm(name, (MATCH_MP extras_lem4 th)) 149 end; 150 151fun prove_and_save_p (a, name, lelement) = 152 let val th = thm_proveP a 153 in 154 save_comb_thm(name, th, lelement) 155 end; 156 157fun prove_and_save_p_helper (a, name) = 158 let val th = thm_proveP a 159 in 160 save_thm(name, th) 161 end; 162 163 164 165 166 167fun MODE_MIX_TAC newtrg (assumptions, gl) = 168 case (dest_term gl) of 169 COMB (rcstu, sim) 170 => case dest_term rcstu of 171 COMB (rcst, unt) 172 => case dest_term rcst of 173 COMB (rcs, i2) 174 => case (dest_term rcs) of 175 COMB (rc, i1) => 176 case (dest_term rc) of 177 COMB (rel, comp) => if ((i2 = ``mode_mix:(arm_state->bool)``) andalso ((unt = ``priv_mode_constraints_v2a``) andalso (sim=``priv_mode_similar``))) 178 then ((SUBGOAL_THEN (mk_comb(mk_comb((mk_comb(rcs, newtrg)), (if (newtrg = ``comb_mode 16w 19w``) then ``priv_mode_constraints_v2a`` else ``priv_mode_constraints_v1``)), sim)) (fn thm => RW_TAC (srw_ss()) [thm, mode_mix_upgrade])) (assumptions, gl)) 179 else (ALL_TAC (assumptions, gl)) 180 | _ => (ALL_TAC (assumptions, gl)) 181 | _ => (ALL_TAC (assumptions, gl)) 182 | _ => (ALL_TAC (assumptions, gl)) 183 | _ => (ALL_TAC (assumptions, gl)) 184 | _ => (ALL_TAC (assumptions, gl)); 185 186 187fun LITTLE_MODE_MIX_TAC newtrg (assumptions, gl) = 188 case (dest_term gl) of 189 COMB (rcstu, sim) 190 => case dest_term rcstu of 191 COMB (rcst, unt) 192 => case dest_term rcst of 193 COMB (rcs, i2) 194 => case (dest_term rcs) of 195 COMB (rc, i1) => 196 case (dest_term rc) of 197 COMB (rel, comp) => if (i2 = ``little_mode_mix:(arm_state->bool)``) 198 then ((SUBGOAL_THEN (mk_comb(mk_comb((mk_comb(rcs, newtrg)),unt), sim)) (fn thm => RW_TAC (srw_ss()) [thm, little_mode_mix_upgrade])) (assumptions, gl)) 199 else (ALL_TAC (assumptions, gl)) 200 | _ => (ALL_TAC (assumptions, gl)) 201 | _ => (ALL_TAC (assumptions, gl)) 202 | _ => (ALL_TAC (assumptions, gl)) 203 | _ => (ALL_TAC (assumptions, gl)) 204 | _ => (ALL_TAC (assumptions, gl)); 205 206 207 208 209 210end 211