connections 0.1.0

//! Galois-connection law predicates, kind-bound and ConnK-bound.
//!
//! Each predicate takes either `&Conn<A, B, L>` (L-laws),
//! `&Conn<A, B, R>` (R-laws), or `&T: ConnL<A=A,B=B> + ConnR<A=A,B=B>` (laws spanning
//! both views). Inputs are passed by value (Conn is `Copy`).
//! Returns `bool`.

use crate::conn::{Conn, ConnL, ConnR, L, R};

// (back-compat re-exports removed under the prefix-strip rename —
// `floor_le_ceil`, `ulp_bound`, `idempotent` are the canonical names.)

// ── L-side predicates ─────────────────────────────────────────────────

/// Galois law (left): `ceil(a) ≤ b ⟺ a ≤ inner(b)`.
pub fn galois_l<A: Copy + Eq + PartialOrd, B: Copy + Eq + PartialOrd>(
    c: &Conn<A, B, L>,
    a: A,
    b: B,
) -> bool {
    (c.ceil(a) <= b) == (a <= c.upper(b))
}

/// Closure law (left): `a ≤ inner(ceil(a))` — unit of `inner ⊣ ceil`.
pub fn closure_l<A: Copy + PartialOrd, B: Copy>(c: &Conn<A, B, L>, a: A) -> bool {
    a <= c.upper(c.ceil(a))
}

/// Kernel law (left): `ceil(inner(b)) ≤ b` — counit of `inner ⊣ ceil`.
pub fn kernel_l<A: Copy, B: Copy + PartialOrd>(c: &Conn<A, B, L>, b: B) -> bool {
    c.ceil(c.upper(b)) <= b
}

/// Monotonicity (left): `a1 ≤ a2 ⟹ ceil(a1) ≤ ceil(a2)`.
pub fn monotone_l<A: Copy + PartialOrd, B: Copy + PartialOrd>(
    c: &Conn<A, B, L>,
    a1: A,
    a2: A,
) -> bool {
    if a1 <= a2 {
        c.ceil(a1) <= c.ceil(a2)
    } else {
        true
    }
}

/// Idempotence (left): `(inner ∘ ceil)² == (inner ∘ ceil)`.
pub fn idempotent_l<A: Copy + Eq, B: Copy>(c: &Conn<A, B, L>, a: A) -> bool {
    let once = c.upper(c.ceil(a));
    let twice = c.upper(c.ceil(once));
    once == twice
}

/// Backwards-compat alias for [`idempotent_l`].
pub fn idempotent<A: Copy + Eq, B: Copy>(c: &Conn<A, B, L>, a: A) -> bool {
    idempotent_l(c, a)
}

/// `upper1` unit law: `a ≤ upper1(c, id, a)`.
pub fn upper1_id_unit<A: Copy + PartialOrd, B: Copy>(c: &Conn<A, B, L>, a: A) -> bool {
    a <= c.upper1(|x| x, a)
}

/// `upper2` collapse-on-projection: `upper2(c, |p, _| p, a, a) == upper1(c, id, a)`.
pub fn upper2_id_diag<A: Copy + Eq, B: Copy>(c: &Conn<A, B, L>, a: A) -> bool {
    c.upper2(|p, _q| p, a, a) == c.upper1(|x| x, a)
}

/// `ceil1` kernel law: `ceil1(c, id, b) ≤ b`.
pub fn ceil1_id_kernel<A: Copy, B: Copy + PartialOrd>(c: &Conn<A, B, L>, b: B) -> bool {
    c.ceil1(|x| x, b) <= b
}

/// `ceil2` collapse-on-projection.
pub fn ceil2_id_diag<A: Copy, B: Copy + Eq>(c: &Conn<A, B, L>, b: B) -> bool {
    c.ceil2(|p, _q| p, b, b) == c.ceil1(|x| x, b)
}

/// Round-trip via ceil: `ceil(upper(b)) == b` (exact-embedding L-Conns).
pub fn roundtrip_ceil<A: Copy, B: Copy + Eq>(c: &Conn<A, B, L>, b: B) -> bool {
    c.ceil(c.upper(b)) == b
}

/// Iso forward round-trip (L): `inner(ceil(a)) == a`. Holds for
/// any L-Conn that is also an iso (no information lost on the
/// `A → B` side); only needs `A: Eq`, so usable on types that
/// don't impl `Ord`.
pub fn iso_roundtrip_l<A: Copy + Eq, B: Copy>(c: &Conn<A, B, L>, a: A) -> bool {
    c.upper(c.ceil(a)) == a
}

/// `b == ceil(a) ⇒ filter_l(a, b)` — the lower edge of the principal
/// filter generated by `a` is contained in itself.
pub fn filter_l_at_ceil<A: Copy, B: Copy + PartialOrd>(c: &Conn<A, B, L>, a: A) -> bool {
    c.filter_l(a, c.ceil(a))
}

