diff --git a/solarkraft/package-lock.json b/solarkraft/package-lock.json index 3df8220a..943a1a27 100644 --- a/solarkraft/package-lock.json +++ b/solarkraft/package-lock.json @@ -29,6 +29,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", @@ -2177,6 +2178,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", @@ -4628,6 +4714,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 84bfc9f8..3e04400c 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", @@ -57,6 +57,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/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..3e243e87 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(#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 + } + } } 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) + }) +})