Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion .clinerules
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down
2 changes: 1 addition & 1 deletion .cursorrules
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down
2 changes: 1 addition & 1 deletion .github/hooks/validate-deed.sh
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,7 @@
# SPDX-License-Identifier: MPL-2.0
# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
#
# 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
Expand Down
2 changes: 1 addition & 1 deletion .github/pull_request_template.md
Original file line number Diff line number Diff line change
Expand Up @@ -21,7 +21,7 @@ Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
- [ ] 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
Expand Down
2 changes: 1 addition & 1 deletion .machine_readable/6a2/LANGUAGES.deed
Original file line number Diff line number Diff line change
Expand Up @@ -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]
Expand Down
3 changes: 2 additions & 1 deletion .machine_readable/root-allow.txt
Original file line number Diff line number Diff line change
Expand Up @@ -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) ───────────────────────────
Expand Down Expand Up @@ -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
Expand Down
2 changes: 1 addition & 1 deletion .windsurfrules
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down
6 changes: 6 additions & 0 deletions Justfile
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
8 changes: 8 additions & 0 deletions Mustfile
Original file line number Diff line number Diff line change
@@ -0,0 +1,8 @@
# SPDX-License-Identifier: MPL-2.0
# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
#
# 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
2 changes: 1 addition & 1 deletion docs/status/ROADMAP.adoc
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down
2 changes: 2 additions & 0 deletions docs/status/TEST-NEEDS.adoc
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
2 changes: 1 addition & 1 deletion launcher/gui-error.sh
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,7 @@
# SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
#
# 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
Expand Down
2 changes: 1 addition & 1 deletion launcher/resolve-desktop-tools.sh
Original file line number Diff line number Diff line change
Expand Up @@ -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.

# ---------------------------------------------------------------------------
Expand Down
2 changes: 1 addition & 1 deletion launcher/soft-attach.sh
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,7 @@
# SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
#
# 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
Expand Down
54 changes: 54 additions & 0 deletions src/manifest/MANIFEST-SCHEMA.adoc
Original file line number Diff line number Diff line change
@@ -0,0 +1,54 @@
// SPDX-License-Identifier: CC-BY-SA-4.0
// Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
= 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.
6 changes: 3 additions & 3 deletions src/manifest/README.adoc
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
12 changes: 12 additions & 0 deletions src/manifest/examples/refused.manifest
Original file line number Diff line number Diff line change
@@ -0,0 +1,12 @@
# SPDX-License-Identifier: MPL-2.0
# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
#
# 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 ())
2 changes: 1 addition & 1 deletion tests/README.adoc
Original file line number Diff line number Diff line change
Expand Up @@ -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`.
18 changes: 18 additions & 0 deletions tests/manifest_spec.sh
Original file line number Diff line number Diff line change
@@ -0,0 +1,18 @@
#!/usr/bin/env bash
# SPDX-License-Identifier: MPL-2.0
# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
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"
Loading