ci: nightly property tests with more cases (#1498)

Thanks @Ian-cmd-ops.

.config/nextest.toml

@@ -16,6 +16,8 @@ not (
         | test(=cmd::plastic::tests::enclosure_snap_fit_follows_resized_front_wall)
     ))
     | (package(solidcraft-kernel) & test(=tests::boolean_identity_on_tangent_primitives))
+    | (package(solidcraft-kernel) & binary(boolean_props))
+    | (package(solidcraft-engine) & binary(atomic_commands))
     | (package(solidcraft-ui-egui) & binary(scenarios) & test(=acceptance_sensor_enclosure))
 )
 """

.github/workflows/ci.yml

@@ -317,6 +317,32 @@ jobs:
           cargo nextest run --archive-file tests.tar.zst --workspace-remap . --extract-to . --extract-overwrite \
             --profile ci --success-output final --run-ignored only -E "binary(action_matrix) & test(=action_matrix_determinism)"
 
+  property-tests:
+    # The boolean property tests and the atomic command tests with many cases. Pull requests skip
+    # them (.config/nextest.toml); pushes to main run them with small defaults (8 cases, seeds 0..4).
+    name: Property tests (many cases)
+    needs: build-tests
+    if: github.event_name == 'schedule' || github.event_name == 'workflow_dispatch'
+    runs-on: ubuntu-24.04
+    timeout-minutes: 60
+    steps:
+      - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1
+      - uses: taiki-e/install-action@1168f6810a3cb30a3514bf5756a3b7f0422c6df8 # v2.87.28
+        with:
+          tool: cargo-nextest
+      - uses: actions/download-artifact@9000827ccba6bdab643e8b6fd33ac0654aef8333 # v8.0.2
+        with:
+          name: nextest-archive
+      - name: Boolean properties and atomic commands
+        # The defaults (8 cases, seeds 0..4) take 159 s and 802 s on a 2-core VM; four times the
+        # cases and twice the seeds are estimated at about 40 minutes there (not yet timed on CI).
+        env:
+          PROPTEST_CASES: "32"
+          ATOMIC_SEEDS: "0..8"
+        run: |
+          cargo nextest run --archive-file tests.tar.zst --workspace-remap . --extract-to . --extract-overwrite \
+            --profile ci --ignore-default-filter --success-output final -E "binary(boolean_props) | binary(atomic_commands)"
+
   doc-tests:
     name: Doc tests
     needs: changes

CONTRIBUTING.md

@@ -180,8 +180,8 @@ Pull requests skip a few heavy tests (one to four minutes each), which run on ev
   `tests::robustness_goldens` (pull requests that touch `crates/kernel` run its `sample_*` part),
   `pattern_suppress_tests::enclosure_arc_extinction_keeps_a_real_sharp_inner_lip_after_resize_and_reopen`,
   `pattern_suppress_tests::enclosure_datums_follow_wall_height_and_board_depth_with_material_proofs`,
-  `cmd::plastic::tests::enclosure_snap_fit_follows_resized_front_wall`
+  `cmd::plastic::tests::enclosure_snap_fit_follows_resized_front_wall`, the `atomic_commands` contract tests
-- `solidcraft-kernel`: `tests::boolean_identity_on_tangent_primitives`
+- `solidcraft-kernel`: `tests::boolean_identity_on_tangent_primitives`, the `boolean_props` property tests
 - `solidcraft-ui-egui` scenarios: `acceptance_sensor_enclosure`
 
 **The action matrix** tries every ordinary action on every face, edge, vertex and body of a

Cargo.lock

@@ -805,6 +805,17 @@ dependencies = [
  "serde",
 ]
 
+[[package]]
+name = "chacha20"
+version = "0.10.2"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "65c35e4b699c7e15ccbe7ee35c005e4fc0a278d22238a2857e6ce2dadeda1b06"
+dependencies = [
+ "cfg-if",
+ "cpufeatures 0.3.1",
+ "rand_core 0.10.1",
+]
+
 [[package]]
 name = "chrono"
 version = "0.4.45"
@@ -1665,6 +1676,7 @@ dependencies = [
  "cfg-if",
  "libc",
  "r-efi 6.0.0",
+ "rand_core 0.10.1",
 ]
 
 [[package]]
@@ -3260,6 +3272,22 @@ version = "1.0.18"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "3d595e54a326bc53c1c197b32d295e14b169e3cfeaa8dc82b529f947fba6bcf5"
 
+[[package]]
+name = "proptest"
+version = "1.12.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "b8530004ccb15eae51c7e40009fbe317f341f804db54dc033eec1c50be28cfa0"
+dependencies = [
+ "bitflags 2.13.2",
+ "chacha20",
+ "core_detect",
+ "num-traits",
+ "rand 0.10.3",
+ "rand_xorshift",
+ "regex-syntax",
+ "unarray",
+]
+
 [[package]]
 name = "pxfm"
 version = "0.1.30"
@@ -3310,7 +3338,17 @@ checksum = "e058c7de0b26af77780c769414d6257830bb240f3c38477dbc2c16e5f54d6d4c"
 dependencies = [
  "libc",
  "rand_chacha",
- "rand_core",
+ "rand_core 0.6.4",
+]
+
+[[package]]
+name = "rand"
+version = "0.10.3"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "65c9fb96cbc91e3478eaae79a69fcd3f1ae4ad052e471fe6732fff548984b4af"
+dependencies = [
+ "getrandom 0.4.3",
+ "rand_core 0.10.1",
 ]
 
 [[package]]
@@ -3320,7 +3358,7 @@ source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "e6c10a63a0fa32252be49d21e7709d4d4baf8d231c2dbce1eaa8141b9b127d88"
 dependencies = [
  "ppv-lite86",
- "rand_core",
+ "rand_core 0.6.4",
 ]
 
 [[package]]
@@ -3332,6 +3370,21 @@ dependencies = [
  "getrandom 0.2.17",
 ]
 
+[[package]]
+name = "rand_core"
+version = "0.10.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "63b8176103e19a2643978565ca18b50549f6101881c443590420e4dc998a3c69"
+
+[[package]]
+name = "rand_xorshift"
+version = "0.5.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "60aa6af80be32871323012e02e6e65f8a7cc7890931ae421d217ad8fe0df2ccf"
+dependencies = [
+ "rand_core 0.10.1",
+]
+
 [[package]]
 name = "range-alloc"
 version = "0.1.5"
@@ -3423,6 +3476,12 @@ dependencies = [
  "bitflags 2.13.2",
 ]
 
+[[package]]
+name = "regex-syntax"
+version = "0.8.11"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "d6f6ff9a378485b298a5286656da665ba74413d36db0979633275d2e708145d4"
+
 [[package]]
 name = "renderdoc-sys"
 version = "1.1.0"
@@ -3669,7 +3728,7 @@ dependencies = [
  "hkdf",
  "num",
  "once_cell",
- "rand",
+ "rand 0.8.8",
  "serde",
  "sha2 0.10.9",
  "zbus 4.4.0",
@@ -4122,6 +4181,7 @@ name = "solidcraft-kernel"
 version = "0.13.1"
 dependencies = [
  "log",
+ "proptest",
  "rayon",
  "serde",
  "serde_json",
@@ -4508,7 +4568,7 @@ source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "97a31fe98d5a0589ad20576260e214af23dea21a8d125da81ad3bbcb666f411f"
 dependencies = [
  "getrandom 0.2.17",
- "rand",
+ "rand 0.8.8",
  "thiserror 1.0.69",
  "truck-base",
  "truck-derivers",
@@ -4649,6 +4709,12 @@ dependencies = [
  "windows-sys 0.61.2",
 ]
 
+[[package]]
+name = "unarray"
+version = "0.1.4"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "eaea85b334db583fe3274d12b4cd1880032beab409c0d774be044d4480ab9a94"
+
 [[package]]
 name = "unicode-general-category"
 version = "1.1.0"
@@ -5739,7 +5805,7 @@ dependencies = [
  "hex",
  "nix",
  "ordered-stream",
- "rand",
+ "rand 0.8.8",
  "serde",
  "serde_repr",
  "sha1 0.10.7",

crates/engine/tests/atomic_commands.rs

@@ -0,0 +1,102 @@
+//! Atomic command tests: the engine's transaction contract, checked on random designs.
+//!
+//! The contract (crates/engine/src/lib.rs, `Session::execute`):
+//! 1. A command that returns an error leaves the design exactly as it was.
+//! 2. Undo back to the start gives the empty design. Redo back to the end gives the final design.
+//! 3. The same commands give the same design every time (no hidden state between runs).
+//!
+//! The designs come from the engine's own fuzzer (`fuzz::run`), so these tests cover every
+//! command it can generate: sketches, extrudes, revolves, holes, patterns, fillets, shells.
+//!
+//! Seeds: `ATOMIC_SEEDS` (default 0..4). Pull requests skip this file (.config/nextest.toml); pushes
+//! to main run it, and the nightly `property-tests` job uses more seeds. A long local run:
+//! `ATOMIC_SEEDS=0..100`.
+
+use solidcraft_doc::Document;
+use solidcraft_engine::{Session, fuzz};
+
+fn seeds() -> std::ops::Range<u64> {
+    let s = std::env::var("ATOMIC_SEEDS").unwrap_or_else(|_| "0..4".into());
+    let (a, b) = s.split_once("..").expect("ATOMIC_SEEDS looks like 0..4");
+    a.parse().unwrap()..b.parse().unwrap()
+}
+
+/// The commands a seed's design runs, flattened.
+fn commands(seed: u64) -> Vec<(String, serde_json::Value)> {
+    fuzz::run(seed, 8).steps.into_iter().flat_map(|s| s.commands).collect()
+}
+
+/// Run the commands. For each failed command, check the design did not change.
+/// Returns the session and a list of contract breaks.
+fn replay(seed: u64, cmds: &[(String, serde_json::Value)]) -> (Session, Vec<String>) {
+    let mut s = Session::default();
+    let mut broken = Vec::new();
+    for (i, (id, p)) in cmds.iter().enumerate() {
+        let before: Document = (*s.doc).clone();
+        if let Err(e) = s.execute(id, p)
+            && *s.doc != before
+        {
+            broken.push(format!("seed {seed} cmd {i} `{id}` failed ({e}) but changed the design"));
+        }
+    }
+    (s, broken)
+}
+
+#[test]
+fn failed_commands_leave_the_design_unchanged() {
+    let mut broken = Vec::new();
+    for seed in seeds() {
+        broken.extend(replay(seed, &commands(seed)).1);
+    }
+    assert!(broken.is_empty(), "{} contract breaks:\n{}", broken.len(), broken.join("\n"));
+}
+
+#[test]
+fn undo_all_then_redo_all_round_trips() {
+    let empty = (*Session::default().doc).clone();
+    let mut broken = Vec::new();
+    for seed in seeds() {
+        let (mut s, _) = replay(seed, &commands(seed));
+        let end: Document = (*s.doc).clone();
+        let mut n = 0;
+        while s.execute("edit.undo", &serde_json::Value::Null).is_ok() {
+            n += 1;
+            assert!(n < 10_000, "seed {seed}: undo never runs out");
+        }
+        if *s.doc != empty {
+            broken.push(format!("seed {seed}: after {n} undos the design is not the empty design"));
+        }
+        for _ in 0..n {
+            if let Err(e) = s.execute("edit.redo", &serde_json::Value::Null) {
+                broken.push(format!("seed {seed}: redo failed: {e}"));
+                break;
+            }
+        }
+        if *s.doc != end {
+            broken.push(format!("seed {seed}: after {n} redos the design is not the design before undo"));
+        }
+    }
+    assert!(broken.is_empty(), "{} contract breaks:\n{}", broken.len(), broken.join("\n"));
+}
+
+#[test]
+fn same_commands_same_design() {
+    let mut broken = Vec::new();
+    for seed in seeds() {
+        let cmds = commands(seed);
+        let (a, _) = replay(seed, &cmds);
+        let (b, _) = replay(seed, &cmds);
+        if *a.doc != *b.doc {
+            broken.push(format!("seed {seed}: two runs of the same commands gave different designs"));
+        }
+        let (va, vb) = (volume(&a), volume(&b));
+        if va.to_bits() != vb.to_bits() {
+            broken.push(format!("seed {seed}: two runs gave volumes {va} and {vb}"));
+        }
+    }
+    assert!(broken.is_empty(), "{} contract breaks:\n{}", broken.len(), broken.join("\n"));
+}
+
+fn volume(s: &Session) -> f64 {
+    s.model.state().bodies.iter().filter_map(|b| solidcraft_kernel::measure(&b.body).ok()).map(|m| m.volume).sum()
+}

crates/kernel/Cargo.toml

@@ -23,3 +23,6 @@ spade = { workspace = true }
 
 [target.'cfg(not(target_arch = "wasm32"))'.dependencies]
 rayon = { workspace = true }
+
+[dev-dependencies]
+proptest = { version = "1", default-features = false, features = ["std"] }

crates/kernel/tests/boolean_props.proptest-regressions

@@ -0,0 +1,7 @@
+# Seeds for failure cases proptest has generated in the past. It is
+# automatically read and these particular cases re-run before any
+# novel cases are generated.
+#
+# It is recommended to check this file in to source control so that
+# everyone who runs the test benefits from these saved cases.
+cc 739d5cbd9e471e0ff65bc2b7c1b9a323c2e769939c73def2e74fb17b0536c1d0 # shrinks to a = [0.0, 2.5, 30.0], sa = [22.5, 5.0, 5.0], b = [22.5, 7.5, 15.0], sb = [5.0, 5.0, 17.5]

crates/kernel/tests/boolean_props.rs

@@ -0,0 +1,220 @@
+//! Property tests for the kernel boolean (`boolean`, `measure`, `transform`).
+//!
+//! Each test states one invariant that every correct B-rep boolean holds. proptest picks the
+//! inputs, and when a case fails it shrinks the inputs to a small case that still fails. Paste
+//! that case into a normal `#[test]` as a regression test.
+//!
+//! Case count: `PROPTEST_CASES` (default 8). Pull requests skip this file (.config/nextest.toml);
+//! pushes to main run it, and the nightly `property-tests` job uses more cases. A long local run:
+//! `PROPTEST_CASES=2000 cargo test -p solidcraft-kernel --test boolean_props`.
+//! proptest saves every failing seed in `tests/boolean_props.proptest-regressions`. Commit it.
+
+use proptest::prelude::*;
+use solidcraft_geom::Vec3;
+use solidcraft_kernel::{Body, BoolOp, boolean, box_solid, cylinder, measure, sphere, transform};
+
+/// Relative volume tolerance. The same 0.2 % that `fuzz::boolean_case` uses.
+const REL: f64 = 2e-3;
+
+#[derive(Clone, Debug)]
+enum Prim {
+    Box { at: [f64; 3], size: [f64; 3] },
+    Cyl { at: [f64; 3], axis: usize, r: f64, h: f64 },
+    Sph { at: [f64; 3], r: f64 },
+}
+
+impl Prim {
+    fn body(&self) -> Body {
+        let v = |p: [f64; 3]| Vec3::new(p[0], p[1], p[2]);
+        let axes = [Vec3::X, Vec3::Y, Vec3::Z];
+        match *self {
+            Prim::Box { at, size } => box_solid(v(at), v([at[0] + size[0], at[1] + size[1], at[2] + size[2]])),
+            Prim::Cyl { at, axis, r, h } => cylinder(v(at), axes[axis], r, h),
+            Prim::Sph { at, r } => sphere(v(at), r),
+        }
+        .expect("a primitive with positive size must build")
+    }
+}
+
+/// Coordinates on a 2.5 mm grid: coincident faces, shared edges and tangencies come up often.
+/// These are the cases that break B-rep booleans.
+fn grid() -> impl Strategy<Value = f64> + Clone {
+    (0u32..=12).prop_map(|i| i as f64 * 2.5)
+}
+/// Size on the grid, never zero.
+fn grid_size() -> impl Strategy<Value = f64> + Clone {
+    (2u32..=12).prop_map(|i| i as f64 * 2.5)
+}
+/// Generic coordinates: almost never coincident. A failure here is a plain bug, not an edge case.
+fn free() -> impl Strategy<Value = f64> + Clone {
+    0.0f64..30.0
+}
+fn free_size() -> impl Strategy<Value = f64> + Clone {
+    3.0f64..30.0
+}
+
+fn prim(c: impl Strategy<Value = f64> + Clone, s: impl Strategy<Value = f64> + Clone) -> impl Strategy<Value = Prim> {
+    let p = [c.clone(), c.clone(), c];
+    prop_oneof![
+        5 => (p.clone(), [s.clone(), s.clone(), s.clone()]).prop_map(|(at, size)| Prim::Box { at, size }),
+        3 => (p.clone(), 0usize..3, s.clone(), s.clone()).prop_map(|(at, axis, r, h)| Prim::Cyl { at, axis, r: r / 2.0, h }),
+        2 => (p, s).prop_map(|(at, r)| Prim::Sph { at, r: r / 2.0 }),
+    ]
+}
+fn grid_prim() -> impl Strategy<Value = Prim> {
+    prim(grid(), grid_size())
+}
+fn free_prim() -> impl Strategy<Value = Prim> {
+    prim(free(), free_size())
+}
+
+/// Volume of a boolean result (an empty result has volume 0). Also fails the case when the
+/// result is not a sound solid.
+fn run(a: &Body, b: &Body, op: BoolOp) -> Result<f64, TestCaseError> {
+    let r = boolean(a, b, op).map_err(|e| TestCaseError::fail(format!("{op:?} returned an error: {e}")))?;
+    match r {
+        None => Ok(0.0),
+        Some(body) => {
+            let bad = body.validity();
+            prop_assert!(bad.is_empty(), "{op:?} result is not a sound solid: {}", bad.join("; "));
+            Ok(measure(&body).map_err(|e| TestCaseError::fail(format!("measure: {e}")))?.volume)
+        }
+    }
+}
+fn vol(b: &Body) -> f64 {
+    measure(b).expect("measure a primitive").volume
+}
+fn close(x: f64, y: f64, scale: f64) -> bool {
+    (x - y).abs() <= REL * scale.max(1e-9)
+}
+
+/// Inclusion-exclusion: V(A∪B) + V(A∩B) = V(A) + V(B), and V(A−B) = V(A) − V(A∩B).
+fn identity(a: &Prim, b: &Prim) -> Result<(), TestCaseError> {
+    let (ba, bb) = (a.body(), b.body());
+    let (va, vb) = (vol(&ba), vol(&bb));
+    let (vu, vi, vc) = (run(&ba, &bb, BoolOp::Union)?, run(&ba, &bb, BoolOp::Intersect)?, run(&ba, &bb, BoolOp::Cut)?);
+    prop_assert!(close(vu + vi, va + vb, va + vb), "union+intersect {} != A+B {} (A {va:.3}, B {vb:.3}, U {vu:.3}, I {vi:.3})", vu + vi, va + vb);
+    prop_assert!(close(vc, va - vi, va + vb), "cut {vc:.3} != A-I {:.3}", va - vi);
+    Ok(())
+}
+
+fn cfg(default: u32) -> ProptestConfig {
+    // The env var overrides the default; proptest reads PROPTEST_CASES itself only when the
+    // config does not set `cases`, so read it here.
+    let cases = std::env::var("PROPTEST_CASES").ok().and_then(|s| s.parse().ok()).unwrap_or(default);
+    ProptestConfig { cases, max_shrink_iters: 200, ..ProptestConfig::default() }
+}
+
+proptest! {
+    #![proptest_config(cfg(8))]
+
+    /// Generic placement: these must all pass. A failure is a real bug.
+    #[test]
+    fn identity_generic(a in free_prim(), b in free_prim()) {
+        identity(&a, &b)?;
+    }
+
+    /// Grid placement: coincident and tangent faces. The hard cases.
+    #[test]
+    fn identity_on_grid(a in grid_prim(), b in grid_prim()) {
+        identity(&a, &b)?;
+    }
+
+    /// Union and intersection do not depend on operand order.
+    #[test]
+    fn commutative(a in grid_prim(), b in grid_prim()) {
+        let (ba, bb) = (a.body(), b.body());
+        let s = vol(&ba) + vol(&bb);
+        for op in [BoolOp::Union, BoolOp::Intersect] {
+            let (ab, ba_) = (run(&ba, &bb, op)?, run(&bb, &ba, op)?);
+            prop_assert!(close(ab, ba_, s), "{op:?}: A,B gives {ab:.4} but B,A gives {ba_:.4}");
+        }
+    }
+
+    /// Moving both operands together does not change the answer. A large offset exposes
+    /// absolute tolerances (1e-6, 1e-9 literals) that should scale with the model.
+    #[test]
+    fn translation_invariant(a in grid_prim(), b in grid_prim(), off in prop::sample::select(vec![0.0, 1.0e3, 1.0e5])) {
+        let (ba, bb) = (a.body(), b.body());
+        let t = Vec3::new(off, -off * 0.7, off * 0.3);
+        let mv = |x: &Body| transform(x, t, Vec3::ZERO, Vec3::Z, 0.0).expect("translate");
+        let (ta, tb) = (mv(&ba), mv(&bb));
+        let s = vol(&ba) + vol(&bb);
+        for op in [BoolOp::Union, BoolOp::Intersect, BoolOp::Cut] {
+            let (here, there) = (run(&ba, &bb, op)?, run(&ta, &tb, op)?);
+            prop_assert!(close(here, there, s), "{op:?} at origin {here:.4}, moved by {off} gives {there:.4}");
+        }
+    }
+
+    /// Scaling the whole problem scales volume by k³. Small parts (0.05x) and large parts
+    /// (40x) expose tolerances that do not scale.
+    #[test]
+    fn scale_invariant(a in grid_prim(), b in grid_prim(), k in prop::sample::select(vec![0.05, 1.0, 40.0])) {
+        let sc = |p: &Prim| match p.clone() {
+            Prim::Box { at, size } => Prim::Box { at: at.map(|x| x * k), size: size.map(|x| x * k) },
+            Prim::Cyl { at, axis, r, h } => Prim::Cyl { at: at.map(|x| x * k), axis, r: r * k, h: h * k },
+            Prim::Sph { at, r } => Prim::Sph { at: at.map(|x| x * k), r: r * k },
+        };
+        let (ba, bb, ka, kb) = (a.body(), b.body(), sc(&a).body(), sc(&b).body());
+        let s = vol(&ba) + vol(&bb);
+        for op in [BoolOp::Union, BoolOp::Intersect, BoolOp::Cut] {
+            let (one, big) = (run(&ba, &bb, op)?, run(&ka, &kb, op)? / (k * k * k));
+            prop_assert!(close(one, big, s), "{op:?} at scale 1 gives {one:.4}, at scale {k} gives {big:.4} (normalised)");
+        }
+    }
+
+    /// A∪A = A, A∩A = A, A−A = nothing.
+    #[test]
+    fn self_operations(a in grid_prim()) {
+        let ba = a.body();
+        let va = vol(&ba);
+        prop_assert!(close(run(&ba, &ba, BoolOp::Union)?, va, va), "A∪A != A");
+        prop_assert!(close(run(&ba, &ba, BoolOp::Intersect)?, va, va), "A∩A != A");
+        prop_assert!(run(&ba, &ba, BoolOp::Cut)? <= REL * va, "A−A is not empty");
+    }
+
+    /// The same inputs give the same output, twice in a row. The boolean keeps thread-local
+    /// state (the nudge guard); this catches state that leaks from one call to the next.
+    #[test]
+    fn deterministic(a in grid_prim(), b in grid_prim()) {
+        let (ba, bb) = (a.body(), b.body());
+        for op in [BoolOp::Union, BoolOp::Intersect, BoolOp::Cut] {
+            let m = |r: Option<Body>| r.map(|x| { let m = measure(&x).unwrap(); (m.volume.to_bits(), m.faces, m.edges) });
+            let first = boolean(&ba, &bb, op).ok().map(m);
+            let second = boolean(&ba, &bb, op).ok().map(m);
+            prop_assert_eq!(first, second, "{:?} gave two different answers for the same input", op);
+        }
+    }
+
+    /// Two boxes whose overlap is known exactly (closed form, no tessellation guesswork).
+    #[test]
+    fn box_box_exact(a in [grid(), grid(), grid()], sa in [grid_size(), grid_size(), grid_size()],
+                     b in [grid(), grid(), grid()], sb in [grid_size(), grid_size(), grid_size()]) {
+        let overlap: f64 = (0..3).map(|i| ((a[i] + sa[i]).min(b[i] + sb[i]) - a[i].max(b[i])).max(0.0)).product();
+        let (pa, pb) = (Prim::Box { at: a, size: sa }, Prim::Box { at: b, size: sb });
+        let (ba, bb) = (pa.body(), pb.body());
+        let (va, vb) = (sa.iter().product::<f64>(), sb.iter().product::<f64>());
+        let s = va + vb;
+        // Per axis: the gap between the boxes (<0 overlap, 0 touch, >0 apart).
+        let gap: Vec<f64> = (0..3).map(|i| a[i].max(b[i]) - (a[i] + sa[i]).min(b[i] + sb[i])).collect();
+        // Touching along an edge or at a corner only: a union there is not a manifold solid.
+        // The kernel refuses it on purpose ("zero-thickness edge contact"). Allowed, as an error.
+        let edge_only = gap.iter().all(|g| *g <= 0.0) && gap.iter().filter(|g| **g == 0.0).count() >= 2;
+        prop_assert!(close(run(&ba, &bb, BoolOp::Intersect)?, overlap, s), "intersect != closed-form overlap {overlap}");
+        prop_assert!(close(run(&ba, &bb, BoolOp::Cut)?, va - overlap, s), "cut != closed form {}", va - overlap);
+        match run(&ba, &bb, BoolOp::Union) {
+            Err(_) if edge_only => {}
+            r => prop_assert!(close(r?, s - overlap, s), "union != closed form {}", s - overlap),
+        }
+    }
+
+    /// Two boxes that share part of a face must fuse into one solid. This is the most common
+    /// join in real parts (a boss on a plate).
+    #[test]
+    fn face_touching_boxes_fuse(x in grid(), y in grid(), w in grid_size(), d in grid_size(), h in grid_size()) {
+        let plate = Prim::Box { at: [0.0, 0.0, 0.0], size: [30.0, 30.0, 5.0] }.body();
+        let boss = Prim::Box { at: [x.min(27.5), y.min(27.5), 5.0], size: [w, d, h] }.body();
+        let (vp, vb) = (vol(&plate), vol(&boss));
+        prop_assert!(close(run(&plate, &boss, BoolOp::Union)?, vp + vb, vp + vb), "plate + boss lost or gained volume");
+    }
+}

docs/book/src/dev/testing.md

@@ -80,8 +80,8 @@ Pull requests skip a few heavy tests (each takes one to four minutes); they run
   `tests::robustness_goldens` (pull requests that touch `crates/kernel` run its `sample_*` part),
   `pattern_suppress_tests::enclosure_arc_extinction_keeps_a_real_sharp_inner_lip_after_resize_and_reopen`,
   `pattern_suppress_tests::enclosure_datums_follow_wall_height_and_board_depth_with_material_proofs`,
-  `cmd::plastic::tests::enclosure_snap_fit_follows_resized_front_wall`
+  `cmd::plastic::tests::enclosure_snap_fit_follows_resized_front_wall`, the `atomic_commands` contract tests
-- `solidcraft-kernel`: `tests::boolean_identity_on_tangent_primitives`
+- `solidcraft-kernel`: `tests::boolean_identity_on_tangent_primitives`, the `boolean_props` property tests
 - `solidcraft-ui-egui` scenarios: `acceptance_sensor_enclosure`
 
 The **action matrix** (`apps/solidcraft-cli/tests/action_matrix.rs`) tries every ordinary action