Module: Rigor::Effects::LiskovCheck

Defined in:
lib/rigor/effects/liskov_check.rb

Overview

Judges an override against the envelope it inherits (ADR-103 WD1 / WD14; #386). The one place effect.liskov-widened is decided.

An envelope is a contract about a method, and Ruby's class PgRepo < Repo says a PgRepo is usable wherever a Repo is. So a bound written on Repo#find binds PgRepo#find too: implementations may be purer than the bound they inherit, never less pure. That is Liskov inclusion applied to the second dimension, and it is what makes the declared lane's nominal carrier (#386, EnvelopeIndex) honest — a caller that imports ≤ io.db from a Repo-typed receiver is entitled to that bound whichever subclass actually arrives.

Two comparisons, and an override is subject to exactly one of them:

  • Proven against the inherited bound — the override declares nothing of its own, so what it does is what the ancestor's bound has to admit. It reads the same lane EnvelopeCheck reads, for the same reasons: the proven closure, undischarged per policy, mutate.local tolerated, taint ignored.
  • Declared against the inherited bound — the override declares its own envelope, and a bound wider than the one it inherits is a Liskov violation in the declaration, before any body is consulted. Two authored bounds compared by subsumption; nothing proven enters it.

The split is exclusive on purpose. An override that declares its own envelope is already held to that envelope by effect.envelope-exceeded, so running the proven comparison too would put two diagnostics on one line for one label. What the author asserted is the thing Liskov has to judge; whether the body honours the assertion is the other rule's question.

Both-sides-authored, in the ADR-35 sense: nothing fires unless an author wrote an envelope on the ancestor. That is the accepted construction the false-positive budget is spent under — a firing is never unsolicited.

Nominal subclassing only. An included module's method is not an override in this slice: Ruby's ancestry puts an includer's own def ahead of the module's rather than under it, and the substitutability argument that licenses the check is the subclass one. The superclasses table is the collector's own, as-written and resolved here exactly as Propagator resolves it, so the relation the check reads and the closed world the proven lane travels can never disagree.

Defined Under Namespace

Classes: Finding

Class Method Summary collapse

Class Method Details

.run(table:, superclasses:, method_envelopes:, class_envelopes:, config_envelopes: {}, positions: EnvelopeCheck::Positions.empty, apply_tolerated: true) ⇒ Array<Finding>

Returns sorted by position then key then label.

Parameters:

  • table (EffectTable) —

    the run's propagated graph.

  • superclasses (Hash{String => Array<String>}) —

    the collector's as-written superclass candidate lists (FileCollection#superclasses).

  • method_envelopes (Hash{String => Envelope}) —

    per-method envelopes, as written.

  • class_envelopes (Hash{String => Envelope}) —

    class- / module-level envelopes, to distribute.

  • config_envelopes (Hash{String => Envelope}) (defaults to: {}) —

    effects.envelopes: entries already resolved to the classes they select.

  • positions (EnvelopeCheck::Positions) (defaults to: EnvelopeCheck::Positions.empty) —

    where the override's def is.

  • apply_tolerated (Boolean) (defaults to: true) —

    false judges against proven — --no-tolerated-effects.

Returns:

  • (Array<Finding>) —

    sorted by position then key then label.



69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
 
# File 'lib/rigor/effects/liskov_check.rb', line 69

def run(table:, superclasses:, method_envelopes:, class_envelopes:, config_envelopes: {},
        positions: EnvelopeCheck::Positions.empty, apply_tolerated: true)
  # The distributed strata, over a base of the raw per-method annotations: a base class whose method
  # exists only in `.rbs` — an abstract `def find: (Integer) -> User` with no Ruby body — has no
  # key in the table and so no distributed entry, and its bound is exactly the one an override
  # inherits. Distribution wins on collision, which is the same value for a key that has both.
  envelopes = method_envelopes.merge(
    EnvelopeCheck.distribute(table, method_envelopes, class_envelopes, config_envelopes)
  )
  return NO_FINDINGS if envelopes.empty?

  parents = parent_map(table, superclasses)
  return NO_FINDINGS if parents.empty?

  findings = []
  keys = table.keys
  keys.each { |key| collect(findings, table, key, envelopes, parents, positions, apply_tolerated) }
  findings.sort_by { |f| [f.path.to_s, f.line, f.key, f.label] }.freeze
end