Skip to content

Conversation

@henba1
Copy link
Collaborator

@henba1 henba1 commented Nov 23, 2025

Introduce VNNLib sidecar for SDP-CROWN that carries image and image_class.

For SDPCrown, carrying the image alongside the VNNLIB property is the cleaner and less error‑prone design than trying to reconstruct a BoundedTensor inside SDP-CROWN from the VNNLIB text.

@henba1 henba1 requested review from AWbosman and Aaron99B November 23, 2025 17:10
@henba1 henba1 self-assigned this Nov 23, 2025
@henba1 henba1 changed the title Henba1 sdp crown changes Introduce VNNLib .npz sidecar in save_vnnlib_property() for image, image_class and epsilon Nov 23, 2025
@codecov
Copy link

codecov bot commented Nov 23, 2025

Codecov Report

✅ All modified and coverable lines are covered by tests.

📢 Thoughts on this report? Let us know!

Copy link
Collaborator

@Aaron99B Aaron99B left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The image is already included in the verification context in the data point. Why do we need it another time?

@henba1
Copy link
Collaborator Author

henba1 commented Nov 25, 2025

The image is already included in the verification context in the data point. Why do we need it another time?

VerificationContext is VERONA-internal state by design of the current auto_verify_module.py, which from verification_context only passes along verification_context.network.path to the verifier via verify_property(...).

Recall that auto-verify verifier API is
def verify_property(
self,
network: Path,
property: Path,
*,
config: Configuration | Path | None = None,
timeout: int = DEFAULT_VERIFICATION_TIMEOUT_SEC,
) -> CompleteVerificationResult:

But SDP-CROWN needs image, image_class/label and epsilon. Thats why we attach it to VNNLib_property

@Aaron99B
Copy link
Collaborator

Can't we include SDP-Crown using a different interface? I would refrain from putting the same image twice in the verification context

@henba1 henba1 changed the title Introduce VNNLib .npz sidecar in save_vnnlib_property() for image, image_class and epsilon L_2: Introduce metadata part in .vnnlib file to persist image, image_class and epsilon for SDP-CROWN Jan 13, 2026
@henba1 henba1 merged commit 03c0593 into main Jan 13, 2026
4 checks passed
@henba1 henba1 deleted the henba1-sdp-crown-changes branch January 13, 2026 15:49
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants