SSL Promela.thy

section "Formalization of Promela semantics"
theory Promela
imports 
  PromelaDatastructures
  PromelaInvariants
  PromelaStatistics
begin

text ‹Auxiliary›

lemma mod_integer_le:
  ‹x mod (a + 1) ≤ b› if ‹a ≤ b› ‹0 < a› for a b x :: integer
using that including integer.lifting proof transfer
  fix a b x :: int
  assume ‹0 < a› ‹a ≤ b›
  have ‹x mod (a + 1) < a + 1›
    by (rule pos_mod_bound) (use ‹0 < a› in simp)
  with ‹a ≤ b› show ‹x mod (a + 1) ≤ b›
    by simp
qed

lemma mod_integer_ge:
  ‹b ≤ x mod (a + 1)› if ‹b ≤ 0› ‹0 < a› for a b x :: integer
using that including integer.lifting proof transfer
  fix a b x :: int
  assume ‹b ≤ 0› ‹0 < a›
  then have ‹0 ≤ x mod (a + 1)›
    by simp
  with ‹b ≤ 0› show ‹b ≤ x mod (a + 1)›
    by simp
qed

text ‹
 After having defined the datastructures, we present in this theory how to construct the transition system and how to generate the successors of a state, \ie the real semantics of a Promela program.
 For the first task, we take the enriched AST as input, the second one operates on the transition system.
 ›

subsection ‹Misc Helpers›
definition add_label :: "String.literal ==> labels ==> nat ==> labels" where
  "add_label l lbls pos = (
     case lm.lookup l lbls of
       None ==> lm.update l pos lbls
     | Some _ ==> abortv STR ''Label given twice: '' l (λ_. lbls))"

definition min_prio :: "edge list ==> integer ==> integer" where
  "min_prio es start = Min ((prio ` set es) ∪ {start})"

lemma min_prio_code [code]:
  "min_prio es start = fold (λe pri. if prio e < pri then prio e else pri) es start"
proof -
  from Min.set_eq_fold have "Min (set (start # map prio es)) = fold min (map prio es) start" by metis
  also have "... = fold (min ∘ prio) es start" by (simp add: fold_map)
  also have "... = fold (λe pri. if prio e < pri then prio e else pri) es start" by (auto intro!: fold_cong)
  finally show ?thesis by (simp add: min_prio_def)
qed
  
definition for_all :: "('a ==> bool) ==> 'a list ==> bool" where
  "for_all f xs ⟷ (∀x ∈ set xs. f x)"

lemma for_all_code[code]:
  "for_all f xs ⟷ foldli xs id (λkv σ. f kv) True"
  by (simp add: for_all_def foldli_conj)

definition find_remove :: "('a ==> bool) ==> 'a list ==> 'a option × 'a list" where
  "find_remove P xs = (case List.find P xs of None ==> (None, xs)
                                            | Some x ==> (Some x, List.remove1 x xs))"

lemma find_remove_code [code]:
  "find_remove P [] = (None, [])"
  "find_remove P (x#xs) = (if P x then (Some x, xs)
                           else apsnd (Cons x) (find_remove P xs))"
  by (induct xs) (auto simp add: find_remove_def dest: find_SomeD split: option.split) 

lemma find_remove_subset:
  "find_remove P xs = (res, xs') ==> set xs' ⊆ set xs"
unfolding find_remove_def
using set_remove1_subset
by (force split: option.splits)

lemma find_remove_length:
  "find_remove P xs = (res, xs') ==> length xs' ≤ length xs"
unfolding find_remove_def
by (induct xs arbitrary: res xs') (auto split: if_splits option.splits)

subsection ‹Variable handling›

text ‹
 Handling variables, with their different scopes (global vs. local),
 and their different types (array vs channel vs bounded) is one of the main challenges
 of the implementation.
 ›

fun lookupVar :: "variable ==> integer option ==> integer" where
  "lookupVar (Var _ val) None = val"
| "lookupVar (Var _ _) (Some _) = abort STR ''Array used on var'' (λ_.0)"
| "lookupVar (VArray _ _ vals) None = vals !! 0" (* sic! *)
| "lookupVar (VArray _ siz vals) (Some idx) = vals !! nat_of_integer idx"

primrec checkVarValue :: "varType ==> integer ==> integer" where
  "checkVarValue (VTBounded lRange hRange) val = (
     if val ≤ hRange ∧ val ≥ lRange then val
     else ― ‹overflowing is well-defined and may actually be used (e.g. bool)›
        if lRange = 0 ∧ val > 0
        then val mod (hRange + 1)
        else ― ‹we do not want to implement C-semantics (ie type casts)›
           abort STR ''Value overflow'' (λ_. lRange))"
| "checkVarValue VTChan val = (
     if val < min_var_value ∨ val > max_var_value
     then abort STR ''Value overflow'' (λ_. 0)
     else val)"

lemma [simp]:
  "variable_inv (Var VTChan 0)"
by simp

context
  fixes type :: varType
  assumes "varType_inv type"
begin

lemma checkVarValue_bounded:
  "checkVarValue type val ∈ {min_var_value..max_var_value}"
  using ‹varType_inv type›
  by (cases type) (auto intro: mod_integer_le mod_integer_ge)

lemma checkVarValue_bounds:
  "min_var_value ≤ checkVarValue type val"
  "checkVarValue type val ≤ max_var_value"
  using checkVarValue_bounded [of val] by simp_all

lemma checkVarValue_Var:
  "variable_inv (Var type (checkVarValue type val))"
  using ‹varType_inv type› by (simp add: checkVarValue_bounds)

end

fun editVar :: "variable ==> integer option ==> integer ==> variable" where
  "editVar (Var type _ ) None val = Var type (checkVarValue type val)"
| "editVar (Var _ _) (Some _) _ = abort STR ''Array used on var'' (λ_. Var VTChan 0)"
| "editVar (VArray type siz vals) None val = (
     let lv = IArray.list_of vals in
     let v' = lv[0:=checkVarValue type val] in
     VArray type siz (IArray v'))"
| "editVar (VArray type siz vals) (Some idx) val = (
     let lv = IArray.list_of vals in
     let v' = lv[(nat_of_integer idx):=checkVarValue type val] in
     VArray type siz (IArray v'))"

lemma editVar_variable_inv:
  assumes "variable_inv v"
  shows "variable_inv (editVar v idx val)"
proof (cases v)
  case (Var type val) with assms have "varType_inv type" by simp
  with Var show ?thesis 
    by (cases idx) 
       (auto intro!: checkVarValue_Var 
             simp del: checkVarValue.simps variable_inv.simps)
next
  case (VArray type siz vals) 
  with assms have [simp, intro!]: "varType_inv type" by simp
  
  show ?thesis
  proof (cases idx)
    case None with assms VArray show ?thesis 
      by (cases "IArray.list_of vals") (auto intro!: checkVarValue_bounds)
  next
    case (Some i)
    note upd_cases = in_set_upd_cases[where l="IArray.list_of vals" and i="nat_of_integer i"]

    from Some VArray assms show ?thesis
      by (cases type)
        (auto elim!: upd_cases intro!: mod_integer_le mod_integer_ge simp add: min_var_value_def)
  qed
qed

definition getVar' 
  :: "bool ==> String.literal ==> integer option
      ==> 'a gState_scheme ==> pState
      ==> integer option" 
where
  "getVar' gl v idx g p = (
          let vars = if gl then gState.vars g else pState.vars p in
          map_option (λx. lookupVar x idx) (lm.lookup v vars))"

definition setVar' 
  :: "bool ==> String.literal ==> integer option
      ==> integer
      ==> 'a gState_scheme ==> pState
      ==> 'a gState_scheme * pState"
 where
  "setVar' gl v idx val g p = (
     if gl then
        if v = STR ''_'' then (g,p) ― ‹‹''_''› is a write-only scratch variable›
        else case lm.lookup v (gState.vars g) of
               None ==> abortv STR ''Unknown global variable: '' v (λ_. (g,p))
             | Some x ==> (g(gState.vars := lm.update v (editVar x idx val)
                                                       (gState.vars g))
                         , p)
     else
        case lm.lookup v (pState.vars p) of
          None ==> abortv STR ''Unknown proc variable: '' v (λ_. (g,p))
        | Some x ==> (g, p(pState.vars := lm.update v (editVar x idx val)
                                                     (pState.vars p))))"

lemma setVar'_gState_inv:
  assumes "gState_inv prog g"
  shows "gState_inv prog (fst (setVar' gl v idx val g p))"
unfolding setVar'_def using assms
by (auto simp add: gState_inv_def lm.correct 
         intro: editVar_variable_inv 
         split: option.splits)

lemma setVar'_gState_progress_rel:
  assumes "gState_inv prog g"
  shows "(g, fst (setVar' gl v idx val g p)) ∈ gState_progress_rel prog"
apply (intro gState_progress_relI)
      apply (fact assms)
    apply (fact setVar'_gState_inv[OF assms])
  apply (auto simp: setVar'_def lm.correct split: option.splits)
done

lemma vardict_inv_process_names:
  assumes "vardict_inv ss proc v"
  and "lm.lookup k v = Some x"
  shows "k ∈ process_names ss proc"
using assms
by (auto simp add: lm.correct vardict_inv_def)

lemma vardict_inv_variable_inv:
  assumes "vardict_inv ss proc v"
  and "lm.lookup k v = Some x"
  shows "variable_inv x"
using assms
by (auto simp add: lm.correct vardict_inv_def)

lemma vardict_inv_updateI:
  assumes "vardict_inv ss proc vs"
  and "x ∈ process_names ss proc"
  and "variable_inv v"
  shows "vardict_inv ss proc (lm.update x v vs)"
using assms
by (auto simp add: lm.correct vardict_inv_def)

lemma update_vardict_inv:
  assumes "vardict_inv ss proc v"
  and "lm.lookup k v = Some x"
  and "variable_inv x'"
  shows "vardict_inv ss proc (lm.update k x' v)"
using assms
by (auto intro!: vardict_inv_updateI vardict_inv_process_names)

lemma setVar'_pState_inv:
  assumes "pState_inv prog p"
  shows "pState_inv prog (snd (setVar' gl v idx val g p))"
unfolding setVar'_def using assms
by (auto split: if_splits option.splits 
         simp add: pState_inv_def
         intro: update_vardict_inv editVar_variable_inv vardict_inv_variable_inv)

lemma setVar'_cl_inv:
  assumes "cl_inv (g,p)"
  shows "cl_inv (setVar' gl v idx val g p)"
unfolding setVar'_def using assms
by (auto split: if_splits option.splits)

definition withVar' 
  :: "bool ==> String.literal ==> integer option
      ==> (integer ==> 'x)
      ==> 'a gState_scheme ==> pState
      ==> 'x"
where
  "withVar' gl v idx f g p = f (the (getVar' gl v idx g p))"

definition withChannel' 
  :: "bool ==> String.literal ==> integer option
      ==> (nat ==> channel ==> 'x)
      ==> 'a gState_scheme ==> pState
      ==> 'x"
where
  "withChannel' gl v idx f g p = (
     let error = λ_. abortv STR ''Variable is not a channel: '' v
                                (λ_. f 0 InvChannel) in
     let abort = λ_. abortv STR ''Channel already closed / invalid: '' v
                                (λ_. f 0 InvChannel)
     in withVar' gl v idx (λi. let i = nat_of_integer i in
                               if i ≥ length (channels g) then error ()
                               else let c = channels g ! i in
                                    case c of
                                      InvChannel ==> abort ()
                                    | _ ==> f i c) g p)"

subsection ‹Expressions›

text ‹Expressions are free of side-effects.

  is in difference to SPIN, where @{term run} is an expression with side-effect. We treat @{term run} as a statement.›

abbreviation "trivCond x ≡ if x then 1 else 0"

fun exprArith :: "'a gState_scheme ==> pState ==> expr ==> integer"
and pollCheck :: "'a gState_scheme ==> pState ==> channel ==> recvArg list ==> bool
                   ==> bool"
and recvArgsCheck :: "'a gState_scheme ==> pState ==> recvArg list ==> integer list
                       ==> bool" 
where
  "exprArith g p (ExprConst x) = x"
| "exprArith g p (ExprMConst x _) = x"

| "exprArith g p ExprTimeOut = trivCond (timeout g)"

| "exprArith g p (ExprLen (ChanRef (VarRef gl name None))) =
     withChannel' gl name None (
       λ_ c. case c of
                Channel _ _ q ==> integer_of_nat (length q)
              | HSChannel _ ==> 0) g p"

| "exprArith g p (ExprLen (ChanRef (VarRef gl name (Some idx)))) =
     withChannel' gl name (Some (exprArith g p idx)) (
      λ_ c. case c of
              Channel _ _ q ==> integer_of_nat (length q)
            | HSChannel _ ==> 0) g p"

| "exprArith g p (ExprEmpty (ChanRef (VarRef gl name None))) =
     trivCond (withChannel' gl name None (
       λ_ c. case c of Channel _ _ q ==> (q = [])
                     | HSChannel _ ==> True) g p)"

| "exprArith g p (ExprEmpty (ChanRef (VarRef gl name (Some idx)))) =
     trivCond (withChannel' gl name (Some (exprArith g p idx)) (
       λ_ c. case c of Channel _ _ q ==> (q = [])
                     | HSChannel _ ==> True) g p)"

| "exprArith g p (ExprFull (ChanRef(VarRef gl name None))) =
     trivCond (withChannel' gl name None (
       λ_ c. case c of
               Channel cap _ q ==> integer_of_nat (length q) ≥ cap
             | HSChannel _ ==> False) g p)"

