feat(2c-G): the fresh owner baseline — strangers compose from the caught-up V_k, history falls back to the immutable birth anchor (PR 3 of 3: G3)

[cryptskii]

PR 3 of 3 for amendment 2c-G, following the owner's delivery ruling of 2026-09-11. This PR implements G3: the fresh owner baseline. It is cut from main after PR 2 (#864) merged.

The owner ruled on three implementation questions for this PR. Those answers are recorded verbatim in the 2c-G doc, §0 "G3 implementation rulings":

• anchor once, after the catch-up run;
• move strangers too, with the anchor and the reserve-proof locator together;
• switch the owner's record in the freeze transaction, and advertise only once the new baseline is quorum-durable.

What this does

After every catch-up, finished or stopped, the last fully materialized generation V_k becomes the owner's authenticated baseline. Once that baseline is quorum-durable, strangers compose from it instead of replaying history from birth.

The anchor.

• plan_owner_baseline takes the walk's own certified V_k, meaning the frontier or a folded parent. It never rebuilds or supplies one.
• A generation the walk did not certify has no state there at all, so an uncertified successor can never be absorbed into a baseline.
• plan_owner_baseline checks every validity condition in the ruling:
  • the vault;
  • the materialized generation;
  • the parent link to the chain just consumed;
  • reserves equal to the owner's admitted leaves, matched by asset;
  • the authenticated storage set, from both the record and the walk;
  • canonical encoding, meaning the state round-trips and commits to c_k.
• owner_baseline_presentation builds the anchor with the same owner-anchor machinery as the birth baseline (build_own_anchor_presentation). It then verifies it with the stranger's own verify_anchor_presentation before keeping it.

The reserve proof. A settle takes the owner's backing from the advertisement's proof. It also requires the composed history, which starts at the advertisement's anchor, to pass through that proof's generation. An anchor ahead of its proof would therefore refuse every settle.

• vault_reserve_proof_at_admitted_head builds the proof from the owner's admitted state: the vault's two reserve leaves under the validated root. It uses the same one-snapshot guard as an admission's own artifact.
• A crash that loses the last apply's AdmittedOutcome cannot leave the anchor ahead of its proof.

One transaction freezes the following, advances the record's baseline, and moves the record's proof locator:

• CCB(V_k) and its presentation, for the vault's storage set;
• the proof, for the root-register set.

This switch is local bookkeeping. Freezing an identical (key, digest) a second time is a no-op, so re-freezing the proof the last admission already froze is safe.

The advertisement. advertise_owner_baseline moves the advertisement only when all of these hold:

• both baseline objects are at quorum;
• the proof can be fetched by content address, exactly as a trader fetches it;
• the proof's generation is not behind the anchor's.

routing_sdk::republish_advertisement_baseline then writes the anchor digest, the proof locator and the reserves in one read-modify-write, and increments updated_state_number. Every other field the owner published is preserved.

Until the advertisement moves, the old, already-published baseline stays valid and trading continues. The advertisement is discovery only: a trader still authenticates the anchor and verifies the proof against the owner's registered root.

Semantics.

• Re-anchoring is idempotent and never moves the baseline backwards.
• The anchor authorizes, re-certifies and re-realizes nothing.
• Nothing trader-side waits on it.

The G3 blocker ruling — the immutable birth anchor

Running the first version exposed a contradiction with the ruling as written. Moving the advertisement's anchor made every earlier settle unverifiable:

• Lineage validation re-runs each past trader settle's 0x0026 reserve-provenance check.
• That check composed history from the advertisement's current anchor.
• Once the anchor passed an older owner proof's generation, the history could no longer reach it, and the check failed with HistoryMissesBaseline or NotTheComposedState.

I stopped and asked. The owner's ruling is recorded verbatim in §0 as "G3 blocker ruling": keep the vault's immutable birth anchor in the advertisement. It is implemented as follows.

• Wire extension. RoutingVaultAdvertisementV1 field 20, birth_anchor_presentation_digest, is transport and discovery metadata, not a new authority object.
  • dsm_app_pb.ts was regenerated with the repo's own proto:gen flags and the vendored protoc. The diff is 13 lines, the field only.
  • A new birth_presentation_digest record column is set once, inside dlv.create's own transaction. Its setter refuses to change the value.
  • The route publisher names the birth anchor, and the baseline republish preserves it.
• History resolution.
  • composed_vault_history now carries from_generation, the owner proof's baseline generation, through the core seam: two defaults, one delegate, and three SDK implementations. The 0x0026 arm and the settle preflight pass it.
  • compose_discovered_inner composes a history walk from the current anchor when that anchor's generation is at or before the needed one, and from the birth anchor otherwise.
  • The birth anchor must decode as this vault's generation-0 state with the genesis parent. It is then authenticated by the same P0–P6 verification as any anchor. A substituted "birth" anchor is refused.
• Result. New quotes, trades and settles compose from the fresh anchor. Historical re-validation composes from birth and stays stable forever.

A related local fix: a dlv.reconcile replay of a settlement applied before the owner's current baseline is satisfied by its consume-once claim and writes nothing. The walk now starts at that baseline, so the settlement is no longer among its folds.

Formal

lean4/DSMFreshBaseline.lean is the 22nd module, and ci.yml now expects 22. It proves:

• the baseline never moves backwards;
• it anchors only a materialized, certified generation;
• re-anchoring is idempotent;
• a freshly frozen baseline starts pending;
• a pending baseline is never advertised;
• every advertisement names an anchor its proof reaches;
• composition reaches the same frontier from any baseline;
• a history walk always reaches the generation it needs and prefers the current anchor (the blocker ruling).

