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.

1 Like

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?

I strongly disagree that any part of our language design should be motivated by ease of “running an entire program as a single file in a web interface”. But your comments are mostly good nonetheless.

In particular, within a specific program I agree that we should think of mod statements in terms of “flattening”, and regardless of location on disk, we should wind up with a canonical tree of modules equivalent to one written in a single file using explicit mod {} blocks.

We should use relative paths to some “project root” which probably we will need to define as the location of some manifest file, similar to Rust and Cargo.toml. Then we can copy Rust in saying that mod mymod; imports the contents of mymod.rs or mymod/mod.rs or mymod/mymod.rs (except that let’s pick one and stick with it please) (and drop Rust’s stupid -/_ conversion rules). We can whitelist our character sets, and between that and relative paths, there will be no cross-system incompatibilites.

It’s easy to define an object’s canonical path by referring to the tree of mods. No re-exports or other shenanigans will affect these canonical paths.

Now, when we introduce external libraries, we need to go beyond the module system and define something analogous to Rust’s “crates”. Here is where we start to get into trouble, and here’s where I think your concern is. What Rust does is very ad-hoc and really not appropriate for a language where we care deeply about supply-chain security. Essentially:

  • rustc itself has very little notion of “crates”; it only knows about rlibs and never treats two distinct rlibs as being the “same” for purpose of type compatibility
  • cargo’s job, among other things, is to compile all the crates into rlibs and to decide which ones are “the same”, which it does using complicated semver-compatibility rules and even more complicated rules surrounding paths, registries, git urls, [patch] overrides, etc. But once it does that, then rustc’s job becomes easy.
  • But the Rust standard library is a special case; this is bundled with rustc, is considered unique by fiat, and you cannot have multiple versions of the standard library in play (and since 1.0 they have made huge efforts, mostly successfully, to ensure that no breaking change ever occurs in stdlib so this can work by everybody just declaring their “minimum supported rust version” and requiring the maximum of all MSRVs in a dependency tree).

The problem of crates, I think, is separate and deserves a separate issue. But I think the broad paradigm of “the compiler just sees a pile of named rlibs, with all names distinct, and each one is a tree of mods with types identified by their path within the rlib, and no two rlibs’ types are equivalent” is the right one.

So we can push our problem out one level to “how do we produce the pile of named rlibs”?

What do we actually want to get out of nominal identity here, in the end?

Without nominal typing we might as well have no type system at all. Without nominal typing users have almost no way to specify or verify the invariants they require on their objects and they will be flying blind.

2 Likes

Thanks, this clears up a lot. Below is a concrete proposal that tries to bring posts #3, #4 and #8 together, with an end-to-end example.

General idea

Let’s start with modules. We can move to Rust 2018-style modules:

  • mod x; is exactly equivalent to mod x { <contents of x.simf> }. Paths are resolved relative to the declaring file, and only declared files are loaded.
  • use only brings names into scope. Unlike the current implementation, it never loads files.
  • crate:: refers to the root of the enclosing crate’s module tree.
  • A module’s identity is its position in the module tree, not the file it came from. Two structurally “equal” types declared in different modules are different types.

Crates and CrateId

A crate is a module tree plus a set of dependencies, each under a local alias. Aliases are chosen by the importer and are not identity. For example, two crates may both use the alias math for different libraries, or use different aliases for the same library.

Identity is a Merkle-style hash over content and dependencies:

CrateId = H_crate( H_files(module tree), H_deps(sorted (alias, CrateId(dep))) )

  • Paths, URLs, git refs and package names are not part of it. Where the code came from is the job of the build tool (e.g. Simplex), not SimplicityHL.
  • Diamonds deduplicate naturally: if A and B both depend on C under different aliases, they both see the same CrateId(C).
  • Dependency cycles between crates are forbidden, since the hash requires a DAG.

A nominal type is then identified by (CrateId, module path, name). Re-exports and use ... as don’t affect it.

Open problem: ordering

