// SPDX-License-Identifier: CC-BY-SA-4.0
// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>

= TRG-PROFILE — {LANGUAGE_NAME}
:toc: left
:toclevels: 2

[cols="1,3"]
|===
| Field | Value

| Language | {LANGUAGE_NAME}
| Repository | {REPO_URL}
| Current TRG Grade | {GRADE}  (X \| F \| E \| D \| C \| B \| A)
| Assessed | {YYYY-MM-DD}
| Assessor | {NAME <email>}
| TRG Spec Version | 1.0
| ARG Profile | spec/ARG-PROFILE.adoc
| FRG Profile | spec/FRG-PROFILE.adoc
| CRG Profile | spec/CRG-PROFILE.adoc
|===

== About this profile

This profile applies the *TRG v1.0* baseline to {LANGUAGE_NAME} and
records the current honest grade, the evidence supporting it per
component, the language-specific tightening obligations, and the path
to the next grade. Per TRG §1.1, profiles may *tighten* the baseline
but never *loosen* it.

TRG = {GRADE} (worst-of any required component per TRG §7). The full
chain of axes for this language:

* ARG: {ARG_GRADE}
* TRG: {GRADE}
* FRG: {FRG_GRADE}
* CRG: {CRG_GRADE} (worst-of any released component)
* RSR: {RSR_LEVEL}

Cross-axis rule: ARG ≤ TRG holds (currently TRG = {GRADE},
ARG = {ARG_GRADE}).

== Component grades

The toolchain decomposes into components drawn from TRG §3. Each
component is graded independently against the four-tier audit format
of TRG §4 (Must / Should / Could / Aspirational → grades E / D / C / B).
The overall TRG grade is the *worst* of any MUST component.

=== Front-end (TRG §3.1)

[cols="1,3,1,4", options="header"]
|===
| # | Component | Grade | Evidence

| F1 | Grammar / Syntax        | {grade} | {Path to .ebnf / .pest / .peg; SoT status}
| F2 | Lexer / Tokeniser       | {grade} | {Path; test coverage; fuzz harness}
| F3 | Parser                  | {grade} | {Path; test coverage}
| F4 | AST                     | {grade} | {Path; invariant documentation}
| F5 | Macro expander          | {grade or N/A} | {Path; N/A if no macros}
| F6 | Import resolver / Modules | {grade} | {Path; cycle-detection evidence}
| F7 | Diagnostics / Errors    | {grade} | {Path; error-code index}
|===

=== Middle-end (TRG §3.2)

[cols="1,3,1,4", options="header"]
|===
| # | Component | Grade | Evidence

| M1 | Semantic analyser       | {grade} | {Path; resolved-name property tests}
| M2 | Type checker            | {grade} | {Path; test corpus}
| M3 | Type-checker oracle     | {grade or N/A} | {Path; N/A if not a verified language}
| M4 | Proof dispatcher        | {grade or N/A} | {Path; N/A if not a verified language}
| M5 | Semantics document      | {grade} | {Path to .adoc / paper; operational + denotational coverage}
|===

=== Back-end (TRG §3.3)

[cols="1,3,1,4", options="header"]
|===
| # | Component | Grade | Evidence

| B1 | Intermediate representation | {grade} | {Path; documented invariants}
| B2 | Code generator (per backend) | {grade} | {Per-backend list; coverage}
| B3 | Backend registry        | {grade or N/A} | {Path; N/A if only one backend}
| B4 | Linker / JIT / eval     | {grade} | {Path; tests}
| B5 | ABI / FFI surface       | {grade} | {Idris2 ABI path; Zig FFI path}
| B6 | Runtime                 | {grade} | {Path; test coverage}
|===

=== Tool surface (TRG §3.4)

[cols="1,3,1,4", options="header"]
|===
| # | Component | Grade | Evidence

| T1 | Compiler driver         | {grade} | {Path to binary; CLI surface tests}
| T2 | Interpreter             | {grade or N/A} | {Path; N/A if compiled-first}
| T3 | REPL                    | {grade or N/A} | {Path; smoke-test coverage}
| T4 | Formatter               | {grade or N/A} | {Path; round-trip property test}
| T5 | LSP server              | {grade or N/A} | {Path; LSP protocol coverage}
| T6 | Debugger                | {grade or N/A} | {Path; integration list}
| T7 | Package manager         | {grade or N/A} | {Path; package-resolution tests}
| T8 | Standard library        | {grade} | {Path; symbol-coverage estimate; test-density}
| T9 | Pipeline orchestrator   | {grade} | {Path; CI integration}
|===

== Language-specific tightening (this profile only)

TRG §1.1 permits per-language tightening. For {LANGUAGE_NAME}, the
following additional obligations apply at the stated grades:

* *Grade D tightening:* {Language-specific obligation, e.g. "AffineScript:
  type checker MUST reject borrow-after-move on every sample in the
  borrow-check fixture suite."}
* *Grade C tightening:* {e.g. "Ephapax: the proof dispatcher MUST emit
  a structured judgment trace for any preservation lemma in the
  active layer."}
* *Grade B tightening:* {Language-specific aspirational obligation.}

These tightenings are *additional* to the baseline — none of the
baseline evidence is waived.

== Canonical Proof Suite extension (if verified language)

Per TRG §6.6, verified languages MUST extend the Canonical Proof Suite
(see `templates/CANONICAL-PROOF-SUITE.adoc`). For {LANGUAGE_NAME}:

* {Proof obligation 1, paradigm-specific, with file path}
* {Proof obligation 2}
* {...}

If the language is not verified, mark this section "N/A" and remove
the M3/M4 rows above.

== What is NOT yet met (honest gaps)

* {Bullet list of specific MUST evidence the toolchain does not currently
  produce, grouped by component}
* {Each gap should be specific enough that a reader can verify by
  inspection of the repo}

== Path to next grade ({NEXT_GRADE})

* {Specific next-step item 1, naming the gated component(s), with
  estimated work}
* {Specific next-step item 2}
* {...}

*Realistic timeline estimate:* {N weeks/months}

== Path to grade beyond that ({GRADE_AFTER_NEXT})

* {Larger items that follow the immediate next grade}

== Demotion risk

* *Lowest:* {What would have to break for the grade to drop by one,
  e.g. "parser corpus regression flag flips to red"}
* *Medium:* {What would have to break for a multi-step demotion}
* *Catastrophic:* {What would force demotion to F, e.g. "type-checker
  unsoundness witness found"}

== Iteration history

[cols="1,1,4", options="header"]
|===
| Date | Grade | Notes

| {YYYY-MM-DD} | {grade} | Initial assessment.
| {YYYY-MM-DD} | {grade} | {Reason for change.}
|===

== Review cycle

* *Routine:* Reassess on every release cycle (per TRG §8).
* *Immediate:* Reassess within 7 days of any MUST-component regression.
* *VeriSimDB drift alert:* Reassess within 24 hours of any drift alert
  from VeriSimDB on this toolchain's attestations.

== Footer

Run `just trg-badge` in this repo to generate the shields.io badge for
the README.

This profile is itself a VCL-total proposition. Its content is
`DECLARE`'d to VeriSimDB on each commit. Drift between the claimed
grade above and the underlying evidence surfaces as a grade-stale alert.
