Merge pull request #1670 from informalsystems/gabriela/stubborn-oneOf

Make `oneOf()` more stubborn

Author: bugarela

CHANGELOG.md

@@ -15,6 +15,9 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 - `quint run` now reports statistics on trace length and the simulation speec in traces/second (#1669)
 
 ### Changed
+
+- `oneOf()` now automatically handles empty sets instead of giving an error and has a retry strategy for small sets (#1670)
+
 ### Deprecated
 ### Removed
 ### Fixed

quint/cli-tests.md

@@ -310,7 +310,6 @@ fi
 <!-- !test check simplePonzi - Run progressInv -->
     quint run \
       --invariant=progressInv --main=simplePonziTest \
-      --seed=0x1f035d45bcece7 \
       ../examples/solidity/SimplePonzi/simplePonzi.qnt
 
 ### OK on run gradualPonzi::noNegativeInv
@@ -327,7 +326,7 @@ fi
 <!-- !test check gradualPonzi - Run progressInv -->
     quint run --invariant=progressInv --main=gradualPonziTest \
       --max-samples=1000 --max-steps=50 \
-      --seed=0x18df4a4a4f958b \
+      --seed=0x144e3011359c7f \
       ../examples/solidity/GradualPonzi/gradualPonzi.qnt
 
 ### FAIL on run gradualPonzi::noLeftoversInv

quint/io-cli-tests.md

@@ -534,9 +534,9 @@ An example execution:
 
 [State 1]
 {
-  balances: Map("alice" -> 0, "bob" -> 0, "charlie" -> -75),
+  balances: Map("alice" -> 0, "bob" -> 0, "charlie" -> -53),
   mbt::actionTaken: "withdraw",
-  mbt::nondetPicks: { account: Some("charlie"), amount: Some(75) }
+  mbt::nondetPicks: { account: Some("charlie"), amount: Some(53) }
 }
 
 [violation] Found an issue (duration).
@@ -631,7 +631,7 @@ The command `run` finds an overflow in Coin.
 
 <!-- !test in run finds overflow -->
 ```
-output=$(quint run --max-steps=5 --seed=0x1e352e160ffb15 --invariant=totalSupplyDoesNotOverflowInv \
+output=$(quint run --max-steps=5 --seed=0x1e352e16100007 --invariant=totalSupplyDoesNotOverflowInv \
   ../examples/tutorials/coin.qnt 2>&1)
 exit_code=$?
 echo "$output" | sed -e 's/([0-9]*ms.*)/(duration)/g' -e 's#^.*coin.qnt#      HOME/coin.qnt#g'
@@ -647,41 +647,41 @@ An example execution:
 {
   balances:
     Map("alice" -> 0, "bob" -> 0, "charlie" -> 0, "eve" -> 0, "null" -> 0),
-  minter: "alice"
+  minter: "bob"
 }
 
 [State 1]
 {
   balances:
     Map(
-      "alice" ->
-        94541396474536885635239092281406920580729946306097367569491485195445962194366,
+      "alice" -> 0,
       "bob" -> 0,
       "charlie" -> 0,
-      "eve" -> 0,
+      "eve" ->
+        111865848465544047420411899136876802528313267264666266547206011867817131473571,
       "null" -> 0
     ),
-  minter: "alice"
+  minter: "bob"
 }
 
 [State 2]
 {
   balances:
     Map(
-      "alice" ->
-        94541396474536885635239092281406920580729946306097367569491485195445962194366,
+      "alice" -> 0,
       "bob" ->
-        53481678647226234506653603827987361074517460680431655489916483293654777859474,
+        106835923319054853476296948761788592011112700034147492144754744060268203518249,
       "charlie" -> 0,
-      "eve" -> 0,
+      "eve" ->
+        111865848465544047420411899136876802528313267264666266547206011867817131473571,
       "null" -> 0
     ),
-  minter: "alice"
+  minter: "bob"
 }
 
 [violation] Found an issue (duration).
 Use --verbosity=3 to show executions.
-Use --seed=0x1e352e160ffb15 to reproduce.
+Use --seed=0x1e352e16100007 to reproduce.
 error: Invariant violated
 ```
 
@@ -691,7 +691,7 @@ The command `run` finds an overflow in Coin and shows the operator calls.
 
 <!-- !test in run shows calls -->
 ```
-output=$(quint run --max-steps=5 --seed=0x1786e678d460ed \
+output=$(quint run --max-steps=5 --seed=0x136507ae9037f5 \
   --invariant=totalSupplyDoesNotOverflowInv \
   --verbosity=3 \
   ../examples/tutorials/coin.qnt 2>&1)
@@ -714,67 +714,61 @@ q::initAndInvariant => true
 {
   balances:
     Map("alice" -> 0, "bob" -> 0, "charlie" -> 0, "eve" -> 0, "null" -> 0),
-  minter: "alice"
+  minter: "eve"
 }
 
 [Frame 1]
 q::stepAndInvariant => true
 ├─ step => true
 │  └─ send(
+│       "eve",
 │       "alice",
-│       "null",
-│       78071281284846825193495013785477188646129629244112530489195111677146856342020
+│       10060541798179252735561881697278111912297141188982098138305297944456003639647
 │     ) => false
 │     └─ require(false) => false
 └─ isUInt(
-     78071281284846825193495013785477188646129629244112530489195111677146856342020
+     10060541798179252735561881697278111912297141188982098138305297944456003639647
    ) => true
 
 [State 1]
 {
   balances:
     Map(
-      "alice" -> 0,
+      "alice" ->
+        10060541798179252735561881697278111912297141188982098138305297944456003639647,
       "bob" -> 0,
       "charlie" -> 0,
       "eve" -> 0,
-      "null" ->
-        78071281284846825193495013785477188646129629244112530489195111677146856342020
+      "null" -> 0
     ),
-  minter: "alice"
+  minter: "eve"
 }
 
 [Frame 2]
 q::stepAndInvariant => false
 ├─ step => true
-│  └─ send(
-│       "alice",
-│       "charlie",
-│       71516992819340132902114648681722204450273946921092387316973942850220744245470
-│     ) => false
-│     └─ require(false) => false
 └─ isUInt(
-     149588274104186958095609662467199393096403576165204917806169054527367600587490
+     119924674537974698230049391428816171173783073186451018303718372310243659214259
    ) => false
 
 [State 2]
 {
   balances:
     Map(
-      "alice" -> 0,
+      "alice" ->
+        10060541798179252735561881697278111912297141188982098138305297944456003639647,
       "bob" -> 0,
       "charlie" ->
-        71516992819340132902114648681722204450273946921092387316973942850220744245470,
+        109864132739795445494487509731538059261485931997468920165413074365787655574612,
       "eve" -> 0,
-      "null" ->
-        78071281284846825193495013785477188646129629244112530489195111677146856342020
+      "null" -> 0
     ),
-  minter: "alice"
+  minter: "eve"
 }
 
 [violation] Found an issue (duration).
 Use --verbosity=3 to show executions.
-Use --seed=0x1786e678d460ed to reproduce.
+Use --seed=0x136507ae9037f5 to reproduce.
 error: Invariant violated
 ```
 
@@ -833,13 +827,13 @@ rm out-itf-mbt-example.itf.json
       [
         "charlie",
         {
-          "#bigint": "79626045751699704635016553258820412024546765398372583361896346889345270192783"
+          "#bigint": "0"
         }
       ],
       [
         "eve",
         {
-          "#bigint": "0"
+          "#bigint": "20086964742617499085873481662929437057498704222762050481882156750446625292787"
         }
       ],
       [
@@ -855,19 +849,19 @@ rm out-itf-mbt-example.itf.json
     "amount": {
       "tag": "Some",
       "value": {
-        "#bigint": "79626045751699704635016553258820412024546765398372583361896346889345270192783"
+        "#bigint": "20086964742617499085873481662929437057498704222762050481882156750446625292787"
       }
     },
     "receiver": {
       "tag": "Some",
-      "value": "charlie"
+      "value": "eve"
     },
     "sender": {
       "tag": "Some",
-      "value": "eve"
+      "value": "null"
     }
   },
-  "minter": "eve"
+  "minter": "null"
 }
 ```
 
@@ -1062,7 +1056,7 @@ cd - > /dev/null
 <!-- !test exit 1 -->
 <!-- !test in verbose test -->
 ```
-output=$(quint test --seed=0x1286bf2e1dacb3 --match=mintTwiceThenSendError \
+output=$(quint test --seed=0x1286bf2e1dad07 --match=mintTwiceThenSendError \
   --verbosity=3 ../examples/tutorials/coin.qnt)
 exit_code=$?
 echo "$output" | sed -e 's/([0-9]*ms)/(duration)/g' -e 's#^.*coin.qnt#      HOME/coin.qnt#g'
@@ -1086,45 +1080,45 @@ init => true
 
 [Frame 1]
 mint(
-  "bob",
+  "alice",
   "eve",
-  74252675173190743514494160784973331842148624838292266741626378055869698233769
+  59566460029516684323034576273723724420849386347074116311626296723707538074470
 ) => true
 ├─ require(true) => true
 └─ require(true) => true
    └─ isUInt(
-        74252675173190743514494160784973331842148624838292266741626378055869698233769
+        59566460029516684323034576273723724420849386347074116311626296723707538074470
       ) => true
 
 [Frame 2]
 mint(
+  "alice",
   "bob",
-  "bob",
-  97700478479458321253548605902971263977055085704583752584562220159652816914987
+  93368484419625019040077192713095698377461332472838851169076929942152020904440
 ) => true
 ├─ require(true) => true
 └─ require(true) => true
    └─ isUInt(
-        97700478479458321253548605902971263977055085704583752584562220159652816914987
+        93368484419625019040077192713095698377461332472838851169076929942152020904440
       ) => true
 
 [Frame 3]
 send(
   "eve",
   "bob",
-  47769583726968424739901588588333904197787985995488944788698867328177315688645
+  58557567944388148967996441447677399573201687288362292728576564719669790227709
 ) => false
 ├─ require(true) => true
 ├─ require(true) => true
 │  └─ isUInt(
-│       26483091446222318774592572196639427644360638842803321952927510727692382545124
+│       1008892085128535355038134826046324847647699058711823583049732004037747846761
 │     ) => true
 └─ require(false) => false
    └─ isUInt(
-        145470062206426745993450194491305168174843071700072697373261087487830132603632
+        151926052364013168008073634160773097950663019761201143897653494661821811132149
       ) => false
 
-    Use --seed=0x1286bf2e1dacb3 --match=mintTwiceThenSendError to repeat.
+    Use --seed=0x1286bf2e1dad07 --match=mintTwiceThenSendError to repeat.
 ```
 
 ### test fails on invalid seed

quint/src/environment.d.ts

@@ -0,0 +1,9 @@
+declare global {
+  namespace NodeJS {
+    interface ProcessEnv {
+      QUINT_RETRY_NONDET_SMALLER_THAN?: string
+    }
+  }
+}
+
+export {}

quint/src/runtime/impl/builder.ts

@@ -27,6 +27,7 @@ import { QuintApp, QuintEx, QuintVar } from '../../ir/quintIr'
 import { LookupDefinition, LookupTable } from '../../names/base'
 import { NamedRegister, VarStorage, initialRegisterValue } from './VarStorage'
 import { List } from 'immutable'
+import { evalNondet } from './nondet'
 
 /**
  * The type returned by the builder in its methods, which can be called to get the
@@ -308,24 +309,12 @@ function buildDefCore(builder: Builder, def: LookupDefinition): EvalFunction {
       const cachedValue = builder.scopedCachedValues.get(def.id)!
 
       const bodyEval = buildExpr(builder, def.expr)
-      if (def.qualifier === 'nondet') {
-        // Create an entry in the map for this nondet pick,
-        // as we want the resulting record to be the same at every state.
-        // Value is optional, and starts with undefined
-        builder.initialNondetPicks.set(def.name, undefined)
-      }
 
       return ctx => {
         if (cachedValue.value === undefined) {
           cachedValue.value = bodyEval(ctx)
         }
 
-        if (def.qualifier === 'nondet') {
-          cachedValue.value
-            .map(value => ctx.varStorage.nondetPicks.set(def.name, value))
-            .mapLeft(_ => ctx.varStorage.nondetPicks.set(def.name, undefined))
-        }
-
         return cachedValue.value
       }
     }
@@ -494,6 +483,32 @@ function buildExprCore(builder: Builder, expr: QuintEx): EvalFunction {
       }
     }
     case 'let': {
+      if (expr.opdef.qualifier === 'nondet') {
+        // For `nondet`, we want to retry the the `oneOf()` call in case the body returns false.
+        // So we take care of the compilation at the let-in level.
+
+        if (expr.opdef.expr.kind !== 'app') {
+          // impossible, added to make Typescript's type checker happy.
+          throw new Error('Impossible case: nondet let expression is not an app')
+        }
+
+        // Create an entry in the map for this nondet pick,
+        // as we want the resulting record to be the same at every state.
+        // Value is optional, and starts with undefined
+        builder.initialNondetPicks.set(expr.opdef.name, undefined)
+
+        // Set up cache and memo in the same way we do for regular let-ins.
+        // We don't need to add it to `scopedCachedValues` since we'll clear
+        // the cache in here
+        let cache: CachedValue = { value: undefined }
+        builder.memo.set(expr.opdef.id, _ => cache.value!)
+
+        const setEval = buildExpr(builder, expr.opdef.expr.args[0])
+        const bodyEval = buildExpr(builder, expr.expr)
+
+        return evalNondet(expr.opdef.name, cache, setEval, bodyEval)
+      }
+
       // First, we create a cached value (a register with optional value) for the definition in this let expression
       let cachedValue = builder.scopedCachedValues.get(expr.opdef.id)
       if (!cachedValue) {