Module bitvector 

Bitvector reflection-symmetry decision procedure.

Proves the bit-permutation identities a compiler needs to justify reflection symmetry in a bitmask counting search (e.g. N-Queens): that mirroring the board left-right (rev_n, reversing the low n bits) commutes with the search’s per-step bit operations. The three identities, for full = (1<<n) - 1:

• L1 full & ¬rev_n(occ) == rev_n(full & ¬occ) — reflecting the occupied set reflects the available set.
• LEM4 rev_n(v<<1) & full == (rev_n(v)>>1) & full — reflection turns a “/”-diagonal step into a “"-diagonal step within the n-bit window.
• LEM5 rev_n(v>>1) & full == (rev_n(v)<<1) & full — and vice versa.

Soundness for ALL n (unbounded)

Each identity is a per-bit transport: output bit i (0 ≤ i < n) is a function of an input bit whose index is affine in (i, n) with the SAME formula for every n — rev_n maps i ↦ n-1-i, the shifts map i ↦ i∓1, and an index outside [0, n) contributes 0. The only n-dependent behaviour is at the two window edges (i near 0 or n-1); the interior is uniform. Exhaustively verifying every i and every input value for n = 1..=PROOF_WIDTH therefore exercises every boundary regime plus the interior; a larger n only adds more interior positions with identical transport. Hence the exhaustive check below is a proof for all n, not a bounded sample — the same soundness model the kernel’s other bitvector certificates (optimize::egraph::Certificate::Bitvector) use, made rigorous by the edge-distance-uniformity of the transport.

The result is constant, so it is memoised and computed once per process.

Constants

PROOF_WIDTH

Width up to which the per-bit identities are exhaustively machine-checked. The edge-distance-uniformity argument (module docs) needs only n ≳ 6 to exercise every boundary regime plus interior, so 16 — which covers every computationally-feasible N-Queens size with margin and runs in ~50ms once (memoised) — certifies the identities for every n.

Functions

reflection_certificate

The certificate: Ok(()) iff the reflection identities are proven (for all n), else the counterexample. Memoised.

reflection_symmetry_proven

true iff left-right reflection is a proven symmetry of a bitmask counting search with one column mask and a conjugate <<1/>>1 diagonal pair — the soundness gate for the symmetry-breaking optimization. Proven for all n.

rev_n

Reverse the low n bits of x (bits ≥ n are ignored). The board reflection.