L_2: Introduce metadata part in .vnnlib file to persist image, image_class and epsilon for SDP-CROWN

ada_verona/database/verification_context.py

@@ -92,11 +92,9 @@ def delete_tmp_path(self) -> None:
         """
         Delete the temporary path and its contents.
         """
-
 
         self.tmp_path.unlink()
 
-
     def save_status_list(self, epsilon_status_list: list[EpsilonStatus]) -> None:
         """
         Save the list of epsilon statuses to a CSV file.
@@ -153,7 +151,7 @@ def from_dict(cls, data: dict) -> "VerificationContext":
         """
         # Recreate the network from its dictionary representation
 
-        network = ONNXNetwork.from_dict(data["network"]) 
+        network = ONNXNetwork.from_dict(data["network"])
         data_point = DataPoint.from_dict(data["data_point"])
         tmp_path = Path(data["tmp_path"])
         property_generator = PropertyGenerator.from_dict(data["property_generator"])
@@ -164,4 +162,4 @@ def from_dict(cls, data: dict) -> "VerificationContext":
             tmp_path=tmp_path,
             property_generator=property_generator,
             save_epsilon_results=save_epsilon_results,
-        )
+        )

ada_verona/verification_module/auto_verify_module.py

@@ -64,15 +64,34 @@ def verify(self, verification_context: VerificationContext, epsilon: float) -> s
             image, verification_context.data_point.label, epsilon
         )
 
+        # SDP-CROWN needs access to the concrete instance (image), label, and epsilon,
+        # but it is executed in a separate process that only receives the `.vnnlib` path.
+        # We therefore embed a small VERONA metadata header into the `.vnnlib` content.
+        if (self.verifier.name == "sdpcrown") and ("; verona_metadata_version:" not in vnnlib_property.content):
+            image_flat = verification_context.data_point.data.detach().cpu().numpy().reshape(-1)
+            image_csv = ",".join(f"{v:.8f}" for v in image_flat)
+            header = (
+                "; verona_metadata_version: 1\n"
+                f"; verona_epsilon: {float(epsilon):.8f}\n"
+                f"; verona_image_class: {int(verification_context.data_point.label)}\n"
+                f"; verona_image: {image_csv}\n"
+            )
+            vnnlib_property.content = header + vnnlib_property.content
+
         verification_context.save_vnnlib_property(vnnlib_property)
 
         if self.config:
             result = self.verifier.verify_property(
-                verification_context.network.path, vnnlib_property.path, timeout=self.timeout, config=self.config
+                verification_context.network.path,
+                vnnlib_property.path,
+                timeout=self.timeout,
+                config=self.config,
             )
         else:
             result = self.verifier.verify_property(
-                verification_context.network.path, vnnlib_property.path, timeout=self.timeout
+                verification_context.network.path,
+                vnnlib_property.path,
+                timeout=self.timeout,
             )
 
         if isinstance(result, Ok):

ada_verona/verification_module/property_generator/one2any_property_generator.py

@@ -21,7 +21,7 @@
 
 class One2AnyPropertyGenerator(PropertyGenerator):
     """One2AnyPropertyGenerator generates properties for untargeted verification of neural networks.
-    This means the property is violated if we can find any class other than the target class 
+    This means the property is violated if we can find any class other than the target class
     that has a higher output value.
     """
 
