docs: refresh human + machine documentation, add a live debt register - #60
Conversation
The three-layer claim checker is this repository's principal subject and was barely documented; the AffineScript same-cube example was over-represented relative to it. This corrects the proportion and fixes what the audit found. HUMAN - ARCHITECTURE.md was template boilerplate: it described src/, tests/, config/ and README.adoc, none of which match this repo, duplicated the real docs/ARCHITECTURE.md, and said nothing at all about the three layers. Rewritten in two parts — Part I the layer architecture (type / trope / sortal, the diode's real scope, the doubling attack, the L3 -> L2 dependency arrow, decided-not-built status), Part II the shipping extractor/classifier. `faces` is now presented as one worked example among six profiles. - README.md said every face's lowering "must normalise to the same canonical text". The verifier was upgraded to compile each face to typed-wasm and compare sha256, with the text diff kept only as a diagnostic. The README had drifted from the tool in exactly the way the tool exists to catch. Corrected, and a three-layer section added with a pointer to ADR-0001. MACHINE - 0-AI-MANIFEST.a2ml: real directory structure (it omitted docs/decisions/, proofs/, examples/, src/ui/); a new (architecture ...) block carrying the three layers, the dependency order, the doubling attack, decided-not-built status and the L1/L2/L3 numbering hazard; a new (debt ...) block; ADR-0001 in milestones; decisions/architecture/debt in canonical-locations. The do-not-paraphrase (core-idea) block is untouched. - Wiki was a one-line default stub; now Home + Three-Layers. DEBT — new docs/DEBT.md, live register across six dimensions - Architecture (HIGH): Layer 1 has no substrate anywhere; Layer 3's equivalence side (move relation, quotient, normal form) does not exist; Layer 2's vocabulary does not match its implementation (p-residue exists in no repo). - CI/CD (CRITICAL): no .github/actions-lock.json, so all workflows are startup_failure on every branch and main has never been green — every other gate is decorative. Includes the gh pr checks diagnosis trap. - Licence: GitHub reported NO licence. Cause found — LICENSE deviated from canonical MPL-2.0 by a trailing space (line 38) and http vs https (line 360). Replaced with the canonical text. SPDX-not-on-line-1 recorded with an explicit warning not to fix by adding headers. - Proof: SameCube.agda is real (--safe, zero postulates, zero holes) but UNGATED; verify-same-cube.sh exits 0 on a missing compiler. - Docs, Code: as above; source is clean (zero TODO/FIXME/todo!/unimplemented!). docs/tech-debt-2026-05-26.md's "RESOLVED" banner was partly wrong and is corrected in place: licence was not actually detected, and proof debt was half closed — the artefact existed, the verification did not. Repo metadata (applied via API, not in this diff): description now states what the tool does rather than "Phase A in progress"; topics replaced with eight concept-level ones — none derivable from GitHub's own signals. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
The audit measured all workflows as startup_failure on every branch and filed C1 as CRITICAL. PR #56 adopted .github/workflows/actions.lock while this was being written, so the headline finding was stale before it landed. Re-measured on main: 10 workflows green (Code Quality, CodeQL, Governance, Guix/Nix, Hypatia, RSR Anti-Pattern, Runtime Policy, Rust CI, Secret Scanner, Security Policy). The gates are real now. C1 is rewritten as RESOLVED with the history kept, and the residue split out: - C2 OSSF Scorecard still startup_failure — the one the lockfile did not reach - C3 Well-Known Standards + Workflow Security Linter fail on CONTENT, untriaged; both were invisible until the lockfile landed because neither could start - C4 no proof gate (unchanged) K1's rationale is inverted accordingly: test coverage was explicitly not worth doing while nothing could run in CI; now Rust CI is green, it is. Same correction applied to the manifest's (debt ...) block and the wiki.
| | `proofs/`, `examples/same-cube/`, `scripts/verify-same-cube.sh` | The `faces` worked example and its grounding check. | | ||
| | `docs/` | `ARCHITECTURE.md` (module contracts), `EXTENDING.md`, `ECHO-TYPES.md`, `DEBT.md`. | | ||
| | `desktop/`, `assets/` | `.desktop` launcher entry and icons. | | ||
| | `src/ui/` | `invariant_path_gui.affine` — an AffineScript GUI sketch. **Not in the Cargo workspace; built by nothing.** Design material, not code. | |
There was a problem hiding this comment.
💡 Quality: src/ui/ layout entry points to wrong path depth
ARCHITECTURE.md's Layout table (and 0-AI-MANIFEST's structure block) describe src/ui/ as containing invariant_path_gui.affine, but the file actually lives at src/ui/tea/invariant_path_gui.affine (one directory deeper). Since this PR's stated purpose is making the docs match the tree exactly, update the entry to reference src/ui/tea/ (or note the nesting) so the path is accurate.
Was this helpful? React with 👍 / 👎
There was a problem hiding this comment.
Configure merge blocking · Maintainers can dismiss this review.
|
Note Automatic reviews are paused because your trial's included automatic processing has been used for this period. Upgrade now, or comment "Gitar review" to run a review anytime. Code Review 👍 Approved with suggestions 0 resolved / 1 findingsRefreshes human and machine documentation to detail the three-layer claim checker and introduces a live debt register. Consider correcting the layout entry point path depth in ARCHITECTURE.md.
💡 Quality: src/ui/ layout entry points to wrong path depth📄 ARCHITECTURE.md:255 📄 0-AI-MANIFEST.a2ml:110 ARCHITECTURE.md's Layout table (and 0-AI-MANIFEST's structure block) describe 🤖 Prompt for agentsOptionsDisplay: compact → Showing less information. Comment with these commands to change the behavior for this request:
Important Your trial ends in 3 days — upgrade now to keep code review, CI analysis, auto-apply, custom automations, and more. Was this helpful? React with 👍 / 👎 | Gitar |
This comment has been minimized.
This comment has been minimized.
#55, #60) Squashes the documentation stack. Three PRs, one commit. #53 — state the idea where agents read it first A (core-idea ...) block in 0-AI-MANIFEST.a2ml, marked DO-NOT-PARAPHRASE: a claim can hold on BOTH sides of a domain transition and still not MEAN the same thing; the invariant is 'the SAME CLAIM here and there'. Previously this existed only in a dated DESIGN.md entry, where it was accurate and invisible, so every agent read the plumbing and reinvented the idea. #55 — ADR-0001: Layer 3 is the SORTAL layer A five-count case against the third layer was built deliberately and attacked adversarially. Three of the five counts broke: - 'the diode abolishes the subject matter' is wrong; the diode constrains edges but cannot constrain the Morse structure at merge/split vertices, so confluence diamonds are closed curves and two of them link with every edge still forward in time. - 'the plane is notation' falls to intrinsic linking. - 'it is only a complexity switch' falls to the doubling attack. The layer is retained as the sortal layer: it adjudicates identity of an argument across presentations, issuing equivalence or obstruction certificates, and it is UPSTREAM of Layer 2's soundness. Also corrects affine vs linear, and names the blind spot that gap creates. #60 — documentation refresh + live debt register ARCHITECTURE.md was template boilerplate describing directories this repo does not have; rewritten around the three layers, which are the principal subject. README described a superseded verification method (canonical text, where the verifier now compares typed-wasm sha256) — the README had drifted from the tool in exactly the way the tool exists to catch. New docs/DEBT.md across six dimensions. LICENSE replaced with canonical MPL-2.0: it deviated by a trailing space and one http/https, and GitHub reported NO licence as a result. Merged with --admin. The main ruleset is unsatisfiable by construction here: required_deployments demands a github-pages deployment that does not occur, code_coverage demands 95% with no coverage reporting configured, and the required context 'governance / Validate Hypatia Baseline' reports SKIPPED. All 14 checks on the docs content were green; the two red workflows (Workflow Security Linter, and a stale Hypatia run) are pre-existing on main and are tracked as C3 in the new debt register.
Stacked on #53. Retargets to
mainautomatically when that merges.The correction that drove this
The three-layer claim checker is this repository's principal subject — and it was barely documented, while the AffineScript same-cube example was over-represented relative to it.
facesis one profile of six, a lens onto a corpus that lives elsewhere: a good demonstration of the idea in miniature, not the subject. This PR fixes that proportion.Human
ARCHITECTURE.mdwas template boilerplate describingsrc/,tests/,config/andREADME.adoc— none of which match this repo — duplicating the realdocs/ARCHITECTURE.md, and saying nothing whatever about the three layers. (Closed PR #58 independently spotted this as "drop false ARCHITECTURE"; it did not land, so the problem persisted.)Rewritten in two parts: Part I the layer architecture — Layer 1 (
type) and what the diode actually buys, with its three open problems (epistemic vs ontic clock, partial-order time, composition-forgery as holonomy); Layer 2 (trope) as actually built intrope-checker/hermeneia, affine with a guarded contraction rule; Layer 3 (sortal), the doubling attack, and theL3 -> L2dependency arrow. Part II the shipping extractor/classifier.README.mdhad drifted from the tool. It said every face's lowering "must normalise to the same canonical text"; the verifier now compiles each face to typed-wasm and comparessha256, keeping text diffs as a diagnostic only. The README asserted something that held on both sides of a transition while no longer meaning the same thing — this repository's own failure mode, turned inward.Machine
0-AI-MANIFEST.a2ml: real structure (it omitteddocs/decisions/,proofs/,examples/,src/ui/); new(architecture …)block with the three layers, dependency order, doubling attack, decided-not-built status and theL1/L2/L3numbering hazard; new(debt …)block; ADR-0001 in milestones. The do-not-paraphrase(core-idea)block is untouched.Wiki was a one-line stub →
Home+Three-Layers(pushed separately — wikis are their own git repo).Debt — new
docs/DEBT.mdThe headline finding went stale mid-audit, and that is recorded rather than hidden. C1 was filed CRITICAL — no lockfile, every workflow
startup_failureon every branch,mainnever green. PR #56 fixed it while this was being written. Re-measured: 10 workflows green onmainincluding Rust CI, CodeQL and Secret Scanner. C1 is now RESOLVED with the history kept, and the residue split into C2 (Scorecard stillstartup_failure), C3 (two workflows failing on content, untriaged — invisible until the lockfile landed), C4 (no proof gate).Other findings:
LICENSEdeviated from canonical MPL-2.0 by a trailing space (line 38) andhttpvshttps(line 360). Replaced with the canonical text.p-residueexists in no repository).SameCube.agdais genuinely good (--safe, zero postulates, zero holes) but ungated.docs/tech-debt-2026-05-26.md's "RESOLVED" banner was partly wrong and is corrected in place: licence was not actually detected, and proof debt was half closed.Repo metadata (applied via API, not in this diff)
Dual-use claim-grounder (Phase A in progress)— vague and stale. Now states what the tool does and its governance role.development, hyperpolymath, open-source, rust, software, tooling— owner name, generic words, and a language GitHub detects itself. Replaced with eight concept-level ones:claim-checking,argumentation,semantic-drift,provenance,cross-domain-equivalence,architecture-decision-records,formal-methods,static-analysis.Verification
0-AI-MANIFEST.a2mlparens and quotes balancereuse lintmissing-info count unchanged from baseline (1, pre-existing) — verified by stashing and re-runningARCHITECTURE.mdexists on disk🤖 Generated with Claude Code