Refactor discriminant lookup

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

@@ -79,18 +79,14 @@ Definedness of the list and list elements is also guaranteed.
 For symbolic enum values, the variant index remains unevaluated but the original (symbolic) discriminant can be restored:
 
 ```k
-  syntax Int ::= size(Discriminants) [function, total]
-  rule size(.Discriminants) => 0
-  rule size(discriminant(_) REST) => 1 +Int size(REST)
-
-  rule #Ceil(#lookupDiscrAux(DISCRS:Discriminants, I:Int))
+  rule #Ceil(#lookupDiscrAux(DISCRS:Discriminants, variantIdx(I)))
     => #Ceil(DISCRS)
      #And #Ceil(I)
      #And {true #Equals 0 <=Int I}
      #And {true #Equals I <Int size(DISCRS)}
     [simplification]
 
-  rule #lookupDiscriminant(typeInfoEnumType(_, _, _, _, _), #findVariantIdxAux(DISCR, DISCRS, _IDX)) => DISCR
+  rule #lookupDiscrAux(DISCRS, #findVariantIdxAux(DISCR, DISCRS, _IDX)) => DISCR
     requires isOneOf(DISCR, DISCRS)
     [simplification, preserves-definedness, symbolic(DISCR)]
 

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

@@ -1111,21 +1111,31 @@ The `getTyOf` helper applies the projections from the `Place` to determine the `
     [preserves-definedness] // valid indexing and sort coercion
 
   syntax Evaluation ::= #discriminant ( Evaluation , MaybeTy ) [strict(1)]
+                      | #discriminantFor ( VariantIdx , TypeInfo )
   // ----------------------------------------------------------------
   rule <k> #discriminant(Aggregate(IDX, _), TY:Ty)
-        => Integer(#lookupDiscriminant(lookupTy(TY), IDX), 0, false) // HACK: bit width 0 means "flexible"
+        => #discriminantFor(IDX, lookupTy(TY))
+        ...
+        </k>
+
+  rule <k> #discriminantFor(variantIdx(I) #as IDX, typeInfoEnumType(_, _, DISCRIMINANTS:Discriminants, _, _))
+        => Integer(#lookupDiscrAux(DISCRIMINANTS, IDX), 0, false) // HACK: bit width 0 means "flexible"
         ...
        </k>
+    requires I <=Int size(DISCRIMINANTS)
+    [preserves-definedness]
 
-  syntax Int ::= #lookupDiscriminant ( TypeInfo , VariantIdx )  [function, total]
-               | #lookupDiscrAux ( Discriminants , Int ) [function]
-  // --------------------------------------------------------------------
-  rule #lookupDiscriminant(typeInfoEnumType(_, _, DISCRIMINANTS, _, _), variantIdx(IDX)) => #lookupDiscrAux(DISCRIMINANTS, IDX)
-    requires isInt(#lookupDiscrAux(DISCRIMINANTS, IDX)) [preserves-definedness]
-  rule #lookupDiscriminant(_OTHER, _) => 0 [owise, preserves-definedness] // default 0. May be undefined behaviour, though.
+  syntax Int ::= size(Discriminants) [function, total]
+  rule size(.Discriminants) => 0
+  rule size(discriminant(_) REST) => 1 +Int size(REST)
+
+  // default 0 for non-enum types. May be undefined behaviour, though.
+  // rule #discriminant(_, _) => 0 [owise]
+
+  syntax Int ::= #lookupDiscrAux ( Discriminants , VariantIdx ) [function]
   // --------------------------------------------------------------------
-  rule #lookupDiscrAux( discriminant(RESULT)         _        , IDX) => RESULT requires IDX ==Int 0
-  rule #lookupDiscrAux( _:Discriminant      MORE:Discriminants, IDX) => #lookupDiscrAux(MORE, IDX -Int 1) requires 0 <Int IDX [owise]
+  rule #lookupDiscrAux( discriminant(RESULT)         _        , variantIdx(I)) => RESULT requires I ==Int 0
+  rule #lookupDiscrAux( _:Discriminant      MORE:Discriminants, variantIdx(I)) => #lookupDiscrAux(MORE, variantIdx(I -Int 1)) requires 0 <Int I [owise]
 ```
 
 ```k

kmir/src/tests/integration/data/crate-tests/two-crate-bin/crate2::main.expected

@@ -2,7 +2,7 @@
 ┌─ 1 (root, init)
 │   #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC
 │
-│  (736 steps)
+│  (741 steps)
 ├─ 3 (terminal)
 │   #EndProgram ~> .K
 │

kmir/src/tests/integration/data/crate-tests/two-crate-dylib/crate2::test_crate1_with.expected

@@ -2,7 +2,7 @@
 ┌─ 1 (root, init)
 │   #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC
 │
-│  (216 steps)
+│  (217 steps)
 ├─ 3 (terminal)
 │   #EndProgram ~> .K
 │

kmir/src/tests/integration/data/prove-rs/show/interior-mut-fail.main.expected

@@ -3,7 +3,7 @@
 │   #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC
 │   span: 0
 │
-│  (877 steps)
+│  (879 steps)
 └─ 3 (stuck, leaf)
     #setUpCalleeData ( monoItemFn ( ... name: symbol ( "** UNKNOWN FUNCTION **" ) ,
     span: 32

kmir/src/tests/integration/data/prove-rs/show/iter_next_2-fail.main.expected

@@ -3,7 +3,7 @@
 │   #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC
 │   span: 0
 │
-│  (2000 steps)
+│  (2003 steps)
 └─ 3 (stuck, leaf)
     #traverseProjection ( toStack ( 1 , local ( 1 ) ) , Range ( .List ) , .Projectio
     span: 146

kmir/src/tests/integration/data/prove-rs/show/niche-enum.main.expected

@@ -3,7 +3,7 @@
 │   #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC
 │   span: 0
 │
-│  (740 steps)
+│  (750 steps)
 ├─ 3 (terminal)
 │   #EndProgram ~> .K
 │   function: main

kmir/src/tests/integration/data/prove-rs/show/transmute-u8-to-enum-changed-discriminant-signed-fail.main.expected

@@ -3,7 +3,7 @@
 │   #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC
 │   span: 0
 │
-│  (102 steps)
+│  (103 steps)
 └─ 3 (stuck, leaf)
     #traverseProjection ( toLocal ( 2 ) , thunk ( #decodeConstant ( constantKindAllo
     span: 153

kmir/src/tests/integration/test_integration.py

@@ -246,7 +246,7 @@ def test_crate_examples(main_crate: Path, kmir: KMIR, update_expected_output: bo
         EXEC_DATA_DIR / 'references' / 'weirdRefs.state',
         None,
     ),
-    ('enum-discriminants', EXEC_DATA_DIR / 'enum' / 'enum.smir.json', EXEC_DATA_DIR / 'enum' / 'enum.state', 136),
+    ('enum-discriminants', EXEC_DATA_DIR / 'enum' / 'enum.smir.json', EXEC_DATA_DIR / 'enum' / 'enum.state', 139),
     (
         'Array-indexing',
         EXEC_DATA_DIR / 'arrays' / 'array_indexing.smir.json',