1(* 2 * Copyright 2018, Data61 3 * Commonwealth Scientific and Industrial Research Organisation (CSIRO) 4 * ABN 41 687 119 230. 5 * 6 * This software may be distributed and modified according to the terms of 7 * the BSD 2-Clause license. Note that NO WARRANTY is provided. 8 * See "LICENSE_BSD2.txt" for details. 9 * 10 * @TAG(DATA61_BSD) 11 *) 12 13open preamble basis bigStepTheory semanticPrimitivesTheory ml_translatorTheory 14 ml_translatorLib ml_progLib cfLib; 15 16structure camkesUtilsLib = struct 17 fun derive_eval_thm_bytes for_eval v_name e len = let 18 val th = get_ml_prog_state () |> get_thm 19 val th = MATCH_MP ml_progTheory.ML_code_Dlet_var th 20 |> REWRITE_RULE [ml_progTheory.ML_code_env_def] 21 val env = get_ml_prog_state() |> get_env 22 val th = th |> CONV_RULE(RESORT_FORALL_CONV(sort_vars["e","s3"])) 23 |> SPEC e |> CONV_RULE SWAP_FORALL_CONV |> SPEC env 24 val st = th |> SPEC_ALL |> concl |> dest_imp |> #1 |> strip_comb |> #2 |> el 1 25 val new_st = ``^st with refs := ^st.refs ++ [W8array (REPLICATE ^(numSyntax.term_of_int len) 0w)]`` 26 val goal = th |> SPEC new_st |> SPEC_ALL |> concl |> dest_imp |> fst 27 val lemma = goal |> (EVAL THENC SIMP_CONV(srw_ss())[semanticPrimitivesTheory.state_component_equality]) 28 val v_thm = prove(mk_imp(lemma |> concl |> rand, goal), 29 rpt strip_tac \\ rveq \\ match_mp_tac(#2(EQ_IMP_RULE lemma)) 30 \\ asm_simp_tac bool_ss []) 31 |> GEN_ALL |> SIMP_RULE std_ss [] |> SPEC_ALL; 32 val v_tm = v_thm |> concl |> strip_comb |> #2 |> last 33 val v_def = define_abbrev false v_name v_tm 34 in v_thm |> REWRITE_RULE [GSYM v_def] end 35end 36