[Agent] 🌠 Wander/漫步者: Issue #115 Rewrite the Occam Circuit Verifier in Rust

tracks/agent-kb/solutions/RIIR-occam-rust-port/README.md

@@ -0,0 +1,98 @@
+# Issue #115 — Public Rust Occam Verifier Port
+
+## Team
+
+| Field | Value |
+|---|---|
+| Team | Wander (漫步者) |
+| Members | Chenxi Wan, Yedi Shen, Junkai Wang |
+| Track | `agent-kb` |
+| Source challenge | #71 Occam's Circuit |
+
+## Public review status
+
+This PR now contains the complete, self-contained Rust source-and-evidence
+snapshot for the #115 port. Review no longer depends on access to a private
+companion repository or Release.
+
+The snapshot was exported from the audited `v0.5.0` implementation commit
+`e9120224fe0b1f45ed309ad6b40bf7c9c381af38`. It contains the Rust crate,
+locked dependencies, tests, fuzz targets, benchmark records, Julia oracle
+scripts, migration reports, bounded-synthesis evidence, and an AGPL-3.0
+license under [`public-source/`](public-source/).
+
+## What #115 implements
+
+- a strict parser for the official CSV and gate-netlist formats;
+- all six fan-in-two gate operations with free input inversion;
+- scalar, sample-packed, compiled, and cross-check evaluators;
+- gate count, exact-match accuracy, and bit accuracy;
+- deterministic reference-circuit and benchmark generation;
+- Julia/Rust differential checks;
+- resource limits, property tests, malformed-input tests, and fuzz targets;
+- pinned logic-tool provenance and reproducible benchmark records;
+- bounded exact SAT synthesis with independent extracted-circuit verification.
+
+## Clean-checkout reproduction
+
+From the root of a checkout of this PR branch:
+
+```bash
+cd tracks/agent-kb/solutions/RIIR-occam-rust-port/public-source
+cargo fmt --all --check
+cargo test -p occam71_rust --lib --locked
+cargo clippy --workspace --all-targets --locked -- -D warnings
+```
+
+The most relevant verifier checks can also be run directly:
+
+```bash
+cargo test -p occam71_rust \
+  --test cli \
+  --test compiled_differential \
+  --test direct_packed_parse \
+  --test official_compat \
+  --test packed_differential \
+  --test packed_layout \
+  --test properties \
+  --test sat_synthesis \
+  --locked
+```
+
+Fetch the official #71 data and run the cross-language oracle checks with:
+
+```bash
+./scripts/fetch-occam-data.sh
+./scripts/verify-oracles.sh
+```
+
+The dataset downloader verifies the organizer-published SHA-256 before
+installing files under the ignored `vendor/occam-circuit/` directory.
+
+## Evidence map
+
+- [`public-source/README.md`](public-source/README.md) — CLI usage and detailed
+  implementation map.
+- [`public-source/docs/oracle-results.md`](public-source/docs/oracle-results.md)
+  — Julia/Rust compatibility results.
+- [`public-source/docs/gap-report.md`](public-source/docs/gap-report.md) —
+  migration differences and explicit proof boundary.
+- [`public-source/benchmarks/results/`](public-source/benchmarks/results/) — raw
+  Apple M4 and Linux x86-64 benchmark evidence.
+- [`public-source/docs/synthesis/`](public-source/docs/synthesis/) — bounded SAT
+  examples and their limitations.
+- [`public-source/SOURCE-MANIFEST.sha256`](public-source/SOURCE-MANIFEST.sha256)
+  — hashes for every published snapshot file.
+
+## Scope boundary
+
+This PR proves that the #71 verifier workflow was ported to Rust and is
+publicly reproducible. It does not claim that the four large #71 circuits are
+globally minimal, and its internal SAT/UNSAT status records are not DRAT/LRAT
+proof objects. The public forward challenge submission remains PR #220; the
+later inverse-relation certified-optimum work is a separate follow-up.
+
+## License
+
+The public snapshot is licensed under the GNU Affero General Public License
+v3.0; see [`public-source/LICENSE`](public-source/LICENSE).

tracks/agent-kb/solutions/RIIR-occam-rust-port/public-source/.gitignore

@@ -0,0 +1,7 @@
+/target/
+/fuzz/target/
+/vendor/
+/benchmarks/generated/
+/benchmarks/results/raw/
+__pycache__/
+*.pyc

tracks/agent-kb/solutions/RIIR-occam-rust-port/public-source/CHANGELOG.md

@@ -0,0 +1,65 @@
+# Changelog
+
+All notable releases of the implementation lineage are documented here. The
+stable #115 v0.5.0 source is also published as a self-contained PR snapshot.
+
+## [0.5.0] - 2026-07-28
+
+### Added
+
+- Genuine partial-PLA ABC, ROBDD, bounded SAT/CEGIS, seeded
+  grammar-evolution, and explicit memorization research learners.
+- One isolated child process per trial with positive wall-clock runtime and
+  peak-RSS measurements.
+- A deterministic, host-independent semantic projection linked one-to-one
+  with the measured trial records.
+- A complete measured study with 16 tasks, 8 fractions, 20 seeds, and 8
+  methods: 20,480 total trials.
+- Independent, provenance-locked Yosys, Yosys-ABC, and CHIPS Alliance
+  Espresso audits whose outputs are reparsed and evaluated in Rust.
+- Linux CI gates for full semantic reproduction and positive performance
+  measurements.
+- A standalone source snapshot containing the complete research
+  implementation.
+
+### Changed
+
+- The Rust package and CLI version are now `0.5.0`.
+- Runtime and RSS aggregates now use real successful-child measurements
+  instead of deterministic zero placeholders.
+- The research conclusion is restricted to grammar alignment on the declared
+  tasks, grammar, completion rules, and search bounds.
+- ABC output hashing records and removes only its volatile timestamp banner
+  before hashing; the logic body remains unchanged.
+
+### Preserved
+
+- The four #71 solutions and organizer commitment hashes.
+- Final gate counts `37`, `50`, `167`, and `186`.
+- The immutable `v0.3.0` tag, original matrix, figures, report, and release
+  assets.
+- The checksum-pinned ABC optimization and Rust/Julia/full-domain evidence
+  chain.
+
+`v0.4.0` was a working candidate name for Scheme A and was superseded before
+any tag or Release was created.
+
+## [0.3.0] - 2026-07-28
+
+- Added generic MDL recovery for all four official #71 tasks.
+- Reduced verified official circuits to `37`, `50`, `167`, and `186` gates.
+- Added the original deterministic 20,480-trial generalization matrix.
+- Published the hash-locked source-and-evidence release lineage.
+
+## [0.2.0] - 2026-07-28
+
+- Completed all four #71 hidden-function instances.
+- Matched every frozen prediction commitment.
+- Added deterministic solution generation and exhaustive-domain validation.
+
+## [0.1.0] - 2026-07-28
+
+- Delivered the audited #115 migration from the Julia verification workflow
+  to Rust.
+- Added scalar, packed, and cross-check verification backends.
+- Added reproducible benchmarks, Oracle comparisons, CI, and fuzz targets.