feat(contract): layering-contract gate — enforce I1 (dep direction) + I3 (shared-ABI drift)

.github/workflows/contract-gate.yml

@@ -0,0 +1,26 @@
+# SPDX-License-Identifier: MPL-2.0
+# Layering-contract gate: enforces the inter-project invariants (I1 dependency
+# direction + I3 shared-ABI drift) that keep this repo composable with the rest
+# of the stack. See CONTRACT.adoc. Self-contained (no reusable); runnable
+# locally as tools/check-contract.sh.
+name: Contract Gate
+on:
+  pull_request:
+    branches: ['**']
+  push:
+    branches: [main, master]
+permissions:
+  contents: read
+concurrency:
+  group: contract-gate-${{ github.ref }}
+  cancel-in-progress: true
+jobs:
+  contract:
+    name: Layering contract (I1 + I3)
+    runs-on: ubuntu-latest
+    timeout-minutes: 5
+    steps:
+      - name: Checkout
+        uses: actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0 # v4.2.2
+      - name: Run contract gate
+        run: bash tools/check-contract.sh

CONTRACT.adoc

@@ -0,0 +1,98 @@
+// SPDX-License-Identifier: CC-BY-SA-4.0
+// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath)
+= typed-wasm — Layering Contract
+:toc: macro
+
+[IMPORTANT]
+====
+This file is the *contract* for anyone — human, LLM, or LAM — working in this
+repo. It states what you *must*, *should*, and *could* do, and what you *must
+not*, *should not*, and *cannot* do, so that independent work here can never
+silently *detach* typed-wasm from the projects it composes with. The
+machine-checked subset is enforced by `tools/check-contract.sh` (config in
+`contract.config.sh`); read "Enforcement" at the bottom.
+====
+
+toc::[]
+
+== Where typed-wasm sits
+
+[source]
+----
+systemet (theory) <- anytype (kernel) <- AffineScript (profile) --emits--> typed-wasm  <--emits-- ephapax
+                                                                             (this repo:
+                                                                              shared target)
+----
+
+typed-wasm is a *language-agnostic, verified compilation target*. It is
+consumed by *multiple independent producers* — today AffineScript and ephapax,
+tomorrow an anytype-derived producer. It is downstream of nobody: it defines a
+contract that others meet.
+
+== The estate invariants (why this file exists)
+
+- *I1 — dependency direction is one-way.* No downstream/sibling repo may be a
+  dependency of typed-wasm. (Enforced.)
+- *I2 — extend, don't redefine.* Additions are fine; redefining a published
+  contract needs an ADR in the owning repo.
+- *I3 — the `typedwasm.*` wire ABI is a multi-producer contract.* It changes
+  only via a coordinated ADR referenced by *every* producer, with an
+  `abi_version` bump. Never unilaterally. (Enforced — the keystone.)
+- *I4 — role purity.* typed-wasm is a *target + verifier*, not a compiler for
+  any one language.
+
+== Rules for this repo
+
+=== MUST
+- Treat the `typedwasm.ownership` / `typedwasm.regions` / capability wire
+  formats as a *versioned, multi-producer ABI*. The verifier's byte codec is
+  the single source of truth; the anchored byte-spec comments in
+  `crates/typed-wasm-verify/src/section.rs` are that truth in prose.
+- Keep the Rust verifier and the Idris2 level proofs the authority; keep
+  cross-producer conformance fixtures green.
+- Bump `CONTRACT_ABI_VERSION` (`contract.config.sh`) + reference a coordinated
+  ADR + re-seal (`tools/check-contract.sh --reseal`) for *any* wire-format
+  change, and land the matching change in every producer in lock-step.
+
+=== SHOULD
+- Add new levels / sections *additively* and behind feature flags
+  (e.g. `unstable-l2`) so existing producers keep verifying unchanged.
+- Version each carrier section explicitly (as `REGIONS_SECTION_VERSION` does).
+
+=== COULD
+- Grow the level proofs, the verifier, the codegen crate, tooling, docs — all
+  role-local and free.
+- Add new producers to the conformance suite.
+
+=== MUST NOT
+- Change an *existing* section's byte format unilaterally, or without a
+  version bump + coordinated ADR + every-producer update. This is the classic
+  detachment: "time to tidy this format" silently breaks AffineScript's and
+  ephapax's emitters. The gate stops it.
+- Assume a single producer, or bake producer-specific lowering into the shared
+  format.
+- Depend on `affinescript`, `ephapax`, `anytype`, or `systemet`.
+
+=== SHOULD NOT
+- Let the prose byte-spec (the anchored comments) drift from the codec.
+
+=== CANNOT (structural — the gate fails the build)
+- Reference a downstream/sibling repo as a dependency (I1).
+- Alter an anchored wire-format region without bumping `abi_version` and
+  re-sealing (I3).
+
+== Enforcement
+
+`tools/check-contract.sh` (wired into CI via `.github/workflows/contract-gate.yml`,
+and runnable locally / as a pre-commit step):
+
+- *I1 (blocking):* scans manifests + `.gitmodules` for a forbidden dependency.
+- *I3 (blocking):* content-hashes the `CONTRACT-ABI-ANCHOR` regions in
+  `section.rs` against sealed digests in `contract.abi.sha256`; any change fails
+  until you bump `abi_version`, cite an ADR, and `--reseal`.
+- *I4 (advisory):* role-purity greps (none for a target).
+
+To change the ABI (the *only* correct way): open a coordinated ADR across
+typed-wasm + AffineScript + ephapax, bump `CONTRACT_ABI_VERSION`, edit the
+format, `tools/check-contract.sh --reseal`, and update every producer's emitter
+in the same landing.

