CLI reports

Copy Markdown View Source

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
mix theoria.kernel.check --generated-size 4 --generated-max-terms 256

The report compares production kernel behavior with the independent reference checker/normalizer, checks deterministic generated typed terms with stable family counts, timing, diagnostics, and configurable bounds, summarizes generated artifact proof strategies, 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. Theoria.Simp.Result.proof_status_counts/1 summarizes checked/missing/unsupported step proofs in a trace.

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. Nested structural lifts may include inner to describe the supported proof method used below the outer constructor path:

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

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