Low-level shift operator implementation

Question

I want a shift operator for an architecture that implements boxing. Basically, the high-level constructs represent integers as 31 bits followed by 1 bit set to one as a tag (so to represent binary int i I use instead 2i+1). Let's denote the box representation as $[[\cdot]]$, then I was able to make the following deductions. Consider x the number to be the shifted value and y the shift value (read the following to understand the whole process):

$[[\text{shift} \, x \, y]] = 2*{\text{shift} \big[\frac{[[x]]-1}{2} \, \frac{[[y]]-1}{2}}\big] + 1 = 2*{\text{shift} \big[\frac{[[x]]-1}{2} \, \frac{[[y]]}{2}}\big] + 1 = $

$= {\big[\text{shift} \; [[x]]-1 \, \frac{[[y]]}{2}}\big] + 1$

Here we can use $\frac{[[x]]-1}{2}$ or $\frac{[[x]]}{2}$ because $[[x]]$ always ends with a one however in the last step we remove the division by two and for $[[x]]$ we have to keep $-1$ but not for $[[y]]$. Please note that this translation is meant for left shifts where the bit structure of $x$ is important, namely if we have $x_1 x_2 x_3 1$ the last bit will be actually used in contrast with the right shift case.

The following is the version for the right shift (again read what follows to understand the process):

$[[\text{shift} \, x \, y]] = 2*{\text{shift} \big[\frac{[[x-1]]}{2} \, \frac{[[y-1]]}{2}}\big] + 1 = 2*{\text{shift} \big[\frac{[[x]]}{2} \, \frac{[[y]]}{2}}\big] + 1 = $

$= {\big[\text{shift} \; [[x]] \, \frac{[[y]]}{2}}\big] + 1$

Here the point is that the last bit is no longer useful and can be ignored.

I wonder if me scheme is correct and efficient in the sense that it may exist other procedure that is more efficient than mine. I would appreaciate as well that you clarify the intuitive ideas I gave for my procedure (if it is correct) reelaborating my assertions with possibly more accurate ones. Also I would appreciate ideas that suggest how to mix this two implementations.