Skip to content

VERIFIER-C7-01: re-pin C299 negative matcher to observed C7 diagnostic (stacked on #496) #497

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

Draft
d6g8k5htny-coder wants to merge 1 commit into
base: agent8/c299-c7-replacement-20261022
Choose a base branch
from
Draft

VERIFIER-C7-01: re-pin C299 negative matcher to observed C7 diagnostic (stacked on #496) #497

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
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
6 changes: 3 additions & 3 deletions frontiers/critical_ridge_20261020/c299_hosted_verify.py
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -212,7 +212,7 @@ def validate_negative_draft(name, returncode, output):
if (returncode != 1 or output.count('error:') != 1
or any(x in flat.lower() for x in forbidden)):
raise RuntimeError('negative control failed for an unrelated reason')
pattern = (r'\A[^\n]*' + re.escape(name) + r'\.lean:\d+:\d+: error: Type mismatch\s*\n'
pattern = (r'\A[^\n]*' + re.escape(name) + r'\.lean:21:2: error: Type mismatch\s*\n'
r'(?P<expression>.*?)\nhas type\s*\n(?P<actual>.*?)'
r'\nbut is expected to have type\s*\n(?P<expected>.*?)\s*\Z')
match = re.fullmatch(pattern, output.strip(), flags=re.S)
Expand All @@ -234,9 +234,9 @@ def validate_negative_draft(name, returncode, output):
premise = r'\(∀ v ∈ V, v ≠ 0 → hessian d f p v v < 0\)'
if not re.fullmatch(premise + r' → ' + re.escape(expected), actual):
raise RuntimeError('actual type is not the omitted premise followed by the expected conclusion')
# Fixed candidate-2 binder names and all four same-ridge conclusion fields.
# Fixed C7 binder rendering (observed at negative-project L21:2) and all four same-ridge conclusion fields.
conclusion = (r'∃ r, r 0 = 0 ∧ ContDiffAt ℝ 2 r 0 ∧ '
r'\(∀ᶠ w in 𝓝 0, ∀ \(z : ↥V\), \(fderiv ℝ f \(p \+ w \+ ↑\(r w\)\)\) ↑z = 0\) ∧ '
r'\(∀ᶠ \(w : E d\) in 𝓝 0, ∀ \(z : ↥V\), \(fderiv ℝ f \(p \+ w \+ ↑\(r w\)\)\) ↑z = 0\) ∧ '
r'∀ \(w : E d\) \(z : ↥V\), hessian d f p \(w \+ ↑\(\(fderiv ℝ r 0\) w\)\) ↑z = 0')
if not re.fullmatch(conclusion, expected):
raise RuntimeError('expected conclusion does not match all four candidate ridge fields')
Expand Down
9 changes: 6 additions & 3 deletions frontiers/critical_ridge_20261020/test_c299_hosted_verify.py
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -180,10 +180,10 @@ def test_source_preflight_can_collect_before_final_predicate_qualification(self)
def test_inactive_draft_negative_sections_reject_forged_fields(self):
"""Section/token-only matching would accept unrelated existential fields."""
v = self.verifier()
# Synthetic prospective rendering only; no actual Lean diagnostic observed.
# Pinned to the C7 rendering observed locally (Lean v4.34.1) at L21:2.
conclusion = (
'∃ r, r 0 = 0 ∧ ContDiffAt ℝ 2 r 0 ∧ '
'(∀ᶠ w in 𝓝 0, ∀ (z : ↥V), (fderiv ℝ f (p + w + ↑(r w))) ↑z = 0) ∧ '
'(∀ᶠ (w : E d) in 𝓝 0, ∀ (z : ↥V), (fderiv ℝ f (p + w + ↑(r w))) ↑z = 0) ∧ '
'∀ (w : E d) (z : ↥V), hessian d f p (w + ↑((fderiv ℝ r 0) w)) ↑z = 0')
target = 'TorusCriticalRidge.exists_negative_partial_gradient_ridge'
for name, expression, premise in (
Expand All @@ -193,7 +193,7 @@ def test_inactive_draft_negative_sections_reject_forged_fields(self):
('WithoutNegativeDefiniteness',
target + ' f p V hsmooth hcritical',
'(∀ v ∈ V, v ≠ 0 → hessian d f p v v < 0)')):
proper = (name + '.lean:23:2: error: Type mismatch\n ' + expression
proper = (name + '.lean:21:2: error: Type mismatch\n ' + expression
+ '\nhas type\n ' + premise + ' → ' + conclusion
+ '\nbut is expected to have type\n ' + conclusion + '\n')
result = v.validate_negative_draft(name, 1, proper)
Expand All @@ -202,6 +202,9 @@ def test_inactive_draft_negative_sections_reject_forged_fields(self):
for code, bad in (
(0, proper), (-9, proper),
(1, proper.replace(name + '.lean', 'Other.lean')),
(1, proper.replace('.lean:21:2:', '.lean:23:2:')),
(1, proper.replace('.lean:21:2:', '.lean:21:3:')),
(1, proper.replace('(∀ᶠ (w : E d) in', '(∀ᶠ w in')),
(1, proper.replace('ContDiffAt ℝ 2 r 0', 'True')),
(1, proper.replace('fderiv ℝ f', 'fderiv ℝ other')),
(1, proper.replace(premise + ' → ', 'Continuous f → ', 1)),
Expand Down
Loading