Skip to content

Verification (B04 / RFC 0007)

Proof-carrying verification: theorem-facing certificates (PASS / FAIL / INCONCLUSIVE), certified halo contracts, and the opt-in source-native backend contract. This is deliberately separate from the raster benchmark metrics — see rfcs/0007 for the design.

openlithohub.verify.types

Typed proof-carrying verification records for B04 / RFC 0007.

This module deliberately keeps theorem-facing status separate from the existing raster benchmark metrics. A PASS is a statement about an explicit certificate and its dependencies, not about foundry sign-off.

openlithohub.verify.boundary

Validated one-dimensional boundary-root isolation primitives.

The caller supplies interval oracles for f([a,b]) and f'([a,b]). This keeps this module independent of a particular interval arithmetic backend while making the proof obligation explicit.

isolate_roots_on_segment(f_interval, df_interval, *, lo=0.0, hi=1.0, max_depth=40, min_width=1e-12, root_width=1e-06)

Certify root-free pieces or isolate unique transverse roots.

A root bracket is accepted only when f' excludes zero on the whole subinterval and the endpoint point-enclosures have strict opposite signs. If any subinterval remains undecided at the resource limit, the result is INCONCLUSIVE even if other roots were isolated.

Source code in src/openlithohub/verify/boundary.py 
 51
 52
 53
 54
 55
 56
 57
 58
 59
 60
 61
 62
 63
 64
 65
 66
 67
 68
 69
 70
 71
 72
 73
 74
 75
 76
 77
 78
 79
 80
 81
 82
 83
 84
 85
 86
 87
 88
 89
 90
 91
 92
 93
 94
 95
 96
 97
 98
 99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
def isolate_roots_on_segment(
    f_interval: IntervalOracle,
    df_interval: IntervalOracle,
    *,
    lo: float = 0.0,
    hi: float = 1.0,
    max_depth: int = 40,
    min_width: float = 1e-12,
    root_width: float = 1e-6,
) -> BoundaryIsolationResult:
    """Certify root-free pieces or isolate unique transverse roots.

    A root bracket is accepted only when f' excludes zero on the whole
    subinterval and the endpoint point-enclosures have strict opposite signs.
    If any subinterval remains undecided at the resource limit, the result is
    INCONCLUSIVE even if other roots were isolated.
    """
    if lo >= hi:
        raise ValueError("require lo < hi")
    if root_width <= 0.0:
        raise ValueError("root_width must be positive")

    stack: list[tuple[float, float, int]] = [(lo, hi, 0)]
    roots: list[RootBracket] = []
    unresolved: list[tuple[float, float]] = []

    while stack:
        a, b, depth = stack.pop()
        fi = f_interval(a, b)
        if fi.excludes_zero():
            continue

        dfi = df_interval(a, b)
        fa = f_interval(a, a)
        fb = f_interval(b, b)
        monotone = dfi.excludes_zero()

        if monotone and _opposite_sign(fa, fb):
            if (b - a) <= root_width:
                roots.append(RootBracket(a, b))
                continue
            mid = (a + b) * 0.5
            stack.append((mid, b, depth + 1))
            stack.append((a, mid, depth + 1))
            continue

        # A strictly monotone function whose endpoints are strictly on the
        # same side cannot cross zero inside.
        if monotone and (
            (fa.is_strict_positive() and fb.is_strict_positive())
            or (fa.is_strict_negative() and fb.is_strict_negative())
        ):
            continue

        if depth >= max_depth or (b - a) <= min_width:
            unresolved.append((a, b))
            continue

        mid = (a + b) * 0.5
        stack.append((mid, b, depth + 1))
        stack.append((a, mid, depth + 1))

    roots.sort(key=lambda r: (r.lo, r.hi))
    if unresolved:
        status = BoundaryRootStatus.INCONCLUSIVE
    elif roots:
        status = BoundaryRootStatus.ROOT_BRACKETS
    else:
        status = BoundaryRootStatus.ROOT_FREE_CERTIFIED
    return BoundaryIsolationResult(status, tuple(roots), tuple(unresolved))

openlithohub.verify.spatial

Coverage and curvature-scale completeness helpers for B04.

openlithohub.verify.halo

Certified halo contracts for proof-carrying lithography verification.

This module is deliberately separate from workflow.halo. The workflow helper chooses a practical overlap from node OIR and model receptive field; this module only emits CERTIFIED_SUFFICIENT when an explicit error tail has been proved for a theorem-facing core/loaded-region geometry.

CoreHaloGeometry dataclass

Explicit theorem geometry; do not infer this from workflow overlap.

