Verification layers

Verification Layers

Three-Layer Pipeline

Verification decomposes into three layers with distinct evaluation times and falsification targets. A loadout that fails Layer I cannot proceed to Layer II; a failure in Layer II renders Layer III meaningless.

Layer	Name	Evaluation Time	Primary Question
I	Static Structural	Template generation time	Does this template satisfy the algebraic laws of the primitive it instantiates?
II	Compositional	Loadout assembly time	Does this combination produce a well-formed trigger graph, and does it contain gain cycles?
III	Stochastic	Design time / seed validation	At what probability does this loadout cross the supercriticality threshold?

Layer I: Static Structural Verification

All checks in this layer are decidable at template parse time. They are treated as compilation errors.

• Trigger completeness: every declared trigger token exists in the global vocabulary.
• Effect emission closure: every EmitTrigger effect emits a known token.
• Charge cost non-negativity: ChargeCost >= 0 unless explicitly declared charge-granting.
• Cooldown positivity: Cooldown > 0 for all active skills.
• Modifier layer declaration: every modifier declares Additive or Multiplicative layer.
• CovarMatrix validity: the item template covariance matrix is positive semi-definite.
• StackBehavior declaration: every skill declares Exclusive, Additive, or Multiplicative stacking.

Layer II: Compositional Verification

The loadout trigger graph G(L) is a directed multigraph. Nodes are skill instances plus a synthetic empty-source node representing the environment. Edges are directed from skill S_i to S_j if any effect emission of S_i matches any trigger of S_j.

Structural checks:

• Reachability from source: every node must be reachable from the empty-source node.
• Condition satisfiability: every edge’s condition predicate must be satisfiable, decided by a three-tier dispatch over the condition string.

Condition satisfiability uses three tiers. A condition naming a vocabulary token is checked against the producible state registry and is satisfiable exactly when the registry contains that state. The registry unions ambient states with effect-derived states: ambient states hold for every loadout by domain construction, with ambient charge availability as the motivating case (every character carries a replenishing charge pool, so a charge_available gate is satisfiable independent of effect tokens), while effect-derived states are inferred from the loadout’s effect tokens. A condition in structured call form (kind(argument=value, ...)) is parsed into a typed temporality and evaluated by the evaluator registered for its kind at a witness context in which the condition just became true — the trigger instant for window conditions, the threshold boundary for accumulating conditions; a verdict that the condition does not hold there marks the targeting edges unsatisfiable. Parse failures and evaluator errors surface as distinct warnings (UNPARSEABLE_CONDITION, CONDITION_EVALUATION_ERROR) without flipping conditions_satisfiable, which stays reserved for genuine unsatisfiability. Any other condition string is opaque: provisionally satisfiable with an OPAQUE_CONDITION warning stating that satisfiability was not verified.

Gain cycle detection is performed via depth-first search. For each detected cycle C, compute gain(C) and cost(C) at maximum support values for the highest reachable tier as a conservative test.

Charge sustainability sub-check: compute the sustainability ratio eta = recovery_rate / consumption_rate. verify_compositional and run_pipeline accept an optional damage_rates carrier (DamageRateData in verification.py), and when it is supplied each skill’s charge economy is weighted by its declared execution rate: consumption_rate = Σ rᵢ · max(charge_cost(sᵢ), 0) and recovery_rate = Σ rᵢ · max(−charge_cost(sᵢ), 0) + 1.0, with uncovered positions degrading to unit rate. Rates are external input at the verification boundary — throughput tempo is combat-context data no loadout-recoverable semantic carries, the same ruling as skill_pathways — keyed by trigger-graph node id so duplicate skills are rateable per position. The resolve_damage_rates seam enforces the authoring contract: keys must name occupied skill positions, and no declared rate may exceed its skill’s maximal consistent execution frequency 1 / effective_cooldown_delay, since a skill on cooldown for d ticks executes at most once per d ticks; cooldown-0 passive skills carry an infinite ceiling, and violations raise ValueError rather than clamping or skipping. When damage_rates is omitted, verification runs the static per-loadout sums unchanged — absence is a zero-cost degenerate case, and all-unit rates reproduce the static report exactly because multiplying by 1.0 is exact in IEEE 754. The ratio’s time basis is the tick: rates are per-tick frequencies, grounded by the ceiling 1 / cooldown_ticks carrying per-tick units, and the base-replenishment addend of 1.0 joins through the implicit day-to-tick exchange inherited from the static computation. Any loadout with a gain cycle and eta >= 1 is classified as a Verified Outlier Candidate and flagged for Layer III confirmation.

Combo surface boundary analysis

The combo surface (combo_surface.py) flags trigger-graph edges crossing restricted pathway boundaries, and Layer II runs it as an opt-in check: verify_compositional and run_pipeline accept an optional skill_pathways mapping, and when it is supplied the check runs and violations surface as the cross_boundary_edges field of the CompositionalReport plus a CROSS_BOUNDARY_EDGES warning, which the canonical LoadoutReport inherits through the warning merge. When the mapping is omitted the check is skipped, because pathway provenance (e.g. CLASS_SKILL versus INTRINSIC) is unrecoverable from the Loadout alone: pathway fields on Skill are forbidden by contract, so pathway assignment is external state, and deriving it inside the pipeline would be silently wrong for class skills. Direct invocation of find_cross_boundary_edges remains available for callers needing a custom ComboSurface boundary. Pathways classify how a skill entered a loadout and are tracked externally through a mapping from node_id to SkillPathway, so the Skill model itself stays source-agnostic. The three pathways are CLASS_SKILL for skills granted by the Ascender’s class or archetype tree, INTRINSIC for skills innate to the Ascender but not tied to a class node, and ITEM_GRANTED for skills provided by equipped relics or other gear. Edges whose source or target pathway is unmapped are skipped rather than treated as violations, so the synthetic environment source never crosses a boundary.

The default ComboSurface restricts edges from CLASS_SKILL and INTRINSIC sources into ITEM_GRANTED targets, the ordered pairs (CLASS_SKILL, ITEM_GRANTED) and (INTRINSIC, ITEM_GRANTED). This preserves design intent: item-granted skills should trigger from their own item-specific conditions or from the environment, not be pulled into chains rooted in class or intrinsic abilities. Edges within the same pathway, edges from CLASS_SKILL to INTRINSIC, and edges from ITEM_GRANTED to any other pathway are unrestricted by default.

Ascender.build_skill_pathways() derives the pathway mapping heuristically. Skills from Ascender.skills tagged "class_skill" map to CLASS_SKILL, untagged skills map to INTRINSIC, and skills from equipped_relics map to ITEM_GRANTED, deduplicating with the same order-preserving logic as build_loadout(). Its positional skill_N keys are the trigger-graph node ids, so its output is the pipeline input by convention.

Constructing a ComboSurface with an explicit restricted_pairs set changes the boundary. An empty set leaves every cross-pathway edge unrestricted, and any pair can be added, including CLASS_SKILL to INTRINSIC or same-pathway pairs.

Theme membership projection

The equip-time theme-membership projection (theme_membership.py) derives per-theme equipped counts from the equipped items’ rolled modifier types against a caller-supplied ThemeCatalog, and Layer II computes it as an opt-in observation: verify_compositional and run_pipeline accept an optional theme_catalog parameter, and when it is supplied each equipped item contributes one count to a theme for each modifier type in its rolled values that belongs to that theme, with the counts surfacing in the theme_membership_counts field of the CompositionalReport (dense over the catalog: every theme carries a count, a theme no equipped item rolls carries zero). When the catalog is omitted the field carries the empty mapping — the degenerate empty membership surface — and no projection code runs. The counts ride the existing CyclesDetected event, which carries the whole compositional report, so the six-event sequence and both replay paths are untouched. The catalog is external input at the verification boundary because theme partitioning is designer vocabulary no loadout-recoverable semantic carries, the same ruling as skill_pathways and damage_rates.

Modifier types belonging to no catalog theme contribute to no count and raise no error — the tolerant unmapped policy. This deliberately diverges from derive_theme_covar’s strict UnmappedModifierType rejection: that derivation must cover every slot it correlates, so a skipped slot silently corrupts the correlation structure, while this projection observes a surface against a designer vocabulary that may legitimately partition only part of the modifier vocabulary, and observation has no computation to corrupt.

The counts are roll-invariant by construction: the projection reads modifier_values keys only, and every instance-roll path writes one entry per declared slot keyed by modifier type, so the keys of an equipped item’s rolled values are exactly its template’s slot modifier types and re-rolling or Layer III resampling leaves every count unchanged. Two same-type slots on one template collapse to one modifier key, so the counting granularity is modifier types present on the equipped surface. Typed DamageType keys need no normalization because StrEnum hash-identity makes find_theme’s frozenset membership match typed members exactly.

The projection is observation-only: it is called at exactly one site (the CompositionalReport construction), its return feeds exactly one constructor argument, no warning is emitted for theme membership (the closed ten-member WarningCode set gains nothing — a projection is not a violation), and no threshold predicate exists anywhere in the change, so stacked composition cannot become a finding. The counts enter no gain, cost, or other verification computation — the gain path (gain_cost.py, cycle_detector.py) imports neither the module nor the catalog — and the projection consumes no randomness, so supplying a catalog alters no verification outcome beyond the counts themselves and leaves Layer III’s sampling sequences seed-identical. Direct invocation of theme_membership_counts remains available for reading equipped composition without running the pipeline.

Layer III: Stochastic Simulation Verification

Layer III estimates the probability that a randomly rolled instance of a loadout achieves supercriticality. It uses Monte Carlo sampling with importance sampling for rare event estimation.

For each simulation run:

1. Sample a rarity tier vector from the drop probability distribution.
2. Sample a modifier value vector by drawing from Beta(alpha, beta) per tier, mapped to support intervals.
3. Evaluate gain cycle supercriticality for the instance by substituting rolled values into gain and cost expressions.
4. Record binary outcome and continuous supercriticality margin.

After N samples, produce a typed LoadoutReport.

Sample Complexity

For outlier probability approximately 10^-3 and relative error 0.1 at 95% confidence, N is approximately 40,000 samples. For Uber Legendary probabilities in the range [10^-6, 10^-4], importance sampling is mandatory to achieve tractable sample counts.

Verification Pipeline as Event-Sourced State

The verification pipeline is modeled as an event-sourced state machine, implemented in pipeline.py. Each run produces an event sequence: TemplateRegistered -> LoadoutAssembled -> GraphConstructed -> CyclesDetected -> StochasticSampleCompleted -> ReportFinalized.

The fold law guarantees that replaying this sequence from any checkpoint produces identical results. This enables incremental verification, audit trails, and seed reproducibility. The finalized LoadoutReport (report.py) is the canonical projection of the CompositionalReport and StochasticReport carried by the CyclesDetected and StochasticSampleCompleted events.