Unsound duplicate VRF checks introduced in Van Rossem?

Hello, since protocol major 11 / Van Rossem, an additional rule checking for VRF duplicates has been introduced. The implementation can roughly be described as:

- The ledger now keeps a map of VRF to non-zero counters
- The map is initialized at the Van Rossem hard fork boundary; it's a map and not a set because there can be duplicates already present; but starting from the hard fork, all new entries can only go up to 1.
- When a pool is registered or re-registered, the registration is rejected if the VRF already exists UNLESS a pool is re-registering with the same VRF
- When updating a pool (a.k.a re-registering), any VRF introduced by a previous registration in the same epoch is dropped from the map; and a new entry is inserted in the map with a counter = 1.
- Nothing happens immediately w.r.t the VRF map during the epoch when processing a pool de-registration certificate.
- During the epoch transition, the VRF map is cleaned up from:
- pools that have effectively unregistered; the counter is decremented and the entry removed if the counter reaches 0.
- dangling VRF entries, which corresponds to previous VRF keys from pools updating their VRF at the epoch boundary.

Now; it seems that there are two edge-cases not properly covered here.

1. If multiple pools (let's say 2), had the same VRF before the hard fork. If one pool re-registers a new VRF, then at the epoch boundary, the VRF ends up in the dangling set and is removed entirely. Thus allowing the VRF to be re-used, despite it still being used by another pool. I don't get why the counter isn't simply decremented here instead?

2. Similarly, if multiple pools existed, and one pool re-register for the first time in an epoch with the same VRF; the existing counter is overwritten with `1`. On the next VRF change, re-use will be allowed despite the VRF key still in use from other pools.

Am I missing something?