README.adoc

@@ -276,3 +276,7 @@ MPL-2.0
 == Author
 
 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+
+== Layering contract
+
+Contributors (human/LLM/LAM): read link:CONTRACT.adoc[CONTRACT.adoc] before changing the wire format or dependencies. It is machine-enforced by `tools/check-contract.sh`.

contract.abi.sha256

@@ -0,0 +1,4 @@
+# ABI-anchor digests (abi_version=1). DO NOT hand-edit.
+# Re-seal ONLY with an abi_version bump + an ADR. tools/check-contract.sh --reseal
+ffac6e2342498c4e189461bd3a9e799ab4786bf0e7970e37ea42af62fb116ad0  crates/typed-wasm-verify/src/section.rs::ownership
+ae1625ae210ebbe6e406a215e747d0102948c9169b6551b6e09b8fe482126902  crates/typed-wasm-verify/src/section.rs::regions

contract.config.sh

@@ -0,0 +1,22 @@
+# SPDX-License-Identifier: MPL-2.0
+# Layering-contract gate config for typed-wasm. Consumed by tools/check-contract.sh.
+# See CONTRACT.adoc for the human-readable rules.
+
+# This repo's role in the stack: theory | kernel | target | profile | producer
+CONTRACT_ROLE="target"
+
+# I1 — dependency direction. typed-wasm is a shared *target*; none of its
+# producers/consumers (or upstream theory/kernel) may appear as a dependency here.
+CONTRACT_FORBIDDEN_DEPS="affinescript ephapax anytype systemet"
+CONTRACT_MANIFESTS="Cargo.toml deno.json crates/typed-wasm-verify/Cargo.toml crates/typed-wasm-codegen/Cargo.toml"
+
+# I3 — the typedwasm.* wire ABI (multi-producer). Anchored byte-spec regions;
+# a change fails the gate unless abi_version is bumped + an ADR referenced + --reseal.
+CONTRACT_ABI_VERSION="1"
+CONTRACT_ABI_ANCHORS="crates/typed-wasm-verify/src/section.rs::ownership crates/typed-wasm-verify/src/section.rs::regions"
+
+# I4 — role purity (advisory). A target must not embed producer-specific lowering.
+# (Left empty: the target's purity is governed mainly by I1; greps here would
+# false-positive on the cross-impl parity comments.)
+CONTRACT_ROLE_DENY=""
+CONTRACT_SRC_DIRS="crates"

crates/typed-wasm-verify/src/section.rs

@@ -3,6 +3,7 @@
 //
 // `typedwasm.ownership` custom-section codec.
 //
+// >>> CONTRACT-ABI-ANCHOR ownership  (see /CONTRACT.adoc; change only via a coordinated ADR + abi_version bump)
 // Wire format (little-endian, byte-aligned):
 //
 //   u32le  count
@@ -11,6 +12,7 @@
 //     u8     n_params
 //     u8[n]  param_kinds  (0=Unrestricted, 1=Linear, 2=SharedBorrow, 3=ExclBorrow)
 //     u8     ret_kind