/// Upward closure: `filter_l(a, b1) && b1 ≤ b2 ⇒ filter_l(a, b2)`.
pub fn filter_l_upward_closed<A: Copy, B: Copy + PartialOrd>(
    c: &Conn<A, B, L>,
    a: A,
    b1: B,
    b2: B,
) -> bool {
    if c.filter_l(a, b1) && b1 <= b2 {
        c.filter_l(a, b2)
    } else {
        true
    }
}

/// `filter_l(a, b) ⟺ a ≤ upper(b)` — principal-filter membership
/// agrees with the Galois-adjoint characterization. Non-trivial:
/// it relies on `ceil ⊣ upper`, so this is a regression test on
/// the L-Galois law witnessed through `filter_l`.
pub fn filter_l_via_upper<A: Copy + PartialOrd, B: Copy + PartialOrd>(
    c: &Conn<A, B, L>,
    a: A,
    b: B,
) -> bool {
    c.filter_l(a, b) == (a <= c.upper(b))
}

// ── R-side predicates ─────────────────────────────────────────────────

/// Galois law (right): `inner(b) ≤ a ⟺ b ≤ floor(a)`.
pub fn galois_r<A: Copy + Eq + PartialOrd, B: Copy + Eq + PartialOrd>(
    c: &Conn<A, B, R>,
    a: A,
    b: B,
) -> bool {
    (c.lower(b) <= a) == (b <= c.floor(a))
}

/// Closure law (right): `inner(floor(a)) ≤ a`.
pub fn closure_r<A: Copy + PartialOrd, B: Copy>(c: &Conn<A, B, R>, a: A) -> bool {
    c.lower(c.floor(a)) <= a
}

/// Kernel law (right): `b ≤ floor(inner(b))`.
pub fn kernel_r<A: Copy, B: Copy + PartialOrd>(c: &Conn<A, B, R>, b: B) -> bool {
    b <= c.floor(c.lower(b))
}

/// Monotonicity (right): `b1 ≤ b2 ⟹ inner(b1) ≤ inner(b2)`.
pub fn monotone_r<A: Copy + PartialOrd, B: Copy + PartialOrd>(
    c: &Conn<A, B, R>,
    b1: B,
    b2: B,
) -> bool {
    if b1 <= b2 {
        c.lower(b1) <= c.lower(b2)
    } else {
        true
    }
}

/// Idempotence (right): the kernel operator is idempotent on its image.
pub fn idempotent_r<A: Copy, B: Copy + Eq>(c: &Conn<A, B, R>, b: B) -> bool {
    let once = c.floor(c.lower(b));
    let twice = c.floor(c.lower(once));
    once == twice
}

/// `lower1` counit law: `lower1(c, id, a) ≤ a`.
pub fn lower1_id_counit<A: Copy + PartialOrd, B: Copy>(c: &Conn<A, B, R>, a: A) -> bool {
    c.lower1(|x| x, a) <= a
}

/// `lower2` collapse-on-projection.
pub fn lower2_id_diag<A: Copy + Eq, B: Copy>(c: &Conn<A, B, R>, a: A) -> bool {
    c.lower2(|p, _q| p, a, a) == c.lower1(|x| x, a)
}

/// `floor1` kernel law: `b ≤ floor1(c, id, b)`.
pub fn floor1_id_kernel<A: Copy, B: Copy + PartialOrd>(c: &Conn<A, B, R>, b: B) -> bool {
    b <= c.floor1(|x| x, b)
}

/// `floor2` collapse-on-projection.
pub fn floor2_id_diag<A: Copy, B: Copy + Eq>(c: &Conn<A, B, R>, b: B) -> bool {
    c.floor2(|p, _q| p, b, b) == c.floor1(|x| x, b)
}

/// Round-trip via floor: `floor(inner(b)) == b` (exact-embedding R-Conns).
pub fn roundtrip_floor<A: Copy, B: Copy + Eq>(c: &Conn<A, B, R>, b: B) -> bool {
    c.floor(c.lower(b)) == b
}

/// `b == floor(a) ⇒ filter_r(a, b)` — the upper edge of the
/// principal ideal generated by `a` is contained in itself.
pub fn filter_r_at_floor<A: Copy, B: Copy + PartialOrd>(c: &Conn<A, B, R>, a: A) -> bool {
    c.filter_r(a, c.floor(a))
}

/// Downward closure: `filter_r(a, b1) && b2 ≤ b1 ⇒ filter_r(a, b2)`.
pub fn filter_r_downward_closed<A: Copy, B: Copy + PartialOrd>(
    c: &Conn<A, B, R>,
    a: A,
    b1: B,
    b2: B,
) -> bool {
    if c.filter_r(a, b1) && b2 <= b1 {
        c.filter_r(a, b2)
    } else {
        true
    }
}

