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