Add certified AIG resynthesis benchmark

[hyizhak]

Summary

• add ElectronicDesignAutomation/CertifiedAIGResynthesis, a proof-carrying Boolean optimization benchmark
• expose arbitrary small-cut AIG replacement with reusable divisors through a compact C++17 policy API
• independently replay every rewrite certificate in Python using exhaustive truth tables over up to eight cut variables
• score reachable AND area and logic depth across adder, barrel-shifter, arbiter, packet-classifier, and CRC workloads
• add unified-evaluator metadata, frozen workload hashes, documentation, baseline results, and EDA catalog entries

Why

This provides a computational-logic frontier task that directly transforms and measures Boolean DAGs rather than simulating a system. The open search problem is to coordinate local equivalences, divisor reuse, balancing, and reconvergent-DAG effects while retaining independently checkable correctness.

The task is self-contained and uses only Python and C++17. It needs no Docker, GPU, network access, external solver, downloaded circuit assets, or vendor EDA tools.

Validation

• direct evaluator from an isolated worktree based on main:
  • valid=1.0
  • combined_score=1.0
  • 6,610 live ANDs and mean depth 108.6
  • 1,546 exhaustive proof rows replayed
  • 3.67 seconds on the current AMD EPYC host
• unified OpenEvolve baseline:
  • algorithm.iterations=0
  • valid=1.0
  • combined_score=1.0
  • process isolation, read-only snapshots, compilation, and artifact collection passed
• immutable-shell modifications and an intentionally non-equivalent certificate were rejected
• a temporary same-arm mux policy scored 1.1367 and improved every workload, confirming measurable headroom
• git diff --cached --check and C++17 warning checks passed

[github-actions]

🤖 AI Code Review (gemini-3-flash-preview)

🇬🇧 English Analysis

1. Executive Summary

• Core Purpose: This PR introduces a new Electronic Design Automation (EDA) benchmark task named CertifiedAIGResynthesis. The task focuses on Boolean logic synthesis, specifically rewriting And-Inverter Graphs (AIGs) to optimize area and depth while providing formal certificates for equivalence checking.
• Modified File Structure & Modifications:
  • TASK_DETAILS.md & TASK_DETAILS_zh-CN.md: Added CertifiedAIGResynthesis to the task list under the ElectronicDesignAutomation category.
  • benchmarks/ElectronicDesignAutomation/CertifiedAIGResynthesis/README.md: Provided task overview, environment requirements (C++17, Python 3.10+), and execution commands.
  • benchmarks/ElectronicDesignAutomation/CertifiedAIGResynthesis/Task.md: Detailed the engineering problem, AIGER representation, API specifications (try_rewrite, replace), and the formal verification replay mechanism.
  • benchmarks/ElectronicDesignAutomation/CertifiedAIGResynthesis/baseline/: Included a reference solution (solution.cpp) implementing constant propagation and structural hashing, along with a result_log.txt for normalization.
  • benchmarks/ElectronicDesignAutomation/CertifiedAIGResynthesis/scripts/init.cpp: Provided the starter code for agents, containing the EVOLVE-BLOCK for logic optimization.
  • benchmarks/ElectronicDesignAutomation/CertifiedAIGResynthesis/verification/evaluator.py: A comprehensive Python script (1000+ lines) for workload generation, C++ compilation, certificate replay, and scoring.
  • benchmarks/ElectronicDesignAutomation/CertifiedAIGResynthesis/references/problem_config.json: Defined five deterministic workloads (adder, shifter, arbiter, classifier, CRC).
  • benchmarks/ElectronicDesignAutomation/CertifiedAIGResynthesis/frontier_eval/: Metadata files for integration with the frontier_eval framework.

2. AI Content Analysis

• Estimated AI Component: 10%
• Reasoning & Evidence: The code exhibits high domain-specific nuance characteristic of expert human engineering. The implementation of the AIGER format (e.g., literal encoding 2 * id + polarity), the truth-table based formal verification replay in evaluator.py, and the specific DAG-aware optimization constraints are highly specialized. While AI might have been used to generate boilerplate for the frontier_eval metadata or standard C++ headers, the core logic (e.g., the Optimizer class interface and the compositional proof logic) reflects deep expertise in logic synthesis and formal methods.

3. Engineering & Economic Assessment

• Engineering Reality Check: This is a high-fidelity, production-grade engineering problem. It moves beyond "toy" examples by requiring "Proof-Carrying Code" (certificates), which is a real-world requirement in safety-critical hardware design to ensure synthesis tools do not introduce functional bugs. It correctly handles edge cases like fanout reconvergence and acyclic constraints.
• Economic Value: High. Logic synthesis is a critical step in semiconductor design. Improving the area (AND node count) and depth (timing) of Boolean networks directly translates to reduced chip manufacturing costs and higher performance. The inclusion of formal certification reduces the downstream cost of verification.

