CLI reports

Theoria exposes native reports for validation, assurance, and proof-producing simplification diagnostics.

Native validation

mix theoria.validate

Runs the Theoria-owned validation corpus: theorem modules, defeq checks, inductive specs, equation metadata, generated artifacts, matcher declarations, and explicit indexed matcher validation.

Kernel differential assurance

mix theoria.kernel.check
mix theoria.kernel.check --verbose
mix theoria.kernel.check --coverage
mix theoria.kernel.check --explain
mix theoria.kernel.check --json --coverage --explain

The report compares production kernel behavior with the independent reference checker/normalizer, replays the Prelude environment, replays theorem-module-installed environments, and replays generated/indexed artifact environments.

These reports are assurance, not a formal proof of kernel correctness. The trusted boundary remains native kernel checking of declarations and artifacts.

Simplification proof diagnostics

mix theoria.simp --capabilities
mix theoria.simp --capabilities --json
mix theoria.simp nat_add_zero --prove --explain
mix theoria.simp nat_add_zero --prove --explain --json

Simp steps expose structured proof results:

step.proof_result.status
step.proof_result.capability
step.proof_result.proof

Theoria.Simp.Result.proof_strategy/1 reports how the final checked artifact was produced: reflexivity, single step, transitive chain, or definitional-equality fallback.

JSON output

JSON output is produced through Jason encoders for report structs and proof diagnostics. Mix tasks should pass structs/maps to Jason.encode!/1; do not hand-roll JSON strings.

Capability output has this shape:

{
  "proof_capabilities": [
    {
      "path": ["arg"],
      "capability": {
        "supported": true,
        "reason": "application_congruence",
        "description": "application congruence"
      }
    }
  ]
}

Kernel JSON reports include timings, total_checks, total_replay_checks, and optional structured explanation entries when --explain is passed with coverage JSON.