Backport p-token tweaks (#672)

This is a collection of changes that were (or appeared) useful while
working on the P-Token domain data model and advancing the property
proofs. Each commit is an addition of its own
* Ceil simplification rules for `#mapOffset` (for the legacy backend,
might not be necessary after all)
* avoid modulus calculations for number truncation (we now have a
function for it)
* project setup: add markdown selectors `symbolic`/`concrete` so we can
separate symbolic backend code blocks
* implement `CastKindIntToInt` for `Bool` -> `Int` (related code was
observed in the wild).
* Implement support for trivial cases of `transmute` (same type only)

The "avoid modulus" requires changes (good changes) on the test
expectations, the changed `Ceil` simplification changes a hash in one
expectation file.

Author: jberthold

kmir/src/kmir/kdist/mir-semantics/lemmas/kmir-lemmas.md

@@ -52,9 +52,14 @@ If nothing is removed, the list remains the same. If all elements are removed, n
 ```
 
 The `#mapOffset` function maps `#adjustRef` over a lists of `Value`s, leaving the list length unchanged.
+Definedness of the list and list elements is also guaranteed.
 
 ```k
   rule size(#mapOffset(L, _)) => size(L) [simplification, preserves-definedness]
+
+  rule #Ceil(#mapOffset(L, _)[I]) => #Ceil(L) #And {true #Equals 0 <=Int I} #And {true #Equals I <Int size(L)} [simplification]
+
+  rule #Ceil(#mapOffset(L, _)) => #Ceil(L) [simplification]
 ```
 
 ## Simplifications for Int

kmir/src/kmir/kdist/mir-semantics/rt/data.md

@@ -1056,6 +1056,30 @@ bit width, signedness, and possibly truncating or 2s-complementing the value.
       [preserves-definedness] // ensures #numTypeOf is defined
 ```
 
+Boolean values can also be cast to Integers (encoding `true` as `1`).
+
+```k
+  rule <k> #cast(BoolVal(VAL), castKindIntToInt, _, TY)
+          =>
+            #intAsType(1, 8, #numTypeOf({TYPEMAP[TY]}:>TypeInfo))
+          ...
+        </k>
+        <types> TYPEMAP </types>
+      requires #isIntType({TYPEMAP[TY]}:>TypeInfo)
+       andBool VAL
+      [preserves-definedness] // ensures #numTypeOf is defined
+
+  rule <k> #cast(BoolVal(VAL), castKindIntToInt, _, TY)
+          =>
+            #intAsType(0, 8, #numTypeOf({TYPEMAP[TY]}:>TypeInfo))
+          ...
+        </k>
+        <types> TYPEMAP </types>
+      requires #isIntType({TYPEMAP[TY]}:>TypeInfo)
+       andBool notBool VAL
+      [preserves-definedness] // ensures #numTypeOf is defined
+```
+
 Casts involving `Float` values are currently not implemented.
 
 ### Casts between pointer types
@@ -1180,15 +1204,37 @@ The original metadata is therefore already stored as `staticSize` to avoid havin
       // [preserves-definedness] // valid type map indexing and sort coercion
 ```
 
+### `Transmute` casts
+
+An unsafe `transmute` operation in Rust is an arbitrary cast between unrelated types based on assumptions that the byte
+representations of the source and target types are somewhat relatable (or else, under full consideration that they are not).
+
+Support for `castKindTransmute` in this semantics is very limited because of the high-level data model applied.
+What can be supported without additional layout consideration is trivial casts between the same underlying type (mutable or not).
+
+```k
+  rule <k> #cast(Reference(_, _, _, _) #as REF, castKindTransmute, TY_SOURCE, TY_TARGET) => REF ... </k>
+       <types> TYPEMAP </types>
+      requires TY_SOURCE in_keys(TYPEMAP)
+       andBool TY_TARGET in_keys(TYPEMAP)
+       andBool TYPEMAP[TY_SOURCE] ==K TYPEMAP[TY_TARGET]
+      [preserves-definedness] // valid map lookups checked
+
+  rule <k> #cast(PtrLocal(_, _, _, _) #as PTR, castKindTransmute, TY_SOURCE, TY_TARGET) => PTR ... </k>
+       <types> TYPEMAP </types>
+      requires TY_SOURCE in_keys(TYPEMAP)
+       andBool TY_TARGET in_keys(TYPEMAP)
+       andBool TYPEMAP[TY_SOURCE] ==K TYPEMAP[TY_TARGET]
+      [preserves-definedness] // valid map lookups checked
+```
+
 ### Other casts involving pointers
 
 | CastKind                     | Description |
 |------------------------------|-------------|
 | PointerExposeProvenance      |             |
 | PointerWithExposedProvenance |             |
 | FnPtrToPtr                   |             |
-| Transmute                    |             |
-
 
 ## Decoding constants from their bytes representation to values
 

kmir/src/kmir/kdist/mir-semantics/rt/numbers.md

@@ -127,27 +127,21 @@ This truncation function is instrumental in the implementation of Integer arithm
           true
         )
     requires #bitWidth(INTTYPE) <=Int WIDTH