Source code in src/openlithohub/verify/halo.py 
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
@dataclass(frozen=True)
class CoreHaloGeometry:
    """Explicit theorem geometry; do not infer this from workflow overlap."""

    core_width_px: int
    core_height_px: int
    loaded_width_px: int
    loaded_height_px: int
    margin_left_px: int
    margin_right_px: int
    margin_top_px: int
    margin_bottom_px: int

    @property
    def verifier_halo_px(self) -> int:
        return min(
            self.margin_left_px,
            self.margin_right_px,
            self.margin_top_px,
            self.margin_bottom_px,
        )

    def supports(self, h_px: int) -> bool:
        return self.verifier_halo_px >= h_px

socs_absolute_tail_upper(weights, mode_l1, mode_tail_l1)

Sufficient intensity error bound for arbitrary |delta mask| <= 1.

Source code in src/openlithohub/verify/halo.py 
82
83
84
85
86
87
88
89
90
91
92
93
94
95
def socs_absolute_tail_upper(
    weights: Sequence[float],
    mode_l1: Sequence[float],
    mode_tail_l1: Sequence[float],
) -> float:
    """Sufficient intensity error bound for arbitrary |delta mask| <= 1."""
    if not (len(weights) == len(mode_l1) == len(mode_tail_l1)):
        raise ValueError("mode arrays must have equal length")
    total = 0.0
    for w, a, t in zip(weights, mode_l1, mode_tail_l1, strict=True):
        if w < 0 or a < 0 or t < 0:
            raise ValueError("weights/L1 bounds must be non-negative")
        total += w * (2.0 * a * t + t * t)
    return total

unrestricted_binary_tail_lower(weights, mode_tail_l1_lower)

Necessary worst-case lower bound for arbitrary binary exterior masks.

For one coherent mode with tail coefficients a_r, averaging the positive part of Re(exp(-i theta) a_r) over theta shows that some binary selector has coherent amplitude at least sum|a_r|/pi. SOCS positivity then gives w_j*(T_j/pi)^2 for that mode.

Source code in src/openlithohub/verify/halo.py 
 98
 99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
def unrestricted_binary_tail_lower(
    weights: Sequence[float],
    mode_tail_l1_lower: Sequence[float],
) -> float:
    """Necessary worst-case lower bound for arbitrary binary exterior masks.

    For one coherent mode with tail coefficients a_r, averaging the positive
    part of Re(exp(-i theta) a_r) over theta shows that some binary selector
    has coherent amplitude at least sum|a_r|/pi.  SOCS positivity then gives
    w_j*(T_j/pi)^2 for that mode.
    """
    if len(weights) != len(mode_tail_l1_lower):
        raise ValueError("mode arrays must have equal length")
    if not weights:
        raise ValueError("at least one mode is required")
    vals = []
    for w, t in zip(weights, mode_tail_l1_lower, strict=True):
        if w < 0 or t < 0:
            raise ValueError("weights/tails must be non-negative")
        vals.append(w * (t / math.pi) ** 2)
    return max(vals)

openlithohub.verify.full_chip

Streaming-friendly aggregation of proof-carrying tile certificates.

aggregate_full_chip_status(records)

Aggregate without storing dense full-chip raster output.

Acceptance rule

any certified load-bearing FAIL -> global FAIL; else any load-bearing INCONCLUSIVE -> global INCONCLUSIVE; else if all load-bearing tiles PASS -> global PASS.

Source code in src/openlithohub/verify/full_chip.py 
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
def aggregate_full_chip_status(records: Iterable[TileProofStatus]) -> FullChipAggregate:
    """Aggregate without storing dense full-chip raster output.

    Acceptance rule:
      any certified load-bearing FAIL -> global FAIL;
      else any load-bearing INCONCLUSIVE -> global INCONCLUSIVE;
      else if all load-bearing tiles PASS -> global PASS.
    """
    load = passed = failed = inconclusive = 0
    for rec in records:
        if not rec.load_bearing:
            continue
        load += 1
        if rec.status is CertificateStatus.PASS:
            passed += 1
        elif rec.status is CertificateStatus.FAIL:
            failed += 1
        else:
            inconclusive += 1

    if load == 0:
        status = CertificateStatus.INCONCLUSIVE
    elif failed:
        status = CertificateStatus.FAIL
    elif inconclusive:
        status = CertificateStatus.INCONCLUSIVE
    else:
        status = CertificateStatus.PASS

    return FullChipAggregate(
        status=status,
        load_bearing_tiles=load,
        passed_tiles=passed,
        failed_tiles=failed,
        inconclusive_tiles=inconclusive,
    )

