Merge branch 'main' into claude/practical-newton-9eFe2

Author: hyperpolymath

.clinerules

@@ -0,0 +1,24 @@
+# SPDX-License-Identifier: MPL-2.0
+# Cline rules for nextgen-typing. Full rules: AGENTS.md / CLAUDE.md.
+
+# ⛔ COORDINATION REPO — NOT A CODE REPO.
+# nextgen-typing documents and connects the type-theory pipeline
+# (katagoria → typell → typed-wasm → PanLL). It does NOT hold compiler,
+# kernel, language, or single-project code — including single-project proofs,
+# benchmarks, and tests.
+#
+# Before creating ANY implementation file or single-project proof here: STOP.
+# Put it in the owning repo. Routing table:
+#   .machine_readable/bot_directives/placement.a2ml   (authoritative)
+#   AGENTS.md                                          (human-readable)
+# CI enforces this: scripts/check-coordination-boundary.sh
+#
+# Only these belong here: coordination/architecture docs, .machine_readable/
+# 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.
+# 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.
+# No believe_me / assert_total / postulate / sorry / Admitted / unsafeCoerce.

.cursorrules

@@ -0,0 +1,24 @@
+# SPDX-License-Identifier: MPL-2.0
+# Cursor rules for nextgen-typing. Full rules: AGENTS.md / CLAUDE.md.
+
+# ⛔ COORDINATION REPO — NOT A CODE REPO.
+# nextgen-typing documents and connects the type-theory pipeline
+# (katagoria → typell → typed-wasm → PanLL). It does NOT hold compiler,
+# kernel, language, or single-project code — including single-project proofs,
+# benchmarks, and tests.
+#
+# Before creating ANY implementation file or single-project proof here: STOP.
+# Put it in the owning repo. Routing table:
+#   .machine_readable/bot_directives/placement.a2ml   (authoritative)
+#   AGENTS.md                                          (human-readable)
+# CI enforces this: scripts/check-coordination-boundary.sh
+#
+# Only these belong here: coordination/architecture docs, .machine_readable/
+# 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.
+# 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.
+# No believe_me / assert_total / postulate / sorry / Admitted / unsafeCoerce.

.github/copilot-instructions.md

@@ -7,6 +7,18 @@ Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 
 # Copilot Instructions
 
+## ⛔ Before Writing Anything — Placement Boundary
+
+`nextgen-typing` is a **coordination repo**, not a code repo. Do NOT add
+compiler/application code or single-project proofs here. If content implements
+or proves something about ONE project, put it in that project's repo. Routing
+table: `.machine_readable/bot_directives/placement.a2ml` (enforced in CI by
+`scripts/check-coordination-boundary.sh`). Full guidance: `AGENTS.md`.
+
+Only these belong here: coordination/architecture docs, `.machine_readable/`
+state, estate governance/CI scaffold, and CROSS-project proofs (importing ≥2
+constituent repos) under `verification/proofs/`.
+
 ## Before Writing Code
 
 - Read `0-AI-MANIFEST.a2ml` in the repo root for canonical file locations.
@@ -47,12 +59,6 @@ Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 - Name the file `Containerfile`, never `Dockerfile`.
 - Base image: `cgr.dev/chainguard/wolfi-base:latest`.
 
-## ABI/FFI
-
-- ABI definitions in Idris2 (`src/interface/abi/`).
-- FFI implementations in Zig (`src/interface/ffi/`).
-- Generated C headers in `src/interface/generated/`.
-
 ## State Files
 
 Never create these in the repo root:

.github/workflows/coordination-boundary.yml

