Make Word shift operations total (#104)

Eliminates Booster aborts on `SLLI` and `SRLI` instructions.

---------

Co-authored-by: devops <devops@runtimeverification.com>

Author: tothtamas28

package/version

@@ -1 +1 @@
-0.1.72
+0.1.73

pyproject.toml

@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "kriscv"
-version = "0.1.72"
+version = "0.1.73"
 description = "K tooling for the RISC-V architecture"
 authors = [
     "Runtime Verification, Inc. <contact@runtimeverification.com>",

src/kriscv/kdist/riscv-semantics/riscv.md

@@ -198,12 +198,15 @@ We then provide rules to consume and execute each instruction from the top of th
 ```k
   rule <instrs> SLLI RD , RS , SHAMT => .K ...</instrs>
        <regs> REGS => writeReg(REGS, RD, readReg(REGS, RS) <<Word SHAMT) </regs>
+    requires 0 <=Int SHAMT
 
   rule <instrs> SRLI RD , RS , SHAMT => .K ...</instrs>
        <regs> REGS => writeReg(REGS, RD, readReg(REGS, RS) >>lWord SHAMT) </regs>
+    requires 0 <=Int SHAMT
 
   rule <instrs> SRAI RD , RS , SHAMT => .K ...</instrs>
        <regs> REGS => writeReg(REGS, RD, readReg(REGS, RS) >>aWord SHAMT) </regs>
+    requires 0 <=Int SHAMT
 ```
 `LUI` builds a 32-bit constant from the 20-bit immediate by setting the 12 least-significant bits to `0`, then sign extends to `XLEN` bits and places the result in register `RD`.
 ```k

src/kriscv/kdist/riscv-semantics/word.md

@@ -101,8 +101,9 @@ is used to zero-out all but the least-significant `XLEN`-bits in case of overflo
   syntax Word ::= Word "xorWord" Word [function, total]
   rule W(I1) xorWord W(I2) => W(I1 xorInt I2)
 
-  syntax Word ::= Word "<<Word" Int [function]
-  rule W(I1) <<Word I2 => chop(I1 <<Int I2)
+  syntax Word ::= Word "<<Word" Int [function, total]
+  rule W(I1) <<Word I2 => chop(I1 <<Int I2) requires 0 <=Int I2
+  rule _     <<Word I2 => W(0)              requires I2 <Int 0
 ```
 For right shifts, we provide both arithmetic and logical variants.
 
@@ -113,12 +114,14 @@ Counterintuitively, we use the arithmetic right shift operator `>>Int` for `Int`
 
 That is, for any `I:Int` underlying some `W(I):Word`, applying `>>Int` will always pad with `0`s, correctly implementing a logical right shift.
 ```k
-  syntax Word ::= Word ">>lWord" Int [function]
-  rule W(I1) >>lWord I2 => W(I1 >>Int I2)
+  syntax Word ::= Word ">>lWord" Int [function, total]
+  rule W(I1) >>lWord I2 => W(I1 >>Int I2) requires 0 <=Int I2
+  rule _     >>lWord I2 => W(0)           requires I2 <Int 0
 ```
 To actually perform an arithmetic shift over `Word`, we first convert to an infinitely sign-extended `Int` of equal value using `Word2SInt`, ensuring `>>Int` will pad with `1`s for a negative `Word`. The final result will still be infinitely sign-extended, so we must `chop` it back to a `Word`.
 ```k
-  syntax Word ::= Word ">>aWord" Int [function]
-  rule W1 >>aWord I2 => chop(Word2SInt(W1) >>Int I2)
+  syntax Word ::= Word ">>aWord" Int [function, total]
+  rule W1 >>aWord I2 => chop(Word2SInt(W1) >>Int I2) requires 0 <=Int I2
+  rule _  >>aWord I2 => W(0)                         requires I2 <Int 0
 endmodule
 ```