Add certified AIG resynthesis benchmark

TASK_DETAILS.md

@@ -203,6 +203,11 @@ We welcome new engineering problem ideas — even without complete verification
       <td><code>holographic_polarization_multiplexing</code></td>
       <td>Polarization-multiplexed holography</td>
     </tr>
+    <tr>
+      <td><b>ElectronicDesignAutomation</b></td>
+      <td><code>CertifiedAIGResynthesis</code></td>
+      <td>Proof-carrying, DAG-aware Boolean resynthesis with exact local equivalence checking and area/depth optimization</td>
+    </tr>
     <tr>
       <td rowspan="2"><b>ComputerSystems</b></td>
       <td><code>MallocLab</code></td>

TASK_DETAILS_zh-CN.md

@@ -203,6 +203,11 @@ Frontier-Eng 目前已覆盖以下领域的任务。每个任务均配有可运
       <td><code>holographic_polarization_multiplexing</code></td>
       <td>偏振复用全息</td>
     </tr>
+    <tr>
+      <td><b>ElectronicDesignAutomation</b></td>
+      <td><code>CertifiedAIGResynthesis</code></td>
+      <td>带证明证书的 DAG 感知布尔重综合，精确验证局部等价性并优化面积与深度</td>
+    </tr>
     <tr>
       <td rowspan="2"><b>ComputerSystems</b></td>
       <td><code>MallocLab</code></td>

benchmarks/ElectronicDesignAutomation/CertifiedAIGResynthesis/README.md

@@ -0,0 +1,69 @@
+# Certified AIG Resynthesis
+
+This benchmark asks an optimization policy to rewrite real combinational Boolean
+networks represented as and-inverter graphs (AIGs). Each proposed small-cut
+replacement is accepted only after exact truth-table equivalence checking and is
+recorded as a replayable certificate. The score rewards fewer reachable AND nodes
+and lower logic depth.
+
+This is a synthesis benchmark, not a timing or traffic simulator: candidate code
+directly changes the Boolean DAG that is measured. The independent Python checker
+reconstructs every accepted transformation from the original AIG and certificate.
+
+## Files
+
+- `Task.md`: complete API, proof format, workloads, limits, and score.
+- `references/problem_config.json`: frozen workload and resource configuration.
+- `references/README.md`: standards and research context.
+- `scripts/init.cpp`: compact editable C++ starter policy.
+- `verification/rewrite_runtime.hpp`: immutable graph API and certificate runtime.
+- `baseline/solution.cpp`: frozen starter used for score normalization.
+- `baseline/result_log.txt`: measured reference run.
+- `verification/evaluator.py`: workload construction, compilation, independent
+  certificate replay, and scoring.
+- `verification/test_evaluator.py`: end-to-end, adversarial-certificate, timeout,
+  isolation, and source-integrity regression tests.
+- `frontier_eval/`: unified-task metadata and its argument-safe evaluator wrapper.
+
+## Requirements
+
+- Linux or another POSIX environment with Python 3.10+;
+- `g++` with C++17 support; and
+- one CPU core and less than 2 GiB RAM.
+
+There are no Python packages, containers, external solvers, downloads, GPUs, or
+vendor EDA tools. The complete starter evaluation takes about 3.3 seconds on the
+repository's current AMD EPYC host, including two C++ compilations and ten circuit
+runs.
+
+## Direct evaluation
+
+From this task directory:
+
+```bash
+python verification/evaluator.py scripts/init.cpp
+```
+
+The starter must report `valid=1.0` and `combined_score=1.0`. A score above 1.0 is
+an improvement over the frozen starter.
+
+## Unified evaluation
+
+From the repository root:
+
+```bash
+python -m frontier_eval \
+  task=unified \
+  task.benchmark=ElectronicDesignAutomation/CertifiedAIGResynthesis \
+  algorithm=openevolve \
+  algorithm.iterations=0
+```
+
+No runtime override is required; the default process isolation and
+`frontier-eval-driver` environment are sufficient.
+
+## Editing contract
+
+Only change code between `EVOLVE-BLOCK-START` and `EVOLVE-BLOCK-END` in
+`scripts/init.cpp`. The evaluator byte-compares both immutable portions against
+the frozen baseline before compiling a candidate.

benchmarks/ElectronicDesignAutomation/CertifiedAIGResynthesis/Task.md