/// `filter_r(a, b) ⟺ lower(b) ≤ a` — principal-ideal membership
/// agrees with the Galois-adjoint characterization. Non-trivial:
/// it relies on `lower ⊣ floor`, so this is a regression test on
/// the R-Galois law witnessed through `filter_r`.
pub fn filter_r_via_lower<A: Copy + PartialOrd, B: Copy + PartialOrd>(
    c: &Conn<A, B, R>,
    a: A,
    b: B,
) -> bool {
    c.filter_r(a, b) == (c.lower(b) <= a)
}

// ── ConnK-bound predicates ──────────────────────────────────────────

/// `floor(a) ≤ ceil(a)` — the rounding-sandwich.
///
/// **Necessary and sufficient for a true adjoint triple.** Equivalent
/// to: `inner` is order-reflecting (`inner(x) ≤ inner(y) ⟹ x ≤ y`).
///
/// Sufficiency: from the closure laws `inner(floor(a)) ≤ a ≤ inner(ceil(a))`,
/// transitivity gives `inner(floor(a)) ≤ inner(ceil(a))`, and
/// order-reflection of `inner` lifts this to `floor(a) ≤ ceil(a)`.
///
/// Necessity: assume `floor(a) ≤ ceil(a)` for every `a`. Take
/// `x, y ∈ B` with `inner(x) ≤ inner(y)`. Then
/// `x ≤ floor(inner(x)) ≤ ceil(inner(x)) ≤ y` — first step is
/// `inner ⊣ floor` kernel, second is the assumption at `a = inner(x)`,
/// third is L-Galois `ceil(a) ≤ b ⟺ a ≤ inner(b)` with the given
/// hypothesis. So `x ≤ y`.
///
/// Required for every marker shipping both `ConnL` and `ConnR`. The
/// `law_battery!` `full` subset enforces both this and its cause —
/// see [`order_reflecting`] for the load-bearing predicate. This
/// predicate is the user-facing fast signal (single quantifier over
/// `A`); `order_reflecting` quantifies over `B²` and thus catches
/// boundary violations with twice the proptest surface area.
pub fn floor_le_ceil<T, A: Copy, B: Copy + PartialOrd>(t: &T, a: A) -> bool
where
    T: ConnL<A = A, B = B> + ConnR<A = A, B = B>,
{
    t.view_r().floor(a) <= t.view_l().ceil(a)
}

/// Swap involution on L-values: `c.swap_l().swap_r() == c`, exact by
/// fn-pointer identity ([`Conn`]'s `PartialEq`). The law that makes
/// `view_l` a lawful spelling of "the direct view".
pub fn swap_involutive_l<A: Copy, B: Copy>(c: &Conn<A, B, L>) -> bool {
    c.swap_l().swap_r() == *c
}

/// Swap involution on R-values: `c.swap_r().swap_l() == c`, exact by
/// fn-pointer identity.
pub fn swap_involutive_r<A: Copy, B: Copy>(c: &Conn<A, B, R>) -> bool {
    c.swap_r().swap_l() == *c
}

/// A lawful triple shares its middle adjoint: the L-view's `upper` and
/// the R-view's `lower` agree pointwise. Checked behaviorally — the
/// two views differ in their outer adjoint, so fn-pointer equality of
/// the whole `Conn` cannot express this.
pub fn shared_middle<T, A, B>(t: &T, b: B) -> bool
where
    T: ConnL<A = A, B = B> + ConnR<A = A, B = B>,
    A: Copy + PartialEq,
    B: Copy,
{
    t.view_l().upper(b) == t.view_r().lower(b)
}

/// `inner(b1) ≤ inner(b2) ⟹ b1 ≤ b2` — `inner` is order-reflecting.
///
/// **The defining property of an adjoint triple.** Given the per-side
/// L/R Galois laws, this is equivalent to [`floor_le_ceil`] (see that
/// predicate's doc for both directions of the proof). Order-reflection
/// is the *cause*; the rounding sandwich is the *corollary*.
///
/// Quantifying over `(b1, b2) ∈ B²` gives a proptest twice the surface
/// area of [`floor_le_ceil`] (which only sees `a ∈ A`), so this catches
/// boundary violations the rounding-sandwich check would miss when the
/// source-side strategy under-samples extremes — the failure mode that
/// hid the Haskell `f09sys` bug for years.
///
/// `inner` is taken from the L view (`t.view_l().upper`); for a true
/// triple the L-view's `upper` and the R-view's `lower` are the same
/// function pointer by construction, so the choice of view is
/// arbitrary.
pub fn order_reflecting<T, A, B>(t: &T, b1: B, b2: B) -> bool
where
    T: ConnL<A = A, B = B> + ConnR<A = A, B = B>,
    A: Copy + PartialOrd,
    B: Copy + PartialOrd,
{
    let l = t.view_l();
    let a1 = l.upper(b1);
    let a2 = l.upper(b2);
    if a1 <= a2 { b1 <= b2 } else { true }
}

