[Automation] Auto-generate property manifest from Lean files

[Th0rgal]

Summary

Automate property manifest generation from Lean theorem declarations, eliminating manual maintenance and sync errors.

Problem

Current State:

• Property manifest (property_manifest.json) manually maintained
• Prone to sync errors between code and manifest
• check_property_manifest.py validates but doesn't generate
• Manual overhead when adding new theorems
• Easy to forget to update manifest

Example Error:

# Developer adds theorem
theorem new_property : ... := by ...

# Forgets to update manifest
# CI fails on next push

Proposed Solution

Create scripts/extract_properties.py

#!/usr/bin/env python3
"""Auto-extract theorem names from Lean proof files"""

import re
import json
from pathlib import Path

def extract_theorems(lean_file: Path) -> list[str]:
    """Parse Lean file for theorem declarations"""
    content = lean_file.read_text()
    
    # Pattern matches: theorem <name> ...
    pattern = r'^\s*theorem\s+(\w+)\s*[:(]'
    theorems = re.findall(pattern, content, re.MULTILINE)
    
    return theorems

def generate_manifest() -> dict:
    """Auto-generate property manifest from all proof files"""
    contracts = [
        'SimpleStorage',
        'Counter', 
        'Ledger',
        'SimpleToken',
        'Authorization',
        'CryptoHash',
        'Marketplace'
    ]
    
    manifest = {}
    
    for contract in contracts:
        proof_file = Path(f'DumbContracts/Specs/{contract}/Proofs.lean')
        
        if not proof_file.exists():
            continue
            
        theorems = extract_theorems(proof_file)
        
        manifest[contract] = {
            'file': str(proof_file),
            'theorems': theorems,
            'count': len(theorems)
        }
    
    return manifest

def main():
    manifest = generate_manifest()
    print(json.dumps(manifest, indent=2))

if __name__ == '__main__':
    main()

Update CI Workflow

# .github/workflows/verify.yml
- name: Generate property manifest
  run: python3 scripts/extract_properties.py > property_manifest_auto.json

- name: Check manifest is up to date
  run: |
    if ! diff property_manifest.json property_manifest_auto.json; then
      echo "ERROR: Property manifest is out of sync"
      echo "Run: python3 scripts/extract_properties.py > property_manifest.json"
      exit 1
    fi

Enhanced Features

Feature 1: Extract property tags

# Parse docstrings for property metadata
def extract_property_metadata(lean_file: Path) -> dict:
    """Extract theorem + metadata from docstrings"""
    pattern = r'/--\s*@property\s+(\w+).*?-/\s*theorem\s+(\w+)'
    # Returns: {theorem_name: {tags: [...], description: "..."}}

Feature 2: Validate test coverage

def check_test_coverage(manifest: dict) -> bool:
    """Ensure every theorem has corresponding test"""
    for contract, data in manifest.items():
        test_file = f'test/Property{contract}.t.sol'
        for theorem in data['theorems']:
            if not has_test(test_file, theorem):
                print(f"Missing test for {contract}::{theorem}")
                return False
    return True

Feature 3: Generate coverage report

def generate_coverage_report(manifest: dict) -> str:
    """Generate markdown coverage report"""
    total = sum(data['count'] for data in manifest.values())
    return f"Total Properties: {total}\n" + ...

Benefits

✅ Eliminates manual errors
✅ Automatically detects new theorems
✅ Reduces maintenance burden
✅ Improves CI reliability
✅ Real-time coverage tracking
✅ Enforces documentation standards

Implementation Plan

Phase 1: Basic Extraction (2 days)

• Implement extract_theorems()
• Generate manifest JSON
• CLI tool

Phase 2: CI Integration (1 day)

• Add to GitHub Actions workflow
• Fail on out-of-sync manifest
• Auto-commit option

Phase 3: Enhanced Features (2 days)

• Metadata extraction
• Test coverage validation
• Coverage report generation

Files Affected

Create:

• scripts/extract_properties.py

Update:

• .github/workflows/verify.yml
• scripts/check_property_manifest.py (use auto-generation)
• property_manifest.json (becomes auto-generated)

Dependencies

None - uses standard Python libraries

Estimated Effort

1 week

Success Criteria

• Script extracts all theorems correctly
• CI validates manifest sync
• Eliminates manual manifest updates
• Coverage report auto-generated
• Documentation updated

Related Issues

• Improves workflow from [Documentation] Create 'Adding Your First Contract' tutorial #66 (First Contract tutorial)
• Supports coverage tracking for [Example Contract] Implement ERC20 standard token with full verification #69 (ERC20)

Future Enhancements

• Extract proof strategies from comments
• Identify sorry placeholders
• Estimate proof complexity
• Generate proof skeleton

[Th0rgal]

This issue is already fully addressed by existing infrastructure in the codebase:

Auto-generation: scripts/extract_property_manifest.py auto-generates test/property_manifest.json from Lean proof files using property_utils.py's extract_manifest_from_proofs().

CI Sync Validation: scripts/check_property_manifest_sync.py validates that the manifest is in sync with Lean proofs — both directions (no missing theorems, no stale entries). This runs in CI at .github/workflows/verify.yml.

Test Coverage: scripts/check_property_coverage.py ensures every theorem in the manifest has a corresponding test (or documented exclusion).

Coverage Reporting: scripts/report_property_coverage.py generates coverage reports (text/markdown/JSON) and posts them to GitHub Step Summary.

CI Integration: All four checks run in the verify workflow:

• check_property_manifest.py — validates test file references
• check_property_manifest_sync.py — validates manifest ↔ Lean sync
• check_property_coverage.py — ensures test coverage
• report_property_coverage.py — generates coverage report

All success criteria from the issue are met:

• ✅ Script extracts all theorems correctly
• ✅ CI validates manifest sync
• ✅ Eliminates manual manifest updates (sync check catches drift)
• ✅ Coverage report auto-generated