Skip to content

Commit 13377dd

Browse files
dsymedsyme
committed
update lean squad
1 parent 51c8f6a commit 13377dd

1 file changed

Lines changed: 175 additions & 7 deletions

File tree

‎workflows/lean-squad.md‎

Lines changed: 175 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -136,7 +136,8 @@ steps:
136136
> /tmp/gh-aw/fv_prs.json || echo "[]" > /tmp/gh-aw/fv_prs.json
137137
138138
python3 - << 'EOF'
139-
import json, os, random
139+
import json, os, random, re
140+
from pathlib import Path
140141
141142
lean_count = int(open('/tmp/gh-aw/lean_count.txt').read().strip() or 0)
142143
rust_count = int(open('/tmp/gh-aw/rust_count.txt').read().strip() or 0)
@@ -155,6 +156,130 @@ steps:
155156
n_issues = len(fv_issues)
156157
n_prs = len(fv_prs)
157158
159+
# Inspect handwritten Lean artifacts to estimate proof maturity.
160+
fvsquad_dir = Path('formal-verification/lean/FVSquad')
161+
handwritten_lean_files = []
162+
if fvsquad_dir.exists():
163+
handwritten_lean_files = [
164+
p for p in fvsquad_dir.rglob('*.lean')
165+
if 'Aeneas/Generated' not in p.as_posix() and '/.lake/' not in p.as_posix()
166+
]
167+
168+
spec_dir = Path('formal-verification/specs')
169+
informal_spec_count = len(list(spec_dir.glob('*_informal.md'))) if spec_dir.exists() else 0
170+
171+
theorem_decl_re = re.compile(r'^\s*(theorem|lemma)\s+\w+', re.M)
172+
sorry_re = re.compile(r'\bsorry\b')
173+
import_re = re.compile(r'^\s*import\s+FVSquad\.(\w+)', re.M)
174+
composition_theorem_re = re.compile(
175+
r'^\s*(theorem|lemma)\s+\w*(compose|composition|equiv|correspond|refine|sound|complete|end_to_end|e2e|bridge|commute|simulation)\w*',
176+
re.M,
177+
)
178+
179+
theorem_count = 0
180+
files_with_sorry = 0
181+
files_without_theorems = 0
182+
cross_file_theorem_files = 0
183+
composition_theorem_count = 0
184+
target_names_from_lean = set()
185+
186+
for lean_file in handwritten_lean_files:
187+
try:
188+
text = lean_file.read_text(encoding='utf-8', errors='ignore')
189+
except Exception:
190+
continue
191+
192+
target_names_from_lean.add(lean_file.stem.lower())
193+
local_theorems = len(theorem_decl_re.findall(text))
194+
theorem_count += local_theorems
195+
if local_theorems == 0:
196+
files_without_theorems += 1
197+
if sorry_re.search(text):
198+
files_with_sorry += 1
199+
200+
if local_theorems > 0 and import_re.search(text):
201+
cross_file_theorem_files += 1
202+
composition_theorem_count += len(composition_theorem_re.findall(text))
203+
204+
handwritten_lean_file_count = len(handwritten_lean_files)
205+
206+
# Parse target coverage from TARGETS.md so proof maturity tracks declared scope,
207+
# not just local theorem/sorry counts.
208+
targets_file = Path('formal-verification/TARGETS.md')
209+
targets_declared_count = 0
210+
targets_phase4plus_count = 0
211+
target_names_from_targets = set()
212+
if targets_file.exists():
213+
try:
214+
targets_text = targets_file.read_text(encoding='utf-8', errors='ignore')
215+
except Exception:
216+
targets_text = ''
217+
218+
target_line_re = re.compile(r'^\s*(?:[-*]\s+)?(?:\d+[.)]\s+)?(?:\*\*)?([A-Za-z0-9_./:-][A-Za-z0-9_ ./:-]{1,100}?)(?:\*\*)?\s*(?:\||$)', re.M)
219+
phase_re = re.compile(r'phase\s*[:=\-]?\s*(\d+)', re.I)
220+
221+
for line in targets_text.splitlines():
222+
line_l = line.lower()
223+
if not line_l.strip():
224+
continue
225+
if any(skip in line_l for skip in ['target', 'phase', 'status', 'priority', 'owner', 'notes']) and '|' in line_l:
226+
continue
227+
228+
m = target_line_re.match(line)
229+
if not m:
230+
continue
231+
name = m.group(1).strip(' -:').lower()
232+
if len(name) < 2:
233+
continue
234+
if any(name.startswith(prefix) for prefix in ['http', 'todo', 'note', 'summary']):
235+
continue
236+
target_names_from_targets.add(name)
237+
238+
pm = phase_re.search(line)
239+
if pm and int(pm.group(1)) >= 4:
240+
targets_phase4plus_count += 1
241+
242+
targets_declared_count = len(target_names_from_targets)
243+
244+
# Infer target names from informal specs as another signal of intended coverage.
245+
target_names_from_specs = set()
246+
if spec_dir.exists():
247+
for spec_file in spec_dir.glob('*_informal.md'):
248+
target_names_from_specs.add(spec_file.stem.replace('_informal', '').lower())
249+
250+
inferred_target_count = max(
251+
targets_declared_count,
252+
len(target_names_from_specs),
253+
handwritten_lean_file_count,
254+
)
255+
256+
proved_like_target_count = 0
257+
for lean_file in handwritten_lean_files:
258+
try:
259+
text = lean_file.read_text(encoding='utf-8', errors='ignore')
260+
except Exception:
261+
continue
262+
local_theorems = len(theorem_decl_re.findall(text))
263+
local_sorry = bool(sorry_re.search(text))
264+
if local_theorems > 0 and not local_sorry:
265+
proved_like_target_count += 1
266+
267+
# Coverage floor: we want broad target coverage and not just isolated local wins.
268+
target_proof_coverage = (
269+
proved_like_target_count / inferred_target_count
270+
if inferred_target_count > 0 else 0.0
271+
)
272+
target_coverage_incomplete = inferred_target_count >= 2 and target_proof_coverage < 0.6
273+
274+
# Composition floor: if we have multiple Lean targets, require some cross-file proof signal.
275+
composition_incomplete = handwritten_lean_file_count >= 2 and (
276+
cross_file_theorem_files == 0 and composition_theorem_count == 0
277+
)
278+
279+
# Heuristic target: each started target/spec should usually have multiple theorems,
280+
# and each handwritten Lean file should contribute proof obligations.
281+
expected_theorem_floor = max(3, informal_spec_count * 2, handwritten_lean_file_count * 2)
282+
158283
task_names = {
159284
1: 'Research & Target Identification',
160285
2: 'Informal Spec Extraction',
@@ -175,23 +300,34 @@ steps:
175300
has_inf_specs = fv_docs >= 2 or lean_count >= 1
176301
has_lean_specs = lean_count >= 1
177302
has_impl = lean_count >= 3
178-
has_proofs = lean_count >= 6
303+
has_proofs = theorem_count >= 1
179304
has_rust = rust_count >= 1
180305
has_ci = bool(has_lean_ci)
181306
has_correspondence_tests = correspondence_test_count >= 1
182307
308+
proof_incomplete = has_impl and (
309+
files_with_sorry > 0
310+
or files_without_theorems > 0
311+
or theorem_count < expected_theorem_floor
312+
or target_coverage_incomplete
313+
or composition_incomplete
314+
)
315+
proof_mature = has_impl and not proof_incomplete
316+
183317
weights = {
184318
1: 10.0 if not has_research else 2.0,
185319
2: (8.0 if not has_inf_specs else 2.0) if has_research else 0.5,
186320
3: (8.0 if not has_lean_specs else 2.0) if has_inf_specs else 0.3,
187321
4: (6.0 if not has_impl else 2.0) if has_lean_specs else 0.2,
188-
5: (6.0 if not has_proofs else 2.0) if has_impl else 0.1,
322+
# Keep proof work highly weighted until we have stronger evidence of maturity.
323+
# This avoids prematurely deprioritizing proofs just because Lean files exist.
324+
5: (12.0 if proof_incomplete else 3.0) if has_impl else 0.1,
189325
6: (10.0 if not has_correspondence else 3.0) if has_impl else 0.5, # correspondence: critical when impl exists but no doc
190-
7: (10.0 if not has_critique else 3.0) if has_proofs else 0.0, # critique: critical when proofs exist but no doc
326+
7: (4.0 if not has_critique else 2.0) if proof_incomplete else ((10.0 if not has_critique else 3.0) if has_proofs else 0.0), # while proofs are incomplete, critique is useful but secondary
191327
8: (12.0 if not has_correspondence_tests else (5.0 if has_rust else 3.0)) if has_impl else 0.2, # correspondence validation: critical once an implementation model exists, especially before runnable tests exist
192328
9: 12.0 if (has_lean_specs and not has_ci) else 2.0, # CI: critical when lean files exist but no CI; regular check otherwise
193-
10: (8.0 if not has_report else 3.0) if has_proofs else (2.0 if has_lean_specs else 0.0), # report: important when proofs exist but no report; available once lean specs exist
194-
11: (8.0 if not has_paper else 3.0) if has_proofs else 0.0, # paper: important when proofs exist but no paper; only available once proofs exist
329+
10: (3.0 if not has_report else 2.0) if proof_incomplete else ((8.0 if not has_report else 3.0) if has_proofs else (2.0 if has_lean_specs else 0.0)), # defer heavy reporting until proof maturity improves
330+
11: (2.0 if not has_paper else 1.0) if proof_incomplete else ((8.0 if not has_paper else 3.0) if has_proofs else 0.0), # defer paper emphasis while proofs are still incomplete
195331
}
196332
197333
run_id = int(os.environ.get('GITHUB_RUN_ID', '0'))
@@ -214,13 +350,28 @@ steps:
214350
print(f'Corr. tests : {correspondence_test_count}')
215351
print(f'FV dir : {bool(fv_dir)}')
216352
print(f'FV docs : {fv_docs}')
353+
print(f'Informal specs: {informal_spec_count}')
354+
print(f'Handwritten Lean files: {handwritten_lean_file_count}')
355+
print(f'Theorem/lemma declarations: {theorem_count}')
356+
print(f'Files with sorry: {files_with_sorry}')
357+
print(f'Files without theorem/lemma: {files_without_theorems}')
358+
print(f'Cross-file theorem files: {cross_file_theorem_files}')
359+
print(f'Composition theorem count: {composition_theorem_count}')
360+
print(f'Expected theorem floor: {expected_theorem_floor}')
361+
print(f'Declared targets (TARGETS.md): {targets_declared_count}')
362+
print(f'Inferred targets (overall): {inferred_target_count}')
363+
print(f'Proved-like targets: {proved_like_target_count}')
364+
print(f'Target proof coverage: {target_proof_coverage:.2f}')
217365
print(f'Open issues : {n_issues}')
218366
print(f'Open FV PRs : {n_prs}')
219367
print(f'Phase flags : research={has_research}, inf_specs={has_inf_specs}, '
220368
f'lean_specs={has_lean_specs}, impl={has_impl}, proofs={has_proofs}, '
221369
f'rust={has_rust}, ci={has_ci}, '
222370
f'correspondence_tests={has_correspondence_tests}, '
223-
f'correspondence={bool(has_correspondence)}, critique={bool(has_critique)}, '
371+
f'correspondence={bool(has_correspondence)}, critique={bool(has_critique)}, '
372+
f'proof_incomplete={proof_incomplete}, proof_mature={proof_mature}, '
373+
f'target_coverage_incomplete={target_coverage_incomplete}, '
374+
f'composition_incomplete={composition_incomplete}, '
224375
f'report={bool(has_report)}, paper={bool(has_paper)}')
225376
print()
226377
print('Task weights:')
@@ -234,13 +385,30 @@ steps:
234385
'lean_count': lean_count, 'rust_count': rust_count,
235386
'fv_dir': bool(fv_dir), 'fv_docs': fv_docs,
236387
'correspondence_test_count': correspondence_test_count,
388+
'informal_spec_count': informal_spec_count,
389+
'handwritten_lean_file_count': handwritten_lean_file_count,
390+
'theorem_count': theorem_count,
391+
'files_with_sorry': files_with_sorry,
392+
'files_without_theorems': files_without_theorems,
393+
'cross_file_theorem_files': cross_file_theorem_files,
394+
'composition_theorem_count': composition_theorem_count,
395+
'expected_theorem_floor': expected_theorem_floor,
396+
'targets_declared_count': targets_declared_count,
397+
'targets_phase4plus_count': targets_phase4plus_count,
398+
'inferred_target_count': inferred_target_count,
399+
'proved_like_target_count': proved_like_target_count,
400+
'target_proof_coverage': round(target_proof_coverage, 3),
237401
'n_issues': n_issues, 'n_prs': n_prs,
238402
'phase_flags': {
239403
'has_research': has_research,
240404
'has_inf_specs': has_inf_specs,
241405
'has_lean_specs': has_lean_specs,
242406
'has_impl': has_impl,
243407
'has_proofs': has_proofs,
408+
'proof_incomplete': proof_incomplete,
409+
'proof_mature': proof_mature,
410+
'target_coverage_incomplete': target_coverage_incomplete,
411+
'composition_incomplete': composition_incomplete,
244412
'has_rust': has_rust,
245413
'has_ci': has_ci,
246414
'has_correspondence_tests': has_correspondence_tests,

0 commit comments

Comments
 (0)