Skip to content

Commit

Permalink
Merge pull request #74 from freespek/th/composite-types
Browse files Browse the repository at this point in the history 
Support Map and Vec
  • Loading branch information
@thpani
thpani authored May 22, 2024
2 parents b37c158 + f0570e1 commit b4224b7
Show file tree
Hide file tree
Showing 2 changed files with 129 additions and 80 deletions.
98 changes: 45 additions & 53 deletions solarkraft/src/instrument.ts
View file
Original file line number Diff line number Diff line change
Expand Up @@ -34,11 +34,10 @@ export function instrumentMonitor(
'Init',
fieldsToInstrument
.map((value, name) => {
const tlaValue = tlaJsonValueOfNative(value)
return tlaJsonEq__NameEx__ValEx(
name,
false,
tlaJsonValEx(tlaJsonTypeOfValue(tlaValue), tlaValue)
tlaJsonOfNative(value)
)
})
.valueSeq()
Expand All @@ -49,10 +48,7 @@ export function instrumentMonitor(
const envRecord = tlaJsonRecord([
{ name: 'height', kind: 'TlaInt', value: contractCall.height },
])
const tlaMethodArgs = contractCall.methodArgs.map((v) => {
const tlaValue = tlaJsonValueOfNative(v)
return tlaJsonValEx(tlaJsonTypeOfValue(tlaValue), tlaValue)
})
const tlaMethodArgs = contractCall.methodArgs.map(tlaJsonOfNative)
const tlaNext = tlaJsonOperDecl__And('Next', [
tlaJsonApplication(
contractCall.method,
Expand All @@ -79,20 +75,7 @@ export function instrumentMonitor(
}

// 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)
}

export function tlaJsonTypeOfPrimitive(v: any) {
switch (typeof v) {
case 'boolean':
return 'TlaBool'
Expand All @@ -101,46 +84,55 @@ export function tlaJsonTypeOfValue(v: any) {
return 'TlaInt'
case 'string':
return 'TlaStr'
default:
assert(false, `Expected primitive type, got ${typeof v}`)
}
}

// 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':
case 'bigint':
case 'number':
case 'string':
return v
case 'object':
// TODO(#46): support composite types (sequence, tuple, record, set, map)
if (Array.isArray(v)) {
// an array
return undefined
// Translate a Native JS value `v` into its corresponding Apalache JSON IR representation.
export function tlaJsonOfNative(v: any): any {
if (typeof v === 'object') {
if (Array.isArray(v)) {
// a JS array / Soroban `Vec`
// [ 1, 2, 3 ] ~~> << 1, 2, 3 >>
return {
type: 'Untyped',
kind: 'OperEx',
oper: 'TUPLE',
args: v.map(tlaJsonOfNative),
}
// an object
if (v.type == 'Buffer') {
// a buffer
// v.data contains the bytes, as integers - render them into a string
return v.data
}
// a "proper" JS object (not an array)
if (v.type == 'Buffer') {
// Soroban `Buffer`
// v.data contains the bytes, as integers - render them into a string
return tlaJsonOfNative(
v.data
.map((x: number) => x.toString(16).padStart(2, '0'))
.join('')
}
// a record or map
return undefined
)
}
// Soroban `Map`
// { "2": 3, "4": 5 } ~~> SetAsFun({ <<"2", 3>>, <<"4", 5>> })
return {
type: 'Untyped',
kind: 'OperEx',
oper: 'Apalache!SetAsFun',
args: [
{
type: 'Untyped',
kind: 'OperEx',
oper: 'SET_ENUM',
args: Object.entries(v).map(([key, value]) =>
tlaJsonOfNative([key, value])
),
},
],
}
}
// a primitive value
// v ~~> ValEx(v)
return tlaJsonValEx(tlaJsonTypeOfPrimitive(v), v)
}

/**
Expand Down
111 changes: 84 additions & 27 deletions solarkraft/test/unit/instrument.test.ts
View file
Original file line number Diff line number Diff line change
Expand Up @@ -7,12 +7,59 @@ import { OrderedMap } from 'immutable'

import {
instrumentMonitor,
tlaJsonTypeOfValue,
tlaJsonValueOfNative,
tlaJsonTypeOfPrimitive,
tlaJsonOfNative,
} from '../../src/instrument.js'

import { instrumentedMonitor as expected } from './verify.instrumentedMonitor.js'

// Assert that `tlaJsonOfNative` returns a proper TLA+ `ValEx` for the primitive JS value `v`
function assertProperValExOfPrimitive(v: any) {
const valEx = tlaJsonOfNative(v)
assert.propertyVal(valEx, 'type', 'Untyped')
assert.propertyVal(valEx, 'kind', 'ValEx')
assert.property(valEx, 'value')
assert.propertyVal(valEx.value, 'value', v)
}

// Assert that `tlaJsonOfNative` returns a proper TLA+ `ValEx` for the Soroban `Buffer` `v`
function assertProperValExOfBuffer(v: any, expected: string) {
const valEx = tlaJsonOfNative(v)
assert.propertyVal(valEx, 'type', 'Untyped')
assert.propertyVal(valEx, 'kind', 'ValEx')
assert.property(valEx, 'value')
assert.propertyVal(valEx.value, 'kind', 'TlaStr')
assert.propertyVal(valEx.value, 'value', expected)
}

// Assert that `tlaJsonOfNative` returns a proper TLA+ sequence constructor for the Soroban `Vec` `v`
function assertProperVec(v: any[]) {
const tla = tlaJsonOfNative(v)
assert.propertyVal(tla, 'type', 'Untyped')
assert.propertyVal(tla, 'kind', 'OperEx')
assert.propertyVal(tla, 'oper', 'TUPLE')
assert.deepPropertyVal(tla, 'args', v.map(tlaJsonOfNative))
}

// Assert that `tlaJsonOfNative` returns a proper Apalache/TLA+ `SetAsFun({<<k1, v1>>, <<k2, v2>>, ...})` for the Soroban `Map` `v`
function assertProperMap(v: any) {
const tla = tlaJsonOfNative(v)
assert.propertyVal(tla, 'type', 'Untyped')
assert.propertyVal(tla, 'kind', 'OperEx')
assert.propertyVal(tla, 'oper', 'Apalache!SetAsFun')
assert.property(tla, 'args')
assert.equal(tla.args.length, 1)
const setEnum = tla.args[0]
assert.propertyVal(setEnum, 'type', 'Untyped')
assert.propertyVal(setEnum, 'kind', 'OperEx')
assert.propertyVal(setEnum, 'oper', 'SET_ENUM')
assert.property(setEnum, 'args')
setEnum.args.forEach((tuple) => {
const key = tuple.args[0].value.value
assertProperVec([key, v[key]])
})
}

describe('Apalache JSON instrumentor', () => {
it('instruments TLA+ monitors', () => {
const monitor = {
Expand Down Expand Up @@ -69,32 +116,42 @@ describe('Apalache JSON instrumentor', () => {
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('decodes primitive Soroban values to Apalache JSON IR ValEx', () => {
assertProperValExOfPrimitive(true)
assertProperValExOfPrimitive(false)
assertProperValExOfPrimitive(-42000)
assertProperValExOfPrimitive(0)
assertProperValExOfPrimitive(1)
assertProperValExOfPrimitive(42000)
assertProperValExOfPrimitive('')
assertProperValExOfPrimitive('asdf')
})

it('decodes Soroban Buffer values to Apalache JSON IR ValEx', () => {
assertProperValExOfBuffer({ type: 'Buffer', data: [0] }, '00')
assertProperValExOfBuffer({ type: 'Buffer', data: [190, 239] }, 'beef')
})

it('decodes Soroban Vec values to Apalache JSON IR', () => {
assertProperVec([])
assertProperVec([1, 2, 3])
assertProperVec(['a', 'b'])
})

it('decodes Soroban Map values to Apalache JSON IR', () => {
assertProperMap({})
assertProperMap({ 1: 'a' })
assertProperMap({ a: 2, b: 3 })
})

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'))
it('finds appropriate types for primitive values', () => {
assert.equal('TlaBool', tlaJsonTypeOfPrimitive(true))
assert.equal('TlaBool', tlaJsonTypeOfPrimitive(false))
assert.equal('TlaInt', tlaJsonTypeOfPrimitive(-42000))
assert.equal('TlaInt', tlaJsonTypeOfPrimitive(0))
assert.equal('TlaInt', tlaJsonTypeOfPrimitive(1))
assert.equal('TlaInt', tlaJsonTypeOfPrimitive(42000))
assert.equal('TlaStr', tlaJsonTypeOfPrimitive(''))
assert.equal('TlaStr', tlaJsonTypeOfPrimitive('asdf'))
})
})

0 comments on commit b4224b7

Please sign in to comment.