Theory Post_Value_Setup_ISSUER

(* The value setup for post confidentiality *)
theory Post_Value_Setup_ISSUER
  imports
    "../Safety_Properties"
    "Post_Observation_Setup_ISSUER"
    "Post_Unwinding_Helper_ISSUER"
begin

locale Post_ISSUER = ObservationSetup_ISSUER
begin

subsubsection ‹Value setup›


datatype "value" =
  isPVal: PVal post ― ‹updating the post content locally›
| isPValS: PValS (PValS_tgtAPI: apiID) post ― ‹sending the post to another node›

lemma filter_isPValS_Nil: "filter isPValS vl = [] ⟷ list_all isPVal vl"
proof(induct vl)
  case (Cons v vl)
  thus ?case by (cases v) auto
qed auto

fun φ :: "(state,act,out) trans ⇒ bool" where
"φ (Trans _ (Uact (uPost uid p pid pst)) ou _) = (pid = PID ∧ ou = outOK)"
|
"φ (Trans _ (COMact (comSendPost uid p aid pid)) ou _) = (pid = PID ∧ ou ≠ outErr)"
(* Added during strengthening: saying ≠ outErr is simpler than actually describing the output, which essentially
   takes some parameters from the post and some values from the state. *)
|
"φ (Trans s _ _ s') = False"

lemma φ_def2:
shows
"φ (Trans s a ou s') ⟷
 (∃uid p pst. a = Uact (uPost uid p PID pst) ∧ ou = outOK) ∨
 (∃uid p aid. a = COMact (comSendPost uid p aid PID) ∧ ou ≠ outErr)"
by (cases "Trans s a ou s'" rule: φ.cases) auto

lemma uPost_out:
assumes 1: "step s a = (ou,s')" and a: "a = Uact (uPost uid p PID pst)" and 2: "ou = outOK"
shows "uid = owner s PID ∧ p = pass s uid"
using 1 2 unfolding a by (auto simp: u_defs)

lemma comSendPost_out:
assumes 1: "step s a = (ou,s')" and a: "a = COMact (comSendPost uid p aid PID)" and 2: "ou ≠ outErr"
shows "ou = O_sendPost (aid, clientPass s aid, PID, post s PID, owner s PID, vis s PID)
       ∧ uid = admin s ∧ p = pass s (admin s)"
using 1 2 unfolding a by (auto simp: com_defs)

lemma φ_def3:
assumes "step s a = (ou,s')"
shows
"φ (Trans s a ou s') ⟷
 (∃pst. a = Uact (uPost (owner s PID) (pass s (owner s PID)) PID pst) ∧ ou = outOK) ∨
 (∃aid. a = COMact (comSendPost (admin s) (pass s (admin s)) aid PID) ∧
        ou = O_sendPost (aid, clientPass s aid, PID, post s PID, owner s PID, vis s PID))"
unfolding φ_def2(* [OF assms] *)
using comSendPost_out[OF assms] uPost_out[OF assms]
by blast

lemma φ_cases:
assumes "φ (Trans s a ou s')"
and "step s a = (ou, s')"
and "reach s"
obtains
  (UpdateT) uid p pID pst where "a = Uact (uPost uid p PID pst)" "ou = outOK" "p = pass s uid"
                                  "uid = owner s PID"
| (Send) uid p aid where "a = COMact (comSendPost uid p aid PID)" "ou ≠ outErr" "p = pass s uid"
                                  "uid = admin s"
proof -
  from assms(1) obtain uid p pst aid where "(a = Uact (uPost uid p PID pst) ∧ ou = outOK) ∨
                                          (a = COMact (comSendPost uid p aid PID) ∧ ou ≠ outErr)"
    unfolding φ_def2(* [OF assms(2)] *) by auto
  then show thesis proof(elim disjE)
    assume "a = Uact (uPost uid p PID pst) ∧ ou = outOK"
    with assms(2) show thesis by (intro UpdateT) (auto simp: u_defs)
  next
    assume "a = COMact (comSendPost uid p aid PID) ∧ ou ≠ outErr"
    with assms(2) show thesis by (intro Send) (auto simp: com_defs)
  qed
qed


fun f :: "(state,act,out) trans ⇒ value" where
"f (Trans s (Uact (uPost uid p pid pst)) _ s') =
 (if pid = PID then PVal pst else undefined)"
|
"f (Trans s (COMact (comSendPost uid p aid pid)) (O_sendPost (_, _, _, pst, _, _)) s') =
 (if pid = PID then PValS aid pst else undefined)"
|
"f (Trans s _ _ s') = undefined"

sublocale Issuer_State_Equivalence_Up_To_PID .

lemma Uact_uPaperC_step_eqButPID:
assumes a: "a = Uact (uPost uid p PID pst)"
and "step s a = (ou,s')"
shows "eqButPID s s'"
using assms unfolding eqButPID_def eeqButPID_def eeqButPID_F_def
by (auto simp: u_defs split: if_splits)


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(* [OF step] φ_def2[OF step1]  *)
  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