@@ -0,0 +1,32 @@
+# SPDX-License-Identifier: MPL-2.0
+# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+#
+# Coordination-boundary guard: nextgen-typing must stay docs + machine-readable
+# state + estate scaffold + CROSS-project proofs only — no compiler/application
+# code and no single-project proofs. Routing table:
+#   .machine_readable/bot_directives/placement.a2ml
+name: Coordination Boundary
+
+on:
+  push:
+    branches: [main, master, develop]
+  pull_request:
+    branches: [main, master, develop]
+
+permissions:
+  contents: read
+
+concurrency:
+  group: coord-boundary-${{ github.ref }}
+  cancel-in-progress: true
+
+jobs:
+  boundary:
+    runs-on: ubuntu-latest
+    timeout-minutes: 5
+    permissions:
+      contents: read
+    steps:
+      - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
+      - name: Enforce coordination boundary
+        run: bash scripts/check-coordination-boundary.sh

.github/workflows/governance.yml

@@ -0,0 +1,16 @@
+# SPDX-License-Identifier: PMPL-1.0-or-later
+name: Governance
+
+on:
+  push:
+    branches: [main, master]
+  pull_request:
+    branches: [main, master]
+  workflow_dispatch:
+
+permissions:
+  contents: read
+
+jobs:
+  governance:
+    uses: hyperpolymath/standards/.github/workflows/governance-reusable.yml@5a93d9d57cc04de4002d6d0ecd336fc7a8698910

.github/workflows/guix-nix-policy.yml

@@ -1,6 +1,15 @@
 # SPDX-License-Identifier: MPL-2.0
 name: Guix/Nix Package Policy
-on: [push, pull_request]
+on:
+  push:
+    branches: [main, master]
+  pull_request:
+
+# Estate guardrail: scope push to default branches (PR fires once, not
+# push+PR) and cancel superseded runs. Safe — read-only PR check.
+concurrency:
+  group: ${{ github.workflow }}-${{ github.ref }}
+  cancel-in-progress: true
 
 permissions:
   contents: read

.github/workflows/hypatia-scan.yml

@@ -1,7 +1,4 @@
-# SPDX-License-Identifier: MPL-2.0
-# Thin wrapper around hyperpolymath/standards hypatia-scan-reusable.yml.
-# See standards#191 for the reusable's purpose and design.
-
+# SPDX-License-Identifier: PMPL-1.0-or-later
 name: Hypatia Security Scan
 
 on:
@@ -13,18 +10,10 @@ on:
     - cron: '0 0 * * 0'
   workflow_dispatch:
 
-# Estate guardrail: cancel superseded runs so re-pushes don't pile up.
-concurrency:
-  group: ${{ github.workflow }}-${{ github.ref }}
-  cancel-in-progress: true
-
 permissions:
   contents: read
-  security-events: write
-  pull-requests: write
+  security-events: read
 
 jobs:
-  hypatia:
-    timeout-minutes: 30
-    uses: hyperpolymath/standards/.github/workflows/hypatia-scan-reusable.yml@915139d73560e65a8240b8fc7768698658502c89
-    secrets: inherit
+  scan:
+    uses: hyperpolymath/standards/.github/workflows/hypatia-scan-reusable.yml@5a93d9d57cc04de4002d6d0ecd336fc7a8698910

.github/workflows/npm-bun-blocker.yml

@@ -1,6 +1,15 @@
 # SPDX-License-Identifier: MPL-2.0
 name: NPM/Bun Blocker
-on: [push, pull_request]
+on:
+  push:
+    branches: [main, master]
+  pull_request:
+
+# Estate guardrail: scope push to default branches (PR fires once, not
+# push+PR) and cancel superseded runs. Safe — read-only PR check.
+concurrency:
+  group: ${{ github.workflow }}-${{ github.ref }}
+  cancel-in-progress: true
 
 permissions:
   contents: read

.github/workflows/quality.yml

@@ -1,6 +1,15 @@
 # SPDX-License-Identifier: MPL-2.0
 name: Code Quality
-on: [push, pull_request]
+on:
+  push:
+    branches: [main, master]
+  pull_request:
+
+# Estate guardrail: scope push to default branches (PR fires once, not
+# push+PR) and cancel superseded runs. Safe — read-only PR check.
+concurrency:
+  group: ${{ github.workflow }}-${{ github.ref }}
+  cancel-in-progress: true
 
 
 permissions: