Skip to content

fix(sofi): beta blockers: S14, A8/S15 settled before P15-9, and a dead cell skipped before its evidence (0241) - #1082

Merged
cryptskii merged 10 commits into
mainfrom
fix/sofi-beta-blockers
Oct 1, 2026
Merged

cryptskii merged 10 commits into
mainfrom
fix/sofi-beta-blockers

Conversation

@cryptskii

@cryptskii cryptskii commented Sep 30, 2026 •

Copy link
Copy Markdown
Collaborator

SoFi and SDK fixes that beta needs, gathered into one PR at the owner's direction (2026-09-30). This is a draft: more lands here, and the evidence pins are refreshed once, at the end.

1. SoFi Amendment S14: a final cell whose fulfillment can never register is skipped (MR-SOFI-0239, MR-SOFI-0343)

Owner ruling, 2026-09-30. route_impossible carried a fifth arm, PositionLost. §23.5 does not list it, and it depended on a particular fulfillment. It is now a skip of its own, RejectedFinalInadmissible, and RouteImpossible keeps the four arms of §23.5.

  • Spec: Amendment S14 in §23.5.
  • Core:
    • ImpossibleArm::PositionLost is deleted.
    • SkipReason::RejectedFinalInadmissible sits in classify_attempt, after FulfillmentImpossible.
    • New test: route_impossibility_reads_nothing_about_a_particular_fulfillment.
  • Lean: positionLost moves from RouteImpossible to finalSkippable. New theorems: route_impossibility_reads_no_fact_about_F and a_lost_position_makes_a_final_cell_skippable.
  • TLA: comments only.
  • Mutations: Rust ×2 and Lean ×2; each turns a named test or theorem red.

