Depends on the tweak encoding landing first.
The note's completeness argument has a step it states in prose and does not prove: that each grinding attempt is a fresh random-oracle query. It rests on two facts about tweaks, both small and both provable here.
First, the map from a randomizer to the encoding query's hash input is injective, so two different randomizers never collide into one query. Second, key generation never issues that query at all: generation uses tweak types 0, 1, 2, 3 and 10, and the encoding query uses type 4, so the two sets of hash inputs are disjoint. Together they are why each attempt's digest can be treated as uniform and independent of the history.
Worth proving in the same file: the chain-step positions 8 * i + k are distinct across all valid chain indices i < 42 and steps k < 8, so no two chain steps anywhere in the scheme share a tweak. That is the concrete form of the domain-separation property the whole construction leans on.
Depends on the tweak encoding landing first.
The note's completeness argument has a step it states in prose and does not prove: that each grinding attempt is a fresh random-oracle query. It rests on two facts about tweaks, both small and both provable here.
First, the map from a randomizer to the encoding query's hash input is injective, so two different randomizers never collide into one query. Second, key generation never issues that query at all: generation uses tweak types 0, 1, 2, 3 and 10, and the encoding query uses type 4, so the two sets of hash inputs are disjoint. Together they are why each attempt's digest can be treated as uniform and independent of the history.
Worth proving in the same file: the chain-step positions
8 * i + kare distinct across all valid chain indicesi < 42and stepsk < 8, so no two chain steps anywhere in the scheme share a tweak. That is the concrete form of the domain-separation property the whole construction leans on.