| "exprArith g p (ExprFull (ChanRef(VarRef gl name (Some idx)))) =
     trivCond (withChannel' gl name (Some (exprArith g p idx)) (
       λ_ c. case c of
               Channel cap _ q ==> integer_of_nat (length q) ≥ cap
             | HSChannel _ ==> False) g p)"

| "exprArith g p (ExprVarRef (VarRef gl name None)) =
     withVar' gl name None id g p"

| "exprArith g p (ExprVarRef (VarRef gl name (Some idx))) =
     withVar' gl name (Some (exprArith g p idx)) id g p"

| "exprArith g p (ExprUnOp UnOpMinus expr) = 0 - exprArith g p expr"
| "exprArith g p (ExprUnOp UnOpNeg expr) = ((exprArith g p expr) + 1) mod 2"

| "exprArith g p (ExprBinOp BinOpAdd lexpr rexpr) =
     (exprArith g p lexpr) + (exprArith g p rexpr)"

| "exprArith g p (ExprBinOp BinOpSub lexpr rexpr) =
     (exprArith g p lexpr) - (exprArith g p rexpr)"

| "exprArith g p (ExprBinOp BinOpMul lexpr rexpr) =
     (exprArith g p lexpr) * (exprArith g p rexpr)"

| "exprArith g p (ExprBinOp BinOpDiv lexpr rexpr) =
     (exprArith g p lexpr) div (exprArith g p rexpr)"

| "exprArith g p (ExprBinOp BinOpMod lexpr rexpr) =
     (exprArith g p lexpr) mod (exprArith g p rexpr)"

| "exprArith g p (ExprBinOp BinOpGr lexpr rexpr) =
     trivCond (exprArith g p lexpr > exprArith g p rexpr)"

| "exprArith g p (ExprBinOp BinOpLe lexpr rexpr) =
     trivCond (exprArith g p lexpr < exprArith g p rexpr)"

| "exprArith g p (ExprBinOp BinOpGEq lexpr rexpr) =
     trivCond (exprArith g p lexpr ≥ exprArith g p rexpr)"

| "exprArith g p (ExprBinOp BinOpLEq lexpr rexpr) =
     trivCond (exprArith g p lexpr ≤ exprArith g p rexpr)"

| "exprArith g p (ExprBinOp BinOpEq lexpr rexpr) =
     trivCond (exprArith g p lexpr = exprArith g p rexpr)"

| "exprArith g p (ExprBinOp BinOpNEq lexpr rexpr) =
     trivCond (exprArith g p lexpr ≠ exprArith g p rexpr)"

| "exprArith g p (ExprBinOp BinOpAnd lexpr rexpr) =
     trivCond (exprArith g p lexpr ≠ 0 ∧ exprArith g p rexpr ≠ 0)"

| "exprArith g p (ExprBinOp BinOpOr lexpr rexpr) =
     trivCond (exprArith g p lexpr ≠ 0 ∨ exprArith g p rexpr ≠ 0)"

| "exprArith g p (ExprCond cexpr texpr fexpr) =
     (if exprArith g p cexpr ≠ 0 then exprArith g p texpr
      else exprArith g p fexpr)"

| "exprArith g p (ExprPoll (ChanRef (VarRef gl name None)) rs srt) =
     trivCond (withChannel' gl name None (
       λ_ c. pollCheck g p c rs srt) g p)"

| "exprArith g p (ExprPoll (ChanRef (VarRef gl name (Some idx))) rs srt) =
     trivCond (withChannel' gl name (Some (exprArith g p idx)) (
       λ_ c. pollCheck g p c rs srt) g p)"

| "pollCheck g p InvChannel _ _ =
     abort STR ''Channel already closed / invalid.'' (λ_. False)"
| "pollCheck g p (HSChannel _) _ _ = False"
| "pollCheck g p (Channel _ _ q) rs srt = (
     if q = [] then False
     else if ¬ srt then recvArgsCheck g p rs (hd q)
     else List.find (recvArgsCheck g p rs) q ≠ None)"

| "recvArgsCheck _ _ [] [] = True"
| "recvArgsCheck _ _ _ [] =
     abort STR ''Length mismatch on receiving.'' (λ_. False)"
| "recvArgsCheck _ _ [] _ =
     abort STR ''Length mismatch on receiving.'' (λ_. False)"
| "recvArgsCheck g p (r#rs) (v#vs) = ((
       case r of
          RecvArgConst c ==> c = v
        | RecvArgMConst c _ ==> c = v
        | RecvArgVar var ==> True
        | RecvArgEval e ==> exprArith g p e = v ) ∧ recvArgsCheck g p rs vs)"

