Pruning point heuristic formula

This is not an actual research post, but rather a technical mathematical one for clarifying a point. I’m using this platform mainly due to latex support.

I might be using basic notation from the prunality proof. However note that pruning point calculation in the actual Kaspa implementation was modified a bit to be non-sliding, as described below.

Definitions

Denote P, F to be the pruning and finality depths respectively.

Define the finality score of a block to be:

FinalityScore(B) := \lfloor BlueScore(B) / F \rfloor

The formula for calculating the pruning point of a block B is as follows:

PruningPoint(B) := \max C \in Chain(B) \text{ s.t. } BlueScore(B) - BlueScore(C) \ge P AND FinalityScore(C) > FinalityScore(PruningPoint(SelectedParent(B)))

In words: we only progress the pruning point of a block if we find a pruning point candidate which has larger finality score than the previous pruning point (i.e. the one we calculated for SelectedParent(B)).

The idea is that the usage of finality score makes the pruning point move in steps of F.

Heuristic

Now, we want to define a heuristic for easily determining that the pruning point did not move, and to do so with out iterating a F–length chain, at least in most cases.

Claim: if FinalityScore(BlueScore(B) - P) \le FinalityScore(PruningPoint(SelectedParent(B))) then
PruningPoint(B) = PruningPoint(SelectedParent(B))

Proof: assume the contrary and denote \pi the pruning point of B. By definition we know that BlueScore(\pi) \le BlueScore(B) - P. So FinalityScore(\pi) \le FinalityScore(BlueScore(B) - P), contradicting the requirement that FinalityScore progressed.

(note: some abuse of notation here by using the block or the blue score of a block or a sum combination in calls to FinalityScore)

However, the current codebase seems to have a wrong formula for this heuristic (see here), with the following condition:

FinalityScore(BlueScore(B)) \le FinalityScore(PruningPoint(SelectedParent(B))+P)

This is not an equal definition due to the floor function in the definition of FinalityScore.

The question for discussion is how safe is it to fix this condition w/o breaking consensus. It seems like there are theoretical cases where the wrong formula returns true while the correct formula returns false, meaning that the current code would skip searching for the new pruning point although it should have performed the search.