Class: Rigor::FlowContribution

Inherits:
Object
  • Object
show all
Defined in:
lib/rigor/flow_contribution.rb,
lib/rigor/flow_contribution/fact.rb,
lib/rigor/flow_contribution/merger.rb,
lib/rigor/flow_contribution/element.rb,
lib/rigor/flow_contribution/conflict.rb,
lib/rigor/flow_contribution/merge_result.rb

Overview

The public packaging of a flow contribution at a single call edge. Plugins, RBS::Extended annotations, and built-in narrowing rules all hand the analyzer this same bundle shape; the inference engine merges contributions through the policy described in ADR-2 § "Plugin Contribution Merging" rather than letting any one source override another silently.

Nine content slots plus a Provenance block. A slot left as nil (or, for collection-shaped slots, an empty collection) means the contribution does not assert anything in that dimension; the merge policy treats it as absent.

The struct is the only shape plugin authors need to learn. Richer or more permissive shapes are not part of the first public contract — see ADR-2 § "Flow Contribution Bundle" for the binding definition.

to_element_list and Merger are implemented; plugin authors should not depend on the Element shape — the bundle is the public contract.

Defined Under Namespace

Modules: Merger Classes: Conflict, Element, Fact, MergeResult, Provenance

Constant Summary collapse

SLOT_NAMES = 
%i[
  return_type
  truthy_facts
  falsey_facts
  post_return_facts
  mutations
  invalidations
  exceptional
  role_conformance
  effects
].freeze
SCALAR_SLOTS =

effects is scalar-shaped like return_type and exceptional: only nil means "asserts nothing". An EMPTY Effects::LabelSet is the positive claim that the call performs no effects — the reading of %a{pure} — so it must not be mistaken for an unset slot the way an empty fact Array is.

%i[return_type exceptional effects].freeze
FACT_VALID_TARGET_KINDS =

Canonical slot payload for the four edge-aware fact slots (truthy_facts, falsey_facts, post_return_facts, plus the equivalent under mutations / invalidations / role_conformance once those carriers grow Fact-shaped variants).

ADR-7 § "Slice 4-A" pins this object as the single canonical translation target for the four parallel contribution carriers the engine has carried so far:

  1. Built-in narrowing rules' direct fact emission (Inference::Narrowing#predicate_scopes).
  2. RBS::Extended predicate-if-* directives (Rigor::RbsExtended::PredicateEffect).
  3. RBS::Extended assert* directives (Rigor::RbsExtended::AssertEffect).
  4. Plugin contributions via narrowing_facts DSL (ADR-52).

Each of those four carriers translates to / from Fact at its boundary; downstream of #to_element_list and Merger.merge, every slot payload is a Fact (or a value that the merger compares by equality and never inspects). The typed RbsExtended::*Effect carriers stay internal to the parser side — they hold the source-text shape, but lose their identity at the read_flow_contribution boundary.

Field set

  • target_kind: :parameter (call-site argument), :self (receiver), or :local (a named local in the surrounding scope). v0.1.8 Pillar 2 Slice 1 added :local so plugins recognising bespoke call shapes (expect(x).to be_a(T)) can narrow a specific scope-bound local without routing through the parameter-name lookup that requires an authoritative RBS sig on the called method. Future slices may extend further (:ivar, :result). The merger is agnostic to the concrete kinds and only requires equality.
  • target_name: a Symbol. For :parameter it's the declared parameter name. For :self it is the literal :self symbol so the field stays non-nil and the merge key is well-defined. For :local it's the local-variable name (e.g. :x for expect(x).to be_a(T)).
  • type: a Rigor::Type::* (Nominal, Refined, IntegerRange, Difference, …) the fact narrows the target toward (when negative is false) or away from (when negative is true).
  • negative: true for the ~T negation form (predicate-if-true x is ~Integer), false for the plain positive form. Mirrors the negative field on PredicateEffect / AssertEffect.

The target accessor returns :self for self-targeted facts and [:parameter, name] otherwise — that's the value Element#target keys on, so two facts that narrow the same parameter from different contribution sources land in the same merge bucket.

%i[parameter self local].freeze
ELEMENT_VALID_EDGES =

Tagged element flattening of a Rigor::FlowContribution bundle — the analyzer-internal representation ADR-2 § "Flow Contribution Bundle" routes through the Merger.

The flattening is mechanical, deterministic, and round-trippable with the bundle: every non-empty slot expands into one or more elements keyed by (target, edge, kind), and an array of elements rebuilds an equivalent bundle when routed through Merger.merge.

Plugin authors should not depend on the element shape — the bundle is the public contract; the element list is the implementation surface the merge policy operates over.

%i[normal truthy falsey post_return exceptional].freeze
ELEMENT_VALID_KINDS = 
%i[
  return_type
  truthy_fact
  falsey_fact
  post_return_fact
  mutation
  invalidation
  exception
  role
  effects
].freeze
CONFLICT_VALID_REASONS =

Records a contradiction between two or more flow contributions detected during Merger.merge. Carried on MergeResult#conflicts so the analyzer / formatter can surface a :contribution_merge diagnostic per ADR-2 § "Plugin Contribution Merging".

ADR-2 § "Plugin Contribution Merging" rules out first-wins / last-wins behaviour: when contributions conflict, both sources are reported and the merger falls back to the nearest non-conflicting higher-tier (or default) value for the affected (target, edge, kind) slot. The conflict object is the carrier of that report.

Slice-3 conflict reasons:

  • :return_type_collapse — two return-type contributions intersect to bot.
  • :exceptional_disagreement — two contributions assert incompatible non-nil exceptional effects.
  • :lower_tier_contradiction — a lower-tier contribution would weaken or contradict a higher-tier proof.
%i[
  return_type_collapse
  exceptional_disagreement
  lower_tier_contradiction
].freeze

Instance Method Summary collapse

Constructor Details

#initialize(return_type: nil, truthy_facts: nil, falsey_facts: nil, post_return_facts: nil, mutations: nil, invalidations: nil, exceptional: nil, role_conformance: nil, effects: nil, provenance: Provenance.builtin) ⇒ FlowContribution

rubocop:disable Metrics/ParameterLists

Parameters:

  • return_type (Object, nil) (defaults to: nil) —

    normal-edge return type. Use nil when the contribution does not refine the return type selected from the RBS contract.

  • truthy_facts (Array, nil) (defaults to: nil) —

    facts that hold only on the truthy control-flow edge. Edge-local: a truthy-edge fact does NOT imply its falsey-edge complement (ADR-2 § "Plugin Contribution Merging").

  • falsey_facts (Array, nil) (defaults to: nil) —

    dual of truthy_facts.

  • post_return_facts (Array, nil) (defaults to: nil) —

    facts that hold after the call returns normally on every edge — the carrier for assertion-style contributions.

  • mutations (Array, nil) (defaults to: nil) —

    receiver and argument mutation effects.

  • invalidations (Array, nil) (defaults to: nil) —

    targeted fact invalidations beyond what mutation effects already imply.

  • exceptional (Object, nil) (defaults to: nil) —

    non-returning, raising, or unreachable effect.

  • role_conformance (Array, nil) (defaults to: nil) —

    capability-role conformance facts the contribution provides.

  • effects (Rigor::Effects::LabelSet, nil) (defaults to: nil) —

    ADR-103 WD5 — the effect labels this call edge attributes to its callee, as an upper bound. nil means "says nothing about effects", which is NOT the same as the empty set (which asserts the call performs none). Merged by union, the conservative direction: two sources that each name part of a call's footprint together name more of it, and neither can shrink the other's claim.

  • provenance (Provenance) (defaults to: Provenance.builtin) —

    source-family, plugin-id, node, and cache-descriptor metadata. Defaults to Provenance.builtin.



