diff --git a/.clinerules b/.clinerules index 0e8f23d..5e4ac6a 100644 --- a/.clinerules +++ b/.clinerules @@ -17,7 +17,7 @@ # state, estate governance/CI scaffold, and CROSS-project proofs in # verification/proofs/ that import >=2 constituent repos (e.g. agda/EchoTyping.agda). -# Then: read 0-AI-MANIFEST.a2ml, then .machine_readable/6a2/STATE.a2ml. +# Then: read 0-AI-MANIFEST.a2ml, then .machine_readable/descriptiles/STATE.a2ml. # Licence MPL-2.0 (never AGPL) + SPDX header on every file. # Banned langs: TypeScript->ReScript, npm/Node->Deno, Go->Rust, Python->Julia/Rust. # Containers: Podman + Containerfile. Build via just. diff --git a/.cursorrules b/.cursorrules index 697cd70..6024e64 100644 --- a/.cursorrules +++ b/.cursorrules @@ -17,7 +17,7 @@ # state, estate governance/CI scaffold, and CROSS-project proofs in # verification/proofs/ that import >=2 constituent repos (e.g. agda/EchoTyping.agda). -# Then: read 0-AI-MANIFEST.a2ml, then .machine_readable/6a2/STATE.a2ml. +# Then: read 0-AI-MANIFEST.a2ml, then .machine_readable/descriptiles/STATE.a2ml. # Licence MPL-2.0 (never AGPL) + SPDX header on every file. # Banned langs: TypeScript->ReScript, npm/Node->Deno, Go->Rust, Python->Julia/Rust. # Containers: Podman + Containerfile. Build via just. diff --git a/.envrc b/.envrc index c3666d9..8b08782 100644 --- a/.envrc +++ b/.envrc @@ -20,7 +20,7 @@ fi export PROJECT_NAME="nextgen-typing — Type Theory Pipeline" export RSR_TIER="infrastructure" # export DATABASE_URL="..." -# export API_KEY="..." +# Supply any service credentials through the ignored .env file, never here. # Source .env if it exists (gitignored) dotenv_if_exists diff --git a/.github/workflows/actions.lock b/.github/workflows/actions.lock index 425ccc8..906100b 100644 --- a/.github/workflows/actions.lock +++ b/.github/workflows/actions.lock @@ -14,7 +14,7 @@ workflows: - 'dependabot/fetch-metadata@v2.2.0' '.github/workflows/dogfood-gate.yml': - 'actions/checkout@v4.3.1' - - 'hyperpolymath/a2ml-ecosystem@main' + - 'hyperpolymath/deed-ecosystem@main' - 'hyperpolymath/k9-ecosystem@main' '.github/workflows/e2e.yml': [] '.github/workflows/governance.yml': [] @@ -125,9 +125,9 @@ dependencies: commit: 'sha1-c6f931105cb2c34c8f901cc885ba1e2e259cf745' owner_id: 9919 repo_id: 259445878 - 'hyperpolymath/a2ml-ecosystem@main': + 'hyperpolymath/deed-ecosystem@main': ref: 'main' - commit: 'sha1-aa4b836bd969df2bc58128cb8e3d20bbc88d5e79' + commit: 'sha1-f7a40a4d5cc82b2e73f861119baa6818d77a448d' owner_id: 6759885 repo_id: 1275649586 'hyperpolymath/k9-ecosystem@main': diff --git a/.github/workflows/dogfood-gate.yml b/.github/workflows/dogfood-gate.yml index 4c240b3..28af733 100644 --- a/.github/workflows/dogfood-gate.yml +++ b/.github/workflows/dogfood-gate.yml @@ -1,5 +1,5 @@ -# SPDX-License-Identifier: MPL-2.0 # This workflow is managed by gh actions-lock. +# SPDX-License-Identifier: MPL-2.0 # Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) # # dogfood-gate.yml — Hyperpolymath Dogfooding Quality Gate @@ -40,7 +40,7 @@ jobs: - name: Validate A2ML manifests if: steps.detect.outputs.count > 0 - uses: hyperpolymath/a2ml-ecosystem/validate-action@main + uses: hyperpolymath/deed-ecosystem/validate-action@f7a40a4d5cc82b2e73f861119baa6818d77a448d # main; same revision as actions.lock with: path: '.' strict: 'false' @@ -385,4 +385,3 @@ jobs: *Generated by the [Dogfood Gate](https://github.com/hyperpolymath/rsr-template-repo) workflow.* *Dogfooding is guinea pig fooding — we test our tools on ourselves.* EOF - diff --git a/.github/workflows/openssf-compliance.yml b/.github/workflows/openssf-compliance.yml index b322a20..b8087f7 100644 --- a/.github/workflows/openssf-compliance.yml +++ b/.github/workflows/openssf-compliance.yml @@ -75,13 +75,13 @@ jobs: exit 1 fi - # Canonical location is .machine_readable/6a2/ (estate standard; - # Hypatia SD004 flags any *.a2ml of the 6a2 set OUTSIDE 6a2/). - if [ ! -f ".machine_readable/6a2/STATE.a2ml" ]; then - echo "::error::.machine_readable/6a2/STATE.a2ml is required" + # Canonical location is .machine_readable/descriptiles/ (estate standard; + # Hypatia SD004 flags any *.a2ml of the descriptiles set OUTSIDE descriptiles/). + if [ ! -f ".machine_readable/descriptiles/STATE.a2ml" ]; then + echo "::error::.machine_readable/descriptiles/STATE.a2ml is required" exit 1 fi - echo ".machine_readable/6a2/STATE.a2ml: OK" + echo ".machine_readable/descriptiles/STATE.a2ml: OK" - name: Check CHANGELOG exists run: | @@ -99,8 +99,8 @@ jobs: # Collect all required files that exist for f in SECURITY.md SECURITY.adoc .github/SECURITY.md LICENSE LICENSE.txt \ CONTRIBUTING.md CONTRIBUTING.adoc README.md README.adoc \ - .machine_readable/6a2/STATE.a2ml .machine_readable/6a2/META.a2ml \ - .machine_readable/6a2/ECOSYSTEM.a2ml CHANGELOG.md CHANGELOG.adoc; do + .machine_readable/descriptiles/STATE.a2ml .machine_readable/descriptiles/META.a2ml \ + .machine_readable/descriptiles/ECOSYSTEM.a2ml CHANGELOG.md CHANGELOG.adoc; do [ -f "$f" ] && REQUIRED_FILES="$REQUIRED_FILES $f" done diff --git a/.github/workflows/workflow-linter.yml b/.github/workflows/workflow-linter.yml index dab29dd..ddf81b9 100644 --- a/.github/workflows/workflow-linter.yml +++ b/.github/workflows/workflow-linter.yml @@ -33,13 +33,13 @@ jobs: failed=0 for file in .github/workflows/*.yml .github/workflows/*.yaml; do [ -f "$file" ] || continue - if ! head -1 "$file" | grep -q "^# SPDX-License-Identifier:"; then + if ! awk '/^#/ { if ($0 ~ /^# SPDX-License-Identifier:/) found=1; next } /^[[:space:]]*$/ { next } { exit } END { exit !found }' "$file"; then echo "ERROR: $file missing SPDX header" failed=1 fi done if [ $failed -eq 1 ]; then - echo "Add '# SPDX-License-Identifier: MPL-2.0' as first line" + echo "Add '# SPDX-License-Identifier: MPL-2.0' to the opening comment header" exit 1 fi echo "All workflows have SPDX headers" @@ -62,24 +62,18 @@ jobs: fi echo "All workflows have permissions declared" - - name: Check SHA-Pinned Actions + - name: Verify action lockfile coverage + env: + GH_TOKEN: ${{ github.token }} + GH_CONFIG_DIR: ${{ runner.temp }}/workflow-linter-gh + XDG_DATA_HOME: ${{ runner.temp }}/workflow-linter-data run: | - echo "=== Checking Action Pinning ===" - # Find any uses: lines that don't have @SHA format - # Pattern: uses: owner/repo@<40-char-hex> - unpinned=$(grep -rnE "^[[:space:]]+uses:" .github/workflows/ | \ - grep -v "@[a-f0-9]\{40\}" | \ - grep -v "uses: \./\|uses: docker://\|uses: actions/github-script" || true) - - if [ -n "$unpinned" ]; then - echo "ERROR: Found unpinned actions:" - echo "$unpinned" - echo "" - echo "Replace version tags with SHA pins, e.g.:" - echo " uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.1" - exit 1 - fi - echo "All actions are SHA-pinned" + # Binary extensions accept release tags, not source commit pins. + # Verify the v0.1.6 linux-amd64 release bytes before executing them. + gh release download v0.1.6 --repo github/gh-actions-lock --pattern linux-amd64 --output "$RUNNER_TEMP/gh-actions-lock" + echo "4181ec1da5408b34b9a542a7ee5c6ce3a4d6ac815c7d0206a00ceca8a817f4e3 $RUNNER_TEMP/gh-actions-lock" | sha256sum --check --strict + chmod +x "$RUNNER_TEMP/gh-actions-lock" + "$RUNNER_TEMP/gh-actions-lock" --verify-local - name: Check for Duplicate Workflows run: | diff --git a/.machine_readable/ai/AI.a2ml b/.machine_readable/ai/AI.a2ml index 147a3c0..d21e8b0 100644 --- a/.machine_readable/ai/AI.a2ml +++ b/.machine_readable/ai/AI.a2ml @@ -21,9 +21,9 @@ constituent repos) under `verification/proofs/`. ## Workflow -1. Read `0-AI-MANIFEST.a2ml`, then `.machine_readable/6a2/STATE.a2ml` for +1. Read `0-AI-MANIFEST.a2ml`, then `.machine_readable/descriptiles/STATE.a2ml` for blockers and next actions. -2. Respect `.machine_readable/6a2/AGENTIC.a2ml` constraints. +2. Respect `.machine_readable/descriptiles/AGENTIC.a2ml` constraints. 3. Before creating any file, confirm placement against `placement.a2ml`. 4. After edits, update STATE with outcomes; commit with a concise message. diff --git a/.machine_readable/ai/README.adoc b/.machine_readable/ai/README.adoc index 1f548bb..a41aed1 100644 --- a/.machine_readable/ai/README.adoc +++ b/.machine_readable/ai/README.adoc @@ -20,5 +20,5 @@ Recommended machine read order: * `.machine_readable/policies/MAINTENANCE-AXES.a2ml` * `.machine_readable/policies/MAINTENANCE-CHECKLIST.a2ml` * `.machine_readable/policies/SOFTWARE-DEVELOPMENT-APPROACH.a2ml` -* `.machine_readable/6a2/STATE.a2ml` -* `.machine_readable/6a2/META.a2ml` +* `.machine_readable/descriptiles/STATE.a2ml` +* `.machine_readable/descriptiles/META.a2ml` diff --git a/.machine_readable/anchors/README.adoc b/.machine_readable/anchors/README.adoc index f2f1a12..bacf290 100644 --- a/.machine_readable/anchors/README.adoc +++ b/.machine_readable/anchors/README.adoc @@ -2,6 +2,6 @@ // Copyright (c) Jonathan D.A. Jewell = anchors Registry -MOVED: the anchor record now lives at `.machine_readable/6a2/anchor/ANCHOR.a2ml` +MOVED: the anchor record now lives at `.machine_readable/descriptiles/anchor/ANCHOR.a2ml` (estate-standardization layout, 2026-06-12). This directory remains only as a forwarding stub for older references. diff --git a/.machine_readable/bot_directives/README.adoc b/.machine_readable/bot_directives/README.adoc index fb866af..3171b3b 100644 --- a/.machine_readable/bot_directives/README.adoc +++ b/.machine_readable/bot_directives/README.adoc @@ -58,7 +58,7 @@ interactive agents. == Relationship to Other Files -* `../6a2/AGENTIC.a2ml` says WHAT agents can do (permissions, gating) +* `../descriptiles/AGENTIC.a2ml` says WHAT agents can do (permissions, gating) * `bot_directives/` says HOW agents should work (methodology) and what the automation fleet may do (fleet-specific) * `CLAUDE.md` (where present) says how Claude specifically should work diff --git a/.machine_readable/bot_directives/gitbot-fleet.a2ml b/.machine_readable/bot_directives/gitbot-fleet.a2ml index 5410351..2dbe8ad 100644 --- a/.machine_readable/bot_directives/gitbot-fleet.a2ml +++ b/.machine_readable/bot_directives/gitbot-fleet.a2ml @@ -26,12 +26,12 @@ ci-green-before-merge = true # Adapted for nextgen-typing: no .claude/CLAUDE.md exists here (listed # defensively), proofs live under verification/proofs/, and the ABI scaffold # under src/interface/ is frozen pending the OQ-001 identity decision -# (see 6a2/STATE.a2ml). The anchor is maintainer-only. +# (see descriptiles/STATE.a2ml). The anchor is maintainer-only. never-touch = [ ".claude/CLAUDE.md", "verification/proofs/", "src/interface/", - ".machine_readable/6a2/anchor/ANCHOR.a2ml", + ".machine_readable/descriptiles/anchor/ANCHOR.a2ml", "LICENSE", ] diff --git a/.machine_readable/bot_directives/placement.a2ml b/.machine_readable/bot_directives/placement.a2ml index 40b78ba..685b979 100644 --- a/.machine_readable/bot_directives/placement.a2ml +++ b/.machine_readable/bot_directives/placement.a2ml @@ -10,7 +10,7 @@ [metadata] version = "1.0.0" -last-updated = "2026-06-19" +last-updated = "2026-09-09" applies-to = "nextgen-typing" precedence = "maintainer > this directive > bot defaults" @@ -51,12 +51,15 @@ rules = [ { subject = "TypeLL kernel: dependent/linear/session types, QTT, proof-carrying code, effects", owns = "typell" }, { subject = "WasmGC memory-safety proofs, verified convergence ABI, aggregate-library conventions", owns = "typed-wasm" }, { subject = "echo-types library: fiber-based structured loss (Echo/EchoLinear/EchoResidue/EchoCharacteristic)", owns = "echo-types", companion = "EchoTypes.jl" }, + { subject = "standpoint-indexed access, warrants and sound proof transport", owns = "epistemic-types" }, + { subject = "evidence-indexed residual models, explorer, candidate-world proofs and tests", owns = "residual-evidence-types" }, + { subject = "cross-project type-family map, shared glossary and connection obligations", owns = "nextgen-typing" }, { subject = "choreographic / multiparty session types", owns = "choreographic-types" }, { subject = "TypeFix Zero / micro-Type-0 calibration calculus", owns = "typefix-zero" }, { subject = "AffineScript language code", owns = "affinescript" }, { subject = "Ephapax language code / region calculus", owns = "ephapax" }, { subject = "query-language type safety (SQL/GraphQL/Cypher/SPARQL/VQL)", owns = "typedqliser", also = "vcl-ut" }, - { subject = "tropical / semiring type theory (Isabelle/Lean)", owns = "tropical-resource-typing" }, + { subject = "tropical / semiring type theory (Isabelle/Lean)", owns = "tropical-types", former-name = "tropical-resource-typing" }, { subject = "transport-adapter / max-plus pathfinding", owns = "protocol-squisher" }, { subject = "eNSAID reference env (downstream consumer of TypeLL)", owns = "panll" }, ] diff --git a/.machine_readable/contractiles/Adjustfile.a2ml b/.machine_readable/contractiles/Adjustfile.a2ml index 295dcb0..74ff056 100644 --- a/.machine_readable/contractiles/Adjustfile.a2ml +++ b/.machine_readable/contractiles/Adjustfile.a2ml @@ -24,9 +24,9 @@ output this repo produces (docs, CLI tooling, diagrams). ## Documentation Drift ### readme-state-sync -- description: README.adoc, docs/ARCHITECTURE.adoc, docs/PIPELINE.adoc and 6a2/{STATE,META,ECOSYSTEM}.a2ml should agree -- tolerance: No contradictions between narrative docs and 6a2 metadata -- corrective: Run the periodic drift scan listed in 6a2/STATE.a2ml critical-next-actions +- description: README.adoc, docs/ARCHITECTURE.adoc, docs/PIPELINE.adoc and descriptiles/{STATE,META,ECOSYSTEM}.a2ml should agree +- tolerance: No contradictions between narrative docs and descriptiles metadata +- corrective: Run the periodic drift scan listed in descriptiles/STATE.a2ml critical-next-actions - severity: advisory ### pipeline-currency @@ -40,7 +40,7 @@ output this repo produces (docs, CLI tooling, diagrams). - tolerance: 0 {{PLACEHOLDER}} markers outside .machine_readable/ai/PLACEHOLDERS.adoc - corrective: Fill per PLACEHOLDERS.adoc (just init or manual sed pass) - severity: advisory -- notes: As of 2026-06-12 placeholders remain in .github/ community files, self-validating/ k9 templates, and QUICKSTART-MAINTAINER.adoc (tracked as OQ-002 in 6a2/STATE.a2ml) +- notes: As of 2026-06-12 placeholders remain in .github/ community files, self-validating/ k9 templates, and QUICKSTART-MAINTAINER.adoc (tracked as OQ-002 in descriptiles/STATE.a2ml) ## Structural Drift diff --git a/.machine_readable/contractiles/Bustfile.a2ml b/.machine_readable/contractiles/Bustfile.a2ml index a6d13db..827c10c 100644 --- a/.machine_readable/contractiles/Bustfile.a2ml +++ b/.machine_readable/contractiles/Bustfile.a2ml @@ -47,7 +47,7 @@ a working recovery path is a gate failure under the bust verb. ### metadata-corruption - description: A .a2ml file becomes unparseable or contradicts reality - class: partial_write -- recovery: restore from git history (git checkout origin/main -- ); 6a2/ is canonical, root pointers are derivable +- recovery: restore from git history (git checkout origin/main -- ); descriptiles/ is canonical, root pointers are derivable - expected-recovery-time-seconds: 300 - status: declared diff --git a/.machine_readable/contractiles/Dustfile.a2ml b/.machine_readable/contractiles/Dustfile.a2ml index 41c3eaa..a963c98 100644 --- a/.machine_readable/contractiles/Dustfile.a2ml +++ b/.machine_readable/contractiles/Dustfile.a2ml @@ -34,10 +34,10 @@ dust items accumulate as warnings, they do not gate. - severity: info ### no-root-scm-state -- description: Root S-expr state files retired — 6a2 A2ML is canonical; root STATE.a2ml is a pointer only (2026-06-12) +- description: Root S-expr state files retired — descriptiles A2ML is canonical; root STATE.a2ml is a pointer only (2026-06-12) - run: "! grep -l '^(state' .machine_readable/*.a2ml 2>/dev/null | head -1 | grep -q ." - severity: warning -- notes: Root META.a2ml / ECOSYSTEM.a2ml still carry S-expr bodies duplicating 6a2/; proposed for the same pointer-ization (see 2026-06-12 checkpoint report) +- notes: Root META.a2ml / ECOSYSTEM.a2ml still carry S-expr bodies duplicating descriptiles/; proposed for the same pointer-ization (see 2026-06-12 checkpoint report) ## Build Artifacts diff --git a/.machine_readable/contractiles/Intentfile.a2ml b/.machine_readable/contractiles/Intentfile.a2ml index fb4d2a4..8be473b 100644 --- a/.machine_readable/contractiles/Intentfile.a2ml +++ b/.machine_readable/contractiles/Intentfile.a2ml @@ -22,7 +22,7 @@ # Provenance: repo-true rewrite at the 2026-06-12 governance checkpoint. # The former root INTENT.contractile was an unfilled rsr-template stub # ({{ONE_PARAGRAPH_PURPOSE}} placeholders); purpose/anti-purpose below are -# populated from README.adoc, EXPLAINME.adoc and 6a2/META.a2ml ADRs. +# populated from README.adoc, EXPLAINME.adoc and descriptiles/META.a2ml ADRs. @abstract: North-star contractile for nextgen-typing, the coordination monorepo for @@ -62,7 +62,7 @@ This repository is NOT: ## If In Doubt If you are unsure whether a change is in scope, ask. Sensitive areas: -- .machine_readable/ contractile definitions and 6a2/anchor/ +- .machine_readable/ contractile definitions and descriptiles/anchor/ - verification/proofs/ + src/interface/ (frozen pending OQ-001) - Governance docs (GOVERNANCE.adoc, MAINTAINERS.adoc, CODEOWNERS) - License policy documents @@ -71,7 +71,7 @@ If you are unsure whether a change is in scope, ask. Sensitive areas: ### decide-oq-001 - description: Decide the identity contradiction — docs-only coordination monorepo vs real proof repo (drop or re-scope the RSR code scaffold) -- probe: grep -q 'OQ-001.*status = "open"' .machine_readable/6a2/STATE.a2ml && echo open +- probe: grep -q 'OQ-001.*status = "open"' .machine_readable/descriptiles/STATE.a2ml && echo open - status: declared - notes: Raised 2026-06-05 (PR #31); blocks proof-debt resolution (6 believe_me markers) @@ -79,7 +79,7 @@ If you are unsure whether a change is in scope, ask. Sensitive areas: - description: Replace remaining template placeholders per .machine_readable/ai/PLACEHOLDERS.adoc - probe: "! grep -rl 'hyperpolymath' .github/ 2>/dev/null | head -1 | grep -q ." - status: declared -- notes: Tracked as OQ-002 in 6a2/STATE.a2ml +- notes: Tracked as OQ-002 in descriptiles/STATE.a2ml ### track-tropical-extensions - description: Track Tropical.thy extensions (linorder instance, tropical matrices, Kleene algebra) in tropical-resource-typing and mirror in docs @@ -102,7 +102,7 @@ If you are unsure whether a change is in scope, ask. Sensitive areas: - notes: Proposed in README.adoc (2026-06-09); design-stage #### drift-scan-automation -- description: Periodic automated drift scan keeping README/ARCHITECTURE/PIPELINE/6a2 synchronized +- description: Periodic automated drift scan keeping README/ARCHITECTURE/PIPELINE/descriptiles synchronized - horizon: near - status: declared diff --git a/.machine_readable/contractiles/Justfile b/.machine_readable/contractiles/Justfile index ebcb4c8..4246729 100644 --- a/.machine_readable/contractiles/Justfile +++ b/.machine_readable/contractiles/Justfile @@ -345,7 +345,7 @@ verify-template: fi # Check for empty SCM files - for f in .machine_readable/6a2/STATE.a2ml .machine_readable/6a2/META.a2ml .machine_readable/6a2/ECOSYSTEM.a2ml; do + for f in .machine_readable/descriptiles/STATE.a2ml .machine_readable/descriptiles/META.a2ml .machine_readable/descriptiles/ECOSYSTEM.a2ml; do if [ -f "$f" ] && grep -q '{{'{{'}}' "$f" 2>/dev/null; then echo "⚠ $f still has template placeholders" FOUND=1 @@ -403,10 +403,10 @@ self-assess: fi done - if [ -d ".machine_readable/6a2" ]; then - echo " ✓ .machine_readable/6a2/ — KEEP (SCM checkpoint files)" + if [ -d ".machine_readable/descriptiles" ]; then + echo " ✓ .machine_readable/descriptiles/ — KEEP (SCM checkpoint files)" else - echo " ✗ .machine_readable/6a2/ — MISSING (RSR violation!)" + echo " ✗ .machine_readable/descriptiles/ — MISSING (RSR violation!)" fi if [ -d ".github/workflows" ]; then diff --git a/.machine_readable/contractiles/Mustfile.a2ml b/.machine_readable/contractiles/Mustfile.a2ml index b6cf465..3dbe9f5 100644 --- a/.machine_readable/contractiles/Mustfile.a2ml +++ b/.machine_readable/contractiles/Mustfile.a2ml @@ -10,7 +10,7 @@ # Folds the former nested contractiles/must/Mustfile.a2ml checks and the # universal invariants of the former root MUST.contractile (both removed # by the estate-standardization merge). Directory checks updated to the -# post-merge flat layout (no nested bust/dust dirs; 6a2/anchor singular). +# post-merge flat layout (no nested bust/dust dirs; descriptiles/anchor singular). @abstract: Physical-state invariants for nextgen-typing, the coordination monorepo @@ -69,13 +69,13 @@ hooks fail if any check fails. - severity: critical ### six-directory-present -- description: 6a2 directory exists with required files -- run: test -d .machine_readable/6a2 && test -f .machine_readable/6a2/META.a2ml && test -f .machine_readable/6a2/ECOSYSTEM.a2ml && test -f .machine_readable/6a2/STATE.a2ml && test -f .machine_readable/6a2/PLAYBOOK.a2ml && test -f .machine_readable/6a2/AGENTIC.a2ml && test -f .machine_readable/6a2/NEUROSYM.a2ml +- description: descriptiles directory exists with required files +- run: test -d .machine_readable/descriptiles && test -f .machine_readable/descriptiles/META.a2ml && test -f .machine_readable/descriptiles/ECOSYSTEM.a2ml && test -f .machine_readable/descriptiles/STATE.a2ml && test -f .machine_readable/descriptiles/PLAYBOOK.a2ml && test -f .machine_readable/descriptiles/AGENTIC.a2ml && test -f .machine_readable/descriptiles/NEUROSYM.a2ml - severity: critical ### anchor-directory -- description: anchor directory exists in 6a2 with ANCHOR.a2ml -- run: test -f .machine_readable/6a2/anchor/ANCHOR.a2ml +- description: anchor directory exists in descriptiles with ANCHOR.a2ml +- run: test -f .machine_readable/descriptiles/anchor/ANCHOR.a2ml - severity: warning ### self-validating-structure @@ -133,7 +133,7 @@ hooks fail if any check fails. - description: No believe_me in Idris2 code - run: "! grep -r 'believe_me' --include='*.idr' . 2>/dev/null | grep -v node_modules | head -1 | grep -q ." - severity: critical -- notes: 6 believe_me markers currently exist in scaffold proof files; recorded tech debt (docs/tech-debt-2026-05-26.md, PRs #12/#18), pending the OQ-001 identity decision in 6a2/STATE.a2ml. The check stays red until that decision lands — do not weaken it to hide the debt. +- notes: 6 believe_me markers currently exist in scaffold proof files; recorded tech debt (docs/tech-debt-2026-05-26.md, PRs #12/#18), pending the OQ-001 identity decision in descriptiles/STATE.a2ml. The check stays red until that decision lands — do not weaken it to hide the debt. ### no-sorry - description: No sorry in Lean code diff --git a/.machine_readable/contractiles/Trustfile.a2ml b/.machine_readable/contractiles/Trustfile.a2ml index 81e2d75..56e235f 100644 --- a/.machine_readable/contractiles/Trustfile.a2ml +++ b/.machine_readable/contractiles/Trustfile.a2ml @@ -62,7 +62,7 @@ explicitly told otherwise. ## Sensitive Areas (explicit approval required) -- .machine_readable/6a2/anchor/ANCHOR.a2ml — maintainer-only authority record +- .machine_readable/descriptiles/anchor/ANCHOR.a2ml — maintainer-only authority record - GOVERNANCE.adoc / MAINTAINERS.adoc / .github/CODEOWNERS — governance - verification/proofs/ + src/interface/ — frozen pending OQ-001 decision - .github/workflows/ — thin wrappers of standards reusables; changes ride diff --git a/.machine_readable/6a2/0-AI-MANIFEST.a2ml b/.machine_readable/descriptiles/0-AI-MANIFEST.a2ml similarity index 84% rename from .machine_readable/6a2/0-AI-MANIFEST.a2ml rename to .machine_readable/descriptiles/0-AI-MANIFEST.a2ml index 4fbca89..92f7f94 100644 --- a/.machine_readable/6a2/0-AI-MANIFEST.a2ml +++ b/.machine_readable/descriptiles/0-AI-MANIFEST.a2ml @@ -1,11 +1,11 @@ # SPDX-License-Identifier: MPL-2.0 # Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) # -# AI Manifest for 6a2 Directory +# AI Manifest for descriptiles Directory ## Purpose -This manifest declares the AI-assistant context for the 6a2 machine-readable metadata directory. +This manifest declares the AI-assistant context for the descriptiles machine-readable metadata directory. ## Canonical Locations diff --git a/.machine_readable/6a2/AGENTIC.a2ml b/.machine_readable/descriptiles/AGENTIC.a2ml similarity index 100% rename from .machine_readable/6a2/AGENTIC.a2ml rename to .machine_readable/descriptiles/AGENTIC.a2ml diff --git a/.machine_readable/6a2/ECOSYSTEM.a2ml b/.machine_readable/descriptiles/ECOSYSTEM.a2ml similarity index 66% rename from .machine_readable/6a2/ECOSYSTEM.a2ml rename to .machine_readable/descriptiles/ECOSYSTEM.a2ml index 68ebaa1..204a3f9 100644 --- a/.machine_readable/6a2/ECOSYSTEM.a2ml +++ b/.machine_readable/descriptiles/ECOSYSTEM.a2ml @@ -6,7 +6,7 @@ [metadata] version = "0.1.0" -last-updated = "2026-06-12" +last-updated = "2026-09-09" [project] name = "nextgen-typing" @@ -22,15 +22,25 @@ projects = [ { name = "typell", relationship = "coordinates", notes = "TypeLL verification kernel. Open-ended progressive type safety. Powers PanLL port 7800." }, { name = "typed-wasm", relationship = "coordinates", notes = "TypeLL applied to WasmGC memory safety + aggregate library for AffineScript/Ephapax." }, { name = "echo-types", relationship = "integrated", notes = "Fiber-based structured-loss formalization integrated into the typesystem (#33, 2026-06-12)." }, + { name = "epistemic-types", relationship = "research-coordination", notes = "Standpoint-indexed modalities, warrants and explicit soundness. Mapped in docs/TYPE-CONNECTIONS.adoc; no new integration certified by the map." }, + { name = "residual-evidence-types", relationship = "research-coordination", notes = "Public work in progress: minimal Agda core proves presence without identification. Narrow Echo fibre and Epistemic SoundWarrant comparisons checked; broader composition, revision and explorer correspondence pending. Receipts in docs/TYPE-CONNECTIONS.adoc." }, + { name = "choreographic-types", relationship = "research-coordination", notes = "Projection, retained distinctions, resource bounds and warrant transport; general K-CUT remains open in reviewed documentation." }, { name = "panll", relationship = "downstream-consumer", notes = "eNSAID reference env. TypeLL runs inside PanLL. Not owned by nextgen-typing." }, { name = "nextgen-languages/affinescript", relationship = "co-product", notes = "Compiles to typed WasmGC. TypeLL grounds its type system." }, { name = "nextgen-languages/ephapax", relationship = "co-product", notes = "Compiles to typed WasmGC. TypeLL grounds its dyadic linear/affine system." }, - { name = "tropical-resource-typing", relationship = "research-artefact", notes = "Isabelle/HOL + Lean 4 tropical type theory work. Feeds into protocol-squisher." }, + { name = "tropical-types", relationship = "research-artefact", notes = "Canonical GitHub name resolved 2026-09-09 from tropical-resource-typing. Resource algebras and bounds; distinct from Echo structure." }, { name = "protocol-squisher", relationship = "co-product", notes = "Transport semilattice; adapter path search is Dijkstra on max-plus semiring (tropical)." }, { name = "nextgen-languages", relationship = "sibling-standard", notes = "Sibling coordination monorepo for the language family." }, { name = "nextgen-databases", relationship = "sibling-standard", notes = "Sibling coordination monorepo for the database family." }, ] +[type-research-map] +guide = "docs/TYPE-CONNECTIONS.adoc" +edge-semantics = "Conceptual relationships and proposed obligations; not imports, integrations, equivalences or proof receipts" +name-resolution-date = "2026-09-09" +former-tropical-name = "tropical-resource-typing -> tropical-types" +historical-research-name = "katagoria -> ideas-to-alphas; distinct from kategoria" + [integration-points] integrations = [ { system = "katagoria", direction = "outbound", protocol = "documentation-reference", notes = "Research upstream and level-candidate feeder for the main chain." }, diff --git a/.machine_readable/6a2/META.a2ml b/.machine_readable/descriptiles/META.a2ml similarity index 98% rename from .machine_readable/6a2/META.a2ml rename to .machine_readable/descriptiles/META.a2ml index 9b00290..83cdcce 100644 --- a/.machine_readable/6a2/META.a2ml +++ b/.machine_readable/descriptiles/META.a2ml @@ -6,7 +6,7 @@ [metadata] version = "0.1.1" -last-updated = "2026-06-12" +last-updated = "2026-09-09" [project-info] type = "monorepo" # library | binary | monorepo | service | website @@ -35,7 +35,7 @@ id = "ADR-003" title = "typed-wasm has dual role (ADR-004 in typed-wasm)" status = "accepted" date = "2026-04-11" -rationale = "typed-wasm is both the TypeLL WASM safety application AND the aggregate library for AffineScript+Ephapax cross-language binary conventions. Both roles are first-class. See typed-wasm/.machine_readable/6a2/META.a2ml#ADR-004." +rationale = "typed-wasm is both the TypeLL WASM safety application AND the aggregate library for AffineScript+Ephapax cross-language binary conventions. Both roles are first-class. See typed-wasm/.machine_readable/descriptiles/META.a2ml#ADR-004." [[architecture-decisions.adrs]] id = "ADR-004" diff --git a/.machine_readable/6a2/NEUROSYM.a2ml b/.machine_readable/descriptiles/NEUROSYM.a2ml similarity index 100% rename from .machine_readable/6a2/NEUROSYM.a2ml rename to .machine_readable/descriptiles/NEUROSYM.a2ml diff --git a/.machine_readable/6a2/PLAYBOOK.a2ml b/.machine_readable/descriptiles/PLAYBOOK.a2ml similarity index 93% rename from .machine_readable/6a2/PLAYBOOK.a2ml rename to .machine_readable/descriptiles/PLAYBOOK.a2ml index 758d390..84d55de 100644 --- a/.machine_readable/6a2/PLAYBOOK.a2ml +++ b/.machine_readable/descriptiles/PLAYBOOK.a2ml @@ -13,7 +13,7 @@ last-updated = "2026-06-12" # target = "container" # container | binary | library | wasm [incident-response] -# 1. Check .machine_readable/6a2/STATE.a2ml for current status +# 1. Check .machine_readable/descriptiles/STATE.a2ml for current status # 2. Review recent commits and CI results # 3. Run `just validate` to check compliance # 4. Run `just security` to audit for vulnerabilities diff --git a/.machine_readable/6a2/README.adoc b/.machine_readable/descriptiles/README.adoc similarity index 97% rename from .machine_readable/6a2/README.adoc rename to .machine_readable/descriptiles/README.adoc index 916a702..97414db 100644 --- a/.machine_readable/6a2/README.adoc +++ b/.machine_readable/descriptiles/README.adoc @@ -1,6 +1,6 @@ // SPDX-License-Identifier: CC-BY-SA-4.0 // Copyright (c) Jonathan D.A. Jewell -# A2ML 6a2 Directory +# A2ML descriptiles Directory This directory contains the 6 core A2ML machine-readable metadata files for this repository. diff --git a/.machine_readable/6a2/STATE.a2ml b/.machine_readable/descriptiles/STATE.a2ml similarity index 88% rename from .machine_readable/6a2/STATE.a2ml rename to .machine_readable/descriptiles/STATE.a2ml index 3c24792..109afe2 100644 --- a/.machine_readable/6a2/STATE.a2ml +++ b/.machine_readable/descriptiles/STATE.a2ml @@ -6,7 +6,7 @@ [metadata] project = "nextgen-typing" version = "0.1.0" -last-updated = "2026-06-19" +last-updated = "2026-09-09" status = "active" [project-context] @@ -72,7 +72,7 @@ actions = [ "Track Tropical.thy extensions (linorder instance, tropical matrices, Kleene algebra) in tropical-resource-typing and mirror progress in nextgen-typing docs.", "Track and link the arXiv paper draft on speculative tropical session types once published.", "Track typed-wasm aggregate ABI convention adoption in AffineScript/Ephapax integration paths as recursive-type support matures.", - "Run periodic drift scans so README.adoc, docs/ARCHITECTURE.adoc, docs/PIPELINE.adoc, and .machine_readable/6a2/{STATE,META,ECOSYSTEM}.a2ml stay synchronized.", + "Run periodic drift scans so README.adoc, docs/ARCHITECTURE.adoc, docs/PIPELINE.adoc, and .machine_readable/descriptiles/{STATE,META,ECOSYSTEM}.a2ml stay synchronized.", ] [maintenance-status] @@ -96,3 +96,16 @@ events = [ part-of = ["hyperpolymath coordination infrastructure"] coordinates = ["typell", "typed-wasm", "katagoria", "tropical-resource-typing", "protocol-squisher"] downstream-consumers = ["panll", "nextgen-languages/affinescript", "nextgen-languages/ephapax"] + +[type-research-map] +review-date = "2026-09-09" +guide = "docs/TYPE-CONNECTIONS.adoc" +graphic = "docs/images/type-connections.svg" +editable-source = "docs/images/type-connections.dot" +families = ["echo-types", "epistemic-types", "tropical-types", "residual-evidence-types", "choreographic-types"] +status = "Documentation map and glossary; arrows are conceptual, not integration or proof claims" +residual-status = "Work in progress: minimal Agda core and narrow Echo/Epistemic comparisons checked; finite explorer separate" +next-residual-milestone = "Dependency-preserving composition and evidence revision/retraction in residual-evidence-types" +proof-validation = "Agda 2.6.4.3 safe/without-K: residual core, three expected rejections and two direct comparisons passed locally and in hosted job 34400282291; whole constituent suites not rerun" +proof-receipt = "https://github.com/hyperpolymath/residual-evidence-types/blob/4325198c10e2e689f084c2f64a27213685a1ffd2/PROOF-STATUS.adoc" +metadata-location = ".machine_readable/descriptiles/" diff --git a/.machine_readable/6a2/anchor/0-AI-MANIFEST.a2ml b/.machine_readable/descriptiles/anchor/0-AI-MANIFEST.a2ml similarity index 100% rename from .machine_readable/6a2/anchor/0-AI-MANIFEST.a2ml rename to .machine_readable/descriptiles/anchor/0-AI-MANIFEST.a2ml diff --git a/.machine_readable/6a2/anchor/ANCHOR.a2ml b/.machine_readable/descriptiles/anchor/ANCHOR.a2ml similarity index 100% rename from .machine_readable/6a2/anchor/ANCHOR.a2ml rename to .machine_readable/descriptiles/anchor/ANCHOR.a2ml diff --git a/.machine_readable/6a2/anchor/README.adoc b/.machine_readable/descriptiles/anchor/README.adoc similarity index 95% rename from .machine_readable/6a2/anchor/README.adoc rename to .machine_readable/descriptiles/anchor/README.adoc index 13cae63..2a6a30c 100644 --- a/.machine_readable/6a2/anchor/README.adoc +++ b/.machine_readable/descriptiles/anchor/README.adoc @@ -1,4 +1,4 @@ -// SPDX-License-Identifier: CC-BY-SA-4.0 +// SPDX-License-Identifier: MPL-2.0 // Copyright (c) Jonathan D.A. Jewell # A2ML Anchor Directory @@ -22,4 +22,3 @@ https://github.com/hyperpolymath/standards/tree/main/anchor-a2ml - [A2ML Repository Template](https://github.com/hyperpolymath/standards/blob/main/A2ML-REPO-TEMPLATE.adoc) - [Anchor A2ML Spec](https://github.com/hyperpolymath/standards/tree/main/anchor-a2ml) - diff --git a/.machine_readable/policies/MAINTENANCE-AXES.a2ml b/.machine_readable/policies/MAINTENANCE-AXES.a2ml index 071f012..84b5512 100644 --- a/.machine_readable/policies/MAINTENANCE-AXES.a2ml +++ b/.machine_readable/policies/MAINTENANCE-AXES.a2ml @@ -18,7 +18,7 @@ machine-entrypoints = [ ".machine_readable/policies/MAINTENANCE-AXES.a2ml", ".machine_readable/policies/MAINTENANCE-CHECKLIST.a2ml", ".machine_readable/policies/SOFTWARE-DEVELOPMENT-APPROACH.a2ml", - ".machine_readable/6a2/META.a2ml", + ".machine_readable/descriptiles/META.a2ml", ".machine_readable/ai/README.adoc", ".machine_readable/bot_directives/README.scm", ] diff --git a/.machine_readable/self-validating/methodology-guard.k9.ncl b/.machine_readable/self-validating/methodology-guard.k9.ncl index 9116ed9..8646f74 100644 --- a/.machine_readable/self-validating/methodology-guard.k9.ncl +++ b/.machine_readable/self-validating/methodology-guard.k9.ncl @@ -61,7 +61,7 @@ let methodology_guard = { state_not_template = { description = "STATE.a2ml must not contain template placeholders", severity = "warning", - file = ".machine_readable/6a2/STATE.a2ml", + file = ".machine_readable/descriptiles/STATE.a2ml", reject_patterns = ["{{PLACEHOLDER}}", "NEXTGEN_TYPING", "rsr-template-repo"], }, diff --git a/.windsurfrules b/.windsurfrules index c399b67..dc671cf 100644 --- a/.windsurfrules +++ b/.windsurfrules @@ -17,7 +17,7 @@ # state, estate governance/CI scaffold, and CROSS-project proofs in # verification/proofs/ that import >=2 constituent repos (e.g. agda/EchoTyping.agda). -# Then: read 0-AI-MANIFEST.a2ml, then .machine_readable/6a2/STATE.a2ml. +# Then: read 0-AI-MANIFEST.a2ml, then .machine_readable/descriptiles/STATE.a2ml. # Licence MPL-2.0 (never AGPL) + SPDX header on every file. # Banned langs: TypeScript->ReScript, npm/Node->Deno, Go->Rust, Python->Julia/Rust. # Containers: Podman + Containerfile. Build via just. diff --git a/0-AI-MANIFEST.a2ml b/0-AI-MANIFEST.a2ml index d2d2f18..8331661 100644 --- a/0-AI-MANIFEST.a2ml +++ b/0-AI-MANIFEST.a2ml @@ -39,9 +39,9 @@ research PoCs → `kategoria`; μType₀ → `typefix-zero`; choreographic types ## Canonical Locations - Pipeline architecture: `docs/ARCHITECTURE.adoc` -- Current state + blockers: `.machine_readable/6a2/STATE.a2ml` -- ADRs: `.machine_readable/6a2/META.a2ml` -- Ecosystem relationships: `.machine_readable/6a2/ECOSYSTEM.a2ml` +- Current state + blockers: `.machine_readable/descriptiles/STATE.a2ml` +- ADRs: `.machine_readable/descriptiles/META.a2ml` +- Ecosystem relationships: `.machine_readable/descriptiles/ECOSYSTEM.a2ml` - Content routing (what goes where): `.machine_readable/bot_directives/placement.a2ml` - Human overview: `README.adoc` - What-is-this explainer: `EXPLAINME.adoc` @@ -49,7 +49,7 @@ research PoCs → `kategoria`; μType₀ → `typefix-zero`; choreographic types ## Startup Sequence For AI Agents 1. Read this manifest. -2. Read `.machine_readable/6a2/STATE.a2ml` for blockers and next actions. +2. Read `.machine_readable/descriptiles/STATE.a2ml` for blockers and next actions. 3. Read `docs/ARCHITECTURE.adoc` for the full pipeline picture. 4. Read `ROADMAP.adoc` for what is and isn't done. @@ -64,14 +64,14 @@ research PoCs → `kategoria`; μType₀ → `typefix-zero`; choreographic types ## PRIORITY ACTION — this repository is not fully initialised 22 substitution token(s) still have no value. **Read -`REQUIRES_INITIALISATION.md` in the repository root before doing anything +`REQUIRES_INITIALISATION.adoc` in the repository root before doing anything else here** — it lists every outstanding token, what it means, and which files it belongs in. Do not fabricate values for them, and do not delete the sections that contain them to quiet a gate. They are unfilled because they need a decision, not because they were overlooked. Resolve what you legitimately -can, leave the rest, and delete `REQUIRES_INITIALISATION.md` only when +can, leave the rest, and delete `REQUIRES_INITIALISATION.adoc` only when nothing outstanding remains. diff --git a/AFFIRMATION.adoc b/AFFIRMATION.adoc index 3c862b8..9233243 100644 --- a/AFFIRMATION.adoc +++ b/AFFIRMATION.adoc @@ -1,305 +1,117 @@ -// SPDX-License-Identifier: CC-BY-SA-4.0 +// SPDX-License-Identifier: MPL-2.0 // SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell -= AFFIRMATION — nextgen-typing, as of 2026-06-16 -:toc: macro -:toclevels: 2 += AFFIRMATION — coordination checks, 2026-09-09 +:toc: -_the No-Bullshit file: what we affirm was true and checkable at this moment_ +This is a bounded verification record for the shared type-family map and +coordination layer. It records observed results, including failures and checks +whose scope is narrower than their success message suggests. -[NOTE] -==== -*Genre.* An *affirmation* is a solemn declaration of the truth of a statement, -made by someone who _declines to swear an oath_. That is exactly what this is: -our truth-as-best-believed at a stamped instant — binding on our honesty, not a -claim of infallibility. It is not the README and not the EXPLAINME: +The previous June affirmation remains available as a +https://github.com/hyperpolymath/nextgen-typing/blob/0b3693acfe09fdd4254cd6a77f2d241f20624b81/AFFIRMATION.adoc[historical snapshot in Git]. +Its dates, paths, toolchain and proof inventory are not current verification receipts. -[cols="1,3,2",options="header"] +== Anchor and scope + +[cols="1,3",options="header"] |=== -| File | Answers | Tense -| `README.adoc` | _Where is this going, and why?_ — the pipeline overview and steering | future / aspirational -| `EXPLAINME.adoc` | _How is it built, and what's the evidence?_ — the coordination mechanism | descriptive / mechanism -| *`AFFIRMATION.adoc`* (this file) | _What can we honestly affirm was *true and checkable* at a stamped moment?_ | a frozen instant, falsifiable +|Field |Observed value +|Repository |`hyperpolymath/nextgen-typing` +|Branch |`docs/type-connections` +|Checked commit |`1a8c836b23115510a0c9b883c0b73f8710f8a18c` +|Check session |2026-09-09 UTC; anchor captured at `20:34:41Z`, followed by the checks below +|Working tree |Clean at the checked commit; the map regenerated without a diff. +This affirmation is added after the checks and does not claim to verify itself. +|Local toolchain |Just 1.56.0; Bash 5.2.37; Git 2.47.3; Agda 2.6.4.3; +Graphviz 2.42.4 +|Checked commit signature |`git log -1 --format='%H %G? %GS'` reported `G` +(good signature), signer `jonathan.jewell@gmail.com`. +|Canonical metadata |`.machine_readable/descriptiles/` |=== -`nextgen-typing` is a *coordination monorepo*, not a compiler or a proof -project. The affirmation that matters here is about the coordination layer -itself: that its registry and cross-file invariants build and are internally -consistent, and that it holds *no* proofs of its own — by design. -==== - -toc::[] - -== What this is, and how it is designed to work - -*What it is.* A short, dated, jointly-signed snapshot of what we can _honestly -and verifiably_ claim about this repo at one exact commit. Nothing here is -marketing (that is the README) and nothing is engineering evidence for a -constituent repo's compiler or proofs (those claims belong in those repos). -This file is the receipt for the coordination layer. - -*How it is designed to work.* Three moving parts make it trustworthy: - -. *Ground truth, not memory.* Every claim below was produced by _running the - tool in the session that wrote this file_ (the pipeline-drift guard, the - must/trust gates, the template-residue check, and the proof-checker harness - this repo ships). Where a status doc said otherwise, the live run wins and we - flag the contradiction. -. *A frozen anchor.* The file names the exact commit SHA, branch, UTC - timestamp, and toolchain (see <>), so "true" always means - "true _at this point_". Move the SHA and this file becomes a draft until - re-run. -. *A real signature.* It is landed by a *signed git commit*; that signature - over this content at the anchored SHA is what makes the affirmation - tamper-evident and attributable — not the prose alone. - -*We are fallible.* We can be wrong, stale, or simply mistaken about our own -work. This file is our best honest belief, not a proof of its own correctness. -Treat it as a falsifiable claim, not gospel. - -== The epistemic contract (read this before you trust _or_ attack) - -This document records our *best joint belief* at the timestamp below. It is -*not a guarantee of correctness.* We may be wrong. We may have missed -something — a drifted doc, a stale registry line, a public description that -overruns the tree. +The observation horizon is this commit's coordination files and the named +checks below. Whole constituent proof suites, production deployments and +general mathematical novelty are outside this record. -*No intentional overclaim.* That is the only guarantee here: we have not -_knowingly_ inflated anything. This repo makes *no* compiler-correctness, -proof-soundness, or benchmark claim, and this file does not invent one. Where a -checker passed, we say "passed". Where one failed, we say "failed" and why. -Where the in-tree proof files are unconfigured RSR template residue, we say so -plainly. If you find an honest claim here that turns out false, that is an -error to be fixed — not a lie. +== Coordination results -*Standing invitation to refute.* You are _invited_ to bulldoze any claim in -this file. We want that. But the fair form of the attack is: - -. Read this file at the stamped commit. -. Reproduce (or fail to reproduce) the checks in <>. -. _Then_ tell us where the discrepancy is, against the artefact as it stood at - this moment — so we can either justify it or concede it on the record. - -An attack that skips steps 1–2 is attacking a strawman of a different date. - -*No fights before the facts are cleared up.* We are not interested in a dispute -over a claim until the discrepancy has actually been checked against the -artefact at this commit and we have had the chance to either justify it or -concede it on the record. Good faith both ways: bring a reproducible -discrepancy and we will fix the claim, the doc, or the registry — promptly and -without defensiveness. The goal is a corrected record, not a won argument. - -== Verifiable anchor - -[cols="1,3"] +[cols="2,1,4",options="header"] |=== -| *Repo* | `hyperpolymath/nextgen-typing` (the type-theory pipeline *coordination monorepo* — contains no compiler code) -| *Branch* | `main` -| *Commit (HEAD)* | `e9897daf4ba1d2104f78abd5f660a870279eda5b` -| *Permalink* | https://github.com/hyperpolymath/nextgen-typing/tree/e9897daf4ba1d2104f78abd5f660a870279eda5b -| *Verified (UTC)* | 2026-06-16T12:28:36Z -| *Working-tree delta at verification* | Clean (`git status --porcelain` empty) at the moment the checks below were run. This AFFIRMATION file is then added as a new untracked file; it does not change any check result above it. The results recorded here are HEAD as-is. -| *Toolchain* | just 1.50.0 · bash 5.2.21 · git 2.43.0 · Idris2 0.8.0 · Lean 4.13.0 · Agda 2.8.0 · Coq 8.18.0 · TLA+ `tlc` not installed -| *HEAD commit signature* | GPG-signed (RSA `9639451754496E51D6B537CAD119017EBF695AB1`, "hyperpolymath", `j.d.a.jewell@open.ac.uk`) — "Good signature" reported by `git log --show-signature`. +|Command |Exit |Meaning and limit +|`just type-map` |0 |SVG regenerates from its DOT source without a diff. +|`just validate-rsr` |0 |The recipe's required files, metadata and policy markers are present. +|`just validate-state` |0 |Its required metadata/project markers are present; +this is not a complete A2ML parser. +|`just validate-coordination` |0 |The repository's ownership boundary check passes. +|`just validate-pipeline-drift` |0 |The named pipeline documents and descriptiles +agree on the guarded chain, invariants and dates (`2026-09-09`). +|`just must-check` |0 |The recipe's licence/README/file-name checks pass. +Its source-header scan examines at most 20 matching Rust/ReScript/Gleam files; +this is not an exhaustive SPDX audit. +|`just trust-license-content` |0 |The recipe's licence-text marker check passes; +it does not establish licence consistency across every file. +|`just trust-no-secrets-committed` |0 |The three prohibited credential-file +paths checked by this recipe are absent. Separately, the deterministic +`sonar analyze secrets` scan of this worktree reported no issues. +|`gh actions-lock --verify-local` |0 |All 28 workflows have lockfile coverage. +The tool notes an inline validator SHA; it matches the lockfile's reviewed pin. +Offline coverage does not establish that mutable upstream refs have not moved. |=== -[IMPORTANT] -If you are reading this at a _later_ commit, the claims may have drifted. -Re-run <> and write a fresh affirmation; do not trust a stale one. - -== Companion documents and repo metadata (cross-check) - -This affirmation should be read against the repo's own public claims. Where they -drift from what we verified, we say so here rather than quietly leave the reader -to find out. - -* *`README.adoc`* — _present_. link:README.adoc[_"nextgen-typing — The - Hyperpolymath Type Theory Pipeline"_]. States plainly: "It does not contain - compiler code." Verified consistent with the tree. -* *`EXPLAINME.adoc`* — _present_. link:EXPLAINME.adoc[]. Explicitly: "This repo - makes *no claims* about compiler correctness, proof soundness, or benchmark - results." Verified consistent with what we ran. -* *`0-AI-MANIFEST.a2ml`* — _present_. The repo's read-first invariant file; - invariant #3 is "No compiler claims here". This AFFIRMATION upholds that - invariant rather than breaching it. -* *GitHub repo description* (fetched in-session via `gh repo view`) — - _"Coordination monorepo for the Hyperpolymath type-theory pipeline — - Kategoria/Katagoria, TypeLL, typed-Wasm, PanLL, and minimal calibration - calculi such as TypeFix Zero."_ *Drift:* the strings "Kategoria", "TypeFix - Zero", and "calibration calculi" do *not* appear anywhere in the tree at this - commit (the README's main chain spells it "katagoria", which it also flags as - *not yet created*). The description is ahead of the artefact; treat it as - steering, not a tree claim. -* *GitHub topics* — `dependent-types`, `formal-methods`, `linear-types`, - `partiality`, `turing-completeness`, `type-theory`, `typed-wasm`, - `universe-hierarchy`. *Caveat:* these describe the _pipeline this repo - coordinates_, not artefacts in this repo. None of `partiality`, - `turing-completeness`, or `universe-hierarchy` corresponds to any - proved-here content — they are properties of the constituent repos - (typell / typed-wasm / tropical-resource-typing), not of this coordination - layer. +The actual `validate-state` recipe was also exercised against isolated fixtures: +valid metadata passed; missing metadata, missing project and absent state failed. +The aggregate `just validate` failed for each invalid fixture. These controls +establish failure propagation, not complete syntax validation. -== The honest state (one breath) +The workflow SPDX check passed the repository and controls for a valid opening +comment header, a missing identifier and an identifier placed after YAML content. +The downloaded `gh-actions-lock` v0.1.6 linux-amd64 binary matched SHA-256 +`4181ec1da5408b34b9a542a7ee5c6ce3a4d6ac815c7d0206a00ceca8a817f4e3` +and successfully ran the same offline coverage check. -*nextgen-typing is a documentation-and-registry coordination layer for the -`katagoria → typell → typed-wasm → PanLL` pipeline. Its job is to keep the -cross-repo story consistent, and at this commit that job is being done: the -pipeline-drift guard and the must/trust correctness gates pass green. It holds -no proofs of its own — the proof directory is unconfigured RSR-template residue -that does not compile as shipped, and every real proof obligation lives in the -constituent repos, exactly as the manifest says it should.* +== Failures and misleading success messages -=== What is solid (and how we checked) - -* *The pipeline-drift registry guard passes — verified green this moment.* - `just validate-pipeline-drift` → `scripts/check-pipeline-drift.sh` exits *0*, - with *every* check PASS: all six canonical files present - (`README.adoc`, `docs/ARCHITECTURE.adoc`, `docs/PIPELINE.adoc`, and the three - `.machine_readable/6a2/` A2ML files); the canonical chain - `katagoria → typell → typed-wasm → PanLL` matches exactly across README, - ARCHITECTURE, PIPELINE, STATE and ECOSYSTEM; the "open-ended TypeLL" framing - is consistent across README/ARCHITECTURE/PIPELINE/META; katagoria marked - Active consistently; dates synchronized (all read `2026-04-12`); and no stale - status phrases. _This is the core "is the coordination internally consistent?" - check, and it is green._ -* *The "must" correctness gate passes.* `just must-check` exits *0*: LICENSE - present, README present, no banned `Dockerfile`/`Makefile`, and SPDX-header - presence on source files. -* *Licence is MPL-2.0, internally consistent.* `just trust-license-content` - passes; the in-tree `LICENSE` is the Mozilla Public License Version 2.0 and - in-tree source/doc files carry `SPDX-License-Identifier: CC-BY-SA-4.0`. (Note: the - `trust-verify` _aggregate_ recipe fails — see loud-failures — but that is a - Containerfile-pinning rule, not a licence problem.) -* *No secrets committed.* `just trust-no-secrets-committed` passes (no `.env`, - `credentials.json`, or `.env.local`). -* *The Coq template proof, taken alone, compiles.* `just proof-check-coq` exits - *0* (`coqc verification/proofs/coq/TypeSafety.v` → exit 0). *But read the - nuance below before reading anything into this:* it proves a toy - expression-language `type_soundness` theorem labelled "Template — replace with - your project's type system", _not_ any nextgen-typing claim. - -=== The honest nuance you must not lose (proved-CORE vs unproved-IMPLEMENTATION) - -*This repo proves nothing about the typing pipeline, and that is correct by -design.* The distinction here is sharper than the usual "proved core vs tested -implementation": - -* The `verification/proofs/` tree (`idris2/`, `lean4/`, `agda/`, `coq/`, - `tlaplus/`) is *unconfigured RSR template residue*. The files say so in their - own headers — e.g. `verification/proofs/idris2/Types.idr` line 5: "Template — - replace with your project's core types." They prove generic example lemmas - (a bounded-`Nat`, a toy expression language), not pipeline properties. -* `PROOF-STATUS.md` reports *0% proven* (0 of 7 obligations) — and the live run - *confirms* this rather than contradicting it: there is no nextgen-typing proof - to run. -* The genuine proof obligations for this pipeline live *in the constituent - repos* (`typell`, `typed-wasm`, `tropical-resource-typing`, `katagoria`), and - this coordination layer makes no claim to have discharged them. Anyone reading - the presence of `.idr`/`.lean`/`.agda`/`.v` files here as "nextgen-typing has - formal proofs" is overclaiming on the repo's behalf. - -=== Known-incomplete but honestly fenced (loud failures, never silent) - -These three checks *fail loudly* at this commit. They are real findings, fenced -here so no reader mistakes them for green: - -* *`just proof-check-idris2` FAILS (exit 1).* The Idris2 template proofs do not - even compile as shipped: `Module name Types does not match file name - "verification/proofs/idris2/Types.idr"` (and the same module-vs-path mismatch - for every `ABI/*.idr`). So the Idris2 "proofs" prove *nothing* right now — a - loud, visible failure, not a silent pass. (`proof-check-all` therefore also - surfaces these failures.) -* *`just proof-scan-dangerous` FAILS (exit 1) — but on false positives.* It - flags 8 files for "dangerous patterns", yet every hit is the _warning comment_ - itself (e.g. the line "All proofs MUST be constructive (no believe_me, no - assert_total)" trips the `believe_me`/`assert_total` matcher). There is no - actual `believe_me`, `sorry`, `Admitted`, or `postulate` in proof position — - the scanner is matching its own documentation. A scanner bug, recorded as - such; not evidence of unsound proofs (there are no load-bearing proofs to be - unsound). -* *`just verify-template` FAILS (exit 1).* Unreplaced `{{PLACEHOLDER}}` template - tokens remain in `QUICKSTART-MAINTAINER.adoc`, `QUICKSTART-DEV.adoc`, - `READINESS.md`, `TEST-NEEDS.md`, `TEMPLATE-STANDARDS-AUDIT.adoc`, and - `container/compose.toml`; the Justfile still references `rsr-template-repo`; - and the Groove manifest still has port `0`. This repo is a partly-uninstantiated - RSR template — honest, visible debt. -* *`just trust-verify` FAILS (exit 1)* at `trust-container-images-pinned`: the - `Containerfile` base images are not digest-pinned (`@sha256:`). A supply-chain - hygiene gap, not a coordination-correctness problem. - -=== Outstanding / weak / refuted (no spin) - -* *Public GitHub description over-runs the tree (drift).* It advertises - "Kategoria/Katagoria … TypeFix Zero … minimal calibration calculi", none of - which exist in the repo at this commit. Not refuted-as-false-claim (it is - steering text), but flagged so the reader is not misled. -* *`katagoria` is declared "✅ Active" in the README table* yet the manifest - (invariant #4) and EXPLAINME both say it "does not exist yet / not yet - created". Internal tension between the status glyph and the prose; the - honest reading is "planned, not created". -* *No nextgen-typing-specific proof exists* — by design, but stated plainly so - no one infers otherwise from the populated `verification/proofs/` tree. -* *TLA+ cannot be checked in this environment* (`tlc` not installed), so - `verification/proofs/tlaplus/StateMachine.tla` was not exercised at all. - -[#reproduce] -== Reproduce it yourself - -From the repo root, at the commit above: - -[source,sh] ----- -git rev-parse HEAD # expect e9897daf4ba1d2104f78abd5f660a870279eda5b -git status --porcelain # expect empty (clean) before adding this file - -just validate-pipeline-drift # expect exit 0 — "PASS: no pipeline drift detected." -just must-check # expect exit 0 — "All must checks passed" -just proof-check-coq # expect exit 0 — toy TEMPLATE proof compiles (not a pipeline claim) - -# The loud failures (expected to FAIL — that is the honest state, not a regression): -just proof-check-idris2 # expect exit 1 — module-name vs file-path mismatch in template .idr files -just proof-scan-dangerous # expect exit 1 — false positives on the warning COMMENTS, no real dangerous tactics -just verify-template # expect exit 1 — unreplaced {{PLACEHOLDER}} tokens + rsr-template-repo refs -just trust-verify # expect exit 1 — Containerfile base images not @sha256-pinned ----- +[cols="2,1,4",options="header"] +|=== +|Command |Exit |Observed result +|`just proof-check-coq` |0 |No `.v` files occur in the enumerated +`verification/proofs/` tree. The success message verifies no Coq theorem. +|`just proof-check-idris2` |0 |No `.idr` files occur in that tree. +The success message verifies no Idris theorem. +|`just proof-scan-dangerous` |1 |One match: the comment saying "zero postulates" +in `verification/proofs/agda/EchoTyping.agda`. This lexical match is not a +proof-position postulate and is not a successful proof audit either. +|`just verify-template` |1 |Unfilled setup placeholders, template references +and the Groove port-zero marker remain. `REQUIRES_INITIALISATION.adoc` tracks +outstanding decisions. The checker also reports placeholder examples in comments. +|`just trust-verify` |1 |The `trust-container-images-pinned` subcheck fails +on the root `Containerfile`. The two earlier trust subchecks pass. +|=== -To confirm the no-proofs-here invariant directly: the files under -`verification/proofs/` self-identify as templates (`grep -n Template -verification/proofs/idris2/Types.idr`), and `PROOF-STATUS.md` reports -*0% proven (0 of 7)*. +These are existing maintenance obligations, left visible. This record does not +turn an empty proof loop or a failed scanner into evidence of verification. +The current Agda cross-project files are present but were not rechecked here. -== One-line characterisation (quote this) +== Separate residual proof evidence -[quote] -____ -"A type-theory pipeline *coordination monorepo* whose registry/docs consistency -guard (`validate-pipeline-drift`) and `must`/licence gates pass green this -moment, that holds *no* proofs of its own — the in-tree proof tree is -unconfigured RSR template residue that does not compile, and all real proof -obligations live in the constituent repos — with honest, loudly-failing -template-instantiation debt (`verify-template`, Idris2 module paths, -Containerfile pinning) still on the queue. A coordination layer, not a verified -artefact. No intentional overclaim." -____ +The first residual milestone belongs to `residual-evidence-types`. +https://github.com/hyperpolymath/residual-evidence-types/actions/runs/34400741631[Its latest checked publication] +passed the minimal Agda core, three expected-rejection controls and two direct +comparisons with the published Echo and Epistemic interfaces. See the +https://github.com/hyperpolymath/residual-evidence-types/blob/b2cd4e2f40005f20d5c4bd9a06051c3215b4db9a/PROOF-STATUS.adoc[proof status at that revision] +for exact statements, pins and standard-library warnings. -== Joint attestation +The link:docs/TYPE-CONNECTIONS.adoc[shared glossary] links those bounded results. +The map's dashed arrows express conceptual relationships and further obligations. +Composition, evidence revision, a certified finite checker and explorer +correspondence remain open in the owning project. -We, the undersigned, assert that *to the best of our joint belief at the -timestamp above, every claim in this file is true and was checked as described* -— with no intentional overclaim, and with the open gaps stated rather than -hidden. +== Reproduce the record -* *Engineering party (AI):* Claude Opus 4.8 (`claude-opus-4-8[1m]`) — ran the - build/test/proof checks recorded here on 2026-06-16T12:28:36Z and stands - behind this wording as a faithful report of those runs. -* *Owner / maintainer:* Jonathan D.A. Jewell — _signs by committing this file - with `-S` (`id_ed25519_signing`); the git commit signature over this content, - at the commit SHA recorded above, is the cryptographic form of this - affirmation._ -+ -Signed-off-date: ____________________ (fill on signing) +Use the checked commit above and run each command in the tables independently, +retaining its exit status and output. A later successful hosted check does not +erase the listed local failures. A later source change needs a new record. -[TIP] -The authoritative, tamper-evident signature is the *signed git commit* that -lands this file. If the SHA in <> matches the parent of that -commit and the commit verifies, this affirmation is anchored. If they don't -match, treat the file as a draft. +This record was prepared by Codex from the actual local runs and linked hosted +results. The checked commit's signature result is recorded separately from +these claims; no additional maintainer attestation is asserted here. diff --git a/AGENTS.adoc b/AGENTS.adoc index 5ed2c5c..dea2771 100644 --- a/AGENTS.adoc +++ b/AGENTS.adoc @@ -1,3 +1,4 @@ +// SPDX-License-Identifier: MPL-2.0 == AGENTS.md — read this before writing any file ____ @@ -88,10 +89,10 @@ CI by `+.github/workflows/coordination-boundary.yml+`. [arabic] . Read `+0-AI-MANIFEST.a2ml+`, then -`+.machine_readable/6a2/STATE.a2ml+`. +`+.machine_readable/descriptiles/STATE.a2ml+`. . Full rules: `+docs/practice/AI-CONVENTIONS.adoc+`. . Licence *MPL-2.0* + SPDX header on every file (never AGPL). -. Banned languages: TypeScript→ReScript, npm/Node→Deno, Go→Rust, +. Banned languages: TypeScript→ReScript, npm/Node/Deno→Bun, Go→Rust, Python→Julia/Rust. Containers: Podman + `+Containerfile+`. Build/test via `+just+`. . No unsound escape hatches in any proof: `+believe_me+`, diff --git a/CLAUDE.md b/CLAUDE.md index 93fe105..af63d59 100644 --- a/CLAUDE.md +++ b/CLAUDE.md @@ -63,7 +63,7 @@ The machine-readable form of this table is the source of truth: ## After the boundary, follow the estate conventions -1. Read `0-AI-MANIFEST.a2ml`, then `.machine_readable/6a2/STATE.a2ml`. +1. Read `0-AI-MANIFEST.a2ml`, then `.machine_readable/descriptiles/STATE.a2ml`. 2. Full rules: `docs/practice/AI-CONVENTIONS.adoc`. 3. Licence **MPL-2.0** + SPDX header on every file (never AGPL). 4. Banned languages: TypeScript→ReScript, npm/Node→Deno, Go→Rust, Python→Julia/Rust. diff --git a/EXPLAINME.adoc b/EXPLAINME.adoc index 683622e..124b94c 100644 --- a/EXPLAINME.adoc +++ b/EXPLAINME.adoc @@ -1,4 +1,4 @@ -// SPDX-License-Identifier: CC-BY-SA-4.0 +// SPDX-License-Identifier: MPL-2.0 // Copyright (c) Jonathan D.A. Jewell = nextgen-typing — Explainme Jonathan D.A. Jewell @@ -56,13 +56,13 @@ repos. Here we only document: | `docs/ARCHITECTURE.adoc` | Full pipeline architecture doc (also served as the creation briefing) -| `.machine_readable/6a2/STATE.a2ml` +| `.machine_readable/descriptiles/STATE.a2ml` | Current state: milestones, blockers, next actions -| `.machine_readable/6a2/META.a2ml` +| `.machine_readable/descriptiles/META.a2ml` | ADRs: open-ended TypeLL, dual-role typed-wasm, katagoria upstream -| `.machine_readable/6a2/ECOSYSTEM.a2ml` +| `.machine_readable/descriptiles/ECOSYSTEM.a2ml` | All related projects and their relationship types |=== @@ -70,5 +70,5 @@ repos. Here we only document: Start with `README.adoc` for a 60-second overview. Read `docs/ARCHITECTURE.adoc` for the full pipeline description. Check -`ROADMAP.adoc` for what is and isn't done. Read `.machine_readable/6a2/STATE.a2ml` +`ROADMAP.adoc` for what is and isn't done. Read `.machine_readable/descriptiles/STATE.a2ml` for blockers and next actions. diff --git a/Justfile b/Justfile index f15269a..6bc20e5 100644 --- a/Justfile +++ b/Justfile @@ -52,7 +52,7 @@ info: @echo "Version: {{version}}" @echo "RSR Tier: {{tier}}" @echo "Recipes: $(just --summary | wc -w)" - @[ -f ".machine_readable/STATE.a2ml" ] && grep -oP 'phase\s*=\s*"\K[^"]+' .machine_readable/STATE.a2ml | head -1 | xargs -I{} echo "Phase: {}" || true + @[ -f ".machine_readable/descriptiles/STATE.a2ml" ] && grep -oP 'phase\s*=\s*"\K[^"]+' .machine_readable/descriptiles/STATE.a2ml | head -1 | xargs -I{} echo "Phase: {}" || true # Run Invariant Path overlay tools for this repository invariant-path *ARGS: @@ -345,7 +345,7 @@ verify-template: fi # Check for empty SCM files - for f in .machine_readable/6a2/STATE.a2ml .machine_readable/6a2/META.a2ml .machine_readable/6a2/ECOSYSTEM.a2ml; do + for f in .machine_readable/descriptiles/STATE.a2ml .machine_readable/descriptiles/META.a2ml .machine_readable/descriptiles/ECOSYSTEM.a2ml; do if [ -f "$f" ] && grep -q '{{'{{'}}' "$f" 2>/dev/null; then echo "⚠ $f still has template placeholders" FOUND=1 @@ -403,10 +403,10 @@ self-assess: fi done - if [ -d ".machine_readable/6a2" ]; then - echo " ✓ .machine_readable/6a2/ — KEEP (SCM checkpoint files)" + if [ -d ".machine_readable/descriptiles" ]; then + echo " ✓ .machine_readable/descriptiles/ — KEEP (SCM checkpoint files)" else - echo " ✗ .machine_readable/6a2/ — MISSING (RSR violation!)" + echo " ✗ .machine_readable/descriptiles/ — MISSING (RSR violation!)" fi if [ -d ".github/workflows" ]; then @@ -541,9 +541,9 @@ verify: check_file "LICENSE" check_either "CONTRIBUTING.md" "CONTRIBUTING.adoc" check_either "README.adoc" "README.md" - check_file ".machine_readable/STATE.a2ml" - check_file ".machine_readable/META.a2ml" - check_file ".machine_readable/ECOSYSTEM.a2ml" + check_file ".machine_readable/descriptiles/STATE.a2ml" + check_file ".machine_readable/descriptiles/META.a2ml" + check_file ".machine_readable/descriptiles/ECOSYSTEM.a2ml" check_either "CHANGELOG.md" "CHANGELOG.adoc" # Check at least 1 workflow exists @@ -1035,24 +1035,24 @@ validate-rsr: for f in .editorconfig .gitignore Justfile README.adoc LICENSE 0-AI-MANIFEST.a2ml; do [ -f "$f" ] || MISSING="$MISSING $f" done - for f in .machine_readable/6a2/STATE.a2ml .machine_readable/6a2/META.a2ml .machine_readable/6a2/ECOSYSTEM.a2ml .machine_readable/6a2/anchor/ANCHOR.a2ml .machine_readable/policies/MAINTENANCE-AXES.a2ml .machine_readable/policies/MAINTENANCE-CHECKLIST.a2ml .machine_readable/policies/SOFTWARE-DEVELOPMENT-APPROACH.a2ml; do + for f in .machine_readable/descriptiles/STATE.a2ml .machine_readable/descriptiles/META.a2ml .machine_readable/descriptiles/ECOSYSTEM.a2ml .machine_readable/descriptiles/anchor/ANCHOR.a2ml .machine_readable/policies/MAINTENANCE-AXES.a2ml .machine_readable/policies/MAINTENANCE-CHECKLIST.a2ml .machine_readable/policies/SOFTWARE-DEVELOPMENT-APPROACH.a2ml; do [ -f "$f" ] || MISSING="$MISSING $f" done - for f in licensing/exhibits/EXHIBIT-A-ETHICAL-USE.txt licensing/exhibits/EXHIBIT-B-QUANTUM-SAFE.txt licensing/texts/MPL-2.0.txt; do + for f in docs/legal/EXHIBIT-A-ETHICAL-USE.txt docs/legal/EXHIBIT-B-QUANTUM-SAFE.txt LICENSES/MPL-2.0.txt; do [ -f "$f" ] || MISSING="$MISSING $f" done for f in docs/governance/MAINTENANCE-CHECKLIST.adoc docs/governance/SOFTWARE-DEVELOPMENT-APPROACH.adoc; do [ -f "$f" ] || MISSING="$MISSING $f" done - if [ -f ".machine_readable/6a2/META.a2ml" ]; then - grep -q 'axis-1 = "must > intend > like"' .machine_readable/6a2/META.a2ml || MISSING="$MISSING META.a2ml:axis-1" - grep -q 'axis-2 = "corrective > adaptive > perfective"' .machine_readable/6a2/META.a2ml || MISSING="$MISSING META.a2ml:axis-2" - grep -q 'axis-3 = "systems > compliance > effects"' .machine_readable/6a2/META.a2ml || MISSING="$MISSING META.a2ml:axis-3" - grep -q 'scoping-first = true' .machine_readable/6a2/META.a2ml || MISSING="$MISSING META.a2ml:scoping-first" - grep -q 'idris-unsound-scan = "believe_me/assert_total"' .machine_readable/6a2/META.a2ml || MISSING="$MISSING META.a2ml:idris-unsound-scan" - grep -q 'audit-focus = "systems in place, documentation explains actual state, safety/security accounted for, observed effects reviewed"' .machine_readable/6a2/META.a2ml || MISSING="$MISSING META.a2ml:audit-focus" - grep -q 'compliance-focus = "seams/compromises/exception register, bounded exceptions, anti-drift checks"' .machine_readable/6a2/META.a2ml || MISSING="$MISSING META.a2ml:compliance-focus" - grep -q 'effects-evidence = "benchmark execution/results and maintainer status dialogue/review"' .machine_readable/6a2/META.a2ml || MISSING="$MISSING META.a2ml:effects-evidence" + if [ -f ".machine_readable/descriptiles/META.a2ml" ]; then + grep -q 'axis-1 = "must > intend > like"' .machine_readable/descriptiles/META.a2ml || MISSING="$MISSING META.a2ml:axis-1" + grep -q 'axis-2 = "corrective > adaptive > perfective"' .machine_readable/descriptiles/META.a2ml || MISSING="$MISSING META.a2ml:axis-2" + grep -q 'axis-3 = "systems > compliance > effects"' .machine_readable/descriptiles/META.a2ml || MISSING="$MISSING META.a2ml:axis-3" + grep -q 'scoping-first = true' .machine_readable/descriptiles/META.a2ml || MISSING="$MISSING META.a2ml:scoping-first" + grep -q 'idris-unsound-scan = "believe_me/assert_total"' .machine_readable/descriptiles/META.a2ml || MISSING="$MISSING META.a2ml:idris-unsound-scan" + grep -q 'audit-focus = "systems in place, documentation explains actual state, safety/security accounted for, observed effects reviewed"' .machine_readable/descriptiles/META.a2ml || MISSING="$MISSING META.a2ml:audit-focus" + grep -q 'compliance-focus = "seams/compromises/exception register, bounded exceptions, anti-drift checks"' .machine_readable/descriptiles/META.a2ml || MISSING="$MISSING META.a2ml:compliance-focus" + grep -q 'effects-evidence = "benchmark execution/results and maintainer status dialogue/review"' .machine_readable/descriptiles/META.a2ml || MISSING="$MISSING META.a2ml:effects-evidence" grep -q 'compliance-tooling = "panic-attack"' .machine_readable/policies/MAINTENANCE-AXES.a2ml || MISSING="$MISSING MAINTENANCE-AXES.a2ml:compliance-tooling" grep -q 'effects-tooling = "ecological checking with sustainabot guidance"' .machine_readable/policies/MAINTENANCE-AXES.a2ml || MISSING="$MISSING MAINTENANCE-AXES.a2ml:effects-tooling" grep -q 'source-human = "docs/governance/MAINTENANCE-CHECKLIST.adoc"' .machine_readable/policies/MAINTENANCE-CHECKLIST.a2ml || MISSING="$MISSING MAINTENANCE-CHECKLIST.a2ml:source-human" @@ -1066,18 +1066,31 @@ validate-rsr: # Validate STATE.a2ml syntax validate-state: - @if [ -f ".machine_readable/STATE.a2ml" ]; then \ - grep -q '^\[metadata\]' .machine_readable/STATE.a2ml && \ - grep -q 'project\s*=' .machine_readable/STATE.a2ml && \ - echo "STATE.a2ml: valid" || echo "STATE.a2ml: INVALID (missing required sections)"; \ + @if [ ! -f ".machine_readable/descriptiles/STATE.a2ml" ]; then \ + echo "No .machine_readable/descriptiles/STATE.a2ml found"; \ + exit 1; \ + elif grep -q '^\[metadata\]' .machine_readable/descriptiles/STATE.a2ml && \ + grep -q 'project\s*=' .machine_readable/descriptiles/STATE.a2ml; then \ + echo "STATE.a2ml: valid"; \ else \ - echo "No .machine_readable/STATE.a2ml found"; \ + echo "STATE.a2ml: INVALID (missing required sections)"; \ + exit 1; \ fi # Validate pipeline doc/A2ML synchronization drift validate-pipeline-drift: ./scripts/check-pipeline-drift.sh . +# Render the shared type-research map for the AsciiDoc README (Graphviz) +type-map: + dot -Tsvg docs/images/type-connections.dot -o docs/images/type-connections.svg + sed -i '2i' docs/images/type-connections.svg + sed -i '2i' docs/images/type-connections.svg + +# Check the boundary between coordination and project implementation +validate-coordination: + ./scripts/check-coordination-boundary.sh + # Validate AI installation guide completeness (finishbot pre-release check) validate-ai-install: #!/usr/bin/env bash @@ -1152,14 +1165,14 @@ validate: validate-rsr validate-state validate-ai-install # Update STATE.a2ml timestamp state-touch: - @if [ -f ".machine_readable/STATE.a2ml" ]; then \ - sed -i 's/last-updated = "[^"]*"/last-updated = "'"$(date +%Y-%m-%d)"'"/' .machine_readable/STATE.a2ml && \ + @if [ -f ".machine_readable/descriptiles/STATE.a2ml" ]; then \ + sed -i 's/last-updated = "[^"]*"/last-updated = "'"$(date +%Y-%m-%d)"'"/' .machine_readable/descriptiles/STATE.a2ml && \ echo "STATE.a2ml timestamp updated"; \ fi # Show current phase from STATE.a2ml state-phase: - @grep -oP 'phase\s*=\s*"\K[^"]+' .machine_readable/STATE.a2ml 2>/dev/null | head -1 || echo "unknown" + @grep -oP 'phase\s*=\s*"\K[^"]+' .machine_readable/descriptiles/STATE.a2ml 2>/dev/null | head -1 || echo "unknown" # ═══════════════════════════════════════════════════════════════════════════════ # GUIX & NIX diff --git a/README.adoc b/README.adoc index a3829cc..a771aa6 100644 --- a/README.adoc +++ b/README.adoc @@ -1,4 +1,4 @@ -// SPDX-License-Identifier: CC-BY-SA-4.0 +// SPDX-License-Identifier: MPL-2.0 // Copyright (c) Jonathan D.A. Jewell = nextgen-typing — Type Theory Pipeline image:https://img.shields.io/badge/OpenSSF-Best_Practices-green?logo=openssourcesecurity[OpenSSF Best Practices,link="https://www.bestpractices.dev/en/projects/new?repo_url=https://github.com/hyperpolymath/nextgen-typing"] @@ -9,7 +9,7 @@ Jonathan D.A. Jewell [TIP] ==== -*AI agents:* read `0-AI-MANIFEST.a2ml` first, then `.machine_readable/6a2/STATE.a2ml`. +*AI agents:* read `0-AI-MANIFEST.a2ml` first, then `.machine_readable/descriptiles/STATE.a2ml`. ==== == What This Is @@ -21,6 +21,43 @@ the cross-project formal-verification proofs in `verification/proofs/`. It documents relationships between type-theoretic repos, tracks the pipeline roadmap, and hosts research artefacts that span multiple projects. +== Type Research: Connections and Meanings + +image::docs/images/type-connections.svg[Echo, Epistemic and Tropical Types connected conceptually to Residual Evidence and Choreographic Types, width=1100] + +*The dashed arrows describe conceptual uses and research obligations.* They +do not certify package dependencies, integration, equivalence or proved +transport. Residual Evidence Types is *work in progress*: its minimal Agda core +now checks presence without value identification, plus narrow Echo and Epistemic +interface comparisons. The guide links the exact proof receipts; the finite +explorer and broader composition/revision programme remain separate obligations. + +[cols="1,3",options="header"] +|=== +|Family |The question it asks +|https://github.com/hyperpolymath/echo-types[Echo Types] +|Which possible origins remain compatible after information loss? +|https://github.com/hyperpolymath/epistemic-types[Epistemic Types] +|Who has access to a claim, with what evidence and soundness conditions? +|https://github.com/hyperpolymath/tropical-types[Tropical Types] +|How do declared resource bounds compose? +|https://github.com/hyperpolymath/residual-evidence-types[Residual Evidence Types] +|Which explanations satisfy the observation and evidence, and what holds for all of them? +|https://github.com/hyperpolymath/choreographic-types[Choreographic Types] +|What is preserved when a global protocol is projected to its participants? +|=== + +link:docs/TYPE-CONNECTIONS.adoc[Read the shared glossary, connection obligations, +ownership guide and first residual milestone]. It distinguishes *residual* +from *residue*, *evidence* from *sound proof*, and *presence* from *value +identification* and *causal role*. These families answer complementary +questions; they are not a ranking of type-system strength. + +Naming note (2026-09-09): `tropical-resource-typing` now resolves on GitHub to +`tropical-types`; the historical `katagoria` name below resolves to +`ideas-to-alphas`. https://github.com/hyperpolymath/kategoria[`kategoria`] is +a distinct language-development repository. + == The Main Chain .... diff --git a/ROADMAP.adoc b/ROADMAP.adoc index fc142b1..561bd17 100644 --- a/ROADMAP.adoc +++ b/ROADMAP.adoc @@ -1,9 +1,27 @@ -// SPDX-License-Identifier: CC-BY-SA-4.0 +// SPDX-License-Identifier: MPL-2.0 // Copyright (c) Jonathan D.A. Jewell = nextgen-typing Roadmap Jonathan D.A. Jewell :toc: +== Type Research Map (2026-09-09) + +* [x] Add a README graphic and shared glossary for Echo, Epistemic, Tropical, + Residual Evidence and Choreographic Types, with explicit arrow meanings. +* [x] Route residual-specific models, proofs and tests to `residual-evidence-types`. +* [x] Build and verify a new minimal residual core in its owning repository; + the separate starter archive remains unrecovered. +* [x] Establish presence without identification, with counterexamples and + explicit nonemptiness, before expanding the calculus. +* [x] Check candidate packaging against actual Echo and a conditional warrant + against actual Epistemic; link the bounded proof receipts in the shared guide. +* [ ] Develop dependency-preserving composition and evidence revision/retraction + in `residual-evidence-types`, then a certified finite checker. +* [ ] Reconcile choreographic "echo loss-grade" vocabulary with the separate + resource-grade, Echo-index and residue-measure meanings. + +See link:docs/TYPE-CONNECTIONS.adoc[connections, meanings and ownership]. + == Near-Term (This Sprint) * [x] Create `katagoria` repo from rsr-template-repo @@ -11,7 +29,7 @@ Jonathan D.A. Jewell * [x] Add `typed-wasm` reference to `nextgen-languages/` monorepo * [x] Write/clean up `docs/ARCHITECTURE.adoc` (pure architecture doc, no briefing framing) * [x] Add `docs/PIPELINE.adoc` (machine-readable A2ML pipeline spec) -* [x] Populate `.machine_readable/6a2/` files with real project state (STATE, META, ECOSYSTEM) +* [x] Populate `.machine_readable/descriptiles/` files with real project state (STATE, META, ECOSYSTEM) * [x] Add nextgen-typing + katagoria ecosystem references to typell and typed-wasm ECOSYSTEM.a2ml * [x] Add ecosystem references to all constituent repos (affinescript, ephapax, tropical-resource-typing, protocol-squisher) * [x] katagoria: first research artefact structure (research/level-candidates/) diff --git a/docs/ARCHITECTURE.adoc b/docs/ARCHITECTURE.adoc index 5ee00bb..e35cd67 100644 --- a/docs/ARCHITECTURE.adoc +++ b/docs/ARCHITECTURE.adoc @@ -1,8 +1,8 @@ -// SPDX-License-Identifier: CC-BY-SA-4.0 +// SPDX-License-Identifier: MPL-2.0 // Copyright (c) Jonathan D.A. Jewell = nextgen-typing: Pipeline Architecture Jonathan D.A. Jewell -2026-04-12 +2026-09-09 :toc: :icons: font @@ -19,6 +19,13 @@ code. It contains: It follows the pattern of `nextgen-languages` and `nextgen-databases`. +The link:TYPE-CONNECTIONS.adoc[type-research map and glossary] positions Echo, +Epistemic, Tropical, Residual Evidence and Choreographic Types by their +questions and explicit research obligations. Its arrows are conceptual; +they do not add an implemented dependency to the historical pipeline below. +The map's name-resolution note distinguishes the old `katagoria` name +(now `ideas-to-alphas`) from the separate `kategoria` project. + == The Main Chain [source] @@ -113,7 +120,7 @@ part of the main chain: Each constituent repo receives: -* A reference to `nextgen-typing` in their `.machine_readable/6a2/ECOSYSTEM.a2ml` +* A reference to `nextgen-typing` in their `.machine_readable/descriptiles/ECOSYSTEM.a2ml` * Their place in the pipeline described in their own docs * The open-ended TypeLL invariant documented in their own ROADMAP diff --git a/docs/PIPELINE.adoc b/docs/PIPELINE.adoc index 9f88a15..19c31b3 100644 --- a/docs/PIPELINE.adoc +++ b/docs/PIPELINE.adoc @@ -1,8 +1,8 @@ -// SPDX-License-Identifier: CC-BY-SA-4.0 +// SPDX-License-Identifier: MPL-2.0 // Copyright (c) Jonathan D.A. Jewell = nextgen-typing: Pipeline Spec (A2ML) Jonathan D.A. Jewell -2026-04-12 +2026-09-09 :toc: :icons: font @@ -16,7 +16,7 @@ tooling and AI agents. Human-oriented architectural narrative remains in ---- [pipeline] id = "hyperpolymath-type-theory-main-chain" -version = "2026-04-12" +version = "2026-09-09" coordination = "nextgen-typing" chain = "katagoria → typell → typed-wasm → PanLL" invariant = "TypeLL is open-ended progressive; L1-L10 is an initial checked set, not a ceiling." @@ -43,15 +43,15 @@ repos = [ [sync-contract] canonical-state-files = [ - ".machine_readable/6a2/STATE.a2ml", - ".machine_readable/6a2/META.a2ml", - ".machine_readable/6a2/ECOSYSTEM.a2ml", + ".machine_readable/descriptiles/STATE.a2ml", + ".machine_readable/descriptiles/META.a2ml", + ".machine_readable/descriptiles/ECOSYSTEM.a2ml", ] -drift-policy = "When pipeline membership or status changes, update README.adoc, docs/ARCHITECTURE.adoc, this file, and the 6a2 state files in the same change set." +drift-policy = "When pipeline membership or status changes, update README.adoc, docs/ARCHITECTURE.adoc, this file, and the descriptiles state files in the same change set." ---- == Consumer Guidance * For narrative context: read `docs/ARCHITECTURE.adoc`. -* For current state: read `.machine_readable/6a2/STATE.a2ml`. -* For ecosystem edges: read `.machine_readable/6a2/ECOSYSTEM.a2ml`. +* For current state: read `.machine_readable/descriptiles/STATE.a2ml`. +* For ecosystem edges: read `.machine_readable/descriptiles/ECOSYSTEM.a2ml`. diff --git a/docs/RSR_OUTLINE.adoc b/docs/RSR_OUTLINE.adoc index 0f8e274..de826a7 100644 --- a/docs/RSR_OUTLINE.adoc +++ b/docs/RSR_OUTLINE.adoc @@ -161,12 +161,13 @@ project/ │ ├── humans.txt │ └── security.txt ├── .machine_readable/ # ALL machine-readable content -│ ├── STATE.a2ml # Project state, progress, blockers -│ ├── META.a2ml # Architecture decisions, governance -│ ├── ECOSYSTEM.a2ml # Ecosystem position, relationships -│ ├── AGENTIC.a2ml # AI agent interaction patterns -│ ├── NEUROSYM.a2ml # Neurosymbolic integration config -│ ├── PLAYBOOK.a2ml # Operational runbook +│ ├── descriptiles/ # Canonical descriptive metadata +│ │ ├── STATE.a2ml # Project state, progress, blockers +│ │ ├── META.a2ml # Architecture decisions, governance +│ │ ├── ECOSYSTEM.a2ml # Ecosystem position, relationships +│ │ ├── AGENTIC.a2ml # AI agent interaction patterns +│ │ ├── NEUROSYM.a2ml # Neurosymbolic integration config +│ │ └── PLAYBOOK.a2ml # Operational runbook │ ├── bot_directives/ # Per-bot rules and constraints │ └── contractiles/ # Policy enforcement contracts │ ├── k9/ # Security levels (Kennel/Yard/Hunt) @@ -217,7 +218,7 @@ project/ * `Justfile` * `README.adoc` * `LICENSE` (MPL-2.0) -* `.machine_readable/6a2/STATE.a2ml` +* `.machine_readable/descriptiles/STATE.a2ml` * `.well-known/security.txt` * `.well-known/ai.txt` * `.well-known/humans.txt` diff --git a/docs/TYPE-CONNECTIONS.adoc b/docs/TYPE-CONNECTIONS.adoc new file mode 100644 index 0000000..c403e36 --- /dev/null +++ b/docs/TYPE-CONNECTIONS.adoc @@ -0,0 +1,214 @@ +// SPDX-License-Identifier: MPL-2.0 +// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell += Type research: connections and shared meanings +:toc: +:icons: font + +This is the shared reading guide for the five research families in the map. +It coordinates vocabulary and ownership; the owning repositories define +their formal interfaces and carry their proof evidence. + +image::images/type-connections.svg[Five type research families connected by explicitly conceptual arrows, width=1100] + +*Read every dashed arrow as a conceptual use or a proposed research task.* +An arrow does not assert a package dependency, a checked bridge, an +equivalence, or a theorem. Residual Evidence Types now has a checked minimal +Agda core and two narrow interface comparisons, described below with proof +receipts. Those results do not discharge every obligation represented by an arrow. + +== What each family means + +[cols="1,2,2",options="header"] +|=== +|Family and owner |Question and object |Boundary + +|https://github.com/hyperpolymath/echo-types[Echo Types] +|Which possible origins lie over an output after a transformation? +`Echo f y = Σ (x : A), f x ≡ y` retains a witness in the ordinary preimage +fibre. The research concerns structured information loss and retained distinctions. +|An output need not identify its actual origin. A numeric measure of a +residue does not determine the residue's structure. + +|https://github.com/hyperpolymath/epistemic-types[Epistemic Types] +|From which standpoint is a claim available, and with what evidence? +`E κ A` indexes access to a claim by a standpoint; warrants record evidence, +and factivity or soundness requires additional structure. +|Possessing evidence is not automatically a proof of its claim. Belief, +knowledge and a sound warrant have different interfaces. + +|https://github.com/hyperpolymath/tropical-types[Tropical Types] +|How do resource bounds compose? A declared resource algebra supplies +operations and laws: max-plus can combine alternatives with `max` and +sequential costs with `+`; bottleneck paths use a different algebra. +|The algebra and cost semantics must be stated. A bound is neither a +probability nor the identity of an information residue. + +|https://github.com/hyperpolymath/residual-evidence-types[Residual Evidence Types] +|Which worlds satisfy both an observation and its evidence constraints? +`Candidate observe r E = Σ (w : W), (observe w ≡ r) × E w`. +Presence and value identification are questions over all admissible worlds. +|The world is not recovered just by constructing a candidate. Real-world +soundness also needs the premise that the actual world is admissible. +The formal library is work in progress. + +|https://github.com/hyperpolymath/choreographic-types[Choreographic Types] +|What happens to retained distinctions, resource bounds and warrants when +a global interaction protocol is projected to local participants? +|The general K-CUT result is open in the reviewed project description. +A causal-order frontier called a cut is not Gentzen cut-elimination; +it is also not a statistical causal-identification result. +|=== + +These are complementary research questions, not successive ranks in a +universal hierarchy of type-system strength. They may be expressible using +ordinary dependent, refinement, modal or graded constructions. A name alone +does not establish a new primitive type or a novelty claim. + +== Shared glossary + +[cols="1,3",options="header"] +|=== +|Term |Meaning in this guide +|Observation |The result of a declared observation function. Keeping only +its sign or magnitude changes that function and can merge distinctions. +|Fibre / fiber |Origins paired with evidence that the observation function +maps them to the specified output. The two spellings mean the same thing. +|Candidate world |One world with evidence of observation compatibility and +the declared constraints. It is an admissible explanation, not an assertion +that this world actually occurred. +|Residual |A discrepancy relative to a declared model. In the imported +example it is `r = u + n`. Additivity is an assumption of that example. +|Residue |Information retained after a transformation. An Echo residue is +not synonymous with a numerical residual or an error term. +|Evidence constraint |A predicate restricting candidate worlds. Choosing +a bound in an explorer does not establish that real observations obey it. +|Standpoint |The agent, observer or evidence state from which a claim is +available. It is an explicit index, not necessarily a probability. +|Warrant |Evidence for a claim from a standpoint. Soundness needs a separate +map from that evidence to the specified claim meaning. +|Soundness |A stated guarantee connecting evidence or a successful check to +the meaning of a claim, under explicit premises. +|Presence |Every admissible world has a nonzero contribution. A meaningful +case also requires evidence that at least one world is admissible. +|Value identification |The queried contribution has the same value in every +admissible world. This does not identify a source or its causal role. +|Confounding |A prospective causal specialisation, requiring a causal model +and its identification assumptions. An unresolved additive contribution alone +does not establish a confounder. +|Inconsistency |No candidate satisfies the declared model and constraints. +The explorer reports a conflict and issues no presence or identification claim; +it does not use an empty candidate set as a useful warrant for every claim. +|Resource grade |An element of a declared resource algebra used for compositional +usage or cost accounting. Which operations compose which behaviours is explicit. +|Echo index |An index of retained information or allowed degradation. It is +distinct from a resource grade and from a numerical measure of a residue. +|Residue measure |An observation of retained information into a measuring +domain. Equal measured values need not mean equal retained information. +|=== + +== What each connection asks us to establish + +[cols="1,2,2",options="header"] +|=== +|Connection |Conceptual relationship |Evidence needed for a stronger claim +|Echo → Residual Evidence +|Refine the observation fibre with the evidence predicate `E`. +|The first core checks an encoding into `Echo.Echo` and both round trips. +Coarsening and dependency-preserving composition laws remain open. +|Epistemic → Residual Evidence +|Make the meaning and evidence obligations of candidate-wide claims explicit. +|The first core checks a `SoundWarrant` for a candidate-wide claim, with an +inhabited case and explicit actual-world premises. Evidence revision and +retraction remain open. +|Echo → Choreographic +|Track the distinctions retained by projection to participants. +|A projection model and correspondence theorem. An informal loss number +cannot stand in for the structure of an Echo residue. +|Epistemic → Choreographic +|Transport warrants with declared standpoint and soundness conditions. +|The relevant K-CUT-WARRANT statement and its proof, including its side conditions. +|Tropical → Choreographic +|Compose bounds for interactions using a stated resource algebra. +|A grading semantics and a projection theorem. A result in another proof +assistant needs a proved correspondence or a port with its laws re-proved. +|=== + +The Choreographic README reviewed for this guide uses the phrase +"echo loss-grade". The Echo foundation contract explicitly separates Echo +indices, residue measures and resource grades. This map preserves that +distinction; reconciling the choreographic interface is an open coordination +task, not an equivalence asserted here. + +== Where things belong + +* `nextgen-typing`: this map, the shared glossary, ownership routing, comparisons + and explicitly cross-project integration obligations. +* `residual-evidence-types`: the residual model, research plan, explorer, + Agda core, and tests or proofs specific to that model. +* `echo-types`, `epistemic-types`, `tropical-types`, `choreographic-types`: + each family's definitions, implementations and own proof evidence. +* `kategoria`: language-development experiments. It is a separate project + from the old `katagoria` repository name, which GitHub now resolves to + `ideas-to-alphas`. +* `typell`: verification-kernel implementation; `typed-wasm`: target and ABI + work; `panll`: the consuming environment. A conceptual connection in this + guide does not establish that any family is integrated into these projects. + +The machine-readable ownership rules are in +link:../.machine_readable/bot_directives/placement.a2ml[placement.a2ml]. + +== First residual milestone: checked, with limits + +The first argument is *presence without identification*. In natural numbers, +`u+n=2` alone admits both `(0,2)` and `(2,0)`. Adding `n≤1` proves `u≠0`, +but `(1,1)` and `(2,0)` still disagree on the value of `u`. Adding `u=0` +then makes the constraints inconsistent, so no inhabited case can be built. + +The new core also checks ordinary evidence-refined fibre round trips, +conditional actual-world soundness, and claim transport under evidence +refinement. Three deliberately invalid modules must be rejected by Agda. +Both actual sibling interfaces are imported by the comparison modules: +Echo's fibre packaging round-trips, and Epistemic's `SoundWarrant` requires +explicit actual-world premises. + +https://github.com/hyperpolymath/residual-evidence-types/blob/4325198c10e2e689f084c2f64a27213685a1ffd2/PROOF-STATUS.adoc[The proof record at the checked revision] +lists the theorem names, commands, pinned sibling revisions and standard-library +warnings. The https://github.com/hyperpolymath/residual-evidence-types/actions/runs/34400282291[hosted Agda proof job] +passed the core, all three rejection controls and both comparisons on 2026-09-09. +This is newly written work; the separate starter archive mentioned in the +imported assessment has not been recovered. + +Next, investigate dependency-preserving composition and evidence revision or +retraction, then prove correspondence with a finite checker. The JavaScript +explorer uses bounded signed integers and has no proved correspondence to the +natural-number core. Causal specialisations and probability adapters require +their own models and obligations. + +== Sources and review boundary + +Reviewed on 2026-09-09: the local README files for the six type-set projects +`echo-types`, `epistemic-types`, `tropical-types`, `choreographic-types`, +`kategoria` and `typell`; the imported residual assessment and explorer; and +the coordination repository's placement, architecture and roadmap documents. +The residual core and its two direct comparison modules were checked locally +and in the linked hosted job with Agda 2.6.4.3 under `--safe --without-K`. +This is a bounded result: the complete constituent proof suites were not +rerun, and unrelated local Epistemic work is outside the receipt. + +Primary project entry points: + +* https://github.com/hyperpolymath/echo-types[Echo Types README and foundation contract] +* https://github.com/hyperpolymath/epistemic-types[Epistemic Types README] +* https://github.com/hyperpolymath/tropical-types[Tropical Types README] +* https://github.com/hyperpolymath/choreographic-types[Choreographic Types README] +* https://github.com/hyperpolymath/residual-evidence-types/blob/main/residual-evidence-assessment.md[Imported residual assessment] + +GitHub repository API lookups on that date resolved `tropical-resource-typing` +to `tropical-types` and `katagoria` to `ideas-to-alphas`, while `kategoria` +resolved to its own repository. The historical pipeline documents retain +the `katagoria` spelling; do not silently conflate it with `kategoria`. + +The graphic is a checked-in SVG so it displays in the AsciiDoc README without +JavaScript or a diagram service. Its editable source is +link:images/type-connections.dot[type-connections.dot]. Rebuild it with +`just type-map` (Graphviz required). diff --git a/docs/images/type-connections.dot b/docs/images/type-connections.dot new file mode 100644 index 0000000..f8f1d3e --- /dev/null +++ b/docs/images/type-connections.dot @@ -0,0 +1,42 @@ +// SPDX-License-Identifier: MPL-2.0 +// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell +digraph TypeConnections { + graph [rankdir=TB, bgcolor="#f5f7fb", pad="0.35", nodesep="0.45", ranksep="0.8", splines=polyline, + fontname="DejaVu Sans", fontsize=22, fontcolor="#17243b", labelloc=t, + label="Type research: questions and connections\n\nnextgen-typing · coordination map · September 2026", + comment="SPDX-License-Identifier: MPL-2.0; SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell"]; + node [shape=box, style="rounded,filled", fillcolor="#ffffff", color="#a6b4c9", + fontname="DejaVu Sans", fontsize=13, fontcolor="#17243b", margin="0.22,0.2", penwidth=1.4]; + edge [style=dashed, color="#61738e", fontcolor="#465773", fontname="DejaVu Sans", fontsize=10, arrowsize=0.65]; + + subgraph foundations { + rank=same; + echo [label=<Echo Types

