docs: record which half of the mirror relation applies to what

08fe300a6c87 · AtlantisPleb · · parent 342720ea8bb4

docs: record which half of the mirror relation applies to what

`EXIT-003` says the mirror is strictly lossy and never an input to recovery.
That is a claim about evidence, and it was being read as a claim about objects.
Before this repository's seed the relation is inverted: the log was seeded from
a `--depth=1` fetch (#179), so 307 commits exist only on the mirror and no
rebuild can produce them.

Re-measured on 2026-08-25, both sides cloned fresh: the forge serves 461
commits on `main`, `git fsck` clean, grafted at five `shallow` boundaries rooted
at the seed `eda094c6`; the mirror serves 767, rooted at `a352f78e`, and holds
`c91327d6`. `EXIT-004` is not violated by that — the clone succeeds and says
where it stops, which its #179 amendment already admits as clean — but the
forge is canonical for its own history only from the seed forward, and that is
now said without softening.

`docs/forge-operator-independence.md` also still carried the sentence #188
corrected in `INVARIANTS.md` and `CLAUDE.md`: that no mirror runs today. It is
where the mirror contract is written in prose, so it joins the guarded set in
`test/openagents/forge/independence_test.exs` rather than being corrected and
left to drift again.

The decision about the 307 commits is recorded with both rejected shapes.
Fabricating WAL entries would invent evidence, because a receipt derives from
every entry and those pushes did not happen. Stopping at "canonical from the
seed forward" leaves the forge's authority holding less than its mirror and the
only copy of a year of history on an account the operator does not control. So
the log gains the bytes and no assertion about who pushed them, which is what
`OpenAgents.Forge.Backfill.import_history/3` already does. Rehearsal 3 gains the
verified recipe: one 7.2 MB bundle from the mirror closes all five boundaries.

The import itself is not performed here. A WAL append cannot be undone, and a
node that cannot materialize it falls back to a rebuild from sequence zero that
rehearsal 3 records as unexercised live. That is an attended operation and is
tracked on its own.

Closes #188.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01SoZMfWRSGnf6FZX2Ar9rQ2
Co-Authored-By
Claude Fable 5 <noreply@anthropic.com>
Closes
#188

Deploy story

What this commit did to the running system — joined from the forge receipt chain, the part a commit page elsewhere cannot show.

Not deployed through the forge lane

No push, promotion, build, or deploy receipt references this commit (receipts are scanned over a bounded recent window). Changes shipped by full node replacement carry their proof in the release gate receipt instead.

Changed files

  • modified INVARIANTS.md
  • modified docs/forge-exit-rehearsals.md
  • modified docs/forge-operator-independence.md
  • modified test/openagents/forge/independence_test.exs

Diff

4 files changed, +201 -11

INVARIANTS.md modified +18 -1

@@ -4782,8 +4782,25 @@ what the forge last pushed there, which is the trade `REPOSITORY-002` records.

4782 4782
And `mirror_now/1` is a force push of every ref, so the mirror overwrites what a
4783 4783
direct push left there rather than merging with it.
4784 4784
4785
Amended 2026-08-25 (issue #188). "Strictly lossy" is a claim about evidence,
4786
and it was being read as a claim about objects. Where a repository's log was
4787
seeded from a shallow fetch, the mirror holds ancestors the WAL never held and
4788
no rebuild can produce — 307 commits for this repository, measured on both
4789
sides — so before the seed the mirror is strictly *richer* and is the only
4790
copy. The invariant is unchanged and the direction still holds: the recovery
4791
path consults no mirror, and a receipt still derives from the WAL alone.
4792
`OpenAgents.Forge.Backfill.import_history/3` closes such a gap the only way an
4793
append-only log can, by appending the missing objects as a `git_bundle` entry
4794
that leaves the ref map unchanged and asserts no push. It takes a file an
4795
operator supplies rather than reaching for a mirror, so it adds no call this
4796
invariant's proof would fail on, and it writes no principal, sequence, or time
4797
that would turn borrowed bytes into evidence of a push.
4798
`docs/forge-operator-independence.md` records which half of the relation
4799
applies to what.
4800
4785 4801
Evidence: `OpenAgents.Forge.Sync`, `OpenAgents.Forge.Pushes`,
4786
`OpenAgents.Forge.PushReceipt`, `OpenAgents.Forge.Verification`, and
4802
`OpenAgents.Forge.PushReceipt`, `OpenAgents.Forge.Verification`,
4803
`OpenAgents.Forge.Backfill`, `test/openagents/forge/backfill_test.exs`, and
4787 4804
`test/openagents/forge/independence_test.exs`.
4788 4805
4789 4806
### EXIT-004 — A clone is complete and self-hosting
docs/forge-exit-rehearsals.md modified +65

@@ -346,6 +346,52 @@ reported rather than reconciled silently.

346 346
   returns `:ok` on success and a typed error when the WAL cannot produce a
347 347
   servable projection. `EXIT-003` turns red if a mirror input is added.
348 348
349
4. Measure history rather than ref maps. Identical ref maps are not identical
350
   history, and this is the step that finds a seeded repository whose log holds
351
   less than its mirror does:
352
353
   ```sh
354
   git clone https://openagents.com/{owner}/{repo}.git forge && \
355
     git -C forge rev-list --count refs/heads/main && \
356
     cat forge/.git/shallow
357
   git clone https://github.com/{owner}/{repo}.git mirror && \
358
     git -C mirror rev-list --count refs/heads/main
359
   ```
360
361
   A `shallow` file on the forge side names the boundaries. Each boundary's
362
   parents are what the log does not hold, and the mirror is where they are.
363
364
5. Where the forge is behind, close it with the objects and not with invented
365
   evidence. `OpenAgents.Forge.Backfill.import_history/3` appends a bundle to
366
   the log as a `git_bundle` entry that leaves the ref map alone and claims no
367
   push. Build the bundle from the mirror, one branch per boundary parent:
368
369
   ```sh
370
   git -C mirror branch --force preseed-1 <parent-of-boundary-1>
371
   # ... one per boundary ...
372
   git -C mirror bundle create pre-seed.bundle preseed-1 preseed-2 ...
373
   git -C mirror bundle verify ../pre-seed.bundle
374
   ```
375
376
   Put the bundle on the node, inside the container, and import it:
377
378
   ```sh
379
   bin/openagents rpc 'OpenAgents.Forge.Backfill.open_boundaries("{storage_key}")'
380
   bin/openagents rpc 'OpenAgents.Forge.Backfill.import_history("{storage_key}", "/tmp/pre-seed.bundle", "operator:{who}")'
381
   ```
382
383
   `import_history/3` proves the bundle against a throwaway repository that
384
   borrows the projection's objects and refuses to write unless every
385
   boundary's recorded parents resolve and the union walks, because an
386
   append-only log cannot retract a bad entry. `{storage_key}` is the
387
   repository's storage key, not its name — `OpenAgents.Forge.RepoRef` is the
388
   only translator, and #190 is the defect that made the difference matter.
389
390
   This is a permanent write on a forge people are pushing to. Watch every node
391
   converge afterwards: a node that cannot materialize the entry falls back to
392
   a full rebuild from sequence zero, which step 3 records as unexercised
393
   against the live projection.
394
349 395
### Result, 2026-08-25
350 396
351 397
**Steps 1 and 2 pass against the live forge.** Both remotes advertise the same

@@ -368,6 +414,25 @@ behavior was exercised locally instead, by three tests in

368 414
live 423-commit projection is untested.
369 415
`docs/2026-08-25-forge-exit-rehearsals-2-to-6.md` records both halves.
370 416
417
**Step 4 re-measured later the same day, and step 5 is prepared but not run.**
418
A fresh clone of each side: the forge serves 461 commits on `main`, `git fsck`
419
clean, grafted at five `shallow` boundaries rooted at `eda094c6`; the mirror
420
serves 767, `git fsck` clean, rooted at `a352f78e`, and `git rev-list --count
421
eda094c6` there is 308 — the seed and its 307 ancestors. The counts are at
422
different tips because the forge was ahead; the gap is unchanged.
423
424
The mirror holds all five boundaries and each one's parent, so a single bundle
425
closes every boundary at once. Built from the mirror by the recipe in step 5
426
over `fdd00d4c`, `e0e61fb1`, `0fcbbbb8`, `f8a7822a`, and `c91327d6`, it is
427
7.2 MB and `git bundle verify` reports a complete history.
428
429
The import itself was not performed. It is a permanent append to a shared
430
production log, its failure mode is the fleet-wide rebuild step 3 has never
431
exercised live, and both belong to an attended operation rather than to a
432
read-only rehearsal. #188 records the decision — import the objects, keep the
433
push record starting at the seed — and
434
`docs/forge-operator-independence.md` carries the reasoning.
435
371 436
## 4. Key rotation
372 437
373 438
**Proves:** that no rotation invalidates an already-issued receipt, and that a
docs/forge-operator-independence.md modified +112 -9

@@ -254,20 +254,123 @@ from the WAL re-derives all of it; recovery from the mirror derives none of it,

254 254
and `EXIT-003` proves both halves.
255 255
256 256
Two operational facts belong here rather than in a footnote. First,
257
`:forge_mirror_urls` is empty in `config/config.exs` and set by no environment,
258
so no mirror runs today and GitHub holds whatever was last pushed to it
259
directly — `REPOSITORY-002` states that trade. Second, `mirror_now/1` is a
260
force push of every ref, so configuring a mirror overwrites whatever direct
261
pushes left there rather than merging with them.
257
`:forge_mirror_urls` is empty in `config/config.exs` but `config/runtime.exs`
258
reads `OPENAGENTS_FORGE_MIRROR_URLS_JSON`, and production sets it for
259
`openagents.com`, so a mirror does run and GitHub holds what the forge last
260
pushed there — `REPOSITORY-002` states that trade, and a direct push to GitHub
261
is overwritten rather than merged. Second, `mirror_now/1` is a force push of
262
every ref, which is the destructive half of that: it overwrites whatever the
263
mirror held rather than reconciling with it. Both statements were false here
264
until #188 measured the deployment against them.
265
266
### The mirror is lossy about evidence and richer about pre-seed objects
267
268
"The mirror is strictly lossy" is true of one thing and false of another, and
269
collapsing the two is what #188 found. The relation has two halves and a
270
boundary between them, and the boundary is the seed commit `eda094c6`.
271
272
**Everything the WAL records — the whole log, from the seed forward.** The
273
mirror is strictly lossy and is never an input to recovery. It carries objects
274
and refs and no evidence, so a forge restored from it serves the same source
275
with no record of who produced it. That is `EXIT-003`, and it is the half that
276
is load-bearing: the recovery path must not be able to consult GitHub, or
277
GitHub becomes authority by accident.
278
279
**Everything before the seed — 307 commits.** The relation is inverted. This
280
repository's log was seeded from a `--depth=1` fetch (#179), so the WAL holds
281
one commit per ref and no ancestry, and no rebuild can produce what the log
282
never held. Those commits are objects with no evidence attached anywhere: no
283
WAL entry, no sequence, no principal, no receipt. The mirror is the only copy
284
of them, which is exactly the input this document said was never an input.
285
286
Measured on 2026-08-25, both sides cloned fresh:
287
288
| Source | `main` commits | `git fsck` | Root of `main` | Holds `c91327d6` |
289
| --- | --- | --- | --- | --- |
290
| The forge | 461 | clean | `eda094c6`, the seed | no |
291
| GitHub mirror | 767 | clean | `a352f78e` | yes |
292
293
The counts are taken at different tips, because the forge was ahead of the
294
mirror when they were read; the gap itself is stable. `git rev-list --count
295
eda094c6` on the mirror is 308 — the seed and its 307 ancestors — and the forge
296
holds the seed alone.
297
298
The forge's clone is not broken by this and `EXIT-004` is not violated by it.
299
The clone succeeds, passes `git fsck`, and writes a `shallow` file naming five
300
reconciled boundaries, which is `EXIT-004`'s stated outcome after #179: history
301
that says where it stops is servable, and history that dangles is not. What is
302
true is narrower and worth saying without softening it — **the forge is
303
canonical for its own history only from the seed forward**, and a reader who
304
wants this repository's first 307 commits has to get them from the mirror.
305
306
### The decision about the 307 commits
307
308
Decided 2026-08-25 (#188): **import the objects, and do not manufacture the
309
evidence.** Three shapes were weighed.
310
311
**Import the objects and a push record for them.** Rejected, because it invents
312
evidence. A WAL entry carries a sequence, a principal, and a time, and
313
`OpenAgents.Forge.Pushes.reconcile_receipts/1` derives a receipt from every
314
entry. Writing entries that claim 307 pushes nobody made would publish receipts
315
for pushes that did not happen, in a log whose entire value is that a receipt
316
derives from the WAL and never from a second authority. Synthesizing the record
317
to make the count come out right destroys the thing the count was measuring,
318
and it is the defect class this tracker keeps finding.
319
320
**Record that the forge is canonical only from the seed forward, and stop.**
321
That is true, it is what this document now says about the present, and it is
322
not enough as an end state. It leaves the forge's own authority holding less
323
than its mirror does, so "GitHub is a mirror and never authority" reads as a
324
statement about the whole repository while being true only about evidence and
325
false about half the objects. It also leaves the only copy of this
326
repository's first year on an account the operator does not control, which is
327
the dependency this document exists to remove.
328
329
**Import the objects and keep the push record starting at the seed.** Chosen.
330
The objects and the evidence are different claims, and only one of them is
331
missing. The log gains the bytes; it gains no assertion about who pushed them.
332
333
`OpenAgents.Forge.Backfill.import_history/3` is that operation and it is
334
already written and proven — `test/openagents/forge/backfill_test.exs`, six
335
tests, including one that rebuilds from sequence zero afterwards and gets the
336
whole history back. It appends the bundle as an ordinary `git_bundle` entry
337
carrying the ref map unchanged, an empty shallow set, and a principal that
338
records who authorized the import rather than who authored the commits. It
339
proves the bundle against a throwaway repository sharing the projection's
340
objects and refuses to touch the log unless every boundary's recorded parents
341
resolve and the union walks the way `git upload-pack` walks it, because an
342
append-only log cannot retract a bad entry.
343
344
This does not weaken `EXIT-003`. The bytes arrive by an operator's hand on one
345
occasion, not by a code path reaching for GitHub: no module on the recovery
346
path gains a mirror call, and the proof that fails on one is untouched. What
347
changes afterwards is that the mirror stops being the only copy of anything.
348
349
**Not yet executed.** The bundle is built and verified — 7.2 MB, `git bundle
350
verify` reports a complete history, and it closes all five recorded boundaries
351
— and the recipe is in rehearsal 3 of `docs/forge-exit-rehearsals.md`. What is
352
left is a production write that cannot be undone: a WAL append is permanent by
353
design, `EXIT-005` makes removing an entry a rewrite of the whole suffix, and
354
if a node fails to materialize the new entry `OpenAgents.Forge.Sync` falls back
355
to a full rebuild from sequence zero, which rehearsal 3 records as never having
356
been run against the live projection. That is an attended operation on a forge
357
people are pushing to, not an unattended one, and it is tracked separately
358
rather than being described here as done.
262 359
263 360
## Exit
264 361
265 362
`EXIT-004` is the narrow claim that actually holds: a clone taken through the
266 363
published Git transport carries every advertised ref, every object behind those
267
refs, and re-serves the same history from somewhere else with the forge deleted.
268
The one omission is the `refs/internal/` namespace, where stack boundary
269
commits are retained without being advertised; the proof asserts that this is
270
the *only* omission, so withholding a branch would turn it red.
364
refs that the WAL holds, and re-serves the same history from somewhere else
365
with the forge deleted. The one withheld namespace is `refs/internal/`, where
366
stack boundary commits are retained without being advertised; the proof asserts
367
that this is the *only* withholding, so hiding a branch would turn it red.
368
369
Where a ref's history reaches back past what the WAL holds, the clone is
370
grafted rather than truncated: a `shallow` file names the boundary, and the
371
copy is complete with respect to what the forge has and honest about where that
372
stops. `EXIT-004`'s #179 amendment states that outcome. The pre-seed section
373
above says what is on the other side of the boundary and where it lives.
271 374
272 375
That is exit for source. It is not yet exit for everything, and the remaining
273 376
gaps are named rather than softened.
test/openagents/forge/independence_test.exs modified +6 -1

@@ -518,11 +518,16 @@ defmodule OpenAgents.Forge.IndependenceTest do

518 518
    # every ref, that made both documents promise the destructive thing was
519 519
    # switched off while it was switched on. Neither claim can return while
520 520
    # runtime still reads that variable.
521
    #
522
    # `docs/forge-operator-independence.md` joined the guarded set with #188:
523
    # it is where the mirror contract is written in prose, it carried the same
524
    # sentence, and the first pass corrected the two files a test named while
525
    # leaving the third to be found by hand a second time.
521 526
    test "does not claim a mirror is unconfigured while runtime configures one" do
522 527
      assert File.read!("config/runtime.exs") =~ "OPENAGENTS_FORGE_MIRROR_URLS_JSON",
523 528
             "the guard below is only meaningful while runtime reads this variable"
524 529
525
      for path <- ["INVARIANTS.md", "CLAUDE.md"] do
530
      for path <- ["INVARIANTS.md", "CLAUDE.md", "docs/forge-operator-independence.md"] do
526 531
        text = File.read!(path)
527 532
528 533
        for claim <- [

This page updates live while a promote is in flight · changelog