Support all Soroban primitive types

freespek · May 21, 2024 · b3b2c1a · b3b2c1a
1 parent 36709f0
commit b3b2c1a
Show file tree

Hide file tree

Showing 2 changed files with 97 additions and 23 deletions.
diff --git a/solarkraft/src/instrument.ts b/solarkraft/src/instrument.ts
@@ -33,13 +33,14 @@ export function instrumentMonitor(
     const tlaInit = tlaJsonOperDecl__And(
         'Init',
         fieldsToInstrument
-            .map((value, name) =>
-                tlaJsonEq__NameEx__ValEx(
+            .map((value, name) => {
+                const tlaValue = tlaJsonValueOfNative(value)
+                return tlaJsonEq__NameEx__ValEx(
                     name,
                     false,
-                    tlaJsonValEx(tlaJsonTypeOfNative(value), value)
+                    tlaJsonValEx(tlaJsonTypeOfValue(tlaValue), tlaValue)
                 )
-            )
+            })
             .valueSeq()
             .toArray()
     )
@@ -48,9 +49,10 @@ export function instrumentMonitor(
     const envRecord = tlaJsonRecord([
         { name: 'height', kind: 'TlaInt', value: contractCall.height },
     ])
-    const tlaMethodArgs = contractCall.methodArgs.map((v) =>
-        tlaJsonValEx(tlaJsonTypeOfNative(v), v)
-    )
+    const tlaMethodArgs = contractCall.methodArgs.map((v) => {
+        const tlaValue = tlaJsonValueOfNative(v)
+        return tlaJsonValEx(tlaJsonTypeOfValue(tlaValue), tlaValue)
+    })
     const tlaNext = tlaJsonOperDecl__And('Next', [
         tlaJsonApplication(
             contractCall.method,
@@ -76,28 +78,67 @@ 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.`
-    )
+// Return the appropriate type for an Apalache JSON IR value `v`.
+export function tlaJsonTypeOfValue(v: any) {
+    if (
+        typeof v === 'symbol' ||
+        typeof v == 'undefined' ||
+        typeof v == 'function' ||
+        typeof v == 'object'
+    ) {
+        console.error(
+            `Unexpected native value of type ${typeof v} in fetcher output:`
+        )
+        console.error(v)
+        assert(false)
+    }
 
     switch (typeof v) {
-        case 'string':
-            return 'TlaStr'
-        case 'number':
-            return 'TlaInt'
+        case 'boolean':
+            return 'TlaBool'
         case 'bigint':
+        case 'number':
             return 'TlaInt'
+        case 'string':
+            return 'TlaStr'
+    }
+}
+
+// Decode a Native JS value `v` into its corresponding Apalache JSON IR representation.
+export function tlaJsonValueOfNative(v: any) {
+    if (
+        typeof v == 'symbol' ||
+        typeof v == 'undefined' ||
+        typeof v == 'function'
+    ) {
+        console.error(
+            `Unexpected native value of type ${typeof v} in fetcher output:`
+        )
+        console.error(v)
+        assert(false)
+    }
+
+    switch (typeof v) {
         case 'boolean':
-            return 'TlaBool'
+        case 'bigint':
+        case 'number':
+        case 'string':
+            return v
         case 'object':
-            // an array or object
             // TODO(#46): support composite types (sequence, tuple, record, set, map)
-            // if (Array.isArray(o)) ...
+            if (Array.isArray(v)) {
+                // an array
+                return undefined
+            }
+            // an object
+            if (v.type == 'Buffer') {
+                // a buffer
+                // v.data contains the bytes, as integers - render them into a string
+                return v.data
+                    .map((x: number) => x.toString(16).padStart(2, '0'))
+                    .join('')
+            }
+            // a record or map
             return undefined
     }
 }

diff --git a/solarkraft/test/unit/instrument.test.ts b/solarkraft/test/unit/instrument.test.ts
@@ -5,7 +5,11 @@ import { describe, it } from 'mocha'
 
 import { OrderedMap } from 'immutable'
 
-import { instrumentMonitor } from '../../src/instrument.js'
+import {
+    instrumentMonitor,
+    tlaJsonTypeOfValue,
+    tlaJsonValueOfNative,
+} from '../../src/instrument.js'
 
 import { instrumentedMonitor as expected } from './verify.instrumentedMonitor.js'
 
@@ -64,4 +68,33 @@ describe('Apalache JSON instrumentor', () => {
         const instrumented = instrumentMonitor(monitor, contractCall)
         assert.deepEqual(expected, instrumented)
     })
+
+    it('decodes Soroban values to Apalache JSON IR values', () => {
+        assert.equal(true, tlaJsonValueOfNative(true))
+        assert.equal(false, tlaJsonValueOfNative(false))
+        assert.equal(-42000, tlaJsonValueOfNative(-42000))
+        assert.equal(0, tlaJsonValueOfNative(0))
+        assert.equal(1, tlaJsonValueOfNative(1))
+        assert.equal(42000, tlaJsonValueOfNative(42000))
+        assert.equal('', tlaJsonValueOfNative(''))
+        assert.equal('asdf', tlaJsonValueOfNative('asdf'))
+        assert.equal('00', tlaJsonValueOfNative({ type: 'Buffer', data: [0] }))
+        assert.equal(
+            'beef',
+            tlaJsonValueOfNative({ type: 'Buffer', data: [190, 239] })
+        )
+    })
+
+    it('finds appropriate types for values', () => {
+        assert.equal('TlaBool', tlaJsonTypeOfValue(true))
+        assert.equal('TlaBool', tlaJsonTypeOfValue(false))
+        assert.equal('TlaInt', tlaJsonTypeOfValue(-42000))
+        assert.equal('TlaInt', tlaJsonTypeOfValue(0))
+        assert.equal('TlaInt', tlaJsonTypeOfValue(1))
+        assert.equal('TlaInt', tlaJsonTypeOfValue(42000))
+        assert.equal('TlaStr', tlaJsonTypeOfValue(''))
+        assert.equal('TlaStr', tlaJsonTypeOfValue('asdf'))
+        assert.equal('TlaStr', tlaJsonTypeOfValue('00'))
+        assert.equal('TlaStr', tlaJsonTypeOfValue('beef'))
+    })
 })