Skip to content

Commit bd83308

Browse files
hyperpolymathclaude
hyperpolymath
and
claude
committed
docs(architecture): cross-repo proof DAG design (closes C14 estate blocker)
Closes the estate-onboarding blocker C14 surfaced in the "what stops echidna from running proof work across the estate" audit: when ephapax `formal/` changes, downstream consumers (proven, valence-shell, verisimdb) do not re-verify until manual notice. The DAG turns that drift window from "weeks" into "the next dispatcher cycle". Design only — no impl. Captures: * Where edges live (consumer-declared `.machine_readable/ proof-deps.a2ml` ingested by echidna; hypatia dispatches). * A2ML schema v1.0 mirroring the C12 manifest tolerance shape (unknown fields ignored, forward-compat). * Discovery: manual v1; automatic v2 (parking on verisimdb#3 cross-prover canonicalisation). * Trigger semantics: path-grained, coalesced, backpressured, fail-open on dispatcher unreachable. * Failure semantics for malformed deps, unreachable refs, dependency cycles, fail_open overrides. * Concrete walk-through: ephapax→{valence-shell, verisimdb, proven}. * Four open decisions explicitly flagged for the owner: edge ref policy, issue vs comment, echo-types special case, fail_open default. * Acceptance criteria for the future impl PR. Estate context: this design names known producer/consumer pairs already in the estate (ephapax, echo-types, kategoria, tropical-resource-typing, vcl-ut) and aligns with the existing echo-types audit rule ([[feedback_proofs_must_check_and_cross_doc_echo_types]]). Cross-references to the rest of the audit punch list: C12 (echidnabot manifest), C15 (hypatia push-fixes wiring), C16 (GNN feedback loop), D22 (estate trust badge), F25 (verisimdb#3 cross-prover RDF). Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
1 parent 04e0e92 commit bd83308

1 file changed

Lines changed: 306 additions & 0 deletions

File tree

‎docs/architecture/CROSS-REPO-PROOF-DAG.md‎

Lines changed: 306 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,306 @@
1+
<!--
2+
SPDX-License-Identifier: MPL-2.0
3+
SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
4+
-->
5+
6+
# Cross-Repo Proof Dependency DAG
7+
8+
**Status**: Design draft — implementation not yet started.
9+
**Closes**: estate blocker **C14** from the 2026-06-03 audit
10+
("when ephapax `formal/` changes, downstream consumers don't re-verify").
11+
12+
---
13+
14+
## Problem
15+
16+
The estate carries several producer/consumer proof relationships that
17+
the current per-repo CI shape does not honour:
18+
19+
| Producer | Path | Known consumers |
20+
|-----------------|-------------------------------|---------------------------------------------------|
21+
| `ephapax` | `formal/PRESERVATION-*.v` | `valence-shell`, `verisimdb`, `proven` |
22+
| `echo-types` | `formal/echo/*.v` | `ephapax` (L3 obligations), `valence-shell` |
23+
| `kategoria` | `formal/*.v` | `verisimdb`, downstream HP type-checker repos |
24+
| `tropical-resource-typing` | `formal/*.v` | `verisimdb` (Q1 foundation) |
25+
| `vcl-ut` | `formal/*.v` | `verisimdb` (P3, V2 foundation pack) |
26+
27+
Today, when a producer's proofs change, no automatic signal walks the
28+
DAG to re-verify downstream. Transitive correctness drift goes
29+
unnoticed until a manual reviewer notices, or until a consumer's own CI
30+
happens to re-run against the new producer SHA. That can be weeks.
31+
32+
This is **C14** in the 2026-06-03 audit's punch list.
33+
34+
---
35+
36+
## Scope (this doc) vs out-of-scope
37+
38+
In-scope:
39+
- Where the DAG lives.
40+
- Edge format (TOML / A2ML).
41+
- Edge-discovery rules (manual + automatic).
42+
- Trigger semantics (which webhook fires which downstream jobs).
43+
- Failure semantics (degraded mode when a consumer can't be reached).
44+
45+
Out-of-scope:
46+
- Term-level proof translation between Coq ↔ Lean ↔ Agda — that is
47+
cross-prover canonicalisation, blocked on `verisimdb#3`.
48+
- Per-theorem dependency tracking (i.e. "only re-verify proofs whose
49+
imports actually touched the producer hunk"). v1 is repo-grain only;
50+
per-theorem precision is a follow-up once the v1 plumbing is real.
51+
52+
---
53+
54+
## Where the DAG lives
55+
56+
**Recommendation: edges declared per-consumer; aggregation in echidna.**
57+
58+
```text
59+
consumer repo echidna (estate dispatcher)
60+
───────────── ─────────────────────────────
61+
.machine_readable/ ┌─────────────────┐
62+
proof-deps.a2ml ───── ingest ───────► │ proof_dag.toml │
63+
│ (synthesised │
64+
consumer repo │ per-fetch) │
65+
───────────── │ │
66+
.machine_readable/ └─────────┬───────┘
67+
proof-deps.a2ml ───── ingest ───────► │
68+
▼
69+
┌─────────────────┐
70+
│ hypatia │
71+
│ (push fixes / │
72+
│ enqueue jobs) │
73+
└─────────┬───────┘
74+
│
75+
▼
76+
┌─────────────────┐
77+
│ echidnabot │
78+
│ (per-repo CI) │
79+
└─────────────────┘
80+
```
81+
82+
Rationale:
83+
84+
- **Edges live in the consumer**, not the producer. Producers shouldn't
85+
need to know who depends on them; the reverse direction (consumer
86+
declares what it pulls from) matches how Coq/Lean/Agda imports already
87+
work and means no producer-side coordination is needed when a new
88+
consumer onboards.
89+
- **Aggregation in echidna** because echidna is already the estate's
90+
prover-aware dispatcher (`src/rust/provers/`, prover-class scheduling,
91+
trust-bridge), and the dispatch decision needs prover metadata that
92+
echidnabot doesn't carry.
93+
- **Trigger orchestration in hypatia** because hypatia is the estate-CI
94+
intelligence layer that already coordinates `gitbot-fleet` and the
95+
"push committed fixes to remotes" contract (see the C15 PR).
96+
97+
---
98+
99+
## Edge format
100+
101+
A new file `proof-deps.a2ml` joins the existing
102+
`.machine_readable/bot_directives/` family:
103+
104+
```toml
105+
# .machine_readable/proof-deps.a2ml
106+
schema_version = "1.0"
107+
directive_type = "proof-deps"
108+
109+
# Each [[depends_on]] entry is one edge from this consumer to a producer.
110+
[[depends_on]]
111+
producer = "hyperpolymath/ephapax"
112+
ref = "main" # branch | tag | exact-sha
113+
paths = ["formal/PRESERVATION-*.v"] # producer-side globs
114+
local_uses = ["formal/L3-ECHO/**/*.v"] # consumer-side proofs that
115+
# transitively rely on producer
116+
rationale = "L3 echo obligations re-use ephapax's preservation_l3."
117+
# Optional gating override:
118+
fail_open = false # if true: producer red doesn't block consumer CI
119+
# (default false — producer red ⇒ consumer red).
120+
121+
[[depends_on]]
122+
producer = "hyperpolymath/echo-types"
123+
ref = "main"
124+
paths = ["formal/echo/*.v"]
125+
local_uses = ["formal/L3-ECHO/EchoAxioms.v"]
126+
rationale = "Echo-types canonical axioms; echo-types audit recorded."
127+
```
128+
129+
Schema notes:
130+
131+
- `producer` is `<owner>/<repo>` — platform-agnostic; same shape works
132+
for Codeberg / Radicle once those adapters land.
133+
- `ref` is normally `main`; per-edge SHA pins are allowed for
134+
reproducibility-critical consumers (e.g. release branches).
135+
- `paths` are producer-side globs — used both for edge invalidation
136+
("did this hunk touch a tracked path?") and for the v2 per-theorem
137+
story.
138+
- `local_uses` documents *why* the edge exists. Mostly for humans, but
139+
hypatia surfaces it in the PR comment so reviewers know what failed.
140+
- Tolerance: unknown fields are ignored. Same forward-compat shape as
141+
the C12 manifest.
142+
143+
---
144+
145+
## Discovery
146+
147+
Two discovery paths feed the DAG:
148+
149+
1. **Manual** — author commits `proof-deps.a2ml` declaring producers.
150+
This is the only path that v1 honours.
151+
2. **Automatic** (v2, after `verisimdb#3`) — extract producer references
152+
from Coq `Require Import`, Lean `import`, Agda `open import`. The
153+
estate's per-language imports vary too widely to do this safely in
154+
v1; a missing edge surfaces as a stale-proof failure within one
155+
producer-change cycle and the author adds it manually.
156+
157+
The aggregator (`echidna ingest-proof-deps`) walks each repo's
158+
`proof-deps.a2ml` via the same `PlatformAdapter::get_file_contents` path
159+
echidnabot already uses for `bot_directives/echidnabot.a2ml`. Edges are
160+
cached for 24h with ETag revalidation. No edge → no behaviour change.
161+
162+
---
163+
164+
## Trigger semantics
165+
166+
```text
167+
producer push to tracked path
168+
│
169+
▼
170+
webhook hits echidna ─────► consult ingested DAG, find consumers
171+
│ (forward edges by `paths` glob match)
172+
▼
173+
for each consumer:
174+
enqueue echidnabot job
175+
payload: { repo, ref, reason: "upstream change",
176+
upstream: { producer, sha, paths } }
177+
│
178+
▼
179+
echidnabot runs that repo's proof check (per C12 manifest)
180+
│
181+
▼
182+
result → comment on producer commit + open / update consumer issue
183+
"ephapax@abc1234 broke valence-shell@formal/L3-ECHO/EchoAxioms.v"
184+
```
185+
186+
Trigger details:
187+
188+
- Path-grained: only producers' commits that touch a tracked `paths`
189+
glob fan out. Touching producer README, CI, or non-tracked source
190+
does not enqueue anything.
191+
- Coalesced: multiple pushes within a 60s window collapse to one
192+
downstream job per consumer.
193+
- Backpressure: hypatia's existing concurrency limits (per-repo
194+
semaphore + global cap) apply. Cascade fan-out is bounded.
195+
- Fail-open: if echidna's DAG cache is stale or unreachable, fall back
196+
to "no edges" — never block producer CI on the dispatcher being down.
197+
198+
---
199+
200+
## Failure semantics
201+
202+
| Condition | Behaviour |
203+
|--------------------------------------------|--------------------------------------------|
204+
| Consumer's `proof-deps.a2ml` is malformed | Log warning; treat as "no edges". No CI block on the consumer. |
205+
| Producer ref not reachable (deleted branch / private repo) | Edge skipped; warning surfaced in the consumer's next PR. |
206+
| Consumer CI red after upstream-triggered run | Issue opened in consumer repo, label `blocked-on:<producer>#<sha>`; `fail_open` overrides this to advisory-only. |
207+
| Producer red + `fail_open = false` | Consumer's `merge_block` (per C12 manifest) gates merges to consumer-main. |
208+
| DAG cycle (A → B → A) | Detected at ingest; cycle edge dropped + filed as `echidna#<issue>` with both repos labelled. v1 logs only; v2 hard-fails ingestion. |
209+
210+
---
211+
212+
## Concrete walk-through
213+
214+
```text
215+
2026-06-XX 10:00 ephapax main pushes commit abc1234
216+
touching formal/PRESERVATION-L3.v
217+
218+
10:00:02 echidna webhook receives push event
219+
matches DAG glob "formal/PRESERVATION-*.v"
220+
consumers: { valence-shell, verisimdb, proven }
221+
222+
10:00:03 hypatia enqueues 3 echidnabot jobs:
223+
valence-shell @ main (proof-set: formal/L3-ECHO/**/*.v)
224+
verisimdb @ main (proof-set: formal/foundation-pack/**)
225+
proven @ main (proof-set: formal/echo-leak/*.v)
226+
227+
10:00:08 echidnabot dispatches Coq jobs (per each repo's
228+
C12 manifest provers list)
229+
230+
10:01:42 results land:
231+
valence-shell GREEN
232+
verisimdb RED (preservation_l3 fails on L2-modality lemma)
233+
proven GREEN
234+
235+
10:01:44 echidna posts comment on ephapax abc1234:
236+
"Downstream impact: verisimdb red — preservation_l3 fails
237+
against L2-modality lemma at line 412."
238+
Opens issue verisimdb#NNN with full diff + the failing
239+
proof excerpt. Adds label "blocked-on:ephapax@abc1234".
240+
```
241+
242+
---
243+
244+
## Open decisions for the owner
245+
246+
1. **Edge ref policy**: do all consumers default to `ref = "main"`, or
247+
should release-branch consumers be required to pin a SHA? Tradeoff:
248+
pinned SHAs are reproducible but go stale; `main` is current but can
249+
silently flip.
250+
2. **Issue spam vs PR comment**: when a producer's main breaks a
251+
consumer, do we open an issue per consumer (high signal, can pile
252+
up) or just comment on the producer commit (no follow-up nudge)?
253+
3. **Echo-types special case**: echo-types is the L3 canonical axioms
254+
producer for ephapax (per estate policy
255+
[[feedback_proofs_must_check_and_cross_doc_echo_types]]). Should
256+
echo-types ↔ ephapax edges be auto-injected by echidna without a
257+
`proof-deps.a2ml` declaration, or stay opt-in like everything else?
258+
4. **`fail_open` default**: producer red ⇒ consumer red is the safer
259+
default but it means an upstream's bad-day red-CI cascades. Should
260+
`fail_open = true` be the default and `fail_open = false` be the
261+
opt-in for hard-coupled consumers?
262+
263+
---
264+
265+
## What this design unblocks
266+
267+
Closing C14 makes three other audit blockers more tractable:
268+
269+
- **C16** (GNN outcome-feedback loop) — per-edge success/failure
270+
signals are exactly the cross-repo training data the GNN currently
271+
doesn't see.
272+
- **F25** (cross-prover RDF alignment, blocked on `verisimdb#3`) — the
273+
DAG gives an empirical ground-truth set of co-evolving proof pairs,
274+
which is the input that translation work needs.
275+
- **D22** (no single green "trust pipeline verified" badge) — the DAG
276+
defines what "fully verified estate" means: every edge green.
277+
278+
---
279+
280+
## Acceptance criteria for the implementation PR (out of scope here)
281+
282+
When this design is implemented:
283+
284+
- [ ] `echidna ingest-proof-deps` walks all repos that echidna already
285+
knows about, parses any `.machine_readable/proof-deps.a2ml`,
286+
and builds `proof_dag.toml` at the daemon level.
287+
- [ ] Producer webhooks fan out via `EdgeEnvelope` events on the
288+
existing `dispatch.rs` channel.
289+
- [ ] hypatia's enqueue path accepts `EdgeEnvelope` and routes to
290+
echidnabot exactly as it does for direct-push events.
291+
- [ ] Cycle detection runs at ingest and logs (v1) / hard-fails (v2).
292+
- [ ] Three estate-shaped fixtures: ephapax→valence-shell,
293+
echo-types→ephapax, kategoria→verisimdb.
294+
- [ ] Sad-path: unreachable producer ref, malformed `proof-deps.a2ml`,
295+
consumer mid-rebase. All degrade gracefully.
296+
297+
---
298+
299+
## See also
300+
301+
- C12 PR — per-repo manifest schema v2.0 (echidnabot).
302+
- C15 PR — hypatia push-fixes wiring (gitbot-fleet).
303+
- `docs/architecture/CORRECTNESS-ARCHITECTURE.md` — the soundness
304+
invariant the DAG must not violate.
305+
- `docs/architecture/VERISIM-ER-SCHEMA.md` — where ingested edges
306+
eventually persist for cross-prover analytics.

0 commit comments

Comments
 (0)