2. DSM Amendment A8 (frontier-relative verification) and SoFi Amendment S15 (a trader's position resolved from public objects)

Owner ruling, 2026-09-30. It settles how a payee accepts a payer, before P15-9 (a trader who has traded cannot pay) is fixed. Today, acceptance walks the payer's whole lineage from genesis and replays every step from evidence fetched from the nodes. That is not the spec's model, and it depends on the plaintext objects G16 records.

  • A8.
    • A receiver never replays a payer's history. Historical semantic validity is inherited through accepted authenticated state; root continuity is checked forward from the receiver's own authenticated frontier, which is the payer's activation root where it has none.
    • Only the offered step is fully validated, plus provenance one hop back.
    • "The register proves which signed claim occupies each authoritative position in that lineage and excludes a conflicting claim from also being authoritative there."
  • S15.
    • A SoFi position inside the frontier-to-parent segment is resolved from SoFi's public objects for that position alone. The result is the selected root, Invalid, or not established.
    • It has no fallback walk.
    • SetupValid reads the setup claim through the root chain.
    • Adoption is the trader's own construction predicate, and a later verifier does not re-run it.
  • Records:
    • MR-DSM-0273–0276 and MR-SOFI-0344–0348 are added.
    • MR-DSM-0275 and MR-SOFI-0347 are Violated today, because the whole-lineage walk replays history.
    • The specs are re-pinned in MASTER §1.

What follows:

  • DSM core builds the generic root-chain verifier.
  • This PR's author (SoFi/SDK) builds peer_position, the SDK presentation, and P15-9 on top of them.
  • P15-9 is proven on the nodes by a_trader_who_has_traded_can_pay, which fails on main today: the payer's balance drops while the payee never credits it.

3. MR-SOFI-0241: a dead cell is skipped before its evidence is fetched

A walk classifying a vault key used to acquire the exercise's full conformance and route evidence before looking at anything. A final cell that was dead on facts needing no evidence therefore stayed live while that evidence was outstanding, and the vault stalled.

It is now fixed as a classification order:

  • establish_ground builds the facts that need no evidence: registration, the trader parent, and each leg's cell and walk.
  • skip_without_evidence skips on any of:
    • arm (iii), a parent consumed elsewhere;
    • arm (iv), a trader parent that can never be compatible;
    • S14's lost position.
  • facts_of asks this before acquiring any evidence.
  • Registration::RootTaken makes S14 hold even when the trader never writes its fulfillment. Without it, a hostile trader could keep its dead cell live.

Proof on the nodes: a_key_whose_fulfillment_can_never_register_is_skipped_without_its_evidence.

  • A rival claim takes the trader's position, and the trader's exercise holds the vault's first key.
  • The request logs show the walk asked only for the key, the next key, the position pair, their chains, and the precommit the registration names.
  • The next key is live.
  • Mutation: with the evidence fetched first, the test goes red, naming the object read.

Records: MR-SOFI-0241 moves from Violated to Partial. Arm (ii), an orphaned parent, still needs the generation that only the vault's pre-state evidence carries.

Local runs (release)

  • dsm crate: 1,607 passed, 0 failed.
  • dsm_sdk SoFi, node end-to-end and peer suites: 24 passed, 0 failed.
  • make lint: exit 0.
  • Lean DSMSofiSuccessorCells: clean, no sorry.
  • ci/conformance_evidence.py: 794 rows, 0 failures; SoFi 219 Met, 5 Violated.

…ed (SoFi Amendment S14)

Owner ruling 2026-09-30 on MR-SOFI-0239. route_impossible carried a fifth
arm, PositionLost, which §23.5 does not list and which depends on a
particular F. Without it, an exercise whose fulfillment can never register
(another claim holds its position) strands the DLV parent's attempt chain
(TLA LostPosition).

- Spec: Amendment S14 in §23.5, a separate skip RejectedFinalInadmissible;
  RouteImpossible(P, E) keeps its four arms. MASTER re-pinned; MR-SOFI-0343.
- Core: ImpossibleArm::PositionLost deleted; SkipReason::RejectedFinalInadmissible
  in classify_attempt, after FulfillmentImpossible, so in-hand refutations
  classify as before. New test: route_impossible reads no fact about F.
- Lean: positionLost leaves RouteImpossible for finalSkippable (route or single
  leg); route_impossibility_reads_no_fact_about_F (rfl) and
  a_lost_position_makes_a_final_cell_skippable. TLA and README: comments.
- Mutations: the lost position back in route_impossible, and the skip removed,
  each turn named tests red; both Lean mutations red.
- Records: MR-SOFI-0239 Met, MR-SOFI-0343 Met, the §6.14 conflict row resolved.
# Conflicts:
#	specs/requirements/CONFORMANCE_GAPS.md
#	specs/requirements/INTENT_MANIFEST.tsv
…rader's position resolved from public objects (SoFi Amendment S15)

Owner ruling 2026-09-30. A receiver never replays a payer's history:
historical semantic validity is inherited through accepted authenticated
state, and root continuity is checked forward from the receiver's own
authenticated frontier (the payer's activation root where it has none).
Only the offered step is fully validated, plus provenance one hop back.
A SoFi position inside that segment is resolved from SoFi's public objects
for that position alone; adoption is the trader's own construction
predicate and is not re-run by a later verifier.

- Explainer: Amendment A8 after A4. SoFi: Amendment S15 at the end of §24.
- MASTER: §1 re-pinned; §7.1 entry; MR-DSM-0273–0276, MR-SOFI-0344–0348.
- CONFORMANCE: the nine rows as they stand today (MR-DSM-0275 and
  MR-SOFI-0347 Violated: the whole-lineage walk replays history); the open
  P15-9 row points at the ruling; totals regenerated.
@cryptskii cryptskii changed the title fix(sofi): beta blockers: Amendment S14, and a trader who has traded can pay (P15-9) fix(sofi): Amendment S14; frontier-relative verification (A8, S15) settled before P15-9 Sep 30, 2026
@cryptskii
cryptskii marked this pull request as ready for review September 30, 2026 22:33
…SOFI-0241)

A walk classifying a vault key acquired the exercise's full conformance and
route evidence before it looked at anything, so a final cell dead on facts
that need no evidence stayed live while that evidence was outstanding, and
the vault stalled. Fixed as a classification order:

- facts: establish_ground (registration, trader parent, each leg's cell and
  walk) is the first stage of establish, which builds on it.
- resolution: skip_without_evidence skips on arm (iii) a parent consumed
  elsewhere, arm (iv) a trader parent that can never be compatible, and
  S14's lost position; a new KeyKnown::Ground arm in the walk.
- resolve: read_legs / complete_facts; facts_of (walked keys only) skips a
  dead cell before acquiring evidence; establish_own reads complete facts.
- registration: Registration::RootTaken when no fulfillment is final at
  K_ful(q) and K_root(q) is held, so S14's lost position holds without the
  trader writing its fulfillment; the facts weigh it against F's own C_q.

Tests: four resolution unit tests (each arm, nothing that needs evidence,
a consistency sweep against classify_attempt, a walk past a dead key) and a
node test proving from the request logs that no evidence object is asked
for. Mutations: evidence first, arm removed, final-on-E removed: all red.
Records: MR-SOFI-0241 Violated -> Partial (arm (ii) still needs the
generation the evidence places); MR-SOFI-0343 note; matrix and manifest.
@cryptskii cryptskii changed the title fix(sofi): Amendment S14; frontier-relative verification (A8, S15) settled before P15-9 fix(sofi): beta blockers: S14, A8/S15 settled before P15-9, and a dead cell skipped before its evidence (0241) Sep 30, 2026
# Conflicts:
#	specs/requirements/CONFORMANCE_GAPS.md
…, one hop deep

Owner ruling 2026-09-30 (raised by DSM core): an authenticated root and a
valid state transition are different facts. A root claim is self-signed, so
a payer could register a root holding a fabricated credit, and a receiver
that only authenticated the root chain would accept a spend of it; a
counterparty's acceptance does not stand for validity when that
counterparty is malicious or the same owner.

A8 now: for each position of the frontier-to-parent segment the receiver
authenticates the authoritative root claim and verifies the transition
producing it against its authenticated parent, with that transition's
directly required evidence and provenance one hop back; verification never
recurses behind that hop and never reads behind the frontier.
MR-DSM-0273 and MR-DSM-0275 rewritten; S15's SetupValid line and
MR-SOFI-0347 follow; MASTER §1 re-pinned; the two rows' notes updated.
# Conflicts:
#	specs/requirements/CONFORMANCE_GAPS.md
Against CI's code-map artifact of a1302cc (Code map run 36793770529,
tree fingerprint equal to this tree's), with the evidence of the 158 rows
run at a1302cc (99 tests: dsm 70, dsm_sdk 28, dsm_storage_node 1;
99 passed, 0 failed).

- 154 rows whose closures this PR's code moved, code class only: repinned.
- MR-SOFI-0239, MR-SOFI-0343 and MR-SOFI-0241 (two symbols): pinned.

The comparator reads 0 failing rows and 602 of 602 pins PINNED.
# Conflicts:
#	specs/requirements/CONFORMANCE_GAPS.md
#	specs/requirements/INTENT_PINS.tsv
#	specs/requirements/MASTER_REQUIREMENTS.md
CI's code map of f874698 (run 36797712743), whose tree fingerprint equals
this tree's, reads 523 PINNED, 76 PIN_STALE (every move code only, from
main's code under these rows) and 3 UNPINNED.

- The 76 are repinned with a plain repin at f874698. Their 64 evidence
  tests passed here in release, on a Postgres of this session's own:
  dsm_sdk lib 27/0, dsm lib 32/0, and the economic_lineage_register,
  economic_write_set, native_reserve_wire and economic_admission_lifecycle
  suites.
- The 3 new rows (MR-SOFI-0239 route_impossible; MR-SOFI-0241
  establish_ground and skip_without_evidence) are pinned at f874698 on
  that run's Pin evidence log.

The comparator reads 602 of 602 pins PINNED and 0 failing rows.
@cryptskii
cryptskii merged commit c0588e7 into main Oct 1, 2026
24 checks passed
cryptskii added a commit that referenced this pull request Oct 1, 2026
CI's code map of b7d9468 (run 36804115818), whose tree fingerprint equals
this tree's, reads 477 PINNED, 125 PIN_STALE (every move code only:
#1085's frontier verifier and #1082's code under these rows) and 7
UNPINNED.

- The 125 are repinned with a plain repin at b7d9468. Their 107 evidence
  tests passed here in release, on a Postgres of this session's own:
  dsm_sdk lib 31/0, dsm lib 64/0, and the economic_admission_lifecycle,
  economic_lineage_register, economic_write_set, native_reserve_wire and
  economic_provenance_semantics suites.
- #1085's 7 new rows are pinned at b7d9468 on that run's Pin evidence
  log: MR-DSM-0273 to 0276, MR-SOFI-0344 (peer_position,
  advance_peer_resolved) and MR-SOFI-0348.

The comparator reads 609 of 609 pins PINNED and 0 failing rows.
cryptskii added a commit that referenced this pull request Oct 1, 2026
…rader's position from public objects (SoFi S15) (#1085)

* fix(sofi): a final cell whose fulfillment can never register is skipped (SoFi Amendment S14)

Owner ruling 2026-09-30 on MR-SOFI-0239. route_impossible carried a fifth
arm, PositionLost, which §23.5 does not list and which depends on a
particular F. Without it, an exercise whose fulfillment can never register
(another claim holds its position) strands the DLV parent's attempt chain
(TLA LostPosition).

- Spec: Amendment S14 in §23.5, a separate skip RejectedFinalInadmissible;
  RouteImpossible(P, E) keeps its four arms. MASTER re-pinned; MR-SOFI-0343.
- Core: ImpossibleArm::PositionLost deleted; SkipReason::RejectedFinalInadmissible
  in classify_attempt, after FulfillmentImpossible, so in-hand refutations
  classify as before. New test: route_impossible reads no fact about F.
- Lean: positionLost leaves RouteImpossible for finalSkippable (route or single
  leg); route_impossibility_reads_no_fact_about_F (rfl) and
  a_lost_position_makes_a_final_cell_skippable. TLA and README: comments.
- Mutations: the lost position back in route_impossible, and the skip removed,
  each turn named tests red; both Lean mutations red.
- Records: MR-SOFI-0239 Met, MR-SOFI-0343 Met, the §6.14 conflict row resolved.

* docs(spec): frontier-relative verification (DSM Amendment A8) and a trader's position resolved from public objects (SoFi Amendment S15)

Owner ruling 2026-09-30. A receiver never replays a payer's history:
historical semantic validity is inherited through accepted authenticated
state, and root continuity is checked forward from the receiver's own
authenticated frontier (the payer's activation root where it has none).
Only the offered step is fully validated, plus provenance one hop back.
A SoFi position inside that segment is resolved from SoFi's public objects
for that position alone; adoption is the trader's own construction
predicate and is not re-run by a later verifier.

- Explainer: Amendment A8 after A4. SoFi: Amendment S15 at the end of §24.
- MASTER: §1 re-pinned; §7.1 entry; MR-DSM-0273–0276, MR-SOFI-0344–0348.
- CONFORMANCE: the nine rows as they stand today (MR-DSM-0275 and
  MR-SOFI-0347 Violated: the whole-lineage walk replays history); the open
  P15-9 row points at the ruling; totals regenerated.

* fix(sofi): a dead cell is skipped before its evidence is fetched (MR-SOFI-0241)

A walk classifying a vault key acquired the exercise's full conformance and
route evidence before it looked at anything, so a final cell dead on facts
that need no evidence stayed live while that evidence was outstanding, and
the vault stalled. Fixed as a classification order:

- facts: establish_ground (registration, trader parent, each leg's cell and
  walk) is the first stage of establish, which builds on it.
- resolution: skip_without_evidence skips on arm (iii) a parent consumed
  elsewhere, arm (iv) a trader parent that can never be compatible, and
  S14's lost position; a new KeyKnown::Ground arm in the walk.
- resolve: read_legs / complete_facts; facts_of (walked keys only) skips a
  dead cell before acquiring evidence; establish_own reads complete facts.
- registration: Registration::RootTaken when no fulfillment is final at
  K_ful(q) and K_root(q) is held, so S14's lost position holds without the
  trader writing its fulfillment; the facts weigh it against F's own C_q.

Tests: four resolution unit tests (each arm, nothing that needs evidence,
a consistency sweep against classify_attempt, a walk past a dead key) and a
node test proving from the request logs that no evidence object is asked
for. Mutations: evidence first, arm removed, final-on-E removed: all red.
Records: MR-SOFI-0241 Violated -> Partial (arm (ii) still needs the
generation the evidence places); MR-SOFI-0343 note; matrix and manifest.

* docs(spec): A8 corrected: every segment step's transition is verified, one hop deep

Owner ruling 2026-09-30 (raised by DSM core): an authenticated root and a
valid state transition are different facts. A root claim is self-signed, so
a payer could register a root holding a fabricated credit, and a receiver
that only authenticated the root chain would accept a spend of it; a
counterparty's acceptance does not stand for validity when that
counterparty is malicious or the same owner.

A8 now: for each position of the frontier-to-parent segment the receiver
authenticates the authoritative root claim and verifies the transition
producing it against its authenticated parent, with that transition's
directly required evidence and provenance one hop back; verification never
recurses behind that hop and never reads behind the frontier.
MR-DSM-0273 and MR-DSM-0275 rewritten; S15's SetupValid line and
MR-SOFI-0347 follow; MASTER §1 re-pinned; the two rows' notes updated.

* feat(economic): frontier-relative peer verification (DSM Amendment A8), core

The peer walk no longer replays a payer's lineage from its activation
root. It starts at the receiver's frontier (PeerFrontier) and validates
every step from there to the target from that step's own evidence. A
credit's source is checked one hop back: the source step is validated,
and its predecessor is authenticated by the source's root chain (claims
only, each claim's key proven by its manifest's authority evidence).
Nothing behind that hop or behind a frontier is read. Owner ruling
2026-09-30: every segment step, one hop.

- PeerFrontier: the payer's activation root, the coordinate a
  verification reached (reached_by), or one the receiver recorded
  (rehydrate_recorded). Private fields. It replaces ValidatedStart.
- PeerFrontiers: the receiver's store, one frontier per peer.
- ConditionalPositionResolver: a C_q inside a chain is resolved from
  SoFi's public objects (S15), and the chain continues from the root it
  selected. A C_q right after the activation root is Invalid, because no
  claim was accepted there for it to name.
- The walk's memo re-walk, cross-identity recursion and depth cap are
  gone.

dsm_sdk does not compile on this commit. Its peer walk wrappers and memo
store change next.

* feat(sdk): the receiver's frontier store and the A8 peer walk

The SDK verifies a peer from this device's frontier for it and records
that frontier only in the transaction that accepts a step from the peer
(DSM Amendment A8).

- Client schema 27. `peer_frontier` replaces `peer_economic_lineage`:
  each row holds a coordinate, its root and the claim accepted there.
  There is no Invalid re-walk and no `closure_stored` watermark.
- economic_registers: StoredFrontiers, and a single `resolve_peer` in
  place of the memo-aware walk, the cache-disabled walk and the memo
  writer.
  - `LiveRegisterResolver` and `RecordingResolver` both verify through
    it.
  - A C_q is resolved by SoFi's peer-position resolver.
- Prevalidation walks from the frontier on every attempt, publishes the
  closure it recorded as Stored, and carries the sender's reached
  frontier. The accept transaction records that frontier beside the
  pair's acceptance.
- Tests:
  - the recipient admission test now asserts the recorded frontier;
  - the two foreign-walk helpers drop the memo clear, since a device
    records no frontier for itself.

dsm_sdk still does not compile. The SoFi call sites (sofi_reads.rs,
sofi_flow.rs) and `VerifierContext::peer_position_resolver` are the
resolver half of this branch.

* feat(sofi): a trader's position resolved from public objects (SoFi Amendment S15)

- lineage: advance_resolved's derivation is shared (derive_resolved);
  advance_peer_resolved is the path of a verifier that is not the trader:
  the same verdict, root and accepted claim, without the adoption
  precondition, which is the trader's own construction predicate (S15).
  BalancesNotDerivable carries validation's refusal.
- resolve: Verifier::peer_position(previous, parent, held) runs the trader's
  stages over this verifier's reads for position q alone and the ladder
  inside advance_peer_resolved; held counts only as the claim (P, F) derive.
  Failures: Incomplete for a read not in hand, Unresolved for facts that do
  not decide q yet, Invalid only for a verified contradiction.
  PeerPositionResolver implements DSM core's ConditionalPositionResolver.
- facts: ResolvedParent (position, selected root, fulfillment) is what the
  facts read of a conditional parent; the SDK derives it from its admitted
  position, the resolver from the root the walk selected.
- node test a_trader_who_has_traded_can_pay (P15-9), red until the SDK
  wiring lands.

* feat(sofi): the SDK reads and relay verify another trader frontier-relatively (A8, S15)

- VerifierContext::peer_position_resolver(): Core's resolver of another
  trader's conditional position over the context's reads, for DSM core's
  frontier-relative walk.
- LiveSofiReads::peer_walk: resolve_peer with that resolver; vault_owner and
  accepted_claim_at use it, so SetupValid reads the trader's accepted claim
  by frontier-relative verification of its lineage (MR-SOFI-0347).
- sofi.relay's parent walk the same.
- resolve: the chain map filled through the entry API (clippy map_entry).

a_trader_who_has_traded_can_pay passes on the nodes (P15-9). Mutations: the
resolver refusing every C_q, and the resolver selecting the void root:
both red (the payee never credits). dsm 1609/0; dsm_sdk sofi, node e2e,
peer and admission suites 46/0.

* test(sdk): frontier-relative verification on the nodes (DSM Amendment A8)

Three node-backed tests.
- a_root_no_transition_explains_is_refused_where_it_sits
  - A device registers, under its own key, a final claim at position 2
    whose root no step of its produced.
  - A verifier meeting it first refuses the lineage at position 2 and
    reads nothing past it.
- a_receiver_reads_nothing_behind_its_frontier
  - B's frontier for A is the coordinate its acceptance verified.
  - When A pays again, B reads A's cell past the frontier and none at
    or behind it.
- a_credits_source_is_validated_one_hop_back_and_no_further
  - C pays A, and A pays B.
  - B validates C's paying step, reading C's claim at 1 and
    authenticating it by its manifest, but reads none of the evidence
    behind C's step at 1.

Also here: clippy clone_on_copy in peer_lineage (a ParentClaimRef is
Copy), and LiveRegisterResolver's doc now describes frontier-relative
verification.

* docs(core): §6.52 records frontier-relative verification; MR-DSM-0273–0276 Met

- MR-DSM-0273, 0274 and 0276 go Missing → Met.
- MR-DSM-0275 goes Violated → Met.
- Each row cites the verifier, the frontier store and the node tests.
- MR-DSM-0276 cites SOFI's `a_trader_who_has_traded_can_pay`.
- MR-DSM-0046 now cites `resolve_peer`, which replaces the deleted
  `resolve_peer_with_cache`.
- The §6 finding on the memo start is marked superseded.
- VERIFICATION_MATRIX gains the three A8 gates, each with its mutation
  control. INTENT_MANIFEST gains MR-DSM-0273–0276 as MUST_REACH from
  the JNI ingress; they are pinned from CI's map.

* docs(sofi): S15 records; adoption is not re-run by another verifier (test)

- lineage: another_verifier_resolves_the_position_without_the_traders_adoptions:
  the facts the trader's own advance refuses for want of an adoption advance
  another verifier to the same root and claim. Mutation: the adoption check
  run on the peer path -> red.
- resolve: peer_position's held-claim equality check removed: registration
  holds F registered only while K_root(q) is final on exactly C_q(P, F), so
  it could never fail; the comment cites where it is enforced.
- S15 "What it reads" made exact: the trader's accepted claims at the setup
  positions its legs name are inside the segment and read through A8.
  MR-SOFI-0346 follows; MASTER re-pinned.
- CONFORMANCE: MR-SOFI-0344, 0345, 0347, 0348 Met; 0346 Partial (bounded by
  the walk; no read-set test of the resolver's own yet); §6.52 SoFi side.
  Matrix rows for P15-9 and 0348; manifest rows for peer_position and
  advance_peer_resolved.

* docs(sofi): S15 "What it reads", the owner's ruling of 2026-09-30

The owner approved widening SoFi Amendment S15's "What it reads" bullet,
with this precision wording. The old "q only" sentence contradicted S15's
own SetupValid rule, which reads the trader's accepted claim at each setup
position the legs name.
- The read set is dependency-directed: within the verifier's
  frontier-to-parent segment it reads position q, the authenticated
  predecessor root at q − 1, and the accepted claim at each setup position
  explicitly named by P's committed legs, not a list the resolver selects.
- Each is authenticated through DSM Amendment A8.
- It reads no unrelated trader position and has no fallback lineage walk.

MR-SOFI-0346's text follows, and MASTER §1 re-pins the SoFi specification
(6fd1bd9…, 2656 lines; one line edited in place, so line-based IDs do
not move). ci/conformance_evidence.py passes (794 rows).

* fix(map): pins for #1085 at b7d9468

CI's code map of b7d9468 (run 36804115818), whose tree fingerprint equals
this tree's, reads 477 PINNED, 125 PIN_STALE (every move code only:
#1085's frontier verifier and #1082's code under these rows) and 7
UNPINNED.

- The 125 are repinned with a plain repin at b7d9468. Their 107 evidence
  tests passed here in release, on a Postgres of this session's own:
  dsm_sdk lib 31/0, dsm lib 64/0, and the economic_admission_lifecycle,
  economic_lineage_register, economic_write_set, native_reserve_wire and
  economic_provenance_semantics suites.
- #1085's 7 new rows are pinned at b7d9468 on that run's Pin evidence
  log: MR-DSM-0273 to 0276, MR-SOFI-0344 (peer_position,
  advance_peer_resolved) and MR-SOFI-0348.

The comparator reads 609 of 609 pins PINNED and 0 failing rows.

* fix(map): the trait-dispatch sentinel names OneHop, the walking resolver's successor

#1085 deletes the walking resolver: the genesis walk is replaced by
frontier-relative verification. The map's trait-dispatch sentinel named
dsm::economic::peer_lineage::WalkingResolver::ProvenanceResolver::anchored_policy_bytes,
which no longer exists, so requirement-map-check failed (sentinel-lost).
The four planted mutation cases that check against the sentinels failed
with it.

The sentinel now names OneHop::ProvenanceResolver::anchored_policy_bytes,
the resolver that validates a credit's source one hop back. It reads the
same: android reached REACHED_VIA_DISPATCH through trait dispatch on a
constructed resolver (CI's map of b7d9468, peer_lineage.rs:905).
rules.tsv's trait-dispatch row cites it.

Against that map, requirement-map-check reads 0 failures, and the planted
cases a-sentinel-reads-otherwise, an-entry-point-appears,
an-entry-point-goes and the-dead-turn-indeterminate pass. requirement_map's
rules test passes.

* fix(ci): the ladder check follows derive_resolved, the advances' private helper

#1085 moved the SoFi ladder call (resolve_position) out of advance_resolved
into derive_resolved, a private helper shared by advance_resolved and the
new advance_peer_resolved (DSM Amendment A8, SoFi Amendment S15).
ci/sofi_validated_root_constructors.sh looked only for the literal call
inside advance_resolved's body, so the Rust gates job failed ("advance_resolved
does not run the ladder"). The property still held: the verdict is derived
inside the advance, and no caller names it.

The check now accepts the ladder in advance_resolved itself or in
derive_resolved, and in the second case requires all of:
- derive_resolved is a private fn in sofi/lineage.rs;
- derive_resolved runs resolve_position;
- derive_resolved is called only from advance_resolved and
  advance_peer_resolved;
- nothing outside lineage.rs calls it.

Mutation controls on lineage.rs, each restored:
- derive_resolved made pub: red, "not a private fn";
- a third caller (advance_peer_resolved renamed): red, "a caller other than
  the two advances";
- its ladder call removed: red, "does not run the ladder".

bash ci/production_safety_checks.sh passes in full on this tree.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant