Update from master (#857)

* `assert_inhabited` implementation 
* `stable-mir-json` upgrade 
* simplifications for bit-shifts/masks in conversions

Author: jberthold

deps/stable-mir-json

@@ -1 +1 @@
-cf0410fba16002276f6fcdc195b7003e145558e9
+20a1bbdfc1fb36fb19539d0d4d91f5a437be7de6

deps/stable-mir-json_release

@@ -6,7 +6,7 @@
 
     flake-utils.url = "github:numtide/flake-utils";
 
-    stable-mir-json-flake.url = "github:runtimeverification/stable-mir-json/cf0410fba16002276f6fcdc195b7003e145558e9";
+    stable-mir-json-flake.url = "github:runtimeverification/stable-mir-json/20a1bbdfc1fb36fb19539d0d4d91f5a437be7de6";
     stable-mir-json-flake = {
       inputs.nixpkgs.follows = "nixpkgs";
       inputs.flake-utils.follows = "flake-utils";

flake.lock

@@ -53,6 +53,29 @@ before it's used. They have no effect on program semantics, and are implemented
   rule <k> #execIntrinsic(IntrinsicFunction(symbol("prefetch_write_instruction")), _ARG1:Operand _ARG2:Operand .Operands, _DEST) => .K ... </k>
 ```
 
+#### Assert Inhabited (`std::intrinsics::assert_inhabited`)
+
+The `assert_inhabited` instrinsic asserts that a type is "inhabited" (able to be instantiated). Types such as
+`Never` (`!`) cannot be instantiated and are uninhabited types. The target / codegen decides how to handle this
+intrinsic, it is not required to panic if the type is not inhabited, it could also perform a NO OP. We have witnessed
+in the case that there is an uninhabited type that the following basic block is `noBasicBlockIdx`, and so we
+error with `#AssertInhabitedFailure` if we see that following the intrinsic. Otherwise, we perform a NO OP.
+
+```k
+  syntax MIRError ::= "AssertInhabitedFailure"
+  rule <k> #execIntrinsic(IntrinsicFunction(symbol("assert_inhabited")), .Operands, _DEST)
+            ~> #continueAt(noBasicBlockIdx)
+        => AssertInhabitedFailure
+       ...
+      </k>
+
+  rule <k> #execIntrinsic(IntrinsicFunction(symbol("assert_inhabited")), .Operands, _DEST)
+        => .K
+       ...
+      </k>
+      [owise]
+```
+
 #### Raw Eq (`std::intrinsics::raw_eq`)
 
 The `raw_eq` intrinsic performs byte-by-byte equality comparison of the memory contents pointed to by two references.

flake.nix

@@ -4,7 +4,7 @@ This file contains basic lemmas required for symbolic execution of MIR programs
 
 Lemmas are simpliciations of symbolic function application that aims to confirm conditions for rewrite rules to avoid spurious branching on symbolic program parts.
 
-Some of the lemmas relate to the control flow implementation in `kmir.md` and will be needed in various proofs (for instance the simplification of list size for partially-symbolic lists of locals or stack frames).  
+Some of the lemmas relate to the control flow implementation in `kmir.md` and will be needed in various proofs (for instance the simplification of list size for partially-symbolic lists of locals or stack frames).
 Others are related to helper functions used for integer arithmetic.
 
 ```k
@@ -20,7 +20,7 @@ module KMIR-LEMMAS
 ```
 ## Simplifications for lists to avoid spurious branching on error cases in control flow
 
-Rewrite rules that look up locals or stack frames require that an index into the respective `List`s in the configuration be within the bounds of the locals list/stack. Therefore, the `size` function on lists needs to be computed. The following simplifications allow for locals and stacks to have concrete values in the beginning but a symbolic rest (of unknown size).  
+Rewrite rules that look up locals or stack frames require that an index into the respective `List`s in the configuration be within the bounds of the locals list/stack. Therefore, the `size` function on lists needs to be computed. The following simplifications allow for locals and stacks to have concrete values in the beginning but a symbolic rest (of unknown size).
 The lists used in the semantics are cons-lists, so only rules with a head element match are required.
 
 ```k
@@ -74,6 +74,24 @@ Definedness of the list and list elements is also guaranteed.
     [simplification]
 ```
 
+## Simplifications for `enum` Discriminants and Variant Indexes
+
+For symbolic enum values, the variant index remains unevaluated but the original (symbolic) discriminant can be restored:
+
+```k
+  rule #lookupDiscriminant(typeInfoEnumType(_, _, _, _, _), #findVariantIdxAux(DISCR, DISCRS, _IDX)) => DISCR
+    requires isOneOf(DISCR, DISCRS)
+    [simplification, preserves-definedness, symbolic(DISCR)]
+
+  syntax Bool ::= isOneOf ( Int , Discriminants ) [function, total]
+  // --------------------------------------------------------------
+  rule isOneOf( _,                       .Discriminants                      ) => false
+  rule isOneOf( I, discriminant(D)                     .Discriminants        ) => I ==Int D
+  rule isOneOf( I, discriminant(mirInt(D))             .Discriminants        ) => I ==Int D
+  rule isOneOf( I, discriminant(D)         ((discriminant(_) _MORE) #as REST)) => I ==Int D orBool isOneOf(I, REST)
+  rule isOneOf( I, discriminant(mirInt(D)) ((discriminant(_) _MORE) #as REST)) => I ==Int D orBool isOneOf(I, REST)
+```
+
 ## Simplifications for Int
 
 These are trivial simplifications driven by syntactic equality, which should be present upstream.
@@ -130,6 +148,14 @@ power of two but the semantics will always operate with these particular ones.
   rule VAL &Int bitmask128 => VAL requires 0 <=Int VAL andBool VAL <=Int bitmask128 [simplification, preserves-definedness, smt-lemma]
 ```
 
+Repeated bit-masking can be simplified in an even more general way:
+
+```k
+     rule (X &Int MASK &Int MASK) => X &Int MASK
+       requires 0 <Int MASK
+       [simplification, smt-lemma]
+```
+
 Support for `transmute` between byte arrays and numbers (and vice-versa) uses computations involving bit masks with 255 and 8-bit shifts.
 To support simplifying round-trip conversion, the following simplifications are essential.
 
@@ -165,6 +191,24 @@ To support simplifying round-trip conversion, the following simplifications are
     [simplification, preserves-definedness, symbolic(VAL)]
 ```
 
+More generally, a value which is composed of sliced bytes can generally be assumed to be in range of a suitable bitmask for the byte length.
+This avoids building up large expressions related to overflow checks and vacuous branches leading to overflow errors.
+
+```k
+  rule ((( _X0 )                                                                     &Int 255) +Int 256 *Int (
+         (( _X1 >>Int 8)                                                              &Int 255) +Int 256 *Int (
+           (( _X2 >>Int 8 >>Int 8)                                                    &Int 255) +Int 256 *Int (
+              (( _X3 >>Int 8 >>Int 8 >>Int 8)                                         &Int 255) +Int 256 *Int (
+                (( _X4 >>Int 8 >>Int 8 >>Int 8 >>Int 8)                               &Int 255) +Int 256 *Int (
+                  (( _X5 >>Int 8 >>Int 8 >>Int 8 >>Int 8 >>Int 8)                     &Int 255) +Int 256 *Int (
+                    (( _X6 >>Int 8 >>Int 8 >>Int 8 >>Int 8 >>Int 8 >>Int 8)           &Int 255) +Int 256 *Int (
+                      (( _X7 >>Int 8 >>Int 8 >>Int 8 >>Int 8 >>Int 8 >>Int 8 >>Int 8) &Int 255)))))))))
+          <=Int bitmask64
+        => true
+    [simplification, preserves-definedness, symbolic]
+```
+
+
 For the case where the (symbolic) byte values are first converted to a number, the round-trip simplification requires different matching.
 First, the bit-masking with `&Int 255` eliminates `Bytes2Int(Int2Bytes(1, ..) +Bytes ..)` enclosing a byte-valued variable:
 

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

@@ -1506,6 +1506,7 @@ Casting a byte array/slice to an integer reinterprets the bytes in little-endian
   rule #littleEndianFromBytes(.List) => 0
   rule #littleEndianFromBytes(ListItem(Integer(BYTE, 8, false)) REST)
     => BYTE +Int 256 *Int #littleEndianFromBytes(REST)
+    [preserves-definedness]
 ```
 
 Casting an integer to a `[u8; N]` array materialises its little-endian bytes.

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

@@ -127,12 +127,14 @@ This truncation function is instrumental in the implementation of Integer arithm
           true
         )
     requires #bitWidth(INTTYPE) <=Int WIDTH
+    [preserves-definedness]
 
   // 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)
+    [preserves-definedness]
 
   // converting to unsigned int types (simple bitmask)
   rule #intAsType(VAL, _, UINTTYPE:UintTy)
@@ -142,6 +144,7 @@ This truncation function is instrumental in the implementation of Integer arithm
           #bitWidth(UINTTYPE),
           false
         )
+    [preserves-definedness]
 ```
 
 ## Alignment of Primitives

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

@@ -0,0 +1,9 @@
+#![feature(core_intrinsics)]
+#![feature(never_type)]
+use std::intrinsics::assert_inhabited;
+
+fn main() {
+    std::hint::black_box(
+        assert_inhabited::<!>() // Up to compiler/CodegenBackend to panic or NOOP
+    );
+}

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

@@ -1,12 +1,16 @@
 #![feature(core_intrinsics)]
-use std::intrinsics;
+use std::intrinsics::{self, assert_inhabited};
 
 fn main() {
     intrinsics::cold_path();
     let b = true;
     intrinsics::likely(b);
     intrinsics::unlikely(b);
     prefetch();
+    assert_inhabited::<i32>(); // Up to compiler/CodegenBackend to panic or NOOP
+    std::hint::black_box(
+        assert_inhabited::<()>() // Trying to stop being optimised away
+    );
 }
 
 fn prefetch() {