/// ULP-bound: `ceil(a) - floor(a) ≤ 1` under a caller-provided
/// rung-extractor.
pub fn ulp_bound<T, A, B, F>(t: &T, a: A, rung: F) -> bool
where
    T: ConnL<A = A, B = B> + ConnR<A = A, B = B>,
    A: Copy,
    B: Copy,
    F: Fn(B) -> i64,
{
    let c_val = rung(t.view_l().ceil(a));
    let f_val = rung(t.view_r().floor(a));
    c_val
        .checked_sub(f_val)
        .is_some_and(|d| (0..=1).contains(&d))
}

/// `interval(t, x).contains(&x)` whenever the bracket is
/// non-empty; vacuously true when the bracket is `Empty`
/// (malformed triple, or antichain endpoints in a partial order).
///
/// As of the `interval` sandwich-postcondition refactor this is
/// **true by construction**: `interval` returns `Closed` only
/// when `lo ≤ x ≤ hi`. Kept as a regression check on `interval`'s
/// body — a bug there would now be caught here directly.
pub fn bracket_contains_x<T, A, B>(t: &T, x: A) -> bool
where
    T: ConnL<A = A, B = B> + ConnR<A = A, B = B>,
    A: Copy + PartialOrd,
    B: Copy,
{
    let i = crate::conn::interval(t, x);
    matches!(i, crate::interval::Interval::Empty) || i.contains(&x)
}

/// Bracket endpoints are themselves grid-aligned: re-bracketing
/// either endpoint produces the singleton interval at that endpoint.
/// This is the *correct* idempotence-flavored property — `lo` and
/// `hi` sit on the boundary between B-cells, so each one is its own
/// bracket.
pub fn bracket_endpoints_self_bracket<T, A, B>(t: &T, x: A) -> bool
where
    T: ConnL<A = A, B = B> + ConnR<A = A, B = B>,
    A: Copy + PartialOrd,
    B: Copy,
{
    match crate::conn::interval(t, x) {
        crate::interval::Interval::Empty => true,
        crate::interval::Interval::Closed { lo, hi } => {
            crate::conn::interval(t, lo) == crate::interval::Interval::Closed { lo, hi: lo }
                && crate::conn::interval(t, hi) == crate::interval::Interval::Closed { lo: hi, hi }
        }
    }
}

/// Bracket endpoints share `x`'s B-cell:
/// `floor(lo) == floor(x) && ceil(hi) == ceil(x)`.
pub fn bracket_endpoints_share_b_cell<T, A, B>(t: &T, x: A) -> bool
where
    T: ConnL<A = A, B = B> + ConnR<A = A, B = B>,
    A: Copy + PartialOrd,
    B: Copy + Eq,
{
    match crate::conn::interval(t, x) {
        crate::interval::Interval::Empty => true,
        crate::interval::Interval::Closed { lo, hi } => {
            t.view_r().floor(lo) == t.view_r().floor(x) && t.view_l().ceil(hi) == t.view_l().ceil(x)
        }
    }
}

/// `round(t, x)` is always one of `t.view_l().ceil(x)` / `t.view_r().floor(x)`.
pub fn round_picks_endpoint<T, A, B>(t: &T, x: A) -> bool
where
    T: ConnL<A = A, B = B> + ConnR<A = A, B = B>,
    A: Copy + PartialOrd + core::ops::Sub<Output = A> + From<u8>,
    B: Copy + Eq,
{
    let r = crate::conn::round(t, x);
    r == t.view_l().ceil(x) || r == t.view_r().floor(x)
}

/// `truncate(t, x)` is always one of `t.view_l().ceil(x)` / `t.view_r().floor(x)`.
pub fn truncate_picks_endpoint<T, A, B>(t: &T, x: A) -> bool
where
    T: ConnL<A = A, B = B> + ConnR<A = A, B = B>,
    A: Copy + PartialOrd + From<u8>,
    B: Copy + Eq,
{
    let v = crate::conn::truncate(t, x);
    v == t.view_l().ceil(x) || v == t.view_r().floor(x)
}

/// Toward-zero contract: `x ≥ 0 ⟹ truncate = floor`, otherwise `= ceil`.
pub fn truncate_toward_zero<T, A, B>(t: &T, x: A) -> bool
where
    T: ConnL<A = A, B = B> + ConnR<A = A, B = B>,
    A: Copy + PartialOrd + From<u8>,
    B: Copy + Eq,
{
    let zero = A::from(0);
    let v = crate::conn::truncate(t, x);
    if x >= zero {
        v == t.view_r().floor(x)
    } else {
        v == t.view_l().ceil(x)
    }
}

/// `round1(t, id, x) == x` for an identity triple.
pub fn round1_id_unit<T, A, B>(t: &T, x: B) -> bool
where
    T: ConnL<A = A, B = B> + ConnR<A = A, B = B>,
    A: Copy + PartialOrd + core::ops::Sub<Output = A> + From<u8>,
    B: Copy + Eq,
{
    crate::conn::round1(t, |a| a, x) == x
}

/// `truncate1(t, id, x) == x` for an identity triple.
pub fn truncate1_id_unit<T, A, B>(t: &T, x: B) -> bool
where
    T: ConnL<A = A, B = B> + ConnR<A = A, B = B>,
    A: Copy + PartialOrd + From<u8>,
    B: Copy + Eq,
{
    crate::conn::truncate1(t, |a| a, x) == x
}

