From 7d64bfd9b7e53b99924b3f8ed866c2b5b9379eaf Mon Sep 17 00:00:00 2001 From: Thomas Pani Date: Mon, 6 May 2024 14:17:26 +0000 Subject: [PATCH 1/6] Add missing test artifact --- .../test/e2e/tla/timelock_state.itf.json | 25 +++++++++++++++++++ 1 file changed, 25 insertions(+) create mode 100644 solarkraft/test/e2e/tla/timelock_state.itf.json diff --git a/solarkraft/test/e2e/tla/timelock_state.itf.json b/solarkraft/test/e2e/tla/timelock_state.itf.json new file mode 100644 index 00000000..1d26d3f3 --- /dev/null +++ b/solarkraft/test/e2e/tla/timelock_state.itf.json @@ -0,0 +1,25 @@ +{ "#meta": { + "format": "ITF", + "varTypes": { + "balance": "Int", + "is_initialized": "Bool", + "last_error": "Str" + }, + "format-description": "https://apalache.informal.systems/docs/adr/015adr-trace.html", + "description": "Created by Apalache on Mon May 06 08:21:52 UTC 2024" + }, + "vars": [ + "is_initialized", + "last_error" + ], + "states": [ + { + "#meta": { + "index": 0 + }, + "balance": { "#bigint": "123" }, + "is_initialized": false, + "last_error": "" + } + ] +} \ No newline at end of file From 4af3a9ea49bcb6c746b75e0bf8820d441efa3a92 Mon Sep 17 00:00:00 2001 From: Thomas Pani Date: Mon, 6 May 2024 14:17:52 +0000 Subject: [PATCH 2/6] Fix printing --- 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 9b52e11b..98b83ac6 100644 --- a/solarkraft/src/verify.ts +++ b/solarkraft/src/verify.ts @@ -49,7 +49,7 @@ export function verify(args: any) { if (apalacheParse.status != 0) { console.error(`Parsing monitor file ${args.monitor} failed:`) - console.error(apalacheParse.stderr) + console.error(apalacheParse.stderr.toString()) return } From 43199745a8280262ca77748e1e469528cb6b0d36 Mon Sep 17 00:00:00 2001 From: Thomas Pani Date: Mon, 6 May 2024 14:18:38 +0000 Subject: [PATCH 3/6] Decode ITF bigint values --- solarkraft/src/instrument.ts | 19 ++++++++++++++++++- 1 file changed, 18 insertions(+), 1 deletion(-) diff --git a/solarkraft/src/instrument.ts b/solarkraft/src/instrument.ts index ceec15fd..cd7d3347 100644 --- a/solarkraft/src/instrument.ts +++ b/solarkraft/src/instrument.ts @@ -12,6 +12,23 @@ type Transaction = { error: string } +// Return true iff `o` is a Javascript object. +function isObject(o: any) { + return typeof o === 'object' && !Array.isArray(o) && o !== null +} + +// Decode an ITF value `value` into a Javascript value. +// TODO(#46): support composite types (sequence, tuple, record, set, map) +function decodeITFValue(value: any) { + if ( + isObject(value) && + Object.prototype.hasOwnProperty.call(value, '#bigint') + ) { + return parseInt(value['#bigint']) + } + return value +} + /** * Return a `State` from an ITF JSON object. * @param itf ITF JSON object, see https://apalache.informal.systems/docs/adr/015adr-trace.html @@ -27,7 +44,7 @@ export function stateFromItf(itf: any): State { .filter(([name]) => name != '#meta') .map(([name, value]) => ({ name: name, - value: value, + value: decodeITFValue(value), type: 'Tla' + varTypes[name], })) return state From 3311f4266721bbf8f4eb1b1bdada98a4a316870f Mon Sep 17 00:00:00 2001 From: Thomas Pani Date: Mon, 6 May 2024 14:19:00 +0000 Subject: [PATCH 4/6] Only instrument state variables that are delcared in the monitor spec --- solarkraft/src/instrument.ts | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/solarkraft/src/instrument.ts b/solarkraft/src/instrument.ts index cd7d3347..9c90b449 100644 --- a/solarkraft/src/instrument.ts +++ b/solarkraft/src/instrument.ts @@ -62,6 +62,13 @@ export function instrumentMonitor( state: State, tx: Transaction ): any { + // Only instrument state variables that are delcared in the monitor spec + // (otherwise we provoke type errors in Apalache Snowcat, via undeclared variables) + const declaredMonitorVariables = monitor.modules[0].declarations + .filter(({ kind }) => kind == 'TlaVarDecl') + .map(({ name }) => name) + state = state.filter(({ name }) => declaredMonitorVariables.includes(name)) + // Add a special variable `last_error` that tracks error messages of failed transactions state.push({ name: 'last_error', type: 'TlaStr', value: '' }) From b5700949210f0361d38a66e3a3872c697549e2f4 Mon Sep 17 00:00:00 2001 From: Thomas Pani Date: Mon, 6 May 2024 14:19:19 +0000 Subject: [PATCH 5/6] Add test with second monitor --- solarkraft/test/e2e/tla/timelock_mon2.tla | 24 +++++++++++++++++++++++ solarkraft/test/e2e/verify.test.ts | 13 ++++++++++-- 2 files changed, 35 insertions(+), 2 deletions(-) create mode 100644 solarkraft/test/e2e/tla/timelock_mon2.tla diff --git a/solarkraft/test/e2e/tla/timelock_mon2.tla b/solarkraft/test/e2e/tla/timelock_mon2.tla new file mode 100644 index 00000000..7be57adc --- /dev/null +++ b/solarkraft/test/e2e/tla/timelock_mon2.tla @@ -0,0 +1,24 @@ +(* + * This specification ensures that a token is properly + * deposited and claimed. + *) +---- MODULE timelock_mon2 ---- +VARIABLES + \* @type: Int; + balance, + \* @type: Str; + last_error + +Deposit(env, from, token, amount, claimants, time_bound) == + \/ /\ balance' = amount + /\ last_error' = "" + \/ /\ UNCHANGED balance + /\ last_error' = "contract is not initialized" + +Claim(env, claimant) == + \/ /\ UNCHANGED balance + /\ last_error' \in { "", "contract is not initialized" } + \/ /\ balance' = 0 + /\ last_error' = "" + +============================= \ No newline at end of file diff --git a/solarkraft/test/e2e/verify.test.ts b/solarkraft/test/e2e/verify.test.ts index 9975edaf..f56af7bb 100644 --- a/solarkraft/test/e2e/verify.test.ts +++ b/solarkraft/test/e2e/verify.test.ts @@ -14,10 +14,19 @@ describe('verify', () => { .run(done) }) - it('reports success on okay monitor', function (done) { + it('reports success on okay monitor1', function (done) { this.timeout(50000) spawn( - 'solarkraft verify --txHash mimimi --monitor test/e2e/tla/timelock_mon1_instrumented_okay.tla --state test/e2e/tla/timelock_state.itf.json' + 'solarkraft verify --txHash mimimi --monitor test/e2e/tla/timelock_mon1.tla --state test/e2e/tla/timelock_state.itf.json' + ) + .wait('[OK]') + .run(done) + }) + + it('reports success on okay monitor2', function (done) { + this.timeout(50000) + spawn( + 'solarkraft verify --txHash mimimi --monitor test/e2e/tla/timelock_mon2.tla --state test/e2e/tla/timelock_state.itf.json' ) .wait('[OK]') .run(done) From 9b9518fa5ccbc9c5b49e627768dde8afc0ecac21 Mon Sep 17 00:00:00 2001 From: Thomas Pani Date: Mon, 6 May 2024 14:38:29 +0000 Subject: [PATCH 6/6] Fix unit test --- solarkraft/test/unit/instrument.test.ts | 37 ++++++++++++++++++- .../test/unit/verify.instrumentedMonitor.ts | 4 ++ 2 files changed, 39 insertions(+), 2 deletions(-) diff --git a/solarkraft/test/unit/instrument.test.ts b/solarkraft/test/unit/instrument.test.ts index 62ad9c6a..6a72a8a1 100644 --- a/solarkraft/test/unit/instrument.test.ts +++ b/solarkraft/test/unit/instrument.test.ts @@ -9,9 +9,42 @@ import { instrumentedMonitor as expected } from './verify.instrumentedMonitor.js describe('Apalache JSON instrumentor', () => { it('instruments TLA+ monitors', () => { - const monitor = { modules: [{ declarations: [] }] } + const monitor = { + modules: [ + { + declarations: [ + { kind: 'TlaVarDecl', name: 'is_initialized' }, + ], + }, + ], + } + const state = [ + { name: 'is_initialized', type: 'TlaBool', value: false }, + ] + const tx = { + functionName: 'Claim', + functionArgs: [{ type: 'TlaStr', value: 'alice' }], + env: { timestamp: 100 }, + error: 'contract is not initialized', + } + + const instrumented = instrumentMonitor(monitor, state, tx) + assert.deepEqual(expected, instrumented) + }) + + it('only instruments variables declared in the monitor', () => { + const monitor = { + modules: [ + { + declarations: [ + { kind: 'TlaVarDecl', name: 'is_initialized' }, + ], + }, + ], + } const state = [ { name: 'is_initialized', type: 'TlaBool', value: false }, + { name: 'additional_variable', type: 'TlaBool', value: false }, ] const tx = { functionName: 'Claim', @@ -21,6 +54,6 @@ describe('Apalache JSON instrumentor', () => { } const instrumented = instrumentMonitor(monitor, state, tx) - assert.deepEqual(instrumented, expected) + assert.deepEqual(expected, instrumented) }) }) diff --git a/solarkraft/test/unit/verify.instrumentedMonitor.ts b/solarkraft/test/unit/verify.instrumentedMonitor.ts index 63e74151..fd69457a 100644 --- a/solarkraft/test/unit/verify.instrumentedMonitor.ts +++ b/solarkraft/test/unit/verify.instrumentedMonitor.ts @@ -2,6 +2,10 @@ const instrumentedMonitor = { modules: [ { declarations: [ + { + kind: 'TlaVarDecl', + name: 'is_initialized', + }, { kind: 'TlaOperDecl', name: 'Init',