add function vs_pushdouble

This is a reminder to myself to port vs_pushdouble (and whatever other divergence we have) from the private repo.