# Changelog

## 0.7.0

Kernel/reference assurance depth, replay diagnostics, and downstream smoke coverage.

- Added structured reference replay diagnostics with declaration phase, kind, dependency context, dependency path, replay order, and pending declarations.
- Added deterministic environment assurance for declaration, let, theorem, and universe-polymorphic chains with configurable `--environment-depth`.
- Added invalid environment rejection assurance with expected reasons for malformed indexes, bad declaration values, bad theorem proofs, duplicate declarations, and unknown dependencies.
- Added structured metadata/reduction replay reports with source breakdowns for Prelude, generated environments, generated artifacts, indexed artifacts, and theorem modules.
- Added `Theoria.Kernel.AssuranceSummary`, kernel/validation corpus summary structs, `docs/assurance.md`, and `mix theoria.kernel.check --assurance-summary` with coverage/JSON support.
- Improved `mix theoria.theorems MODULE` to load downstream theorem modules directly.
- Added downstream Mix project smoke coverage and package file boundary checks.

## 0.6.0

Proof-producing rewrite expansion and structured generated assurance reports.

- Added an experimental deterministic typed generator module and wired generated-term checks into kernel differential reports.
- Added kernel-checked proof lifting for `EqRec` base/proof rewrite paths, including supported nested paths.
- Added kernel-checked proof lifting for supported constructor value rewrite paths, including `let` values.
- Equality chains now bridge missing definitional-equality steps when composing explicit checked proofs.
- Kernel differential reports now include structured generated-term reports with configurable bounds, timing, diagnostics, and family counts.
- Generated-term assurance now covers deterministic `let`, `forall`, Bool equality, and Bool/Nat beta families.
- Proof capability JSON can expose nested `inner` capabilities for composed structural lifts.
- Simp results now expose proof status counts for trace reports.
- Kernel differential reports now summarize generated artifact proof strategies with a structured proof-strategy report.
- Proof capabilities now include step-aware diagnostics for parent-specific boundaries such as `Refl.value` and type-changing paths.

## 0.5.0

Structured assurance reports, proof diagnostics, and theorem/artifact replay.

### Added

- Added structured kernel assurance reports with reference replay, theorem-module replay, generated/indexed artifact replay, coverage, explanation, and timing metadata.
- Added `mix theoria.kernel.check --coverage`, `--explain`, and richer JSON output backed by Jason encoders.
- Added proof capability reporting through `Theoria.Rewrite.Proof.Capabilities`, `mix theoria.simp --explain`, and `mix theoria.simp --capabilities`.
- Added structured proof diagnostics via `Theoria.Rewrite.Proof.Result` and proof capability structs.
- Added equality-chain proof strategy metadata and direct simp result proof accessors.
- Added explicit universe constraint sets, solver explanations, and a symbolic regression matrix.
- Added theorem-module, artifact replay, kernel explanation, timing, and proof capability report structs.
- Added typed generated-term property coverage and direct `EqRec` reference normalization tests.
- Added examples for kernel reports and simp capabilities.
- Added `docs/reports.md` and `docs/release_0_5.md`.

### Changed

- Replaced separate rewrite/simp step proof fields with a structured `proof_result`.
- Split term quote and Prelude-specific quote sugar out of the main DSL facade.
- Extracted constant/axiom, theorem, definition, matcher, and inductive admission boundaries from the main kernel module.
- Fixed universe-parameter installation for polymorphic generated artifacts.
- Extended proof-producing rewrite support to nested application paths and selected equality-side paths.
- Made binder and `EqRec` proof-path boundaries explicit through capability reporting and tests.

### Validation

- Kernel differential checks now include theorem-module-installed environment replay and generated/indexed artifact environment replay.
- Reference properties now cover typed dependent fragments and `EqRec` over reflexivity.
- Native validation, docs, Dialyzer, Credo, ExDNA, Reach checks, tests, and Lean oracle validation remain clean.
## 0.4.0

Proof-producing rewrite/simp automation and Elixir-authored kernel assurance groundwork.

- Added `Theoria.Equality.Chain` as equality trace realization groundwork.
- Added `Theoria.Simp.Result` and proof-aware `Theoria.Simp.Step` metadata.
- Added `Simp.normalize(..., prove: true)`, `Simp.realize/3`, and `Simp.add_theorem/4` for checked simplification artifacts and explicit theorem installation.
- Added `realize: true` support for generated equation rewrite databases so rules can carry checked source artifacts.
- Added `mix theoria.equations --realize`, `mix theoria.simp --prove`, named simp examples, and example scripts to expose checked artifacts from the CLI and package integration paths.
- Added rewrite-step path and substitution tracking through structural rewrites and wired simp traces to consume rewrite-step metadata.
- Added `Theoria.Rewrite.Proof` for instantiated rule proofs and supported application function/argument congruence lifting.
- Added lazy rewrite-rule realization with `realize: :lazy`.
- Added proof-status diagnostics on rewrite and simp steps.
- Added JSON output for equation realization and simp proof examples.
- Added Elixir-authored kernel spec metadata, a reference checker for core terms, a reference normalizer with reference primitive recursor reductions, Bool/Nat/List/Vec corpus cases, rejection/theorem/generated-artifact/indexed-artifact differential checks, and `mix theoria.kernel.check`.
- Updated equality chains to combine available step proofs with transitivity.
- Added trusted boundary documentation and architecture policy guards for kernel-checked artifacts versus untrusted automation.
- Hardened definitional equality so diagnostic binder names no longer affect de Bruijn alpha-equivalent terms.
- Removed the unsound symbolic universe upper-bound shortcut and normalized universe `max` modulo commutativity/associativity for level equality.
- Avoided atom creation from CLI input in theorem, equation, and simp Mix tasks.
- Extracted definition and matcher declaration admission into trusted-adjacent kernel admission modules.
- Split theorem macro implementation out of the core term-construction DSL facade.
- Named the indexed Vec matcher case frame to isolate fragile de Bruijn positions from the main planning flow.

## 0.3.0

- Introduced structured `Theoria.Equation.Identity` identities for ordinary, unfold, matcher, and indexed matcher equations.
- Removed generated equation declaration atoms; installed generated equations now use structured `Theoria.Equation.Identity` values as environment keys.
- Added `Theoria.Equation.Realized` so generated equation checking is an anonymous artifact phase before optional theorem installation.
- Added selector-based indexed matcher equation lookup/realization and opt-in Vec indexed equation theorem installation.
- Added indexed matcher equation identity metadata recording in opt-in Vec environments.
- Carried structured equation identities through rewrite/simp rule metadata and friendly CLI/Lean labels.
- Added proof-aware rewrite rule fields for future proof-producing simp traces.
- Split indexed matcher packages into explicit statement, lemma, realization, and installation phases.
- Added explicit indexed matcher rewrite/simp database constructors behind opt-in policy.
- Generated the Lean oracle mirror declaration for the validation Vec matcher from the checked matcher type.

## 0.2.0

Second experimental release after the initial Hex publication.

- Hardened equation/matcher metadata validation and registry checks.
- Added in-memory equation registry snapshots and centralized generated-theorem realization.
- Derived matcher descriptors from checked recursor metadata for the supported Bool/Nat/List fragment.
- Added architecture regression tests for equation/matcher layering.
- Added release-boundary documentation and clearer experimental/internal API labels.

## 0.1.0

Initial experimental release.

- Added a small dependent proof/spec kernel with explicit checked environments.
- Added core terms, normalization, local definitions, universe parameters, equality, and theorem declarations.
- Added theorem modules and Mix tasks for theorem validation and installation workflows.
- Added Logic, Equality, Bool, Nat, List, and Vec libraries with theorem corpora.
- Added inductive specifications, generated recursors/inductors, checked metadata, and iota reduction.
- Added native validation via `mix theoria.check` and `mix theoria.validate`.
- Added contributor-only Lean oracle validation via generated Lean source.
- Added internal equation compiler metadata for supported Bool/Nat/List definitions.
- Added checked matcher declarations, generated ordinary equations, matcher equations, unfold equations, and registry validation.
- Added experimental rewrite and simp groundwork consuming generated equation metadata.
- Added ExDoc guides, CI, Reach architecture checks, Credo, ExDNA, Dialyzer, and docs build validation.