text ‹@{const getVar'} etc.\ do operate on name, index, \ldots directly. Lift them to use @{const VarRef} instead.›

fun liftVar where
  "liftVar f (VarRef gl v idx) argm g p =
      f gl v (map_option (exprArith g p) idx) argm g p"

definition "getVar v = liftVar (λgl v idx arg. getVar' gl v idx) v ()"
definition "setVar = liftVar setVar'"
definition "withVar = liftVar withVar'"

primrec withChannel
  where "withChannel (ChanRef v) = liftVar withChannel' v"

lemma setVar_gState_progress_rel:
  assumes "gState_inv prog g"
  shows "(g, fst (setVar v val g p)) ∈ gState_progress_rel prog"
unfolding setVar_def
by (cases v) (simp add: setVar'_gState_progress_rel[OF assms])

lemmas setVar_gState_inv = 
  setVar_gState_progress_rel[THEN gState_progress_rel_gState_invI2]

lemma setVar_pState_inv:
  assumes "pState_inv prog p"
  shows "pState_inv prog (snd (setVar v val g p))"
unfolding setVar_def 
by (cases v) (auto simp add: setVar'_pState_inv assms)

lemma setVar_cl_inv:
  assumes "cl_inv (g,p)"
  shows "cl_inv (setVar v val g p)"
unfolding setVar_def 
by (cases v) (auto simp add: setVar'_cl_inv assms)

subsection ‹Variable declaration›

lemma channel_inv_code [code]:
  "channel_inv (Channel cap ts q)
  ⟷ cap ≤ max_array_size
    ∧ 0 ≤ cap
    ∧ for_all varType_inv ts
    ∧ length ts ≤ max_array_size
    ∧ length q ≤ max_array_size
    ∧ for_all (λx. length x = length ts
                   ∧ for_all (λy. y ≥ min_var_value
                                 ∧ y ≤ max_var_value) x) q" 
  "channel_inv (HSChannel ts)
  ⟷ for_all varType_inv ts ∧ length ts ≤ max_array_size"
  by (auto simp add: for_all_def) force+

primrec toVariable 
  :: "'a gState_scheme ==> pState ==> varDecl ==> String.literal * variable * channels" 
where
  "toVariable g p (VarDeclNum lb hb name siz init) = (
     let type = VTBounded lb hb in
     if ¬ varType_inv type then abortv STR ''Invalid var def (varType_inv failed): '' name
                                       (λ_. (name, Var VTChan 0, []))
     else
       let
         init = checkVarValue type (case init of
                                      None ==> 0
                                    | Some e ==> exprArith g p e);
         v = (case siz of
                None ==> Var type init
              | Some s ==> if nat_of_integer s ≤ max_array_size
                         then VArray type (nat_of_integer s)
                                          (IArray.tabulate (s, λ_. init))
                         else abortv STR ''Invalid var def (array too large): '' name
                                      (λ_. Var VTChan 0))
        in
           (name, v, []))"

| "toVariable g p (VarDeclChan name siz types) = (
     let
       size = (case siz of None ==> 1 | Some s ==> nat_of_integer s);
       chans = (case types of
                  None ==> []
                | Some (cap, tys) ==>
                    let C = (if cap = 0 then HSChannel tys
                             else Channel cap tys []) in
                    if ¬ channel_inv C
                    then abortv STR ''Invalid var def (channel_inv failed): ''
                                name (λ_. [])
                    else replicate size C);
       cidx = (case types of
                 None ==> 0
               | Some _ ==> integer_of_nat (length (channels g)));
       v = (case siz of
              None ==> Var VTChan cidx
            | Some s ==> if nat_of_integer s ≤ max_array_size
                       then VArray VTChan (nat_of_integer s)
                                          (IArray.tabulate (s,
                                             λi. if cidx = 0 then 0
                                                 else i + cidx))
                       else abortv STR ''Invalid var def (array too large): ''
                                   name (λ_. Var VTChan 0))
     in
        (name, v, chans))"

lemma toVariable_variable_inv:
  assumes "gState_inv prog g"
  shows "variable_inv (fst (snd (toVariable g p v)))"
using assms
apply (cases v)
  apply (auto intro!: checkVarValue_Var 
              simp del: variable_inv.simps checkVarValue.simps varType_inv.simps 
              split: if_splits option.splits)
      apply (auto intro!: mod_integer_ge mod_integer_le simp add: min_var_value_def)
    apply (simp_all add: assms gState_inv_def 
               max_channels_def max_var_value_def min_var_value_def max_array_size_def)
    including integer.lifting
    apply (transfer', simp)+
done

lemma toVariable_channels_inv:
  shows "∀x ∈ set (snd (snd (toVariable g p v))). channel_inv x"
by (cases v) auto

lemma toVariable_channels_inv':
  shows "toVariable g p v = (a,b,c) ==> ∀x ∈ set c. channel_inv x"
using toVariable_channels_inv
by (metis snd_conv)

lemma toVariable_variable_inv':
  shows "gState_inv prog g ==> toVariable g p v = (a,b,c) ==> variable_inv b"
by (metis snd_conv fst_conv toVariable_variable_inv)

definition mkChannels 
  :: "'a gState_scheme ==> pState ==> channels ==> 'a gState_scheme * pState"
 where
  "mkChannels g p cs = (
     if cs = [] then (g,p) else
     let l = length (channels g) in
     if l + length cs > max_channels
     then abort STR ''Too much channels'' (λ_. (g,p))
     else let
            cs_p = map integer_of_nat [l..<l + length cs];
            g' = g(channels := channels g @ cs);
            p' = p(pState.channels := pState.channels p @ cs_p)
          in
            (g', p'))"

lemma mkChannels_gState_progress_rel:
  "gState_inv prog g
   ==> set cs ⊆ Collect channel_inv
   ==> (g, fst (mkChannels g p cs)) ∈ gState_progress_rel prog"
unfolding mkChannels_def
by (intro gState_progress_relI) 
   (auto simp add: gState_inv_def gState.defs cl_inv_def)

lemmas mkChannels_gState_inv = 
  mkChannels_gState_progress_rel[THEN gState_progress_rel_gState_invI2]

lemma mkChannels_pState_inv:
  "pState_inv prog p
   ==> cl_inv (g,p)
   ==> pState_inv prog (snd (mkChannels g p cs))"
unfolding mkChannels_def
including integer.lifting
  apply (auto simp add: pState_inv_def pState.defs gState_inv_def dest!: cl_inv_lengthD)
    apply (transfer', simp)+
    done

lemma mkChannels_cl_inv:
  "cl_inv (g,p) ==> cl_inv (mkChannels g p cs)"
unfolding mkChannels_def
by (auto simp add: pState.defs dest: cl_inv_lengthD intro!: cl_invI)

definition mkVarChannel 
  :: "varDecl
      ==> ((var_dict ==> var_dict) ==> 'a gState_scheme * pState
         ==> 'a gState_scheme * pState)
      ==> 'a gState_scheme ==> pState
      ==> 'a gState_scheme * pState" 
where
  "mkVarChannel v upd g p = (
         let
             (k,v,cs) = toVariable g p v;
             (g',p') = upd (lm.update k v) (g,p)
         in
            mkChannels g' p' cs)"

lemma mkVarChannel_gState_inv:
  assumes "gState_inv prog g"
  and "∧k v' cs. toVariable g p v = (k,v',cs)
                 ==> gState_inv prog (fst (upd (lm.update k v') (g,p)))"
  shows "gState_inv prog (fst (mkVarChannel v upd g p))"
using assms unfolding mkVarChannel_def
by (force split: varDecl.split prod.split
          intro!: mkChannels_gState_inv
          dest: toVariable_channels_inv') 

lemma mkVarChannel_gState_progress_rel:
  assumes "gState_inv prog g"
  and "∧k v' cs. toVariable g p v = (k,v',cs)
             ==> (g, fst (upd (lm.update k v') (g,p))) ∈ gState_progress_rel prog"
  shows "(g, fst (mkVarChannel v upd g p)) ∈ gState_progress_rel prog"
proof -
  obtain k v' cs where 1: "toVariable g p v = (k,v',cs)" by (metis prod.exhaust)
  obtain g' p' where 2: "(g',p') = upd (lm.update k v') (g,p)" by (metis prod.exhaust)
  with 1 assms have *: "(g, g') ∈ gState_progress_rel prog" by (metis fst_conv)

  also from 1 2 have "(g', fst (mkChannels g' p' cs)) ∈ gState_progress_rel prog"
    by (force intro!: mkChannels_gState_progress_rel gState_progress_rel_gState_invI2[OF *]
              dest: toVariable_channels_inv')
  finally have "(g, fst (mkChannels g' p' cs)) ∈ gState_progress_rel prog" .
  thus ?thesis using 1 2 by (auto simp add: mkVarChannel_def split: prod.split)
qed
  
lemma mkVarChannel_pState_inv:
  assumes "pState_inv prog p"
  and "cl_inv (g,p)"
  and "∧k v' cs. toVariable g p v = (k,v',cs)
                  ==> cl_inv (upd (lm.update k v') (g,p))"
  and "∧k v' cs. toVariable g p v = (k,v',cs)
                  ==> pState_inv prog (snd (upd (lm.update k v') (g,p)))"
  shows "pState_inv prog (snd (mkVarChannel v upd g p))"
using assms unfolding mkVarChannel_def
by (force split: varDecl.split prod.split 
          intro!: mkChannels_pState_inv)

lemma mkVarChannel_cl_inv:
  assumes "cl_inv (g,p)"
  and "∧k v' cs. toVariable g p v = (k,v',cs)
                 ==> cl_inv (upd (lm.update k v') (g,p))"
  shows "cl_inv (mkVarChannel v upd g p)"
using assms unfolding mkVarChannel_def
by (force split: varDecl.split prod.splits 
          intro!: mkChannels_cl_inv)

definition mkVarChannelProc 
  :: "procVarDecl ==> 'a gState_scheme ==> pState ==> 'a gState_scheme * pState" 
where
  "mkVarChannelProc v g p = (
     let
       v' = case v of
              ProcVarDeclNum lb hb name siz init ==>
                  VarDeclNum lb hb name siz init
           | ProcVarDeclChan name siz ==>
                 VarDeclChan name siz None;
       (k,v,cs) = toVariable g p v'
     in
       mkVarChannel v' (apsnd ∘ pState.vars_update) g p)"

lemma mkVarChannelProc_gState_progress_rel:
  assumes "gState_inv prog g"
  shows "(g, fst (mkVarChannelProc v g p)) ∈ gState_progress_rel prog"
unfolding mkVarChannelProc_def
using assms
by (auto intro!: mkVarChannel_gState_progress_rel)

lemmas mkVarChannelProc_gState_inv = 
  mkVarChannelProc_gState_progress_rel[THEN gState_progress_rel_gState_invI2]

lemma toVariable_name:
  "toVariable g p (VarDeclNum lb hb name sz init) = (x,a,b) ==> x = name"
  "toVariable g p (VarDeclChan name sz t) = (x, a, b) ==> x = name"
by (auto split: if_splits)

declare toVariable.simps[simp del]

lemma statesDecls_process_names:
  assumes "v ∈ statesDecls (states prog !! (pState.idx p))"
  shows "procVarDeclName v ∈ process_names (states prog !! (pState.idx p))
                                           (processes prog !! (pState.idx p))"
using assms
by (cases "processes prog !! (pState.idx p)") (auto simp add: statesNames_def)

lemma mkVarChannelProc_pState_inv:
  assumes "pState_inv prog p"
  and "gState_inv prog g"
  and "cl_inv (g, p)"
  and decl: "v ∈ statesDecls (states prog !! (pState.idx p))"
  shows "pState_inv prog (snd (mkVarChannelProc v g p))"
unfolding mkVarChannelProc_def
using assms statesDecls_process_names[OF decl]
by (auto intro!: mkVarChannel_pState_inv)
   (auto dest: toVariable_name 
         split: procVarDecl.splits 
         intro: toVariable_variable_inv' vardict_inv_updateI
         simp add: pState_inv_def)

lemma mkVarChannelProc_cl_inv:
  assumes "cl_inv (g,p)"
  shows "cl_inv (mkVarChannelProc v g p)"
unfolding mkVarChannelProc_def using assms
by (auto intro!: mkVarChannel_cl_inv)

subsection ‹Folding›
text ‹
 Fold over lists (and lists of lists) of @{typ step}/@{typ stmnt}. The folding functions are
 doing a bit more than that, e.g.\ ensuring the offset into the program array is correct.
 ›

definition step_fold' where
  "step_fold' g steps (lbls :: labels) pri pos
             (nxt :: edgeIndex) (onxt :: edgeIndex option) iB =
     foldr (λstep (pos, nxt, lbls, es).
              let (e,enxt,lbls) = g step (lbls, pri, pos, nxt, onxt, iB)
              in (pos + length e, enxt, lbls, es@e)
    ) steps (pos, nxt, lbls, [])"

definition step_fold where
  "step_fold g steps lbls pri pos nxt onxt iB = (
         let (_,nxt,lbls,s) = step_fold' g steps lbls pri pos nxt onxt iB
          in (s,nxt,lbls))"

lemma step_fold'_cong:
  assumes "lbls = lbls'"
  and "pri = pri'"
  and "pos = pos'"
  and "steps = steps'"
  and "nxt = nxt'"
  and "onxt = onxt'"
  and "iB = iB'"
  and "∧x d. x ∈ set steps ==> g x d = g' x d"
  shows "step_fold' g steps lbls pri pos nxt onxt iB =
         step_fold' g' steps' lbls' pri' pos' nxt' onxt' iB'"
unfolding step_fold'_def 
by (auto intro: foldr_cong simp add: assms)

lemma step_fold_cong[fundef_cong]:
  assumes "lbls = lbls'"
  and "pri = pri'"
  and "pos = pos'"
  and "steps = steps'"
  and "nxt = nxt'"
  and "onxt = onxt'"
  and "iB = iB'"
  and "∧x d. x ∈ set steps ==> g x d = g' x d"
  shows "step_fold g steps lbls pri pos nxt onxt iB =
         step_fold g' steps' lbls' pri' pos' nxt' onxt' iB'"
unfolding step_fold_def
by (auto simp: assms cong: step_fold'_cong)

fun step_foldL_step where
  "step_foldL_step _ _ _ [] (pos, nxt, lbls, es, is) = (pos, nxt, lbls, es, is)"
| "step_foldL_step g pri onxt (s#steps) (pos, nxt, lbls, es, is) = (
     let (pos', nxt', lbls', ss') = step_fold' g steps lbls pri pos nxt onxt False in
     let (s', nxt'', lbls'') = g s (lbls',pri,pos',nxt',onxt,True) in
     let rs = butlast s'; s'' = last s' in
     (pos' + length rs, nxt, lbls'', es@ss'@rs, s''#is))"

definition step_foldL where
  "step_foldL g stepss lbls pri pos nxt onxt =
     foldr (step_foldL_step g pri onxt) stepss (pos,nxt,lbls,[],[])"

lemma step_foldL_step_cong:
  assumes "pri = pri'"
  and "onxt = onxt'"
  and "s = s'"
  and "d = d'"
  and "∧x d. x ∈ set s ==> g x d = g' x d"
  shows "step_foldL_step g pri onxt s d = step_foldL_step g' pri' onxt' s' d'"
using assms
by (cases d', cases s') (simp_all cong: step_fold'_cong)
  
lemma step_foldL_cong[fundef_cong]:
  assumes "lbls = lbls'"
  and "pri = pri'"
  and "pos = pos'"
  and "stepss = stepss'"
  and "nxt = nxt'"
  and "onxt = onxt'"
  and "∧x x' d. x ∈ set stepss ==> x' ∈ set x ==> g x' d = g' x' d"
  shows "step_foldL g stepss lbls pri pos nxt onxt =
         step_foldL g' stepss' lbls' pri' pos' nxt' onxt'"
unfolding step_foldL_def
using assms
apply (cases stepss')
  apply simp
  apply (force intro!: foldr_cong step_foldL_step_cong)
done

subsection ‹Starting processes›
definition modProcArg 
  :: "(procArg * integer) ==> String.literal * variable" 
where
  "modProcArg x = (
     case x of
       (ProcArg ty name, val) ==> if varType_inv ty
                                then let init = checkVarValue ty val
                                     in (name, Var ty init)
                                else abortv STR ''Invalid proc arg (varType_inv failed)''
                                            name (λ_. (name, Var VTChan 0)))"

definition emptyProc :: "pState"
  ― ‹The empty process.›
where
  "emptyProc = (pid = 0, vars = lm.empty (), pc = 0, channels = [], idx = 0 )"

lemma vardict_inv_empty:
  "vardict_inv ss proc (lm.empty())"
unfolding vardict_inv_def
by (simp add: lm.correct)

lemma emptyProc_cl_inv[simp]:
  "cl_inv (g, emptyProc)"
by (simp add: cl_inv_def emptyProc_def)

lemma emptyProc_pState_inv:
  assumes "program_inv prog"
  shows "pState_inv prog emptyProc"
proof -
  from assms have "IArray.length (states prog !! 0) > 0"
    by (intro program_inv_length_states) (auto simp add: program_inv_def)
  with assms show ?thesis
    unfolding pState_inv_def program_inv_def emptyProc_def
    by (auto simp add: vardict_inv_empty)
qed

fun mkProc 
  :: "'a gState_scheme ==> pState
    ==> String.literal ==> expr list ==> process ==> nat
    ==> 'a gState_scheme * pState" 
where
  "mkProc g p name args (sidx, start, argDecls, decls) pidN = (
     let start = case start of
                   Index x ==> x
                 | _ ==> abortv STR ''Process start is not index: '' name (λ_. 0)
     in
      ― ‹sanity check›
      if length args ≠ length argDecls
      then abortv STR ''Signature mismatch: '' name (λ_. (g,emptyProc))
      else
        let
          ― ‹evaluate args (in the context of the calling process)›
          eArgs = map (exprArith g p) args;
        
          ― ‹replace the init part of ‹argDecls››
          argVars = map modProcArg (zip argDecls eArgs);
        
          ― ‹add ‹_pid› to vars›
          pidI = integer_of_nat pidN;
          argVars = (STR ''_pid'', Var (VTBounded 0 pidI) pidI)#argVars;
          argVars = lm.to_map argVars;
        
          ― ‹our new process›
          p = ( pid = pidN, vars = argVars, pc = start, channels = [], idx = sidx )
        in
          ― ‹apply the declarations›
          foldl (λ(g,p) d. mkVarChannel d (apsnd ∘ pState.vars_update) g p)
                (g,p)
                decls)"

lemma mkProc_gState_progress_rel:
  assumes "gState_inv prog g"
  shows "(g, fst (mkProc g p name args (processes prog !! sidx) pidN)) ∈
          gState_progress_rel prog"
proof -
  obtain sidx' start argDecls decls  where 
    p: "processes prog !! sidx = (sidx', start, argDecls, decls)"
    by (metis prod.exhaust)

  from assms have 
    "∧p. (g, fst (foldl (λ(g,p) d. mkVarChannel d (apsnd ∘ pState.vars_update) g p)
                         (g,p) decls))
          ∈ gState_progress_rel prog"
  proof (induction decls arbitrary: g p)
    case (Cons d decls)
    obtain g' p' where 
      new: "(g',p') = (mkVarChannel d (apsnd ∘ pState.vars_update) g p)" 
      by (metis prod.exhaust)
    hence "g' = fst ..." by (metis fst_conv)
    with Cons.prems have g_g': "(g,g') ∈ gState_progress_rel prog" 
      by (auto intro: mkVarChannel_gState_progress_rel)
    also note Cons.IH[OF g_g'[THEN gState_progress_rel_gState_invI2], of p']
    finally show ?case by (auto simp add: o_def new)
  qed simp
  thus ?thesis using assms p by auto
qed

lemmas mkProc_gState_inv = 
  mkProc_gState_progress_rel[THEN gState_progress_rel_gState_invI2]

lemma mkProc_pState_inv:
  assumes "program_inv prog"
  and "gState_inv prog g"
  and "pidN ≤ max_procs" and "pidN > 0"
  and "sidx < IArray.length (processes prog)"
  and "fst (processes prog !! sidx) = sidx"
  shows "pState_inv prog (snd (mkProc g p name args (processes prog !! sidx) pidN))"
proof -
  obtain sidx' start argDecls decls  where 
    "processes prog !! sidx = (sidx', start, argDecls, decls)"
    by (metis prod.exhaust)
  with assms have 
    p_def: "processes prog !! sidx = (sidx, start, argDecls, decls)" 
           "IArray.list_of (processes prog) ! sidx = (sidx, start, argDecls, decls)" 
    by simp_all
  with assms have "(sidx,start,argDecls,decls) ∈ set (IArray.list_of (processes prog))" 
    by (force dest: nth_mem)
  
  with assms obtain s where s: "start = Index s" "s < IArray.length (states prog !! sidx)"
    unfolding program_inv_def by auto
  
  hence P_inv: "pState_inv prog (
                   pid = pidN,
                   vars = lm.to_map
                          ((STR ''_pid'', Var (VTBounded 0 (integer_of_nat pidN))
                             (integer_of_nat pidN))
                          # map modProcArg (zip argDecls (map (exprArith g p) args))),
                   pc = s, channels = [], idx = sidx)"
    unfolding pState_inv_def
    using assms[unfolded program_inv_def]
    including integer.lifting
    apply (simp add: p_def)
    apply (intro lm_to_map_vardict_inv)
    apply auto
              apply (simp add: max_procs_def max_var_value_def)
              apply transfer'
              apply simp
            apply transfer'
            apply simp
          apply (simp add: min_var_value_def)
          apply transfer'
          apply simp
        apply (simp add: max_var_value_def max_procs_def)
        apply transfer'
        apply simp
      apply (drule set_zip_leftD)
      apply (force simp add: modProcArg_def 
                   split: procArg.splits if_splits 
                   intro!: image_eqI)
    apply (clarsimp simp add: modProcArg_def 
                    split: procArg.splits if_splits 
                    simp del: variable_inv.simps)
    apply (intro checkVarValue_Var)
    apply assumption
    done

  from p_def have 
    "varDeclName ` set decls ⊆
      process_names (states prog !! sidx) (processes prog !! sidx)" 
    by auto
  with ‹gState_inv prog g› have 
    F_inv: "∧p. [ pState_inv prog p; sidx = pState.idx p; cl_inv (g,p) ]
                ==> pState_inv prog
                   (snd (foldl (λ(g,p) d. mkVarChannel d (apsnd ∘ pState.vars_update) g p)
                               (g,p) decls))"
  proof (induction decls arbitrary: g p)
    case (Cons d ds) hence 
      decl: "varDeclName d ∈ process_names (states prog !! pState.idx p)
                                           (processes prog !! pState.idx p)" 
      by simp
    
    obtain g' p' where 
      new: "(g',p') = (mkVarChannel d (apsnd ∘ pState.vars_update) g p)" 
      by (metis prod.exhaust)
    hence p': "p' = snd ..." and g': "g' = fst ..." 
      by (metis snd_conv fst_conv)+
    with Cons.prems have "pState_inv prog p'" 
      apply (auto intro!: mkVarChannel_pState_inv)
      apply (simp add: pState_inv_def)
      apply (intro vardict_inv_updateI)
          apply simp
        apply (cases d)
          apply (force dest!: toVariable_name)
        apply (force dest!: toVariable_name)
      apply (intro toVariable_variable_inv')
        apply assumption+
      done
    moreover 
    from p' Cons.prems have "pState.idx p' = sidx" 
      by (auto simp add: mkVarChannel_def mkChannels_def split: prod.split)
    moreover 
    from new Cons.prems have "cl_inv (g',p')" 
      by (auto intro!: mkVarChannel_cl_inv)
    moreover 
    from g' Cons.prems have "gState_inv prog g'" 
      by (auto intro!: mkVarChannel_gState_inv)
    moreover 
    from Cons.prems have 
      "varDeclName ` set ds ⊆
          process_names (states prog !! sidx) (processes prog !! sidx)" 
      by simp
    ultimately 
    have 
      "pState_inv prog
         (snd (foldl (λ(g,p) d. mkVarChannel d (apsnd ∘ pState.vars_update) g p)
                     (g',p') ds))"
      using Cons.IH[of p' g'] by (simp add: o_def)
    with new show ?case by (simp add: o_def)
  qed simp

  show ?thesis 
    by (auto simp add: p_def s cl_inv_def 
             intro: F_inv[OF P_inv]) 
       (blast intro: emptyProc_pState_inv assms)
qed

lemma mkProc_cl_inv:
  assumes "cl_inv (g,p)"
  shows "cl_inv (mkProc g p name args (processes prog !! sidx) pidN)"
proof -
  note IArray.sub_def [simp del]
  obtain sidx' start argDecls decls  
    where [simp]: "processes prog !! sidx = (sidx', start, argDecls, decls)"
    by (metis prod.exhaust)

  have 
    P_inv: "∧s v. cl_inv (g, (pid = pidN, vars = v, pc = s, channels = [], idx = sidx' ))" 
    by (simp add: cl_inv_def)
  
  have 
    "∧p. cl_inv(g,p) ==>
         cl_inv (foldl (λ(g,p) d. mkVarChannel d (apsnd ∘ pState.vars_update) g p)
                       (g,p) decls)"
  proof (induction decls arbitrary: g p)
    case (Cons d ds)
    obtain g' p' where 
      new: "(g',p') = (mkVarChannel d (apsnd ∘ pState.vars_update) g p)" 
      by (metis prod.exhaust)
    with Cons.prems have "cl_inv (g',p')"
      by (auto intro!: mkVarChannel_cl_inv)
    
    from Cons.IH[OF this] new show ?case by (simp add: o_def)
  qed simp
  
  from this[OF P_inv] show ?thesis by auto
qed

declare mkProc.simps[simp del]

definition runProc 
  :: "String.literal ==> expr list ==> program
      ==> 'a gState_scheme ==> pState
      ==> 'a gState_scheme * pState" 
where
  "runProc name args prog g p = (
     if length (procs g) ≥ max_procs
     then abort STR ''Too many processes'' (λ_. (g,p))
     else let pid = length (procs g) + 1 in
          case lm.lookup name (proc_data prog) of
            None ==> abortv STR ''No such process: '' name
                          (λ_. (g,p))
          | Some proc_idx ==>
               let (g', proc) = mkProc g p name args (processes prog !! proc_idx) pid
               in (g'(procs := procs g @ [proc]), p))"

lemma runProc_gState_progress_rel:
  assumes "program_inv prog"
  and "gState_inv prog g"
  and "pState_inv prog p"
  and "cl_inv (g,p)"
  shows "(g, fst (runProc name args prog g p)) ∈ gState_progress_rel prog"
proof (cases "length (procs g) < max_procs")
  note IArray.sub_def [simp del]

  case True thus ?thesis
  proof (cases "lm.lookup name (proc_data prog)")
    case (Some proc_idx)
    hence *: "proc_idx < IArray.length (processes prog)" 
             "fst (processes prog !! proc_idx) = proc_idx"
      using assms 
      by (simp_all add: lm.correct program_inv_def)
      
    obtain g' p' where 
      new: "(g',p') = mkProc g p name args (processes prog !! proc_idx) (length (procs g) + 1)"
      by (metis prod.exhaust)
    hence g': "g' = fst ..." and p': "p' = snd ..." 
      by (metis snd_conv fst_conv)+
    from assms g' have "(g, g') ∈ gState_progress_rel prog " 
      by (auto intro!: mkProc_gState_progress_rel)

    moreover 
    from * assms True p' have "pState_inv prog p'" 
      by (auto intro!: mkProc_pState_inv)
    moreover 
    from assms new have "cl_inv (g',p')" 
      by (auto intro!: mkProc_cl_inv)
    ultimately show ?thesis
      using True Some new assms
      unfolding runProc_def gState_progress_rel_def
      by (clarsimp split: prod.split) 
         (auto simp add: gState_inv_def cl_inv_def)
  next
    case None with assms show ?thesis by (auto simp add: runProc_def)
  qed
next
  case False with assms show ?thesis by (auto simp add: runProc_def)
qed

lemmas runProc_gState_inv = 
  runProc_gState_progress_rel[THEN gState_progress_rel_gState_invI2]

lemma runProc_pState_id:
  "snd (runProc name args prog g p) = p"
unfolding runProc_def
by (auto split: if_splits split: option.split prod.split)

lemma runProc_pState_inv:
  assumes "pState_inv prog p"
  shows "pState_inv prog (snd (runProc name args prog g p))"
by (simp add: assms runProc_pState_id)

lemma runProc_cl_inv:
  assumes "program_inv prog"
  and "gState_inv prog g"
  and "pState_inv prog p"
  and "cl_inv (g,p)"
  shows "cl_inv (runProc name args prog g p)"
proof -
  obtain g' p' where *: "runProc name args prog g p = (g',p')" 
    by (metis prod.exhaust)
  with runProc_gState_progress_rel[OF assms, of name args] have 
    "length (channels g) ≤ length (channels g')" 
    by (simp add: gState_progress_rel_def)
  moreover from * runProc_pState_id have "p' = p" by (metis snd_conv)
  ultimately show ?thesis by (metis ‹cl_inv (g,p)› * cl_inv_trans)
qed

subsection ‹AST to edges›

type_synonym ast = "AST.module list"

text ‹In this section, the AST is translated into the transition system.›

text ‹
 Handling atomic blocks is non-trivial. Therefore, we do this in an extra pass:
 @{term lp} and @{term hp} are the positions of the start and the end of
 the atomic block. Every edge pointing into this range is therefore marked as
 @{term Atomic}. If they are pointing somewhere else, they are set to @{term InAtomic},
 meaning: they start \emph{in} an atomic block, but leave it afterwards.
 ›
definition atomize :: "nat ==> nat ==> edge list ==> edge list" where
  "atomize lp hp es = fold (λe es.
     let e' = case target e of
                 LabelJump _ None ==>
                    ― ‹Labels are checked again later on, when they›
                    ― ‹are going to be resolved. Hence it is safe to say›
                    ― ‹‹atomic› here, especially as the later algorithm›
                    ― ‹relies on targets in atomic blocks to be marked as such.›
                    e( atomic := InAtomic )
                | LabelJump _ (Some via) ==>
                    if lp ≤ via ∧ hp ≥ via then e( atomic := Atomic )
                    else e( atomic := InAtomic )
                | Index p' ==>
                    if lp ≤ p' ∧ hp ≥ p' then e( atomic := Atomic )
                    else e( atomic := InAtomic )
      in e'#es) es []"

fun skip ― ‹No-(edge)›
where 
  "skip (lbls, pri, pos, nxt, _) =
  ([[(cond = ECExpr (ExprConst 1),
       effect = EEId, target = nxt, prio = pri,
       atomic = NonAtomic)]], Index pos, lbls)"

text ‹
 The AST is walked backwards. This allows to know the next state directly.

 Parameters used:
 \begin{description}
 \item[lbls] Map of Labels
 \item[pri] Current priority
 \item[pos] Current position in the array
 \item[nxt] Next state
 \item[onxt] Previous 'next state' (where to jump after a 'do')
 \item[inBlock] Needed for certain constructs to calculate the layout of the array
 \end{description}
 ›

fun stepToState 
  :: "step
      ==> (labels * integer * nat * edgeIndex * edgeIndex option * bool)
      ==> edge list list * edgeIndex * labels"
and stmntToState 
  :: "stmnt
      ==> (labels * integer * nat * edgeIndex * edgeIndex option * bool)
      ==> edge list list * edgeIndex * labels"
where
  "stepToState (StepStmnt s None) data = stmntToState s data"
| "stepToState (StepStmnt s (Some u)) (lbls, pri, pos, nxt, onxt, _) = (
     let
        ― ‹the ‹unless› part›
        (ues,_,lbls') = stmntToState u (lbls, pri, pos, nxt, onxt, True);
        u = last ues; ues = butlast ues;
        pos' = pos + length ues;
    
        ― ‹find minimal current priority›
        pri = min_prio u pri;

        ― ‹the guarded part --›
        ― ‹priority is decreased, because there is now a new unless part with›
        ― ‹higher prio›
        (ses,spos,lbls'') = stmntToState s (lbls', pri - 1, pos', nxt, onxt, False);
 
        ― ‹add an edge to the unless part for each generated state›
        ses = map (List.append u) ses
     in
        (ues@ses,spos,lbls''))"

| "stepToState (StepDecl decls) (lbls, pri, pos, nxt, onxt, _) = (
     let edgeF = λd (lbls,pri,pos,nxt,_).
        ([[(cond = ECTrue, effect = EEDecl d, target = nxt,
             prio = pri, atomic = NonAtomic)]], Index pos, lbls)
     in
        step_fold edgeF decls lbls pri pos nxt onxt False)"

| "stepToState StepSkip (lbls,_,_,nxt,_) = ([],nxt,lbls)"

| "stmntToState (StmntAtomic steps) (lbls, pri, pos, nxt, onxt, inBlock) = (
    let (es,pos',lbls') = step_fold stepToState steps lbls pri pos nxt onxt inBlock in
    let es' = map (atomize pos (pos + length es)) es in
    (es', pos', lbls'))"

| "stmntToState (StmntLabeled l s) (lbls, pri, pos, d) = (
     let
         (es, pos', lbls) = stmntToState s (lbls, pri, pos, d);
         
         ― ‹We don't resolve goto-chains. If the labeled stmnt returns only a jump,›
         ― ‹use this goto state.›
         lpos = case pos' of Index p ==> p | _ ==> pos;
         lbls' = add_label l lbls lpos
     in
       (es, pos', lbls'))"

| "stmntToState (StmntDo stepss) (lbls, pri, pos, nxt, onxt, inBlock) = (
    let
       ― ‹construct the different branches›
       ― ‹‹nxt› in those branches points current pos (it is a loop after all)›
       ― ‹‹onxt› then is the current ‹nxt› (needed for break, f.ex.)›
       (_,_,lbls,es,is) = step_foldL stepToState stepss lbls pri
                                     (pos+1) (Index pos) (Some nxt);

       ― ‹put the branch starting points (‹is›) into the array›
       es' = concat is # es
    in
      if inBlock then
           ― ‹inside another DO or IF or UNLESS›
           ― ‹‹⟶› append branches again, so they can be consumed›
           (es' @ [concat is], Index pos, lbls)
      else
          (es', Index pos, lbls)
   )"

| "stmntToState (StmntIf stepss) (lbls, pri, pos, nxt, onxt, _) = (
     let (pos,_,lbls,es,is) = step_foldL stepToState stepss lbls pri pos nxt onxt
     in (es @ [concat is], Index pos, lbls))"

| "stmntToState (StmntSeq steps) (lbls, pri, pos, nxt, onxt, inBlock) =
     step_fold stepToState steps lbls pri pos nxt onxt inBlock"


| "stmntToState (StmntAssign v e) (lbls, pri, pos, nxt, _) =
   ([[(cond = ECTrue, effect = EEAssign v e, target = nxt, prio = pri,
        atomic = NonAtomic)]], Index pos, lbls)"

| "stmntToState (StmntAssert e) (lbls, pri, pos, nxt, _) =
   ([[(cond = ECTrue, effect = EEAssert e, target = nxt, prio = pri,
        atomic = NonAtomic)]], Index pos, lbls)"

| "stmntToState (StmntCond e) (lbls, pri, pos, nxt, _) =
   ([[(cond = ECExpr e, effect = EEId, target = nxt, prio = pri,
        atomic = NonAtomic)]], Index pos, lbls)"

| "stmntToState StmntElse (lbls, pri, pos, nxt, _) =
   ([[(cond = ECElse, effect = EEId, target = nxt, prio = pri,
        atomic = NonAtomic )]], Index pos, lbls)"

| "stmntToState StmntBreak (lbls,pri,_,_,Some onxt,_) =
   ([[(cond = ECTrue, effect = EEGoto, target = onxt, prio = pri,
        atomic = NonAtomic )]], onxt, lbls)"
| "stmntToState StmntBreak (_,_,_,_,None,_) =
   abort STR ''Misplaced break'' (λ_. ([],Index 0,lm.empty()))"

| "stmntToState (StmntRun n args) (lbls, pri, pos, nxt, onxt, _) =
   ([[(cond = ECRun n, effect = EERun n args, target = nxt, prio = pri,
        atomic = NonAtomic )]], Index pos,lbls)"

| "stmntToState (StmntGoTo l) (lbls, pri, pos, _) =
   ([[(cond = ECTrue, effect = EEGoto, target = LabelJump l None, prio = pri,
        atomic = NonAtomic )]], LabelJump l (Some pos), lbls)"

| "stmntToState (StmntSend v e srt) (lbls, pri, pos, nxt, _) =
   ([[(cond = ECSend v, effect = EESend v e srt, target = nxt, prio = pri,
        atomic = NonAtomic )]], Index pos, lbls)"

| "stmntToState (StmntRecv v r srt rem) (lbls, pri, pos, nxt, _) =
   ([[(cond = ECRecv v r srt, effect = EERecv v r srt rem, target = nxt, prio = pri,
        atomic = NonAtomic )]], Index pos, lbls)"

| "stmntToState StmntSkip d = skip d"

subsubsection ‹Setup›
definition endState :: "edge list" where
  ― ‹An extra state added to each process marking its end.›
  "endState = [( cond = ECFalse, effect = EEEnd, target = Index 0, prio = 0,
                  atomic = NonAtomic)]"

definition resolveLabel :: "String.literal ==> labels ==> nat" where
  "resolveLabel l lbls = (
     case lm.lookup l lbls of
       None ==> abortv STR ''Unresolved label: '' l (λ_. 0)
     | Some pos ==> pos)"

primrec resolveLabels :: "edge list list ==> labels ==> edge list ==> edge list" where
  "resolveLabels _ _ [] = []"
| "resolveLabels edges lbls (e#es) = (
    let check_atomic = λpos. fold (λe a. a ∧ inAtomic e) (edges ! pos) True in
    case target e of
      Index _ ==> e
    | LabelJump l None ==>
         let pos = resolveLabel l lbls in
           e(target := Index pos,
              atomic := if inAtomic e then
                           if check_atomic pos then Atomic
                           else InAtomic
                        else NonAtomic )
     | LabelJump l (Some via) ==>
          let pos = resolveLabel l lbls in
            e(target := Index pos,
               ― ‹NB: ‹isAtomic› instead of ‹inAtomic›, cf ‹atomize()››
               atomic := if isAtomic e then
                            if check_atomic pos ∧ check_atomic via then Atomic
                            else InAtomic
                         else atomic e )
   ) # (resolveLabels edges lbls es)"

definition calculatePrios :: "edge list list ==> (integer * edge list) list" where
  "calculatePrios ess = map (λes. (min_prio es 0, es)) ess"

definition toStates :: "step list ==> states * edgeIndex * labels" where
  "toStates steps = (
    let
       (states,pos,lbls) = step_fold stepToState steps (lm.empty())
                                     0 1 (Index 0) None False;
       pos = (case pos of
                Index _ ==> pos
              | LabelJump l _ ==> Index (resolveLabel l lbls));
       states = endState # states;
       states = map (resolveLabels states lbls) states;
       states = calculatePrios states
    in
    case pos of Index s ==>
          if s < length states then (IArray states, pos, lbls)
          else abort STR ''Start index out of bounds'' (λ_. (IArray states, Index 0, lbls)))"

lemma toStates_inv:
  assumes "toStates steps = (ss,start,lbls)"
  shows "∃s. start = Index s ∧ s < IArray.length ss"
    and "IArray.length ss > 0"
  using assms
  unfolding toStates_def calculatePrios_def
  by (auto split: prod.splits edgeIndex.splits if_splits)

(* returns: states * is_active * name * labels * process *)
primrec toProcess 
  :: "nat ==> proc ==> states * nat * String.literal * (labels * process)"
 where
  "toProcess sidx (ProcType act name args decls steps) = (
     let
       (states, start, lbls) = toStates steps;
       act = (case act of
                None ==> 0
              | Some None ==> 1
              | Some (Some x) ==> nat_of_integer x)
     in
        (states, act, name, lbls, sidx, start, args, decls))"
| "toProcess sidx (Init decls steps) = (
      let (states, start, lbls) = toStates steps in
      (states, 1, STR '':init:'', lbls, sidx, start, [], decls))"

lemma toProcess_sidx:
  "toProcess sidx p = (ss,a,n,l,idx,r) ==> idx = sidx"
by (cases p) (simp_all split: prod.splits)

lemma toProcess_states_nonempty:
  "toProcess sidx p = (ss,a,n,l,idx,r) ==> IArray.length ss > 0"
by (cases p) (force split: prod.splits dest: toStates_inv(2))+

lemma toProcess_start:
  "toProcess sidx p = (ss,a,n,l,idx,start,r)
   ==> ∃s. start = Index s ∧ s < IArray.length ss"
by (cases p) (force split: prod.splits dest: toStates_inv(1))+


lemma toProcess_startE:
  assumes "toProcess sidx p = (ss,a,n,l,idx,start,r)"
  obtains s where "start = Index s" "s < IArray.length ss"
  using toProcess_start[OF assms]
  by blast

text ‹
 The main construction function. Takes an AST
 and returns an initial state,
 and the program (= transition system).
 ›

definition setUp :: "ast ==> program × gState" where
  "setUp ast = (
      let
       (decls, procs, _) = preprocess ast;
       assertVar = Var (VTBounded 0 1) 0;
 
       pre_procs = map (case_prod toProcess) (List.enumerate 1 procs);

       procs = IArray ((0, Index 0, [], []) # map (λ(_,_,_,_,p). p) pre_procs);
       labels = IArray (lm.empty() # map (λ(_,_,_,l,_). l) pre_procs);
       states = IArray (IArray [(0,[])] # map (λ(s,_). s) pre_procs);
       names = IArray (STR ''invalid'' # map (λ(_,_,n,_). n) pre_procs);

       proc_data = lm.to_map (map (λ(_,_,n,_,idx,_). (n,idx)) pre_procs);
       
       prog = ( processes = procs, labels = labels, states = states,
                 proc_names = names, proc_data = proc_data );
     
       g = ( vars = lm.sng (STR ''__assert__'') assertVar,
              channels = [InvChannel], timeout = False, procs = [] );
       g' = foldl (λg d.
                    fst (mkVarChannel d (apfst ∘ gState.vars_update) g emptyProc)
                  ) g decls;
       g'' = foldl (λg (_,a,name,_).
                    foldl (λg name.
                              fst (runProc name [] prog g emptyProc)
                          ) g (replicate a name)
                   ) g' pre_procs
      in
       (prog, g''))"

lemma setUp_program_inv':
  "program_inv (fst (setUp ast))"
proof (rule program_invI, goal_cases)
  case 1 show ?case by (simp add: setUp_def split: prod.split)
next
  case 2 show ?case by (simp add: setUp_def split: prod.split)
next
  case 3 thus ?case
    by (auto simp add: setUp_def o_def  
             split: prod.splits 
             dest!: toProcess_states_nonempty)
next
  case 4 thus ?case
    unfolding setUp_def
    by (auto simp add: lm.correct o_def in_set_enumerate_eq nth_enumerate_eq 
            dest!: subsetD[OF Misc.ran_map_of] toProcess_sidx 
            split: prod.splits)
  (* TODO: Change name Misc.ran_map_of \<longrightarrow> ran_map_of_ss, as it collides 
      with AList.ran_map_of *)
next
  case 5 thus ?case
    apply (auto simp add: setUp_def o_def split: prod.splits)
    apply (frule toProcess_sidx)
    apply (frule toProcess_start)
    apply (auto simp: in_set_enumerate_eq nth_enumerate_eq)
    done
qed

lemma setUp_program_inv:
  assumes "setUp ast = (prog,g)"
  shows "program_inv prog"
using assms setUp_program_inv' 
by (metis fst_conv)

lemma setUp_gState_inv:
  assumes "setUp ast = (prog, g)"
  shows "gState_inv prog g"
proof -
  from assms have p_INV: "program_inv prog" by (fact setUp_program_inv)

  {
    fix prog :: program
    assume *: "program_inv prog"
    let ?g = "( vars = lm.sng (STR ''__assert__'') (Var (VTBounded 0 1) 0),
                 channels = [InvChannel], timeout = False, procs = [] )"

    have g1: "gState_inv prog ?g"
      by (simp add: gState_inv_def max_channels_def lm_correct max_var_value_def)
    {
      fix g decls
      assume "gState_inv prog g"
      hence "gState_inv prog (foldl (λg d.
                   fst (mkVarChannel d (apfst ∘ gState.vars_update) g emptyProc)
                  ) g decls)"
        apply (rule foldl_rule)
        apply (intro mkVarChannel_gState_inv)
          apply simp
        apply (frule_tac g=σ in toVariable_variable_inv')
          apply assumption
        apply (auto simp add: gState_inv_def lm.correct)
        done
    }
    note g2 = this[OF g1]

    {
      fix g :: "'a gState_scheme" and pre_procs
      assume "gState_inv prog g"
      hence "gState_inv prog (foldl (λg (_,a,name,_).
                 foldl (λg name.
                         fst (runProc name [] prog g emptyProc)
                       ) g (replicate a name)
              ) g pre_procs)"
        apply (rule foldl_rule)
        apply (clarsimp split: prod.splits)
        apply (rule foldl_rule)
          apply (auto intro!: runProc_gState_inv emptyProc_pState_inv *)
        done
    }
    note this[OF g2]
  } note g_INV = this

  from assms p_INV show ?thesis
    unfolding setUp_def
    by (auto split: prod.splits intro!: g_INV)
qed


subsection ‹Semantic Engine›

text ‹
 After constructing the transition system, we are missing the final part:
 The successor function on this system. We use SPIN-nomenclature and call it
 \emph{semantic engine}.
 ›

definition "assertVar ≡ VarRef True (STR ''__assert__'') None"

subsubsection ‹Evaluation of Edges›

fun evalRecvArgs 
  :: "recvArg list ==> integer list ==> gState_I ==> pState ==> gState_I * pState"
where
  "evalRecvArgs [] [] g l = (g,l)"
| "evalRecvArgs _ [] g l =
     abort STR ''Length mismatch on receiving.'' (λ_. (g,l))"
| "evalRecvArgs [] _ g l =
     abort STR ''Length mismatch on receiving.'' (λ_. (g,l))"
| "evalRecvArgs (r#rs) (v#vs) g l = (
     let (g,l) =
       case r of
          RecvArgVar var ==> setVar var v g l
        | _ ==> (g,l)
     in evalRecvArgs rs vs g l)"

primrec evalCond 
  :: "edgeCond ==> gState_I ==> pState ==> bool"
where
  "evalCond ECTrue _ _ ⟷ True"
| "evalCond ECFalse _ _ ⟷ False"
| "evalCond (ECExpr e) g l ⟷ exprArith g l e ≠ 0"
| "evalCond (ECRun _) g l ⟷ length (procs g) < 255"
| "evalCond ECElse g l ⟷ gState_I.else g"
| "evalCond (ECSend v) g l ⟷
     withChannel v (λ_ c.
       case c of
         Channel cap _ q ==> integer_of_nat (length q) < cap
       | HSChannel _ ==> True) g l"
| "evalCond (ECRecv v rs srt) g l ⟷
     withChannel v (λi c.
       case c of
         HSChannel _ ==> handshake g ≠ 0 ∧ recvArgsCheck g l rs (hsdata g)
       | _ ==> pollCheck g l c rs srt) g l"

fun evalHandshake 
  :: "edgeCond ==> nat ==> gState_I ==> pState ==> bool"
where
  "evalHandshake (ECRecv v _ _) h g l
    ⟷ h = 0
     ∨ withChannel v (λi c. case c of
                             HSChannel _ ==> i = h
                           | Channel _ _ _ ==> False) g l"
| "evalHandshake _ h _ _ ⟷ h = 0"

primrec evalEffect 
  :: "edgeEffect ==> program ==> gState_I ==> pState ==> gState_I * pState"
where
  "evalEffect EEEnd _ g l = (g,l)"
| "evalEffect EEId _ g l = (g,l)"
| "evalEffect EEGoto _ g l = (g,l)"
| "evalEffect (EEAssign v e) _ g l = setVar v (exprArith g l e) g l"
| "evalEffect (EEDecl d) _ g l = mkVarChannelProc d g l"
| "evalEffect (EERun name args) prog g l = runProc name args prog g l"
| "evalEffect (EEAssert e) _ g l = (
     if exprArith g l e = 0
     then setVar assertVar 1 g l
     else (g,l))"
| "evalEffect (EESend v es srt) _ g l = withChannel v (λi c.
     let
       ab = λ_. abort STR ''Length mismatch on sending.'' (λ_. (g,l));
       es = map (exprArith g l) es
     in
       if ¬ for_all (λx. x ≥ min_var_value ∧ x ≤ max_var_value) es
       then abort STR ''Invalid Channel'' (λ_. (g,l))
       else
          case c of
            Channel cap ts q ==>
              if length ts ≠ length es ∨ ¬ (length q < max_array_size)
              then ab()
              else let
                     q' = if ¬ srt then q@[es]
                          else let
                            q = map lexlist q;
                            q' = insort (lexlist es) q
                          in map unlex q';
                     g = gState.channels_update (λcs.
                              cs[ i := Channel cap ts q' ]) g
                   in (g,l)
          | HSChannel ts ==>
              if length ts ≠ length es then ab()
              else (g(hsdata := es, handshake := i), l)
          | InvChannel ==> abort STR ''Trying to send on invalid channel'' (λ_. (g,l))
    ) g l"
| "evalEffect (EERecv v rs srt rem) _ g l = withChannel v (λi c.
     case c of
       Channel cap ts qs ==>
          if qs = [] then abort STR ''Recv from empty channel'' (λ_. (g,l))
          else
             let
               (q', qs') = if ¬ srt then (hd qs, tl qs)
                           else apfst the (find_remove (recvArgsCheck g l rs) qs);
               (g,l) = evalRecvArgs rs q' g l;
               g = if rem
                   then gState.channels_update (λcs. cs[ i := Channel cap ts qs']) g
                   else g
                     ― ‹messages are not removed -- so no need to update anything›
             in (g,l)
      | HSChannel _ ==>
             let (g,l) = evalRecvArgs rs (hsdata g) g l in
             let g = g( handshake := 0, hsdata := [] )
             in (g,l)
      | InvChannel ==> abort STR ''Receiving on invalid channel'' (λ_. (g,l))
   ) g l"

lemma statesDecls_effect:
  assumes "ef ∈ effect ` edgeSet ss"
  and "ef = EEDecl d"
  shows "d ∈ statesDecls ss"
proof -
  from assms obtain e where "e ∈ edgeSet ss" "ef = effect e" by auto
  thus ?thesis  using assms
    unfolding statesDecls_def
    by (auto simp add: edgeDecls_def 
             intro!: bexI[where x = e] 
             split: edgeEffect.split)
qed

lemma evalRecvArgs_pState_inv:
  assumes "pState_inv prog p"
  shows "pState_inv prog (snd (evalRecvArgs rargs xs g p))"
  using assms
proof (induction rargs xs arbitrary: p g rule: list_induct2')
  case (4 r rs x xs) thus ?case
  proof (cases r)
    case (RecvArgVar v)
    obtain g' p' where  new: "setVar v x g p = (g',p')" by (metis prod.exhaust)
    hence "p' = snd (setVar v x g p)" by simp
    with "4" have "pState_inv prog p'" by (auto intro!: setVar_pState_inv)
    from "4.IH"[OF this] RecvArgVar new show ?thesis by simp
  qed simp_all
qed simp_all

lemma evalRecvArgs_pState_inv':
  assumes "evalRecvArgs rargs xs g p = (g', p')"
  and "pState_inv prog p"
  shows "pState_inv prog p'"
using assms evalRecvArgs_pState_inv 
by (metis snd_conv)

lemma evalRecvArgs_gState_progress_rel:
  assumes "gState_inv prog g"
  shows "(g, fst (evalRecvArgs rargs xs g p)) ∈ gState_progress_rel prog"
  using assms
proof (induction rargs xs arbitrary: p g rule: list_induct2')
  case (4 r rs x xs) thus ?case
  proof (cases r)
    case (RecvArgVar v)
    obtain g' p' where new: "setVar v x g p = (g',p')" by (metis prod.exhaust)
    hence "g' = fst (setVar v x g p)" by simp
    with "4" have "(g, g') ∈ gState_progress_rel prog" 
      by (auto intro!: setVar_gState_progress_rel)
    also hence "gState_inv prog g'" 
      by (rule gState_progress_rel_gState_invI2)
    note "4.IH"[OF this, of p']
    finally show ?thesis using RecvArgVar new by simp
  qed simp_all
qed simp_all

lemmas evalRecvArgs_gState_inv = 
  evalRecvArgs_gState_progress_rel[THEN gState_progress_rel_gState_invI2]

lemma evalRecvArgs_cl_inv:
  assumes "cl_inv (g,p)"
  shows "cl_inv (evalRecvArgs rargs xs g p)"
  using assms
proof (induction rargs xs arbitrary: p g rule: list_induct2')
  case (4 r rs x xs) thus ?case
  proof (cases r)
    case (RecvArgVar v) 
    with 4 have "cl_inv (setVar v x g p)" 
      by (auto intro!: setVar_cl_inv)
    with "4.IH" RecvArgVar show ?thesis 
      by (auto split: prod.splits)
  qed simp_all
qed simp_all

lemma evalEffect_pState_inv:
  assumes "pState_inv prog p"
  and "gState_inv prog g"
  and "cl_inv (g,p)"
  and "e ∈ effect ` edgeSet (states prog !! pState.idx p)"
  shows "pState_inv prog (snd (evalEffect e prog g p))"
  using assms
proof (cases e)
  case (EEDecl d) 
  with assms have "d ∈ statesDecls (states prog !! pState.idx p)"
    using statesDecls_effect 
    by simp
  with assms EEDecl show ?thesis
    by (auto simp del: IArray.sub_def 
             intro!: mkVarChannelProc_pState_inv)
next
  case (EESend c es srt) 
  then obtain v where "ChanRef v = c" by (cases c) simp
  with EESend assms show ?thesis
    by (cases v) (auto simp add: withChannel'_def withVar'_def split: channel.split)
next
  case (EERecv c es srt) 
  then obtain v where "ChanRef v = c" by (cases c) simp
  with EERecv assms show ?thesis
    by (cases v)  
       (auto simp: withChannel'_def withVar'_def 
             split: prod.splits channel.split 
             dest: evalRecvArgs_pState_inv')
qed (clarsimp_all intro!: setVar_pState_inv runProc_pState_inv)

lemma evalEffect_gState_progress_rel:
  assumes "program_inv prog"
  and "gState_inv prog g"
  and "pState_inv prog p"
  and "cl_inv (g,p)"
  shows "(g, fst (evalEffect e prog g p)) ∈ gState_progress_rel prog"
using assms
proof (cases e)
  case EEAssert 
  with assms show ?thesis 
    by (auto intro: setVar_gState_progress_rel)
next
  case EEAssign 
  with assms show ?thesis 
    by (auto intro: setVar_gState_progress_rel)
next
  case EEDecl 
  with assms show ?thesis 
    by (auto intro: mkVarChannelProc_gState_progress_rel)
next
  case EERun 
  with assms show ?thesis 
    by (auto intro: runProc_gState_progress_rel)
next
  case (EESend c es srt) 
  then obtain v where v: "c = ChanRef v" by (metis chanRef.exhaust)
  obtain idx where idx: "nat_of_integer (the (getVar v g p)) = idx" by blast
  note idx' = idx[symmetric, unfolded getVar_def]
  show ?thesis
  proof (cases "idx < length (gState.channels g)")
    case True 
    note DEF = True EESend v idx' assms
    
    show ?thesis
    proof (cases "gState.channels g ! idx")
      case (Channel cap ts q) 
      with True have "Channel cap ts q ∈ set (gState.channels g)" 
        by (metis nth_mem)
      with assms have "channel_inv (Channel cap ts q)" 
        by (auto simp add: gState_inv_def simp del: channel_inv.simps)
      with Channel DEF show ?thesis
        by (cases v) 
           (auto simp add: withChannel'_def withVar'_def for_all_def
                 split: channel.split 
                 intro!: gState_progress_rel_channels_update)
    next
      case HSChannel with DEF show ?thesis 
        by (cases v) 
           (auto simp: withChannel'_def withVar'_def gState_progress_rel_def 
                       gState_inv_def
                split: channel.split)
    next
      case InvChannel with DEF show ?thesis 
        by (cases v) (auto simp add: withChannel'_def withVar'_def)
    qed
  next
    case False with EESend idx' v assms show ?thesis 
      by (cases v) (auto simp add: withChannel'_def withVar'_def)
  qed
next
  case (EERecv c rs srt rem) 
  then obtain v where v: "c = ChanRef v" by (metis chanRef.exhaust)
  obtain idx where idx: "nat_of_integer (the (getVar v g p)) = idx" by blast
  note idx' = idx[symmetric, unfolded getVar_def]
  show ?thesis
  proof (cases "idx < length (gState.channels g)")
    case True 
    note DEF = True EERecv v idx' assms
    show ?thesis
    proof (cases "gState.channels g ! idx")
      note channel_inv.simps[simp del]
      case (Channel cap ts q) 
      with True have "Channel cap ts q ∈ set (gState.channels g)" 
        by (metis nth_mem)
      with assms have c_inv: "channel_inv (Channel cap ts q)" 
        by (auto simp add: gState_inv_def simp del: channel_inv.simps)
      moreover obtain res q' where 
        "apfst the (find_remove (recvArgsCheck g p rs) q) = (res, q')" 
        by (metis prod.exhaust)
      moreover hence "q' = snd (find_remove (recvArgsCheck g p rs) q)"
        by (simp add: apfst_def map_prod_def split: prod.splits)
      with find_remove_subset find_remove_length have 
        "set q' ⊆ set q" "length q' ≤ length q" 
        by (metis surjective_pairing)+
      with c_inv have "channel_inv (Channel cap ts q')" 
        by (auto simp add: channel_inv.simps)
      moreover {
        assume "q ≠ []"
        hence "set (tl q) ⊆ set q" using tl_subset by auto
        with c_inv have "channel_inv (Channel cap ts (tl q))" 
          by (auto simp add: channel_inv.simps)
      } 
      moreover {
        fix res g' p'
        assume "evalRecvArgs rs res g p = (g',p')" 
        with evalRecvArgs_gState_progress_rel assms have 
          "(g,g') ∈ gState_progress_rel prog" 
          by (metis fst_conv)
        hence "length (channels g) ≤ length (channels g')" 
          by (simp add: gState_progress_rel_def)
      }
      ultimately show ?thesis using Channel DEF
        apply (cases v) 
        apply (auto simp add: withChannel'_def withVar'_def for_all_def 
                    split: channel.split prod.split
                    elim: fstE 
                    intro!: evalRecvArgs_gState_progress_rel 
                            gState_progress_rel_channels_update_step)
          apply force+
        done
    next
      case HSChannel 
      obtain g' p' where *: "evalRecvArgs rs (hsdata g) g p = (g',p')" 
        by (metis prod.exhaust)
      with assms have "(g,g') ∈ gState_progress_rel prog" 
        by (auto elim!: fstE intro!: evalRecvArgs_gState_progress_rel)
      also hence "gState_inv prog g'" by blast
      hence "(g',g'(handshake := 0, hsdata := [])) ∈ gState_progress_rel prog" 
        by (auto simp add: gState_progress_rel_def gState_inv_def)
      finally 
      have "(g,g'(handshake := 0, hsdata := [])) ∈ gState_progress_rel prog" .
      with DEF HSChannel * show ?thesis 
        by (cases v) (auto simp add: withChannel'_def withVar'_def for_all_def 
                           split: channel.split prod.split)
    next
      case InvChannel with DEF show ?thesis 
        by (cases v) (auto simp add: withChannel'_def withVar'_def)
    qed
  next
    case False with EERecv idx' v assms show ?thesis 
      by (cases v) (auto simp add: withChannel'_def withVar'_def)
  qed
qed simp_all

lemma evalEffect_cl_inv:
  assumes "cl_inv (g,p)"
  and "program_inv prog"
  and "gState_inv prog g"
  and "pState_inv prog p"
  shows "cl_inv (evalEffect e prog g p)"
  using assms
proof (cases e)
  case EERun with assms show ?thesis by (force intro!: runProc_cl_inv)
next
  case (EESend c es srt) then obtain v where "ChanRef v = c" by (cases c) simp
  with EESend assms show ?thesis
    by (cases v)
       (auto simp add: withChannel'_def withVar'_def split: channel.split
             intro!: cl_inv_channels_update)
next
  case (EERecv c es srt) then obtain v where "ChanRef v = c" by (cases c) simp
  with EERecv assms show ?thesis
    apply (cases v)
    apply (auto simp add: withChannel'_def withVar'_def split: channel.split prod.split
                intro!: cl_inv_channels_update)
    apply (metis evalRecvArgs_cl_inv)+
    done
qed (simp_all add: setVar_cl_inv mkVarChannelProc_cl_inv)

subsubsection ‹Executable edges›

text ‹
 To find a successor global state, we first need to find all those edges which are executable
 (\ie the condition evaluates to true).
 ›
type_synonym choices = "(edge * pState) list"
  ― ‹A choice is an executable edge and the process it belongs to.›

definition getChoices :: "gState_I ==> pState ==> edge list ==> choices" where
  "getChoices g p = foldl (λE e.
      if evalHandshake (cond e) (handshake g) g p ∧ evalCond (cond e) g p
      then (e,p)#E
      else E) []"

lemma getChoices_sub_edges_fst:
  "fst ` set (getChoices g p es) ⊆ set es"
unfolding getChoices_def
by (rule foldl_rule_aux) auto

lemma getChoices_sub_edges:
  "(a,b) ∈ set (getChoices g p es) ==> a ∈ set es"
using getChoices_sub_edges_fst
by force

lemma getChoices_p_snd:
  "snd ` set (getChoices g p es) ⊆ {p}"
unfolding getChoices_def
by (rule foldl_rule_aux) auto

lemma getChoices_p:
  "(a,b) ∈ set (getChoices g p es) ==> b = p"
using getChoices_p_snd
by force

definition sort_by_pri where
  "sort_by_pri min_pri edges = foldl (λes e.
      let idx = nat_of_integer (abs (prio e))
      in if idx > min_pri
         then abort STR ''Invalid priority'' (λ_. es)
         else let ep = e # (es ! idx) in es[idx := ep]
      ) (replicate (min_pri + 1) []) edges"

lemma sort_by_pri_edges':
  assumes "set edges ⊆ A"
  shows "set (sort_by_pri min_pri edges) ⊆ {xs. set xs ⊆ A}"
using assms
unfolding sort_by_pri_def
apply (rule_tac I="λσ _. (∀x ∈ set σ. set x ⊆ A) ∧ length σ = min_pri + 1" in foldl_rule_aux_P)
    apply simp
  apply (force dest!: subsetD[OF set_update_subset_insert] 
               split: if_splits)
apply force
done

lemma sort_by_pri_edges:
  assumes "set edges ⊆ A"
  and "es ∈ set (sort_by_pri min_pri edges)"
  shows "set es ⊆ A"
using sort_by_pri_edges'[OF assms(1)] assms
by auto

lemma sort_by_pri_length:
  "length (sort_by_pri min_pri edges) = min_pri + 1"
unfolding sort_by_pri_def
by (rule foldl_rule_aux_P [where I="λσ _. length σ = min_pri + 1"]) 
   simp_all

definition executable 
  :: "states iarray ==> gState_I ==> choices nres"
  ― ‹Find all executable edges›
 where
  "executable ss g = (
      let procs = procs g in
      nfoldli procs (λ_. True) (λp E.
        if (exclusive g = 0 ∨ exclusive g = pid p) then do {
            let (min_pri, edges) = (ss !! pState.idx p) !! pc p;
            ASSERT(set edges ⊆ edgeSet (ss !! pState.idx p));

            (E',_,_) ←
               if min_pri = 0 then do {
                  WHILE_T (λ(E,brk,_). E = [] ∧ brk = 0) (λ (_, _, ELSE). do {
                     let g = g(gState_I.else := ELSE);
                         E = getChoices g p edges
                     in
                         if E = [] then (
                            if ¬ ELSE then RETURN (E, 0::nat, True)
                            else RETURN (E, 1, False))
                         else RETURN (E, 1, ELSE) }) ([], 0::nat, False)
                } else do {
                  let min_pri = nat_of_integer (abs min_pri);
                  let pri_edges = sort_by_pri min_pri edges;
                  ASSERT (∀es ∈ set pri_edges.
                             set es ⊆ edgeSet (ss !! pState.idx p));
                  let pri_edges = IArray pri_edges;

                  WHILE_T (λ(E,pri,_). E = [] ∧ pri ≤ min_pri) (λ(_, pri, ELSE). do {
                     let es = pri_edges !! pri;
                     let g = g(gState_I.else := ELSE);
                     let E = getChoices g p es;
                     if E = [] then (
                         if ¬ ELSE then RETURN (E,pri,True)
                         else RETURN (E, pri + 1, False))
                     else RETURN (E, pri, ELSE) }) ([], 0, False)
                };
            RETURN (E'@E)
        } else RETURN E
      ) []
 )"

definition
  "while_rel1 =
          measure (λx. if x = [] then 1 else 0)
  <*lex*> measure (λx. if x = 0 then 1 else 0)
  <*lex*> measure (λx. if ¬ x then 1 else 0)"

lemma wf_while_rel1: 
  "wf while_rel1"
unfolding while_rel1_def
by auto

definition
  "while_rel2 mp =
          measure (λx. if x = [] then 1 else 0)
  <*lex*> measure (λx. (mp + 1) - x)
  <*lex*> measure (λx. if ¬ x then 1 else 0)"

lemma wf_while_rel2: 
  "wf (while_rel2 mp)"
unfolding while_rel2_def
by auto

lemma executable_edgeSet:
  assumes "gState_inv prog g"
  and "program_inv prog"
  and "ss = states prog"
  shows "executable ss g
    ≤ SPEC (λcs. ∀(e,p) ∈ set cs.
                    e ∈ edgeSet (ss !! pState.idx p)
                  ∧ pState_inv prog p
                  ∧ cl_inv (g,p))"
  unfolding executable_def
  using assms
  apply (refine_rcg refine_vcg nfoldli_rule[where 
              I="λ_ _ cs. ∀(e,p) ∈ set cs.
                              e ∈ edgeSet (ss !! pState.idx p)
                            ∧ pState_inv prog p
                            ∧ cl_inv (g,p)"])
          apply simp
        apply (rename_tac p l1 l2 σ e p')
        apply (subgoal_tac "pState_inv prog p")
          apply (clarsimp simp add: edgeSet_def pState_inv_def)[]
          apply (rule_tac x="IArray.list_of
                               (IArray.list_of (states prog) ! pState.idx p) ! pc p" in bexI)
            apply simp
          apply (force intro!: nth_mem)
        apply (force simp add: gState_inv_def)
      apply (refine_rcg refine_vcg wf_while_rel1 WHILET_rule[where 
                 I="λ(cs,_,_). ∀(e,p) ∈ set cs.
                                  e ∈ edgeSet (ss !! pState.idx p)
                                ∧ pState_inv prog p
                                ∧ cl_inv (g,p)" 
                 and R=while_rel1])
        apply (vc_solve solve: asm_rl simp add: while_rel1_def)
      apply (frule getChoices_p)
      using  getChoices_sub_edges apply (force simp add: gState_inv_def)
    using sort_by_pri_edges apply fastforce
  apply (rename_tac min_pri pri_edges)
  apply (rule_tac I="λ(cs,_,_). ∀(e,p) ∈ set cs.
                                  e ∈ edgeSet (ss !! pState.idx p)
                                ∧ pState_inv prog p
                                ∧ cl_inv (g,p)" 
              and R="while_rel2 (nat_of_integer (abs min_pri))" 
               in WHILET_rule)
        apply (simp add: wf_while_rel2)
      apply simp
    apply (refine_rcg refine_vcg)
        apply (clarsimp_all split: prod.split simp add: while_rel2_def)
      apply (metis diff_less_mono lessI)
    apply (rename_tac idx' else e p')
    apply (frule getChoices_p)
    apply (frule getChoices_sub_edges) 
    apply (subgoal_tac 
             "sort_by_pri (nat_of_integer ∣min_pri∣) pri_edges ! idx'
                 ∈ set (sort_by_pri (nat_of_integer ∣min_pri∣) pri_edges)")
      apply (auto simp add: assms gState_inv_def)[]
    apply (force simp add: sort_by_pri_length)
  apply (auto simp add: assms)
  done

lemma executable_edgeSet':
  assumes "gState_inv prog g"
  and "program_inv prog"
  shows "executable (states prog) g
  ≤ SPEC (λcs. ∀(e,p) ∈ set cs.
                  e ∈ edgeSet ((states prog) !! pState.idx p)
                ∧ pState_inv prog p
                ∧ cl_inv(g,p))"
using executable_edgeSet[where ss = "states prog"] assms
by simp

schematic_goal executable_refine:
  "RETURN (?ex s g) ≤ executable s g"
unfolding executable_def
by (refine_transfer)

concrete_definition executable_impl for s g uses executable_refine

subsubsection ‹Successor calculation›

function to_I where
  "to_I ( gState.vars = v, channels = ch, timeout = t, procs = p )
     = ( gState.vars = v, channels = ch, timeout = False, procs = p,
          handshake = 0, hsdata = [], exclusive = 0, gState_I.else = False )"
by (metis gState.cases) (metis gState.ext_inject)
termination by lexicographic_order

function "from_I" where
  "from_I ( gState.vars = v, channels = ch, timeout = t, procs = p, … = m )
       = ( gState.vars = v, channels = ch, timeout = t, procs = p )"
by (metis gState.surjective) (metis gState.ext_inject)
termination by lexicographic_order

function reset_I where
  "reset_I ( gState.vars = v, channels = ch, timeout = t, procs = p,
             handshake = hs, hsdata = hsd, exclusive = _, gState_I.else = _ )
        = ( gState.vars = v, channels = ch, timeout = False, procs = p,
             handshake = 0, hsdata = if hs ≠ 0 then hsd else [], exclusive = 0,
             gState_I.else = False )"
by (metis (full_types)  gState_I.surjective unit.exhaust)
   (metis gState.select_convs gState_I.select_convs)
termination by lexicographic_order

lemma gState_inv_to_I:
  "gState_inv prog g = gState_inv prog (to_I g)"
by (cases g, simp add: gState_inv_def cl_inv_def)

lemma gState_inv_from_I:
  "gState_inv prog g = gState_inv prog (from_I g)"
by (cases g, simp add: gState_inv_def cl_inv_def)

lemma gState_inv_reset_I:
  "gState_inv prog g = gState_inv prog (reset_I g)"
by (cases g, simp add: gState_inv_def cl_inv_def)

lemmas gState_inv_I_simps = 
  gState_inv_to_I gState_inv_from_I gState_inv_reset_I

definition removeProcs 
  ― ‹Remove ended processes, if there is no running one with a higher pid.›
where
  "removeProcs ps = foldr (λp (dead,sd,ps,dcs).
           if dead ∧ pc p = 0 then (True, True, ps, pState.channels p @ dcs)
           else (False, sd, p#ps, dcs)) ps (True, False, [], [])"


lemma removeProcs_subset':
  "set (fst (snd (snd (removeProcs ps)))) ⊆ set ps"
unfolding removeProcs_def
apply (subst foldr_conv_foldl)
apply (rule foldl_rule_aux_P[where I="λ(_,_,ps',_) _. set ps' ⊆ set ps"])
    apply simp
  apply (clarsimp split: if_splits)
    apply force
  apply (rename_tac p)
  apply (case_tac "p = x")
    apply (subst set_rev[symmetric])
    apply simp
  apply force
apply force
done

lemma removeProcs_length':
  "length (fst (snd (snd (removeProcs ps)))) ≤ length ps"
unfolding removeProcs_def
apply (subst foldr_conv_foldl)
apply (rule foldl_rule_aux_P[where 
        I="λ(_,_,ps',_) ps''. length ps' + length ps'' ≤ length ps"])
    apply (auto split: if_splits)
done

lemma removeProcs_subset:
  "removeProcs ps = (dead,sd,ps',dcs) ==> set ps' ⊆ set ps"
using removeProcs_subset'
by (metis fst_conv snd_conv)

lemma removeProcs_length:
  "removeProcs ps = (dead,sd,ps',dcs) ==> length ps' ≤ length ps"
using removeProcs_length'
by (metis fst_conv snd_conv)

definition cleanChans :: "integer list ==> channels ==> channels" 
  ― ‹Mark channels of closed processes as invalid.›
where
  "cleanChans dchans cs = snd (foldl (λ(i,cs) c.
       if List.member dchans i then (i + 1, cs@[InvChannel])
       else (i + 1, cs@[c])) (0, []) cs)"

lemma cleanChans_channel_inv:
  assumes "set cs ⊆ Collect channel_inv"
  shows "set (cleanChans dchans cs) ⊆ Collect channel_inv"
using assms
unfolding cleanChans_def
apply (rule_tac foldl_rule_aux)
  apply (force split: if_splits)+
done

lemma cleanChans_length:
  "length (cleanChans dchans cs) = length cs"
unfolding cleanChans_def
by (rule foldl_rule_aux_P[where 
       I="λ(_,cs') cs''. length cs' + length cs'' = length cs"]) 
   (force split: if_splits)+

definition checkDeadProcs :: "'a gState_scheme ==> 'a gState_scheme" where
  "checkDeadProcs g = (
     let (_, soDied, procs, dchans) = removeProcs (procs g) in
     if soDied then
         g( procs := procs, channels := cleanChans dchans (channels g))
     else g)"

lemma checkDeadProcs_gState_progress_rel:
  assumes "gState_inv prog g"
  shows "(g, checkDeadProcs g) ∈ gState_progress_rel prog"
using assms cleanChans_length[where cs="channels g"] 
      cleanChans_channel_inv[where cs="channels g"]
unfolding checkDeadProcs_def
apply (intro gState_progress_relI)
      apply assumption
    apply (clarsimp split: if_splits prod.splits)
    apply (frule removeProcs_length)
    apply (frule removeProcs_subset)
    apply (auto simp add: gState_inv_def cl_inv_def)[]
  apply (clarsimp split: if_splits prod.splits)+
done

lemma gState_progress_rel_exclusive:
  "(g, g') ∈ gState_progress_rel prog
   ==> (g, g'(exclusive := p)) ∈ gState_progress_rel prog"
by (simp add:  gState_progress_rel_def gState_inv_def cl_inv_def)

definition applyEdge 
  :: "program ==> edge ==> pState ==> gState_I ==> gState_I nres"
 where
  "applyEdge prog e p g = do {
    
         let (g',p') = evalEffect (effect e) prog g p;
         ASSERT ((g,g') ∈ gState_progress_rel prog);
         ASSERT (pState_inv prog p');
         ASSERT (cl_inv (g',p'));

         let p'' = (case target e of Index t ==>
                     if t < IArray.length (states prog !! pState.idx p') then p'(pc := t)
                     else abort STR ''Edge target out of bounds'' (λ_. p')
                   | _ ==> abort STR ''Edge target not Index'' (λ_. p'));
         ASSERT (pState_inv prog p'');

         let g'' = g'(procs := list_update (procs g') (pid p'' - 1) p'');
         ASSERT ((g',g'') ∈ gState_progress_rel prog);

         let g''' = (if isAtomic e ∧ handshake g'' = 0
                     then g''( exclusive := pid p'' )
                     else g'');
         ASSERT ((g',g''') ∈ gState_progress_rel prog);
         
         let g_f = (if pc p'' = 0 then checkDeadProcs g''' else g''');
         ASSERT ((g''',g_f) ∈ gState_progress_rel prog);
         RETURN g_f }"

lemma applyEdge_gState_progress_rel:
  assumes "program_inv prog"
  and "gState_inv prog g"
  and "pState_inv prog p"
  and "cl_inv (g,p)"
  and "e ∈ edgeSet (states prog !! pState.idx p)"
  shows "applyEdge prog e p g ≤ SPEC (λg'. (g,g') ∈ gState_progress_rel prog)"
using assms
unfolding applyEdge_def
apply (intro refine_vcg)

apply (force elim: fstE intro!: evalEffect_gState_progress_rel)

apply (force elim: sndE intro!: evalEffect_pState_inv)

apply (drule subst)
apply (rule evalEffect_cl_inv)
apply assumption+

apply (cases "target e")
apply (clarsimp simp add: pState_inv_def)
apply simp

apply (frule gState_progress_rel_gState_invI2)
apply (cases "target e")
  apply (clarsimp split: if_splits)
  apply (intro gState_progress_relI)
    apply assumption
    apply (auto simp add: gState_inv_def cl_inv_def  
                dest!: subsetD[OF set_update_subset_insert])[]
    apply (simp add: cl_inv_def)
    apply simp
  apply (intro gState_progress_relI)
    apply assumption
    apply (auto simp add: gState_inv_def cl_inv_def 
                dest!: subsetD[OF set_update_subset_insert])[]
    apply (simp add: cl_inv_def)
    apply simp
  apply (clarsimp split: if_splits)
  apply (intro gState_progress_relI)
    apply assumption
    apply (auto simp add: gState_inv_def cl_inv_def 
                dest!: subsetD[OF set_update_subset_insert])[]
    apply (simp add: cl_inv_def)
    apply simp

apply (auto split: if_splits intro!: gState_progress_rel_exclusive)[]

apply (force intro!: checkDeadProcs_gState_progress_rel)

apply (blast intro!: gState_progress_rel_trans)
done

schematic_goal applyEdge_refine:
  "RETURN (?ae prog e p g) ≤ applyEdge prog e p g"
unfolding applyEdge_def
by (refine_transfer)

concrete_definition applyEdge_impl for e p g uses applyEdge_refine

definition nexts 
  :: "program ==> gState ==> gState ls nres"
  ― ‹The successor function›
where
  "nexts prog g = (
     let
       f = from_I;
       g = to_I g
     in

        REC (λD g. do {
          E ← executable (states prog) g;
          if E = [] then
            if handshake g ≠ 0 then
              ― ‹HS not possible -- remove current step›
              RETURN (ls.empty())
            else if exclusive g ≠ 0 then
              ― ‹Atomic blocks -- just return current state›
              RETURN (ls.sng (f g))
            else if ¬ timeout g then
              ― ‹Set timeout›
              D (g(timeout := True))
            else
              ― ‹If all else fails: stutter›
              RETURN (ls.sng (f (reset_I g)))
          else
             ― ‹Setting the internal variables (exclusive, handshake, ...) to 0›
             ― ‹is safe -- they are either set by the edges, or not thought›
             ― ‹to be used outside executable.›
             let g = reset_I g in
             nfoldli E (λ_. True) (λ(e,p) G.
                 applyEdge prog e p g 🍋 (λ g'.
                 if handshake g' ≠ 0 ∨ isAtomic e then do {
                    G_R ← D g';
                    if ls.isEmpty G_R ∧ handshake g' = 0 then
                       ― ‹this only happens if the next step is a handshake, which fails›
                       ― ‹hence we stay at the current state›
                       RETURN (ls.ins (f g') G)
                    else
                       RETURN (ls.union G_R G)
                 } else RETURN (ls.ins (f g') G))) (ls.empty())
         }) g
         🍋 (λG. if ls.isEmpty G then RETURN (ls.sng (f g)) else RETURN G)
)"

lemma gState_progress_rel_intros:
  "(to_I g, gI') ∈ gState_progress_rel prog
       ==> (g, from_I gI') ∈ gState_progress_rel prog"
  "(gI, gI') ∈ gState_progress_rel prog
       ==> (gI, reset_I gI') ∈ gState_progress_rel prog"
  "(to_I g, gI') ∈ gState_progress_rel prog
       ==> (to_I g, gI'(timeout := t)) ∈ gState_progress_rel prog"
unfolding gState_progress_rel_def
by (cases g, cases gI', cases gI, force simp add: gState_inv_def cl_inv_def)+

lemma gState_progress_rel_step_intros:
  "(to_I g, g') ∈ gState_progress_rel prog
      ==> (reset_I g', g'') ∈ gState_progress_rel prog
      ==> (g, from_I g'') ∈ gState_progress_rel prog"
  "(to_I g, g') ∈ gState_progress_rel prog
      ==> (reset_I g', g'') ∈ gState_progress_rel prog
      ==> (to_I g, g'') ∈ gState_progress_rel prog"
unfolding gState_progress_rel_def
by (cases g, cases g', cases g'', force simp add: gState_inv_def cl_inv_def)+

lemma cl_inv_reset_I:
  "cl_inv(g,p) ==> cl_inv(reset_I g, p)"
  by (cases g) (simp add: cl_inv_def)

lemmas refine_helpers = 
  gState_progress_rel_intros gState_progress_rel_step_intros cl_inv_reset_I


lemma nexts_SPEC:
  assumes "gState_inv prog g"
  and "program_inv prog"
  shows "nexts prog g ≤ SPEC (λgs. ∀g' ∈ ls.α gs. (g,g') ∈ gState_progress_rel prog)"
  using assms
  unfolding nexts_def
  apply (refine_rcg refine_vcg REC_rule[where 
           pre="λg'. (to_I g,g') ∈ gState_progress_rel prog"])
    apply (simp add: gState_inv_to_I)
  apply (rule order_trans[OF executable_edgeSet'])
      apply (drule gState_progress_rel_gState_invI2)
      apply assumption
    apply assumption
  apply (refine_rcg refine_vcg nfoldli_rule[where 
             I="λ_ _ σ. ∀g' ∈ ls.α σ. (g,g') ∈ gState_progress_rel prog"] 
          order_trans[OF applyEdge_gState_progress_rel])
        apply (vc_solve intro: refine_helpers solve: asm_rl simp add: ls.correct)
  apply (rule order_trans)
    apply (rprems)
    apply (vc_solve intro: refine_helpers solve: asm_rl simp add: ls.correct)
  apply (rule order_trans)
    apply rprems
    apply (vc_solve intro: refine_helpers solve: asm_rl simp add: ls.correct)
  done

lemma RETURN_dRETURN:
  "RETURN f ≤ f' ==> nres_of (dRETURN f) ≤ f'"
unfolding nres_of_def
by simp

lemma executable_dRETURN:
  "nres_of (dRETURN (executable_impl prog g)) ≤ executable prog g"
using executable_impl.refine
by (simp add: RETURN_dRETURN)

lemma applyEdge_dRETURN:
  "nres_of (dRETURN (applyEdge_impl prog e p g)) ≤ applyEdge prog e p g"
using applyEdge_impl.refine
by (simp add: RETURN_dRETURN)

schematic_goal nexts_code_aux:
  "nres_of (?nexts prog g) ≤ nexts prog g"
  unfolding nexts_def 
  by (refine_transfer the_resI executable_dRETURN applyEdge_dRETURN)

concrete_definition nexts_code_aux for prog g uses nexts_code_aux
prepare_code_thms nexts_code_aux_def

subsubsection ‹Handle non-termination›

text ‹
 A Promela model may include non-terminating parts. Therefore we cannot guarantee, that @{const nexts} will actually terminate.
 To avoid having to deal with this in the model checker, we fail in case of non-termination.
 ›

(* TODO: Integrate such a concept into refine_transfer! *)
definition SUCCEED_abort where
  "SUCCEED_abort msg dm m = (
     case m of
       RES X ==> if X={} then Code.abort msg (λ_. dm) else RES X
     | _ ==> m)"


definition dSUCCEED_abort where
  "dSUCCEED_abort msg dm m = (
     case m of
       dSUCCEEDi ==> Code.abort msg (λ_. dm)
     | _ ==> m)"

definition ref_succeed where
  "ref_succeed m m' ⟷ m ≤ m' ∧chapter AFP

lemma dSUCCEED_abort_SUCCEED_abort:
   "[ RETURN dm' ≤ dm; ref_succeed (nres_of m') m ] 
       ==> nres_of (dSUCCEED_abort msg (dRETURN dm') (m')) 
           ≤ SUCCEED_abort msg dm m"
unfolding dSUCCEED_abort_def SUCCEED_abort_def ref_succeed_def
by (auto split: dres.splits nres.splits)

text ‹The final successor function now incorporates:
  \begin{enumerate}
    \item @{const Promela.nexts}
    \item handling of non-termination
  \end{enumerate}›
definition nexts_code where
  "nexts_code prog g = 
     the_res (dSUCCEED_abort (STR ''The Universe is broken!'') 
                             (dRETURN (ls.sng g)) 
                             (nexts_code_aux prog g))"

lemma nexts_code_SPEC:
  assumes "gState_inv prog g"
  and "program_inv prog"
  shows "g' ∈ ls.α (nexts_code prog g) 
         ==> (g,g') ∈ gState_progress_rel prog"
unfolding nexts_code_def
unfolding dSUCCEED_abort_def
using assms
using order_trans[OF nexts_code_aux.refine nexts_SPEC[OF assms(1,2)]]
by (auto split: dres.splits simp: ls.correct)

subsection ‹Finiteness of the state space›

inductive_set reachable_states
  for P :: program
  and g_s :: gState ― ‹start state›
where
"g_s ∈ reachable_states P g_s" |
"g ∈ reachable_states P g_s ==> x ∈ ls.α (nexts_code P g) 
                               ==> x ∈ reachable_states P g_s"

lemmas reachable_states_induct[case_names init step] =
  reachable_states.induct[split_format (complete)]

lemma reachable_states_finite:
  assumes "program_inv prog"
  and "gState_inv prog g"
  shows "finite (reachable_states prog g)"
proof (rule finite_subset[OF _ gStates_finite[of _ g]])
  define INV where "INV g' ⟷ g' ∈ (gState_progress_rel prog)^* `` {g} ∧ gState_inv prog g'" for g'

  {
    fix g'
    have "g' ∈ reachable_states prog g ==> INV g'"
    proof (induct rule: reachable_states_induct)
      case init with assms show ?case by (simp add: INV_def)
    next
      case (step g g')
      from step(2,3) have
        "(g, g') ∈ gState_progress_rel prog"
        using nexts_code_SPEC[OF _ ‹program_inv prog›]
        unfolding INV_def by auto
      thus ?case using step(2) unfolding INV_def by auto
    qed
   }

  thus "reachable_states prog g ⊆ 
        (gState_progress_rel prog)^* `` {g}"
    unfolding INV_def by auto
qed

subsection ‹Traces›

text ‹When trying to generate a lasso, we have a problem: We only have a list of global
states. But what are the transitions to come from one to the other?

This problem shall be tackled by @{term replay}: Given two states, it generates a list of
transitions that was taken.›

(* Give a list of edges that lead from g\<^sub>1 to g\<^sub>2 *)
definition replay :: "program ==> gState ==> gState ==> choices nres" where
  "replay prog g₁ g₂ = (
     let 
       g₁ = to_I g₁;
       check = λg. from_I g = g₂
     in
       REC_T (λD g. do {
       E ← executable (states prog) g;
       if E = [] then 
         if check g then RETURN []
         else if ¬ timeout g then D (g(timeout := True))
         else abort STR ''Stuttering should not occur on replay'' 
                    (λ_. RETURN [])
       else
          let g = reset_I g in
          nfoldli E (λE. E = []) (λ(e,p) _.
             applyEdge prog e p g 🍋 (λg'.
               if handshake g' ≠ 0 ∨ isAtomic e then do {
                 E_R ← D g';
                 if E_R = [] then
                    if check g' then RETURN [(e,p)] else RETURN []
                 else
                    RETURN ((e,p) # E_R)
                } else if check g' then RETURN [(e,p)] else RETURN [])
             ) []
       }) g₁
)"

lemma abort_refine[refine_transfer]:
  "nres_of (f ()) ≤ F () ==> nres_of (abort s f) ≤ abort s F"
  "f() ≠ dSUCCEED ==> abort s f ≠ dSUCCEED"
by auto

schematic_goal replay_code_aux:
  "RETURN (?replay prog g₁ g₂) ≤ replay prog g₁ g₂"
unfolding replay_def applyEdge_def
by (refine_transfer the_resI executable_dRETURN)

concrete_definition replay_code for prog g₁ g₂ uses replay_code_aux
prepare_code_thms replay_code_def

subsubsection ‹Printing of traces›
(* Might go to another theory *)

definition procDescr
  :: "(integer ==> string) ==> program ==> pState ==> string"
where
  "procDescr f prog p = (
     let 
        name = String.explode (proc_names prog !! pState.idx p);
        id = f (integer_of_nat (pid p))
     in
        name @ '' ('' @ id @ '')'')"

definition printInitial
  :: "(integer ==> string) ==> program ==> gState ==> string"
where
  "printInitial f prog g₀ = (
       let psS = printList (procDescr f prog) (procs g₀) [] [] ''  '' in
       ''Initially running: '' @ psS)"

abbreviation "lf ≡ CHR 0x0A"

fun printConfig
  :: "(integer ==> string) ==> program ==> gState option ==> gState ==> string"
where
  "printConfig f prog None g₀ = printInitial f prog g₀"
| "printConfig f prog (Some g₀) g₁ = (
           let eps = replay_code prog g₀ g₁ in
           let print = (λ(e,p). procDescr f prog p @ '': '' @ printEdge f (pc p) e)
           in if eps = [] ∧ g₁ = g₀ then ''    -- stutter --''
              else printList print eps [] [] (lf#''    ''))"

definition "printConfigFromAST f ≡ printConfig f o fst o setUp"

subsection ‹Code export›

code_identifier
  code_module "PromelaInvariants" ⇀ (SML) Promela
| code_module "PromelaDatastructures" ⇀ (SML) Promela

definition "executable_triv prog g = executable_impl (snd prog) g"
definition "apply_triv prog g ep = applyEdge_impl prog (fst ep) (snd ep) (reset_I g)"

export_code
  setUp printProcesses printConfigFromAST nexts_code executable_triv apply_triv
  extractLTLs lookupLTL
  checking SML

export_code
  setUp printProcesses printConfigFromAST nexts_code executable_triv apply_triv
  extractLTLs lookupLTL
  in SML
  file ‹Promela.sml›

end