[Bug] Record protocol counters may overflow

**Describe the bug**
While verifying the F* code generated from Bertie, we found that the record protocol message/encryption counters could potentially overflow. We should trigger an error to prevent this.

See e.g. https://github.com/cryspen/bertie/blob/39c45ce83357da202151d7919293f3e5f83c345b/proofs/fstar/extraction-panic-free/Bertie.Tls13record.fst#L227

**To Reproduce**

**Expected behavior**

**Actual behavior**

**Screenshots or debug log**

**Platform (please complete the following information):**

**Additional context**

Start at proofs/fstar/extraction-panic-free/Bertie.Tls13record.fst around line 227 and trace how record protocol message and encryption counters are handled. Done means counter overflow triggers an error instead of continuing, with the generated Bertie verification behavior checked against that requirement.

Written by the indexing model from the issue text.