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

[JunkaiWang-TheoPhy]

Between two stars, a tool becomes real when it can be rebuilt from what both worlds leave on the bench.

在两颗恒星之间，能用两个世界留在工作台上的材料重新造出的工具，才真正存在。

第一幕 · 在出发以前，先让工具学会诚实

第三章 · 在两颗星之间重造工具

真正可靠的工具，应当能在另一个世界的工作台上重新诞生。我们把实现、测试、基准与证书一并留下，

让迁移不只是换一种语言，而是让每一步都可以重新核验。

← 上一章：火星温室里最后一盏绿灯     ·     下一章：让语言学会拒绝漂亮的错误 →

Team

Field	Value
Team name	Wander (漫步者)
Members	Chenxi Wan, Yedi Shen, Junkai Wang
Contact	WangTheoPhys@outlook.com

Public reviewability resolved

This PR now contains the self-contained public source-and-evidence snapshot for
the #115 Rust port. Review no longer requires access to a private companion
repository or Release.

• Public snapshot commit: c1bf94e67053943d27440fa48e978e07b922e6ef
• Rust workspace: public-source/
• Reproduction guide: README.md
• Hash manifest: SOURCE-MANIFEST.sha256

The snapshot is an audited export of implementation commit
e9120224fe0b1f45ed309ad6b40bf7c9c381af38 (v0.5.0). It contains the Rust
crate, locked dependencies, tests, fuzz targets, benchmark protocols and raw
records, Julia oracle scripts, migration reports, bounded-synthesis evidence,
and AGPL-3.0 license. The 326 published content files are hash-covered; the
manifest itself is the sole additional tracked snapshot file.

Implemented port

• strict official CSV and gate-netlist parsers;
• scalar, sample-packed, compiled, and cross-check evaluators;
• all six official fan-in-two gates with free input inversion;
• gate count, exact-match accuracy, and bit accuracy;
• deterministic dataset/reference-circuit generation;
• Julia/Rust differential verification;
• resource limits, property tests, malformed-input tests, and fuzz targets;
• reproducible Apple M4 and Linux x86-64 benchmark records;
• bounded exact SAT synthesis with independent extracted-circuit verification.

Clean-checkout validation

Run from the PR checkout root:

cd tracks/agent-kb/solutions/RIIR-occam-rust-port/public-source
./scripts/fetch-occam-data.sh
cargo fmt --all --check
cargo test -p occam71_rust --lib --locked
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
cargo clippy --workspace --all-targets --locked -- -D warnings
./scripts/verify-oracles.sh
shasum -a 256 -c SOURCE-MANIFEST.sha256

Observed on the published snapshot:

• 52 library tests passed;
• 18 focused integration tests passed and one explicit million-row stress test
  remained ignored by design;
• cargo fmt --check and clippy -D warnings passed;
• Julia 1.12.6 independently verified official-add-8, practice-add-n4, and
  practice-mul-n4;
• every manifest entry verified successfully.

Scope boundary

This PR establishes a public, bit-exact, reproducible Rust port of the #71
verifier workflow. It does not claim global minimality for the four large #71
circuits. The 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.

[JunkaiWang-TheoPhy]

@shinaoka @GiggleLiu Status correction and final update (July 29, 2026): Ranger's #115 Rust migration remains complete and ready for review. The companion source/evidence repository is now private; the earlier public-repository wording is superseded. The complete #71 submission remains in #220. The authorized private v0.6.0 source-and-evidence Release is https://github.com/JunkaiWang-TheoPhy/quantum-harness-115-occam-rust-port/releases/tag/v0.6.0 at commit 0e1b1aa2970e9b22818a690b9400eb785bbdea51. It adds the audited Scheme 2 protocol, while all unmeasured Stage B conclusions remain explicitly not estimated/not tested.

[JunkaiWang-TheoPhy]

v0.6.0 final private-release handoff

The #115 implementation remains completed. Its private companion release has
now been finalized:

• companion commit: 0e1b1aa2970e9b22818a690b9400eb785bbdea51;
• annotated tag: v0.6.0 (points to that exact commit);
• private Release: https://github.com/JunkaiWang-TheoPhy/quantum-harness-115-occam-rust-port/releases/tag/v0.6.0;
• attached paper: unified-occam-v0.6.0.pdf;
• PDF SHA-256: 05dee9bbaa52bd1ae1e86aeba84cb75e481ae8848482d887cc34dd02e1739c74.

The complete pre-publish audit passed before tagging. The companion repository
was rechecked as private after release. This handoff does not change the
scientific boundary: Stage B measured 0 of 437,232 planned cells, so the sample
law, strict grokking transition, scaling law, and MPS-plus-SAT frontier remain
not estimated/not tested. Related challenge submission: #220; issues: #115 and
#71.

[GiggleLiu]

As landed in this repository this PR is a 32-line pointer: the implementation, evidence and release all live in a private repository, so nothing here is reviewable. The underlying #71 result is the same registry-matching exercise as #220.

Trivial result, but marked complete. Please drop "Finished" from the title until the artifacts are public and the claim goes beyond matching four known formulas.

[GiggleLiu]

For anyone continuing this work: I have posted an extension to the challenge in the issue itself — #71 (comment)

Short version: invert the same four functions. The forward direction could not test Occam's razor, because the ground truth was already a compact circuit. The inverse direction splits the instance set — x+y and |x−y| stay linear, while x·y and x²+y² do not, and in the bounded-width/Bayesian-network model that split is a theorem rather than an open problem.

The comment states the deliverable (a certified minimum with a machine-checkable UNSAT refutation), the relation semantics (any valid preimage counts), a mandatory negative control, and how to certify success probability if you use randomised gates. Please read it before planning further work here.

[JunkaiWang-TheoPhy]

Small before-deadline update: the private implementation repository now also has a separate inverse-relation extension branch, codex/inverse-relation-extension, pushed under JunkaiWang-TheoPhy/quantum-harness-115-occam-rust-port. That branch adds relation semantics, accepted-output rows, canonical preimage selection, reference inverse circuit synthesis, and exhaustive verification tests. It is intentionally scoped as a prototype/verifier step only: no global minimality, inverse theorem, or DRAT/LRAT proof claim is made here.

[JunkaiWang-TheoPhy]

Thanks; the public-reviewability objection was correct. The Rust port existed,
but a private companion repository did not make this PR independently
reviewable.

That blocker is now addressed in the PR branch. Commit
c1bf94e
publishes the self-contained Rust source and evidence directly under
tracks/agent-kb/solutions/RIIR-occam-rust-port/public-source/.
It includes locked dependencies, parser/evaluator/verifier source, scalar,
packed and compiled differential tests, fuzz targets, benchmark protocols and
raw records, Julia oracle scripts, migration reports, bounded-synthesis
evidence, an AGPL-3.0 license, and a 326-file SHA-256 manifest.

I re-ran the public snapshot from its nested workspace: 52 library tests and 18
focused integration tests passed; cargo fmt --check and
clippy -D warnings passed; Julia independently verified the official and two
practice oracle cases; and every manifest entry verified. The exact commands
and immutable links are now at the top of the PR body.

The claim boundary is also explicit: this closes the #115 public Rust-port
reviewability gap, but it does not claim global minimality for the four large
#71 circuits. The separate inverse-relation/DRAT-LRAT work remains a follow-up
and is not used to justify this port.

[JunkaiWang-TheoPhy]

@GiggleLiu Independent clean-room reproducibility audit of the public #115 handoff (2026-07-31).

I started from an empty temporary Git repository and fetched the two immutable commits over public HTTPS with interactive prompting and the Git credential helper disabled. Both commits were retrievable without private-repository access:

• [challenge]: Port any challenge of this school to Rust #115 source commit: c1bf94e67053943d27440fa48e978e07b922e6ef
• certified inverse evidence cross-check: 58e9bb573db81c5a7811db8690897eb73850d8b4

#115 public-source results

From the clean checkout of the public-source directory:

• shasum -a 256 -c SOURCE-MANIFEST.sha256: 326/326 entries OK.
• cargo fmt --all --check: passed.
• cargo test -p occam71_rust --lib --locked: 52/52 passed.
• The eight focused integration targets listed in the public README: 18/18 passed; the explicit one-million-row ingestion regression remained ignored by design.
• cargo clippy --workspace --all-targets --locked -- -D warnings: passed.
• The organizer dataset download matched SHA-256 c15f84839a365dd9daab686ccfd58a50ce286d5f1071d7f093e9fdd091ecaa1b.
• Julia 1.12.6 independently agreed with Rust for official-add-8, practice-add-n4, and practice-mul-n4.

I also ran the public generic-MDL controls separately: 9/9 tests passed across mdl_enumerator, mdl_official, and mdl_synthetic. These cover same-declared-width candidate comparison and multiplication recovery, label-independent recovery of the four official semantics, recovery of twelve unseen synthetic functions, and the random/permuted-label negative control. This is evidence that the added generic search surface is not limited to the old four-family label/unique-width lookup path; it is not a claim that the forward A-D circuits are globally minimum.

Independent certificate cross-check

I built drat-trim directly from pinned checker commit 2e3b2dc0ecf938addbd779d42877b6ed69d9a985 and checked the committed CNF/DRAT pairs:

Complete n=2 inverse relation	Explicit circuit check	Lower-bound proof
Add	5 gates; 8/8 rows; 0 mismatches	4-gate DRAT: s VERIFIED
AbsDiff	1 gate; 4/4 rows; 0 mismatches	0-gate DRAT: s VERIFIED
Multiply	8 gates; 16/16 rows; 0 mismatches	7-gate DRAT: s VERIFIED

All six CNF/DRAT SHA-256 values matched their public manifests. The 67,381,560-byte Multiply proof also returned HTTP 200 from its unauthenticated raw.githubusercontent.com URL.

This audit removes the concrete #115 reviewability blocker: the Rust implementation is now public source and reproducible from an immutable commit rather than a pointer to a private repository. The scientific boundary remains explicit: the certified minima above apply only to the stated n=2 inverse relations and do not prove the original forward A-D circuits globally minimal, larger-width minima, or asymptotic optimality.