ITF serialization of `Value`s #36

Kukovec · 2024-04-22T15:47:51Z

closes #35

Introduces the following:

the State type
A rudimentary type system, notationally based on that of Apalache, with type literals from Soroban (u32, symb, etc.)
An ITF representation (of a single state) as a length-1 trace
modifies validity checks on collections, to require homogeneous contents, unless explicitly allowed otherwise.

thpani

A first set of comments.

The ITF-serialization of state looks good.

I've not had time to look at all the code for supporting nonhomogenous collections.

solarkraft/test/io/itf.test.ts

solarkraft/test/state/value.test.ts

thpani · 2024-04-22T18:11:10Z

solarkraft/src/io/itf.ts

+        case 'arr':
+            // array of 0/1 s, must be wrapped
+            return v.val.map(numWrap)


afaict, for a byte[] = 101 this would give

[{ "#bigint": "1" }, { "#bigint": "0" }, { "#bigint": "1" }]

?

Yes, I did it for consistency, but for Bytes specifically, we could deviate from ITF and just use the JS numbers, since it's only 0s and 1s, b/c I do agree that it's a bit clunky.

If it's an array of zeroes and ones, why would not we just wrap it as a string, e.g., by introducing a new kinds of a field { "#bytes": "101" }, or by just using an array of numbers, as you are suggesting. Actually, ITF does not prohibit JS numbers from being used for the small ranges.

IIRC we had a discussion about standardizing this in Apalache where every value was #bigint. But yeah, we don't have to 100% copy ITF here

Why do we encode a bytes[] as bits in the first place?

because I'm illiterate apparently

Is this question resolved? I am not sure I understand the last comment.

Yes, I fixed it. bytes = number now, and the validations check for 2^8

solarkraft/src/io/itf.ts

solarkraft/src/state/value.ts

thpani · 2024-04-23T07:26:45Z

solarkraft/src/state/value.ts

+        case 'arr':
+            return 'Bytes'


How is 'arr' different from the other basic types?

I'll add a comment about this inline, but I wanted to convey that Bytes, while it is a collection, is basically atomic as a type, since it's always an array of exactly 0s or 1s. I felt like using the word array/arr might give the impression that this is an array in the traditional sense, i.e. a fixed-sized ordered collection of arbitrary values, which is very much not supported (but there is Vec).

I have added a comment on that. I think it would improve our understanding of the issue if you added a link to the original description of this datatypes in Stellar or Soroban SDK?

konnov

Left a few comments

konnov · 2024-04-23T12:46:46Z

solarkraft/src/io/itf.ts

+        case 'arr':
+            // array of 0/1 s, must be wrapped
+            return v.val.map(numWrap)


If it's an array of zeroes and ones, why would not we just wrap it as a string, e.g., by introducing a new kinds of a field { "#bytes": "101" }, or by just using an array of numbers, as you are suggesting. Actually, ITF does not prohibit JS numbers from being used for the small ranges.

konnov · 2024-04-23T12:47:38Z

solarkraft/src/io/itf.ts

+        timeStyle: 'long',
+    })
+
+    // const desc = `Created by Solarkraft on ${formatter.format(new Date().getTime())}`


Suggested change

// const desc = `Created by Solarkraft on ${formatter.format(new Date().getTime())}`

Oh, actually, considering the other response I made, it should be this line that stays uncommented and the line below removed. Either way, do you have a preference for one of the two approaches to dates?

Idk. Perhaps, using the UTC date would be more consistent. I don't have any strong preference.

konnov · 2024-04-23T12:49:51Z

solarkraft/src/state/value.ts

+}
+
+// Returns the full type annotation of the provided (possibly complex) Value `v`.
+// It uses Apalache-style type notation, with Soroban type primitives.


what is Apalache-style type notation? What we see below looks like Soroban to me.

Well, our "maps" are A -> B

thpani · 2024-04-23T13:23:39Z

@Kukovec your last commit deleted ~2kLOC from the npm lockfile.
I doubt that's intended?

Kukovec · 2024-04-23T13:27:32Z

@Kukovec your last commit deleted ~2kLOC from the npm lockfile. I doubt that's intended?

I have not touched it beyond what npm run test, npm run lint and git commit do, I have no why it's like that.

konnov · 2024-04-23T13:33:53Z

@Kukovec your last commit deleted ~2kLOC from the npm lockfile. I doubt that's intended?

