[codex] add Bug Zoo v0

[TSavo]

What changed

This PR adds the first executable Bug Zoo slice:

• Documents the key ProofIR lemma: ProofIR may be lossy because it is universal over contract boundaries, not host-language implementation detail.
• Adds paper 09, Lossy Boundary Compression: Why ProofIR Is Universal Because It Forgets.
• Adds bug-zoo/ with the first live species, BZ-SHAPE-005-java-null-boundary-equivalence.
• Adds a Java ProvekIt-native lifter surface and shared Java contract expression parsing so ProvekIt-native, Spring Web, JML, and Cofoja surfaces can converge on canonical ProofIR predicates without copied parsers.
• Adds provekit zoo, a Rust CLI runner that validates specimen manifests, runs host checks, invokes specimen-owned lifter RPC launchers, compares canonical ProofIR CIDs, checks the expected missing edge, and emits strict JSON output.
• Adds a Rust smoke test that runs the actual provekit zoo command against the Java specimen when Maven/JDK are available.

Why

The zoo is meant to prove that bug species are executable objects, not static advisory prose. The first specimen demonstrates the core claim: ordinary code passes its host checks, two different contract surfaces lift to the same ProofIR boundary, and the missing edge becomes reproducible and content-addressed:

maybe_null(name) => non_null(name)

This is exposed, not patched. The historical fix is not the oracle; the protocol catches the missing obligation.

Validation

Passed locally:

• mvn -f implementations/java/pom.xml -pl provekit-lift-java-integration-tests -am test -Dtest=CrossDomainContractEquivalenceTest
• mvn -f implementations/java/pom.xml -pl provekit-lift-java-core,provekit-lift-java-provekit-native,provekit-lift-java-spring-web,provekit-lift-java-integration-tests -am test
• cd implementations/rust && cargo test -p provekit-cli cmd_zoo::tests
• cd implementations/rust && cargo test -p provekit-cli --test zoo_smoke
• cd implementations/rust && cargo run -p provekit-cli -- zoo ../../bug-zoo/species/BZ-SHAPE-005-java-null-boundary-equivalence --json

Final JSON check returned ok: true; the provekit-native and spring-web ProofIR CIDs were identical:

blake3-512:0d611d8478a205ff040e7d0bcf6c21b12051340ecc5f00c3953af632b23fc01e069b4ad8a8699869163e135b9fde85792eba6acc54cd75cb3d3cc6a40a99ded4

Notes

The working tree still contains unrelated local changes outside this PR scope. This branch stages only the Bug Zoo/ProofIR slice.

Summary by CodeRabbit

Release Notes

• New Features

  • Added provekit proof and provekit zoo CLI subcommands for contract verification and cross-framework boundary comparison
  • Introduced Bug Zoo framework enabling equivalent contract boundary verification across different implementations (initial Java null-boundary specimen)
  • Added support for ProvekIt-native contract annotation extraction

• Documentation

  • New whitepaper on lossy boundary compression and ProofIR universality
  • Added Bug Zoo design specification and implementation guidance
  • Enhanced README clarifying canonical projection and boundary contract terminology

• Tests

  • Added integration tests for cross-domain contract equivalence verification
  • Added smoke test for Bug Zoo specimen workflow validation

[coderabbitai]

Caution

Review failed

The pull request is closed.

ℹ️ Recent review info

⚙️ Run configuration

Configuration used: Organization UI

Review profile: CHILL

Plan: Pro

Run ID: 1b7b6da9-4cb1-403a-a4bd-f4fbae10380e

📥 Commits

Reviewing files that changed from the base of the PR and between 61e4442 and abe832e.

⛔ Files ignored due to path filters (1)

• implementations/rust/Cargo.lock is excluded by !**/*.lock

📒 Files selected for processing (41)

• README.md
• bug-zoo/README.md
• bug-zoo/species/BZ-SHAPE-005-java-null-boundary-equivalence/.gitignore
• bug-zoo/species/BZ-SHAPE-005-java-null-boundary-equivalence/README.md
• bug-zoo/species/BZ-SHAPE-005-java-null-boundary-equivalence/exposed/equivalence.json
• bug-zoo/species/BZ-SHAPE-005-java-null-boundary-equivalence/exposed/provekit-native/expected-diagnostic.txt
• bug-zoo/species/BZ-SHAPE-005-java-null-boundary-equivalence/exposed/provekit-native/expected.proofir.json
• bug-zoo/species/BZ-SHAPE-005-java-null-boundary-equivalence/exposed/provekit-native/harness/src/main/java/com/provekit/contract/Requires.java
• bug-zoo/species/BZ-SHAPE-005-java-null-boundary-equivalence/exposed/provekit-native/harness/src/main/java/zoo/UserDirectory.java
• bug-zoo/species/BZ-SHAPE-005-java-null-boundary-equivalence/exposed/provekit-native/kit-rpc/run-java-lifter.sh
• bug-zoo/species/BZ-SHAPE-005-java-null-boundary-equivalence/exposed/sat-witness.json
• bug-zoo/species/BZ-SHAPE-005-java-null-boundary-equivalence/exposed/spring-web/expected-diagnostic.txt
• bug-zoo/species/BZ-SHAPE-005-java-null-boundary-equivalence/exposed/spring-web/expected.proofir.json
• bug-zoo/species/BZ-SHAPE-005-java-null-boundary-equivalence/exposed/spring-web/harness/src/main/java/org/springframework/web/bind/annotation/RequestParam.java
• bug-zoo/species/BZ-SHAPE-005-java-null-boundary-equivalence/exposed/spring-web/harness/src/main/java/zoo/UserDirectory.java
• bug-zoo/species/BZ-SHAPE-005-java-null-boundary-equivalence/exposed/spring-web/kit-rpc/run-java-lifter.sh
• bug-zoo/species/BZ-SHAPE-005-java-null-boundary-equivalence/lab/harness/run.sh
• bug-zoo/species/BZ-SHAPE-005-java-null-boundary-equivalence/lab/harness/src/main/java/zoo/UserDirectoryHarness.java
• bug-zoo/species/BZ-SHAPE-005-java-null-boundary-equivalence/lab/kit-rpc/README.md
• bug-zoo/species/BZ-SHAPE-005-java-null-boundary-equivalence/lab/library/src/main/java/zoo/UserDirectory.java
• bug-zoo/species/BZ-SHAPE-005-java-null-boundary-equivalence/specimen.yaml
• bug-zoo/species/BZ-SHAPE-005-java-null-boundary-equivalence/wild/README.md
• docs/papers/09-lossy-boundary-compression.md
• docs/papers/README.md
• docs/superpowers/plans/2026-05-06-bug-zoo-v0.md
• docs/superpowers/specs/2026-05-06-bug-zoo-design.md
• implementations/java/pom.xml
• implementations/java/provekit-lift-java-cofoja/src/main/java/com/provekit/lift/cofoja/CofojaExtractor.java
• implementations/java/provekit-lift-java-core/src/main/java/com/provekit/lift/AnnotationSupport.java
• implementations/java/provekit-lift-java-core/src/main/java/com/provekit/lift/ContractExpressionParser.java
• implementations/java/provekit-lift-java-integration-tests/pom.xml
• implementations/java/provekit-lift-java-integration-tests/src/test/java/com/provekit/lift/CrossDomainContractEquivalenceTest.java
• implementations/java/provekit-lift-java-jml/src/main/java/com/provekit/lift/jml/JmlExtractor.java
• implementations/java/provekit-lift-java-provekit-native/pom.xml
• implementations/java/provekit-lift-java-provekit-native/src/main/java/com/provekit/lift/provekitnative/ProvekitNativeExtractor.java
• implementations/java/provekit-lift-java-provekit-native/src/main/resources/META-INF/services/com.provekit.lift.Extractor
• implementations/rust/provekit-cli/Cargo.toml
• implementations/rust/provekit-cli/src/cmd_proof.rs
• implementations/rust/provekit-cli/src/cmd_zoo.rs
• implementations/rust/provekit-cli/src/main.rs
• implementations/rust/provekit-cli/tests/zoo_smoke.rs

---

Walkthrough

This PR implements Bug Zoo v0, an executable infrastructure for verifying that heterogeneous host-language contract representations canonicalize to identical boundary predicates. The changes include ProofIR documentation and lossy-compression rationale, a Java null-boundary specimen with two implementations, unified contract expression parsing across extractors, and a Rust CLI that orchestrates specimen verification via lift RPC and ProofIR CID comparison.

Changes

Bug Zoo v0: Specimen Infrastructure & Lossy Boundary Compression

Layer / File(s)	Summary
Concept & Design Documentation README.md, docs/papers/*, docs/superpowers/*	Reframe ProvekIt thesis as boundary-focused lossy compression; introduce ProofIR universality via obligatioin preservation. Add full whitepaper on lossy-boundary compression, Bug Zoo design spec, and v0 implementation plan.
Java Core Contract Parsing Utilities implementations/java/provekit-lift-java-core/src/main/java/com/provekit/lift/*	Extract AnnotationSupport.belongsToFamily() for family-based annotation matching and ContractExpressionParser with tokenizer and recursive-descent parser for universal contract expression → JSON-AST conversion.
Unified Extractor Refactoring implementations/java/provekit-lift-java-cofoja/..., implementations/java/provekit-lift-java-jml/...	Refactor CofojaExtractor and JmlExtractor to delegate expression parsing to shared ContractExpressionParser instead of embedding parsing logic; reduce code duplication.
ProvekitNativeExtractor Implementation implementations/java/provekit-lift-java-provekit-native/..., implementations/java/pom.xml	Create new Maven module with ProvekitNativeExtractor implementing Extractor for @Requires/@Ensures/@invariant annotations; register via ServiceLoader; wire into parent POM and integration tests.
BZ-SHAPE-005 Specimen Definition bug-zoo/species/BZ-SHAPE-005-java-null-boundary-equivalence/	Define complete specimen with lab baseline (UserDirectory.lookup), two exposures (provekit-native using @Requires, spring-web using @RequestParam), lift RPC scripts, expected ProofIR/diagnostics, equivalence spec, and sat-witness artifacts.
Java Integration & Testing Updates implementations/java/provekit-lift-java-integration-tests/*	Add ProvekitNativeExtractor dependency to integration tests; extend CrossDomainContractEquivalenceTest to verify native annotations lift to same IR as Bean Validation across null and numeric constraints.
Rust CLI Implementation implementations/rust/provekit-cli/src/cmd_proof.rs, implementations/rust/provekit-cli/src/cmd_zoo.rs, implementations/rust/provekit-cli/src/main.rs	Implement cmd_proof for proof artifact validation and cmd_zoo for specimen orchestration including manifest parsing, host-check execution, lift RPC invocation with JSON-RPC plumbing, ProofIR canonicalization/hashing, CID comparison, and equivalence verification.
End-to-End Integration Testing implementations/rust/provekit-cli/tests/zoo_smoke.rs	Add smoke test verifying BZ-SHAPE-005 specimen end-to-end: Java/Maven preflight, provekit zoo --json execution, JSON parsing, ok/error validation, and proof IR CID equality between native and spring-web surfaces with blake3-512 prefix.

Estimated code review effort

🎯 4 (Complex) | ⏱️ ~60 minutes

The PR spans heterogeneous changes across documentation (high-level framing), Java architecture (extractor unification and new module), and Rust CLI implementation (manifest orchestration and RPC plumbing). While individual layers are coherent, the breadth of changes and the need to verify integration across Java/Rust/specimen requires careful attention to data flow, RPC contract, CID canonicalization, and test assertions.

Poem

🐰 A thousand boundary paths now converge,
ProofIR's forgetting makes them merge—
ProvekIt-native talks to Spring's demand,
One lossy truth, content-addressed, and planned!
Bug Zoo opens wide to show the way,
Same CID sings across the day. 🌿

✨ Finishing Touches

📝 Generate docstrings

• Create stacked PR
• Commit on current branch

🧪 Generate unit tests (beta)

• Create PR with unit tests
• Commit unit tests in branch codex/bug-zoo-v0

---

Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out.

❤️ Share

• X
• Mastodon
• Reddit
• LinkedIn

_{Comment @coderabbitai help to get the list of available commands and usage tips.}

[TSavo]

I found a build-blocking issue: the branch wires in a new proof subcommand but does not include the backing module, so provekit-cli fails to compile.

[TSavo]

This branch adds mod cmd_proof; and routes the proof subcommand through cmd_proof, but it does not add implementations/rust/provekit-cli/src/cmd_proof.rs. macOS CI is failing with error[E0583]: file not found for module cmd_proof, and any normal Rust build of provekit-cli will fail until the module is added or these references are removed.