From 6dee786b095ca18806004bfc931932417e2615fe Mon Sep 17 00:00:00 2001 From: Thomas Pani Date: Fri, 19 Apr 2024 10:48:14 +0000 Subject: [PATCH 1/4] Launch Apalache on `verify` --- solarkraft/src/main.ts | 16 +++++++++++----- solarkraft/src/verify.ts | 39 ++++++++++++++++++++++++++++++++++++++- 2 files changed, 49 insertions(+), 6 deletions(-) diff --git a/solarkraft/src/main.ts b/solarkraft/src/main.ts index ecc69d78..c1395f5a 100644 --- a/solarkraft/src/main.ts +++ b/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, } diff --git a/solarkraft/src/verify.ts b/solarkraft/src/verify.ts index 5262e56d..d3adb86b 100644 --- a/solarkraft/src/verify.ts +++ b/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: 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', 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 + } + } } From 8015f875268b89add891df221974342557670969 Mon Sep 17 00:00:00 2001 From: Thomas Pani Date: Fri, 19 Apr 2024 10:53:07 +0000 Subject: [PATCH 2/4] Add e2e tests --- solarkraft/package-lock.json | 152 ++++++++++++++++++ solarkraft/package.json | 5 +- solarkraft/test/e2e/tla/timelock_mon1.tla | 37 +++++ .../tla/timelock_mon1_instrumented_fail.tla | 14 ++ .../tla/timelock_mon1_instrumented_okay.tla | 14 ++ solarkraft/test/e2e/verify.test.ts | 33 ++++ 6 files changed, 253 insertions(+), 2 deletions(-) create mode 100644 solarkraft/test/e2e/tla/timelock_mon1.tla create mode 100644 solarkraft/test/e2e/tla/timelock_mon1_instrumented_fail.tla create mode 100644 solarkraft/test/e2e/tla/timelock_mon1_instrumented_okay.tla create mode 100644 solarkraft/test/e2e/verify.test.ts diff --git a/solarkraft/package-lock.json b/solarkraft/package-lock.json index 973869de..d20da494 100644 --- a/solarkraft/package-lock.json +++ b/solarkraft/package-lock.json @@ -28,6 +28,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", @@ -2171,6 +2172,91 @@ "node": ">=10" } }, + "node_modules/nexpect": { + "version": "0.6.0", + "resolved": "https://registry.npmjs.org/nexpect/-/nexpect-0.6.0.tgz", + "integrity": "sha512-gG4cO0zoNG+kaPesw516hPVEKLW3YizGU8UWMr5lpkHKOgoTWcu4sPQN7rWVAIL4Ck87zM4N8immPUhYPdDz3g==", + "dev": true, + "dependencies": { + "cross-spawn": "^6.0.5" + }, + "engines": { + "node": ">=6" + } + }, + "node_modules/nexpect/node_modules/cross-spawn": { + "version": "6.0.5", + "resolved": "https://registry.npmjs.org/cross-spawn/-/cross-spawn-6.0.5.tgz", + "integrity": "sha512-eTVLrBSt7fjbDygz805pMnstIs2VTBNkRm0qxZd+M7A5XDdxVRWO5MxGBXZhjY4cqLYLdtrGqRf8mBPmzwSpWQ==", + "dev": true, + "dependencies": { + "nice-try": "^1.0.4", + "path-key": "^2.0.1", + "semver": "^5.5.0", + "shebang-command": "^1.2.0", + "which": "^1.2.9" + }, + "engines": { + "node": ">=4.8" + } + }, + "node_modules/nexpect/node_modules/path-key": { + "version": "2.0.1", + "resolved": "https://registry.npmjs.org/path-key/-/path-key-2.0.1.tgz", + "integrity": "sha512-fEHGKCSmUSDPv4uoj8AlD+joPlq3peND+HRYyxFz4KPw4z926S/b8rIuFs2FYJg3BwsxJf6A9/3eIdLaYC+9Dw==", + "dev": true, + "engines": { + "node": ">=4" + } + }, + "node_modules/nexpect/node_modules/semver": { + "version": "5.7.2", + "resolved": "https://registry.npmjs.org/semver/-/semver-5.7.2.tgz", + "integrity": "sha512-cBznnQ9KjJqU67B52RMC65CMarK2600WFnbkcaiwWq3xy/5haFJlshgnpjovMVJ+Hff49d8GEn0b87C5pDQ10g==", + "dev": true, + "bin": { + "semver": "bin/semver" + } + }, + "node_modules/nexpect/node_modules/shebang-command": { + "version": "1.2.0", + "resolved": "https://registry.npmjs.org/shebang-command/-/shebang-command-1.2.0.tgz", + "integrity": "sha512-EV3L1+UQWGor21OmnvojK36mhg+TyIKDh3iFBKBohr5xeXIhNBcx8oWdgkTEEQ+BEFFYdLRuqMfd5L84N1V5Vg==", + "dev": true, + "dependencies": { + "shebang-regex": "^1.0.0" + }, + "engines": { + "node": ">=0.10.0" + } + }, + "node_modules/nexpect/node_modules/shebang-regex": { + "version": "1.0.0", + "resolved": "https://registry.npmjs.org/shebang-regex/-/shebang-regex-1.0.0.tgz", + "integrity": "sha512-wpoSFAxys6b2a2wHZ1XpDSgD7N9iVjg29Ph9uV/uaP9Ex/KXlkTZTeddxDPSYQpgvzKLGJke2UU0AzoGCjNIvQ==", + "dev": true, + "engines": { + "node": ">=0.10.0" + } + }, + "node_modules/nexpect/node_modules/which": { + "version": "1.3.1", + "resolved": "https://registry.npmjs.org/which/-/which-1.3.1.tgz", + "integrity": "sha512-HxJdYWq1MTIQbJ3nw0cqssHoTNU267KlrDuGZ1WYlxDStUtKUhOaJmh112/TZmHxxUfuJqPXSOm7tDyas0OSIQ==", + "dev": true, + "dependencies": { + "isexe": "^2.0.0" + }, + "bin": { + "which": "bin/which" + } + }, + "node_modules/nice-try": { + "version": "1.0.5", + "resolved": "https://registry.npmjs.org/nice-try/-/nice-try-1.0.5.tgz", + "integrity": "sha512-1nh45deeb5olNY7eX82BkPO7SSxR5SSYJiPTrTdFUVYwAl8CKMA5N9PjTYkHiRjisVcxcQ1HXdLhx2qxxJzLNQ==", + "dev": true + }, "node_modules/noms": { "version": "0.0.0", "resolved": "https://registry.npmjs.org/noms/-/noms-0.0.0.tgz", @@ -4617,6 +4703,72 @@ } } }, + "nexpect": { + "version": "0.6.0", + "resolved": "https://registry.npmjs.org/nexpect/-/nexpect-0.6.0.tgz", + "integrity": "sha512-gG4cO0zoNG+kaPesw516hPVEKLW3YizGU8UWMr5lpkHKOgoTWcu4sPQN7rWVAIL4Ck87zM4N8immPUhYPdDz3g==", + "dev": true, + "requires": { + "cross-spawn": "^6.0.5" + }, + "dependencies": { + "cross-spawn": { + "version": "6.0.5", + "resolved": "https://registry.npmjs.org/cross-spawn/-/cross-spawn-6.0.5.tgz", + "integrity": "sha512-eTVLrBSt7fjbDygz805pMnstIs2VTBNkRm0qxZd+M7A5XDdxVRWO5MxGBXZhjY4cqLYLdtrGqRf8mBPmzwSpWQ==", + "dev": true, + "requires": { + "nice-try": "^1.0.4", + "path-key": "^2.0.1", + "semver": "^5.5.0", + "shebang-command": "^1.2.0", + "which": "^1.2.9" + } + }, + "path-key": { + "version": "2.0.1", + "resolved": "https://registry.npmjs.org/path-key/-/path-key-2.0.1.tgz", + "integrity": "sha512-fEHGKCSmUSDPv4uoj8AlD+joPlq3peND+HRYyxFz4KPw4z926S/b8rIuFs2FYJg3BwsxJf6A9/3eIdLaYC+9Dw==", + "dev": true + }, + "semver": { + "version": "5.7.2", + "resolved": "https://registry.npmjs.org/semver/-/semver-5.7.2.tgz", + "integrity": "sha512-cBznnQ9KjJqU67B52RMC65CMarK2600WFnbkcaiwWq3xy/5haFJlshgnpjovMVJ+Hff49d8GEn0b87C5pDQ10g==", + "dev": true + }, + "shebang-command": { + "version": "1.2.0", + "resolved": "https://registry.npmjs.org/shebang-command/-/shebang-command-1.2.0.tgz", + "integrity": "sha512-EV3L1+UQWGor21OmnvojK36mhg+TyIKDh3iFBKBohr5xeXIhNBcx8oWdgkTEEQ+BEFFYdLRuqMfd5L84N1V5Vg==", + "dev": true, + "requires": { + "shebang-regex": "^1.0.0" + } + }, + "shebang-regex": { + "version": "1.0.0", + "resolved": "https://registry.npmjs.org/shebang-regex/-/shebang-regex-1.0.0.tgz", + "integrity": "sha512-wpoSFAxys6b2a2wHZ1XpDSgD7N9iVjg29Ph9uV/uaP9Ex/KXlkTZTeddxDPSYQpgvzKLGJke2UU0AzoGCjNIvQ==", + "dev": true + }, + "which": { + "version": "1.3.1", + "resolved": "https://registry.npmjs.org/which/-/which-1.3.1.tgz", + "integrity": "sha512-HxJdYWq1MTIQbJ3nw0cqssHoTNU267KlrDuGZ1WYlxDStUtKUhOaJmh112/TZmHxxUfuJqPXSOm7tDyas0OSIQ==", + "dev": true, + "requires": { + "isexe": "^2.0.0" + } + } + } + }, + "nice-try": { + "version": "1.0.5", + "resolved": "https://registry.npmjs.org/nice-try/-/nice-try-1.0.5.tgz", + "integrity": "sha512-1nh45deeb5olNY7eX82BkPO7SSxR5SSYJiPTrTdFUVYwAl8CKMA5N9PjTYkHiRjisVcxcQ1HXdLhx2qxxJzLNQ==", + "dev": true + }, "noms": { "version": "0.0.0", "resolved": "https://registry.npmjs.org/noms/-/noms-0.0.0.tgz", diff --git a/solarkraft/package.json b/solarkraft/package.json index 2f3c526f..d3b057c0 100644 --- a/solarkraft/package.json +++ b/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", diff --git a/solarkraft/test/e2e/tla/timelock_mon1.tla b/solarkraft/test/e2e/tla/timelock_mon1.tla new file mode 100644 index 00000000..2ad32a00 --- /dev/null +++ b/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' = "" + +============================= diff --git a/solarkraft/test/e2e/tla/timelock_mon1_instrumented_fail.tla b/solarkraft/test/e2e/tla/timelock_mon1_instrumented_fail.tla new file mode 100644 index 00000000..e309b313 --- /dev/null +++ b/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" +=========================================== \ No newline at end of file diff --git a/solarkraft/test/e2e/tla/timelock_mon1_instrumented_okay.tla b/solarkraft/test/e2e/tla/timelock_mon1_instrumented_okay.tla new file mode 100644 index 00000000..6d9cfd2c --- /dev/null +++ b/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" +=========================================== \ No newline at end of file diff --git a/solarkraft/test/e2e/verify.test.ts b/solarkraft/test/e2e/verify.test.ts new file mode 100644 index 00000000..d84c5ac3 --- /dev/null +++ b/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) + }) +}) From d54a95afb350509efa90de11a8513e50c399338e Mon Sep 17 00:00:00 2001 From: Thomas Pani Date: Fri, 19 Apr 2024 12:48:44 +0000 Subject: [PATCH 3/4] Check executions up to length 1 --- solarkraft/src/verify.ts | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/solarkraft/src/verify.ts b/solarkraft/src/verify.ts index d3adb86b..d6a5a8b0 100644 --- a/solarkraft/src/verify.ts +++ b/solarkraft/src/verify.ts @@ -28,7 +28,7 @@ export function verify(args: any) { } console.log(`Running Apalache (check ${args.monitor})...`) - const child = spawnSync(APALACHE_BIN, ['check', args.monitor]) + const child = spawnSync(APALACHE_BIN, ['check', '--length=1', args.monitor]) switch (child.status) { case 0: { From 30a1b6a3c7536e287e8d1dff26afdf52c9878a17 Mon Sep 17 00:00:00 2001 From: Thomas Pani Date: Fri, 19 Apr 2024 12:51:02 +0000 Subject: [PATCH 4/4] Record issue --- solarkraft/src/verify.ts | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/solarkraft/src/verify.ts b/solarkraft/src/verify.ts index d6a5a8b0..3e243e87 100644 --- a/solarkraft/src/verify.ts +++ b/solarkraft/src/verify.ts @@ -11,7 +11,7 @@ import { spawnSync } from 'child_process' import { existsSync } from 'node:fs' import path from 'node:path' -// TODO: fix hardcoded path to Apalache +// TODO(#34): fix hardcoded path to Apalache const APALACHE_DIST = '/opt/apalache' const APALACHE_BIN = path.join(APALACHE_DIST, 'bin', 'apalache-mc')