Engine: rework global name representation

[W95Psp]

This PR implements #1163.
It is expected most of the issues in #1135.

This PR is about:

• the internal representation of the global concrete identifiers in the engine
• the interface for manipulating those identifiers in the rest of the engine

Motivation

The previous design for global identifiers assumed every identifiers came from Rust. This was true at that time.

Since then, we shifted from that. The engine now creates names in the following situations:

• pre and post conditions on traits (those don't exist in Rust, we thus need to create identifiers)
• casts operations for enum with explicit representations (those are primitive in Rust, thus have no identifier)
• corss-module bundles of mutually recursive items (we now create new modules, containing only new identifiers)

The assumption that all the identifiers come from Rust is thus now completly broken, hence the need to move out from the current design.

A second motivation is the fact Rust identifiers were coming without any "kind" information: in the engine, we were not able to state whether a given identifier was, say, a struct or a function.
This was a big problem when printing names in the backends: the name of, e.g., a type cannot be printed with the same logic as, e.g., a constant.

Previous design

A concrete identifier in hax was basically a tuple containing:

• a slightly modified raw Rust DefId
• a metadata that gave a hint about the kind of item we were dealing with

In the previous design, we added incrementally hooks into that raw rust DefId representation so that we could alter the identifiers. This was providing us a way to create new identifiers.

Printing names

Rust have a very flexible namespacing.
Modules are just one way of doing namespacing: item declaration is allowed in expression bodies, thus items can be nested arbitrarily.

It is possible e.g. to define a module within an anonymous const within a method implementation.

The logic for printing name was very complicated and hard to maintain or to fix.

New design

Frontend

#1198 made the frontend output a definition kind along with any Rust definition identifier. Before that, #1054 added a parent information for each Rust defition identifier.

Together, those two PRs makes the frontend output, for each defintiion identifiers: (1) the full chain of identifiers up to the crate root (2) a precise definition kind, informing us precisely about the definition.

Engine

Representation

Now the engine has a representation for concrete identifiers in three layers:

• raw Rust identifiers: the DefId type, generated from Rust to OCaml, defined by the frontend
• Explicit_def_id: wraps a rust raw identifier, adding a metadata to disambiguate types and constructor (see the documentation of this module for more details)
• Concrete_ident: a Explicit_def_id that can be moved to a fresh module name and/or have a hygenic suffix

Concrete_ident is an type that describes an eventual need of freshness: the underlying explicit def id are never touched. Before Concrete_ident, every identifier comes from Rust.

The freshness of concrete identifier is guaranteed lazily: when one request the rendering of a concrete identifier, then the engine will produce a stable but fresh name.

View

Working with raw rust identifier is difficult, espcially for rendering identifiers as string in the backends.

Rust represents identifiers as a crate and a path. Each chunk of the path of an Rust identifier is roughly a level of nest in Rust. The path lacks informations about definition kinds.

There is two kinds of nesting for items.

• Confort: e.g. the user decides to embed a struct within a function to work with it locally.
• Relational: e.g. an associated method has to be under a trait, or a field as to be under a constructor.

Instead, the view transform each path as a list of smaller relational paths. For instance, consider the following piece of code:

mod a {
   impl MyTrait for MyType {
        fn assoc_fn() {
            struct LocalStruct {
                 field: u8,
            };
        }
   }
}

Here, the Rust raw definition identifier of LocalStruct is roughly a::my_crate::<Impl 0>::assoc_fn::LocalStruct::field.

The view for LocalStruct looks like:

{
   path: ["mycrate"; "a"],
   name_path: [
        `AssociatedItem ("assoc_fn", `Impl 0);
        `Field ("field", `Constructor ("LocalStruct", `Struct "LocalStruct"))
   ]
}

Such a hierachical path approach makes printing names much easier under the following constraints:

• ensuring names do not clash
• making sure the Rust namespaces map to the correct namespaces in the backends (e.g. Rust puts constructor in the same namespace as functions, this is not true for F*)
• items can generally cannot be nested in the backends, thus we need to fake nesting.

Progress

• Frontend/exporter: Add a kind field to DefIdContents #1198
• explicit def ids (see module Explicit_def_id)
• view interface (see module Concrete_ident_view_types)
• intepret Rust names as views (see module Concrete_ident_view)
• fresh modules (see module Concrete_ident > Fresh_module)
• redesign the API for printing names from the backends (this offers an API much more flexible, in the spirit of Raw view on concrete_ident #793 and [META] Engine: enhancements to the concrete ident view API #973)
• redesign the API of concrete idents (see module Concrete_ident)
• propagate the changes of the API everywhere
• documentation
• make the engine not crash on existing code: the DefKinds of Rust have 31 variants, and I need to ensure that any combination is handled correctly by the view
• kill any regression in the printing logic for identifiers in the F* backend:
  • tests folder
  • examples folder
  • Bertie
  • Libcrux
  • Sandwich
• go though each issue of [Meta] Naming issues #1135, and check if the PR fixes the issue:
  • Cyclic dependency with trait impl #1124
  • Engine: name clash with nested mod and fns #1136
  • traits in recursive bundles are called v_... instead of t_... #1156
  • Engine: name clash for items within trait methods #1161
  • Constructor prefixed with t_ in rec bundle #1169
  • Engine: F*: Missing rec qualifier in a mutually recursive top-level let #1158
  • Multiple tuple structs naming inconsistency. #1097
  • engine: F*: wrong field name for enum variant with record payload #1132
  • Clash of constructor names in recursive bundle #1274
• Revert the following:
  • fix(engine) Fix crash with hax_lib::fstar::before in recursive bundles #1179

Review status

@karthikbhargavan and @maximebuyse, you can already take a look at the all modified OCaml modules in the subdirectoy engine/lib/concrete_idents.

[maximebuyse]

I get a crash on the following example:

mod a {
    #[derive(PartialEq/* , Eq, Copy, Clone, Debug */)]
    struct Test();


    pub fn g(){super::b::h()}
}

mod b {

    pub fn h(){super::a::g()}
}

Here is the error message (with a change to make the ident readable):

Fatal error: exception Failure("Fatal error: in dependency analysis, we construct a renaming key-value list with a guarantee of unicity in keys. However, we found the following key twice:rust_primitives::hax::dropped_body_pre")

[maximebuyse]

I get a crash on the following example:

mod a {
    #[derive(PartialEq/* , Eq, Copy, Clone, Debug */)]
    struct Test();


    pub fn g(){super::b::h()}
}

mod b {

    pub fn h(){super::a::g()}
}

Here is the error message (with a change to make the ident readable):

Fatal error: exception Failure("Fatal error: in dependency analysis, we construct a renaming key-value list with a guarantee of unicity in keys. However, we found the following key twice:rust_primitives::hax::dropped_body_pre")

I pushed a fix to that (removing dummy methods in opaque trait impls), and to another small problem.

The next problem I have can be reproduced with:

mod a {
   struct Test {
    r: i32
   }


    pub fn g(){super::b::h()}
}

mod b {

    enum Test {
        A(i32)
    }

    pub fn h(){super::a::g()}
}

Open this code snippet in the playground

We discussed this and the problem is that the internal representation of paths within modules carries information about which kind of items they represent. So the ident of enum Test and struct Test are considered different which is wrong because in the end they are rendered in the same way. We should compare them rendered, but there is one problem with that: trait method names in trait impls, and trait definitions would be considered clashing (and one would be renamed), and this is wrong.

[maximebuyse]

I fixed all the bugs I found. I tested on sandwich which now type-checks when extracted with this branch (it even works without patch). For libcrux we need a few changes to the raw fstar that I have put in cryspen/libcrux#774.

[maximebuyse]

Libcrux CI succeeded with this PR: https://github.com/cryspen/libcrux/actions/runs/13048916135/job/36405261000.

I just have one thread opened about a comment, I think we should merge soon.

[maximebuyse]

I reverted #1075 as part of this branch to avoid conflicts. The corresponding issue will still be fixed thanks to the new naming.

[karthikbhargavan]

Generally, the changes look fine to me. Let' merge, but first also ask Lasse to take a quick look if he has time?

[W95Psp]

@cmester0, this PR is changing the names within hax, and this will probably break things in the Coq or SSProve backends and/or examples.
Let's collect regressions, I can help fixing things if needed, let me know.

[maximebuyse]

The ml-kem job failed in the merge queue. The reason is that the dependency to hax-lib in the Cargo.toml points to the main branch of hax. So even if using this PR for both the extraction and the F* core lib works, the job fails (because it uses this PR for extraction and main for the F* core lib)