From ddb6f1998f358446da97d7d7234707dcb590ec66 Mon Sep 17 00:00:00 2001
From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com>
Date: Sat, 16 May 2026 22:24:58 +0100
Subject: [PATCH] policy(LANGUAGE-POLICY): codify Interface & Architecture Law
 (v1.2.0)

Normative, estate-wide, day-1 law:
- ABI=Idris2, API+FFI=Zig; Rust/SPARK is app-logic only and never the
  abi/api/ffi layer or a migration target; '-> Rust' migration docs are
  themselves off-policy drift (canonical target is Zig)
- V-lang only when it is Coq (outside the sanctioned v-ecosystem /
  awesome-v); V-stub-gen recipes are re-emergence engines, delete them
- Strict typed boundaries: every cross-language/cross-trust boundary =
  Idris2 correctness contract + Zig transaction interface (exemplars:
  snifs for NIFs, typed-wasm for WASM)
- No gatekeeperless gateways: every gateway fronts a policy gate
  (distinct from the social 'graduated trust' contribution model)

Adds normative section + v1.2.0 amendment + header rev bump.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
---
 .../spec/LANGUAGE-POLICY.adoc                 | 59 +++++++++++++++++--
 1 file changed, 54 insertions(+), 5 deletions(-)

diff --git a/rhodium-standard-repositories/spec/LANGUAGE-POLICY.adoc b/rhodium-standard-repositories/spec/LANGUAGE-POLICY.adoc
index 03d221d6..afbaa95e 100644
--- a/rhodium-standard-repositories/spec/LANGUAGE-POLICY.adoc
+++ b/rhodium-standard-repositories/spec/LANGUAGE-POLICY.adoc
@@ -3,17 +3,18 @@
 
 = RSR Language Policy
 :author: Jonathan D.A. Jewell (hyperpolymath)
-:revnumber: 1.1.0
-:revdate: 2026-04-10
+:revnumber: 1.2.0
+:revdate: 2026-05-16
 :toc: left
 :icons: font
 :source-repo: https://github.com/hyperpolymath/cccp
 
 [NOTE]
 ====
-*Version Status*: v1.1.0 — allowed/banned lists amended 2026-04-10. See §Amendments
-at the bottom of this document for the rationale and the full change list. The
-prior v1.0.0 freeze was lifted on the same date.
+*Version Status*: v1.2.0 — codifies the Interface & Architecture Law
+(ABI=Idris2, API+FFI=Zig; strict typed boundaries; no gatekeeperless gateways)
+as a normative section, 2026-05-16. v1.1.0 amended the allowed/banned lists
+2026-04-10. See §Amendments at the bottom for rationale and the full change list.
 ====
 
 == Terminology: "Rust" means "Rust/SPARK"
@@ -239,6 +240,54 @@ the reach order is:
      consideration)
    * `Node.js` as a standalone runtime — replaced by Deno
 
+== Interface & Architecture Law (NORMATIVE)
+
+This is a day-1, estate-wide structural law. It is non-negotiable and applies
+to *every* repository.
+
+=== Layer languages
+
+* **ABI layer → Idris2** (`src/abi/*.idr`): formal types + proofs. Always.
+* **FFI layer → pure Zig** (`ffi/zig/`). Always — since day 1.
+* **API layer → pure Zig** (`src/api/zig/`). Always — since V was dropped for APIs.
+
+Rust/SPARK is *application* logic only (per §Terminology); it is **never** the
+ABI, API, or FFI layer, and is **never** the target of an abi/api/ffi migration.
+C is never an estate API/ABI/FFI layer either. A `MIGRATION.adoc`, `CLAUDE.md`,
+manifest comment, or build file that says "→ Rust" / "canonical Rust rewrite of
+the API" is **itself off-policy drift**: the canonical target is the Zig
+implementation. Stray `src/api/rust/` API crates are debt to remove, not a
+destination. Consumers may still *call* the C ABI from any language — that is
+consumer-side binding, not the layer implementation.
+
+=== V-lang only when it is Coq
+
+V-lang is banned (see §Banned Languages); the migration target is **Zig, never
+Rust**. The sanctioned exception is the `developer-ecosystem/v-ecosystem/`
+subtree (and `awesome-v`, a curated list — never touched). Outside those, a `.v`
+file or "V" reference in code, docs, `CLAUDE.md`, `Justfile`, `Containerfile`,
+or `flake.nix` is acceptable **only when it is a Coq/Rocq proof**
+(`Require Import` / `Theorem` / `Qed.`). All other V references are drift to
+remove. V-stub-generation recipes are *re-emergence engines* and must be
+deleted, not merely disabled.
+
+=== Strict typed boundaries
+
+Every cross-language or cross-trust boundary MUST be type-protected and
+correctness-gated: an **Idris2 correctness contract** (proven ABI/protocol) plus
+a **Zig transaction interface** (the marshalling / C-ABI / wire layer). This
+covers in-process FFI, NIFs (exemplar: the `snifs` repo), WASM boundaries
+(exemplar: the `typed-wasm` repo), API gateways, gRPC/GraphQL/REST edges, DB and
+service connectors, and any (de)serialisation trust boundary. An
+untyped/unproven boundary is non-conformant and blocks.
+
+=== No gatekeeperless gateways
+
+Every gateway / API edge MUST front a policy gate (authentication + entitlement
++ rate-limiting). A gateway without a gatekeeper is a defect, not a later-phase
+nicety. (This is a *runtime access-control* rule and is distinct from the
+social "graduated trust without gatekeeping" contribution model.)
+
 == Machine-Readable Policy
 
 See link:../spec.scm/language-policy.scm[spec.scm/language-policy.scm] for tooling integration.