Today ordering is simple: files are atomic units, and a post-order DFS sorts them topologically along their use edges (introduced in #279). With a structure like

A -> B -> C
A -> C

the result can interleave crates: some files from C, then some from B, then more from C.

With module trees this changes. Each crate is loaded as a whole (its root file plus every declared mod), so crates become atomic by construction. Ordering crates is still a DFS, just over crates instead of files, with a deterministic tie-break (e.g. by CrateId).

The remaining problem is ordering inside a crate. The AST is analyzed in a single pass, so an item must come before anything that uses it. Once modules sit where their mod is written, the driver can no longer reorder them:

// lib.simf
mod a;    // a.simf: use crate::b::f;   <- b is not analyzed yet
mod b;    // b.simf: pub fn f() {}

I see two options:

  1. Require users to declare modules and imports in dependency order. (I think this is the worse option.)
  2. Resolve the order automatically, e.g. collect all declarations in a crate first and then resolve use statements. This also allows modules that refer to each other, but it’s more work.

This is still an open question.

Example

keys/                 # dependency: simc ... --dep keys=keys/
  lib.simf            # crate root (like src/lib.rs)
  kind.simf

project/
  main.simf           # entry crate root (like src/main.rs)
  action.simf

keys/lib.simf

pub mod kind;

keys/kind.simf

pub enum Kind { Cold([u8; 64]), Hot([u8; 64]) }

project/action.simf

pub enum Action { Inherit([u8; 64]), Spend }

project/main.simf

mod action;

use crate::action::Action;
use keys::kind::Kind;        // `keys` is in scope from --dep, as with --extern in Rust

fn main() {
    let action: Action = witness::ACTION;
    let kind: Kind = witness::KIND;
    /* ... */
}

Single-file form

Each dependency becomes a top-level crate block tagged with its CrateId, plus an explicit alias that takes the place of --extern. The root crate is not wrapped, and every use path stays exactly as written. The syntax is a placeholder:

extern crate "3f2a9c..." {
    pub mod kind {
        pub enum Kind { Cold([u8; 64]), Hot([u8; 64]) }
    }
}

extern crate "3f2a9c..." as keys;

mod action {
    pub enum Action { Inherit([u8; 64]), Spend }
}

use crate::action::Action;
use keys::kind::Kind;

fn main() { /* ... */ }

Properties:

  • Crate blocks only appear at the top level. Crates form a DAG, so they can’t be nested.
  • A program without dependencies is already in this form.
  • Flattening becomes idempotent: flatten(flatten(p)) == flatten(p). Today it isn’t. The driver wraps the entry file in mod unit_0 { ... }, so fn main ends up inside a module, and flattening the output again fails with MainOutOfEntryFile. Even with main at the top level, every flatten would add another wrapper layer.
  • The CMR is the same as in the multi-file build, since names never reach Simplicity.

Note: keys could contain both lib.simf and main.simf, acting like two kinds of manifest. Each compilation uses exactly one of them as its root: lib.simf when keys is loaded as a dependency (e.g. --dep keys=keys/lib.simf), main.simf when it’s compiled as an entry point. This separates what is published as a library from binaries and test-only modules, which can be declared in main.simf alone.

ABI

Root crate types use crate::, and dependency types use their CrateId. The root’s own CrateId is never printed, because it changes on every edit and would break witness files. Each entry also carries the full definition, with variants in order, so tools can encode values:

{
  "crates": { "3f2a9c...": { "alias": "keys" } },
  "witness_types": {
    "ACTION": {
      "type": "crate::action::Action",
      "def": { "enum": [["Inherit", "[u8; 64]"], ["Spend", "()"]] }
    },
    "KIND": {
      "type": "3f2a9c...::kind::Kind",
      "def": { "enum": [["Cold", "[u8; 64]"], ["Hot", "[u8; 64]"]] }
    }
  }
}

Witness files are unchanged.

{ "ACTION": "Action::Inherit(0x...)", "KIND": "Kind::Hot(0x...)" }

If a second, different dependency also had an enum called Kind, its witness would carry a different CrateId in the ABI, and the value would be checked against that type. Colliding names or aliases can’t be confused.

Out of scope: domain separation

This post doesn’t address hashing. TypeId changes whenever a crate’s code changes, so it must not be used as a domain separator for hash(value), since committed hashes have to survive upgrades. This can be handled separately, along the lines of post #4 (explicit opt-in with a user-chosen tag). Nothing here blocks it.

Questions

  1. Syntax: what should crate blocks and aliases look like? The placeholders above are extern crate "<id>" { ... } and extern crate "<id>" as <alias>;.
  2. What should H_files hash: raw file bytes, a normalized module tree, or something else? Only a normalized form lets the compiler verify the ids in the single-file form, so this needs further discussion.
  3. How should a crate’s role (library vs entry point) be specified: inferred from how the file is passed, or with an explicit flag?

Following up on the open questions from #9.

Ordering. Crates already form a DAG, since CrateId hashes the dependencies. I propose the same rule inside a crate: the use graph between modules must be acyclic, so module a can’t import from b while b imports from a. With that, the driver sorts modules topologically, and users never have to order mod or use declarations. In the single-file form, dependencies become top-level crate blocks listed in that order. Item order doesn’t affect the CMR, so the driver is free to reorder items.

Hashing. I’d use the same tagged SHA-256 construction as for debug symbols, applied to the parsed module tree: items, names, types and module structure, plus the (alias, CrateId) pairs of dependencies. Source positions and compiler-assigned file ids are excluded, so reformatting or changing the order in which dependencies are found doesn’t change the id. We can narrow the hashed fields later.

ABI. #9 puts CrateId into ABI type names, which we prefer to hide. Here’s how Lean 4 and Rocq name items from libraries:

  • Lean 4: a module’s name is its file path inside the package’s source directory (Mathlib/Data/Nat/Basic.lean → Mathlib.Data.Nat.Basic) (reference). A declaration is identified by that name alone. If two imports define the same name, the import fails (Environment.lean).
  • Rocq: the build binds each library directory to a logical name with -Q dir Name (manual), and that name prefixes every kernel name in the library (ModPath).

Both work because each library has one global name for the whole build. In #9, aliases are chosen by each importer, so they aren’t unique: the root and a dependency can both use keys for different crates. Keying the ABI by alias would make those two indistinguishable.

Another option is to name a dependency by its alias chain from the root (keys vs a/keys). That makes names unique, but they then depend on the whole graph: if the root later adds a direct dependency on a crate it previously reached through a, that crate’s ABI names change although its code and CrateId didn’t.

So with freely chosen aliases, CrateId is the only name that is both unique and independent of the graph. We can keep it in the ABI only, and never put it in argument or witness files