diff --git a/Cargo.lock b/Cargo.lock
index 0b6542b48..7b21cfbc6 100644
--- a/Cargo.lock
+++ b/Cargo.lock
@@ -437,6 +437,7 @@ dependencies = [
  "proc-macro2",
  "quote",
  "syn 1.0.109",
+ "tracing",
 ]
 
 [[package]]
diff --git a/cli/driver/Cargo.toml b/cli/driver/Cargo.toml
index adeb664b5..0f33501ff 100644
--- a/cli/driver/Cargo.toml
+++ b/cli/driver/Cargo.toml
@@ -7,6 +7,7 @@ homepage.workspace = true
 edition.workspace = true
 repository.workspace = true
 readme.workspace = true
+description = "The custom rustc driver used by hax."
 
 [package.metadata.rust-analyzer]
 rustc_private = true
diff --git a/cli/options/Cargo.toml b/cli/options/Cargo.toml
index 9c9289f72..f302e3f18 100644
--- a/cli/options/Cargo.toml
+++ b/cli/options/Cargo.toml
@@ -8,7 +8,7 @@ edition.workspace = true
 repository.workspace = true
 readme.workspace = true
 build = "build.rs"
-description = "hax cli options"
+description = "The CLI options read by the `cargo-hax` binary."
 
 [dependencies]
 serde.workspace = true
diff --git a/cli/options/engine/Cargo.toml b/cli/options/engine/Cargo.toml
index c38856459..2a649bb7b 100644
--- a/cli/options/engine/Cargo.toml
+++ b/cli/options/engine/Cargo.toml
@@ -7,7 +7,7 @@ homepage.workspace = true
 edition.workspace = true
 repository.workspace = true
 readme.workspace = true
-description = "hax cli options engine helper crate"
+description = "Defines the data type of the input of the engine. The (OCaml) engine reads JSON on stdin and deserializes the payload according to the JSON Schemas defined by this crate."
 
 [dependencies]
 serde.workspace = true
diff --git a/engine/dune-project b/engine/dune-project
index 8936a52b7..6df3f59e8 100644
--- a/engine/dune-project
+++ b/engine/dune-project
@@ -5,20 +5,20 @@
 (generate_opam_files true)
 
 (source
- (github username/reponame))
+ (github hacspec/hax))
 
-(authors "Author Name")
+(authors "Hax Authors")
 
-(maintainers "Maintainer Name")
+(maintainers "Hax Authors")
 
-(license LICENSE)
+(license "Apache-2.0")
 
-(documentation https://url/to/documentation)
+(documentation https://hacspec.org/hax/)
 
 (package
  (name hax-engine)
- (synopsis "A short synopsis")
- (description "A longer description")
+ (synopsis "The engine of hax, a Rust verification tool")
+ (description "Hax is divided in two: a frontend (written in Rust) and an engine (written in OCaml). This is the engine.")
  (depends
         ocaml
         dune
@@ -55,6 +55,5 @@
         sedlex
         )
  (tags
-  (topics "to describe" your project)))
+  (topics rust verification)))
 
-; See the complete stanza docs at https://dune.readthedocs.io/en/stable/dune-files.html#dune-project
diff --git a/engine/hax-engine.opam b/engine/hax-engine.opam
index 852dec1a8..72ba3a4c3 100644
--- a/engine/hax-engine.opam
+++ b/engine/hax-engine.opam
@@ -1,14 +1,15 @@
 # This file is generated by dune, edit dune-project instead
 opam-version: "2.0"
