[Epic] M3: Fetch type info from WASM

[thpani]

Currently, we sometimes require users to annotate types (using fetch --typemap) to disambiguate XDR types when translating to Apalache types.

In particular, string-typed Soroban Vecs and Enums are indistinguishable at the type level.

[thpani]

Workflow using stellar-cli:

$ stellar contract fetch --id CAPUXZNADOIO2RBXGAPCYIZI55FVVYGMDZL6RR26S5KFCFHRXBHQN4SP --network testnet >set.wasm
$ stellar contract inspect --wasm set.wasm --output xdr-base64-array

inspect.rs uses wasmparser to extract the contract spec.

[thpani]

example enum declaration

example function with UDT param

[thpani]

Workflow using stellar-sdk:

const client = await new sdk.contract.Client.from({
    rpcUrl: 'https://soroban-testnet.stellar.org',
    contractId: 'CAPUXZNADOIO2RBXGAPCYIZI55FVVYGMDZL6RR26S5KFCFHRXBHQN4SP'
})
console.log(client.spec.jsonSchema().definitions?.set_struct.properties.args)
console.log(client.spec.jsonSchema().definitions?.MyStruct)
console.log(client.spec.funcs().map(f => f.name().toString()))
console.log(client.spec.findEntry('MyStruct'))

outputs

{
  additionalProperties: false,
  properties: { v: { '$ref': '#/definitions/MyStruct' } },
  type: 'object',
  required: [ 'v' ]
}
{
  description: '* A simple two-field structure.',
  properties: {
    a: { '$ref': '#/definitions/U32' },
    b: { '$ref': '#/definitions/I128' },
    additionalProperties: false
  },
  required: [ 'a', 'b' ],
  type: 'object'
}
[
  'init',       'set_bool',    'get_bool',
  'set_u32',    'get_u32',     'set_i32',
  'get_i32',    'set_u64',     'get_u64',
  'set_i64',    'get_i64',     'set_u128',
  'get_u128',   'set_i128',    'get_i128',
  'set_sym',    'get_sym',     'set_bytes',
  'get_bytes',  'set_bytes32', 'get_bytes32',
  'set_vec',    'get_vec',     'vec_push',
  'set_map',    'get_map',     'map_set',
  'map_get',    'set_address', 'get_address',
  'set_struct', 'get_struct',  'set_enum',
  'get_enum'
]
ChildUnion {
  _switch: ChildEnum { name: 'scSpecEntryUdtStructV0', value: 1 },
  _arm: 'udtStructV0',
  _armType: [class ChildStruct extends Struct] {
    structName: 'ScSpecUdtStructV0',
    _fields: [ [Array], [Array], [Array], [Array] ]
  },
  _value: ChildStruct {
    _attributes: {
      doc: <Buffer 2a 20 41 20 73 69 6d 70 6c 65 20 74 77 6f 2d 66 69 65 6c 64 20 73 74 72 75 63 74 75 72 65 2e>,
      lib: <Buffer >,
      name: <Buffer 4d 79 53 74 72 75 63 74>,
      fields: [Array]
    }
  }
}

[thpani]

It's worth reading the conversion code in contract.Spec: scValToNative and nativeToScVal. It uses the contract.Spec to coerce ScVals / native values into the proper native / XDR representation. We can do the same with ScVals -> TLA+ values.

Exporting the contract spec in the fetcher would allow us to disambiguate types of function parameters and returns.
NB: For storage fields, we would still have to rely on type information from the monitor to disambiguate values.

The alternative is to rely on type info from the monitor for all conversions.

[thpani]

While we can get function signatures from WASM, it does not solve our problem with typing storage.

Instead, we should do what Soroban itself is doing: take the data we get, and attempt to coerce it into the type given in the monitor (and fail if we can't). For this, we first need to finalize the monitor format in #136.