Audit evidence claims and disable unsupported product paths

.clinerules

@@ -1,43 +1,26 @@
 # SPDX-License-Identifier: MPL-2.0
 # Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
-# Authoritative source: docs/AI-CONVENTIONS.md
+# Authoritative guidance: docs/AI-CONVENTIONS.adoc
 
-# STARTUP: Read 0-AI-MANIFEST.a2ml first, then .machine_readable/STATE.a2ml.
+# STARTUP
+# Read 0-AI-MANIFEST.a2ml, .machine_readable/6a2/STATE.a2ml, and
+# .machine_readable/6a2/anchor/ANCHOR.a2ml.
 
-# LICENSE
-# All original code: MPL-2.0.
-# Never AGPL-3.0. MPL-2.0 only as platform-required fallback.
-# SPDX header required on every source file.
-# Copyright: Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
-
-# STATE FILES (.machine_readable/ ONLY)
-# Never create in repo root: STATE.a2ml, META.a2ml, ECOSYSTEM.a2ml,
-# AGENTIC.a2ml, NEUROSYM.a2ml, PLAYBOOK.a2ml.
-# The .machine_readable/ directory is the single source of truth.
-
-# BANNED PATTERNS
-# Idris2: believe_me, assert_total, assert_smaller, unsafePerformIO
-# Haskell: unsafeCoerce, unsafePerformIO, undefined, error
-# OCaml: Obj.magic, Obj.repr, Obj.obj
-# Coq: Admitted
-# Lean: sorry
-# Rust: transmute (unless FFI with // SAFETY: comment)
+# EVIDENCE
+# Distinguish Idris2 model checks, Zig tests, ABI conformance, binding links,
+# and protocol interoperability. Source-pattern scripts are not proofs.
+# Record missing tools and explicit skips; never report an unrun check as passing.
 
-# BANNED LANGUAGES
-# TypeScript -> ReScript
-# Node.js / npm / bun -> Deno
-# Go -> Rust
-# Python -> Julia or Rust
+# FAIL-CLOSED
+# Do not report authentication, crypto, or backend operations as successful
+# without required secrets/material and a verified implementation.
+# Do not build, sign, push, or deploy the current container scaffolding.
 
-# CONTAINERS
-# Runtime: Podman (never Docker).
-# File: Containerfile (never Dockerfile).
-# Base: cgr.dev/chainguard/wolfi-base:latest or cgr.dev/chainguard/static:latest.
+# LANGUAGES
+# Idris2 and Zig are used in selected packages. Existing binding languages are
+# permitted as source inventory; their operational support is unverified.
+# Do not add a new runtime/language without documenting scope and toolchains.
 
-# ABI/FFI
-# ABI: Idris2 with dependent types (src/abi/).
-# FFI: Zig with C ABI (ffi/zig/).
-# Headers: generated/abi/.
-
-# BUILD: Use just (justfile) for all tasks.
-# STYLE: Descriptive names. Document all files. SPDX headers everywhere.
+# LICENSE
+# Preserve file-level SPDX and third-party notices. Original project source is
+# generally MPL-2.0. Follow docs/AI-CONVENTIONS.adoc for details.

.cursorrules

@@ -1,47 +1,22 @@
 # SPDX-License-Identifier: MPL-2.0
 # Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
-# Authoritative source: docs/AI-CONVENTIONS.md
+# Authoritative guidance: docs/AI-CONVENTIONS.adoc
 
-# Read 0-AI-MANIFEST.a2ml in the repo root FIRST for canonical file locations.
+# Read 0-AI-MANIFEST.a2ml, .machine_readable/6a2/STATE.a2ml, and
+# .machine_readable/6a2/anchor/ANCHOR.a2ml before editing.
 
-# LICENSE
-# All original code: MPL-2.0 (SPDX header required on every file).
-# Never use AGPL-3.0. Fallback to MPL-2.0 only when platform requires it.
-# Copyright: Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+# Be precise about evidence: Idris2 model builds, Zig tests, generated ABI
+# checks, binding links, and protocol interoperability are different claims.
+# Grep-based smoke checks are not runtime tests or formal proofs.
 
-# STATE FILES
-# .a2ml metadata files go in .machine_readable/ ONLY.
-# Never create STATE.a2ml, META.a2ml, ECOSYSTEM.a2ml, AGENTIC.a2ml,
-# NEUROSYM.a2ml, or PLAYBOOK.a2ml in the repository root.
+# Keep unavailable authentication/cryptographic operations fail-closed. Do not
+# publish or deploy the current container scaffolding.
 
