diff --git a/.clinerules b/.clinerules index fe11e22..7299e80 100644 --- a/.clinerules +++ b/.clinerules @@ -25,7 +25,7 @@ # BANNED LANGUAGES # TypeScript -> ReScript -# Node.js / npm / bun -> Deno +# JS reach order (panoply): Bun → Deno → pnpm → npm (see docs/practice/JS-RUNTIME-ORDER.adoc) # Go -> Rust # Python -> Julia or Rust diff --git a/.cursorrules b/.cursorrules index e7b19ba..aa2dc92 100644 --- a/.cursorrules +++ b/.cursorrules @@ -24,7 +24,7 @@ # BANNED LANGUAGES # TypeScript -> use ReScript -# Node.js / npm / bun -> use Deno +# JS reach order (panoply): Bun → Deno → pnpm → npm (see docs/practice/JS-RUNTIME-ORDER.adoc) # Go -> use Rust # Python -> use Julia or Rust diff --git a/.github/hooks/validate-deed.sh b/.github/hooks/validate-deed.sh index e5c53f5..b6812b5 100755 --- a/.github/hooks/validate-deed.sh +++ b/.github/hooks/validate-deed.sh @@ -2,7 +2,7 @@ # SPDX-License-Identifier: MPL-2.0 # Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) # -# validate-a2ml.sh — A2ML manifest validation script +# validate-deed.sh — DEED / machine-readable validation script # # Scans for .deed and .deed files and validates: # 1. Required fields: agent-id or pedigree name, version diff --git a/.github/pull_request_template.md b/.github/pull_request_template.md index 03bffa5..5cc25f9 100644 --- a/.github/pull_request_template.md +++ b/.github/pull_request_template.md @@ -21,7 +21,7 @@ Copyright (c) Jonathan D.A. Jewell - [ ] Tests pass (`just test` or equivalent) - [ ] Code is formatted (`just fmt` or equivalent) - [ ] Linter is clean (no new warnings or errors) -- [ ] No banned language patterns (no TypeScript, no npm/bun, no Go/Python) +- [ ] No banned language patterns (no TypeScript, no Go/Python; JS reach: Bun → Deno → pnpm → npm) - [ ] No `unsafe` blocks without `// SAFETY:` comments - [ ] No banned functions (`believe_me`, `unsafeCoerce`, `Obj.magic`, `Admitted`, `sorry`) - [ ] SPDX license headers present on all new/modified source files diff --git a/.machine_readable/6a2/LANGUAGES.deed b/.machine_readable/6a2/LANGUAGES.deed index 3a0ef67..7957ff8 100644 --- a/.machine_readable/6a2/LANGUAGES.deed +++ b/.machine_readable/6a2/LANGUAGES.deed @@ -12,7 +12,7 @@ last-updated = "2026-06-21" abi-proofs = "idris2" # src/interface/Abi/, verification/proofs/idris2/ ffi = "zig" # src/interface/ffi/ proofs = ["coq", "agda", "idris2"] # verification/proofs/ -config = ["nickel", "a2ml"] # .machine_readable/ +config = ["nickel", "deed"] # .machine_readable/ build = ["just", "bash"] [planned] diff --git a/.machine_readable/root-allow.txt b/.machine_readable/root-allow.txt index 8c5edae..ca24b2f 100644 --- a/.machine_readable/root-allow.txt +++ b/.machine_readable/root-allow.txt @@ -29,6 +29,7 @@ CHANGELOG.adoc # Current changelog after the AsciiDoc migration. # ─── Build entry points (must live at root for their tooling) ──────────────── Justfile # delegates phases to build/just/*.just +Mustfile # root contractile pointer → .machine_readable/contractiles/Mustfile.deed coordination.k9 # repo-local session binding (template-mandated) # ─── Conventional dotfiles (tool-required at root) ─────────────────────────── @@ -60,7 +61,7 @@ www/ # site-operations bundle; canonical .well-known/ live LICENSES/ # REUSE/SPDX licence texts (LICENSES/MPL-2.0.txt) .machine_readable/ # AI manifests, contractiles, custom-format configs .well-known/ -build/ # contractile.just, setup.sh, flake.{nix,lock}, guix.scm, .guix-channel, Containerfile +build/ # contractile.just, setup.sh, guix.scm, .guix-channel, Containerfile ci/ # .gitlab-ci.yml, .pre-commit-config.yaml (root shims if tools require) docs/ # onboarding/, status/, governance/, ... docs-template/ # template-only: scaffolding docs copied into new repos diff --git a/.windsurfrules b/.windsurfrules index fe11e22..7299e80 100644 --- a/.windsurfrules +++ b/.windsurfrules @@ -25,7 +25,7 @@ # BANNED LANGUAGES # TypeScript -> ReScript -# Node.js / npm / bun -> Deno +# JS reach order (panoply): Bun → Deno → pnpm → npm (see docs/practice/JS-RUNTIME-ORDER.adoc) # Go -> Rust # Python -> Julia or Rust diff --git a/Justfile b/Justfile index 08c96c6..a6a255b 100644 --- a/Justfile +++ b/Justfile @@ -191,6 +191,12 @@ language-audit: api-test: cd src/api/zig && zig test adapter.zig +# Specification artefact gates (#5 #6 #7) — not a checker +spec-tests: + bash tests/core_spec.sh + bash tests/evidence_spec.sh + bash tests/manifest_spec.sh + # Run the full merge-requirement test suite # Categories: execution (`test`) + E2E + aspect + bench + lifecycle + P2P test-all: test e2e aspect bench lifecycle p2p diff --git a/Mustfile b/Mustfile new file mode 100644 index 0000000..c6ecefb --- /dev/null +++ b/Mustfile @@ -0,0 +1,8 @@ +# SPDX-License-Identifier: MPL-2.0 +# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +# +# Root Mustfile — contractile physical-state contract. +# Canonical body: .machine_readable/contractiles/Mustfile.deed +# Run with: must check (when contractile CLI is present) + +@include: .machine_readable/contractiles/Mustfile.deed diff --git a/docs/status/ROADMAP.adoc b/docs/status/ROADMAP.adoc index 3586768..efb14a2 100644 --- a/docs/status/ROADMAP.adoc +++ b/docs/status/ROADMAP.adoc @@ -20,7 +20,7 @@ Design phase. Charter + RSR spine + Core/Evidence *specs*. No Core checker. * [ ] Owner: keep or delete Coq/Agda/Lean/TLA proof stubs (Idris2-only FV policy vs RSR template) * [ ] Implement Zig API adapter beyond `NotImplemented` when a gateway exists * [ ] Desktop launcher via launch-scaffolder when a GUI exists -* [ ] Root `Mustfile` (contractile, not Makefile) +* [x] Root `Mustfile` (pointer to `.machine_readable/contractiles/Mustfile.deed`) == Charter product diff --git a/docs/status/TEST-NEEDS.adoc b/docs/status/TEST-NEEDS.adoc index 7174fc7..6abc432 100644 --- a/docs/status/TEST-NEEDS.adoc +++ b/docs/status/TEST-NEEDS.adoc @@ -22,6 +22,8 @@ Idris2 ABI / Zig FFI scaffold, not language semantics. | *Lifecycle tests* | 1 | `tests/lifecycle.sh` — zig build/test/clean; skips Idris2 if absent | *P2P tests* | 1 | `tests/p2p.sh` — honest SKIP until a peer protocol exists; FAIL if P2P-shaped source appears untested | *Core spec tests* | 1 | `tests/core_spec.sh` — guards issue #5 specification artefacts +| *Evidence spec tests* | 1 | `tests/evidence_spec.sh` — kinds + refused example (#6) +| *Manifest spec tests* | 1 | `tests/manifest_spec.sh` — schema + refused example (#7, no emitter) | *Workflow tests* | 1 | `tests/workflows/validate_workflows_test.sh` | *Benchmarks* | 3 | `benches/template_bench.sh` (Zig build, Zig tests, workflow validation) | *Fuzz tests* | 0 | `verification/fuzzing/` scaffold present; no harness wired yet diff --git a/launcher/gui-error.sh b/launcher/gui-error.sh index b4ffd88..b865367 100755 --- a/launcher/gui-error.sh +++ b/launcher/gui-error.sh @@ -3,7 +3,7 @@ # SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) # # gui-error.sh — reference implementation of [error-visibility] from -# launcher/launcher-standard.a2ml. +# launcher/launcher-standard.deed. # # When the launcher runs in a GUI context (no TTY + DISPLAY or # WAYLAND_DISPLAY set), errors written only to stderr disappear: the diff --git a/launcher/resolve-desktop-tools.sh b/launcher/resolve-desktop-tools.sh index 9d57d87..cb8d82d 100755 --- a/launcher/resolve-desktop-tools.sh +++ b/launcher/resolve-desktop-tools.sh @@ -17,7 +17,7 @@ # (e.g. missing optional verify-desktop-integrity.sh). # # The ladders mirror [resolution].desktop-tools-search and -# [resolution].standard-search in the a2ml. They MUST stay in sync — see the +# [resolution].standard-search in the deed. They MUST stay in sync — see the # CI gate referenced in launcher/README.adoc §Sync requirement. # --------------------------------------------------------------------------- diff --git a/launcher/soft-attach.sh b/launcher/soft-attach.sh index 1658849..e9096cf 100755 --- a/launcher/soft-attach.sh +++ b/launcher/soft-attach.sh @@ -3,7 +3,7 @@ # SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) # # soft-attach.sh — reference implementation of [soft-attach] from -# launcher/launcher-standard.a2ml. +# launcher/launcher-standard.deed. # # Soft-attach = optional ecosystem integrations that the launcher invokes # IF they are installed, and silently skips otherwise. Downstream diff --git a/src/manifest/MANIFEST-SCHEMA.adoc b/src/manifest/MANIFEST-SCHEMA.adoc new file mode 100644 index 0000000..793d857 --- /dev/null +++ b/src/manifest/MANIFEST-SCHEMA.adoc @@ -0,0 +1,54 @@ +// SPDX-License-Identifier: CC-BY-SA-4.0 +// Copyright (c) Jonathan D.A. Jewell += Safety-envelope manifest schema (issue #7) +:revdate: 2026-09-20 + +A manifest is the *per-program, per-backend* statement of which guarantees +were earned and which were not. It is the deliverable. There is **no emitter** +yet: this document is the data model only. + +== Central rule (emitter, when it exists) + +. No guarantee without an envelope. +. No envelope without evidence. +. No composition without a named composition rule. + +A reader must be able to see what is **not** guaranteed. Silence is not +absence of risk. + +== On-disk form + +S-expression, one top form `(manifest ...)`. Keywords: + +[cols="1,3"] +|=== +| `:schema-version` | REQUIRED. Semver string. +| `:program` | REQUIRED. Subject identity (name or content hash). +| `:backend` | REQUIRED. Backend id the envelopes are relative to. +| `:status` | REQUIRED. `draft` \| `refused` \| `emitted`. +| `:earned` | List of envelope records. +| `:unearned` | List of named guarantees that were **not** earned. +| `:composition-rules` | Named rules that license combining envelopes. Empty unless a rule exists. +|=== + +Each earned envelope: + +[cols="1,3"] +|=== +| `:name` | Envelope name. +| `:scope` | Feature subset / projection / compiler mode (free text until Core exists). +| `:evidence` | Pointer to an evidence artefact (`:kind` + path or hash). +|=== + +`:status refused` is the honest value until an emitter runs. Do not write +`:status emitted` without an emitter and evidence that is not itself refused. + +== Example + +See `examples/refused.manifest` — empty earned set, explicit unearned +guarantees, refused status. + +== Non-goals (this commit) + +* No emitter, no CI consumer, no backend contract (#9). +* Do not close issue #7 until an emitter enforces the three rules. diff --git a/src/manifest/README.adoc b/src/manifest/README.adoc index ca1701a..1cefee7 100644 --- a/src/manifest/README.adoc +++ b/src/manifest/README.adoc @@ -10,9 +10,9 @@ absence of type errors. [IMPORTANT] ==== -*Not yet implemented.* Sketch area per the -xref:../../docs/architecture/DESIGN-DISCIPLINE.adoc[charter]. No manifest schema -or emitter exists yet (design phase). +*Schema specified; no emitter yet.* See xref:MANIFEST-SCHEMA.adoc[MANIFEST-SCHEMA.adoc] +and `examples/refused.manifest` (honest `:status refused`, empty `:earned`). +Issue #7 stays open until an emitter enforces the three rules. ==== == What a manifest records diff --git a/src/manifest/examples/refused.manifest b/src/manifest/examples/refused.manifest new file mode 100644 index 0000000..5484a13 --- /dev/null +++ b/src/manifest/examples/refused.manifest @@ -0,0 +1,12 @@ +# SPDX-License-Identifier: MPL-2.0 +# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +# +# Honest refused manifest: no emitter, no Core checker, no backend contract. +(manifest + :schema-version "0.1.0" + :program "panoply-core" + :backend "none" + :status refused + :earned () + :unearned (total-correctness memory-safety confluence) + :composition-rules ()) diff --git a/tests/README.adoc b/tests/README.adoc index fa7dcdb..ca4f45f 100644 --- a/tests/README.adoc +++ b/tests/README.adoc @@ -3,5 +3,5 @@ = tests Shell gates: `e2e.sh`, `aspect_tests.sh`, `lifecycle.sh`, `p2p.sh`, -`core_spec.sh`, `evidence_spec.sh`. Zig tests live under +`core_spec.sh`, `evidence_spec.sh`, `manifest_spec.sh`. Zig tests live under `src/interface/ffi/`. See `docs/status/TEST-NEEDS.adoc`. diff --git a/tests/manifest_spec.sh b/tests/manifest_spec.sh new file mode 100755 index 0000000..88bcc43 --- /dev/null +++ b/tests/manifest_spec.sh @@ -0,0 +1,18 @@ +#!/usr/bin/env bash +# SPDX-License-Identifier: MPL-2.0 +# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +set -euo pipefail +ROOT="$(cd "$(dirname "${BASH_SOURCE[0]}")/.." && pwd)" +cd "$ROOT" +FAIL=0 +fail() { echo "FAIL: $*"; FAIL=$((FAIL+1)); } +pass() { echo "PASS: $*"; } + +[[ -f src/manifest/MANIFEST-SCHEMA.adoc ]] && pass "schema spec" || fail "missing MANIFEST-SCHEMA" +[[ -f src/manifest/examples/refused.manifest ]] && pass "example" || fail "missing example" +grep -q ':status refused' src/manifest/examples/refused.manifest && pass "honest refused" || fail "example must be refused" +grep -q ':earned ()' src/manifest/examples/refused.manifest && pass "empty earned" || fail "must not claim earned envelopes" +grep -q 'No emitter' src/manifest/MANIFEST-SCHEMA.adoc && pass "schema admits no emitter" || fail "must not claim an emitter" + +echo "FAIL=$FAIL" +exit "$FAIL"