Reachability Lattice & Scoring Model

Status: v0 implemented in Signals (bucket model); v1 lattice model in design (Sprint 0401). Owners: Scanner Guild · Signals Guild · Policy Guild. Audience: Signals and Policy engineers, and anyone consuming reachability scores in release gates.

Stella Ops models reachability as a deterministic, evidence-linked outcome that can safely represent “unknown” without silently producing false safety. Signals produces a ReachabilityFactDocument with per-target states[] and a top-level score that is stable under replays.

This guide covers two layers:

• §1–§8 — the v0 bucket model, which is live in Signals today and drives current policy decisions.
• §9 — the v1 formal lattice model, a forward design that adds algebraic join/meet operations over a 7-state lattice.

Public vocabulary (D4/D9, ratified + contract implemented 2026-06-10): the buckets and states in this guide are internal scoring vocabulary. The only verdict vocabulary that may cross a public boundary (Console, CLI, VEX, policy expressions, OCI referrer payloads) is the §7.0 lattice of reachability-sink-strategy.md— reachable:proven / reachable:likely / not-observed / unknown (+ not-present, reserved for L2 linker facts, not emittable yet) — implemented canonically as PublicReachabilityVerdict in src/Scanner/__Libraries/StellaOps.Scanner.Contracts/PublicReachabilityVerdict.cs with machine-checked naming rules (no public unreachable/safe string) and per-verdict minimum-evidence gates (not-observed always carries a coverage statement). The v0 unreachable bucket therefore surfaces publicly as not-observed + coverage, never as a plain “unreachable”. Signals bucket scoring is rebased onto the public verdict (2026-06-11, sprint SPRINT_20260610_002 LATTICE): when the recompute request carries a scan-side PublicReachabilityVerdictObject for a target (ReachabilityRecomputeRequest.PublicVerdicts, fed from Scanner’s GET /reachability/verdicts/{imageDigest}), Signals consumes it 1:1 — the state’s bucket IS the lattice wire name, the v1 lattice state folds from the verdict via ReachabilityLattice.FromPublicVerdict (joining Signals’ runtime lane), and no Signals-side BFS runs for that target. The v0 bucket recompute described in §1–§8 is the fallback only for targets with no verdict object.

1. Current model (Signals v0)

Signals scoring (src/Signals/StellaOps.Signals/Services/ReachabilityScoringService.cs) computes, for each target symbol:

• reachable: whether there exists a path from the selected entryPoints[] to target.
• bucket: a coarse classification of why the target is/was reachable.
• confidence (0…1): a bounded confidence value.
• weight (0…1): bucket multiplier.
• score (0…1): confidence * weight.
• path[]: the discovered path (if reachable), deterministically ordered.
• evidence.runtimeHits[]: runtime hit symbols that appear on the chosen path.

The fact-level score is the average of per-target scores, penalized by unknowns pressure (see §4).

2. Buckets & default weights

Bucket assignment is deterministic and uses this precedence:

1. unreachable — no path exists.
2. entrypoint — the target itself is an entrypoint.
3. runtime — at least one runtime hit overlaps the discovered path.
4. direct — reachable and the discovered path is length ≤ 2.
5. unknown — reachable but none of the above classifications apply.

Default weights (configurable via SignalsOptions:Scoring:ReachabilityBuckets):

3. Confidence (reachable vs unreachable)

Default confidence values (configurable via SignalsOptions:Scoring:*):

Rules:

• Base confidence is reachableConfidence when reachable=true, otherwise unreachableConfidence.
• When reachable=true and runtime evidence overlaps the selected path, add runtimeBonus (bounded by maxConfidence).
• The final confidence is clamped to [minConfidence, maxConfidence].

4. Unknowns pressure (missing/ambiguous evidence)

Signals tracks unresolved symbols/edges as Unknowns (see docs/modules/signals/guides/unknowns-registry.md). The number of unknowns for a subject influences the final score:

unknownsPressure = unknownsCount / (targetsCount + unknownsCount)
pressurePenalty  = min(unknownsPenaltyCeiling, unknownsPressure)
fact.score       = avg(states[i].score) * (1 - pressurePenalty)

Default unknownsPenaltyCeiling is 0.35 (configurable).

This keeps the system deterministic while preventing unknown-heavy subjects from appearing “safe” by omission.

5. Evidence references & determinism anchors

