Theory Outer_Friend_Issuer_State_Indistinguishability

(* The state equivalence used for the unwinding proofs for the friendship confidentiality
   properties *)
theory Outer_Friend_Issuer_State_Indistinguishability
  imports Outer_Friend_Issuer_Observation_Setup
begin

subsubsection ‹Unwinding helper definitions and lemmas›

context OuterFriendIssuer
begin

fun filterUIDs :: "(apiID × userID) list ⇒ (apiID × userID) list" where
"filterUIDs auidl = filter (λauid. (snd auid) ∈ UIDs (fst auid)) auidl"

fun removeUIDs :: "(apiID × userID) list ⇒ (apiID × userID) list" where
"removeUIDs auidl = filter (λauid. (snd auid) ∉ UIDs (fst auid)) auidl"

(* The notion of two (apiID × userID) lists being equal on observers: *)
fun eqButUIDs :: "(apiID × userID) list ⇒ (apiID × userID) list ⇒ bool" where
"eqButUIDs uidl uidl1 = (filterUIDs uidl = filterUIDs uidl1)"

lemma eqButUIDs_eq[simp,intro!]: "eqButUIDs uidl uidl"
by auto

lemma eqButUIDs_sym:
assumes "eqButUIDs uidl uidl1"
shows "eqButUIDs uidl1 uidl"
using assms by auto

lemma eqButUIDs_trans:
assumes "eqButUIDs uidl uidl1" and "eqButUIDs uidl1 uidl2"
shows "eqButUIDs uidl uidl2"
using assms by auto

lemma eqButUIDs_remove1_cong:
assumes "eqButUIDs uidl uidl1"
shows "eqButUIDs (remove1 auid uidl) (remove1 auid uidl1)"
using assms by (auto simp: filter_remove1)

lemma eqButUIDs_snoc_cong:
assumes "eqButUIDs uidl uidl1"
(*and "uid' ∈∈ uidl ⟷ uid' ∈∈ uidl1"*)
shows "eqButUIDs (uidl ## auid') (uidl1 ## auid')"
using assms by auto


(* The notion of two functions each taking a userID being equal everywhere but on UID,
   where they are eqButUIDs. *)
definition eqButUIDf where
"eqButUIDf frds frds1 ≡
  eqButUIDs (frds UID) (frds1 UID)
∧ (∀uid. uid ≠ UID ⟶ frds uid = frds1 uid)"

lemmas eqButUIDf_intro = eqButUIDf_def[THEN meta_eq_to_obj_eq, THEN iffD2]

lemma eqButUIDf_eeq[simp,intro!]: "eqButUIDf frds frds"
unfolding eqButUIDf_def by auto

lemma eqButUIDf_sym:
assumes "eqButUIDf frds frds1" shows "eqButUIDf frds1 frds"
using assms unfolding eqButUIDf_def
by auto

lemma eqButUIDf_trans:
assumes "eqButUIDf frds frds1" and "eqButUIDf frds1 frds2"
shows "eqButUIDf frds frds2"
using assms unfolding eqButUIDf_def by auto

lemma eqButUIDf_cong:
assumes "eqButUIDf frds frds1"
and "uid ≠ UID ⟹ uu = uu1"
and "uid = UID ⟹ eqButUIDs uu uu1"
shows "eqButUIDf (frds (uid := uu)) (frds1(uid := uu1))"
using assms unfolding eqButUIDf_def by auto

lemma eqButUIDf_not_UID:
"⟦eqButUIDf frds frds1; uid ≠ UID⟧ ⟹ frds uid = frds1 uid"
unfolding eqButUIDf_def by (auto split: if_splits)

(* The notion of two states being equal everywhere but on the friendship requests or status of users UID1 and UID2: *)
definition eqButUID :: "state ⇒ state ⇒ bool" where
"eqButUID s s1 ≡
 admin s = admin s1 ∧

 pendingUReqs s = pendingUReqs s1 ∧ userReq s = userReq s1 ∧
 userIDs s = userIDs s1 ∧ user s = user s1 ∧ pass s = pass s1 ∧

 pendingFReqs s = pendingFReqs s1 ∧
 friendReq s = friendReq s1 ∧
 friendIDs s = friendIDs s1 ∧

 postIDs s = postIDs s1 ∧ admin s = admin s1 ∧
 post s = post s1 ∧ vis s = vis s1 ∧
 owner s = owner s1 ∧

 pendingSApiReqs s = pendingSApiReqs s1 ∧ sApiReq s = sApiReq s1 ∧
 serverApiIDs s = serverApiIDs s1 ∧ serverPass s = serverPass s1 ∧
 outerPostIDs s = outerPostIDs s1 ∧ outerPost s = outerPost s1 ∧ outerVis s = outerVis s1 ∧
 outerOwner s = outerOwner s1 ∧
 eqButUIDf (sentOuterFriendIDs s) (sentOuterFriendIDs s1) ∧
 recvOuterFriendIDs s = recvOuterFriendIDs s1 ∧

 pendingCApiReqs s = pendingCApiReqs s1 ∧ cApiReq s = cApiReq s1 ∧
 clientApiIDs s = clientApiIDs s1 ∧ clientPass s = clientPass s1 ∧
 sharedWith s = sharedWith s1"

lemmas eqButUID_intro = eqButUID_def[THEN meta_eq_to_obj_eq, THEN iffD2]

lemma eqButUID_refl[simp,intro!]: "eqButUID s s"
unfolding eqButUID_def by auto

lemma eqButUID_sym[sym]:
assumes "eqButUID s s1" shows "eqButUID s1 s"
using assms eqButUIDf_sym unfolding eqButUID_def by auto

lemma eqButUID_trans[trans]:
assumes "eqButUID s s1" and "eqButUID s1 s2" shows "eqButUID s s2"
using assms eqButUIDf_trans unfolding eqButUID_def by metis

(* Implications from eqButUID, including w.r.t. auxiliary operations: *)
lemma eqButUID_stateSelectors:
assumes "eqButUID s s1"
shows "admin s = admin s1"
"pendingUReqs s = pendingUReqs s1" "userReq s = userReq s1"
"userIDs s = userIDs s1" "user s = user s1" "pass s = pass s1"
"pendingFReqs s = pendingFReqs s1"
"friendReq s = friendReq s1"
"friendIDs s = friendIDs s1"

"postIDs s = postIDs s1"
"post s = post s1" "vis s = vis s1"
"owner s = owner s1"

"pendingSApiReqs s = pendingSApiReqs s1" "sApiReq s = sApiReq s1"
"serverApiIDs s = serverApiIDs s1" "serverPass s = serverPass s1"
"outerPostIDs s = outerPostIDs s1" "outerPost s = outerPost s1" "outerVis s = outerVis s1"
"outerOwner s = outerOwner s1"
"eqButUIDf (sentOuterFriendIDs s) (sentOuterFriendIDs s1)"
"recvOuterFriendIDs s = recvOuterFriendIDs s1"

"pendingCApiReqs s = pendingCApiReqs s1" "cApiReq s = cApiReq s1"
"clientApiIDs s = clientApiIDs s1" "clientPass s = clientPass s1"
"sharedWith s = sharedWith s1"

"IDsOK s = IDsOK s1"
using assms unfolding eqButUID_def IDsOK_def[abs_def] by auto

lemmas eqButUID_eqButUIDf = eqButUID_stateSelectors(22)

lemma eqButUID_eqButUIDs:
"eqButUID s s1 ⟹ eqButUIDs (sentOuterFriendIDs s UID) (sentOuterFriendIDs s1 UID)"
unfolding eqButUID_def eqButUIDf_def by auto

lemma eqButUID_not_UID:
"eqButUID s s1 ⟹ uid ≠ UID ⟹ sentOuterFriendIDs s uid = sentOuterFriendIDs s1 uid"
unfolding eqButUID_def eqButUIDf_def by auto