// ── Birkhoff median axioms (triple-bound) ─────────────────────────────

/// Median axiom 1 (idempotence): `median(t, x, x, y) == x`.
pub fn median_idempotent<T, A>(t: &T, x: A, y: A) -> bool
where
    T: ConnL<A = (A, A), B = A> + ConnR<A = (A, A), B = A>,
    A: Copy + Eq,
{
    crate::conn::median(t, x, x, y) == x
}

/// Median axiom 2 (rotation).
pub fn median_rotate<T, A>(t: &T, x: A, y: A, z: A) -> bool
where
    T: ConnL<A = (A, A), B = A> + ConnR<A = (A, A), B = A>,
    A: Copy + Eq,
{
    crate::conn::median(t, x, y, z) == crate::conn::median(t, z, x, y)
}

/// Median axiom 3 (last-two swap).
pub fn median_swap_yz<T, A>(t: &T, x: A, y: A, z: A) -> bool
where
    T: ConnL<A = (A, A), B = A> + ConnR<A = (A, A), B = A>,
    A: Copy + Eq,
{
    crate::conn::median(t, x, y, z) == crate::conn::median(t, x, z, y)
}

/// Median axiom 4 (associativity).
pub fn median_associative<T, A>(t: &T, w: A, x: A, y: A, z: A) -> bool
where
    T: ConnL<A = (A, A), B = A> + ConnR<A = (A, A), B = A>,
    A: Copy + Eq,
{
    let lhs = crate::conn::median(t, crate::conn::median(t, x, w, y), w, z);
    let rhs = crate::conn::median(t, x, w, crate::conn::median(t, y, w, z));
    lhs == rhs
}

// ── law_battery! macro ──────────────────────────────────────────────
//
// Generates the standard property-test battery for a `Conn` marker
// inside a fresh `mod $mod_name` block. Subsumes the per-host-type
// `props_for_pair!` macros that lived in `src/fixed/i*.rs` and the
// hand-rolled blocks in `time/duration.rs`, `addr/ip.rs`, `char.rs`,
// `float/f064.rs`, etc. (Plan 31 T2.)

