Module: Rigor::Effects::EnvelopeCheck

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

Overview

Judges each method's declared envelope against what the run actually proved (ADR-103 WD1 / WD8; #383). The one place effect.envelope-exceeded is decided.

Three rules make this FP-safe, and each is load-bearing:

  • It reads the PROVEN lane only, never the declared one and never taint. A non-exhaustive summary reads "these effects, and possibly more" and contributes no finding of its own; what it did prove is still proven, so a proven label outside the bound still fires. That is "as strict as proven" (robustness-principle.md), and it is why an unresolved call can never manufacture one.
  • The bound binds the method's CODE, transitively. The envelope is a contract about what the method does, and a repository that calls a helper that calls Net::HTTP does perform HTTP. So the comparison is against EffectTable::Entry#proven — the fixpoint's closure over project callees — not against the unit's own direct summary.
  • mutate.local is tolerated by every envelope, %a{pure} included (Rigor::Effects::Envelope#tolerates?).

effects.tolerated: discharges, per origin (#385). The comparison reads EffectTable::Entry#undischarged rather than proven: the propagator has already dropped every origin bundle the policy discharges and closed the rest over the graph, so a pure-declared method that logs is silent under tolerated: [telemetry] while the File.read two lines down still fires. apply_tolerated: false — --no-tolerated-effects — judges against proven instead, which is the audit switch that makes the policy inspectable rather than invisible.

Defined Under Namespace

Classes: Finding, Positions

Class Method Summary collapse

Class Method Details

.distribute(table, method_envelopes, class_envelopes, config_envelopes) ⇒ Object

Resolves the per-method envelope for every unit the table knows, nearest wins:

per-method annotation  >  class-level annotation  >  `effects.envelopes:` entry

The two class-shaped strata distribute identically — an envelope keyed by a class name reaches every method key of THAT Ruby class, so a subclass's keys never match and a module distributes to its own methods only — and are applied in that order, so a written annotation always wins over a convention. Which config entry a class matched was already decided by ConfigEnvelopes.for_classes.

Public because LiskovCheck resolves the ancestor's envelope by exactly these rules: an inherited bound has to be the same bound the ancestor is itself held to, or the two checks would disagree about what the author wrote.



124
125
126
127
128
129
130
131
132
133
134
135
136
 
# File 'lib/rigor/effects/envelope_check.rb', line 124

def distribute(table, method_envelopes, class_envelopes, config_envelopes)
  resolved = {}
  unless class_envelopes.empty? && config_envelopes.empty?
    keys_by_class(table).each do |class_name, keys|
      envelope = class_envelopes[class_name] || config_envelopes[class_name]
      next if envelope.nil?

      keys.each { |key| resolved[key] = envelope.rebind(key) }
    end
  end
  method_envelopes.each { |key, envelope| resolved[key] = envelope if table[key] }
  resolved
end

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

Returns sorted by position then key then label, so a run explains identically twice.

Parameters:

  • table (EffectTable) —

    the run's propagated graph.

  • 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 (ConfigEnvelopes.for_classes), to distribute at the lowest precedence.

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

    the discovery tables a finding's def position is read from.

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

    false judges against the undischarged-by-policy proven lane — the --no-tolerated-effects audit switch.

Returns:

  • (Array<Finding>) —

    sorted by position then key then label, so a run explains identically twice.



100
101
102
103
104
105
106
107
108
109
110
 
# File 'lib/rigor/effects/envelope_check.rb', line 100

def run(table:, method_envelopes:, class_envelopes:, config_envelopes: {},
        positions: Positions.empty, apply_tolerated: true)
  envelopes = distribute(table, method_envelopes, class_envelopes, config_envelopes)
  return NO_FINDINGS if envelopes.empty?

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