I have not touched it beyond what npm run test, npm run lint and git commit do, I have no why it's like that.

Oh, that's indeed strange. It looks like all of yargs and eslint is about to be removed from package-lock.json. There are plenty of packages I have no idea about though.

Kukovec · 2024-04-23T13:42:35Z

I just took the package-lock that was on remote main, still no idea what caused the deletion.

konnov

I have left a few comments on the unresolved issues. I think we should resolve as much as we can asap and merge this PR.

konnov · 2024-05-07T16:20:04Z

solarkraft/src/state/value.ts

+            // As a type, `Bytes` is atomic, even though it is an array. We avoid `arr`, as it could imply
+            // a generic array type, which does not exist.
+            return 'Bytes'


I do not understand what it means for a type to be atomic. Atomicity means that a value is updated in a single machine instruction, or it is updated in a way such that another thread/process cannot interfere with an update. Do you mean that a value of type Bytes is opaque in the sense that it cannot be decomposed into smaller pieces? I am still not sure about the second sentence. What is a generic array type that does not exist?

Atomic as in the smallest type-term (or in this context, not a generic collection). E.g. Array[T] would be a generic array, which Bytes is not. There is Vec, which is a dynamic, non-fixed sized collection, but there are no arrays in the Rust sense.

I'll rewrite this a bit.

konnov · 2024-05-07T16:22:27Z

solarkraft/src/state/value.ts

+        case 'arr':
+            return 'Bytes'


I have added a comment on that. I think it would improve our understanding of the issue if you added a link to the original description of this datatypes in Stellar or Soroban SDK?

konnov · 2024-05-07T16:24:14Z

solarkraft/src/io/itf.ts

+        timeStyle: 'long',
+    })
+
+    // const desc = `Created by Solarkraft on ${formatter.format(new Date().getTime())}`


Idk. Perhaps, using the UTC date would be more consistent. I don't have any strong preference.

itf

d074630

Kukovec requested review from thpani, konnov and andrey-kuprianov April 22, 2024 15:47

fix'd test

516d4b0

thpani reviewed Apr 23, 2024

View reviewed changes

PR comments

3d6e342

Kukovec requested a review from thpani April 23, 2024 11:50

konnov reviewed Apr 23, 2024

View reviewed changes

Kukovec added 2 commits April 23, 2024 15:36

PR comments

1c51d1e

yoinked PL from origin/main]

8acd481

Kukovec requested a review from konnov May 6, 2024 14:23

konnov approved these changes May 7, 2024

View reviewed changes

Kukovec added 2 commits May 7, 2024 18:52

PR comments

f9bb6a3

PR comments

0743872

Kukovec merged commit 1406d59 into main May 7, 2024
2 checks passed

Kukovec deleted the jk/itf branch May 7, 2024 16:59

konnov added this to the M1: Transaction extractor milestone May 10, 2024

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

ITF serialization of `Value`s #36

ITF serialization of `Value`s #36

Kukovec commented Apr 22, 2024 •

edited

Loading

thpani left a comment

thpani Apr 22, 2024

Kukovec Apr 23, 2024

konnov Apr 23, 2024

Kukovec Apr 23, 2024

thpani Apr 23, 2024

Kukovec Apr 23, 2024

konnov May 7, 2024

Kukovec May 7, 2024

thpani Apr 23, 2024

Kukovec Apr 23, 2024

konnov May 7, 2024

konnov left a comment

konnov Apr 23, 2024

konnov Apr 23, 2024

Kukovec Apr 23, 2024

konnov May 7, 2024

konnov Apr 23, 2024

Kukovec Apr 23, 2024

thpani commented Apr 23, 2024

Kukovec commented Apr 23, 2024

konnov commented Apr 23, 2024

Kukovec commented Apr 23, 2024

konnov left a comment

konnov May 7, 2024

Kukovec May 7, 2024

Kukovec May 7, 2024

konnov May 7, 2024

konnov May 7, 2024

ITF serialization of Values #36

ITF serialization of Values #36

Conversation

Kukovec commented Apr 22, 2024 • edited Loading

thpani left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

konnov left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

thpani commented Apr 23, 2024

Kukovec commented Apr 23, 2024

konnov commented Apr 23, 2024

Kukovec commented Apr 23, 2024

konnov left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

ITF serialization of `Value`s #36

ITF serialization of `Value`s #36

Kukovec commented Apr 22, 2024 •

edited

Loading