-# BANNED PATTERNS
-# Idris2: believe_me, assert_total, assert_smaller, unsafePerformIO
-# Haskell: unsafeCoerce, unsafePerformIO, undefined, error
-# OCaml: Obj.magic, Obj.repr, Obj.obj
-# Coq: Admitted
-# Lean: sorry
-# Rust: transmute (unless FFI with // SAFETY: comment)
+# Existing language bindings are source inventory, not supported-language
+# promises. Do not add a language/runtime without recording rationale and a
+# reproducible toolchain plan.
 
-# BANNED LANGUAGES
-# TypeScript -> use ReScript
-# Node.js / npm / bun -> use Deno
-# Go -> use Rust
-# Python -> use Julia or Rust
+# Preserve per-file SPDX identifiers, third-party notices, and repository
+# licensing rules. Original source is generally MPL-2.0.
 
-# CONTAINERS
-# Runtime: Podman (never Docker)
-# File: Containerfile (never Dockerfile)
-# Base: cgr.dev/chainguard/wolfi-base:latest
-
-# ABI/FFI STANDARD
-# ABI definitions: Idris2 with dependent types (src/abi/)
-# FFI implementation: Zig with C ABI (ffi/zig/)
-# Generated C headers: generated/abi/
-
-# BUILD SYSTEM
-# Use just (justfile) for all build, test, lint, and format tasks.
-
-# CODE STYLE
-# Use descriptive variable names.
-# Annotate and document all files.
-# Add SPDX-License-Identifier header to every source file.
+# Use configured Justfile tasks; `fmt-check` checks Git whitespace only.

.devcontainer/devcontainer.json

@@ -21,7 +21,7 @@
     "ghcr.io/nickel-lang/devcontainer-feature:0": {}
   },
 
-  "postCreateCommand": "just deps",
+  "postCreateCommand": "just info",
 
   "remoteUser": "nonroot",
 

.github/CONTRIBUTING.md

@@ -1,126 +1,76 @@
-# Clone the repository
-
-git clone https://github.com/hyperpolymath/proven-servers.git
-cd proven-servers
-
-# Using Guix (recommended for reproducibility)
-
-guix develop
-
-# Or using toolbox/distrobox
-
-toolbox create proven-servers-dev
-toolbox enter proven-servers-dev
-# Install dependencies manually
-
-# Verify setup
-
-just check   # or: cargo check / mix compile / etc.
-just test    # Run test suite
-
-### Repository Structure
-
-```text
-proven-servers/
-├── src/ # Source code (Perimeter 1-2)
-├── lib/ # Library code (Perimeter 1-2)
-├── extensions/ # Extensions (Perimeter 2)
-├── plugins/ # Plugins (Perimeter 2)
-├── tools/ # Tooling (Perimeter 2)
-├── docs/ # Documentation (Perimeter 3)
-│   ├── architecture/ # ADRs, specs (Perimeter 2)
-│   └── proposals/ # RFCs (Perimeter 3)
-├── examples/ # Examples (Perimeter 3)
-├── spec/ # Spec tests (Perimeter 3)
-├── tests/ # Test suite (Perimeter 2-3)
-├── .machine_readable/ # ALL machine-readable content (Perimeter 1)
-│   ├── \*.a2ml # State files (STATE, META, ECOSYSTEM, etc.)
-│   ├── bot_directives/ # Bot configs
-│   └── contractiles/ # Policy contracts (k9, dust, lust, must, trust)
-├── .well-known/ # Protocol files (Perimeter 1-3)
-├── .github/ # GitHub config (Perimeter 1)
-│   ├── CONTRIBUTING.md # This file
-│   ├── ISSUE_TEMPLATE/
-│   └── workflows/
-├── CHANGELOG.md
-├── CODE_OF_CONDUCT.md
-├── GOVERNANCE.md
-├── LICENSE
-├── MAINTAINERS.md
-├── README.adoc
-├── SECURITY.md
-├── flake.nix # Nix flake — fallback (Perimeter 1)
-├── guix.scm # Guix package — primary (Perimeter 1)
-└── Justfile # Task runner (Perimeter 1)
-```
-
-    ---
-
-## How to Contribute
-
-### Reporting Bugs
-
-    **Before reporting**:
-    1. Search existing issues
-    2. Check if it's already fixed in `main`
-    3. Determine which perimeter the bug affects
-
-    **When reporting**:
-
-    Use the [bug report template](.github/ISSUE_TEMPLATE/bug_report.md) and include:
-
-    - Clear, descriptive title
-    - Environment details (OS, versions, toolchain)
-    - Steps to reproduce
-    - Expected vs actual behaviour
-    - Logs, screenshots, or minimal reproduction
-
-### Suggesting Features
-
-    **Before suggesting**:
-    1. Check the [roadmap](ROADMAP.md) if available
-    2. Search existing issues and discussions
-    3. Consider which perimeter the feature belongs to
+<!-- SPDX-License-Identifier: CC-BY-SA-4.0 -->
+<!-- Copyright (c) 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk> -->
 