@@ -75,7 +75,7 @@ def create_vnnlib_property(self, image: np.array, image_class: int, epsilon: flo
             result += f"(assert (>= X_{i} {x_lb[i]:.8f}))\n"
 
         result += "\n; Definition of output constraints\n"
-    
+
         result += "(assert (or\n"
         for i in range(self.number_classes):
             if i == image_class:
@@ -85,7 +85,10 @@ def create_vnnlib_property(self, image: np.array, image_class: int, epsilon: flo
 
         property_name = f"property_{image_class}_{str(epsilon).replace('.', '_')}"
 
-        return VNNLibProperty(name=property_name, content=result)
+        return VNNLibProperty(
+            name=property_name,
+            content=result,
+        )
 
     def get_dict_for_epsilon_result(self) -> dict:
         """
@@ -110,8 +113,7 @@ def to_dict(self) -> dict:
             type=self.__class__.__name__,
             module=self.__class__.__module__,
         )
-
-
+
     @classmethod
     def from_dict(cls, data: dict):
         """

ada_verona/verification_module/property_generator/one2one_property_generator.py

@@ -26,7 +26,7 @@ class One2OnePropertyGenerator(PropertyGenerator):
 
     def __init__(self, target_class: int, number_classes: int = 10, data_lb: int = 0, data_ub: int = 1):
         """
-        Initialize the One2OnePropertyGenerator with the target class, number of classes, data lower bound, 
+        Initialize the One2OnePropertyGenerator with the target class, number of classes, data lower bound,
         and data upper bound.
         Args:
             target_class (int): The target class for the property.
@@ -84,7 +84,10 @@ def create_vnnlib_property(self, image: np.array, image_class: int, epsilon: flo
 
         property_name = f"property_{image_class}_{str(epsilon).replace('.', '_')}"
 
-        return VNNLibProperty(name=property_name, content=result)
+        return VNNLibProperty(
+            name=property_name,
+            content=result,
+        )
 
     def get_dict_for_epsilon_result(self) -> dict:
         """
@@ -102,7 +105,7 @@ def to_dict(self) -> dict:
         Returns:
             dict: The dictionary representation of the One2OnePropertyGenerator.
         """
-        
+
         return dict(
             target_class=self.target_class,
             number_classes=self.number_classes,
@@ -111,8 +114,7 @@ def to_dict(self) -> dict:
             type=self.__class__.__name__,
             module=self.__class__.__module__,
         )
-
-
+
     @classmethod
     def from_dict(cls, data: dict):
         """

ada_verona/verification_module/verification_module.py

@@ -22,5 +22,5 @@
 class VerificationModule(ABC):
     @abstractmethod
     def verify(self, verification_context: VerificationContext, epsilon: float) -> str | CompleteVerificationData:
-        """Main method to verify an image for a given network and epsilon value"""
+        """Main method to verify an image (or other data instance) for a given network and epsilon value."""
         raise NotImplementedError

tests/test_verification_module/test_auto_verify_module_sdpcrown_metadata.py

@@ -0,0 +1,116 @@
+# Copyright 2025 ADA Reseach Group and VERONA council. All Rights Reserved.
+#
+# Licensed under the Apache License, Version 2.0 (the "License");
+# you may not use this file except in compliance with the License.
+# You may obtain a copy of the License at
+#
+#     http://www.apache.org/licenses/LICENSE-2.0
+#
+# Unless required by applicable law or agreed to in writing, software
+# distributed under the License is distributed on an "AS IS" BASIS,
+# WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+# See the License for the specific language governing permissions and
+# limitations under the License.
+# ==============================================================================
+
+from __future__ import annotations
+
+from pathlib import Path
+
+import numpy as np
+import pytest
+import torch
+from result import Ok
+
+from ada_verona.database.dataset.data_point import DataPoint
+from ada_verona.database.machine_learning_model.onnx_network import ONNXNetwork
+from ada_verona.database.verification_context import VerificationContext
+from ada_verona.database.verification_result import CompleteVerificationData
+from ada_verona.verification_module.auto_verify_module import AutoVerifyModule
+from ada_verona.verification_module.property_generator.one2any_property_generator import One2AnyPropertyGenerator
+
+
+class _CapturingVerifier:
+    def __init__(self, name: str):
+        self.name = name
+        self.seen_network: Path | None = None
+        self.seen_property: Path | None = None
+
+    def verify_property(self, network: Path, property: Path, **kwargs):  # noqa: A002
+        self.seen_network = network
+        self.seen_property = property
+        return Ok(CompleteVerificationData(result="UNSAT", took=0.0))
+
+
+def _parse_verona_header(vnnlib_text: str) -> tuple[float, int, np.ndarray]:
+    epsilon = None
+    image_class = None
+    image_csv = None
+
+    for raw_line in vnnlib_text.splitlines():
+        line = raw_line.strip()
+        if not line.startswith(";"):
+            break
+        if line.startswith("; verona_epsilon:"):
+            epsilon = float(line.split(":", 1)[1].strip())
+        elif line.startswith("; verona_image_class:"):
+            image_class = int(line.split(":", 1)[1].strip())
+        elif line.startswith("; verona_image:"):
+            image_csv = line.split(":", 1)[1].strip()
+
+    assert epsilon is not None
+    assert image_class is not None
+    assert image_csv is not None
+
+    return epsilon, image_class, np.fromstring(image_csv, sep=",", dtype=np.float32)
+
+
+def test_sdpcrown_injects_verona_metadata_header(tmp_path: Path):
+    network_path = tmp_path / "network.onnx"
+    network_path.write_text("", encoding="utf-8")
+
+    verification_context = VerificationContext(
+        network=ONNXNetwork(network_path),
+        data_point=DataPoint(id="1", label=2, data=torch.tensor([0.1, 0.2, 0.3], dtype=torch.float32)),
+        tmp_path=tmp_path,
+        property_generator=One2AnyPropertyGenerator(number_classes=10, data_lb=0, data_ub=1),
+    )
+
+    verifier = _CapturingVerifier(name="sdpcrown")
+    module = AutoVerifyModule(verifier=verifier, timeout=1.0)
+
+    epsilon = 0.1
+    result = module.verify(verification_context, epsilon=epsilon)
+    assert result.result == "UNSAT"
+
+    assert verifier.seen_property is not None
+    vnnlib_text = verifier.seen_property.read_text(encoding="utf-8")
+
+    assert vnnlib_text.startswith("; verona_metadata_version: 1\n")
+
+    parsed_epsilon, parsed_label, parsed_image = _parse_verona_header(vnnlib_text)
+    assert parsed_epsilon == pytest.approx(epsilon)
+    assert parsed_label == 2
+    assert np.allclose(parsed_image, verification_context.data_point.data.detach().cpu().numpy().reshape(-1))
+
+
+def test_non_sdpcrown_does_not_inject_metadata(tmp_path: Path):
+    network_path = tmp_path / "network.onnx"
+    network_path.write_text("", encoding="utf-8")
+
+    verification_context = VerificationContext(
+        network=ONNXNetwork(network_path),
+        data_point=DataPoint(id="1", label=2, data=torch.tensor([0.1, 0.2, 0.3], dtype=torch.float32)),
+        tmp_path=tmp_path,
+        property_generator=One2AnyPropertyGenerator(number_classes=10, data_lb=0, data_ub=1),
+    )
+
+    verifier = _CapturingVerifier(name="not_sdpcrown")
+    module = AutoVerifyModule(verifier=verifier, timeout=1.0)
+
+    result = module.verify(verification_context, epsilon=0.1)
+    assert result.result == "UNSAT"
+
+    assert verifier.seen_property is not None
+    vnnlib_text = verifier.seen_property.read_text(encoding="utf-8")
+    assert "; verona_metadata_version:" not in vnnlib_text