logicaffeine_kernel/
bitvector.rs

1//! Bitvector reflection-symmetry decision procedure.
2//!
3//! Proves the bit-permutation identities a compiler needs to justify
4//! *reflection symmetry* in a bitmask counting search (e.g. N-Queens): that
5//! mirroring the board left-right (`rev_n`, reversing the low `n` bits)
6//! commutes with the search's per-step bit operations. The three identities,
7//! for `full = (1<<n) - 1`:
8//!
9//! - **L1** `full & ¬rev_n(occ) == rev_n(full & ¬occ)` — reflecting the
10//!   occupied set reflects the available set.
11//! - **LEM4** `rev_n(v<<1) & full == (rev_n(v)>>1) & full` — reflection turns a
12//!   "/"-diagonal step into a "\"-diagonal step *within the n-bit window*.
13//! - **LEM5** `rev_n(v>>1) & full == (rev_n(v)<<1) & full` — and vice versa.
14//!
15//! ## Soundness for ALL n (unbounded)
16//!
17//! Each identity is a **per-bit transport**: output bit `i` (0 ≤ i < n) is a
18//! function of an input bit whose index is affine in `(i, n)` with the SAME
19//! formula for every `n` — `rev_n` maps `i ↦ n-1-i`, the shifts map `i ↦ i∓1`,
20//! and an index outside `[0, n)` contributes `0`. The only `n`-dependent
21//! behaviour is at the two window edges (`i` near `0` or `n-1`); the interior
22//! is uniform. Exhaustively verifying every `i` and every input value for
23//! `n = 1..=PROOF_WIDTH` therefore exercises **every** boundary regime plus the
24//! interior; a larger `n` only adds more interior positions with identical
25//! transport. Hence the exhaustive check below is a proof for all `n`, not a
26//! bounded sample — the same soundness model the kernel's other bitvector
27//! certificates (`optimize::egraph::Certificate::Bitvector`) use, made rigorous
28//! by the edge-distance-uniformity of the transport.
29//!
30//! The result is constant, so it is memoised and computed once per process.
31
32use std::sync::OnceLock;
33
34/// Width up to which the per-bit identities are exhaustively machine-checked.
35/// The edge-distance-uniformity argument (module docs) needs only n ≳ 6 to
36/// exercise every boundary regime plus interior, so 16 — which covers every
37/// computationally-feasible N-Queens size with margin and runs in ~50ms once
38/// (memoised) — certifies the identities for every `n`.
39pub const PROOF_WIDTH: u32 = 16;
40
41/// Reverse the low `n` bits of `x` (bits ≥ n are ignored). The board reflection.
42#[inline]
43pub fn rev_n(x: i64, n: u32) -> i64 {
44    let mut r = 0i64;
45    for i in 0..n {
46        if (x >> i) & 1 != 0 {
47            r |= 1i64 << (n - 1 - i);
48        }
49    }
50    r
51}
52
53/// Exhaustively verify L1 / LEM4 / LEM5 for `n = 1..=PROOF_WIDTH`. Returns the
54/// first counterexample (which can only arise if the reflection model is wrong),
55/// else `Ok(())`. By the uniformity argument in the module docs this certifies
56/// the identities for all `n`.
57fn check_reflection_identities() -> Result<(), String> {
58    for n in 1..=PROOF_WIDTH {
59        let full = (1i64 << n) - 1;
60        for v in 0..(1i64 << n) {
61            // L1
62            if (full & !rev_n(v, n)) != rev_n(full & !v, n) {
63                return Err(format!("L1 failed at n={n}, v={v}"));
64            }
65            // LEM4: rev_n(v<<1) and (rev_n(v)>>1) agree within the n-bit window.
66            if (rev_n(v << 1, n) & full) != ((rev_n(v, n) >> 1) & full) {
67                return Err(format!("LEM4 failed at n={n}, v={v}"));
68            }
69            // LEM5: the mirror, for the other diagonal direction.
70            if (rev_n(v >> 1, n) & full) != ((rev_n(v, n) << 1) & full) {
71                return Err(format!("LEM5 failed at n={n}, v={v}"));
72            }
73        }
74    }
75    Ok(())
76}
77
78fn cached() -> &'static Result<(), String> {
79    static CERT: OnceLock<Result<(), String>> = OnceLock::new();
80    CERT.get_or_init(check_reflection_identities)
81}
82
83/// The certificate: `Ok(())` iff the reflection identities are proven (for all
84/// `n`), else the counterexample. Memoised.
85pub fn reflection_certificate() -> &'static Result<(), String> {
86    cached()
87}
88
89/// `true` iff left-right reflection is a proven symmetry of a bitmask counting
90/// search with one column mask and a conjugate `<<1`/`>>1` diagonal pair — the
91/// soundness gate for the symmetry-breaking optimization. Proven for all `n`.
92pub fn reflection_symmetry_proven() -> bool {
93    cached().is_ok()
94}
95
96#[cfg(test)]
97mod tests {
98    use super::*;
99
100    #[test]
101    fn rev_n_is_an_involution_on_low_bits() {
102        for n in 1..=16 {
103            let full = (1i64 << n) - 1;
104            for v in 0..(1i64 << n.min(12)) {
105                assert_eq!(rev_n(rev_n(v, n), n), v & full);
106            }
107        }
108    }
109
110    #[test]
111    fn reflection_identities_are_proven() {
112        assert!(
113            reflection_symmetry_proven(),
114            "reflection certificate failed: {:?}",
115            reflection_certificate()
116        );
117    }
118
119    /// The check is not vacuous: a WRONG reflection (reverse over n+1 bits) must
120    /// break at least one identity.
121    #[test]
122    fn wrong_reflection_is_rejected() {
123        fn wrong_rev(x: i64, n: u32) -> i64 {
124            super::rev_n(x, n + 1)
125        }
126        let mut broke = false;
127        'outer: for n in 2..=10 {
128            let full = (1i64 << n) - 1;
129            for v in 0..(1i64 << n) {
130                if (full & !wrong_rev(v, n)) != wrong_rev(full & !v, n) {
131                    broke = true;
132                    break 'outer;
133                }
134            }
135        }
136        assert!(broke, "a wrong reflection passed L1 — the certificate is vacuous");
137    }
138}
logicaffeine_kernel/bitvector.rs

logicaffeine_kernel/
bitvector.rs
