feat: support no_std consumers with embedded CI coverage

.github/workflows/ci.yml

@@ -63,3 +63,30 @@
 
       - name: Test
         run: just test-no-coverage
+
+  no_alloc:
+    name: Build / no-std, no-alloc
+    runs-on: ubuntu-latest
+
+    steps:
+      - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1
+
+      - name: Install Determinate Nix
+        uses: DeterminateSystems/determinate-nix-action@d96678350ffd6a456235832eb11e1c491589b7bb # v3.21.8
+        with:
+          extra-conf: lazy-trees = true
+
+      - name: Set up FlakeHub Cache
+        uses: DeterminateSystems/flakehub-cache-action@77c6bddd7d747943530aaa578c57f233ee5d920e # v3.21.8
+
+      - name: Install Rust (stable)
+        uses: actions-rust-lang/setup-rust-toolchain@166cdcfd11aee3cb47222f9ddb555ce30ddb9659 # v1.17.0
+        with:
+          toolchain: stable
+          target: thumbv6m-none-eabi
+
+      - name: Enter Nix devshell
+        uses: nicknovitski/nix-develop@9be7cfb4b10451d3390a75dc18ad0465bed4932a # v1.2.1
+
+      - name: Build (no-std, no-alloc)
+        run: just build-no-alloc

.gitignore

@@ -1,5 +1,6 @@
 # rust
 /target/
+/ensure-no-alloc/target/
 **/*.rs.bk
 
 # direnv

README.md

@@ -22,6 +22,14 @@ Annotate functions and methods with "contracts", using _invariants_, _pre-condit
 
 [dbc]: https://en.wikipedia.org/wiki/Design_by_contract
 
+## `no_std` support
+
+Contracts support `#![no_std]` consumers without an allocator. No feature flag is required. The procedural macro runs on the build host and uses `std` there; the generated checks do not. Contract expressions must also be compatible with `no_std`. Logging and MIRAI modes depend on the consumer's logging or MIRAI setup and are not covered by this guarantee.
+
+CI builds the `ensure-no-alloc` consumer for `thumbv6m-none-eabi`, with `just build-no-alloc`.
+
+## Example
+
 ```rust
 pub struct Library {
     available: HashSet<String>,

ensure-no-alloc/Cargo.toml

@@ -0,0 +1,7 @@
+[package]
+name = "ensure-no-alloc"
+publish = false
+edition = "2018"
+
+[dependencies]
+contracts = { path = ".." }

ensure-no-alloc/src/compat_test.rs

@@ -0,0 +1,46 @@
+use contracts::*;
+
+#[contract(
+    requires(value < u32::MAX, "Increment must not overflow"),
+    ensures(ret == value + 1),
+)]
+fn increment(value: u32) -> u32 {
+    value + 1
+}
+
+struct Counter(u32);
+
+#[invariant(self.0 < 100)]
+impl Counter {
+    #[debug_requires(self.0 < 99)]
+    #[debug_ensures(self.0 == old(self.0) + 1)]
+    fn increment(&mut self) {
+        self.0 = increment(self.0);
+    }
+}
+
+#[contract_trait]
+trait ReadCounter {
+    #[ensures(ret < 100)]
+    fn read(&self) -> u32;
+}
+
+#[contract_trait]
+impl ReadCounter for Counter {
+    fn read(&self) -> u32 {
+        self.0
+    }
+}
+
+#[test_requires(value < 100)]
+#[test_ensures(ret == value)]
+#[test_invariant(value < 100)]
+fn identity(value: u32) -> u32 {
+    value
+}
+
+pub fn exercise() {
+    let mut counter = Counter(0);
+    counter.increment();
+    assert_eq!(identity(counter.read()), 1);
+}

ensure-no-alloc/src/main.rs

@@ -0,0 +1,21 @@
+#![no_std]
+#![no_main]
+
+// Do not add a global allocator: the build must fail if generated contracts require one.
+mod compat_test;
+
+#[panic_handler]
+fn panic(_info: &core::panic::PanicInfo<'_>) -> ! {
+    loop {
+        core::hint::spin_loop();
+    }
+}
+
+#[no_mangle]
+pub extern "C" fn _start() -> ! {
+    compat_test::exercise();
+
+    loop {
+        core::hint::spin_loop();
+    }
+}

justfile

@@ -43,10 +43,16 @@ test-no-coverage:
     RUSTDOCFLAGS="-D warnings" cargo {{ toolchain }} doc --workspace --no-deps --all-features
 
 # Test workspace and generate coverage files
-test: test-no-coverage
+test: test-no-coverage build-no-alloc
     # @just test-coverage-codecov
     # @just test-coverage-lcov
 
+# Build a consumer without the standard library or an allocator.
+build-no-alloc:
+    cargo {{ toolchain }} build --target=thumbv6m-none-eabi --manifest-path=ensure-no-alloc/Cargo.toml
+    # Compile test-only contracts without the standard test harness.
+    cargo {{ toolchain }} rustc --target=thumbv6m-none-eabi --manifest-path=ensure-no-alloc/Cargo.toml -- --cfg test
+
 # Test workspace using MSRV
 test-msrv: downgrade-for-msrv test
 

src/lib.rs

@@ -17,6 +17,14 @@
 //! If the last argument to an attribute is a string constant it will be
 //! inserted into the assertion message.
 //!
+//! ## `no_std` support
+//!
+//! Contracts support `#![no_std]` consumers without an allocator. No feature flag is required.
+//! The procedural macro runs on the build host and uses `std` there; the generated checks do not.
+//! Contract expressions must also be compatible with `no_std`.
+//! Logging and MIRAI modes depend on the consumer's logging or MIRAI setup and are not covered
+//! by this guarantee.
+//!
 //! ## Example
 //!
 //! ```rust