[Bug] Record protocol counters may overflow

[karthikbhargavan]

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.

bertie/proofs/fstar/extraction-panic-free/Bertie.Tls13record.fst

Line 227 in 39c45ce

assume (v n < maxint u64_inttype);

To Reproduce

Expected behavior

Actual behavior

Screenshots or debug log

Platform (please complete the following information):

Additional context