Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Programmatically instrument TLA+ monitor #39

Merged
merged 5 commits into from
Apr 30, 2024
Merged

Programmatically instrument TLA+ monitor #39

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
dcbe3f1
Programmatically instrument TLA+ monitor
thpani Apr 29, 2024
94ba9ea
Add type declarations
thpani Apr 29, 2024
54b3528
Rename function
thpani Apr 30, 2024
76d8ce1
Move expected test output
thpani Apr 30, 2024
0c9a2b1
Factor out TLA+ monitor instrumentation
thpani Apr 30, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
154 changes: 154 additions & 0 deletions solarkraft/src/instrument.ts
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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] }
}
8 changes: 4 additions & 4 deletions solarkraft/src/verify.ts
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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'
Expand All @@ -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`
Expand Down
26 changes: 26 additions & 0 deletions solarkraft/test/unit/instrument.test.ts
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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)
})
})
148 changes: 148 additions & 0 deletions solarkraft/test/unit/verify.instrumentedMonitor.ts
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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 }