I agree that the behavior uint64 var3 = (uint64)(int64)var0; is somewhat unnatural, but converting a negative value as an unsigned value is bound to cause surprising results. Your solution is just as surprising: uint64 var4 = (uint64)(uint32)var0; has the disadvantage that converting the resulting value back to a signed type int64 does not produce the original value, whereas the C semantics do ensure that.
In other words (int64)var3 == var0 for all values of var0, but (int64)var4 == var0 only holds for positive values of var0.
I rest my case.
