[Bug] Trunc Length in Client Hello

[karthikbhargavan]

Describe the bug
While verifying the F* code, the treatment of trunc_len seems to be wrong.
It is treated as the length of the suffix in some places and as the length of the prefix in others.
This bears investigation.

See e.g.

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

Line 2287 in 39c45ce

assume(v chlen >= v trunc_len + v hlen);

To Reproduce

Expected behavior

Actual behavior

Screenshots or debug log

Platform (please complete the following information):

Additional context