@@ -0,0 +1,175 @@
+# Certified, Budgeted AIG Resynthesis
+
+## Engineering problem
+
+Logic synthesis repeatedly replaces a subgraph with a cheaper equivalent one.
+The hard part is not merely discovering Boolean identities: useful flows must
+coordinate local choices on a shared DAG, reuse existing divisors, trade area
+against depth, and never change any output function. A rewrite that looks good as
+a tree can lose once fanout and reconvergence are considered.
+
+This task exposes that problem directly. A C++ policy receives a mutable
+and-inverter graph (AIG), proposes arbitrary local replacement AIGs, and obtains a
+Boolean proof obligation for each proposal. The immutable runtime emits only
+accepted transformations. A separate Python implementation then replays the
+certificate and exhaustively checks each obligation before measuring the final
+DAG. No probabilistic simulation is used for correctness.
+
+The central open engineering question is how to search a large space of locally
+equivalent expressions while making globally beneficial, DAG-aware decisions
+under a strict rewrite budget. Equality-saturation scheduling, cut enumeration,
+NPN-aware libraries, exact small-function synthesis, divisor selection, and
+learned rewrite orchestration can all be explored inside the same interface.
+
+## Boolean representation
+
+Inputs are dense, combinational ASCII AIGER (`aag`) networks:
+
+- node 0 is constant false and literal 1 is constant true;
+- positive literal `2 * id` denotes a node;
+- xor with 1 denotes complemented polarity; and
+- every non-input node is a two-input AND.
+
+The frozen evaluator deterministically constructs five engineering circuit
+families from `references/problem_config.json`:
+
+1. a 96-bit ripple-carry adder;
+2. a 64-bit logical barrel shifter;
+3. a 128-request fixed-priority arbiter;
+4. a 48-rule, 12-bit-per-rule packet classifier; and
+5. a 64-bit update of a 32-bit CRC state.
+
+The front ends deliberately retain several semantically redundant lowering forms
+that arise from mux expansion, guarding, repeated expressions, and generic
+Boolean lowering. Workload bytes and SHA-256 digests are deterministic and are
+reported in `artifacts.json`.
+
+## Candidate interface
+
+Only this function is editable:
+
+```cpp
+void optimize(certified_aig::Optimizer& optimizer);
+```
+
+The immutable class provides graph inspection plus two mutation calls:
+
+```cpp
+bool try_rewrite(
+    uint32_t root,
+    const std::vector<uint32_t>& leaves,
+    const std::vector<uint32_t>& divisors,
+    const std::vector<LocalAnd>& local_ands,
+    uint32_t local_output);
+
+bool replace(
+    uint32_t root,
+    uint32_t replacement_global_literal,
+    const std::vector<uint32_t>& leaves);
+```
+
+Useful read methods include `first_and_id()`, `node_count()`, `is_and(id)`,
+`is_active(id)`, `resolve(literal)`, `fanins(id)`, `output_literal(index)`,
+`primary_support(root)`, and `truth_table(root, leaves, &table)`. Their
+implementations and precise failure conditions are visible in
+`verification/rewrite_runtime.hpp`.
+
+`try_rewrite` may synthesize any acyclic local AIG. With `k` cut leaves and `d`
+divisors, local literal references are:
+
+- reference 0: false;
+- references `1..k`: the positive boundary leaves;
+- references `k+1..k+d`: supplied global divisor literals; and
+- subsequent references: local AND results in order.
+
+Each literal is encoded as `2 * reference + polarity`. A local AND may reference
+only an earlier value. Divisors can lie outside the root cone, enabling real
+DAG-aware reuse, but each divisor must be a function of the same cut leaves and
+must not depend on the rewritten root.
+
+## Certificate and formal validity
+
+The candidate executable writes a line-oriented certificate. The immutable C++
+runtime checks proposals before recording them, but that check is not trusted for
+the score. `verification/evaluator.py` independently parses the original AAG and
+replays every certificate line.
+
+For a cut of `k <= 8` leaves, the checker:
+
+1. confirms that every path through the current root cone terminates at a listed
+   leaf or constant;
+2. evaluates the old root on all `2^k` assignments;
+3. independently evaluates every external divisor over the same assignments and
+   rejects root-dependent divisors;
+4. evaluates the proposed local AIG on all assignments;
+5. requires bit-for-bit equality; and
+6. only then redirects the root and appends replacement nodes.
+
+Because every step is an exact equivalence and later steps operate on the graph
+produced by earlier ones, the sequence is a compositional proof that all primary
+outputs retain their original Boolean functions. The checker also detects cycles,
+forward references, stale nodes, uncovered input paths, malformed certificates,
+and resource-limit violations.
+
+## Resource limits
+
+The public limits are:
+
+- at most 8 cut leaves;
+- at most 16 external divisors per rewrite;
+- at most 64 new ANDs per rewrite;
+- at most 20,000 accepted rewrites per workload;
+- at most 300,000 total nodes;
+- a 16 MB certificate; and
+- at most 64 candidate processes per real user where `RLIMIT_NPROC` is supported;
+- 4 seconds of candidate execution per workload by default.
+
+The evaluator additionally limits process address space to 2 GiB and compiles
+with `g++ -std=c++17 -O2`. Compilation time is not part of the candidate execution
+budget, but it is included in reported evaluator wall time.
+
+## Objective
+
+After replay, the checker traverses only nodes reachable from primary outputs:
+
+- `A`: number of reachable AND nodes; and
+- `D`: maximum AND level from any primary input or constant to an output.
+
+Let `A_b, D_b` be the frozen starter result and `A_c, D_c` the candidate result
+for one workload. Its score is
+
+```text
+(A_b / A_c)^0.75 * (D_b / D_c)^0.25
+```
+
+`combined_score` is the geometric mean across all five workloads. The starter is
+exactly 1.0. Invalid source edits, compilation failures, timeouts, altered inputs,
+invalid certificates, or degenerate final graphs produce `valid=0.0` and score
+0.0.
+
+Candidate execution and proof replay are isolated per workload. A failed workload
+records its baseline, candidate, or scoring error while later workloads continue.
+Successful workload scores remain visible through `partial_combined_score` for
+diagnosis; the official `combined_score` stays zero unless all five workloads pass,
+so skipping a difficult circuit cannot improve a candidate's result.
+
+The initial policy performs constant propagation, idempotence/complement
+simplification, and exact structural hashing. It intentionally leaves substantial
+headroom for cut resynthesis, absorption, mux reasoning, balancing, and divisor
+reuse.
+
+## Reproducibility and direct evaluation
+
+No network access or nondeterministic input is used. The workload builder, config,
+baseline, C++ runtime, and Python proof checker are all included and marked
+read-only by the unified evaluator.
+
+```bash
+python verification/evaluator.py scripts/init.cpp \
+  --metrics-out metrics.json \
+  --artifacts-out artifacts.json
+```
+
+`metrics.json` contains numeric leaderboard fields. `artifacts.json` contains the
+per-workload input digests, baseline and candidate area/depth, rewrite counts,
+truth-table rows checked, certificate digests, and process runtimes.

