Theory SM.SM_Semantics

section ‹Semantics of SM›
theory SM_Semantics
imports SM_State SM_Cfg Gen_Scheduler
begin

  section ‹Evaluation of Expressions›
  subsection ‹Basic operations›
  text ‹Attention: Silently overflows, using 2's complement.
    This should match Java-semantics. In C, signed overflow is undefined!›

  context
    includes bit_operations_syntax
  begin

  primrec eval_bin_op :: "bin_op  val  val  val" where
    "eval_bin_op bo_plus v1 v2 = v1+v2"
  | "eval_bin_op bo_minus v1 v2 = v1-v2"
  | "eval_bin_op bo_mul v1 v2 = v1*v2"
  | "eval_bin_op bo_div v1 v2 = v1 sdiv v2"
  | "eval_bin_op bo_mod v1 v2 = v1 smod v2"
  | "eval_bin_op bo_less v1 v2 = val_of_bool (v1 < v2)"
  | "eval_bin_op bo_less_eq v1 v2 = val_of_bool (v1  v2)"
  | "eval_bin_op bo_eq v1 v2 = val_of_bool (v1 = v2)"
  | "eval_bin_op bo_and v1 v2 = v1 AND v2"
  | "eval_bin_op bo_or v1 v2 = v1 OR v2"
  | "eval_bin_op bo_xor v1 v2 = v1 XOR v2"

  primrec eval_un_op :: "un_op  val  val" where
    "eval_un_op uo_minus v = -v"  ― ‹Attention: Silently overflows. @{term "-min_int = min_int"}!›
  | "eval_un_op uo_not v = NOT v"

  end

  subsection ‹Expressions›
  abbreviation exists_var :: "valuation  ident  bool" where
    "exists_var s x  x  dom s"

  abbreviation update_var :: "ident  val  valuation  valuation" where
    "update_var x v s  s(xv)"

  fun eval_exp :: "exp  focused_state  val" where
    "eval_exp (e_var x) (ls,gs) = do {
      let lv = local_state.variables ls; let gv = global_state.variables gs;
      case lv x of
        Some v  Some v
      | None  (case gv x of
          Some v  Some v
        | None  None)
    }"
  | "eval_exp (e_localvar x) (ls,gs) = local_state.variables ls x"
  | "eval_exp (e_globalvar x) (ls,gs) = global_state.variables gs x"
  | "eval_exp (e_const n) fs = do {
      assert_option (nmin_signed  nmax_signed);
      Some (signed_of_int n)
    }"
  | "eval_exp (e_bin bop e1 e2) fs = do {
      v1eval_exp e1 fs;
      v2eval_exp e2 fs;
      Some (eval_bin_op bop v1 v2)
      }"
  | "eval_exp (e_un uop e) fs = do {
      veval_exp e fs;
      Some (eval_un_op uop v)
      }"

  subsection ‹Local Actions›

  text ‹Enabledness and effects of actions›
  primrec la_en :: "focused_state  action  bool" where
    "la_en fs (AAssign c _ _) = do { v  eval_exp c fs; Some (bool_of_val v)}"
  | "la_en fs (AAssign_local c _ _) = do { v  eval_exp c fs; Some (bool_of_val v)}"
  | "la_en fs (AAssign_global c _ _) = do { v  eval_exp c fs; Some (bool_of_val v)}"
  | "la_en fs (ATest e) = do {
      v  eval_exp e fs;
      Some (bool_of_val v)}"
  | "la_en _ (ASkip) = Some True"

  text ‹Extension (for run, handshake): Let action have scheduler effect›
  fun la_ex :: "focused_state  action  focused_state" where
    "la_ex (ls,gs) (AAssign c x e) = do {
      u  eval_exp c (ls,gs);
      assert_option (bool_of_val u);
      v  eval_exp e (ls,gs);
      if exists_var (local_state.variables ls) x then do {
        let ls = local_state.variables_update (update_var x v) ls;
        Some (ls,gs)
      } else do {
        assert_option (exists_var (global_state.variables gs) x);
        let gs = global_state.variables_update (update_var x v) gs;
        Some (ls,gs)
      }
    }"
  | "la_ex (ls,gs) (AAssign_local c x e) = do {
      u  eval_exp c (ls,gs);
      assert_option (bool_of_val u);
      v  eval_exp e (ls,gs);
      assert_option (exists_var (local_state.variables ls) x);
      let ls = local_state.variables_update (update_var x v) ls;
      Some (ls,gs)
    }"
  | "la_ex (ls,gs) (AAssign_global c x e) = do {
      u  eval_exp c (ls,gs);
      assert_option (bool_of_val u);
      v  eval_exp e (ls,gs);
      assert_option (exists_var (global_state.variables gs) x);
      let gs = global_state.variables_update (update_var x v) gs;
      Some (ls,gs)
    }"
  | "la_ex fs (ATest e) = do {
      v  eval_exp e fs;
      assert_option (bool_of_val v); 
      Some fs
    }"
  | "la_ex fs ASkip = Some fs"


  subsection "Scheduling"
  type_synonym local_config = "(cmd,local_state) local_config"
  type_synonym global_config = "(cmd,local_state,global_state) global_config"
  
  interpretation li: Gen_Scheduler cfg la_en la_ex .

  subsection ‹Initial State›
  definition init_valuation :: "var_decl list  valuation" where
    "init_valuation vd x  if x  set vd then Some 0 else None"

  lemma init_valuation_eq_Some[simp]: "init_valuation vd x = Some v  xset vd  v=0"  
    unfolding init_valuation_def by auto

  lemma init_valuation_eq_None[simp]: "init_valuation vd x = None  xset vd"  
    unfolding init_valuation_def by auto

  definition init_pc :: "proc_decl  local_config" where
    "init_pc pd  
      local_config.command = proc_decl.body pd,
      local_config.state = 
        local_state.variables = init_valuation (proc_decl.local_vars pd)
      
    "

  definition init_gc :: "program  global_config" where
    "init_gc prog  
      global_config.processes = mset (map init_pc (program.processes prog)),
      global_config.state = 
        global_state.variables = init_valuation (program.global_vars prog)
      
    "

  subsection "Semantics Reference Point"
  
  interpretation li: Gen_Scheduler_linit cfg la_en la_ex "{init_gc prog}" global_config.state
    for prog .
  
  abbreviation "ref_is_run  li.sa.is_run"
  abbreviation "ref_accept  li.sa.accept"

end