Theory Post_Value_Setup_RECEIVER

(* The value setup for paper confidentiality *)
theory Post_Value_Setup_RECEIVER
  imports
    "../Safety_Properties"
    "Post_Observation_Setup_RECEIVER"
    "Post_Unwinding_Helper_RECEIVER"
begin

subsubsection ‹Value setup›

locale Post_RECEIVER = ObservationSetup_RECEIVER
begin

datatype "value" = PValR post ― ‹post content received from the issuer node›


fun φ :: "(state,act,out) trans ⇒ bool" where
"φ (Trans _ (COMact (comReceivePost aid sp pid pst uid vs)) ou _) =
(aid = AID ∧ pid = PID ∧ ou = outOK)"
|
"φ (Trans s _ _ s') = False"

lemma φ_def2:
"φ (Trans s a ou s') ⟷
 (∃uid p pst vs. a = COMact (comReceivePost AID p PID pst uid vs) ∧ ou = outOK)"
by (cases "Trans s a ou s'" rule: φ.cases) auto

lemma comReceivePost_out:
assumes 1: "step s a = (ou,s')" and a: "a = COMact (comReceivePost AID p PID pst uid vs)" and 2: "ou = outOK"
shows "p = serverPass s AID"
using 1 2 unfolding a by (auto simp: com_defs)

lemma φ_def3:
assumes "step s a = (ou,s')"
shows
"φ (Trans s a ou s') ⟷
 (∃uid pst vs. a = COMact (comReceivePost AID (serverPass s AID) PID pst uid vs) ∧ ou = outOK)"
unfolding φ_def2
using comReceivePost_out[OF assms]
by blast

lemma φ_cases:
assumes "φ (Trans s a ou s')"
and "step s a = (ou, s')"
and "reach s"
obtains
  (Recv) uid sp aID pID pst vs where "a = COMact (comReceivePost aID sp pID pst uid vs)" "ou = outOK"
                                 "sp = serverPass s AID"
                                  "aID = AID" "pID = PID"
proof -
  from assms(1) obtain sp pst uid vs where "a = COMact (comReceivePost AID sp PID pst uid vs) ∧ ou = outOK"
    unfolding φ_def2 by auto
  then show thesis proof -
    assume "a = COMact (comReceivePost AID sp PID pst uid vs) ∧ ou = outOK"
    with assms(2) show thesis by (intro Recv) (auto simp: com_defs)
  qed
qed


fun f :: "(state,act,out) trans ⇒ value" where
"f (Trans s (COMact (comReceivePost aid sp pid pst uid vs)) _ s') =
 (if aid = AID ∧ pid = PID then PValR pst else undefined)"
|
"f (Trans s _ _ s') = undefined"


sublocale Receiver_State_Equivalence_Up_To_PID .

lemma eqButPID_step_φ_imp:
assumes ss1: "eqButPID s s1"
and step: "step s a = (ou,s')" and step1: "step s1 a = (ou1,s1')"
and φ: "φ (Trans s a ou s')"
shows "φ (Trans s1 a ou1 s1')"
proof-
  have s's1': "eqButPID s' s1'"
  using eqButPID_step local.step ss1 step1 by blast
  show ?thesis using step step1 φ
  using eqButPID_stateSelectors[OF ss1]
  unfolding φ_def2
  by (auto simp: u_defs com_defs)
qed

lemma eqButPID_step_φ:
assumes s's1': "eqButPID s s1"
and step: "step s a = (ou,s')" and step1: "step s1 a = (ou1,s1')"
shows "φ (Trans s a ou s') = φ (Trans s1 a ou1 s1')"
by (metis eqButPID_step_φ_imp eqButPID_sym assms)


end

end