-synopsis: "A short synopsis"
-description: "A longer description"
-maintainer: ["Maintainer Name"]
-authors: ["Author Name"]
-license: "LICENSE"
-tags: ["topics" "to describe" "your" "project"]
-homepage: "https://github.com/username/reponame"
-doc: "https://url/to/documentation"
-bug-reports: "https://github.com/username/reponame/issues"
+synopsis: "The engine of hax, a Rust verification tool"
+description:
+  "Hax is divided in two: a frontend (written in Rust) and an engine (written in OCaml). This is the engine."
+maintainer: ["Hax Authors"]
+authors: ["Hax Authors"]
+license: "Apache-2.0"
+tags: ["topics" "rust" "verification"]
+homepage: "https://github.com/hacspec/hax"
+doc: "https://hacspec.org/hax/"
+bug-reports: "https://github.com/hacspec/hax/issues"
 depends: [
   "ocaml"
   "dune" {>= "3.0"}
@@ -56,7 +57,7 @@ build: [
     "@doc" {with-doc}
   ]
 ]
-dev-repo: "git+https://github.com/username/reponame.git"
+dev-repo: "git+https://github.com/hacspec/hax.git"
 depexts: [
   ["nodejs"] {}
-]
\ No newline at end of file
+]
diff --git a/frontend/diagnostics/Cargo.toml b/frontend/diagnostics/Cargo.toml
index 3b3ba0664..d506a5a64 100644
--- a/frontend/diagnostics/Cargo.toml
+++ b/frontend/diagnostics/Cargo.toml
@@ -7,7 +7,7 @@ homepage.workspace = true
 edition.workspace = true
 repository.workspace = true
 readme.workspace = true
-description = "hax diagnostics helper crate"
+description = "This crate defines types that represent the various errors that can occur in hax."
 
 [package.metadata.rust-analyzer]
 rustc_private=true
diff --git a/frontend/exporter/Cargo.toml b/frontend/exporter/Cargo.toml
index 5873503cf..3ac731416 100644
--- a/frontend/exporter/Cargo.toml
+++ b/frontend/exporter/Cargo.toml
@@ -7,7 +7,7 @@ homepage.workspace = true
 edition.workspace = true
 repository.workspace = true
 readme.workspace = true
-description = "hax frontend exporter helper crate"
+description = "Provides mirrors of the algebraic data types used in the Rust compilers, removing indirections and inlining various pieces of information."
 
 [package.metadata.rust-analyzer]
 rustc_private=true
diff --git a/frontend/exporter/adt-into/Cargo.toml b/frontend/exporter/adt-into/Cargo.toml
index bfb209c3a..eb292ec28 100644
--- a/frontend/exporter/adt-into/Cargo.toml
+++ b/frontend/exporter/adt-into/Cargo.toml
@@ -7,7 +7,7 @@ homepage.workspace = true
 edition.workspace = true
 repository.workspace = true
 readme.workspace = true
-description = "hax adt into helper crate"
+description = "Provides the `adt_into` procedural macro, allowing for mirroring data types with small variations."
 
 [lib]
 proc-macro = true
@@ -18,3 +18,5 @@ syn.workspace = true
 proc-macro2 = "1.0"
 quote = "1.0"
 
