Merge pull request #47 from freespek/th/instrument-only-monitor-vars

Instrument only monitor variables
freespek · May 6, 2024 · b0502fa · b0502fa
2 parents c64a12b + 9b9518f
commit b0502fa
Show file tree

Hide file tree

Showing 7 changed files with 125 additions and 6 deletions.
diff --git 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
@@ -45,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: '' })
 

diff --git 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
     }
 

diff --git a/solarkraft/test/e2e/tla/timelock_mon2.tla 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' = ""
+
+=============================
diff --git a/solarkraft/test/e2e/tla/timelock_state.itf.json 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": ""
+    }
+  ]
+}
diff --git 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)

diff --git 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
@@ -2,6 +2,10 @@ const instrumentedMonitor = {
     modules: [
         {
             declarations: [
+                {
+                    kind: 'TlaVarDecl',
+                    name: 'is_initialized',
+                },
                 {
                     kind: 'TlaOperDecl',
                     name: 'Init',