From dcbe3f13b14b8d7ad59733d0eaf276fbaecf5f62 Mon Sep 17 00:00:00 2001 From: Thomas Pani Date: Mon, 29 Apr 2024 13:28:06 +0000 Subject: [PATCH 1/5] Programmatically instrument TLA+ monitor --- solarkraft/src/verify.ts | 155 ++++++++++++++++++++++++- solarkraft/test/unit/verify.test.ts | 170 ++++++++++++++++++++++++++++ 2 files changed, 321 insertions(+), 4 deletions(-) create mode 100644 solarkraft/test/unit/verify.test.ts diff --git a/solarkraft/src/verify.ts b/solarkraft/src/verify.ts index 3e243e87..47db184e 100644 --- a/solarkraft/src/verify.ts +++ b/solarkraft/src/verify.ts @@ -2,10 +2,6 @@ * @license * [Apache-2.0](https://github.com/freespek/solarkraft/blob/main/LICENSE) */ -/** - * Verify transactions fetched from the ledger - * @param args the arguments parsed by yargs - */ import { spawnSync } from 'child_process' import { existsSync } from 'node:fs' @@ -15,6 +11,157 @@ import path from 'node:path' const APALACHE_DIST = '/opt/apalache' const APALACHE_BIN = path.join(APALACHE_DIST, 'bin', 'apalache-mc') +/** + * Return an instrumented monitor specification. + * @param monitor A TLA+ monitor, as returned from `apalache typecheck --output=temp.json` + * @param state The blockchain state before executing the transaction / the monitor. + * @param tx The transaction being applied to `state`. + * @returns The instrumented TLA+ monitor. + */ +export function instrumentMonitor( + monitor: any, + state: State, + tx: Transaction +): any { + // Add a special variable `last_error` that tracks error messages of failed transactions + state.push({ name: 'last_error', type: 'TlaStr', value: '' }) + + // Declaration of "Init" (according to `state`) + const tlaInit = tlaJsonOperDecl__Conjunction( + 'Init', + state.map((binding) => + tlaJsonEq__NameEx__ValEx( + binding.name, + false, + tlaJsonValEx(binding.type, binding.value) + ) + ) + ) + + // Declaration of "Next" (according to `tx`) + const envRecord = tlaJsonRecord([ + { name: 'timestamp', kind: 'TlaInt', value: tx.env.timestamp }, + ]) + const txArgs = tx.functionArgs.map((v) => tlaJsonValEx(v.type, v.value)) + const tlaNext = tlaJsonOperDecl__Conjunction('Next', [ + tlaJsonApplication(tx.functionName, [envRecord].concat(txArgs)), + tlaJsonEq__NameEx__ValEx( + 'last_error', + true, + tlaJsonValEx('TlaStr', tx.error) + ), + ]) + + // Instantiate the monitor spec with declarations of "Init" and "Next" + const extendedDeclarations = monitor['modules'][0]['declarations'].concat([ + tlaInit, + tlaNext, + ]) + const extendedModule = { + ...monitor['modules'][0], + declarations: extendedDeclarations, + } + return { ...monitor, modules: [extendedModule] } +} + +/** + * Return an Apalache TLA+ operator declaration of the form `operDeclName` == `conjuncts`_0 /\ ... /\ `conjuncts`_n. + * @param operDeclName Operator name + * @param conjuncts Body conjuncts + * @returns The operator declaration in Apalache IR JSON: https://apalache.informal.systems/docs/adr/005adr-json.html + */ +function tlaJsonOperDecl__Conjunction( + operDeclName: string, + conjuncts: any +): any { + return { + type: 'Untyped', + kind: 'TlaOperDecl', + name: operDeclName, + formalParams: [], + isRecursive: false, + body: { + type: 'Untyped', + kind: 'OperEx', + oper: 'AND', + args: conjuncts, + }, + } +} + +/** + * Return an Apalache TLA+ name expression. + * @returns the name expression in Apalache IR JSON: https://apalache.informal.systems/docs/adr/005adr-json.html + */ +function tlaJsonNameEx(name: string): any { + return { type: 'Untyped', kind: 'NameEx', name: name } +} + +/** + * Return an Apalache TLA+ value expression. + * @param kind Apalache type (e.g., "TlaStr" or "TlaBool") + * @param value Expression value + * @returns The value expression in Apalache IR JSON: https://apalache.informal.systems/docs/adr/005adr-json.html + */ +function tlaJsonValEx(kind: string, value: any): any { + return { + type: 'Untyped', + kind: 'ValEx', + value: { kind: kind, value: value }, + } +} + +/** + * Return an Apalache TLA+ record. + * @param bindings Interleaved array of field names and field values. + * @returns The record in Apalache IR JSON: https://apalache.informal.systems/docs/adr/005adr-json.html + */ +function tlaJsonRecord(bindings: any): any { + return { + type: 'Untyped', + kind: 'OperEx', + oper: 'RECORD', + args: bindings.flatMap((binding) => [ + tlaJsonValEx('TlaStr', binding.name), + tlaJsonValEx(binding.kind, binding.value), + ]), + } +} + +/** + * Return an Apalache TLA+ operator application. + * @param operName Name of the operator to apply. + * @param args Application arguments + * @returns The operator application in Apalache IR JSON: https://apalache.informal.systems/docs/adr/005adr-json.html + */ +function tlaJsonApplication(operName: string, args: any): any { + return { + type: 'Untyped', + kind: 'OperEx', + oper: 'OPER_APP', + args: [tlaJsonNameEx(operName)].concat(args), + } +} + +/** + * Return an Apalache equality expression applied to a name expression LHS, and a value expression RHS, optionally priming the LHS. + * @param name LHS name. + * @param prime True iff `name` should appear primed in the expression. + * @param valEx RHS value. + * @returns The equality in Apalache IR JSON: https://apalache.informal.systems/docs/adr/005adr-json.html + */ +function tlaJsonEq__NameEx__ValEx(name: any, prime: boolean, valEx: any): any { + const nameEx = { type: 'Untyped', kind: 'NameEx', name: name } + const lhs = prime + ? { type: 'Untyped', kind: 'OperEx', oper: 'PRIME', args: [nameEx] } + : nameEx + return { type: 'Untyped', kind: 'OperEx', oper: 'EQ', args: [lhs, valEx] } +} + +/** + * Verify transactions fetched from the ledger + * @param args the arguments parsed by yargs + */ export function verify(args: any) { console.log( `*** WARNING: THIS IS A MOCK. NOTHING IS IMPLEMENTED YET. ***\n` diff --git a/solarkraft/test/unit/verify.test.ts b/solarkraft/test/unit/verify.test.ts new file mode 100644 index 00000000..faac7d1a --- /dev/null +++ b/solarkraft/test/unit/verify.test.ts @@ -0,0 +1,170 @@ +// an example unit test to copy from + +import { assert } from 'chai' +import { describe, it } from 'mocha' + +import { instrumentMonitor } from '../../src/verify.js' + +describe('verify command', () => { + it('instruments TLA+ monitors', () => { + const monitor = { modules: [{ declarations: [] }] } + 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) + const expected = { + modules: [ + { + declarations: [ + { + kind: 'TlaOperDecl', + name: 'Init', + type: 'Untyped', + formalParams: [], + isRecursive: false, + body: { + kind: 'OperEx', + oper: 'AND', + type: 'Untyped', + args: [ + { + kind: 'OperEx', + oper: 'EQ', + type: 'Untyped', + args: [ + { + kind: 'NameEx', + name: 'is_initialized', + type: 'Untyped', + }, + { + kind: 'ValEx', + type: 'Untyped', + value: { + kind: 'TlaBool', + value: false, + }, + }, + ], + }, + { + kind: 'OperEx', + oper: 'EQ', + type: 'Untyped', + args: [ + { + kind: 'NameEx', + name: 'last_error', + type: 'Untyped', + }, + { + kind: 'ValEx', + type: 'Untyped', + value: { + kind: 'TlaStr', + value: '', + }, + }, + ], + }, + ], + }, + }, + { + kind: 'TlaOperDecl', + name: 'Next', + type: 'Untyped', + formalParams: [], + isRecursive: false, + body: { + kind: 'OperEx', + oper: 'AND', + type: 'Untyped', + args: [ + { + kind: 'OperEx', + oper: 'OPER_APP', + type: 'Untyped', + args: [ + { + kind: 'NameEx', + name: 'Claim', + type: 'Untyped', + }, + { + kind: 'OperEx', + oper: 'RECORD', + type: 'Untyped', + args: [ + { + kind: 'ValEx', + type: 'Untyped', + value: { + kind: 'TlaStr', + value: 'timestamp', + }, + }, + { + kind: 'ValEx', + type: 'Untyped', + value: { + kind: 'TlaInt', + value: 100, + }, + }, + ], + }, + { + kind: 'ValEx', + type: 'Untyped', + value: { + kind: 'TlaStr', + value: 'alice', + }, + }, + ], + }, + { + kind: 'OperEx', + oper: 'EQ', + type: 'Untyped', + args: [ + { + kind: 'OperEx', + oper: 'PRIME', + type: 'Untyped', + args: [ + { + kind: 'NameEx', + name: 'last_error', + type: 'Untyped', + }, + ], + }, + { + kind: 'ValEx', + type: 'Untyped', + value: { + kind: 'TlaStr', + value: 'contract is not initialized', + }, + }, + ], + }, + ], + }, + }, + ], + }, + ], + } + assert.deepEqual(instrumented, expected) + }) +}) From 94ba9ea1457875940adb24a59e9687ab549429fc Mon Sep 17 00:00:00 2001 From: Thomas Pani Date: Mon, 29 Apr 2024 13:34:08 +0000 Subject: [PATCH 2/5] Add type declarations --- solarkraft/src/verify.ts | 11 +++++++++++ 1 file changed, 11 insertions(+) diff --git a/solarkraft/src/verify.ts b/solarkraft/src/verify.ts index 47db184e..a8212c74 100644 --- a/solarkraft/src/verify.ts +++ b/solarkraft/src/verify.ts @@ -11,6 +11,17 @@ import path from 'node:path' const APALACHE_DIST = '/opt/apalache' const APALACHE_BIN = path.join(APALACHE_DIST, 'bin', 'apalache-mc') +// TODO(#38): Replace stubs with ITF +type Value = { type: string; value: any } +type Binding = { name: string; type: string; value: any } +type State = Binding[] +type Transaction = { + functionName: string + functionArgs: Value[] + env: { timestamp: number } + error: string +} + /** * Return an instrumented monitor specification. * @param monitor A TLA+ monitor, as returned from `apalache typecheck --output=temp.json` From 54b3528e08f1bde8fc6ca22de5ef952c9fc4c65f Mon Sep 17 00:00:00 2001 From: Thomas Pani Date: Tue, 30 Apr 2024 09:30:33 +0000 Subject: [PATCH 3/5] Rename function --- solarkraft/src/verify.ts | 9 +++------ 1 file changed, 3 insertions(+), 6 deletions(-) diff --git a/solarkraft/src/verify.ts b/solarkraft/src/verify.ts index a8212c74..25bca9ba 100644 --- a/solarkraft/src/verify.ts +++ b/solarkraft/src/verify.ts @@ -38,7 +38,7 @@ export function instrumentMonitor( state.push({ name: 'last_error', type: 'TlaStr', value: '' }) // Declaration of "Init" (according to `state`) - const tlaInit = tlaJsonOperDecl__Conjunction( + const tlaInit = tlaJsonOperDecl__And( 'Init', state.map((binding) => tlaJsonEq__NameEx__ValEx( @@ -54,7 +54,7 @@ export function instrumentMonitor( { name: 'timestamp', kind: 'TlaInt', value: tx.env.timestamp }, ]) const txArgs = tx.functionArgs.map((v) => tlaJsonValEx(v.type, v.value)) - const tlaNext = tlaJsonOperDecl__Conjunction('Next', [ + const tlaNext = tlaJsonOperDecl__And('Next', [ tlaJsonApplication(tx.functionName, [envRecord].concat(txArgs)), tlaJsonEq__NameEx__ValEx( 'last_error', @@ -81,10 +81,7 @@ export function instrumentMonitor( * @param conjuncts Body conjuncts * @returns The operator declaration in Apalache IR JSON: https://apalache.informal.systems/docs/adr/005adr-json.html */ -function tlaJsonOperDecl__Conjunction( - operDeclName: string, - conjuncts: any -): any { +function tlaJsonOperDecl__And(operDeclName: string, conjuncts: any): any { return { type: 'Untyped', kind: 'TlaOperDecl', From 76d8ce12f3fb15c2d1e0e5dec6be29b445f4d38b Mon Sep 17 00:00:00 2001 From: Thomas Pani Date: Tue, 30 Apr 2024 09:31:25 +0000 Subject: [PATCH 4/5] Move expected test output --- .../test/unit/verify.instrumentedMonitor.ts | 148 ++++++++++++++++++ solarkraft/test/unit/verify.test.ts | 148 +----------------- 2 files changed, 150 insertions(+), 146 deletions(-) create mode 100644 solarkraft/test/unit/verify.instrumentedMonitor.ts diff --git a/solarkraft/test/unit/verify.instrumentedMonitor.ts b/solarkraft/test/unit/verify.instrumentedMonitor.ts new file mode 100644 index 00000000..63e74151 --- /dev/null +++ b/solarkraft/test/unit/verify.instrumentedMonitor.ts @@ -0,0 +1,148 @@ +const instrumentedMonitor = { + modules: [ + { + declarations: [ + { + kind: 'TlaOperDecl', + name: 'Init', + type: 'Untyped', + formalParams: [], + isRecursive: false, + body: { + kind: 'OperEx', + oper: 'AND', + type: 'Untyped', + args: [ + { + kind: 'OperEx', + oper: 'EQ', + type: 'Untyped', + args: [ + { + kind: 'NameEx', + name: 'is_initialized', + type: 'Untyped', + }, + { + kind: 'ValEx', + type: 'Untyped', + value: { + kind: 'TlaBool', + value: false, + }, + }, + ], + }, + { + kind: 'OperEx', + oper: 'EQ', + type: 'Untyped', + args: [ + { + kind: 'NameEx', + name: 'last_error', + type: 'Untyped', + }, + { + kind: 'ValEx', + type: 'Untyped', + value: { + kind: 'TlaStr', + value: '', + }, + }, + ], + }, + ], + }, + }, + { + kind: 'TlaOperDecl', + name: 'Next', + type: 'Untyped', + formalParams: [], + isRecursive: false, + body: { + kind: 'OperEx', + oper: 'AND', + type: 'Untyped', + args: [ + { + kind: 'OperEx', + oper: 'OPER_APP', + type: 'Untyped', + args: [ + { + kind: 'NameEx', + name: 'Claim', + type: 'Untyped', + }, + { + kind: 'OperEx', + oper: 'RECORD', + type: 'Untyped', + args: [ + { + kind: 'ValEx', + type: 'Untyped', + value: { + kind: 'TlaStr', + value: 'timestamp', + }, + }, + { + kind: 'ValEx', + type: 'Untyped', + value: { + kind: 'TlaInt', + value: 100, + }, + }, + ], + }, + { + kind: 'ValEx', + type: 'Untyped', + value: { + kind: 'TlaStr', + value: 'alice', + }, + }, + ], + }, + { + kind: 'OperEx', + oper: 'EQ', + type: 'Untyped', + args: [ + { + kind: 'OperEx', + oper: 'PRIME', + type: 'Untyped', + args: [ + { + kind: 'NameEx', + name: 'last_error', + type: 'Untyped', + }, + ], + }, + { + kind: 'ValEx', + type: 'Untyped', + value: { + kind: 'TlaStr', + value: 'contract is not initialized', + }, + }, + ], + }, + ], + }, + }, + ], + }, + ], +} + +export { instrumentedMonitor } diff --git a/solarkraft/test/unit/verify.test.ts b/solarkraft/test/unit/verify.test.ts index faac7d1a..cc87ab7a 100644 --- a/solarkraft/test/unit/verify.test.ts +++ b/solarkraft/test/unit/verify.test.ts @@ -5,6 +5,8 @@ import { describe, it } from 'mocha' import { instrumentMonitor } from '../../src/verify.js' +import { instrumentedMonitor as expected } from './verify.instrumentedMonitor.js' + describe('verify command', () => { it('instruments TLA+ monitors', () => { const monitor = { modules: [{ declarations: [] }] } @@ -19,152 +21,6 @@ describe('verify command', () => { } const instrumented = instrumentMonitor(monitor, state, tx) - const expected = { - modules: [ - { - declarations: [ - { - kind: 'TlaOperDecl', - name: 'Init', - type: 'Untyped', - formalParams: [], - isRecursive: false, - body: { - kind: 'OperEx', - oper: 'AND', - type: 'Untyped', - args: [ - { - kind: 'OperEx', - oper: 'EQ', - type: 'Untyped', - args: [ - { - kind: 'NameEx', - name: 'is_initialized', - type: 'Untyped', - }, - { - kind: 'ValEx', - type: 'Untyped', - value: { - kind: 'TlaBool', - value: false, - }, - }, - ], - }, - { - kind: 'OperEx', - oper: 'EQ', - type: 'Untyped', - args: [ - { - kind: 'NameEx', - name: 'last_error', - type: 'Untyped', - }, - { - kind: 'ValEx', - type: 'Untyped', - value: { - kind: 'TlaStr', - value: '', - }, - }, - ], - }, - ], - }, - }, - { - kind: 'TlaOperDecl', - name: 'Next', - type: 'Untyped', - formalParams: [], - isRecursive: false, - body: { - kind: 'OperEx', - oper: 'AND', - type: 'Untyped', - args: [ - { - kind: 'OperEx', - oper: 'OPER_APP', - type: 'Untyped', - args: [ - { - kind: 'NameEx', - name: 'Claim', - type: 'Untyped', - }, - { - kind: 'OperEx', - oper: 'RECORD', - type: 'Untyped', - args: [ - { - kind: 'ValEx', - type: 'Untyped', - value: { - kind: 'TlaStr', - value: 'timestamp', - }, - }, - { - kind: 'ValEx', - type: 'Untyped', - value: { - kind: 'TlaInt', - value: 100, - }, - }, - ], - }, - { - kind: 'ValEx', - type: 'Untyped', - value: { - kind: 'TlaStr', - value: 'alice', - }, - }, - ], - }, - { - kind: 'OperEx', - oper: 'EQ', - type: 'Untyped', - args: [ - { - kind: 'OperEx', - oper: 'PRIME', - type: 'Untyped', - args: [ - { - kind: 'NameEx', - name: 'last_error', - type: 'Untyped', - }, - ], - }, - { - kind: 'ValEx', - type: 'Untyped', - value: { - kind: 'TlaStr', - value: 'contract is not initialized', - }, - }, - ], - }, - ], - }, - }, - ], - }, - ], - } assert.deepEqual(instrumented, expected) }) }) From 0c9a2b11bf7dda832f1868b3a0992734cd10f811 Mon Sep 17 00:00:00 2001 From: Thomas Pani Date: Tue, 30 Apr 2024 09:38:17 +0000 Subject: [PATCH 5/5] Factor out TLA+ monitor instrumentation --- solarkraft/src/instrument.ts | 154 +++++++++++++++++ solarkraft/src/verify.ts | 155 ------------------ .../{verify.test.ts => instrument.test.ts} | 4 +- 3 files changed, 156 insertions(+), 157 deletions(-) create mode 100644 solarkraft/src/instrument.ts rename solarkraft/test/unit/{verify.test.ts => instrument.test.ts} (87%) diff --git a/solarkraft/src/instrument.ts b/solarkraft/src/instrument.ts new file mode 100644 index 00000000..2a82045c --- /dev/null +++ b/solarkraft/src/instrument.ts @@ -0,0 +1,154 @@ +// TODO(#38): Replace stubs with ITF +type Value = { type: string; value: any } +type Binding = { name: string; type: string; value: any } +type State = Binding[] +type Transaction = { + functionName: string + functionArgs: Value[] + env: { timestamp: number } + error: string +} + +/** + * Return an instrumented monitor specification. + * @param monitor A TLA+ monitor, as returned from `apalache typecheck --output=temp.json` + * @param state The blockchain state before executing the transaction / the monitor. + * @param tx The transaction being applied to `state`. + * @returns The instrumented TLA+ monitor. + */ +export function instrumentMonitor( + monitor: any, + state: State, + tx: Transaction +): any { + // Add a special variable `last_error` that tracks error messages of failed transactions + state.push({ name: 'last_error', type: 'TlaStr', value: '' }) + + // Declaration of "Init" (according to `state`) + const tlaInit = tlaJsonOperDecl__And( + 'Init', + state.map((binding) => + tlaJsonEq__NameEx__ValEx( + binding.name, + false, + tlaJsonValEx(binding.type, binding.value) + ) + ) + ) + + // Declaration of "Next" (according to `tx`) + const envRecord = tlaJsonRecord([ + { name: 'timestamp', kind: 'TlaInt', value: tx.env.timestamp }, + ]) + const txArgs = tx.functionArgs.map((v) => tlaJsonValEx(v.type, v.value)) + const tlaNext = tlaJsonOperDecl__And('Next', [ + tlaJsonApplication(tx.functionName, [envRecord].concat(txArgs)), + tlaJsonEq__NameEx__ValEx( + 'last_error', + true, + tlaJsonValEx('TlaStr', tx.error) + ), + ]) + + // Instantiate the monitor spec with declarations of "Init" and "Next" + const extendedDeclarations = monitor['modules'][0]['declarations'].concat([ + tlaInit, + tlaNext, + ]) + const extendedModule = { + ...monitor['modules'][0], + declarations: extendedDeclarations, + } + return { ...monitor, modules: [extendedModule] } +} + +/** + * Return an Apalache TLA+ operator declaration of the form `operDeclName` == `conjuncts`_0 /\ ... /\ `conjuncts`_n. + * @param operDeclName Operator name + * @param conjuncts Body conjuncts + * @returns The operator declaration in Apalache IR JSON: https://apalache.informal.systems/docs/adr/005adr-json.html + */ +function tlaJsonOperDecl__And(operDeclName: string, conjuncts: any): any { + return { + type: 'Untyped', + kind: 'TlaOperDecl', + name: operDeclName, + formalParams: [], + isRecursive: false, + body: { + type: 'Untyped', + kind: 'OperEx', + oper: 'AND', + args: conjuncts, + }, + } +} + +/** + * Return an Apalache TLA+ name expression. + * @returns the name expression in Apalache IR JSON: https://apalache.informal.systems/docs/adr/005adr-json.html + */ +function tlaJsonNameEx(name: string): any { + return { type: 'Untyped', kind: 'NameEx', name: name } +} + +/** + * Return an Apalache TLA+ value expression. + * @param kind Apalache type (e.g., "TlaStr" or "TlaBool") + * @param value Expression value + * @returns The value expression in Apalache IR JSON: https://apalache.informal.systems/docs/adr/005adr-json.html + */ +function tlaJsonValEx(kind: string, value: any): any { + return { + type: 'Untyped', + kind: 'ValEx', + value: { kind: kind, value: value }, + } +} + +/** + * Return an Apalache TLA+ record. + * @param bindings Interleaved array of field names and field values. + * @returns The record in Apalache IR JSON: https://apalache.informal.systems/docs/adr/005adr-json.html + */ +function tlaJsonRecord(bindings: any): any { + return { + type: 'Untyped', + kind: 'OperEx', + oper: 'RECORD', + args: bindings.flatMap((binding) => [ + tlaJsonValEx('TlaStr', binding.name), + tlaJsonValEx(binding.kind, binding.value), + ]), + } +} + +/** + * Return an Apalache TLA+ operator application. + * @param operName Name of the operator to apply. + * @param args Application arguments + * @returns The operator application in Apalache IR JSON: https://apalache.informal.systems/docs/adr/005adr-json.html + */ +function tlaJsonApplication(operName: string, args: any): any { + return { + type: 'Untyped', + kind: 'OperEx', + oper: 'OPER_APP', + args: [tlaJsonNameEx(operName)].concat(args), + } +} + +/** + * Return an Apalache equality expression applied to a name expression LHS, and a value expression RHS, optionally priming the LHS. + * @param name LHS name. + * @param prime True iff `name` should appear primed in the expression. + * @param valEx RHS value. + * @returns The equality in Apalache IR JSON: https://apalache.informal.systems/docs/adr/005adr-json.html + */ +function tlaJsonEq__NameEx__ValEx(name: any, prime: boolean, valEx: any): any { + const nameEx = { type: 'Untyped', kind: 'NameEx', name: name } + const lhs = prime + ? { type: 'Untyped', kind: 'OperEx', oper: 'PRIME', args: [nameEx] } + : nameEx + return { type: 'Untyped', kind: 'OperEx', oper: 'EQ', args: [lhs, valEx] } +} \ No newline at end of file diff --git a/solarkraft/src/verify.ts b/solarkraft/src/verify.ts index 25bca9ba..c6bd8dce 100644 --- a/solarkraft/src/verify.ts +++ b/solarkraft/src/verify.ts @@ -11,161 +11,6 @@ import path from 'node:path' const APALACHE_DIST = '/opt/apalache' const APALACHE_BIN = path.join(APALACHE_DIST, 'bin', 'apalache-mc') -// TODO(#38): Replace stubs with ITF -type Value = { type: string; value: any } -type Binding = { name: string; type: string; value: any } -type State = Binding[] -type Transaction = { - functionName: string - functionArgs: Value[] - env: { timestamp: number } - error: string -} - -/** - * Return an instrumented monitor specification. - * @param monitor A TLA+ monitor, as returned from `apalache typecheck --output=temp.json` - * @param state The blockchain state before executing the transaction / the monitor. - * @param tx The transaction being applied to `state`. - * @returns The instrumented TLA+ monitor. - */ -export function instrumentMonitor( - monitor: any, - state: State, - tx: Transaction -): any { - // Add a special variable `last_error` that tracks error messages of failed transactions - state.push({ name: 'last_error', type: 'TlaStr', value: '' }) - - // Declaration of "Init" (according to `state`) - const tlaInit = tlaJsonOperDecl__And( - 'Init', - state.map((binding) => - tlaJsonEq__NameEx__ValEx( - binding.name, - false, - tlaJsonValEx(binding.type, binding.value) - ) - ) - ) - - // Declaration of "Next" (according to `tx`) - const envRecord = tlaJsonRecord([ - { name: 'timestamp', kind: 'TlaInt', value: tx.env.timestamp }, - ]) - const txArgs = tx.functionArgs.map((v) => tlaJsonValEx(v.type, v.value)) - const tlaNext = tlaJsonOperDecl__And('Next', [ - tlaJsonApplication(tx.functionName, [envRecord].concat(txArgs)), - tlaJsonEq__NameEx__ValEx( - 'last_error', - true, - tlaJsonValEx('TlaStr', tx.error) - ), - ]) - - // Instantiate the monitor spec with declarations of "Init" and "Next" - const extendedDeclarations = monitor['modules'][0]['declarations'].concat([ - tlaInit, - tlaNext, - ]) - const extendedModule = { - ...monitor['modules'][0], - declarations: extendedDeclarations, - } - return { ...monitor, modules: [extendedModule] } -} - -/** - * Return an Apalache TLA+ operator declaration of the form `operDeclName` == `conjuncts`_0 /\ ... /\ `conjuncts`_n. - * @param operDeclName Operator name - * @param conjuncts Body conjuncts - * @returns The operator declaration in Apalache IR JSON: https://apalache.informal.systems/docs/adr/005adr-json.html - */ -function tlaJsonOperDecl__And(operDeclName: string, conjuncts: any): any { - return { - type: 'Untyped', - kind: 'TlaOperDecl', - name: operDeclName, - formalParams: [], - isRecursive: false, - body: { - type: 'Untyped', - kind: 'OperEx', - oper: 'AND', - args: conjuncts, - }, - } -} - -/** - * Return an Apalache TLA+ name expression. - * @returns the name expression in Apalache IR JSON: https://apalache.informal.systems/docs/adr/005adr-json.html - */ -function tlaJsonNameEx(name: string): any { - return { type: 'Untyped', kind: 'NameEx', name: name } -} - -/** - * Return an Apalache TLA+ value expression. - * @param kind Apalache type (e.g., "TlaStr" or "TlaBool") - * @param value Expression value - * @returns The value expression in Apalache IR JSON: https://apalache.informal.systems/docs/adr/005adr-json.html - */ -function tlaJsonValEx(kind: string, value: any): any { - return { - type: 'Untyped', - kind: 'ValEx', - value: { kind: kind, value: value }, - } -} - -/** - * Return an Apalache TLA+ record. - * @param bindings Interleaved array of field names and field values. - * @returns The record in Apalache IR JSON: https://apalache.informal.systems/docs/adr/005adr-json.html - */ -function tlaJsonRecord(bindings: any): any { - return { - type: 'Untyped', - kind: 'OperEx', - oper: 'RECORD', - args: bindings.flatMap((binding) => [ - tlaJsonValEx('TlaStr', binding.name), - tlaJsonValEx(binding.kind, binding.value), - ]), - } -} - -/** - * Return an Apalache TLA+ operator application. - * @param operName Name of the operator to apply. - * @param args Application arguments - * @returns The operator application in Apalache IR JSON: https://apalache.informal.systems/docs/adr/005adr-json.html - */ -function tlaJsonApplication(operName: string, args: any): any { - return { - type: 'Untyped', - kind: 'OperEx', - oper: 'OPER_APP', - args: [tlaJsonNameEx(operName)].concat(args), - } -} - -/** - * Return an Apalache equality expression applied to a name expression LHS, and a value expression RHS, optionally priming the LHS. - * @param name LHS name. - * @param prime True iff `name` should appear primed in the expression. - * @param valEx RHS value. - * @returns The equality in Apalache IR JSON: https://apalache.informal.systems/docs/adr/005adr-json.html - */ -function tlaJsonEq__NameEx__ValEx(name: any, prime: boolean, valEx: any): any { - const nameEx = { type: 'Untyped', kind: 'NameEx', name: name } - const lhs = prime - ? { type: 'Untyped', kind: 'OperEx', oper: 'PRIME', args: [nameEx] } - : nameEx - return { type: 'Untyped', kind: 'OperEx', oper: 'EQ', args: [lhs, valEx] } -} - /** * Verify transactions fetched from the ledger * @param args the arguments parsed by yargs diff --git a/solarkraft/test/unit/verify.test.ts b/solarkraft/test/unit/instrument.test.ts similarity index 87% rename from solarkraft/test/unit/verify.test.ts rename to solarkraft/test/unit/instrument.test.ts index cc87ab7a..62ad9c6a 100644 --- a/solarkraft/test/unit/verify.test.ts +++ b/solarkraft/test/unit/instrument.test.ts @@ -3,11 +3,11 @@ import { assert } from 'chai' import { describe, it } from 'mocha' -import { instrumentMonitor } from '../../src/verify.js' +import { instrumentMonitor } from '../../src/instrument.js' import { instrumentedMonitor as expected } from './verify.instrumentedMonitor.js' -describe('verify command', () => { +describe('Apalache JSON instrumentor', () => { it('instruments TLA+ monitors', () => { const monitor = { modules: [{ declarations: [] }] } const state = [