+[dev-dependencies]
+tracing.workspace = true
diff --git a/frontend/exporter/adt-into/README.md b/frontend/exporter/adt-into/README.md
new file mode 100644
index 000000000..951f91e3c
--- /dev/null
+++ b/frontend/exporter/adt-into/README.md
@@ -0,0 +1,15 @@
+# hax adt into
+
+This crate provides the `adt_into` procedural macro, allowing for
+mirroring data types with small variations.
+
+This crate is used by the frontend of hax, where we need to mirror a
+big part of the data types defined by the Rust compiler. While the
+abstract syntax trees (ASTs) from the Rust compiler expose a lot of
+indirections (identifiers one should lookup, additional informations
+reachable only via interactive queries), hax exposes the same ASTs,
+removing indirections and inlining additional informations.
+
+The `adt_into` derive macro can be used on `struct`s and `enum`s. `adt_into` then looks for another `#[args(<GENERICS>, from: FROM_TYPE, state: STATE_TYPE as SOME_NAME)]` attribute. Such an attribute means that the `struct` or `enum` mirrors the type `FROM_TYPE`, and that the transformation is carried along with a state of type `STATE_TYPE` that will be accessible via the name `SOME_NAME`.
+
+An example is available in the `tests` folder.
diff --git a/frontend/exporter/adt-into/tests/lib.rs b/frontend/exporter/adt-into/tests/lib.rs
new file mode 100644
index 000000000..efe14789d
--- /dev/null
+++ b/frontend/exporter/adt-into/tests/lib.rs
@@ -0,0 +1,56 @@
+/// For the example, let's assume we are working with `Literal`, an
+/// ADT that represents literal values. Suppose strings are
+/// represented via an identifier stored in a state `State`.
+pub mod source {
+    use std::collections::HashMap;
+    #[derive(Clone, Debug)]
+    pub struct State(pub HashMap<StringId, String>);
+
+    #[derive(Copy, Clone, Debug, Eq, PartialEq, Hash)]
+    pub struct StringId(u32);
+
+    #[derive(Clone, Debug)]
+    pub enum Literal {
+        Integer(u32),
+        String(StringId),
+    }
+}
+
+/// Here, we mirror the same data type `Literal`, but with a small
+/// difference: there is no `StringId` any longer: we define a `impl`
+/// of `SInto` specifically for `StringId`, that ships with a stateful
+/// lookup. Magically, everytime a mirrored datatype annotated with
+/// `AdtInto` will have a field or a variant of type String while the
+/// original type was `StringId`, the lookup will be done
+/// automatically.
+mod mirrored {
+    use super::{sinto::*, source};
+    use hax_adt_into::*;
+
+    #[derive(AdtInto)]
+    #[args(<>, from: source::Literal, state: source::State as s)]
+    pub enum Literal {
+        Integer(u32),
+        String(String),
+    }
+
+    impl SInto<source::State, String> for source::StringId {
+        fn sinto(&self, s: &source::State) -> String {
+            s.0.get(self).unwrap().clone()
+        }
+    }
+}
+
+/// Definition of the `sinto` trait used by the `AdtInto` macro
+pub mod sinto {
+    pub trait SInto<S, To> {
+        fn sinto(&self, s: &S) -> To;
+    }
+
+    /// Default implementation for type implementing Copy
+    impl<S, T: Copy> SInto<S, T> for T {
+        fn sinto(&self, _s: &S) -> T {
+            *self
+        }
+    }
+}
diff --git a/frontend/exporter/options/Cargo.toml b/frontend/exporter/options/Cargo.toml
index ce948398d..fadcbc905 100644
--- a/frontend/exporter/options/Cargo.toml
+++ b/frontend/exporter/options/Cargo.toml
@@ -7,7 +7,7 @@ homepage.workspace = true
 edition.workspace = true
 repository.workspace = true
 readme.workspace = true
-description = "hax frontend options"
+description = "The options the `hax-frontend-exporter` crate is sensible to."
 
 [dependencies]
 serde.workspace = true
diff --git a/hax-lib-protocol-macros/Cargo.toml b/hax-lib-protocol-macros/Cargo.toml
index 0cb376255..de9561465 100644
--- a/hax-lib-protocol-macros/Cargo.toml
+++ b/hax-lib-protocol-macros/Cargo.toml
@@ -8,8 +8,6 @@ edition.workspace = true
 repository.workspace = true
 readme.workspace = true
 
-# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
-
 [lib]
 proc-macro = true
 
diff --git a/hax-lib-protocol/Cargo.toml b/hax-lib-protocol/Cargo.toml
index 073e1fbba..0dee6ef9e 100644
--- a/hax-lib-protocol/Cargo.toml
+++ b/hax-lib-protocol/Cargo.toml
@@ -8,7 +8,5 @@ edition.workspace = true
 repository.workspace = true
 readme.workspace = true
 
-# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
-
 [dependencies]
 libcrux = "0.0.2-pre.2"