benchmarks/ElectronicDesignAutomation/CertifiedAIGResynthesis/baseline/result_log.txt

@@ -0,0 +1,57 @@
+CertifiedAIGResynthesis baseline validation
+Date: 2026-07-17
+
+Host
+  OS: Linux 5.15.0-153-generic x86_64
+  CPU: 2 x AMD EPYC 7313 (32 physical / 64 logical cores total)
+  Python: 3.10.12
+  Compiler: g++ 11.4.0
+  Candidate process cap: RLIMIT_NPROC=64 where supported
+  GPU/container/external solver: not used
+
+Direct command (from task directory)
+  python verification/evaluator.py scripts/init.cpp \
+    --metrics-out metrics.json --artifacts-out artifacts.json
+
+Direct metrics
+  valid: 1.0
+  combined_score: 1.0
+  partial_combined_score: 1.0
+  runtime_s: 3.584659181535244
+  scenario_count: 5
+  successful_scenario_count: 5
+  failed_scenario_count: 0
+  baseline_total_area: 6610
+  candidate_total_area: 6610
+  baseline_mean_depth: 108.6
+  candidate_mean_depth: 108.6
+  checked_truth_rows: 1546
+
+Per-workload frozen starter result
+  ripple_adder_96:       area=934,  depth=222, rewrites=28
+  barrel_shifter_64:    area=1153, depth=18,  rewrites=176
+  priority_arbiter_128: area=359,  depth=128, rewrites=44
+  packet_classifier_48x12: area=926, depth=83, rewrites=181
+  crc32_update_64:      area=3238, depth=92,  rewrites=221
+
+Unified command (from repository root)
+  .venvs/frontier-eval-driver/bin/python -m frontier_eval \
+    task=unified \
+    task.benchmark=ElectronicDesignAutomation/CertifiedAIGResynthesis \
+    algorithm=openevolve \
+    algorithm.iterations=0
+
+Unified result
+  exit code: 0
+  valid: 1.0
+  combined_score: 1.0
+  evaluator runtime_s: 3.1896
+  read-only/copy/process-isolation path: passed
+
+Development headroom check
+  A temporary candidate adding only same-arm mux elimination was independently
+  replayed by the same evaluator. It scored 1.1367188441269405, reduced total
+  live ANDs from 6610 to 5893, and reduced mean depth from 108.6 to 97.6. Its
+  minimum per-workload score was 1.0705928226806747. This candidate is not the
+  committed starter; the measurement confirms optimization headroom in every
+  frozen workload before more advanced cut synthesis or divisor reuse.