Skip to content

Commit 6ed0675

Browse files
docs(architecture): cross-repo proof DAG design (closes C14 estate blocker) (#217)
## Summary Design-only PR (no impl) for the estate-blocker **C14** from the 2026-06-03 audit: today, when a producer like `ephapax/formal/` changes, downstream consumers (`proven`, `valence-shell`, `verisimdb`) don't re-verify until manual notice — drift window measured in weeks. The doc lands at `docs/architecture/CROSS-REPO-PROOF-DAG.md` and captures: - **Where edges live** — consumer-declared `.machine_readable/proof-deps.a2ml`, ingested by echidna, dispatched by hypatia. Consumers know what they pull; producers don't need to know who pulls them. - **Schema** (A2ML v1.0, mirrors C12 tolerance shape — unknown fields ignored, forward-compat). - **Discovery** — manual v1; automatic v2 parking on `verisimdb#3`. - **Trigger semantics** — path-grained, coalesced, backpressured, fail-open on dispatcher unreachable. - **Failure semantics** — malformed deps / unreachable refs / dependency cycles / `fail_open` overrides. - **Concrete walk-through** — ephapax → {valence-shell, verisimdb, proven}. - **Four owner decisions** flagged explicitly: edge ref policy, issue vs comment, echo-types special case, `fail_open` default. - **Acceptance criteria** for the future impl PR. ## Why this PR is design-only The doc enumerates the producer/consumer pairs already in the estate (ephapax, echo-types, kategoria, tropical-resource-typing, vcl-ut) and aligns with [[feedback_proofs_must_check_and_cross_doc_echo_types]]. The owner-decision section needs sign-off before implementation begins — committing the design first means the impl PR can move fast once the four open questions are settled. ## What this unblocks - **C16** (GNN outcome-feedback loop) — per-edge success/failure is the cross-repo training signal. - **F25** (cross-prover RDF alignment) — empirical ground-truth set for translation. - **D22** (estate trust badge) — defines what "fully verified estate" means. ## Test plan - [x] Doc cross-links existing files (`CORRECTNESS-ARCHITECTURE.md`, `VERISIM-ER-SCHEMA.md`) — those file paths verified to exist. - [x] Producer/consumer table reflects the actual estate (ephapax↔valence-shell↔verisimdb↔proven). - [ ] Owner reviews the four open decisions and answers in PR comments. ## Estate context This PR is **#2 of 5** in the C12/C14/C15/B7/D18 critical-blocker pass coming out of the echidna estate-scale audit. - C12 PR (echidnabot): hyperpolymath/echidnabot#84 - C15 PR: in flight (gitbot-fleet) - B7 + D18 PRs: queued 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
1 parent 9eef662 commit 6ed0675

0 file changed

File tree

    0 commit comments

    Comments
     (0)