4. Quality Assurance

• Verification & Testing:
  • frontier_eval Integration: Yes.
  • task_name: CertifiedAIGResynthesis.
  • Execution & Dependencies: The README.md clearly documents the python -m frontier_eval command and the g++ C++17 requirement. Environment setup is minimal and well-explained.
• Documentation Quality: High. The Task.md provides a rigorous mathematical and engineering definition of the problem. The README.md is concise and actionable. No significant grammatical errors or formatting inconsistencies were detected.
• Organizational Structure: Logical and modular. The separation of baseline, scripts, verification, and references follows standard benchmark repository patterns.

5. Security & Privacy Check

• Sensitive Files: Clean. No .env, API keys, or IDE-specific files (.vscode/) were found in the diff.
• Absolute Paths: None detected. The evaluator.py and C++ files use relative paths and Path(__file__) for resource discovery.

---

🇨🇳 中文分析

1. 摘要

• 核心目的: 此 PR 引入了一个名为 CertifiedAIGResynthesis 的新电子设计自动化 (EDA) 基准测试任务。该任务专注于布尔逻辑综合，特别是重写与非图 (AIG) 以优化面积和深度，同时提供用于等价性检查的形式化证书。
• 修改的文件结构与变更摘要:
  • TASK_DETAILS.md & TASK_DETAILS_zh-CN.md: 在 ElectronicDesignAutomation 类别下新增了 CertifiedAIGResynthesis 任务。
  • benchmarks/ElectronicDesignAutomation/CertifiedAIGResynthesis/README.md: 提供了任务概述、环境要求（C++17, Python 3.10+）和运行命令。
  • benchmarks/ElectronicDesignAutomation/CertifiedAIGResynthesis/Task.md: 详细说明了工程问题、AIGER 表示法、API 规范（try_rewrite, replace）以及形式化验证回放机制。
  • benchmarks/ElectronicDesignAutomation/CertifiedAIGResynthesis/baseline/: 包含了实现常数传播和结构哈希的参考解决方案 (solution.cpp)，以及用于分值归一化的 result_log.txt。
  • benchmarks/ElectronicDesignAutomation/CertifiedAIGResynthesis/scripts/init.cpp: 提供了智能体的初始代码，包含用于逻辑优化的 EVOLVE-BLOCK 区域。
  • benchmarks/ElectronicDesignAutomation/CertifiedAIGResynthesis/verification/evaluator.py: 一个复杂的 Python 脚本（1000+ 行），用于工作负载生成、C++ 编译、证书回放和评分。
  • benchmarks/ElectronicDesignAutomation/CertifiedAIGResynthesis/references/problem_config.json: 定义了五个确定性工作负载（加法器、移位器、仲裁器、分类器、CRC）。
  • benchmarks/ElectronicDesignAutomation/CertifiedAIGResynthesis/frontier_eval/: 用于集成到 frontier_eval 框架的元数据文件。

2. AI 成分分析

• 预估 AI 含量: 10%
• 判断依据与证据: 代码展示了专家级人工工程特有的高度领域特定细微差别。AIGER 格式的实现（例如文字编码 2 * id + polarity）、evaluator.py 中基于真值表的形式化验证回放，以及特定的 DAG 感知优化约束都具有高度专业性。虽然 AI 可能被用于生成 frontier_eval 元数据或标准 C++ 头文件的模板，但核心逻辑（如 Optimizer 类接口和组合证明逻辑）反映了在逻辑综合和形式化方法方面的深厚专业知识。

3. 工程与经济评估

• 工程现实检验: 这是一个高保真、生产级别的工程问题。它超越了“玩具”示例，要求提供“携带证明的代码”（证书），这是安全关键型硬件设计中的现实需求，以确保综合工具不会引入功能性 Bug。它正确处理了扇出重聚和无环约束等边缘情况。
• 经济价值: 高。逻辑综合是半导体设计的关键步骤。改进布尔网络的面积（AND 节点数）和深度（时序）直接转化为降低芯片制造成本和提高性能。包含形式化认证降低了下游验证的成本。

4. 质量保证

• 验证与测试:
  • frontier_eval 集成: 是。
  • task_name: CertifiedAIGResynthesis。
  • 运行与依赖: README.md 清晰地记录了 python -m frontier_eval 命令和 g++ C++17 要求。环境设置简单且解释详尽。
• 文档质量: 高。Task.md 提供了问题的严谨数学和工程定义。README.md 简洁且具有可操作性。未检测到明显的语法错误或格式不一致。
• 组织结构: 逻辑清晰且模块化。baseline、scripts、verification 和 references 的分离符合标准基准测试仓库模式。

