Skip to content

Commit 8504f1e

Browse files
feat(contract): layering-contract gate — enforce I1 (dep direction) + I3 (shared-ABI drift) (#206)
**Draft for owner ratification** — this is governance; it constrains future work, so it lands only on your review. ## Why Independent work in any one repo must not silently **detach** it from the stack it composes with: ``` systemet (theory) ← anytype (kernel) ← AffineScript (profile) → typed-wasm ← ephapax ``` typed-wasm owns the shared **`typedwasm.*` wire ABI** — the highest-detachment-risk contract in the estate (a "let me just tidy this format" change silently breaks AffineScript's and ephapax's emitters). This makes that structurally impossible. ## What - **`CONTRACT.adoc`** — the rules for anyone (human/LLM/LAM) working here: must / should / could + must-not / should-not / cannot, scoped to typed-wasm's role as the shared multi-producer target. - **`tools/check-contract.sh`** — a generic, config-driven gate (the same script every repo will carry). Enforces: - **I1 (blocking)** — no downstream/sibling repo as a dependency (scans manifests + `.gitmodules` only; prose never false-fails). - **I3 (blocking)** — the wire ABI is **content-anchored**: the byte-spec comments in `section.rs` are wrapped in `CONTRACT-ABI-ANCHOR` markers and hashed into `contract.abi.sha256`. Any change fails until you bump `abi_version`, cite a coordinated ADR, and `--reseal`. - **I4 (advisory)** — role-purity greps (none for a target). - **`.github/workflows/contract-gate.yml`** — CI wiring (self-contained, SHA-pinned). - `section.rs` — anchor markers around the ownership + regions byte-spec comments (comments only; `cargo check` clean). ## Proven to bite ``` SIMULATE I3 (tidy the ownership format) → ERROR I3 violation … GATE FAILED SIMULATE I1 (add ephapax git dep) → ERROR I1 violation … GATE FAILED revert both → OK: contract gate — I1 + I3 hold ``` Runnable locally today (`tools/check-contract.sh`); the CI job enforces once the estate Actions billing block clears. ## Rollout typed-wasm is the **reference** (it owns the shared ABI). Companions to follow as their own draft PRs in **AffineScript, ephapax, anytype, systemet**, each with the role-appropriate `CONTRACT.adoc` + the same gate. Left **un-armed** for your ratification. 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-authored-by: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
1 parent 331ad7d commit 8504f1e

7 files changed

Lines changed: 260 additions & 0 deletions

File tree

Lines changed: 26 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,26 @@
1+
# SPDX-License-Identifier: MPL-2.0
2+
# Layering-contract gate: enforces the inter-project invariants (I1 dependency
3+
# direction + I3 shared-ABI drift) that keep this repo composable with the rest
4+
# of the stack. See CONTRACT.adoc. Self-contained (no reusable); runnable
5+
# locally as tools/check-contract.sh.
6+
name: Contract Gate
7+
on:
8+
pull_request:
9+
branches: ['**']
10+
push:
11+
branches: [main, master]
12+
permissions:
13+
contents: read
14+
concurrency:
15+
group: contract-gate-${{ github.ref }}
16+
cancel-in-progress: true
17+
jobs:
18+
contract:
19+
name: Layering contract (I1 + I3)
20+
runs-on: ubuntu-latest
21+
timeout-minutes: 5
22+
steps:
23+
- name: Checkout
24+
uses: actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0 # v4.2.2
25+
- name: Run contract gate
26+
run: bash tools/check-contract.sh

CONTRACT.adoc

Lines changed: 98 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,98 @@
1+
// SPDX-License-Identifier: CC-BY-SA-4.0
2+
// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath)
3+
= typed-wasm — Layering Contract
4+
:toc: macro
5+
6+
[IMPORTANT]
7+
====
8+
This file is the *contract* for anyone — human, LLM, or LAM — working in this
9+
repo. It states what you *must*, *should*, and *could* do, and what you *must
10+
not*, *should not*, and *cannot* do, so that independent work here can never
11+
silently *detach* typed-wasm from the projects it composes with. The
12+
machine-checked subset is enforced by `tools/check-contract.sh` (config in
13+
`contract.config.sh`); read "Enforcement" at the bottom.
14+
====
15+
16+
toc::[]
17+
18+
== Where typed-wasm sits
19+
20+
[source]
21+
----
22+
systemet (theory) <- anytype (kernel) <- AffineScript (profile) --emits--> typed-wasm <--emits-- ephapax
23+
(this repo:
24+
shared target)
25+
----
26+
27+
typed-wasm is a *language-agnostic, verified compilation target*. It is
28+
consumed by *multiple independent producers* — today AffineScript and ephapax,
29+
tomorrow an anytype-derived producer. It is downstream of nobody: it defines a
30+
contract that others meet.
31+
32+
== The estate invariants (why this file exists)
33+
34+
- *I1 — dependency direction is one-way.* No downstream/sibling repo may be a
35+
dependency of typed-wasm. (Enforced.)
36+
- *I2 — extend, don't redefine.* Additions are fine; redefining a published
37+
contract needs an ADR in the owning repo.
38+
- *I3 — the `typedwasm.*` wire ABI is a multi-producer contract.* It changes
39+
only via a coordinated ADR referenced by *every* producer, with an
40+
`abi_version` bump. Never unilaterally. (Enforced — the keystone.)
41+
- *I4 — role purity.* typed-wasm is a *target + verifier*, not a compiler for
42+
any one language.
43+
44+
== Rules for this repo
45+
46+
=== MUST
47+
- Treat the `typedwasm.ownership` / `typedwasm.regions` / capability wire
48+
formats as a *versioned, multi-producer ABI*. The verifier's byte codec is
49+
the single source of truth; the anchored byte-spec comments in
50+
`crates/typed-wasm-verify/src/section.rs` are that truth in prose.
51+
- Keep the Rust verifier and the Idris2 level proofs the authority; keep
52+
cross-producer conformance fixtures green.
53+
- Bump `CONTRACT_ABI_VERSION` (`contract.config.sh`) + reference a coordinated
54+
ADR + re-seal (`tools/check-contract.sh --reseal`) for *any* wire-format
55+
change, and land the matching change in every producer in lock-step.
56+
57+
=== SHOULD
58+
- Add new levels / sections *additively* and behind feature flags
59+
(e.g. `unstable-l2`) so existing producers keep verifying unchanged.
60+
- Version each carrier section explicitly (as `REGIONS_SECTION_VERSION` does).
61+
62+
=== COULD
63+
- Grow the level proofs, the verifier, the codegen crate, tooling, docs — all
64+
role-local and free.
65+
- Add new producers to the conformance suite.
66+
67+
=== MUST NOT
68+
- Change an *existing* section's byte format unilaterally, or without a
69+
version bump + coordinated ADR + every-producer update. This is the classic
70+
detachment: "time to tidy this format" silently breaks AffineScript's and
71+
ephapax's emitters. The gate stops it.
72+
- Assume a single producer, or bake producer-specific lowering into the shared
73+
format.
74+
- Depend on `affinescript`, `ephapax`, `anytype`, or `systemet`.
75+
76+
=== SHOULD NOT
77+
- Let the prose byte-spec (the anchored comments) drift from the codec.
78+
79+
=== CANNOT (structural — the gate fails the build)
80+
- Reference a downstream/sibling repo as a dependency (I1).
81+
- Alter an anchored wire-format region without bumping `abi_version` and
82+
re-sealing (I3).
83+
84+
== Enforcement
85+
86+
`tools/check-contract.sh` (wired into CI via `.github/workflows/contract-gate.yml`,
87+
and runnable locally / as a pre-commit step):
88+
89+
- *I1 (blocking):* scans manifests + `.gitmodules` for a forbidden dependency.
90+
- *I3 (blocking):* content-hashes the `CONTRACT-ABI-ANCHOR` regions in
91+
`section.rs` against sealed digests in `contract.abi.sha256`; any change fails
92+
until you bump `abi_version`, cite an ADR, and `--reseal`.
93+
- *I4 (advisory):* role-purity greps (none for a target).
94+
95+
To change the ABI (the *only* correct way): open a coordinated ADR across
96+
typed-wasm + AffineScript + ephapax, bump `CONTRACT_ABI_VERSION`, edit the
97+
format, `tools/check-contract.sh --reseal`, and update every producer's emitter
98+
in the same landing.

README.adoc

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -276,3 +276,7 @@ MPL-2.0
276276
== Author
277277

278278
Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
279+
280+
== Layering contract
281+
282+
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

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,4 @@
1+
# ABI-anchor digests (abi_version=1). DO NOT hand-edit.
2+
# Re-seal ONLY with an abi_version bump + an ADR. tools/check-contract.sh --reseal
3+
ffac6e2342498c4e189461bd3a9e799ab4786bf0e7970e37ea42af62fb116ad0 crates/typed-wasm-verify/src/section.rs::ownership
4+
ae1625ae210ebbe6e406a215e747d0102948c9169b6551b6e09b8fe482126902 crates/typed-wasm-verify/src/section.rs::regions

contract.config.sh

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

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

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -3,6 +3,7 @@
33
//
44
// `typedwasm.ownership` custom-section codec.
55
//
6+
// >>> CONTRACT-ABI-ANCHOR ownership (see /CONTRACT.adoc; change only via a coordinated ADR + abi_version bump)
67
// Wire format (little-endian, byte-aligned):
78
//
89
// u32le count
@@ -11,6 +12,7 @@
1112
// u8 n_params
1213
// u8[n] param_kinds (0=Unrestricted, 1=Linear, 2=SharedBorrow, 3=ExclBorrow)
1314
// u8 ret_kind
15+
// <<< CONTRACT-ABI-ANCHOR ownership
1416
//
1517
// Rust port of `Tw_verify.parse_ownership_section_payload` plus the
1618
// inverse encoder mirroring `Codegen.build_ownership_section`. The OCaml
@@ -248,6 +250,7 @@ mod tests {
248250
// UNSTABLE: the wire format here may change before the proposal moves to
249251
// [accepted].
250252
//
253+
// >>> CONTRACT-ABI-ANCHOR regions (see /CONTRACT.adoc; change only via a coordinated ADR + abi_version bump)
251254
// Wire format (little-endian, byte-aligned, lenient on truncation —
252255
// matches the LenientReader pattern used by ownership):
253256
//
@@ -266,6 +269,7 @@ mod tests {
266269
// u8 nullability (0=NonNull, 1=Nullable)
267270
// u32le cardinality (1=single, n>1=fixed array, 0=unbounded/dynamic)
268271
// u32le region_byte_size (sum-check; verifier may compare to its own calc)
272+
// <<< CONTRACT-ABI-ANCHOR regions
269273
//
270274
// L15 capabilities (`typedwasm.capabilities`) and the access-site mapping
271275
// from wasm `memarg` back to (region, field) are out of scope of this

tools/check-contract.sh

Lines changed: 102 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,102 @@
1+
#!/usr/bin/env bash
2+
# SPDX-License-Identifier: MPL-2.0
3+
# SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath)
4+
#
5+
# check-contract.sh — the estate layering-contract gate (generic; identical in
6+
# every repo). Enforces the inter-project invariants that keep
7+
# systemet <- anytype <- AffineScript -> typed-wasm <- ephapax
8+
# composable, so independent work in one repo cannot silently DETACH it.
9+
# Behaviour comes from contract.config.sh at the repo root. See CONTRACT.adoc.
10+
#
11+
# I1 Dependency direction one-way -> BLOCKING
12+
# I3 Shared ABI is a multi-producer contract -> BLOCKING (content-anchored)
13+
# I4 Role purity -> ADVISORY
14+
# Presence: CONTRACT.adoc + back-link -> BLOCKING (presence)
15+
#
16+
# Usage: tools/check-contract.sh # check
17+
# tools/check-contract.sh --reseal # rewrite contract.abi.sha256
18+
# # (ONLY with an abi_version bump + ADR)
19+
set -uo pipefail
20+
cd "$(dirname "$0")/.."
21+
RESEAL=0; [ "${1:-}" = "--reseal" ] && RESEAL=1
22+
RED=$'\033[31m'; GRN=$'\033[32m'; YEL=$'\033[33m'; DIM=$'\033[2m'; RST=$'\033[0m'
23+
fail=0; warn=0
24+
err() { printf '%sERROR%s %s\n' "$RED" "$RST" "$1"; fail=1; }
25+
note() { printf '%swarn%s %s\n' "$YEL" "$RST" "$1"; warn=$((warn+1)); }
26+
ok() { printf '%sok%s %s\n' "$GRN" "$RST" "$1"; }
27+
28+
[ -f contract.config.sh ] || { err "contract.config.sh missing"; exit 1; }
29+
# shellcheck disable=SC1091
30+
. ./contract.config.sh
31+
: "${CONTRACT_ROLE:?contract.config.sh must set CONTRACT_ROLE}"
32+
: "${CONTRACT_ABI_VERSION:=none}"
33+
DIGEST_FILE="contract.abi.sha256"
34+
35+
# Presence
36+
if [ -f CONTRACT.adoc ]; then ok "CONTRACT.adoc present (role: ${CONTRACT_ROLE})"
37+
else err "CONTRACT.adoc missing — the rules for this repo are not written down"; fi
38+
if grep -rql 'CONTRACT\.adoc' README* .claude/CLAUDE.md 2>/dev/null; then ok "back-link to CONTRACT.adoc present"
39+
else note "no README/CLAUDE back-link to CONTRACT.adoc"; fi
40+
41+
# I1 — dependency direction (manifests + .gitmodules only; never prose)
42+
i1=0
43+
for name in ${CONTRACT_FORBIDDEN_DEPS:-}; do
44+
for m in ${CONTRACT_MANIFESTS:-} .gitmodules; do
45+
[ -f "$m" ] || continue
46+
if grep -nE "(hyperpolymath/${name}([./\"' ]|\$)|^[[:space:]]*\"?${name}\"?[[:space:]]*=)" "$m" \
47+
| grep -vE '^\s*#|SPDX' >/dev/null 2>&1; then
48+
err "I1 violation: '${name}' referenced as a dependency in ${m} (must not depend on downstream)"; i1=$((i1+1))
49+
fi
50+
done
51+
done
52+
[ "$i1" -eq 0 ] && ok "I1 dependency direction clean (forbidden deps: ${CONTRACT_FORBIDDEN_DEPS:-none})"
53+
54+
# I3 — shared-ABI drift (content-anchored regions)
55+
extract_region() { awk -v m="$2" '
56+
$0 ~ (">>> CONTRACT-ABI-ANCHOR " m "($|[^A-Za-z0-9_-])") {on=1; next}
57+
$0 ~ ("<<< CONTRACT-ABI-ANCHOR " m "($|[^A-Za-z0-9_-])") {on=0}
58+
on {print}' "$1"; }
59+
compute() { for a in ${CONTRACT_ABI_ANCHORS:-}; do
60+
f="${a%%::*}"; mk="${a##*::}"
61+
[ -f "$f" ] || { echo "MISSING $a"; continue; }
62+
reg="$(extract_region "$f" "$mk")"
63+
[ -z "$reg" ] && { echo "NOMARKER $a"; continue; }
64+
printf '%s %s\n' "$(printf '%s' "$reg" | sha256sum | cut -d' ' -f1)" "$a"
65+
done; }
66+
if [ -n "${CONTRACT_ABI_ANCHORS:-}" ]; then
67+
if [ "$RESEAL" -eq 1 ]; then
68+
{ echo "# ABI-anchor digests (abi_version=${CONTRACT_ABI_VERSION}). DO NOT hand-edit."
69+
echo "# Re-seal ONLY with an abi_version bump + an ADR. tools/check-contract.sh --reseal"
70+
compute; } > "$DIGEST_FILE"
71+
ok "re-sealed ${DIGEST_FILE} at abi_version=${CONTRACT_ABI_VERSION}"
72+
else
73+
[ -f "$DIGEST_FILE" ] || err "I3: ${DIGEST_FILE} missing — run tools/check-contract.sh --reseal"
74+
cur="$(compute)"
75+
if echo "$cur" | grep -qE '^(MISSING|NOMARKER)'; then
76+
echo "$cur" | grep -E '^(MISSING|NOMARKER)' | while read -r k a; do err "I3: anchor ${a}: ${k}"; done; fail=1
77+
fi
78+
exp="$(grep -vE '^\s*#' "$DIGEST_FILE" 2>/dev/null)"
79+
if [ "$(printf '%s' "$cur" | sort)" = "$(printf '%s' "$exp" | sort)" ]; then
80+
ok "I3 shared-ABI anchors unchanged (abi_version=${CONTRACT_ABI_VERSION})"
81+
else
82+
err "I3 violation: a shared-ABI anchor changed — this is a MULTI-PRODUCER ABI (${CONTRACT_FORBIDDEN_DEPS:-producers})."
83+
printf ' %sTo change it: bump CONTRACT_ABI_VERSION, reference a coordinated ADR, --reseal, update every producer.%s\n' "$DIM" "$RST"
84+
printf ' %sDo NOT re-seal to make this pass in isolation.%s\n' "$DIM" "$RST"
85+
diff <(printf '%s\n' "$exp"|sort) <(printf '%s\n' "$cur"|sort) | sed 's/^/ /' || true
86+
fi
87+
fi
88+
else ok "I3 not applicable (no shared-ABI anchors for role ${CONTRACT_ROLE})"; fi
89+
90+
# I4 — role purity (advisory)
91+
if [ -n "${CONTRACT_ROLE_DENY:-}" ]; then
92+
while IFS='|' read -r rx msg; do
93+
[ -z "$rx" ] && continue
94+
hits="$(grep -rInE "$rx" ${CONTRACT_SRC_DIRS:-src lib} 2>/dev/null | grep -vE 'CONTRACT|contract\.' | head -3)"
95+
[ -n "$hits" ] && { note "I4 (role purity): ${msg}"; printf '%s\n' "$hits" | sed 's/^/ /'; }
96+
done <<< "${CONTRACT_ROLE_DENY}"
97+
else ok "I4 no role-purity denials declared"; fi
98+
99+
echo
100+
if [ "$fail" -ne 0 ]; then
101+
printf '%sCONTRACT GATE FAILED%s — this change would detach the repo from the stack. See CONTRACT.adoc.\n' "$RED" "$RST"; exit 1; fi
102+
printf '%sOK%s: contract gate — I1 + I3 hold%s\n' "$GRN" "$RST" "$([ "$warn" -gt 0 ] && echo " (${warn} advisory warning(s))")"

0 commit comments

Comments
 (0)