Merge pull request #65 from freespek/th/read-fetcher

Read state from the new fetcher
freespek · May 17, 2024 · b8b9c78 · b8b9c78
2 parents 5096a6b + 6d8f8eb
commit b8b9c78
Show file tree

Hide file tree

Showing 11 changed files with 674 additions and 229 deletions.
diff --git a/solarkraft/package-lock.json b/solarkraft/package-lock.json
diff --git a/solarkraft/package.json b/solarkraft/package.json
@@ -47,6 +47,7 @@
     "@types/urijs": "^1.19.25",
     "axios": "^1.6.7",
     "chalk": "^5.3.0",
+    "glob": "^10.3.15",
     "immutable": "^5.0.0-beta.5",
     "json-bigint": "^1.0.0",
     "source-licenser": "^2.0.6",

diff --git a/solarkraft/src/fetch.ts b/solarkraft/src/fetch.ts
@@ -78,7 +78,7 @@ export async function fetch(args: any) {
                         console.log(`+ save: ${entry.height}`)
                         saveContractCallEntry(args.home, entry)
                     }
-                } // else: shall we also store reverted transactions?
+                } // TODO(#61): else: shall we also store reverted transactions?
 
                 nEvents++
                 if (nEvents % HEIGHT_FETCHING_PERIOD === 0) {

diff --git a/solarkraft/src/instrument.ts b/solarkraft/src/instrument.ts
@@ -1,101 +1,67 @@
+import { assert } from 'console'
+import { ContractCallEntry } from './fetcher/storage.js'
+
 /**
  * @license
  * [Apache-2.0](https://github.com/freespek/solarkraft/blob/main/LICENSE)
  */
-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 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
- * @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: decodeITFValue(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`
- * @param state The blockchain state before executing the transaction / the monitor.
- * @param tx The transaction being applied to `state`.
+ * @param contractCall The contract call, fetched from the ledger.
  * @returns The instrumented TLA+ monitor.
  */
 export function instrumentMonitor(
     monitor: any,
-    state: State,
-    tx: Transaction
+    contractCall: ContractCallEntry
 ): 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))
+    const fieldsToInstrument = contractCall.oldFields.filter((value, key) =>
+        declaredMonitorVariables.includes(key)
+    )
 
+    // TODO(#61): handle failed transactions
     // Add a special variable `last_error` that tracks error messages of failed transactions
-    state.push({ name: 'last_error', type: 'TlaStr', value: '' })
+    // fieldsToInstrument.push({ name: 'last_error', type: 'TlaStr', value: '' })
 
-    // Declaration of  "Init" (according to `state`)
+    // Declaration of  "Init" (according to `contractCall.oldFields`)
     const tlaInit = tlaJsonOperDecl__And(
         'Init',
-        state.map((binding) =>
-            tlaJsonEq__NameEx__ValEx(
-                binding.name,
-                false,
-                tlaJsonValEx(binding.type, binding.value)
+        fieldsToInstrument
+            .map((value, name) =>
+                tlaJsonEq__NameEx__ValEx(
+                    name,
+                    false,
+                    tlaJsonValEx(tlaJsonTypeOfNative(value), value)
+                )
             )
-        )
+            .valueSeq()
+            .toArray()
     )
 
     // Declaration of "Next" (according to `tx`)
     const envRecord = tlaJsonRecord([
-        { name: 'timestamp', kind: 'TlaInt', value: tx.env.timestamp },
+        { name: 'height', kind: 'TlaInt', value: contractCall.height },
     ])
-    const txArgs = tx.functionArgs.map((v) => tlaJsonValEx(v.type, v.value))
+    const tlaMethodArgs = contractCall.methodArgs.map((v) =>
+        tlaJsonValEx(tlaJsonTypeOfNative(v), v)
+    )
     const tlaNext = tlaJsonOperDecl__And('Next', [
-        tlaJsonApplication(tx.functionName, [envRecord].concat(txArgs)),
-        tlaJsonEq__NameEx__ValEx(
-            'last_error',
-            true,
-            tlaJsonValEx('TlaStr', tx.error)
+        tlaJsonApplication(
+            contractCall.method,
+            [envRecord].concat(tlaMethodArgs)
         ),
+        // TODO(#61): handle failed transactions
+        // tlaJsonEq__NameEx__ValEx(
+        //     'last_error',
+        //     true,
+        //     tlaJsonValEx('TlaStr', tx.error)
+        // ),
     ])
 
     // Instantiate the monitor spec with declarations of "Init" and "Next"
@@ -110,6 +76,32 @@ export function instrumentMonitor(
     return { ...monitor, modules: [extendedModule] }
 }
 
+// Decode a Native JS value `v` into its corresponding Apalache IR type.
+function tlaJsonTypeOfNative(v: any) {
+    assert(
+        typeof v !== 'symbol' &&
+            typeof v !== 'undefined' &&
+            typeof v !== 'function',
+        `Unexpected native value ${v} of type ${typeof v} in fetcher output.`
+    )
+
+    switch (typeof v) {
+        case 'string':
+            return 'TlaStr'
+        case 'number':
+            return 'TlaInt'
+        case 'bigint':
+            return 'TlaInt'
+        case 'boolean':
+            return 'TlaBool'
+        case 'object':
+            // an array or object
+            // TODO(#46): support composite types (sequence, tuple, record, set, map)
+            // if (Array.isArray(o)) ...
+            return undefined
+    }
+}
+
 /**
  * Return an Apalache TLA+ operator declaration of the form `operDeclName` == `conjuncts`_0 /\ ... /\ `conjuncts`_n.
  * @param operDeclName Operator name

diff --git a/solarkraft/src/main.ts b/solarkraft/src/main.ts
@@ -71,12 +71,6 @@ const verifyCmd = {
                 desc: 'Monitors to check against',
                 type: 'array',
                 demandOption: true,
-            })
-            .option('state', {
-                // TODO(#38): read state from fetcher output
-                desc: 'ITF file encoding ledger state',
-                type: 'string',
-                demandOption: true,
             }),
     handler: verify,
 }

diff --git a/solarkraft/src/verify.ts b/solarkraft/src/verify.ts
@@ -8,10 +8,12 @@ import { rmSync } from 'fs'
 import { existsSync, readFileSync, writeFileSync } from 'node:fs'
 import path from 'node:path'
 
+import { globSync } from 'glob'
 import { temporaryFile } from 'tempy'
 import { Either, left, right, mergeInOne } from '@sweet-monads/either'
 
-import { instrumentMonitor, stateFromItf } from './instrument.js'
+import { loadContractCallEntry, storagePath } from './fetcher/storage.js'
+import { instrumentMonitor } from './instrument.js'
 
 type Result<T> = Either<string, T>
 type ApalacheResult = Result<void>
@@ -106,36 +108,35 @@ export function verify(args: any) {
             return
         }
     }
-    if (!existsSync(args.state)) {
-        console.log(`The ITF state file ${args.state} does not exist.`)
+
+    // Resolve fetcher entry in storage from txHash
+    const entryPaths = globSync(
+        path.join(storagePath(args.home), '**', `entry-${args.txHash}.json`)
+    )
+    if (entryPaths.length === 0) {
+        console.error(
+            `No entries found for tx hash ${args.txHash}. Run 'solarkraft fetch' first.`
+        )
         console.log('[Error]')
         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}`)
+    if (entryPaths.length > 1) {
+        console.error(
+            `Too many entries (${entryPaths.length}) found for tx hash ${args.txHash}.`
+        )
         console.log('[Error]')
         return
     }
+    const entryPath = entryPaths[0]
 
-    // TODO(#38): Read ledger state and `tx` from fetcher output
-    const state = stateFromItf(itf)
-    const tx = {
-        functionName: 'Claim',
-        functionArgs: [{ type: 'TlaStr', value: 'alice' }],
-        env: { timestamp: 100 },
-        error: 'contract is not initialized',
-    }
+    // Read the state from fetcher output
+    const contractCall = loadContractCallEntry(entryPath)
 
     // Check all monitors
     const resultsPerMonitor: Result<ApalacheResult>[] = args.monitor.map(
         (monitorPath: string) =>
             getApalacheJsonIr(monitorPath)
-                .map((jsonIr: any) => instrumentMonitor(jsonIr, state, tx))
+                .map((jsonIr: any) => instrumentMonitor(jsonIr, contractCall))
                 .chain(apalacheCheck)
                 // Print the monitor's result
                 .map((apalacheResult) => {

diff --git a/solarkraft/test/e2e/tla/.stor/asdf/100/entry-timelock.json b/solarkraft/test/e2e/tla/.stor/asdf/100/entry-timelock.json
@@ -0,0 +1,18 @@
+{
+  "height": 100,
+  "txHash": "0xasdf",
+  "contractId": "0xqwer",
+  "returnValue": null,
+  "method": "Claim",
+  "methodArgs": ["alice"],
+  "fields": [
+      ["balance", 123],
+      ["is_initialized", false],
+      ["last_error", ""]
+  ],
+  "oldFields": [
+      ["balance", 123],
+      ["is_initialized", false],
+      ["last_error", ""]
+  ]
+}
diff --git a/solarkraft/test/e2e/tla/timelock_state.itf.json b/solarkraft/test/e2e/tla/timelock_state.itf.json
diff --git a/solarkraft/test/e2e/verify.test.ts b/solarkraft/test/e2e/verify.test.ts
@@ -5,9 +5,9 @@ import { describe, it } from 'mocha'
 import { spawn } from 'nexpect'
 
 describe('verify', () => {
-    it('errors on missing file', function (done) {
+    it('errors on missing monitor', function (done) {
         spawn(
-            'solarkraft verify --txHash mimimi --monitor doesnotexist --state test/e2e/tla/timelock_state.itf.json'
+            'solarkraft verify --home test/e2e/tla/ --txHash timelock --monitor doesnotexist'
         )
             .wait('The monitor file doesnotexist does not exist.')
             .expect('[Error]')
@@ -16,7 +16,15 @@ describe('verify', () => {
 
     it('errors on no monitors given', function (done) {
         spawn(
-            'solarkraft verify --txHash mimimi --monitor --state test/e2e/tla/timelock_state.itf.json'
+            'solarkraft verify --home test/e2e/tla/ --txHash timelock --monitor'
+        )
+            .wait('[Error]')
+            .run(done)
+    })
+
+    it('errors on missing tx hash', function (done) {
+        spawn(
+            'solarkraft verify --home test/e2e/tla/ --txHash doesnotexist --monitor test/e2e/tla/timelock_mon1.tla'
         )
             .wait('[Error]')
             .run(done)
@@ -25,7 +33,7 @@ describe('verify', () => {
     it('reports success on okay monitor1', function (done) {
         this.timeout(50000)
         spawn(
-            'solarkraft verify --txHash mimimi --monitor test/e2e/tla/timelock_mon1.tla --state test/e2e/tla/timelock_state.itf.json'
+            'solarkraft verify --home test/e2e/tla/ --txHash timelock --monitor test/e2e/tla/timelock_mon1.tla'
         )
             .wait('[OK]')
             .run(done)
@@ -34,7 +42,7 @@ describe('verify', () => {
     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'
+            'solarkraft verify --home test/e2e/tla/ --txHash timelock --monitor test/e2e/tla/timelock_mon2.tla'
         )
             .wait('[OK]')
             .run(done)
@@ -43,7 +51,7 @@ describe('verify', () => {
     it('reports success on two okay monitors', function (done) {
         this.timeout(50000)
         spawn(
-            'solarkraft verify --txHash mimimi --monitor test/e2e/tla/timelock_mon1.tla test/e2e/tla/timelock_mon2.tla --state test/e2e/tla/timelock_state.itf.json'
+            'solarkraft verify --home test/e2e/tla/ --txHash timelock --monitor test/e2e/tla/timelock_mon1.tla test/e2e/tla/timelock_mon2.tla'
         )
             .wait('[OK]')
             .run(done)
@@ -52,7 +60,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 --state test/e2e/tla/timelock_state.itf.json'
+            'solarkraft verify --home test/e2e/tla/ --txHash timelock --monitor test/e2e/tla/timelock_mon1_instrumented_fail.tla'
         )
             .wait('unable to reproduce the transaction')
             .wait('[Fail]')
@@ -62,7 +70,7 @@ describe('verify', () => {
     it('reports failure on deadlocking monitor, if another succeeding monitor is present', function (done) {
         this.timeout(50000)
         spawn(
-            'solarkraft verify --txHash mimimi --monitor test/e2e/tla/timelock_mon1_instrumented_fail.tla test/e2e/tla/timelock_mon2.tla --state test/e2e/tla/timelock_state.itf.json'
+            'solarkraft verify --home test/e2e/tla/ --txHash timelock --monitor test/e2e/tla/timelock_mon1_instrumented_fail.tla test/e2e/tla/timelock_mon2.tla'
         )
             .wait('[Fail]')
             .run(done)