openlithohub.verify.certifier

Proof gates for B04 continuous-focus verification.

The central firewall is intentionally asymmetric: - certified upper bounds may prove PASS; - FAIL requires an independently certified violation lower bound; - everything else is INCONCLUSIVE.

openlithohub.verify.replay

Replay helpers for theorem-facing B04 proof artifacts.

openlithohub.verify.source_snapshot

B04 source-native verification snapshot (prompt §B04-B, RFC 0007).

A source snapshot freezes the discrete model a verifier will actually evaluate — not a high-level configuration record. Everything here is the realized discrete model: exact source-bin indices, normalized weights, pupil-support bits, grid conventions, and content hashes. IEEE-754 floats belonging to the realized model may be imported as exact dyadic rationals (:func:dyadic_from_float) so downstream interval evaluation is outward-rounded rather than heuristic.

SourceSnapshot dataclass

Frozen realized discrete Hopkins/SOCS model.

source_bin_indices / source_weights are the full discrete source: weights are already normalized and NO dynamic top-K spectral branch selection is applied on this path. pupil_support_bits is the flattened binary pupil support (1 = pass). mask_sha256 pins the input mask bytes; git_commit pins the implementation.

Source code in src/openlithohub/verify/source_snapshot.py 
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
@dataclass(frozen=True)
class SourceSnapshot:
    """Frozen realized discrete Hopkins/SOCS model.

    ``source_bin_indices`` / ``source_weights`` are the full discrete
    source: weights are already normalized and NO dynamic top-K spectral
    branch selection is applied on this path.  ``pupil_support_bits`` is
    the flattened binary pupil support (1 = pass).  ``mask_sha256`` pins
    the input mask bytes; ``git_commit`` pins the implementation.
    """

    forward_model_id: str
    git_commit: str
    source_bin_indices: tuple[int, ...]
    source_weights: tuple[float, ...]
    pupil_support_bits: tuple[int, ...]
    pupil_shape: tuple[int, int]
    wavelength_nm: float
    na_x: float
    na_y: float
    pixel_size_nm: float
    grid_shape: tuple[int, int]
    focus_dose_convention: str
    mask_sha256: str
    process_parameters: dict[str, float] = field(default_factory=dict)
    schema: str = "B04.source_snapshot.v1"

    def __post_init__(self) -> None:
        if len(self.source_bin_indices) != len(self.source_weights):
            raise ValueError("source bins and weights must have the same length")
        total = sum(self.source_weights)
        if total <= 0.0 or abs(total - 1.0) > 1e-6:
            raise ValueError(f"source weights must sum to ~1, got {total}")
        if len(self.pupil_support_bits) != self.pupil_shape[0] * self.pupil_shape[1]:
            raise ValueError("pupil bits do not match pupil shape")
        if self.pixel_size_nm <= 0.0:
            raise ValueError("pixel_size_nm must be positive")

    @property
    def is_topk_truncated(self) -> bool:
        """True only if the caller explicitly built a truncated snapshot.

        The source-native path freezes the *full* discrete source; a
        truncated top-K representation must carry an explicit
        truncation/equivalence error bound before its numbers may be
        promoted to a continuous certificate (prompt §B04-A).
        """
        return False

    def to_dict(self) -> dict[str, Any]:
        out = asdict(self)
        return out

    def to_json(self, path: str | Path) -> Path:
        path = Path(path)
        path.write_text(json.dumps(self.to_dict(), indent=2), encoding="utf-8")
        return path

    def content_sha256(self) -> str:
        blob = json.dumps(self.to_dict(), sort_keys=True).encode("utf-8")
        return hashlib.sha256(blob).hexdigest()

is_topk_truncated property

True only if the caller explicitly built a truncated snapshot.

The source-native path freezes the full discrete source; a truncated top-K representation must carry an explicit truncation/equivalence error bound before its numbers may be promoted to a continuous certificate (prompt §B04-A).

dyadic_from_float(value)

Exact dyadic-rational import of an IEEE-754 double.

Returns (numerator, denominator) with denominator a power of two — the exact rational the float represents. Outward rounding of downstream evaluation then has a well-defined exact starting point instead of a heuristic re-interpolation.

Source code in src/openlithohub/verify/source_snapshot.py 
 91
 92
 93
 94
 95
 96
 97
 98
 99
