Theory Outer_Friend_Receiver_State_Indistinguishability

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

subsubsection ‹Unwinding helper definitions and lemmas›

context OuterFriendReceiver
begin

(* The notion of two (apiID × userID) lists being equal except for an occurrence of (AID, UID): *)
fun eqButUIDl :: "(apiID × userID) list ⇒ (apiID × userID) list ⇒ bool" where
"eqButUIDl auidl auidl1 = (remove1 (AID,UID) auidl = remove1 (AID,UID) auidl1)"

lemma eqButUIDl_eq[simp,intro!]: "eqButUIDl auidl auidl"
by auto

lemma eqButUIDl_sym:
assumes "eqButUIDl auidl auidl1"
shows "eqButUIDl auidl1 auidl"
using assms by auto

lemma eqButUIDl_trans:
assumes "eqButUIDl auidl auidl1" and "eqButUIDl auidl1 auidl2"
shows "eqButUIDl auidl auidl2"
using assms by auto

lemma eqButUIDl_remove1_cong:
assumes "eqButUIDl auidl auidl1"
shows "eqButUIDl (remove1 auid auidl) (remove1 auid auidl1)"
using assms by (auto simp: remove1_commute)


lemma eqButUIDl_snoc_cong:
assumes "eqButUIDl auidl auidl1"
and "auid' ∈∈ auidl ⟷ auid' ∈∈ auidl1"
shows "eqButUIDl (auidl ## auid') (auidl1 ## auid')"
using assms by (auto simp: remove1_append remove1_idem)


(* The notion of two functions each taking a userID being equal for observers,
   and eqButUIDs for others. *)
