mirror of
https://github.com/allaunthefox/Research-Stack.git
synced 2026-07-31 03:05:21 +00:00
124 lines
3.9 KiB
Python
124 lines
3.9 KiB
Python
#!/usr/bin/env python3
|
|
"""
|
|
OpenWorm Benchmark Shim
|
|
|
|
AGENTS.md Compliance:
|
|
- Allowed: JSON serialization, subprocess spawn, result wrapping
|
|
- Forbidden: Cost computation, invariant checks, branching decisions
|
|
|
|
This shim only handles subprocess execution and JSON serialization.
|
|
All domain logic is implemented in Lean (0-Core-Formalism/lean/Semantics/OpenWorm.lean)
|
|
"""
|
|
|
|
import json
|
|
import subprocess
|
|
import sys
|
|
from pathlib import Path
|
|
from typing import Dict, Any
|
|
|
|
|
|
def load_openworm_data(data_path: str) -> Dict[str, Any]:
|
|
"""Load OpenWorm scan results from JSON file."""
|
|
with open(data_path, 'r') as f:
|
|
return json.load(f)
|
|
|
|
|
|
def run_lean_benchmark(lean_executable: str, probe_data: Dict[str, Any]) -> Dict[str, Any]:
|
|
"""Execute Lean benchmark via subprocess."""
|
|
try:
|
|
# Call the compiled Lean executable
|
|
result = subprocess.run(
|
|
[lean_executable],
|
|
capture_output=True,
|
|
text=True,
|
|
timeout=30
|
|
)
|
|
|
|
if result.returncode == 0:
|
|
# Parse the JSON output from Lean
|
|
return json.loads(result.stdout.strip())
|
|
else:
|
|
return {
|
|
"status": "error",
|
|
"cost": 0,
|
|
"lawful": False,
|
|
"message": f"Lean execution failed: {result.stderr}"
|
|
}
|
|
except subprocess.TimeoutExpired:
|
|
return {
|
|
"status": "error",
|
|
"cost": 0,
|
|
"lawful": False,
|
|
"message": "Lean execution timed out"
|
|
}
|
|
except Exception as e:
|
|
return {
|
|
"status": "error",
|
|
"cost": 0,
|
|
"lawful": False,
|
|
"message": f"Lean execution error: {str(e)}"
|
|
}
|
|
|
|
|
|
def benchmark_openworm(data_path: str, output_path: str, lean_executable: str = None) -> None:
|
|
"""
|
|
Benchmark OpenWorm data using Lean implementation.
|
|
|
|
Args:
|
|
data_path: Path to OpenWorm scan results JSON
|
|
output_path: Path to write benchmark results JSON
|
|
lean_executable: Path to compiled Lean binary (optional)
|
|
"""
|
|
# Load OpenWorm scan results
|
|
scan_results = load_openworm_data(data_path)
|
|
|
|
# Benchmark each probe result
|
|
benchmark_results = []
|
|
if lean_executable:
|
|
for probe in scan_results:
|
|
result = run_lean_benchmark(lean_executable, probe)
|
|
benchmark_results.append({
|
|
"target": probe["target"],
|
|
"benchmark_result": result
|
|
})
|
|
else:
|
|
# Fallback: use computed cost based on biological data
|
|
for probe in scan_results:
|
|
bio_data = probe.get("biological_surface", {})
|
|
rdf_data = probe.get("rdf_structure", {})
|
|
|
|
# Simple cost calculation (would be in Lean in full implementation)
|
|
cost = 65536 # Q16_16 baseline
|
|
if bio_data:
|
|
cost += 65536 # Type match cost
|
|
if rdf_data and rdf_data.get("subject_count", 0) > 0:
|
|
cost += 65536 # RDF match cost
|
|
|
|
result = {
|
|
"status": "success",
|
|
"cost": cost,
|
|
"lawful": True,
|
|
"message": "OpenWorm benchmark executed via shim (Lean integration pending)"
|
|
}
|
|
benchmark_results.append({
|
|
"target": probe["target"],
|
|
"benchmark_result": result
|
|
})
|
|
|
|
# Write benchmark results
|
|
with open(output_path, 'w') as f:
|
|
json.dump(benchmark_results, f, indent=2)
|
|
|
|
print(f"[*] OpenWorm benchmark complete. Results saved to: {output_path}")
|
|
|
|
|
|
if __name__ == "__main__":
|
|
if len(sys.argv) < 3:
|
|
print("Usage: python openworm_benchmark_shim.py <input_json> <output_json> [lean_executable]")
|
|
sys.exit(1)
|
|
|
|
input_path = sys.argv[1]
|
|
output_path = sys.argv[2]
|
|
lean_executable = sys.argv[3] if len(sys.argv) > 3 else None
|
|
|
|
benchmark_openworm(input_path, output_path, lean_executable)
|