persistent verification status

solarkraft/.gitignore

@@ -1,2 +1,3 @@
 node_modules
 dist
+_apalache-out

solarkraft/src/fetcher/storage.ts

@@ -28,6 +28,7 @@ const JSONbig = JSONbigint({ useNativeBigInt: true })
  */
 export type FieldsMap = OrderedMap<string, any>
 
+export type VerificationStatus = 'ok' | 'fail' | 'unverified'
 /**
  * A storage entry for a performed contract call.
  */
@@ -72,6 +73,11 @@ export interface ContractCallEntry {
      * when the storage goes over TTL.
      */
     oldFields: FieldsMap
+
+    /**
+     * Flag which tracks whether this particular entry has already been verified, and, if it was, the verification result.
+     */
+    verification?: VerificationStatus
 }
 
 /**
@@ -81,7 +87,7 @@ export interface ListEntry {
     contractId: string
     height: number
     txHash: string
-    verification: 'ok' | 'fail' | 'unverified'
+    verification: VerificationStatus
 }
 
 /**
@@ -112,11 +118,14 @@ export function storagePath(solarkraftHome: string): string {
  */
 export function saveContractCallEntry(home: string, entry: ContractCallEntry) {
     const filename = getEntryFilename(storagePath(home), entry)
+    const verificationStatus: VerificationStatus =
+        entry.verification ?? 'unverified'
     // convert OrderedMaps to arrays
     const simplified = {
         ...entry,
         fields: entry.fields.toArray(),
         oldFields: entry.oldFields.toArray(),
+        verification: verificationStatus,
     }
     const contents = JSONbig.stringify(simplified)
     writeFileSync(filename, contents)
@@ -141,6 +150,7 @@ export function loadContractCallEntry(filename: string): ContractCallEntry {
         returnValue: loaded.returnValue,
         fields: OrderedMap<string, any>(loaded.fields),
         oldFields: OrderedMap<string, any>(loaded.oldFields),
+        verification: loaded.verification ?? 'unverified',
     }
 }
 
@@ -167,12 +177,19 @@ export function* yieldListEntriesForContract(
                 )
                 if (ledgerDirent.isFile() && matcher) {
                     const txHash = matcher[1]
-                    // TODO: read the verification result and report it
+                    const filename = join(
+                        ledgerDirent.path,
+                        `entry-${txHash}.json`
+                    )
+                    const contents = JSONbig.parse(
+                        readFileSync(filename, 'utf-8')
+                    )
+                    const status = contents['verification'] ?? 'unverified'
                     yield {
                         contractId,
                         height,
                         txHash,
-                        verification: 'unverified',
+                        verification: status,
                     }
                 }
             }

solarkraft/src/verify.ts

@@ -12,7 +12,12 @@ import { globSync } from 'glob'
 import { temporaryFile } from 'tempy'
 import { Either, left, right, mergeInOne } from '@sweet-monads/either'
 
-import { loadContractCallEntry, storagePath } from './fetcher/storage.js'
+import {
+    loadContractCallEntry,
+    saveContractCallEntry,
+    storagePath,
+    VerificationStatus,
+} from './fetcher/storage.js'
 import { instrumentMonitor } from './instrument.js'
 
 type Result<T> = Either<string, T>
@@ -135,6 +140,8 @@ export function verify(args: any) {
     // Read the state from fetcher output
     const contractCall = loadContractCallEntry(entryPath)
 
+    let verificationStatus: VerificationStatus = 'unverified'
+
     // Check all monitors
     const resultsPerMonitor: Result<ApalacheResult>[] = args.monitor.map(
         (monitorPath: string) =>
@@ -147,16 +154,25 @@ export function verify(args: any) {
                     console.log(
                         `${path.basename(monitorPath)}: ${errorStringOrOK}`
                     )
+                    apalacheResult
+                        .map(() => (verificationStatus = 'ok'))
+                        .mapLeft(() => (verificationStatus = 'fail'))
                     return apalacheResult
                 })
                 .mapLeft((error) => {
                     console.log(
                         `${path.basename(monitorPath)}: Internal error, see below`
                     )
+                    verificationStatus = 'fail'
                     return error
                 })
     )
 
+    saveContractCallEntry(args.home, {
+        ...contractCall,
+        verification: verificationStatus,
+    })
+
     // Print accumulated result
     mergeInOne(resultsPerMonitor)
         .map((apalacheResults) => {

solarkraft/test/e2e/tla/.stor/0xqwer/100/entry-0xasdf.json

@@ -0,0 +1 @@
+{"height":100,"contractId":"0xqwer","txHash":"0xasdf","method":"Claim","methodArgs":["alice"],"returnValue":null,"fields":[["balance",123],["is_initialized",false],["last_error",""]],"oldFields":[["balance",123],["is_initialized",false],["last_error",""]],"verification":"ok"}

solarkraft/test/e2e/tla/.stor/asdf/100/entry-timelock.json

@@ -4,15 +4,36 @@
   "contractId": "0xqwer",
   "returnValue": null,
   "method": "Claim",
-  "methodArgs": ["alice"],
+  "methodArgs": [
+    "alice"
+  ],
   "fields": [
-      ["balance", 123],
-      ["is_initialized", false],
-      ["last_error", ""]
+    [
+      "balance",
+      123
+    ],
+    [
+      "is_initialized",
+      false
+    ],
+    [
+      "last_error",
+      ""
+    ]
   ],
   "oldFields": [
-      ["balance", 123],
-      ["is_initialized", false],
-      ["last_error", ""]
-  ]
+    [
+      "balance",
+      123
+    ],
+    [
+      "is_initialized",
+      false
+    ],
+    [
+      "last_error",
+      ""
+    ]
+  ],
+  "verification": "unverified"
 }