# Low-level division operator implementation

A few weeks ago, I asked this question on the implementation of the shift operator for an architecture that implements boxing. Reviewing my implementation I found out that the division operator wasn't correctly done. My language should implement the construct L3IntDiv that implements floored division in contrast with truncated division used for instance in Java. For example $\frac{-14}{5}$ should give -3 and not -2. For that purpose it relies on an instruction Div that also implements floor division. So the main challenge is to deal with the boxing representation in an efficient way.

The translation I was doing for my construct was as follows:

L3IntDiv(x,y) {
c1 = -1
t2 = ArithShift(x,c1)
r = Div(t1,t2)
n = Sub(r,c1)
}


Remember that the convention is that the shift to the right takes a negative argument and the shift to the left a positive argument. Also the shift left fills the bit-array with zeros and the right shift just removes digits introducing zeros by the left hand side.

But the actual code that works looks as follows (note the replacement by OR at the last line):

L3IntDiv(x,y){
c1 = -1
c2 = 1
t2 = ArithShift(y,c1)
r = Div(t1,t2)
n = Or(r,c2)
}


The formal deduction that I did looked as follows:

$[[x \,/ y]] = 2*{\Big[\frac{\frac{[[x]]-1}{2}}{ \frac{[[y]]-1}{2}}}\Big] + 1 =2*{\Big[\frac{\frac{[[x]]}{2}}{\frac{[[y]]}{2}}}\Big] + 1$

I don't think this notation is fair, instead of dividing by two I should write shift to the right.

$[[x \,/ y]] = 2*{\Big[\frac{\frac{[[x]]-1}{2}}{ \frac{[[y]]-1}{2}}}\Big] + 1 =2*{\Big[\frac{shiftRight([[x]],1)}{shiftRight([[y]],1)}}\Big] + 1$

In summary, I'm asking for a reasoning that would give me the specified division operation (floor division) from the box representation of the integers (with the notation [[⋅]]) and how does this fit the second implementation.

Remember that 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) and that I'm denoting the box representation as [[⋅]].

Edit:

To formaly deal with this operations it might be of use wikipedia.