implement the new operator "expect"

doc/lang.md

@@ -2,7 +2,7 @@
 
 | Revision | Date       | Author                                                  |
 |:---------|:-----------|:--------------------------------------------------------|
-| 34       | 09.10.2023 | Igor Konnov, Shon Feder, Jure Kukovec, Gabriela Moreira, Thomas Pani |
+| 35       | 12.12.2023 | Igor Konnov, Shon Feder, Jure Kukovec, Gabriela Moreira, Thomas Pani |
 
 This document presents language constructs in the same order as the [summary of
 TLA+](https://lamport.azurewebsites.net/tla/summary.pdf).
@@ -64,6 +64,7 @@ Table of Contents
       * [Then](#then)
       * [Reps](#reps)
         * [Example](#example)
+      * [Expect](#expect)
       * [Fail](#fail)
     * [Temporal operators](#temporal-operators)
       * [Always](#always)
@@ -1754,6 +1755,39 @@ to be disabled.
 
 *Mode:* Run.
 
+#### Expect
+
+The operator `expect` has the following syntax:
+
+```scala
+A.expect(P)
+expect(A, P)
+```
+
+The left-hand side `A` must be an action or a run. The right-hand side `P` must
+be a non-action Boolean expression.
+
+The semantics of this operator is as follows:
+
+- Evaluate action `A`:
+  - When `A`'s result is `false`, emit a runtime error.
+  - When `A`'s result is `true`:
+    - Commit the variable updates.
+    - Evaluate `P`:
+      - If `P` evaluates to `false`, emit a runtime error (similar to `assert`).
+      - If `P` evaluates to `true`, rollback to the previous state and return `true`.
+
+##### Example
+
+```bluespec
+var n: int
+run expectConditionOkTest = (n' = 0).then(n' = 3).expect(n == 3)
+run expectConditionFailsTest = (n' = 0).then(n' = 3).expect(n == 4)
+run expectRunFailsTest = (n' = 0).then(all { n == 2, n' = 3 }).expect(n == 4)
+```
+
+*Mode:* Run.
+
 ### Temporal operators
 
 Temporal operators describe infinite executions.

quint/src/builtin.qnt

@@ -795,6 +795,9 @@ module builtin {
   ///  - `a` is true for a step from `s1` to `s2`, and
   ///  - `b` holds true in `s2`.
   ///
+  /// If `a` evaluates to `false`, evaluation of `a.expect(b)`
+  /// fails with an error message.
+  ///
   /// ### Examples
   ///
   /// ```

quint/src/ir/quintIr.ts

@@ -136,6 +136,7 @@ export const builtinOpCodes = [
   'and',
   'append',
   'assert',
+  'expect',
   'assign',
   'chooseSome',
   'concat',

quint/src/runtime/impl/compilerImpl.ts

@@ -920,6 +920,10 @@ export class CompilerVisitor implements IRVisitor {
           })
           break
 
+        case 'expect':
+          this.translateExpect(app)
+          break
+
         case 'assert':
           this.applyFun(app.id, 1, cond => {
             if (!cond.toBool()) {
@@ -1303,6 +1307,57 @@ export class CompilerVisitor implements IRVisitor {
     this.compStack.push(mkFunComputable(lazyCompute))
   }
 
+  // Translate A.expect(P):
+  //  - Evaluate A.
+  //  - When A's result is 'false', emit a runtime error.
+  //  - When A's result is 'true':
+  //    - Commit the variable updates: Shift the primed variables to unprimed.
+  //    - Evaluate `P`.
+  //    - If `P` evaluates to `false`, emit a runtime error (similar to `assert`).
+  //    - If `P` evaluates to `true`, rollback to the previous state and return `true`.
+  private translateExpect(app: ir.QuintApp): void {
+    // The code below is an adaption of chainAllOrThen.
+    // If someone finds how to nicely combine both, please refactor.
+    if (this.compStack.length !== 2) {
+      this.errorTracker.addCompileError(app.id, 'QNT501', `Not enough arguments on stack for "${app.opcode}"`)
+      return
+    }
+    const [action, pred] = this.compStack.splice(-2)
+    const lazyCompute = (): Maybe<EvalResult> => {
+      const savedNextVars = this.snapshotNextVars()
+      const savedTrace = this.trace()
+      const actionResult = action.eval()
+      if (actionResult.isNone() || !(actionResult.value as RuntimeValue).toBool()) {
+        // 'A' evaluates to 'false', or produces an error.
+        // Restore the values of the next variables.
+        this.recoverNextVars(savedNextVars)
+        this.resetTrace(just(rv.mkList(savedTrace)))
+        // expect emits an error when the run could not finish
+        this.errorTracker.addRuntimeError(app.args[0].id, 'QNT508', 'Cannot continue to "expect"')
+        return none()
+      } else {
+        // temporarily, switch to the next frame, to make a look-ahead evaluation
+        const savedVarsAfterAction = this.snapshotVars()
+        const savedNextVarsAfterAction = this.snapshotNextVars()
+        const savedTraceAfterAction = this.trace()
+        this.shiftVars()
+        // evaluate P
+        const predResult = pred.eval()
+        // rollback to the previous state in any case
+        this.recoverVars(savedVarsAfterAction)
+        this.recoverNextVars(savedNextVarsAfterAction)
+        this.resetTrace(just(rv.mkList(savedTraceAfterAction)))
+        if (predResult.isNone() || !(predResult.value as RuntimeValue).toBool()) {
+          this.errorTracker.addRuntimeError(app.args[1].id, 'QNT508', 'Expect condition does not hold true')
+          return none()
+        }
+        return predResult
+      }
+    }
+
+    this.compStack.push(mkFunComputable(lazyCompute))
+  }
+
   // translate n.reps(A)
   private translateReps(app: ir.QuintApp): void {
     if (this.compStack.length < 2) {

quint/test/runtime/compile.test.ts

@@ -999,6 +999,28 @@ describe('compiling specs to runtime values', () => {
       assertVarAfterCall('n', '3', 'run1', input)
     })
 
+    it('expect fails when left-hand side is false', () => {
+      const input = dedent(
+        `var n: int
+        |run run1 = (n' = 0).then(all { n == 1, n' = 3 }).expect(n < 3)
+        `
+      )
+
+      evalVarAfterCall('n', 'run1', input)
+        .mapRight(m => assert.fail(`Expected the run to fail, found: ${m}`))
+    })
+
+    it('expect and then expect fail', () => {
+      const input = dedent(
+        `var n: int
+        |run run1 = (n' = 0).then(n' = 3).expect(n == 3).then(n' = 4).expect(n == 3)
+        `
+      )
+
+      evalVarAfterCall('n', 'run1', input)
+        .mapRight(m => assert.fail(`Expected the run to fail, found: ${m}`))
+    })
+
     it('q::debug', () => {
       // `q::debug(s, a)` returns `a`
       const input = dedent(