Merge pull request #983 from hacspec/dummy-lib

feat(hax-lib): intro. `hax` feature

.cargo/config.toml

@@ -0,0 +1,2 @@
+[build]
+rustflags = ["--cfg", "hax"]

.utils/jq_utils.jq

@@ -0,0 +1,27 @@
+# Removes a field from an object at any depth
+def remove_field(field):
+    walk(if type == "object" and has(field) then del(.[field]) else . end);
+
+# Remove `table_id` indirections whenever a value is found
+def thir_drop_table_id_nodes:
+    walk(if type == "object" and has("cache_id") and has("value") and .value then .value else . end);
+
+# Prints a THIR def_id as a string, useful for searching
+def thir_str_of_def_id_contents:
+  (
+      [.krate]
+    + [
+          .path.[]
+        | try (.disambiguator as $d | .data | . as $data | keys | .[0] | $data[.] + (if $d > 0 then "#" + $d else "" end))
+        | select(type == "string")]
+  ) | join("::");
+
+# Prints all THIR def_ids
+def thir_str_of_def_ids:
+     thir_drop_table_id_nodes | walk(
+          # if type == "object" and has("contents") and (.contents | type) == "object" and .contents | has("krate") and .contents | has("path") then
+          if try(. as $o | ($o.contents.krate | type == "string") and ($o.contents.path | type == "array")) catch false then
+            .contents | thir_str_of_def_id_contents
+          else
+            .
+          end);

Cargo.toml

@@ -6,8 +6,8 @@ members = [
      "cli/driver",
      "test-harness",
      "hax-lib",
-     "hax-lib-macros",
-     "hax-lib-macros/types",
+     "hax-lib/macros",
+     "hax-lib/macros/types",
      "hax-lib-protocol",
      "hax-lib-protocol-macros",
      "hax-bounded-integers",
@@ -23,8 +23,8 @@ default-members = [
      "cli/driver",
      "test-harness",
      "hax-lib",
-     "hax-lib-macros",
-     "hax-lib-macros/types",
+     "hax-lib/macros",
+     "hax-lib/macros/types",
      "hax-lib-protocol",
      "hax-lib-protocol-macros",
      "engine/names",
@@ -74,8 +74,8 @@ annotate-snippets = "0.11"
 hax-frontend-exporter = { path = "frontend/exporter", version = "=0.1.0-alpha.1", default-features = false }
 hax-adt-into = { path = "frontend/exporter/adt-into", version = "=0.1.0-alpha.1" }
 hax-frontend-exporter-options = { path = "frontend/exporter/options", version = "=0.1.0-alpha.1" }
-hax-lib-macros-types = { path = "hax-lib-macros/types", version = "=0.1.0-alpha.1" }
-hax-lib-macros = { path = "hax-lib-macros", version = "=0.1.0-alpha.1" }
+hax-lib-macros = { path = "hax-lib/macros", version = "=0.1.0-alpha.1" }
+hax-lib-macros-types = { path = "hax-lib/macros/types", version = "=0.1.0-alpha.1" }
 hax-lib = { path = "hax-lib", version = "=0.1.0-alpha.1" }
 hax-engine-names = { path = "engine/names", version = "=0.1.0-alpha.1" }
 hax-types = { path = "hax-types", version = "=0.1.0-alpha.1" }

book/src/tutorial/panic-freedom.md

@@ -86,7 +86,7 @@ anything might happen: the function might panic, might run forever,
 erase your disk, or anything.
 
 The helper crate
-[hax-lib-macros](https://github.com/hacspec/hax/tree/main/hax-lib-macros)
+[hax-lib](https://github.com/hacspec/hax/tree/main/hax-lib)
 provdes the `requires`
 [proc-macro](https://doc.rust-lang.org/reference/procedural-macros.html)
 which lets user writting pre-conditions directly in Rust.

engine/names/extract/build.rs

@@ -17,8 +17,8 @@ mod id_table {
 
     #[derive(Clone, PartialEq, Eq, PartialOrd, Ord, Serialize, Deserialize)]
     pub struct Node<T> {
-        value: Arc<T>,
-        id: u32,
+        pub value: Arc<T>,
+        pub id: u32,
     }
 
     impl<T> std::ops::Deref for Node<T> {
@@ -84,6 +84,7 @@ fn def_id_to_str(def_id: &DefId) -> (Value, String) {
     } else {
         &def_id.krate
     };
+
     // Update the crate name in the json output as well.
     let mut json = serde_json::to_value(def_id).unwrap();
     json["contents"]["value"]["krate"] = Value::String(crate_name.to_owned());
@@ -97,6 +98,15 @@ fn def_id_to_str(def_id: &DefId) -> (Value, String) {
     (json, path)
 }
 
+/// Checks whether a def id refers to a macro or not.
+/// We don't want to extract macro names.
+fn is_macro(did: &DefId) -> bool {
+    let Some(last) = did.contents.value.path.last() else {
+        return false;
+    };
+    matches!(last.data, DefPathItem::MacroNs { .. })
+}
+
 fn reader_to_str(s: String) -> String {
     let json: Value = match serde_json::from_str(&s) {
         Ok(v) => v,
@@ -107,6 +117,7 @@ fn reader_to_str(s: String) -> String {
 
     let def_ids = def_ids
         .into_iter()
+        .filter(|did| !is_macro(did))
         .map(|did| {
             let (json, krate_name) = def_id_to_str(&did);
             (serde_json::to_string(&json).unwrap(), krate_name)

examples/Cargo.toml

@@ -10,7 +10,6 @@ members = [
 resolver = "2"
 
 [workspace.dependencies]
-hax-lib-macros = { path = "../hax-lib-macros" }
 hax-lib = { path = "../hax-lib" }
 hax-bounded-integers = { path = "../hax-bounded-integers" }
 

examples/kyber_compress/Cargo.toml

@@ -6,5 +6,4 @@ edition = "2021"
 # See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
 
 [dependencies]
-hax-lib-macros.workspace = true
 hax-lib.workspace = true

examples/sha256/Cargo.toml

@@ -8,4 +8,4 @@ edition = "2021"
 path = "src/sha256.rs"
 
 [dependencies]
-hax-lib-macros.workspace = true
+hax-lib.workspace = true

examples/sha256/src/sha256.rs

@@ -1,4 +1,3 @@
-use hax_lib_macros as hax;
 use std::convert::TryInto;
 
 const BLOCK_SIZE: usize = 64;
@@ -50,7 +49,7 @@ const HASH_INIT: Hash = [
     0x5be0cd19u32,
 ];
 
-#[hax::requires(i < 4)]
+#[hax_lib::requires(i < 4)]
 pub fn sigma(x: u32, i: usize, op: usize) -> u32 {
     let mut tmp: u32 = x.rotate_right(OP_TABLE[3 * i + 2].into());
     if op == 0 {