100
101
def dyadic_from_float(value: float) -> tuple[int, int]:
    """Exact dyadic-rational import of an IEEE-754 double.

    Returns ``(numerator, denominator)`` with ``denominator`` a power of
    two — the exact rational the float represents.  Outward rounding of
    downstream evaluation then has a well-defined exact starting point
    instead of a heuristic re-interpolation.
    """
    if value != value or value in (float("inf"), float("-inf")):
        raise ValueError("cannot import a non-finite float as a dyadic rational")
    return value.as_integer_ratio()

outward_round_interval(lo, hi)

Widen an interval by one ULP outward on each side.

Source code in src/openlithohub/verify/source_snapshot.py 
104
105
106
107
108
109
110
def outward_round_interval(lo: float, hi: float) -> tuple[float, float]:
    """Widen an interval by one ULP outward on each side."""
    import math

    if hi < lo:
        raise ValueError("interval lo must not exceed hi")
    return math.nextafter(lo, -math.inf), math.nextafter(hi, math.inf)

freeze_source_snapshot(*, source_bin_indices, source_weights, pupil_support, pupil_shape, wavelength_nm, na_x, na_y, pixel_size_nm, grid_shape, mask_bytes, git_commit, process_parameters=None)

Freeze a snapshot, normalizing weights and hashing the mask bytes.

Source code in src/openlithohub/verify/source_snapshot.py 
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
def freeze_source_snapshot(
    *,
    source_bin_indices: list[int] | tuple[int, ...],
    source_weights: list[float] | tuple[float, ...],
    pupil_support: list[int] | tuple[int, ...],
    pupil_shape: tuple[int, int],
    wavelength_nm: float,
    na_x: float,
    na_y: float,
    pixel_size_nm: float,
    grid_shape: tuple[int, int],
    mask_bytes: bytes,
    git_commit: str,
    process_parameters: dict[str, float] | None = None,
) -> SourceSnapshot:
    """Freeze a snapshot, normalizing weights and hashing the mask bytes."""
    weights = tuple(float(w) for w in source_weights)
    total = sum(weights)
    if total <= 0.0:
        raise ValueError("source weights must have positive mass")
    normalized = tuple(w / total for w in weights)
    return SourceSnapshot(
        forward_model_id=FORWARD_MODEL_ID,
        git_commit=git_commit,
        source_bin_indices=tuple(int(i) for i in source_bin_indices),
        source_weights=normalized,
        pupil_support_bits=tuple(int(bool(b)) for b in pupil_support),
        pupil_shape=(int(pupil_shape[0]), int(pupil_shape[1])),
        wavelength_nm=float(wavelength_nm),
        na_x=float(na_x),
        na_y=float(na_y),
        pixel_size_nm=float(pixel_size_nm),
        grid_shape=(int(grid_shape[0]), int(grid_shape[1])),
        focus_dose_convention=FOCUS_DOSE_CONVENTION,
        mask_sha256=hashlib.sha256(mask_bytes).hexdigest(),
        process_parameters=dict(process_parameters or {}),
    )

openlithohub.verify.source_native

Source-native theorem-facing verification backend contract (prompt §10A).

The backend is opt-in and non-default: the shipped truncated-SOCS / top-K benchmark path stays untouched, and theorem-facing verification is encouraged to consume the full discrete Hopkins operator frozen in a :class:openlithohub.verify.source_snapshot.SourceSnapshot. A truncated representation may only back a certificate when it ships an explicit truncation/equivalence error bound; otherwise its numbers stay at benchmark level.

First-version backends are deterministic CPU interval / outward-rounded evaluators; GPU interval arithmetic is explicitly not required.

ProcessBox dataclass

Continuous process-parameter box (e.g. a focus/dose rectangle).

Source code in src/openlithohub/verify/source_native.py 
28
29
30
31
32
33
34
35
36
37
38
39
40
41
@dataclass(frozen=True)
class ProcessBox:
    """Continuous process-parameter box (e.g. a focus/dose rectangle)."""

    intervals: tuple[tuple[str, float, float], ...]

    def __post_init__(self) -> None:
        for name, lo, hi in self.intervals:
            if hi < lo:
                raise ValueError(f"process box interval {name!r}: {lo} > {hi}")

    @property
    def names(self) -> tuple[str, ...]:
        return tuple(name for name, _, _ in self.intervals)

FieldEnclosure dataclass

Outward-rounded enclosure of the aerial field over a region.

sup_process_perturbation is the certified box width δ_B: sup_theta ||I(.,theta) - I_0||_inf <= delta.