Which origins remain compatible
after information loss?

echo-types · Agda research library>, + URL="https://github.com/hyperpolymath/echo-types"]; + epistemic [label=<Epistemic Types

Who has access to a claim,
with what evidence and soundness?

epistemic-types · Agda prototype>, + URL="https://github.com/hyperpolymath/epistemic-types"]; + tropical [label=<Tropical Types

How do declared resource
bounds compose?

tropical-types · Lean research library>, + URL="https://github.com/hyperpolymath/tropical-types"]; + } + + subgraph research { + rank=same; + residual [color="#bf7515", fillcolor="#fff4de", penwidth=2, + label=<Residual Evidence Types

Which explanations satisfy the observation
and evidence, and what holds for all of them?

WORK IN PROGRESS · minimal Agda core checked
residual-evidence-types · finite explorer separate>, + URL="https://github.com/hyperpolymath/residual-evidence-types"]; + choreographic [fillcolor="#ebf3fd", color="#7f9bbb", + label=<Choreographic Types

What is preserved when a global protocol
is projected to its participants?

choreographic-types · research programme
K-CUT remains open>, + URL="https://github.com/hyperpolymath/choreographic-types"]; + } + + echo -> residual [label="refine the fibre\nwith evidence"]; + epistemic -> residual [label="state claim meanings\nand soundness obligations"]; + echo -> choreographic [label="retain distinctions\nthrough projection"]; + epistemic -> choreographic [label="transport warrants\nunder conditions"]; + tropical -> choreographic [label="compose bounds\nfor interactions"]; + + boundaries [shape=box, color="#c7d1df", fillcolor="#e8edf4", + label=<Keep the meanings separate

Resource grade ≠ Echo index ≠ residue measure
Evidence token ≠ sound proof  ·  Presence ≠ identified value ≠ causal role

Dashed arrows show conceptual use or proposed research.
They do not certify imports, integration, equivalence, or proved transport.>]; + residual -> boundaries [style=invis]; + choreographic -> boundaries [style=invis]; +} diff --git a/docs/images/type-connections.svg b/docs/images/type-connections.svg new file mode 100644 index 0000000..e87eeee --- /dev/null +++ b/docs/images/type-connections.svg @@ -0,0 +1,133 @@ + + + + + + + + + +TypeConnections + +Type research: questions and connections +nextgen-typing · coordination map · September 2026 + + +echo + + +Echo Types +Which origins remain compatible +after information loss? +echo-types · Agda research library + + + + + +residual + + +Residual Evidence Types +Which explanations satisfy the observation +and evidence, and what holds for all of them? +WORK IN PROGRESS + · minimal Agda core checked +residual-evidence-types · finite explorer separate + + + + + +echo->residual + + +refine the fibre +with evidence + + + +choreographic + + +Choreographic Types +What is preserved when a global protocol +is projected to its participants? +choreographic-types · research programme +K-CUT remains open + + + + + +echo->choreographic + + +retain distinctions +through projection + + + +epistemic + + +Epistemic Types +Who has access to a claim, +with what evidence and soundness? +epistemic-types · Agda prototype + + + + + +epistemic->residual + + +state claim meanings +and soundness obligations + + + +epistemic->choreographic + + +transport warrants +under conditions + + + +tropical + + +Tropical Types +How do declared resource +bounds compose? +tropical-types · Lean research library + + + + + +tropical->choreographic + + +compose bounds +for interactions + + + +boundaries + +Keep the meanings separate +Resource grade ≠ Echo index ≠ residue measure +Evidence token ≠ sound proof  ·  Presence ≠ identified value ≠ causal role +Dashed arrows show conceptual use or proposed research. +They do not certify imports, integration, equivalence, or proved transport. + + + + + diff --git a/docs/practice/AI-CONVENTIONS.adoc b/docs/practice/AI-CONVENTIONS.adoc index 1ff18e1..6f3de4e 100644 --- a/docs/practice/AI-CONVENTIONS.adoc +++ b/docs/practice/AI-CONVENTIONS.adoc @@ -17,12 +17,12 @@ See `AGENTS.md` for the routing table. ## Session Startup 1. Read `0-AI-MANIFEST.a2ml` FIRST (mandatory gatekeeper). -2. Read `.machine_readable/6a2/STATE.a2ml` for current status and blockers. -3. Read `.machine_readable/anchors/ANCHOR.a2ml` for canonical authority boundaries. +2. Read `.machine_readable/descriptiles/STATE.a2ml` for current status and blockers. +3. Read `.machine_readable/descriptiles/anchor/ANCHOR.a2ml` for canonical authority boundaries. 4. Read `.machine_readable/policies/MAINTENANCE-AXES.a2ml` for maintenance/audit sequencing. 5. Read `.machine_readable/policies/MAINTENANCE-CHECKLIST.a2ml` for baseline controls. 6. Read `.machine_readable/policies/SOFTWARE-DEVELOPMENT-APPROACH.a2ml` for execution order. -7. Read `.machine_readable/AGENTIC.a2ml` for agent constraints. +7. Read `.machine_readable/descriptiles/AGENTIC.a2ml` for agent constraints. ## License @@ -30,7 +30,7 @@ See `AGENTS.md` for the routing table. - Fallback (platform-required only): MPL-2.0 with comment explaining why. - NEVER use AGPL-3.0. - Preserve third-party licenses verbatim. -- Every source file needs `# SPDX-License-Identifier: CC-BY-SA-4.0`. +- Every original source file needs `SPDX-License-Identifier: MPL-2.0` in its language's comment syntax. ## Author Attribution @@ -61,7 +61,7 @@ MAINTENANCE-CHECKLIST.a2ml, or SOFTWARE-DEVELOPMENT-APPROACH.a2ml in the reposit | Banned | Use Instead | |---------------------|--------------------| | TypeScript | ReScript | -| Node.js / npm / bun | Deno | +| Node.js / npm / Deno | Bun | | Go | Rust | | Python | Julia / Rust | @@ -90,9 +90,9 @@ Use `just` (Justfile) for all build, test, lint, and format tasks. ## References - `0-AI-MANIFEST.a2ml` -- universal AI entry point -- `.machine_readable/AGENTIC.a2ml` -- agent permissions and constraints -- `.machine_readable/6a2/STATE.a2ml` -- current project state -- `.machine_readable/anchors/ANCHOR.a2ml` -- canonical authority and policy boundary +- `.machine_readable/descriptiles/AGENTIC.a2ml` -- agent permissions and constraints +- `.machine_readable/descriptiles/STATE.a2ml` -- current project state +- `.machine_readable/descriptiles/anchor/ANCHOR.a2ml` -- canonical authority and policy boundary - `.machine_readable/policies/MAINTENANCE-AXES.a2ml` -- canonical axis sequencing and audit requirements - `.machine_readable/policies/MAINTENANCE-CHECKLIST.a2ml` -- baseline maintenance checklist policy - `.machine_readable/policies/SOFTWARE-DEVELOPMENT-APPROACH.a2ml` -- axis execution approach policy diff --git a/docs/wikis/Project-Status.adoc b/docs/wikis/Project-Status.adoc index b2f7029..29f7efe 100644 --- a/docs/wikis/Project-Status.adoc +++ b/docs/wikis/Project-Status.adoc @@ -5,7 +5,7 @@ :icons: font Dated status entries for nextgen-typing. Newest first. Canonical -machine-readable state lives in `.machine_readable/6a2/STATE.a2ml`. +machine-readable state lives in `.machine_readable/descriptiles/STATE.a2ml`. == 2026-06-12 — Estate standardization + governance checkpoint diff --git a/scripts/check-pipeline-drift.sh b/scripts/check-pipeline-drift.sh index 6ad3520..fd4c9c8 100755 --- a/scripts/check-pipeline-drift.sh +++ b/scripts/check-pipeline-drift.sh @@ -3,7 +3,7 @@ # Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) # # Pipeline drift guard for nextgen-typing. -# Ensures canonical pipeline docs and 6a2 machine-readable state stay aligned. +# Ensures canonical pipeline docs and descriptiles machine-readable state stay aligned. set -euo pipefail @@ -13,9 +13,9 @@ ERRORS=0 README="$REPO_ROOT/README.adoc" ARCHITECTURE="$REPO_ROOT/docs/ARCHITECTURE.adoc" PIPELINE="$REPO_ROOT/docs/PIPELINE.adoc" -STATE="$REPO_ROOT/.machine_readable/6a2/STATE.a2ml" -META="$REPO_ROOT/.machine_readable/6a2/META.a2ml" -ECOSYSTEM="$REPO_ROOT/.machine_readable/6a2/ECOSYSTEM.a2ml" +STATE="$REPO_ROOT/.machine_readable/descriptiles/STATE.a2ml" +META="$REPO_ROOT/.machine_readable/descriptiles/META.a2ml" +ECOSYSTEM="$REPO_ROOT/.machine_readable/descriptiles/ECOSYSTEM.a2ml" CANON_CHAIN="katagoria → typell → typed-wasm → PanLL" CHAIN_REGEX='katagoria[[:space:]]*→[[:space:]]*typell[[:space:]]*→[[:space:]]*typed-wasm[[:space:]]*→[[:space:]]*PanLL'