-    [preserves-definedness] // positive shift, divisor non-zero
 
   // widening: nothing to do: VAL does not change (enough bits to represent, no sign change possible)
   rule #intAsType(VAL, WIDTH, INTTYPE:IntTy)
       =>
         Integer(VAL, #bitWidth(INTTYPE), true)
     requires WIDTH <Int #bitWidth(INTTYPE)
 
-  // converting to unsigned int types
-  // truncate (if necessary), then add bias to make non-negative, then truncate again
+  // converting to unsigned int types (simple bitmask)
   rule #intAsType(VAL, _, UINTTYPE:UintTy)
       =>
         Integer(
-          (VAL %Int (1 <<Int #bitWidth(UINTTYPE) )
-            +Int (1 <<Int #bitWidth(UINTTYPE)))
-          %Int (1 <<Int #bitWidth(UINTTYPE) )
-          ,
+          truncate(VAL, #bitWidth(UINTTYPE), Unsigned),
           #bitWidth(UINTTYPE),
           false
         )
-    [preserves-definedness] // positive shift, divisor non-zero
 ```
 
 ## Alignment of Primitives

kmir/src/kmir/kdist/plugin.py

@@ -42,7 +42,6 @@ def deps(self) -> tuple[str, ...]:
 def _default_args(src_dir: Path) -> dict[str, Any]:
     return {
         'include_dirs': [src_dir],
-        'md_selector': 'k',
         'warnings_to_errors': True,
         'syntax_module': 'KMIR-AST',
     }
@@ -54,6 +53,7 @@ def _default_args(src_dir: Path) -> dict[str, Any]:
         lambda src_dir: {
             'main_file': src_dir / 'mir-semantics/kmir.md',
             'backend': PykBackend.LLVM,
+            'md_selector': 'k & ! symbolic',
             **_default_args(src_dir),
         },
     ),
@@ -62,13 +62,15 @@ def _default_args(src_dir: Path) -> dict[str, Any]:
             'main_file': src_dir / 'mir-semantics/kmir.md',
             'backend': PykBackend.LLVM,
             'llvm_kompile_type': LLVMKompileType.C,
+            'md_selector': 'k & ! symbolic',
             **_default_args(src_dir),
         },
     ),
     'haskell': KompileTarget(
         lambda src_dir: {
             'main_file': src_dir / 'mir-semantics/kmir.md',
             'backend': PykBackend.HASKELL,
+            'md_selector': 'k & ! concrete',
             **_default_args(src_dir),
         },
     ),

kmir/src/tests/integration/data/crate-tests/single-lib/testing::test_add_in_range.expected

@@ -9,7 +9,7 @@
 ┃ (branch)
 ┣━━┓ subst: .Subst
 ┃  ┃ constraint:
-┃  ┃     notBool ARG_UINT1:Int +Int 340282366920938463463374607431768211456 %Int 340282366920938463463374607431768211456 +Int ARG_UINT2:Int +Int 340282366920938463463374607431768211456 %Int 340282366920938463463374607431768211456 <=Int 18446744073709551615
+┃  ┃     notBool ARG_UINT1:Int +Int ARG_UINT2:Int <=Int 18446744073709551615
 ┃  │
 ┃  ├─ 4
 ┃  │   #selectBlock ( switchTargets ( ... branches: branch ( 0 , basicBlockIdx ( 1 ) )
@@ -20,7 +20,7 @@
 ┃
 ┗━━┓ subst: .Subst
    ┃ constraint:
-   ┃     ARG_UINT1:Int +Int 340282366920938463463374607431768211456 %Int 340282366920938463463374607431768211456 +Int ARG_UINT2:Int +Int 340282366920938463463374607431768211456 %Int 340282366920938463463374607431768211456 <=Int 18446744073709551615
+   ┃     ARG_UINT1:Int +Int ARG_UINT2:Int <=Int 18446744073709551615
    │
    ├─ 5
    │   #selectBlock ( switchTargets ( ... branches: branch ( 0 , basicBlockIdx ( 1 ) )

kmir/src/tests/integration/data/prove-rs/show/symbolic-args-fail.eats_all_args.expected

@@ -60,7 +60,7 @@
 ┃     ┃  │   #EndProgram ~> .K
 ┃     ┃  │
 ┃     ┃  ┊  constraint:
-┃     ┃  ┊      Ceil_a90d0b00
+┃     ┃  ┊      Ceil_3c8e32fd
 ┃     ┃  ┊  subst: ...
 ┃     ┃  └─ 2 (leaf, target, terminal)
 ┃     ┃      #EndProgram ~> .K
@@ -123,7 +123,7 @@
       ┃  │   #EndProgram ~> .K
       ┃  │
       ┃  ┊  constraint:
-      ┃  ┊      Ceil_a90d0b00
+      ┃  ┊      Ceil_3c8e32fd
       ┃  ┊  subst: ...
       ┃  └─ 2 (leaf, target, terminal)
       ┃      #EndProgram ~> .K