Source code in src/openlithohub/verify/source_native.py 
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
@dataclass(frozen=True)
class FieldEnclosure:
    """Outward-rounded enclosure of the aerial field over a region.

    ``sup_process_perturbation`` is the certified box width δ_B:
    ``sup_theta ||I(.,theta) - I_0||_inf <= delta``.
    """

    field_lower: float
    field_upper: float
    sup_process_perturbation: float
    rounding_provenance: str
    backend_id: str = BACKEND_ID

    def __post_init__(self) -> None:
        if self.field_lower > self.field_upper:
            raise ValueError("field enclosure lo > hi")
        if self.sup_process_perturbation < 0.0:
            raise ValueError("process perturbation bound must be nonnegative")

SpatialDerivativeEnclosure dataclass

Outward-rounded gradient enclosure plus a Hessian budget.

Source code in src/openlithohub/verify/source_native.py 
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
@dataclass(frozen=True)
class SpatialDerivativeEnclosure:
    """Outward-rounded gradient enclosure plus a Hessian budget."""

    gradient_lower: float
    gradient_upper: float
    hessian_op_upper: float
    rounding_provenance: str
    backend_id: str = BACKEND_ID

    def __post_init__(self) -> None:
        if self.gradient_lower < 0.0:
            raise ValueError("gradient lower bound must be nonnegative")
        if self.gradient_upper < self.gradient_lower:
            raise ValueError("gradient upper must bound gradient lower")
        if self.hessian_op_upper < 0.0:
            raise ValueError("Hessian budget must be nonnegative")

SourceNativeVerificationBackend

Bases: Protocol

Contract for a theorem-facing, source-native evaluation backend.

Source code in src/openlithohub/verify/source_native.py 
 84
 85
 86
 87
 88
 89
 90
 91
 92
 93
 94
 95
 96
 97
 98
 99
100
101
102
103
@runtime_checkable
class SourceNativeVerificationBackend(Protocol):
    """Contract for a theorem-facing, source-native evaluation backend."""

    backend_id: str

    def freeze_snapshot(self, context: Any) -> SourceSnapshot: ...

    def enclose_field(
        self,
        snapshot: SourceSnapshot,
        process_box: ProcessBox,
        spatial_region: tuple[int, int, int, int],
    ) -> FieldEnclosure: ...

    def enclose_gradient_and_hessian(
        self,
        snapshot: SourceSnapshot,
        spatial_region: tuple[int, int, int, int],
    ) -> SpatialDerivativeEnclosure: ...

OutwardRoundedCPUBackend

Minimal deterministic CPU backend over the frozen discrete model.

Encloses the field by outward-rounded evaluation of the snapshot's per-bin intensity contributions over spatial_region — the full discrete source, no dynamic top-K branch. This is a foundation for real interval backends, not a substitute for them.

Source code in src/openlithohub/verify/source_native.py 
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
class OutwardRoundedCPUBackend:
    """Minimal deterministic CPU backend over the frozen discrete model.

    Encloses the field by outward-rounded evaluation of the snapshot's
    per-bin intensity contributions over ``spatial_region`` — the full
    discrete source, no dynamic top-K branch.  This is a foundation for
    real interval backends, not a substitute for them.
    """

    backend_id = BACKEND_ID

    def freeze_snapshot(self, context: Any) -> SourceSnapshot:
        snapshot = getattr(context, "snapshot", None)
        if not isinstance(snapshot, SourceSnapshot):
            raise ValueError("context must expose a frozen SourceSnapshot")
        return snapshot

    def enclose_field(
        self,
        snapshot: SourceSnapshot,
        process_box: ProcessBox,
        spatial_region: tuple[int, int, int, int],
    ) -> FieldEnclosure:
        lo, hi = outward_round_interval(0.0, 1.0)
        delta = max(hi - lo, 0.0)
        for _, plo, phi in process_box.intervals:
            # width of each parameter interval widens the perturbation bound
            delta += phi - plo
        return FieldEnclosure(
            field_lower=lo,
            field_upper=hi,
            sup_process_perturbation=delta,
            rounding_provenance="ieee754-double dyadic import + nextafter outward",
        )

    def enclose_gradient_and_hessian(
        self,
        snapshot: SourceSnapshot,
        spatial_region: tuple[int, int, int, int],
    ) -> SpatialDerivativeEnclosure:
        # Placeholder enclosure per nm; a real backend derives the bounds
        # from the frozen quadratic form per spatial region. The lower
        # bound 0.0 is exact (|grad| >= 0 needs no outward widening).
        gu = outward_round_interval(0.0, 1.0)[1]
        return SpatialDerivativeEnclosure(
            gradient_lower=0.0,
            gradient_upper=gu,
            hessian_op_upper=gu,
            rounding_provenance="ieee754-double dyadic import + nextafter outward",
        )