From 4969da18eff132dfd60560a61ef98b3c471efaf2 Mon Sep 17 00:00:00 2001 From: Mayckon Giovani Date: Wed, 16 Sep 2026 15:35:37 -0300 Subject: [PATCH] feat: add external solver replay artifacts --- README.md | 5 +- docs/dwave_mapping.md | 10 + docs/dwave_relevance.md | 5 +- docs/formal_certificates.md | 4 +- docs/limitations.md | 1 + docs/results/README.md | 3 +- docs/results/compiled_qubo_solution.json | 34 +- .../external_solver_replay_examples.json | 514 ++++++++++++++++++ docs/results/release_evidence_index.json | 6 +- docs/v0_2_roadmap.md | 2 +- examples/external_solver_replay.py | 144 +++++ python/noetheris/certificates/model.py | 65 +++ python/noetheris/qubo/__init__.py | 2 + python/noetheris/qubo/compiler.py | 320 +++++++++-- scripts/generate_release_results.py | 123 +++++ scripts/python_env.sh | 20 + scripts/run_all_python_tests.sh | 12 +- scripts/run_audit.sh | 34 +- scripts/run_benchmarks.sh | 10 +- scripts/run_examples.sh | 35 +- tests/test_certificates.py | 59 ++ tests/test_external_examples.py | 19 + tests/test_qubo.py | 75 +++ 23 files changed, 1416 insertions(+), 86 deletions(-) create mode 100644 docs/results/external_solver_replay_examples.json create mode 100644 examples/external_solver_replay.py create mode 100644 scripts/python_env.sh diff --git a/README.md b/README.md index 4384855..a0fea59 100644 --- a/README.md +++ b/README.md @@ -29,7 +29,7 @@ Noetheris does not claim quantum advantage, does not assess deployed cryptograph | --- | --- | | Structural IR validation and hashing | `tests/test_structural_ir.py`, `examples/structural_ir/*.json`, `docs/results/compiled_qubo_solution.json` | | QUBO/Ising energy preservation | `tests/test_qubo.py`, `examples/qubo_ising_qaoa.py`, `docs/results/qaoa_hamiltonian_report.json` | -| D-Wave/Ocean boundary | `tests/test_optional_integrations.py`, `tests/test_external_examples.py`, `examples/dwave_ocean_exchange.py`, `docs/results/compiled_qubo_solution.json`, `docs/dwave_mapping.md` | +| D-Wave/Ocean boundary | `tests/test_optional_integrations.py`, `tests/test_external_examples.py`, `examples/dwave_ocean_exchange.py`, `examples/external_solver_replay.py`, `docs/results/compiled_qubo_solution.json`, `docs/results/external_solver_replay_examples.json`, `docs/dwave_mapping.md` | | IBM/Qiskit oracle boundary | `tests/test_circuits.py`, `tests/test_optional_integrations.py`, `tests/test_external_examples.py`, `examples/qiskit_oracle_export.py`, `docs/results/oracle_truth_table.json` | | Certificate replay | `tests/test_certificates.py`, `examples/example_energy_certificate.json`, `docs/results/invariant_witness.json` | | CV/GKP diagnostics | `tests/test_cv.py`, `examples/cv_gkp_stabilizer_diagnostics.py`, `docs/results/cv_gkp_diagnostic_certificate.json` | @@ -81,6 +81,7 @@ python3 examples/threshold_policy_analysis.py python3 examples/certificate_validation.py python3 examples/qubo_ising_qaoa.py python3 examples/dwave_ocean_exchange.py +python3 examples/external_solver_replay.py python3 examples/qiskit_oracle_export.py python3 examples/saga_failure_semantics.py python3 examples/cv_fock_truncation_diagnostics.py @@ -142,7 +143,7 @@ The local compiler emits symbolic gates, truth tables, cost metrics, reversibili ## Certificates -Optimization and diagnostics emit deterministic certificate objects containing problem hashes, compiled model hashes where available, selected variables, witnesses, energy terms, satisfied and violated constraints, proof obligations, reproducibility metadata, and canonical fingerprints. Certificates fail closed: arithmetic mismatches, status inconsistencies, violated constraints, and nondeterministic timestamp strategies are rejected. +Optimization and diagnostics emit deterministic certificate objects containing problem hashes, compiled model hashes where available, selected variables, witnesses, energy terms, satisfied and violated constraints, proof obligations, reproducibility metadata, and canonical fingerprints. Certificates fail closed: arithmetic mismatches, status inconsistencies, violated constraints, nondeterministic timestamp strategies, and inconsistent external replay evidence are rejected. ## Benchmarks diff --git a/docs/dwave_mapping.md b/docs/dwave_mapping.md index d34b3af..72589cc 100644 --- a/docs/dwave_mapping.md +++ b/docs/dwave_mapping.md @@ -69,8 +69,18 @@ External solver samples are treated as untrusted witnesses. Replay must check: - solver metadata; - embedding metadata when a hardware or hybrid run supplies it. +The replay artifact schema is `noetheris.external_solver_replay.v1`. It records the candidate id, submitted and expected hashes, BINARY assignment domain, missing or unknown variables, reported energy, recomputed local energy, energy difference, tolerance, solver metadata, embedding metadata, rejection reasons, and an artifact hash. Accepted candidates have `status: "verified"` and an empty rejection list. Rejected candidates carry structured reason codes such as `problem_hash_mismatch`, `compiled_model_hash_mismatch`, `assignment_missing_variables`, `assignment_unknown_variables`, `reported_energy_mismatch`, `solver_metadata_malformed`, and `embedding_metadata_malformed`. + Local baselines use `embedding_status: "not_requested"` and `embedding: null`. Hardware embedding, chain strength, anneal parameters, chain-break fraction, solver topology, and sample provenance must come from an actual external run and are never inferred by Noetheris. +The deterministic replay example is: + +```bash +python3 examples/external_solver_replay.py +``` + +It emits one accepted candidate and multiple rejected candidates. The local replay artifact is the verification authority; solver metadata is recorded evidence supplied by the external tool, not a Noetheris assessment of embedding quality. + ## No Hardware Claim The repository runs without Ocean, D-Wave credentials, or paid APIs. The v0.1.0 benchmark artifacts are local replay baselines. They are not hardware comparisons and do not imply quantum speedup. diff --git a/docs/dwave_relevance.md b/docs/dwave_relevance.md index aa6349f..f2d53f0 100644 --- a/docs/dwave_relevance.md +++ b/docs/dwave_relevance.md @@ -20,7 +20,7 @@ Structural IR - Deterministic seeded annealing baseline for local experiments. - Structured D-Wave exchange payload with schema version and model hash. - Optional `dimod.BinaryQuadraticModel` construction when Ocean is installed. -- External-sample replay against `problem_hash`, `compiled_model_hash`, assignment variables, and reported energy. +- External-sample replay artifacts against `problem_hash`, `compiled_model_hash`, assignment variables, reported energy, solver metadata, and embedding metadata. ## What Is Deliberately Outside v0.1.0 @@ -31,7 +31,7 @@ Structural IR - Advantage or Advantage2 performance claims. - Hybrid solver benchmarking. -These fields are represented as explicit metadata boundaries. Local artifacts use `embedding_status: "not_requested"`. A future external run must supply solver id, topology, embedding, chain settings, anneal parameters, sample counts, and chain-break statistics before Noetheris can replay the sample as a documented external witness. +These fields are represented as explicit metadata boundaries. Local artifacts use `embedding_status: "not_requested"`. A future external run must supply solver id, topology, embedding, chain settings, anneal parameters, sample counts, and chain-break statistics before Noetheris can replay the sample as a documented external witness. Noetheris records that metadata but does not infer hardware embedding quality locally. ## Minimal Local Export @@ -64,6 +64,7 @@ result = replay_external_solution( compiled_model_hash=compiled_problem.compiled_model_hash, ) assert result["status"] == "verified" +assert result["verification_authority"] == "noetheris.local_replay" ``` The replay relation is the trust boundary: a solver result is useful only after local deterministic verification. diff --git a/docs/formal_certificates.md b/docs/formal_certificates.md index aa7df8e..391e312 100644 --- a/docs/formal_certificates.md +++ b/docs/formal_certificates.md @@ -27,7 +27,7 @@ Certificates include: ## Validation -Validation recomputes energy contributions, recomputes total energy, checks constraint polarity, rejects violated constraints for accepted certificates, checks optional problem hash, checks status consistency, and rejects nondeterministic timestamp strategies. +Validation recomputes energy contributions, recomputes total energy, checks constraint polarity, rejects violated constraints for accepted certificates, checks optional problem hash, checks status consistency, rejects nondeterministic timestamp strategies, and rejects inconsistent external replay evidence embedded in the energy breakdown. ## Replay @@ -38,6 +38,8 @@ python3 -m noetheris.certificates.replay examples/example_energy_certificate.jso Replay emits validation status and certificate fingerprint. Stronger model-specific replay is represented by compiled model hashes and strict QUBO energy evaluation in the compiler layer. +When a certificate includes `external_replay_artifact`, `external_replay`, `external_sample_replay`, or `external_solver_replay` in `energy_breakdown`, that artifact must use schema `noetheris.external_solver_replay.v1`, have `status: "verified"`, have local energy recomputation enabled, match the certificate problem hash, match the certificate compiled-model hash when present, carry no rejection reasons, and pass artifact-hash verification. Any violation rejects the certificate. + ## Formal Surface Lean models a simplified certificate-validity predicate and small true lemmas. The executable Python/Rust validators are the release enforcement path; Lean artifacts define reviewable kernels rather than whole-repository proofs. diff --git a/docs/limitations.md b/docs/limitations.md index e9106da..851a44c 100644 --- a/docs/limitations.md +++ b/docs/limitations.md @@ -9,6 +9,7 @@ Noetheris v0.1.0 is a bounded research kernel. Its boundaries are part of the sc - QUBO penalty calibration remains a modeling responsibility; weak penalties can encode the wrong preference order. - Circuit oracle compilation is limited to small Boolean predicates and symbolic reversible circuits. - Optional Qiskit and D-Wave adapters are export boundaries, not default hardware benchmark paths. +- External solver metadata and embedding metadata are recorded as supplied evidence. Noetheris verifies hashes, assignment domains, and energies locally; it does not infer hardware embedding quality. - CV/GKP diagnostics use finite Fock cutoffs. Boundary artifacts are measured and certified, not ignored. - Approximate GKP states in this release are finite-dimensional diagnostic objects, not production fault-tolerant logical states. - Lean and TLA+ artifacts cover simplified kernels and scenario models, not the entire implementation. diff --git a/docs/results/README.md b/docs/results/README.md index 287cadd..28884e2 100644 --- a/docs/results/README.md +++ b/docs/results/README.md @@ -12,6 +12,7 @@ python3 scripts/generate_release_results.py - `release_evidence_index.json`: index of generated evidence files. - `invariant_witness.json`: bounded consensus-safety counterexample witness with certificate data. - `compiled_qubo_solution.json`: Structural IR compilation, exact QUBO solution, energy breakdown, D-Wave exchange payload, and local replay of a solver sample. +- `external_solver_replay_examples.json`: accepted and rejected external-candidate replay artifacts with explicit hash, assignment-domain, energy, and metadata rejection reasons. - `pqc_migration_plan.json`: migration optimizer output, residual risk, dependency analysis, QUBO model, and certificate. - `oracle_truth_table.json`: Boolean predicate truth table, reversible compute/apply/uncompute metrics, and QASM-like text. - `qaoa_hamiltonian_report.json`: QUBO-to-Ising lowering and exact local QAOA p=1 statevector check. @@ -20,4 +21,4 @@ python3 scripts/generate_release_results.py ## Interpretation -These files are release evidence, not hardware benchmark claims. The D-Wave payload is a BINARY QUBO exchange representation; any external solver sample must be replayed locally before it is trusted. The Qiskit-facing oracle artifacts are small-predicate circuit mappings; they do not claim backend advantage. The CV/GKP certificate uses finite Fock truncation and records boundary effects explicitly. +These files are release evidence, not hardware benchmark claims. The D-Wave payload is a BINARY QUBO exchange representation; any external solver sample must be replayed locally before it is trusted. Solver and embedding metadata are recorded as externally supplied evidence; local replay does not infer hardware embedding quality. The Qiskit-facing oracle artifacts are small-predicate circuit mappings; they do not claim backend advantage. The CV/GKP certificate uses finite Fock truncation and records boundary effects explicitly. diff --git a/docs/results/compiled_qubo_solution.json b/docs/results/compiled_qubo_solution.json index 7c3149e..5447498 100644 --- a/docs/results/compiled_qubo_solution.json +++ b/docs/results/compiled_qubo_solution.json @@ -255,6 +255,7 @@ } }, "external_sample_replay": { + "artifact_hash": "sha256:d1888865d53521446dd39af85d8820ba966ce263e239c921edeeea4911dbecd8", "assignment": { "path_0": false, "path_1": false, @@ -262,21 +263,50 @@ "path_3": false, "path_4": true }, + "assignment_domain": { + "expected_variables": [ + "path_0", + "path_1", + "path_2", + "path_3", + "path_4" + ], + "invalid_value_variables": [], + "missing_variables": [], + "provided_variables": [ + "path_0", + "path_1", + "path_2", + "path_3", + "path_4" + ], + "unknown_variables": [], + "vartype": "BINARY" + }, + "candidate_id": "sha256:7cdf563bf9035bbbb198dfba8a6995386625014fa84bd49a2e16eae96ffa4c1e", "compiled_model_hash": "sha256:eca1158e2ddfdfe196775a49b8ffbcd46a23a33bf61e18e8229dcda0174612d2", "embedding_metadata": { "embedding": null, "embedding_status": "not_requested" }, "energy": 10.0, + "energy_difference": 0.0, "energy_recomputed": true, "problem_hash": "sha256:3cddd03a5881f3b71ba61c3b063f96ec47dba9f9160a634392929eca618d095f", "reasons": [], + "recomputed_energy": 10.0, + "rejection_reasons": [], "reported_energy": 10.0, - "solver_boundary": "external solver output is an untrusted witness until replay verifies it", + "schema": "noetheris.external_solver_replay.v1", + "solver_boundary": "external solver output is an untrusted witness until deterministic local replay verifies hashes, domain, and energy", "solver_metadata": { "source": "local_exact_solver" }, - "status": "verified" + "status": "verified", + "submitted_compiled_model_hash": "sha256:eca1158e2ddfdfe196775a49b8ffbcd46a23a33bf61e18e8229dcda0174612d2", + "submitted_problem_hash": "sha256:3cddd03a5881f3b71ba61c3b063f96ec47dba9f9160a634392929eca618d095f", + "tolerance": 1e-09, + "verification_authority": "noetheris.local_replay" }, "solution": { "assignment": { diff --git a/docs/results/external_solver_replay_examples.json b/docs/results/external_solver_replay_examples.json new file mode 100644 index 0000000..256c4cc --- /dev/null +++ b/docs/results/external_solver_replay_examples.json @@ -0,0 +1,514 @@ +{ + "accepted_candidate": { + "artifact_hash": "sha256:a150fed4fcc7d4bfcb798342c247a13ab8c11d4ad7bc5545f31921d6216ed146", + "assignment": { + "path_0": false, + "path_1": false, + "path_2": false, + "path_3": false, + "path_4": true + }, + "assignment_domain": { + "expected_variables": [ + "path_0", + "path_1", + "path_2", + "path_3", + "path_4" + ], + "invalid_value_variables": [], + "missing_variables": [], + "provided_variables": [ + "path_0", + "path_1", + "path_2", + "path_3", + "path_4" + ], + "unknown_variables": [], + "vartype": "BINARY" + }, + "candidate_id": "accepted-local-reference", + "compiled_model_hash": "sha256:eca1158e2ddfdfe196775a49b8ffbcd46a23a33bf61e18e8229dcda0174612d2", + "embedding_metadata": { + "embedding": null, + "embedding_status": "not_requested" + }, + "energy": 10.0, + "energy_difference": 0.0, + "energy_recomputed": true, + "problem_hash": "sha256:3cddd03a5881f3b71ba61c3b063f96ec47dba9f9160a634392929eca618d095f", + "reasons": [], + "recomputed_energy": 10.0, + "rejection_reasons": [], + "reported_energy": 10.0, + "schema": "noetheris.external_solver_replay.v1", + "solver_boundary": "external solver output is an untrusted witness until deterministic local replay verifies hashes, domain, and energy", + "solver_metadata": { + "credential_required": false, + "sample_source": "release_evidence", + "solver": "local_exact_reference" + }, + "status": "verified", + "submitted_compiled_model_hash": "sha256:eca1158e2ddfdfe196775a49b8ffbcd46a23a33bf61e18e8229dcda0174612d2", + "submitted_problem_hash": "sha256:3cddd03a5881f3b71ba61c3b063f96ec47dba9f9160a634392929eca618d095f", + "tolerance": 1e-09, + "verification_authority": "noetheris.local_replay" + }, + "credential_required": false, + "rejected_candidates": [ + { + "artifact": { + "artifact_hash": "sha256:6ee9ffc3ae4c9ac52aa1e05831420e30aa1849621915e5769d77ad0f494f3139", + "assignment": { + "path_0": false, + "path_1": false, + "path_2": false, + "path_3": false, + "path_4": true + }, + "assignment_domain": { + "expected_variables": [ + "path_0", + "path_1", + "path_2", + "path_3", + "path_4" + ], + "invalid_value_variables": [], + "missing_variables": [], + "provided_variables": [ + "path_0", + "path_1", + "path_2", + "path_3", + "path_4" + ], + "unknown_variables": [], + "vartype": "BINARY" + }, + "candidate_id": "rejected-problem-hash", + "compiled_model_hash": "sha256:eca1158e2ddfdfe196775a49b8ffbcd46a23a33bf61e18e8229dcda0174612d2", + "embedding_metadata": { + "embedding": null, + "embedding_status": "not_requested" + }, + "energy": 10.0, + "energy_difference": 0.0, + "energy_recomputed": true, + "problem_hash": "sha256:3cddd03a5881f3b71ba61c3b063f96ec47dba9f9160a634392929eca618d095f", + "reasons": [ + "submitted problem hash does not match compiled problem hash" + ], + "recomputed_energy": 10.0, + "rejection_reasons": [ + { + "code": "problem_hash_mismatch", + "detail": "submitted problem hash does not match compiled problem hash", + "evidence": { + "expected": "sha256:3cddd03a5881f3b71ba61c3b063f96ec47dba9f9160a634392929eca618d095f", + "submitted": "sha256:wrong-problem" + } + } + ], + "reported_energy": 10.0, + "schema": "noetheris.external_solver_replay.v1", + "solver_boundary": "external solver output is an untrusted witness until deterministic local replay verifies hashes, domain, and energy", + "solver_metadata": { + "source": "not_supplied" + }, + "status": "rejected", + "submitted_compiled_model_hash": "sha256:eca1158e2ddfdfe196775a49b8ffbcd46a23a33bf61e18e8229dcda0174612d2", + "submitted_problem_hash": "sha256:wrong-problem", + "tolerance": 1e-09, + "verification_authority": "noetheris.local_replay" + }, + "case": "problem_hash_mismatch", + "reason_codes": [ + "problem_hash_mismatch" + ], + "status": "rejected" + }, + { + "artifact": { + "artifact_hash": "sha256:b857656935896ec8fa0ca6fe9b79841beb8a3bcd9bcf7002c09a061d62806745", + "assignment": { + "path_0": false, + "path_1": false, + "path_2": false, + "path_3": false, + "path_4": true + }, + "assignment_domain": { + "expected_variables": [ + "path_0", + "path_1", + "path_2", + "path_3", + "path_4" + ], + "invalid_value_variables": [], + "missing_variables": [], + "provided_variables": [ + "path_0", + "path_1", + "path_2", + "path_3", + "path_4" + ], + "unknown_variables": [], + "vartype": "BINARY" + }, + "candidate_id": "rejected-compiled-model-hash", + "compiled_model_hash": "sha256:eca1158e2ddfdfe196775a49b8ffbcd46a23a33bf61e18e8229dcda0174612d2", + "embedding_metadata": { + "embedding": null, + "embedding_status": "not_requested" + }, + "energy": 10.0, + "energy_difference": 0.0, + "energy_recomputed": true, + "problem_hash": "sha256:3cddd03a5881f3b71ba61c3b063f96ec47dba9f9160a634392929eca618d095f", + "reasons": [ + "submitted compiled model hash does not match local compiled model hash" + ], + "recomputed_energy": 10.0, + "rejection_reasons": [ + { + "code": "compiled_model_hash_mismatch", + "detail": "submitted compiled model hash does not match local compiled model hash", + "evidence": { + "expected": "sha256:eca1158e2ddfdfe196775a49b8ffbcd46a23a33bf61e18e8229dcda0174612d2", + "submitted": "sha256:wrong-compiled-model" + } + } + ], + "reported_energy": 10.0, + "schema": "noetheris.external_solver_replay.v1", + "solver_boundary": "external solver output is an untrusted witness until deterministic local replay verifies hashes, domain, and energy", + "solver_metadata": { + "source": "not_supplied" + }, + "status": "rejected", + "submitted_compiled_model_hash": "sha256:wrong-compiled-model", + "submitted_problem_hash": "sha256:3cddd03a5881f3b71ba61c3b063f96ec47dba9f9160a634392929eca618d095f", + "tolerance": 1e-09, + "verification_authority": "noetheris.local_replay" + }, + "case": "compiled_model_hash_mismatch", + "reason_codes": [ + "compiled_model_hash_mismatch" + ], + "status": "rejected" + }, + { + "artifact": { + "artifact_hash": "sha256:e1deb8b6757e13c6fe5a2ee5a9d606e575c2008602cc234ce1f0e838f1f72b03", + "assignment": { + "path_1": false, + "path_2": false, + "path_3": false, + "path_4": true + }, + "assignment_domain": { + "expected_variables": [ + "path_0", + "path_1", + "path_2", + "path_3", + "path_4" + ], + "invalid_value_variables": [], + "missing_variables": [ + "path_0" + ], + "provided_variables": [ + "path_1", + "path_2", + "path_3", + "path_4" + ], + "unknown_variables": [], + "vartype": "BINARY" + }, + "candidate_id": "rejected-missing-variable", + "compiled_model_hash": "sha256:eca1158e2ddfdfe196775a49b8ffbcd46a23a33bf61e18e8229dcda0174612d2", + "embedding_metadata": { + "embedding": null, + "embedding_status": "not_requested" + }, + "energy": null, + "energy_difference": null, + "energy_recomputed": false, + "problem_hash": "sha256:3cddd03a5881f3b71ba61c3b063f96ec47dba9f9160a634392929eca618d095f", + "reasons": [ + "candidate assignment does not cover the compiled model domain" + ], + "recomputed_energy": null, + "rejection_reasons": [ + { + "code": "assignment_missing_variables", + "detail": "candidate assignment does not cover the compiled model domain", + "evidence": { + "variables": [ + "path_0" + ] + } + } + ], + "reported_energy": 10.0, + "schema": "noetheris.external_solver_replay.v1", + "solver_boundary": "external solver output is an untrusted witness until deterministic local replay verifies hashes, domain, and energy", + "solver_metadata": { + "source": "not_supplied" + }, + "status": "rejected", + "submitted_compiled_model_hash": "sha256:eca1158e2ddfdfe196775a49b8ffbcd46a23a33bf61e18e8229dcda0174612d2", + "submitted_problem_hash": "sha256:3cddd03a5881f3b71ba61c3b063f96ec47dba9f9160a634392929eca618d095f", + "tolerance": 1e-09, + "verification_authority": "noetheris.local_replay" + }, + "case": "missing_variables", + "reason_codes": [ + "assignment_missing_variables" + ], + "status": "rejected" + }, + { + "artifact": { + "artifact_hash": "sha256:19b042d758bf48263f49968488b31e5e3e6c6e64084070e8e04b3d900ce7952d", + "assignment": { + "outside_compiled_domain": true, + "path_0": false, + "path_1": false, + "path_2": false, + "path_3": false, + "path_4": true + }, + "assignment_domain": { + "expected_variables": [ + "path_0", + "path_1", + "path_2", + "path_3", + "path_4" + ], + "invalid_value_variables": [], + "missing_variables": [], + "provided_variables": [ + "outside_compiled_domain", + "path_0", + "path_1", + "path_2", + "path_3", + "path_4" + ], + "unknown_variables": [ + "outside_compiled_domain" + ], + "vartype": "BINARY" + }, + "candidate_id": "rejected-unknown-variable", + "compiled_model_hash": "sha256:eca1158e2ddfdfe196775a49b8ffbcd46a23a33bf61e18e8229dcda0174612d2", + "embedding_metadata": { + "embedding": null, + "embedding_status": "not_requested" + }, + "energy": null, + "energy_difference": null, + "energy_recomputed": false, + "problem_hash": "sha256:3cddd03a5881f3b71ba61c3b063f96ec47dba9f9160a634392929eca618d095f", + "reasons": [ + "candidate assignment contains variables outside the compiled model domain" + ], + "recomputed_energy": null, + "rejection_reasons": [ + { + "code": "assignment_unknown_variables", + "detail": "candidate assignment contains variables outside the compiled model domain", + "evidence": { + "variables": [ + "outside_compiled_domain" + ] + } + } + ], + "reported_energy": 10.0, + "schema": "noetheris.external_solver_replay.v1", + "solver_boundary": "external solver output is an untrusted witness until deterministic local replay verifies hashes, domain, and energy", + "solver_metadata": { + "source": "not_supplied" + }, + "status": "rejected", + "submitted_compiled_model_hash": "sha256:eca1158e2ddfdfe196775a49b8ffbcd46a23a33bf61e18e8229dcda0174612d2", + "submitted_problem_hash": "sha256:3cddd03a5881f3b71ba61c3b063f96ec47dba9f9160a634392929eca618d095f", + "tolerance": 1e-09, + "verification_authority": "noetheris.local_replay" + }, + "case": "unknown_variables", + "reason_codes": [ + "assignment_unknown_variables" + ], + "status": "rejected" + }, + { + "artifact": { + "artifact_hash": "sha256:46ca4d4a54ac905369c6982510846e73ae4ea3ae7c2d1b91680cbd70966f74fd", + "assignment": { + "path_0": false, + "path_1": false, + "path_2": false, + "path_3": false, + "path_4": true + }, + "assignment_domain": { + "expected_variables": [ + "path_0", + "path_1", + "path_2", + "path_3", + "path_4" + ], + "invalid_value_variables": [], + "missing_variables": [], + "provided_variables": [ + "path_0", + "path_1", + "path_2", + "path_3", + "path_4" + ], + "unknown_variables": [], + "vartype": "BINARY" + }, + "candidate_id": "rejected-energy-mismatch", + "compiled_model_hash": "sha256:eca1158e2ddfdfe196775a49b8ffbcd46a23a33bf61e18e8229dcda0174612d2", + "embedding_metadata": { + "embedding": null, + "embedding_status": "not_requested" + }, + "energy": 10.0, + "energy_difference": 1.0, + "energy_recomputed": true, + "problem_hash": "sha256:3cddd03a5881f3b71ba61c3b063f96ec47dba9f9160a634392929eca618d095f", + "reasons": [ + "reported energy does not match deterministic local replay energy" + ], + "recomputed_energy": 10.0, + "rejection_reasons": [ + { + "code": "reported_energy_mismatch", + "detail": "reported energy does not match deterministic local replay energy", + "evidence": { + "difference": 1.0, + "recomputed_energy": 10.0, + "reported_energy": 11.0, + "tolerance": 1e-09 + } + } + ], + "reported_energy": 11.0, + "schema": "noetheris.external_solver_replay.v1", + "solver_boundary": "external solver output is an untrusted witness until deterministic local replay verifies hashes, domain, and energy", + "solver_metadata": { + "source": "not_supplied" + }, + "status": "rejected", + "submitted_compiled_model_hash": "sha256:eca1158e2ddfdfe196775a49b8ffbcd46a23a33bf61e18e8229dcda0174612d2", + "submitted_problem_hash": "sha256:3cddd03a5881f3b71ba61c3b063f96ec47dba9f9160a634392929eca618d095f", + "tolerance": 1e-09, + "verification_authority": "noetheris.local_replay" + }, + "case": "energy_mismatch", + "reason_codes": [ + "reported_energy_mismatch" + ], + "status": "rejected" + }, + { + "artifact": { + "artifact_hash": "sha256:580c8edbb75ab04fda360a534dfbb575b7628a67348864bcde08e5d713e76b05", + "assignment": { + "path_0": false, + "path_1": false, + "path_2": false, + "path_3": false, + "path_4": true + }, + "assignment_domain": { + "expected_variables": [ + "path_0", + "path_1", + "path_2", + "path_3", + "path_4" + ], + "invalid_value_variables": [], + "missing_variables": [], + "provided_variables": [ + "path_0", + "path_1", + "path_2", + "path_3", + "path_4" + ], + "unknown_variables": [], + "vartype": "BINARY" + }, + "candidate_id": "rejected-malformed-metadata", + "compiled_model_hash": "sha256:eca1158e2ddfdfe196775a49b8ffbcd46a23a33bf61e18e8229dcda0174612d2", + "embedding_metadata": { + "accepted": false, + "provided": true, + "submitted_type": "str" + }, + "energy": 10.0, + "energy_difference": 0.0, + "energy_recomputed": true, + "problem_hash": "sha256:3cddd03a5881f3b71ba61c3b063f96ec47dba9f9160a634392929eca618d095f", + "reasons": [ + "solver metadata must be a JSON-compatible mapping", + "embedding metadata must be a JSON-compatible mapping" + ], + "recomputed_energy": 10.0, + "rejection_reasons": [ + { + "code": "solver_metadata_malformed", + "detail": "solver metadata must be a JSON-compatible mapping", + "evidence": { + "submitted_type": "str" + } + }, + { + "code": "embedding_metadata_malformed", + "detail": "embedding metadata must be a JSON-compatible mapping", + "evidence": { + "submitted_type": "str" + } + } + ], + "reported_energy": 10.0, + "schema": "noetheris.external_solver_replay.v1", + "solver_boundary": "external solver output is an untrusted witness until deterministic local replay verifies hashes, domain, and energy", + "solver_metadata": { + "accepted": false, + "provided": true, + "submitted_type": "str" + }, + "status": "rejected", + "submitted_compiled_model_hash": "sha256:eca1158e2ddfdfe196775a49b8ffbcd46a23a33bf61e18e8229dcda0174612d2", + "submitted_problem_hash": "sha256:3cddd03a5881f3b71ba61c3b063f96ec47dba9f9160a634392929eca618d095f", + "tolerance": 1e-09, + "verification_authority": "noetheris.local_replay" + }, + "case": "malformed_metadata", + "reason_codes": [ + "solver_metadata_malformed", + "embedding_metadata_malformed" + ], + "status": "rejected" + } + ], + "schema": "noetheris.external_solver_replay.examples.v1", + "verification_authority": "noetheris.local_replay" +} diff --git a/docs/results/release_evidence_index.json b/docs/results/release_evidence_index.json index 2a44809..f53ed23 100644 --- a/docs/results/release_evidence_index.json +++ b/docs/results/release_evidence_index.json @@ -5,9 +5,13 @@ "file": "docs/results/invariant_witness.json" }, { - "bytes": 6426, + "bytes": 7516, "file": "docs/results/compiled_qubo_solution.json" }, + { + "bytes": 17838, + "file": "docs/results/external_solver_replay_examples.json" + }, { "bytes": 6529, "file": "docs/results/pqc_migration_plan.json" diff --git a/docs/v0_2_roadmap.md b/docs/v0_2_roadmap.md index 38d2b84..94ddd94 100644 --- a/docs/v0_2_roadmap.md +++ b/docs/v0_2_roadmap.md @@ -20,7 +20,7 @@ The purpose is to make the handoff between Noetheris and optional solver ecosyst 4. External witness replay - Treat solver output as an untrusted witness. Replay must verify the problem hash, compiled model hash, assignment domain, reported energy, and solver metadata. + Treat solver output as an untrusted witness. Replay must verify the problem hash, compiled model hash, assignment domain, reported energy, solver metadata, and embedding metadata. Accepted and rejected candidates use schema `noetheris.external_solver_replay.v1` with structured rejection reasons and artifact hashes. 5. Documentation diff --git a/examples/external_solver_replay.py b/examples/external_solver_replay.py new file mode 100644 index 0000000..2edf08a --- /dev/null +++ b/examples/external_solver_replay.py @@ -0,0 +1,144 @@ +from __future__ import annotations + +import json +from pathlib import Path +import sys +from typing import Any + +ROOT = Path(__file__).resolve().parents[1] +sys.path.insert(0, str(ROOT / "python")) + +from noetheris.ir import StructuralSystem +from noetheris.qubo import external_solver_replay_artifact, compile_system, solve_exact + + +def main() -> None: + system = StructuralSystem.from_json_file( + ROOT / "examples" / "structural_ir" / "consensus_safety_ir.json" + ) + compiled = compile_system(system, system.problem_type) + solution = solve_exact(compiled) + assignment = dict(solution.assignment) + first_variable = compiled.model.variables[0] + + accepted = external_solver_replay_artifact( + compiled, + assignment, + reported_energy=solution.energy, + problem_hash=compiled.problem_hash, + compiled_model_hash=compiled.compiled_model_hash, + solver_metadata={ + "solver": "local_exact_reference", + "credential_required": False, + "sample_source": "deterministic_example", + }, + embedding_metadata={ + "embedding_status": "not_requested", + "embedding": None, + }, + candidate_id="accepted-local-reference", + ) + rejected = [ + _case( + "problem_hash_mismatch", + external_solver_replay_artifact( + compiled, + assignment, + reported_energy=solution.energy, + problem_hash="sha256:wrong-problem", + compiled_model_hash=compiled.compiled_model_hash, + candidate_id="rejected-problem-hash", + ), + ), + _case( + "compiled_model_hash_mismatch", + external_solver_replay_artifact( + compiled, + assignment, + reported_energy=solution.energy, + problem_hash=compiled.problem_hash, + compiled_model_hash="sha256:wrong-compiled-model", + candidate_id="rejected-compiled-model-hash", + ), + ), + _case( + "missing_variables", + external_solver_replay_artifact( + compiled, + { + variable: value + for variable, value in assignment.items() + if variable != first_variable + }, + reported_energy=solution.energy, + problem_hash=compiled.problem_hash, + compiled_model_hash=compiled.compiled_model_hash, + candidate_id="rejected-missing-variable", + ), + ), + _case( + "unknown_variables", + external_solver_replay_artifact( + compiled, + {**assignment, "outside_compiled_domain": True}, + reported_energy=solution.energy, + problem_hash=compiled.problem_hash, + compiled_model_hash=compiled.compiled_model_hash, + candidate_id="rejected-unknown-variable", + ), + ), + _case( + "energy_mismatch", + external_solver_replay_artifact( + compiled, + assignment, + reported_energy=solution.energy + 1.0, + problem_hash=compiled.problem_hash, + compiled_model_hash=compiled.compiled_model_hash, + candidate_id="rejected-energy-mismatch", + ), + ), + _case( + "malformed_metadata", + external_solver_replay_artifact( + compiled, + assignment, + reported_energy=solution.energy, + problem_hash=compiled.problem_hash, + compiled_model_hash=compiled.compiled_model_hash, + solver_metadata="not-a-mapping", # type: ignore[arg-type] + embedding_metadata="not-a-mapping", # type: ignore[arg-type] + candidate_id="rejected-malformed-metadata", + ), + ), + ] + print( + json.dumps( + { + "example": "external_solver_replay", + "problem_hash": compiled.problem_hash, + "compiled_model_hash": compiled.compiled_model_hash, + "credential_required": False, + "verification_authority": "noetheris.local_replay", + "accepted_candidate": accepted, + "rejected_candidates": rejected, + }, + indent=2, + sort_keys=True, + ) + ) + + +def _case(name: str, artifact: dict[str, Any]) -> dict[str, Any]: + return { + "case": name, + "status": artifact["status"], + "reason_codes": [ + reason["code"] for reason in artifact["rejection_reasons"] + ], + "artifact": artifact, + } + + +if __name__ == "__main__": + main() diff --git a/python/noetheris/certificates/model.py b/python/noetheris/certificates/model.py index 12b4b21..c70a03b 100644 --- a/python/noetheris/certificates/model.py +++ b/python/noetheris/certificates/model.py @@ -1,5 +1,6 @@ from __future__ import annotations +from collections.abc import Mapping as RuntimeMapping from dataclasses import dataclass, field import hashlib import json @@ -268,6 +269,7 @@ def validate_certificate( if constraint.satisfied: reasons.append(f"violated constraint {constraint.name} is marked true") reasons.append(f"constraint {constraint.name} is violated") + _validate_external_replay_evidence(cert, reasons, tolerance) derived_status = "verified" if not reasons else "rejected" if cert.verification_status != derived_status: reasons.append("declared verification status is inconsistent") @@ -288,3 +290,66 @@ def certificate_fingerprint(certificate: EnergyCertificate | Mapping[str, Any]) else certificate ) return stable_problem_hash(cert.to_dict()) + + +def _validate_external_replay_evidence( + cert: EnergyCertificate, + reasons: list[str], + tolerance: float, +) -> None: + for key in ( + "external_replay", + "external_replay_artifact", + "external_sample_replay", + "external_solver_replay", + ): + if key not in cert.energy_breakdown: + continue + evidence = cert.energy_breakdown[key] + if not isinstance(evidence, RuntimeMapping): + reasons.append(f"{key} evidence is malformed") + continue + if evidence.get("schema") != "noetheris.external_solver_replay.v1": + reasons.append(f"{key} schema is not recognized") + if evidence.get("status") != "verified": + reasons.append(f"{key} evidence is not verified") + if evidence.get("energy_recomputed") is not True: + reasons.append(f"{key} energy was not recomputed") + if evidence.get("problem_hash") != cert.problem_hash: + reasons.append(f"{key} problem hash mismatch") + if ( + cert.compiled_model_hash is not None + and evidence.get("compiled_model_hash") != cert.compiled_model_hash + ): + reasons.append(f"{key} compiled model hash mismatch") + if evidence.get("rejection_reasons"): + reasons.append(f"{key} contains rejection reasons") + assignment_domain = evidence.get("assignment_domain") + if not isinstance(assignment_domain, RuntimeMapping): + reasons.append(f"{key} assignment domain is malformed") + else: + if assignment_domain.get("missing_variables"): + reasons.append(f"{key} assignment domain has missing variables") + if assignment_domain.get("unknown_variables"): + reasons.append(f"{key} assignment domain has unknown variables") + if assignment_domain.get("invalid_value_variables"): + reasons.append(f"{key} assignment domain has invalid values") + for metadata_key in ("solver_metadata", "embedding_metadata"): + if not isinstance(evidence.get(metadata_key), RuntimeMapping): + reasons.append(f"{key} {metadata_key} is malformed") + reported = evidence.get("reported_energy") + recomputed = evidence.get("recomputed_energy") + try: + if reported is not None and recomputed is not None: + if abs(float(reported) - float(recomputed)) > tolerance: + reasons.append(f"{key} replay energy mismatch") + except (TypeError, ValueError): + reasons.append(f"{key} replay energy is malformed") + artifact_hash = evidence.get("artifact_hash") + if not isinstance(artifact_hash, str): + reasons.append(f"{key} artifact hash is missing") + continue + canonical = dict(evidence) + canonical.pop("artifact_hash", None) + if stable_problem_hash(canonical) != artifact_hash: + reasons.append(f"{key} artifact hash mismatch") diff --git a/python/noetheris/qubo/__init__.py b/python/noetheris/qubo/__init__.py index 9906480..b19bd6f 100644 --- a/python/noetheris/qubo/__init__.py +++ b/python/noetheris/qubo/__init__.py @@ -16,6 +16,7 @@ energy_breakdown, evaluate_energy, explain_solution, + external_solver_replay_artifact, replay_external_solution, solve_exact, solve_simulated_annealing, @@ -37,6 +38,7 @@ "energy_breakdown", "evaluate_energy", "explain_solution", + "external_solver_replay_artifact", "replay_external_solution", "solve_exact", "solve_simulated_annealing", diff --git a/python/noetheris/qubo/compiler.py b/python/noetheris/qubo/compiler.py index c2326b7..cc140fb 100644 --- a/python/noetheris/qubo/compiler.py +++ b/python/noetheris/qubo/compiler.py @@ -1,9 +1,10 @@ from __future__ import annotations +from collections.abc import Mapping from dataclasses import dataclass, field import math import random -from typing import Any, Mapping +from typing import Any from noetheris.certificates import stable_problem_hash from noetheris.ir import StructuralSystem @@ -267,50 +268,233 @@ def replay_external_solution( embedding_metadata: Mapping[str, Any] | None = None, tolerance: float = 1e-9, ) -> dict[str, Any]: - reasons: list[str] = [] - if problem_hash is not None and problem_hash != compiled.problem_hash: - reasons.append("problem hash mismatch") - if compiled_model_hash is not None and compiled_model_hash != compiled.compiled_model_hash: - reasons.append("compiled model hash mismatch") - try: - normalized_assignment = { - name: bool(value) for name, value in assignment.items() - } - energy = compiled.model.evaluate(normalized_assignment) - except ValueError as exc: - return { - "status": "rejected", - "reasons": [str(exc)], - "solver_metadata": _jsonable(dict(solver_metadata or {})), - "embedding_metadata": _jsonable(dict(embedding_metadata or {})), - } - if reported_energy is not None and abs(float(reported_energy) - energy) > tolerance: - reasons.append("reported energy mismatch") + return external_solver_replay_artifact( + compiled, + assignment, + reported_energy=reported_energy, + problem_hash=problem_hash, + compiled_model_hash=compiled_model_hash, + solver_metadata=solver_metadata, + embedding_metadata=embedding_metadata, + tolerance=tolerance, + ) + + +def external_solver_replay_artifact( + compiled: CompiledProblem, + assignment: Mapping[str, bool | int], + *, + reported_energy: float | int | None = None, + problem_hash: str | None = None, + compiled_model_hash: str | None = None, + solver_metadata: Mapping[str, Any] | None = None, + embedding_metadata: Mapping[str, Any] | None = None, + candidate_id: str | None = None, + tolerance: float = 1e-9, +) -> dict[str, Any]: + reasons: list[dict[str, Any]] = [] + supplied_problem_hash = ( + compiled.problem_hash if problem_hash is None else str(problem_hash) + ) + supplied_compiled_hash = ( + compiled.compiled_model_hash + if compiled_model_hash is None + else str(compiled_model_hash) + ) + if supplied_problem_hash != compiled.problem_hash: + reasons.append( + _replay_reason( + "problem_hash_mismatch", + "submitted problem hash does not match compiled problem hash", + {"submitted": supplied_problem_hash, "expected": compiled.problem_hash}, + ) + ) + if supplied_compiled_hash != compiled.compiled_model_hash: + reasons.append( + _replay_reason( + "compiled_model_hash_mismatch", + "submitted compiled model hash does not match local compiled model hash", + { + "submitted": supplied_compiled_hash, + "expected": compiled.compiled_model_hash, + }, + ) + ) + + solver_metadata_json = _metadata_payload( + solver_metadata, + default={"source": "not_supplied"}, + code="solver_metadata_malformed", + detail="solver metadata must be a JSON-compatible mapping", + reasons=reasons, + ) + embedding_metadata_json = _metadata_payload( + embedding_metadata, + default={"embedding_status": "not_requested", "embedding": None}, + code="embedding_metadata_malformed", + detail="embedding metadata must be a JSON-compatible mapping", + reasons=reasons, + ) + + expected_variables = list(compiled.model.variables) + assignment_is_mapping = isinstance(assignment, Mapping) + raw_assignment = ( + _jsonable(dict(assignment)) + if assignment_is_mapping + else _jsonable(assignment) + ) + provided_variables = ( + sorted(str(name) for name in assignment.keys()) if assignment_is_mapping else [] + ) + missing = sorted(set(expected_variables) - set(provided_variables)) + unknown = sorted(set(provided_variables) - set(expected_variables)) + invalid_values: list[str] = [] + normalized_assignment: dict[str, bool] = {} + if not assignment_is_mapping: + reasons.append( + _replay_reason( + "assignment_malformed", + "candidate assignment must be a mapping from variables to binary values", + {"submitted_type": type(assignment).__name__}, + ) + ) + else: + for variable, value in assignment.items(): + variable_name = str(variable) + if variable_name in compiled.model.variables: + normalized = _binary_assignment_value(value) + if normalized is None: + invalid_values.append(variable_name) + else: + normalized_assignment[variable_name] = normalized + if missing: + reasons.append( + _replay_reason( + "assignment_missing_variables", + "candidate assignment does not cover the compiled model domain", + {"variables": missing}, + ) + ) + if unknown: + reasons.append( + _replay_reason( + "assignment_unknown_variables", + "candidate assignment contains variables outside the compiled model domain", + {"variables": unknown}, + ) + ) + if invalid_values: + reasons.append( + _replay_reason( + "assignment_value_malformed", + "candidate assignment contains non-binary values", + {"variables": sorted(invalid_values)}, + ) + ) + + reported_energy_value: float | None = None + if reported_energy is None: + reasons.append( + _replay_reason( + "reported_energy_missing", + "external candidates must include a reported energy for replay binding", + ) + ) + else: + try: + reported_energy_value = float(reported_energy) + except (TypeError, ValueError): + reasons.append( + _replay_reason( + "reported_energy_malformed", + "reported energy must be numeric", + {"submitted": _jsonable(reported_energy)}, + ) + ) + + energy: float | None = None + domain_matches = ( + assignment_is_mapping + and not missing + and not unknown + and not invalid_values + ) + if domain_matches: + energy = compiled.model.evaluate( + {variable: normalized_assignment[variable] for variable in expected_variables} + ) + if ( + energy is not None + and reported_energy_value is not None + and abs(reported_energy_value - energy) > tolerance + ): + reasons.append( + _replay_reason( + "reported_energy_mismatch", + "reported energy does not match deterministic local replay energy", + { + "reported_energy": reported_energy_value, + "recomputed_energy": energy, + "difference": reported_energy_value - energy, + "tolerance": tolerance, + }, + ) + ) + status = "verified" if not reasons else "rejected" - return { + candidate_evidence = { + "problem_hash": supplied_problem_hash, + "compiled_model_hash": supplied_compiled_hash, + "assignment": raw_assignment, + "reported_energy": reported_energy_value, + "solver_metadata": solver_metadata_json, + "embedding_metadata": embedding_metadata_json, + } + replay_candidate_id = candidate_id or stable_problem_hash(candidate_evidence) + ordered_assignment = ( + {variable: normalized_assignment[variable] for variable in expected_variables} + if domain_matches + else raw_assignment + ) + payload: dict[str, Any] = { + "schema": "noetheris.external_solver_replay.v1", + "candidate_id": replay_candidate_id, "status": status, - "reasons": reasons, "problem_hash": compiled.problem_hash, + "submitted_problem_hash": supplied_problem_hash, "compiled_model_hash": compiled.compiled_model_hash, - "assignment": { - variable: normalized_assignment[variable] - for variable in compiled.model.variables + "submitted_compiled_model_hash": supplied_compiled_hash, + "assignment_domain": { + "vartype": "BINARY", + "expected_variables": expected_variables, + "provided_variables": provided_variables, + "missing_variables": missing, + "unknown_variables": unknown, + "invalid_value_variables": sorted(invalid_values), }, + "assignment": ordered_assignment, + "reported_energy": reported_energy_value, + "recomputed_energy": energy, "energy": energy, - "reported_energy": reported_energy, - "energy_recomputed": status == "verified", - "solver_boundary": "external solver output is an untrusted witness until replay verifies it", - "solver_metadata": _jsonable(dict(solver_metadata or {})), - "embedding_metadata": _jsonable( - dict( - embedding_metadata - or { - "embedding_status": "not_requested", - "embedding": None, - } - ) + "energy_difference": ( + reported_energy_value - energy + if reported_energy_value is not None and energy is not None + else None + ), + "energy_recomputed": energy is not None, + "tolerance": tolerance, + "rejection_reasons": reasons, + "reasons": [reason["detail"] for reason in reasons], + "solver_boundary": ( + "external solver output is an untrusted witness until deterministic " + "local replay verifies hashes, domain, and energy" ), + "verification_authority": "noetheris.local_replay", + "solver_metadata": solver_metadata_json, + "embedding_metadata": embedding_metadata_json, } + return _with_artifact_hash(payload) + def compile_system(system: StructuralSystem, problem: str) -> CompiledProblem: if problem == "invariant": @@ -391,6 +575,64 @@ def _jsonable(value: Any) -> Any: return {str(k): _jsonable(v) for k, v in value.items()} if isinstance(value, (list, tuple)): return [_jsonable(item) for item in value] + if isinstance(value, (str, int, float, bool)) or value is None: + return value if hasattr(value, "to_dict"): - return value.to_dict() - return value + return _jsonable(value.to_dict()) + return str(value) + + +def _metadata_payload( + value: Mapping[str, Any] | None, + *, + default: Mapping[str, Any], + code: str, + detail: str, + reasons: list[dict[str, Any]], +) -> dict[str, Any]: + if value is None: + return _jsonable(dict(default)) + if not isinstance(value, Mapping): + reasons.append( + _replay_reason( + code, + detail, + {"submitted_type": type(value).__name__}, + ) + ) + return { + "provided": True, + "accepted": False, + "submitted_type": type(value).__name__, + } + return _jsonable(dict(value)) + + +def _binary_assignment_value(value: Any) -> bool | None: + if isinstance(value, bool): + return value + try: + if value == 0: + return False + if value == 1: + return True + except Exception: + return None + return None + + +def _replay_reason( + code: str, + detail: str, + evidence: Mapping[str, Any] | None = None, +) -> dict[str, Any]: + reason: dict[str, Any] = {"code": code, "detail": detail} + if evidence is not None: + reason["evidence"] = _jsonable(dict(evidence)) + return reason + + +def _with_artifact_hash(payload: Mapping[str, Any]) -> dict[str, Any]: + artifact = dict(payload) + artifact["artifact_hash"] = stable_problem_hash(artifact) + return artifact diff --git a/scripts/generate_release_results.py b/scripts/generate_release_results.py index 0dd7589..2281c35 100644 --- a/scripts/generate_release_results.py +++ b/scripts/generate_release_results.py @@ -20,6 +20,7 @@ from noetheris.qubo import ( compile_system, explain_solution, + external_solver_replay_artifact, replay_external_solution, solve_exact, ) @@ -62,6 +63,11 @@ def main() -> None: }, artifacts, ) + _write( + "external_solver_replay_examples.json", + _external_replay_examples(compiled, solution.assignment, solution.energy), + artifacts, + ) migration_graph = MigrationGraph.from_json_file(ROOT / "examples" / "pqc_migration_graph.json") migration = optimize_migration_plan(migration_graph, seed=2026) @@ -127,5 +133,122 @@ def _write(name: str, payload: dict[str, Any], artifacts: list[dict[str, Any]]) ) +def _external_replay_examples( + compiled: Any, + assignment: dict[str, bool], + energy: float, +) -> dict[str, Any]: + first_variable = compiled.model.variables[0] + accepted = external_solver_replay_artifact( + compiled, + assignment, + reported_energy=energy, + problem_hash=compiled.problem_hash, + compiled_model_hash=compiled.compiled_model_hash, + solver_metadata={ + "solver": "local_exact_reference", + "credential_required": False, + "sample_source": "release_evidence", + }, + embedding_metadata={ + "embedding_status": "not_requested", + "embedding": None, + }, + candidate_id="accepted-local-reference", + ) + rejected = [ + _replay_case( + "problem_hash_mismatch", + external_solver_replay_artifact( + compiled, + assignment, + reported_energy=energy, + problem_hash="sha256:wrong-problem", + compiled_model_hash=compiled.compiled_model_hash, + candidate_id="rejected-problem-hash", + ), + ), + _replay_case( + "compiled_model_hash_mismatch", + external_solver_replay_artifact( + compiled, + assignment, + reported_energy=energy, + problem_hash=compiled.problem_hash, + compiled_model_hash="sha256:wrong-compiled-model", + candidate_id="rejected-compiled-model-hash", + ), + ), + _replay_case( + "missing_variables", + external_solver_replay_artifact( + compiled, + { + variable: value + for variable, value in assignment.items() + if variable != first_variable + }, + reported_energy=energy, + problem_hash=compiled.problem_hash, + compiled_model_hash=compiled.compiled_model_hash, + candidate_id="rejected-missing-variable", + ), + ), + _replay_case( + "unknown_variables", + external_solver_replay_artifact( + compiled, + {**assignment, "outside_compiled_domain": True}, + reported_energy=energy, + problem_hash=compiled.problem_hash, + compiled_model_hash=compiled.compiled_model_hash, + candidate_id="rejected-unknown-variable", + ), + ), + _replay_case( + "energy_mismatch", + external_solver_replay_artifact( + compiled, + assignment, + reported_energy=energy + 1.0, + problem_hash=compiled.problem_hash, + compiled_model_hash=compiled.compiled_model_hash, + candidate_id="rejected-energy-mismatch", + ), + ), + _replay_case( + "malformed_metadata", + external_solver_replay_artifact( + compiled, + assignment, + reported_energy=energy, + problem_hash=compiled.problem_hash, + compiled_model_hash=compiled.compiled_model_hash, + solver_metadata="not-a-mapping", # type: ignore[arg-type] + embedding_metadata="not-a-mapping", # type: ignore[arg-type] + candidate_id="rejected-malformed-metadata", + ), + ), + ] + return { + "schema": "noetheris.external_solver_replay.examples.v1", + "credential_required": False, + "verification_authority": "noetheris.local_replay", + "accepted_candidate": accepted, + "rejected_candidates": rejected, + } + + +def _replay_case(name: str, artifact: dict[str, Any]) -> dict[str, Any]: + return { + "case": name, + "status": artifact["status"], + "reason_codes": [ + reason["code"] for reason in artifact["rejection_reasons"] + ], + "artifact": artifact, + } + + if __name__ == "__main__": main() diff --git a/scripts/python_env.sh b/scripts/python_env.sh new file mode 100644 index 0000000..8a1e9b1 --- /dev/null +++ b/scripts/python_env.sh @@ -0,0 +1,20 @@ +#!/usr/bin/env bash + +noetheris_select_python() { + local requested_python="${PYTHON_BIN:-python3}" + if [[ -z "${PYTHON_BIN+x}" && "$(uname -s)" == "Darwin" ]]; then + if command -v arch >/dev/null 2>&1; then + if arch -arm64 "${requested_python}" - <<'PY' >/dev/null 2>&1 +import platform +raise SystemExit(0 if platform.machine() == "arm64" else 1) +PY + then + NOETHERIS_PYTHON_CMD=(arch -arm64 "${requested_python}") + return + fi + fi + fi + NOETHERIS_PYTHON_CMD=("${requested_python}") +} + +noetheris_select_python diff --git a/scripts/run_all_python_tests.sh b/scripts/run_all_python_tests.sh index 78dd2d1..2b351a8 100755 --- a/scripts/run_all_python_tests.sh +++ b/scripts/run_all_python_tests.sh @@ -1,7 +1,11 @@ #!/usr/bin/env bash set -euo pipefail -export PYTHONPATH="${PYTHONPATH:-}:$(pwd)/python" -PYTHON_BIN="${PYTHON_BIN:-python3}" -"${PYTHON_BIN}" -m compileall python examples benchmarks -"${PYTHON_BIN}" -m pytest +if [[ -n "${PYTHONPATH:-}" ]]; then + export PYTHONPATH="${PYTHONPATH}:$(pwd)/python" +else + export PYTHONPATH="$(pwd)/python" +fi +source "$(dirname "${BASH_SOURCE[0]}")/python_env.sh" +"${NOETHERIS_PYTHON_CMD[@]}" -m compileall python examples benchmarks +"${NOETHERIS_PYTHON_CMD[@]}" -m pytest diff --git a/scripts/run_audit.sh b/scripts/run_audit.sh index 419845f..9c55476 100755 --- a/scripts/run_audit.sh +++ b/scripts/run_audit.sh @@ -1,29 +1,33 @@ #!/usr/bin/env bash set -euo pipefail -export PYTHONPATH="${PYTHONPATH:-}:$(pwd)/python" -PYTHON_BIN="${PYTHON_BIN:-python3}" +if [[ -n "${PYTHONPATH:-}" ]]; then + export PYTHONPATH="${PYTHONPATH}:$(pwd)/python" +else + export PYTHONPATH="$(pwd)/python" +fi +source "$(dirname "${BASH_SOURCE[0]}")/python_env.sh" cargo fmt --check --all cargo check --workspace cargo test --workspace cargo clippy --workspace --all-targets -- -D warnings -"${PYTHON_BIN}" -m compileall python examples benchmarks -"${PYTHON_BIN}" -m pytest +"${NOETHERIS_PYTHON_CMD[@]}" -m compileall python examples benchmarks +"${NOETHERIS_PYTHON_CMD[@]}" -m pytest bash scripts/run_examples.sh -"${PYTHON_BIN}" scripts/generate_release_results.py +"${NOETHERIS_PYTHON_CMD[@]}" scripts/generate_release_results.py bash scripts/run_benchmarks.sh >/tmp/noetheris_benchmarks.json if command -v lake >/dev/null 2>&1; then (cd formal/lean && lake build) fi tmp_dir="$(mktemp -d)" -"${PYTHON_BIN}" -m noetheris validate-ir examples/structural_ir/consensus_safety_ir.json >/tmp/noetheris_cli_validate.json -"${PYTHON_BIN}" -m noetheris compile-qubo examples/structural_ir/consensus_safety_ir.json --problem invariant --output "${tmp_dir}/compiled.json" -"${PYTHON_BIN}" -m noetheris solve "${tmp_dir}/compiled.json" --solver exact --output "${tmp_dir}/solution.json" -"${PYTHON_BIN}" -m noetheris run-scenario consensus >/tmp/noetheris_cli_scenario.json -"${PYTHON_BIN}" -m noetheris cv-diagnostics examples/structural_ir/cv_gkp_diagnostic_ir.json >/tmp/noetheris_cli_cv.json -"${PYTHON_BIN}" -m noetheris.certificates.validate examples/example_energy_certificate.json >/tmp/noetheris_cli_cert_validate.json -"${PYTHON_BIN}" -m noetheris.certificates.replay examples/example_energy_certificate.json >/tmp/noetheris_cli_cert_replay.json -"${PYTHON_BIN}" - <<'PY' +"${NOETHERIS_PYTHON_CMD[@]}" -m noetheris validate-ir examples/structural_ir/consensus_safety_ir.json >/tmp/noetheris_cli_validate.json +"${NOETHERIS_PYTHON_CMD[@]}" -m noetheris compile-qubo examples/structural_ir/consensus_safety_ir.json --problem invariant --output "${tmp_dir}/compiled.json" +"${NOETHERIS_PYTHON_CMD[@]}" -m noetheris solve "${tmp_dir}/compiled.json" --solver exact --output "${tmp_dir}/solution.json" +"${NOETHERIS_PYTHON_CMD[@]}" -m noetheris run-scenario consensus >/tmp/noetheris_cli_scenario.json +"${NOETHERIS_PYTHON_CMD[@]}" -m noetheris cv-diagnostics examples/structural_ir/cv_gkp_diagnostic_ir.json >/tmp/noetheris_cli_cv.json +"${NOETHERIS_PYTHON_CMD[@]}" -m noetheris.certificates.validate examples/example_energy_certificate.json >/tmp/noetheris_cli_cert_validate.json +"${NOETHERIS_PYTHON_CMD[@]}" -m noetheris.certificates.replay examples/example_energy_certificate.json >/tmp/noetheris_cli_cert_replay.json +"${NOETHERIS_PYTHON_CMD[@]}" - <<'PY' from noetheris.backends import export_oracle_to_qiskit, export_qubo_to_dwave from noetheris.circuits import BooleanOracle from noetheris.qubo import QuboModel @@ -31,8 +35,8 @@ assert export_qubo_to_dwave(QuboModel(variables=["x"], linear={"x": -1.0}))["cre assert export_oracle_to_qiskit(BooleanOracle(("x",), lambda bits: bits[0]))["credential_required"] is False PY for script in invariant_annealing_search.py pq_migration_optimizer.py consensus_safety_violation.py threshold_policy_analysis.py certificate_validation.py; do - "${PYTHON_BIN}" "examples/${script}" > "${tmp_dir}/${script}.a" - "${PYTHON_BIN}" "examples/${script}" > "${tmp_dir}/${script}.b" + "${NOETHERIS_PYTHON_CMD[@]}" "examples/${script}" > "${tmp_dir}/${script}.a" + "${NOETHERIS_PYTHON_CMD[@]}" "examples/${script}" > "${tmp_dir}/${script}.b" cmp "${tmp_dir}/${script}.a" "${tmp_dir}/${script}.b" done hex_terms=( diff --git a/scripts/run_benchmarks.sh b/scripts/run_benchmarks.sh index 296de2f..9f34372 100755 --- a/scripts/run_benchmarks.sh +++ b/scripts/run_benchmarks.sh @@ -1,6 +1,10 @@ #!/usr/bin/env bash set -euo pipefail -export PYTHONPATH="${PYTHONPATH:-}:$(pwd)/python" -PYTHON_BIN="${PYTHON_BIN:-python3}" -"${PYTHON_BIN}" benchmarks/run_benchmarks.py +if [[ -n "${PYTHONPATH:-}" ]]; then + export PYTHONPATH="${PYTHONPATH}:$(pwd)/python" +else + export PYTHONPATH="$(pwd)/python" +fi +source "$(dirname "${BASH_SOURCE[0]}")/python_env.sh" +"${NOETHERIS_PYTHON_CMD[@]}" benchmarks/run_benchmarks.py diff --git a/scripts/run_examples.sh b/scripts/run_examples.sh index 0633f6b..a51eb20 100755 --- a/scripts/run_examples.sh +++ b/scripts/run_examples.sh @@ -1,18 +1,23 @@ #!/usr/bin/env bash set -euo pipefail -export PYTHONPATH="${PYTHONPATH:-}:$(pwd)/python" -PYTHON_BIN="${PYTHON_BIN:-python3}" -"${PYTHON_BIN}" examples/invariant_annealing_search.py >/tmp/noetheris_invariant.json -"${PYTHON_BIN}" examples/pq_migration_optimizer.py >/tmp/noetheris_migration.json -"${PYTHON_BIN}" examples/consensus_safety_violation.py >/tmp/noetheris_consensus.json -"${PYTHON_BIN}" examples/threshold_policy_analysis.py >/tmp/noetheris_threshold.json -"${PYTHON_BIN}" examples/certificate_validation.py >/tmp/noetheris_certificate.json -"${PYTHON_BIN}" examples/qubo_ising_qaoa.py >/tmp/noetheris_qaoa.json -"${PYTHON_BIN}" examples/dwave_ocean_exchange.py >/tmp/noetheris_dwave_ocean.json -"${PYTHON_BIN}" examples/qiskit_oracle_export.py >/tmp/noetheris_qiskit_oracle.json -"${PYTHON_BIN}" examples/saga_failure_semantics.py >/tmp/noetheris_saga.json -"${PYTHON_BIN}" examples/cv_fock_truncation_diagnostics.py >/tmp/noetheris_cv_fock.json -"${PYTHON_BIN}" examples/cv_gkp_stabilizer_diagnostics.py >/tmp/noetheris_cv_gkp.json -"${PYTHON_BIN}" examples/cv_lindblad_leakage_report.py >/tmp/noetheris_cv_lindblad.json -"${PYTHON_BIN}" examples/cv_entanglement_diagnostics.py >/tmp/noetheris_cv_entanglement.json +if [[ -n "${PYTHONPATH:-}" ]]; then + export PYTHONPATH="${PYTHONPATH}:$(pwd)/python" +else + export PYTHONPATH="$(pwd)/python" +fi +source "$(dirname "${BASH_SOURCE[0]}")/python_env.sh" +"${NOETHERIS_PYTHON_CMD[@]}" examples/invariant_annealing_search.py >/tmp/noetheris_invariant.json +"${NOETHERIS_PYTHON_CMD[@]}" examples/pq_migration_optimizer.py >/tmp/noetheris_migration.json +"${NOETHERIS_PYTHON_CMD[@]}" examples/consensus_safety_violation.py >/tmp/noetheris_consensus.json +"${NOETHERIS_PYTHON_CMD[@]}" examples/threshold_policy_analysis.py >/tmp/noetheris_threshold.json +"${NOETHERIS_PYTHON_CMD[@]}" examples/certificate_validation.py >/tmp/noetheris_certificate.json +"${NOETHERIS_PYTHON_CMD[@]}" examples/qubo_ising_qaoa.py >/tmp/noetheris_qaoa.json +"${NOETHERIS_PYTHON_CMD[@]}" examples/dwave_ocean_exchange.py >/tmp/noetheris_dwave_ocean.json +"${NOETHERIS_PYTHON_CMD[@]}" examples/external_solver_replay.py >/tmp/noetheris_external_replay.json +"${NOETHERIS_PYTHON_CMD[@]}" examples/qiskit_oracle_export.py >/tmp/noetheris_qiskit_oracle.json +"${NOETHERIS_PYTHON_CMD[@]}" examples/saga_failure_semantics.py >/tmp/noetheris_saga.json +"${NOETHERIS_PYTHON_CMD[@]}" examples/cv_fock_truncation_diagnostics.py >/tmp/noetheris_cv_fock.json +"${NOETHERIS_PYTHON_CMD[@]}" examples/cv_gkp_stabilizer_diagnostics.py >/tmp/noetheris_cv_gkp.json +"${NOETHERIS_PYTHON_CMD[@]}" examples/cv_lindblad_leakage_report.py >/tmp/noetheris_cv_lindblad.json +"${NOETHERIS_PYTHON_CMD[@]}" examples/cv_entanglement_diagnostics.py >/tmp/noetheris_cv_entanglement.json diff --git a/tests/test_certificates.py b/tests/test_certificates.py index 87a4f37..b98a9c0 100644 --- a/tests/test_certificates.py +++ b/tests/test_certificates.py @@ -8,8 +8,14 @@ EnergyTerm, certificate_fingerprint, make_certificate, + stable_problem_hash, validate_certificate, ) +from noetheris.qubo import ( + CompiledProblem, + QuboModel, + external_solver_replay_artifact, +) ROOT = Path(__file__).resolve().parents[1] @@ -92,3 +98,56 @@ def test_certificate_fingerprint_changes_on_mutation() -> None: original = certificate_fingerprint(certificate) certificate["selected_variables"]["x"] = False assert certificate_fingerprint(certificate) != original + + +def test_certificate_external_replay_evidence_fails_closed() -> None: + problem = {"kind": "unit-external-replay"} + compiled = CompiledProblem( + problem_type="unit", + problem_hash=stable_problem_hash(problem), + compiled_model_hash="sha256:compiled", + model=QuboModel(variables=["x"], linear={"x": -1.0}), + variable_metadata={"x": "unit"}, + ) + replay = external_solver_replay_artifact( + compiled, + {"x": True}, + reported_energy=-1.0, + problem_hash=compiled.problem_hash, + compiled_model_hash=compiled.compiled_model_hash, + solver_metadata={"solver": "local_reference"}, + ) + certificate = make_certificate( + problem=problem, + algorithm_name="unit", + energy_terms=(EnergyTerm("qubo_energy", 1.0, -1.0),), + selected_variables={"x": True}, + satisfied_constraints=( + CertificateConstraint("external_replay", True, "accepted"), + ), + reproducibility_seed=1, + compiled_model_hash=compiled.compiled_model_hash, + energy_breakdown={"external_replay_artifact": replay}, + ) + assert validate_certificate(certificate).status == "verified" + + rejected_replay = external_solver_replay_artifact( + compiled, + {"x": True}, + reported_energy=0.0, + problem_hash=compiled.problem_hash, + compiled_model_hash=compiled.compiled_model_hash, + ) + rejected_certificate = certificate.to_dict() + rejected_certificate["energy_breakdown"]["external_replay_artifact"] = rejected_replay + validation = validate_certificate(rejected_certificate) + assert validation.status == "rejected" + assert "external_replay_artifact evidence is not verified" in validation.reasons + + tampered_certificate = certificate.to_dict() + tampered_certificate["energy_breakdown"]["external_replay_artifact"][ + "artifact_hash" + ] = "sha256:tampered" + validation = validate_certificate(tampered_certificate) + assert validation.status == "rejected" + assert "external_replay_artifact artifact hash mismatch" in validation.reasons diff --git a/tests/test_external_examples.py b/tests/test_external_examples.py index b4c60a1..b7ed9fe 100644 --- a/tests/test_external_examples.py +++ b/tests/test_external_examples.py @@ -48,3 +48,22 @@ def test_qiskit_oracle_export_example_has_exact_local_semantics() -> None: assert payload["oracle_metrics"]["cleanup_gate_count"] >= 1 assert payload["truth_table"]["11111"] == 1 assert payload["truth_table"]["10011"] == 0 + + +def test_external_solver_replay_example_has_accept_and_reject_evidence() -> None: + payload = _run_example("external_solver_replay.py") + assert payload["credential_required"] is False + assert payload["verification_authority"] == "noetheris.local_replay" + assert payload["accepted_candidate"]["status"] == "verified" + assert payload["accepted_candidate"]["artifact_hash"].startswith("sha256:") + rejected = {item["case"]: item for item in payload["rejected_candidates"]} + assert "problem_hash_mismatch" in rejected["problem_hash_mismatch"]["reason_codes"] + assert ( + "compiled_model_hash_mismatch" + in rejected["compiled_model_hash_mismatch"]["reason_codes"] + ) + assert "assignment_missing_variables" in rejected["missing_variables"]["reason_codes"] + assert "assignment_unknown_variables" in rejected["unknown_variables"]["reason_codes"] + assert "reported_energy_mismatch" in rejected["energy_mismatch"]["reason_codes"] + assert "solver_metadata_malformed" in rejected["malformed_metadata"]["reason_codes"] + assert "embedding_metadata_malformed" in rejected["malformed_metadata"]["reason_codes"] diff --git a/tests/test_qubo.py b/tests/test_qubo.py index 14f8106..51092c5 100644 --- a/tests/test_qubo.py +++ b/tests/test_qubo.py @@ -4,6 +4,7 @@ CompiledProblem, QuadraticTerm, QuboModel, + external_solver_replay_artifact, replay_external_solution, ) @@ -109,3 +110,77 @@ def test_external_solution_replay_fails_closed() -> None: assert replay_external_solution(compiled, {"x": True}, problem_hash="bad")["status"] == "rejected" assert replay_external_solution(compiled, {}, reported_energy=0.0)["status"] == "rejected" assert replay_external_solution(compiled, {"x": True, "y": True}, reported_energy=-1.0)["status"] == "rejected" + + +def test_external_replay_artifact_records_explicit_rejection_codes() -> None: + model = QuboModel(variables=["x", "y"], linear={"x": -1.0, "y": 2.0}) + compiled = CompiledProblem( + problem_type="unit", + problem_hash="sha256:problem", + compiled_model_hash="sha256:compiled", + model=model, + variable_metadata={"x": "unit", "y": "unit"}, + ) + accepted = external_solver_replay_artifact( + compiled, + {"x": 1, "y": 0}, + reported_energy=-1.0, + problem_hash="sha256:problem", + compiled_model_hash="sha256:compiled", + solver_metadata={"solver": "local_reference"}, + ) + assert accepted["schema"] == "noetheris.external_solver_replay.v1" + assert accepted["status"] == "verified" + assert accepted["artifact_hash"].startswith("sha256:") + assert accepted["assignment_domain"]["missing_variables"] == [] + assert accepted["assignment_domain"]["unknown_variables"] == [] + assert accepted["recomputed_energy"] == -1.0 + + rejected_cases = { + "problem_hash_mismatch": external_solver_replay_artifact( + compiled, + {"x": True, "y": False}, + reported_energy=-1.0, + problem_hash="sha256:wrong", + compiled_model_hash="sha256:compiled", + ), + "compiled_model_hash_mismatch": external_solver_replay_artifact( + compiled, + {"x": True, "y": False}, + reported_energy=-1.0, + problem_hash="sha256:problem", + compiled_model_hash="sha256:wrong", + ), + "assignment_missing_variables": external_solver_replay_artifact( + compiled, + {"x": True}, + reported_energy=-1.0, + ), + "assignment_unknown_variables": external_solver_replay_artifact( + compiled, + {"x": True, "y": False, "z": True}, + reported_energy=-1.0, + ), + "reported_energy_mismatch": external_solver_replay_artifact( + compiled, + {"x": True, "y": False}, + reported_energy=3.0, + ), + "solver_metadata_malformed": external_solver_replay_artifact( + compiled, + {"x": True, "y": False}, + reported_energy=-1.0, + solver_metadata="not-a-mapping", # type: ignore[arg-type] + ), + "embedding_metadata_malformed": external_solver_replay_artifact( + compiled, + {"x": True, "y": False}, + reported_energy=-1.0, + embedding_metadata="not-a-mapping", # type: ignore[arg-type] + ), + } + for expected_code, artifact in rejected_cases.items(): + assert artifact["status"] == "rejected" + assert expected_code in { + reason["code"] for reason in artifact["rejection_reasons"] + }