Hotfix discriminant refactor 2 (#930)

* reverts the rewrite counts in the golden files (by removing the
rewrite symbol introduced in #923
* new helper functions to ensure definedness of discriminant/variantIdx
lookup
* Fixes p-token proofs (while still passing sync_native in SPL token)

Author: jberthold

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

@@ -86,10 +86,14 @@ For symbolic enum values, the variant index remains unevaluated but the original
      #And {true #Equals I <Int size(DISCRS)}
     [simplification]
 
-  rule #lookupDiscrAux(DISCRS, #findVariantIdxAux(DISCR, DISCRS, _IDX)) => DISCR
+  rule #lookupDiscrAux(_, #findVariantIdxAux(DISCR, DISCRS, _IDX)) => DISCR
     requires isOneOf(DISCR, DISCRS)
     [simplification, preserves-definedness, symbolic(DISCR)]
 
+  rule asInt(#findVariantIdxAux(DISCR, DISCRS, C)) <Int X => size(DISCRS) +Int C <=Int X
+    requires isOneOf(DISCR, DISCRS)
+    [simplification, symbolic(DISCR)]
+
   syntax Bool ::= isOneOf ( Int , Discriminants ) [function, total]
   // --------------------------------------------------------------
   rule isOneOf( _,                       .Discriminants                      ) => false

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

@@ -1111,31 +1111,37 @@ 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)
-        => #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"
+        => Integer(#lookupDiscrAux(discriminantsOf(lookupTy(TY)), IDX), 0, false) // HACK: bit width 0 means "flexible"
         ...
        </k>
-    requires I <=Int size(DISCRIMINANTS)
+    requires asInt(IDX) <Int size(discriminantsOf(lookupTy(TY)))
+     andBool 0 <=Int asInt(IDX) // must not be `err(_)`
+     andBool 0 <Int size(discriminantsOf(lookupTy(TY))) // must be an enum
     [preserves-definedness]
 
+  // // default 0 for non-enum types. May be undefined behaviour, though.
+  // rule #discriminant(_, _) => Integer(0, 0, false) [priority(100)]
+
+  syntax Int ::= asInt( VariantIdx ) [function, total]
+  // -------------------------------------------------
+  rule asInt(variantIdx(I)) => I
+  rule asInt(err(_)) => -1 // HAAAAAAACK
+
   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 Discriminants ::= discriminantsOf( TypeInfo ) [function, total]
+  // -------------------------------------------------------------------
+  rule discriminantsOf(typeInfoEnumType(_, _, DISCRIMINANTS, _, _)) => DISCRIMINANTS
+  rule discriminantsOf(            _OTHER_                        ) => .Discriminants [owise]
 
   syntax Int ::= #lookupDiscrAux ( Discriminants , VariantIdx ) [function]
   // --------------------------------------------------------------------
   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]
+  rule #lookupDiscrAux( _:Discriminant      MORE:Discriminants, variantIdx(I)) => #lookupDiscrAux(MORE, variantIdx(I -Int 1)) requires 0 <Int I
 ```
 
 ```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
 │
-│  (741 steps)
+│  (736 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
 │
-│  (217 steps)
+│  (216 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
 │
-│  (879 steps)
+│  (877 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
 │
-│  (2003 steps)
+│  (2000 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
 │
-│  (750 steps)
+│  (740 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
 │
-│  (103 steps)
+│  (102 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', 139),
+    ('enum-discriminants', EXEC_DATA_DIR / 'enum' / 'enum.smir.json', EXEC_DATA_DIR / 'enum' / 'enum.state', 136),
     (
         'Array-indexing',
         EXEC_DATA_DIR / 'arrays' / 'array_indexing.smir.json',