Read ITF in monitor executor

solarkraft/src/instrument.ts

@@ -2,7 +2,6 @@
  * @license
  * [Apache-2.0](https://github.com/freespek/solarkraft/blob/main/LICENSE)
  */
-// TODO(#38): Replace stubs with ITF
 type Value = { type: string; value: any }
 type Binding = { name: string; type: string; value: any }
 type State = Binding[]
@@ -13,6 +12,27 @@ type Transaction = {
     error: string
 }
 
+/**
+ * Return a `State` from an ITF JSON object.
+ * @param itf ITF JSON object, see https://apalache.informal.systems/docs/adr/015adr-trace.html
+ * @returns `State`
+ */
+export function stateFromItf(itf: any): State {
+    // const vars = itf['vars'] // e.g., [ "is_initialized", "last_error" ]
+    const varTypes = itf['#meta']['varTypes'] // e.g., { "is_initialized": "Bool", "last_error": "Str" }
+    const initState = itf['states'][0] // e.g., [ { "is_initialized": false, "last_error": "" }, state1, ... ]
+    delete initState['#meta']
+
+    const state = Object.entries(initState)
+        .filter(([name]) => name != '#meta')
+        .map(([name, value]) => ({
+            name: name,
+            value: value,
+            type: 'Tla' + varTypes[name],
+        }))
+    return state
+}
+
 /**
  * Return an instrumented monitor specification.
  * @param monitor A TLA+ monitor, as returned from `apalache typecheck --output=temp.json`

solarkraft/src/main.ts

@@ -58,6 +58,12 @@ const verifyCmd = {
                 desc: 'Monitor to check against',
                 type: 'string',
                 demandOption: true,
+            })
+            .option('state', {
+                // TODO(#38): read state from fetcher output
+                desc: 'ITF file encoding ledger state',
+                type: 'string',
+                demandOption: true,
             }),
     handler: verify,
 }

solarkraft/src/verify.ts

@@ -10,7 +10,7 @@ import path from 'node:path'
 
 import { temporaryFile } from 'tempy'
 
-import { instrumentMonitor } from './instrument.js'
+import { instrumentMonitor, stateFromItf } from './instrument.js'
 
 // TODO(#34): fix hardcoded path to Apalache
 const APALACHE_DIST = '/opt/apalache'
@@ -32,6 +32,11 @@ export function verify(args: any) {
         console.log('[Error]')
         return
     }
+    if (!existsSync(args.state)) {
+        console.log(`The ITF state file ${args.state} does not exist.`)
+        console.log('[Error]')
+        return
+    }
 
     // Use Apalache to parse the monitor TLA+ to JSON IR
     console.log(`Parsing monitor ${args.monitor}`)
@@ -57,9 +62,18 @@ export function verify(args: any) {
         return
     }
 
+    // Read the state from ITF
+    let itf: any
+    try {
+        itf = JSON.parse(readFileSync(args.state, 'utf8'))
+    } catch (err) {
+        console.error(`Failed to read state from ITF: ${err}`)
+        return
+    }
+
     // Instrument the monitor
     // TODO(#38): Read `state` and `tx` from fetcher output
-    const state = [{ name: 'is_initialized', type: 'TlaBool', value: false }]
+    const state = stateFromItf(itf)
     const tx = {
         functionName: 'Claim',
         functionArgs: [{ type: 'TlaStr', value: 'alice' }],

solarkraft/test/e2e/verify.test.ts

@@ -6,7 +6,9 @@ import { spawn } from 'nexpect'
 
 describe('verify', () => {
     it('fails on missing file', function (done) {
-        spawn('solarkraft verify --txHash mimimi --monitor doesnotexist')
+        spawn(
+            'solarkraft verify --txHash mimimi --monitor doesnotexist --state test/e2e/tla/timelock_state.itf.json'
+        )
             .wait('The monitor file doesnotexist does not exist.')
             .expect('[Error]')
             .run(done)
@@ -15,7 +17,7 @@ describe('verify', () => {
     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'
+            'solarkraft verify --txHash mimimi --monitor test/e2e/tla/timelock_mon1_instrumented_okay.tla --state test/e2e/tla/timelock_state.itf.json'
         )
             .wait('[OK]')
             .run(done)
@@ -24,7 +26,7 @@ describe('verify', () => {
     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'
+            'solarkraft verify --txHash mimimi --monitor test/e2e/tla/timelock_mon1_instrumented_fail.tla --state test/e2e/tla/timelock_state.itf.json'
         )
             .wait('Monitor is unable to reproduce the transaction')
             .expect('[Fail]')