Mutations, each proved as the negation of a named sample, with the unmutated control refused:

• L1: remove the backwards guard;
• L2: remove the quorum gate;
• L3: anchor past the materialized generation;
• L4: drop the birth fallback.

Tests

These are targeted --release runs, filtered by each edited module's path. CI is the board.

dsm

• dlv::composed_history:: unit tests: 9/0.

• Integration binaries that exercise the 0x0026 history arm: economic_dlv_settle_provenance 16/0, economic_provenance_wire 18/0, economic_root_primitives 26/0, bundle_acceptance_write_set 12/0, trader_acceptance_producer 9/0.

  provenance.rs and peer_lineage.rs have no unit tests of their own. The trait change is covered by these binaries.

dsm_sdk lib

• handlers::dlv_routes::: 62 of 63 passed on the full run. The one failure was a test whose premise the blocker ruling made obsolete; it was rewritten and now passes (1/0). Details below.
• handlers::storage_routes:: 20/0 (1 ignored), sdk::economic_admission_flow:: 1/0, sdk::vault_state_composition:: 17/0, sdk::routing_sdk:: 15/0, sdk::routing_path_sdk:: 43/0.
• sdk::route_commit_sdk:: 4/0, storage::client_db::amm_vault_records:: 12/0, handlers::route_routes:: 6/0, sdk::economic_registers:: 17/0.

New route tests

• a_caught_up_owner_moves_its_baseline_and_strangers_compose_from_it:
  • the fresh baseline is exactly V_2, and the advertisement moves with its anchor and proof together;
  • the owner and a stranger both compose from V_2 with no replayed history, and reach an identical c_n;
  • a third trader settles, the next catch-up anchors V_3, and a repeat pass with nothing owed writes nothing.
• a_partial_catch_up_anchors_only_its_last_fully_applied_generation.
• the_baseline_plan_refuses_every_altered_fact (pure). It refuses altered reserves, an uncertified generation, another storage set, a broken parent link, and a generation with no parent.
• a_baseline_below_quorum_never_moves_the_advertisement. The advertisement stays put while publication fails, trading continues off it, and it moves once publication heals.
• a_proof_that_predates_its_anchor_still_settles_through_the_birth_fallback.
• history_walks_fall_back_to_the_immutable_birth_anchor_and_refuse_a_substituted_one.

Dependent test changed

• The close round-trip now counts 6 immutable objects instead of 4: birth, plus the G3 baseline, plus terminal.

The rewritten test. The first run was 55/6, with two root causes:

• A (local): replaying a settlement applied before the owner's baseline failed. Fixed via its consume-once claim.
• B (the blocker): moving the anchor made earlier settles unverifiable. Fixed per the owner's blocker ruling.

After those fixes, round 2 was 62/1. The one failure asserted that an advertisement pairing the fresh anchor with the birth proof refuses settles. The birth fallback now makes that pairing harmless, so the test was rewritten to assert the settle goes through.

Lean: 22/22 modules. L1–L4 are red on their named samples, and each unmutated control refuses.

Mutation controls

Each mutation is applied to a byte copy of the file. A named test is run, and the file is then restored and checked byte-for-byte.

#	Mutation	Test that goes red
B1	drop the advertisement's quorum gate	a_baseline_below_quorum_never_moves_the_advertisement: "a pending baseline never becomes the discovery baseline"
B2	re-anchor the same generation (<= → <)	stays green; see the finding below
B3	drop the parent-link check	the_baseline_plan_refuses_every_altered_fact: "a broken parent link must not plan"
B4	the republish keeps the ad's old proof while the anchor moves	a_caught_up_owner_moves_its_baseline_and_strangers_compose_from_it: anchor and proof no longer move together
B5	drop the admitted-reserves check	the_baseline_plan_refuses_every_altered_fact: "altered reserves must not plan"
B6	drop the birth fallback	history_walks_fall_back_to_the_immutable_birth_anchor_and_refuse_a_substituted_one: "it starts at birth"
B7	drop the birth-state check	the same test: the substituted anchor is accepted

Finding (B2). Re-anchoring an already-anchored generation is byte-idempotent even without the <= short-circuit:

• the presentation signature is deterministic, so the record's presentation bytes come out identical;
• a freeze of an identical (key, digest) is a no-op;
• the record rewrite writes the same bytes;
• the advertisement republish reports unchanged.

The short-circuit therefore saves work; it is not a gate. Its "never backwards" half guards a state that cannot occur, because the record baseline never runs ahead of the admitted generation (a close moves both). The idempotence property itself is asserted by the test and proved in Lean. The test's doc comment had claimed this control goes red; it is corrected in the second commit.

Two earlier controls were invalid and were redefined before the run:

• B4 first renamed a call to a function that does not exist, so it could not compile.
• B6 and B7 were added for the blocker ruling.

The runner treats any could not compile as an invalid control.

Gates:

• make lint exits 0. Its one eslint warning is in frontend code this PR does not touch.
• ci/production_safety_checks.sh exits 0: clippy with production lints, plus TLA+.

Docs

• 2c-G doc §0: the owner's G3 implementation rulings, verbatim.
• sofispecs.instructions.md Req 6.31: now marked implemented, with the birth-anchor fallback.
• 2c-G doc §0: the G3 blocker ruling, verbatim.