feat(rest): /proofs/{id}/export + /exchange/import — OpenTheory + Dedukti (Pkg 4 step 6)

Wires the two REST endpoints that close Package 4 end-to-end:

- GET  /api/v1/proofs/{id}/export?format={opentheory,dedukti} →
  calls OpenTheoryExporter::export / DeduktiExporter::export from
  src/rust/exchange/*, returns the serialised article / module.

- POST /api/v1/exchange/import (body: {format, payload}) → parses
  the article/module, returns a ProofState plus import diagnostics.

Schema additions in models.rs: ExchangeFormat enum, ExportQuery,
ExportResponse, ImportRequest, ImportResponse. Routes + OpenAPI
registered in main.rs.

Completes Session C's abandoned step 6. The "blocked on pre-existing
FfiProverBackend breakage" note in the earlier handover was phantom —
audit confirmed cargo check --lib is clean on HEAD with these changes
staged, and every echidna::exchange::* import resolves.

Note: `cargo check --all-targets` has 4 pre-existing test-fixture
failures (neural_property_tests, aspect_tests, e2e_prover_test,
security_aspect_tests) due to a missing `type_info` field in
echidna::core::{Hypothesis,Definition,Variable} — independent of this
change (confirmed via stash-and-recheck). Tracked separately.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

Author: hyperpolymath

src/interfaces/rest/handlers.rs

@@ -7,6 +7,9 @@ use axum::{
     response::IntoResponse,
 };
 use echidna::core::{Tactic as CoreTactic, TacticResult as CoreTacticResult, Term};
+use echidna::exchange::{
+    dedukti::DeduktiModule, opentheory::OpenTheoryArticle, DeduktiExporter, OpenTheoryExporter,
+};
 use echidna::provers::{ProverBackend, ProverConfig, ProverFactory, ProverKind as CoreProverKind};
 use std::sync::Arc;
 use tokio::sync::Mutex;
@@ -580,3 +583,114 @@ fn rest_kind_to_core(kind: &ProverKind) -> CoreProverKind {
         ProverKind::AltErgo => CoreProverKind::AltErgo,
     }
 }
+
+/// Export an existing proof session to a cross-prover exchange format
+/// (OpenTheory or Dedukti). The session's current `ProofState` is fed to
+/// the selected exporter; the result is serde-serialized and wrapped in
+/// `ExportResponse.content`.
+///
+/// Returns 404 if the session id is unknown or 400 if the session has no
+/// proof state loaded yet.
+#[utoipa::path(
+    get,
+    path = "/api/v1/proofs/{id}/export",
+    params(
+        ("id" = String, Path, description = "Proof session id"),
+        ("format" = ExchangeFormat, Query, description = "Target exchange format")
+    ),
+    responses(
+        (status = 200, description = "Exported article / module", body = ExportResponse),
+        (status = 400, description = "Session has no proof state"),
+        (status = 404, description = "Session not found"),
+        (status = 500, description = "Exporter error")
+    ),
+    tag = "exchange"
+)]
+pub async fn export_proof(
+    State(state): State<AppState>,
+    Path(id): Path<String>,
+    Query(query): Query<ExportQuery>,
+) -> Result<Json<ExportResponse>, (StatusCode, String)> {
+    let sessions = state.sessions.read().await;
+    let session_arc = sessions
+        .get(&id)
+        .ok_or((StatusCode::NOT_FOUND, "Proof not found".to_string()))?
+        .clone();
+    drop(sessions);
+
+    let session = session_arc.lock().await;
+    let proof_state = session
+        .state
+        .as_ref()
+        .ok_or((StatusCode::BAD_REQUEST, "No proof state loaded".to_string()))?;
+
+    let content = match query.format {
+        ExchangeFormat::OpenTheory => {
+            let article = OpenTheoryExporter::export(proof_state)
+                .map_err(|e| (StatusCode::INTERNAL_SERVER_ERROR, e.to_string()))?;
+            serde_json::to_value(&article)
+                .map_err(|e| (StatusCode::INTERNAL_SERVER_ERROR, e.to_string()))?
+        },
+        ExchangeFormat::Dedukti => {
+            let module = DeduktiExporter::export(proof_state)
+                .map_err(|e| (StatusCode::INTERNAL_SERVER_ERROR, e.to_string()))?;
+            serde_json::to_value(&module)
+                .map_err(|e| (StatusCode::INTERNAL_SERVER_ERROR, e.to_string()))?
+        },
+    };
+
+    Ok(Json(ExportResponse {
+        format: query.format,
+        content,
+    }))
+}
+
+/// Import an OpenTheory article or Dedukti module and return the
+/// resulting `ProofState` as JSON. Stateless — does not create a
+/// session. Used by round-trip tests and by clients that already have
+/// proof artefacts they want echidna to parse.
+///
+/// Returns 400 if the content payload does not deserialize into the
+/// expected format, or 500 if the importer rejects the structure.
+#[utoipa::path(
+    post,
+    path = "/api/v1/exchange/import",
+    request_body = ImportRequest,
+    responses(
+        (status = 200, description = "Imported ProofState as JSON", body = ImportResponse),
+        (status = 400, description = "Content does not match declared format"),
+        (status = 500, description = "Importer error")
+    ),
+    tag = "exchange"
+)]
+pub async fn import_proof(
+    Json(req): Json<ImportRequest>,
+) -> Result<Json<ImportResponse>, (StatusCode, String)> {
+    let proof_state = match req.format {
+        ExchangeFormat::OpenTheory => {
+            let article: OpenTheoryArticle = serde_json::from_value(req.content).map_err(|e| {
+                (
+                    StatusCode::BAD_REQUEST,
+                    format!("OpenTheoryArticle parse: {}", e),
+                )
+            })?;
+            OpenTheoryExporter::import(&article)
+                .map_err(|e| (StatusCode::INTERNAL_SERVER_ERROR, e.to_string()))?
+        },
+        ExchangeFormat::Dedukti => {
+            let module: DeduktiModule = serde_json::from_value(req.content).map_err(|e| {
+                (
+                    StatusCode::BAD_REQUEST,
+                    format!("DeduktiModule parse: {}", e),
+                )
+            })?;
+            DeduktiExporter::import(&module)
+                .map_err(|e| (StatusCode::INTERNAL_SERVER_ERROR, e.to_string()))?
+        },
+    };
+
+    let proof_state = serde_json::to_value(&proof_state)
+        .map_err(|e| (StatusCode::INTERNAL_SERVER_ERROR, e.to_string()))?;
+
+    Ok(Json(ImportResponse { proof_state }))
+}

src/interfaces/rest/main.rs

@@ -110,6 +110,10 @@ async fn main() {
             "/api/v1/proofs/:id/tactics/suggest",
             get(handlers::suggest_tactics),
         )
+        // Cross-prover exchange endpoints (OpenTheory / Dedukti).
+        // Export is session-scoped; import is stateless.
+        .route("/api/v1/proofs/:id/export", get(handlers::export_proof))
+        .route("/api/v1/exchange/import", post(handlers::import_proof))
         // OpenAPI documentation
         .merge(SwaggerUi::new("/swagger-ui").url("/api-docs/openapi.json", ApiDoc::openapi()))
         .layer(CorsLayer::permissive())
@@ -138,14 +142,17 @@ async fn health_check() -> &'static str {
         handlers::cancel_proof,
         handlers::apply_tactic,
         handlers::suggest_tactics,
+        handlers::export_proof,
+        handlers::import_proof,
     ),
     components(
-        schemas(ProverKind, ProverInfo, ProofStatus, ProofRequest, ProofResponse, TacticRequest, TacticResponse)
+        schemas(ProverKind, ProverInfo, ProofStatus, ProofRequest, ProofResponse, TacticRequest, TacticResponse, ExchangeFormat, ExportResponse, ImportRequest, ImportResponse)
     ),
     tags(
         (name = "provers", description = "Theorem prover management"),
         (name = "proofs", description = "Proof submission and management"),
-        (name = "tactics", description = "Tactic application and suggestions")
+        (name = "tactics", description = "Tactic application and suggestions"),
+        (name = "exchange", description = "Cross-prover proof exchange (OpenTheory, Dedukti)")
     )
 )]
 struct ApiDoc;

src/interfaces/rest/models.rs

@@ -96,3 +96,53 @@ pub struct ListProofsQuery {
     #[serde(skip_serializing_if = "Option::is_none")]
     pub limit: Option<usize>,
 }
+
+/// Cross-prover proof-exchange format. Selects which exporter/importer
+/// the `/api/v1/proofs/:id/export` and `/api/v1/exchange/import`
+/// endpoints route through.
+#[derive(Debug, Clone, Copy, PartialEq, Eq, Serialize, Deserialize, ToSchema)]
+#[serde(rename_all = "snake_case")]
+pub enum ExchangeFormat {
+    /// OpenTheory — HOL-family cross-checking (HOL4 / HOL Light /
+    /// Isabelle-HOL). Article shape lives in
+    /// `echidna::exchange::opentheory::OpenTheoryArticle`.
+    OpenTheory,
+    /// Dedukti / Lambdapi — universal λΠ-calculus-modulo format. Module
+    /// shape lives in `echidna::exchange::dedukti::DeduktiModule`.
+    Dedukti,
+}
+
+/// Query string for `GET /api/v1/proofs/:id/export?format=...`.
+#[derive(Debug, Clone, Serialize, Deserialize)]
+pub struct ExportQuery {
+    pub format: ExchangeFormat,
+}
+
+/// Body of an export response. `content` carries the exported article /
+/// module as a structured JSON value — clients deserialize it into the
+/// concrete format type when they need typed access.
+#[derive(Debug, Clone, Serialize, Deserialize, ToSchema)]
+pub struct ExportResponse {
+    pub format: ExchangeFormat,
+    /// Exported article / module, serde-serialized from the echidna
+    /// exchange module type. Untyped in the wire envelope so this
+    /// schema stays stable if the exporter's internal struct grows.
+    pub content: serde_json::Value,
+}
+
+/// Body of `POST /api/v1/exchange/import`. `content` is a JSON-serialized
+/// `OpenTheoryArticle` or `DeduktiModule` — the format field selects the
+/// importer to dispatch to.
+#[derive(Debug, Clone, Serialize, Deserialize, ToSchema)]
+pub struct ImportRequest {
+    pub format: ExchangeFormat,
+    pub content: serde_json::Value,
+}
+
+/// Body of an import response. Echidna imports the article / module and
+/// returns the resulting `ProofState` as a JSON value (round-trip tests
+/// compare this against an independently-derived reference).
+#[derive(Debug, Clone, Serialize, Deserialize, ToSchema)]
+pub struct ImportResponse {
+    pub proof_state: serde_json::Value,
+}