I put the 64-bit check in deliberately. As I understand it, the json_decode function in current releases of PHP casts JSON long values to floats on 32-bit platforms. It looks like a future release will allow representing longs as strings on 32-bit via a JSON_BIGINT_AS_STRING option, but it's not available now, unfortunately. So even if I did my PHP bit-twiddling using the GMP library, I wouldn't be able to get the actual value out of the JSON, unless I parsed the JSON myself.
I'll build a 32-bit VM and see if I can figure out something.
Another option would be to start from scratch and build the PHP lib using the C library as an extension, though when I first took a look at that, it didn't look feasible.
Any other ideas? I'm open to suggestions.