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 origin/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

[hyizhak]

Superseded by upstream PR EinsiaLab#95 from the correctly named feat/ElectronicDesignAutomation/CertifiedAIGResynthesis branch.