From 98c219b2bc320dac79ad0c010dde6a382e382cb1 Mon Sep 17 00:00:00 2001
From: Rob Ede <robjtede@icloud.com>
Date: Thu, 10 Sep 2026 10:02:52 +0100
Subject: [PATCH 1/3] feat: support no_std consumers with embedded CI coverage

---
 .github/workflows/ci.yml         |  5 +++
 .gitignore                       |  1 +
 README.md                        |  8 +++++
 ensure-no-std/Cargo.lock         | 54 ++++++++++++++++++++++++++++++++
 ensure-no-std/Cargo.toml         |  7 +++++
 ensure-no-std/src/compat_test.rs | 46 +++++++++++++++++++++++++++
 ensure-no-std/src/main.rs        | 20 ++++++++++++
 justfile                         |  8 ++++-
 src/lib.rs                       |  8 +++++
 9 files changed, 156 insertions(+), 1 deletion(-)
 create mode 100644 ensure-no-std/Cargo.lock
 create mode 100644 ensure-no-std/Cargo.toml
 create mode 100644 ensure-no-std/src/compat_test.rs
 create mode 100644 ensure-no-std/src/main.rs

diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index 7cbccd2..301e23c 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -48,6 +48,7 @@ jobs:
         uses: actions-rust-lang/setup-rust-toolchain@166cdcfd11aee3cb47222f9ddb555ce30ddb9659 # v1.17.0
         with:
           toolchain: ${{ matrix.toolchain.version }}
+          target: thumbv6m-none-eabi
 
       - name: Install cargo-nextest
         uses: taiki-e/install-action@3d7d7cd5ac7f994c1892ae0c06165095b9139094 # v2.85.1
@@ -63,3 +64,7 @@ jobs:
 
       - name: Test
         run: just test-no-coverage
+
+      - name: Build (no-std)
+        if: matrix.toolchain.name == 'stable'
+        run: just build-no-std
diff --git a/.gitignore b/.gitignore
index e9b2ce0..f5396fd 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1,5 +1,6 @@
 # rust
 /target/
