Nominal Types and Module Identification in SimplicityHL

In this Github issue about Ctx8 ergonomics it is proposed that we should have a built-in method to compute the hashes of Simplicity values. Currently, to do this you must manually destructure your object into basic Simplicity types and then invoke jets (one for each size of data) which update a sha256 engine. This is verbose, error-prone, and also invites high-level design mistakes regarding “what data gets hashed in what order” because it distracts the programmer with minutiae.

It would be much better if we could just write hash(value) regardless of the type of value.

But what exactly should this hash builtin do? (it is a builtin, not a function, because it must be polymorphic over its input type and SimplicityHL functions do not support this).

Well, we want this builtin to be a “secure hash function”. For our purposes, this means that no two distinct values are ever encoded as the same bits when feeding them into the hash engine. If we achieve this property, and we model SHA256 as a random oracle, then we automatically get all the security properties we might want: collision resistance, first and second preimage resistance, binding and hiding, etc. The question of “how do we encode data to be hashed” is a thorny one and not unique to Simplicity. The Rust Hash trait attempts to achieve this, for example. (Although Rust fails, even within the stdlib; it distinguishes &str strings from &[u8] bytestrings by suffixing a fix 0xff byte, meaning that a &str can be encoded the same way as a (&[u8], u8). If it’s okay that values of different types are encoded the same way, then why bother with the 0xff? Incoherent. So clearly this is not an easy property for even large software projects to properly define.)

An abvious way to implement hash is to just break apart the data into individual pieces and then hash that, like users are doing manually. Essentially “lower the value to its base Simplicity type, then encode that in the ‘compact encoding’ used by the Bit Machine”. Like with Rust’s Hash, this achieves our goal as long as we always use a fixed datatype (though often in surprising ways; the obvious way to encode a variable-length bytestring is to length-prefix it, but Simplicity instead breaks it into a series of optional power-of-two-length arrays).

But “collision resistant assuming a fixed type” is not sufficient. Bitcoin’s consensus code has multiple issues related to interpreting a hash of one object as a hash of a differently-typed object. CVE-2012-2459 (hashing a single SHA256 hash the same as a pair of SHA256 hashes) comes to mind, as does the issue solved by the Great Consensus Cleanup wherein a 64-byte transaction may be hashed the same as two transaction hashes. In both cases, nodes that are unaware of the bug may disagree on the contents of a given block, even if they agree on its hash. So clearly this is not an easy property for projects to achieve even when it’s critical to their security model.

However, we have the benefit of experience, and the knowledge that there is a standard way to prevent this class of bugs/attacks. We just need to domain-separate the hashes using BIP-0340 tagged hashes where the domain separation is per-type. Domain-separating by Simplicity type is easy: we already have a unique type identifier, the TMR, that we can just use as a tagged hash. Unfortunately, Simplicity does not distinguish between (u4, u4) and u8, for example, let alone types like Distance(u16) and Duration(u16). This is bad, and particularly bad because “structurally equal” types like these are the most likely to have values that might be confused for each other.

So we instead need to domain-separate by SimplicityHL type, and here’s where things get tricky. Currently SimplicityHL’s type system is really bad. It also supports only structural typing, so you can’t define newtypes which the compiler considers distinct, and it also conflates things like (u4, u4) and u8. It just adds a couple things iike lists and arrays to Simplicity’s bare-bones type system. So before we can domain-separate our hashes, we need a type identifier, and before we can define a type identifier, we need a coherent notion of what types are even distinct. The current “everything is the same if it’s shaped the same” situation is obviously untenable, but what will a better solution look like?

It’s easy enough to define a TMR-like hash for the built-in SimplicityHL types (which are essentially just the Simplicity types plus list and array) and further tweak it to distinguish built-in names like u16 from the (u8, u8)s that comprise them, and Distance(u16)/Duration(16). But what should we do with enums, enum variants, and other user-defined types? Clearly we do not want two types to get the the same hash if they come from different libraries, even if they have the same structure and even if they have the same name. But we also want the same type from the same library to always get the same hash. This requires we define “same type” and “same library” (or rather, “same module”) in a way where all users agree.

Again, Rust has little to offer us: its notion of the “same library” is actually that of “semver-compatible libraries” which are defined by the dtolnay/semver crate in weird and surprising ways. Cargo then lays on further rules for incompatibility based on the source of the crate (and registry sources have their own complex rules which don’t include any code signing or namespacing or anything), and allows these things to be overridden locally with [patch] and other methods. And then it takes this stew of ad-hoc rules and feeds them all into some hash that it gives to rustc which then separates the rlibs based on it. So we will need a different approach to modules.

Summing up: we need to define a coherent notion of type identity, which first requires we define a coherent notion of module identity. (And the latter is a whole separate discussion.) Until we do this, we can’t in-good-conscious offer a convenient API for hashing SimplicityHL values.

Very insightful and this topic is much more nuanced than I originally thought.

Importing libraries is nuanced as well. We do not precompile imported files, but rather include them before compilation. So my question is, should a multi-file SimplicityHL program have an exact equivalent single file SimplicityHL program? It is very useful to have a single file in certain use cases, such as including an uncompiled SimplicityHL program on a webpage dapp.

For most programs, there is little need to differentiate single file and multi-file. But when the exact types are important, as you’ve stated for hashing, we need to decide how this single file aggregation is done.

I think we should support inline mod {} syntax as in Rust. So use mymodule; is the same as mod mymodule { /* contents of mymodule.simf inline here */ }.

2 Likes

After thinking about this a bit more:

  • As I said above, mod x {} should be exactly equivalent to mod x where x refers to some x.simf (or whatever) file. This matches Rust where all modules live in a tree of mod {}s, and while you can make the API have whatever shape you want by using pub and use creatively, in the end everything’s “true name” is determined by where it lives in the mod tree. In particular, if you have two mod xs, even if the are identical (or even come from the same file), they are distinct modules and their types are not compatible.
  • However, in Rust, crates don’t work this way. The closest thing to mod is extern crate, and this creates a DAG, not a tree. If two extern crate invocations refer to “the same crate” then they really will pull in the same crate, and all types will be identical.

In SimplicityHL, like in Rust, I think we’ll need both concepts. The mod one is the “easy one” so I guess we should start with that, and we should maybe simulate external crates with some sort of include macro. (This is basically what we’re doing now, but I might like to tweak the syntax to make it clearer that this is more like a preprocessor hack than a principled solution. A principled solution is going to need to sort out this notion of “crate identity”.)

As for the “easy problem” of mods, we still would like to form a deterministic ID for every type. So suppose you have something like the following Rust code.

mod mymodule {
    pub struct MyType {
        pub x: usize,
        y: u64,
    }
}
pub use mymodule::MyType as MyType2;

In the corresponding SimplicityHL code, should the “type ID” of MyType change if

  • we add or remove private fields?
  • we change the visibility of existing fields?
  • we reorder fields?
  • we rename the type at its definition site?
  • we rename the type at its pub use site?
  • we rename the module?
  • we move the module to another place in the codebase? what if we re-export it at its old location?
  • etc etc

I don’t think there’s an obvious answer to any of these questions, and if we’re going to use the type ID for domain separation of hashes, then we’re in trouble no matter what. If we change the type ID when a user doesn’t expect it, then we will invalidate existing committed data and/or make contracts incompatible with each other. If we don’t change the type ID when the type has meaningfully changed, we risk introducing bugs where a hash of an object can be reinterpreted as a hash of a different object.

Furthermore, any change that we define to change the type ID becomes an API-breaking change, which will be pretty frustrating if it includes field reorderings or manipulations of private fields.

So for hashing purposes I think we need to back up and make the user explicitly opt into their types being hashable, and when they do, they should choose a domain separator. The compiler and LSP should suggest using (the hash of) “crate/mymodule/MyType/v1”, where crate can be replaced by the crate name if available (BTW do we have a word for “crates”? Should we just steal “crate”?).

They should optionally be able to specify the exact algorithm for hashing values of the type, but if not, the default one should take the user’s domain separator, mix some sort of (structural, not nominal) TMR into it, and then just hash the bits of the data (including all private fields, and do this in order).

Furthermore, to assist implementors (and partially solve the original “hashing is annoying” GIthub issue that started this whole thing) we should provide:

  • a structural_hash builtin which computes the “default hash” for an object
  • a raw_hash builtin which is only available for primitive types and which directly hashes bits with no domain separation or length prefixing or anything else

Probably both of these should consume a Ctx8 context and return an updated one, so anyone using them directly will need 1 or 2 lines of boilerplate (but no more).

Just to continue on modules/nominal types

Here is an example of a simf program after compilation:

mod unit_2 {
    pub fn not(bit: bool) -> bool {
    <u1>::into(jet::complement_1(<bool>::into(bit)))}
    pub fn or(a: bool, b: bool) -> bool {
    <u1>::into(jet::or_1(<bool>::into(a), <bool>::into(b)))}
    pub fn and(a: bool, b: bool) -> bool {
    <u1>::into(jet::and_1(<bool>::into(a), <bool>::into(b)))}
    pub fn xor(a: bool, b: bool) -> bool {
    and(or(a, b), not(and(a, b)))}
}
mod unit_4 {
    use crate::unit_2::{not, or, and};
    ...
}

Those 2 and 4 are not actual names of dirs/files, they are generated by the compiler itself

I believe this was yet another decision to reduce scope. And this is one of the reasons why enums cannot be used in the deps

We don’t really have specs for how simc does things, but perhaps we should write up the correct method of combining files, so that other preprocessors can do the same.

In support of the module and nominal types discussion, I want to lay out why we need modules and dependencies at all, and walk through why identifying nominal enums turned out to be so hard.

Let’s start with terminology. Dependencies let one .simf file load another. Modules, by contrast, exist for scoping and for flattening.

The main purpose of flattening is to make it possible to run a multi-file program in a web application, so the whole program can be shipped as a single string. This works because the AST stage already treats a program as a flat array of items in a well-defined order. The real problem flattening has to solve is: for a given item, which file did it come from, and in what order should files be loaded? Modules fit this well, because the driver already tracks each dependency by the order in which it’s discovered. Since we never reorder items within a file, we can treat each file as an atomic unit and wrap it in a mod <name> { ... } block. The only remaining question is what to name it, and since the driver already assigns each file a number (also used as its file_id), we reuse that number directly, which is why under the hood we end up with mod unit_N { ... }.

So what’s the problem with this for nominal enums? First, identification. Given a function f(x), we don’t want some y that merely resembles x to be substitutable in its place. So we need a precise way to say when two enum types actually count as “the same.”

The obvious first idea: compare the enum’s name and arms, plus the path to where it’s declared (multi-file enums PR 414). But a full absolute path differs machine to machine, compile the same program on Linux and on Windows and you get different paths. So maybe a path relative to some root? That runs into a different wall: a dependency can point at literally any directory on disk, so there’s no shared root to be relative to. Two different relative paths can end up pointing at the exact same block of code, and the same relative path can point at two entirely different blocks of code, depending on where that dependency happens to be mounted.

Okay, so what about identifying it the way use already does use <dep-name|crate>::<path>::<item>? Closer, but now the dep-name itself is arbitrary: I can call the standard library std in one project and std_hl in another, and get a different qualified path for identical code either way.

Then there’s re-exports. What if the item in question is just a re-export of something declared elsewhere? Two different use paths can point at the exact same underlying declaration under two different names, so a path alone can’t carry the whole notion of identity.

And even setting all of that aside, we have flattening itself: once a dependency is flattened into a consumer program, its internal structure, and any path we’d assigned it, no longer matches the structure it had as a standalone dependency. (unit_N itself is a good example of just how unstable this can get, because it’s assigned by discovery order, which shifts whenever an unrelated use changes anywhere upstream.)

All of which makes me wonder whether we should tie ourselves to paths at all, given how many ways they break.

Open to pushback and to redirecting this line of thinking. What do we actually want to get out of nominal identity here, in the end?