mix credence.equiv (credence v0.8.0)

Copy Markdown

Classify-time behavioural-equivalence pre-check (Tunex 07 §3.11, 08 T1.4).

Given a before expression and a proposed after expression (the rewrite, NOT a whole module — this is the expression-level / T1 check, the dominant case and where ~all followup.md divergences live), run both over a curated adversarial battery and emit a trichotomy verdict:

MIX_ENV=test mix credence.equiv --before b.exs --after a.exs --vars s
  • EQUIVALENT — same outcome (strict ===, or same exception class) on every admitted input. With --minimal-set, also reports the minimal assumption switch set that makes it so ([] = no-promise / strict-safe).
  • REPAIR — before raises on every input and after returns a value on ≥1. The before has no valid output, so the fix is a correction, not a behaviour change (the mark_equivalence_repair family). Prints the exception class + N/N raised for the implementer's reason string.
  • DIVERGES — before produced a valid value on some input that after disagrees with (a real behaviour change), or after does not compile.

Run env

🔴 Must run under MIX_ENV=test — it reuses Credence.BehaviourEquivalence (eval_outcome/2) + the curated Credence.EquivalenceInputs battery, both of which live in test/support/ (compiled only under :test). The task aborts with guidance otherwise. (Dynamic dispatch is used for those two modules so the task still compiles clean under :dev.)

Options

  • --before FILE / --after FILE — the two expression snippets (required).
  • --vars a,b — ordered free-var names of the expression (required).
  • --dim d1,d2 — EquivalenceInputs dimension(s) to run (default: all that fit the var count). Names: term_lists, signed_integers, unicode_strings, single_codepoint_strings, multi_codepoint_strings, stability_lists.
  • --inputs-file FILE — an Elixir term (a list) overriding the battery; for multi-var, each element is a tuple/list of positional args. (The escape hatch for the unresolved multi-var input-set question.)
  • --assumptions a,b — run in that admitted domain (filters the battery).
  • --minimal-set — report the minimal switch set making before ≡ after.
  • --compare-messages — compare exception messages too (default: class only).

Determinism: fixed battery, never StreamData. Names no rule.