p4_exec_semScript.sml

open HolKernel boolLib Parse bossLib;

val _ = new_theory "p4_exec_sem";

open p4Syntax;
open ottTheory;
open p4Theory p4_auxTheory;

(*********************************)
(* Expression-related shorthands *)

Definition is_v_def:
 (is_v (e_v v) = T) /\
 (is_v _ = F)
End

Definition get_v_def:
 (get_v (e_v v) = SOME v) /\
 (get_v _ = NONE)
End

Definition is_v_bool_def:
 (is_v_bool (e_v (v_bool b)) = T) /\
 (is_v_bool _ = F)
End

Definition is_v_bit_def:
 (is_v_bit (e_v (v_bit bitv)) = T) /\
 (is_v_bit _ = F)
End

(* NOTE: Error messages serialised using 32 bits *)
Definition is_v_err_def:
 (is_v_err (e_v (v_bit (bl, 32))) = T) /\
 (is_v_err _ = F)
End

Definition is_v_str_def:
 (is_v_str (e_v (v_str x)) = T) /\
 (is_v_str _ = F)
End

Definition is_var_def:
 (is_var (e_var x) = T) /\
 (is_var _ = F)
End

Definition unop_exec_def:
 (unop_exec unop_neg (v_bool b) = SOME (v_bool ~b))
 /\
 (unop_exec unop_compl (v_bit bitv) = SOME (v_bit (bitv_bl_unop bnot bitv)))
 /\
 (unop_exec unop_neg_signed (v_bit bitv) = SOME (v_bit (bitv_unop unop_neg_signed bitv)))
 /\
 (unop_exec unop_un_plus (v_bit bitv) = SOME (v_bit bitv))
 /\
 (unop_exec unop v = NONE)
End

Definition e_exec_unop_def:
 (e_exec_unop unop (e_v v) = unop_exec unop v)
  /\
 (e_exec_unop _ _ = NONE)
End

Definition cast_exec_def:
 (cast_exec (cast_unsigned n) (v_bit bitv) = SOME (v_bit $ bitv_cast n bitv))
 /\
 (cast_exec (cast_unsigned n) (v_bool b) = SOME (v_bit $ bool_cast n b))
 /\
 (cast_exec (cast_bool) (v_bit bitv) = SOME (v_bool $ to_bool_cast bitv))
 /\
 (cast_exec _ _ = NONE)
End

Definition e_exec_cast_def:
 (e_exec_cast (cast_unsigned n) (e_v v) = cast_exec (cast_unsigned n) v)
  /\
 (e_exec_cast (cast_bool) (e_v v) = cast_exec (cast_bool) v)
  /\
 (e_exec_cast _ _ = NONE)
End

(* TODO: Split binop into binop, binpred, ... to reduce copypaste? *)
Definition binop_exec_def:
 (binop_exec binop_mul (v_bit bitv1) (v_bit bitv2) =
  case bitv_binop binop_mul bitv1 bitv2 of
  | SOME bitv3 => SOME (v_bit bitv3)
  | NONE => NONE)
 /\
 (binop_exec binop_div (v_bit bitv1) (v_bit bitv2) =
  case bitv_binop binop_div bitv1 bitv2 of
  | SOME bitv3 => SOME (v_bit bitv3)
  | NONE => NONE)
 /\
 (binop_exec binop_mod (v_bit bitv1) (v_bit bitv2) =
  case bitv_binop binop_mod bitv1 bitv2 of
  | SOME bitv3 => SOME (v_bit bitv3)
  | NONE => NONE)
 /\
 (binop_exec binop_add (v_bit bitv1) (v_bit bitv2) =
  case bitv_binop binop_add bitv1 bitv2 of
  | SOME bitv3 => SOME (v_bit bitv3)
  | NONE => NONE)
 /\
 (binop_exec binop_sat_add (v_bit bitv1) (v_bit bitv2) =
  case bitv_binop binop_sat_add bitv1 bitv2 of
  | SOME bitv3 => SOME (v_bit bitv3)
  | NONE => NONE)
 /\
 (binop_exec binop_sub (v_bit bitv1) (v_bit bitv2) =
  case bitv_binop binop_sub bitv1 bitv2 of
  | SOME bitv3 => SOME (v_bit bitv3)
  | NONE => NONE)
 /\
 (binop_exec binop_sat_sub (v_bit bitv1) (v_bit bitv2) =
  case bitv_binop binop_sat_sub bitv1 bitv2 of
  | SOME bitv3 => SOME (v_bit bitv3)
  | NONE => NONE)
 /\
 (binop_exec binop_shl (v_bit bitv1) (v_bit bitv2) =
  SOME (v_bit (bitv_bl_binop shiftl bitv1 ((\(bl, n). (v2n bl, n)) bitv2))))
 /\
 (binop_exec binop_shr (v_bit bitv1) (v_bit bitv2) =
  SOME (v_bit (bitv_bl_binop shiftr bitv1 ((\(bl, n). (v2n bl, n)) bitv2))))
 /\
 (binop_exec binop_le (v_bit bitv1) (v_bit bitv2) =
  case bitv_binpred binop_le bitv1 bitv2 of
  | SOME b => SOME (v_bool b)
  | NONE => NONE)
 /\
 (binop_exec binop_ge (v_bit bitv1) (v_bit bitv2) =
  case bitv_binpred binop_ge bitv1 bitv2 of
  | SOME b => SOME (v_bool b)
  | NONE => NONE)
 /\
 (binop_exec binop_lt (v_bit bitv1) (v_bit bitv2) =
  case bitv_binpred binop_lt bitv1 bitv2 of
  | SOME b => SOME (v_bool b)
  | NONE => NONE)
 /\
 (binop_exec binop_gt (v_bit bitv1) (v_bit bitv2) =
  case bitv_binpred binop_gt bitv1 bitv2 of
  | SOME b => SOME (v_bool b)
  | NONE => NONE)
 /\
 (* TODO: This would generalize easily in theory, but
  * gives rise to enormously many autogenerated cases *)
 (binop_exec binop_neq (v_bit bitv1) (v_bit bitv2) =
  SOME (v_bool (bitv1 <> bitv2)))
 /\
 (binop_exec binop_neq (v_bool b1) (v_bool b2) =
  SOME (v_bool (b1 <> b2)))
 /\
 (binop_exec binop_eq (v_bit bitv1) (v_bit bitv2) =
  SOME (v_bool (bitv1 = bitv2)))
 /\
 (binop_exec binop_eq (v_bool b1) (v_bool b2) =
  SOME (v_bool (b1 = b2)))
 /\
 (binop_exec binop_and (v_bit bitv1) (v_bit bitv2) =
  SOME (v_bit (bitv_bl_binop band bitv1 bitv2)))
 /\
 (binop_exec binop_xor (v_bit bitv1) (v_bit bitv2) =
  SOME (v_bit (bitv_bl_binop bxor bitv1 bitv2)))
 /\
 (binop_exec binop_or (v_bit bitv1) (v_bit bitv2) =
  SOME (v_bit (bitv_bl_binop bor bitv1 bitv2)))
 /\
 (binop_exec binop v1 v2 = NONE)
End

Definition e_exec_binop_def:
 (e_exec_binop (e_v v1) binop (e_v v2) = binop_exec binop v1 v2)
  /\
 (e_exec_binop _ _ _ = NONE)
End

Definition e_exec_short_circuit_def:
 (e_exec_short_circuit (v_bool T) binop_bin_and e = SOME e)
  /\
 (e_exec_short_circuit (v_bool F) binop_bin_and e = SOME (e_v (v_bool F)))
  /\
 (e_exec_short_circuit (v_bool T) binop_bin_or e = SOME (e_v (v_bool T)))
  /\
 (e_exec_short_circuit (v_bool F) binop_bin_or e = SOME e)
  /\
 (e_exec_short_circuit _ _ _ = NONE)
End

(* Field access *)
Definition e_exec_acc_def:
 (e_exec_acc (e_acc (e_v (v_struct f_v_list)) f) =
  case FIND (\(k, v). k = f) f_v_list of
  | SOME (f, v) => SOME (e_v v)
  | NONE => NONE)
  /\
 (e_exec_acc (e_acc (e_v (v_header boolv f_v_list)) f) =
  case FIND (\(k, v). k = f) f_v_list of
  | SOME (f, v) => SOME (e_v v)
  | NONE => NONE)
  /\
 (e_exec_acc _ = NONE)
End

Definition e_exec_select_def:
 (e_exec_select (e_v v) s_l_x_l x =
  case v of
  | v_struct x_v_l =>
   (case (FIND (\ (s_list, x'). match_all (ZIP(SND $ UNZIP x_v_l,s_list))) s_l_x_l) of
    | SOME (s_list, x') => SOME x'
    | NONE => SOME x)
  | _ => SOME x) /\
 (e_exec_select _ _ _ = NONE)
End

Definition e_exec_concat_def:
 (e_exec_concat (e_v (v_bit bitv1)) (e_v (v_bit bitv2)) =
  SOME (v_bit (bitv_concat bitv1 bitv2)))
  /\
 (e_exec_concat _ _ = NONE)
End

Definition e_exec_slice_def:
 (e_exec_slice (e_v (v_bit bitv1)) (e_v (v_bit bitv2)) (e_v (v_bit bitv3)) =
  SOME (v_bit (slice bitv1 bitv2 bitv3)))
  /\
 (e_exec_slice _ _ _ = NONE)
End

(********************************)
(* Statement-related shorthands *)

Definition is_empty_def:
 (is_empty stmt_empty = T) /\
 (is_empty _ = F)
End

Definition is_empty_singleton_def:
 (is_empty_singleton [stmt_empty] = T) /\
 (is_empty_singleton _ = F)
End

Definition get_ret_v_def:
 (get_ret_v (stmt_ret (e_v v)) = SOME v) /\
 (get_ret_v (stmt_seq (stmt_ret (e_v v)) stmt) = SOME v) /\
 (get_ret_v _ = NONE)
End

Definition stmt_exec_ass_def:
 (stmt_exec_ass lval (e_v v) ss =
  assign ss v lval)
  /\
 (stmt_exec_ass _ _ _ = NONE)
End

Definition stmt_exec_init_def:
 (stmt_exec_init varn (e_v v) ss = initialise ss varn v)
End

Definition stmt_exec_trans_def:
 (stmt_exec_trans (e_v (v_str x)) = SOME (status_trans x))
  /\
 (stmt_exec_trans _ = NONE)
End

Definition stmt_exec_cond_def:
 (stmt_exec_cond (e_v (v_bool T)) =
  SOME T)
  /\
 (stmt_exec_cond (e_v (v_bool F)) =
  SOME F)
  /\
 (stmt_exec_cond _ = NONE)
End

Definition e_state_size_def:
 (e_state_size ((ctx:'a ctx), (g_scope_list:g_scope_list), (scope_list:scope_list), (e:e)) = e_size e)
End

(* TODO: Write explicit NONE-reducing clauses for operands of wrong types?
 *       This would reduce warnings *)
(* TODO: Use let-statements to avoid duplicate "MAP FST", et cetera *)
(* Defn.tgoal (Hol_defn "e_exec" ` *)
Definition e_exec_def:
 (********************)
 (* Variable look-up *)
 (e_exec (ctx:'a ctx) (g_scope_list:g_scope_list) (scope_list:scope_list) (e_var x) =
  case lookup_vexp2 scope_list g_scope_list x of
  | SOME v => SOME (e_v v, [])
  | NONE => NONE)
  /\
 (******************************)
 (* Struct/header field access *)
 (e_exec ctx g_scope_list scope_list (e_acc e_v_struct x) =
  if is_v e_v_struct
  then
   (case e_exec_acc (e_acc e_v_struct x) of
    | SOME v => SOME (v, [])
    | NONE => NONE)
   else
    (case e_exec ctx g_scope_list scope_list e_v_struct of
     | SOME (e_v_struct', frame_list) =>
      SOME (e_acc e_v_struct' x, frame_list)
     | NONE => NONE))
  /\
 (*********************************)
 (* Struct/header field reduction *)
 (e_exec ctx g_scope_list scope_list (e_struct x_e_l) =
  case unred_mem_index (MAP SND x_e_l) of
  | SOME i =>
   (case e_exec ctx g_scope_list scope_list (EL i (MAP SND x_e_l)) of
    | SOME (e', frame_list) => SOME (e_struct (ZIP (MAP FST x_e_l, (LUPDATE e' i (MAP SND x_e_l)))), frame_list)
    | NONE => NONE)
  | NONE => SOME (e_v (v_struct (ZIP (MAP FST x_e_l, vl_of_el (MAP SND x_e_l)))), []))
  /\
 (************************)
 (* Function/extern call *)
 (e_exec (apply_table_f, ext_map, func_map, b_func_map, pars_map, tbl_map) g_scope_list scope_list (e_call funn e_l) =
  (case lookup_funn_sig_body funn func_map b_func_map ext_map of
    | SOME (stmt, x_d_l) =>
     if LENGTH x_d_l = LENGTH e_l
     then
      (case unred_arg_index (MAP SND x_d_l) e_l of
       | SOME i =>
        (case e_exec (apply_table_f, ext_map, func_map, b_func_map, pars_map, tbl_map) g_scope_list scope_list (EL i e_l) of
         | SOME (e', frame_list) => SOME (e_call funn (LUPDATE e' i e_l), frame_list)
         | NONE => NONE)
       | NONE =>
        (case copyin (MAP FST x_d_l) (MAP SND x_d_l) e_l g_scope_list scope_list of
         | SOME scope => 
          SOME (e_var (varn_star funn), [(funn, [stmt], [scope])])
         | NONE => NONE))
     else NONE
    | NONE => NONE))
  /\
 (********)
 (* Cast *)
 (e_exec ctx g_scope_list scope_list (e_cast cast e) =
  if is_v e
  then
   (case e_exec_cast cast e of
    | SOME v => SOME (e_v v, [])
    | NONE => NONE)
  else
   (case e_exec ctx g_scope_list scope_list e of
    | SOME (e', frame_list) => SOME (e_cast cast e', frame_list)
    | NONE => NONE))
  /\
 (********************)
 (* Unary arithmetic *)
 (e_exec ctx g_scope_list scope_list (e_unop unop e) =
  if is_v e
  then 
   (case e_exec_unop unop e of
    | SOME v => SOME (e_v v, [])
    | NONE => NONE)
  else
   (case e_exec ctx g_scope_list scope_list e of
    | SOME (e', frame_list) => SOME (e_unop unop e', frame_list)
    | NONE => NONE))
  /\
 (*********************)
 (* Binary arithmetic *)
 (e_exec ctx g_scope_list scope_list (e_binop e1 binop e2) =
  (case e1 of
   | (e_v v) =>
    if is_short_circuitable binop
    then
     (case e_exec_short_circuit v binop e2 of
      | SOME e' => SOME (e', [])
      | NONE => NONE)
    else if is_v e2
    then
     (case e_exec_binop e1 binop e2 of
      | SOME v' => SOME (e_v v', [])
      | NONE => NONE)
    else
     (case e_exec ctx g_scope_list scope_list e2 of
      | SOME (e2', frame_list) => SOME (e_binop e1 binop e2', frame_list)
      | NONE => NONE)
   | _ =>
    (case e_exec ctx g_scope_list scope_list e1 of
     | SOME (e1', frame_list) => SOME (e_binop e1' binop e2, frame_list)
     | NONE => NONE)))
  /\
 (**********)
 (* Select *)
 (e_exec ctx g_scope_list scope_list (e_select e s_l_x_l x) =
  if is_v e
  then
   (case e_exec_select e s_l_x_l x of
    | SOME x' => SOME (e_v (v_str x'), [])
    | NONE => NONE)
  else
   (case e_exec ctx g_scope_list scope_list e of
    | SOME (e', frame_list) => SOME (e_select e' s_l_x_l x, frame_list)
    | NONE => NONE))
  /\
 (*****************)
 (* Concatenation *)
 (e_exec ctx g_scope_list scope_list (e_concat e1 e2) =
  if is_v_bit e1
  then 
   (if is_v_bit e2
    then 
     (case e_exec_concat e1 e2 of
      | SOME v => SOME (e_v v, [])
      | NONE => NONE)
    else
     (case e_exec ctx g_scope_list scope_list e2 of
      | SOME (e2', frame_list) => SOME (e_concat e1 e2', frame_list)
      | NONE => NONE))
  else
   (case e_exec ctx g_scope_list scope_list e1 of
    | SOME (e1', frame_list) => SOME (e_concat e1' e2, frame_list)
    | NONE => NONE))
  /\
 (***********)
 (* Slicing *)
 (e_exec ctx g_scope_list scope_list (e_slice e1 e2 e3) =
  if (is_v_bit e2 /\ is_v_bit e3)
  then
   (if is_v_bit e1
    then 
     (case e_exec_slice e1 e2 e3 of
      | SOME v => SOME (e_v v, [])
      | NONE => NONE)
    else
     (case e_exec ctx g_scope_list scope_list e1 of
      | SOME (e1', frame_list) => SOME (e_slice e1' e2 e3, frame_list)
      | NONE => NONE))
   else NONE)
  /\
 (e_exec _ _ _ _ = NONE)
Termination
WF_REL_TAC `measure e_state_size` >>
fs [e_state_size_def, e_size_def] >>
REPEAT STRIP_TAC >| [
  IMP_RES_TAC unred_arg_index_in_range >>
  IMP_RES_TAC rich_listTheory.EL_MEM >>
  IMP_RES_TAC e3_size_mem >>
  fs [],

  IMP_RES_TAC unred_mem_index_in_range >>
  IMP_RES_TAC rich_listTheory.EL_MEM >>
  `e_size (EL i (MAP SND x_e_l)) < e1_size x_e_l` suffices_by (
   fs []
  ) >>
  `e2_size (EL i (MAP FST x_e_l), EL i (MAP SND x_e_l)) < e1_size x_e_l` suffices_by (
   rpt strip_tac >>
   irule arithmeticTheory.LESS_TRANS >>
   qexists_tac `e2_size (EL i (MAP FST x_e_l),EL i (MAP SND x_e_l))` >>
   fs [e_e2_size_less]
  ) >>
  subgoal `MEM (EL i x_e_l) x_e_l` >- (
   irule rich_listTheory.EL_MEM >>
   fs [listTheory.LENGTH_MAP]
  ) >>
  imp_res_tac e1_size_mem >>
  metis_tac [EL_pair_list, listTheory.LENGTH_MAP]
]
End
(*
val e_exec_ind = tryfind (uncurry DB.fetch) [("scratch", "e_exec_ind"),
                                             ("p4_exec_sem", "e_exec_ind")];
val _ = save_thm("e_exec_ind", e_exec_ind);
*)

(*
val measure_stmt_state_size_def = Define `
 (measure_stmt_state_size ((ctx:ctx), (g_scope_list:g_scope_list), (frame_list:frame_list), (ctrl:ctrl), (status:status))
                          ((ctx':ctx), (g_scope_list':g_scope_list), (frame_list':frame_list), (ctrl':ctrl), (status':status)) =
  if LENGTH frame_list <> LENGTH frame_list'
  then LENGTH frame_list < LENGTH frame_list'
  else if LENGTH (FST $ SND $ HD frame_list) <> LENGTH (FST $ SND $ HD frame_list')
  then LENGTH (FST $ SND $ HD frame_list) < LENGTH (FST $ SND $ HD frame_list')
  else (stmt_size (HD $ FST $ SND $ HD frame_list) < stmt_size (HD $ FST $ SND $ HD frame_list')))
`;
*)

Definition is_consts_exec_def:
 (is_consts_exec [] = T) /\
 (is_consts_exec (h::t) = ((is_const h) /\ (is_consts_exec t)))
End

Theorem vl_of_el_MAP_e_v:
!el.
is_consts_exec el ==>
el = MAP e_v (vl_of_el el)
Proof
Induct_on `el` >- (
 fs [is_consts_exec_def, vl_of_el_def]
) >>
rpt strip_tac >>
fs [is_consts_exec_def, vl_of_el_def] >>
Cases_on `h` >> (
 fs [is_const_def]
) >>
fs [v_of_e_def]
QED

Definition stmt_exec_def:
 (******************************************)
 (* Catch-all clauses for special statuses *)
 (stmt_exec (ctx:'a ctx) ((ascope:'a, g_scope_list:g_scope_list, frame_list:frame_list, status_returnv v):'a state) = NONE)
  /\
 (stmt_exec _ (_, _, _, status_trans x) = NONE)
  /\
 (* Empty frame list *)
 (stmt_exec _ (_, _, [], _) = NONE)
  /\
 (* Empty scope stack *)
 (stmt_exec _ (_, _, [(funn, stmt_stack, [])], _) = NONE)
  /\
 (**************)
 (* Assignment *)
 (stmt_exec ctx (ascope, g_scope_list, [(funn, [stmt_ass lval e], scope_list)], status_running) =
  if is_v e
  then
   (case stmt_exec_ass lval e (scope_list++g_scope_list) of
    | SOME scope_list'' =>
     (case separate scope_list'' of
      | (SOME g_scope_list', SOME scope_list') =>
       SOME (ascope, g_scope_list', [(funn, [stmt_empty], scope_list')], status_running)
      | _ => NONE)
    | NONE => NONE)
  else
   (case e_exec ctx g_scope_list scope_list e of
    | SOME (e', frame_list) =>
     SOME (ascope, g_scope_list, frame_list++[(funn, [stmt_ass lval e'], scope_list)], status_running)
    | _ => NONE))
  /\
 (**************)
 (* Transition *)
 (stmt_exec ctx (ascope, g_scope_list, [(funn, [stmt_trans e], scope_list)], status_running) =
  if is_v e
  then
   if is_v_str e
   then
    (case stmt_exec_trans e of
     | SOME status' => SOME (ascope, g_scope_list, [(funn, [stmt_empty], scope_list)], status')
     | NONE => NONE)
    else NONE
  else
   (case e_exec ctx g_scope_list scope_list e of
    | SOME (e', frame_list) =>
     SOME (ascope, g_scope_list, frame_list++[(funn, [stmt_trans e'], scope_list)], status_running)
    | NONE => NONE))
  /\
 (***************)
 (* Conditional *)
 (stmt_exec ctx (ascope, g_scope_list, [(funn, [stmt_cond e stmt1 stmt2], scope_list)], status_running) =
  (* TODO: Make this more efficient by using a single get_v_bool e *)
  if is_v_bool e
  then
   (case stmt_exec_cond e of
    | SOME T => SOME (ascope, g_scope_list, [(funn, [stmt1], scope_list)], status_running)
    | SOME F => SOME (ascope, g_scope_list, [(funn, [stmt2], scope_list)], status_running)
    | NONE => NONE)
  else
   (case e_exec ctx g_scope_list scope_list e of
    | SOME (e', frame_list) =>
     SOME (ascope, g_scope_list, frame_list++[(funn, [stmt_cond e' stmt1 stmt2], scope_list)], status_running)
    | NONE => NONE))
  /\
 (*********************)
 (* Table application *)
 (stmt_exec (apply_table_f, ext_map, func_map, b_func_map, pars_map, tbl_map) (ascope, g_scope_list, [(funn, [stmt_app t_name e_l], scope_list)], status_running) =
  (case index_not_const e_l of
   | SOME i =>
    (case e_exec (apply_table_f, ext_map, func_map, b_func_map, pars_map, tbl_map) g_scope_list scope_list (EL i e_l) of
     | SOME (e', frame_list) =>
      SOME (ascope, g_scope_list, frame_list++[(funn, [stmt_app t_name (LUPDATE e' i e_l)], scope_list)], status_running)
     | NONE => NONE)
   | NONE =>
    (case ALOOKUP tbl_map t_name of
     | SOME (mk_l, (default_f, default_f_args)) =>
      (if LENGTH mk_l = LENGTH e_l
       then
        (case apply_table_f (t_name, e_l, mk_l, (default_f, default_f_args), ascope) of
         | SOME (f, f_args) =>
          (if is_consts_exec f_args
           then
            SOME (ascope, g_scope_list, [(funn, [stmt_ass lval_null (e_call (funn_name f) f_args)], scope_list)], status_running)
           else NONE)
         | NONE => NONE)
       else NONE)
     | NONE => NONE)))
  /\
 (**********)
 (* Return *)
 (stmt_exec ctx (ascope, g_scope_list, [(funn, [stmt_ret e], scope_list)], status_running) =
  (case get_v e of
   | SOME v => SOME (ascope, g_scope_list, [(funn, [stmt_empty], scope_list)], status_returnv v)
   | NONE => 
    (case e_exec ctx g_scope_list scope_list e of
     | SOME (e', frame_list) =>
      SOME (ascope, g_scope_list, frame_list++[(funn, [stmt_ret e'], scope_list)], status_running)
     | NONE => NONE)))
  /\
 (**********)
 (* Extern *)
 (stmt_exec (apply_table_f, ext_map, func_map, b_func_map, pars_map, tbl_map) (ascope, g_scope_list, [(funn, [stmt_ext], scope_list)], status_running) =
  (case lookup_ext_fun funn ext_map of
   | SOME ext_fun =>
    (case ext_fun (ascope, g_scope_list, scope_list) of
     | SOME (ascope', scope_list', status') =>
      SOME (ascope', g_scope_list, [(funn, [stmt_empty], scope_list')], status')
     | NONE => NONE)
   | NONE => NONE))
  /\
 (*********)
 (* Block *)
 (stmt_exec ctx (ascope, g_scope_list, [(funn, [stmt_block decl_list stmt], scope_list)], status_running) =
   SOME (ascope, g_scope_list, [(funn, [stmt]++[stmt_empty], ((declare_list_in_fresh_scope decl_list)::scope_list))], status_running))
  /\
 (************)
 (* Sequence *)
 (stmt_exec ctx (ascope, g_scope_list, [(funn, [stmt_seq stmt1 stmt2], scope_list)], status_running) =
  if is_empty stmt1
  then SOME (ascope, g_scope_list, [(funn, [stmt2], scope_list)], status_running)
  else
   (* Note: this only allows for 0 or 1 frame being added, or (exclusively) 1 stmt element *)
   (case stmt_exec ctx (ascope, g_scope_list, [(funn, [stmt1], scope_list)], status_running) of
    | SOME (ascope', g_scope_list', [(funn, [stmt1'], scope_list')], status') =>
     (case status' of 
      | status_running =>
       SOME (ascope', g_scope_list', [(funn, [stmt_seq stmt1' stmt2], scope_list')], status_running)
      | _ =>
       SOME (ascope', g_scope_list', [(funn, [stmt1'], scope_list')], status'))
    | SOME (ascope', g_scope_list', [(funn, stmt1''::[stmt1'], scope_list')], status_running) =>
     SOME (ascope', g_scope_list', [(funn, [stmt1'']++[stmt_seq stmt1' stmt2], scope_list')], status_running)
    | SOME (ascope', g_scope_list', (frame::[(funn, [stmt1'], scope_list')]), status_running) =>
     SOME (ascope', g_scope_list', (frame::[(funn, [stmt_seq stmt1' stmt2], scope_list')]), status_running)
    | _ => NONE))
  /\
 (*********************)
 (* Stmt stack clause *)
 (*********************)
 (* TODO: Should the case statement be handled by better matching in the clause? *)
 (stmt_exec ctx (ascope, g_scope_list, [(funn, stmt_empty::stmt_stack, scope_list)], status) =
  case stmt_stack of
  | [] => NONE
  | _ =>
   (case scope_list of
    | [] => NONE
    | (h_scope::scope_list') => SOME (ascope, g_scope_list, [(funn, stmt_stack, TL (h_scope::scope_list'))], status)))
  /\
 (* TODO: This clause gets expanded into multiple clauses to account for all different
  *       statements. An alternative solution, which may be even more convoluted,
  *       could be to make mutually recursive functions *)
 (stmt_exec ctx (ascope, g_scope_list, [(funn, stmt::stmt_stack, scope_list)], status) =
   (case stmt_exec ctx (ascope, g_scope_list, [(funn, [stmt], scope_list)], status) of
   | SOME (ascope', g_scope_list', frame_list', status') =>
    (case frame_list' of
     (* Regular case *)
     | [(funn, [stmt'], scope_list')] =>
      SOME (ascope', g_scope_list', [(funn, stmt'::stmt_stack, scope_list')], status')
     (* Block entry *)
     | [(funn, stmt''::[stmt'], scope_list')] =>
      SOME (ascope', g_scope_list', [(funn, stmt''::(stmt'::stmt_stack), scope_list')], status')
     (* Function call *)
     | ((funn', [stmt'], scope_list')::[(funn, [stmt''], scope_list)]) =>
      SOME (ascope', g_scope_list', ((funn', [stmt'], scope_list')::[(funn, stmt''::stmt_stack, scope_list)]), status')
     (* TODO: What can happen here? *)
     | _ => NONE)
   | NONE => NONE))
  /\
 (stmt_exec _ _ = NONE)
End

Theorem exec_stmt_SOME_init_running:
!ctx ascope ascope' g_scope_list g_scope_list' funn stmt frame_list' scope_list status status'.
stmt_exec ctx (ascope, g_scope_list, [(funn, [stmt], scope_list)], status) =
        SOME (ascope', g_scope_list', frame_list', status') ==>
 status = status_running
Proof
rpt strip_tac >>
Cases_on `stmt` >> (
 fs []
) >> (
 Cases_on `status` >> (
  fs [stmt_exec_def]
 )
)
QED

Theorem e_exec_new_frame:
!ctx g_scope_list scope_list e e' frame_list'.
e_exec ctx g_scope_list scope_list e = SOME (e',frame_list') ==>
(frame_list' = [] \/
 ?funn stmt scope. frame_list' = [(funn, [stmt], [scope])])
Proof
`!ctx g_scope_list scope_list e.
 (\ctx' g_scope_list' scope_list' e'.
  !e'' frame_list''.
  e_exec ctx' g_scope_list' scope_list' e' = SOME (e'', frame_list'') ==>
  (frame_list'' = [] \/
   ?funn'' stmt'' scope''. frame_list'' = [(funn'', [stmt''], [scope''])])
 ) ctx g_scope_list scope_list e` suffices_by (
 metis_tac []
) >>
irule e_exec_ind >>
fs [e_exec_def] >>
rpt strip_tac >| [
 Cases_on `lookup_funn_sig_body funn func_map b_func_map ext_map` >> (
  fs []
 ) >>
 PairCases_on `x` >>
 fs [] >>
 Cases_on `unred_arg_index (MAP SND x1) e_l` >> (
  fs []
 ) >| [
  Cases_on `copyin (MAP FST x1) (MAP SND x1) e_l g_scope_list scope_list` >> (
   fs []
  ) >>
  metis_tac [],

  Cases_on `e_exec (apply_table_f,ext_map,func_map,b_func_map,pars_map,tbl_map) g_scope_list
              scope_list (EL x e_l)` >> (
   fs []
  ) >>
  PairCases_on `x'` >>
  fs []
 ],

 (* Unop *)
 Cases_on `is_v e` >> (
  fs []
 ) >| [
  Cases_on `e_exec_cast cast e` >> (
   fs []
  ),

  Cases_on `e_exec ctx g_scope_list scope_list e` >> (
   fs []
  ) >>
  PairCases_on `x` >>
  fs []
 ],

 (* TODO: Weird blob goal... *)
 Cases_on `e1` >> (
  fs [e_exec_def]
 ) >| [
  Cases_on `is_short_circuitable binop` >> (
   fs []
  ) >| [
   Cases_on `e_exec_short_circuit v binop e2` >> (
    fs []
   ),

   Cases_on `is_v e2` >> (
    fs []
   ) >| [
    Cases_on `e_exec_binop (e_v v) binop e2` >> (
     fs []
    ),

    Cases_on `e_exec ctx g_scope_list scope_list e2` >> (
     fs []
    ) >>
    PairCases_on `x` >>
    fs []
   ]
  ],

  Cases_on `lookup_vexp2 scope_list g_scope_list v` >> (
   fs []
  ),

  Cases_on `is_v e` >> (
   fs []
  ) >- (
   Cases_on `e_exec_acc (e_acc e s)` >> (
    fs []
   )
  ) >>
  Cases_on `e_exec ctx g_scope_list scope_list e` >> (
   fs []
  ) >>
  PairCases_on `x` >>
  fs [],

  Cases_on `is_v e` >> (
   fs []
  ) >| [
   Cases_on `e_exec_unop u e` >> (
    fs []
   ),

   Cases_on `e_exec ctx g_scope_list scope_list e` >> (
    fs []
   ) >>
   PairCases_on `x` >>
   fs []
  ],

  (* Cast *)
  Cases_on `is_v e` >> (
   fs []
  ) >| [
   Cases_on `e_exec_cast c e` >> (
    fs []
   ),

   Cases_on `e_exec ctx g_scope_list scope_list e` >> (
    fs []
   ) >>
   PairCases_on `x` >>
   fs []
  ],

  (* TODO: Interesting... *)
  Cases_on `case e of
             e_v v =>
               if is_short_circuitable b then
                 case e_exec_short_circuit v b e0 of
                   NONE => NONE
                 | SOME e' => SOME (e',[])
               else if is_v e0 then
                 case e_exec_binop e b e0 of
                   NONE => NONE
                 | SOME v' => SOME (e_v v',[])
               else
                 (case e_exec ctx g_scope_list scope_list e0 of
                    NONE => NONE
                  | SOME (e2',frame_list) =>
                    SOME (e_binop e b e2',frame_list))
           | e_var v25 =>
             (case e_exec ctx g_scope_list scope_list e of
                NONE => NONE
              | SOME (e1',frame_list) => SOME (e_binop e1' b e0,frame_list))
           | e_list v26 =>
             (case e_exec ctx g_scope_list scope_list e of
                NONE => NONE
              | SOME (e1',frame_list) => SOME (e_binop e1' b e0,frame_list))
           | e_acc v27 v28 =>
             (case e_exec ctx g_scope_list scope_list e of
                NONE => NONE
              | SOME (e1',frame_list) => SOME (e_binop e1' b e0,frame_list))
           | e_unop v29 v30 =>
             (case e_exec ctx g_scope_list scope_list e of
                NONE => NONE
              | SOME (e1',frame_list) => SOME (e_binop e1' b e0,frame_list))
           | e_cast v29 v30 =>
             (case e_exec ctx g_scope_list scope_list e of
                NONE => NONE
              | SOME (e1',frame_list) => SOME (e_binop e1' b e0,frame_list))
           | e_binop v31 v32 v33 =>
             (case e_exec ctx g_scope_list scope_list e of
                NONE => NONE
              | SOME (e1',frame_list) => SOME (e_binop e1' b e0,frame_list))
           | e_concat v34 v35 =>
             (case e_exec ctx g_scope_list scope_list e of
                NONE => NONE
              | SOME (e1',frame_list) => SOME (e_binop e1' b e0,frame_list))
           | e_slice v36 v37 v38 =>
             (case e_exec ctx g_scope_list scope_list e of
                NONE => NONE
              | SOME (e1',frame_list) => SOME (e_binop e1' b e0,frame_list))
           | e_call v39 v40 =>
             (case e_exec ctx g_scope_list scope_list e of
                NONE => NONE
              | SOME (e1',frame_list) => SOME (e_binop e1' b e0,frame_list))
           | e_select v41 v42 v43 =>
             (case e_exec ctx g_scope_list scope_list e of
                NONE => NONE
              | SOME (e1',frame_list) => SOME (e_binop e1' b e0,frame_list))
           | e_struct v44 =>
             (case e_exec ctx g_scope_list scope_list e of
                NONE => NONE
              | SOME (e1',frame_list) => SOME (e_binop e1' b e0,frame_list))
           | e_header v45 v46 =>
             case e_exec ctx g_scope_list scope_list e of
               NONE => NONE
             | SOME (e1',frame_list) => SOME (e_binop e1' b e0,frame_list)` >> (
   fs []
  ) >>
  PairCases_on `x` >>
  fs [],

  (* Concatenation *)
  Cases_on `is_v_bit e` >> Cases_on `is_v_bit e0` >> (
   fs []
  ) >| [
   Cases_on `e_exec_concat e e0` >> (
    fs []
   ),

   Cases_on `e_exec ctx g_scope_list scope_list e0` >> (
    fs []
   ) >>
   PairCases_on `x` >>
   fs [],

   Cases_on `e_exec ctx g_scope_list scope_list e` >> (
    fs []
   ) >>
   PairCases_on `x` >>
   fs [],

   Cases_on `e_exec ctx g_scope_list scope_list e` >> (
    fs []
   ) >>
   PairCases_on `x` >>
   fs []
  ],

  (* Slicing *)
  Cases_on `is_v_bit e0` >> Cases_on `is_v_bit e1'` >> (
   fs []
  ) >>
  Cases_on `is_v_bit e` >> (
   fs []
  ) >| [
   Cases_on `e_exec_slice e e0 e1'` >> (
    fs []
   ),

   Cases_on `e_exec ctx g_scope_list scope_list e` >> (
    fs []
   ) >>
   PairCases_on `x` >>
   fs []
  ],

  (* Function call *)
  Cases_on `e_exec ctx g_scope_list scope_list (e_call f l)` >> (
   fs []
  ) >>
  PairCases_on `x` >>
  fs [],

  (* Select *)
  Cases_on `is_v e` >> (
   fs []
  ) >| [
   Cases_on `e_exec_select e l s` >> (
    fs []
   ),

   Cases_on `e_exec ctx g_scope_list scope_list e` >> (
    fs []
   ) >>
   PairCases_on `x` >>
   fs []
  ],

  (* Struct *)
  Cases_on `unred_mem_index (MAP SND l)` >> (
   fs []
  ) >>
  Cases_on `e_exec ctx g_scope_list scope_list (EL x (MAP SND l))` >> (
   fs []
  ) >>
  PairCases_on `x'` >>
  fs []
 ],

 (* Slicing *)
 Cases_on `is_v_bit e1` >> (
  fs []
 ) >| [
  Cases_on `e_exec_slice e1 e2 e3` >> (
   fs []
  ),

  Cases_on `e_exec ctx g_scope_list scope_list e1` >> (
   fs []
  ) >>
  PairCases_on `x` >>
  fs []
 ],

 (* Concatenation *)
 Cases_on `is_v_bit e1` >> Cases_on `is_v_bit e2` >> (
  fs []
 ) >| [
  Cases_on `e_exec_concat e1 e2` >> (
   fs []
  ),

  Cases_on `e_exec ctx g_scope_list scope_list e2` >> (
   fs []
  ) >>
  PairCases_on `x` >>
  fs [],

  Cases_on `e_exec ctx g_scope_list scope_list e1` >> (
   fs []
  ) >>
  PairCases_on `x` >>
  fs [],

  Cases_on `e_exec ctx g_scope_list scope_list e1` >> (
   fs []
  ) >>
  PairCases_on `x` >>
  fs []
 ],

 (* Access *)
 Cases_on `is_v e_v_struct` >> (
  fs []
 ) >| [
  Cases_on `e_exec_acc (e_acc e_v_struct x)` >> (
   fs []
  ),

  Cases_on `e_exec ctx g_scope_list scope_list e_v_struct` >> (
   fs []
  ) >>
  PairCases_on `x'` >>
  fs []
 ],

 (* Select *)
 Cases_on `is_v e` >> (
  fs []
 ) >| [
  Cases_on `e_exec_select e s_l_x_l x` >> (
   fs []
  ),

  Cases_on `e_exec ctx g_scope_list scope_list e` >> (
   fs []
  ) >>
  PairCases_on `x'` >>
  fs []
 ],

 (* Struct? *)
 Cases_on `unred_mem_index (MAP SND x_e_l)` >> (
  fs []
 ) >>
 Cases_on `e_exec ctx g_scope_list scope_list (EL x (MAP SND x_e_l))` >> (
  fs []
 ) >>
 PairCases_on `x'` >>
 fs [],

 (* Unop *)
 Cases_on `is_v e` >> (
  fs []
 ) >| [
  Cases_on `e_exec_unop unop e` >> (
   fs []
  ),

  Cases_on `e_exec ctx g_scope_list scope_list e` >> (
   fs []
  ) >>
  PairCases_on `x` >>
  fs []
 ],

 (* Variable lookup *)
 Cases_on `lookup_vexp2 scope_list g_scope_list x` >> (
  fs []
 )
]
QED

Theorem exec_stmt_ass_SOME_REWRS:
!ctx ascope ascope' g_scope_list g_scope_list' funn lval e stmt_stack frame_list' scope_list status'.
stmt_exec ctx (ascope, g_scope_list, [(funn, (stmt_ass lval e)::stmt_stack, scope_list)], status_running) =
        SOME (ascope', g_scope_list', frame_list', status') <=>
 (is_v e ==>
  ?scope_list'' scope_list'.
   (stmt_exec_ass lval e (scope_list++g_scope_list) = SOME scope_list'') /\
   (separate scope_list'' = (SOME g_scope_list', SOME scope_list')) /\
   (frame_list' = [(funn, (stmt_empty)::stmt_stack, scope_list')])) /\
 (~is_v e ==>
  ?e' frame_list''.
   (e_exec ctx g_scope_list scope_list e = SOME (e', frame_list'')) /\
   (g_scope_list' = g_scope_list) /\
   (frame_list' = (frame_list''++[(funn, (stmt_ass lval e')::stmt_stack, scope_list)]))) /\
 scope_list <> [] /\
 ascope' = ascope /\
 status' = status_running
Proof
rpt strip_tac >>
Cases_on `scope_list` >> Cases_on `stmt_stack` >> (
 fs [stmt_exec_def]
) >>
Cases_on `is_v e` >> (
 fs []
) >| [
 Cases_on `stmt_exec_ass lval e ((h::t) ++ g_scope_list)` >> (
  fs []
 ) >>
 Cases_on `separate x` >>  Cases_on `q` >>  Cases_on `r` >> (
  fs []
 ) >>
 metis_tac [],

 Cases_on `e_exec ctx g_scope_list (h::t) e` >> (
  fs []
 ) >>
 PairCases_on `x` >>
 fs [] >>
 metis_tac [],

 Cases_on `stmt_exec_ass lval e ((h::t) ++ g_scope_list)` >> (
  fs []
 ) >>
 Cases_on `separate x` >>  Cases_on `q` >>  Cases_on `r` >> (
  fs []
 ) >>
 metis_tac [],

 Cases_on `e_exec ctx g_scope_list (h::t) e` >> (
  fs []
 ) >>
 PairCases_on `x` >>
 fs [] >>
 IMP_RES_TAC e_exec_new_frame >> (
  fs []
 ) >| [
  metis_tac [],

  metis_tac []  
 ]
]
QED

Theorem exec_stmt_trans_SOME_REWRS:
!ctx ascope ascope' g_scope_list g_scope_list' funn e stmt_stack frame_list' scope_list status'.
stmt_exec ctx (ascope, g_scope_list, [(funn, (stmt_trans e)::stmt_stack, scope_list)], status_running) =
        SOME (ascope', g_scope_list', frame_list', status') <=>
 (is_v e ==>
  is_v_str e /\
  ?status''.
   stmt_exec_trans e = SOME status'' /\
   frame_list' = [(funn,stmt_empty::stmt_stack,scope_list)] /\ status' = status'') /\
 (~is_v e ==>
  ?e' frame_list''.
   e_exec ctx g_scope_list scope_list e = SOME (e', frame_list'') /\
   frame_list' = frame_list'' ++ [(funn,(stmt_trans e')::stmt_stack,scope_list)] /\
   status' = status_running) /\
 g_scope_list' = g_scope_list /\
 scope_list <> [] /\
 ascope' = ascope
Proof
rpt strip_tac >>
Cases_on `scope_list` >> Cases_on `stmt_stack` >> Cases_on `is_v e` >> (
 fs [stmt_exec_def]
) >| [
 (* TODO: Not needed? *)
 Cases_on `is_v_str e` >> (
  fs []
 ) >>
 Cases_on `stmt_exec_trans e` >> (
  fs []
 ) >>
 metis_tac [],

 Cases_on `e_exec ctx g_scope_list (h::t) e` >> (
  fs []
 ) >>
 PairCases_on `x` >> (
  fs []
 ) >>
 metis_tac [],

 Cases_on `is_v_str e` >> (
  fs []
 ) >>
 Cases_on `stmt_exec_trans e` >> (
  fs []
 ) >>
 metis_tac [],

 Cases_on `e_exec ctx g_scope_list (h::t) e` >> (
  fs []
 ) >>
 PairCases_on `x` >>
 fs [] >>
 IMP_RES_TAC e_exec_new_frame >> (
  fs []
 ) >| [
  metis_tac [],

  metis_tac []
 ]
]
QED

Theorem exec_stmt_cond_SOME_REWRS:
!ctx ascope ascope' g_scope_list g_scope_list' funn e stmt1 stmt2 stmt_stack frame_list' scope_list status'.
stmt_exec ctx (ascope, g_scope_list, [(funn, (stmt_cond e stmt1 stmt2)::stmt_stack, scope_list)], status_running) =
        SOME (ascope', g_scope_list', frame_list', status') <=>
 (is_v_bool e ==>
  ?b.
   stmt_exec_cond e = SOME b /\
   (b = T ==> frame_list' = [(funn, stmt1::stmt_stack, scope_list)]) /\
   (b = F ==> frame_list' = [(funn, stmt2::stmt_stack, scope_list)])) /\
 (~is_v_bool e ==>
  ?e' frame_list''.
   e_exec ctx g_scope_list scope_list e = SOME (e', frame_list'') /\
   frame_list' = frame_list'' ++ [(funn, (stmt_cond e' stmt1 stmt2)::stmt_stack, scope_list)]) /\
 g_scope_list' = g_scope_list /\
 scope_list <> [] /\
 ascope' = ascope /\
 status' = status_running
Proof
rpt strip_tac >>
Cases_on `scope_list` >> Cases_on `stmt_stack` >> Cases_on `is_v_bool e` >> (
 fs [stmt_exec_def]
) >| [
 Cases_on `stmt_exec_cond e` >> (
  fs []
 ) >>
 Cases_on `x` >> (
  fs []
 ) >| [
  metis_tac [],

  metis_tac []
 ],

 Cases_on `e_exec ctx g_scope_list (h::t) e` >> (
  fs []
 ) >>
 Cases_on `x` >> (
  fs []
 ) >>
 metis_tac [],

 Cases_on `stmt_exec_cond e` >> (
  fs []
 ) >>
 Cases_on `x` >> (
  fs []
 ) >| [
  metis_tac [],

  metis_tac []
 ],

 Cases_on `e_exec ctx g_scope_list (h::t) e` >> (
  fs []
 ) >>
 PairCases_on `x` >>
 fs [] >>
 IMP_RES_TAC e_exec_new_frame >> (
  fs []
 ) >| [
  metis_tac [],

  metis_tac []
 ]
]
QED

Theorem exec_stmt_app_SOME_REWRS:
!apply_table_f ext_map func_map b_func_map pars_map tbl_map ascope ascope' g_scope_list g_scope_list' funn t_name e_l stmt_stack frame_list' scope_list status'.
stmt_exec (apply_table_f, ext_map, func_map, b_func_map, pars_map, tbl_map) (ascope, g_scope_list, [(funn, (stmt_app t_name e_l)::stmt_stack, scope_list)], status_running) =
        SOME (ascope', g_scope_list', frame_list', status') <=>
 (index_not_const e_l = NONE  ==> ?mk_l f f_args default_f default_f_args. ALOOKUP tbl_map t_name = SOME (mk_l, (default_f, default_f_args)) /\
                       apply_table_f (t_name, e_l, mk_l, (default_f, default_f_args), ascope) = SOME (f, f_args) /\
                       is_consts_exec f_args /\
                       LENGTH mk_l = LENGTH e_l /\
                       frame_list' = [(funn, (stmt_ass lval_null (e_call (funn_name f) f_args))::stmt_stack, scope_list)]) /\
 (!i. index_not_const e_l = SOME i ==>
  ?e' frame_list''. e_exec (apply_table_f, ext_map, func_map, b_func_map, pars_map, tbl_map) g_scope_list scope_list (EL i e_l) = SOME (e', frame_list'') /\
                    frame_list' = frame_list'' ++ [(funn, (stmt_app t_name (LUPDATE e' i e_l))::stmt_stack, scope_list)]) /\
 g_scope_list' = g_scope_list /\
 scope_list <> [] /\
 ascope' = ascope /\
 status' = status_running
Proof
rpt strip_tac >>
Cases_on `scope_list` >> Cases_on `stmt_stack` >> Cases_on `index_not_const e_l` >> (
 fs [stmt_exec_def]
) >| [
 Cases_on `ALOOKUP tbl_map t_name` >> (
  fs []
 ) >>
 PairCases_on `x` >>
 fs [] >>
 Cases_on `apply_table_f (t_name,e_l,x0,(x1,x2),ascope)` >> (
  fs []
 ) >>
 PairCases_on `x` >> (
  fs []
 ) >>
 metis_tac [],

 Cases_on `e_exec (apply_table_f,ext_map,func_map,b_func_map,pars_map,tbl_map) g_scope_list (h::t) (EL x e_l)` >> (
  fs []
 ) >>
 PairCases_on `x'` >>
 fs [] >>
 metis_tac [],

 Cases_on `ALOOKUP tbl_map t_name` >> (
  fs []
 ) >>
 PairCases_on `x` >>
 fs [] >>
 Cases_on `apply_table_f (t_name,e_l,x0,(x1,x2),ascope)` >> (
  fs []
 ) >>
 PairCases_on `x` >>
 fs [] >>
 Cases_on `LENGTH x0 = LENGTH e_l` >> (
  fs []
 ) >>
 Cases_on `is_consts_exec x1'` >> (
  fs []
 ) >>
 metis_tac [],

 Cases_on `e_exec (apply_table_f,ext_map,func_map,b_func_map,pars_map,tbl_map) g_scope_list (h::t) (EL x e_l)` >> (
  fs []
 ) >>
 PairCases_on `x'` >>
 fs [] >>
 IMP_RES_TAC e_exec_new_frame >> (
  fs []
 ) >| [
  metis_tac [],

  metis_tac []
 ]
]
QED

Theorem exec_stmt_ret_SOME_REWRS:
!ctx ascope ascope' g_scope_list g_scope_list' funn e stmt_stack frame_list' scope_list status'.
stmt_exec ctx (ascope, g_scope_list, [(funn, (stmt_ret e)::stmt_stack, scope_list)], status_running) =
        SOME (ascope', g_scope_list', frame_list', status') <=>
 (!v. get_v e = SOME v ==>
  frame_list' = [(funn,stmt_empty::stmt_stack,scope_list)] /\
  status' = status_returnv v) /\
 (get_v e = NONE ==>
  ?e' frame_list''.
  e_exec ctx g_scope_list scope_list e = SOME (e', frame_list'') /\
  frame_list' = frame_list'' ++ [(funn,(stmt_ret e')::stmt_stack,scope_list)] /\
  status' = status_running) /\
 g_scope_list' = g_scope_list /\
 scope_list <> [] /\
 ascope' = ascope
Proof
rpt strip_tac >>
Cases_on `scope_list` >> Cases_on `stmt_stack` >> Cases_on `get_v e` >> (
 fs [stmt_exec_def]
) >| [
 Cases_on `e_exec ctx g_scope_list (h::t) e` >> (
  fs []
 ) >>
 PairCases_on `x` >>
 fs [] >>
 metis_tac [],

 metis_tac [],

 Cases_on `e_exec ctx g_scope_list (h::t) e` >> (
  fs []
 ) >>
 PairCases_on `x` >>
 fs [] >>
 IMP_RES_TAC e_exec_new_frame >> (
  fs []
 ) >| [
  metis_tac [],

  metis_tac []
 ],

 metis_tac []
]
QED

Theorem exec_stmt_ext_SOME_REWRS:
!apply_table_f ext_map func_map b_func_map pars_map tbl_map ascope ascope' g_scope_list g_scope_list' funn stmt_stack frame_list' scope_list status'.
stmt_exec (apply_table_f, ext_map, func_map, b_func_map, pars_map, tbl_map) (ascope, g_scope_list, [(funn, stmt_ext::stmt_stack, scope_list)], status_running) =
        SOME (ascope', g_scope_list', frame_list', status') <=>
 (?ext_fun.
   lookup_ext_fun funn ext_map = SOME ext_fun /\
   ?scope_list'' ascope'' status''.
    ext_fun (ascope, g_scope_list, scope_list) = SOME (ascope'', scope_list'', status'') /\
    g_scope_list' = g_scope_list /\
    frame_list' = [(funn, stmt_empty::stmt_stack, scope_list'')] /\
    status' = status'' /\
    scope_list <> [] /\
    ascope' = ascope'')
Proof
rpt strip_tac >>
Cases_on `scope_list` >> Cases_on `stmt_stack` >> (
 fs [stmt_exec_def]
) >| [
 Cases_on `lookup_ext_fun funn ext_map` >> (
  fs []
 ) >>
 Cases_on `x (ascope,g_scope_list,h::t)` >> (
  fs []
 ) >>
 PairCases_on `x'` >>
 fs [] >>
 metis_tac [],

 Cases_on `lookup_ext_fun funn ext_map` >> (
  fs []
 ) >>
 Cases_on `x (ascope,g_scope_list,h::t)` >> (
  fs []
 ) >>
 PairCases_on `x'` >>
 fs [] >>
 metis_tac []
]
QED

Theorem exec_stmt_block_SOME_REWRS:
!ctx ascope ascope' g_scope_list g_scope_list' funn decl_list stmt stmt_stack frame_list' scope_list status'.
stmt_exec ctx (ascope, g_scope_list, [(funn, (stmt_block decl_list stmt)::stmt_stack, scope_list)], status_running) =
        SOME (ascope', g_scope_list', frame_list', status') <=>
 scope_list <> [] /\
 g_scope_list' = g_scope_list /\
 frame_list' = [(funn, stmt::(stmt_empty::stmt_stack), ((declare_list_in_fresh_scope decl_list)::(scope_list)))] /\
 ascope' = ascope /\
 status' = status_running
Proof
rpt strip_tac >>
Cases_on `scope_list` >> Cases_on `stmt_stack` >> (
 fs [stmt_exec_def]
) >> (
 metis_tac []
)
QED

Theorem stmt_exec_block:
!ctx ascope ascope' g_scope_list g_scope_list' funn frame' funn' stmt stmt_stack stmt_stack' h_scope scope_list scope_list' status'.
stmt <> stmt_empty ==>
stmt_exec ctx
          (ascope,g_scope_list,[(funn,stmt::stmt_stack,h_scope::scope_list)],status_running) =
        SOME
          (ascope',g_scope_list',frame'++[(funn',stmt_stack',scope_list')],status') ==>
?stmt_stack''. stmt_stack''++stmt_stack = stmt_stack' /\
stmt_exec ctx
          (ascope,g_scope_list,[(funn,[stmt],h_scope::scope_list)],status_running) =
        SOME
          (ascope',g_scope_list',frame'++[(funn',stmt_stack'',scope_list')],status')
Proof
rpt strip_tac >>
Cases_on `stmt` >> (
 fs []
) >| [
 (* Assign *)
 fs [exec_stmt_ass_SOME_REWRS] >>
 Cases_on `is_v e` >> (
  fs []
 ),

 (* Conditional *)
 fs [exec_stmt_cond_SOME_REWRS] >>
 Cases_on `is_v_bool e` >> (
  fs []
 ) >>
 Cases_on `b` >> (
  fs []
 ),

 (* Block entry *)
 fs [exec_stmt_block_SOME_REWRS],

 (* Return *)
 fs [exec_stmt_ret_SOME_REWRS] >>
 Cases_on `get_v e` >> (
  fs []
 ),

 (* Seq *)
 Cases_on `stmt_stack` >> (
  fs []
 ) >>
 fs [stmt_exec_def] >>
 Cases_on `is_empty s` >> (
  fs []
 ) >>
 Cases_on `stmt_exec ctx
               (ascope,g_scope_list,[(funn,[s],h_scope::scope_list)],status_running)` >> (
  fs []
 ) >>
 PairCases_on `x` >> (
  fs []
 ) >>
 Cases_on `x2` >> (
  fs []
 ) >>
 Cases_on `t'` >> (
  fs []
 ) >| [
  PairCases_on `h'` >> (
   fs []
  ) >>
  Cases_on `h'1` >> (
   fs []
  ) >>
  Cases_on `t'` >> (
   fs []
  ) >| [
   Cases_on `x3` >> (
    fs []
   ),

   Cases_on `t''` >> (
    fs []
   ) >>
   Cases_on `x3` >> (
    fs []
   )
  ],

  Cases_on `t''` >> (
   fs []
  ) >>
  Cases_on `x3` >> (
   fs []
  ) >>
(* TODO: Why needed to add this??? *)
  PairCases_on `h''` >> (
   fs []
  ) >>
  Cases_on `h''1` >> (
   fs []
  ) >>
  Cases_on `t'` >> (
   fs []
  ) >>
(* TODO: End of new addition *)
  PairCases_on `h'` >>
  fs [] >>
  Cases_on `h'1` >> (
   fs []
  ) >>
  Cases_on `frame'` >> (
   fs []
  ) >| [
   Cases_on `t'` >> (
    fs []
   ) >>
   Cases_on `t''` >> (
    fs []
   ),

   Cases_on `t'` >> (
    fs []
   ) >>
   Cases_on `t'3'` >> (
    fs []
   )
  ]
 ],

 (* Transition *)
 fs [exec_stmt_trans_SOME_REWRS] >>
 Cases_on `is_v e` >> (
  fs []
 ),

 (* Apply *)
 PairCases_on `ctx` >>
 fs [exec_stmt_app_SOME_REWRS] >>
 Cases_on `index_not_const l` >> (
  fs []
 ),

 (* Extern *)
 PairCases_on `ctx` >>
 fs [exec_stmt_ext_SOME_REWRS]
]
QED

Theorem stmt_exec_block_sing:
!ctx ascope ascope' g_scope_list g_scope_list' funn funn' stmt stmt_stack stmt_stack' h_scope scope_list scope_list' status'.
stmt <> stmt_empty ==>
stmt_exec ctx
          (ascope,g_scope_list,[(funn,stmt::stmt_stack,h_scope::scope_list)],status_running) =
        SOME
          (ascope',g_scope_list',[(funn',stmt_stack',scope_list')],status') ==>
?stmt_stack''. stmt_stack''++stmt_stack = stmt_stack' /\
stmt_exec ctx
          (ascope,g_scope_list,[(funn,[stmt],h_scope::scope_list)],status_running) =
        SOME
          (ascope',g_scope_list',[(funn',stmt_stack'',scope_list')],status')
Proof
rpt strip_tac >>
IMP_RES_TAC (Q.SPECL [`ctx`, `ascope`, `ascope'`, `g_scope_list`, `g_scope_list'`, `funn`, `[]`] stmt_exec_block) >>
fs [listTheory.APPEND_NIL]
QED

(* TODO: This should track some invariants of stmt_exec under regular conditions,
 * i.e. funn of current frame, ... *)
Theorem stmt_exec_inv_sing:
!ctx ascope ascope' g_scope_list g_scope_list' frame' funn funn' stmt_stack stmt_stack' scope_list scope_list' status status'.
stmt_exec ctx (ascope, g_scope_list, [(funn,stmt_stack,scope_list)], status) =
 SOME (ascope', g_scope_list', frame'++[(funn',stmt_stack',scope_list')], status') ==>
funn = funn' /\
(frame' = [] \/
 ?funn'' stmt' scope'.
  frame' = [(funn'', [stmt'], [scope'])]
)
Proof
`!ctx ascope g_scope_list funn stmt_stack scope_list status.
 (\ctx' state'.
  !ascope' g_scope_list' funn' stmt_stack' scope_list' status' ascope'' g_scope_list'' frame'' funn'' stmt_stack'' scope_list'' status''.
  state' = (ascope',g_scope_list',[(funn',stmt_stack',scope_list')],status') ==>
  stmt_exec ctx' (ascope',g_scope_list',[(funn',stmt_stack',scope_list')],status') =
   SOME (ascope'', g_scope_list'', frame''++[(funn'',stmt_stack'',scope_list'')], status'') ==>
  (funn' = funn'' /\
   (frame'' = [] \/
    ?funn''' stmt'' scope''.
     frame'' = [(funn''', [stmt''], [scope''])]
   ))
 ) ctx (ascope, g_scope_list, [(funn,stmt_stack,scope_list)], status)` suffices_by (
 metis_tac []
) >>
rpt strip_tac >>
irule stmt_exec_ind >>
rpt strip_tac >| [
 (* Apply *)
 fs [exec_stmt_app_SOME_REWRS] >>
 rpt strip_tac >> (
  Cases_on `index_not_const e_l` >> (
   fs []
  )
 ) >>
 metis_tac [e_exec_new_frame],

 (* Extern *)
 rename1 `[(funn,[stmt_ext],scope::scope_list)]` >>
 fs [stmt_exec_def] >>
 Cases_on `lookup_ext_fun funn ext_map` >> (
  fs []
 ) >>
 Cases_on `x (ascope,g_scope_list,scope::scope_list)` >> (
  fs []
 ) >>
 PairCases_on `x'` >> (
  fs []
 ),

 (* Return *)
 fs [exec_stmt_ret_SOME_REWRS] >>
 rpt strip_tac >> (
  Cases_on `get_v e` >> (
   fs []
  )
 ) >>
 metis_tac [e_exec_new_frame],

 (* Trans *)
 fs [exec_stmt_trans_SOME_REWRS] >>
 metis_tac [e_exec_new_frame],

 (* Return (stack case) *)
 fs [exec_stmt_ret_SOME_REWRS] >>
 metis_tac [],

 (* Trans (stack case) *)
 fs [exec_stmt_trans_SOME_REWRS] >>
 metis_tac [],

 (* Cond *)
 fs [exec_stmt_cond_SOME_REWRS] >>
 metis_tac [e_exec_new_frame],

 (* Cond (stack case) *)
 fs [exec_stmt_cond_SOME_REWRS] >>
 metis_tac [],

 (* Apply (stack case) *)
 rename1 `stmt_app t_name e_l` >>
 fs [] >>
 rpt strip_tac >> (
  subgoal `stmt_app t_name e_l <> stmt_empty` >- (
   fs []
  ) >>
  IMP_RES_TAC stmt_exec_block >>
  fs [exec_stmt_app_SOME_REWRS]
 ),

 fs [stmt_exec_def],

 (* Block entry *)
 fs [exec_stmt_block_SOME_REWRS],

 fs [stmt_exec_def],

 (* Block exit *)
 fs [stmt_exec_def] >>
 Cases_on `stmt_stack` >> (
  fs []
 ),

 fs [stmt_exec_def],

 (* Assign *)
 fs [exec_stmt_ass_SOME_REWRS] >>
 metis_tac [e_exec_new_frame],

 (* Assign (stack case) *)
 fs [exec_stmt_ass_SOME_REWRS] >>
 metis_tac [],

 (* Extern (stack case) *)
 fs [] >>
 rpt strip_tac >>
 subgoal `stmt_ext <> stmt_empty` >- (
  fs []
 ) >>
 IMP_RES_TAC stmt_exec_block >>
 fs [exec_stmt_ext_SOME_REWRS],

 (* Seq *)
 fs [stmt_exec_def] >>
 Cases_on `is_empty stmt1` >> (
  fs []
 ) >>
 rename1 `[(funn,[stmt1],scope::scope_list)]` >>
 Cases_on `stmt_exec ctx
               (ascope,g_scope_list,[(funn,[stmt1],scope::scope_list)],status_running)` >> (
  fs []
 ) >>
 PairCases_on `x` >>
 fs [] >>
 Cases_on `x2` >> (
  fs []
 ) >>
 Cases_on `t` >> (
  fs []
 ) >| [
  PairCases_on `h` >>
  fs [] >>
  Cases_on `h1` >> (
   fs []
  ) >>
  Cases_on `t` >> (
   fs []
  ) >| [
   Cases_on `x3` >> (
    fs []
   ),

   Cases_on `t'` >> (
    fs []
   ) >>
   Cases_on `x3` >> (
    fs []
   )
  ],

  Cases_on `t'` >> (
   fs []
  ) >>
  Cases_on `x3` >> (
   fs []
  ) >>
  PairCases_on `h'` >>
  fs [] >>
  Cases_on `h'1` >> (
   fs []
  ) >>
  Cases_on `t` >> (
   fs []
  )
 ],

 (* Seq (stack case) *)
 fs [] >>
 rpt strip_tac >>
 rename1 `stmt_seq stmt1 stmt2` >>
 subgoal `stmt_seq stmt1 stmt2 <> stmt_empty` >- (
  fs []
 ) >>
 IMP_RES_TAC stmt_exec_block >>
 fs [stmt_exec_def],

 (* Initial trans status *)
 fs [stmt_exec_def],

 (* Initial return status *)
 fs [stmt_exec_def],

 fs [],

 fs []
]
QED

Theorem stmt_exec_inv_sing_noframe:
!ctx ascope ascope' g_scope_list g_scope_list' funn funn' stmt_stack stmt_stack' scope_list scope_list' status status'.
stmt_exec ctx (ascope, g_scope_list, [(funn,stmt_stack,scope_list)], status) =
 SOME (ascope', g_scope_list', [(funn',stmt_stack',scope_list')], status') ==>
funn = funn'
Proof
rpt strip_tac >>
ASSUME_TAC (Q.SPECL [`ctx`, `ascope`, `ascope'`, `g_scope_list`, `g_scope_list'`, `[]`] stmt_exec_inv_sing) >>
fs [listTheory.APPEND_NIL] >>
metis_tac []
QED

Theorem exec_stmt_seq_SOME_REWRS:
!ctx ascope ascope' g_scope_list g_scope_list' funn stmt1 stmt2 stmt_stack frame_list' scope_list status'.
stmt_exec ctx (ascope, g_scope_list, [(funn, (stmt_seq stmt1 stmt2)::stmt_stack, scope_list)], status_running) =
        SOME (ascope', g_scope_list', frame_list', status') <=>
 scope_list <> [] /\
 (is_empty stmt1 ==>
  g_scope_list' = g_scope_list /\
  frame_list' = [(funn, stmt2::stmt_stack, scope_list)] /\
  ascope' = ascope /\
  status' = status_running) /\
 (~is_empty stmt1 ==>
  ?g_scope_list'' frame_list'' ascope'' status''.
   stmt_exec ctx (ascope, g_scope_list, [(funn, [stmt1], scope_list)], status_running) =
    SOME (ascope'', g_scope_list'', frame_list'', status'') /\
   g_scope_list' = g_scope_list'' /\
   ascope' = ascope'' /\
   status' = status'' /\ (
   (?stmt1' scope_list'.
     frame_list'' = [(funn, [stmt1'], scope_list')] /\
     (status'' = status_running ==> frame_list' = [(funn, (stmt_seq stmt1' stmt2)::stmt_stack, scope_list')]) /\
     (status'' <> status_running ==> frame_list' = [(funn, stmt1'::stmt_stack, scope_list')])) \/
   (?stmt1' stmt1'' scope_list'.
     frame_list'' = [(funn, stmt1''::([stmt1']), scope_list')] /\
     status'' = status_running /\
     frame_list' = [(funn, stmt1''::((stmt_seq stmt1' stmt2)::stmt_stack), scope_list')]
     ) \/
   (?stmt1' funn' stmt' scope' scope_list'.
     frame_list'' = ((funn', [stmt'], [scope'])::[(funn, [stmt1'], scope_list')]) /\
     status'' = status_running /\
     frame_list' = ((funn', [stmt'], [scope'])::[(funn, (stmt_seq stmt1' stmt2)::stmt_stack, scope_list')]))))
Proof
rpt strip_tac >>
Cases_on `scope_list` >> Cases_on `stmt_stack` >> Cases_on `is_empty stmt1` >> (
 fs [stmt_exec_def]
) >| [
 metis_tac [],

 Cases_on `stmt_exec ctx
             (ascope,g_scope_list,[(funn,[stmt1],h::t)],status_running)` >> (
  fs []
 ) >>
 PairCases_on `x` >>
 fs [] >>
 Cases_on `x2` >> (
  fs []
 ) >>
 Cases_on `t'` >> (
  fs []
 ) >| [
  PairCases_on `h'` >>
  fs [] >>
  Cases_on `h'1` >> (
   fs []
  ) >>
  Cases_on `t'` >> (
   fs []
  ) >| [
   Cases_on `x3` >> (
    Cases_on `status'` >> (
     fs []
    )
   ) >> (
    metis_tac [stmt_exec_inv_sing_noframe]
   ),

   Cases_on `t''` >> (
    fs []
   ) >>
   Cases_on `x3` >> (
    Cases_on `status'` >> (
     fs []
    )
   ) >>
   metis_tac [stmt_exec_inv_sing_noframe]
  ],

  Cases_on `t''` >> (
   fs []
  ) >>
  Cases_on `x3` >> (
   fs []
  ) >- (
   PairCases_on `h''` >>
   fs [] >>
   Cases_on `h''1` >> (
    fs []
   ) >>
   Cases_on `t'` >> (
    fs []
   ) >>
   assume_tac (Q.SPECL [`ctx`, `ascope`, `x0`, `g_scope_list`, `x1`, `[h']`] stmt_exec_inv_sing) >>
   fs [] >>
   RES_TAC >>
   `funn = h''0` suffices_by (
    metis_tac []
   ) >>
   fs [] >>
   metis_tac []
  ) >> (
   Cases_on `status'` >> (
    fs []
   )
  )
 ],

 metis_tac [],

 Cases_on `stmt_exec ctx
             (ascope,g_scope_list,[(funn,[stmt1],h::t)],status_running)` >> (
  fs []
 ) >>
 PairCases_on `x` >>
 fs [] >>
 Cases_on `x2` >> (
  fs []
 ) >>
 Cases_on `t''` >> (
  fs []
 ) >| [
  PairCases_on `h''` >>
  fs [] >>
  Cases_on `h''1` >> (
   fs []
  ) >>
  Cases_on `t''` >> (
   fs []
  ) >| [
   Cases_on `x3` >> (
    Cases_on `status'` >> (
     fs []
    )
   ) >> (
    metis_tac [stmt_exec_inv_sing_noframe]
   ),

   Cases_on `t'''` >> (
    fs []
   ) >>
   Cases_on `x3` >> (
    Cases_on `status'` >> (
     fs []
    )
   ) >>
   metis_tac [stmt_exec_inv_sing_noframe]
  ],

  Cases_on `t'''` >> (
   fs []
  ) >>
  Cases_on `x3` >> (
   Cases_on `status'` >> (
    fs []
   )
  ) >> (
   PairCases_on `h'''` >>
   fs [] >>
   Cases_on `h'''1` >> (
    fs []
   ) >>
   Cases_on `t''` >> (
    fs []
   )
  ) >| [
   (* Running *)
   PairCases_on `h''` >>
   fs [] >>
   Cases_on `h''1` >> (
    fs []
   ) >>
   assume_tac (Q.SPECL [`ctx`, `ascope`, `x0`, `g_scope_list`, `x1`, `[(h''0,h''::t'',h''2)]`] stmt_exec_inv_sing) >>
   fs [] >>
   RES_TAC >>
   Cases_on `t''` >> (
    fs []
   ) >>
   metis_tac [],

   (* Return *)
   PairCases_on `h''` >>
   fs [] >>
   Cases_on `h''1` >> (
    fs []
   ) >>
   Cases_on `t''` >> (
    fs []
   ) >>
   Cases_on `t'''` >> (
    fs []
   ),

   (* Transition *)
   PairCases_on `h''` >>
   fs [] >>
   Cases_on `h''1` >> (
    fs []
   ) >>
   Cases_on `t''` >> (
    fs []
   ) >>
   Cases_on `t'''` >> (
    fs []
   )
  ]
 ]
]
QED

(* TODO: Make use of something like the below
val exec_stmt_REWRS =
  [exec_stmt_ext_SOME_REWRS,
   exec_stmt_app_SOME_REWRS,
   exec_stmt_ret_SOME_REWRS,
   exec_stmt_trans_SOME_REWRS,
   exec_stmt_cond_SOME_REWRS,
   exec_stmt_block_SOME_REWRS,
   exec_stmt_ass_SOME_REWRS,
   exec_stmt_seq_SOME_REWRS];
*)


(* Reduction of a single statement is invariant over the addition of a lower statement stack. *)
(* Converse to stmt_exec_block *)
Theorem stmt_exec_lemma:
!ctx ascope g_scope1 g_scope2 g_scope1' g_scope2' funn stmt stmt' stmts scope_list scope_list'.
stmt_exec (ctx:'a ctx)
          (ascope,[g_scope1; g_scope2],[(funn,[stmt],scope_list)],
           status_running) =
 SOME (ascope,[g_scope1'; g_scope2'],[(funn,[stmt'],scope_list')],status_running) ==>
stmt_exec (ctx:'a ctx)
               (ascope,[g_scope1; g_scope2],[(funn,stmt::stmts,scope_list)],
                status_running) =
 SOME (ascope,[g_scope1'; g_scope2'],[(funn,stmt'::stmts,scope_list')],status_running)
Proof
Induct_on ‘stmt’ >- (
 rpt strip_tac >>
 Cases_on ‘scope_list’ >> (
  fs[stmt_exec_def]
 )
) >- (
 fs[exec_stmt_ass_SOME_REWRS]
) >- (
 fs[exec_stmt_cond_SOME_REWRS]
) >- (
 fs[exec_stmt_block_SOME_REWRS]
) >- (
 fs[exec_stmt_ret_SOME_REWRS]
) >- (
 fs[exec_stmt_seq_SOME_REWRS]
) >- (
 fs[exec_stmt_trans_SOME_REWRS]
) >- (
 rpt strip_tac >>
 PairCases_on ‘ctx’ >>
 fs[exec_stmt_app_SOME_REWRS]
) >- (
 rpt strip_tac >>
 PairCases_on ‘ctx’ >>
 fs[exec_stmt_ext_SOME_REWRS]
)
QED

(* This states an invariant of the steps where the final status is Return *)
Theorem stmt_exec_status_returnv_inv:
!ctx ascope ascope' g_scope_list g_scope_list' funn stmt_stack scope_list frame_list' v.
stmt_exec ctx (ascope, g_scope_list, [(funn, stmt_stack, scope_list)], status_running) =
        SOME (ascope', g_scope_list', frame_list', status_returnv v) ==>
(* TODO: No longer holds when extern can change status to Return... *)
(* ascope' = ascope /\
 g_scope_list' = g_scope_list /\ *)
 ?stmt_stack' scope_list'. frame_list' = [(funn, stmt_stack', scope_list')]
Proof
`!ctx ascope g_scope_list funn stmt_stack scope_list.
 (\ctx' state'.
  !ascope' g_scope_list' funn' stmt_stack' scope_list' ascope'' g_scope_list'' frame_list'' v''.
  state' = (ascope',g_scope_list',[(funn',stmt_stack',scope_list')],status_running) ==>
  stmt_exec ctx' (ascope',g_scope_list',[(funn',stmt_stack',scope_list')],status_running) =
   SOME (ascope'', g_scope_list'', frame_list'', status_returnv v'') ==>
  (?stmt_stack'' scope_list''. frame_list'' = [(funn', stmt_stack'', scope_list'')])
 ) ctx (ascope, g_scope_list, [(funn,stmt_stack,scope_list)], status_running)` suffices_by (
 metis_tac []
) >>
rpt strip_tac >>
irule stmt_exec_ind >>
rpt strip_tac >| [
 fs [exec_stmt_app_SOME_REWRS],

 fs [exec_stmt_ext_SOME_REWRS] >>
 rpt strip_tac >>
 qexistsl_tac [`[stmt_empty]`, `scope_list''`] >>
 fs [],

 fs [exec_stmt_ret_SOME_REWRS] >>
 rpt strip_tac >>
 Cases_on `get_v e` >> (
  fs []
 ),

 fs [exec_stmt_trans_SOME_REWRS],

 fs [exec_stmt_ret_SOME_REWRS] >>
 rpt strip_tac >>
 rename1 `get_v e` >>
 Cases_on `get_v e` >> (
  fs []
 ),

 fs [exec_stmt_trans_SOME_REWRS],

 fs [exec_stmt_cond_SOME_REWRS],

 fs [exec_stmt_cond_SOME_REWRS],

 pairLib.PairCases_on `ctx` >>
 rename1 `(ctx0, ext_map, func_map, b_func_map, pars_map, tbl_map)` >>
 rename1 `(apply_table_f, ext_map, func_map, b_func_map, pars_map, tbl_map)` >>
 fs [exec_stmt_app_SOME_REWRS],

 fs [stmt_exec_def],

 fs [exec_stmt_block_SOME_REWRS],

 fs [stmt_exec_def] >>
 Cases_on `stmt_stack` >> (
  fs []
 ),

 fs [stmt_exec_def] >>
 Cases_on `stmt_stack` >> (
  fs []
 ),

 fs [stmt_exec_def],

 fs [exec_stmt_ass_SOME_REWRS],

 fs [exec_stmt_ass_SOME_REWRS],

 pairLib.PairCases_on `ctx` >>
 rename1 `(ctx0, ext_map, func_map, b_func_map, pars_map, tbl_map)` >>
 rename1 `(apply_table_f, ext_map, func_map, b_func_map, pars_map, tbl_map)` >>
 fs [exec_stmt_ext_SOME_REWRS] >>
 rpt strip_tac >>
 rename1 `stmt_empty::v218::v219` >>
 qexistsl_tac [`stmt_empty::v218::v219`, `scope_list''`] >>
 fs [],

 (* TODO: Written to avoid time-consuming simplification *)
 FULL_SIMP_TAC bool_ss [] >>
 rename1 `[(funn,[stmt_seq stmt1 stmt2],scope::scope_list)]` >>
 rpt strip_tac >> (
  fs [exec_stmt_seq_SOME_REWRS] >>
  rw [] >>
  Cases_on `is_empty stmt1` >> (
   fs []
  ) >| [
   fs [stmt_exec_def],

   fs [exec_stmt_seq_SOME_REWRS]
  ]
 ),

 (* TODO: Written to avoid time-consuming simplification *)
 FULL_SIMP_TAC bool_ss [] >>
 rename1 `[(funn,stmt_seq stmt1 stmt2::stmt'::stmt_stack,scope::scope_list)]` >>
 rpt strip_tac >> (
  subgoal `ascope = ascope' /\ g_scope_list = g_scope_list' /\ funn = funn' /\ scope::scope_list = scope_list'` >- (
   fs []
  ) >>
  PAT_X_ASSUM ``(ascope,g_scope_list,[(funn,stmt_seq stmt1 stmt2::stmt'::stmt_stack,scope::scope_list)],
                 status_running) =
                 (ascope',g_scope_list',[(funn',stmt_stack',scope_list')],
                  status_running)`` (fn thm => fs [GSYM thm]) >>
  fs [exec_stmt_seq_SOME_REWRS] >>
  rw [] >>
  gs []
 ),

 fs [stmt_exec_def],

 fs [stmt_exec_def],

 fs [],

 fs []
]
QED

(* Then, define an executable semantics which performs execution until out of fuel. *)
(* Note that all concrete operations remain the same *)
(* Note that expression multi-step execution makes little sense with the current semantics... *)
Definition stmt_multi_exec_def:
 (stmt_multi_exec _ state 0 =
  SOME state)
 /\
 (stmt_multi_exec ctx state (SUC fuel) =
  case stmt_exec ctx state of
  | SOME state' => stmt_multi_exec ctx state' fuel
  | NONE => NONE)
End

(**************************)
(*  Frame list semantics  *)
(**************************)

Definition frames_exec_def:
 (******************************************)
 (* Catch-all clauses for special statuses *)
 (frames_exec (ctx:'a ctx) ((ascope:'a, g_scope_list:g_scope_list, frame_list:frame_list, status_returnv v):'a state) = NONE)
  /\
 (frames_exec _ (_, _, _, status_trans x) = NONE)
  /\
 (* Empty frame list *)
 (frames_exec _ (_, _, [], _) = NONE)
  /\
 (*********)
 (* Comp2 + Comp1 case of multiple frames *)
 (frames_exec (apply_table_f, ext_map, func_map, b_func_map, pars_map, tbl_map) (ascope, g_scope_list, ((funn, stmt_stack, scope_list)::((funn', stmt_stack', scope_list')::frame_list'')), status_running) =
  (case scopes_to_pass funn func_map b_func_map g_scope_list of
   | SOME g_scope_list' =>
    (case map_to_pass funn b_func_map of
     | SOME b_func_map' =>
      (case tbl_to_pass funn b_func_map tbl_map of
       | SOME tbl_map' =>
        (case stmt_exec (apply_table_f, ext_map, func_map, b_func_map', pars_map, tbl_map') (ascope, g_scope_list', [(funn, stmt_stack, scope_list)], status_running) of
         | SOME (ascope', g_scope_list'', frame_list', status') =>
          (case status' of
           | status_returnv v =>
            (* Comp2 *)
            (case frame_list' of
             | [(funn, stmt_stack'', scope_list'')] =>
              (case assign g_scope_list'' v (lval_varname (varn_star funn)) of
               | SOME g_scope_list''' =>
                (case scopes_to_retrieve funn func_map b_func_map g_scope_list g_scope_list''' of
                 | SOME g_scope_list'''' =>
                  (case lookup_funn_sig_body funn func_map b_func_map ext_map of
                   | SOME (stmt'', x_d_l) =>
                    (case scopes_to_pass funn' func_map b_func_map g_scope_list'''' of
                     | SOME g_scope_list''''' =>
                      (case copyout (MAP FST x_d_l) (MAP SND x_d_l) g_scope_list''''' scope_list' scope_list'' of
                       | SOME (g_scope_list'''''', scope_list''') =>
                        (case scopes_to_retrieve funn' func_map b_func_map g_scope_list'''' g_scope_list'''''' of
                         | SOME g_scope_list''''''' =>
                          SOME (ascope', g_scope_list''''''', ((funn', stmt_stack', scope_list''')::frame_list''), status_running)
                         | _ => NONE)
                       | _ => NONE)
                     | _ => NONE)
                   | _ => NONE)
                 | _ => NONE)
               | NONE => NONE)
             | _ => NONE)
           | _ => 
            (* Comp1 *)
            (case scopes_to_retrieve funn func_map b_func_map g_scope_list g_scope_list'' of
             | SOME g_scope_list''' =>
              SOME (ascope', g_scope_list''', frame_list'++((funn', stmt_stack', scope_list')::frame_list''), status')
             | _ => NONE))
         | _ => NONE)
       | _ => NONE)
     | _ => NONE)
   | _ => NONE))
  /\
 (*********)
 (* Comp1, remaining cases *)
 (frames_exec (apply_table_f, ext_map, func_map, b_func_map, pars_map, tbl_map) (ascope, g_scope_list, [(funn, stmt_stack, scope_list)], status_running) =
  (case scopes_to_pass funn func_map b_func_map g_scope_list of
   | SOME g_scope_list' =>
    (case map_to_pass funn b_func_map of
     | SOME b_func_map' =>
      (case tbl_to_pass funn b_func_map tbl_map of
       | SOME tbl_map' =>
        (case stmt_exec (apply_table_f, ext_map, func_map, b_func_map', pars_map, tbl_map') (ascope, g_scope_list', [(funn, stmt_stack, scope_list)], status_running) of
         | SOME (ascope', g_scope_list'', frame_list', status') =>
          (case scopes_to_retrieve funn func_map b_func_map g_scope_list g_scope_list'' of
           | SOME g_scope_list''' =>
            SOME (ascope', g_scope_list''', frame_list', status')
           | _ => NONE)
         | _ => NONE)
       | _ => NONE)
     | _ => NONE)
   | _ => NONE))
 /\
 (frames_exec _ _ = NONE)
End

(***********************************)
(*  Architectural-level semantics  *)
(***********************************)

Definition state_fin_exec_def:
 state_fin_exec status frame_list =
  case frame_list of
  | [(funn, [stmt_empty], scope_list)] =>
   (case status of
    | status_trans x =>
     if x = "accept" \/ x = "reject"
     then T
     else F
    | _ => T)
  | _ =>
   (case status of
    | status_returnv v => T
    | status_trans x =>
     if x = "accept" \/ x = "reject"
     then T
     else F
    | _ => F)
End

Theorem state_fin_exec_equiv:
!status frame_list:frame_list.
 state_fin_exec status frame_list <=> state_fin status frame_list
Proof
fs [state_fin_def, state_fin_exec_def] >>
Cases_on `frame_list` >> (
 fs []
) >- (
 Cases_on `status` >> (
  fs []
 )
) >>
Cases_on `t` >> (
 fs []
) >- (
 PairCases_on `h` >>
 fs [] >>
 Cases_on `h1` >> (
  fs []
 ) >- (
  Cases_on `status` >> (
   fs []
  )
 ) >>
 Cases_on `h` >> (
  fs []
 ) >- (
  Cases_on `t` >> (
   fs []
  ) >> (
   Cases_on `status` >> (
    fs []
   )
  ) >- (
   metis_tac []
  )
 ) >> (
  Cases_on `status` >> (
   fs []
  )
 )
) >>
Cases_on `status` >> (
 fs []
)
QED

(* TODO: Outsource the stuff that causes too many case splits to other functions
 *       i.e. exec_arch_e, exec_arch_update_return_frame, exec_arch_assign, ... *)
Definition arch_exec_def:
 (arch_exec ((ab_list, pblock_map, ffblock_map, input_f, output_f, copyin_pbl, copyout_pbl, apply_table_f, ext_map, func_map):'a actx)
            (((i, in_out_list, in_out_list', scope):'a aenv), g_scope_list:g_scope_list, arch_frame_list_regular frame_list, status:status) =
  (case EL i ab_list of
   | (arch_block_pbl x el) =>
    (case ALOOKUP pblock_map x of
     | SOME (pbl_type, x_d_list, b_func_map, decl_list, pars_map, tbl_map) =>
      if state_fin_exec status frame_list
      then
       (case lookup_block_body x b_func_map of
        | SOME stmt =>
         (* TODO: The below LENGTH check is only used for proofs (e.g. soundness proof) *)
         (if LENGTH el = LENGTH x_d_list
          then
           (* pbl_ret *)
           (* TODO: OK to only copy out from block-global scope here? *)
           (case copyout_pbl (g_scope_list, scope, MAP SND x_d_list, MAP FST x_d_list, set_fin_status pbl_type status) of
            | SOME scope' =>
             SOME ((i+1, in_out_list, in_out_list', scope'), LASTN 1 g_scope_list,
                   arch_frame_list_empty, status_running)
            | _ => NONE)
          else NONE)
        | NONE => NONE)
      else
       (case status of
        | status_trans x' =>
         (* parser_trans *)
         (case pbl_type of
          | pbl_type_parser =>
           (case ALOOKUP pars_map x' of
            | SOME stmt' =>
             SOME ((i, in_out_list, in_out_list', scope), g_scope_list, (arch_frame_list_regular [(funn_name x', [stmt'], [ [] ])]), status_running)
            | _ => NONE)
          | _ => NONE)
        | status_running =>
         (* pbl_exec *)
         (case frames_exec (apply_table_f, ext_map, func_map, b_func_map, pars_map, tbl_map) (scope, g_scope_list, frame_list, status) of
          | SOME (scope', g_scope_list', frame_list', status') =>
           SOME ((i, in_out_list, in_out_list', scope'), g_scope_list', (arch_frame_list_regular frame_list'), status')
          | _ => NONE)
        | _ => NONE)
     | _ => NONE)
   | _ => NONE)
 )
 /\
 (arch_exec (ab_list, pblock_map, ffblock_map, input_f, output_f, copyin_pbl, copyout_pbl, apply_table_f, ext_map, func_map)
            ((i, in_out_list, in_out_list', scope), g_scope_list,
             arch_frame_list_empty, status_running) =
  (case EL i ab_list of
   (* in *)
   | arch_block_inp =>
    (case input_f (in_out_list, scope) of
     | SOME (in_out_list'', scope') => 
      SOME ((i+1, in_out_list'', in_out_list', scope'), g_scope_list, arch_frame_list_empty,
             status_running)
     | NONE => NONE)
   | (arch_block_pbl x el) =>
    (case ALOOKUP pblock_map x of
     (* pbl_init *)
     | SOME (pbl_type, x_d_list, b_func_map, decl_list, pars_map, tbl_map) =>
      (case lookup_block_body x b_func_map of
       | SOME stmt =>
        (* TODO: The below LENGTH check is only used for proofs (e.g. soundness proof) *)
        (if LENGTH el = LENGTH x_d_list
         then
          (case copyin_pbl ((MAP FST x_d_list), (MAP SND x_d_list), el, scope) of
           | SOME scope' =>
            (case oLASTN 1 g_scope_list of
             | SOME [g_scope] =>
              let g_scope_list' = ([declare_list_in_scope (decl_list, scope')]++[g_scope]) in
               (case initialise_var_stars func_map b_func_map ext_map g_scope_list' of
                | SOME g_scope_list'' =>
                 SOME ((i, in_out_list, in_out_list', scope), g_scope_list'',
                       arch_frame_list_regular [(funn_name x, [stmt], [ [] ])], status_running)
                | NONE => NONE)
             | _ => NONE)
           | _ => NONE)
         else NONE)
       | NONE => NONE)
     | _ => NONE)
   (* ffbl *)
   | (arch_block_ffbl x) =>
    (case ALOOKUP ffblock_map x of
     | SOME (ffblock_ff ff) =>
      (case ff scope of
       | SOME scope' =>
        SOME ((i+1, in_out_list, in_out_list', scope'), g_scope_list, arch_frame_list_empty, status_running)
       | NONE => NONE)
     | NONE => NONE)
   (* out *)
   | arch_block_out =>
    (case output_f (in_out_list', scope) of
     | SOME (in_out_list'', scope') =>
      SOME ((0, in_out_list, in_out_list'', scope'), g_scope_list, arch_frame_list_empty,
            status_running)
     | NONE => NONE)
  )
 )
/\
(arch_exec _ _ = NONE)
End

(* Fuel-powered multi-step architectural-level executable semantics *)
Definition arch_multi_exec_def:
 (arch_multi_exec actx (aenv, g_scope_list, arch_frame_list, status) 0 =
  SOME (aenv, g_scope_list, arch_frame_list, status))
  /\
 (arch_multi_exec actx (aenv, g_scope_list, arch_frame_list, status) (SUC fuel) =
  case arch_exec actx (aenv, g_scope_list, arch_frame_list, status) of
  | SOME (aenv', g_scope_list', arch_frame_list', status') =>
   arch_multi_exec actx (aenv', g_scope_list', arch_frame_list', status') fuel
  | NONE => NONE)
End

Theorem arch_multi_exec_1:
!actx s s'.
 arch_multi_exec actx s 1 = SOME s' <=> arch_exec actx s = SOME s'
Proof
rpt strip_tac >>
PairCases_on ‘s’ >>
REWRITE_TAC [arithmeticTheory.ONE, arch_multi_exec_def] >>
Cases_on ‘arch_exec actx ((s0,s1,s2,s3),s4,s5,s6)’ >> (
 fs[]
) >>
PairCases_on ‘x’ >>
fs[]
QED

Theorem arch_multi_exec_add:
!actx aenv g_scope_list arch_frame_list status m n.
arch_multi_exec actx (aenv, g_scope_list, arch_frame_list, status) (m+n) =
 case arch_multi_exec actx (aenv, g_scope_list, arch_frame_list, status) n of
 | SOME (aenv', g_scope_list', arch_frame_list', status') =>
  arch_multi_exec actx (aenv', g_scope_list', arch_frame_list', status') m
 | NONE => NONE
Proof
Induct_on `n` >- (
 fs [arch_multi_exec_def]
) >>
rpt strip_tac >>
fs [arch_multi_exec_def, arithmeticTheory.ADD_CLAUSES] >>
Cases_on `arch_exec actx (aenv,g_scope_list,arch_frame_list,status)` >> (
 fs []
) >>
PairCases_on `x` >>
fs []
QED

(* TODO: What to call this? Compose? Combine? *)
Theorem arch_multi_exec_comp_1_tl:
!actx aenv g_scope_list arch_frame_list status m aenv' g_scope_list' arch_frame_list' status' aenv'' g_scope_list'' arch_frame_list'' status''.
arch_multi_exec actx (aenv, g_scope_list, arch_frame_list, status) 1 =
  SOME (aenv', g_scope_list', arch_frame_list', status') ==>
arch_multi_exec actx (aenv', g_scope_list', arch_frame_list', status') m =
  SOME (aenv'', g_scope_list'', arch_frame_list'', status'') ==>
arch_multi_exec actx (aenv, g_scope_list, arch_frame_list, status) (1+m) =
  SOME (aenv'', g_scope_list'', arch_frame_list'', status'')
Proof
rpt strip_tac >>
FULL_SIMP_TAC pure_ss [Once arithmeticTheory.ADD_COMM] >>
fs [arch_multi_exec_add]
QED

Theorem arch_multi_exec_split_1_tl:
!actx aenv g_scope_list arch_frame_list status m aenv'' g_scope_list'' arch_frame_list'' status''.
arch_multi_exec actx (aenv, g_scope_list, arch_frame_list, status) (m+1) =
  SOME (aenv'', g_scope_list'', arch_frame_list'', status'') ==>
(?aenv' g_scope_list' arch_frame_list' status'.
 arch_multi_exec actx (aenv, g_scope_list, arch_frame_list, status) m =
   SOME (aenv', g_scope_list', arch_frame_list', status') ==>
 arch_multi_exec actx (aenv', g_scope_list', arch_frame_list', status') 1 =
   SOME (aenv'', g_scope_list'', arch_frame_list'', status''))
Proof
rpt strip_tac >>
FULL_SIMP_TAC pure_ss [Once arithmeticTheory.ADD_COMM] >>
fs [arch_multi_exec_add] >>
Cases_on `arch_multi_exec actx (aenv,g_scope_list,arch_frame_list,status) m` >> (
 fs []
) >>
PairCases_on `x` >>
qexistsl_tac [`(x0,x1,x2,x3)`, `x4`, `x5`, `x6`] >>
fs []
QED

Theorem arch_multi_exec_comp_n_tl:
!n m actx assl aenv g_scope_list arch_frame_list status aenv' g_scope_list' arch_frame_list' status' aenv'' g_scope_list'' arch_frame_list'' status''.
arch_multi_exec actx (aenv, g_scope_list, arch_frame_list, status) n =
  SOME (aenv', g_scope_list', arch_frame_list', status') ==>
arch_multi_exec actx (aenv', g_scope_list', arch_frame_list', status') m =
  SOME (aenv'', g_scope_list'', arch_frame_list'', status'') ==>
arch_multi_exec actx (aenv, g_scope_list, arch_frame_list, status) (n+m) =
  SOME (aenv'', g_scope_list'', arch_frame_list'', status'')
Proof
rpt strip_tac >>
gs[] >>
fs [arch_multi_exec_add]
QED

(* TODO: use only this shape... *)
Theorem arch_multi_exec_comp_n_tl_alt:
!n m actx s s' s''.
arch_multi_exec actx s n =
  SOME s' ==>
arch_multi_exec actx s' m =
  SOME s'' ==>
arch_multi_exec actx s (n+m) =
  SOME s''
Proof
rpt strip_tac >>
gs[] >>
PairCases_on ‘s’ >>
PairCases_on ‘s'’ >>
PairCases_on ‘s''’ >>
fs [arch_multi_exec_add]
QED

Theorem arch_multi_exec_comp_1_tl_assl:
!m actx assl aenv g_scope_list arch_frame_list status aenv' g_scope_list' arch_frame_list' status' aenv'' g_scope_list'' arch_frame_list'' status''.
(assl ==> arch_multi_exec actx (aenv, g_scope_list, arch_frame_list, status) 1 =
  SOME (aenv', g_scope_list', arch_frame_list', status')) ==>
(assl ==> arch_multi_exec actx (aenv', g_scope_list', arch_frame_list', status') m =
  SOME (aenv'', g_scope_list'', arch_frame_list'', status'')) ==>
(assl ==> arch_multi_exec actx (aenv, g_scope_list, arch_frame_list, status) (1+m) =
  SOME (aenv'', g_scope_list'', arch_frame_list'', status''))
Proof
metis_tac[arch_multi_exec_comp_1_tl]
QED

Theorem arch_multi_exec_comp_n_tl_assl:
!n m actx assl aenv g_scope_list arch_frame_list status aenv' g_scope_list' arch_frame_list' status' aenv'' g_scope_list'' arch_frame_list'' status''.
(assl ==> arch_multi_exec actx (aenv, g_scope_list, arch_frame_list, status) n =
  SOME (aenv', g_scope_list', arch_frame_list', status')) ==>
(assl ==> arch_multi_exec actx (aenv', g_scope_list', arch_frame_list', status') m =
  SOME (aenv'', g_scope_list'', arch_frame_list'', status'')) ==>
(assl ==> arch_multi_exec actx (aenv, g_scope_list, arch_frame_list, status) (n+m) =
  SOME (aenv'', g_scope_list'', arch_frame_list'', status''))
Proof
rpt strip_tac >>
gs [] >>
fs [arch_multi_exec_add]
QED

Theorem arch_multi_exec_comp_n_tl_assl_conj:
!n m actx assl aenv g_scope_list arch_frame_list status aenv' g_scope_list' arch_frame_list' status' aenv'' g_scope_list'' arch_frame_list'' status''.
((assl ==> arch_multi_exec actx (aenv, g_scope_list, arch_frame_list, status) n =
  SOME (aenv', g_scope_list', arch_frame_list', status')) /\
 (assl ==> arch_multi_exec actx (aenv', g_scope_list', arch_frame_list', status') m =
  SOME (aenv'', g_scope_list'', arch_frame_list'', status''))) ==>
(assl ==> arch_multi_exec actx (aenv, g_scope_list, arch_frame_list, status) (n+m) =
  SOME (aenv'', g_scope_list'', arch_frame_list'', status''))
Proof
metis_tac[arch_multi_exec_comp_n_tl_assl]
QED

Theorem arch_multi_exec_comp_n_tl_assl_conj_nomidassl:
!n m actx assl aenv g_scope_list arch_frame_list status aenv' g_scope_list' arch_frame_list' status' aenv'' g_scope_list'' arch_frame_list'' status''.
((assl ==> arch_multi_exec actx (aenv, g_scope_list, arch_frame_list, status) n =
  SOME (aenv', g_scope_list', arch_frame_list', status')) /\
 (arch_multi_exec actx (aenv', g_scope_list', arch_frame_list', status') m =
  SOME (aenv'', g_scope_list'', arch_frame_list'', status''))) ==>
(assl ==> arch_multi_exec actx (aenv, g_scope_list, arch_frame_list, status) (n+m) =
  SOME (aenv'', g_scope_list'', arch_frame_list'', status''))
Proof
metis_tac[arch_multi_exec_comp_n_tl_assl_conj]
QED

Theorem arch_multi_exec_arch_frame_list_regular:
!ab_list pblock_map ffblock_map input_f output_f copyin_pbl
 copyout_pbl apply_table_f ext_map func_map aenv g_scope_list g_scope_list' arch_frame_list frame_list' n i io_list io_list' ascope.
arch_multi_exec (ab_list,pblock_map,ffblock_map,input_f,output_f,copyin_pbl,
        copyout_pbl,apply_table_f,ext_map,func_map)
          (aenv,g_scope_list,arch_frame_list,
           status_running) (SUC n) =
        SOME
          ((i,io_list,io_list',ascope),g_scope_list',
           arch_frame_list_regular frame_list',status_running) ==>
?x el pbl_type x_d_list b_func_map decl_list pars_map tbl_map.
 EL i ab_list = arch_block_pbl x el /\
 ALOOKUP pblock_map x =
          SOME (pbl_type,x_d_list,b_func_map,decl_list,pars_map,tbl_map)
Proof
rpt strip_tac >>
fs[SUC_ADD_ONE] >>
FULL_SIMP_TAC pure_ss [Once arithmeticTheory.ADD_SYM] >>
fs[arch_multi_exec_add] >>
Cases_on ‘arch_multi_exec
             (ab_list,pblock_map,ffblock_map,input_f,output_f,copyin_pbl,
              copyout_pbl,apply_table_f,ext_map,func_map)
             (aenv,g_scope_list,arch_frame_list,
              status_running) n’ >> (
 fs[]
) >>
PairCases_on ‘x’ >>
fs[] >>
FULL_SIMP_TAC pure_ss [Once arithmeticTheory.ONE] >>
fs[arch_multi_exec_def] >>
Cases_on ‘x5’ >- (
 Cases_on ‘x6’ >> (
  fs[arch_exec_def]
 ) >>
 Cases_on ‘EL x0 ab_list’ >> (
  fs[]
 ) >| [
  Cases_on ‘input_f (x1,x3)’ >> (
   fs[]
  ) >>
  PairCases_on ‘x’ >>
  fs[],

  Cases_on ‘ALOOKUP pblock_map s’ >> (
   fs[]
  ) >>
  PairCases_on ‘x’ >>
  fs[] >>
  Cases_on ‘lookup_block_body s x2'’ >> (
   fs[]
  ) >>
  Cases_on ‘LENGTH l = LENGTH x1'’ >> (
   fs[]
  ) >>
  Cases_on ‘copyin_pbl (MAP FST x1',MAP SND x1',l,x3)’ >> (
   fs[]
  ) >>
  Cases_on ‘oLASTN 1 x4’ >> (
   fs[]
  ) >>
  Cases_on ‘x''’ >> (
   fs[]
  ) >>
  Cases_on ‘t’ >> (
   fs[]
  ) >>
  Cases_on ‘initialise_var_stars func_map x2' ext_map
               [declare_list_in_scope (x3',x'); h]’ >> (
   fs[]
  ) >>
  gvs[],

  Cases_on ‘ALOOKUP ffblock_map s’ >> (
   fs[]
  ) >>
  Cases_on ‘x’ >>
  fs[] >>
  Cases_on ‘f x3’ >> (
   fs[]
  ),

  Cases_on ‘output_f (x2,x3)’ >> (
   fs[]
  ) >>
  PairCases_on ‘x’ >>
  fs[]
 ]
) >>
fs[arch_exec_def] >>
Cases_on ‘EL x0 ab_list’ >> (
 fs[]
) >>
Cases_on ‘ALOOKUP pblock_map s’ >> (
 fs[]
) >>
PairCases_on ‘x’ >>
fs[] >>
Cases_on ‘state_fin_exec x6 l’ >> (
 fs[]
) >- (
 Cases_on ‘lookup_block_body s x2'’ >> (
  fs[]
 ) >>
 Cases_on ‘LENGTH l' = LENGTH x1'’ >> (
  fs[]
 ) >>
 Cases_on ‘copyout_pbl
              (x4,x3,MAP SND x1',MAP FST x1',set_fin_status x0' x6)’ >> (
  fs[]
 )
) >>
Cases_on ‘x6’ >> (
 fs[]
) >- (
 Cases_on ‘frames_exec (apply_table_f,ext_map,func_map,x2',x4',x5)
              (x3,x4,l,status_running)’ >> (
  fs[]
 ) >>
 PairCases_on ‘x’ >>
 fs[] >>
 gvs[]
) >>
Cases_on ‘x0'’ >> (
 fs[]
) >>
Cases_on ‘ALOOKUP x4' s'’ >> (
 fs[]
) >>
gvs[]
QED

        
(**********)
(*  Misc  *)
(**********)
(* TODO  
(* Then, define the closure of the small step reduction. *)
val (stmt_clos_sem_rules, stmt_clos_sem_ind, stmt_clos_sem_cases) = Hol_reln`
(* Base clause: *)
(!ctx state state'.
 stmt_red ctx state state' ==> 
 stmt_clos_red ctx state state')
(* Inductive clause: *)
/\
(!ctx state state' state''.
 (stmt_red ctx state state' /\ 
  stmt_clos_red ctx state' state'') ==> 
 stmt_clos_red ctx state state'')
`;


(* Then, prove that the multi-step executable semantics is sound with respect to the
 * closure of the small-step reduction *)
Theorem stmt_multi_exec_sound_red:
 !ctx state state' fuel.
  stmt_multi_exec ctx state fuel = SOME state' ==>
  stmt_clos_red ctx state state'
Proof
 TODO
QED
*)

(*
(* TODO: some kind of (multi-step) CakeML-adjusted executable semantics definition *)
Definition e_exec_cake_def:
 (e_exec_cake (e_unop unop_neg (e_v (v_bool b))) stacks status =
   SOME (e_v (v_bool ~b)))
  /\
 (e_exec_cake (e_unop unop_compl (e_v (v_bit bitv))) stacks status =
  SOME (e_v (v_bit (bitv_bl_unop bnot bitv))))
  \/gi
 (e_exec_cake (e_unop unop_neg_signed (e_v (v_bit bitv))) stacks status =
  SOME (e_v (v_bit (bitv_unop unop_neg_signed bitv))))
  /\
 (e_exec_cake (e_unop unop_un_plus (e_v (v_bit bitv))) stacks status =
  SOME (e_v (v_bit bitv)))
  /\
 (e_exec_cake _ stacks status = NONE)
End

(* TODO: At this point, expect to translate lists to lists and fmaps to mlmaps and make casts for all non-64-bit words *)
Theorem sem_expr_exe_cake_equiv:
 !e stacks.
  e_exec_cake e stacks status_running = e_exec_multi e stacks status_running
Proof
 TODO
QED
*)

val _ = export_theory ();