The doc buffer sometimes doesn't display decreases clauses; for instance here:
CommonDH.keyShareEntriesBytes_aux
/mnt/f/dev/sec/everest/fstar-master/mitls-fstar/src/tls/CommonDH.fst(699,16-699,40)
Type
b: bytes{UInt32.v (len b) < 65536} -> kes: list keyShareEntry -> Prims.Tot bytes kes
Documentation
Serializing function for a list of KeyShareEntry
where the range should be Prims.Tot bytes (decreases kes).
The doc buffer sometimes doesn't display decreases clauses; for instance here:
where the range should be
Prims.Tot bytes (decreases kes)
.