Skip to content

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

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
henba1 merged 13 commits into from
Jan 13, 2026
Merged

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

Show file tree
Hide file tree
Changes from 4 commits
Commits
Show all changes
13 commits
Select commit Hold shift + click to select a range
8467268
Add image and image_class to vnnlib_property
henba1 Nov 23, 2025
d30d425
Save image and image_class as vnnlib_property sidecar
henba1 Nov 23, 2025
e51bf12
In implemmented property generators: epsilon, image and image class a…
henba1 Nov 23, 2025
db4d465
Fix linter issues
henba1 Nov 23, 2025
a0d3bfd
remove inline comment in save_vnnlib_property()
henba1 Nov 25, 2025
c9d0198
Refactor auto_verify_module slightly and make documentation text in v…
henba1 Nov 23, 2025
afddba4
sdpcrown: embed image/label/epsilon in vnnlib (no npz sidecar)
henba1 Jan 13, 2026
6f047a4
fix docstring misalignment with test
henba1 Jan 13, 2026
ff83bd8
remove redundant data from vnnlib_property
henba1 Jan 13, 2026
1a9d52a
make condition more readable
henba1 Jan 13, 2026
e535ed8
test for sdpcrown metadata
henba1 Jan 13, 2026
1b3281e
Merge branch 'main' into henba1-sdp-crown-changes
henba1 Jan 13, 2026
c6ac570
adjust test to include Ok(CompleteVerificationData(...)
henba1 Jan 13, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
12 changes: 12 additions & 0 deletions ada_verona/database/verification_context.py
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -15,6 +15,7 @@

from pathlib import Path

import numpy as np
import pandas as pd

from ada_verona.database.dataset.data_point import DataPoint
Expand Down Expand Up @@ -87,6 +88,17 @@ def save_vnnlib_property(self, vnnlib_property: VNNLibProperty) -> None:
with open(save_path, "w") as f:
f.write(vnnlib_property.content)
vnnlib_property.path = save_path

# Optionally store additional metadata for verifiers that need direct access
# to the original image and class (e.g. SDP-CROWN).
if vnnlib_property.image is not None or vnnlib_property.image_class is not None:
meta_path = self.tmp_path / f"{vnnlib_property.name}.npz"
np.savez_compressed(
meta_path,
image=vnnlib_property.image,
image_class=-1 if vnnlib_property.image_class is None else vnnlib_property.image_class,
epsilon=-1.0 if vnnlib_property.epsilon is None else vnnlib_property.epsilon,
)

def delete_tmp_path(self) -> None:
"""
Expand Down
5 changes: 5 additions & 0 deletions ada_verona/database/vnnlib_property.py
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -16,6 +16,8 @@
from dataclasses import dataclass
from pathlib import Path

import numpy as np


@dataclass
class VNNLibProperty:
Expand All @@ -24,3 +26,6 @@ class VNNLibProperty:
name: str
content: str
path: Path = None
epsilon: float | None = None
image: np.ndarray | None = None
image_class: int | None = None
8 changes: 7 additions & 1 deletion ada_verona/verification_module/property_generator/one2any_property_generator.py
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -85,7 +85,13 @@ 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,
epsilon=epsilon,
image=image,
image_class=image_class,
)

def get_dict_for_epsilon_result(self) -> dict:
"""
Expand Down
8 changes: 7 additions & 1 deletion ada_verona/verification_module/property_generator/one2one_property_generator.py
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -84,7 +84,13 @@ 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,
epsilon=epsilon,
image=image,
image_class=image_class,
)

def get_dict_for_epsilon_result(self) -> dict:
"""
Expand Down