Fix Lean guard verifier negation parsing (#1315)

* fix lean guard verifier negation parsing

* ci: allow Lean runtime lane to finish

---------

Co-authored-by: morluto <76467478+morluto@users.noreply.github.com>

Author: yuelgrace1810-ops

.github/workflows/ci.yml

@@ -200,7 +200,7 @@ jobs:
   lean:
     name: Lean Runtime
     runs-on: ubuntu-latest
-    timeout-minutes: 20
+    timeout-minutes: 30
     steps:
       - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1
         with:

benchmarks/datasets/mathematical-benchmarks-v1/lean-guard-scope-assurance/tests/Dockerfile

@@ -1,6 +1,6 @@
 FROM python:3.12-slim@sha256:57cd7c3a7a273101a6485ba99423ee568157882804b1124b4dd04266317710de
 RUN python -m pip install --no-cache-dir attrs==26.1.0 jsonschema==4.26.0 jsonschema-specifications==2025.9.1 referencing==0.37.0 rpds-py==2026.6.3 typing-extensions==4.16.0
-LABEL jacobian.checksum="ee7fce1e17e0ff36dc68add1648233edeafcef6ae67f567bc7d93c2fb6ce2e7d"
+LABEL jacobian.checksum="095a8c611a726fb7cac8964c0f85fd3db12ec89b9549c8398bb9b948215ef3ab"
 LABEL jacobian.task="jacobian/lean-guard-scope-assurance"
 COPY expected.json input.json test.sh verifier.py verifier_support.py public_contract.json /tests/
 COPY input.json /app/input.json

benchmarks/datasets/mathematical-benchmarks-v1/lean-guard-scope-assurance/tests/verifier.py

@@ -95,7 +95,7 @@ def _result_item_ok(item, case):
                 reason_text,
             )
             or re.search(
-                r"\b(?:no|not)\b[^.;\n]{0,40}\b(?:division|divisor)\b",
+                r"\b(?:no|not)\b[^.;\n]{0,40}\bdivision\s+by\s+zero\b",
                 reason_text,
             )
         )

benchmarks/validation/mathematical_benchmarks_v1/test_lean_guard_scope_assurance.py

@@ -0,0 +1,54 @@
+from __future__ import annotations
+
+import importlib.util
+import sys
+from pathlib import Path
+
+ROOT = Path(__file__).parents[3]
+TASK = (
+    ROOT / "benchmarks/datasets/mathematical-benchmarks-v1/lean-guard-scope-assurance"
+)
+
+
+def _module():
+    sys.path.insert(0, str(TASK / "tests"))
+    spec = importlib.util.spec_from_file_location(
+        "lean_guard_scope_assurance_verifier", TASK / "tests/verifier.py"
+    )
+    assert spec and spec.loader
+    module = importlib.util.module_from_spec(spec)
+    spec.loader.exec_module(module)
+    return module
+
+
+def _allzero_bad_guard_case() -> dict[str, object]:
+    return {
+        "id": "allzero_bad_lt_guard",
+        "ofnat_zero_equals_one": True,
+        "lt_is_universal": True,
+    }
+
+
+def test_accepts_negated_guard_strength_with_positive_zero_divisor_finding() -> None:
+    module = _module()
+    item = {
+        "id": "allzero_bad_lt_guard",
+        "findings": ["DIVISION_BY_ZERO"],
+        "reason": (
+            "The universal order guard does not supply a sound nonzero divisor "
+            "fact, so the divisor remains semantically zero."
+        ),
+    }
+
+    assert module._result_item_ok(item, _allzero_bad_guard_case())
+
+
+def test_rejects_reason_that_denies_division_by_zero() -> None:
+    module = _module()
+    item = {
+        "id": "allzero_bad_lt_guard",
+        "findings": ["DIVISION_BY_ZERO"],
+        "reason": "There is not division by zero because the divisor is safe.",
+    }
+
+    assert not module._result_item_ok(item, _allzero_bad_guard_case())