test: add Qiskit oracle semantics reports

docs/circuit_oracle_compiler.md

@@ -9,3 +9,5 @@ O_phi |x>|y> = |x>|y xor phi(x)>.
 ```
 
 The compiler emits symbolic compute/apply/uncompute gates, a truth table, QASM-like text, cost metrics, cleanup-gate counts, and a reversibility check. Optional Qiskit truth-table synthesis is available for small predicates when Qiskit is installed; no IBM Quantum credentials are required.
+
+The Qiskit semantic report checks direct `BoolExpr` evaluation against the symbolic oracle truth table. If Qiskit is installed, Noetheris also records local `QuantumCircuit` summary metadata produced from that verified table. This is intentionally exponential in logical variable count and is scoped to small predicates.

docs/ibm_quantum_mapping.md

@@ -22,13 +22,22 @@ Dynamic circuits are relevant when verification, branching, or mid-circuit measu
 
 The repository runs locally without IBM Quantum credentials. Optional Qiskit export is skipped when Qiskit is unavailable and does not affect certificate validation. When Qiskit is installed, Noetheris can synthesize a small truth-table oracle into a `QuantumCircuit` summary for review.
 
+The v0.2 semantic report compares:
+
+- direct `BoolExpr.evaluate` truth-table evaluation;
+- symbolic oracle truth-table evaluation;
+- reversible cleanup checks;
+- optional Qiskit circuit summary metadata when `qiskit` is installed.
+
+The Qiskit summary is synthesized from the verified local truth table. Noetheris does not treat it as backend execution and does not use it as evidence of hardware behavior.
+
 The executable local example is:
 
 ```bash
 python3 examples/qiskit_oracle_export.py
 ```
 
-It emits the exact truth table, symbolic reversible gates, cleanup metrics, QASM-like text, and an optional local Qiskit circuit summary.
+It emits the exact truth table, symbolic reversible gates, cleanup metrics, QASM-like text, semantic checks, and an optional local Qiskit circuit summary.
 
 ## QAOA Relevance
 

docs/ibm_quantum_relevance.md

@@ -20,13 +20,16 @@ Structural predicate
 - Metrics for logical variables, ancilla count, cleanup gates, gate count, and depth estimate.
 - QASM-like text for review without Qiskit.
 - Optional Qiskit circuit synthesis from truth tables for small predicates when Qiskit is installed.
+- Semantic export reports comparing `BoolExpr`, symbolic-oracle truth tables, reversibility checks, and optional local `QuantumCircuit` summaries.
 - Exact local QAOA p=1 statevector check over tiny QUBO-derived Hamiltonians.
 
 ## Trust Boundary
 
 The Qiskit export path is an integration boundary, not a backend-execution claim. It requires no IBM Quantum credentials. It does not model transpilation, calibration, noise, scheduling, dynamic circuits, queue behavior, or fault-tolerant resources.
 
-The symbolic oracle and Qiskit export are exponential in predicate width when synthesized from truth tables. That is acceptable for v0.1.0 release evidence because the goal is semantic correctness for small predicates, not scalable circuit synthesis.
+The symbolic oracle and Qiskit export are exponential in predicate width when synthesized from truth tables. That is acceptable for release evidence because the goal is semantic correctness for small predicates, not scalable circuit synthesis.
+
+The optional Qiskit summary is not a simulation result. It records a local `QuantumCircuit` produced from the verified truth table and keeps `backend_execution: false`.
 
 ## Minimal Local Export
 

examples/qiskit_oracle_export.py

@@ -34,6 +34,7 @@ def main() -> None:
                 "policy": "2-of-3 custody authorization with whitelist and time window",
                 "qiskit_status": exported["status"],
                 "oracle_metrics": exported["oracle_metrics"],
+                "semantic_report": exported["semantic_report"],
                 "truth_table": exported["truth_table"],
                 "qiskit_circuit_summary": exported["qiskit_circuit_summary"],
                 "qasm_like": exported["qasm_like"].splitlines(),

python/noetheris/backends/__init__.py

@@ -9,6 +9,7 @@
     export_bool_expr_to_qiskit,
     export_oracle_to_qiskit,
     qasm_like_export,
+    qiskit_oracle_semantics_report,
     qiskit_status,
 )
 
@@ -20,6 +21,7 @@
     "ocean_bqm_parity_report",
     "qubo_exchange_payload",
     "qasm_like_export",
+    "qiskit_oracle_semantics_report",
     "qiskit_status",
     "replay_external_sample",
 ]

python/noetheris/backends/qiskit.py

@@ -1,7 +1,9 @@
 from __future__ import annotations
 
+from itertools import product
 from typing import Any
 
+from noetheris.certificates import stable_problem_hash
 from noetheris.circuits import BooleanOracle, BoolExpr, build_oracle
 
 
@@ -35,51 +37,140 @@ def export_oracle_to_qiskit(oracle: BooleanOracle) -> dict[str, Any]:
 
 
 def export_bool_expr_to_qiskit(expression: BoolExpr, *, name: str = "phi") -> dict[str, Any]:
+    semantics = qiskit_oracle_semantics_report(expression, name=name)
+    return {
+        "status": semantics["qiskit_status"],
+        "oracle_metrics": semantics["oracle_metrics"],
+        "truth_table": semantics["truth_table"],
+        "qasm_like": semantics["qasm_like"],
+        "qiskit_circuit_summary": semantics["qiskit_circuit_summary"],
+        "credential_required": False,
+        "export_policy": "truth-table synthesis is exact for small predicates and exponential in input width",
+        "semantic_report": semantics,
+    }
+
+
+def qiskit_oracle_semantics_report(
+    expression: BoolExpr, *, name: str = "phi"
+) -> dict[str, Any]:
     oracle = build_oracle(expression, name=name)
-    table = oracle.truth_table()
+    expression_table = _expression_truth_table(expression)
+    oracle_table = oracle.truth_table()
+    truth_table_hash = stable_problem_hash(
+        {
+            "variables": list(oracle.variables),
+            "truth_table": expression_table,
+        }
+    )
     status = qiskit_status()
-    circuit_summary: dict[str, Any] | None = None
+    circuit_summary = _qiskit_circuit_summary(
+        oracle,
+        expression_table,
+        name=name,
+        available=status["available"],
+    )
     if status["available"]:
-        try:
-            from qiskit import QuantumCircuit  # type: ignore
-
-            width = len(oracle.variables)
-            target = width
-            circuit = QuantumCircuit(width + 1, name=f"O_{name}")
-            for bitstring, value in sorted(table.items()):
-                if not value:
-                    continue
-                false_controls = [
-                    index for index, bit in enumerate(bitstring) if bit == "0"
-                ]
-                for index in false_controls:
-                    circuit.x(index)
-                if width == 0:
-                    circuit.x(target)
-                elif width == 1:
-                    circuit.cx(0, target)
-                else:
-                    circuit.mcx(list(range(width)), target)
-                for index in reversed(false_controls):
-                    circuit.x(index)
-            circuit_summary = {
-                "class": "qiskit.QuantumCircuit",
-                "num_qubits": circuit.num_qubits,
-                "depth": circuit.depth(),
-                "size": circuit.size(),
-                "name": circuit.name,
-            }
-        except Exception as exc:
-            circuit_summary = {
-                "class": "qiskit.QuantumCircuit",
-                "export_error": exc.__class__.__name__,
-            }
+        qiskit_semantics = {
+            "status": (
+                "export_error"
+                if circuit_summary and "export_error" in circuit_summary
+                else "synthesized_from_verified_truth_table"
+            ),
+            "truth_table_hash": truth_table_hash,
+            "backend_execution": False,
+            "equivalence_basis": (
+                "local BoolExpr truth table equals symbolic oracle truth table; "
+                "Qiskit circuit is synthesized from that verified table"
+            ),
+        }
+    else:
+        qiskit_semantics = {
+            "status": "qiskit_unavailable",
+            "truth_table_hash": truth_table_hash,
+            "backend_execution": False,
+            "equivalence_basis": "Qiskit package unavailable; local truth table remains authoritative",
+        }
     return {
-        "status": status,
+        "variables": list(oracle.variables),
+        "truth_table": expression_table,
+        "truth_table_hash": truth_table_hash,
+        "truth_table_entries": len(expression_table),
+        "true_rows": [
+            bitstring for bitstring, value in sorted(expression_table.items()) if value
+        ],
+        "bool_expr_truth_table": expression_table,
+        "symbolic_oracle_truth_table": oracle_table,
+        "semantic_checks": {
+            "bool_expr_matches_symbolic_oracle": expression_table == oracle_table,
+            "reversibility_check": oracle.reversibility_check(),
+            "complete_truth_table": len(expression_table) == 2 ** len(oracle.variables),
+        },
         "oracle_metrics": oracle.cost_metrics(),
-        "truth_table": table,
         "qasm_like": oracle.qasm_like(),
+        "qiskit_status": status,
         "qiskit_circuit_summary": circuit_summary,
+        "qiskit_semantics": qiskit_semantics,
         "credential_required": False,
-        "export_policy": "truth-table synthesis is exact for small predicates and exponential in input width",
+        "synthesis_limit": "truth-table synthesis is exponential in logical variable count",
     }
+
+
+def _expression_truth_table(expression: BoolExpr) -> dict[str, int]:
+    variables = expression.variables()
+    table: dict[str, int] = {}
+    for bits in product((False, True), repeat=len(variables)):
+        assignment = dict(zip(variables, bits))
+        table["".join("1" if bit else "0" for bit in bits)] = int(
+            expression.evaluate(assignment)
+        )
+    return table
+
+
+def _qiskit_circuit_summary(
+    oracle: Any,
+    table: dict[str, int],
+    *,
+    name: str,
+    available: bool,
+) -> dict[str, Any] | None:
+    if not available:
+        return None
+    try:
+        from qiskit import QuantumCircuit  # type: ignore
+
+        width = len(oracle.variables)
+        target = width
+        circuit = QuantumCircuit(width + 1, name=f"O_{name}")
+        for bitstring, value in sorted(table.items()):
+            if not value:
+                continue
+            false_controls = [
+                index for index, bit in enumerate(bitstring) if bit == "0"
+            ]
+            for index in false_controls:
+                circuit.x(index)
+            if width == 0:
+                circuit.x(target)
+            elif width == 1:
+                circuit.cx(0, target)
+            else:
+                circuit.mcx(list(range(width)), target)
+            for index in reversed(false_controls):
+                circuit.x(index)
+        return {
+            "class": "qiskit.QuantumCircuit",
+            "num_qubits": circuit.num_qubits,
+            "depth": circuit.depth(),
+            "size": circuit.size(),
+            "name": circuit.name,
+            "synthesis": "exact_truth_table_multi_controlled_x",
+            "truth_table_entries": len(table),
+            "true_rows": [
+                bitstring for bitstring, value in sorted(table.items()) if value
+            ],
+        }
+    except Exception as exc:
+        return {
+            "class": "qiskit.QuantumCircuit",
+            "export_error": exc.__class__.__name__,
+        }

tests/test_qiskit_semantics.py

@@ -0,0 +1,124 @@
+from __future__ import annotations
+
+from itertools import product
+import sys
+from types import SimpleNamespace
+from typing import Callable
+
+import pytest
+
+from noetheris.backends import (
+    export_bool_expr_to_qiskit,
+    qiskit_oracle_semantics_report,
+)
+from noetheris.circuits import AND, EQ, IMPLIES, OR, XOR, BoolExpr
+
+
+Predicate = Callable[[dict[str, bool]], bool]
+
+
+def _expected_table(variables: tuple[str, ...], predicate: Predicate) -> dict[str, int]:
+    table: dict[str, int] = {}
+    for bits in product((False, True), repeat=len(variables)):
+        assignment = dict(zip(variables, bits))
+        table["".join("1" if bit else "0" for bit in bits)] = int(
+            predicate(assignment)
+        )
+    return table
+
+
+def _cases() -> list[tuple[str, BoolExpr, tuple[str, ...], Predicate]]:
+    a = BoolExpr.var("a")
+    b = BoolExpr.var("b")
+    c = BoolExpr.var("c")
+    return [
+        ("and", AND(a, b), ("a", "b"), lambda bits: bits["a"] and bits["b"]),
+        ("or", OR(a, b), ("a", "b"), lambda bits: bits["a"] or bits["b"]),
+        ("xor", XOR(a, b), ("a", "b"), lambda bits: bits["a"] ^ bits["b"]),
+        (
+            "implies",
+            IMPLIES(a, b),
+            ("a", "b"),
+            lambda bits: (not bits["a"]) or bits["b"],
+        ),
+        ("eq", EQ(a, b), ("a", "b"), lambda bits: bits["a"] == bits["b"]),
+        (
+            "threshold_two_of_three",
+            OR(AND(a, b), AND(a, c), AND(b, c)),
+            ("a", "b", "c"),
+            lambda bits: sum(1 for value in bits.values() if value) >= 2,
+        ),
+    ]
+
+
+@pytest.mark.parametrize("name,expression,variables,predicate", _cases())
+def test_qiskit_oracle_semantics_match_bool_expr_and_symbolic_oracle(
+    name: str,
+    expression: BoolExpr,
+    variables: tuple[str, ...],
+    predicate: Predicate,
+) -> None:
+    expected = _expected_table(variables, predicate)
+    report = qiskit_oracle_semantics_report(expression, name=name)
+    payload = export_bool_expr_to_qiskit(expression, name=name)
+    assert report["variables"] == list(variables)
+    assert report["truth_table"] == expected
+    assert report["bool_expr_truth_table"] == expected
+    assert report["symbolic_oracle_truth_table"] == expected
+    assert report["semantic_checks"] == {
+        "bool_expr_matches_symbolic_oracle": True,
+        "reversibility_check": True,
+        "complete_truth_table": True,
+    }
+    assert report["truth_table_entries"] == 2 ** len(variables)
+    assert report["oracle_metrics"]["logical_variables"] == len(variables)
+    assert report["oracle_metrics"]["cleanup_gate_count"] >= 1
+    assert report["oracle_metrics"]["depth_estimate"] == report["oracle_metrics"]["gate_count"]
+    assert report["qiskit_semantics"]["backend_execution"] is False
+    assert "exponential" in report["synthesis_limit"]
+    assert payload["credential_required"] is False
+    assert payload["truth_table"] == expected
+    assert payload["semantic_report"]["truth_table_hash"] == report["truth_table_hash"]
+
+
+def test_qiskit_semantics_report_summarizes_local_quantum_circuit(monkeypatch) -> None:
+    class LocalQuantumCircuit:
+        def __init__(self, num_qubits: int, *, name: str):
+            self.num_qubits = num_qubits
+            self.name = name
+            self.operations: list[tuple[str, tuple[object, ...]]] = []
+
+        def x(self, qubit: int) -> None:
+            self.operations.append(("x", (qubit,)))
+
+        def cx(self, control: int, target: int) -> None:
+            self.operations.append(("cx", (control, target)))
+
+        def mcx(self, controls: list[int], target: int) -> None:
+            self.operations.append(("mcx", (tuple(controls), target)))
+
+        def depth(self) -> int:
+            return len(self.operations)
+
+        def size(self) -> int:
+            return len(self.operations)
+
+    local_qiskit = SimpleNamespace(
+        __version__="local-test",
+        QuantumCircuit=LocalQuantumCircuit,
+    )
+    monkeypatch.setitem(sys.modules, "qiskit", local_qiskit)
+    expression = AND(BoolExpr.var("a"), BoolExpr.var("b"))
+    payload = export_bool_expr_to_qiskit(expression, name="and_policy")
+    summary = payload["qiskit_circuit_summary"]
+    assert payload["status"] == {"available": True, "qiskit": "local-test"}
+    assert summary["class"] == "qiskit.QuantumCircuit"
+    assert summary["name"] == "O_and_policy"
+    assert summary["num_qubits"] == 3
+    assert summary["truth_table_entries"] == 4
+    assert summary["true_rows"] == ["11"]
+    assert summary["synthesis"] == "exact_truth_table_multi_controlled_x"
+    assert payload["semantic_report"]["qiskit_semantics"]["status"] == (
+        "synthesized_from_verified_truth_table"
+    )
+    assert payload["semantic_report"]["qiskit_semantics"]["backend_execution"] is False