castfn u2uint64{v : nat | v <= 0xFFFFFFFFFFFFFFFF}(v : uint v) : uint64 v