Possible optimsation in the definition of auth difference

[DMRobertson]

Link to problem area:

https://spec.matrix.org/unstable/rooms/v10/#definitions

Auth difference. The auth difference is calculated by first calculating the full auth chain for each state $S_i$, that is the union of the auth chains for each event in $S_i$, and then taking every event that doesn’t appear in every auth chain. If $C_i$ is the full auth chain of $S_i$, then the auth difference is  $\bigcup_i C_i − \bigcap_i C_i$.

Issue

As written, this requires fetching and inspecting the auth chains for all events in each state map $S_i$
That is, we must process the set of events $\bigcup_i S_i$.

I claim that we only need to fetch and inspect the auth chains of events in the conflicted state set $S_\text{conflicted} = \bigcup_i S_i - \bigcap_i S_i$.

Proof.

$$\begin{align*}
\DeclareMathOperator\fullauthchain{FullAuthChain}
\DeclareMathOperator\authchain{AuthChain}
\text{auth difference as written} &= \bigcup_i C_i − \bigcap_i C_i \
&= \bigcup_i \fullauthchain(S_i) − \bigcap_i \fullauthchain(S_i) \
&= \bigcup_i \left(\bigcup_{e \in S_i} \authchain(e) \right) − \bigcap_i \left(\bigcup_{e \in S_i} \authchain(e) \right)  \
&= \bigcup_{e \in \bigcup_i S_i} \authchain(e) − \bigcap_i \left(\bigcup_{e \in S_i} \authchain(e) \right)
\end{align*}$$

Suppose that $f \in S_\text{unconflicted} = \bigcap_i S_i$ is an event in the unconflicted state map.
Then:

• $\authchain(f)$ is contained in the first term $\bigcup_{e \in \bigcup_i S_i} \authchain(e)$.
• $\authchain(f)f$ is contained in the second term $\bigcap_i \left(\bigcup_{e \in S_i} \authchain(e) \right)$.

Therefore $\authchain(f)$ does not belong to the auth difference: it will added by the first term only to be removed by the second term. Therefore we so we can omit events $f \in \bigcap_i S_i$ in both unions without changing the final result of the computation. INCORRECT, SEE BELOW.

$$\begin{align*}
\DeclareMathOperator\fullauthchain{FullAuthChain}
\DeclareMathOperator\authchain{AuthChain}
\text{auth difference as written} &= \bigcup_{e \in \bigcup_i S_i} \authchain(e) − \bigcap_i \left(\bigcup_{e \in S_i} \authchain(e) \right) \
&= \bigcup_{e \in \bigcup_i S_i - \bigcap_i S_i} \authchain(e) − \bigcap_i \left(\bigcup_{e \in S_i - \bigcap_i S_i} \authchain(e) \right) \
&= \bigcup_{e \in S_\text{conflicted}} \authchain(e) − \bigcap_i \left(\bigcup_{e \in S_i - S_\text{unconflicted}} \authchain(e) \right) \
&= \fullauthchain (S_\text{conflicted}) − \bigcap_i \fullauthchain (S_i - S_\text{unconflicted})
\end{align*}$$

If this reasoning is sound, one could argue that this is an implementation detail rather than a spec concern. But I think the idea is interesting enough to consider a change to the spec anyway.

It was not sound.

[DMRobertson]

(Original post edited with some improvements to notation.)

[DMRobertson]

@erikjohnston and I now believe the above to be mistaken. The second line of the second block of maths. Consider an event x in AuthChain(f) that is also in Auth(e), where f is unconflicted but e is conflicted. Then x will belong to the big union but not in the big intersection. Hence x will belong tot he proposed auth difference, but not in the current auth difference.

I will PR reverting the corresponding spec change. #1132.

[DMRobertson]

Corrected maths:

$$\begin{align*} \DeclareMathOperator\fullauthchain{FullAuthChain} \DeclareMathOperator\authchain{AuthChain} \text{auth difference as written} &= \bigcup_i C_i − \bigcap_i C_i \\ &= \bigcup_i \fullauthchain(S_i) − \bigcap_i \fullauthchain(S_i) \\ &= \bigcup_i \left(\bigcup_{e \in S_i} \authchain(e) \right) − \bigcap_i \left(\bigcup_{e \in S_i} \authchain(e) \right)  \\ &= \bigcup_{e \in \bigcup_i S_i} \authchain(e) − \bigcap_i \left(\bigcup_{e \in S_i} \authchain(e) \right) \end{align*}$$

Suppose that $f \in S_\text{unconflicted} = \bigcap_i S_i$ is an event in the unconflicted state map.
Then:

• $\authchain(f)$ is contained in the first term $\bigcup_{e \in \bigcup_i S_i} \authchain(e)$.
• $\authchain(f)$ is contained in the second term $\bigcap_i \left(\bigcup_{e \in S_i} \authchain(e) \right)$.

Therefore $\authchain(f)$ does not belong to the auth difference: it will added by the first term only to be removed by the second term. Therefore we so we can omit events $f \in \bigcap_i S_i$ in both unions without changing the final result of the computation. Therefore we so we can omit events $f \in \bigcap_i S_i$ from the first union without changing the difference of sets.

$$\begin{align*} \DeclareMathOperator\fullauthchain{FullAuthChain} \DeclareMathOperator\authchain{AuthChain} \text{auth difference as written} &= \bigcup_{e \in \bigcup_i S_i} \authchain(e) − \bigcap_i \left(\bigcup_{e \in S_i} \authchain(e) \right) \\ &= \bigcup_{e \in \bigcup_i S_i - \bigcap_i S_i} \authchain(e) − \bigcap_i \left(\bigcup_{e \in S_i} \authchain(e) \right) \\ &= \bigcup_{e \in S_\text{conflicted}} \authchain(e) − \bigcap_i \left(\bigcup_{e \in S_i} \authchain(e) \right) \end{align*}$$

[DMRobertson]

TL;DR:

• Maths wrong. Can still narrow the big union term, but that might not make much difference to an implementation. Depends on how it's chosen to compute the auth difference.
• Not convinced the prototype implementation was correct either.
• Stateres on a test room was fine. Suspect because a) examples not complicated enough, b) unconflicted state get splatted at the end.
• Stateres being fine makes this an interesting experiement!
• Spec change reverted.