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 3e243e87..c6bd8dce 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,10 @@ import path from 'node:path' const APALACHE_DIST = '/opt/apalache' const APALACHE_BIN = path.join(APALACHE_DIST, 'bin', 'apalache-mc') +/** + * 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/instrument.test.ts b/solarkraft/test/unit/instrument.test.ts new file mode 100644 index 00000000..62ad9c6a --- /dev/null +++ b/solarkraft/test/unit/instrument.test.ts @@ -0,0 +1,26 @@ +// an example unit test to copy from + +import { assert } from 'chai' +import { describe, it } from 'mocha' + +import { instrumentMonitor } from '../../src/instrument.js' + +import { instrumentedMonitor as expected } from './verify.instrumentedMonitor.js' + +describe('Apalache JSON instrumentor', () => { + 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) + assert.deepEqual(instrumented, expected) + }) +}) 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 }