Skip to content

EXPLAINME.adoc

Latest commit

 

History

History
81 lines (64 loc) · 3.97 KB

EXPLAINME.adoc

File metadata and controls

81 lines (64 loc) · 3.97 KB
Raw

EXPLAINME — trope-checker (developer deep-dive)

The README is the pitch; this is how it actually works and why it is shaped this way.

Table of Contents

1. The one job

check : TropeIR → Verdict. Everything else (schema, verified core, conformance) exists to make that one pure function trustworthy and portable. The checker never sees a source program — only the IR. That is the whole portability story (HC-1).

2. Idris2 through-and-through

The checker is one Idris2 codebase. The verified core (verification/proofs/idris2/, package trope) defines and proves the grade algebra (L1/L2, decidable ⊑, the veridicality and generation results). The executable (src/idris2/, Checker.Json → Checker.Decode → Checker.Check → Main) reuses that very algebra — it imports Trope.Grade/Trope.Coords/ Trope.Fidelity and composes with the same gradeCompose and coordinate orders. So there is no "second core kept in sync": the thing that runs is the thing that is proved, plus a JSON front-end. The conformance suite then guards against front-end/regression drift rather than against two divergent implementations. A Rust fast-core remains a deferred option (calculus §9.3), validated — if ever built — against this reference via the same suite.

There is no Python anywhere (estate rule); the runners are bash + jq.

3. Data flow

  1. Parse the IR JSON (Checker/Json.idr — a small parser for the IR subset).

  2. Decode + validate (Checker/Decode.idr): this is the validation boundary. HC-4 (bond coherent with the bearer’s fate) and HC-3 (no deceptive grades, no untagged merge) are enforced here; a rejection names the coordinate (e.g. edges/e/grade/bond: incoherent with the bearer’s fate (HC-4)). The JSON Schema (schemas/) is the language-neutral published contract; the decoder is the executable reference validator, and the two encode the same rules.

  3. Accumulate grades over the DAG (Checker/Check.idr): roots get ε; a single-input edge composes acc(source) ▷ grade(edge); a fuse edge takes the retention-meet of its two inputs then composes.

  4. Decide floor(use_model) ⊑ acc(output). If it fails, walk edges to find the witness: the first edge whose accumulated grade dropped below the floor in a failing coordinate.

4. The grade, concretely

Grade = (fate : Φ→Fate, bond, merge). Fate = Present | Attenuated δ | Predicated | Dropped | Falsified; Bond = Intact | Withheld | Severed | Misbound; Merge = Single | Fused | Conflated. The deceptive duals (Falsified/Misbound/Conflated) are each their coordinate’s bottom: absorbing under ▷, below every honest value, so any honest floor fails against them. Under the prevent profile they are not even decodable into a valid IR (the decoder rejects them, naming the coordinate).

5. Reading the proofs

idris2 --typecheck verification/proofs/idris2/trope.ipkg. Start in Trope.Fidelity (the δ dimension), then Trope.Coords (the three coordinates + per-coordinate laws), then Trope.Grade/Trope.Laws (the assembled grade + L1/L2/decidability), then Trope.Veridicality and Trope.Generation (the structure results). What is and is not proved is in docs/status/PROOF-STATUS.adoc — read it before believing any claim.

6. Building and running

just check          # typecheck core + build the tropecheck binary + conformance
just trope-build    # install the core package, build src/idris2/build/exec/tropecheck
src/idris2/build/exec/tropecheck tests/conformance/fixtures/duck-collapse.ir.json

7. Extending

A new front-end: see docs/CONTRIBUTING-A-FRONTEND.adoc. A new effect or grade coordinate: change the calculus first, then the schema, then the verified core, then the decoder/checker, then the conformance suite — in that order, small verified increments (HC-5).