-    **When suggesting**:
+# Contributing to proven-servers
 
-    Use the [feature request template](.github/ISSUE_TEMPLATE/feature_request.md) and include:
+Thank you for helping improve this repository. It contains protocol models,
+Idris2 packages, Zig FFI prototypes, language-binding sources, tests, and
+maintenance material. It is **not** a production server distribution, and the
+20 language-named binding directories are an inventory rather than a support
+promise.
 
-    - Problem statement (what pain point does this solve?)
-    - Proposed solution
-    - Alternatives considered
-    - Which perimeter this affects
+## Before you start
 
-### Your First Contribution
+1. Read [README.adoc](../README.adoc), [QUICKSTART-DEV.adoc](../QUICKSTART-DEV.adoc),
+   [AI conventions](../docs/AI-CONVENTIONS.adoc), and the package-local README.
+2. Check [READINESS.adoc](../READINESS.adoc) and
+   [PROOF-NEEDS.adoc](../PROOF-NEEDS.adoc) for current evidence limits.
+3. For security reports, follow [SECURITY.adoc](../SECURITY.adoc); do not use a
+   public issue or pull request to disclose a vulnerability.
 
-    Look for issues labelled:
+## Development workflow
 
-    - [`good first issue`](https://github.com/hyperpolymath/proven-servers/labels/good%20first%20issue) — Simple Perimeter 3 tasks
-    - [`help wanted`](https://github.com/hyperpolymath/proven-servers/labels/help%20wanted) — Community help needed
-    - [`documentation`](https://github.com/hyperpolymath/proven-servers/labels/documentation) — Docs improvements
-    - [`perimeter-3`](https://github.com/hyperpolymath/proven-servers/labels/perimeter-3) — Community sandbox scope
+Use a focused branch and a package-specific change. Before opening a PR:
 
-    ---
-
-## Development Workflow
-
-### Branch Naming
-
-docs/short-description # Documentation (P3) test/what-added # Test
-additions (P3) feat/short-description # New features (P2)
-fix/issue-number-description # Bug fixes (P2) refactor/what-changed #
-Code improvements (P2) security/what-fixed # Security fixes (P1-2)
-
-
-### Commit Messages
-
-    We follow [Conventional Commits](https://www.conventionalcommits.org/):
-
-type(scope): description
-
-Body: what changed and why.
-
-Footer: issue reference, e.g. Closes #123
-\[optional body\]
+```sh
+just validate
+just test-static
+# When installed, run the applicable compiler checks:
+just build-idris
+just build-zig
+just test-zig
+```
 
-\[optional footer\]
+`just test-static` runs source-pattern and inventory heuristics; it is not a
+runtime test, formal proof, ABI-conformance test, or security certification.
+The compiler-backed tasks require Idris2 and Zig. Record exact compiler
+versions and clearly list any checks that could not run. Toolchain versions are
+not yet fully pinned repository-wide.
+
+For changes to an individual component, also follow that package's README and
+manifest. An Idris2 build validates only the definitions in the selected
+`.ipkg`; a Zig test supports only the code paths it executes. Neither alone
+proves that a separate header or language binding conforms.
+
+## Change expectations
+
+* Keep changes small and explain the problem and evidence in the PR.
+* Preserve fail-closed behavior where credentials, key material, or a verified
+  backend is absent. Do not turn an unavailable security operation into a
+  success path.
+* Do not claim bindings are wired/supported until they build, link, and run
+  against the intended native library.
+* Update `.machine_readable/BINDINGS.a2ml`, `READINESS.adoc`, or
+  `PROOF-NEEDS.adoc` only when current evidence justifies the change.
+* Preserve file-level SPDX identifiers and third-party license notices.
+* Keep root `Justfile` synchronized with
+  `.machine_readable/contractiles/Justfile`.
+* Do not build, sign, push, or deploy the container scaffolding; no runnable
+  application target is established.
+
+There is no repository-wide language formatter or complete multi-language lint
+matrix. `just fmt-check` checks Git whitespace only; do not describe it as code
+formatting.
+
+## Pull requests
+
+Use the repository PR template. Include:
+
+* a summary and motivation;
+* affected packages and any compatibility impact;
+* exact test/build commands and outcomes, with tool versions;
+* explicit skipped checks and remaining risks;
+* relevant issue or advisory references, when applicable.
+
+A green source grep or historical audit report is not evidence that modified
+native code builds today. Maintainers review changes before merging.