Merge pull request #656 from hacspec/franziskus/hax-lib-release1

prepare hax-lib for publishing

PUBLISHING.md

@@ -8,20 +8,29 @@ Here is the list of the crates in this repository (excluding `tests`
 and `examples`):
 
 - `hax-test-harness` **(doesn't need to be published)**
+
+## cargo-hax
+
 1. `hax-frontend-exporter-options` (`frontend/exporter/options `)
 2. `hax-adt-into` (`frontend/exporter/adt-into`)
 3. `hax-frontend-exporter` (`frontend/exporter`)
 4. `hax-cli-options` (`cli/options`)
 5. `hax-diagnostics` (`frontend/diagnostics`)
 6. `hax-cli-options-engine` (`cli/options/engine`)
 7. `hax-subcommands` (binaries) (`cli/subcommands`)
-    - `cargo-hax`
-    - `hax-export-json-schemas`
-    - `hax-pretty-print-diagnostics`
-- `hax-lib-macros`
-- `hax-lint`
+   - `cargo-hax`
+   - `hax-export-json-schemas`
+   - `hax-pretty-print-diagnostics`
+
 - `hax-phase-debug-webapp`
 - `hax-driver`
 
+## hax-lib
+
+1. `hax-lib-macros-types`
+2. `hax-lib-macros`
+3. `hax-lib`
 
+---
 
+- `hax-lint`

hax-lib-macros/Cargo.toml

@@ -6,7 +6,8 @@ license.workspace = true
 homepage.workspace = true
 edition.workspace = true
 repository.workspace = true
-readme.workspace = true
+readme = "README.md"
+description = "Hax-specific proc-macros for Rust programs"
 
 [lib]
 proc-macro = true
@@ -15,8 +16,13 @@ proc-macro = true
 proc-macro-error = "1.0.4"
 proc-macro2.workspace = true
 quote.workspace = true
+syn = { version = "2.0", features = [
+    "full",
+    "visit-mut",
+    "extra-traits",
+    "parsing",
+] }
 hax-lib-macros-types.workspace = true
-syn = { version = "2.0", features = ["full", "visit-mut", "extra-traits", "parsing"] }
 
 [dev-dependencies]
 hax-lib = { path = "../hax-lib" }

hax-lib-macros/README.md

@@ -0,0 +1,8 @@
+# hax proc macros
+
+Hax-specific proc-macros for Rust programs.
+
+This crate defines proc macros to be used in Rust programs that are extracted with
+hax.
+It provides proc macros such as `requires` and `ensures` to define pre- and post-conditions
+for functions.

hax-lib-macros/types/Cargo.toml

@@ -6,7 +6,8 @@ license.workspace = true
 homepage.workspace = true
 edition.workspace = true
 repository.workspace = true
-readme.workspace = true
+readme = "README.md"
+description = "Hax-internal types"
 
 [dependencies]
 serde.workspace = true
@@ -16,5 +17,3 @@ quote.workspace = true
 proc-macro2.workspace = true
 uuid = { version = "1.5", features = ["v4"] }
 
-[features]
-schemars = ["dep:schemars"]

hax-lib-macros/types/README.md

@@ -0,0 +1,3 @@
+# hax internal types
+
+A crate that defines the types of the various payloads of the attributes produced by the crate `hax-lib-macros` and consumed internally by the engine of hax.

hax-lib/Cargo.toml

@@ -9,8 +9,6 @@ repository.workspace = true
 readme = "README.md"
 description = "Hax-specific helpers for Rust programs"
 
-# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
-
 [dependencies]
 hax-lib-macros = { workspace = true, optional = true }
 num-bigint = { version = "0.4.3", default-features = false }

hax-lib/README.md

@@ -0,0 +1,17 @@
+# hax library
+
+This crate contains helpers that can be used when writing Rust code that is proven
+through the hax toolchain.
+
+**⚠️ The code in this crate has no effect when compiled without the `--cfg hax`.**
+
+## Examples:
+
+```rust
+fn sum(x: Vec<u32>, y: Vec<u32>) -> Vec<u32> {
+  hax_lib::assume!(x.len() == y.len());
+  hax_lib::assert!(hax_lib::forall(|i: usize| hax_lib::implies(i < x.len(), || x[i] < 4242)));
+  hax_lib::debug_assert!(hax_lib::exists(|i: usize| hax_lib::implies(i < x.len(), || x[i] > 123)));
+  x.into_iter().zip(y.into_iter()).map(|(x, y)| x + y).collect()
+}
+```