72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
 
# File 'lib/rigor/flow_contribution.rb', line 72

def initialize(return_type: nil, truthy_facts: nil, falsey_facts: nil,
               post_return_facts: nil, mutations: nil, invalidations: nil,
               exceptional: nil, role_conformance: nil, effects: nil,
               provenance: Provenance.builtin)
  # rubocop:enable Metrics/ParameterLists
  @return_type = return_type
  @truthy_facts = freeze_collection(truthy_facts)
  @falsey_facts = freeze_collection(falsey_facts)
  @post_return_facts = freeze_collection(post_return_facts)
  @mutations = freeze_collection(mutations)
  @invalidations = freeze_collection(invalidations)
  @exceptional = exceptional
  @role_conformance = freeze_collection(role_conformance)
  @effects = effects
  @provenance = provenance
  freeze
end

Instance Method Details

#==(other) ⇒ Object Also known as: eql? 



137
138
139
 
# File 'lib/rigor/flow_contribution.rb', line 137

def ==(other)
  other.is_a?(FlowContribution) && to_h == other.to_h
end

#empty? ⇒ Boolean

Returns true when every content slot is unset (nil or an empty collection). Provenance does not count toward emptiness — an empty bundle still carries source attribution.

Returns:

  • (Boolean) —

    true when every content slot is unset (nil or an empty collection). Provenance does not count toward emptiness — an empty bundle still carries source attribution.



92
93
94
 
# File 'lib/rigor/flow_contribution.rb', line 92

def empty?
  SLOT_NAMES.all? { |slot| slot_empty?(slot, public_send(slot)) }
end

#hash ⇒ Object 



142
143
144
 
# File 'lib/rigor/flow_contribution.rb', line 142

def hash
  to_h.hash
end

#to_element_list ⇒ Array<Element>

Flattens this bundle into a tagged element list keyed by (target, edge, kind). The flattening is mechanical and round-trippable through Rigor::FlowContribution::Merger.merge: feeding the result back through the merger produces an equivalent bundle.

Layout:

slot edge kind target
return_type normal return_type :return
truthy_facts truthy truthy_fact (per-fact target)
falsey_facts falsey falsey_fact (per-fact target)
post_return_facts post_return post_return_fact (per-fact target)
mutations normal mutation (per-mutation target)
invalidations normal invalidation (per-fact target)
exceptional exceptional exception :raise
role_conformance normal role (per-role target)
effects normal effects :effects

Returns:



121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
 
# File 'lib/rigor/flow_contribution.rb', line 121

def to_element_list # rubocop:disable Metrics/AbcSize
  elements = []
  elements << element_for(:return, :normal, :return_type, return_type) unless return_type.nil?
  Array(truthy_facts).each { |fact| elements << element_for(fact_target(fact), :truthy, :truthy_fact, fact) }
  Array(falsey_facts).each { |fact| elements << element_for(fact_target(fact), :falsey, :falsey_fact, fact) }
  Array(post_return_facts).each do |fact|
    elements << element_for(fact_target(fact), :post_return, :post_return_fact, fact)
  end
  Array(mutations).each { |m| elements << element_for(fact_target(m), :normal, :mutation, m) }
  Array(invalidations).each { |i| elements << element_for(fact_target(i), :normal, :invalidation, i) }
  elements << element_for(:raise, :exceptional, :exception, exceptional) unless exceptional.nil?
  Array(role_conformance).each { |r| elements << element_for(fact_target(r), :normal, :role, r) }
  elements << element_for(:effects, :normal, :effects, effects) unless effects.nil?
  elements.freeze
end

#to_h ⇒ Object 



96
97
98
99
100
 
# File 'lib/rigor/flow_contribution.rb', line 96

def to_h
  SLOT_NAMES.each_with_object(provenance: provenance.to_h) do |slot, acc|
    acc[slot] = public_send(slot)
  end
end