Signals produces stable references intended for downstream evidence chains:

• metadata.fact.digest — canonical digest of the reachability fact (sha256:<hex>).
• metadata.fact.version — monotonically increasing integer for the same subjectKey.
• Callgraph ingestion returns a deterministic graphHash (sha256) for the normalized callgraph.

Downstream services (Policy, UI/CLI explainers, replay tooling) should use these fields as stable evidence references.

6. Policy-facing guidance (avoid false “not affected”)

Policy should treat unreachable (or low fact score) as insufficient to claim “not affected” unless:

• the reachability evidence is present and referenced (metadata.fact.digest), and
• confidence is above a high-confidence threshold.

When evidence is missing or confidence is low, the correct output is under investigation rather than “not affected”.

7. Signals API pointers

• Signals reachability guide — fact ingest and scoring flow.
• Signals unknowns registry — how unresolved symbols/edges are tracked.
• Signals OpenAPI — generated endpoint contract.

8. Roadmap (tracked in Sprint 0401)

• Introduce first-class uncertainty state lists + an entropy-derived riskScore.
• Extend evidence refs to include CAS/DSSE pointers for graph-level and edge-bundle attestations (see Hybrid attestation).

9. Formal Lattice Model v1 (design — Sprint 0401)

The v0 bucket model provides coarse classification. The v1 lattice model introduces a formal 7-state lattice with algebraic join/meet operations for monotonic, deterministic reachability analysis across evidence types.

9.1 State Definitions

9.2 Lattice Ordering (Hasse Diagram)

                    Contested (X)
                   /     |     \
                  /      |      \
     ConfirmedReachable  |  ConfirmedUnreachable
          (CR)           |          (CU)
           |  \         /           / |
           |   \       /           /  |
           |    \     /           /   |
     RuntimeObserved  RuntimeUnobserved
          (RO)              (RU)
           |                 |
           |                 |
     StaticallyReachable  StaticallyUnreachable
          (SR)              (SU)
                \          /
                 \        /
                  Unknown (U)

9.3 Join Rules (⊔ — least upper bound)

When combining evidence from multiple sources, use the join operation:

U  ⊔ S  = S          (any evidence beats unknown)
SR ⊔ RO = CR         (static reachable + runtime hit = confirmed)
SU ⊔ RU = CU         (static unreachable + runtime miss = confirmed)
SR ⊔ RU = X          (static reachable but runtime miss = contested)
SU ⊔ RO = X          (static unreachable but runtime hit = contested)
CR ⊔ CU = X          (conflicting confirmations = contested)
X  ⊔ *  = X          (contested absorbs all)

Full join table:

9.4 Meet Rules (⊓ — greatest lower bound)

Used for conservative intersection (e.g., multi-entry-point consensus):

U  ⊓ *  = U          (unknown is bottom)
CR ⊓ CR = CR         (agreement preserved)
X  ⊓ S  = S          (drop contested to either side)

9.5 Monotonicity Properties

1. Evidence accumulation is monotonic: Once state rises in the lattice, it cannot descend without explicit revocation.
2. Revocation resets to Unknown: When evidence is invalidated (e.g., graph invalidation), state resets to U.
3. Contested states require human triage: X state triggers policy flags and UI attention.

9.6 Mapping v0 Buckets to v1 States

9.7 Policy Decision Matrix

9.8 Implementation Notes

• State storage: ReachabilityFactDocument.states[].latticeState field (enum)
• Join implementation: ReachabilityLattice.Join(a, b) in src/Signals/StellaOps.Signals/Services/
• Backward compatibility: v0 bucket computed from v1 state for API consumers

9.9 Evidence Chain Requirements

Each lattice state transition must be accompanied by evidence references:

{
  "symbol": "sym:java:...",
  "latticeState": "CR",
  "previousState": "SR",
  "evidence": {
    "static": {
      "graphHash": "blake3:...",
      "pathLength": 3,
      "confidence": 0.92
    },
    "runtime": {
      "probeId": "probe:...",
      "hitCount": 47,
      "observedAt": "2025-12-13T10:00:00Z"
    }
  },
  "transitionAt": "2025-12-13T10:00:00Z"
}

Related documentation

• Reachability evidence policy gates — how lattice states gate VEX status transitions.
• Evidence schema — richgraph-v1 evidence fields.
• Signals reachability guide — runtime + static union and scoring.