From bcc2ac6f8f2ad14a35d831ba4b0374fbce392e8c Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Mon, 24 Aug 2026 08:20:15 +0100 Subject: [PATCH] refactor: migrate repository documentation from Markdown to AsciiDoc --- ARCHITECTURE.adoc | 299 +++++++++++++++ ARCHITECTURE.md | 267 -------------- CHANGELOG.adoc | 47 +++ CHANGELOG.md | 45 --- CODE_OF_CONDUCT.adoc | 339 ++++++++++++++++++ CODE_OF_CONDUCT.md | 327 ----------------- CONTRIBUTING.adoc | 32 ++ CONTRIBUTING.md | 36 -- DESIGN.adoc | 97 +++++ DESIGN.md | 55 --- GOVERNANCE.adoc | 60 ++++ GOVERNANCE.md | 60 ---- README.adoc | 191 ++++++++++ README.md | 177 --------- SECURITY.adoc | 22 ++ SECURITY.md | 25 -- docs/ARCHITECTURE.adoc | 44 +++ docs/ARCHITECTURE.md | 32 -- docs/DEBT.adoc | 329 +++++++++++++++++ docs/DEBT.md | 306 ---------------- docs/ECHO-TYPES.adoc | 92 +++++ docs/ECHO-TYPES.md | 78 ---- docs/EXTENDING.adoc | 41 +++ docs/EXTENDING.md | 31 -- docs/reports/audit/audit-2026-04-15-post.adoc | 25 ++ docs/reports/audit/audit-2026-04-15-post.md | 17 - docs/reports/audit/audit-2026-04-15-pre.adoc | 22 ++ docs/reports/audit/audit-2026-04-15-pre.md | 17 - docs/tech-debt-2026-05-26.adoc | 95 +++++ docs/tech-debt-2026-05-26.md | 73 ---- examples/same-cube/README.adoc | 76 ++++ examples/same-cube/README.md | 70 ---- examples/seed_examples.adoc | 14 + examples/seed_examples.md | 12 - profiles/echidna.adoc | 6 + profiles/echidna.md | 8 - profiles/faces.adoc | 100 ++++++ profiles/faces.md | 90 ----- profiles/hypatia.adoc | 6 + profiles/hypatia.md | 8 - profiles/panll.adoc | 6 + profiles/panll.md | 8 - profiles/pmpl.adoc | 47 +++ profiles/pmpl.md | 47 --- profiles/standards-docs.adoc | 68 ++++ profiles/standards-docs.md | 69 ---- proofs/README.adoc | 38 ++ proofs/README.md | 36 -- 48 files changed, 2096 insertions(+), 1894 deletions(-) create mode 100644 ARCHITECTURE.adoc delete mode 100644 ARCHITECTURE.md create mode 100644 CHANGELOG.adoc delete mode 100644 CHANGELOG.md create mode 100644 CODE_OF_CONDUCT.adoc delete mode 100644 CODE_OF_CONDUCT.md create mode 100644 CONTRIBUTING.adoc delete mode 100644 CONTRIBUTING.md create mode 100644 DESIGN.adoc delete mode 100644 DESIGN.md create mode 100644 GOVERNANCE.adoc delete mode 100644 GOVERNANCE.md create mode 100644 README.adoc delete mode 100644 README.md create mode 100644 SECURITY.adoc delete mode 100644 SECURITY.md create mode 100644 docs/ARCHITECTURE.adoc delete mode 100644 docs/ARCHITECTURE.md create mode 100644 docs/DEBT.adoc delete mode 100644 docs/DEBT.md create mode 100644 docs/ECHO-TYPES.adoc delete mode 100644 docs/ECHO-TYPES.md create mode 100644 docs/EXTENDING.adoc delete mode 100644 docs/EXTENDING.md create mode 100644 docs/reports/audit/audit-2026-04-15-post.adoc delete mode 100644 docs/reports/audit/audit-2026-04-15-post.md create mode 100644 docs/reports/audit/audit-2026-04-15-pre.adoc delete mode 100644 docs/reports/audit/audit-2026-04-15-pre.md create mode 100644 docs/tech-debt-2026-05-26.adoc delete mode 100644 docs/tech-debt-2026-05-26.md create mode 100644 examples/same-cube/README.adoc delete mode 100644 examples/same-cube/README.md create mode 100644 examples/seed_examples.adoc delete mode 100644 examples/seed_examples.md create mode 100644 profiles/echidna.adoc delete mode 100644 profiles/echidna.md create mode 100644 profiles/faces.adoc delete mode 100644 profiles/faces.md create mode 100644 profiles/hypatia.adoc delete mode 100644 profiles/hypatia.md create mode 100644 profiles/panll.adoc delete mode 100644 profiles/panll.md create mode 100644 profiles/pmpl.adoc delete mode 100644 profiles/pmpl.md create mode 100644 profiles/standards-docs.adoc delete mode 100644 profiles/standards-docs.md create mode 100644 proofs/README.adoc delete mode 100644 proofs/README.md diff --git a/ARCHITECTURE.adoc b/ARCHITECTURE.adoc new file mode 100644 index 0000000..6b4edef --- /dev/null +++ b/ARCHITECTURE.adoc @@ -0,0 +1,299 @@ +== Architecture + +____ +*Read `+0-AI-MANIFEST.a2ml+` first.* Its `+(core-idea …)+` block is the +canonical statement of what this repository is for, and it is marked +do-not-paraphrase. This file describes how the work is arranged; it does +not restate the idea. +____ + +Invariant Path is a claim-path debugger, not a truth engine. It has two +faces: + +[arabic] +. *The governance front-end for a three-layer claim checker.* This is +where the layer architecture is decided and recorded. Most of the +intellectual work lives here. +. *A working extractor and classifier.* A Rust CLI that finds claim +transitions in repository artifacts and records what each one preserves +and loses. This is what currently ships. + +The second is not an implementation of the first. Keeping that +distinction visible is the point of this document. + +''''' + +=== Part I — The three-layer claim checker + +A claim is checked by three layers, each answering a question the others +cannot. `+nextgen-language-evangeliser+` names this repository as the +_governance front-end_ for that architecture: rulings are recorded here +as ADRs, and each equivalence claim is anchored to its code locations +plus a witness, human-in-the-loop and editable. + +==== Layer 1 — `+type+`: formal admissibility + +Checkable on *form alone*, with no judgement of evidence quality. Three +sub-layers: + +* *Well-formedness* — is this a claim at all? +* *Continuity / through-line* — does the argument connect end to end? +* *Temporality — "`the diode`"* — a forward-only ordering constraint: +evidence must precede conclusion, no backward edges, applied *per +claim-type*. + +The diode was sited in Layer 1 deliberately, so that anything downstream +inherits strand orientations from a clean form-only rule rather than +from Layer 2’s purpose-indexed judgements. + +*What is settled, and what is not.* The diode is correct but narrower +than it looks: it rejects only _label-honest_ backward edges. Three open +problems are recorded in ADR-0001: + +* Its clock must be *epistemic* (when evidence was committed) rather +than ontic (when events happened), or retrodiction — history, forensics +— falsely fails to type-check. +* Epistemic time across multiple sources is therefore a *partial order*, +not a scalar clock, so verdicts must be proved invariant across +admissible interleavings of causally incomparable commits. +* Because the diode applies _per claim-type_, differently-clocked charts +glue together, and a composite path can run forward in every chart while +its endpoints reach backwards globally. ADR-0001 calls this +*composition-forgery*; it is a holonomy phenomenon — every chart flat, +the twist in the gluing. + +==== Layer 2 — `+trope+`: particularity and warrant + +*Purpose-indexed*, per strand: does individuated, context-bound evidence +survive the leap to _this_ conclusion for _this_ use? + +This is the layer with a real implementation, and it lives in +`+trope-checker+` and `+hermeneia+`, not here: + +* a six-coordinate *`+Grade+`* — four `+Fate+` fields plus `+Bond+` and +`+Merge+` (`+Trope/Grade.idr+`); +* nine *`+p-*+` effects* in +`+trope-particularity-workbench/vocabulary/+`, of which three are +_deceptive_ and absorbing under composition; +* a *`+Floor+`* — a use-model expressed as a partial demand vector +(`+Checker/Ir.idr+`); +* a verdict `+Sufficient | Insufficient+` that *carries a witness edge* +on failure (`+Checker/Check.idr+`); +* *p-sufficiency*, defined as `+floor(U) ⊑ acc(v)+` — the declared floor +lies below the accumulated grade in a componentwise retention order. + +Grades compose associatively along transformation paths, with the +fidelity coordinate accumulating tropically. + +*Resource discipline: affine, with a guarded contraction rule.* At most +once — weakening is free, contraction is not — but contraction _is_ +permitted when a resemblance warrant licenses it. That is not plain +affine logic, and the distinction is load-bearing; see the doubling +attack below. + +==== Layer 3 — `+sortal+`: identity across presentations + +Ruled 2026-08-05 in `+docs/decisions/0001-the-sortal-layer.adoc+`, after +a five-count case against the layer was built deliberately and *three of +the five counts broke* under adversarial review. + +The layer adjudicates *identity of an argument across presentations*, +and issues one of two things: + +* an *equivalence certificate* — a sequence of moves, every intermediate +of which still passes Layers 1 and 2, transforming one presentation into +the other; +* an *obstruction certificate* — an invariant separating them under the +same quotient. + +Detection and equivalence-certification are *dual*, so "`it is only an +equivalence proof`" is the job stated correctly, not a demotion. + +The name is from the same literature `+trope+` came from: a *sortal* +supplies a _criterion of identity_ and a _principle of counting_ for its +instances. Both halves do work — the criterion decides "`same +argument`", the count decides whether two corroborating lines are two +witnesses or one witness echoed. + +==== The doubling attack, and why Layer 3 precedes Layer 2 + +Present one derivation *twice*, paraphrased, under distinct labels. +Every node is label-honest, so the diode is silent. Every chain +terminates in genuinely attested exogenous anchors, so attestation and +well-foundedness both pass. Each copy individually passes Layer 2. + +The doubled web and an honestly-redundant two-witness web have +*identical pass/fail profiles on every subdiagram* — yet corroboration +weight is two versus one. + +This is not an illegal contraction. It is a contraction that was +*mandatory and never taken*, and the affine resource algebra is +structurally blind to it: nothing illegal happened, two distinct labels +really were spent once each. Whether they were the same token is a fact +about _identity_, which is not a resource property. + +Hence the dependency arrow that the original design was missing: + +.... +Layer 1 (type) ──orientations──▶ Layer 3 (sortal) ──identities──▶ Layer 2 (trope) +.... + +Overlapping presentations must be recognised as the same argument +*before* resource accounting runs, or Layer 2 double-counts. Layer 3 is +upstream of Layer 2’s soundness, not decoration downstream of it. + +==== Status: decided, not built + +*Nothing in this repository implements these layers.* ADR-0001 is a +decision record about an architecture, and says so. A survey of existing +formal work (recorded in the ADR) found: + +* *Layer 1* — no substrate anywhere in the estate. No syntax of claims, +no ordering on evidence events. Must be built from scratch. +* *Layer 2* — real support from `+tropical-types+` (the retention order +derived from one line of idempotence, axiom-free, behind a genuine CI +gate) and `+echo-types+` (path-independence of degradation holds +precisely if the retention order is propositional, with a countermodel). +* *Layer 3* — roughly a quarter, obstruction side only. `+echo-types+` +supplies the fibre `+Echo f y = Σ A (λ x → f x ≡ y)+` — "`which distinct +presentations collapsed to the same argument`" — and "`identified +members count once`". There is *nothing* on the equivalence side: no +move relation, no quotient, no normal form, anywhere. + +Two candidate substrates were investigated and *refuted with evidence*: +QuandleDB (a homonym — topological invariants are blind to labels, so a +quandle fingerprint cannot see the doubling attack and would return +false positives) and absolute-zero’s CNO (machine-checked refutation +against its own Coq). + +==== Conventions + +Do not write bare `+L1+` / `+L2+` / `+L3+`. Three unrelated L-numberings +are live in adjacent repositories, and both neighbours put temporality +at _their_ L9 while this architecture puts it at Layer 1c. Write +`+Layer 1 (type)+`, `+Layer 2 (trope)+`, `+Layer 3 (sortal)+`; prefix +foreign references `+kat-L7+`, `+ty-L9+`. + +''''' + +=== Part II — The shipping tool + +What actually compiles and runs today: a pipeline from artifact text to +a reviewable record. + +.... +artifact text + │ + ▼ + extractor candidate claim transitions, anchored by trigger phrase + │ and byte span + ▼ + classifier invariant type; losses/preserved; break condition; + │ a Classification + ▼ + annotations JSONL, upsert-on-write, visibility + status + │ + ▼ + CLI scan / accept / dismiss / clarify / add / update / overlay +.... + +Two commitments explain most of the code. + +*Heuristics are deliberately strict.* The extractor triggers on explicit +transition markers and accepts false negatives to avoid annotation noise +(`+DESIGN.md+`, 2026-04-10). A noisy suggester costs more trust than it +saves. + +*The path is retained, never discarded.* A bare `+Classification+` +cannot recover the claim-path that produced it, so +`+ClassificationOutcome+` carries `+losses+` and `+preserved+` alongside +the verdict — the `+echo-types+` fibre discipline applied to a +classifier. See `+docs/ECHO-TYPES.md+`. + +==== Domain model + +In `+crates/invariant-path-core/src/model.rs+`: + +* *`+ClaimCandidate+`* — source span, target text, matched trigger, path +description. +* *`+InvariantType+`* — what is meant to be preserved: +`+CausalRelationship+`, `+StatisticalRelationship+`, +`+LogicalImplication+`, `+Mechanism+`, `+RiskProbability+`, +`+NormativeBridge+`, `+ResourceBudget+`, `+Provenance+`. +* *`+Classification+`* — `+ValidPath+`, `+Overextended+`, +`+Conflation+`, `+Incomplete+`, `+Abstain+`. +* *`+ClassificationOutcome+`* — the verdict _plus_ `+losses+`, +`+preserved+`, break condition. The retained echo. +* *`+Annotation+`* — the persisted record, with `+Visibility+` and +`+Status+`. + +The classifier is pure and offline: term lists in `+classifier.rs+`, no +model, no network, no external state. + +==== Profiles + +A profile is a *lens onto a corpus that lives elsewhere*. It names a +target by path and *vendors nothing*. `+pmpl.md+` is the reference +implementation. + +The rule exists because a profile carrying a copy of its target drifts +from the real thing and then grounds a claim about a stale fixture +_while reporting success_ — this tool’s own failure mode, turned inward. +Profiles are named for their *target*, not for one claim about it. + +Six exist: `+echidna+`, `+faces+`, `+hypatia+`, `+panll+`, `+pmpl+`, +`+standards-docs+`. + +`+faces+` is the one worked example that is fully grounded end to end: +it checks that AffineScript’s several surface syntaxes all lower to one +canonical form, by compiling each to typed-wasm and comparing `+sha256+` +hashes. It is a good demonstration of the whole idea in miniature — and +it is _an example_, not the subject of this repository. It also violates +the profile rule twice (it vendors its corpus, and it is named for a +claim rather than a target), which is issue #54. Details in +`+profiles/faces.md+`; its Agda companion is `+proofs/SameCube.agda+`. + +=== Layout + +[width="100%",cols="50%,50%",options="header",] +|=== +|Path |What lives there +|`+docs/decisions/+` |*ADRs — the layer rulings. Start at ADR-0001.* + +|`+crates/invariant-path-core/+` |The library: `+extractor.rs+`, +`+classifier.rs+`, `+model.rs+`, `+annotations.rs+`, `+doc_claims.rs+`, +`+pipeline.rs+`. + +|`+crates/invariant-path-cli/+` |The binary. Single `+main.rs+`; parsing +and output only. + +|`+schemas/annotation.schema.json+` |The contract between this tool and +anything reading its store. + +|`+profiles/+` |One markdown file per target corpus. Vendors nothing. + +|`+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. +|=== + +The Cargo workspace is exactly the two crates in `+members+`; nothing +under `+src/+` is compiled. + +=== What this is not + +* Not a truth engine. It never decides whether a claim is true. +* Not an implementation of the three layers. Those are decided, not +built. +* Not a prover. `+proofs/+` grounds one claim in one worked example. +* Not networked. No service, no telemetry, no model calls. +* Not a general NLP pipeline. The classifier is term lists and pattern +matches, chosen so a reader can audit every decision it makes. diff --git a/ARCHITECTURE.md b/ARCHITECTURE.md deleted file mode 100644 index 5e88e4f..0000000 --- a/ARCHITECTURE.md +++ /dev/null @@ -1,267 +0,0 @@ - - -# Architecture - -> **Read `0-AI-MANIFEST.a2ml` first.** Its `(core-idea …)` block is the canonical -> statement of what this repository is for, and it is marked do-not-paraphrase. -> This file describes how the work is arranged; it does not restate the idea. - -Invariant Path is a claim-path debugger, not a truth engine. It has two faces: - -1. **The governance front-end for a three-layer claim checker.** This is where - the layer architecture is decided and recorded. Most of the intellectual - work lives here. -2. **A working extractor and classifier.** A Rust CLI that finds claim - transitions in repository artifacts and records what each one preserves and - loses. This is what currently ships. - -The second is not an implementation of the first. Keeping that distinction -visible is the point of this document. - ---- - -## Part I — The three-layer claim checker - -A claim is checked by three layers, each answering a question the others -cannot. `nextgen-language-evangeliser` names this repository as the *governance -front-end* for that architecture: rulings are recorded here as ADRs, and each -equivalence claim is anchored to its code locations plus a witness, -human-in-the-loop and editable. - -### Layer 1 — `type`: formal admissibility - -Checkable on **form alone**, with no judgement of evidence quality. Three -sub-layers: - -- **Well-formedness** — is this a claim at all? -- **Continuity / through-line** — does the argument connect end to end? -- **Temporality — "the diode"** — a forward-only ordering constraint: evidence - must precede conclusion, no backward edges, applied **per claim-type**. - -The diode was sited in Layer 1 deliberately, so that anything downstream -inherits strand orientations from a clean form-only rule rather than from Layer -2's purpose-indexed judgements. - -**What is settled, and what is not.** The diode is correct but narrower than it -looks: it rejects only *label-honest* backward edges. Three open problems are -recorded in ADR-0001: - -- Its clock must be **epistemic** (when evidence was committed) rather than - ontic (when events happened), or retrodiction — history, forensics — falsely - fails to type-check. -- Epistemic time across multiple sources is therefore a **partial order**, not - a scalar clock, so verdicts must be proved invariant across admissible - interleavings of causally incomparable commits. -- Because the diode applies *per claim-type*, differently-clocked charts glue - together, and a composite path can run forward in every chart while its - endpoints reach backwards globally. ADR-0001 calls this **composition-forgery**; - it is a holonomy phenomenon — every chart flat, the twist in the gluing. - -### Layer 2 — `trope`: particularity and warrant - -**Purpose-indexed**, per strand: does individuated, context-bound evidence -survive the leap to *this* conclusion for *this* use? - -This is the layer with a real implementation, and it lives in -`trope-checker` and `hermeneia`, not here: - -- a six-coordinate **`Grade`** — four `Fate` fields plus `Bond` and `Merge` - (`Trope/Grade.idr`); -- nine **`p-*` effects** in `trope-particularity-workbench/vocabulary/`, of - which three are *deceptive* and absorbing under composition; -- a **`Floor`** — a use-model expressed as a partial demand vector - (`Checker/Ir.idr`); -- a verdict `Sufficient | Insufficient` that **carries a witness edge** on - failure (`Checker/Check.idr`); -- **p-sufficiency**, defined as `floor(U) ⊑ acc(v)` — the declared floor lies - below the accumulated grade in a componentwise retention order. - -Grades compose associatively along transformation paths, with the fidelity -coordinate accumulating tropically. - -**Resource discipline: affine, with a guarded contraction rule.** At most once -— weakening is free, contraction is not — but contraction *is* permitted when a -resemblance warrant licenses it. That is not plain affine logic, and the -distinction is load-bearing; see the doubling attack below. - -### Layer 3 — `sortal`: identity across presentations - -Ruled 2026-08-05 in `docs/decisions/0001-the-sortal-layer.adoc`, after a -five-count case against the layer was built deliberately and **three of the -five counts broke** under adversarial review. - -The layer adjudicates **identity of an argument across presentations**, and -issues one of two things: - -- an **equivalence certificate** — a sequence of moves, every intermediate of - which still passes Layers 1 and 2, transforming one presentation into the - other; -- an **obstruction certificate** — an invariant separating them under the same - quotient. - -Detection and equivalence-certification are **dual**, so "it is only an -equivalence proof" is the job stated correctly, not a demotion. - -The name is from the same literature `trope` came from: a **sortal** supplies a -*criterion of identity* and a *principle of counting* for its instances. Both -halves do work — the criterion decides "same argument", the count decides -whether two corroborating lines are two witnesses or one witness echoed. - -### The doubling attack, and why Layer 3 precedes Layer 2 - -Present one derivation **twice**, paraphrased, under distinct labels. Every -node is label-honest, so the diode is silent. Every chain terminates in -genuinely attested exogenous anchors, so attestation and well-foundedness both -pass. Each copy individually passes Layer 2. - -The doubled web and an honestly-redundant two-witness web have **identical -pass/fail profiles on every subdiagram** — yet corroboration weight is two -versus one. - -This is not an illegal contraction. It is a contraction that was **mandatory -and never taken**, and the affine resource algebra is structurally blind to it: -nothing illegal happened, two distinct labels really were spent once each. -Whether they were the same token is a fact about *identity*, which is not a -resource property. - -Hence the dependency arrow that the original design was missing: - -``` -Layer 1 (type) ──orientations──▶ Layer 3 (sortal) ──identities──▶ Layer 2 (trope) -``` - -Overlapping presentations must be recognised as the same argument **before** -resource accounting runs, or Layer 2 double-counts. Layer 3 is upstream of -Layer 2's soundness, not decoration downstream of it. - -### Status: decided, not built - -**Nothing in this repository implements these layers.** ADR-0001 is a decision -record about an architecture, and says so. A survey of existing formal work -(recorded in the ADR) found: - -- **Layer 1** — no substrate anywhere in the estate. No syntax of claims, no - ordering on evidence events. Must be built from scratch. -- **Layer 2** — real support from `tropical-types` (the retention order derived - from one line of idempotence, axiom-free, behind a genuine CI gate) and - `echo-types` (path-independence of degradation holds precisely if the - retention order is propositional, with a countermodel). -- **Layer 3** — roughly a quarter, obstruction side only. `echo-types` supplies - the fibre `Echo f y = Σ A (λ x → f x ≡ y)` — "which distinct presentations - collapsed to the same argument" — and "identified members count once". There - is **nothing** on the equivalence side: no move relation, no quotient, no - normal form, anywhere. - -Two candidate substrates were investigated and **refuted with evidence**: -QuandleDB (a homonym — topological invariants are blind to labels, so a quandle -fingerprint cannot see the doubling attack and would return false positives) -and absolute-zero's CNO (machine-checked refutation against its own Coq). - -### Conventions - -Do not write bare `L1` / `L2` / `L3`. Three unrelated L-numberings are live in -adjacent repositories, and both neighbours put temporality at *their* L9 while -this architecture puts it at Layer 1c. Write `Layer 1 (type)`, -`Layer 2 (trope)`, `Layer 3 (sortal)`; prefix foreign references `kat-L7`, -`ty-L9`. - ---- - -## Part II — The shipping tool - -What actually compiles and runs today: a pipeline from artifact text to a -reviewable record. - -``` -artifact text - │ - ▼ - extractor candidate claim transitions, anchored by trigger phrase - │ and byte span - ▼ - classifier invariant type; losses/preserved; break condition; - │ a Classification - ▼ - annotations JSONL, upsert-on-write, visibility + status - │ - ▼ - CLI scan / accept / dismiss / clarify / add / update / overlay -``` - -Two commitments explain most of the code. - -**Heuristics are deliberately strict.** The extractor triggers on explicit -transition markers and accepts false negatives to avoid annotation noise -(`DESIGN.md`, 2026-04-10). A noisy suggester costs more trust than it saves. - -**The path is retained, never discarded.** A bare `Classification` cannot -recover the claim-path that produced it, so `ClassificationOutcome` carries -`losses` and `preserved` alongside the verdict — the `echo-types` fibre -discipline applied to a classifier. See `docs/ECHO-TYPES.md`. - -### Domain model - -In `crates/invariant-path-core/src/model.rs`: - -- **`ClaimCandidate`** — source span, target text, matched trigger, path - description. -- **`InvariantType`** — what is meant to be preserved: `CausalRelationship`, - `StatisticalRelationship`, `LogicalImplication`, `Mechanism`, - `RiskProbability`, `NormativeBridge`, `ResourceBudget`, `Provenance`. -- **`Classification`** — `ValidPath`, `Overextended`, `Conflation`, - `Incomplete`, `Abstain`. -- **`ClassificationOutcome`** — the verdict *plus* `losses`, `preserved`, break - condition. The retained echo. -- **`Annotation`** — the persisted record, with `Visibility` and `Status`. - -The classifier is pure and offline: term lists in `classifier.rs`, no model, no -network, no external state. - -### Profiles - -A profile is a **lens onto a corpus that lives elsewhere**. It names a target -by path and **vendors nothing**. `pmpl.md` is the reference implementation. - -The rule exists because a profile carrying a copy of its target drifts from the -real thing and then grounds a claim about a stale fixture *while reporting -success* — this tool's own failure mode, turned inward. Profiles are named for -their **target**, not for one claim about it. - -Six exist: `echidna`, `faces`, `hypatia`, `panll`, `pmpl`, `standards-docs`. - -`faces` is the one worked example that is fully grounded end to end: it checks -that AffineScript's several surface syntaxes all lower to one canonical form, -by compiling each to typed-wasm and comparing `sha256` hashes. It is a good -demonstration of the whole idea in miniature — and it is *an example*, not the -subject of this repository. It also violates the profile rule twice (it vendors -its corpus, and it is named for a claim rather than a target), which is issue -#54. Details in `profiles/faces.md`; its Agda companion is `proofs/SameCube.agda`. - -## Layout - -| Path | What lives there | -|---|---| -| `docs/decisions/` | **ADRs — the layer rulings. Start at ADR-0001.** | -| `crates/invariant-path-core/` | The library: `extractor.rs`, `classifier.rs`, `model.rs`, `annotations.rs`, `doc_claims.rs`, `pipeline.rs`. | -| `crates/invariant-path-cli/` | The binary. Single `main.rs`; parsing and output only. | -| `schemas/annotation.schema.json` | The contract between this tool and anything reading its store. | -| `profiles/` | One markdown file per target corpus. Vendors nothing. | -| `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. | - -The Cargo workspace is exactly the two crates in `members`; nothing under -`src/` is compiled. - -## What this is not - -- Not a truth engine. It never decides whether a claim is true. -- Not an implementation of the three layers. Those are decided, not built. -- Not a prover. `proofs/` grounds one claim in one worked example. -- Not networked. No service, no telemetry, no model calls. -- Not a general NLP pipeline. The classifier is term lists and pattern matches, - chosen so a reader can audit every decision it makes. diff --git a/CHANGELOG.adoc b/CHANGELOG.adoc new file mode 100644 index 0000000..3884bc4 --- /dev/null +++ b/CHANGELOG.adoc @@ -0,0 +1,47 @@ +== Changelog + +All notable changes to `+invariant-path+` will be documented in this +file. + +This file is generated from conventional commits by the +https://github.com/hyperpolymath/standards/blob/main/.github/workflows/changelog-reusable.yml[`+changelog-reusable.yml+`] +workflow (`+hyperpolymath/standards#206+`). Adopt the workflow in this +repo’s CI to keep this file in sync automatically — see +https://github.com/hyperpolymath/standards/blob/main/templates/cliff.toml[`+templates/cliff.toml+`] +for the canonical config. + +The format follows https://keepachangelog.com/en/1.1.0/[Keep a +Changelog]; this project aims to follow +https://semver.org/spec/v2.0.0.html[Semantic Versioning]. + +=== [Unreleased] + +==== Fixed + +* fix(ci): adopt canonical hypatia-scan.yml (env.HOME/scanner-layout + +Comment-step gate) (#7) +* fix(ci): adopt canonical hypatia-scan.yml (env.HOME/scanner-layout + +Comment-step gate) (#2) + +==== Documentation + +* docs: record tech-debt audit findings (2026-05-26) +* docs(readme): add SPDX header and/or standard badges +* docs: add post-audit status report for M5 sweep +* docs: add post-audit status report + +==== CI + +* ci(rust): convert rust-ci.yml to thin wrapper (standards#174) (#12) +* ci: bump actions/upload-artifact SHA to current v4 (#1) +* ci: add 13 standard RSR workflows (copied from rsr-template-repo) + +=== Pre-history + +Prior commits to this file’s introduction are recorded in git history +but not formally classified into Keep-a-Changelog sections. To backfill, +run `+git cliff -o CHANGELOG.md+` locally using the canonical +https://github.com/hyperpolymath/standards/blob/main/templates/cliff.toml[`+cliff.toml+`] +— this is one-shot mechanical work. + +''''' diff --git a/CHANGELOG.md b/CHANGELOG.md deleted file mode 100644 index 25cc444..0000000 --- a/CHANGELOG.md +++ /dev/null @@ -1,45 +0,0 @@ - - -# Changelog - -All notable changes to `invariant-path` will be documented in this file. - -This file is generated from conventional commits by the -[`changelog-reusable.yml`](https://github.com/hyperpolymath/standards/blob/main/.github/workflows/changelog-reusable.yml) -workflow (`hyperpolymath/standards#206`). Adopt the workflow in this repo's CI to keep this file in sync automatically — see -[`templates/cliff.toml`](https://github.com/hyperpolymath/standards/blob/main/templates/cliff.toml) -for the canonical config. - -The format follows [Keep a Changelog](https://keepachangelog.com/en/1.1.0/); -this project aims to follow [Semantic Versioning](https://semver.org/spec/v2.0.0.html). - -## [Unreleased] - -### Fixed - -- fix(ci): adopt canonical hypatia-scan.yml (env.HOME/scanner-layout + Comment-step gate) (#7) -- fix(ci): adopt canonical hypatia-scan.yml (env.HOME/scanner-layout + Comment-step gate) (#2) - -### Documentation - -- docs: record tech-debt audit findings (2026-05-26) -- docs(readme): add SPDX header and/or standard badges -- docs: add post-audit status report for M5 sweep -- docs: add post-audit status report - -### CI - -- ci(rust): convert rust-ci.yml to thin wrapper (standards#174) (#12) -- ci: bump actions/upload-artifact SHA to current v4 (#1) -- ci: add 13 standard RSR workflows (copied from rsr-template-repo) - -## Pre-history - -Prior commits to this file's introduction are recorded in git history but not formally classified into Keep-a-Changelog sections. To backfill, run `git cliff -o CHANGELOG.md` locally using the canonical [`cliff.toml`](https://github.com/hyperpolymath/standards/blob/main/templates/cliff.toml) — this is one-shot mechanical work. - ---- - - diff --git a/CODE_OF_CONDUCT.adoc b/CODE_OF_CONDUCT.adoc new file mode 100644 index 0000000..ff3f3db --- /dev/null +++ b/CODE_OF_CONDUCT.adoc @@ -0,0 +1,339 @@ +== Code of Conduct + +=== Our Pledge + +We as members, contributors, and leaders pledge to make participation in +Squisher Corpus a harassment-free experience for everyone, regardless of +age, body size, visible or invisible disability, ethnicity, sex +characteristics, gender identity and expression, level of experience, +education, socio-economic status, nationality, personal appearance, +race, caste, colour, religion, or sexual identity and orientation. + +We pledge to act and interact in ways that contribute to an open, +welcoming, diverse, inclusive, and healthy community. + +We recognise that a thriving open source community requires +*psychological safety* — an environment where people can contribute, ask +questions, make mistakes, and learn without fear of ridicule or +retaliation. + +''''' + +=== Our Standards + +==== Expected Behaviour + +The following behaviours contribute to a positive environment: + +*Communication* - Using welcoming and inclusive language - Being +respectful of differing viewpoints and experiences - Giving and +gracefully accepting constructive feedback - Assuming good intent while +addressing impact - Communicating clearly and patiently, especially with +newcomers + +*Collaboration* - Focusing on what is best for the community - Showing +empathy and kindness toward other community members - Being +collaborative rather than competitive - Mentoring and supporting less +experienced contributors - Celebrating others’ contributions and +successes + +*Professionalism* - Accepting responsibility and apologising to those +affected by our mistakes - Learning from the experience and avoiding +repetition - Respecting others’ time and attention - Staying on topic in +project spaces - Following project guidelines and conventions + +*Accessibility* - Using plain language and avoiding unnecessary jargon - +Providing alt text for images and transcripts for audio/video - Being +patient with those using assistive technologies - Accommodating +different communication styles and needs - Recognising that not everyone +communicates the same way + +==== Unacceptable Behaviour + +The following behaviours are considered harassment and are unacceptable: + +*Harassment* - The use of sexualised language or imagery, and sexual +attention or advances of any kind - Trolling, insulting or derogatory +comments, and personal or political attacks - Public or private +harassment - Deliberate intimidation, stalking, or following (online or +in-person) - Unwelcome physical contact or simulated physical contact +(e.g., emoji) - Sustained disruption of talks, events, or online +discussions + +*Discrimination* - Discriminatory jokes and language - Posting or +threatening to post others’ personally identifying information +("`doxing`") - Advocating for, or encouraging, any of the above +behaviour - Microaggressions — subtle, often unintentional, +discriminatory comments or actions + +*Professional Misconduct* - Publishing others’ private information +without explicit permission - Misrepresenting affiliation or +contributions - Plagiarism or claiming credit for others’ work - +Retaliating against anyone who reports a Code of Conduct violation - +Other conduct which could reasonably be considered inappropriate in a +professional setting + +==== Grey Areas + +Some situations require judgement. When uncertain: + +* *Intent vs Impact*: Good intentions do not excuse harmful impact. +Focus on making things right. +* *Power Dynamics*: Those with more power (maintainers, employers, +experienced contributors) must be especially mindful of their impact. +* *Cultural Differences*: What’s acceptable varies by culture. When in +doubt, err on the side of caution and ask. +* *Humour*: Jokes at others’ expense are rarely funny to everyone. Punch +up, not down. + +''''' + +=== Scope + +This Code of Conduct applies within all community spaces, including: + +*Online Spaces* - Repository discussions, issues, and pull/merge +requests - Project chat channels (Matrix, Discord, Slack, IRC) - Mailing +lists and forums - Social media when representing the project - Video +calls and virtual meetings + +*In-Person Spaces* - Conferences, meetups, and events - Workshops and +training sessions - Any gathering where you represent the project + +*Representation* This Code of Conduct also applies when an individual is +officially representing the community in public spaces. Examples +include: + +* Using an official project email address +* Posting via an official social media account +* Acting as an appointed representative at an event +* Speaking on behalf of the project + +''''' + +=== Enforcement + +==== Reporting + +If you experience or witness unacceptable behaviour, or have any other +concerns, please report it as soon as possible. + +*How to Report* + +[width="99%",cols="30%,33%,37%",options="header",] +|=== +|Method |Details |Best For +|*Email* |j.d.a.jewell@open.ac.uk |Detailed reports, sensitive matters + +|*Private Message* |Contact any maintainer directly |Quick questions, +minor issues + +|*Anonymous Form* |[Link to form if available] |When you need anonymity +|=== + +*What to Include* + +* Your contact information (unless anonymous) +* Names/usernames of those involved +* Description of what happened +* When and where it occurred +* Any witnesses +* Any supporting evidence (screenshots, links) +* How you would like us to respond (if you have a preference) + +*What Happens Next* + +[arabic] +. You will receive acknowledgment within *48 hours* +. The maintainers will review the report +. We may ask for additional information +. We will determine appropriate action +. We will inform you of the outcome (respecting others’ privacy) + +==== Confidentiality + +All reports will be handled with discretion: + +* Reporter identity is protected by default +* Details are shared only with those who need to know +* We will ask before naming you in any communication +* Anonymous reports are accepted and investigated + +==== Conflicts of Interest + +If a maintainers member is involved in an incident: + +* They will recuse themselves from the process +* Another maintainer or external party will handle the report +* We will disclose any potential conflicts + +''''' + +=== Enforcement Guidelines + +The maintainers will follow these guidelines in determining +consequences: + +==== 1. Correction + +*Community Impact*: Use of inappropriate language or other behaviour +deemed unprofessional or unwelcome. + +*Consequence*: A private, written warning providing clarity around the +nature of the violation and an explanation of why the behaviour was +inappropriate. A public apology may be requested. + +*Duration*: Immediate + +==== 2. Warning + +*Community Impact*: A violation through a single incident or series of +actions. + +*Consequence*: A warning with consequences for continued behaviour. No +interaction with the people involved, including unsolicited interaction +with those enforcing the Code of Conduct, for a specified period. This +includes avoiding interactions in community spaces as well as external +channels like social media. Violating these terms may lead to a +temporary or permanent ban. + +*Duration*: 1-4 weeks + +==== 3. Temporary Ban + +*Community Impact*: A serious violation of community standards, +including sustained inappropriate behaviour. + +*Consequence*: A temporary ban from any sort of interaction or public +communication with the community for a specified period. No public or +private interaction with the people involved, including unsolicited +interaction with those enforcing the Code of Conduct, is allowed during +this period. Violating these terms may lead to a permanent ban. + +*Duration*: 1-6 months + +==== 4. Permanent Ban + +*Community Impact*: Demonstrating a pattern of violation of community +standards, including sustained inappropriate behaviour, harassment of an +individual, or aggression toward or disparagement of classes of +individuals. + +*Consequence*: A permanent ban from any sort of public interaction +within the community. + +*Duration*: Permanent (with appeal rights after 12 months) + +==== Enforcement Across Perimeters + +For contributors with elevated access (Perimeter 2 or 1): + +[cols=",",options="header",] +|=== +|Level |Additional Consequence +|Correction |Noted in contributor record +|Warning |Access privileges may be temporarily reduced +|Temporary Ban |Access reduced to Perimeter 3 for ban duration +|Permanent Ban |All access revoked +|=== + +''''' + +=== Appeals + +If you believe an enforcement decision was made in error: + +[arabic] +. *Wait 7 days* after the decision (cooling-off period) +. *Email* j.d.a.jewell@open.ac.uk with subject line "`Appeal: [Original +Report ID]`" +. *Explain* why you believe the decision should be reconsidered +. *Provide* any new information not previously available + +*Appeals Process* + +* Appeals are reviewed by a different maintainers member than the +original +* You will receive a response within 14 days +* The appeals decision is final +* You may only appeal once per incident + +*Grounds for Appeal* + +* Procedural errors in the original investigation +* New evidence not previously available +* Disproportionate response to the violation +* Misunderstanding of facts + +''''' + +=== Supporting Those Who Report + +We are committed to supporting those who report violations: + +*We Will* - Believe and take all reports seriously - Respect your +privacy and confidentiality preferences - Keep you informed of progress +(if you wish) - Take steps to protect you from retaliation - Provide +resources if you need support + +*We Will Not* - Require you to confront the person directly - Dismiss +reports without investigation - Reveal your identity without consent - +Tolerate retaliation against reporters - Rush you to make decisions + +''''' + +=== Prevention + +Beyond enforcement, we actively work to prevent issues: + +*Onboarding* - All contributors are expected to read this Code of +Conduct - Perimeter 2 applicants must confirm they’ve read and +understood it - Maintainers receive additional training on enforcement + +*Culture* - We model the behaviour we expect - We intervene early when +we see potential issues - We thank people for positive contributions - +We create opportunities for diverse voices + +*Review* - This Code of Conduct is reviewed annually - Community +feedback is welcomed - Changes are communicated clearly + +''''' + +=== Acknowledgments + +This Code of Conduct is adapted from: + +* https://www.contributor-covenant.org/[Contributor Covenant], version +2.1 +* https://www.djangoproject.com/conduct/[Django Code of Conduct] +* https://www.rust-lang.org/policies/code-of-conduct[Rust Code of +Conduct] +* https://www.python.org/psf/conduct/[Python Community Code of Conduct] + +We thank these communities for their leadership in creating welcoming +spaces. + +''''' + +=== Questions? + +If you have questions about this Code of Conduct: + +* Open a +https://github.com/hyperpolymath/squisher-corpus/discussions[Discussion] +(for general questions) +* Email j.d.a.jewell@open.ac.uk (for private questions) +* Contact any maintainer directly + +''''' + +=== Summary + +*Be kind. Be respectful. Be collaborative.* + +We’re all here because we care about this project. Let’s make it a place +where everyone can do their best work. + +''''' + +Last updated: 2026 · Based on Contributor Covenant 2.1 diff --git a/CODE_OF_CONDUCT.md b/CODE_OF_CONDUCT.md deleted file mode 100644 index 8267cd4..0000000 --- a/CODE_OF_CONDUCT.md +++ /dev/null @@ -1,327 +0,0 @@ -# Code of Conduct - - - -## Our Pledge - -We as members, contributors, and leaders pledge to make participation in Squisher Corpus a harassment-free experience for everyone, regardless of age, body size, visible or invisible disability, ethnicity, sex characteristics, gender identity and expression, level of experience, education, socio-economic status, nationality, personal appearance, race, caste, colour, religion, or sexual identity and orientation. - -We pledge to act and interact in ways that contribute to an open, welcoming, diverse, inclusive, and healthy community. - -We recognise that a thriving open source community requires **psychological safety** — an environment where people can contribute, ask questions, make mistakes, and learn without fear of ridicule or retaliation. - ---- - -## Our Standards - -### Expected Behaviour - -The following behaviours contribute to a positive environment: - -**Communication** -- Using welcoming and inclusive language -- Being respectful of differing viewpoints and experiences -- Giving and gracefully accepting constructive feedback -- Assuming good intent while addressing impact -- Communicating clearly and patiently, especially with newcomers - -**Collaboration** -- Focusing on what is best for the community -- Showing empathy and kindness toward other community members -- Being collaborative rather than competitive -- Mentoring and supporting less experienced contributors -- Celebrating others' contributions and successes - -**Professionalism** -- Accepting responsibility and apologising to those affected by our mistakes -- Learning from the experience and avoiding repetition -- Respecting others' time and attention -- Staying on topic in project spaces -- Following project guidelines and conventions - -**Accessibility** -- Using plain language and avoiding unnecessary jargon -- Providing alt text for images and transcripts for audio/video -- Being patient with those using assistive technologies -- Accommodating different communication styles and needs -- Recognising that not everyone communicates the same way - -### Unacceptable Behaviour - -The following behaviours are considered harassment and are unacceptable: - -**Harassment** -- The use of sexualised language or imagery, and sexual attention or advances of any kind -- Trolling, insulting or derogatory comments, and personal or political attacks -- Public or private harassment -- Deliberate intimidation, stalking, or following (online or in-person) -- Unwelcome physical contact or simulated physical contact (e.g., emoji) -- Sustained disruption of talks, events, or online discussions - -**Discrimination** -- Discriminatory jokes and language -- Posting or threatening to post others' personally identifying information ("doxing") -- Advocating for, or encouraging, any of the above behaviour -- Microaggressions — subtle, often unintentional, discriminatory comments or actions - -**Professional Misconduct** -- Publishing others' private information without explicit permission -- Misrepresenting affiliation or contributions -- Plagiarism or claiming credit for others' work -- Retaliating against anyone who reports a Code of Conduct violation -- Other conduct which could reasonably be considered inappropriate in a professional setting - -### Grey Areas - -Some situations require judgement. When uncertain: - -- **Intent vs Impact**: Good intentions do not excuse harmful impact. Focus on making things right. -- **Power Dynamics**: Those with more power (maintainers, employers, experienced contributors) must be especially mindful of their impact. -- **Cultural Differences**: What's acceptable varies by culture. When in doubt, err on the side of caution and ask. -- **Humour**: Jokes at others' expense are rarely funny to everyone. Punch up, not down. - ---- - -## Scope - -This Code of Conduct applies within all community spaces, including: - -**Online Spaces** -- Repository discussions, issues, and pull/merge requests -- Project chat channels (Matrix, Discord, Slack, IRC) -- Mailing lists and forums -- Social media when representing the project -- Video calls and virtual meetings - -**In-Person Spaces** -- Conferences, meetups, and events -- Workshops and training sessions -- Any gathering where you represent the project - -**Representation** -This Code of Conduct also applies when an individual is officially representing the community in public spaces. Examples include: - -- Using an official project email address -- Posting via an official social media account -- Acting as an appointed representative at an event -- Speaking on behalf of the project - ---- - -## Enforcement - -### Reporting - -If you experience or witness unacceptable behaviour, or have any other concerns, please report it as soon as possible. - -**How to Report** - -| Method | Details | Best For | -|--------|---------|----------| -| **Email** | j.d.a.jewell@open.ac.uk | Detailed reports, sensitive matters | -| **Private Message** | Contact any maintainer directly | Quick questions, minor issues | -| **Anonymous Form** | [Link to form if available] | When you need anonymity | - -**What to Include** - -- Your contact information (unless anonymous) -- Names/usernames of those involved -- Description of what happened -- When and where it occurred -- Any witnesses -- Any supporting evidence (screenshots, links) -- How you would like us to respond (if you have a preference) - -**What Happens Next** - -1. You will receive acknowledgment within **48 hours** -2. The maintainers will review the report -3. We may ask for additional information -4. We will determine appropriate action -5. We will inform you of the outcome (respecting others' privacy) - -### Confidentiality - -All reports will be handled with discretion: - -- Reporter identity is protected by default -- Details are shared only with those who need to know -- We will ask before naming you in any communication -- Anonymous reports are accepted and investigated - -### Conflicts of Interest - -If a maintainers member is involved in an incident: - -- They will recuse themselves from the process -- Another maintainer or external party will handle the report -- We will disclose any potential conflicts - ---- - -## Enforcement Guidelines - -The maintainers will follow these guidelines in determining consequences: - -### 1. Correction - -**Community Impact**: Use of inappropriate language or other behaviour deemed unprofessional or unwelcome. - -**Consequence**: A private, written warning providing clarity around the nature of the violation and an explanation of why the behaviour was inappropriate. A public apology may be requested. - -**Duration**: Immediate - -### 2. Warning - -**Community Impact**: A violation through a single incident or series of actions. - -**Consequence**: A warning with consequences for continued behaviour. No interaction with the people involved, including unsolicited interaction with those enforcing the Code of Conduct, for a specified period. This includes avoiding interactions in community spaces as well as external channels like social media. Violating these terms may lead to a temporary or permanent ban. - -**Duration**: 1-4 weeks - -### 3. Temporary Ban - -**Community Impact**: A serious violation of community standards, including sustained inappropriate behaviour. - -**Consequence**: A temporary ban from any sort of interaction or public communication with the community for a specified period. No public or private interaction with the people involved, including unsolicited interaction with those enforcing the Code of Conduct, is allowed during this period. Violating these terms may lead to a permanent ban. - -**Duration**: 1-6 months - -### 4. Permanent Ban - -**Community Impact**: Demonstrating a pattern of violation of community standards, including sustained inappropriate behaviour, harassment of an individual, or aggression toward or disparagement of classes of individuals. - -**Consequence**: A permanent ban from any sort of public interaction within the community. - -**Duration**: Permanent (with appeal rights after 12 months) - -### Enforcement Across Perimeters - -For contributors with elevated access (Perimeter 2 or 1): - -| Level | Additional Consequence | -|-------|----------------------| -| Correction | Noted in contributor record | -| Warning | Access privileges may be temporarily reduced | -| Temporary Ban | Access reduced to Perimeter 3 for ban duration | -| Permanent Ban | All access revoked | - ---- - -## Appeals - -If you believe an enforcement decision was made in error: - -1. **Wait 7 days** after the decision (cooling-off period) -2. **Email** j.d.a.jewell@open.ac.uk with subject line "Appeal: [Original Report ID]" -3. **Explain** why you believe the decision should be reconsidered -4. **Provide** any new information not previously available - -**Appeals Process** - -- Appeals are reviewed by a different maintainers member than the original -- You will receive a response within 14 days -- The appeals decision is final -- You may only appeal once per incident - -**Grounds for Appeal** - -- Procedural errors in the original investigation -- New evidence not previously available -- Disproportionate response to the violation -- Misunderstanding of facts - ---- - -## Supporting Those Who Report - -We are committed to supporting those who report violations: - -**We Will** -- Believe and take all reports seriously -- Respect your privacy and confidentiality preferences -- Keep you informed of progress (if you wish) -- Take steps to protect you from retaliation -- Provide resources if you need support - -**We Will Not** -- Require you to confront the person directly -- Dismiss reports without investigation -- Reveal your identity without consent -- Tolerate retaliation against reporters -- Rush you to make decisions - ---- - -## Prevention - -Beyond enforcement, we actively work to prevent issues: - -**Onboarding** -- All contributors are expected to read this Code of Conduct -- Perimeter 2 applicants must confirm they've read and understood it -- Maintainers receive additional training on enforcement - -**Culture** -- We model the behaviour we expect -- We intervene early when we see potential issues -- We thank people for positive contributions -- We create opportunities for diverse voices - -**Review** -- This Code of Conduct is reviewed annually -- Community feedback is welcomed -- Changes are communicated clearly - ---- - -## Acknowledgments - -This Code of Conduct is adapted from: - -- [Contributor Covenant](https://www.contributor-covenant.org/), version 2.1 -- [Django Code of Conduct](https://www.djangoproject.com/conduct/) -- [Rust Code of Conduct](https://www.rust-lang.org/policies/code-of-conduct) -- [Python Community Code of Conduct](https://www.python.org/psf/conduct/) - -We thank these communities for their leadership in creating welcoming spaces. - ---- - -## Questions? - -If you have questions about this Code of Conduct: - -- Open a [Discussion](https://github.com/hyperpolymath/squisher-corpus/discussions) (for general questions) -- Email j.d.a.jewell@open.ac.uk (for private questions) -- Contact any maintainer directly - ---- - -## Summary - -**Be kind. Be respectful. Be collaborative.** - -We're all here because we care about this project. Let's make it a place where everyone can do their best work. - ---- - -Last updated: 2026 · Based on Contributor Covenant 2.1 diff --git a/CONTRIBUTING.adoc b/CONTRIBUTING.adoc new file mode 100644 index 0000000..5802f21 --- /dev/null +++ b/CONTRIBUTING.adoc @@ -0,0 +1,32 @@ +== Contributing to Invariant Path + +Thanks for your interest. This is a small, focused MVP maintained by one +person; contributions that keep it small are the most welcome kind. + +=== Getting started + +[source,bash] +---- +cargo build --workspace +cargo test --workspace +---- + +No external services or toolchains are needed for the core; the +AffineScript `+faces+` examples and the Agda proof are optional extras +that degrade to SKIP when their toolchains are absent. + +=== What’s useful + +* Bug reports with a minimal input text and the annotation you expected +* New extraction triggers or classifier heuristics, *with tests* (see +`+crates/invariant-path-core/src/lib.rs+` for the test style) and an +entry in `+docs/EXTENDING.md+` +* Precision/recall evaluation corpora — the biggest known gap + +=== Ground rules + +* Code is MPL-2.0, docs are CC-BY-SA-4.0; keep SPDX headers on new files +* `+#![forbid(unsafe_code)]+` stays +* `+cargo test --workspace+` must pass; `+cargo fmt+` before committing +* Heuristics favour false negatives over noise (see `+DESIGN.md+`) — a +change that makes the tool chattier needs a strong justification diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md deleted file mode 100644 index 1298d9b..0000000 --- a/CONTRIBUTING.md +++ /dev/null @@ -1,36 +0,0 @@ - - -# Contributing to Invariant Path - -Thanks for your interest. This is a small, focused MVP maintained by one -person; contributions that keep it small are the most welcome kind. - -## Getting started - -```bash -cargo build --workspace -cargo test --workspace -``` - -No external services or toolchains are needed for the core; the AffineScript -`faces` examples and the Agda proof are optional extras that degrade to SKIP -when their toolchains are absent. - -## What's useful - -- Bug reports with a minimal input text and the annotation you expected -- New extraction triggers or classifier heuristics, **with tests** (see - `crates/invariant-path-core/src/lib.rs` for the test style) and an entry in - `docs/EXTENDING.md` -- Precision/recall evaluation corpora — the biggest known gap - -## Ground rules - -- Code is MPL-2.0, docs are CC-BY-SA-4.0; keep SPDX headers on new files -- `#![forbid(unsafe_code)]` stays -- `cargo test --workspace` must pass; `cargo fmt` before committing -- Heuristics favour false negatives over noise (see `DESIGN.md`) — a change - that makes the tool chattier needs a strong justification diff --git a/DESIGN.adoc b/DESIGN.adoc new file mode 100644 index 0000000..ac17e69 --- /dev/null +++ b/DESIGN.adoc @@ -0,0 +1,97 @@ +== Invariant Path MVP Design Log + +=== 2026-04-10 — Initial Placement + +* Decision: build a standalone monorepo-style workspace at +`+/var/mnt/eclipse/repos/invariant-path+`. +* Tradeoff: wrappers in `+echidna+`, `+panll+`, and `+hypatia+` call the +shared CLI instead of duplicating logic. +* Reasoning: this keeps heuristics inspectable and consistent while +still enabling repo-specific usage patterns. + +=== 2026-04-10 — Heuristic Philosophy + +* Decision: favor strict trigger-based extraction with explicit +transition markers. +* Tradeoff: we intentionally accept false negatives to reduce annotation +noise. +* Reasoning: contributors can always add/edit annotations manually; +noisy auto-suggestions hurt trust. + +=== 2026-04-10 — Storage Model + +* Decision: use append-friendly JSONL (`+annotations.jsonl+`) with +upsert-on-write semantics. +* Tradeoff: not ideal for very large datasets, but easy to inspect and +diff in git. +* Reasoning: MVP prioritizes transparency and editability over +throughput. + +=== 2026-04-10 — Profile Injection via Wrappers + +* Decision: each target repo (`+echidna+`, `+panll+`, `+hypatia+`) gets +a tiny shell wrapper that injects a default `+--profile+` for `+scan+`. +* Tradeoff: wrappers rely on local path `+../invariant-path+` and +`+cargo run+`, not a globally installed binary. +* Reasoning: fastest path to real usage across multiple repos while +preserving one shared implementation. + +=== 2026-04-10 — Status Semantics in CLI + +* Decision: map core UX actions directly to commands: `+accept+`, +`+dismiss+`, `+clarify+`, `+add+`, `+update+`, plus `+overlay toggle+`. +* Tradeoff: no rich side panel UI in MVP; interaction is CLI-first with +JSON output. +* Reasoning: preserves complete editability and auditability while +keeping implementation small. + +=== 2026-04-10 — Desktop and Start Menu Integration + +* Decision: add a shared launcher at +`+/var/mnt/eclipse/repos/.desktop-tools/invariant-path-launcher.sh+` +plus an install script that writes `+.desktop+` entries to start menu +and desktop locations. +* Tradeoff: launcher defaults to CLI-friendly `+Terminal=true+` because +Invariant Path is currently a CLI-first tool. +* Reasoning: satisfies immediate usability from Start Menu, desktop, and +repo-root without introducing an incomplete GUI overlay. + +=== 2026-04-10 — Repo-Root Invocation Standard + +* Decision: expose `+invariant-path+` entry points in each integrated +repo through `+scripts/invariant-path.sh+` and +`+just invariant-path ...+`. +* Tradeoff: requires shared workspace path `+../invariant-path+` to +exist. +* Reasoning: keeps behavior consistent across repos while preserving a +single source of truth for extractor/classifier logic. + +=== 2026-04-10 — Desktop Installer Idempotence + +* Decision: make `+scripts/install-desktop.sh+` remove a destination +`+.desktop+` file if it exists but is not writable, then reinstall with +deterministic modes (`+444+` in app menu, `+555+` on Desktop/Shortcuts). +* Tradeoff: replacement is explicit rather than in-place update, but +content and permissions remain deterministic from template + destination +policy. +* Reasoning: GNU `+install+` can fail on existing read-only targets; +KDE/Plasma desktop launchers also need execute bits to avoid launch +aborts. + +=== 2026-06-18 — Faces same-cube profile (`+faces+`) + +* Decision: add a `+faces+` profile (`+profiles/faces.md+`), a same-cube +corpus (`+examples/same-cube/+`), and a verifier +(`+scripts/verify-same-cube.sh+`) that grounds the AffineScript +"`different faces, same cube`" invariant — every face’s `+preview-*+` +lowering must normalise to the same canonical text. +* Tradeoff: v1 compares normalised canonical _text_, not ASTs, and SKIPs +when no `+affinescript+` binary is reachable (grounding happens in CI). +It can’t yet catch two different canonical texts that typecheck to the +same cube. +* Reasoning: per-face snapshot tests (`+affinescript/tests/faces/+`) +catch drift _within_ a face but never compare face A’s cube against face +B’s. The cross-face equality is the load-bearing claim; this profile is +the claim-path debugger that locates which face breaks it. Doc-profile +shape (markdown + script), so no change to the Rust core or CLI — +consistent with the `+pmpl+` / `+standards-docs+` profiles. diff --git a/DESIGN.md b/DESIGN.md deleted file mode 100644 index 674e20d..0000000 --- a/DESIGN.md +++ /dev/null @@ -1,55 +0,0 @@ -# Invariant Path MVP Design Log - -## 2026-04-10 — Initial Placement - -- Decision: build a standalone monorepo-style workspace at `/var/mnt/eclipse/repos/invariant-path`. -- Tradeoff: wrappers in `echidna`, `panll`, and `hypatia` call the shared CLI instead of duplicating logic. -- Reasoning: this keeps heuristics inspectable and consistent while still enabling repo-specific usage patterns. - -## 2026-04-10 — Heuristic Philosophy - -- Decision: favor strict trigger-based extraction with explicit transition markers. -- Tradeoff: we intentionally accept false negatives to reduce annotation noise. -- Reasoning: contributors can always add/edit annotations manually; noisy auto-suggestions hurt trust. - -## 2026-04-10 — Storage Model - -- Decision: use append-friendly JSONL (`annotations.jsonl`) with upsert-on-write semantics. -- Tradeoff: not ideal for very large datasets, but easy to inspect and diff in git. -- Reasoning: MVP prioritizes transparency and editability over throughput. - -## 2026-04-10 — Profile Injection via Wrappers - -- Decision: each target repo (`echidna`, `panll`, `hypatia`) gets a tiny shell wrapper that injects a default `--profile` for `scan`. -- Tradeoff: wrappers rely on local path `../invariant-path` and `cargo run`, not a globally installed binary. -- Reasoning: fastest path to real usage across multiple repos while preserving one shared implementation. - -## 2026-04-10 — Status Semantics in CLI - -- Decision: map core UX actions directly to commands: `accept`, `dismiss`, `clarify`, `add`, `update`, plus `overlay toggle`. -- Tradeoff: no rich side panel UI in MVP; interaction is CLI-first with JSON output. -- Reasoning: preserves complete editability and auditability while keeping implementation small. - -## 2026-04-10 — Desktop and Start Menu Integration - -- Decision: add a shared launcher at `/var/mnt/eclipse/repos/.desktop-tools/invariant-path-launcher.sh` plus an install script that writes `.desktop` entries to start menu and desktop locations. -- Tradeoff: launcher defaults to CLI-friendly `Terminal=true` because Invariant Path is currently a CLI-first tool. -- Reasoning: satisfies immediate usability from Start Menu, desktop, and repo-root without introducing an incomplete GUI overlay. - -## 2026-04-10 — Repo-Root Invocation Standard - -- Decision: expose `invariant-path` entry points in each integrated repo through `scripts/invariant-path.sh` and `just invariant-path ...`. -- Tradeoff: requires shared workspace path `../invariant-path` to exist. -- Reasoning: keeps behavior consistent across repos while preserving a single source of truth for extractor/classifier logic. - -## 2026-04-10 — Desktop Installer Idempotence - -- Decision: make `scripts/install-desktop.sh` remove a destination `.desktop` file if it exists but is not writable, then reinstall with deterministic modes (`444` in app menu, `555` on Desktop/Shortcuts). -- Tradeoff: replacement is explicit rather than in-place update, but content and permissions remain deterministic from template + destination policy. -- Reasoning: GNU `install` can fail on existing read-only targets; KDE/Plasma desktop launchers also need execute bits to avoid launch aborts. - -## 2026-06-18 — Faces same-cube profile (`faces`) - -- Decision: add a `faces` profile (`profiles/faces.md`), a same-cube corpus (`examples/same-cube/`), and a verifier (`scripts/verify-same-cube.sh`) that grounds the AffineScript "different faces, same cube" invariant — every face's `preview-*` lowering must normalise to the same canonical text. -- Tradeoff: v1 compares normalised canonical *text*, not ASTs, and SKIPs when no `affinescript` binary is reachable (grounding happens in CI). It can't yet catch two different canonical texts that typecheck to the same cube. -- Reasoning: per-face snapshot tests (`affinescript/tests/faces/`) catch drift *within* a face but never compare face A's cube against face B's. The cross-face equality is the load-bearing claim; this profile is the claim-path debugger that locates which face breaks it. Doc-profile shape (markdown + script), so no change to the Rust core or CLI — consistent with the `pmpl` / `standards-docs` profiles. diff --git a/GOVERNANCE.adoc b/GOVERNANCE.adoc new file mode 100644 index 0000000..9b836fb --- /dev/null +++ b/GOVERNANCE.adoc @@ -0,0 +1,60 @@ +== Governance + +=== Overview + +This project is governed by the following principles and structures to +ensure transparent, inclusive, and effective decision-making. + +=== Roles and Responsibilities + +==== Maintainers + +Maintainers are responsible for: - Reviewing and merging pull requests - +Managing releases and versioning - Ensuring code quality and standards - +Triaging issues and bug reports - Community engagement and support + +==== Contributors + +Contributors are expected to: - Follow the code of conduct - Submit +well-documented pull requests - Write tests for new functionality - +Maintain existing tests - Update documentation as needed + +=== Decision Making + +==== Minor Changes + +* Can be made by any maintainer +* Include bug fixes, documentation updates, dependency updates + +==== Major Changes + +* Require discussion in issues or pull requests +* Include new features, architectural changes, API changes +* Need approval from at least 2 maintainers + +==== Breaking Changes + +* Require RFC (Request for Comments) process +* Need approval from majority of maintainers +* Must include migration guide + +=== Code of Conduct + +All participants are expected to follow our Code of Conduct. Violations +can be reported to the maintainers. + +=== Communication + +* *Issues*: For bug reports and feature requests +* *Discussions*: For questions and general discussion +* *Pull Requests*: For code contributions + +=== Licensing + +All contributions are made under the terms of the repository’s LICENSE +file. By submitting a pull request, you agree to license your +contributions accordingly. + +''''' + +_Last updated: 2026-07-18_ diff --git a/GOVERNANCE.md b/GOVERNANCE.md deleted file mode 100644 index e27364c..0000000 --- a/GOVERNANCE.md +++ /dev/null @@ -1,60 +0,0 @@ -# Governance - -## Overview - -This project is governed by the following principles and structures to ensure transparent, inclusive, and effective decision-making. - -## Roles and Responsibilities - -### Maintainers - -Maintainers are responsible for: -- Reviewing and merging pull requests -- Managing releases and versioning -- Ensuring code quality and standards -- Triaging issues and bug reports -- Community engagement and support - -### Contributors - -Contributors are expected to: -- Follow the code of conduct -- Submit well-documented pull requests -- Write tests for new functionality -- Maintain existing tests -- Update documentation as needed - -## Decision Making - -### Minor Changes -- Can be made by any maintainer -- Include bug fixes, documentation updates, dependency updates - -### Major Changes -- Require discussion in issues or pull requests -- Include new features, architectural changes, API changes -- Need approval from at least 2 maintainers - -### Breaking Changes -- Require RFC (Request for Comments) process -- Need approval from majority of maintainers -- Must include migration guide - -## Code of Conduct - -All participants are expected to follow our Code of Conduct. Violations can be reported to the maintainers. - -## Communication - -- **Issues**: For bug reports and feature requests -- **Discussions**: For questions and general discussion -- **Pull Requests**: For code contributions - -## Licensing - -All contributions are made under the terms of the repository's LICENSE file. -By submitting a pull request, you agree to license your contributions accordingly. - ---- - -*Last updated: 2026-07-18* diff --git a/README.adoc b/README.adoc new file mode 100644 index 0000000..f5230a0 --- /dev/null +++ b/README.adoc @@ -0,0 +1,191 @@ +https://www.bestpractices.dev/en/projects/new?repo_url=https://github.com/hyperpolymath/invariant-path[image:https://img.shields.io/badge/OpenSSF-Best_Practices-green?logo=opensourcesecurity[OpenSSF +Best Practices]] +link:LICENSE[image:https://img.shields.io/badge/License-MPL--2.0-blue.svg[License: +MPL-2.0]] + +== Invariant Path + +*Invariant Path traces what a claim _means_ when it crosses from one +domain into another — and finds the crossings where the meaning quietly +changed.* + +It is a claim-path debugger, not a truth engine. It does not decide +whether a claim is true. It shows you the path a claim took, and where +along that path it stopped meaning what it meant at the start. + +=== The idea + +A claim is asserted in some domain. It is then re-expressed in another — +a specification lowered into code, a licence text asserting facts about +its own file tree, a source language emitted through several backends, a +proof obligation discharged in a different logic. + +Two things can be true at once: + +* the claim holds on *both* sides of the transition, and +* it does *not mean the same thing* on both sides. + +That second case is the one this tool exists for. Nothing on the surface +signals it: both sides pass their own checks, both look green, and the +divergence is invisible precisely because each side is internally +consistent. The invariant is not "`the claim is true here and true +there`" — it is *"`the claim is the _same claim_ here and there.`"* That +is the path, and the path is what has to be invariant. + +==== The failure is silent, which is why it needs tooling + +Per-domain tests are the wrong instrument by construction. A test inside +domain A checks A against itself; a test inside domain B checks B +against itself. Neither can see that A’s claim and B’s claim have +drifted apart, because *cross-domain equality is not expressible from +inside either domain.* Every individual test can pass forever while the +thing you actually care about is already broken. + +==== The worked example: "`different faces, same cube`" + +AffineScript presents several _faces_ — surface syntaxes — that all +lower to one canonical form. Per-face snapshot tests catch drift +_within_ a face and never compare face A’s cube against face B’s. *The +cross-face equality is the load-bearing claim*, and no per-face test can +state it. + +Invariant Path grounds that claim: each face is compiled to typed-wasm +and the modules are compared by `+sha256+`, so the faces must land in +*one wasm equivalence class*. The wasm _is_ the cube, which makes this a +far stronger bar than matching canonical text. When a face falls outside +the class, a normalised text diff is printed to locate _where_ — as a +diagnostic, not as the check itself. + +This is one worked example, not the subject of the repository. See +`+profiles/faces.md+` for its limits, including the two classes the +`+greet+` corpus genuinely splits into. + +=== The three-layer claim checker + +Invariant Path is the *governance front-end* for a layered checker. Each +layer answers a question the others cannot: + +[width="100%",cols="34%,33%,33%",options="header",] +|=== +|Layer |Name |Question +|1 |*type* |Is this admissible _on form alone_? Well-formedness, +through-line, and a forward-only ordering on evidence — "`the diode`". + +|2 |*trope* |Does this particular evidence survive the leap to this +conclusion _for this use_? Purpose-indexed warrant. + +|3 |*sortal* |Are these two presentations _the same argument_? Identity, +and therefore counting. +|=== + +Layer 3 was ruled on in +link:docs/decisions/0001-the-sortal-layer.adoc[ADR-0001] after a +five-count case against it was built deliberately and three of the five +counts broke. Its killer case is the *doubling attack*: one derivation +presented twice, paraphrased, under distinct labels is invisible to +every Layer 1 and Layer 2 check — identical pass/fail on every +subdiagram — while corroboration weight is two instead of one. That is +why Layer 3 runs _before_ Layer 2: identity must be settled before +resource accounting, or Layer 2 double-counts. + +*These layers are decided, not built.* The ADR is a decision record. +What ships today is the extractor, classifier and annotation store +described below. Open architectural gaps are tracked in +link:docs/DEBT.md[`+docs/DEBT.md+`]. + +=== Its dual: 007 and hermeneutic semantics + +Invariant Path and the hermeneutic-semantics work in `+007+` are two +halves of one concern, and each is the other’s mirror: + +[width="100%",cols="25%,25%,25%,25%",options="header",] +|=== +| |Syntax |Semantics |The silent failure +|*Invariant Path* |*different* |must be *the same* |forms diverge in +meaning while each stays self-consistent + +|*007 / hermeneutic* |*the same* |may be *read differently* |one form +silently carries two readings, and the wrong one is assumed +|=== + +_Many forms, one meaning_ against _one form, many meanings_. Both fail +the same way — silently, because the surface text carries no signal of +the divergence. If you are working on one, read the other; a fix in +either that ignores the dual will be incomplete. + +=== What a profile is + +A *profile* is a lens this tool applies to a corpus that lives +*somewhere else*. It names a target corpus by path, states the claim +being traced, and supplies whatever verifier grounds it. + +*A profile does not vendor the corpus it examines.* See +`+profiles/pmpl.md+` for the intended shape: it points at the +palimpsest-license tree and copies nothing. A profile that carries a +copy of its target will drift from the real thing and quietly start +grounding a claim about a stale fixture — which is this tool’s own +failure mode, turned inward. + +== Workspace Layout + +* `+crates/invariant-path-core+` — extractor, classifier, schema models, +and annotation storage API +* `+crates/invariant-path-cli+` — CLI/TUI-adjacent interface for scan + +annotation editing +* `+schemas/annotation.schema.json+` — JSON schema for persisted +annotations +* `+docs/ARCHITECTURE.md+` — minimal architecture proposal +* `+docs/EXTENDING.md+` — extension guide for invariant types and +heuristics +* `+examples/+` — seeded examples. NOTE: `+examples/same-cube/+` +currently vendors an AffineScript corpus, which contradicts the profile +rule above; see the open issue to point it at the real tree instead. +* `+profiles/+` — profile notes for `+echidna+`, `+panll+`, `+hypatia+`, +`+pmpl+`, `+standards-docs+`, and `+faces+` (AffineScript "`different +faces, same cube`" — pending rename to `+affinescript+`, matching the +others, which are named for their target corpus rather than for one +claim inside it) +* `+scripts/verify-same-cube.sh+` — grounds the faces same-cube +invariant (see `+profiles/faces.md+`) + +== Quick Start + +[source,bash] +---- +cargo run -p invariant-path-cli -- scan --file ./README.md --artifact-uri repo://README.md --json +---- + +[source,bash] +---- +cargo run -p invariant-path-cli -- annotations list --json +---- + +[source,bash] +---- +cargo run -p invariant-path-cli -- doc-claims scan --file ./README.md --json +---- + +== CLI Surface + +The CLI currently provides five subcommands: + +* `+scan+` — extract and classify claim transitions from a file +* `+annotations+` — list/add/update/accept/dismiss/clarify persisted +annotations +* `+overlay+` — toggle overlay state +* `+profiles+` — list built-in scan profiles (`+generic+`, `+echidna+`, +`+panll+`, `+hypatia+`) +* `+doc-claims+` — ground factual doc claims (file paths, command +hygiene) against the filesystem + +There is no interactive TUI yet; all interaction is CLI-first with +`+--json+` output. + +== Launcher Integration (maintainer machine only) + +The `+./invariant-path+` and `+./invariant-path-launcher+` wrappers, the +desktop template (`+desktop/invariant-path.desktop+`), and +`+scripts/install-desktop.sh+` delegate to a launcher script that lives +outside this repository (`+/var/mnt/eclipse/repos/.desktop-tools/+`). On +any other machine they print a clear message and exit; use +`+cargo run -p invariant-path-cli+` directly instead. diff --git a/README.md b/README.md deleted file mode 100644 index c266541..0000000 --- a/README.md +++ /dev/null @@ -1,177 +0,0 @@ - - -[![OpenSSF Best Practices](https://img.shields.io/badge/OpenSSF-Best_Practices-green?logo=opensourcesecurity)](https://www.bestpractices.dev/en/projects/new?repo_url=https://github.com/hyperpolymath/invariant-path) -[![License: MPL-2.0](https://img.shields.io/badge/License-MPL--2.0-blue.svg)](LICENSE) - -# Invariant Path - -**Invariant Path traces what a claim *means* when it crosses from one domain -into another — and finds the crossings where the meaning quietly changed.** - -It is a claim-path debugger, not a truth engine. It does not decide whether a -claim is true. It shows you the path a claim took, and where along that path it -stopped meaning what it meant at the start. - -## The idea - -A claim is asserted in some domain. It is then re-expressed in another — a -specification lowered into code, a licence text asserting facts about its own -file tree, a source language emitted through several backends, a proof -obligation discharged in a different logic. - -Two things can be true at once: - -* the claim holds on **both** sides of the transition, and -* it does **not mean the same thing** on both sides. - -That second case is the one this tool exists for. Nothing on the surface -signals it: both sides pass their own checks, both look green, and the -divergence is invisible precisely because each side is internally consistent. -The invariant is not "the claim is true here and true there" — it is -**"the claim is the *same claim* here and there."** That is the path, and the -path is what has to be invariant. - -### The failure is silent, which is why it needs tooling - -Per-domain tests are the wrong instrument by construction. A test inside domain -A checks A against itself; a test inside domain B checks B against itself. -Neither can see that A's claim and B's claim have drifted apart, because -**cross-domain equality is not expressible from inside either domain.** Every -individual test can pass forever while the thing you actually care about is -already broken. - -### The worked example: "different faces, same cube" - -AffineScript presents several *faces* — surface syntaxes — that all lower to -one canonical form. Per-face snapshot tests catch drift *within* a face and -never compare face A's cube against face B's. **The cross-face equality is the -load-bearing claim**, and no per-face test can state it. - -Invariant Path grounds that claim: each face is compiled to typed-wasm and the -modules are compared by `sha256`, so the faces must land in **one wasm -equivalence class**. The wasm *is* the cube, which makes this a far stronger -bar than matching canonical text. When a face falls outside the class, a -normalised text diff is printed to locate *where* — as a diagnostic, not as the -check itself. - -This is one worked example, not the subject of the repository. See -`profiles/faces.md` for its limits, including the two classes the `greet` -corpus genuinely splits into. - -## The three-layer claim checker - -Invariant Path is the **governance front-end** for a layered checker. Each -layer answers a question the others cannot: - -| Layer | Name | Question | -|---|---|---| -| 1 | **type** | Is this admissible *on form alone*? Well-formedness, through-line, and a forward-only ordering on evidence — "the diode". | -| 2 | **trope** | Does this particular evidence survive the leap to this conclusion *for this use*? Purpose-indexed warrant. | -| 3 | **sortal** | Are these two presentations *the same argument*? Identity, and therefore counting. | - -Layer 3 was ruled on in -[ADR-0001](docs/decisions/0001-the-sortal-layer.adoc) after a five-count case -against it was built deliberately and three of the five counts broke. Its -killer case is the **doubling attack**: one derivation presented twice, -paraphrased, under distinct labels is invisible to every Layer 1 and Layer 2 -check — identical pass/fail on every subdiagram — while corroboration weight is -two instead of one. That is why Layer 3 runs *before* Layer 2: identity must be -settled before resource accounting, or Layer 2 double-counts. - -**These layers are decided, not built.** The ADR is a decision record. What -ships today is the extractor, classifier and annotation store described below. -Open architectural gaps are tracked in [`docs/DEBT.md`](docs/DEBT.md). - -## Its dual: 007 and hermeneutic semantics - -Invariant Path and the hermeneutic-semantics work in `007` are two halves of one -concern, and each is the other's mirror: - -| | Syntax | Semantics | The silent failure | -|---|---|---|---| -| **Invariant Path** | **different** | must be **the same** | forms diverge in meaning while each stays self-consistent | -| **007 / hermeneutic** | **the same** | may be **read differently** | one form silently carries two readings, and the wrong one is assumed | - -*Many forms, one meaning* against *one form, many meanings*. Both fail the same -way — silently, because the surface text carries no signal of the divergence. -If you are working on one, read the other; a fix in either that ignores the -dual will be incomplete. - -## What a profile is - -A **profile** is a lens this tool applies to a corpus that lives **somewhere -else**. It names a target corpus by path, states the claim being traced, and -supplies whatever verifier grounds it. - -**A profile does not vendor the corpus it examines.** See `profiles/pmpl.md` -for the intended shape: it points at the palimpsest-license tree and copies -nothing. A profile that carries a copy of its target will drift from the real -thing and quietly start grounding a claim about a stale fixture — which is this -tool's own failure mode, turned inward. - -# Workspace Layout - -- `crates/invariant-path-core` — extractor, classifier, schema models, - and annotation storage API - -- `crates/invariant-path-cli` — CLI/TUI-adjacent interface for scan + - annotation editing - -- `schemas/annotation.schema.json` — JSON schema for persisted - annotations - -- `docs/ARCHITECTURE.md` — minimal architecture proposal - -- `docs/EXTENDING.md` — extension guide for invariant types and - heuristics - -- `examples/` — seeded examples. NOTE: `examples/same-cube/` currently - vendors an AffineScript corpus, which contradicts the profile rule - above; see the open issue to point it at the real tree instead. - -- `profiles/` — profile notes for `echidna`, `panll`, `hypatia`, `pmpl`, - `standards-docs`, and `faces` (AffineScript "different faces, same - cube" — pending rename to `affinescript`, matching the others, which - are named for their target corpus rather than for one claim inside it) - -- `scripts/verify-same-cube.sh` — grounds the faces same-cube invariant - (see `profiles/faces.md`) - -# Quick Start - -```bash -cargo run -p invariant-path-cli -- scan --file ./README.md --artifact-uri repo://README.md --json -``` - -```bash -cargo run -p invariant-path-cli -- annotations list --json -``` - -```bash -cargo run -p invariant-path-cli -- doc-claims scan --file ./README.md --json -``` - -# CLI Surface - -The CLI currently provides five subcommands: - -- `scan` — extract and classify claim transitions from a file -- `annotations` — list/add/update/accept/dismiss/clarify persisted annotations -- `overlay` — toggle overlay state -- `profiles` — list built-in scan profiles (`generic`, `echidna`, `panll`, `hypatia`) -- `doc-claims` — ground factual doc claims (file paths, command hygiene) against the filesystem - -There is no interactive TUI yet; all interaction is CLI-first with `--json` output. - -# Launcher Integration (maintainer machine only) - -The `./invariant-path` and `./invariant-path-launcher` wrappers, the desktop -template (`desktop/invariant-path.desktop`), and `scripts/install-desktop.sh` -delegate to a launcher script that lives outside this repository -(`/var/mnt/eclipse/repos/.desktop-tools/`). On any other machine they print a -clear message and exit; use `cargo run -p invariant-path-cli` directly instead. diff --git a/SECURITY.adoc b/SECURITY.adoc new file mode 100644 index 0000000..8ef6ba6 --- /dev/null +++ b/SECURITY.adoc @@ -0,0 +1,22 @@ +== Security Policy + +=== Reporting a vulnerability + +Email j.d.a.jewell@open.ac.uk with a description and reproduction steps. +Please do not open public issues for security reports. You should +receive an acknowledgement within 14 days. + +=== Scope + +Invariant Path is a local CLI that reads files you point it at and +writes JSONL annotations under the working directory. It makes no +network calls. The most security-relevant surfaces are: + +* Path handling in `+doc-claims+` grounding +(`+crates/invariant-path-core/src/doc_claims.rs+`) +* JSONL parsing in the annotation store +(`+crates/invariant-path-core/src/annotations.rs+`) + +=== Supported versions + +Only the latest release on `+main+` is supported. diff --git a/SECURITY.md b/SECURITY.md deleted file mode 100644 index e611e0c..0000000 --- a/SECURITY.md +++ /dev/null @@ -1,25 +0,0 @@ - - -# Security Policy - -## Reporting a vulnerability - -Email with a description and reproduction steps. -Please do not open public issues for security reports. You should receive an -acknowledgement within 14 days. - -## Scope - -Invariant Path is a local CLI that reads files you point it at and writes -JSONL annotations under the working directory. It makes no network calls. -The most security-relevant surfaces are: - -- Path handling in `doc-claims` grounding (`crates/invariant-path-core/src/doc_claims.rs`) -- JSONL parsing in the annotation store (`crates/invariant-path-core/src/annotations.rs`) - -## Supported versions - -Only the latest release on `main` is supported. diff --git a/docs/ARCHITECTURE.adoc b/docs/ARCHITECTURE.adoc new file mode 100644 index 0000000..828b6e5 --- /dev/null +++ b/docs/ARCHITECTURE.adoc @@ -0,0 +1,44 @@ +== Minimal Architecture Proposal + +Invariant Path is split into four inspectable modules: + +[arabic] +. `+extractor+` + +* Input: repository artifact text. +* Output: candidate claim transitions anchored by trigger phrases and +spans. + +[arabic, start=2] +. `+classifier+` + +* Input: extracted candidate transition. +* Output: invariant type, preserved/losses, break condition, and +classification enum. + +[arabic, start=3] +. `+annotations+` + +* Input: machine suggestions and manual edits. +* Output: persisted overlay records with visibility and status controls. + +[arabic, start=4] +. `+ui+` (CLI first) + +* Input: user command intents (`+scan+`, `+accept+`, `+dismiss+`, +`+clarify+`, `+add+`, `+update+`). +* Output: JSON/human-readable overlays; optional persisted suggestions. + +=== Data Flow + +`+artifact text -> extractor -> classifier -> suggestion annotations -> user edits -> stored overlay+` + +=== Integration Strategy + +* Shared core workspace: `+invariant-path+`. +* Repo wrappers: +** `+echidna/scripts/invariant-path.sh+` +** `+panll/scripts/invariant-path.sh+` +** `+hypatia/scripts/invariant-path.sh+` +* Profiles allow domain-specific defaults without changing core +extraction/classification logic. diff --git a/docs/ARCHITECTURE.md b/docs/ARCHITECTURE.md deleted file mode 100644 index 3e8c62d..0000000 --- a/docs/ARCHITECTURE.md +++ /dev/null @@ -1,32 +0,0 @@ -# Minimal Architecture Proposal - -Invariant Path is split into four inspectable modules: - -1. `extractor` -- Input: repository artifact text. -- Output: candidate claim transitions anchored by trigger phrases and spans. - -2. `classifier` -- Input: extracted candidate transition. -- Output: invariant type, preserved/losses, break condition, and classification enum. - -3. `annotations` -- Input: machine suggestions and manual edits. -- Output: persisted overlay records with visibility and status controls. - -4. `ui` (CLI first) -- Input: user command intents (`scan`, `accept`, `dismiss`, `clarify`, `add`, `update`). -- Output: JSON/human-readable overlays; optional persisted suggestions. - -## Data Flow - -`artifact text -> extractor -> classifier -> suggestion annotations -> user edits -> stored overlay` - -## Integration Strategy - -- Shared core workspace: `invariant-path`. -- Repo wrappers: - - `echidna/scripts/invariant-path.sh` - - `panll/scripts/invariant-path.sh` - - `hypatia/scripts/invariant-path.sh` -- Profiles allow domain-specific defaults without changing core extraction/classification logic. diff --git a/docs/DEBT.adoc b/docs/DEBT.adoc new file mode 100644 index 0000000..d2ce1f2 --- /dev/null +++ b/docs/DEBT.adoc @@ -0,0 +1,329 @@ +== Debt register — invariant-path + +*Audited 2026-08-05* by reading the tree and querying the GitHub API. +This is the _live_ register: findings stay until closed, and each +carries the evidence that would prove it fixed. + +Supersedes `+docs/tech-debt-2026-05-26.md+`, whose "`RESOLVED`" banner +overstates the proof item — see link:#p1[P1]. + +[cols=",,,",options="header",] +|=== +| |Dimension |Open |Worst +|A |Architecture — the three layers |3 |*HIGH* +|C |CI/CD |3 |MEDIUM +|L |Licence |2 |MEDIUM +|D |Docs |3 |MEDIUM +|P |Proof |2 |MEDIUM +|K |Code |1 |LOW +|=== + +''''' + +=== Architecture debt + +This is where the substantial work is, and where the substantial gaps +are. ADR-0001 settled Layer 3’s charter and name; it did not build +anything, and it was explicit about what remains. + +### A1 — Layer 1 has no substrate anywhere. `+HIGH+` + +A survey of `+_TYPES _SET+` and `+_PROVER-SOLVER _SET+` (recorded in +ADR-0001) found *no syntax of claims, premises, steps or evidence in any +repository*, and *no ordering on evidence events of any kind*. All three +sub-layers — well-formedness, continuity, temporality — must be built +from scratch. + +Two names promise otherwise and do not deliver: `+choreographic-types+` +has never contained a line of source on any branch, and typell’s "`Level +9 Temporal safety`" passes iff a named field is present, examining no +event and no order. + +*Closed when:* a claim syntax and an evidence-event ordering exist, with +the diode enforced on the latter. + +==== A2 — Layer 3’s equivalence side does not exist. `+HIGH+` + +`+echo-types+` supplies roughly a quarter of the layer, and only the +_obstruction_ half: the fibre `+Echo f y = Σ A (λ x → f x ≡ y)+`, an +invariant separating two members of one fibre, and "`identified members +count once`". + +There is *no move relation, no quotient, and no normal form anywhere* — +which is the entire equivalence-certificate side. And the one piece most +needed is `+echo-types+`’ own unclosed debt: propositional truncation is +_postulated_ under `+--safe+` and constructed only in a `+--cubical+` +island that Agda’s flag rules forbid the main cone from importing. +"`Merely inhabited versus how many witnesses`" is exactly what the +doubling attack turns on. + +Two candidate substrates were investigated and *refuted with evidence* — +QuandleDB and absolute-zero’s CNO — so this is not a matter of wiring +something up. Do not reopen either without new evidence; both +refutations are in ADR-0001. + +*Recorded ruling:* mechanise in *Agda `+--cubical+`*, not Idris 2. The +core construction is a quotient by admissible moves, and Idris 2’s QTT +cannot host quotients or higher inductive types. + +*Closed when:* a move relation and a quotient exist, and an equivalence +certificate can be produced and checked for a worked pair. + +==== A3 — Layer 2’s vocabulary does not match its implementation. `+MEDIUM+` + +The terms in circulation — strength, consistency, coherence, +resemblance-warrant-on-merge, p-residue, p-sufficiency — are not the +terms in code. Only *p-sufficiency* is real (`+floor(U) ⊑ acc(v)+`). +*`+p-residue+` does not exist in any repository in the estate.* + +What is built (`+trope-checker+`) is a six-coordinate `+Grade+`, nine +`+p-*+` effects, a `+Floor+`, and a witness-carrying `+Verdict+`. + +This matters beyond tidiness: part of the ADR-0001 argument read +p-residue as affine resource accounting — a term that could not be +grounded — so the reachability result should be re-derived against the +actual grade algebra. +`+trope-particularity-workbench/tests/check-vocabulary.sh+` hard-fails +on any vocabulary entry outside the nine effects, so introducing these +terms as if established would break a live gate. + +Left deliberately unreconciled in ADR-0001 rather than quietly +harmonised. + +*Closed when:* a ruling records whether the six terms are a new Layer 2 +design superseding the grade algebra, an informal gloss of it, or drift. + +''''' + +=== CI/CD debt + +==== C1 — The lockfile epidemic is CURED. `+RESOLVED 2026-08-05+` + +Until 2026-08-05 there was no Actions lockfile, and *every* workflow +terminated as `+startup_failure+` before a single step ran, on every +branch. `+main+` had never been green, which made every other gate +decorative. + +Fixed by PR #56, which adopted `+.github/workflows/actions.lock+`. +Re-measured on `+main+` the same day — latest run per workflow: + +.... +GREEN (10) Code Quality · CodeQL Security Analysis · Governance · + Guix/Nix Package Policy · Hypatia Security Scan · + RSR Anti-Pattern Check · Runtime Policy · Rust CI · + Secret Scanner · Security Policy +.... + +The gates are now real: Rust CI, CodeQL and Secret Scanner actually +execute and can actually fail. Three residual items remain, tracked +below. + +____ +*Diagnosis trap, retained because it will recur.* `+gh pr checks+` shows +_nothing wrong_ for a parse-rejected workflow — it emits no check run at +all, so a PR looks unchecked rather than broken. Use +`+gh run list --branch +`; a `+?status=failure+` query also +*excludes* `+startup_failure+`. +____ + +==== C2 — OSSF Scorecard still fails to start. `+MEDIUM+` + +The one workflow the lockfile fix did not reach: `+OSSF Scorecard+` is +still `+startup_failure+` on `+main+`, so it has never produced a +result. PR #59 proposes making it periodic rather than per-push, which +may or may not address the startup cause — the two are independent. + +*Closed when:* Scorecard produces a conclusion other than +`+startup_failure+`. + +____ +PR #59 proposes dropping Scorecard’s `+push+` trigger so it runs on a +schedule only. That is right on signal-discipline grounds — Scorecard +measures the _repository’s_ posture, not the change under review — but +it does *not* fix this finding: a scheduled run will still fail to start +for whatever the underlying cause is. It changes when the failure is +visible, not whether it happens. +____ + +==== C3 — Two workflows fail on content. `+MEDIUM+` + +Genuine failures, not startup problems — which means they are now doing +their job and reporting something real: + +* `+Well-Known Standards (RFC 9116 + RSR)+` +* `+Workflow Security Linter+` + +Both were invisible until the lockfile landed, because neither could +start. Neither has been triaged. + +*Closed when:* each either passes or has its finding recorded here as +accepted. + +==== C4 — No proof gate. `+MEDIUM+` + +No workflow invokes Agda, and none runs `+scripts/verify-same-cube.sh+`. +The CI half of link:#p1[P1] and link:#p2[P2]. Unaffected by the lockfile +fix. + +*Closed when:* a workflow compiles `+proofs/SameCube.agda+` and runs the +verifier, and both can fail the build. + +''''' + +=== Licence debt + +==== L1 — GitHub reported *no licence* for this repository. `+RESOLVED+` + +`+gh repo view --json licenseInfo+` returns `+null+`, despite a 373-line +MPL-2.0 `+LICENSE+` at the root and `+license = "MPL-2.0"+` in +`+Cargo.toml+`. The repository shows as unlicensed to anyone browsing it +and to tooling reading the API. + +Cause: `+LICENSE+` deviates from canonical MPL-2.0 in two places — a +*trailing space* at line 38, and `+http://+` rather than `+https://+` at +line 360. `+LICENSES/MPL-2.0.txt+` is the clean copy. + +*RESOLVED 2026-08-05.* `+LICENSE+` was replaced with the canonical text +and the change merged to `+main+`; detection recomputed and now reports: + +.... +$ gh api repos/hyperpolymath/invariant-path/license --jq '{name:.license.spdx_id, path:.path}' +{"name":"MPL-2.0","path":"LICENSE"} +.... + +Note for anyone re-testing this: detection *lags the push*. An immediate +`+gh repo view --json licenseInfo+` still returned `+null+` and only +cleared after a pause — long enough to look like the fix had failed. +Re-check before concluding. + +==== L2 — SPDX headers are not on line 1. `+MEDIUM+` + +Twelve of thirteen root-level documents open with `+ - -# Debt register — invariant-path - -**Audited 2026-08-05** by reading the tree and querying the GitHub API. This is -the *live* register: findings stay until closed, and each carries the evidence -that would prove it fixed. - -Supersedes `docs/tech-debt-2026-05-26.md`, whose "RESOLVED" banner overstates -the proof item — see [P1](#p1). - -| | Dimension | Open | Worst | -|---|---|---|---| -| A | Architecture — the three layers | 3 | **HIGH** | -| C | CI/CD | 3 | MEDIUM | -| L | Licence | 2 | MEDIUM | -| D | Docs | 3 | MEDIUM | -| P | Proof | 2 | MEDIUM | -| K | Code | 1 | LOW | - ---- - -## Architecture debt - -This is where the substantial work is, and where the substantial gaps are. -ADR-0001 settled Layer 3's charter and name; it did not build anything, and it -was explicit about what remains. - - -### A1 — Layer 1 has no substrate anywhere. `HIGH` - -A survey of `_TYPES _SET` and `_PROVER-SOLVER _SET` (recorded in ADR-0001) -found **no syntax of claims, premises, steps or evidence in any repository**, -and **no ordering on evidence events of any kind**. All three sub-layers — -well-formedness, continuity, temporality — must be built from scratch. - -Two names promise otherwise and do not deliver: `choreographic-types` has never -contained a line of source on any branch, and typell's "Level 9 Temporal -safety" passes iff a named field is present, examining no event and no order. - -**Closed when:** a claim syntax and an evidence-event ordering exist, with the -diode enforced on the latter. - -### A2 — Layer 3's equivalence side does not exist. `HIGH` - -`echo-types` supplies roughly a quarter of the layer, and only the -*obstruction* half: the fibre `Echo f y = Σ A (λ x → f x ≡ y)`, an invariant -separating two members of one fibre, and "identified members count once". - -There is **no move relation, no quotient, and no normal form anywhere** — which -is the entire equivalence-certificate side. And the one piece most needed is -`echo-types`' own unclosed debt: propositional truncation is *postulated* under -`--safe` and constructed only in a `--cubical` island that Agda's flag rules -forbid the main cone from importing. "Merely inhabited versus how many -witnesses" is exactly what the doubling attack turns on. - -Two candidate substrates were investigated and **refuted with evidence** — -QuandleDB and absolute-zero's CNO — so this is not a matter of wiring something -up. Do not reopen either without new evidence; both refutations are in -ADR-0001. - -**Recorded ruling:** mechanise in **Agda `--cubical`**, not Idris 2. The core -construction is a quotient by admissible moves, and Idris 2's QTT cannot host -quotients or higher inductive types. - -**Closed when:** a move relation and a quotient exist, and an equivalence -certificate can be produced and checked for a worked pair. - -### A3 — Layer 2's vocabulary does not match its implementation. `MEDIUM` - -The terms in circulation — strength, consistency, coherence, -resemblance-warrant-on-merge, p-residue, p-sufficiency — are not the terms in -code. Only **p-sufficiency** is real (`floor(U) ⊑ acc(v)`). **`p-residue` does -not exist in any repository in the estate.** - -What is built (`trope-checker`) is a six-coordinate `Grade`, nine `p-*` -effects, a `Floor`, and a witness-carrying `Verdict`. - -This matters beyond tidiness: part of the ADR-0001 argument read p-residue as -affine resource accounting — a term that could not be grounded — so the -reachability result should be re-derived against the actual grade algebra. -`trope-particularity-workbench/tests/check-vocabulary.sh` hard-fails on any -vocabulary entry outside the nine effects, so introducing these terms as if -established would break a live gate. - -Left deliberately unreconciled in ADR-0001 rather than quietly harmonised. - -**Closed when:** a ruling records whether the six terms are a new Layer 2 -design superseding the grade algebra, an informal gloss of it, or drift. - ---- - -## CI/CD debt - -### C1 — The lockfile epidemic is CURED. `RESOLVED 2026-08-05` - -Until 2026-08-05 there was no Actions lockfile, and **every** workflow -terminated as `startup_failure` before a single step ran, on every branch. -`main` had never been green, which made every other gate decorative. - -Fixed by PR #56, which adopted `.github/workflows/actions.lock`. Re-measured on -`main` the same day — latest run per workflow: - -``` -GREEN (10) Code Quality · CodeQL Security Analysis · Governance · - Guix/Nix Package Policy · Hypatia Security Scan · - RSR Anti-Pattern Check · Runtime Policy · Rust CI · - Secret Scanner · Security Policy -``` - -The gates are now real: Rust CI, CodeQL and Secret Scanner actually execute and -can actually fail. Three residual items remain, tracked below. - -> **Diagnosis trap, retained because it will recur.** `gh pr checks` shows -> *nothing wrong* for a parse-rejected workflow — it emits no check run at all, -> so a PR looks unchecked rather than broken. Use `gh run list --branch `; -> a `?status=failure` query also **excludes** `startup_failure`. - -### C2 — OSSF Scorecard still fails to start. `MEDIUM` - -The one workflow the lockfile fix did not reach: `OSSF Scorecard` is still -`startup_failure` on `main`, so it has never produced a result. PR #59 proposes -making it periodic rather than per-push, which may or may not address the -startup cause — the two are independent. - -**Closed when:** Scorecard produces a conclusion other than `startup_failure`. - -> PR #59 proposes dropping Scorecard's `push` trigger so it runs on a schedule -> only. That is right on signal-discipline grounds — Scorecard measures the -> *repository's* posture, not the change under review — but it does **not** fix -> this finding: a scheduled run will still fail to start for whatever the -> underlying cause is. It changes when the failure is visible, not whether it -> happens. - -### C3 — Two workflows fail on content. `MEDIUM` - -Genuine failures, not startup problems — which means they are now doing their -job and reporting something real: - -- `Well-Known Standards (RFC 9116 + RSR)` -- `Workflow Security Linter` - -Both were invisible until the lockfile landed, because neither could start. -Neither has been triaged. - -**Closed when:** each either passes or has its finding recorded here as -accepted. - -### C4 — No proof gate. `MEDIUM` - -No workflow invokes Agda, and none runs `scripts/verify-same-cube.sh`. The CI -half of [P1](#p1) and [P2](#p2). Unaffected by the lockfile fix. - -**Closed when:** a workflow compiles `proofs/SameCube.agda` and runs the -verifier, and both can fail the build. - ---- - -## Licence debt - -### L1 — GitHub reported **no licence** for this repository. `RESOLVED` - -`gh repo view --json licenseInfo` returns `null`, despite a 373-line MPL-2.0 -`LICENSE` at the root and `license = "MPL-2.0"` in `Cargo.toml`. The repository -shows as unlicensed to anyone browsing it and to tooling reading the API. - -Cause: `LICENSE` deviates from canonical MPL-2.0 in two places — a **trailing -space** at line 38, and `http://` rather than `https://` at line 360. -`LICENSES/MPL-2.0.txt` is the clean copy. - -**RESOLVED 2026-08-05.** `LICENSE` was replaced with the canonical text and the -change merged to `main`; detection recomputed and now reports: - -``` -$ gh api repos/hyperpolymath/invariant-path/license --jq '{name:.license.spdx_id, path:.path}' -{"name":"MPL-2.0","path":"LICENSE"} -``` - -Note for anyone re-testing this: detection **lags the push**. An immediate -`gh repo view --json licenseInfo` still returned `null` and only cleared after -a pause — long enough to look like the fix had failed. Re-check before -concluding. - -### L2 — SPDX headers are not on line 1. `MEDIUM` - -Twelve of thirteen root-level documents open with ` - - -# Invariant Path × echo-types — structured loss as a first-class object - -Invariant Path is the **application example** of the -[`echo-types`](https://github.com/hyperpolymath/echo-types) programme: it is a -runtime that *keeps echoes instead of discarding them*. - -## The correspondence - -echo-types formalises **fiber-based structured loss**. For a function -`f : A → B`, the *echo* of an output `y` is the fiber - -``` -Echo f y := Σ (x : A) , (f x ≡ y) -``` - -— the proof-relevant record of **which** inputs `f` collapsed onto `y`. A -non-injective `f` *forgets* that "which"; the echo is exactly what you must -retain to recover it. - -Invariant Path's classifier is such an `f`: - -```rust -classify_candidate : ClaimCandidate -> ClassificationOutcome -``` - -Many distinct claim-paths collapse to the same `Classification` -(`ValidPath | Overextended | Conflation | Incomplete | Abstain`). The bare -classification is the lossy codomain value; **the claim-path is the echo**. - -| echo-types | Invariant Path | -|---------------------------|--------------------------------------------------| -| `f : A → B` (lossy map) | `classify_candidate` (claim-path → classification) | -| codomain value `y` | `Classification` | -| `Echo f y` (the fiber) | the retained `ClaimCandidate` + `ClassificationOutcome` | -| residue / structured loss | `ClassificationOutcome.losses : Vec` | -| no-section (irreversible) | a `Classification` alone cannot recover its path | -| the section that recovers | `Annotation.path_description` (retained provenance) | - -The domain model already names the loss: `ClassificationOutcome` carries -`losses` and `preserved` precisely because a classification that *dropped* the -path would be untraceable. echo-types is the mechanised backbone of that design -choice — Invariant Path is "a claim-path debugger, not a truth engine" exactly -because it stores echoes. - -## Worked example (runnable + tested) - -```bash -cargo run -p invariant-path-core --example echo_structured_loss -cargo test -p invariant-path-core --test echo_structured_loss -``` - -Two genuinely different claim-paths — -`benchmark accuracy ⟶ general capability` and -`the theorem proves ⟶ production guarantee` — both classify as `Overextended`, -yet retain **distinct** structured losses (`task_transfer` vs -`implementation_gap`). The classifier is non-injective; the echo keeps what it -drops. See: - -- `crates/invariant-path-core/examples/echo_structured_loss.rs` -- `crates/invariant-path-core/tests/echo_structured_loss.rs` - -## Cross-repo - -The same `Echo` underlies the type-system integration across the estate, all -machine-checked under `--safe --without-K`: - -- **nextgen-typing** — `verification/proofs/agda/EchoTyping.agda`: affine - subtyping *is* echo `weaken`; refinement erasure *is* a fiber. -- **nextgen-languages / kitchenspeak** — `proofs/agda/EchoBridge.agda`: the `@` - sensor witness *is* `Echo (fired …) true`. -- **phronesis** — `academic/formal-verification/agda/PhronesisEcho.agda`: an - ethical verdict's provenance *is* `Echo verdict v`. - -Invariant Path is where that theory is *used*: a tool whose reason to exist is -to retain the echo. diff --git a/docs/EXTENDING.adoc b/docs/EXTENDING.adoc new file mode 100644 index 0000000..554a81a --- /dev/null +++ b/docs/EXTENDING.adoc @@ -0,0 +1,41 @@ +== Extending Invariant Path + +=== Add a New Invariant Type + +[arabic] +. Edit `+crates/invariant-path-core/src/model.rs+` and add the enum +variant to `+InvariantType+`. +. Update `+infer_invariant_type+` in +`+crates/invariant-path-core/src/classifier.rs+` with keyword rules. +. Add test cases in `+crates/invariant-path-core/src/lib.rs+` tests. +. If persistence schema should enforce it, update +`+schemas/annotation.schema.json+` enum. + +=== Add or Tune Heuristics + +[arabic] +. Edit trigger phrases in +`+crates/invariant-path-core/src/extractor.rs+`. +. Edit high-value jump maps in +`+crates/invariant-path-core/src/classifier.rs+`. +. Keep heuristics explicit and local; avoid hidden statistical/ML +behavior in MVP. +. Add/adjust tests for both positive and negative examples. + +=== Profile-Specific Behavior + +Profiles are currently selected by CLI flag +(`+--profile echidna|panll|hypatia+`). + +To add one: + +[arabic] +. Update `+ProfilePreset+` in `+crates/invariant-path-cli/src/main.rs+`. +. Add default artifact globs and visibility policy. +. Add a smoke test scenario in `+examples/+`. + +=== Design Constraints + +* Every automatic judgment must remain user-editable. +* Favor false negatives over noisy false positives. +* Keep storage inspectable and git-friendly. diff --git a/docs/EXTENDING.md b/docs/EXTENDING.md deleted file mode 100644 index c924b5e..0000000 --- a/docs/EXTENDING.md +++ /dev/null @@ -1,31 +0,0 @@ -# Extending Invariant Path - -## Add a New Invariant Type - -1. Edit `crates/invariant-path-core/src/model.rs` and add the enum variant to `InvariantType`. -2. Update `infer_invariant_type` in `crates/invariant-path-core/src/classifier.rs` with keyword rules. -3. Add test cases in `crates/invariant-path-core/src/lib.rs` tests. -4. If persistence schema should enforce it, update `schemas/annotation.schema.json` enum. - -## Add or Tune Heuristics - -1. Edit trigger phrases in `crates/invariant-path-core/src/extractor.rs`. -2. Edit high-value jump maps in `crates/invariant-path-core/src/classifier.rs`. -3. Keep heuristics explicit and local; avoid hidden statistical/ML behavior in MVP. -4. Add/adjust tests for both positive and negative examples. - -## Profile-Specific Behavior - -Profiles are currently selected by CLI flag (`--profile echidna|panll|hypatia`). - -To add one: - -1. Update `ProfilePreset` in `crates/invariant-path-cli/src/main.rs`. -2. Add default artifact globs and visibility policy. -3. Add a smoke test scenario in `examples/`. - -## Design Constraints - -- Every automatic judgment must remain user-editable. -- Favor false negatives over noisy false positives. -- Keep storage inspectable and git-friendly. diff --git a/docs/reports/audit/audit-2026-04-15-post.adoc b/docs/reports/audit/audit-2026-04-15-post.adoc new file mode 100644 index 0000000..e9e4045 --- /dev/null +++ b/docs/reports/audit/audit-2026-04-15-post.adoc @@ -0,0 +1,25 @@ +== Post-audit Status Report: invariant-path + +* *Date:* 2026-04-15 +* *Status:* Complete (M5 Sweep) +* *Repo:* /var/mnt/eclipse/repos/invariant-path + +=== Actions Taken + +[arabic] +. Standard CI/Workflow Sweep: Added blocker workflows +(`+ts-blocker.yml+`, `+npm-bun-blocker.yml+`) and updated `+Justfile+`. +. SCM-to-A2ML Migration: Staged and committed deletions of legacy +`+.scm+` files. +. Lockfile Sweep: Generated and tracked missing lockfiles where +manifests were present. +. Static Analysis: Verified with `+panic-attack assail+`. + +=== Findings Summary + +* 8 unwrap/expect calls in crates/invariant-path-core/src/lib.rs +* 19 unwrap/expect calls in crates/invariant-path-core/src/doc_claims.rs + +=== Final Grade + +* *CRG Grade:* D (Promoted from E/X) - CI and lockfiles are in place. diff --git a/docs/reports/audit/audit-2026-04-15-post.md b/docs/reports/audit/audit-2026-04-15-post.md deleted file mode 100644 index 970d8bd..0000000 --- a/docs/reports/audit/audit-2026-04-15-post.md +++ /dev/null @@ -1,17 +0,0 @@ -# Post-audit Status Report: invariant-path -- **Date:** 2026-04-15 -- **Status:** Complete (M5 Sweep) -- **Repo:** /var/mnt/eclipse/repos/invariant-path - -## Actions Taken -1. Standard CI/Workflow Sweep: Added blocker workflows (`ts-blocker.yml`, `npm-bun-blocker.yml`) and updated `Justfile`. -2. SCM-to-A2ML Migration: Staged and committed deletions of legacy `.scm` files. -3. Lockfile Sweep: Generated and tracked missing lockfiles where manifests were present. -4. Static Analysis: Verified with `panic-attack assail`. - -## Findings Summary -- 8 unwrap/expect calls in crates/invariant-path-core/src/lib.rs -- 19 unwrap/expect calls in crates/invariant-path-core/src/doc_claims.rs - -## Final Grade -- **CRG Grade:** D (Promoted from E/X) - CI and lockfiles are in place. diff --git a/docs/reports/audit/audit-2026-04-15-pre.adoc b/docs/reports/audit/audit-2026-04-15-pre.adoc new file mode 100644 index 0000000..bbc607e --- /dev/null +++ b/docs/reports/audit/audit-2026-04-15-pre.adoc @@ -0,0 +1,22 @@ +== Pre-audit Status Report: invariant-path + +* *Date:* 2026-04-15 +* *Status:* In-progress (M5 Sweep) +* *Repo:* `+/var/mnt/eclipse/repos/invariant-path+` + +=== Current State Assessment + +* *Lockfiles:* `+Cargo.lock+` is present. +* *Workflows:* `+.github/workflows+` is missing. +* *Git status:* Clean, but no remotes found. + +=== Identified Gaps + +[arabic] +. Missing `+.github/workflows+`. +. No git remotes configured (potential issue for CI/CD synchronization). + +=== Initial Safety Check + +* *Secrets:* No secrets detected. +* *Panics:* To be verified via `+panic-attack assail+`. diff --git a/docs/reports/audit/audit-2026-04-15-pre.md b/docs/reports/audit/audit-2026-04-15-pre.md deleted file mode 100644 index bfd8f88..0000000 --- a/docs/reports/audit/audit-2026-04-15-pre.md +++ /dev/null @@ -1,17 +0,0 @@ -# Pre-audit Status Report: invariant-path -- **Date:** 2026-04-15 -- **Status:** In-progress (M5 Sweep) -- **Repo:** `/var/mnt/eclipse/repos/invariant-path` - -## Current State Assessment -- **Lockfiles:** `Cargo.lock` is present. -- **Workflows:** `.github/workflows` is missing. -- **Git status:** Clean, but no remotes found. - -## Identified Gaps -1. Missing `.github/workflows`. -2. No git remotes configured (potential issue for CI/CD synchronization). - -## Initial Safety Check -- **Secrets:** No secrets detected. -- **Panics:** To be verified via `panic-attack assail`. diff --git a/docs/tech-debt-2026-05-26.adoc b/docs/tech-debt-2026-05-26.adoc new file mode 100644 index 0000000..9b2ade1 --- /dev/null +++ b/docs/tech-debt-2026-05-26.adoc @@ -0,0 +1,95 @@ +== Tech-Debt Audit — invariant-path — 2026-05-26 + +____ +*SUPERSEDED — 2026-08-05 by link:DEBT.md[`+DEBT.md+`].* Kept for audit +history. + +The 2026-07-02 "`RESOLVED`" banner was *partly wrong* and is corrected +here: + +* _Licence_ — `+LICENSE+` existed, but deviated from canonical MPL-2.0 +by a trailing space and one `+http+`/`+https+`, and *GitHub reported no +licence at all* until 2026-08-05. Now fixed; see `+DEBT.md+` L1. +* _Proof_ — `+proofs/SameCube.agda+` exists and is good work, but *no +workflow compiles it*, so the proof is ungated: it would not go red if +it broke. Existing is not being checked. Proof debt was half closed, not +closed; see `+DEBT.md+` P1. +* _Changelog_ — accurate, `+CHANGELOG.md+` does exist. + +Do not action this file. Work from `+DEBT.md+`. +____ + +*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:* `+CRITICAL+`. + +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 + +No proof-bearing files (`+*.v+`, `+*.lean+`, `+*.agda+`, `+*.idr+`, +`+*.idr2+`, `+*.fst+`, `+*.dfy+`, `+*.tla+`, `+*.ads+`, `+*.adb+`) found +in this repo. + +*Recommended next move:* none. + +=== 2. Licence debt + +[cols=",",options="header",] +|=== +|Field |Value +|LICENSE file |`+NONE+` +|SPDX header |`+NONE+` +|Manifest licence |`+MPL-2.0+` +|Body classifier |`+UNKNOWN+` +|Severity |`+CRITICAL+` +|Notes |`+no-LICENSE-file+` +|=== + +*Recommended next move:* add a `+LICENSE+` file at the repo root. Estate +default is `+MPL-2.0+` (see +`+hyperpolymath/standards/.github/LICENSE.template+`). If this repo is +intentionally proprietary, add a single-line `+LICENSE+` saying so (no +SPDX identifier exists; use a `+LicenseRef-+` prefix in any manifest). + +=== 3. Documentation debt + +[cols=",",options="header",] +|=== +|Field |Value +|README lines |79 +|`+docs/+` files |4 +|`+docs/+` LoC |97 +|CHANGELOG.md |N +|CONTRIBUTING.md |N +|CODE_OF_CONDUCT.md |N +|SECURITY.md |N +|Severity |`+MEDIUM+` +|=== + +*Recommended next move:* introduce a `+docs/+` directory. The README at +79 lines has likely grown to do the work of `+docs/+` — split it into a +thin README + `+docs/architecture.md+`, `+docs/usage.md+`, etc. +Heavy-wiki exemplars to copy from: `+affinescript+`, `+boj-server+`, +`+echidna+`, `+hypatia+`. + +Additionally: *CHANGELOG.md is missing.* 65% of estate repos lack one — +adopting a CHANGELOG (or auto-generating via `+git-cliff+`) is a +recommended estate-wide follow-up. + +=== 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 1308257..0000000 --- a/docs/tech-debt-2026-05-26.md +++ /dev/null @@ -1,73 +0,0 @@ - - -# Tech-Debt Audit — invariant-path — 2026-05-26 - -> **SUPERSEDED — 2026-08-05 by [`DEBT.md`](DEBT.md).** Kept for audit history. -> -> The 2026-07-02 "RESOLVED" banner was **partly wrong** and is corrected here: -> -> * *Licence* — `LICENSE` existed, but deviated from canonical MPL-2.0 by a -> trailing space and one `http`/`https`, and **GitHub reported no licence at -> all** until 2026-08-05. Now fixed; see `DEBT.md` L1. -> * *Proof* — `proofs/SameCube.agda` exists and is good work, but **no workflow -> compiles it**, so the proof is ungated: it would not go red if it broke. -> Existing is not being checked. Proof debt was half closed, not closed; see -> `DEBT.md` P1. -> * *Changelog* — accurate, `CHANGELOG.md` does exist. -> -> Do not action this file. Work from `DEBT.md`. - -**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:** `CRITICAL`. - -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 - -No proof-bearing files (`*.v`, `*.lean`, `*.agda`, `*.idr`, `*.idr2`, `*.fst`, `*.dfy`, `*.tla`, `*.ads`, `*.adb`) found in this repo. - -**Recommended next move:** none. - -## 2. Licence debt - -| Field | Value | -|---|---| -| LICENSE file | `NONE` | -| SPDX header | `NONE` | -| Manifest licence | `MPL-2.0` | -| Body classifier | `UNKNOWN` | -| Severity | `CRITICAL` | -| Notes | `no-LICENSE-file` | - -**Recommended next move:** add a `LICENSE` file at the repo root. Estate default is `MPL-2.0` (see `hyperpolymath/standards/.github/LICENSE.template`). If this repo is intentionally proprietary, add a single-line `LICENSE` saying so (no SPDX identifier exists; use a `LicenseRef-` prefix in any manifest). - -## 3. Documentation debt - -| Field | Value | -|---|---| -| README lines | 79 | -| `docs/` files | 4 | -| `docs/` LoC | 97 | -| CHANGELOG.md | N | -| CONTRIBUTING.md | N | -| CODE_OF_CONDUCT.md | N | -| SECURITY.md | N | -| Severity | `MEDIUM` | - -**Recommended next move:** introduce a `docs/` directory. The README at 79 lines has likely grown to do the work of `docs/` — split it into a thin README + `docs/architecture.md`, `docs/usage.md`, etc. Heavy-wiki exemplars to copy from: `affinescript`, `boj-server`, `echidna`, `hypatia`. - -Additionally: **CHANGELOG.md is missing.** 65% of estate repos lack one — adopting a CHANGELOG (or auto-generating via `git-cliff`) is a recommended estate-wide follow-up. - -## 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/examples/same-cube/README.adoc b/examples/same-cube/README.adoc new file mode 100644 index 0000000..a30c99c --- /dev/null +++ b/examples/same-cube/README.adoc @@ -0,0 +1,76 @@ +== Same-cube corpus + +Each subdirectory here is *one program written in every AffineScript +face*. The files are deliberately the _same_ program (identical strings, +identical structure) — not the demonstrative, different-string examples +in `+affinescript/examples/faces/+`. That is the whole point: if they +are the same program, every face should lower to the *same cube*. + +.... +greet/ + canonical.affine face: canonical (the reference cube) + rattle.affine face: rattlescript -> preview-python + jaffa.affine face: jaffascript -> preview-js + pseudo.affine face: pseudoscript -> preview-pseudocode + lucid.affine face: lucidscript -> preview-lucid + cafe.affine face: cafescripto -> preview-cafe +.... + +=== Ground the invariant + +[source,sh] +---- +scripts/verify-same-cube.sh examples/same-cube/greet \ + --out .machine_readable/audits/same-cube.jsonl +---- + +The verifier detects each file’s face from its `+face:+` pragma, +*compiles it to typed-wasm* (`+compile --face +`), and +sha256-compares the modules — the wasm _is_ the cube, so byte-identical +wasm is the rigorous bar. For any face outside the canonical class it +also prints the `+preview-*+` text diff as a diagnostic of _where_ the +lowering diverges. Output is a per-face table, the wasm equivalence +classes, and invariant-path claim records (`+Grounded+` / +`+Ungrounded+`). Needs an `+affinescript+` binary (PATH, +`+--affinescript+`, `+AFFINESCRIPT+`, or `+../affinescript/_build+`); +without one it SKIPs. + +This is a *claim-path debugger*, not a rubber stamp: a `+DIFF+` is the +tool locating which face leaves the cube and showing exactly where. + +=== Grounded result — `+greet+` (2026-06-18, affinescript @ main) + +Run against a freshly-built compiler, the six faces compile to *two* +distinct wasm modules: + +[cols=",",options="header",] +|=== +|wasm class |faces +|`+56c454be…+` |canonical, *jaffa*, *cafe* +|`+2ff63dd1…+` |*rattle*, *pseudo*, *lucid* +|=== + +The split is *not* a transformer crash — all six compile, type-check, +and print the same string. It is a real, characterised divergence in +_lowering style_: rattle/pseudo/lucid render the trailing call as a +*tail expression* (`+fn main() … { println(x) }+`), while +canonical/jaffa/cafe keep it as a *statement* (`+{ println(x); }+`). For +`+println : … -> ()+` both return unit, so the programs are +*observationally identical* — but the emitted wasm is not +byte-identical. + +So _"`different faces, same cube`"_ is true *observationally* but *false +at the byte-wasm level* for this corpus: the face transformers do not +currently agree on trailing-statement lowering. Tracked as an +affinescript transformer- consistency item. (lucid additionally emits a +`+module Greet;+` decl and drops the `+-{IO}->+` annotation in its +preview text; neither changes the wasm class.) + +=== Adding a program + +Add a sibling directory (e.g. `+counter/+`) with one file per face, each +carrying the right `+face:+` pragma and encoding the identical program. +Keep to surface features the transformers handle today (see the "`Known +transformer gaps`" table in +`+affinescript/examples/faces/README.adoc+`); divergences show up as +extra wasm classes — useful signal, not noise. diff --git a/examples/same-cube/README.md b/examples/same-cube/README.md deleted file mode 100644 index e3cf846..0000000 --- a/examples/same-cube/README.md +++ /dev/null @@ -1,70 +0,0 @@ - - -# Same-cube corpus - -Each subdirectory here is **one program written in every AffineScript face**. -The files are deliberately the *same* program (identical strings, identical -structure) — not the demonstrative, different-string examples in -`affinescript/examples/faces/`. That is the whole point: if they are the same -program, every face should lower to the **same cube**. - -``` -greet/ - canonical.affine face: canonical (the reference cube) - rattle.affine face: rattlescript -> preview-python - jaffa.affine face: jaffascript -> preview-js - pseudo.affine face: pseudoscript -> preview-pseudocode - lucid.affine face: lucidscript -> preview-lucid - cafe.affine face: cafescripto -> preview-cafe -``` - -## Ground the invariant - -```sh -scripts/verify-same-cube.sh examples/same-cube/greet \ - --out .machine_readable/audits/same-cube.jsonl -``` - -The verifier detects each file's face from its `face:` pragma, **compiles it to -typed-wasm** (`compile --face `), and sha256-compares the modules — the -wasm *is* the cube, so byte-identical wasm is the rigorous bar. For any face -outside the canonical class it also prints the `preview-*` text diff as a -diagnostic of *where* the lowering diverges. Output is a per-face table, the -wasm equivalence classes, and invariant-path claim records (`Grounded` / -`Ungrounded`). Needs an `affinescript` binary (PATH, `--affinescript`, -`AFFINESCRIPT`, or `../affinescript/_build`); without one it SKIPs. - -This is a **claim-path debugger**, not a rubber stamp: a `DIFF` is the tool -locating which face leaves the cube and showing exactly where. - -## Grounded result — `greet` (2026-06-18, affinescript @ main) - -Run against a freshly-built compiler, the six faces compile to **two** distinct -wasm modules: - -| wasm class | faces | -|---|---| -| `56c454be…` | canonical, **jaffa**, **cafe** | -| `2ff63dd1…` | **rattle**, **pseudo**, **lucid** | - -The split is **not** a transformer crash — all six compile, type-check, and -print the same string. It is a real, characterised divergence in *lowering -style*: rattle/pseudo/lucid render the trailing call as a **tail expression** -(`fn main() … { println(x) }`), while canonical/jaffa/cafe keep it as a -**statement** (`{ println(x); }`). For `println : … -> ()` both return unit, so -the programs are **observationally identical** — but the emitted wasm is not -byte-identical. - -So *"different faces, same cube"* is true **observationally** but **false at the -byte-wasm level** for this corpus: the face transformers do not currently agree -on trailing-statement lowering. Tracked as an affinescript transformer- -consistency item. (lucid additionally emits a `module Greet;` decl and drops -the `-{IO}->` annotation in its preview text; neither changes the wasm class.) - -## Adding a program - -Add a sibling directory (e.g. `counter/`) with one file per face, each carrying -the right `face:` pragma and encoding the identical program. Keep to surface -features the transformers handle today (see the "Known transformer gaps" table -in `affinescript/examples/faces/README.adoc`); divergences show up as extra -wasm classes — useful signal, not noise. diff --git a/examples/seed_examples.adoc b/examples/seed_examples.adoc new file mode 100644 index 0000000..0b39d7b --- /dev/null +++ b/examples/seed_examples.adoc @@ -0,0 +1,14 @@ +== Seed Examples + +[arabic] +. This benchmark proves the model can reason. +. This theorem guarantees production safety. +. This cost reduction means transition is easy. +. This model result shows all workers are motivated by incentives. +. This uncertainty means we should delay action. +. Under assumptions, the local result implies all deployments are safe. +. The pilot data implies we should change policy immediately. +. The proof implies the corollary in the same formal system. +. In practice, this benchmark suggests gains but does not guarantee +real-world performance. +. Clearly, this single test means every environment is secure. diff --git a/examples/seed_examples.md b/examples/seed_examples.md deleted file mode 100644 index 679583a..0000000 --- a/examples/seed_examples.md +++ /dev/null @@ -1,12 +0,0 @@ -# Seed Examples - -1. This benchmark proves the model can reason. -2. This theorem guarantees production safety. -3. This cost reduction means transition is easy. -4. This model result shows all workers are motivated by incentives. -5. This uncertainty means we should delay action. -6. Under assumptions, the local result implies all deployments are safe. -7. The pilot data implies we should change policy immediately. -8. The proof implies the corollary in the same formal system. -9. In practice, this benchmark suggests gains but does not guarantee real-world performance. -10. Clearly, this single test means every environment is secure. diff --git a/profiles/echidna.adoc b/profiles/echidna.adoc new file mode 100644 index 0000000..1ba757b --- /dev/null +++ b/profiles/echidna.adoc @@ -0,0 +1,6 @@ +== Echidna Profile + +Primary use: proof/spec claim linting. + +Focus transitions: - theorem -> guarantee - local result -> universal +claim - assumption-bound result -> general truth diff --git a/profiles/echidna.md b/profiles/echidna.md deleted file mode 100644 index 47b0c43..0000000 --- a/profiles/echidna.md +++ /dev/null @@ -1,8 +0,0 @@ -# Echidna Profile - -Primary use: proof/spec claim linting. - -Focus transitions: -- theorem -> guarantee -- local result -> universal claim -- assumption-bound result -> general truth diff --git a/profiles/faces.adoc b/profiles/faces.adoc new file mode 100644 index 0000000..a004d18 --- /dev/null +++ b/profiles/faces.adoc @@ -0,0 +1,100 @@ +== Profile: faces + +*Target corpus:* the AffineScript face family — +`+affinescript/examples/faces/+`, the `+examples/same-cube/+` corpus in +this repo, and the face brand-surface repos (`+rattlescript+`, +`+jaffascript+`, `+pseudoscript+`, `+lucidscript+`, `+cafescripto+`). +*Mode:* invariant-grounding (behavioural equality, not doc-claims) +*Purpose:* Keep the load-bearing AffineScript claim — _"`different +faces, same cube`"_ — grounded in the actual behaviour of the face +transformers. + +=== Why this profile exists + +AffineScript is one canonical language (the "`cube`"). Each _face_ +(ADR-010) is an alternative surface syntax — RattleScript (Python), +JaffaScript (JS/TS), PseudoScript (pseudocode), LucidScript +(PureScript/Haskell), CafeScripto (CoffeeScript) — lowered to canonical +AffineScript by a pure text transformer (`+lib/_face.ml+`) and +previewed with `+preview-*+`. + +The whole architecture rests on one invariant: + +____ +For a given program, *every face lowers to the same canonical cube* +(modulo whitespace and comment placement), and therefore to the same +typed-wasm output. +____ + +That is a _claim_. Like any claim, it can rot: a transformer edit can +silently make one face diverge while the others still pass their own +round-trip tests. Per-face snapshot tests +(`+affinescript/tests/faces/+`) catch _drift within a face_ but not +_divergence between faces_ — they never compare face A’s cube against +face B’s. This profile grounds the cross-face equality directly: it is a +claim-path debugger for the same-cube invariant, locating _which_ face +breaks the cube and _where_. + +=== The claim path + +.... +face source (greet/rattle.affine, …) ← evidence / specification + │ preview- ← transition (transformer T) + ▼ +typed-wasm module (compile --face) ← the cube itself + │ sha256-equality vs canonical wasm ← grounding check + ▼ +"same cube" holds for this program ← conclusion (Grounded | Ungrounded) +.... + +=== Invocation + +[source,sh] +---- +# Ground the bundled same-cube corpus (needs an `affinescript` binary on +# PATH, or a dune build of it — see the script's resolver). +scripts/verify-same-cube.sh examples/same-cube/greet \ + --out .machine_readable/audits/same-cube.jsonl + +# Any directory of sibling face files for ONE program works: +scripts/verify-same-cube.sh path/to/-faces/ +---- + +A face brand-surface repo grounds its own examples by pointing the +shared workspace at its corpus (the `+tools/invariant-path/+` hook), +e.g.: + +[source,sh] +---- +just invariant-path same-cube examples/ +---- + +=== What it catches + +* A face whose lowering compiles to a *different typed-wasm module* than +the canonical reference (the cross-face equality break the per-face +snapshots miss). Comparing wasm — the cube itself — also avoids +text-only false-positives (e.g. tail-expression vs statement lowering, +observationally identical but textually different). +* A face example that fails to parse or compile (round-trip / build +break). +* A corpus where one face silently encodes a _different_ program. + +When faces split into more than one wasm class, the `+preview-*+` text +diff is printed per divergence so you can see _where_ the lowering parts +ways. + +=== Limits + +* *Byte-identical* wasm is stricter than *observational* equivalence: +two faces can print the same thing and return the same value yet emit +different wasm. The grounded `+greet+` result is exactly this — +rattle/pseudo/lucid vs canonical/jaffa/cafe split into two classes over +a trailing-statement lowering choice. The tool reports the wasm +_classes_ and leaves "`are these classes observationally equal?`" to the +reader; it does not execute the modules to compare runtime output. +* It grounds the corpora it is given; it does not enumerate all +programs. +* Effect-handler lowering soundness (tracked in affinescript #555); a +face that exercises `+handle+` may converge in text yet diverge at +runtime. diff --git a/profiles/faces.md b/profiles/faces.md deleted file mode 100644 index d45ddf7..0000000 --- a/profiles/faces.md +++ /dev/null @@ -1,90 +0,0 @@ - - -# Profile: faces - -**Target corpus:** the AffineScript face family — -`affinescript/examples/faces/`, the `examples/same-cube/` corpus in this -repo, and the face brand-surface repos (`rattlescript`, `jaffascript`, -`pseudoscript`, `lucidscript`, `cafescripto`). -**Mode:** invariant-grounding (behavioural equality, not doc-claims) -**Purpose:** Keep the load-bearing AffineScript claim — *"different faces, -same cube"* — grounded in the actual behaviour of the face transformers. - -## Why this profile exists - -AffineScript is one canonical language (the "cube"). Each *face* (ADR-010) -is an alternative surface syntax — RattleScript (Python), JaffaScript -(JS/TS), PseudoScript (pseudocode), LucidScript (PureScript/Haskell), -CafeScripto (CoffeeScript) — lowered to canonical AffineScript by a pure -text transformer (`lib/_face.ml`) and previewed with `preview-*`. - -The whole architecture rests on one invariant: - -> For a given program, **every face lowers to the same canonical cube** -> (modulo whitespace and comment placement), and therefore to the same -> typed-wasm output. - -That is a *claim*. Like any claim, it can rot: a transformer edit can -silently make one face diverge while the others still pass their own -round-trip tests. Per-face snapshot tests (`affinescript/tests/faces/`) -catch *drift within a face* but not *divergence between faces* — they -never compare face A's cube against face B's. This profile grounds the -cross-face equality directly: it is a claim-path debugger for the -same-cube invariant, locating *which* face breaks the cube and *where*. - -## The claim path - -``` -face source (greet/rattle.affine, …) ← evidence / specification - │ preview- ← transition (transformer T) - ▼ -typed-wasm module (compile --face) ← the cube itself - │ sha256-equality vs canonical wasm ← grounding check - ▼ -"same cube" holds for this program ← conclusion (Grounded | Ungrounded) -``` - -## Invocation - -```sh -# Ground the bundled same-cube corpus (needs an `affinescript` binary on -# PATH, or a dune build of it — see the script's resolver). -scripts/verify-same-cube.sh examples/same-cube/greet \ - --out .machine_readable/audits/same-cube.jsonl - -# Any directory of sibling face files for ONE program works: -scripts/verify-same-cube.sh path/to/-faces/ -``` - -A face brand-surface repo grounds its own examples by pointing the shared -workspace at its corpus (the `tools/invariant-path/` hook), e.g.: - -```sh -just invariant-path same-cube examples/ -``` - -## What it catches - -- A face whose lowering compiles to a **different typed-wasm module** than the - canonical reference (the cross-face equality break the per-face snapshots - miss). Comparing wasm — the cube itself — also avoids text-only - false-positives (e.g. tail-expression vs statement lowering, observationally - identical but textually different). -- A face example that fails to parse or compile (round-trip / build break). -- A corpus where one face silently encodes a *different* program. - -When faces split into more than one wasm class, the `preview-*` text diff is -printed per divergence so you can see *where* the lowering parts ways. - -## Limits - -- **Byte-identical** wasm is stricter than **observational** equivalence: two - faces can print the same thing and return the same value yet emit different - wasm. The grounded `greet` result is exactly this — rattle/pseudo/lucid vs - canonical/jaffa/cafe split into two classes over a trailing-statement - lowering choice. The tool reports the wasm *classes* and leaves "are these - classes observationally equal?" to the reader; it does not execute the - modules to compare runtime output. -- It grounds the corpora it is given; it does not enumerate all programs. -- Effect-handler lowering soundness (tracked in affinescript #555); a - face that exercises `handle` may converge in text yet diverge at runtime. diff --git a/profiles/hypatia.adoc b/profiles/hypatia.adoc new file mode 100644 index 0000000..c1acf3f --- /dev/null +++ b/profiles/hypatia.adoc @@ -0,0 +1,6 @@ +== Hypatia Profile + +Primary use: CI/CD intelligence docs, ADRs, issue/PR rationale checking. + +Focus transitions: - data -> policy - probability -> certainty - +benchmark -> capability diff --git a/profiles/hypatia.md b/profiles/hypatia.md deleted file mode 100644 index c2b7b8f..0000000 --- a/profiles/hypatia.md +++ /dev/null @@ -1,8 +0,0 @@ -# Hypatia Profile - -Primary use: CI/CD intelligence docs, ADRs, issue/PR rationale checking. - -Focus transitions: -- data -> policy -- probability -> certainty -- benchmark -> capability diff --git a/profiles/panll.adoc b/profiles/panll.adoc new file mode 100644 index 0000000..966a867 --- /dev/null +++ b/profiles/panll.adoc @@ -0,0 +1,6 @@ +== PanLL Profile + +Primary use: design and runtime behavior documentation claims. + +Focus transitions: - model -> reality - benchmark -> capability - +descriptive -> normative diff --git a/profiles/panll.md b/profiles/panll.md deleted file mode 100644 index f10edaf..0000000 --- a/profiles/panll.md +++ /dev/null @@ -1,8 +0,0 @@ -# PanLL Profile - -Primary use: design and runtime behavior documentation claims. - -Focus transitions: -- model -> reality -- benchmark -> capability -- descriptive -> normative diff --git a/profiles/pmpl.adoc b/profiles/pmpl.adoc new file mode 100644 index 0000000..82f1a48 --- /dev/null +++ b/profiles/pmpl.adoc @@ -0,0 +1,47 @@ +== Profile: pmpl + +*Target corpus:* `+~/Documents/hyperpolymath-repos/palimpsest-license/+` +*Mode:* doc-claims (factual grounding) *Purpose:* Keep the Palimpsest +Public License (PMPL) text grounded in the file system claims it makes +about itself, the Palimpsest covenant, the standard SPDX header form, +and the legal-fallback chain to MPL-2.0. + +=== Why this profile exists + +The PMPL text and its accompanying covenant are _normative_ documents: +they make promises about how the licence behaves, where the canonical +text lives, what SPDX identifier to use, and what the legal fallback is. +If the text references `+LICENSE-MPL-2.0+` and that file isn’t in the +repo, the licence is making a false structural claim about its own +fallback. That’s a worse kind of bullshit than the ordinary kind: +_licence-text bullshit_. So we ground it. + +=== Invocation + +[source,sh] +---- +cargo run --quiet -p invariant-path-cli -- doc-claims \ + --root ~/Documents/hyperpolymath-repos/palimpsest-license \ + --out ~/Documents/hyperpolymath-repos/palimpsest-license/.machine_readable/audits/doc-claims.jsonl +---- + +=== What v1 catches + +* `+LICENSE+`, `+LICENSE-MPL-2.0+`, `+PALIMPSEST-COVENANT.md+`, +`+NOTICE+` etc. referenced from the licence text — must actually exist +in the repo. +* Backtick-quoted SPDX-License-Identifier examples — verifies the +identifier strings are syntactically the ones the licence policy +document expects. +* Cross-references to estate-wide canonical paths +(`+standards/LICENCE-POLICY.adoc+`, etc.) — flagged as cross-repo by the +standards-docs profile workflow. + +=== What v1 does NOT catch (yet) + +* _Semantic_ claims about clauses ("`section 3.2 grants X`"). Grounding +those needs a clause-level parser. +* Translation-equivalence claims ("`the French version says the same +thing`"). Out of scope. +* Re-licensing chains across third-party dependencies. That’s the job of +the upcoming PLASMA repo-sweeper, not invariant-path. diff --git a/profiles/pmpl.md b/profiles/pmpl.md deleted file mode 100644 index b0252b2..0000000 --- a/profiles/pmpl.md +++ /dev/null @@ -1,47 +0,0 @@ - - -# Profile: pmpl - -**Target corpus:** `~/Documents/hyperpolymath-repos/palimpsest-license/` -**Mode:** doc-claims (factual grounding) -**Purpose:** Keep the Palimpsest Public License (PMPL) text grounded in -the file system claims it makes about itself, the Palimpsest covenant, -the standard SPDX header form, and the legal-fallback chain to MPL-2.0. - -## Why this profile exists - -The PMPL text and its accompanying covenant are *normative* documents: -they make promises about how the licence behaves, where the canonical -text lives, what SPDX identifier to use, and what the legal fallback is. -If the text references `LICENSE-MPL-2.0` and that file isn't in the -repo, the licence is making a false structural claim about its own -fallback. That's a worse kind of bullshit than the ordinary kind: -*licence-text bullshit*. So we ground it. - -## Invocation - -```sh -cargo run --quiet -p invariant-path-cli -- doc-claims \ - --root ~/Documents/hyperpolymath-repos/palimpsest-license \ - --out ~/Documents/hyperpolymath-repos/palimpsest-license/.machine_readable/audits/doc-claims.jsonl -``` - -## What v1 catches - -- `LICENSE`, `LICENSE-MPL-2.0`, `PALIMPSEST-COVENANT.md`, `NOTICE` etc. - referenced from the licence text — must actually exist in the repo. -- Backtick-quoted SPDX-License-Identifier examples — verifies the - identifier strings are syntactically the ones the licence policy - document expects. -- Cross-references to estate-wide canonical paths - (`standards/LICENCE-POLICY.adoc`, etc.) — flagged as cross-repo by - the standards-docs profile workflow. - -## What v1 does NOT catch (yet) - -- *Semantic* claims about clauses ("section 3.2 grants X"). Grounding - those needs a clause-level parser. -- Translation-equivalence claims ("the French version says the same - thing"). Out of scope. -- Re-licensing chains across third-party dependencies. That's the job - of the upcoming PLASMA repo-sweeper, not invariant-path. diff --git a/profiles/standards-docs.adoc b/profiles/standards-docs.adoc new file mode 100644 index 0000000..05a5fb3 --- /dev/null +++ b/profiles/standards-docs.adoc @@ -0,0 +1,68 @@ +== Profile: standards-docs + +*Target corpus:* `+~/Documents/hyperpolymath-repos/standards/+` *Mode:* +doc-claims (factual grounding) *Purpose:* Keep the hyperpolymath +standards corpus honest. Every file path the standards documents +reference should actually exist; every A2ML key claim should resolve; +every "`command X returns clean`" should be verifiable from a CI +artefact. + +=== Why this profile exists + +The standards repo is the _single source of truth_ for what the +hyperpolymath estate claims about itself (CRG, TRG, RSR, Immaculate +Guide, Palimpsest, A2ML format, k9-svc, etc.). When a standards document +says "`the canonical proof suite lives at +`+templates/CANONICAL-PROOF-SUITE.adoc+``", that file had better exist. +When it doesn’t, the standard is making a factual claim about a file +system state that isn’t true — i.e. it is _bullshitting_ about itself. + +This profile is the panic-attacker for that prose. + +=== Invocation + +From the invariant-path workspace: + +[source,sh] +---- +cargo run --quiet -p invariant-path-cli -- doc-claims \ + --root ~/Documents/hyperpolymath-repos/standards \ + --out ~/Documents/hyperpolymath-repos/standards/.machine_readable/audits/doc-claims.jsonl +---- + +Exit code 2 on any ungrounded claim. Wire this into the standards repo’s +CI just like `+panic-attack assail+`. + +=== Known limitations (v1) + +* *Single-root scan.* A claim like `+\'0-AI-MANIFEST.a2ml\'+` in +`+standards/foo.adoc+` is not "`the AI manifest of the _standards_ +repo`" — it’s a generic statement about the per-repo manifest +convention. v1 will mark it as ungrounded relative to `+standards/+`. +Multi-root / cross-repo grounding is on the roadmap. +* *Recogniser surface.* v1 understands backtick-quoted paths, +A2ML-presence assertions, and command-clean claims. It does not yet +understand version-pin claims, badge claims, or "`X is at Y line N`" +positional references. Those are easy adds and should follow real usage. +* *No A2ML parser yet.* A2ML key checks are lexical only. Replace with a +real parser when `+a2ml-rs+` is available. +* *No `+--allow-exec+` resolver.* Command-clean claims are reported as +Unknown by default. CI artefact-based resolution is planned (read the +most recent recorded run from `+.machine_readable/audits/+`). + +=== Triage workflow + +A first run on a real corpus will return a _lot_ of ungrounded claims. +Triage them in this order: + +[arabic] +. *Drift.* The claim is false because the file got renamed or moved. Fix +the standard. +. *Vaporware.* The claim names a file that was promised but never +created. Either create the file or remove the claim. +. *Cross-repo reference.* The claim is correct but lives in a different +repo. Note for v2 (multi-root mode); for now, accept the ungrounded +result with an inline `++` marker (suppression +syntax also v2). +. *Genuine bug in the recogniser.* The claim isn’t really a claim. File +an issue against invariant-path with the offending sentence. diff --git a/profiles/standards-docs.md b/profiles/standards-docs.md deleted file mode 100644 index 3bc19ed..0000000 --- a/profiles/standards-docs.md +++ /dev/null @@ -1,69 +0,0 @@ - - -# Profile: standards-docs - -**Target corpus:** `~/Documents/hyperpolymath-repos/standards/` -**Mode:** doc-claims (factual grounding) -**Purpose:** Keep the hyperpolymath standards corpus honest. Every file -path the standards documents reference should actually exist; every -A2ML key claim should resolve; every "command X returns clean" should be -verifiable from a CI artefact. - -## Why this profile exists - -The standards repo is the *single source of truth* for what the -hyperpolymath estate claims about itself (CRG, TRG, RSR, Immaculate -Guide, Palimpsest, A2ML format, k9-svc, etc.). When a standards document -says "the canonical proof suite lives at `templates/CANONICAL-PROOF-SUITE.adoc`", -that file had better exist. When it doesn't, the standard is making a -factual claim about a file system state that isn't true — i.e. it is -*bullshitting* about itself. - -This profile is the panic-attacker for that prose. - -## Invocation - -From the invariant-path workspace: - -```sh -cargo run --quiet -p invariant-path-cli -- doc-claims \ - --root ~/Documents/hyperpolymath-repos/standards \ - --out ~/Documents/hyperpolymath-repos/standards/.machine_readable/audits/doc-claims.jsonl -``` - -Exit code 2 on any ungrounded claim. Wire this into the standards repo's -CI just like `panic-attack assail`. - -## Known limitations (v1) - -- **Single-root scan.** A claim like `` `0-AI-MANIFEST.a2ml` `` in - `standards/foo.adoc` is not "the AI manifest of the *standards* repo" - — it's a generic statement about the per-repo manifest convention. - v1 will mark it as ungrounded relative to `standards/`. Multi-root / - cross-repo grounding is on the roadmap. -- **Recogniser surface.** v1 understands backtick-quoted paths, - A2ML-presence assertions, and command-clean claims. It does not yet - understand version-pin claims, badge claims, or "X is at Y line N" - positional references. Those are easy adds and should follow real - usage. -- **No A2ML parser yet.** A2ML key checks are lexical only. Replace with - a real parser when `a2ml-rs` is available. -- **No `--allow-exec` resolver.** Command-clean claims are reported as - Unknown by default. CI artefact-based resolution is planned (read the - most recent recorded run from `.machine_readable/audits/`). - -## Triage workflow - -A first run on a real corpus will return a *lot* of ungrounded claims. -Triage them in this order: - -1. **Drift.** The claim is false because the file got renamed or moved. - Fix the standard. -2. **Vaporware.** The claim names a file that was promised but never - created. Either create the file or remove the claim. -3. **Cross-repo reference.** The claim is correct but lives in a - different repo. Note for v2 (multi-root mode); for now, accept the - ungrounded result with an inline `` marker - (suppression syntax also v2). -4. **Genuine bug in the recogniser.** The claim isn't really a claim. - File an issue against invariant-path with the offending sentence. diff --git a/proofs/README.adoc b/proofs/README.adoc new file mode 100644 index 0000000..3321058 --- /dev/null +++ b/proofs/README.adoc @@ -0,0 +1,38 @@ +== Proofs + +Machine-checked proofs supporting the `+faces+` profile and the +same-cube verifier. + +=== `+SameCube.agda+` + +The lemma underneath the same-cube grounding. Running +`+verify-same-cube.sh+` against a real affinescript build splits the +`+greet+` corpus into two wasm classes — `+{ a; }+` (statement; the +canonical/jaffa/cafe class) vs `+{ a }+` (tail-expression; the +rattle/pseudo/lucid class). This module proves that for a +*unit-returning* effectful action those two lowerings are +_observationally identical_ (same effect trace, same unit return), so +the split denotes the *same cube*. It also pins the boundary: for a +non-unit tail the two lowerings have different _result types_, so a +value-returning corpus would genuinely diverge — which is the precise +formal reason the equivalence is unit-tail-only. + +Check it: + +[source,sh] +---- +agda --safe proofs/SameCube.agda # or: just proofs +---- + +`+--safe+` rules out postulates and other escape hatches, so this is a +real constructive proof, not an assertion. Agda 2.6.x; self-contained +(no stdlib), with `+Trace+` abstracted as a module parameter. + +=== Scope + +This proves the _observational_ equivalence of the two lowering styles +for the unit case. The stronger obligation — full *transformer +semantics-preservation* (every `+lib/_face.ml+` transform +preserves the typed-wasm denotation for all programs) — remains future +work; it needs the affinescript AST + wasm semantics formalised, not +just this block-lowering fragment. diff --git a/proofs/README.md b/proofs/README.md deleted file mode 100644 index 817ddbe..0000000 --- a/proofs/README.md +++ /dev/null @@ -1,36 +0,0 @@ - - -# Proofs - -Machine-checked proofs supporting the `faces` profile and the same-cube -verifier. - -## `SameCube.agda` - -The lemma underneath the same-cube grounding. Running `verify-same-cube.sh` -against a real affinescript build splits the `greet` corpus into two wasm -classes — `{ a; }` (statement; the canonical/jaffa/cafe class) vs `{ a }` -(tail-expression; the rattle/pseudo/lucid class). This module proves that for a -**unit-returning** effectful action those two lowerings are *observationally -identical* (same effect trace, same unit return), so the split denotes the -**same cube**. It also pins the boundary: for a non-unit tail the two lowerings -have different *result types*, so a value-returning corpus would genuinely -diverge — which is the precise formal reason the equivalence is unit-tail-only. - -Check it: - -```sh -agda --safe proofs/SameCube.agda # or: just proofs -``` - -`--safe` rules out postulates and other escape hatches, so this is a real -constructive proof, not an assertion. Agda 2.6.x; self-contained (no stdlib), -with `Trace` abstracted as a module parameter. - -## Scope - -This proves the *observational* equivalence of the two lowering styles for the -unit case. The stronger obligation — full **transformer semantics-preservation** -(every `lib/_face.ml` transform preserves the typed-wasm denotation for -all programs) — remains future work; it needs the affinescript AST + wasm -semantics formalised, not just this block-lowering fragment.