diff --git a/docs/tech-debt-2026-05-26.adoc b/docs/tech-debt-2026-05-26.adoc new file mode 100644 index 0000000..177a3e9 --- /dev/null +++ b/docs/tech-debt-2026-05-26.adoc @@ -0,0 +1,74 @@ +// SPDX-License-Identifier: CC-BY-SA-4.0 +// Copyright (c) Jonathan D.A. Jewell += Tech-Debt Audit — contractiles — 2026-05-26 + +*Source:* estate-wide automated scan 2026-05-26. +*Companion:* https://github.com/hyperpolymath/standards/tree/main/docs/audits[`hyperpolymath/standards` 2026-05-26-estate-*-debt audits]. +*Combined severity:* `LOW`. + +This file records the *raw findings* — it does not by itself fix the debt. Each section ends with a 'Recommended next move' line; closing the debt is follow-up work. + +== 1. Proof debt + +Scanner counted the following markers in proof-bearing files of this repo: + +---- +files= 13 | Coq-Axm/Adm= 0 | Lean-srry/ax= 0 | Agda-pst= 0 | Idr-blv= 6 | Idr-prtl= 0 | Fstr-asm= 0 | TODO= 0 | Unsafe= 0 +---- + +*Total markers:* 6. *Severity:* `>06`. + +*Marker types* (any non-zero counts above): +* Coq `Axiom`/`Admitted` — unconditional proof escapes. +* Lean `sorry`/`axiom` — Lean's equivalent. +* Agda `postulate` — accepted axiomatically. +* Idris2 `believe_me`/`assert_total` — runtime-safe coercion / totality assumption. +* Idris2 top-level `partial` — totality-check waived. +* F\* `assume val`/`admit_p` — F\* admit. +* `TODO PROOF` / `OWED:` — self-documented debt markers. +* `unsafePerformIO`/`unsafeCoerce` — soundness-relevant escape hatches in Haskell/Rust source. + +*Recommended next move:* triage each finding into one of: (a) discharge by proof, (b) cover with property-tests + a documented refutation budget, or (c) annotate as a known/necessary axiom (e.g. `funExt`) in `docs/proof-debt.md`. + +== 2. Licence debt + +[cols="1,1",options="header"] +|=== +|Field |Value +|LICENSE file |`LICENSE` +|SPDX header |`MPL-2.0` +|Manifest licence |`NONE` +|Body classifier |`Palimp-MPL-2.0` +|Severity |`ok` +|=== + + +*Recommended next move:* none for licence. + +== 3. Documentation debt + +[cols="1,1",options="header"] +|=== +|Field |Value +|README lines |186 +|`docs/` files |70 +|`docs/` LoC |4218 +|CHANGELOG.md |Y +|CONTRIBUTING.md |N +|CODE_OF_CONDUCT.md |N +|SECURITY.md |N +|Severity |`OK` +|=== + + +*Recommended next move:* none for docs. + +== Cross-references + +* Estate proof-debt audit: `hyperpolymath/standards/docs/audits/2026-05-26-estate-proof-debt.md` +* Estate licence-debt audit: `hyperpolymath/standards/docs/audits/2026-05-26-estate-licence-debt.md` +* Estate documentation-debt audit: `hyperpolymath/standards/docs/audits/2026-05-26-estate-documentation-debt.md` + +''' + +🤖 Generated by Claude Code estate-wide tech-debt scan (2026-05-26). This file is informational — closing the debt is follow-up work owned by the maintainer. diff --git a/docs/tech-debt-2026-05-26.md b/docs/tech-debt-2026-05-26.md deleted file mode 100644 index eb8709f..0000000 --- a/docs/tech-debt-2026-05-26.md +++ /dev/null @@ -1,70 +0,0 @@ - -# Tech-Debt Audit — contractiles — 2026-05-26 - -**Source:** estate-wide automated scan 2026-05-26. -**Companion:** [`hyperpolymath/standards` 2026-05-26-estate-*-debt audits](https://github.com/hyperpolymath/standards/tree/main/docs/audits). -**Combined severity:** `LOW`. - -This file records the *raw findings* — it does not by itself fix the debt. Each section ends with a 'Recommended next move' line; closing the debt is follow-up work. - -## 1. Proof debt - -Scanner counted the following markers in proof-bearing files of this repo: - -``` -files= 13 | Coq-Axm/Adm= 0 | Lean-srry/ax= 0 | Agda-pst= 0 | Idr-blv= 6 | Idr-prtl= 0 | Fstr-asm= 0 | TODO= 0 | Unsafe= 0 -``` - -**Total markers:** 6. **Severity:** `>06`. - -**Marker types** (any non-zero counts above): -- Coq `Axiom`/`Admitted` — unconditional proof escapes. -- Lean `sorry`/`axiom` — Lean's equivalent. -- Agda `postulate` — accepted axiomatically. -- Idris2 `believe_me`/`assert_total` — runtime-safe coercion / totality assumption. -- Idris2 top-level `partial` — totality-check waived. -- F\* `assume val`/`admit_p` — F\* admit. -- `TODO PROOF` / `OWED:` — self-documented debt markers. -- `unsafePerformIO`/`unsafeCoerce` — soundness-relevant escape hatches in Haskell/Rust source. - -**Recommended next move:** triage each finding into one of: (a) discharge by proof, (b) cover with property-tests + a documented refutation budget, or (c) annotate as a known/necessary axiom (e.g. `funExt`) in `docs/proof-debt.md`. - -## 2. Licence debt - -| Field | Value | -|---|---| -| LICENSE file | `LICENSE` | -| SPDX header | `MPL-2.0` | -| Manifest licence | `NONE` | -| Body classifier | `Palimp-MPL-2.0` | -| Severity | `ok` | - -**Recommended next move:** none for licence. - -## 3. Documentation debt - -| Field | Value | -|---|---| -| README lines | 186 | -| `docs/` files | 70 | -| `docs/` LoC | 4218 | -| CHANGELOG.md | Y | -| CONTRIBUTING.md | N | -| CODE_OF_CONDUCT.md | N | -| SECURITY.md | N | -| Severity | `OK` | - -**Recommended next move:** none for docs. - -## Cross-references - -- Estate proof-debt audit: `hyperpolymath/standards/docs/audits/2026-05-26-estate-proof-debt.md` -- Estate licence-debt audit: `hyperpolymath/standards/docs/audits/2026-05-26-estate-licence-debt.md` -- Estate documentation-debt audit: `hyperpolymath/standards/docs/audits/2026-05-26-estate-documentation-debt.md` - ---- - -🤖 Generated by Claude Code estate-wide tech-debt scan (2026-05-26). This file is informational — closing the debt is follow-up work owned by the maintainer.