Bind the Python package to NajaEDA through its shipped headers

.github/workflows/regress-python.yml

@@ -36,7 +36,7 @@ jobs:
         with:
           python-version: '3.12'
 
-      # The SDK-selection tests require CMake 3.30 or newer.
+      # The provider-selection tests require CMake 3.30 or newer.
       - uses: jwlawson/actions-setup-cmake@v2
         with:
           cmake-version: '3.31.x'

ci/prepare_python_release.py

@@ -16,7 +16,7 @@
 import re
 
 
-DEVELOPMENT_REQUIREMENT = "najaeda==0.7.26"
+DEVELOPMENT_REQUIREMENT = "najaeda==0.7.27"
 PUBLISHED_REQUIREMENT = "najaeda==0.7.24"
 CMAKE_OPTION = "KEPLER_USE_PUBLISHED_NAJAEDA"
 VERSION_PATTERN = r'KEPLER_VERSION\s*\{\s*"(?P<value>[0-9]+\.[0-9]+\.[0-9]+)"'

ci/shared_naja_wheels.py

@@ -2,7 +2,7 @@
 # Copyright 2026 keplertech.io
 # SPDX-License-Identifier: GPL-3.0-only
 
-"""Build a local SDK provider for CI, and repair consumers without copying it.
+"""Build a local NajaEDA provider for CI, and repair consumers without copying it.
 
 The provider is a separate wheel. This helper never publishes either package.
 After the matching NajaEDA release exists, ordinary isolated pip builds can
@@ -24,7 +24,7 @@
 # version number as the NajaEDA release it is based on, so the version alone
 # cannot tell the two providers apart.
 USE_PUBLISHED_PROVIDER = os.environ.get("KEPLER_USE_PUBLISHED_NAJAEDA") == "1"
-PROVIDER_REQUIREMENT = "najaeda==0.7.24" if USE_PUBLISHED_PROVIDER else "najaeda==0.7.26"
+PROVIDER_REQUIREMENT = "najaeda==0.7.24" if USE_PUBLISHED_PROVIDER else "najaeda==0.7.27"
 
 
 def run(*arguments: str, env: dict[str, str] | None = None) -> None:
@@ -135,7 +135,7 @@ def repair_external(wheel: Path, destination: Path, dependencies: dict[str, Path
         if dependencies:
             command += ["--exclude", os.pathsep.join(dependencies)]
         else:
-            # Keep the provider's SDK import-library DLL names stable.
+            # Keep the DLL names matching the provider's shipped import libraries.
             command += ["--no-mangle", "naja_*.dll;libnaja_*.dll"]
         run(*command, str(wheel))
     else:

docs/python-api.md

@@ -17,8 +17,9 @@ For local regression without wheels or publishing, use the
 [source regression runner](python-regression.md). It compiles both Python
 packages from this checkout and tests their shared runtime.
 
-The default development build uses the matching NajaEDA shared-runtime SDK,
-version `0.7.26` in `thirdparty/naja`. Build both packages from this
+The default development build links the NajaEDA wheel built from
+`thirdparty/naja` (version `0.7.27`), which ships the headers matching its
+libraries under `najaeda/sdk/include`. Build both packages from this
 recursive checkout in one virtual environment, with the native build
 dependencies installed:
 
@@ -31,14 +32,13 @@ python -m pip install --no-build-isolation .
 Default wheel CI runs on relevant pull requests, pushes to `main`, `v*` tags, and manual
 runs. It builds and installs a separate local provider wheel for every
 Python/platform combination. Only a manual `publish` request adds a second,
-parallel set of jobs against published NajaEDA `0.7.24` wheels through KF's
-version-specific compatibility adapter. Only published-provider jobs must
+parallel set of jobs against published NajaEDA `0.7.24` wheels, which ship no
+headers; `KEPLER_USE_PUBLISHED_NAJAEDA` takes them from that release's verified
+source archive instead. Only published-provider jobs must
 pass for publication; development-provider jobs remain independent regression
 checks. Only wheels tested against the published provider are uploaded.
-The adapter obtains matching release headers, links the installed native
-libraries, and checks their identity before sharing designs. Those wheels
-require `najaeda==0.7.24`, which pip installs normally. There is no separate
-provider checkbox; see [release instructions](python-release.md).
+Those wheels require `najaeda==0.7.24`, which pip installs normally. There is
+no separate provider checkbox; see [release instructions](python-release.md).
 
 `BUILD_KEPLER_PYTHON=ON` is a Python-only CMake build. Build the standalone
 executable separately with `BUILD_KEPLER_PYTHON=OFF`; it continues to use the
@@ -66,10 +66,12 @@ Maintainers can publish tested wheels using the manual
 ## Shared NajaEDA runtime
 
 `najaeda` is a runtime dependency of `kepler_formal` and is imported before
-Kepler's native extension. Development builds use its versioned native API to
-check build and runtime identity. The published-provider adapter instead checks
-the pinned release's native-file fingerprints, exported Python types, and live
-universe identity. Both paths reject mismatches before accepting live designs.
+Kepler's native extension. The extension links the installed package's own
+`libnaja_*` libraries and records their version, git hash and file
+fingerprints at build time. At import it checks those, the exported Python
+types, and the live universe identity, and rejects any mismatch before
+accepting live designs. The same checks apply to development and published
+providers.
 
 For compatibility, `kepler_formal.najaeda` and all of its submodules are
 aliases to the original package:

docs/python-regression.md

@@ -1,7 +1,8 @@
 # Python regression from source
 
 The regression builds NajaEDA from the pinned `thirdparty/naja` submodule,
-then builds Kepler's Python extension against that NajaEDA SDK. Both packages
+then builds Kepler's Python extension against that NajaEDA's installed
+libraries and headers. Both packages
 are installed with CMake into a private directory. No wheels, package index,
 or publishing are involved.
 

docs/python-release.md

@@ -56,8 +56,8 @@ and [GitHub environment protection documentation](https://docs.github.com/en/act
 
 After the workflow is present on the repository's default branch, open
 **Actions → Python wheels → Run workflow**. Leave `publish` unchecked and
-`version` empty. These jobs use locally built NajaEDA `0.7.26` from the
-pinned submodule and its shared-runtime SDK. The workflow builds, repairs,
+`version` empty. These jobs use locally built NajaEDA `0.7.27` from the
+pinned submodule, whose wheel ships its headers. The workflow builds, repairs,
 and tests wheels, then stores them as Actions artifacts. Use this to check a
 branch before merging.
 
@@ -86,9 +86,10 @@ repository defaults and development jobs stay on the development provider
 with the option off. Build and runtime pins must match, so installations of
 a published-provider Kepler wheel select the same NajaEDA release.
 
-Published NajaEDA does not supply the development shared-runtime SDK. This
-compatibility path is deliberately pinned to `0.7.24` and uses released native
-symbols, including the private DNL cache integration. It is not a general ABI
+Published NajaEDA `0.7.24` ships no headers, so this path takes them from the
+release's verified source archive and is deliberately pinned to that version.
+Both providers are linked the same way, through released native symbols
+including the private DNL cache integration. This is not a general ABI
 guarantee for arbitrary NajaEDA versions; any provider upgrade requires a new
 compatibility review and the complete wheel tests. It does not change NajaEDA
 or bundle a second Naja runtime.

pyproject.toml

@@ -2,7 +2,7 @@
 # SPDX-License-Identifier: Apache-2.0
 
 [build-system]
-requires = ["scikit-build-core>=0.11.3,<0.12", "najaeda==0.7.26"]
+requires = ["scikit-build-core>=0.11.3,<0.12", "najaeda==0.7.27"]
 build-backend = "scikit_build_core.build"
 
 [project]
@@ -11,7 +11,7 @@ description = "Native Python interface for Kepler Formal equivalence checking"
 authors = [{name = "keplertech.io", email = "contact@keplertech.io"}]
 readme = "src/python/README.rst"
 requires-python = ">=3.10"
-dependencies = ["najaeda==0.7.26"]
+dependencies = ["najaeda==0.7.27"]
 license = {file = "LICENSE.rst"}
 dynamic = ["version"]
 classifiers = [

regress/run_python_regress.py

@@ -43,7 +43,7 @@ def main():
     stage = build / "packages"
     environment = build / "venv"
     # Keep system and user Python packages out of the test environment. Both
-    # projects use this exact interpreter, compiler configuration, and SDK.
+    # projects use this exact interpreter, compiler configuration, and headers.
     venv.EnvBuilder(with_pip=False).create(environment)
     python = environment / ("Scripts/python.exe" if os.name == "nt" else "bin/python")
     env = dict(os.environ, PYTHONPATH=str(stage), PYTHONNOUSERSITE="1",
@@ -74,7 +74,7 @@ def run(*command):
             f"-DCMAKE_INSTALL_PREFIX={stage}",
         ]
         try:
-            # Fail early rather than reaching the SDK-selection regression
+            # Fail early rather than reaching the provider-selection regression
             # after compiling with an older CMake.
             version_check = build / "check_cmake.cmake"
             version_check.write_text("cmake_minimum_required(VERSION 3.30)\n")
@@ -91,10 +91,10 @@ def run(*command):
 import sys
 from pathlib import Path
 import najaeda
-from najaeda import sdk
 stage = Path(sys.argv[1]).resolve()
-assert Path(najaeda.__file__).resolve().is_relative_to(stage), najaeda.__file__
-assert Path(sdk.get_cmake_dir()).resolve().is_relative_to(stage), sdk.get_cmake_dir()
+root = Path(najaeda.__file__).resolve().parent
+assert root.is_relative_to(stage), najaeda.__file__
+assert (root / 'sdk/include/naja/core/NajaVersion.h').is_file(), 'NajaEDA ships no headers'
 print('Source-built NajaEDA:', najaeda.__file__)
 """, stage)
 
@@ -104,11 +104,6 @@ def run(*command):
             run("cmake", "--build", consumer, "--target", "kepler_formal_native",
                 "kepler-borrowed-native-tests", "--parallel", args.jobs)
             run("cmake", "--install", consumer, "--component", "python")
-            if sys.platform == "darwin":
-                # The SDK signs the build artifact. CMake then adjusts its
-                # install RPATH, invalidating that signature on Apple Silicon.
-                for extension in (stage / "kepler_formal").glob("_native*.so"):
-                    run("codesign", "--force", "--sign", "-", extension)
             run(python, "-c", """
 import sys
 from pathlib import Path

src/python/CMakeLists.txt

@@ -16,13 +16,7 @@ add_library(kepler_borrowed_designs STATIC KeplerBorrowedDesigns.cpp KeplerNajaS
 target_include_directories(kepler_borrowed_designs PUBLIC ${CMAKE_CURRENT_SOURCE_DIR})
 target_link_libraries(kepler_borrowed_designs PUBLIC kepler_verification_support)
 
-if(KEPLER_USE_PUBLISHED_NAJAEDA)
-  set(kepler_runtime_source KeplerPublishedNajaRuntime.cpp)
-  target_compile_definitions(kepler_borrowed_designs PUBLIC KEPLER_USE_PUBLISHED_NAJAEDA=1)
-else()
-  set(kepler_runtime_source KeplerNajaRuntime.cpp)
-endif()
-Python3_add_library(kepler_formal_native MODULE WITH_SOABI PyKeplerFormal.cpp ${kepler_runtime_source})
+Python3_add_library(kepler_formal_native MODULE WITH_SOABI PyKeplerFormal.cpp KeplerNajaRuntime.cpp)
 set_target_properties(kepler_formal_native PROPERTIES
   OUTPUT_NAME _native
   CXX_VISIBILITY_PRESET hidden
@@ -32,6 +26,9 @@ target_compile_definitions(kepler_formal_native PRIVATE
   KEPLER_FORMAL_VERSION="${PROJECT_VERSION}"
   KEPLER_FORMAL_GIT_HASH="${KEPLER_FORMAL_GIT_HASH}"
 )
+if(KEPLER_USE_PUBLISHED_NAJAEDA)
+  target_compile_definitions(kepler_formal_native PRIVATE KEPLER_USE_PUBLISHED_NAJAEDA=1)
+endif()
 target_include_directories(kepler_formal_native PRIVATE ${PROJECT_SOURCE_DIR}/src/bin)
 target_link_libraries(kepler_formal_native PRIVATE
   kepler_borrowed_designs
@@ -55,6 +52,15 @@ install(TARGETS
   PUBLIC_HEADER DESTINATION kepler_formal/include
   COMPONENT python-headers
 )
+if(APPLE)
+  # The provider fixup ad-hoc signs the module after linking. Installing
+  # rewrites its RPATH, which invalidates that signature, and Apple Silicon
+  # then kills the importing process. Sign the installed copy again.
+  install(CODE "execute_process(COMMAND codesign --force --sign -
+      \"\${CMAKE_INSTALL_PREFIX}/kepler_formal/$<TARGET_FILE_NAME:kepler_formal_native>\"
+      COMMAND_ERROR_IS_FATAL ANY)"
+    COMPONENT python)
+endif()
 
 install(
   DIRECTORY ${CMAKE_CURRENT_SOURCE_DIR}/kepler_formal

src/python/KeplerNajaRuntime.cpp

@@ -3,56 +3,120 @@
 
 #include "KeplerNajaRuntime.h"
 
-#include <cstring>
+#include <memory>
 
-#include "NajaPythonRuntimeAPI.h"
-#include "NajaRuntimeBuild.h"
+#include "KeplerNajaProviderBuild.h"
 #include "NLUniverse.h"
+#include "PyNLUniverse.h"
+#include "PySNLDesign.h"
 
 namespace KEPLER_FORMAL {
 namespace {
 
-const NajaPythonRuntimeAPI* getRuntimeAPI(PyObject* errorType) {
-  const auto* api = NajaPythonRuntime_Import();
-  if (api == nullptr) {
-    return nullptr;
+struct PyObjectDeleter {
+  void operator()(PyObject* object) const { Py_XDECREF(object); }
+};
+using OwnedPyObject = std::unique_ptr<PyObject, PyObjectDeleter>;
+
+bool validateProviderBuild() {
+  // The GIL serializes this check. Each process checks the provider's bytes
+  // once; subsequent calls still validate the live types and universe below.
+  static bool validated = false;
+  if (validated) {
+    return true;
   }
-  if (api->build_id == nullptr || api->runtime_identity == nullptr ||
-      api->get_universe == nullptr || api->unwrap_design == nullptr) {
-    PyErr_SetString(errorType, "Incomplete NajaEDA native runtime API");
-    return nullptr;
+  OwnedPyObject helper(PyImport_ImportModule("kepler_formal._provider_check"));
+  if (helper == nullptr) {
+    return false;
+  }
+  OwnedPyObject result(PyObject_CallMethod(
+      helper.get(), "validate_provider", "sss", KEPLER_NAJA_PROVIDER_MANIFEST,
+      KEPLER_NAJA_PROVIDER_VERSION, KEPLER_NAJA_PROVIDER_GIT_HASH));
+  if (result == nullptr) {
+    return false;
   }
-  if (std::strcmp(api->build_id, NAJA_RUNTIME_BUILD_ID) != 0) {
+  validated = true;
+  return true;
+}
+
+bool requireIdentityString(PyObject* module, const char* method,
+                           const char* expected, PyObject* errorType) {
+  OwnedPyObject value(PyObject_CallMethod(module, method, nullptr));
+  if (value == nullptr) {
+    return false;
+  }
+  if (!PyUnicode_Check(value.get()) ||
+      PyUnicode_CompareWithASCIIString(value.get(), expected) != 0) {
     PyErr_Format(errorType,
-                 "NajaEDA native build mismatch: provider %.80s, Kepler %.80s",
-                 api->build_id, NAJA_RUNTIME_BUILD_ID);
-    return nullptr;
+                 "Kepler Formal was built against NajaEDA with %s() = %s",
+                 method, expected);
+    return false;
+  }
+  return true;
+}
+
+}  // namespace
+
+bool validateNajaRuntime(PyObject* errorType) {
+  OwnedPyObject module(PyImport_ImportModule("najaeda.naja"));
+  if (module == nullptr ||
+      !requireIdentityString(module.get(), "getVersion",
+                             KEPLER_NAJA_PROVIDER_VERSION, errorType) ||
+      !requireIdentityString(module.get(), "getGitHash",
+                             KEPLER_NAJA_PROVIDER_GIT_HASH, errorType) ||
+      !validateProviderBuild()) {
+    return false;
+  }
+
+  OwnedPyObject designType(PyObject_GetAttrString(module.get(), "SNLDesign"));
+  OwnedPyObject universeType(PyObject_GetAttrString(module.get(), "NLUniverse"));
+  if (designType == nullptr || universeType == nullptr) {
+    return false;
   }
-  if (api->runtime_identity != naja::NL::NLUniverse::getRuntimeIdentity()) {
+  // Compare live exported objects: the type objects Python sees must be the
+  // ones this extension linked, or two Naja copies are loaded.
+  if (designType.get() != reinterpret_cast<PyObject*>(&PYNAJA::PyTypeSNLDesign) ||
+      universeType.get() != reinterpret_cast<PyObject*>(&PYNAJA::PyTypeNLUniverse)) {
     PyErr_SetString(
         errorType,
         "NajaEDA and Kepler Formal did not load the same native runtime");
-    return nullptr;
+    return false;
+  }
+  OwnedPyObject pythonUniverse(
+      PyObject_CallMethod(universeType.get(), "get", nullptr));
+  if (pythonUniverse == nullptr) {
+    return false;
   }
-  if (api->get_universe() != naja::NL::NLUniverse::get()) {
+  OwnedPyObject linkedUniverse(
+      PYNAJA::PyNLUniverse_Link(naja::NL::NLUniverse::get()));
+  if (linkedUniverse == nullptr) {
+    return false;
+  }
+  if (pythonUniverse.get() != linkedUniverse.get()) {
     PyErr_SetString(errorType,
                     "NajaEDA and Kepler Formal disagree on the active universe");
-    return nullptr;
+    return false;
   }
-  return api;
-}
-
-}  // namespace
-
-bool validateNajaRuntime(PyObject* errorType) {
-  return getRuntimeAPI(errorType) != nullptr;
+  return true;
 }
 
 naja::NL::SNLDesign* unwrapNajaDesign(PyObject* object) {
-  const auto* api = getRuntimeAPI(PyExc_RuntimeError);
-  return api == nullptr
-             ? nullptr
-             : static_cast<naja::NL::SNLDesign*>(api->unwrap_design(object));
+  if (!validateNajaRuntime(PyExc_RuntimeError)) {
+    return nullptr;
+  }
+  if (object == nullptr || !PyObject_TypeCheck(object, &PYNAJA::PyTypeSNLDesign)) {
+    PyErr_SetString(PyExc_TypeError,
+                    "Expected an SNLDesign from this NajaEDA runtime");
+    return nullptr;
+  }
+  // Naja clears the wrapper's native pointer when the design, its library,
+  // database or universe is destroyed.
+  auto* design = reinterpret_cast<PYNAJA::PySNLDesign*>(object)->object_;
+  if (design == nullptr) {
+    PyErr_SetString(PyExc_ReferenceError, "The NajaEDA design was destroyed");
+    return nullptr;
+  }
+  return design;
 }
 
 }  // namespace KEPLER_FORMAL