Re: [quicwg/base-drafts] Largest Reference algorithm can produce invalid values (#2112)

[Bence Béky <[e-mail]>]

I was able to convince myself that the current algorithm cannot produce invalid
values.  Here's my reasoning:

```python

# Because of the way Largest Reference is encoded.
assert(0 < LargestReference)
assert(LargestReference <= 2 * MaxEntries)
# A decoder should signal an error if the input is out of this range.

if LargestReference > 0:
  LargestReference -= 1

  assert(0 <= LargestReference)
  assert(LargestReference < 2 * MaxEntries)

  CurrentWrapped = TotalNumberOfInserts mod (2 * MaxEntries)

  assert(0 <= CurrentWrapped)
  assert(CurrentWrapped < 2 * MaxEntries)

  if CurrentWrapped >= LargestReference + MaxEntries:
    # Largest Reference wrapped around 1 extra time
    assert(CurrentWrapped >= LargestReference + MaxEntries)
    LargestReference += 2 * MaxEntries
    assert(CurrentWrapped >= LargestReference - MaxEntries)

    # Because CurrentWrapped < 2 * MaxEntries
    # and LargestReferencee >= 2 * MaxEntries.
    assert(CurrentWrapped - MaxEntries < LargestReference)

  else if CurrentWrapped + MaxEntries < LargestReference
    # Decoder wrapped around 1 extra time
    assert(CurrentWrapped + MaxEntries < LargestReference)
    CurrentWrapped += 2 * MaxEntries
    assert(CurrentWrapped - MaxEntries < LargestReference)

    # Because LargestReference < 2 * MaxEntries
    # and CurrentWrapped >= 2 * MaxEntries.
    assert(LargestReference <= CurrentWrapped + MaxEntries)

  # If either of these had been false, one of the branches above would have been
  # executed, making both of these true.
  assert(LargestReference <= CurrentWrapped + MaxEntries)
  assert(CurrentWrapped - MaxEntries < LargestReference)

  assert(TotalNumberOfInserts mod (2 * MaxEntries) == CurrentWrapped mod (2 * MaxEntries))
  # therefore the following line does not change LargestReference mod (2 * MaxEntries).

  LargestReference += TotalNumberOfInserts - CurrentWrapped

  # Substituting into the above inequalities, we get
  assert(TotalNumberOfInserts - MaxEntries < LargestReference)
  assert(LargestReference - MaxEntries <= TotalNumberOfInserts)

  # This is exactly what we want:
  # Entry TotalNumberOfInserts - MaxEntries is evicted,
  # entry LargestReference is referenced,
  # entry LargestReference - MaxEntries is presumably evicted
  # (unless the encoder references LargestReference it but does not emit it
  # until later, which is crazy),
  # entry TotalNumberOfInserts is acknowledged.
  # The spec requires that an evicted entry cannot be referenced and
  # every evicted entry must be acknowledged.
```

Therefore I belive that this issue can be closed.

However, I am worried that `TotalNumberOfInserts - CurrentWrapped` might
underflow if one is doing unsigned arithmetics.

-- 
You are receiving this because you are subscribed to this thread.
Reply to this email directly or view it on GitHub:
https://github.com/quicwg/base-drafts/issues/2112#issuecomment-449414630