+/ensure-no-std/target/
 **/*.rs.bk
 
 # direnv
diff --git a/README.md b/README.md
index 5f5bbd1..8b6caae 100644
--- a/README.md
+++ b/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-std` consumer for `thumbv6m-none-eabi`, with `just build-no-std`.
+
+## Example
+
 ```rust
 pub struct Library {
     available: HashSet<String>,
diff --git a/ensure-no-std/Cargo.lock b/ensure-no-std/Cargo.lock
new file mode 100644
index 0000000..43159bf
--- /dev/null
+++ b/ensure-no-std/Cargo.lock
@@ -0,0 +1,54 @@
+# This file is automatically @generated by Cargo.
+# It is not intended for manual editing.
+version = 3
+
+[[package]]
+name = "contracts"
+version = "0.6.9"
+dependencies = [
+ "proc-macro2",
+ "quote",
+ "syn",
+]
+
+[[package]]
+name = "ensure-no-std"
+version = "0.0.0"
+dependencies = [
+ "contracts",
+]
+
+[[package]]
+name = "proc-macro2"
+version = "1.0.107"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "985e7ec9bb745e6ce6535b544d84d6cd6f7ad8bd711c398938ae983b91a766d9"
+dependencies = [
+ "unicode-ident",
+]
+
+[[package]]
+name = "quote"
+version = "1.0.47"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "1fbf4db142a473a8d80c26bbf18454ed458bf8d26c8219c331daecfdbd079001"
+dependencies = [
+ "proc-macro2",
+]
+
+[[package]]
+name = "syn"
+version = "3.0.5"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "12df2e0110f65b775f769bb17ef989067a1d931b2eb822bd4346631eeada89f9"
+dependencies = [
+ "proc-macro2",
+ "quote",
+ "unicode-ident",
+]
+
+[[package]]
+name = "unicode-ident"
+version = "1.0.24"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "e6e4313cd5fcd3dad5cafa179702e2b244f760991f45397d14d4ebf38247da75"
diff --git a/ensure-no-std/Cargo.toml b/ensure-no-std/Cargo.toml
new file mode 100644
index 0000000..860be40
--- /dev/null
+++ b/ensure-no-std/Cargo.toml
@@ -0,0 +1,7 @@
+[package]
+name = "ensure-no-std"
+publish = false
+edition = "2018"
+
+[dependencies]
+contracts = { path = ".." }
diff --git a/ensure-no-std/src/compat_test.rs b/ensure-no-std/src/compat_test.rs
new file mode 100644
index 0000000..9e1aa6d
--- /dev/null
+++ b/ensure-no-std/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);
+}
diff --git a/ensure-no-std/src/main.rs b/ensure-no-std/src/main.rs
new file mode 100644
index 0000000..42aba8c
--- /dev/null
+++ b/ensure-no-std/src/main.rs
@@ -0,0 +1,20 @@
+#![no_std]
+#![no_main]
+
+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();
+    }
+}
diff --git a/justfile b/justfile
index b6592ac..f30ed6c 100644
--- a/justfile
+++ b/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-std
     # @just test-coverage-codecov
     # @just test-coverage-lcov
 
+# Build a consumer without the standard library or an allocator.
+build-no-std:
+    cargo {{ toolchain }} build --target=thumbv6m-none-eabi --manifest-path=ensure-no-std/Cargo.toml
+    # Compile test-only contracts without the standard test harness.
+    cargo {{ toolchain }} rustc --target=thumbv6m-none-eabi --manifest-path=ensure-no-std/Cargo.toml -- --cfg test
+
 # Test workspace using MSRV
 test-msrv: downgrade-for-msrv test
 
diff --git a/src/lib.rs b/src/lib.rs
index c2622e3..879675d 100644
--- a/src/lib.rs
+++ b/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

From 025d0f665f2363d97ae813589b07021cc2a69ed8 Mon Sep 17 00:00:00 2001
From: Rob Ede <robjtede@icloud.com>
Date: Thu, 10 Sep 2026 10:05:27 +0100
Subject: [PATCH 2/3] test: make no-alloc consumer guarantee explicit

---
 .github/workflows/ci.yml                              | 4 ++--
 .gitignore                                            | 2 +-
 README.md                                             | 2 +-
 {ensure-no-std => ensure-no-alloc}/Cargo.lock         | 2 +-
 {ensure-no-std => ensure-no-alloc}/Cargo.toml         | 2 +-
 {ensure-no-std => ensure-no-alloc}/src/compat_test.rs | 0
 {ensure-no-std => ensure-no-alloc}/src/main.rs        | 1 +
 justfile                                              | 8 ++++----
 8 files changed, 11 insertions(+), 10 deletions(-)
 rename {ensure-no-std => ensure-no-alloc}/Cargo.lock (97%)
 rename {ensure-no-std => ensure-no-alloc}/Cargo.toml (77%)
 rename {ensure-no-std => ensure-no-alloc}/src/compat_test.rs (100%)
 rename {ensure-no-std => ensure-no-alloc}/src/main.rs (76%)

diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index 301e23c..6bd96ce 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -65,6 +65,6 @@ jobs:
       - name: Test
         run: just test-no-coverage
 
-      - name: Build (no-std)
+      - name: Build (no-std, no-alloc)
         if: matrix.toolchain.name == 'stable'
-        run: just build-no-std
+        run: just build-no-alloc
diff --git a/.gitignore b/.gitignore
index f5396fd..d2cf712 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1,6 +1,6 @@
 # rust
 /target/
-/ensure-no-std/target/
+/ensure-no-alloc/target/
 **/*.rs.bk
 
 # direnv