/// Generate a property-test battery for an adjoint connection.
///
/// `conn:` accepts a value expression — either a triple-marker
/// instance (`TripleIdI32`, `Q008Q000`, …) or a `Conn<_,_,K>` const
/// (`TIMENANO`, `U032I032`, …). The projections (`.view_l()` /
/// `.view_r()`) extract the appropriate one-sided `Conn` from
/// either shape.
///
/// Each invocation emits `mod $mod_name { ... }` containing the
/// requested subset of the standard property checks:
///
/// | Subset (`subset:` flag) | Tests emitted | Trait bounds on `A` / `B` |
/// |-------------------------|---------------|---------------------------|
/// | `full` (default)        | `galois_l`, `galois_r`, `closure_l`, `closure_r`, `kernel_l`, `kernel_r`, `monotone_l`, `monotone_r`, `idempotent`, `floor_le_ceil`, `order_reflecting`, `bracket_contains_x`, `bracket_endpoints_self_bracket`, `bracket_endpoints_share_b_cell` | `A`, `B`: `Copy + Eq + PartialOrd` |
/// | `numeric_only`          | `full` ∪ `round_picks_endpoint`, `truncate_picks_endpoint`, `truncate_toward_zero`                                    | adds `A: Sub<Output = A> + From<u8>` |
/// | `l_only`                | `galois_l`, `closure_l`, `kernel_l`, `monotone_l`, `idempotent`, `filter_l_at_ceil`, `filter_l_upward_closed`, `filter_l_via_upper` | same |
/// | `r_only`                | `galois_r`, `closure_r`, `kernel_r`, `monotone_r`, `filter_r_at_floor`, `filter_r_downward_closed`, `filter_r_via_lower` (no `idempotent`; that is L-side) | same |
/// | `iso_only`              | `idempotent`, `iso_roundtrip_l`, `roundtrip_ceil`                                                                     | `A`: `Copy + Eq`; `B`: `Copy + Eq` (no `Ord` required) |
///
/// `cases: N` optionally overrides the proptest case count
/// (default: 256, the proptest default; set to 64 for expensive
/// generators like full-range `i128`).
///
/// ```text
/// connections::law_battery! {
///     mod q008q000,
///     conn: Q008Q000,
///     fine:   any::<i8>().prop_map(FixedI8::<U8>::from_bits),
///     coarse: any::<i8>().prop_map(FixedI8::<U0>::from_bits),
/// }
///
/// connections::law_battery! {
///     mod q000i032_iso,
///     conn: Q000I032,
///     fine:   any::<i32>().prop_map(FixedI32::<U0>::from_bits),
///     coarse: any::<i32>(),
///     subset: iso_only,
/// }
/// ```
#[macro_export]
macro_rules! law_battery {
    // ── Public top-level arms (forward to internal @batch arms) ──

    // full (default), no cases override
    (mod $m:ident, conn: $c:expr, fine: $f:expr, coarse: $cs:expr $(,)?) => {
        $crate::law_battery!(@batch full, $m, $c, $f, $cs,
            ::proptest::test_runner::Config::default());
    };
    (mod $m:ident, conn: $c:expr, fine: $f:expr, coarse: $cs:expr, cases: $n:expr $(,)?) => {
        $crate::law_battery!(@batch full, $m, $c, $f, $cs,
            ::proptest::test_runner::Config { cases: $n,
                .. ::proptest::test_runner::Config::default() });
    };

    // numeric_only — superset of `full`; adds round/truncate
    // contract properties that need `A: Sub<Output = A> + From<u8>`.
    (mod $m:ident, conn: $c:expr, fine: $f:expr, coarse: $cs:expr,
     subset: numeric_only $(,)?) => {
        $crate::law_battery!(@batch numeric_only, $m, $c, $f, $cs,
            ::proptest::test_runner::Config::default());
    };
    (mod $m:ident, conn: $c:expr, fine: $f:expr, coarse: $cs:expr,
     subset: numeric_only, cases: $n:expr $(,)?) => {
        $crate::law_battery!(@batch numeric_only, $m, $c, $f, $cs,
            ::proptest::test_runner::Config { cases: $n,
                .. ::proptest::test_runner::Config::default() });
    };

    // l_only
    (mod $m:ident, conn: $c:expr, fine: $f:expr, coarse: $cs:expr, subset: l_only $(,)?) => {
        $crate::law_battery!(@batch l_only, $m, $c, $f, $cs,
            ::proptest::test_runner::Config::default());
    };
    (mod $m:ident, conn: $c:expr, fine: $f:expr, coarse: $cs:expr, subset: l_only,
     cases: $n:expr $(,)?) => {
        $crate::law_battery!(@batch l_only, $m, $c, $f, $cs,
            ::proptest::test_runner::Config { cases: $n,
                .. ::proptest::test_runner::Config::default() });
    };

    // r_only
    (mod $m:ident, conn: $c:expr, fine: $f:expr, coarse: $cs:expr, subset: r_only $(,)?) => {
        $crate::law_battery!(@batch r_only, $m, $c, $f, $cs,
            ::proptest::test_runner::Config::default());
    };
    (mod $m:ident, conn: $c:expr, fine: $f:expr, coarse: $cs:expr, subset: r_only,
     cases: $n:expr $(,)?) => {
        $crate::law_battery!(@batch r_only, $m, $c, $f, $cs,
            ::proptest::test_runner::Config { cases: $n,
                .. ::proptest::test_runner::Config::default() });
    };

    // iso_only
    (mod $m:ident, conn: $c:expr, fine: $f:expr, coarse: $cs:expr, subset: iso_only $(,)?) => {
        $crate::law_battery!(@batch iso_only, $m, $c, $f, $cs,
            ::proptest::test_runner::Config::default());
    };
    (mod $m:ident, conn: $c:expr, fine: $f:expr, coarse: $cs:expr, subset: iso_only,
     cases: $n:expr $(,)?) => {
        $crate::law_battery!(@batch iso_only, $m, $c, $f, $cs,
            ::proptest::test_runner::Config { cases: $n,
                .. ::proptest::test_runner::Config::default() });
    };

    // ── Internal @batch arms ──
    //
    // `full` and `numeric_only` share their 14-test core via the
    // hidden `@props_full` arm; `numeric_only` then layers on the
    // arithmetic-bound contract tests via `@props_numeric_extras`.
    // Editing the `full` test set means editing `@props_full` —
    // both batteries pick up the change.

    (@batch full, $m:ident, $c:expr, $f:expr, $cs:expr, $cfg:expr) => {
        mod $m {
            #[allow(unused_imports)]
            use super::*;
            #[allow(unused_imports)]
            use ::proptest::prelude::*;
            #[allow(unused_imports)]
            use $crate::conn::{ConnL as _, ConnR as _};
            $crate::law_battery!(@props_full, $c, $f, $cs, $cfg);
        }
    };

    (@batch numeric_only, $m:ident, $c:expr, $f:expr, $cs:expr, $cfg:expr) => {
        mod $m {
            #[allow(unused_imports)]
            use super::*;
            #[allow(unused_imports)]
            use ::proptest::prelude::*;
            #[allow(unused_imports)]
            use $crate::conn::{ConnL as _, ConnR as _};
            $crate::law_battery!(@props_full, $c, $f, $cs, $cfg);
            $crate::law_battery!(@props_numeric_extras, $c, $f, $cs, $cfg);
        }
    };

    // The shared body for `full` and `numeric_only` — 14 tests.
    (@props_full, $c:expr, $f:expr, $cs:expr, $cfg:expr) => {
        ::proptest::proptest! {
            #![proptest_config($cfg)]
            #[test]
            fn galois_l(a in $f, b in $cs) {
                ::proptest::prop_assert!(
                    $crate::prop::conn::galois_l(&($c).swap_l().swap_r(), a, b));
            }
            #[test]
            fn galois_r(a in $f, b in $cs) {
                ::proptest::prop_assert!(
                    $crate::prop::conn::galois_r(&($c).swap_r().swap_l(), a, b));
            }
            #[test]
            fn closure_l(a in $f) {
                ::proptest::prop_assert!(
                    $crate::prop::conn::closure_l(&($c).swap_l().swap_r(), a));
            }
            #[test]
            fn closure_r(a in $f) {
                ::proptest::prop_assert!(
                    $crate::prop::conn::closure_r(&($c).swap_r().swap_l(), a));
            }
            #[test]
            fn kernel_l(b in $cs) {
                ::proptest::prop_assert!(
                    $crate::prop::conn::kernel_l(&($c).swap_l().swap_r(), b));
            }
            #[test]
            fn kernel_r(b in $cs) {
                ::proptest::prop_assert!(
                    $crate::prop::conn::kernel_r(&($c).swap_r().swap_l(), b));
            }
            #[test]
            fn monotone_l(a1 in $f, a2 in $f) {
                ::proptest::prop_assert!(
                    $crate::prop::conn::monotone_l(&($c).swap_l().swap_r(), a1, a2));
            }
            #[test]
            fn monotone_r(b1 in $cs, b2 in $cs) {
                ::proptest::prop_assert!(
                    $crate::prop::conn::monotone_r(&($c).swap_r().swap_l(), b1, b2));
            }
            #[test]
            fn idempotent(a in $f) {
                ::proptest::prop_assert!(
                    $crate::prop::conn::idempotent(&($c).swap_l().swap_r(), a));
            }
            #[test]
            fn floor_le_ceil(a in $f) {
                ::proptest::prop_assert!(
                    $crate::prop::conn::floor_le_ceil(&($c), a));
            }
            #[test]
            fn swap_involution(_x in ::proptest::strategy::Just(())) {
                ::proptest::prop_assert!(
                    $crate::prop::conn::swap_involutive_l(&($c).swap_l().swap_r()));
                ::proptest::prop_assert!(
                    $crate::prop::conn::swap_involutive_r(&($c).swap_r().swap_l()));
            }
            #[test]
            fn shared_middle(b in $cs) {
                ::proptest::prop_assert!(
                    $crate::prop::conn::shared_middle(&($c), b));
            }
            #[test]
            fn order_reflecting(b1 in $cs, b2 in $cs) {
                ::proptest::prop_assert!(
                    $crate::prop::conn::order_reflecting(&($c), b1, b2));
            }
            #[test]
            fn bracket_contains_x(a in $f) {
                ::proptest::prop_assert!(
                    $crate::prop::conn::bracket_contains_x(&($c), a));
            }
            #[test]
            fn bracket_endpoints_self_bracket(a in $f) {
                ::proptest::prop_assert!(
                    $crate::prop::conn::bracket_endpoints_self_bracket(&($c), a));
            }
            #[test]
            fn bracket_endpoints_share_b_cell(a in $f) {
                ::proptest::prop_assert!(
                    $crate::prop::conn::bracket_endpoints_share_b_cell(&($c), a));
            }
        }
    };

    // The numeric-only extras: round/truncate contract properties
    // requiring `A: Sub<Output = A> + From<u8>`. Layered on top of
    // `@props_full` by `@batch numeric_only`.
    (@props_numeric_extras, $c:expr, $f:expr, $cs:expr, $cfg:expr) => {
        ::proptest::proptest! {
            #![proptest_config($cfg)]
            #[test]
            fn round_picks_endpoint(a in $f) {
                ::proptest::prop_assert!(
                    $crate::prop::conn::round_picks_endpoint(&($c), a));
            }
            #[test]
            fn truncate_picks_endpoint(a in $f) {
                ::proptest::prop_assert!(
                    $crate::prop::conn::truncate_picks_endpoint(&($c), a));
            }
            #[test]
            fn truncate_toward_zero(a in $f) {
                ::proptest::prop_assert!(
                    $crate::prop::conn::truncate_toward_zero(&($c), a));
            }
        }
    };

    (@batch l_only, $m:ident, $c:expr, $f:expr, $cs:expr, $cfg:expr) => {
        mod $m {
            #[allow(unused_imports)]
            use super::*;
            #[allow(unused_imports)]
            use ::proptest::prelude::*;
            #[allow(unused_imports)]
            use $crate::conn::ConnL as _;
            ::proptest::proptest! {
                #![proptest_config($cfg)]
                #[test]
                fn galois_l(a in $f, b in $cs) {
                    ::proptest::prop_assert!(
                        $crate::prop::conn::galois_l(&($c), a, b));
                }
                #[test]
                fn closure_l(a in $f) {
                    ::proptest::prop_assert!(
                        $crate::prop::conn::closure_l(&($c), a));
                }
                #[test]
                fn kernel_l(b in $cs) {
                    ::proptest::prop_assert!(
                        $crate::prop::conn::kernel_l(&($c), b));
                }
                #[test]
                fn monotone_l(a1 in $f, a2 in $f) {
                    ::proptest::prop_assert!(
                        $crate::prop::conn::monotone_l(&($c), a1, a2));
                }
                #[test]
                fn idempotent(a in $f) {
                    ::proptest::prop_assert!(
                        $crate::prop::conn::idempotent(&($c), a));
                }
                #[test]
                fn filter_l_at_ceil(a in $f) {
                    ::proptest::prop_assert!(
                        $crate::prop::conn::filter_l_at_ceil(&($c), a));
                }
                #[test]
                fn filter_l_upward_closed(a in $f, b1 in $cs, b2 in $cs) {
                    // Bias toward `b1 ≤ b2` so the implication's
                    // antecedent isn't false ~half the time. For
                    // antichain pairs (where `partial_cmp` is None),
                    // the swap is a no-op and the test still passes
                    // vacuously, as before.
                    let (b1, b2) = if b1 <= b2 { (b1, b2) } else { (b2, b1) };
                    ::proptest::prop_assert!(
                        $crate::prop::conn::filter_l_upward_closed(
                            &($c), a, b1, b2));
                }
                #[test]
                fn filter_l_via_upper(a in $f, b in $cs) {
                    ::proptest::prop_assert!(
                        $crate::prop::conn::filter_l_via_upper(
                            &($c), a, b));
                }
            }
        }
    };

    (@batch r_only, $m:ident, $c:expr, $f:expr, $cs:expr, $cfg:expr) => {
        mod $m {
            #[allow(unused_imports)]
            use super::*;
            #[allow(unused_imports)]
            use ::proptest::prelude::*;
            #[allow(unused_imports)]
            use $crate::conn::ConnR as _;
            ::proptest::proptest! {
                #![proptest_config($cfg)]
                #[test]
                fn galois_r(a in $f, b in $cs) {
                    ::proptest::prop_assert!(
                        $crate::prop::conn::galois_r(&($c).swap_r().swap_l(), a, b));
                }
                #[test]
                fn closure_r(a in $f) {
                    ::proptest::prop_assert!(
                        $crate::prop::conn::closure_r(&($c).swap_r().swap_l(), a));
                }
                #[test]
                fn kernel_r(b in $cs) {
                    ::proptest::prop_assert!(
                        $crate::prop::conn::kernel_r(&($c).swap_r().swap_l(), b));
                }
                #[test]
                fn monotone_r(b1 in $cs, b2 in $cs) {
                    ::proptest::prop_assert!(
                        $crate::prop::conn::monotone_r(&($c).swap_r().swap_l(), b1, b2));
                }
                #[test]
                fn filter_r_at_floor(a in $f) {
                    ::proptest::prop_assert!(
                        $crate::prop::conn::filter_r_at_floor(&($c).swap_r().swap_l(), a));
                }
                #[test]
                fn filter_r_downward_closed(a in $f, b1 in $cs, b2 in $cs) {
                    // Bias toward `b2 ≤ b1` so the implication's
                    // antecedent isn't false ~half the time
                    // (downward-closed wants the larger element
                    // first). Antichain pairs collapse vacuously
                    // as before.
                    let (b1, b2) = if b2 <= b1 { (b1, b2) } else { (b2, b1) };
                    ::proptest::prop_assert!(
                        $crate::prop::conn::filter_r_downward_closed(
                            &($c).swap_r().swap_l(), a, b1, b2));
                }
                #[test]
                fn filter_r_via_lower(a in $f, b in $cs) {
                    ::proptest::prop_assert!(
                        $crate::prop::conn::filter_r_via_lower(
                            &($c).swap_r().swap_l(), a, b));
                }
            }
        }
    };

    (@batch iso_only, $m:ident, $c:expr, $f:expr, $cs:expr, $cfg:expr) => {
        mod $m {
            #[allow(unused_imports)]
            use super::*;
            #[allow(unused_imports)]
            use ::proptest::prelude::*;
            #[allow(unused_imports)]
            use $crate::conn::ConnL as _;
            ::proptest::proptest! {
                #![proptest_config($cfg)]
                #[test]
                fn idempotent(a in $f) {
                    ::proptest::prop_assert!(
                        $crate::prop::conn::idempotent(&($c).swap_l().swap_r(), a));
                }
                #[test]
                fn iso_roundtrip_l(a in $f) {
                    ::proptest::prop_assert!(
                        $crate::prop::conn::iso_roundtrip_l(&($c).swap_l().swap_r(), a));
                }
                #[test]
                fn roundtrip_ceil(b in $cs) {
                    ::proptest::prop_assert!(
                        $crate::prop::conn::roundtrip_ceil(&($c).swap_l().swap_r(), b));
                }
            }
        }
    };
}