Launch Apalache on monitor files

solarkraft/package.json

@@ -31,13 +31,13 @@
   ],
   "scripts": {
     "compile": "genversion -e src/version.ts && tsc",
-    "e2e": "./test/e2e/run-tests.sh",
+    "e2e": "mocha --loader=ts-node/esm test/e2e/**/*.test.ts",
     "format": "prettier --config .prettierrc 'src/**/*.ts' 'test/**/*.ts' --write",
     "license": "source-licenser --config-file licenser-config.yaml .",
     "lint": "eslint src test",
     "prepare": "cd .. && husky solarkraft/.husky",
     "snapshot": "git archive --format=tar.gz -o solarkraft-`git rev-parse --short HEAD`.tar.gz --prefix=solarkraft/ HEAD",
-    "test": "mocha --loader=ts-node/esm test/**/*.test.ts"
+    "test": "mocha --loader=ts-node/esm --exclude test/e2e/**/*.test.ts test/**/*.test.ts"
   },
   "dependencies": {
     "@sweet-monads/either": "^3.3.1",
@@ -56,6 +56,7 @@
     "genversion": "^3.2.0",
     "husky": "^9.0.11",
     "mocha": "^10.3.0",
+    "nexpect": "^0.6.0",
     "prettier": "^3.2.5",
     "ts-node": "^10.9.2",
     "typescript": "^5.4.5",

solarkraft/src/main.ts

@@ -48,11 +48,17 @@ const verifyCmd = {
     command: ['verify'],
     desc: 'verify a previously fetched transaction',
     builder: (yargs: any) =>
-        defaultOpts(yargs).option('txHash', {
-            desc: 'Transaction hash',
-            type: 'string',
-            demandOption: true,
-        }),
+        defaultOpts(yargs)
+            .option('txHash', {
+                desc: 'Transaction hash',
+                type: 'string',
+                demandOption: true,
+            })
+            .option('monitor', {
+                desc: 'Monitor to check against',
+                type: 'string',
+                demandOption: true,
+            }),
     handler: verify,
 }
 

solarkraft/src/verify.ts

@@ -6,10 +6,47 @@
  * Verify transactions fetched from the ledger
  * @param args the arguments parsed by yargs
  */
+
+import { spawnSync } from 'child_process'
+import { existsSync } from 'node:fs'
+import path from 'node:path'
+
+// TODO(#34): fix hardcoded path to Apalache
+const APALACHE_DIST = '/opt/apalache'
+const APALACHE_BIN = path.join(APALACHE_DIST, 'bin', 'apalache-mc')
+
 export function verify(args: any) {
     console.log(
         `*** WARNING: THIS IS A MOCK. NOTHING IS IMPLEMENTED YET. ***\n`
     )
     console.log(`Verifying transaction: ${args.txHash}...`)
-    console.log(`[OK]`)
+
+    if (!existsSync(args.monitor)) {
+        console.log(`The monitor file ${args.monitor} does not exist.`)
+        console.log('[Error]')
+        return
+    }
+
+    console.log(`Running Apalache (check ${args.monitor})...`)
+    const child = spawnSync(APALACHE_BIN, ['check', '--length=1', args.monitor])
+
+    switch (child.status) {
+        case 0: {
+            console.log('[OK]')
+            break
+        }
+        case 12: {
+            // Deadlock
+            console.log('Monitor is unable to reproduce the transaction')
+            console.log('[Fail]')
+            break
+        }
+        default: {
+            console.log(
+                `Internal error: Apalache failed with error code ${child.status}`
+            )
+            console.log('[Error]')
+            break
+        }
+    }
 }

solarkraft/test/e2e/tla/timelock_mon1.tla

@@ -0,0 +1,37 @@
+(*
+ * This specification ensures that the Timelock methods properly
+ * handle initialization.
+ *)
+---- MODULE timelock_mon1 ----
+VARIABLES
+    \* @type: Bool;
+    is_initialized,
+    \* @type: Str;
+    last_error
+
+Deposit(env, from, token, amount, claimants, time_bound) ==
+    \/ /\ ~is_initialized
+       /\ is_initialized' = TRUE
+       /\ last_error' = ""
+    \/ /\ is_initialized
+       /\ UNCHANGED is_initialized
+       /\ last_error' = "contract has been already initialized"
+
+Claim(env, claimant) ==
+    \/ /\ ~is_initialized
+       /\ UNCHANGED is_initialized
+       (* the contract simply panics instead of reporting a nice error *)
+       /\ last_error' = "contract is not initialized"
+    \/ /\ is_initialized
+       /\ UNCHANGED is_initialized
+       /\ last_error' \in {
+            "",
+            "time predicate is not fulfilled",
+            "claimant is not allowed to claim this balance"
+          }
+    (* the below behavior is not present in the contract *)
+    \/ /\ is_initialized
+       /\ is_initialized' = FALSE
+       /\ last_error' = "" 
+
+=============================

solarkraft/test/e2e/tla/timelock_mon1_instrumented_fail.tla

@@ -0,0 +1,14 @@
+---- MODULE timelock_mon1_instrumented_fail ----
+EXTENDS timelock_mon1
+
+Init ==
+    (* is_initialized is initialized from the current ledger state *)
+    /\ is_initialized = FALSE
+    /\ last_error = ""
+
+Next ==
+    (* the contract method being called along with its parameters *)
+    /\ Claim([ timestamp |-> 100 ], "alice")
+    (* the error message as produced by the contract invocation *)
+    /\ last_error' = "transaction simulation failed: host invocation failed"
+===========================================

solarkraft/test/e2e/tla/timelock_mon1_instrumented_okay.tla

@@ -0,0 +1,14 @@
+---- MODULE timelock_mon1_instrumented_okay ----
+EXTENDS timelock_mon1
+
+Init ==
+    (* is_initialized is initialized from the current ledger state *)
+    /\ is_initialized = FALSE
+    /\ last_error = ""
+
+Next ==
+    (* the contract method being called along with its parameters *)
+    /\ Claim([ timestamp |-> 100 ], "alice")
+    (* the error message as produced by the contract invocation *)
+    /\ last_error' = "contract is not initialized"
+===========================================

solarkraft/test/e2e/verify.test.ts

@@ -0,0 +1,33 @@
+// Integration tests for the `verify` command
+
+import { describe, it } from 'mocha'
+
+import { spawn } from 'nexpect'
+
+describe('verify', () => {
+    it('fails on missing file', function (done) {
+        spawn('solarkraft verify --txHash mimimi --monitor doesnotexist')
+            .wait('The monitor file doesnotexist does not exist.')
+            .expect('[Error]')
+            .run(done)
+    })
+
+    it('reports success on okay monitor', function (done) {
+        this.timeout(50000)
+        spawn(
+            'solarkraft verify --txHash mimimi --monitor test/e2e/tla/timelock_mon1_instrumented_okay.tla'
+        )
+            .wait('[OK]')
+            .run(done)
+    })
+
+    it('reports failure on deadlocking monitor', function (done) {
+        this.timeout(50000)
+        spawn(
+            'solarkraft verify --txHash mimimi --monitor test/e2e/tla/timelock_mon1_instrumented_fail.tla'
+        )
+            .wait('Monitor is unable to reproduce the transaction')
+            .expect('[Fail]')
+            .run(done)
+    })
+})