Coda is a new cryptocurrency that uses zk-SNARKs to dramatically reduce the size of data needed by nodes running its protocol. Nodes communicate in a format automatically derived from type definitions in OCaml source files. As the Coda software evolves, these formats for sent data may change. We wish to allow nodes running older versions of the software to communicate with newer versions. To achieve that, we identify stable types that must not change over time, so that their serializations also do not change.
To enforce the stability of types, we use three OCaml extension point (“ppx”) implementations. One ppx is a linter that enforces usage patterns of stable types. For example, the linter enforces that all serialized types are marked as versioned, and that serialized types cannot be generated by functor applications. Another ppx marks types as versioned. The typechecker assures that such types are made up only of other versioned types, even when they’re defined in other files. Errors flagged by the linter and version ppx are made visible in editors running the Merlin tool for OCaml.
The last ppx allows marking a module of stable types and generating boilerplate definitions, including annotations to indicate that the contained types are serializable and versioned. Serialized data contains an automatically-generated version byte that identifies a particular version, which we can deserialize and transform to the latest version.
Coda developers are aware that stable types should not be modified, but mistakes can happen. We can run the version ppx in a special way to print out representations of versioned types. A script in the Coda continuous integration setup uses that facility to compare versioned types in Github pull requests, and flags inadvertent changes.
By combining these techniques, we propose a simple and flexible strategy for future-compatible communication in OCaml.
Fri 28 Aug Times are displayed in time zone: Eastern Time (US & Canada) change
|11:30 - 12:00|
|OCaml Under The Hood: SmartPy|
Sebastien MondetTQ Tezos
|12:00 - 12:30|
|A Declarative Syntax Definition for OCaml|
Luis Eduardo de Souza AmorimDelft University of Technology, Netherlands, Eelco VisserDelft University of TechnologyPre-print
|12:30 - 13:00|
|LexiFi Runtime Types|
|13:00 - 13:30|
|Types in amber|