definition eqButUIDf where
"eqButUIDf frds frds1 ≡
  (∀uid. if uid ∈ UIDs AID' then frds uid = frds1 uid else eqButUIDl (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 fastforce

lemma eqButUIDf_cong:
assumes "eqButUIDf frds frds1"
and "uid ∈ UIDs AID' ⟹ uu = uu1"
and "uid ∉ UIDs AID' ⟹ eqButUIDl uu uu1"
shows "eqButUIDf (frds (uid := uu)) (frds1(uid := uu1))"
using assms unfolding eqButUIDf_def by auto
(*
lemma eqButUIDf_eqButUIDl:
assumes "eqButUIDf frds frds1"
shows "eqButUIDl UID2 (frds UID1) (frds1 UID1)"
  and "eqButUIDl UID1 (frds UID2) (frds1 UID2)"
using assms unfolding eqButUIDf_def by (auto split: if_splits)
*)
lemma eqButUIDf_UIDs:
"⟦eqButUIDf frds frds1; uid ∈ UIDs AID'⟧ ⟹ frds uid = frds1 uid"
unfolding eqButUIDf_def by (auto split: if_splits)
(*
lemma eqButUIDf_not_UID':
assumes eq1: "eqButUIDf frds frds1"
and uid: "(uid,uid') ∉ {(UID1,UID2), (UID2,UID1)}"
shows "uid ∈∈ frds uid' ⟷ uid ∈∈ frds1 uid'"
proof -
  from uid have "(uid' = UID1 ∧ uid ≠ UID2)
               ∨ (uid' = UID2 ∧ uid ≠ UID1)
               ∨ (uid' ∉ {UID1,UID2})" (is "?u1 ∨ ?u2 ∨ ?n12")
    by auto
  then show ?thesis proof (elim disjE)
    assume "?u1"
    moreover then have "uid ∈∈ remove1 UID2 (frds uid') ⟷ uid ∈∈ remove1 UID2 (frds1 uid')"
      using eq1 unfolding eqButUIDf_def by auto
    ultimately show ?thesis by auto
  next
    assume "?u2"
    moreover then have "uid ∈∈ remove1 UID1 (frds uid') ⟷ uid ∈∈ remove1 UID1 (frds1 uid')"
      using eq1 unfolding eqButUIDf_def by auto
    ultimately show ?thesis by auto
  next
    assume "?n12"
    then show ?thesis using eq1 unfolding eqButUIDf_def by auto
  qed
qed

(* The notion of two functions each taking two userID arguments being
  equal everywhere but on the values (UID1,UID2) and (UID2,UID1): *)
definition eqButUID12 where
"eqButUID12 freq freq1 ≡
 ∀ uid uid'. if (uid,uid') ∈ {(UID1,UID2), (UID2,UID1)} then True else freq uid uid' = freq1 uid uid'"

lemmas eqButUID12_intro = eqButUID12_def[THEN meta_eq_to_obj_eq, THEN iffD2]

lemma eqButUID12_eeq[simp,intro!]: "eqButUID12 freq freq"
unfolding eqButUID12_def by auto

lemma eqButUID12_sym:
assumes "eqButUID12 freq freq1" shows "eqButUID12 freq1 freq"
using assms unfolding eqButUID12_def
by presburger

lemma eqButUID12_trans:
assumes "eqButUID12 freq freq1" and "eqButUID12 freq1 freq2"
shows "eqButUID12 freq freq2"
using assms unfolding eqButUID12_def by (auto split: if_splits)

lemma eqButUID12_cong:
assumes "eqButUID12 freq freq1"
(*and "uid = UID1 ⟹ eqButUID2 uu uu1"*)
and "¬ (uid,uid') ∈ {(UID1,UID2), (UID2,UID1)} ⟹ uu = uu1"
shows "eqButUID12 (fun_upd2 freq uid uid' uu) (fun_upd2 freq1 uid uid' uu1)"
using assms unfolding eqButUID12_def fun_upd2_def by (auto split: if_splits)

lemma eqButUID12_not_UID:
"⟦eqButUID12 freq freq1; ¬ (uid,uid') ∈ {(UID1,UID2), (UID2,UID1)}⟧ ⟹ freq uid uid' = freq1 uid uid'"
unfolding eqButUID12_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 ∧
 sentOuterFriendIDs s = sentOuterFriendIDs s1 ∧
 eqButUIDf (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"
"sentOuterFriendIDs s = sentOuterFriendIDs s1"
"eqButUIDf (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

lemma eqButUID_UIDs:
"eqButUID s s1 ⟹ uid ∈ UIDs AID' ⟹ recvOuterFriendIDs s uid = recvOuterFriendIDs s1 uid"
unfolding eqButUID_def eqButUIDf_def by auto

lemma eqButUID_recvOuterFriends_UIDs:
assumes "eqButUID s s1"
and "uid ≠ UID ∨ aid ≠ AID"
shows "(aid, uid) ∈∈ recvOuterFriendIDs s uid' ⟷ (aid, uid) ∈∈ recvOuterFriendIDs s1 uid'"
using assms unfolding eqButUID_def eqButUIDf_def
proof -
  have "(aid, uid) ∈∈ remove1 (AID,UID) (recvOuterFriendIDs s uid')
    ⟷ (aid, uid) ∈∈ remove1 (AID,UID) (recvOuterFriendIDs s1 uid')"
    using assms unfolding eqButUID_def eqButUIDf_def by (cases "uid' ∈ UIDs AID'") auto
  then show ?thesis using assms by auto
qed

lemma eqButUID_remove1_UID_recvOuterFriends:
assumes "eqButUID s s1"
shows "remove1 (AID,UID) (recvOuterFriendIDs s uid) = remove1 (AID,UID) (recvOuterFriendIDs s1 uid)"
using assms unfolding eqButUID_def eqButUIDf_def by (cases "uid ∈ UIDs AID'") auto


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 ⟹ uu1 = uu2 ⟹ eqButUID (s ⦇sentOuterFriendIDs := uu1⦈) (s1 ⦇sentOuterFriendIDs := uu2⦈)"
"⋀ uu1 uu2. eqButUID s s1 ⟹ eqButUIDf 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

end

end