[rdtsc]

> Unfortunately JSON numbers are 64 bit floats, so if you're standards compliant you have to treat them as such,

Are you sure? Looking at https://www.json.org/json-en.html I don't see anything about 64 bit floats.