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
6 changes: 0 additions & 6 deletions .machine_readable/arrival-pack/0.1-AI-MANIFEST.deed

This file was deleted.

8 changes: 0 additions & 8 deletions .machine_readable/arrival-pack/README.adoc

This file was deleted.

6 changes: 0 additions & 6 deletions .machine_readable/coaptation/0.1-AI-MANIFEST.deed

This file was deleted.

8 changes: 0 additions & 8 deletions .machine_readable/coaptation/README.adoc

This file was deleted.

6 changes: 0 additions & 6 deletions .machine_readable/coaptation/core/0.1-AI-MANIFEST.deed

This file was deleted.

8 changes: 0 additions & 8 deletions .machine_readable/coaptation/core/README.adoc

This file was deleted.

6 changes: 0 additions & 6 deletions .machine_readable/coaptation/receipts/0.1-AI-MANIFEST.deed

This file was deleted.

8 changes: 0 additions & 8 deletions .machine_readable/coaptation/receipts/README.adoc

This file was deleted.

6 changes: 0 additions & 6 deletions archetypes/0.1-AI-MANIFEST.deed

This file was deleted.

8 changes: 0 additions & 8 deletions archetypes/README.adoc

This file was deleted.

31 changes: 31 additions & 0 deletions docs/reports/PONS-ASINORUM.adoc
Original file line number Diff line number Diff line change
@@ -0,0 +1,31 @@
// SPDX-License-Identifier: CC-BY-SA-4.0
// Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
= pons-asinorum vs panoply (2026-09-20)

== What happened

GitHub `hyperpolymath/pons-asinorum` **does** have an implementation
(commit `ed2a3c46` M0+M1+M2: workspace, engine skeleton, T0 catalogue +
falsifier). `crates/pons-cli` builds; `pons scan` runs.

The **root README.adoc still says** “Planning complete; implementation
not started.” That sentence is **stale**. That is why Phase 10 treated
it as plan-only (#101).

== What it actually scans

T0 rules + tree-sitter for **Python, JavaScript/JSX, TypeScript/TSX,
Rust only**. Panoply application code is Idris2 + Zig + Bash.

Ran `pons scan` (release binary, 2026-09-20) on this tree: **zero
findings**, exit 0 — expected, not a clean bill of health for Idris/Zig.

== What is not done

* Idris2 / Zig / Bash grammars
* Dataflow / typestate (T1/T2) beyond the skeleton
* README status line

Issue **#101** remains open until either (a) pons covers this estate’s
languages, or (b) we document N/A and close as “scanner not applicable
yet”. Prefer (a). Do not close charter issues on an empty scan.
6 changes: 3 additions & 3 deletions docs/status/ROADMAP.adoc
Original file line number Diff line number Diff line change
Expand Up @@ -32,10 +32,10 @@ Effort: S <1d · M 2–5d · L >1w
|===
| ID | Item | Rationale | Class | Effort | Deps

| H1 | Populate or drop `arrival-pack/` `coaptation/` | empty holdings | 🟡 | S | owner
| H1 | Drop empty `arrival-pack/` `coaptation/` | **done** 2026-09-20 | 🟡 | S | —
| H2 | Live deeds under `descriptiles/` only | **done** 2026-09-20 | 🟡 | S | —
| H3 | `www/dns` keep or delete | not a site | 🟡 | S | owner
| H4 | Remove `archetypes/` if not a mint | template leftover | 🟢 | S | owner
| H3 | Drop `www/dns` (keep `www/.well-known`) | **done** 2026-09-20 | 🟡 | S | —
| H4 | Remove `archetypes/` (not a mint) | **done** 2026-09-20 | 🟢 | S | —
| H5 | Relocate `.gitlab-ci.yml` → `ci/` | GitLab setting | 🟡 | S | GitLab
| H6 | Relocate `.pre-commit-config.yaml` → `ci/` | invocation | 🟡 | S | hooks
| H7 | Gatekeeper `0.x-AI-MANIFEST.deed` stay kv or convert | G1.1 remainder | 🟡 | M | ABNF
Expand Down
7 changes: 7 additions & 0 deletions src/backends/BACKEND-CONTRACT.adoc
Original file line number Diff line number Diff line change
Expand Up @@ -34,4 +34,11 @@ Path: `src/backends/zig-ffi/CONTRACT.adoc`
Same program, two backends ⇒ two manifests. `scripts/emit-manifest.sh`
takes the backend id as argv. Both current backends refuse Core envelopes.

== Coprocessor catalogue (`src/backends/coprocessor/CONTRACT.adoc`)

Named ids (`cpu-x86-64`, `gpu-cuda`, `gpu-rocm`, `gpu-oneapi`, `tpu`,
`npu`, `vpu`, `fpga`, `qpu`, `crypto-pu`, `math-pu`, `physics-pu`,
`io-pu`, `audio-pu`, `video-pu`) all **uphold nothing**. They are
inventory for a future lowering, not Intel/NVIDIA/AMD product support.

Do not close #9 until a lowering exists that preserves a named guarantee.
6 changes: 3 additions & 3 deletions src/backends/README.adoc
Original file line number Diff line number Diff line change
Expand Up @@ -10,9 +10,9 @@ Nothing survives lowering for free.

[IMPORTANT]
====
*Contracts written for `none` and `zig-ffi`.* See
xref:BACKEND-CONTRACT.adoc[BACKEND-CONTRACT.adoc]. No lowering that preserves
a Core guarantee. Issue #9 stays open.
*Contracts written for `none`, `zig-ffi`, and a coprocessor **catalogue**
(FPGA/QPU/TPU/NPU/GPU/…).* All coprocessor ids refuse. No lowering that
preserves a Core guarantee. Issue #9 stays open.
====

== What a backend contract states
Expand Down
59 changes: 59 additions & 0 deletions src/backends/coprocessor/CONTRACT.adoc
Original file line number Diff line number Diff line change
@@ -0,0 +1,59 @@
// SPDX-License-Identifier: CC-BY-SA-4.0
// Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
= Coprocessor backends (catalogue, not a lowering)
:revdate: 2026-09-20

These ids are **named contracts with empty earned sets**. There is no
codegen, no bitstream, no CUDA/ROCm kernel, no QASM. A Core program
lowered here (when lowering exists) **refuses** until a named guarantee
has a check/proof/runtime means.

Do **not** treat this file as “full support” for Intel / NVIDIA / AMD /
Xeon / Ryzen. Host *detection* is a later tool surface; it does not
mint envelopes.

== Classes (ids)

[cols="1,2,3",options="header"]
|===
| Id | Class | Upholds today

| `cpu-x86-64` | High-end x86-64 (Core i9 / Ryzen 9 / Xeon / Ryzen Pro class) | nothing
| `gpu-cuda` | NVIDIA CUDA-class | nothing
| `gpu-rocm` | AMD ROCm-class | nothing
| `gpu-oneapi` | Intel oneAPI/Level Zero-class | nothing
| `tpu` | Tensor / systolic | nothing
| `npu` | On-die NPU | nothing
| `vpu` | Vector (AVX-512 / SVE-class) | nothing
| `fpga` | FPGA bitstream / HLS | nothing
| `qpu` | Quantum (QASM-class) | nothing
| `crypto-pu` | AES-NI / SHA-NI / dedicated crypto | nothing
| `math-pu` | Decimal / big-float / CAS offload | nothing
| `physics-pu` | Physics/simulation offload | nothing
| `io-pu` | DPDK / SPDK / SmartNIC-class | nothing
| `audio-pu` | DSP / audio pipeline | nothing
| `video-pu` | Encode/decode / media | nothing
|===

== Means (all absent)

* Check: none (no Core checker, no ISA verifier).
* Proof: none (no preservation theorem for any class).
* Runtime discipline: none (no driver contract, no device fence).

== Cannot uphold (all classes)

Total-correctness, Core typing, memory-safety of Idris values, timing
side-channel freedom, quantum correctness, FPGA timing closure,
cross-vendor portability.

== Emitter

`scripts/emit-manifest.sh <id>` must refuse (`:earned` empty) for every
id above until that class has a lowering. Default remains `none`.

== Gate to leave this catalogue

A class leaves “nothing” only when: (1) Core checker exists, (2) a
lowering preserves a *named* guarantee, (3) tests fire on a refused
program and pass on an accepted one. Until then issue **#9 stays open**.
5 changes: 5 additions & 0 deletions src/backends/coprocessor/README.adoc
Original file line number Diff line number Diff line change
@@ -0,0 +1,5 @@
// SPDX-License-Identifier: CC-BY-SA-4.0
// Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
= coprocessor

Catalogue of future lowering ids. See `CONTRACT.adoc`. No codegen.
6 changes: 0 additions & 6 deletions www/dns/0.1-AI-MANIFEST.deed

This file was deleted.

8 changes: 0 additions & 8 deletions www/dns/README.adoc

This file was deleted.

Loading