5. 安全与隐私检查

• 敏感文件: 未发现异常。Diff 中未发现 .env、API 密钥或 IDE 特定文件（如 .vscode/）。
• 绝对路径: 未检测到。evaluator.py 和 C++ 文件使用相对路径和 Path(__file__) 进行资源定位。

[wrh-human]

Review — CertifiedAIGResynthesis (PR #95)

Thank you for contributing CertifiedAIGResynthesis. This PR excels in engineering value, verification mechanism, and search space design, with most of the core work being of high quality. Detailed analysis below:

---

1. Domain, Economic Value, and Frontier-Eng Fit ✅

EDA logic synthesis (AIG resynthesis) is a real engineering domain — it is the core engine of open-source tools such as ABC and Mockturtle. Better area and depth translate directly into reduced chip cost and power consumption, giving the task clear economic value. The task requires the agent to discover locally equivalent rewrite rules on a shared DAG, starting from a feasible baseline and iteratively improving via a verifier. This aligns well with Frontier-Eng's stated mission.

2. Not purely numerical ✅

The agent edits C++ rewrite strategies (how to enumerate cuts, select divisors, and construct local subgraphs), not numerical parameters. This requires understanding circuit DAG topology, fanout/reconvergence, cut enumeration, and Boolean equivalence — structural engineering reasoning, not parameter optimization.

3. Search space ✅

Each rewrite is bounded by ≤8 leaves, ≤16 divisors, ≤64 ANDs, and ≤20000 total rewrites. The combinatorial explosion makes brute-force search infeasible. The baseline uses only constant propagation, structural hashing, and basic idempotence/complement simplification. A single mux-elimination rule was verified to achieve a 13.6% improvement, confirming substantial headroom.

4. Evaluator and engineering verification ✅

This is the strongest part of the PR. After the candidate runs, ProofChecker independently replays every certificate line and exhaustively checks truth tables for all 2^k (k ≤ 8) input assignments. Verification includes:

• Path coverage (all leaves must be reachable from the root)
• Divisor independence (divisors must not depend on the rewritten root)
• Functional equivalence (bit-for-bit truth-table match)
• Cycle detection and forward-reference checking
• Input integrity (SHA-256 digest verification)

The scoring formula (A_b/A_c)^0.75 × (D_b/D_c)^0.25 has a reasonable weight distribution. This is genuine engineering verification, not a "toy" simulation.

5. Constraints and verifier enforcement ✅

problem_config.json defines a complete set of constraints, and the proof checker enforces them strictly during replay. Input integrity is checked via SHA-256, certificate existence and size are validated, and EVOLVE-BLOCK violations are caught via byte-level comparison against the baseline.

6. Baseline experiment ✅

result_log.txt is thorough: per-workload area/depth/rewrite counts, a headroom check, and environment details (Linux, g++ 11.4, EPYC). All circuits are deterministically generated from config with no randomness and frozen SHA-256 hashes, making them fully reproducible.

---

Issues to address before merging

Issue 1: No test file

This PR has zero tests — no test_evaluator.py exists. At minimum, the following should be added:

• An end-to-end test verifying valid=1.0 and combined_score=1.0 for the baseline.
• A test rejecting EVOLVE-BLOCK boundary violations.
• A test rejecting certificates with incorrect truth tables or cycles.
• A test verifying that candidate timeouts or crashes are reported correctly.

(The README lists g++ as a prerequisite, so assuming g++ in tests is reasonable.)

Issue 2: Workload loop lacks per-workload error isolation

The workload loop (lines 920–990) has no try/except. If workload 3 fails (candidate crash, certificate parse error, or timeout), the entire evaluation terminates with valid=0 and no partial results retained. The agent receives no feedback about which workload failed or why. This should be restructured with per-workload try/except and per-workload error recording, similar to the KernelBlockEncoding refactor.

Issue 3: Missing RLIMIT_NPROC in _resource_limits

The _resource_limits function sets RLIMIT_CPU, RLIMIT_AS, RLIMIT_FSIZE, and RLIMIT_NOFILE, but does not set RLIMIT_NPROC. A candidate could fork child processes without limit within the evaluation window. Please add:

try:
    resource.setrlimit(resource.RLIMIT_NPROC, (64, 64))
except (AttributeError, ValueError, OSError):
    pass

---

Non-blocking suggestion

The workload IDs in problem_config.json (w1–w5) are not immediately descriptive. Consider using the actual circuit names from result_log.txt (e.g., ripple_adder_96) or adding a kind/description field for better readability.

---

Summary

The core problem definition, independent exhaustive truth-table checker, search space design, and baseline documentation are all well-executed. The three issues above should be fixed before merging. The domain and approach are a strong fit for Frontier-Eng. Ready to merge after those fixes.