diff --git a/kmir/src/kmir/kdist/mir-semantics/lemmas/kmir-lemmas.md b/kmir/src/kmir/kdist/mir-semantics/lemmas/kmir-lemmas.md
index 5dbd60d37..6feadad80 100644
--- a/kmir/src/kmir/kdist/mir-semantics/lemmas/kmir-lemmas.md
+++ b/kmir/src/kmir/kdist/mir-semantics/lemmas/kmir-lemmas.md
@@ -119,10 +119,18 @@ power of two but the semantics will always operate with these particular ones.
   rule bitmask32  => ( 1 <<Int 32 ) -Int 1
   rule bitmask64  => ( 1 <<Int 64 ) -Int 1
   rule bitmask128 => ( 1 <<Int 128) -Int 1
-
 ```
 
 
+## Simplifications for `Int` Inequalities
+
+The following simplifications are useful for conditions in overflow checks and bitwise operations.
+
+```k
+rule [int-and-255-geq-0]: 0 <=Int _ &Int 255 => true [simplification, smt-lemma]
+rule [int-and-255-lt-256]: _ &Int 255 <Int 256 => true [simplification, smt-lemma]
+```
+
 ```k
 endmodule
 ```
\ No newline at end of file
diff --git a/kmir/src/kmir/kdist/mir-semantics/rt/data.md b/kmir/src/kmir/kdist/mir-semantics/rt/data.md
index 78bf6d132..0de30d00d 100644
--- a/kmir/src/kmir/kdist/mir-semantics/rt/data.md
+++ b/kmir/src/kmir/kdist/mir-semantics/rt/data.md
@@ -1067,6 +1067,31 @@ Type casts between a number of different types exist in MIR.
 
 ```k
   syntax Evaluation ::= #cast( Evaluation, CastKind, MaybeTy, Ty ) [strict(1)]
+  syntax Evaluation ::= castAux ( Value, CastKind, MaybeTypeInfo, TypeInfo ) [function, no-evaluators]
+  syntax MaybeTypeInfo ::= TypeInfo | "TypeInfoUnknown" 
+  // ----------------------------------------------------------------
+  rule <k> #cast(VAL, CASTKIND, TyUnknown, TY_TARGET)
+        => castAux(VAL, CASTKIND, TypeInfoUnknown, {TYPEMAP[TY_TARGET]}:>TypeInfo)
+           // castAux handles the actual casting
+       ...
+       </k>
+       <types> TYPEMAP </types>
+    requires TY_TARGET in_keys(TYPEMAP)
+     andBool isTypeInfo(TYPEMAP[TY_TARGET])
+    [priority(160), preserves-definedness] 
+    // low priority, because this is only for writing simplification rules for now
+    // valid map lookups checked
+  rule <k> #cast(VAL, CASTKIND, TY_SOURCE:Ty, TY_TARGET)
+        => castAux(VAL, CASTKIND, {TYPEMAP[TY_SOURCE]}:>TypeInfo, {TYPEMAP[TY_TARGET]}:>TypeInfo)
+           // castAux handles the actual casting
+       ...
+       </k>
+       <types> TYPEMAP </types>
+    requires TY_SOURCE in_keys(TYPEMAP) andBool isTypeInfo(TYPEMAP[TY_SOURCE])
+     andBool TY_TARGET in_keys(TYPEMAP) andBool isTypeInfo(TYPEMAP[TY_TARGET])
+    [priority(160), preserves-definedness]
+  rule castAux(VAL, CASTKIND, TYPE_SOURCE, TYPE_TARGET) => thunk(castAux(VAL, CASTKIND, TYPE_SOURCE, TYPE_TARGET)) [concrete]
+    // thunk to avoid re-evaluation of castAux
 ```
 
 ### Number Type Casts
diff --git a/kmir/src/kmir/kdist/mir-semantics/symbolic/p-token.md b/kmir/src/kmir/kdist/mir-semantics/symbolic/p-token.md
index bd3fdd28c..82a347a05 100644
--- a/kmir/src/kmir/kdist/mir-semantics/symbolic/p-token.md
+++ b/kmir/src/kmir/kdist/mir-semantics/symbolic/p-token.md
@@ -193,10 +193,18 @@ The code uses some helper sorts for better readability.
   syntax List ::= #asU8s ( Int )            [function]
                 | #asU8List ( List , Int ) [function]
   // -------------------------------------
-  rule #asU8s(X) => #asU8List(.List, X)
+  rule #asU8s(X) => #asU8List(.List, X) [concrete]
   rule #asU8List(ACC, _) => ACC requires 8 <=Int size(ACC) [priority(40)] // always cut at 8 bytes
   rule #asU8List(ACC, X) => #asU8List( ACC ListItem(Integer( X &Int 255, 8, false)) , X >>Int 8) [preserves-definedness]
 
+  // mapping an offset over bytes produced by #asU8s has no effect
+  rule #mapOffset(#asU8s(X), _) => #asU8s(X) [simplification, preserves-definedness]
+
+  // Shortcut transmute: [u8; 8] (from #asU8s) to u64
+  rule castAux(Range(#asU8s(X)), castKindTransmute, _TY_SOURCE, TY_TARGET) => Integer(X, 64, false)
+    requires TY_TARGET ==K typeInfoPrimitiveType(primTypeUint(uintTyU64))
+    [simplification, preserves-definedness]
+
   rule toAmount(fromAmount(AMT)) => AMT [simplification, preserves-definedness]
   rule fromAmount(toAmount(VAL)) => VAL [simplification, preserves-definedness]