mirror of
https://github.com/google/brotli.git
synced 2026-02-04 05:35:09 +00:00
How to prove correctness: 1) when `position` is `0`, `max_length` is allowed to be `ringbuffer_size` 2) in other words: `position + max_length <= ringbuffer_size` 3) `ringbuffer_mask == ringbuffer_size - 1` 4) thus `position + max_length <= ringbuffer_size + 1` PiperOrigin-RevId: 836145553