+// <<< CONTRACT-ABI-ANCHOR ownership
 //
 // Rust port of `Tw_verify.parse_ownership_section_payload` plus the
 // inverse encoder mirroring `Codegen.build_ownership_section`. The OCaml
@@ -248,6 +250,7 @@ mod tests {
 // UNSTABLE: the wire format here may change before the proposal moves to
 // [accepted].
 //
+// >>> CONTRACT-ABI-ANCHOR regions  (see /CONTRACT.adoc; change only via a coordinated ADR + abi_version bump)
 // Wire format (little-endian, byte-aligned, lenient on truncation —
 // matches the LenientReader pattern used by ownership):
 //
@@ -266,6 +269,7 @@ mod tests {
 //           u8     nullability   (0=NonNull, 1=Nullable)
 //           u32le  cardinality   (1=single, n>1=fixed array, 0=unbounded/dynamic)
 //       u32le  region_byte_size  (sum-check; verifier may compare to its own calc)
+// <<< CONTRACT-ABI-ANCHOR regions
 //
 // L15 capabilities (`typedwasm.capabilities`) and the access-site mapping
 // from wasm `memarg` back to (region, field) are out of scope of this

tools/check-contract.sh

@@ -0,0 +1,102 @@
+#!/usr/bin/env bash
+# SPDX-License-Identifier: MPL-2.0
+# SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath)
+#
+# check-contract.sh — the estate layering-contract gate (generic; identical in
+# every repo). Enforces the inter-project invariants that keep
+#   systemet <- anytype <- AffineScript -> typed-wasm <- ephapax
+# composable, so independent work in one repo cannot silently DETACH it.
+# Behaviour comes from contract.config.sh at the repo root. See CONTRACT.adoc.
+#
+#   I1  Dependency direction one-way          -> BLOCKING
+#   I3  Shared ABI is a multi-producer contract -> BLOCKING (content-anchored)
+#   I4  Role purity                           -> ADVISORY
+#   Presence: CONTRACT.adoc + back-link       -> BLOCKING (presence)
+#
+# Usage: tools/check-contract.sh            # check
+#        tools/check-contract.sh --reseal   # rewrite contract.abi.sha256
+#                                            #   (ONLY with an abi_version bump + ADR)
+set -uo pipefail
+cd "$(dirname "$0")/.."
+RESEAL=0; [ "${1:-}" = "--reseal" ] && RESEAL=1
+RED=$'\033[31m'; GRN=$'\033[32m'; YEL=$'\033[33m'; DIM=$'\033[2m'; RST=$'\033[0m'
+fail=0; warn=0
+err()  { printf '%sERROR%s   %s\n' "$RED" "$RST" "$1"; fail=1; }
+note() { printf '%swarn%s    %s\n'  "$YEL" "$RST" "$1"; warn=$((warn+1)); }
+ok()   { printf '%sok%s      %s\n'  "$GRN" "$RST" "$1"; }
+
+[ -f contract.config.sh ] || { err "contract.config.sh missing"; exit 1; }
+# shellcheck disable=SC1091
+. ./contract.config.sh
+: "${CONTRACT_ROLE:?contract.config.sh must set CONTRACT_ROLE}"
+: "${CONTRACT_ABI_VERSION:=none}"
+DIGEST_FILE="contract.abi.sha256"
+
+# Presence
+if [ -f CONTRACT.adoc ]; then ok "CONTRACT.adoc present (role: ${CONTRACT_ROLE})"
+else err "CONTRACT.adoc missing — the rules for this repo are not written down"; fi
+if grep -rql 'CONTRACT\.adoc' README* .claude/CLAUDE.md 2>/dev/null; then ok "back-link to CONTRACT.adoc present"
+else note "no README/CLAUDE back-link to CONTRACT.adoc"; fi
+
+# I1 — dependency direction (manifests + .gitmodules only; never prose)
+i1=0
+for name in ${CONTRACT_FORBIDDEN_DEPS:-}; do
+  for m in ${CONTRACT_MANIFESTS:-} .gitmodules; do
+    [ -f "$m" ] || continue
+    if grep -nE "(hyperpolymath/${name}([./\"' ]|\$)|^[[:space:]]*\"?${name}\"?[[:space:]]*=)" "$m" \
+         | grep -vE '^\s*#|SPDX' >/dev/null 2>&1; then
+      err "I1 violation: '${name}' referenced as a dependency in ${m} (must not depend on downstream)"; i1=$((i1+1))
+    fi
+  done
+done
+[ "$i1" -eq 0 ] && ok "I1 dependency direction clean (forbidden deps: ${CONTRACT_FORBIDDEN_DEPS:-none})"
+
+# I3 — shared-ABI drift (content-anchored regions)
+extract_region() { awk -v m="$2" '
+  $0 ~ (">>> CONTRACT-ABI-ANCHOR " m "($|[^A-Za-z0-9_-])") {on=1; next}
+  $0 ~ ("<<< CONTRACT-ABI-ANCHOR " m "($|[^A-Za-z0-9_-])") {on=0}
+  on {print}' "$1"; }
+compute() { for a in ${CONTRACT_ABI_ANCHORS:-}; do
+    f="${a%%::*}"; mk="${a##*::}"
+    [ -f "$f" ] || { echo "MISSING  $a"; continue; }
+    reg="$(extract_region "$f" "$mk")"
+    [ -z "$reg" ] && { echo "NOMARKER $a"; continue; }
+    printf '%s  %s\n' "$(printf '%s' "$reg" | sha256sum | cut -d' ' -f1)" "$a"
+  done; }
+if [ -n "${CONTRACT_ABI_ANCHORS:-}" ]; then
+  if [ "$RESEAL" -eq 1 ]; then
+    { echo "# ABI-anchor digests (abi_version=${CONTRACT_ABI_VERSION}). DO NOT hand-edit."
+      echo "# Re-seal ONLY with an abi_version bump + an ADR. tools/check-contract.sh --reseal"
+      compute; } > "$DIGEST_FILE"
+    ok "re-sealed ${DIGEST_FILE} at abi_version=${CONTRACT_ABI_VERSION}"
+  else
+    [ -f "$DIGEST_FILE" ] || err "I3: ${DIGEST_FILE} missing — run tools/check-contract.sh --reseal"
+    cur="$(compute)"
+    if echo "$cur" | grep -qE '^(MISSING|NOMARKER)'; then
+      echo "$cur" | grep -E '^(MISSING|NOMARKER)' | while read -r k a; do err "I3: anchor ${a}: ${k}"; done; fail=1
+    fi
+    exp="$(grep -vE '^\s*#' "$DIGEST_FILE" 2>/dev/null)"
+    if [ "$(printf '%s' "$cur" | sort)" = "$(printf '%s' "$exp" | sort)" ]; then
+      ok "I3 shared-ABI anchors unchanged (abi_version=${CONTRACT_ABI_VERSION})"
+    else
+      err "I3 violation: a shared-ABI anchor changed — this is a MULTI-PRODUCER ABI (${CONTRACT_FORBIDDEN_DEPS:-producers})."
+      printf '        %sTo change it: bump CONTRACT_ABI_VERSION, reference a coordinated ADR, --reseal, update every producer.%s\n' "$DIM" "$RST"
+      printf '        %sDo NOT re-seal to make this pass in isolation.%s\n' "$DIM" "$RST"
+      diff <(printf '%s\n' "$exp"|sort) <(printf '%s\n' "$cur"|sort) | sed 's/^/          /' || true
+    fi
+  fi
+else ok "I3 not applicable (no shared-ABI anchors for role ${CONTRACT_ROLE})"; fi
+
+# I4 — role purity (advisory)
+if [ -n "${CONTRACT_ROLE_DENY:-}" ]; then
+  while IFS='|' read -r rx msg; do
+    [ -z "$rx" ] && continue
+    hits="$(grep -rInE "$rx" ${CONTRACT_SRC_DIRS:-src lib} 2>/dev/null | grep -vE 'CONTRACT|contract\.' | head -3)"
+    [ -n "$hits" ] && { note "I4 (role purity): ${msg}"; printf '%s\n' "$hits" | sed 's/^/          /'; }
+  done <<< "${CONTRACT_ROLE_DENY}"
+else ok "I4 no role-purity denials declared"; fi
+
+echo
+if [ "$fail" -ne 0 ]; then
+  printf '%sCONTRACT GATE FAILED%s — this change would detach the repo from the stack. See CONTRACT.adoc.\n' "$RED" "$RST"; exit 1; fi
+printf '%sOK%s: contract gate — I1 + I3 hold%s\n' "$GRN" "$RST" "$([ "$warn" -gt 0 ] && echo " (${warn} advisory warning(s))")"