diff --git a/README.md b/README.md
index 8b6caae..16a6e66 100644
--- a/README.md
+++ b/README.md
@@ -26,7 +26,7 @@ Annotate functions and methods with "contracts", using _invariants_, _pre-condit
 
 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-std` consumer for `thumbv6m-none-eabi`, with `just build-no-std`.
+CI builds the `ensure-no-alloc` consumer for `thumbv6m-none-eabi`, with `just build-no-alloc`.
 
 ## Example
 
diff --git a/ensure-no-std/Cargo.lock b/ensure-no-alloc/Cargo.lock
similarity index 97%
rename from ensure-no-std/Cargo.lock
rename to ensure-no-alloc/Cargo.lock
index 43159bf..26428d3 100644
--- a/ensure-no-std/Cargo.lock
+++ b/ensure-no-alloc/Cargo.lock
@@ -12,7 +12,7 @@ dependencies = [
 ]
 
 [[package]]
-name = "ensure-no-std"
+name = "ensure-no-alloc"
 version = "0.0.0"
 dependencies = [
  "contracts",
diff --git a/ensure-no-std/Cargo.toml b/ensure-no-alloc/Cargo.toml
similarity index 77%
rename from ensure-no-std/Cargo.toml
rename to ensure-no-alloc/Cargo.toml
index 860be40..1773d2c 100644
--- a/ensure-no-std/Cargo.toml
+++ b/ensure-no-alloc/Cargo.toml
@@ -1,5 +1,5 @@
 [package]
-name = "ensure-no-std"
+name = "ensure-no-alloc"
 publish = false
 edition = "2018"
 
diff --git a/ensure-no-std/src/compat_test.rs b/ensure-no-alloc/src/compat_test.rs
similarity index 100%
rename from ensure-no-std/src/compat_test.rs
rename to ensure-no-alloc/src/compat_test.rs
diff --git a/ensure-no-std/src/main.rs b/ensure-no-alloc/src/main.rs
similarity index 76%
rename from ensure-no-std/src/main.rs
rename to ensure-no-alloc/src/main.rs
index 42aba8c..64faea0 100644
--- a/ensure-no-std/src/main.rs
+++ b/ensure-no-alloc/src/main.rs
@@ -1,6 +1,7 @@
 #![no_std]
 #![no_main]
 
+// Do not add a global allocator: the build must fail if generated contracts require one.
 mod compat_test;
 
 #[panic_handler]
diff --git a/justfile b/justfile
index f30ed6c..184097d 100644
--- a/justfile
+++ b/justfile
@@ -43,15 +43,15 @@ test-no-coverage:
     RUSTDOCFLAGS="-D warnings" cargo {{ toolchain }} doc --workspace --no-deps --all-features
 
 # Test workspace and generate coverage files
-test: test-no-coverage build-no-std
+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-std:
-    cargo {{ toolchain }} build --target=thumbv6m-none-eabi --manifest-path=ensure-no-std/Cargo.toml
+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-std/Cargo.toml -- --cfg test
+    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

From 2e3ee21e424dcb297ccc727bc27529f1889dbde7 Mon Sep 17 00:00:00 2001
From: Rob Ede <robjtede@icloud.com>
Date: Thu, 10 Sep 2026 10:40:59 +0100
Subject: [PATCH 3/3] ci: run no-alloc build in a separate job

---
 .github/workflows/ci.yml | 26 ++++++++++++++++++++++++--
 1 file changed, 24 insertions(+), 2 deletions(-)

diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index 6bd96ce..c8f2670 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -48,7 +48,6 @@ jobs:
         uses: actions-rust-lang/setup-rust-toolchain@166cdcfd11aee3cb47222f9ddb555ce30ddb9659 # v1.17.0
         with:
           toolchain: ${{ matrix.toolchain.version }}
-          target: thumbv6m-none-eabi
 
       - name: Install cargo-nextest
         uses: taiki-e/install-action@3d7d7cd5ac7f994c1892ae0c06165095b9139094 # v2.85.1
@@ -65,6 +64,29 @@ jobs:
       - 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)
-        if: matrix.toolchain.name == 'stable'
         run: just build-no-alloc