Quelle  SPRViewNonDet.thy

(*<*)
theory SPRViewNonDet
imports
  SPRView
  KBPsAuto
begin
(*>*)

subsection‹Perfect Recall in Non-deterministic Broadcast Environments›

text_raw‹
 begin{figure}[ht]
 begin{isabellebody}%
 ›
record ('a, 'ePubAct, 'es, 'pPubAct, 'ps) BEState =
  es :: "'es"
  ps :: "'a ==> 'ps"
  pubActs :: "'ePubAct × ('a ==> 'pPubAct)"

locale FiniteBroadcastEnvironment =
  Environment jkbp envInit envAction envTrans envVal envObs
    for jkbp :: "('a :: finite, 'p, ('pPubAct :: finite × 'ps :: finite)) JKBP"
    and envInit
         :: "('a, 'ePubAct :: finite, 'es :: finite, 'pPubAct, 'ps) BEState list"
    and envAction :: "('a, 'ePubAct, 'es, 'pPubAct, 'ps) BEState
                   ==> ('ePubAct × 'ePrivAct) list"
    and envTrans :: "('ePubAct × 'ePrivAct)
                  ==> ('a ==> ('pPubAct × 'ps))
                  ==> ('a, 'ePubAct, 'es, 'pPubAct, 'ps) BEState
                  ==> ('a, 'ePubAct, 'es, 'pPubAct, 'ps) BEState"
    and envVal :: "('a, 'ePubAct, 'es, 'pPubAct, 'ps) BEState ==> 'p ==> bool"
    and envObs :: "'a ==> ('a, 'ePubAct, 'es, 'pPubAct, 'ps) BEState
                ==> ('cobs × 'ps × ('ePubAct × ('a ==> 'pPubAct)))"

+ fixes envObsC :: "'es ==> 'cobs"
    and envActionES :: "'es ==> ('ePubAct × ('a ==> 'pPubAct))
                            ==> ('ePubAct × 'ePrivAct) list"
    and envTransES :: "('ePubAct × 'ePrivAct) ==> ('a ==> 'pPubAct)
                    ==> 'es ==> 'es"
  defines envObs_def: "envObs a ≡ (λs. (envObsC (es s), ps s a, pubActs s))"
      and envAction_def: "envAction s ≡ envActionES (es s) (pubActs s)"
      and envTrans_def:
           "envTrans eact aact s ≡ ( es = envTransES eact (fst ∘ aact) (es s)
                                    , ps = snd ∘ aact
                                    , pubActs = (fst eact, fst ∘ aact) )"
text_raw‹
 \end{isabellebody}%
 \caption{Finite broadcast environments with non-deterministic KBPs.}
 \label{fig:kbps-theory-broadcast-envs}
 end{figure}
 ›

(*<*)
instance BEState_ext :: (finite, finite, finite, finite, finite, finite) finite
proof
 let ?U = "UNIV :: ('a, 'b, 'c, 'd, 'e, 'f) BEState_ext set"
 { fix x :: "('a, 'b, 'c, 'd, 'e, 'f) BEState_scheme"
   have "∃a b c d. x = BEState_ext a b c d"
     by (cases x) simp
 } then have U:
   "?U = (λ(((a, b), c), d). BEState_ext a b c d) ` (((UNIV × UNIV) × UNIV) × UNIV)"
     by (auto simp add: image_def)
 show "finite ?U" by (simp add: U)
qed

(*>*)
text‹

 label{sec:kbps-theory-spr-non-deterministic-protocols}

  completeness we reproduce the results of 🍋‹"Ron:1996"›
  non-deterministic KBPs in broadcast environments.

  determinism requirement is replaced by the constraint that actions
  split into public and private components, where the private part
  the agents' private states, and the public part is
  and recorded in the system state. Moreover the protocol of
  environment is only a function of the environment state, and not
  agents' private states. Once again an agent's view consists of the
  observation and their private state. The situation is described
  the locale in Figure~\ref{fig:kbps-theory-broadcast-envs}. Note
  as we do not intend to generate code for this case, we adopt more
  but less effective representations.

  goal in the following is to instantiate the @{term
 SimIncrEnvironment"} locale with respect to the assumptions made in
  @{term "FiniteBroadcastEnvironment"} locale. We begin by defining
  simulation machinery to the previous section.

 ›

context FiniteBroadcastEnvironment
begin

text‹

  for the deterministic variant, we abstract traces using the common
 . Note that this now includes the public part of the
 ' actions.

 ›

definition
  tObsC :: "('a, 'ePubAct, 'es, 'pPubAct, 'ps) BEState Trace
         ==> ('cobs × 'ePubAct × ('a ==> 'pPubAct)) Trace"
where
  "tObsC ≡ tMap (λs. (envObsC (es s), pubActs s))"
(*<*)

lemma spr_jview_tObsC:
  assumes "spr_jview a t = spr_jview a t'"
  shows "tObsC t = tObsC t'"
  using SPR.sync[rule_format, OF assms] assms
  by (induct rule: trace_induct2) (auto simp: envObs_def tObsC_def)

lemma tObsC_tLength:
  "tObsC t = tObsC t' ==> tLength t = tLength t'"
  unfolding tObsC_def by (rule tMap_eq_imp_tLength_eq)

lemma tObsC_tStep_eq_inv:
  "tObsC t' = tObsC (t ↝ s) ==> ∃t'' s'. t' = t'' ↝ s'"
  unfolding tObsC_def by auto

lemma tObsC_prefix_closed[dest]:
  "tObsC (t ↝ s) = tObsC (t' ↝ s') ==> tObsC t = tObsC t'"
  unfolding tObsC_def by simp

lemma tObsC_tLast[iff]:
  "tLast (tObsC t) = (envObsC (es (tLast t)), pubActs (tLast t))"
  unfolding tObsC_def by simp

lemma tObsC_tStep:
  "tObsC (t ↝ s) = tObsC t ↝ (envObsC (es s), pubActs s)"
  unfolding tObsC_def by simp

lemma tObsC_initial[iff]:
  "tFirst (tObsC t) = (envObsC (es (tFirst t)), pubActs (tFirst t))"
  "tObsC (tInit s) = tInit (envObsC (es s), pubActs s)"
  "tObsC t = tInit cobs ⟷ (∃s. t = tInit s ∧ envObsC (es s) = fst cobs ∧ pubActs s = snd cobs)"
  unfolding tObsC_def by auto

lemma spr_tObsC_trc_aux:
  assumes "(t, t') ∈ (∪a. relations SPR.MC a)^*"
  shows "tObsC t = tObsC t'"
  using assms
  apply (induct)
   apply simp
  apply clarsimp
  apply (rule_tac a=x in spr_jview_tObsC)
  apply simp
  done

(*>*)
text‹

  we introduce common and agent-specific abstraction functions:

 ›

definition
  tObsC_abs :: "('a, 'ePubAct, 'es, 'pPubAct, 'ps) BEState Trace
             ==> ('a, 'ePubAct, 'es, 'pPubAct, 'ps) BEState Relation"
where
  "tObsC_abs t ≡ { (tFirst t', tLast t')
                   |t'. t' ∈ SPR.jkbpC ∧ tObsC t' = tObsC t }"

definition
  agent_abs :: "'a ==> ('a, 'ePubAct, 'es, 'pPubAct, 'ps) BEState Trace
             ==> ('a, 'ePubAct, 'es, 'pPubAct, 'ps) BEState Relation"
where
  "agent_abs a t ≡ { (tFirst t', tLast t')
                     |t'. t' ∈ SPR.jkbpC ∧ spr_jview a t' = spr_jview a t }"
(*<*)

lemma tObsC_abs_jview_eq[dest, intro]:
  "spr_jview a t' = spr_jview a t
    ==> tObsC_abs t = tObsC_abs t'"
  unfolding tObsC_abs_def by (fastforce dest: spr_jview_tObsC)

lemma tObsC_absI[intro]:
  "[ t' ∈ SPR.jkbpC; tObsC t' = tObsC t; u = tFirst t'; v = tLast t' ]
    ==> (u, v) ∈ tObsC_abs t"
  unfolding tObsC_abs_def by blast

lemma tObsC_abs_conv:
  "(u, v) ∈ tObsC_abs t
    ⟷ (∃t'. t' ∈ SPR.jkbpC ∧ tObsC t' = tObsC t ∧ u = tFirst t' ∧ v = tLast t')"
  unfolding tObsC_abs_def by blast

lemma agent_absI[elim]:
  "[ t' ∈ SPR.jkbpC; spr_jview a t' = spr_jview a t; u = tFirst t'; v = tLast t' ]
    ==> (u, v) ∈ agent_abs a t"
  unfolding agent_abs_def by blast

lemma agent_abs_tLastD[simp]:
  "(u, v) ∈ agent_abs a t ==> envObs a v = envObs a (tLast t)"
  unfolding agent_abs_def by auto

lemma agent_abs_inv[dest]:
  "(u, v) ∈ agent_abs a t
    ==> ∃t'. t' ∈ SPR.jkbpC ∧ spr_jview a t' = spr_jview a t
           ∧ u = tFirst t' ∧ v = tLast t'"
  unfolding agent_abs_def by blast

(*>*)

end (* context FiniteBroadcastEnvironment *)

text‹

  simulation is identical to that in the previous section:

 ›

record ('a, 'ePubAct, 'es, 'pPubAct, 'ps) SPRstate =
  sprFst :: "('a, 'ePubAct, 'es, 'pPubAct, 'ps) BEState"
  sprLst :: "('a, 'ePubAct, 'es, 'pPubAct, 'ps) BEState"
  sprCRel :: "('a, 'ePubAct, 'es, 'pPubAct, 'ps) BEState Relation"

context FiniteBroadcastEnvironment
begin

definition
  spr_sim :: "('a, 'ePubAct, 'es, 'pPubAct, 'ps) BEState Trace
           ==> ('a, 'ePubAct, 'es, 'pPubAct, 'ps) SPRstate"
where
  "spr_sim ≡ λt. ( sprFst = tFirst t, sprLst = tLast t, sprCRel = tObsC_abs t )"
(*<*)

lemma spr_sim_tFirst_tLast:
  "[ spr_sim t = s; t ∈ SPR.jkbpC ] ==> (sprFst s, sprLst s) ∈ sprCRel s"
  unfolding spr_sim_def by auto

(*>*)
text‹

  Kripke structure over simulated traces is also the same:

 ›

definition
  spr_simRels :: "'a ==> ('a, 'ePubAct, 'es, 'pPubAct, 'ps) SPRstate Relation"
where
  "spr_simRels ≡ λa. { (s, s') |s s'.
                         envObs a (sprFst s) = envObs a (sprFst s')
                       ∧ envObs a (sprLst s) = envObs a (sprLst s')
                       ∧ sprCRel s = sprCRel s' }"

definition
  spr_simVal :: "('a, 'ePubAct, 'es, 'pPubAct, 'ps) SPRstate ==> 'p ==> bool"
where
  "spr_simVal ≡ envVal ∘ sprLst"

abbreviation
  "spr_simMC ≡ mkKripke (spr_sim ` SPR.jkbpC) spr_simRels spr_simVal"
(*<*)

lemma spr_simVal_def2[iff]:
  "spr_simVal (spr_sim t) = envVal (tLast t)"
  unfolding spr_sim_def spr_simVal_def by simp


(*>*)
text‹

  usual, showing that @{term "spr_sim"} is in fact a simulation is
  for all properties except for reverse simulation. For that we
  proof techniques similar to those of
 🍋‹"DBLP:journals/tocl/LomuscioMR00"›: the goal is to show that,
  @{term "t ∈ jkbpC"}, we can construct a trace @{term "t' ∈
 "} indistinguishable from @{term "t"} by agent @{term "a"}, based
  the public actions, the common observation and @{term "a"}'s
  and initial states.

  do this we define a splicing operation:

 ›

definition
  sSplice :: "'a
           ==> ('a, 'ePubAct, 'es, 'pPubAct, 'ps) BEState
           ==> ('a, 'ePubAct, 'es, 'pPubAct, 'ps) BEState
           ==> ('a, 'ePubAct, 'es, 'pPubAct, 'ps) BEState"
where
  "sSplice a s s' ≡ s( ps := (ps s)(a := ps s' a) )"
(*<*)

lemma sSplice_es[simp]:
  "es (sSplice a s s') = es s"
  unfolding sSplice_def by simp

lemma sSplice_pubActs[simp]:
  "pubActs (sSplice a s s') = pubActs s"
  unfolding sSplice_def by simp

lemma sSplice_envObs[simp]:
  assumes init: "envObs a s = envObs a s'"
  shows "sSplice a s s' = s"
proof -
  from init have "ps s a = ps s' a"
    by (auto simp: envObs_def)
  thus ?thesis
    unfolding sSplice_def by (simp add: fun_upd_idem_iff)
qed

lemma sSplice_envObs_a:
  assumes "envObsC (es s) = envObsC (es s')"
  assumes "pubActs s = pubActs s'"
  shows "envObs a (sSplice a s s') = envObs a s'"
  using assms
  unfolding sSplice_def envObs_def by simp

lemma sSplice_envObs_not_a:
  assumes "a' ≠ a"
  shows "envObs a' (sSplice a s s') = envObs a' s"
  using assms
  unfolding sSplice_def envObs_def by simp

(*>*)
text‹

  effect of @{term "sSplice a s s'"} is to update @{term "s"} with
 {term "a"}'s private state in @{term "s'"}. The key properties are
  provided the common observation on @{term "s"} and @{term "s'"}
  the same, then agent @{term "a"}'s observation on @{term "sSplice
  s s'"} is the same as
 at @{term "s'"}, while everyone else's is the
  as at @{term "s"}.

  hoist this operation pointwise to traces:

 ›

abbreviation
  tSplice :: "('a, 'ePubAct, 'es, 'pPubAct, 'ps) BEState Trace
            ==> 'a
            ==> ('a, 'ePubAct, 'es, 'pPubAct, 'ps) BEState Trace
            ==> ('a, 'ePubAct, 'es, 'pPubAct, 'ps) BEState Trace"
      (‹_ ⋈ _› [55, 1000, 56] 55)
where
  "t _{<^esub>⋈ t' ≡ tZip (sSplice a) t t'"}
(*<*)

declare sSplice_envObs_a[simp] sSplice_envObs_not_a[simp]

lemma tSplice_tObsC:
  assumes tObsC: "tObsC t = tObsC t'"
  shows "tObsC (t _{<^esub>⋈ t') = tObsC t"}
  using tObsC_tLength[OF tObsC] tObsC
  by (induct rule: trace_induct2) (simp_all add: tObsC_tStep)

lemma tSplice_spr_jview_a:
  assumes tObsC: "tObsC t = tObsC t'"
  shows "spr_jview a (t _{<^esub>⋈ t') = spr_jview a t'"}
  using tObsC_tLength[OF tObsC] tObsC
  by (induct rule: trace_induct2) (simp_all add: tObsC_tStep spr_jview_def)

lemma tSplice_spr_jview_not_a:
  assumes tObsC: "tObsC t = tObsC t'"
  assumes aa': "a ≠ a'"
  shows "spr_jview a' (t _{<^esub>⋈ t') = spr_jview a' t"}
  using tObsC_tLength[OF tObsC] tObsC aa'
  by (induct rule: trace_induct2) (simp_all add: tObsC_tStep spr_jview_def)

lemma tSplice_es:
  assumes tLen: "tLength t = tLength t'"
  shows "es (tLast (t _{<^esub>⋈ t')) = es (tLast t)"}
  using tLen by (induct rule: trace_induct2) simp_all

lemma tSplice_pubActs:
  assumes tLen: "tLength t = tLength t'"
  shows "pubActs (tLast (t _{<^esub>⋈ t')) = pubActs (tLast t)"}
  using tLen by (induct rule: trace_induct2) simp_all

lemma tSplice_envAction:
  assumes tLen: "tLength t = tLength t'"
  shows "envAction (tLast (t _{<^esub>⋈ t')) = envAction (tLast t)"}
  unfolding envAction_def
  using tSplice_es[OF tLen] tSplice_pubActs[OF tLen]
  by simp

lemma tSplice_tFirst[simp]:
  assumes tLen: "tLength t = tLength t'"
  assumes init: "envObs a (tFirst t) = envObs a (tFirst t')"
  shows "tFirst (t _{<^esub>⋈ t') = tFirst t"}
  using tLen init by (induct rule: trace_induct2) simp_all

lemma tSplice_tLast[simp]:
  assumes tLen: "tLength t = tLength t'"
  assumes last: "envObs a (tLast t) = envObs a (tLast t')"
  shows "tLast (t _{<^esub>⋈ t') = tLast t"}
  using tLen last
  unfolding envObs_def
  apply (induct rule: trace_induct2)
  apply (auto iff: sSplice_def fun_upd_idem_iff)
  done

(*>*)
text‹

  key properties are that after splicing, if @{term "t"} and @{term
 t'"} have the same common observation, then so does @{term "t ⋈
 '"}, and for all agents @{term "a' ≠ a"}, the view @{term "a'"} has
  @{term "t ⋈ t'"} is the same as it has of @{term "t"}, while for
 {term "a"} it is the same as @{term "t'"}.

  can conclude that provided the two traces are initially
  to @{term "a"}, and not commonly distinguishable,
  @{term "t ⋈ t'"} is a canonical trace:

 ›

lemma tSplice_jkbpC:
  assumes tt': "{t, t'} ⊆ SPR.jkbpC"
  assumes init: "envObs a (tFirst t) = envObs a (tFirst t')"
  assumes tObsC: "tObsC t = tObsC t'"
  shows "t _{<^esub>⋈ t' ∈ SPR.jkbpC"}
(*<*)
using tObsC_tLength[OF tObsC] tt' init tObsC
proof(induct rule: trace_induct2)
  case (tInit s s') thus ?case by simp
next
  case (tStep s s' t t')

  hence tt': "t _{<^esub>⋈ t' ∈ SPR.jkbpC"}
    and tLen: "tLength t' = tLength t"
    and tObsC: "tObsC (t ↝ s) = tObsC (t' ↝ s')"
    by auto

  hence tt'n: "t _{<^esub>⋈ t' ∈ SPR.jkbpCn (tLength t)"}
    by auto

  from tStep
  have ts: "t ↝ s ∈ SPR.jkbpCn (Suc (tLength t))"
   and t's': "t' ↝ s' ∈ SPR.jkbpCn (Suc (tLength t'))"
    apply -
     apply ((rule SPR.jkbpC_tLength_inv, simp_all)[1])+
    done

  from ts obtain eact aact
    where eact: "eact ∈ set (envAction (tLast t))"
      and aact: "∀a. aact a ∈ set (jAction (SPR.mkM (SPR.jkbpCn (tLength t))) t a)"
      and trans: "envTrans eact aact (tLast t) = s"
    apply (auto iff: Let_def)
    done

  from t's' obtain eact' aact'
    where eact': "eact' ∈ set (envAction (tLast t'))"
      and aact': "∀a. aact' a ∈ set (jAction (SPR.mkM (SPR.jkbpCn (tLength t'))) t' a)"
      and trans': "envTrans eact' aact' (tLast t') = s'"
    apply (auto iff: Let_def)
    done

  define aact'' where "aact'' = aact (a := aact' a)"

  from tObsC trans trans'
  have aact''_fst: "fst ∘ aact'' = fst ∘ aact"
    unfolding envTrans_def aact''_def
    apply -
    apply (rule ext)
    apply (auto iff: tObsC_tStep)
    apply (erule o_eq_elim)
    apply simp
    done

  from tObsC trans trans'
  have aact''_snd: "snd ∘ aact'' = (snd ∘ aact)(a := ps s' a)"
    unfolding envTrans_def aact''_def
    apply -
    apply (rule ext)
    apply auto
    done

  have "envTrans eact aact'' (tLast (t _{<^esub>⋈ t'))}
      = sSplice a (envTrans eact aact (tLast t)) s'"
    apply (simp only: envTrans_def sSplice_def)
    using tSplice_es[OF tLen[symmetric]] aact''_fst aact''_snd
    apply clarsimp
    done

  moreover

  { fix a'
    have "aact'' a' ∈ set (jAction (SPR.mkM (SPR.jkbpCn (tLength t))) (t _{<^esub>⋈ t') a')"}
    proof(cases "a' = a")
      case False
      with tStep have "jAction (SPR.mkM (SPR.jkbpCn (tLength t))) (t _{<^esub>⋈ t') a'}
                     = jAction (SPR.mkM (SPR.jkbpCn (tLength t))) t a'"
        apply -
        apply (rule S5n_jAction_eq)
         apply simp
        unfolding SPR.mkM_def
        using tSplice_spr_jview_not_a tt'
        apply auto
        done
      with False aact show ?thesis
        unfolding aact''_def by simp
    next
      case True
      with tStep have "jAction (SPR.mkM (SPR.jkbpCn (tLength t))) (t _{<^esub>⋈ t') a}
                     = jAction (SPR.mkM (SPR.jkbpCn (tLength t))) t' a"
        apply -
        apply (rule S5n_jAction_eq)
         apply simp
        unfolding SPR.mkM_def
        using tSplice_spr_jview_a tt'
        apply auto
        done
      with True aact' tLen show ?thesis
        unfolding aact''_def by simp
    qed }

  moreover

  from tStep have "envAction (tLast (t _{<^esub>⋈ t')) = envAction (tLast t)"}
    using tSplice_envAction by blast

  moreover note eact trans tt'n

  ultimately have "(t _{<^esub>⋈ t') ↝ sSplice a s s' ∈ SPR.jkbpCn (Suc (tLength t))"}
    apply (simp add: Let_def del: split_paired_Ex)
    apply (rule exI[where x="eact"])
    apply (rule exI[where x="aact''"])
    apply simp
    done

  thus ?case
    apply (simp only: tZip.simps)
    apply blast
    done
qed

lemma spr_sim_r:
  "sim_r SPR.MC spr_simMC spr_sim"
proof(rule sim_rI)
  fix a p q'
  assume pT: "p ∈ worlds SPR.MC"
     and fpq': "(spr_sim p, q') ∈ relations spr_simMC a"
  from fpq' obtain uq fq vq
    where q': "q' = ( sprFst = uq, sprLst = vq, sprCRel = tObsC_abs p )"
      and uq: "envObs a (tFirst p) = envObs a uq"
      and vq: "envObs a (tLast p) = envObs a vq"
    unfolding mkKripke_def spr_sim_def spr_simRels_def
    by fastforce

  from fpq' have "q' ∈ worlds spr_simMC" by simp
  with q' have "(uq, vq) ∈ tObsC_abs p"
    using spr_sim_tFirst_tLast[where s=q']
    apply auto
    done

  then obtain t
    where tT: "t ∈ SPR.jkbpC"
      and tp: "tObsC t = tObsC p"
      and tuq: "tFirst t = uq"
      and tvq: "tLast t = vq"
    by (auto iff: tObsC_abs_conv)

  define q where "q = t _{<^esub>⋈ p"}

  from tp tuq uq
  have "spr_jview a p = spr_jview a q"
    unfolding q_def by (simp add: tSplice_spr_jview_a)

  with pT tT tp tuq uq
  have pt: "(p, q) ∈ relations SPR.MC a"
    unfolding SPR.mkM_def q_def by (simp add: tSplice_jkbpC)
  from q' uq vq tp tuq tvq
  have ftq': "spr_sim q = q'"
    unfolding spr_sim_def q_def
    using tSplice_tObsC[where a=a and t=t and t'=p]
    apply clarsimp
    apply (intro conjI)
      apply (auto dest: tObsC_tLength)[2]
    unfolding tObsC_abs_def (* FIXME abstract *)
    apply simp
    done
  from pt ftq'
  show "∃q. (p, q) ∈ relations SPR.MC a ∧ spr_sim q = q'"
    by blast
qed

(*>*)
text‹

  proof is by induction over @{term "t"} and @{term "t'"}, and
  crucially on the public actions being recorded in the state
  commonly observed. Showing the reverse simulation property is then
 .

 ›

lemma spr_sim: "sim SPR.MC spr_simMC spr_sim"
(*<*)
proof
  show "sim_range SPR.MC spr_simMC spr_sim"
    by (rule sim_rangeI) (simp_all add: spr_sim_def)
next
  show "sim_val SPR.MC spr_simMC spr_sim"
    by (rule sim_valI) simp
next
  show "sim_f SPR.MC spr_simMC spr_sim"
    unfolding spr_simRels_def spr_sim_def mkKripke_def SPR.mkM_def
    by (rule sim_fI, auto simp del: split_paired_Ex)
next
  show "sim_r SPR.MC spr_simMC spr_sim"
    by (rule spr_sim_r)
qed

(*>*)
end (* context FiniteBroadcastEnvironment *)

sublocale FiniteBroadcastEnvironment
        < SPR: SimIncrEnvironment jkbp envInit envAction envTrans envVal
                                       spr_jview envObs spr_jviewInit spr_jviewIncr
                                       spr_sim spr_simRels spr_simVal
(*<*)
  by standard (simp add: spr_sim)

(*>*)
text‹

  algorithmic representations and machinery of the deterministic
  case suffice for this one too, and so we omit the details.

 FloatBarrier

 ›
(*<*)

end
(*>*)