lemma eqButUID_sentOuterFriends_UIDs:
assumes "eqButUID s s1"
and "uid' ∈ UIDs aid"
shows "(aid, uid') ∈∈ sentOuterFriendIDs s UID ⟷ (aid, uid') ∈∈ sentOuterFriendIDs s1 UID"
proof -
  have "(aid, uid') ∈∈ filterUIDs (sentOuterFriendIDs s UID)
    ⟷ (aid, uid') ∈∈ filterUIDs (sentOuterFriendIDs s1 UID)"
    using assms unfolding eqButUID_def eqButUIDf_def by auto
  then show ?thesis using assms by auto
qed

lemma eqButUID_sentOuterFriendIDs_cong:
assumes "eqButUID s s1"
and "uid' ∉ UIDs aid"
shows "eqButUID (s⦇sentOuterFriendIDs := (sentOuterFriendIDs s)(UID := sentOuterFriendIDs s UID ## (aid, uid'))⦈) s1"
and "eqButUID s (s1⦇sentOuterFriendIDs := (sentOuterFriendIDs s1)(UID := sentOuterFriendIDs s1 UID ## (aid, uid'))⦈)"
and "eqButUID s (s1⦇sentOuterFriendIDs := (sentOuterFriendIDs s1)(UID := remove1 (aid, uid') (sentOuterFriendIDs s1 UID))⦈)"
and "eqButUID (s⦇sentOuterFriendIDs := (sentOuterFriendIDs s)(UID := remove1 (aid, uid') (sentOuterFriendIDs s UID))⦈) s1"
using assms unfolding eqButUID_def eqButUIDf_def by (auto simp: filter_remove1)

lemma eqButUID_cong:
"⋀ uu1 uu2. eqButUID s s1 ⟹ uu1 = uu2 ⟹ eqButUID (s ⦇admin := uu1⦈) (s1 ⦇admin := uu2⦈)"

"⋀ uu1 uu2. eqButUID s s1 ⟹ uu1 = uu2 ⟹ eqButUID (s ⦇pendingUReqs := uu1⦈) (s1 ⦇pendingUReqs := uu2⦈)"
"⋀ uu1 uu2. eqButUID s s1 ⟹ uu1 = uu2 ⟹ eqButUID (s ⦇userReq := uu1⦈) (s1 ⦇userReq := uu2⦈)"
"⋀ uu1 uu2. eqButUID s s1 ⟹ uu1 = uu2 ⟹ eqButUID (s ⦇userIDs := uu1⦈) (s1 ⦇userIDs := uu2⦈)"
"⋀ uu1 uu2. eqButUID s s1 ⟹ uu1 = uu2 ⟹ eqButUID (s ⦇user := uu1⦈) (s1 ⦇user := uu2⦈)"
"⋀ uu1 uu2. eqButUID s s1 ⟹ uu1 = uu2 ⟹ eqButUID (s ⦇pass := uu1⦈) (s1 ⦇pass := uu2⦈)"

"⋀ uu1 uu2. eqButUID s s1 ⟹ uu1 = uu2 ⟹ eqButUID (s ⦇postIDs := uu1⦈) (s1 ⦇postIDs := uu2⦈)"
"⋀ uu1 uu2. eqButUID s s1 ⟹ uu1 = uu2 ⟹ eqButUID (s ⦇owner := uu1⦈) (s1 ⦇owner := uu2⦈)"
"⋀ uu1 uu2. eqButUID s s1 ⟹ uu1 = uu2 ⟹ eqButUID (s ⦇post := uu1⦈) (s1 ⦇post := uu2⦈)"
"⋀ uu1 uu2. eqButUID s s1 ⟹ uu1 = uu2 ⟹ eqButUID (s ⦇vis := uu1⦈) (s1 ⦇vis := uu2⦈)"

"⋀ uu1 uu2. eqButUID s s1 ⟹ uu1 = uu2 ⟹ eqButUID (s ⦇pendingFReqs := uu1⦈) (s1 ⦇pendingFReqs := uu2⦈)"
"⋀ uu1 uu2. eqButUID s s1 ⟹ uu1 = uu2 ⟹ eqButUID (s ⦇friendReq := uu1⦈) (s1 ⦇friendReq := uu2⦈)"
"⋀ uu1 uu2. eqButUID s s1 ⟹ uu1 = uu2 ⟹ eqButUID (s ⦇friendIDs := uu1⦈) (s1 ⦇friendIDs := uu2⦈)"

"⋀ uu1 uu2. eqButUID s s1 ⟹ uu1 = uu2 ⟹ eqButUID (s ⦇pendingSApiReqs := uu1⦈) (s1 ⦇pendingSApiReqs := uu2⦈)"
"⋀ uu1 uu2. eqButUID s s1 ⟹ uu1 = uu2 ⟹ eqButUID (s ⦇sApiReq := uu1⦈) (s1 ⦇sApiReq := uu2⦈)"
"⋀ uu1 uu2. eqButUID s s1 ⟹ uu1 = uu2 ⟹ eqButUID (s ⦇serverApiIDs := uu1⦈) (s1 ⦇serverApiIDs := uu2⦈)"
"⋀ uu1 uu2. eqButUID s s1 ⟹ uu1 = uu2 ⟹ eqButUID (s ⦇serverPass := uu1⦈) (s1 ⦇serverPass := uu2⦈)"
"⋀ uu1 uu2. eqButUID s s1 ⟹ uu1 = uu2 ⟹ eqButUID (s ⦇outerPostIDs := uu1⦈) (s1 ⦇outerPostIDs := uu2⦈)"
"⋀ uu1 uu2. eqButUID s s1 ⟹ uu1 = uu2 ⟹ eqButUID (s ⦇outerPost := uu1⦈) (s1 ⦇outerPost := uu2⦈)"
"⋀ uu1 uu2. eqButUID s s1 ⟹ uu1 = uu2 ⟹ eqButUID (s ⦇outerVis := uu1⦈) (s1 ⦇outerVis := uu2⦈)"
"⋀ uu1 uu2. eqButUID s s1 ⟹ uu1 = uu2 ⟹ eqButUID (s ⦇outerOwner := uu1⦈) (s1 ⦇outerOwner := uu2⦈)"
"⋀ uu1 uu2. eqButUID s s1 ⟹ eqButUIDf uu1 uu2 ⟹ eqButUID (s ⦇sentOuterFriendIDs := uu1⦈) (s1 ⦇sentOuterFriendIDs := uu2⦈)"
"⋀ uu1 uu2. eqButUID s s1 ⟹ uu1 = uu2 ⟹ eqButUID (s ⦇recvOuterFriendIDs := uu1⦈) (s1 ⦇recvOuterFriendIDs := uu2⦈)"

"⋀ uu1 uu2. eqButUID s s1 ⟹ uu1 = uu2 ⟹ eqButUID (s ⦇pendingCApiReqs := uu1⦈) (s1 ⦇pendingCApiReqs := uu2⦈)"
"⋀ uu1 uu2. eqButUID s s1 ⟹ uu1 = uu2 ⟹ eqButUID (s ⦇cApiReq := uu1⦈) (s1 ⦇cApiReq := uu2⦈)"
"⋀ uu1 uu2. eqButUID s s1 ⟹ uu1 = uu2 ⟹ eqButUID (s ⦇clientApiIDs := uu1⦈) (s1 ⦇clientApiIDs := uu2⦈)"
"⋀ uu1 uu2. eqButUID s s1 ⟹ uu1 = uu2 ⟹ eqButUID (s ⦇clientPass := uu1⦈) (s1 ⦇clientPass := uu2⦈)"
"⋀ uu1 uu2. eqButUID s s1 ⟹ uu1 = uu2 ⟹ eqButUID (s ⦇sharedWith := uu1⦈) (s1 ⦇sharedWith:= uu2⦈)"
unfolding eqButUID_def by auto


lemma distinct_remove1_idem: "distinct xs ⟹ remove1 y (remove1 y xs) = remove1 y xs"
by (induction xs) (auto simp add: remove1_idem)

(* major *) lemma eqButUID_step:
assumes ss1: "eqButUID s s1"
and step: "step s a = (ou,s')"
and step1: "step s1 a = (ou1,s1')"
and rs: "reach s"
and rs1: "reach s1"
shows "eqButUID s' s1'"
proof -
  note simps = eqButUID_stateSelectors s_defs c_defs d_defs u_defs r_defs l_defs com_defs
               eqButUID_sentOuterFriends_UIDs eqButUID_not_UID
  from assms show ?thesis proof (cases a)
    case (Sact sa) with assms show ?thesis by (cases sa) (auto simp add: simps intro!: eqButUID_cong)
  next
    case (Cact ca) with assms show ?thesis by (cases ca) (auto simp add: simps intro!: eqButUID_cong)
  next
    case (Uact ua) with assms show ?thesis by (cases ua) (auto simp add: simps intro!: eqButUID_cong)
  next
    case (Ract ra) with assms show ?thesis by (cases ra) (auto simp add: simps intro!: eqButUID_cong)
  next
    case (Lact la) with assms show ?thesis by (cases la) (auto simp add: simps intro!: eqButUID_cong)
  next
    case (COMact ca)
      with assms show ?thesis proof (cases ca)
        case (comSendCreateOFriend uid p aid uid')
          then show ?thesis
            using COMact assms eqButUID_eqButUIDf[OF ss1] eqButUID_eqButUIDs[OF ss1]
            by (cases "uid = UID"; cases "uid' ∈ UIDs aid")
               (auto simp: simps intro!: eqButUID_cong eqButUIDf_cong intro: eqButUID_sentOuterFriendIDs_cong)
      next
        case (comSendDeleteOFriend uid p aid uid')
          then show ?thesis
            using COMact assms eqButUID_eqButUIDf[OF ss1] eqButUID_eqButUIDs[OF ss1]
            by (cases "uid = UID"; cases "uid' ∈ UIDs aid")
               (auto simp: simps filter_remove1 intro!: eqButUID_cong eqButUIDf_cong intro: eqButUID_sentOuterFriendIDs_cong)
      qed (auto simp: simps intro!: eqButUID_cong)
  next
    case (Dact da) with assms show ?thesis by (cases da) (auto simp add: simps intro!: eqButUID_cong)
  qed
qed

end

end