feat: rule engine and smt

.github/workflows/rust.yml

@@ -24,6 +24,11 @@ jobs:
         with:
           components: rustfmt, clippy
 
+      - name: Install Z3
+        run: |
+          sudo apt-get update
+          sudo apt-get install -y libz3-dev libdbus-1-dev libudev-dev pkg-config
+
       - name: Cache cargo registry & build artifacts
         uses: actions/cache@v5
         with:
@@ -71,6 +76,11 @@ jobs:
       - name: Install stable Rust toolchain
         uses: dtolnay/rust-toolchain@stable
 
+      - name: Install Z3
+        run: |
+          sudo apt-get update
+          sudo apt-get install -y libz3-dev libdbus-1-dev libudev-dev pkg-config
+
       - name: Cache cargo registry & build artifacts
         uses: actions/cache@v5
         with:
@@ -122,6 +132,11 @@ jobs:
       - name: Install stable Rust toolchain
         uses: dtolnay/rust-toolchain@stable
 
+      - name: Install Z3
+        run: |
+          sudo apt-get update
+          sudo apt-get install -y libz3-dev libdbus-1-dev libudev-dev pkg-config
+
       - name: Cache cargo registry & build artifacts
         uses: actions/cache@v5
         with:
@@ -149,3 +164,71 @@ jobs:
             echo "::error::Uncommitted snapshot changes detected. Run INSTA_UPDATE=new cargo test --test sarif_snapshots -p sanctifier-core --no-default-features then cargo insta accept --workspace and commit the .snap files."
             exit 1
           fi
+
+  # ---------------------------------------------------------------------------
+  # Rule engine orchestration — integration/e2e coverage
+  # Covers: RuleRegistry pipeline, determinism, custom rules, output stability.
+  # ---------------------------------------------------------------------------
+  rule-engine-e2e:
+    name: Rule Engine Orchestration (integration/e2e)
+    runs-on: ubuntu-latest
+
+    steps:
+      - name: Checkout repository
+        uses: actions/checkout@v6
+
+      - name: Install stable Rust toolchain
+        uses: dtolnay/rust-toolchain@stable
+
+      - name: Install Z3
+        run: |
+          sudo apt-get update
+          sudo apt-get install -y libz3-dev libdbus-1-dev libudev-dev pkg-config
+
+      - name: Cache cargo registry & build artifacts
+        uses: actions/cache@v5
+        with:
+          path: |
+            ~/.cargo/registry
+            ~/.cargo/git
+            target
+          key: ${{ runner.os }}-cargo-rule-e2e-${{ hashFiles('**/Cargo.lock') }}
+          restore-keys: |
+            ${{ runner.os }}-cargo-rule-e2e-
+
+      - name: Run rule engine orchestration integration tests
+        run: cargo test --test rule_engine_orchestration_test -p sanctifier-core
+
+  # ---------------------------------------------------------------------------
+  # Z3 backend module boundaries — integration coverage for S011
+  # Covers: smt::types, smt::invariants, smt::backend, smt::benchmark.
+  # ---------------------------------------------------------------------------
+  smt-module-boundaries:
+    name: Z3 Backend Module Boundaries (S011)
+    runs-on: ubuntu-latest
+
+    steps:
+      - name: Checkout repository
+        uses: actions/checkout@v6
+
+      - name: Install stable Rust toolchain
+        uses: dtolnay/rust-toolchain@stable
+
+      - name: Install Z3
+        run: |
+          sudo apt-get update
+          sudo apt-get install -y libz3-dev libdbus-1-dev libudev-dev pkg-config
+
+      - name: Cache cargo registry & build artifacts
+        uses: actions/cache@v5
+        with:
+          path: |
+            ~/.cargo/registry
+            ~/.cargo/git
+            target
+          key: ${{ runner.os }}-cargo-smt-boundaries-${{ hashFiles('**/Cargo.lock') }}
+          restore-keys: |
+            ${{ runner.os }}-cargo-smt-boundaries-
+
+      - name: Run Z3 module boundary integration tests
+        run: cargo test --test smt_module_boundaries_test -p sanctifier-core

DOCUMENTATION_INDEX.md

@@ -183,6 +183,7 @@
 - Comprehensive remediation guidance with checked/saturating alternatives
 - Deduplication strategy and output formats
 - Known limitations and configuration options
+
 **[docs/rules/s001-auth-gap.md](docs/rules/s001-auth-gap.md)** - S001: Missing Authorization Guard (`auth_gap`)
 
 - What constitutes a privileged operation (storage mutation, external call)
@@ -199,6 +200,38 @@
 - Examples and remediation guidance
 - Reference implementations and test coverage
 
+### Rule Engine Orchestration — Integration/E2E Coverage
+
+**[specs/rule-engine-behavior.md](specs/rule-engine-behavior.md)**
+
+- Formal specification: discovery order, filtering, deduplication, exit codes
+- Integration/e2e test suite: [`tooling/sanctifier-core/tests/rule_engine_orchestration_test.rs`](tooling/sanctifier-core/tests/rule_engine_orchestration_test.rs)
+  - Registry population and deduplication
+  - Per-rule firing and `run_all` consistency
+  - Determinism across repeated calls
+  - Custom regex rule execution
+  - Registry extensibility without breaking existing rules
+  - End-to-end multi-file scan pipeline
+  - Output format (`RuleViolation`) JSON stability
+- CI job: `rule-engine-e2e` in [`.github/workflows/rust.yml`](.github/workflows/rust.yml)
+
+### Z3 Backend Invariants (S011) — Module Boundaries
+
+**Finding code:** `S011` — see [`docs/error-codes.md`](docs/error-codes.md)
+
+**Module layout** (`tooling/sanctifier-core/src/smt/`):
+
+| Sub-module | File | Responsibility |
+|---|---|---|
+| `types` | [`src/smt/types.rs`](tooling/sanctifier-core/src/smt/types.rs) | All shared data types and error enums |
+| `invariants` | [`src/smt/invariants.rs`](tooling/sanctifier-core/src/smt/invariants.rs) | `#[invariant]` AST parsing + Z3 verification |
+| `backend` | [`src/smt/backend.rs`](tooling/sanctifier-core/src/smt/backend.rs) | `SmtVerifier`, fixed-point proof dispatch |
+| `benchmark` | [`src/smt/benchmark.rs`](tooling/sanctifier-core/src/smt/benchmark.rs) | Latency micro-benchmark for CI artifact |
+| `mod` | [`src/smt/mod.rs`](tooling/sanctifier-core/src/smt/mod.rs) | Public re-export facade (zero breaking surface) |
+
+- Integration/boundary test suite: [`tooling/sanctifier-core/tests/smt_module_boundaries_test.rs`](tooling/sanctifier-core/tests/smt_module_boundaries_test.rs)
+- CI job: `smt-module-boundaries` in [`.github/workflows/rust.yml`](.github/workflows/rust.yml)
+
 ### WASM Module Versioning & Input Validation
 
 **[docs/wasm-versioning-alignment.md](docs/wasm-versioning-alignment.md)** - WASM module hardening