Updates from master (#932)

* Control `haskell_threads` via `max-workers` option
* README upate
* Discriminant refactoring

Author: jberthold

README.md

@@ -9,7 +9,13 @@ Also included is the `kmir` tool, a python script that acts as a front-end to th
 
 ### KMIR Setup
 
-Pre-requisites: `python >= 3.10`, [`uv`](https://docs.astral.sh/uv/), `pip >= 20.0.2`, `gcc >= 11.4.0`, `cargo == nightly-2024-11-29`, `k >= v7.1.205`. To install K, follow the steps available in [K's Quick Start instructions](https://github.com/runtimeverification/k?tab=readme-ov-file#quick-start). 
+Pre-requisites:
+- `python >= 3.10`
+- [`uv`](https://docs.astral.sh/uv/)
+- `pip >= 20.0.2`
+- `gcc >= 11.4.0`
+- `cargo == nightly-2024-11-29`
+- K. The required K version is specified in `deps/k_release`. To install K, follow the steps available in [K's Quick Start instructions](https://github.com/runtimeverification/k?tab=readme-ov-file#quick-start).
 
 ```bash
 make build

kmir/src/kmir/_prove.py

@@ -149,6 +149,7 @@ def _prove_parallel(
             'module_name': kmir.definition.main_module_name,
             'bug_report': kmir.bug_report,
             'simplify_each': 30,
+            'haskell_threads': opts.max_workers,
         }
     ) as server:
 

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