diff --git a/.github/workflows/actions.lock b/.github/workflows/actions.lock index 3b43957..c751eb8 100644 --- a/.github/workflows/actions.lock +++ b/.github/workflows/actions.lock @@ -12,7 +12,8 @@ workflows: - 'dependabot/fetch-metadata@v3.1.0' '.github/workflows/dogfood-gate.yml': - 'actions/checkout@v7.0.1' - '.github/workflows/e2e.yml': [] + '.github/workflows/e2e.yml': + - 'actions/checkout@v7.0.1' '.github/workflows/estate-rules.yml': - 'actions/checkout@v7.0.1' '.github/workflows/governance.yml': [] diff --git a/.github/workflows/e2e.yml b/.github/workflows/e2e.yml index 5ac82a9..6201f27 100644 --- a/.github/workflows/e2e.yml +++ b/.github/workflows/e2e.yml @@ -1,19 +1,9 @@ # This workflow is managed by gh actions-lock. # SPDX-License-Identifier: MPL-2.0 -# This workflow is managed by gh actions-lock. -# This workflow is managed by gh actions-lock. # Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) # -# RSR Standard E2E + Aspect + Benchmark Workflow Template -# -# Covers ALL merge requirement test categories: -# - E2E (end-to-end pipeline tests) -# - Aspect (cross-cutting concern validation) -# - Benchmarks (performance regression detection) -# - Readiness (Component Readiness Grade: D/C/B) -# -# INSTRUCTIONS: Uncomment and customise the section matching your stack. -# Delete sections that don't apply. See examples in each job. +# E2E + aspect + spec gates. Zig is installed from the official tarball +# (no extra Actions). Idris2 is not assumed on the runner. name: E2E + Aspect + Bench on: @@ -23,6 +13,7 @@ on: - 'src/**' - 'ffi/**' - 'tests/**' + - 'verification/**' - '.github/workflows/e2e.yml' pull_request: branches: [main, master] @@ -30,160 +21,40 @@ on: - 'src/**' - 'ffi/**' - 'tests/**' + - 'verification/**' workflow_dispatch: permissions: read-all concurrency: group: e2e-${{ github.ref }} cancel-in-progress: true jobs: -# ─── End-to-End Tests ────────────────────────────────────────────── -# Uncomment ONE of the following e2e job blocks matching your stack. - -## === RUST E2E === -# e2e: -# name: E2E — Full Pipeline -# runs-on: ubuntu-latest -# timeout-minutes: 15 -# steps: -# - uses: actions/checkout@34e114876b0b11c390a56381ad16ebd13914f8d5 # v4 -# - uses: dtolnay/rust-toolchain@4be9e76fd7c4901c61fb841f559994984270fce7 # stable -# - uses: Swatinem/rust-cache@779680da715d629ac1d338a641029a2f4372abb5 # v2 -# - run: cargo build --release -# - run: bash tests/e2e.sh -# # OR: cargo test --test end_to_end -- --nocapture - -## === ZIG FFI E2E === -# e2e: -# name: E2E — FFI Pipeline -# runs-on: ubuntu-latest -# timeout-minutes: 15 -# steps: -# - uses: actions/checkout@34e114876b0b11c390a56381ad16ebd13914f8d5 # v4 -# - uses: goto-bus-stop/setup-zig@abea47f85e598557f500fa1fd2ab7464fcb39406 # v2.2.1 -# with: -# version: 0.15.1 -# - run: cd ffi/zig && zig build test -# - run: bash tests/e2e.sh - -## === ELIXIR E2E === -# e2e: -# name: E2E — Full Pipeline -# runs-on: ubuntu-latest -# timeout-minutes: 15 -# steps: -# - uses: actions/checkout@34e114876b0b11c390a56381ad16ebd13914f8d5 # v4 -# - uses: erlef/setup-beam@fc68ffb90438ef2936bbb3251622353b3dcb2f93 # v1.24.0 -# with: -# otp-version: '27.0' -# elixir-version: '1.17' -# - run: mix deps.get && mix compile --warnings-as-errors -# - run: mix test test/integration/e2e_test.exs --trace - -## === DENO/RESCRIPT E2E === -# e2e: -# name: E2E — Full Pipeline -# runs-on: ubuntu-latest -# timeout-minutes: 15 -# steps: -# - uses: actions/checkout@34e114876b0b11c390a56381ad16ebd13914f8d5 # v4 -# - uses: denoland/setup-deno@667a34cdef165d8d2b2e98dde39547c9daac7282 # v2.0.4 -# with: -# deno-version: v2.x -# - run: deno install --node-modules-dir=auto -# - run: deno task res:build # ReScript compile -# - run: deno test tests/e2e/ - -## === PLAYWRIGHT (Browser E2E) === -# e2e-playwright: -# name: Playwright — ${{ matrix.project }} -# runs-on: ubuntu-latest -# timeout-minutes: 20 -# strategy: -# fail-fast: false -# matrix: -# project: [chromium-1080p, firefox-1080p, webkit-1080p] -# steps: -# - uses: actions/checkout@34e114876b0b11c390a56381ad16ebd13914f8d5 # v4 -# - uses: denoland/setup-deno@667a34cdef165d8d2b2e98dde39547c9daac7282 # v2.0.4 -# with: -# deno-version: v2.x -# - run: deno install --node-modules-dir=auto -# - run: npx playwright install --with-deps -# - run: npx playwright test --project=${{ matrix.project }} -# - uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02 # v4 -# if: failure() -# with: -# name: playwright-traces-${{ matrix.project }} -# path: test-results/**/trace.zip -# retention-days: 7 - -## === HASKELL E2E === -# e2e: -# name: E2E — Full Pipeline -# runs-on: ubuntu-latest -# timeout-minutes: 15 -# steps: -# - uses: actions/checkout@34e114876b0b11c390a56381ad16ebd13914f8d5 # v4 -# - uses: haskell-actions/setup@cd0d9bdd65b20557f41bea4dbe43d0b5fbbfe553 # v2.11.0 -# with: -# ghc-version: '9.6' -# cabal-version: '3.10' -# - run: cabal build all -# - run: bash tests/integration-test.sh - -# ─── Aspect Tests ────────────────────────────────────────────────── -# Cross-cutting concerns: thread safety, ABI contracts, SPDX, dangerous patterns -# Uncomment and customise: - -# aspect-tests: -# name: Aspect — Architectural Invariants -# runs-on: ubuntu-latest -# timeout-minutes: 10 -# steps: -# - uses: actions/checkout@34e114876b0b11c390a56381ad16ebd13914f8d5 # v4 -# - run: bash tests/aspect_tests.sh - -# ─── Benchmarks ──────────────────────────────────────────────────── -# Performance regression detection. Uncomment matching stack: - -## === RUST BENCH === -# benchmarks: -# name: Bench — Performance Regression -# runs-on: ubuntu-latest -# timeout-minutes: 15 -# steps: -# - uses: actions/checkout@34e114876b0b11c390a56381ad16ebd13914f8d5 # v4 -# - uses: dtolnay/rust-toolchain@4be9e76fd7c4901c61fb841f559994984270fce7 # stable -# - uses: Swatinem/rust-cache@779680da715d629ac1d338a641029a2f4372abb5 # v2 -# - run: cargo bench 2>&1 | tee /tmp/bench-results.txt -# - uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02 # v4 -# if: always() -# with: -# name: benchmark-results -# path: /tmp/bench-results.txt -# retention-days: 30 - -## === ZIG BENCH === -# benchmarks: -# name: Bench — Performance Regression -# runs-on: ubuntu-latest -# timeout-minutes: 15 -# steps: -# - uses: actions/checkout@34e114876b0b11c390a56381ad16ebd13914f8d5 # v4 -# - uses: goto-bus-stop/setup-zig@abea47f85e598557f500fa1fd2ab7464fcb39406 # v2.2.1 -# with: -# version: 0.15.1 -# - run: cd ffi/zig && zig build bench - -# ─── Readiness (CRG) ────────────────────────────────────────────── -# Component Readiness Grade: D (runs) → C (correct) → B (edge cases) - -# readiness: -# name: Readiness — Grade D/C/B -# runs-on: ubuntu-latest -# timeout-minutes: 10 -# steps: -# - uses: actions/checkout@34e114876b0b11c390a56381ad16ebd13914f8d5 # v4 -# - uses: dtolnay/rust-toolchain@4be9e76fd7c4901c61fb841f559994984270fce7 # stable -# - uses: Swatinem/rust-cache@779680da715d629ac1d338a641029a2f4372abb5 # v2 -# - run: cargo test --test readiness -- --nocapture + aspect-tests: + name: Aspect — Architectural Invariants + runs-on: ubuntu-latest + timeout-minutes: 10 + steps: + - uses: actions/checkout@v7.0.1 + - run: bash tests/aspect_tests.sh + - run: bash tests/core_spec.sh + - run: bash tests/evidence_spec.sh + - run: bash tests/manifest_spec.sh + - run: bash tests/backend_spec.sh + - run: bash tests/projection_spec.sh + + e2e-zig: + name: E2E — Zig FFI + runs-on: ubuntu-latest + timeout-minutes: 15 + steps: + - uses: actions/checkout@v7.0.1 + - name: Install Zig 0.15.1 + run: | + set -euo pipefail + curl -fsSL -o /tmp/zig.tar.xz \ + https://ziglang.org/download/0.15.1/zig-x86_64-linux-0.15.1.tar.xz + tar -xJf /tmp/zig.tar.xz -C /tmp + echo "/tmp/zig-x86_64-linux-0.15.1" >> "$GITHUB_PATH" + - run: zig version + - run: bash tests/e2e.sh + - run: bash tests/p2p.sh + - run: cd src/api/zig && zig test adapter.zig diff --git a/.machine_readable/6a2/AGENTIC.deed b/.machine_readable/6a2/AGENTIC.deed index 6abf434..d05b87d 100644 --- a/.machine_readable/6a2/AGENTIC.deed +++ b/.machine_readable/6a2/AGENTIC.deed @@ -1,51 +1,21 @@ -# SPDX-License-Identifier: MPL-2.0 -# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) -# -# AGENTIC.deed — AI agent constraints and capabilities -# Defines what AI agents can and cannot do in this repository. - -[metadata] -version = "0.1.0" -last-updated = "2026-04-11" - -[agent-permissions] -can-edit-source = true -can-edit-tests = true -can-edit-docs = true -can-edit-config = true -can-create-files = true - -[agent-constraints] -# What AI agents must NOT do: -# - Never use banned language patterns (believe_me, unsafeCoerce, etc.) -# - Never commit secrets or credentials -# - Never use banned languages (TypeScript, Python, Go, etc.) -# - Never place state files in repository root (must be in .machine_readable/) -# - Never use AGPL license (use MPL-2.0) - -[maintenance-integrity] -fail-closed = true -require-evidence-per-step = true -allow-silent-skip = false -require-rerun-after-fix = true -release-claim-requires-hard-pass = true - -# ============================================================================ -# METHODOLOGY (ADR-002) -# ============================================================================ -# Detailed methodology configuration lives in: -# .machine_readable/bot_directives/methodology.deed -# .machine_readable/bot_directives/coverage.deed -# .machine_readable/bot_directives/debt.deed -# -# AGENTIC.deed declares WHAT agents can do (permissions, gating). -# bot_directives/ declares HOW agents should work (methodology). - -[methodology] -instructions-dir = ".machine_readable/bot_directives/" -default-mode = "hybrid" - -[automation-hooks] -# on-enter: Read 0-AI-MANIFEST.deed, then STATE.deed, then bot_directives/ -# on-exit: Update STATE.deed, coverage.deed, and debt.deed with session outcomes -# on-commit: Run just validate-rsr +;; SPDX-FileCopyrightText: © 2026 Jonathan D.A. Jewell (hyperpolymath) +;; SPDX-License-Identifier: MPL-2.0 +(repo-deed + :schema-version "1.0.0" + :canonical-name "panoply-agentic" + :repo-uuid #u5"hyperpolymath/panoply" + :beholding-chora #u5"estate/chora" + :last-updated "2026-09-20" + (agent-permissions + :can-edit-source true + :can-edit-tests true + :can-edit-docs true + :can-edit-config true + :can-create-files true) + (maintenance-integrity + :fail-closed true + :require-evidence-per-step true + :allow-silent-skip false) + (methodology + :instructions-dir ".machine_readable/bot_directives/" + :default-mode "hybrid")) diff --git a/.machine_readable/6a2/LANGUAGES.deed b/.machine_readable/6a2/LANGUAGES.deed index 7957ff8..f1f4d82 100644 --- a/.machine_readable/6a2/LANGUAGES.deed +++ b/.machine_readable/6a2/LANGUAGES.deed @@ -1,22 +1,16 @@ -# SPDX-License-Identifier: MPL-2.0 -# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) -# -# LANGUAGES.deed — Languages present in this repository -# -[metadata] -version = "0.1.0" -last-updated = "2026-06-21" - -[present] -# Languages currently in the tree. -abi-proofs = "idris2" # src/interface/Abi/, verification/proofs/idris2/ -ffi = "zig" # src/interface/ffi/ -proofs = ["coq", "agda", "idris2"] # verification/proofs/ -config = ["nickel", "deed"] # .machine_readable/ -build = ["just", "bash"] - -[planned] -# The Panoply Core checker, evidence formats, and manifest tooling are not yet -# implemented (see STATE.deed). Their implementation language is TBD per the -# design discipline (docs/architecture/DESIGN-DISCIPLINE.adoc). -core = "TBD" +;; SPDX-FileCopyrightText: © 2026 Jonathan D.A. Jewell (hyperpolymath) +;; SPDX-License-Identifier: MPL-2.0 +(repo-deed + :schema-version "1.0.0" + :canonical-name "panoply-languages" + :repo-uuid #u5"hyperpolymath/panoply" + :beholding-chora #u5"estate/chora" + :last-updated "2026-09-20" + (present + :abi-proofs "idris2" + :ffi "zig" + :proofs ("idris2") + :config ("nickel" "deed") + :build ("just" "bash")) + (planned + :core "TBD")) diff --git a/.machine_readable/6a2/NEUROSYM.deed b/.machine_readable/6a2/NEUROSYM.deed index 569f862..3396439 100644 --- a/.machine_readable/6a2/NEUROSYM.deed +++ b/.machine_readable/6a2/NEUROSYM.deed @@ -1,23 +1,12 @@ -# SPDX-License-Identifier: MPL-2.0 -# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) -# -# NEUROSYM.deed — Neurosymbolic integration metadata -# Configuration for Hypatia scanning and symbolic reasoning. - -[metadata] -version = "0.1.0" -last-updated = "2026-04-11" - -[hypatia-config] -scan-enabled = true -scan-depth = "standard" # quick | standard | deep -report-format = "logtalk" - -[symbolic-rules] -# Custom symbolic rules for this project -# - { name = "no-unsafe-ffi", pattern = "believe_me|unsafeCoerce", severity = "critical" } - -[neural-config] -# Neural pattern detection settings -# confidence-threshold = 0.85 -# model = "hypatia-v2" +;; SPDX-FileCopyrightText: © 2026 Jonathan D.A. Jewell (hyperpolymath) +;; SPDX-License-Identifier: MPL-2.0 +(repo-deed + :schema-version "1.0.0" + :canonical-name "panoply-neurosym" + :repo-uuid #u5"hyperpolymath/panoply" + :beholding-chora #u5"estate/chora" + :last-updated "2026-09-20" + (hypatia-config + :scan-enabled true + :scan-depth "standard" + :report-format "logtalk")) diff --git a/.machine_readable/6a2/PLAYBOOK.deed b/.machine_readable/6a2/PLAYBOOK.deed index 33c82df..2c3d96b 100644 --- a/.machine_readable/6a2/PLAYBOOK.deed +++ b/.machine_readable/6a2/PLAYBOOK.deed @@ -1,137 +1,12 @@ -# SPDX-License-Identifier: MPL-2.0 -# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) -# -# PLAYBOOK.deed — Operational playbook -# Runbooks, incident response, deployment procedures. - -[metadata] -version = "0.1.0" -last-updated = "2026-04-11" - -[deployment] -# method = "gitops" # gitops | manual | ci-triggered -# target = "container" # container | binary | library | wasm - -[incident-response] -# 1. Check .machine_readable/6a2/STATE.deed for current status -# 2. Review recent commits and CI results -# 3. Run `just validate` to check compliance -# 4. Run `just security` to audit for vulnerabilities - -[release-process] -# 1. Update version in STATE.deed, META.deed, Justfile -# 2. Run `just release-preflight` (validate + quality + security + maint-hard-pass) -# 3. Optional local permission hardening: `just perms-snapshot && just perms-lock` -# 4. Tag and push -# 5. Restore local permissions if needed: `just perms-restore` -# 6. Run `just container-push` if applicable - -[maintenance-operations] -# Baseline audit: -# just maint-audit -# Hard release gate: -# just maint-hard-pass -# Permission audit: -# just perms-audit - -[rsr-repo-skeleton] -# Canonical organisation of any RSR-derived repository. -# Used by tooling, human onboarding, and the scheduled downstream sweep agent. -# The 5-PR cleanup pattern (below) brings a non-conforming repository into -# compliance with this skeleton. -# -# This section is the single source of truth for "what does an RSR repo look -# like?". Other docs (TOPOLOGY, AUDIT, etc.) describe the repo at hand; -# this describes the canonical shape that all RSR repos share. - -skeleton-version = "1.0" -last-updated = "2026-04-30" -authority-allowlist = ".machine_readable/root-allow.txt" -enforcement-workflow = ".github/workflows/estate-rules.yml" - -# === Required at root === -# README.adoc High-level pitch (project entry point) -# AUDIT.adoc Local gate summary (release-readiness) -# EXPLAINME.adoc Developer deep-dive (architecture & invariants) -# 0-AI-MANIFEST.deed AI agent work-allocation policy -# LICENSE Repo license (root-bound by convention) -# CHANGELOG.md One of the recognised .md exceptions (see below) -# Justfile Task runner — thin, imports per-section files from build/just/ -# coordination.k9 Repo-local session binding - -# === Required directories === -# .github/ CONTRIBUTING.md, CODE_OF_CONDUCT.md, SECURITY.md, workflows/ -# .machine_readable/ AI manifests (0.1-AI-MANIFEST.deed), 6a2/ checkpoints, -# contractiles/, configs/, anchors/, policies/, scripts/, svc/ -# build/ contractile.just, guix.scm, .guix-channel, Containerfile, -# just/*.just (Justfile section imports) -# docs/ onboarding/, status/, architecture/, governance/ (all .adoc) -# session/ dispatch.sh, custom-checks.k9, local-hooks.sh -# src/ Project source (Idris2 ABI under abi/, Zig FFI under ffi/) -# tests/, benches/, examples/, features/, scripts/, verification/, container/ - -# === Documentation format rule === -# `.adoc` is the default for all general docs (TOPOLOGY, READINESS, ROADMAP, -# TEST-NEEDS, PROOF-NEEDS, PROOF-STATUS, llm-warmup-*, etc.). -# -# `.md` is reserved ONLY for files GitHub's community-health rules -# special-case by name: -# CONTRIBUTING.md CODE_OF_CONDUCT.md SECURITY.md CHANGELOG.md -# -# Enforcement: `scripts/check-no-md-in-docs.sh` (fails if any *.md under docs/). - -# === Banned: ziguage === -# V (vlang.io) is banned estate-wide. Replaced by `zig-unified-api-adapter` -# (16 endpoints + transaction-based firewall gating). Do not introduce -# zig code, scaffolders, or references. Note that Coq theorem files use -# the same `.v` extension and are unaffected — the rule looks at content -# patterns, not the extension. -# -# Enforcement: `scripts/check-no-vlang.sh`. - -# === Justfile structure (post-split) === -# The root Justfile is thin — it holds `set` directives, project metadata -# variables, and the `default`/`help`/`info` recipes. Each major section -# lives in its own file under build/just/ and is brought in via `import?`. -# -# Imported sections (in the canonical split): -# build/just/init.just INIT recipe (template bootstrap) -# build/just/assess.just self-assess + verify (OpenSSF compliance) -# build/just/validate.just validate-rsr/state/ai-install + aggregate -# build/just/proofs.just proof-check-{all,idris2,lean4,agda,coq}, -# proof-scan-dangerous, proof-status -# build/just/groove.just Groove protocol setup (after zig removed) -# -# Daily-use recipes (BUILD, TEST, LINT, RUN, DEPS, DOCS, CONTAINER, CI, -# SECURITY, STATE, GUIX/NIX, MATRIX, VERSION CONTROL, UTILITIES, SESSION) -# stay in the root Justfile where users expect to find them. - -# === 5-PR cleanup pattern === -# Apply these branches (in order) to bring a non-conforming downstream repo -# into compliance with this skeleton: -# -# 1. chore/root-cleanup Relocate root sprawl per root-allow.txt; add -# scripts/check-root-shape.sh; remove stub -# health files shadowed by .github/ versions. -# 2. chore/remove-zig Purge zig remnants (gen-v-connector recipe, -# "V-TRIPLE" section header, "V-triple -# connectors" comment in groove.deed). -# 3. chore/md-to-adoc Port general docs in docs/ from .md to .adoc; -# update validate-template.sh to accept .adoc -# fallbacks. -# 4. chore/estate-rules-ci Add scripts/check-no-md-in-docs.sh + check-no- -# vlang.sh + .github/workflows/estate-rules.yml. -# 5. chore/-hygiene Repo-specific drift cleanup (case collisions, -# template-derivation drift in titles, etc.). - -# === Reference scripts === -# scripts/check-root-shape.sh Root allowlist validator -# scripts/check-no-md-in-docs.sh AsciiDoc-by-default validator -# scripts/check-no-vlang.sh zig ban validator -# scripts/validate-template.sh Aggregate RSR compliance (workflows, SPDX, etc.) - -# === Reference memory entries (for AI agents) === -# feedback_adoc_default_md_for_githealth AsciiDoc-by-default rule -# feedback_v_lang_banned zig ban -# project_zig_unified_api Replacement for v-triple/zig -# feedback_gh_workflow_scope OAuth scope for workflow files +;; SPDX-FileCopyrightText: © 2026 Jonathan D.A. Jewell (hyperpolymath) +;; SPDX-License-Identifier: MPL-2.0 +;; Operational notes remain in docs/; this deed only carries identity + pointers. +(repo-deed + :schema-version "1.0.0" + :canonical-name "panoply-playbook" + :repo-uuid #u5"hyperpolymath/panoply" + :beholding-chora #u5"estate/chora" + :last-updated "2026-09-20" + :authority-allowlist ".machine_readable/root-allow.txt" + :enforcement-workflow ".github/workflows/estate-rules.yml" + :skeleton-version "1.0") diff --git a/.machine_readable/6a2/STATE.deed b/.machine_readable/6a2/STATE.deed index beb46fd..74fe77c 100644 --- a/.machine_readable/6a2/STATE.deed +++ b/.machine_readable/6a2/STATE.deed @@ -23,6 +23,6 @@ (milestone :name charter :completion 100) (milestone :name core :completion 20) (milestone :name evidence :completion 20) - (milestone :name manifest :completion 0) - (milestone :name projections :completion 0) - (milestone :name backends :completion 0))) + (milestone :name manifest :completion 40) + (milestone :name projections :completion 20) + (milestone :name backends :completion 20))) diff --git a/.machine_readable/6a2/anchors/ANCHOR.deed b/.machine_readable/6a2/anchors/ANCHOR.deed index 77561f7..33c73da 100644 --- a/.machine_readable/6a2/anchors/ANCHOR.deed +++ b/.machine_readable/6a2/anchors/ANCHOR.deed @@ -1,62 +1,17 @@ -# SPDX-License-Identifier: MPL-2.0 -# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) -# -# ANCHOR.deed - authoritative anchor for this repository - -[metadata] -version = "1.0.0" -last-updated = "2026-06-21" - -[anchor] -schema = "hyperpolymath.anchor/1" -repo = "hyperpolymath/panoply" -authority = "upstream-canonical" - -purpose = [ - "Define canonical semantics and policy boundaries for this repository.", - "Declare what downstream/satellite repos can extend but not redefine.", - "Provide a stable golden path and invariant contract for release readiness.", -] - -[identity] -project = "Panoply" -kind = "monorepo" # language | library | service | tool -one-sentence = "An envelope-first language discipline: every safety claim explicit, scoped, inspectable, and mechanically accountable." -domain = "programming-languages" - -[semantic-authority] -policy = "canonical" - -owns = [ - "Project semantics and specification", - "Invariant definitions and contractiles", - "Reference implementation behavior", -] - -[implementation-policy] -allowed = ["Rust", "Idris2", "Zig", "Scheme", "Shell", "Just", "AsciiDoc", "Markdown"] -forbidden = ["Node.js", "npm"] - -[golden-path] -smoke-test-command = [ - "just test", - "just quality", -] - -success-criteria = [ - "Core tests pass", - "Quality gates pass", - "No unresolved critical security findings", -] - -[satellite-policy] -must-pin-upstream = true -must-declare-authority = true -must-have-anchor = true -must-have-golden-path = true - -[semantic-authority-files] -language-spec = "SPECIFICATION.md" -formal-proofs = "docs/proofs/PROOFS.adoc" -type-theory = "docs/theory/THEORY.adoc" -algorithms = "docs/theory/ALGORITHMS.adoc" +;; SPDX-FileCopyrightText: © 2026 Jonathan D.A. Jewell (hyperpolymath) +;; SPDX-License-Identifier: MPL-2.0 +(repo-deed + :schema-version "1.0.0" + :canonical-name "panoply-anchor" + :repo-uuid #u5"hyperpolymath/panoply" + :beholding-chora #u5"estate/chora" + :last-updated "2026-09-20" + :schema "hyperpolymath.anchor/1" + :authority "upstream-canonical" + (identity + :project "Panoply" + :kind "monorepo" + :domain "programming-languages") + (implementation-policy + :allowed ("Idris2" "Zig" "Scheme" "Shell" "Just" "AsciiDoc" "Markdown") + :forbidden ("Python" "Go" "TypeScript"))) diff --git a/.machine_readable/bot_directives/coverage.deed b/.machine_readable/bot_directives/coverage.deed index 31632e0..162a573 100644 --- a/.machine_readable/bot_directives/coverage.deed +++ b/.machine_readable/bot_directives/coverage.deed @@ -1,61 +1,9 @@ -# SPDX-License-Identifier: MPL-2.0 -# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) -# -# coverage.deed — Session coverage tracking -# Updated at the end of each AI agent session. -# Persists what was visited, what was skipped, and what has MUSTs. -# -# Reference: ADR-002 in standards/agentic-a2ml/docs/ - -[metadata] -version = "1.0.0" -last-updated = "2026-06-21" - -# ============================================================================ -# COVERAGE STATE -# ============================================================================ -# Updated by agents at session end. Tracks which components have been -# visited and which have known MUSTs that were skipped. - -[coverage] -total-components = 0 -visited-components = 0 -coverage-percent = 0 - -# ============================================================================ -# VISITED COMPONENTS -# ============================================================================ -# Component → session date + ring reached -# Agents add entries as they work through components. -# -# Example: -# [coverage.visited.emergency-room] -# date = "2026-03-23" -# ring = 2 -# fixes = 3 -# notes = "boot-guardian built, shutdown-marshal built" - -# ============================================================================ -# SKIPPED COMPONENTS WITH MUSTS -# ============================================================================ -# Components with known MUSTs that were not visited in the most recent session. -# These become P1 inputs for the next session's Phase 0. -# -# Example: -# [coverage.skipped-musts.session-sentinel] -# priority = "P0" -# issue = "56 SIGABRTs in 4 days, D-Bus race condition" -# discovered = "2026-03-23" - -# ============================================================================ -# CHERRY-PICKING AUDIT -# ============================================================================ -# At session end, agents report whether they chose easy work over hard work. -# This is the accountability mechanism for the weighted priority system. -# -# [coverage.cherry-picking] -# easy-high-completed = 3 -# hard-high-completed = 1 -# easy-low-completed = 2 -# hard-low-deferred = 4 -# assessment = "Correctly prioritised — all MUST items addressed before COULDs" +;; SPDX-FileCopyrightText: © 2026 Jonathan D.A. Jewell (hyperpolymath) +;; SPDX-License-Identifier: MPL-2.0 +(repo-deed + :schema-version "1.0.0" + :canonical-name "panoply-coverage" + :repo-uuid #u5"hyperpolymath/panoply" + :beholding-chora #u5"estate/chora" + :last-updated "2026-09-20" + (coverage :total-components 0 :visited-components 0 :coverage-percent 0)) diff --git a/.machine_readable/bot_directives/debt.deed b/.machine_readable/bot_directives/debt.deed index 230726b..c7f77b9 100644 --- a/.machine_readable/bot_directives/debt.deed +++ b/.machine_readable/bot_directives/debt.deed @@ -1,49 +1,9 @@ -# SPDX-License-Identifier: MPL-2.0 -# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) -# -# debt.deed — Meander debt list -# Things found but not fixed. Carried between sessions. -# Becomes the next session's Phase 0 input. -# -# Reference: ADR-002 in standards/agentic-a2ml/docs/ - -[metadata] -version = "1.0.0" -last-updated = "2026-06-21" - -# ============================================================================ -# DEBT ITEMS -# ============================================================================ -# Each item has: component, issue, effort (easy|medium|hard), impact (high|medium|low), -# priority (should|could), and discovered date. -# -# Items are consumed (removed) when fixed. New items are added at session end. -# The debt list prevents the "one more wave" loop — found things are persisted, -# not forgotten, and not used as justification for infinite meandering. - -# ============================================================================ -# SHOULD — would fix next wave -# ============================================================================ -# These are inputs for the next session if the user says "keep going". -# -# Example: -# [[debt.should]] -# component = "system-tools/monitoring/observatory" -# issue = "Stale duplicate of root observatory/" -# effort = "easy" -# impact = "medium" -# discovered = "2026-03-23" - -# ============================================================================ -# COULD — would fix eventually -# ============================================================================ -# These are low-priority items that don't justify a session on their own. -# They get picked up when an agent is in the area for other reasons. -# -# Example: -# [[debt.could]] -# component = "cicada" -# issue = "RSR_OUTLINE.adoc references banned AGPL-3.0" -# effort = "easy" -# impact = "low" -# discovered = "2026-03-23" +;; SPDX-FileCopyrightText: © 2026 Jonathan D.A. Jewell (hyperpolymath) +;; SPDX-License-Identifier: MPL-2.0 +(repo-deed + :schema-version "1.0.0" + :canonical-name "panoply-debt" + :repo-uuid #u5"hyperpolymath/panoply" + :beholding-chora #u5"estate/chora" + :last-updated "2026-09-20" + (debt :should () :could ())) diff --git a/.machine_readable/bot_directives/methodology.deed b/.machine_readable/bot_directives/methodology.deed index 0e7e8cd..e0fe8c4 100644 --- a/.machine_readable/bot_directives/methodology.deed +++ b/.machine_readable/bot_directives/methodology.deed @@ -1,107 +1,15 @@ -# SPDX-License-Identifier: MPL-2.0 -# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) -# -# methodology.deed — AI agent methodology configuration -# Declares how agents should approach work in this repository. -# Read at session start by any AI agent (Claude, Gemini, Copilot, etc.) -# -# Reference: ADR-002 in standards/agentic-a2ml/docs/ - -[metadata] -version = "1.0.0" -last-updated = "2026-06-21" -spec = "https://github.com/hyperpolymath/standards/blob/main/agentic-a2ml/docs/ADR-002-methodology-layer.adoc" - -# ============================================================================ -# MODE SELECTION -# ============================================================================ -# convergent: find gaps, fill them, build infrastructure (default for ops/infra) -# divergent: find what's strongest, push it further (for research/creative) -# hybrid: audit 20% of budget, then focus 80% on top MUSTs (default for most) - -[methodology] -default-mode = "hybrid" -ring-ceiling = 2 # Hard ceiling for ring expansion (0-3) -wave-cap = 2 # Max waves before requiring user "keep going" -spike-required = true # Every session must ship code, not just designs - -# ============================================================================ -# PRIORITY WEIGHTS -# ============================================================================ -# MUST (3x): Blocking the current work → fix immediately -# SHOULD (2x): Degrading quality of current work → fix if in zone -# COULD (1x): Improving quality of adjacent work → add to debt list - -[methodology.priority-weights] -must = 3 -should = 2 -could = 1 - -# ============================================================================ -# CONVERGENT BUDGET (when mode = convergent or hybrid) -# ============================================================================ -# How to allocate effort across work types. -# Prevents over-polishing docs while structural work waits. - -[methodology.convergent-budget] -structural = 70 # % for new modules, compilation fixes, wiring, integration -corrective = 20 # % for bugs found, broken imports, stale references -perfective = 10 # % for SPDX headers, doc updates, formatting, style - -# ============================================================================ -# UNIQUE STRENGTH (when mode = divergent) -# ============================================================================ -# What makes this project special. Agents should DEEPEN this, not broaden it. -# Customise this per project — the template default is generic. - -[methodology.unique-strength] -description = "explicit, scoped, inspectable safety envelopes" -deepen-not-broaden = true - -# ============================================================================ -# DIVERGENT INVARIANTS -# ============================================================================ -# Constraints that divergent mode must NOT violate. -# These are the riverbanks — diverge within them, not across. -# "Amplify uniqueness" means deepen, not broaden. -# -# Test before any divergent action: -# "Does this deepen the existing strength, or add a parallel strength?" -# If parallel → stop. Note as cross-project insight. - -[methodology.divergent-invariants] -rules = [ - # Customise per project. Examples: - # "Idris2 only for formal verification — no Lean4, Coq, Agda", - # "believe_me count must remain zero", - # "FFI architecture: Idris2 → RefC → Zig → C ABI (no shortcuts)", -] - -# Optional: language invariant for the core strength -# If set, divergent mode will not introduce other languages for this purpose -# language-invariant = "idris2" - -# ============================================================================ -# CONSTRAINT HINTS -# ============================================================================ -# Help Phase 0 find the critical chain faster. -# Updated at session end with newly discovered constraints. - -[methodology.known-constraints] -constraints = [ - # Customise per project. Examples: - # "End-to-end build has never been verified", - # "libproject.so does not exist yet — all bindings call stubs", -] - -# ============================================================================ -# STATE FILE VALIDATION -# ============================================================================ -# Phase 0 reads STATE.deed first but it may be broken. -# These rules detect corrupt/template/stale state files. - -[methodology.state-validation] -reject-if-contains = ["{{PLACEHOLDER}}", "PANOPLY", "rsr-template-repo"] -reject-if-project-name-mismatch = true -staleness-threshold-days = 90 -fallback-files = ["TODO.md", "TODO.adoc", "ROADMAP.adoc", "README.adoc"] +;; SPDX-FileCopyrightText: © 2026 Jonathan D.A. Jewell (hyperpolymath) +;; SPDX-License-Identifier: MPL-2.0 +(repo-deed + :schema-version "1.0.0" + :canonical-name "panoply-methodology" + :repo-uuid #u5"hyperpolymath/panoply" + :beholding-chora #u5"estate/chora" + :last-updated "2026-09-20" + (methodology + :default-mode "hybrid" + :ring-ceiling 2 + :wave-cap 2 + :spike-required true) + (priority-weights :must 3 :should 2 :could 1) + (unique-strength :description "explicit, scoped, inspectable safety envelopes")) diff --git a/.machine_readable/policies/MAINTENANCE-AXES.deed b/.machine_readable/policies/MAINTENANCE-AXES.deed index eb38e38..8517fab 100644 --- a/.machine_readable/policies/MAINTENANCE-AXES.deed +++ b/.machine_readable/policies/MAINTENANCE-AXES.deed @@ -1,54 +1,14 @@ -# SPDX-License-Identifier: MPL-2.0 -# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) -# -# Canonical maintenance governance model - -[metadata] -version = "1.0.0" -last-updated = "2026-06-21" -scope = "repo" - -[discovery] -human-entrypoints = [ - "README.adoc", - "docs/maintenance/MAINTENANCE-CHECKLIST.md", - "docs/practice/SOFTWARE-DEVELOPMENT-APPROACH.adoc", -] -machine-entrypoints = [ - ".machine_readable/policies/MAINTENANCE-AXES.deed", - ".machine_readable/policies/MAINTENANCE-CHECKLIST.deed", - ".machine_readable/policies/SOFTWARE-DEVELOPMENT-APPROACH.deed", - ".machine_readable/6a2/META.deed", - ".machine_readable/ai/README.adoc", - ".machine_readable/bot_directives/README.scm", -] -bots = ["hypatia", "gitbot-fleet", "repo visitors"] - -[axes] -axis-1 = "must > intend > like" -axis-2 = "corrective > adaptive > perfective" -axis-3 = "systems > compliance > effects" -execution-order = "axis-1 > axis-2 > axis-3" - -[axis-1-scoping] -required = true -sources = "README, roadmap, status docs, maintenance checklist, CI/security docs" -markers = "TODO/FIXME/XXX/HACK/STUB/PARTIAL" -idris-unsound-markers = "believe_me/assert_total" -output = "scoped work assembly in must/intend/like buckets" - -[axis-2-maintenance] -corrective-first = true -adaptive-second = true -adaptive-focus = "scope changes, stale references, obsolete work culling" -perfective-third = true -perfective-source = "honest state from axis-1 after corrective/adaptive updates" - -[axis-3-audit] -systems-check = true -compliance-check = true -effects-check = true -compliance-focus = "seams/compromises/exception register and anti-drift" -compliance-tooling = "panic-attack" -effects-tooling = "ecological checking with sustainabot guidance" -effects-evidence = "benchmark evidence and maintainer dialogue/status review" +;; SPDX-FileCopyrightText: © 2026 Jonathan D.A. Jewell (hyperpolymath) +;; SPDX-License-Identifier: MPL-2.0 +(repo-deed + :schema-version "1.0.0" + :canonical-name "panoply-maintenance-axes" + :repo-uuid #u5"hyperpolymath/panoply" + :beholding-chora #u5"estate/chora" + :last-updated "2026-09-20" + :scope "repo" + (axes + :axis-1 "must > intend > like" + :axis-2 "corrective > adaptive > perfective" + :axis-3 "systems > compliance > effects" + :execution-order "axis-1 > axis-2 > axis-3")) diff --git a/.machine_readable/policies/MAINTENANCE-CHECKLIST.deed b/.machine_readable/policies/MAINTENANCE-CHECKLIST.deed index 6a3771e..f443d48 100644 --- a/.machine_readable/policies/MAINTENANCE-CHECKLIST.deed +++ b/.machine_readable/policies/MAINTENANCE-CHECKLIST.deed @@ -1,159 +1,15 @@ -# SPDX-License-Identifier: MPL-2.0 -# Cross-repo maintenance baseline (machine-readable canonical) - -[metadata] -version = "1.1.0" -last-updated = "2026-02-24" -scope = "cross-repo" -source-human = "docs/governance/MAINTENANCE-CHECKLIST.adoc" -companion-human = "docs/governance/SOFTWARE-DEVELOPMENT-APPROACH.adoc" -companion-machine = ".machine_readable/policies/SOFTWARE-DEVELOPMENT-APPROACH.deed" - -[policy] -single-source = true -notes = "Use this file as canonical machine policy and keep markdown synchronized." - -[maintenance-axes] -scoping-first = true -execution-order = ["scoping", "axis-1", "axis-2", "axis-3"] -axis-1 = "must > intend > like" -axis-2 = "corrective > adaptive > perfective" -axis-3 = "systems > compliance > effects" - -[scoping] -inputs_required = [ - "README", - "roadmap", - "status-docs", - "maintenance-checklist", - "ci-and-security-docs", -] - -marker_scan_required = [ - "TODO", - "FIXME", - "XXX", - "HACK", - "STUB", - "PARTIAL", -] - -idris_unsound_scan_required = [ - "believe_me", - "assert_total", -] - -scope_assembly_buckets = ["must", "intend", "like"] - -[axis-2-maintenance-rules] -corrective-first = true -adaptive-second = true -adaptive_examples = [ - "scope-change reconciliation", - "stale-reference removal", - "obsolete-work culling", -] -perfective-third = true -perfective_source = "axis-1 honest state after corrective/adaptive updates" - -[axis-3-audit-rules] -systems-check = true -documentation-honesty-check = true -safety-security-accounted-check = true -effects-review-check = true -benchmark-evidence-required = true -maintainer-dialogue-review-required = true -compliance-seams-check = true -exception-register-required = true -exception-bounded-scope-required = true -policy-drift-contamination-check = true -example-drift-risk = "single TypeScript exception causing broad ReScript->TypeScript migration" -compliance-tooling = "panic-attack" -effects-tooling = "ecological checking with sustainabot guidance" - -[generic-cleanup-finish-off] -root-cleanup-required = true -stale-work-cull-required = true -docs-parity-required = true -machine-human-sync-required = true -compliance-finish-off-required = true -effects-finish-off-required = true -release-prep-summary-required = true -next-actions-required = ["corrective", "adaptive", "perfective"] - -[must] -root_control_files = [ - ".gitignore", - ".gitattributes", - ".editorconfig", - ".tool-versions", - "Containerfile", - "Justfile", -] - -root_hosting_files = [ - "CNAME", - ".nojekyll", -] - -ownership_files = [ - "MAINTAINER", - ".github/CODEOWNERS", -] - -machine_readable_required = [ - ".machine_readable/6a2/anchors/ANCHOR.deed", - ".machine_readable/contractiles/", - ".machine_readable/ai/", - ".machine_readable/bot_directives/", -] - -contractiles_required = [ - "Mustfile", - "Trustfile", - "Intentfile", -] - -security_required = [ - ".well-known/security.txt", - "ci-security-scan", -] - -quality_gate_required = [ - "format", - "lint", - "unit-tests", - "integration-tests", - "p2p-tests", - "e2e-tests", - "bench-smoke", - "docs-check", - "security-scan", -] - -abi_ffi_policy = [ - "ABI Idris2 in src/interface/abi/*.idr", - "FFI Zig in ffi/**/*.zig", -] - -[should] -docs_primary_format = "adoc" -docs_structure = [ - "docs/theory", - "docs/practice", - "docs/whitepapers/academic", - "docs/whitepapers/industry", - "docs/proofs", - "docs/reports", -] - -root_minimization = true -well_known_metadata = true -roadmap_honesty_with_dates = true -ci_doc_format_policy = true - -[could] -generate_human_from_machine = true -mode_aware_bots = ["corrective", "adaptive", "perfective", "audit"] -topology_dashboard = true -exception_registry = true +;; SPDX-FileCopyrightText: © 2026 Jonathan D.A. Jewell (hyperpolymath) +;; SPDX-License-Identifier: MPL-2.0 +(repo-deed + :schema-version "1.0.0" + :canonical-name "panoply-maintenance-checklist" + :repo-uuid #u5"hyperpolymath/panoply" + :beholding-chora #u5"estate/chora" + :last-updated "2026-09-20" + :scope "cross-repo" + :source-human "docs/governance/MAINTENANCE-CHECKLIST.adoc" + (policy :single-source true) + (maintenance-axes + :axis-1 "must > intend > like" + :axis-2 "corrective > adaptive > perfective" + :axis-3 "systems > compliance > effects")) diff --git a/.machine_readable/policies/SOFTWARE-DEVELOPMENT-APPROACH.deed b/.machine_readable/policies/SOFTWARE-DEVELOPMENT-APPROACH.deed index d7967d2..bf32b79 100644 --- a/.machine_readable/policies/SOFTWARE-DEVELOPMENT-APPROACH.deed +++ b/.machine_readable/policies/SOFTWARE-DEVELOPMENT-APPROACH.deed @@ -1,53 +1,11 @@ -# SPDX-License-Identifier: MPL-2.0 -# General software development approach (machine-readable) - -[metadata] -version = "1.0.0" -last-updated = "2026-02-24" -scope = "cross-repo" -source-human = "docs/governance/SOFTWARE-DEVELOPMENT-APPROACH.adoc" - -[execution] -order = ["axis-1", "axis-2", "axis-3"] - -[axis-1] -name = "scope" -priority = "must > intend > like" -inputs = [ - "README", - "roadmap", - "status-docs", - "ci-and-security-docs", -] -marker-scan = ["TODO", "FIXME", "XXX", "HACK", "STUB", "PARTIAL"] -idris-unsound-scan = ["believe_me", "assert_total"] -output = "scoped-work-assembly" - -[axis-2] -name = "maintenance" -priority = "corrective > adaptive > perfective" -corrective = "defect/regression/safety/security fixes" -adaptive = "scope reconciliation, stale-reference removal, obsolete-work culling" -perfective = "quality improvements derived from axis-1 honest state" - -[axis-3] -name = "audit" -priority = "systems > compliance > effects" -systems = "required systems present and operating" -compliance = "exceptions explicit, bounded, and drift-resistant" -effects = "benchmark/operational impact evidence captured and reviewed" -compliance-tooling = "panic-attack" -effects-tooling = "ecological checking with sustainabot guidance" - -[cleanup-finish-off] -root-cleanup = true -stale-work-cull = true -docs-sync-human-machine = true -compliance-audit = true -effects-audit = true -release-summary = ["must", "should", "could"] -next-actions = ["corrective", "adaptive", "perfective"] - -[collaboration] -maintainer-dialogue-required = true -dialogue-topics = ["what changed", "why", "remaining risks"] +;; SPDX-FileCopyrightText: © 2026 Jonathan D.A. Jewell (hyperpolymath) +;; SPDX-License-Identifier: MPL-2.0 +(repo-deed + :schema-version "1.0.0" + :canonical-name "panoply-sda" + :repo-uuid #u5"hyperpolymath/panoply" + :beholding-chora #u5"estate/chora" + :last-updated "2026-09-20" + :scope "cross-repo" + :source-human "docs/governance/SOFTWARE-DEVELOPMENT-APPROACH.adoc" + (execution :order ("axis-1" "axis-2" "axis-3"))) diff --git a/Justfile b/Justfile index a6a255b..7735649 100644 --- a/Justfile +++ b/Justfile @@ -196,6 +196,9 @@ spec-tests: bash tests/core_spec.sh bash tests/evidence_spec.sh bash tests/manifest_spec.sh + bash tests/backend_spec.sh + bash tests/projection_spec.sh + bash scripts/emit-manifest.sh >/dev/null # Run the full merge-requirement test suite # Categories: execution (`test`) + E2E + aspect + bench + lifecycle + P2P diff --git a/build/just/proofs.just b/build/just/proofs.just index b124d7a..3cd37bc 100644 --- a/build/just/proofs.just +++ b/build/just/proofs.just @@ -1,18 +1,11 @@ # SPDX-License-Identifier: MPL-2.0 # Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) # -# FORMAL VERIFICATION (PROOFS) -# -# Imported by ../../Justfile via `import? "build/just/proofs.just"`. -# Recipes here check formal proofs across Idris2, Lean4, Agda, and Coq, plus -# scan for dangerous/unsafe constructs and report status. Run via -# `just proof-check-all` for the full sweep. +# Formal verification — Idris2 only (estate FV language). -# Check all formal proofs (Idris2 + Lean4 + Agda + Coq) -proof-check-all: proof-check-idris2 proof-check-lean4 proof-check-agda proof-check-coq proof-scan-dangerous +proof-check-all: proof-check-idris2 proof-scan-dangerous @echo "=== All proof checks complete ===" -# Check Idris2 proofs (ABI, types, dependent type proofs) proof-check-idris2: #!/usr/bin/env bash set -euo pipefail @@ -22,7 +15,7 @@ proof-check-idris2: exit 0 fi ERRORS=0 - for f in $(find verification/proofs/idris2 -name '*.idr' 2>/dev/null); do + while IFS= read -r f; do echo -n " Checking $f ... " if idris2 --check "$f" 2>/dev/null; then echo "OK" @@ -30,125 +23,35 @@ proof-check-idris2: echo "FAIL" ERRORS=$((ERRORS + 1)) fi - done + done < <(find verification/proofs/idris2 -name '*.idr' 2>/dev/null) if [ "$ERRORS" -gt 0 ]; then echo "FAIL: $ERRORS Idris2 proof(s) failed" exit 1 fi echo "PASS: All Idris2 proofs verified" -# Check Lean4 proofs -proof-check-lean4: - #!/usr/bin/env bash - set -euo pipefail - echo "=== Checking Lean4 proofs ===" - if ! command -v lean &>/dev/null; then - echo "SKIP: lean not installed" - exit 0 - fi - ERRORS=0 - for f in $(find verification/proofs/lean4 -name '*.lean' 2>/dev/null); do - echo -n " Checking $f ... " - if lean "$f" 2>/dev/null; then - echo "OK" - else - echo "FAIL" - ERRORS=$((ERRORS + 1)) - fi - done - if [ "$ERRORS" -gt 0 ]; then - echo "FAIL: $ERRORS Lean4 proof(s) failed" - exit 1 - fi - echo "PASS: All Lean4 proofs verified" - -# Check Agda proofs -proof-check-agda: - #!/usr/bin/env bash - set -euo pipefail - echo "=== Checking Agda proofs ===" - if ! command -v agda &>/dev/null; then - echo "SKIP: agda not installed" - exit 0 - fi - ERRORS=0 - for f in $(find verification/proofs/agda -name '*.agda' 2>/dev/null); do - echo -n " Checking $f ... " - if agda --safe "$f" 2>/dev/null; then - echo "OK" - else - echo "FAIL" - ERRORS=$((ERRORS + 1)) - fi - done - if [ "$ERRORS" -gt 0 ]; then - echo "FAIL: $ERRORS Agda proof(s) failed" - exit 1 - fi - echo "PASS: All Agda proofs verified" - -# Check Coq proofs -proof-check-coq: - #!/usr/bin/env bash - set -euo pipefail - echo "=== Checking Coq proofs ===" - if ! command -v coqc &>/dev/null; then - echo "SKIP: coqc not installed" - exit 0 - fi - ERRORS=0 - for f in $(find verification/proofs/coq -name '*.v' 2>/dev/null); do - echo -n " Checking $f ... " - if coqc "$f" 2>/dev/null; then - echo "OK" - else - echo "FAIL" - ERRORS=$((ERRORS + 1)) - fi - done - if [ "$ERRORS" -gt 0 ]; then - echo "FAIL: $ERRORS Coq proof(s) failed" - exit 1 - fi - echo "PASS: All Coq proofs verified" - -# Scan for dangerous patterns in proof files (believe_me, sorry, Admitted, etc.) proof-scan-dangerous: #!/usr/bin/env bash set -euo pipefail echo "=== Scanning for dangerous patterns in proofs ===" DANGEROUS=0 - PATTERNS="believe_me|assert_total|postulate|sorry|Admitted|unsafeCoerce|Obj\.magic" - for f in $(find verification/proofs -name '*.idr' -o -name '*.lean' -o -name '*.agda' -o -name '*.v' 2>/dev/null); do + PATTERNS="believe_me|assert_total|postulate|sorry|Admitted|unsafeCoerce|Obj\\.magic" + while IFS= read -r f; do MATCHES=$(grep -nE "$PATTERNS" "$f" 2>/dev/null || true) if [ -n "$MATCHES" ]; then echo " DANGEROUS: $f" echo "$MATCHES" | sed 's/^/ /' DANGEROUS=$((DANGEROUS + 1)) fi - done + done < <(find verification/proofs -name '*.idr' 2>/dev/null) if [ "$DANGEROUS" -gt 0 ]; then echo "FAIL: $DANGEROUS file(s) contain dangerous patterns" exit 1 fi echo "PASS: No dangerous patterns found in proofs" -# Show proof status summary proof-status: #!/usr/bin/env bash echo "=== Proof Status ===" - echo "" echo "Idris2: $(find verification/proofs/idris2 -name '*.idr' 2>/dev/null | wc -l) files" - echo "Lean4: $(find verification/proofs/lean4 -name '*.lean' 2>/dev/null | wc -l) files" - echo "Agda: $(find verification/proofs/agda -name '*.agda' 2>/dev/null | wc -l) files" - echo "Coq: $(find verification/proofs/coq -name '*.v' 2>/dev/null | wc -l) files" - echo "TLA+: $(find verification/proofs/tlaplus -name '*.tla' 2>/dev/null | wc -l) files" - echo "" - # PROOF-STATUS may live at root, docs/status/ (post-#20), .md or .adoc (post-#23) - for candidate in docs/status/PROOF-STATUS.adoc docs/status/PROOF-STATUS.md PROOF-STATUS.adoc PROOF-STATUS.md; do - if [ -f "$candidate" ]; then - grep -E "^\| \*\*Total\*\*|^\| \*Total\*" "$candidate" 2>/dev/null || echo "(No summary row in $candidate)" - exit 0 - fi - done - echo "(No PROOF-STATUS file found at root or docs/status/)" + grep -E "^\| \*Total\*" docs/status/PROOF-STATUS.adoc 2>/dev/null || true diff --git a/docs/reports/LANGUAGE-AUDIT.adoc b/docs/reports/LANGUAGE-AUDIT.adoc index 7825c19..39ee38c 100644 --- a/docs/reports/LANGUAGE-AUDIT.adoc +++ b/docs/reports/LANGUAGE-AUDIT.adoc @@ -21,13 +21,8 @@ No TypeScript, Python, Go, Java, Rust, Ada, V-lang application code. == Proof-scaffold languages (RSR template, not application) -These live only under `verification/proofs/` as **stubs**: Coq (`.v`), -Agda, Lean4, TLA+. Estate language policy names Idris2 as the sole -*formal-verification language* for new work. These files are template -holdings, not a second ABI. - -**Check with owner:** keep as multi-prover sketch (RSR template) or -delete non-Idris2 proof trees? Not deleted in this phase. +Removed 2026-09-20. Idris2 is the sole FV language. Proofs live only under +`verification/proofs/idris2/`. == Config / docs (not CCCP “languages”) diff --git a/docs/status/PROOF-NEEDS.adoc b/docs/status/PROOF-NEEDS.adoc index 6336a73..f426886 100644 --- a/docs/status/PROOF-NEEDS.adoc +++ b/docs/status/PROOF-NEEDS.adoc @@ -48,7 +48,7 @@ These proofs come from the rsr-template-repo and MUST be present in every repo: | # | Proof | Status | File | TP-1 | Core data type well-formedness | Needed | `verification/proofs/idris2/Types.idr` -| TP-2 | Public API type safety (exported functions) | Needed | `verification/proofs/lean4/ApiTypes.lean` +| TP-2 | Public API type safety (exported functions) | Needed | Idris2 (Lean4 tree removed) | |=== == Project-Specific Proofs diff --git a/docs/status/PROOF-STATUS.adoc b/docs/status/PROOF-STATUS.adoc index 5cbcf0e..dfae212 100644 --- a/docs/status/PROOF-STATUS.adoc +++ b/docs/status/PROOF-STATUS.adoc @@ -10,8 +10,8 @@ |=== | Category | Total | Done | In Progress | Blocked | Remaining -| ABI/FFI (ABI) | 5 | 0 | 0 | 0 | 5 -| Typing (TP) | 2 | 0 | 0 | 0 | 2 +| ABI/FFI (ABI) | 5 | 1 | 0 | 0 | 4 +| Typing (TP) | 2 | 0 | 0 | 1 | 1 | Invariant (INV) | 0 | 0 | 0 | 0 | 0 | Security (SEC) | 0 | 0 | 0 | 0 | 0 | Concurrency (CONC) | 0 | 0 | 0 | 0 | 0 @@ -65,7 +65,7 @@ | ABI-4 | FFI function return type proofs | ABI | Idris2 | P1 | 2h | ABI-5 | C ABI compliance | ABI | Idris2 | P1 | 4h | TP-1 | Core data type well-formedness | TP | Idris2 | P1 | 4h -| TP-2 | Public API type safety | TP | Lean4 | P2 | 4h +| TP-2 | Public API type safety | TP | Idris2 | P2 | 4h | |=== == Verification Commands diff --git a/docs/status/ROADMAP.adoc b/docs/status/ROADMAP.adoc index efb14a2..935abf0 100644 --- a/docs/status/ROADMAP.adoc +++ b/docs/status/ROADMAP.adoc @@ -16,8 +16,8 @@ Design phase. Charter + RSR spine + Core/Evidence *specs*. No Core checker. * [ ] Relocate `.gitlab-ci.yml` → `ci/` after GitLab setting update * [ ] Relocate `.pre-commit-config.yaml` → `ci/` after invocation pattern decided * [ ] Convert remaining `0.x-AI-MANIFEST.deed` files from TOML/prose or keep as exempt gatekeeper docs -* [ ] Wire `e2e.yml` jobs (aspect + zig) with SHA-pinned actions -* [ ] Owner: keep or delete Coq/Agda/Lean/TLA proof stubs (Idris2-only FV policy vs RSR template) +* [x] Wire `e2e.yml` jobs (aspect + zig) with SHA-pinned actions +* [x] 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 * [x] Root `Mustfile` (pointer to `.machine_readable/contractiles/Mustfile.deed`) @@ -26,8 +26,8 @@ Design phase. Charter + RSR spine + Core/Evidence *specs*. No Core checker. * [x] #5 Core syntax + judgements specified (checker not implemented) * [x] #6 Evidence kinds specified (no emitter) -* [ ] #7 Manifest schema + emitter -* [ ] #8 Projections -* [ ] #9 Backends -* [ ] #10 First mechanised obligation +* [ ] #7 Manifest schema + fail-closed emitter (do not close) +* [ ] #8 null projection + refuse≡refuse witness (do not close) +* [ ] #9 none + zig-ffi contracts (do not close) +* [ ] #10 ABI-1 in-tree Idris2 (do not close; typecheck SKIP without idris2) * [ ] #11 Hypatia ignore from findings dump diff --git a/scripts/emit-manifest.sh b/scripts/emit-manifest.sh new file mode 100755 index 0000000..4a7e282 --- /dev/null +++ b/scripts/emit-manifest.sh @@ -0,0 +1,51 @@ +#!/usr/bin/env bash +# SPDX-License-Identifier: MPL-2.0 +# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +# +# Fail-closed manifest emitter (#7). +# No guarantee without an envelope; no envelope without non-refused evidence; +# no composition without a named rule. +set -euo pipefail +ROOT="$(cd "$(dirname "${BASH_SOURCE[0]}")/.." && pwd)" +EVIDENCE="${1:-$ROOT/src/evidence/examples/core-typing.evidence}" +BACKEND="${2:-none}" +OUT="${3:-}" + +if [[ ! -f "$EVIDENCE" ]]; then + echo "emit-manifest: missing evidence: $EVIDENCE" >&2 + exit 2 +fi + +status="refused" +if grep -q ':status accepted' "$EVIDENCE"; then + status="accepted" +elif grep -q ':status refused' "$EVIDENCE"; then + status="refused" +else + echo "emit-manifest: evidence has no :status" >&2 + exit 2 +fi + +if [[ "$status" != "accepted" ]]; then + # Central rule: refused or missing evidence ⇒ empty earned, refused manifest. + body=$(cat <&2 + exit 1 +fi + +if [[ -n "$OUT" ]]; then + printf '%s\n' "$body" > "$OUT" +else + printf '%s\n' "$body" +fi diff --git a/src/backends/BACKEND-CONTRACT.adoc b/src/backends/BACKEND-CONTRACT.adoc new file mode 100644 index 0000000..7d7256b --- /dev/null +++ b/src/backends/BACKEND-CONTRACT.adoc @@ -0,0 +1,37 @@ +// SPDX-License-Identifier: CC-BY-SA-4.0 +// Copyright (c) Jonathan D.A. Jewell += Backend contracts (issue #9) +:revdate: 2026-09-20 + +A backend does **not** inherit Core guarantees. It upholds only what this +contract names. + +== `none` (design-phase default) + +Path: `src/backends/none/CONTRACT.adoc` + +* Upholds: nothing. +* Means: none. +* Cannot uphold: total-correctness, memory-safety, confluence, any Core + envelope. +* Envelope the emitter uses: `:backend none`. + +A Core program lowered to `none` always yields a **refused** manifest with +empty `:earned`. + +== `zig-ffi` (FFI scaffold) + +Path: `src/backends/zig-ffi/CONTRACT.adoc` + +* Upholds: C-ABI calling convention of the Zig FFI exports, as far as the + Zig type checker and unit tests go (**check**, not proof). +* Cannot uphold: Core typing, preservation, memory-safety of Idris values. +* A Core-earned guarantee does **not** appear on this backend unless this + contract names it. Today it names none of the Core envelopes. + +== Backend-relative manifests + +Same program, two backends ⇒ two manifests. `scripts/emit-manifest.sh` +takes the backend id as argv. Both current backends refuse Core envelopes. + +Do not close #9 until a lowering exists that preserves a named guarantee. diff --git a/src/backends/README.adoc b/src/backends/README.adoc index 38005d6..8d72274 100644 --- a/src/backends/README.adoc +++ b/src/backends/README.adoc @@ -10,9 +10,9 @@ Nothing survives lowering for free. [IMPORTANT] ==== -*Not yet implemented.* Sketch area per the -xref:../../docs/architecture/DESIGN-DISCIPLINE.adoc[charter]. No backend exists -yet (design phase). +*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. ==== == What a backend contract states diff --git a/src/backends/none/CONTRACT.adoc b/src/backends/none/CONTRACT.adoc new file mode 100644 index 0000000..4717d3c --- /dev/null +++ b/src/backends/none/CONTRACT.adoc @@ -0,0 +1,6 @@ +// SPDX-License-Identifier: CC-BY-SA-4.0 +// Copyright (c) Jonathan D.A. Jewell += Backend `none` + +Upholds nothing. Used when no target exists. Manifest `:backend none`, +`:status refused`, `:earned ()`. diff --git a/src/backends/zig-ffi/CONTRACT.adoc b/src/backends/zig-ffi/CONTRACT.adoc new file mode 100644 index 0000000..1af2181 --- /dev/null +++ b/src/backends/zig-ffi/CONTRACT.adoc @@ -0,0 +1,7 @@ +// SPDX-License-Identifier: CC-BY-SA-4.0 +// Copyright (c) Jonathan D.A. Jewell += Backend `zig-ffi` + +Upholds: Zig FFI export calling convention (check via `zig build test`). +Does **not** uphold Core typing or any Core-earned envelope. +Manifest `:backend zig-ffi` is still refused for Core guarantees. diff --git a/src/manifest/README.adoc b/src/manifest/README.adoc index 1cefee7..ec9a069 100644 --- a/src/manifest/README.adoc +++ b/src/manifest/README.adoc @@ -10,9 +10,9 @@ absence of type errors. [IMPORTANT] ==== -*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. +*Schema specified; fail-closed emitter at `scripts/emit-manifest.sh`.* +See xref:MANIFEST-SCHEMA.adoc[MANIFEST-SCHEMA.adoc] and +`examples/refused.manifest`. Issue #7 stays open until accepted evidence exists. ==== == What a manifest records diff --git a/src/projections/PROJECTION.adoc b/src/projections/PROJECTION.adoc new file mode 100644 index 0000000..90f58a1 --- /dev/null +++ b/src/projections/PROJECTION.adoc @@ -0,0 +1,26 @@ +// SPDX-License-Identifier: CC-BY-SA-4.0 +// Copyright (c) Jonathan D.A. Jewell += Projections (issue #8) +:revdate: 2026-09-20 + +A projection elaborates an accepted program into **Core + evidence + +manifest**, or **rejects**. There is no Core checker, so the only honest +projection today is **`null`**: it rejects every program. + +== `null` projection + +Path: `src/projections/null/` + +* Accept: never. +* Reject: always (no Core elaboration). +* Evidence: none produced. +* Manifest: emitter writes `:status refused`. + +== Equivalence witness + +Two rejections of the empty input are the same program (the empty +program, not accepted). Witness file: +`src/projections/null/equivalence-refuse-refuse.witness` + +This is **not** an equivalence of two accepted elaborations. Do not close +#8 until a surface exists that can accept a program. diff --git a/src/projections/README.adoc b/src/projections/README.adoc index d147303..f320bb2 100644 --- a/src/projections/README.adoc +++ b/src/projections/README.adoc @@ -9,9 +9,9 @@ must elaborate every program it accepts into Core + evidence + manifest. [IMPORTANT] ==== -*Not yet implemented.* Sketch area per the -xref:../../docs/architecture/DESIGN-DISCIPLINE.adoc[charter]. No projection -exists yet (design phase). +*Only the `null` projection exists* (always rejects). See +xref:PROJECTION.adoc[PROJECTION.adoc]. Issue #8 stays open until a surface +can accept a program. ==== == Why "projection" and not "face" diff --git a/src/projections/null/equivalence-refuse-refuse.witness b/src/projections/null/equivalence-refuse-refuse.witness new file mode 100644 index 0000000..a30e58a --- /dev/null +++ b/src/projections/null/equivalence-refuse-refuse.witness @@ -0,0 +1,8 @@ +# SPDX-License-Identifier: MPL-2.0 +# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +(projection-equivalence + :schema-version "0.1.0" + :left (projection :name null :input "" :result rejected) + :right (projection :name null :input "" :result rejected) + :status witnessed + :note "Both sides reject; no Core term exists to compare.") diff --git a/tests/backend_spec.sh b/tests/backend_spec.sh new file mode 100755 index 0000000..ac3c34e --- /dev/null +++ b/tests/backend_spec.sh @@ -0,0 +1,15 @@ +#!/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/backends/BACKEND-CONTRACT.adoc ]] && pass "contract spec" || fail "missing BACKEND-CONTRACT" +[[ -f src/backends/none/CONTRACT.adoc ]] && pass "none" || fail "none" +[[ -f src/backends/zig-ffi/CONTRACT.adoc ]] && pass "zig-ffi" || fail "zig-ffi" +grep -q 'Upholds nothing' src/backends/none/CONTRACT.adoc && pass "none upholds nothing" || fail "none must uphold nothing" +echo "FAIL=$FAIL" +exit "$FAIL" diff --git a/tests/e2e.sh b/tests/e2e.sh index c19a59f..3379bb4 100755 --- a/tests/e2e.sh +++ b/tests/e2e.sh @@ -71,9 +71,11 @@ bold "Preflight checks" if command -v idris2 >/dev/null 2>&1; then green " Found idris2: $(idris2 --version 2>&1 | head -1)" + HAVE_IDRIS2=1 else - red "idris2 not found on PATH" - exit 1 + yellow " SKIP: idris2 not on PATH (ABI section)" + HAVE_IDRIS2=0 + SKIP=$((SKIP + 1)) fi if command -v zig >/dev/null 2>&1; then diff --git a/tests/evidence_spec.sh b/tests/evidence_spec.sh index c2cbdb1..4ff19a9 100755 --- a/tests/evidence_spec.sh +++ b/tests/evidence_spec.sh @@ -16,6 +16,8 @@ grep -q ':status refused' src/evidence/examples/core-typing.evidence && pass "ho head -5 panoply_chora.deed | grep -q 'repo-deed' && pass "panoply_chora.deed is repo-deed" || fail "chora" grep -q '\[metadata\]' panoply_chora.deed && fail "chora must not be TOML" || pass "chora is not TOML" grep -q '\[metadata\]' .machine_readable/6a2/STATE.deed && fail "STATE still TOML" || pass "STATE is s-expression" +grep -q '\[metadata\]' .machine_readable/6a2/LANGUAGES.deed && fail "LANGUAGES still TOML" || pass "LANGUAGES is s-expression" +grep -q '\[metadata\]' .machine_readable/6a2/AGENTIC.deed && fail "AGENTIC still TOML" || pass "AGENTIC is s-expression" echo "FAIL=$FAIL" exit "$FAIL" diff --git a/tests/projection_spec.sh b/tests/projection_spec.sh new file mode 100755 index 0000000..c5790f6 --- /dev/null +++ b/tests/projection_spec.sh @@ -0,0 +1,14 @@ +#!/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/projections/PROJECTION.adoc ]] && pass "projection spec" || fail "missing" +[[ -f src/projections/null/equivalence-refuse-refuse.witness ]] && pass "witness" || fail "witness" +grep -q ':result rejected' src/projections/null/equivalence-refuse-refuse.witness && pass "reject witnessed" || fail "must reject" +echo "FAIL=$FAIL" +exit "$FAIL" diff --git a/verification/proofs/README.adoc b/verification/proofs/README.adoc index eb22d4c..a85d056 100644 --- a/verification/proofs/README.adoc +++ b/verification/proofs/README.adoc @@ -9,22 +9,9 @@ This directory contains formal proofs organised by proof assistant. [source] ---- proofs/ -├── idris2/ # Idris2 proofs (ABI, dependent types) -│ ├── ABI/ # ABI-specific proofs (mandatory) -│ │ ├── Pointers.idr # Non-null pointer safety -│ │ ├── Layout.idr # Memory layout correctness -│ │ ├── Platform.idr # Platform type size proofs -│ │ ├── Foreign.idr # FFI return type proofs -│ │ └── Compliance.idr # C ABI compliance -│ └── Types.idr # Core data type well-formedness -├── lean4/ # Lean4 proofs (algebra, lattices) -│ └── ApiTypes.lean -├── agda/ # Agda proofs (induction, metatheory) -│ └── Properties.agda -├── coq/ # Coq proofs (type systems, compilation) -│ └── TypeSafety.v -└── tlaplus/ # TLA+ specs (distributed protocols) - └── StateMachine.tla +└── idris2/ # sole FV language + ├── ABI/ + └── Types.idr ---- == Verification Commands diff --git a/verification/proofs/agda/Properties.agda b/verification/proofs/agda/Properties.agda deleted file mode 100644 index d78d9d0..0000000 --- a/verification/proofs/agda/Properties.agda +++ /dev/null @@ -1,37 +0,0 @@ --- SPDX-License-Identifier: MPL-2.0 --- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) --- --- Agda Proof Template: Inductive and coinductive properties --- Replace with your project's domain-specific proofs. --- All proofs must be total (no postulate, no {-# TERMINATING #-}). - -module Properties where - -open import Data.Nat using (ℕ; zero; suc; _+_; _≤_; z≤n; s≤s; _<_) -open import Data.Nat.Properties using (+-comm; +-assoc; ≤-refl; ≤-trans) -open import Data.List using (List; []; _∷_; length; _++_) -open import Data.List.Properties using (length-++ ) -open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong; sym; trans) - --- Example: Proof that list append preserves total length --- Replace with your project's domain proofs. - -append-length : ∀ {A : Set} (xs ys : List A) → - length (xs ++ ys) ≡ length xs + length ys -append-length xs ys = length-++ xs - --- Example: Monotonicity proof template --- Use for state machines, confidence scores, trust levels -record Monotone {A : Set} (_≤A_ : A → A → Set) (f : A → A) : Set where - field - preserves : ∀ {x y} → x ≤A y → f x ≤A f y - --- Example: Idempotence proof template --- Use for normalisation, deduplication, formatting -record Idempotent {A : Set} (_≡A_ : A → A → Set) (f : A → A) : Set where - field - idem : ∀ (x : A) → f (f x) ≡A f x - --- Example: Natural number successor is monotone -suc-monotone : Monotone _≤_ suc -suc-monotone = record { preserves = s≤s } diff --git a/verification/proofs/coq/TypeSafety.v b/verification/proofs/coq/TypeSafety.v deleted file mode 100644 index 8f5b418..0000000 --- a/verification/proofs/coq/TypeSafety.v +++ /dev/null @@ -1,73 +0,0 @@ -(* SPDX-License-Identifier: MPL-2.0 *) -(* Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) *) -(* - Coq Proof Template: Type system soundness - Replace with your project's type system proofs. - All proofs must be complete — NO Admitted allowed. -*) - -Require Import Coq.Lists.List. -Require Import Coq.Arith.Arith. -Require Import Coq.Bool.Bool. -Import ListNotations. - -(** * Example: Simple expression language with type safety *) -(** Replace this entire section with your project's type system. *) - -(** Types *) -Inductive ty : Type := - | TyNat : ty - | TyBool : ty. - -(** Expressions *) -Inductive expr : Type := - | EConst : nat -> expr - | ETrue : expr - | EFalse : expr - | EPlus : expr -> expr -> expr - | EEq : expr -> expr -> expr. - -(** Values *) -Inductive value : Type := - | VNat : nat -> value - | VBool : bool -> value. - -(** Typing relation *) -Inductive has_type : expr -> ty -> Prop := - | T_Const : forall n, has_type (EConst n) TyNat - | T_True : has_type ETrue TyBool - | T_False : has_type EFalse TyBool - | T_Plus : forall e1 e2, - has_type e1 TyNat -> has_type e2 TyNat -> - has_type (EPlus e1 e2) TyNat - | T_Eq : forall e1 e2, - has_type e1 TyNat -> has_type e2 TyNat -> - has_type (EEq e1 e2) TyBool. - -(** Evaluation *) -Inductive eval : expr -> value -> Prop := - | E_Const : forall n, eval (EConst n) (VNat n) - | E_True : eval ETrue (VBool true) - | E_False : eval EFalse (VBool false) - | E_Plus : forall e1 e2 n1 n2, - eval e1 (VNat n1) -> eval e2 (VNat n2) -> - eval (EPlus e1 e2) (VNat (n1 + n2)) - | E_Eq : forall e1 e2 n1 n2, - eval e1 (VNat n1) -> eval e2 (VNat n2) -> - eval (EEq e1 e2) (VBool (Nat.eqb n1 n2)). - -(** Value typing *) -Definition value_has_type (v : value) (t : ty) : Prop := - match v, t with - | VNat _, TyNat => True - | VBool _, TyBool => True - | _, _ => False - end. - -(** Type soundness: well-typed expressions evaluate to well-typed values *) -Theorem type_soundness : forall e t v, - has_type e t -> eval e v -> value_has_type v t. -Proof. - intros e t v Htype Heval. - induction Htype; inversion Heval; subst; simpl; auto. -Qed. diff --git a/verification/proofs/lean4/ApiTypes.lean b/verification/proofs/lean4/ApiTypes.lean deleted file mode 100644 index 9ed78b7..0000000 --- a/verification/proofs/lean4/ApiTypes.lean +++ /dev/null @@ -1,44 +0,0 @@ --- SPDX-License-Identifier: MPL-2.0 --- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) --- --- Typing Proof: Public API type safety --- Template — replace with your project's API types. --- Proves properties about exported function signatures. - --- Example: Result type used across API boundaries -inductive ApiResult (α : Type) where - | ok : α → ApiResult α - | error : Nat → String → ApiResult α - -namespace ApiResult - -- Proof: map preserves structure (functor law: map id = id) - def map (f : α → β) : ApiResult α → ApiResult β - | .ok v => .ok (f v) - | .error c m => .error c m - - theorem map_id : ∀ (r : ApiResult α), map id r = r := by - intro r - cases r with - | ok v => simp [map] - | error c m => simp [map] - - -- Proof: map composition (functor law: map (g ∘ f) = map g ∘ map f) - theorem map_comp (f : α → β) (g : β → γ) : - ∀ (r : ApiResult α), map (g ∘ f) r = map g (map f r) := by - intro r - cases r with - | ok v => simp [map, Function.comp] - | error c m => simp [map] - --- Example: Bounded confidence value (0.0 to 1.0 modelled as Nat/1000) --- Replace with your project's numeric invariants -structure BoundedNat (max : Nat) where - val : Nat - le_max : val ≤ max - -theorem bounded_nat_le (b : BoundedNat max) : b.val ≤ max := - b.le_max - --- Proof: zero is always bounded -def zeroBounded (h : 0 < max) : BoundedNat max := - ⟨0, Nat.zero_le max⟩ diff --git a/verification/proofs/tlaplus/StateMachine.tla b/verification/proofs/tlaplus/StateMachine.tla deleted file mode 100644 index f348494..0000000 --- a/verification/proofs/tlaplus/StateMachine.tla +++ /dev/null @@ -1,91 +0,0 @@ ---------------------------- MODULE StateMachine ---------------------------- -(* SPDX-License-Identifier: MPL-2.0 *) -(* Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) *) -(* *) -(* TLA+ Specification Template: State Machine *) -(* Replace with your project's distributed protocol or state machine. *) -(* Use TLC model checker to verify properties. *) -(* *) -(* Example: A simple request pipeline with safety properties. *) -(* Replace States, Init, Next with your project's actual states. *) -(***************************************************************************) - -EXTENDS Naturals, Sequences, FiniteSets - -CONSTANTS - MaxRequests \* Upper bound on concurrent requests (for model checking) - -VARIABLES - state, \* Current pipeline state - processed, \* Number of processed requests - queue \* Request queue - -vars == <> - -\* Pipeline states — replace with your project's states -States == {"idle", "scanning", "routing", "dispatching", "done", "failed"} - -\* Valid transitions — replace with your project's transition rules -ValidTransition(from, to) == - \/ from = "idle" /\ to = "scanning" - \/ from = "scanning" /\ to = "routing" - \/ from = "scanning" /\ to = "failed" - \/ from = "routing" /\ to = "dispatching" - \/ from = "routing" /\ to = "failed" - \/ from = "dispatching" /\ to = "done" - \/ from = "dispatching" /\ to = "failed" - \/ from = "done" /\ to = "idle" - \/ from = "failed" /\ to = "idle" - -\* Initial state -Init == - /\ state = "idle" - /\ processed = 0 - /\ queue = <<>> - -\* Transition action -Transition(newState) == - /\ ValidTransition(state, newState) - /\ state' = newState - /\ IF newState = "done" - THEN processed' = processed + 1 - ELSE processed' = processed - /\ UNCHANGED queue - -\* Enqueue a request (only when idle or scanning) -Enqueue == - /\ state \in {"idle", "scanning"} - /\ Len(queue) < MaxRequests - /\ queue' = Append(queue, "request") - /\ UNCHANGED <> - -\* Next-state relation -Next == - \/ \E s \in States : Transition(s) - \/ Enqueue - -\* Fairness: the system must eventually process -Spec == Init /\ [][Next]_vars /\ WF_vars(Next) - -\* ---- SAFETY PROPERTIES ---- - -\* State is always valid -TypeInvariant == state \in States - -\* Processed count never decreases (monotonicity) -ProcessedMonotonic == processed >= 0 - -\* Queue never exceeds max -QueueBounded == Len(queue) <= MaxRequests - -\* No impossible transitions (e.g., idle -> done) -NoSkipStates == - [][state' # state => - ValidTransition(state, state')]_state - -\* ---- LIVENESS PROPERTIES ---- - -\* Every request eventually completes or fails -EventualCompletion == <>(state = "done" \/ state = "failed") - -============================================================================