From e1f7a9fe921bedc0c9e3fbc414d35fb327d46dfa Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Mon, 7 Sep 2026 02:14:40 +0100 Subject: [PATCH 1/3] fix(proofs): enforce semantic evidence and continuity CI gates --- .github/workflows/actions.lock | 28 + .github/workflows/agda.yml | 54 -- .github/workflows/codeql.yml | 7 +- .github/workflows/governance.yml | 1 + .github/workflows/label-triage.yml | 1 + .github/workflows/labels.yml | 1 + .github/workflows/proofs.yml | 65 ++ .github/workflows/push-email-notify.yml | 3 +- .github/workflows/secret-scanner.yml | 1 + .gitignore | 3 + .../{6a2 => descriptiles}/0-AI-MANIFEST.a2ml | 8 +- .../{6a2 => descriptiles}/AGENTIC.a2ml | 10 +- .../{6a2 => descriptiles}/ECOSYSTEM.a2ml | 10 +- .../{6a2 => descriptiles}/META.a2ml | 8 +- .../{6a2 => descriptiles}/NEUROSYM.a2ml | 10 +- .../{6a2 => descriptiles}/PLAYBOOK.a2ml | 12 +- .../{6a2 => descriptiles}/README.adoc | 0 .../{6a2 => descriptiles}/STATE.a2ml | 25 +- .../proof-transport/ProofTransport.a2ml | 120 +-- .machine_readable/proof-transport/README.adoc | 13 +- .../proof-transport/proof-transport.k9.ncl | 30 +- .well-known/ai.txt | 10 +- .well-known/humans.txt | 2 +- 0-AI-MANIFEST.a2ml | 32 +- AFFIRMATION.adoc | 12 +- AUDIT.adoc | 322 +------ CHANGELOG.adoc | 141 +-- CONTRIBUTING.adoc | 179 ++-- EXPLAINME.adoc | 61 +- Justfile | 16 +- PROOF-STATUS.adoc | 45 +- README.adoc | 91 +- coordination.k9 | 11 +- docs/README.adoc | 28 +- docs/ci-safety.adoc | 62 ++ docs/continuity-foundations.adoc | 174 ++++ docs/proof-transport.adoc | 820 +++--------------- docs/what-epistemic-is.adoc | 24 +- explainme.adoc | 75 +- src/EpistemicTypes/All.agda | 1 + src/EpistemicTypes/ContinuityExamples.agda | 188 ++++ src/EpistemicTypes/EchoBridge.agda | 183 +++- src/EpistemicTypes/ProofTransport.agda | 350 +++----- src/EpistemicTypes/ProofTransportExample.agda | 232 +++-- src/EpistemicTypes/ReadConsistency.agda | 350 +++----- src/EpistemicTypes/SurrealBridge.agda | 34 +- tests/check-proofs.sh | 13 + tests/check-rejections.sh | 36 + tests/integration/CanonicalEcho.agda | 34 + tests/reject/FakeFreshness.agda | 8 + tests/reject/ForgedAcceptance.agda | 10 + tests/reject/ForgedResidue.agda | 9 + tests/reject/ForkedHistory.agda | 7 + tests/reject/InventedMigration.agda | 14 + tests/reject/LyingVerifier.agda | 10 + tests/reject/MismatchedSource.agda | 9 + tests/reject/ReplayedArtifact.agda | 9 + tests/reject/ReplayedHolder.agda | 9 + tests/reject/StaleSample.agda | 9 + tests/reject/UnderstatedBound.agda | 9 + 60 files changed, 1996 insertions(+), 2043 deletions(-) create mode 100644 .github/workflows/actions.lock delete mode 100644 .github/workflows/agda.yml create mode 100644 .github/workflows/proofs.yml rename .machine_readable/{6a2 => descriptiles}/0-AI-MANIFEST.a2ml (88%) rename .machine_readable/{6a2 => descriptiles}/AGENTIC.a2ml (89%) rename .machine_readable/{6a2 => descriptiles}/ECOSYSTEM.a2ml (87%) rename .machine_readable/{6a2 => descriptiles}/META.a2ml (97%) rename .machine_readable/{6a2 => descriptiles}/NEUROSYM.a2ml (89%) rename .machine_readable/{6a2 => descriptiles}/PLAYBOOK.a2ml (84%) rename .machine_readable/{6a2 => descriptiles}/README.adoc (100%) rename .machine_readable/{6a2 => descriptiles}/STATE.a2ml (74%) create mode 100644 docs/ci-safety.adoc create mode 100644 docs/continuity-foundations.adoc create mode 100644 src/EpistemicTypes/ContinuityExamples.agda create mode 100644 tests/check-proofs.sh create mode 100644 tests/check-rejections.sh create mode 100644 tests/integration/CanonicalEcho.agda create mode 100644 tests/reject/FakeFreshness.agda create mode 100644 tests/reject/ForgedAcceptance.agda create mode 100644 tests/reject/ForgedResidue.agda create mode 100644 tests/reject/ForkedHistory.agda create mode 100644 tests/reject/InventedMigration.agda create mode 100644 tests/reject/LyingVerifier.agda create mode 100644 tests/reject/MismatchedSource.agda create mode 100644 tests/reject/ReplayedArtifact.agda create mode 100644 tests/reject/ReplayedHolder.agda create mode 100644 tests/reject/StaleSample.agda create mode 100644 tests/reject/UnderstatedBound.agda diff --git a/.github/workflows/actions.lock b/.github/workflows/actions.lock new file mode 100644 index 0000000..c4148f8 --- /dev/null +++ b/.github/workflows/actions.lock @@ -0,0 +1,28 @@ +# This file is machine-generated by `gh actions-lock`. +# Do not edit by hand; run `gh actions-lock` to update. +# Docs: https://gh.io/actions-lockfile +version: 'v0.0.2' +workflows: + '.github/workflows/codeql.yml': + - 'actions/checkout@v6.0.3' + - 'github/codeql-action@v4.36.2' + '.github/workflows/proofs.yml': + - 'actions/checkout@v6.0.3' + '.github/workflows/push-email-notify.yml': + - 'hyperpolymath/smtp-notify-action@v0.2.0' +dependencies: + 'actions/checkout@v6.0.3': + ref: 'v6.0.3' + commit: 'sha1-df4cb1c069e1874edd31b4311f1884172cec0e10' + owner_id: 44036562 + repo_id: 197814629 + 'github/codeql-action@v4.36.2': + ref: 'v4.36.2' + commit: 'sha1-8aad20d150bbac5944a9f9d289da16a4b0d87c1e' + owner_id: 9919 + repo_id: 259445878 + 'hyperpolymath/smtp-notify-action@v0.2.0': + ref: 'v0.2.0' + commit: 'sha1-ede1191ef6ff3ac02c4f4d9efdf837ee517e11d7' + owner_id: 6759885 + repo_id: 1352485172 diff --git a/.github/workflows/agda.yml b/.github/workflows/agda.yml deleted file mode 100644 index f1e99bb..0000000 --- a/.github/workflows/agda.yml +++ /dev/null @@ -1,54 +0,0 @@ -# SPDX-License-Identifier: MPL-2.0 -# SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell -# Agda — typecheck the epistemic-types proof suite. -# -# The repo is deliberately stdlib-free (built with --no-libraries; only -# Agda.Primitive / Agda.Builtin.*), so no standard-library setup is needed -# and the apt-packaged Agda suffices. The canonical aggregator is -# src/EpistemicTypes/All.agda, which transitively imports every module and -# carries {-# OPTIONS --safe --without-K #-} per module. This is the proof -# verification the repo previously lacked entirely. -name: Agda - -on: - # Direct pushes only on integration branches; PRs cover feature branches. - push: - branches: [main, master] - pull_request: - -# Estate guardrail: cancel superseded runs. Safe — read-only typecheck, -# no publish or mutation. -concurrency: - group: ${{ github.workflow }}-${{ github.ref }} - cancel-in-progress: true - -permissions: - contents: read - -jobs: - check: - runs-on: ubuntu-latest - timeout-minutes: 20 - steps: - - name: Checkout - uses: actions/checkout@df4cb1c069e1874edd31b4311f1884172cec0e10 # v6.0.3 - - - name: Install Agda - run: | - sudo apt-get update - sudo apt-get install -y agda - - - name: Toolchain provenance - run: agda --version | head -n1 - - - name: Typecheck canonical target (stdlib-free) - run: | - set -e - agda --no-libraries -i src src/EpistemicTypes/All.agda - echo "epistemic-types: src/EpistemicTypes/All.agda typechecks (exit 0)." - - - name: Re-check with warnings promoted to errors (no unsolved metas) - run: | - set -e - agda --no-libraries -i src -W error src/EpistemicTypes/All.agda - echo "epistemic-types: clean under -W error (no unsolved metas/constraints/termination issues)." diff --git a/.github/workflows/codeql.yml b/.github/workflows/codeql.yml index d425342..a6cd26d 100644 --- a/.github/workflows/codeql.yml +++ b/.github/workflows/codeql.yml @@ -1,3 +1,4 @@ +# This workflow is managed by gh actions-lock. # SPDX-License-Identifier: MPL-2.0 # SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell name: CodeQL Security Analysis @@ -41,15 +42,15 @@ jobs: steps: - name: Checkout - uses: actions/checkout@df4cb1c069e1874edd31b4311f1884172cec0e10 # v6.0.3 + uses: actions/checkout@v6.0.3 - name: Initialize CodeQL - uses: github/codeql-action/init@8aad20d150bbac5944a9f9d289da16a4b0d87c1e # v3 + uses: github/codeql-action/init@v4.36.2 with: languages: ${{ matrix.language }} build-mode: ${{ matrix.build-mode }} - name: Perform CodeQL Analysis - uses: github/codeql-action/analyze@8aad20d150bbac5944a9f9d289da16a4b0d87c1e # v3 + uses: github/codeql-action/analyze@v4.36.2 with: category: "/language:${{ matrix.language }}" diff --git a/.github/workflows/governance.yml b/.github/workflows/governance.yml index d8c88d3..7ce96ba 100644 --- a/.github/workflows/governance.yml +++ b/.github/workflows/governance.yml @@ -1,3 +1,4 @@ +# This workflow is managed by gh actions-lock. # SPDX-License-Identifier: MPL-2.0 name: Governance diff --git a/.github/workflows/label-triage.yml b/.github/workflows/label-triage.yml index 9886e92..814a192 100644 --- a/.github/workflows/label-triage.yml +++ b/.github/workflows/label-triage.yml @@ -1,3 +1,4 @@ +# This workflow is managed by gh actions-lock. # SPDX-License-Identifier: MPL-2.0 name: Label Triage diff --git a/.github/workflows/labels.yml b/.github/workflows/labels.yml index c80b676..83ab941 100644 --- a/.github/workflows/labels.yml +++ b/.github/workflows/labels.yml @@ -1,3 +1,4 @@ +# This workflow is managed by gh actions-lock. # SPDX-License-Identifier: MPL-2.0 name: Labels diff --git a/.github/workflows/proofs.yml b/.github/workflows/proofs.yml new file mode 100644 index 0000000..400fff7 --- /dev/null +++ b/.github/workflows/proofs.yml @@ -0,0 +1,65 @@ +# This workflow is managed by gh actions-lock. + +name: Proof Safety + +on: + push: + branches: [main] + pull_request: + merge_group: + workflow_dispatch: + +permissions: + contents: read + +concurrency: + group: ${{ github.workflow }}-${{ github.ref }} + cancel-in-progress: true + +jobs: + core: + name: Proof core and rejection controls + runs-on: ubuntu-24.04 + timeout-minutes: 15 + container: debian:13-slim@sha256:d7e12182ce18b85b93007c1dedf31f2d29e01ccf3182cc4017c709b6259bc132 + steps: + - name: Install authenticated Debian toolchain packages + run: | + apt-get update + apt-get install --no-install-recommends -y ca-certificates git ripgrep agda-bin=2.6.4.3-1+b2 + - uses: actions/checkout@v6.0.3 + with: + persist-credentials: false + - name: Verify toolchain and proof constructions + run: | + test "$(agda --version)" = 'Agda version 2.6.4.3' + bash tests/check-proofs.sh + bash tests/check-rejections.sh + + echo: + name: Canonical Echo correspondence + runs-on: ubuntu-24.04 + timeout-minutes: 15 + container: debian:13-slim@sha256:d7e12182ce18b85b93007c1dedf31f2d29e01ccf3182cc4017c709b6259bc132 + steps: + - name: Install authenticated Debian toolchain packages + run: | + apt-get update + apt-get install --no-install-recommends -y ca-certificates git agda-bin=2.6.4.3-1+b2 agda-stdlib=2.1-4 + - uses: actions/checkout@v6.0.3 + with: + persist-credentials: false + - name: Checkout reviewed canonical Echo source + uses: actions/checkout@v6.0.3 + with: + repository: hyperpolymath/echo-types + ref: 46cd1a32d4dcf1020f01dd1aab41f816742da10e + path: .ci-deps/echo-types + persist-credentials: false + - name: Prove representation round trips and lowering agreement + run: | + test "$(agda --version)" = 'Agda version 2.6.4.3' + agda --no-libraries --safe --without-K --double-check --ignore-interfaces \ + -W error -W noUnsupportedIndexedMatch -i src -i tests/integration \ + -i .ci-deps/echo-types/proofs/agda -i /usr/share/agda-stdlib/src \ + tests/integration/CanonicalEcho.agda diff --git a/.github/workflows/push-email-notify.yml b/.github/workflows/push-email-notify.yml index 0689291..676f498 100644 --- a/.github/workflows/push-email-notify.yml +++ b/.github/workflows/push-email-notify.yml @@ -1,3 +1,4 @@ +# This workflow is managed by gh actions-lock. # SPDX-License-Identifier: MPL-2.0 # Dormant push-email notification. ARMED by setting the repo variable # PUSH_EMAIL_ENABLED=true (the single on/off switch). Addresses are pre-filled; @@ -39,7 +40,7 @@ jobs: timeout-minutes: 5 steps: - name: Send push notification email - uses: hyperpolymath/smtp-notify-action@ede1191ef6ff3ac02c4f4d9efdf837ee517e11d7 # v0.2.0 + uses: hyperpolymath/smtp-notify-action@v0.2.0 with: server_address: ${{ secrets.SMTP_HOST }} server_port: ${{ secrets.SMTP_PORT }} diff --git a/.github/workflows/secret-scanner.yml b/.github/workflows/secret-scanner.yml index d325a5c..5bf0622 100644 --- a/.github/workflows/secret-scanner.yml +++ b/.github/workflows/secret-scanner.yml @@ -1,3 +1,4 @@ +# This workflow is managed by gh actions-lock. # SPDX-License-Identifier: MPL-2.0 # Calls the estate's shared secret scanner (gitleaks + rust-secrets + # shell-secrets). Added because this repository had NO leak scanning at all. diff --git a/.gitignore b/.gitignore index 068797e..ec8bd0e 100644 --- a/.gitignore +++ b/.gitignore @@ -2,3 +2,6 @@ _build/ *~ .DS_Store + +# Ephemeral canonical-integration checkout +/.ci-deps/ diff --git a/.machine_readable/6a2/0-AI-MANIFEST.a2ml b/.machine_readable/descriptiles/0-AI-MANIFEST.a2ml similarity index 88% rename from .machine_readable/6a2/0-AI-MANIFEST.a2ml rename to .machine_readable/descriptiles/0-AI-MANIFEST.a2ml index e639cb9..49e6832 100644 --- a/.machine_readable/6a2/0-AI-MANIFEST.a2ml +++ b/.machine_readable/descriptiles/0-AI-MANIFEST.a2ml @@ -1,4 +1,4 @@ -# 0-AI-MANIFEST.a2ml — AI-assistant context for the 6a2 directory +# 0-AI-MANIFEST.a2ml — AI-assistant context for the descriptiles directory # epistemic-types: directory manifest, modeling rules, and the typecheck command. [manifest] @@ -23,15 +23,15 @@ factivity = "Separate factive knowledge from non-factive belief." warrants = "Use explicit warrant objects where possible." scope = "Keep modules small and type-check frequently; keep to a single-tool Agda library checked by 'just check'." echo_distinction = "Echo-types are min-plus-graded loss/residue modalities; epistemic types are standpoint/warrant/access modalities." -no_collapse = "Do not collapse Echo r A and E κ A. Their composition is meaningful, but they are not the same modality." +no_collapse = "Do not collapse Echo C y and E κ A. Their composition is meaningful, but they are not the same modality." [typecheck] command = "agda --no-libraries -i src src/EpistemicTypes/All.agda" just-target = "just check" -agda-version = "2.8.0" +agda-version = "2.6.4.3" [canonical-locations] -# The 6a2 directory is authoritative for this repo's machine-readable metadata. +# The descriptiles directory is authoritative for this repo's machine-readable metadata. # Present in this directory (right-sized for a small formal-methods prototype): present = [ "0-AI-MANIFEST.a2ml", "STATE.a2ml", "README.adoc" ] diff --git a/.machine_readable/6a2/AGENTIC.a2ml b/.machine_readable/descriptiles/AGENTIC.a2ml similarity index 89% rename from .machine_readable/6a2/AGENTIC.a2ml rename to .machine_readable/descriptiles/AGENTIC.a2ml index d0f68d7..d8725ee 100644 --- a/.machine_readable/6a2/AGENTIC.a2ml +++ b/.machine_readable/descriptiles/AGENTIC.a2ml @@ -12,7 +12,7 @@ last-updated = "2026-06-15" [agent-permissions] can-edit-source = true # Agda modules under src/EpistemicTypes/ can-edit-docs = true # readme.adoc, explainme.adoc, AsciiDoc docs -can-edit-machine-readable = true # .machine_readable/ (6a2, proof-transport) +can-edit-machine-readable = true # .machine_readable/ (descriptiles, proof-transport) can-edit-build = true # Justfile, epistemic-types.agda-lib, .gitignore can-create-files = true can-edit-license = false # LICENSE / SPDX are owner-manual — agents MUST NOT touch @@ -29,7 +29,7 @@ can-add-spdx-headers = false # repo is intentionally SPDX-free; keep it consist # is a plain indexed endofunctor (map only). Do NOT add a generic return, # reflect, join, or extract that is not justified by an explicit field or proof. # Laws appear as fields when not derivable; they are never assumed silently. -# - Never collapse Echo r A (min-plus graded loss/residue) into E κ A. Their +# - Never collapse Echo C y (certified residue and separately measured bounds) into E κ A. Their # composition is meaningful; they are not the same modality. # - Never break the ProofTransport no-smuggling discipline: verify upgrades # Data -> Proof only with the receiver's OWN checker + evidence; transmit @@ -37,12 +37,12 @@ can-add-spdx-headers = false # repo is intentionally SPDX-free; keep it consist # certifies. Do not weaken proofNeedsChecker. # Repository hygiene: # - Never place state files in the repository root. Machine-readable state lives -# under .machine_readable/ (6a2, proof-transport). +# under .machine_readable/ (descriptiles, proof-transport). # - Never edit LICENSE or add SPDX-License-Identifier / copyright headers. # Licensing (classified MPL-2.0 as the owner's sole repo) is owner-manual only. # - Never commit secrets or credentials. # - Keep docs in AsciiDoc; do not rename or duplicate readme.adoc / explainme.adoc. -# - Do not add CI / GitHub Actions workflows or badges (not enabled; see AUDIT.adoc). +# - Maintain the owner-authorized proof and security CI gates; never bypass failing checks. [maintenance-integrity] fail-closed = true @@ -56,7 +56,7 @@ release-claim-requires-hard-pass = true # The single source of truth for "does it hold". command = "just check" underlying = "agda --no-libraries -i src src/EpistemicTypes/All.agda" -agda-version = "2.8.0" +agda-version = "2.6.4.3" entrypoint = "src/EpistemicTypes/All.agda" expected = "type-checks clean, no postulates, no warnings" diff --git a/.machine_readable/6a2/ECOSYSTEM.a2ml b/.machine_readable/descriptiles/ECOSYSTEM.a2ml similarity index 87% rename from .machine_readable/6a2/ECOSYSTEM.a2ml rename to .machine_readable/descriptiles/ECOSYSTEM.a2ml index 7fa99f3..24f4c52 100644 --- a/.machine_readable/6a2/ECOSYSTEM.a2ml +++ b/.machine_readable/descriptiles/ECOSYSTEM.a2ml @@ -12,13 +12,13 @@ type = "formal-methods-library" purpose = "A small, deliberately honest Agda formalization of standpoint-indexed modal / epistemic / echo-like type formers. Favours mathematical honesty over a large API: constructive, no postulates, no standard library." [stack] -language = "Agda 2.8.0" +language = "Agda 2.6.4.3" options = "--safe --without-K" libraries = "none — built with 'agda --no-libraries' against Agda.Builtin.* and Agda.Primitive only" machine-readable = "a2ml + Nickel/k9" docs = "AsciiDoc" check = "just check == agda --no-libraries -i src src/EpistemicTypes/All.agda" -notes = "Single-tool Agda library. No JS/TS/Python, no containers, no CI (see AUDIT.adoc)." +notes = "Single-tool Agda library. The core has no runtime dependencies; CI uses a pinned Debian verification container." [core] form = "E : K -> Set ℓ -> Set ℓ (E κ A = 'A is epistemically available at standpoint κ')" @@ -27,7 +27,7 @@ modules = [ "EpistemicTypes.Base — Modality / LawfulModality / FactiveModality / BeliefModality / ReturnModality", "EpistemicTypes.Warrant — Warrant / Epi / SoundWarrant", "EpistemicTypes.Access — Preorder + AccessibleModality transport 'increase'", - "EpistemicTypes.EchoBridge — min-plus graded loss/residue 'Echo r A', kept distinct from E κ A", + "EpistemicTypes.EchoBridge — certified residue and separately measured bounds 'Echo C y', kept distinct from E κ A", "EpistemicTypes.SurrealBridge — SurrealAccess carrier + GradedSurrealModality + daySurrealAccess finite birthday tower", "EpistemicTypes.Examples", "EpistemicTypes.ProofTransport — standpoint-indexed proof transport across trust boundaries", @@ -43,8 +43,8 @@ no-smuggling = "proofNeedsChecker: no checker-free Proof -> Proof transport is e [related-projects] projects = [ - { name = "echo-types", relationship = "sibling-formalism", notes = "Agda loss-with-residue (min-plus graded) formalism. EpistemicTypes.EchoBridge's 'Echo r A' composes with it; kept deliberately distinct from the epistemic E κ A modality (no collapse)." }, + { name = "echo-types", relationship = "sibling-formalism", notes = "Agda loss-with-residue (min-plus graded) formalism. EpistemicTypes.EchoBridge's 'Echo C y' composes with it; kept deliberately distinct from the epistemic E κ A modality (no collapse)." }, { name = "ephapax", relationship = "sibling-formal-language", notes = "Sibling formal language; its four-layer redesign carries echo obligations. Echo / standpoint vocabulary is shared at the conceptual level, not via a code dependency." }, - { name = "standards", relationship = "estate-foundation", notes = "Estate RSR / standards repo plus k9-svc and a2ml tooling. Supplies the 6a2 layout and the contractile / k9 rendering conventions this repo's .machine_readable mirrors." }, + { name = "standards", relationship = "estate-foundation", notes = "Estate RSR / standards repo plus k9-svc and a2ml tooling. Supplies the descriptiles layout and the contractile / k9 rendering conventions this repo's .machine_readable mirrors." }, { name = "a2ml + k9", relationship = "rendering-target", notes = "Machine-readable a2ml + Nickel/k9 contractile tooling. The engineering rendering target for ProofTransport: the standpoint-indexed proof-transport core is rendered to a2ml/k9 under .machine_readable/proof-transport/." } ] diff --git a/.machine_readable/6a2/META.a2ml b/.machine_readable/descriptiles/META.a2ml similarity index 97% rename from .machine_readable/6a2/META.a2ml rename to .machine_readable/descriptiles/META.a2ml index c156dc1..39835a8 100644 --- a/.machine_readable/6a2/META.a2ml +++ b/.machine_readable/descriptiles/META.a2ml @@ -57,8 +57,8 @@ consequence = "The project is self-contained and reproducible with just an Agda [architecture-decisions.ADR-005] title = "Keep Echo grades distinct from epistemic standpoints" status = "accepted" -context = "`EchoBridge` provides a min-plus-graded loss/residue modality `Echo r A`. It is tempting to identify the grade `r` with an epistemic standpoint `κ`, collapsing two different ideas." -decision = "`Echo r A` (graded loss/residue) and `E κ A` (standpoint-indexed epistemic availability) are kept as separate type formers. Their composition is meaningful and intended, but they are never the same modality." +context = "`EchoBridge` provides a min-plus-graded loss/residue modality `Echo C y`. It is tempting to identify the grade `r` with an epistemic standpoint `κ`, collapsing two different ideas." +decision = "`Echo C y` (graded loss/residue) and `E κ A` (standpoint-indexed epistemic availability) are kept as separate type formers. Their composition is meaningful and intended, but they are never the same modality." consequence = "The echo bridge can be extended without dragging in a full graded comonad, and standpoint reasoning stays independent of loss accounting." [architecture-decisions.ADR-006] @@ -72,7 +72,7 @@ consequence = "No-smuggling holds structurally rather than by side-condition. Th build-tool = "just" build-command = "just check" check-command = "agda --no-libraries -i src src/EpistemicTypes/All.agda" -agda-version = "2.8.0" +agda-version = "2.6.4.3" package-manager = "none (single agda-lib; no external Agda dependencies)" ci-platform = "none (billing wall; see AUDIT.adoc)" container-runtime = "none" @@ -82,7 +82,7 @@ posture = "Mathematical honesty over API size. The library is small on purpose: base-interface = "`E : K -> Set ℓ -> Set ℓ`, read `E κ A` = 'A is epistemically available at standpoint κ'. The base is a plain indexed endofunctor (map only) — not a monad or comonad — so no return/reflect is assumed for free." factivity = "Factive knowledge and non-factive belief are distinct interfaces (FactiveModality vs BeliefModality), preventing belief from being read as knowledge." access = "`Access` adds a preorder over standpoints and an `AccessibleModality` whose `increase` transports availability along the preorder." -echo = "`EchoBridge` supplies a min-plus-graded loss/residue modality `Echo r A`, kept structurally distinct from epistemic availability; the two compose but never collapse (see ADR-005)." +echo = "`EchoBridge` supplies a min-plus-graded loss/residue modality `Echo C y`, kept structurally distinct from epistemic availability; the two compose but never collapse (see ADR-005)." surreal = "`SurrealBridge` offers an abstract `SurrealAccess` carrier with a `GradedSurrealModality` and a finite-birthday tower `daySurrealAccess`, as instances of the abstract access interface rather than a full surreal-number library." proof-transport = "`ProofTransport` formalizes standpoint-indexed proof transport across trust boundaries with statuses Data/Code/Claimed/Receipt/Proof/ProofUnder and modes Public/Designated/IssuerMediated/EnvironmentMediated/OpaqueReceipt; no-smuggling is by construction (see ADR-006)." modules = "Base, Warrant, Access, EchoBridge, SurrealBridge, Examples, ProofTransport, ProofTransportExample, with All re-exporting the development." diff --git a/.machine_readable/6a2/NEUROSYM.a2ml b/.machine_readable/descriptiles/NEUROSYM.a2ml similarity index 89% rename from .machine_readable/6a2/NEUROSYM.a2ml rename to .machine_readable/descriptiles/NEUROSYM.a2ml index ecfda3a..1296e08 100644 --- a/.machine_readable/6a2/NEUROSYM.a2ml +++ b/.machine_readable/descriptiles/NEUROSYM.a2ml @@ -1,7 +1,7 @@ # NEUROSYM.a2ml — Neurosymbolic integration metadata # Hypatia scanning + symbolic-rule configuration for epistemic-types. # This is a small Agda formal-methods prototype, checked by `just check` -# (== `agda --no-libraries -i src src/EpistemicTypes/All.agda`, Agda 2.8.0). +# (== `agda --no-libraries -i src src/EpistemicTypes/All.agda`, Agda 2.6.4.3). # Rules below are right-sized to that single-tool library; honesty over breadth. [metadata] @@ -33,7 +33,7 @@ rules = [ { name = "no-no-termination-check", pattern = "\\{-# NO_TERMINATION_CHECK #-\\}", severity = "critical", note = "Legacy termination bypass; forbidden for the same reason as TERMINATING." }, { name = "no-stdlib-import", pattern = "open import (Data|Relation|Function|Algebra|Category|Codata|Effect|Foreign|IO|Reflection|Tactic|Agda\\.Builtin\\.Reflection)\\b", severity = "high", note = "Repo builds with `agda --no-libraries`; only `Agda.Builtin.*` and `Agda.Primitive` are permitted. A standard-library import would not type-check under `just check` and breaks the self-contained guarantee." }, { name = "no-unsafe-options", pattern = "\\{-# OPTIONS[^#]*--type-in-type", severity = "critical", note = "`--type-in-type` is inconsistent; the repo target is `--safe --without-K`." }, - { name = "echo-not-collapsed", pattern = "Echo .* = .* E ", severity = "medium", note = "Heuristic: Echo r A (min-plus graded loss/residue) and E kappa A (epistemic availability) are distinct modalities. Their composition is meaningful; their identification is a modelling error. Manual review on hit." } + { name = "echo-not-collapsed", pattern = "Echo .* = .* E ", severity = "medium", note = "Heuristic: Echo C y (certified residue and separately measured bounds) and E kappa A (epistemic availability) are distinct modalities. Their composition is meaningful; their identification is a modelling error. Manual review on hit." } ] [symbolic-rules.notes] @@ -47,9 +47,9 @@ safe-flags = "--safe --without-K" # Neural pattern detection is not configured for this prototype. # A formal Agda library is better served by the deterministic symbolic rules # above and by the type-checker than by learned pattern matching. -enabled = false +enabled = true [ci] -# No CI is configured for this repository (no GitHub Actions workflows, no badges). +# CI checks core proofs, semantic rejections, pinned Echo correspondence and workflow/secret security. # See AUDIT.adoc. Verification is local via `just check`. -enabled = false +enabled = true diff --git a/.machine_readable/6a2/PLAYBOOK.a2ml b/.machine_readable/descriptiles/PLAYBOOK.a2ml similarity index 84% rename from .machine_readable/6a2/PLAYBOOK.a2ml rename to .machine_readable/descriptiles/PLAYBOOK.a2ml index 48bbeaa..56d4f9b 100644 --- a/.machine_readable/6a2/PLAYBOOK.a2ml +++ b/.machine_readable/descriptiles/PLAYBOOK.a2ml @@ -1,6 +1,6 @@ # PLAYBOOK.a2ml — Operational playbook # Runbook for epistemic-types: a single-tool Agda library checked by `just check`. -# Concise and specific to this repo. There is no service to deploy and no CI. +# Concise and specific to this repo. There is no service to deploy; CI verifies the proof and security contracts. [metadata] version = "0.1.0" @@ -19,7 +19,7 @@ ci = "not enabled (see AUDIT.adoc)" # The single source of truth for 'is the library healthy?'. command = "just check" expands-to = "agda --no-libraries -i src src/EpistemicTypes/All.agda" -agda-version = "2.8.0" +agda-version = "2.6.4.3" options = "--safe --without-K" dependencies = "none (only Agda.Builtin.* / Agda.Primitive; no standard library; no postulates)" green-means = "All.agda re-exports every module and the whole library typechecks." @@ -27,20 +27,20 @@ green-means = "All.agda re-exports every module and the whole library typechecks [incident-response] # 'Incident' here = the library stopped typechecking. steps = [ - "1. Read .machine_readable/6a2/STATE.a2ml for current status, assumptions, and the module list.", + "1. Read .machine_readable/descriptiles/STATE.a2ml for current status, assumptions, and the module list.", "2. Run `just check` to reproduce the failure (same as `agda --no-libraries -i src src/EpistemicTypes/All.agda`).", "3. Read the Agda error: it names the failing module under src/EpistemicTypes/ and the offending goal or type.", "4. Open and inspect that failing module; fix the definition or the field standing in for a not-yet-derived law.", "5. Re-run `just check` until green; the whole library must typecheck via All.agda." ] honesty-rule = "Never silence a failure with a postulate or by weakening --safe/--without-K. Laws appear as explicit fields when they are not derivable." -boundary-rule = "Do not collapse Echo r A (min-plus graded loss/residue) into E κ A (standpoint/warrant/access). Their composition is meaningful; they are not the same modality." +boundary-rule = "Do not collapse Echo C y (certified residue and separately measured bounds) into E κ A (standpoint/warrant/access). Their composition is meaningful; they are not the same modality." [release-process] steps = [ - "1. Bump version in .machine_readable/6a2/STATE.a2ml and META.a2ml.", + "1. Bump version in .machine_readable/descriptiles/STATE.a2ml and META.a2ml.", "2. Run `just check` and confirm it is green.", - "3. Update CHANGELOG.md with the changes for this version.", + "3. Update CHANGELOG.adoc with the changes for this version.", "4. Tag the release at the green commit." ] preconditions = "`just check` is green; no postulates introduced; --safe --without-K still hold." diff --git a/.machine_readable/6a2/README.adoc b/.machine_readable/descriptiles/README.adoc similarity index 100% rename from .machine_readable/6a2/README.adoc rename to .machine_readable/descriptiles/README.adoc diff --git a/.machine_readable/6a2/STATE.a2ml b/.machine_readable/descriptiles/STATE.a2ml similarity index 74% rename from .machine_readable/6a2/STATE.a2ml rename to .machine_readable/descriptiles/STATE.a2ml index 489eb35..87e89e9 100644 --- a/.machine_readable/6a2/STATE.a2ml +++ b/.machine_readable/descriptiles/STATE.a2ml @@ -20,33 +20,36 @@ discipline = "Constructive. Compiles under {-# OPTIONS --safe --without-K #-}. N honesty-rule = "Laws appear as explicit fields when not derivable; lawful instances are added only after proving or explicitly assuming the laws. No smuggling." [build] -checker = "Agda 2.8.0" +checker = "Agda 2.6.4.3" command = "just check" -expands-to = "agda --no-libraries -i src src/EpistemicTypes/All.agda" +expands-to = "bash tests/check-proofs.sh && bash tests/check-rejections.sh" aggregator = "src/EpistemicTypes/All.agda re-exports every module." [modules] # Agda modules under src/EpistemicTypes/. list = [ - "EpistemicTypes.Base", - "EpistemicTypes.Warrant", "EpistemicTypes.Access", - "EpistemicTypes.SurrealBridge", + "EpistemicTypes.All", + "EpistemicTypes.Base", + "EpistemicTypes.ContinuityExamples", "EpistemicTypes.EchoBridge", "EpistemicTypes.Examples", "EpistemicTypes.ProofTransport", "EpistemicTypes.ProofTransportExample", + "EpistemicTypes.ReadConsistency", + "EpistemicTypes.SurrealBridge", + "EpistemicTypes.Warrant", ] [modules.detail] base = "Modality / LawfulModality / FactiveModality / BeliefModality / ReturnModality. The base form E κ A reads 'A is epistemically available at standpoint κ'." warrant = "Warrant / Epi / SoundWarrant." access = "Preorder + AccessibleModality transport 'increase'." -echo-bridge = "Min-plus graded loss/residue 'Echo r A', kept deliberately distinct from E κ A." +echo-bridge = "Certified residue Echo C y, explicit source compatibility, recovery/migration laws and measured resource bounds; distinct from E κ A." surreal-bridge = "SurrealAccess carrier + GradedSurrealModality + daySurrealAccess finite birthday tower." examples = "Worked instances exercising the interfaces." -proof-transport = "Standpoint-indexed proof transport across trust boundaries. View : Agent -> Artifact -> Status -> Claim -> Set; statuses Data/Code/Claimed/Receipt/Proof/ProofUnder; modes Public/Designated/IssuerMediated/EnvironmentMediated/OpaqueReceipt. transmit downgrades a sender's Proof to a receiver's Receipt; verify upgrades Data->Proof only with the receiver's OWN checker+evidence; public is portable, designated is receiver-bound, receipt-only never certifies; proofNeedsChecker = structural no-smuggling." -proof-transport-example = "A K9-SVC / A2ML attestation: issuer K9SVC, receiver Alice, third party Bob, claim ActionWasPerformed, artifact AttestationBlob." +proof-transport = "proofSound derives Meaning holder artifact claim from an accepted sound checker. Receipts alone do not certify; transfer requires the target-holder meaning." +proof-transport-example = "Boolean certificate checker with legitimate acceptance and refutations for false claims, changed artifacts and holder-sensitive replay." [route-to-mvp] milestones = [ @@ -69,7 +72,7 @@ items = [ ] [progress-summary] -note = "Prototype. The base interface and all eight modules typecheck under 'just check' (Agda 2.8.0, --safe --without-K, --no-libraries, no postulates). The endofunctor/Modality formers, Warrant, Access transport, EchoBridge residue, SurrealBridge tower, ProofTransport, and its K9-SVC/A2ML attestation example are in place. Remaining work is semantics and lawful instances — see [roadmap]." +note = "Prototype. The base interface and all eleven modules typecheck under 'just check' (Agda 2.6.4.3, --safe --without-K, --no-libraries, no postulates). The endofunctor/Modality formers, Warrant, Access transport, EchoBridge residue, SurrealBridge tower, ProofTransport, and its K9-SVC/A2ML attestation example are in place. Remaining work is semantics and lawful instances — see [roadmap]." [blockers-and-issues] # No active blockers. @@ -83,8 +86,8 @@ actions = [ ] [ci] -enabled = false -note = "CI is not enabled (see AUDIT.adoc). Checking is local via 'just check'." +enabled = true +note = "Proof and security CI are configured; see docs/ci-safety.adoc for merge requirements." [ecosystem] part-of = ["RSR Framework", "echo / epistemic formal-methods siblings"] diff --git a/.machine_readable/proof-transport/ProofTransport.a2ml b/.machine_readable/proof-transport/ProofTransport.a2ml index 8080d78..ec099bc 100644 --- a/.machine_readable/proof-transport/ProofTransport.a2ml +++ b/.machine_readable/proof-transport/ProofTransport.a2ml @@ -1,97 +1,71 @@ [spec] id = "proof-transport" -title = "Standpoint-indexed proof transport across trust boundaries" +title = "Proof transport with explicit semantic soundness" +api_status = "breaking prototype correction, unreleased" +updated = "2026-09-07" research_module = "EpistemicTypes.ProofTransport" research_source = "src/EpistemicTypes/ProofTransport.agda" example_module = "EpistemicTypes.ProofTransportExample" example_source = "src/EpistemicTypes/ProofTransportExample.agda" engineering_k9 = ".machine_readable/proof-transport/proof-transport.k9.ncl" +thesis = "Every proof status entails the stated holder/artifact/claim meaning through successful sound verification." -thesis = "Proofhood is standpoint-indexed. Transmission across a trust boundary moves bytes (von Neumann), not proofhood (Curry-Howard). A receiver recovers proofhood only with its own checker (verifier) plus evidence (certificate)." +[parameters] +Agent = "Set of holders." +Claim = "Set of claim labels; labels alone are not propositions." +Artifact = "Set of artifacts including any context the claim requires." +Meaning = "Agent -> Artifact -> Claim -> Set: the proposition to establish." +Payload = "Artifact -> Claim -> Set: certificate data without assumed validity." -[entities] -Agent = "Who holds a standpoint / view." -Claim = "What is asserted." -Artifact = "The von Neumann object: bytes, code, certificate." -Boundary = "A directed trust boundary, from a sender to a receiver." -Mode = "How an attestation is verified." -Status = "Epistemic status of an artefact for a holder w.r.t. a claim." -Gap = "A reason an upgrade to Proof fails." -Checker = "A holder's capability to verify, in a mode, that an artefact certifies a claim." -Evidence = "The certificate payload; plain data that crosses the boundary freely." -View = "The judgement View holder artifact status claim." +[verification] +CertificateCheck = "check : Payload a c -> Bool; sound : (p : Payload a c) -> check p = true -> Meaning holder a c." +Evidence = "Mode-indexed wrapper carrying a Payload a c." +Checker = "A mode-indexed CertificateCheck; designated mode pins the holder." +proof_introduction = "Certifying m, checker, evidence, and runChecker checker evidence = true." +verify = "Evaluates the check; successful verification yields Proof, false yields InvalidEvidence." +opaque = "OpaqueReceipt always yields OpaqueGap." +tryUpgrade = "Additionally emits MissingChecker or MissingEvidence." [statuses] -values = [ - "Data", - "Code", - "Claimed", - "Receipt", - "Proof", - "ProofUnder" -] +values = ["Data", "Code", "Claimed", "Receipt", "Proof", "ProofUnder"] [modes] -Public = "Publicly checkable; transferable; the checker is portable to any agent." -Designated = "Bound to one designated party; the checker is receiver-bound (deniable to third parties)." -IssuerMediated = "Requires the holder to trust the issuer." -EnvironmentMediated = "Requires a runtime / environment context." -OpaqueReceipt = "Acknowledges receipt only; never certifies the underlying claim." +Public = "Reusable checking algorithm; transport requires Meaning r a c -> Meaning q a c." +Designated = "Checker index pins designation to holder; not a cryptographic deniability theorem." +IssuerMediated = "Must supply the same acceptance soundness obligation; issuer authority is not inferred from its name." +EnvironmentMediated = "Must supply the same acceptance soundness obligation; environmental assumptions belong in Meaning." +OpaqueReceipt = "Non-certifying." [gaps] -values = [ - "TrivialGap", - "DesignatedGap", - "EnvironmentGap", - "IssuerTrustGap", - "OpaqueGap", - "MissingChecker", - "MissingEvidence", - "MissingContext" -] - -[judgement] -view = "View : Agent -> Artifact -> Status -> Claim -> Set" -intro_cheap = "Data, Code, Claimed, Receipt are freely introducible." -intro_proof = "ProofUnder m requires Certifying m, Checker holder m, and Evidence m; Proof is reached only by forgetting the mode of a ProofUnder." - -[operations] -transmit = "Boundary -> View (from b) a Proof c -> View (to b) a Receipt c (transport downgrades proof to receipt)." -verify = "Checker holder m a c -> Evidence m a c -> View holder a Data c -> Either Gap (View holder a Proof c)." -tryUpgrade = "Maybe Checker -> Maybe Evidence -> View Data -> Either Gap (View Proof) (names MissingChecker / MissingEvidence)." +values = ["TrivialGap", "DesignatedGap", "EnvironmentGap", "IssuerTrustGap", "OpaqueGap", "MissingChecker", "MissingEvidence", "MissingContext", "InvalidEvidence"] +realized = ["OpaqueGap", "MissingChecker", "MissingEvidence", "InvalidEvidence"] [theorems] -checkableTransportUpgrades = "Sender proof + boundary + receiver data + receiver checker + evidence => Either Gap (receiver Proof). The sender proof and boundary are unused: only the receiver-side checker + evidence justify the upgrade." -publicTransfer = "A public checker + public evidence upgrades data to proof." -publicIsPortable = "Checker r Public a c -> Checker q Public a c (public verification is not bound to one receiver)." -designatedTransfer = "The designated receiver can verify a designated attestation addressed to it." -designatedBindsHolder = "Checker holder (Designated d) a c -> d = holder (no third party can hold a checker for another's designation)." -opaqueNotCertifying = "There is no Certifying instance for OpaqueReceipt." +proofSound = "View holder a Proof c -> Meaning holder a c." +proofCannotSupportFalse = "Not (Meaning holder a c) -> Not (View holder a Proof c)." +proofHasSuccessfulCheck = "Extracts checker, payload evidence, and its accepted-check equality." +proofNeedsChecker = "Weaker structural projection; alone did not establish semantic soundness in the previous model." +publicIsPortable = "Requires an explicit implication between source and receiver meanings." +designatedBindsHolder = "Checker holder (Designated d) a c -> d = holder." +opaqueNotCertifying = "Certifying OpaqueReceipt is empty." verifyReceiptIsGap = "verify receiptCheck ev v = left OpaqueGap." -proofNeedsChecker = "Every View holder a Proof c yields the holder's own mode, Certifying witness, checker, and evidence — so no checker-free Proof -> Proof transport is exported (no smuggling)." - -[honesty] -no_smuggling = "The receiver never gets Proof claim without checker/evidence premises present (enforced structurally by View's constructors)." -conservative_transport = "transmit yields only Receipt; no exported function View sender a Proof c -> View receiver a Proof c." -options = "Compiles under --safe --without-K; no postulates; no standard library (agda --no-libraries)." - -[mapping] -von_neumann = "Artifact + Data/Code: a program / proof object can cross the wall as data." -curry_howard = "Proof / ProofUnder: a checked program can be a proof of a proposition." -proof_carrying_code = "Evidence = certificate (travels); Checker = the consumer-side re-checker." -epistemic_types = "Proofhood is standpoint-indexed and must be transported/upgraded for the receiver, not assumed to transfer automatically." [scenario] -id = "k9-svc-attestation" -issuer = "K9SVC" receiver = "Alice" third_party = "Bob" -claim = "ActionWasPerformed" -artifact = "AttestationBlob" -case_1 = "AttestationBlob is raw Data for Alice." -case_2 = "Alice upgrades to Proof ActionWasPerformed with her designated checker + evidence." -case_3 = "Bob has only Receipt K9SVC ActionWasPerformed across the boundary, and cannot hold the Alice-designated checker — unless the attestation is public, which is portable." +claim = "ArtifactIsTrue" +artifact = "Boolean true; the claim means artifact = true." +payload = "Boolean certificate; the checking function rejects false payloads or false artifacts." +negative_claim = "ImpossibleClaim has empty meaning and cannot have a Proof status." +holder_case = "A meaning holder = Alice cannot be silently transported to Bob." + +[verification_gate] +command = "just check" +positive = "Complete safe Agda library including acceptance, rejection, semantic soundness, and holder-boundary proofs." +negative = ["LyingVerifier", "ForgedAcceptance", "ReplayedArtifact", "ReplayedHolder"] +negative_gate = "Must reach the expected type error; unrelated failures do not pass." [scope] -intentionally_small = "This is a compositional core, not a full PCC system; cryptography, A2ML, and K9-SVC are not fully modelled." -future = "Concrete checkers, issuer-trust contexts, and a graded/Echo bridge for partial proofs." +model_boundary = "Soundness is relative to the supplied Meaning, checker proof, and Agda implementation." +not_established = ["physical action occurrence", "cryptography", "runtime integration", "hardware continuity", "external-store freshness", "canonical Echo bridge"] +retraction = "The earlier freely constructible checker/evidence tokens supported structural status bookkeeping only." diff --git a/.machine_readable/proof-transport/README.adoc b/.machine_readable/proof-transport/README.adoc index 5a559aa..23b2372 100644 --- a/.machine_readable/proof-transport/README.adoc +++ b/.machine_readable/proof-transport/README.adoc @@ -10,7 +10,7 @@ The Agda module is the authority; these files mirror it for A2ML/K9 tooling. | `ProofTransport.a2ml` | A2ML spec: entities, statuses, modes, gaps, judgement, operations, - theorems, the honesty discipline, and the K9-SVC scenario — for agents. + theorems, semantic soundness, and the Boolean certificate scenario — for agents. | `proof-transport.k9.ncl` | K9 contractile at `'Kennel` leash (pure data, no eval): the same model as a @@ -21,7 +21,8 @@ The Agda module is the authority; these files mirror it for A2ML/K9 tooling. Proofhood is standpoint-indexed. Transmission across a trust boundary moves bytes (von Neumann), not proofhood (Curry-Howard). A receiver recovers -proofhood only with its own checker (verifier) plus evidence (certificate) — +proofhood only through an accepted payload and a verifier's proof that +acceptance entails the explicit holder/artefact/claim meaning — the proof-carrying-code pattern, made standpoint-relative. == Correspondence @@ -35,15 +36,15 @@ the proof-carrying-code pattern, made standpoint-relative. | `Gap` | `gaps` | `transmit` | `law.transmit_yields = "Receipt"` | `verify` / `checkableTransportUpgrades` | `law.upgrade_requires` -| `publicIsPortable` | `modes.Public.portable = true` +| `publicIsPortable` | `modes.Public.portable = true` with `law.public_portability_requires` | `designatedBindsHolder` | `modes.Designated.receiver_bound = true` | `opaqueNotCertifying` | `modes.OpaqueReceipt.certifies = false` -| `proofNeedsChecker` | `law.no_free_proof_transfer = true` -| `ProofTransportExample` | `scenario` (K9SVC / Alice / Bob) +| `proofSound` | `law.semantic_guarantee` +| `ProofTransportExample` | `scenario` (Boolean artefact, certificate, Alice / Bob) |=== NOTE: `modes.*.gap_on_fail` in the k9 file is a *reserved* failure mapping. The -research core today constructs only `OpaqueGap` (via `verify`) and +research core today constructs `OpaqueGap` or `InvalidEvidence` (via `verify`) and `MissingChecker` / `MissingEvidence` (via `tryUpgrade`) — see `law.gaps_realized_today`. The remaining gaps are vocabulary for a future refinement, not behaviour the core implements yet. diff --git a/.machine_readable/proof-transport/proof-transport.k9.ncl b/.machine_readable/proof-transport/proof-transport.k9.ncl index 9136ed7..a273c4a 100644 --- a/.machine_readable/proof-transport/proof-transport.k9.ncl +++ b/.machine_readable/proof-transport/proof-transport.k9.ncl @@ -8,20 +8,20 @@ # # Thesis: proofhood is standpoint-indexed. Transmission across a trust boundary # moves bytes (von Neumann), not proofhood (Curry-Howard). A receiver recovers -# proofhood only with its own checker (verifier) + evidence (certificate) — the +# proofhood only through a sound checking function and an accepted payload — the # proof-carrying-code pattern, made standpoint-relative. let Leash = [| 'Kennel, 'Yard, 'Hunt |] in let Mode = [| 'Public, 'Designated, 'IssuerMediated, 'EnvironmentMediated, 'OpaqueReceipt |] in let Gap = [| 'TrivialGap, 'DesignatedGap, 'EnvironmentGap, 'IssuerTrustGap, - 'OpaqueGap, 'MissingChecker, 'MissingEvidence, 'MissingContext + 'OpaqueGap, 'MissingChecker, 'MissingEvidence, 'MissingContext, 'InvalidEvidence |] in # Per-mode transport semantics. let ModeRule = { certifies | Bool, # can a matching checker + evidence yield Proof? - portable | Bool, # is the checker reconstructible by any agent? + portable | Bool, # supported ONLY with an explicit meaning implication receiver_bound | Bool, # is the checker pinned to one designated holder? gap_on_fail | Gap, # RESERVED: the gap a future refinement would report # for this mode. The core does NOT yet emit these per @@ -33,22 +33,24 @@ let ModeRule = { contractile = { name = "proof-transport", - version = "0.1.0", + version = "0.2.0-unreleased", research_counterpart = "src/EpistemicTypes/ProofTransport.agda", example_counterpart = "src/EpistemicTypes/ProofTransportExample.agda", - summary = "Proofhood is standpoint-indexed; transmission moves bytes, not proofhood.", + summary = "Proof status entails an explicit meaning through accepted sound verification.", }, # The transport law, as data (cf. `transmit`, `checkableTransportUpgrades`, # `proofNeedsChecker` in the Agda module). law = { transmit_yields = "Receipt", # sender Proof crosses as Receipt - upgrade_requires = ["Certifying", "Checker", "Evidence"], + upgrade_requires = ["Certifying", "SoundChecker", "PayloadEvidence", "AcceptedCheckEquality"], + semantic_guarantee = "View holder a Proof c -> Meaning holder a c", + public_portability_requires = "Meaning r a c -> Meaning q a c", no_free_proof_transfer = true, # no Proof -> Proof without a checker # The research core currently CONSTRUCTS only these gaps: `verify` emits - # OpaqueGap (receipt-only); `tryUpgrade` emits MissingChecker / MissingEvidence. + # OpaqueGap (receipt-only) or InvalidEvidence; tryUpgrade also emits missing-resource gaps. # All other gaps (including modes.*.gap_on_fail) are reserved vocabulary. - gaps_realized_today = ["OpaqueGap", "MissingChecker", "MissingEvidence"], + gaps_realized_today = ["OpaqueGap", "MissingChecker", "MissingEvidence", "InvalidEvidence"], }, # Statuses an artefact can hold relative to a holder (data `Status`). @@ -81,25 +83,25 @@ let ModeRule = { # All gaps in the vocabulary (data `Gap`). gaps = [ "TrivialGap", "DesignatedGap", "EnvironmentGap", "IssuerTrustGap", - "OpaqueGap", "MissingChecker", "MissingEvidence", "MissingContext", + "OpaqueGap", "MissingChecker", "MissingEvidence", "MissingContext", "InvalidEvidence", ], - # The worked K9-SVC attestation scenario (mirrors ProofTransportExample.agda). + # The worked Boolean certificate scenario; no physical action is asserted. scenario = { issuer = "K9SVC", receiver = "Alice", third_party = "Bob", - claim = "ActionWasPerformed", - artifact = "AttestationBlob", + claim = "ArtifactIsTrue", + artifact = "Boolean true", cases = [ { who = "Alice", mode = 'Data, holds = ["blob"], result = "raw data; no claim certified" }, { who = "Alice", mode = 'Designated, holds = ["blob", "designated_checker", "designated_evidence"], - result = "Proof ActionWasPerformed" }, + result = "Proof that the Boolean artifact equals true, after successful sound check" }, { who = "Bob", mode = 'Receipt, holds = ["blob_via_transmit"], result = "Receipt only — designated checker is Alice-bound, so Bob cannot upgrade" }, { who = "Bob", mode = 'Public, holds = ["blob", "public_checker", "public_evidence"], - result = "Proof ActionWasPerformed — public checking is portable" }, + result = "Proof ArtifactIsTrue after successful check and supplied holder-meaning implication" }, ], }, diff --git a/.well-known/ai.txt b/.well-known/ai.txt index 067e6aa..60ae8f6 100644 --- a/.well-known/ai.txt +++ b/.well-known/ai.txt @@ -20,15 +20,15 @@ Disallow-Generation: yes # library, and must not weaken the --safe --without-K guarantees. # # For AI agent integration instructions, see: -# .machine_readable/6a2/0-AI-MANIFEST.a2ml (universal AI entry point) -# .machine_readable/6a2/STATE.a2ml (structured project state) +# .machine_readable/descriptiles/0-AI-MANIFEST.a2ml (universal AI entry point) +# .machine_readable/descriptiles/STATE.a2ml (structured project state) # .machine_readable/proof-transport/ (a2ml + k9 rendering of the # ProofTransport attestation model) # # Human-facing docs: readme.adoc, explainme.adoc # # Build / check: 'just check' -# == agda --no-libraries -i src src/EpistemicTypes/All.agda (Agda 2.8.0) +# == agda --no-libraries -i src src/EpistemicTypes/All.agda (Agda 2.6.4.3) # -# No CI is enabled for this repository (see AUDIT.adoc); there are no -# GitHub Actions workflows, badges, containers, or external pipelines. +# CI is enabled: proof constructions, semantic rejections, canonical Echo +# correspondence, CodeQL Actions and secret scanning. See docs/ci-safety.adoc. diff --git a/.well-known/humans.txt b/.well-known/humans.txt index dfd5dd3..8172f83 100644 --- a/.well-known/humans.txt +++ b/.well-known/humans.txt @@ -21,6 +21,6 @@ Components: Agda formalization of standpoint-indexed modal / epistemic / echo-like type formers; favours mathematical honesty over a large API. Constructive, no standard library (Agda.Builtin.* only). Languages: Agda (source), a2ml + Nickel/k9 (machine-readable), AsciiDoc (docs) -Tools: just, Agda 2.8.0 +Tools: just, Agda 2.6.4.3 Build: just check == agda --no-libraries -i src src/EpistemicTypes/All.agda CI: not enabled (see AUDIT.adoc) diff --git a/0-AI-MANIFEST.a2ml b/0-AI-MANIFEST.a2ml index 7c04fa7..ed84a53 100644 --- a/0-AI-MANIFEST.a2ml +++ b/0-AI-MANIFEST.a2ml @@ -4,7 +4,7 @@ title = "epistemic-types — universal AI agent entry point" version = "0.1.0" format = "a2ml" status = "prototype" -last-updated = "2026-06-15" +last-updated = "2026-09-07" [project] name = "epistemic-types" @@ -16,12 +16,12 @@ summary = "Core form E : K -> Set ℓ -> Set ℓ, read 'A is epistemically avail [canonical-locations] machine-readable = ".machine_readable/" -state = ".machine_readable/6a2/STATE.a2ml" -meta = ".machine_readable/6a2/META.a2ml" -ecosystem = ".machine_readable/6a2/ECOSYSTEM.a2ml" -agentic = ".machine_readable/6a2/AGENTIC.a2ml" -neurosym = ".machine_readable/6a2/NEUROSYM.a2ml" -playbook = ".machine_readable/6a2/PLAYBOOK.a2ml" +state = ".machine_readable/descriptiles/STATE.a2ml" +meta = ".machine_readable/descriptiles/META.a2ml" +ecosystem = ".machine_readable/descriptiles/ECOSYSTEM.a2ml" +agentic = ".machine_readable/descriptiles/AGENTIC.a2ml" +neurosym = ".machine_readable/descriptiles/NEUROSYM.a2ml" +playbook = ".machine_readable/descriptiles/PLAYBOOK.a2ml" proof-transport-spec = ".machine_readable/proof-transport/ProofTransport.a2ml" proof-transport-contractile = ".machine_readable/proof-transport/proof-transport.k9.ncl" proof-transport-readme = ".machine_readable/proof-transport/README.adoc" @@ -36,7 +36,7 @@ format = "AsciiDoc (.adoc) is the default; existing lowercase doc filenames are scm-files-location = ".machine_readable/ ONLY — a2ml and scm/Nickel/k9 files never live at repo root" license = "MPL-2.0" build = "just check" -build-expansion = "agda --no-libraries -i src src/EpistemicTypes/All.agda" +build-expansion = "safe Agda All.agda check plus tests/check-rejections.sh" agda-options = "{-# OPTIONS --safe --without-K #-} ; no postulates; no Agda standard library (only Agda.Builtin.* / Agda.Primitive)" agda-version = "2.8.0" echo-distinction = "Do not collapse Echo r A and E κ A. Echo-types are min-plus-graded loss/residue; epistemic types are standpoint/warrant/access modalities. Their composition is meaningful; they are not the same modality." @@ -64,7 +64,7 @@ EchoBridge = "Min-plus graded loss/residue 'Echo r A', kept distinct from E κ A SurrealBridge = "SurrealAccess carrier plus GradedSurrealModality plus daySurrealAccess finite-birthday tower." Examples = "Worked instances of the abstract interfaces." ProofTransport = "Standpoint-indexed proof transport across trust boundaries." -ProofTransportExample = "K9-SVC / A2ML attestation scenario: issuer K9SVC, receiver Alice, third party Bob, claim ActionWasPerformed, artifact AttestationBlob." +ProofTransportExample = "Sound Boolean certificate checks; valid acceptance, bad payload/artefact rejection, false-claim and holder-boundary impossibility." [proof-transport] thesis = "Proofhood is standpoint-indexed. Transmission across a trust boundary moves bytes (von Neumann), not proofhood (Curry-Howard); a receiver recovers proofhood only with its OWN checker plus evidence." @@ -72,21 +72,21 @@ view = "View : Agent -> Artifact -> Status -> Claim -> Set" statuses = [ "Data", "Code", "Claimed", "Receipt", "Proof", "ProofUnder" ] modes = [ "Public", "Designated", "IssuerMediated", "EnvironmentMediated", "OpaqueReceipt" ] transmit = "downgrades a sender's Proof to a receiver's Receipt" -verify = "upgrades Data -> Proof only with the receiver's OWN checker and evidence" +verify = "evaluates the receiver's sound check; acceptance yields Proof, rejection yields InvalidEvidence" laws = [ - "public is portable", + "public transport requires an explicit implication between holder meanings", "designated is receiver-bound", "receipt-only never certifies", - "proofNeedsChecker = structural no-smuggling", + "proofNeedsChecker = weaker structural projection; proofSound entails Meaning holder a c", ] authority = "The Agda module src/EpistemicTypes/ProofTransport.agda is authoritative; the .machine_readable/proof-transport/ rendering mirrors it for a2ml/k9 tooling." [session-startup] step-1 = "Read this manifest (0-AI-MANIFEST.a2ml)." -step-2 = "Read .machine_readable/6a2/STATE.a2ml for current project state, module list, and roadmap." -step-3 = "Read .machine_readable/6a2/META.a2ml for architecture and design decisions." -step-4 = "Read .machine_readable/6a2/ECOSYSTEM.a2ml for ecosystem position and sibling repos." -step-5 = "Read .machine_readable/6a2/AGENTIC.a2ml, NEUROSYM.a2ml, and PLAYBOOK.a2ml for agent guidance." +step-2 = "Read .machine_readable/descriptiles/STATE.a2ml for current project state, module list, and roadmap." +step-3 = "Read .machine_readable/descriptiles/META.a2ml for architecture and design decisions." +step-4 = "Read .machine_readable/descriptiles/ECOSYSTEM.a2ml for ecosystem position and sibling repos." +step-5 = "Read .machine_readable/descriptiles/AGENTIC.a2ml, NEUROSYM.a2ml, and PLAYBOOK.a2ml for agent guidance." step-6 = "Read readme.adoc and explainme.adoc for the human-facing overview." step-7 = "Run 'just check' to type-check src/EpistemicTypes/All.agda before and after changes." diff --git a/AFFIRMATION.adoc b/AFFIRMATION.adoc index ec68649..433d2d1 100644 --- a/AFFIRMATION.adoc +++ b/AFFIRMATION.adoc @@ -2,6 +2,14 @@ // SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell = AFFIRMATION — epistemic-types, as of 2026-06-16 :toc: macro + +NOTE: The dated historical affirmation below is superseded in scope by the +2026-09-07 repairs. Proof transport now entails its explicit Meaning; +ReadConsistency now models store histories with contents agreement; Echo now +uses certified residues, source compatibility, migration laws, and separate +measured bounds. Neither these proofs nor the earlier affirmation establishes +external-store or runtime refinement. Current evidence and limitations are in +`PROOF-STATUS.adoc` and `docs/continuity-foundations.adoc`. :toclevels: 2 _the No-Bullshit file: what we affirm was true and checkable at this moment_ @@ -180,7 +188,7 @@ logic, and it carries no LICENSE.* ** `ProofTransport.designatedBindsHolder` (`d ≡ holder`), `ProofTransport.opaqueNotCertifying` (`¬ Certifying OpaqueReceipt`), `ProofTransport.verifyReceiptIsGap` (a receipt-only verify is `left OpaqueGap`) - — the public-portable / designated-bound / receipt-never-certifies trichotomy. + — the explicitly qualified public portability / designated-bound / receipt-never-certifies distinction. ** `ReadConsistency.freshnessPropagatesUnderWrites`, `resyncRecoversFresh`, `syncChainEndsFresh`, `freshNotStale` — version-monotone re-sync liveness. ** `Access` preorder + monotone-transport laws, instantiated for real in @@ -227,7 +235,7 @@ sound" is overclaiming: it proves _its own_ formal statements, full stop. `# SPDX-License-Identifier: CC-BY-SA-4.0` line *and* a `# SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell ...` line (not prose mentions). The other `SPDX` strings (`CONTRIBUTING.md`, `AUDIT.adoc`, - `GOVERNANCE.adoc`, `.machine_readable/6a2/AGENTIC.a2ml`) are prose / policy + `GOVERNANCE.adoc`, `.machine_readable/descriptiles/AGENTIC.a2ml`) are prose / policy text. So the licence *classification* is already asserted MPL-2.0 inside those two workflow headers, while the source tree and the `LICENSE` file remain owner-pending. Per `AUDIT.adoc` and estate policy the licence is diff --git a/AUDIT.adoc b/AUDIT.adoc index 798309f..149749c 100644 --- a/AUDIT.adoc +++ b/AUDIT.adoc @@ -1,295 +1,53 @@ -= RSR Compliance Audit: epistemic-types -Jonathan D.A. Jewell (hyperpolymath) -v0.1.0, 2026-06-15 += epistemic-types: proof and repository safeguards +:revdate: 2026-09-07 :toc: -:toclevels: 2 -:sectnums: -== Purpose +== Current scope -This document is the repo-local RSR (Repository Standards & Readiness) audit -gate for `hyperpolymath/epistemic-types`. It records, honestly and in one -place, which Bronze and Silver requirements are *present*, which are -*owner-pending* (deliberately not actionable by an automated agent), and which -are *intentionally omitted* with a stated rationale. +This is a constructive Agda research library, at prototype maturity. Its current +claims are enumerated in link:PROOF-STATUS.adoc[], link:docs/proof-transport.adoc[] +and link:docs/continuity-foundations.adoc[]. The proof-transport, store freshness +and Echo relations have been reformulated to establish explicit semantic +obligations. Earlier stronger interpretations of token-only constructions are +withdrawn; successful typechecking alone did not establish those interpretations. -Canonical standards live in the `standards` repository. This file does not -restate them; it states where this specific repository sits against them. +== Verification and merge requirements -`epistemic-types` is a small, deliberately honest Agda formalization of -standpoint-indexed modal / epistemic / echo-like type formers. It favours -mathematical honesty over a large API. It is constructive, compiles under -`{-# OPTIONS --safe --without-K #-}`, has no postulates, and uses no Agda -standard library (built with `agda --no-libraries`, only `Agda.Builtin.*` and -`Agda.Primitive`). The audit posture below is sized for *a single-tool Agda -library checked by `just check`*, not for an application stack. +The owner authorized proof/security CI and protected-main enforcement on +2026-09-07. Earlier statements in this audit forbidding CI because of an estate +billing incident are superseded. Existing GitHub workflows already run; their +current proof coverage is extended by this change. -[IMPORTANT] -==== -*Current tier: approaching Bronze.* Every structural and documentation -requirement under our control is either present or part of the current -documentation pass. The single gating item for Bronze is `LICENSE`, which is -*owner-manual* (see <>). Silver is a later target and is tracked -here for direction only. -==== +* The eleven-module core is checked with Agda 2.6.4.3, safe mode, without-K, + internal double checking and warnings as errors. Each source module is checked. +* Eleven deliberate rejection fixtures must fail for their intended type mismatch. +* Canonical Echo residue correspondence is checked against pinned sibling source. +* CodeQL analyzes Actions workflows, and the shared scanner checks secrets. +* Main receives changes through PRs with required proof/security checks. Signed + commits and existing repository rules remain applicable. -== Status vocabulary +See link:docs/ci-safety.adoc[] for exact gates and limitations. A configured +workflow is not evidence of a successful run; inspect the PR's checks at the +commit being merged. No release-readiness, physical-uptime or certification +claim follows from these gates. -PRESENT:: The artefact exists in the repository (or is authored as part of this -documentation pass) and is consistent with the repo's actual state. -OWNER-PENDING:: A real requirement that an automated agent *must not* fulfil. -Reserved for the human owner under estate policy. Each entry explains why. -INTENTIONALLY-OMITTED:: Not applicable to a pure Agda library, or owned -elsewhere in the estate. Each entry explains why omission is correct, not -accidental debt. +== Canonical project description -== Bronze requirements +Machine-readable project descriptions are under `.machine_readable/descriptiles/`. +Proof-transport specifications remain under `.machine_readable/proof-transport/`. +The core imports only Agda builtins; external standard-library and Echo dependencies +are confined to the separate integration check. -[cols="3,1,5",options="header"] -|=== -| Requirement | Status | Notes +== Licence and ownership -| Project entry doc (`readme.adoc`) -| PRESENT -| Lowercase `readme.adoc`. Existing name is kept deliberately; not renamed or -duplicated to `README.adoc`. +`LICENSE` and the existing SPDX declarations are owner-managed. They are already +present; earlier statements that the repository lacked a licence are obsolete. +Agents must not create or change licensing declarations or copyright headers +without the owner's instruction. This CI/proof update does not change them. -| Plain-language explainer (`explainme.adoc`) -| PRESENT -| Lowercase `explainme.adoc` (EXPLAINME role). Existing name kept; not renamed -to `EXPLAINME.adoc`. +== Remaining obligations -| 6a2 machine-readable set (`.machine_readable/6a2/`) -| PRESENT -| `0-AI-MANIFEST.a2ml`, `STATE.a2ml`, `README.adoc`. `STATE.a2ml` declares the -`prototype` status, the eight `EpistemicTypes.*` modules, and the roadmap. - -| `CONTRIBUTING` -| PRESENT -| `CONTRIBUTING.md` (Markdown permitted by GitHub community-health special -casing). Right-sized: how to run `just check`, the no-postulates rule, and the -echo/epistemic no-collapse rule. - -| `SECURITY` -| PRESENT -| `SECURITY.md`. A formal Agda library has a small surface; the policy is -correspondingly small (coordinate disclosure to the owner; no runtime, no -network, no secrets). - -| `CODE_OF_CONDUCT` -| PRESENT -| `CODE_OF_CONDUCT.md`. - -| `CHANGELOG` -| PRESENT -| `CHANGELOG.md`. Opens at `0.1.0` (`prototype`). - -| `GOVERNANCE` -| PRESENT -| `GOVERNANCE.adoc`. Single-owner governance; decisions and merges rest with -the owner. - -| `MAINTAINERS` -| PRESENT -| `MAINTAINERS.adoc`. Sole maintainer: Jonathan D.A. Jewell (hyperpolymath). - -| `.well-known/` estate metadata -| PRESENT -| Repository self-description for estate tooling. - -| `.editorconfig` -| PRESENT -| Editor normalisation across `.agda`, `.a2ml`, `.ncl`, and `.adoc`. - -| `.gitattributes` -| PRESENT -| Line-ending and language attributes; keeps Agda Unicode and `.adoc` text -consistent. - -| Coordination contract (`coordination.k9`) -| PRESENT -| Repo-level k9 coordination descriptor for estate agents. - -| Narrative docs (`docs/`) -| PRESENT -| Longer-form design notes that would crowd `readme.adoc`. - -| Reproducible check entrypoint (`Justfile`) -| PRESENT -| `just check` == `agda --no-libraries -i src src/EpistemicTypes/All.agda` -(Agda 2.8.0). `default` aliases `check`. - -| Agda library descriptor (`epistemic-types.agda-lib`) -| PRESENT -| `name: epistemic-types`, `include: src`. - -| Source builds with the declared discipline -| PRESENT -| `src/EpistemicTypes/All.agda` re-exports the tree and type-checks under -`--safe --without-K`, no postulates, no stdlib. - -| `LICENSE` -| OWNER-PENDING -| *Gating item for Bronze.* See <>. - -| SPDX headers on all files -| OWNER-PENDING -| See <>. The repository is currently SPDX-free and is kept -internally consistent on purpose. -|=== - -== Silver requirements (direction, not yet claimed) - -These are tracked so the next steps are visible. None is claimed as met. - -[cols="3,1,5",options="header"] -|=== -| Requirement | Status | Notes - -| Concrete model instances (Kripke / evidence-state) -| OWNER-PENDING -| Roadmap item. The prototype intentionally exposes interfaces -(`Modality`, `LawfulModality`, `FactiveModality`, `BeliefModality`, -`ReturnModality`) and abstract access (`Preorder`, `AccessibleModality`) -without committing to a single semantics. Lawful instances are added only once -laws are proved or explicitly assumed. - -| Echo-types cross-formalism linkage -| PRESENT -| `EpistemicTypes.EchoBridge` provides a min-plus graded loss/residue -`Echo r A`, kept distinct from `E κ A`, designed to compose with the sibling -`echo-types` library *without importing it*. Deeper linkage is a Silver-level -commitment. - -| Surreal access fragment -| PRESENT -| `EpistemicTypes.SurrealBridge` gives `SurrealAccess`, -`GradedSurrealModality`, and a finite `daySurrealAccess` birthday tower. Richer -day-bounded fragments remain roadmap. - -| Proof-transport engineering rendering -| PRESENT -| `EpistemicTypes.ProofTransport` / `ProofTransportExample` plus the -`.machine_readable/proof-transport/` a2ml + k9 rendering. Full k9-svc / a2ml -tooling integration is a later, estate-level commitment. - -| Per-file SPDX + verified provenance -| OWNER-PENDING -| Blocked on the same owner-manual licence decision as Bronze. -|=== - -[#owner-pending] -== Owner-pending items (why an agent must not auto-apply) - -Under estate licence policy, *licence and SPDX changes are manual, file-by-file, -and owner-only*. An automated agent must not create a `LICENSE` file, must not -add `SPDX-License-Identifier` lines, and must not add copyright header lines — -*even when the policy-correct answer is known*. - -LICENSE:: -The correct classification for this repository is *MPL-2.0* (owner's sole -repo). This is recorded here only as a recommendation. The agent does not write -it. Rationale for the hard rule: a single mis-stamped header can seed an -invented repository "story" that later sweeps treat as law; licence drift across -the estate has been costly to unwind; and several sibling repos carry -*intentional* non-default licensing (for example son-shared AGPL repos) that a -naive sweep would corrupt. The blast radius of an automated licence edit is -therefore disproportionate to its apparent simplicity, so it is reserved to the -owner. - -SPDX headers:: -Same rationale. The repository is currently SPDX-free and is deliberately kept -that way until the owner applies headers as one manual, consistent action -alongside `LICENSE`. Partial or agent-applied SPDX would make the tree -inconsistent and would pre-empt the owner's licence decision. - -Because both items are owner-manual, *Bronze cannot be auto-completed*. This is -expected and is not a defect in this audit. - -== Intentionally omitted (with rationale) - -GitHub Actions CI workflows (CodeQL, Scorecard, etc.):: -*Omitted on purpose.* There is an estate-wide GitHub Actions billing wall, and -the Scorecard workflow is known-broken across the estate. Adding workflows here -would produce red, non-running, or unbillable jobs and would imply a CI posture -that does not exist. The real gate is local: `just check`. No CI badges are -claimed anywhere in this repository. - -Container / devcontainer (`Dockerfile`, `.devcontainer/`):: -*Not applicable.* This is a pure Agda library with no runtime, service, or -deployment target. The only toolchain dependency is Agda 2.8.0 invoked with -`--no-libraries`. A container would add weight without adding reproducibility -beyond the `Justfile` + `.agda-lib`. - -Contractiles (`Intent`/`Must`/`Trust`/`Adjust`/`Dust`/`Bust` files):: -*Owned elsewhere.* The canonical contractile layout lives as the trident master -in the `standards` subdir. Duplicating contractile scaffolding into a small -prototype would be over-scope and would risk re-propagating stale copies. This -repository defers to the estate canon. - -`guix.scm` / `flake.guix` packaging:: -*Future, not yet done.* The library is not yet packaged for Guix or Guix. This -is honest deferral, not hidden debt; the `Justfile` entrypoint is sufficient for -the prototype tier. Packaging may be added once the API stabilises beyond -`prototype`. - -Application-stack artefacts (fuzzing, benchmarks, CADRE, Elixir, CRDTs, Deno, -container orchestration):: -*Not applicable* to a single-tool Agda formalization. None is implied or -claimed. - -== Honest tier statement - -`epistemic-types` is *approaching Bronze*. All structural, documentation, and -machine-readable requirements within agent control are present (or authored in -this pass), the source type-checks under a strict, honesty-first discipline, -and every omission above is deliberate and justified. - -The *single gating item* for Bronze is `LICENSE` (with accompanying SPDX), which -is *owner-manual* by estate policy. The recommendation on record is *MPL-2.0*. -Until the owner applies it, this repository should not be described as Bronze, -`stable`, or released, and no automated agent should attempt to close the gap. - -== Bot requirement - -Agents operating in this repository must treat this document as a key root audit -gate. In particular they must not: create or edit `LICENSE`; add SPDX or -copyright headers; add GitHub Actions workflows or CI badges; rename -`readme.adoc` or `explainme.adoc`; or make release/readiness claims that -conflict with the tier statement above. - -== Proof-trust verification (2026-06-16) - -An out-of-band ground-truth audit (cold typecheck + flag probes, not doc-trust) -was run before an external project built on these proofs. It *affirms* the -honesty claims above; it makes no Bronze/release claim and changes no source. - -* *Build (ground truth).* `agda --no-libraries -i src src/EpistemicTypes/All.agda` - exits 0; re-run with `-W error` (promotes unsolved metas / constraints / - termination issues to errors) *still* exits 0. All 10 modules carry - `{-# OPTIONS --safe --without-K #-}`; the repo is stdlib-free (only - `Agda.Primitive` / `Agda.Builtin.*`), so the estate's dangling-stdlib gotcha - does not apply here. -* *`--safe` is genuinely enforced* — proven by an honesty probe: injecting - `postulate evil : {A : Set} → A` into a copy of `Base.agda` is *rejected* - (`[SafeFlagPostulate]`, exit 42). So the clean build is a real verification, - not a no-op flag. -* *Zero escape hatches* — `postulate` / `sorry` / hole / `TERMINATING` / - `trustMe` / `axiom` count is 0 in every file (including comments); zero - orphan modules (all 10 in the checked import graph). -* *Named results are real proofs* (not blanks/postulates): - `ReadConsistency.freshnessPropagatesUnderWrites` / `resyncRecoversFresh` / - `syncChainEndsFresh`; `Warrant.sound-epi` (non-factive by construction — - no `Evidence → A` field); `ProofTransport.{proofNeedsChecker, - designatedBindsHolder, opaqueNotCertifying, verifyReceiptIsGap}` (no - checker-free `Proof → Proof` transport is exported); the `Access` preorder + - monotone-transport laws, instantiated for real in `Examples` / - `ReadConsistency`. -* *Honest caveat for downstream builders.* `EchoBridge.agda` is a deliberate - *scaffold* — real tropical-grade plumbing (`gradeMin`/`gradePlus`, `Echo`, - `EpistemicEcho`) but *no proven graded-loss theorems*; those live partially - in `SurrealBridge` (day-loss). This is a ~736-line specification lens, a - sound seed rather than a complete logic. - -*Verdict: trustworthy — GO* as the epistemic specification lens. The -LLM-fraud concern that motivated the audit did not materialise. +Model meanings and assumptions still require review. External store correspondence, +concurrent runtime behavior, bounded memory, actual output authority and physical +properties are separate obligations. The detector contract developed in Firmboot +uses these foundations but does not confer those guarantees on this library. diff --git a/CHANGELOG.adoc b/CHANGELOG.adoc index b175c01..abc31dc 100644 --- a/CHANGELOG.adoc +++ b/CHANGELOG.adoc @@ -6,58 +6,85 @@ The format is based on https://keepachangelog.com/en/1.1.0/[Keep a Changelog], and this project adheres to https://semver.org/spec/v2.0.0.html[Semantic Versioning]. -Dates are ISO 8601 (`+YYYY-MM-DD+`). This is a small, deliberately -honest Agda formalization that favours mathematical honesty over a large -API; the changelog records what is actually proved, not what is aspired -to. +Dates are ISO 8601 (`YYYY-MM-DD`). This is a small, deliberately honest +Agda formalization that favours mathematical honesty over a large API; +the changelog records what is actually proved, not what is aspired to. === https://github.com/hyperpolymath/epistemic-types/compare/v0.1.0...HEAD[Unreleased] +[[fixed--2026-09-07]] +==== Fixed — 2026-09-07 + +* Replaced version-only read relabelling with store histories, coherent +views, stale-cache proofs, actual model reads, and explicit evidence +stability. +* Replaced unconstrained `Echo r A` with certified `Echo C y`, explicit +source provenance, recovery and migration obligations, and a general +collision-based impossibility proof. Resource budgets now require +measure inequalities. +* Removed arbitrary surreal Echo retagging; its concrete instance now +weakens a proved bound while preserving retained data. +* Added `ContinuityExamples`, seven additional semantic rejection +controls, and optional round-trip/lowering correspondence with canonical +Echo sources. These are breaking research APIs; see +`docs/continuity-foundations.adoc`. +* Closed the token-only proof-transport soundness gap: every `Proof` +status now entails a supplied `Meaning holder artifact claim` via +`proofSound`. +* Breaking API: `Meaning` and `Payload` module parameters; executable +sound certificate checks; payload-carrying evidence; accepted-check +witnesses; explicit meaning transport for public checker portability. +* `verify` rejects invalid certificates. Boolean acceptance/rejection +examples replace the earlier ungrounded `ActionWasPerformed` scenario. +* `just check` includes four deliberate type-error regression controls. +* Historical transport claims below describe the earlier prototype; +checker and evidence tokens alone did not establish semantic truth. + ==== Added -* `+EpistemicTypes.ProofTransport+`: standpoint-indexed proof transport +* `EpistemicTypes.ProofTransport`: standpoint-indexed proof transport across trust boundaries. -** `+View : Agent -> Artifact -> Status -> Claim -> Set+`, with statuses -`+Data+` / `+Code+` / `+Claimed+` / `+Receipt+` / `+Proof+` / -`+ProofUnder+`. -** Transport modes `+Public+` / `+Designated+` / `+IssuerMediated+` / -`+EnvironmentMediated+` / `+OpaqueReceipt+`. -** `+transmit+` downgrades a sender’s `+Proof+` to a receiver’s -`+Receipt+`; `+verify+` upgrades `+Data -> Proof+` only with the -receiver’s OWN checker and evidence. Public views are portable, -designated views are receiver-bound, and receipt-only views never -certify. -** `+proofNeedsChecker+`: the structural no-smuggling guarantee. -* `+EpistemicTypes.ProofTransportExample+`: a worked K9-SVC / A2ML -attestation scenario — issuer `+K9SVC+`, receiver `+Alice+`, third party -`+Bob+`, claim `+ActionWasPerformed+`, artifact `+AttestationBlob+` — +** `View : Agent -++>++ Artifact -++>++ Status -++>++ Claim -++>++ Set`, +with statuses `Data` / `Code` / `Claimed` / `Receipt` / `Proof` / +`ProofUnder`. +** Transport modes `Public` / `Designated` / `IssuerMediated` / +`EnvironmentMediated` / `OpaqueReceipt`. +** `transmit` downgrades a sender's `Proof` to a receiver's `Receipt`; +`verify` upgrades `Data -++>++ Proof` only with the receiver's OWN +checker and evidence. Public views are portable, designated views are +receiver-bound, and receipt-only views never certify. +** `proofNeedsChecker`: the structural no-smuggling guarantee. +* `EpistemicTypes.ProofTransportExample`: a worked K9-SVC / A2ML +attestation scenario — issuer `K9SVC`, receiver `Alice`, third party +`Bob`, claim `ActionWasPerformed`, artifact `AttestationBlob` — exercising transmit, receipt non-certification, and receiver-local verification. -* Engineering rendering of proof transport for `+a2ml+` / `+k9+` -consumers under `+.machine_readable/proof-transport/+` -(`+ProofTransport.a2ml+`, `+proof-transport.k9.ncl+`, `+README.adoc+`), -targeting the estate `+a2ml+` + `+k9+` contractile tooling. -* `+EpistemicTypes.SurrealBridge+`: graded upgrade of surreal-numbered +* Engineering rendering of proof transport for `a2ml` / `k9` consumers +under `.machine++_++readable/proof-transport/` (`ProofTransport.a2ml`, +`proof-transport.k9.ncl`, `README.adoc`), targeting the estate `a2ml` +{plus} `k9` contractile tooling. +* `EpistemicTypes.SurrealBridge`: graded upgrade of surreal-numbered access. -** `+SurrealAccess+` carrier and `+GradedSurrealModality+`. -** `+daySurrealAccess+`, a finite birthday-tower account of standpoint +** `SurrealAccess` carrier and `GradedSurrealModality`. +** `daySurrealAccess`, a finite birthday-tower account of standpoint access. ==== Changed -* `+EpistemicTypes.All+` re-export aggregator extended to include -`+ProofTransport+`, `+ProofTransportExample+`, and the upgraded -`+SurrealBridge+`. -* RSR-compliance and documentation pass: machine-readable `+6a2+` -descriptors (`+0-AI-MANIFEST.a2ml+`, `+STATE.a2ml+`) and AsciiDoc docs -(`+readme.adoc+`, `+explainme.adoc+`) brought into line with the current +* `EpistemicTypes.All` re-export aggregator extended to include +`ProofTransport`, `ProofTransportExample`, and the upgraded +`SurrealBridge`. +* RSR-compliance and documentation pass: machine-readable `descriptiles` +descriptors (`0-AI-MANIFEST.a2ml`, `STATE.a2ml`) and AsciiDoc docs +(`readme.adoc`, `explainme.adoc`) brought into line with the current module set. Existing lowercase doc filenames are preserved deliberately. ==== Notes * Continuous integration is not enabled for this repository (see -`+AUDIT.adoc+`). Verification is local-only via `+just check+`. +`AUDIT.adoc`). Verification is local-only via `just check`. +[[010---2026-06-15]] === https://github.com/hyperpolymath/epistemic-types/releases/tag/v0.1.0[0.1.0] - 2026-06-15 Prototype baseline: the first honest formalization of standpoint-indexed @@ -65,32 +92,30 @@ modal / epistemic / echo-like type formers. ==== Added -* `+EpistemicTypes.Base+`: the core interface. -`+E : K -> Set ℓ -> Set ℓ+`, where `+E κ A+` reads "``+A+` is -epistemically available at standpoint `+κ+``". This is a plain indexed -endofunctor (`+map+` only) — deliberately NOT a monad or comonad, with -no generic `+return+` / `+reflect+`. Provides `+Modality+`, -`+LawfulModality+`, `+FactiveModality+`, `+BeliefModality+`, and -`+ReturnModality+`. -* `+EpistemicTypes.Warrant+`: `+Warrant+`, `+Epi+`, and -`+SoundWarrant+`. -* `+EpistemicTypes.Access+`: a `+Preorder+` on standpoints and an -`+AccessibleModality+` whose `+increase+` transports availability along -the preorder. -* `+EpistemicTypes.EchoBridge+`: min-plus graded loss / residue -`+Echo r A+`, kept deliberately distinct from `+E κ A+`. Composes with -the sibling `+echo-types+` loss-with-residue formalism. -* `+EpistemicTypes.SurrealBridge+`: initial `+SurrealAccess+` carrier -and graded surreal modality. -* `+EpistemicTypes.Examples+`: small worked instances of the above. -* `+EpistemicTypes.All+`: re-export aggregator over the public modules. -* Build tooling: a `+Justfile+` with `+just check+`, defined as -`+agda --no-libraries -i src src/EpistemicTypes/All.agda+` (Agda 2.8.0), -plus the `+epistemic-types.agda-lib+` library descriptor. +* `EpistemicTypes.Base`: the core interface. +`E : K -++>++ Set ℓ -++>++ Set ℓ`, where `E κ A` reads "`A` is +epistemically available at standpoint `κ`". This is a plain indexed +endofunctor (`map` only) — deliberately NOT a monad or comonad, with no +generic `return` / `reflect`. Provides `Modality`, `LawfulModality`, +`FactiveModality`, `BeliefModality`, and `ReturnModality`. +* `EpistemicTypes.Warrant`: `Warrant`, `Epi`, and `SoundWarrant`. +* `EpistemicTypes.Access`: a `Preorder` on standpoints and an +`AccessibleModality` whose `increase` transports availability along the +preorder. +* `EpistemicTypes.EchoBridge`: min-plus graded loss / residue +`Echo r A`, kept deliberately distinct from `E κ A`. Composes with the +sibling `echo-types` loss-with-residue formalism. +* `EpistemicTypes.SurrealBridge`: initial `SurrealAccess` carrier and +graded surreal modality. +* `EpistemicTypes.Examples`: small worked instances of the above. +* `EpistemicTypes.All`: re-export aggregator over the public modules. +* Build tooling: a `Justfile` with `just check`, defined as +`agda --no-libraries -i src src/EpistemicTypes/All.agda` (Agda 2.8.0), +plus the `epistemic-types.agda-lib` library descriptor. ==== Project conventions -* Compiles under `+{-# OPTIONS --safe --without-K #-}+`. +* Compiles under `++{++-++#++ OPTIONS --safe --without-K ++#++-}`. * No postulates. -* No Agda standard library: built with `+agda --no-libraries+`, using -only `+Agda.Builtin.*+` and `+Agda.Primitive+`. +* No Agda standard library: built with `agda --no-libraries`, using only +`Agda.Builtin.++*++` and `Agda.Primitive`. diff --git a/CONTRIBUTING.adoc b/CONTRIBUTING.adoc index 2c1e934..d7b0a4c 100644 --- a/CONTRIBUTING.adoc +++ b/CONTRIBUTING.adoc @@ -1,10 +1,10 @@ == Contributing to epistemic-types -`+epistemic-types+` is a small, deliberately honest Agda formalization -of standpoint-indexed modal / epistemic / echo-like type formers. It +`epistemic-types` is a small, deliberately honest Agda formalization of +standpoint-indexed modal / epistemic / echo-like type formers. It favours mathematical honesty over a large API. Contributions are welcome, but the bar is *everything still type-checks under -`+--safe --without-K+`, with no shortcuts*. +`--safe --without-K`, with no shortcuts*. * *Author:* Jonathan D.A. Jewell (hyperpolymath) j.d.a.jewell@open.ac.uk * *Version:* 0.1.0 (status: prototype) @@ -12,58 +12,58 @@ welcome, but the bar is *everything still type-checks under ''''' +[[contribution-model--tri-perimeter-contribution-framework-tpcf]] === Contribution model — Tri-Perimeter Contribution Framework (TPCF) epistemic-types follows the estate-wide *Tri-Perimeter Contribution Framework (TPCF)* — graduated trust without gatekeeping: * *Perimeter 1 — Core Systems (maintainers only).* The proof kernel: -`+src/EpistemicTypes/*.agda+` (Base, Access, Warrant, ProofTransport, -the EchoBridge/SurrealBridge), the `+All.agda+` wiring, and build -tooling. +`src/EpistemicTypes/++*++.agda` (Base, Access, Warrant, ProofTransport, +the EchoBridge/SurrealBridge), the `All.agda` wiring, and build tooling. * *Perimeter 2 — Expert Extensions (trusted contributors).* New epistemic/standpoint modules, examples, and bridges. Apply via issue → -review → merge, with `+just check+` green. -* *Perimeter 3 — Community Sandbox (open to all).* Docs (`+.adoc+`), -`+.well-known/+`, AI manifests, spec proposals. +review → merge, with `just check` green. +* *Perimeter 3 — Community Sandbox (open to all).* Docs (`.adoc`), +`.well-known/`, AI manifests, spec proposals. ==== Fork workflow External contributors use the standard *fork*-and-pull-request workflow: -fork the repository, branch from `+main+`, run `+just check+` (the full -`+--safe --without-K+` type-check) locally, and open a PR. Proofs are -load-bearing — a red `+agda+` check blocks merge, and no `+postulate+` / -`+believe_me+` shortcuts are accepted. +fork the repository, branch from `main`, run `just check` (the full +`--safe --without-K` type-check) locally, and open a PR. Proofs are +load-bearing — a red `agda` check blocks merge, and no `postulate` / +`believe++_++me` shortcuts are accepted. === Build and check -There is exactly one thing to run, and it must stay green: +The combined proof and rejection gate must stay green: .... just check .... -which is: - -.... -agda --no-libraries -i src src/EpistemicTypes/All.agda -.... +This checks every source module (including `All.agda`) and runs +`tests/check-rejections.sh`. Deliberate rejection fixtures stay outside +the positive `All.agda` import graph. Requirements: -* *Agda 2.8.0*. -* *No Agda standard library.* The build runs with `+--no-libraries+`; -the only imports allowed are from `+Agda.Builtin.*+` and -`+Agda.Primitive+`. Do not add a dependency on `+agda-stdlib+` or any -other library. +* *Agda 2.6.4.3*. +* *No Agda standard library.* The build runs with `--no-libraries`; the +only external core imports allowed are from `Agda.Builtin.++*++` and +`Agda.Primitive`. The optional `tests/integration/CanonicalEcho.agda` +checks correspondence with actual sibling sources through +`just check-canonical`; its dependencies stay outside the default core +gate. -`+All.agda+` re-exports every module, so `+just check+` checks the whole -library. A change is not done until `+just check+` passes with no errors +`All.agda` imports every core module, so `just check` checks the whole +library. A change is not done until `just check` passes with no errors and no warnings. -There is no CI (see `+AUDIT.adoc+` / repo notes — CI is not enabled). -The type-checker run above is the gate. Run it locally before opening a -PR. +CI checks every source module, semantic rejection controls and pinned canonical +Echo correspondence. Proof and security gates must pass before merge; see +link:docs/ci-safety.adoc[]. Run the local checks before opening a PR. ''''' @@ -72,83 +72,86 @@ PR. These are non-negotiable. A PR that breaks any of them will not be merged. -* *No `+postulate+`.* Nothing is asserted without proof. If a law holds, +* *No `postulate`.* Nothing is asserted without proof. If a law holds, prove it; if it does not, it is not stated as if it did. Where a law is not derivable but is needed, it appears as an explicit _field_ the -caller must supply (see `+LawfulModality+`, `+FactiveModality+`, -`+BeliefModality+`), so the assumption is visible at the type level -rather than smuggled in. -* *No standard library.* As above: `+Agda.Builtin.*+` and -`+Agda.Primitive+` only. -* *`+--safe --without-K+`.* Every module compiles under -`+{-# OPTIONS --safe --without-K #-}+`. This rules out `+postulate+`, -unsafe pragmas, axiom K, and `+--type-in-type+`. Do not weaken these -options. +caller must supply (see `LawfulModality`, `FactiveModality`, +`BeliefModality`), so the assumption is visible at the type level rather +than smuggled in. +* *No standard library.* As above: `Agda.Builtin.++*++` and +`Agda.Primitive` only. +* *`--safe --without-K`.* Every module compiles under +`++{++-++#++ OPTIONS --safe --without-K ++#++-}`. This rules out +`postulate`, unsafe pragmas, axiom K, and `--type-in-type`. Do not +weaken these options. * *No too-strong rules.* Keep the interfaces as weak as the proofs -allow. The base form `+E : K → Set ℓ → Set ℓ+` is a plain indexed -endofunctor (`+map+` only) — it is *not* a monad or comonad, and there -is no generic `+return+`/`+reflect+`. Do not promote it to one. If -something needs more structure, add a _named_ stronger interface -(e.g. `+ReturnModality+`) that callers opt into, and keep the base -interface untouched. +allow. The base form `E : K → Set ℓ → Set ℓ` is a plain indexed +endofunctor (`map` only) — it is *not* a monad or comonad, and there is +no generic `return`/`reflect`. Do not promote it to one. If something +needs more structure, add a _named_ stronger interface (e.g. +`ReturnModality`) that callers opt into, and keep the base interface +untouched. * *Add lemmas with proofs, not admits.* New results land as complete -proofs closed with normal Agda terms. No holes (`+?+`), no admit-shaped -escapes, no `+TERMINATING+`/`+NON_COVERING+` pragmas to paper over gaps. +proofs closed with normal Agda terms. No holes (`?`), no admit-shaped +escapes, no `TERMINATING`/`NON++_++COVERING` pragmas to paper over gaps. ==== Keep the bridges distinct The library is careful about what is and is not the same thing. Preserve these separations when extending: -* `+Echo r A+` (the min-plus graded loss/residue in `+EchoBridge+`) is -*not* `+E κ A+`. Keep the echo bridge separate; do not collapse it into -the modality, and do not import a full graded comonad to get it. -* In `+ProofTransport+`, the no-smuggling discipline is the point: -`+transmit+` downgrades a sender’s `+Proof+` to a receiver’s -`+Receipt+`; `+verify+` upgrades `+Data → Proof+` only with the -receiver’s *own* checker and evidence; public proofs are portable, -designated ones are receiver-bound, and a receipt alone never certifies -(`+proofNeedsChecker+`). Any new transport rule must respect these — no -rule that lets one agent’s `+Proof+` become another’s without the -receiver’s own checker. +* `Echo C y` carries a specified residue certificate. `MatchesSource` is +compatibility, not unique historical provenance. `BoundedEcho` measures +a residue separately; it is not a retention index or an epistemic +standpoint. +* A `ReadView s` must entail its contents equality. Writes must not +silently refresh cached values; evidence transport needs its stability +proof. +* In `ProofTransport`, every proof status must entail its explicit +`Meaning` via `proofSound`. Preserve the successful-check witness and +the verifier's soundness obligation. Public transport needs an explicit +implication between holder meanings; evidence tokens alone never +suffice. `just check` must pass both the positive library and the +deliberate type-error regression controls. ''''' === Adding a module or lemma [arabic] -. Put Agda source under `+src/EpistemicTypes/+` and add the new module -to the `+import+`/re-export list in `+src/EpistemicTypes/All.agda+` so -`+just check+` covers it. -. Open each module with `+{-# OPTIONS --safe --without-K #-}+`. +. Put Agda source under `src/EpistemicTypes/` and add the new module to +the `import`/re-export list in `src/EpistemicTypes/All.agda` so +`just check` covers it. +. Open each module with +`++{++-++#++ OPTIONS --safe --without-K ++#++-}`. . Keep modules small and single-purpose, mirroring the existing layout: -`+Base+`, `+Warrant+`, `+Access+`, `+EchoBridge+`, `+SurrealBridge+`, -`+ProofTransport+`, `+ProofTransportExample+`, `+Examples+`. +`Base`, `Warrant`, `Access`, `EchoBridge`, `SurrealBridge`, +`ProofTransport`, `ProofTransportExample`, `Examples`. . State assumptions as interface fields, not postulates. Add lawful instances only after the laws are proved or explicitly required as fields. -. Run `+just check+`. +. Run `just check`. If a change touches the ProofTransport engineering rendering (the a2ml/k9 attestation target under -`+.machine_readable/proof-transport/+`), keep the Agda model and the +`.machine++_++readable/proof-transport/`), keep the Agda model and the machine-readable description in step. ''''' === Documentation -* *AsciiDoc (`+.adoc+`) is the default* for documentation. Update the -relevant `+.adoc+` file alongside any behavioural or interface change. -* Existing docs keep their current lowercase names: `+readme.adoc+` and -`+explainme.adoc+`. Do *not* rename or duplicate them. -* Machine-readable descriptions live under `+.machine_readable/+` (a2ml -+ Nickel/k9). a2ml files use the canonical TOML-like dialect: -`+[section]+` headers, `+key = "value"+`, arrays `+[ "a", "b" ]+`, -inline tables `+{ k = "v", j = "w" }+`. +* *AsciiDoc (`.adoc`) is the default* for documentation. Update the +relevant `.adoc` file alongside any behavioural or interface change. +* Existing docs keep their current lowercase names: `readme.adoc` and +`explainme.adoc`. Do *not* rename or duplicate them. +* Machine-readable descriptions live under `.machine++_++readable/` +(a2ml {plus} Nickel/k9). a2ml files use the canonical TOML-like dialect: +`++[++section++]++` headers, `key = "value"`, arrays +`++[++ "a", "b" ++]++`, inline tables `++{++ k = "v", j = "w" }`. * Only these files may be Markdown (GitHub community-health -special-casing): `+CONTRIBUTING.md+`, `+CODE_OF_CONDUCT.md+`, -`+SECURITY.md+`, `+CHANGELOG.md+`. Everything else is `+.adoc+`. +special-casing): `CONTRIBUTING.adoc`, `CODE++_++OF++_++CONDUCT.md`, +`SECURITY.md`, `CHANGELOG.adoc`. Everything else is `.adoc`. ''''' @@ -176,8 +179,8 @@ Commits]: [optional footer] .... -Typical scopes match the modules: `+base+`, `+warrant+`, `+access+`, -`+echo+`, `+surreal+`, `+proof-transport+`, `+docs+`. +Typical scopes match the modules: `base`, `warrant`, `access`, `echo`, +`surreal`, `proof-transport`, `docs`. ==== Signed commits @@ -193,12 +196,12 @@ Unsigned commits will be asked to be re-signed before merge. ==== Before you open a PR [arabic] -. `+just check+` passes — no errors, no warnings. -. No `+postulate+`, no library imports, no `+?+`/admits, no weakened +. `just check` passes — no errors, no warnings. +. No `postulate`, no library imports, no `?`/admits, no weakened pragmas. . The honesty rules above still hold (weak base interface, distinct bridges, no proof-smuggling in transport). -. Relevant `+.adoc+` and `+.machine_readable/+` files updated. +. Relevant `.adoc` and `.machine++_++readable/` files updated. . Commits are conventional and signed. Keep PRs small and focused — one idea, one proof obligation, easy to @@ -208,8 +211,8 @@ check. === Licence note -The licence is owner-managed. Do *not* add `+LICENSE+`, -`+SPDX-License-Identifier+` headers, or copyright header lines in a PR. +The licence is owner-managed. Do *not* add `LICENSE`, +`SPDX-License-Identifier` headers, or copyright header lines in a PR. The repo is currently SPDX-free and stays consistent; licensing is handled separately by the owner. @@ -217,16 +220,16 @@ handled separately by the owner. === Ecosystem siblings -`+epistemic-types+` sits alongside (and should stay coherent with) these +`epistemic-types` sits alongside (and should stay coherent with) these estate repos: -* *echo-types* — Agda loss-with-residue formalism; `+EchoBridge+` -composes with it. Audit it before duplicating echo machinery here. +* *echo-types* — Agda loss-with-residue formalism; `EchoBridge` composes +with it. Audit it before duplicating echo machinery here. * *ephapax* — sibling formal language (four-layer redesign with echo obligations). * *standards* — estate RSR/standards, k9-svc, and a2ml tooling. -* *a2ml / k9* — machine-readable + contractile tooling; the engineering -target for `+ProofTransport+`. +* *a2ml / k9* — machine-readable {plus} contractile tooling; the +engineering target for `ProofTransport`. When a contribution overlaps a sibling (especially echo-types), prefer reusing or extending it upstream over re-deriving it locally. diff --git a/EXPLAINME.adoc b/EXPLAINME.adoc index aaa1494..62041ec 100644 --- a/EXPLAINME.adoc +++ b/EXPLAINME.adoc @@ -48,31 +48,48 @@ How this is implemented:: Caveat:: This is a standard Kripke-style accessibility relation, repackaged as an explicit record. The laws are assumed (fields), not derived. This is honest — the prototype does not constrain the accessibility relation beyond preorder. -=== Surreal bridge adds tropical-graded access loss +=== Store views, residues, and resource bounds -[quote, README.adoc] -____ -SurrealBridge enriches the preorder: each access step carries a tropical grade measuring the information loss or refinement cost of the access. -____ +`ReadConsistency.agda` uses finite store histories. Every read view proves its +value agrees with its indexed history; cached reads additionally prove ancestry. +Writes preserve the old sample and make it stale. Synchronization obtains the +current contents in the model. Evidence survives changes only through an +explicit stability proof. These results do not establish an external scheduler +or shared-memory implementation. -How this is implemented:: -`link:src/EpistemicTypes/SurrealBridge.agda[]` defines `SurrealAccess` record with `magnitude-loss : x ≤♯ y → Grade`, plus `loss-refl` and `loss-trans` laws. Defines `GradedSurrealModality` showing transport degrades echo grades: `E x (Echo r A) → E y (Echo (gradePlus r (magnitude-loss p)) A)`. Concrete instance: `daySurrealAccess` using `Nat` standpoints where grade = birthday steps. +`EchoBridge.agda` replaces the unconstrained residue token with `Echo C y`, whose +certificate means `Retention.Cert C residue y`. `MatchesSource` establishes +compatibility with a candidate source, not unique historical origin. Recovery +and migration require their own laws. The examples prove useful migration of a +retained component and refute every adequate migration of a discarded component. -Caveat:: -**This is not the Conway proper class of surreals.** It is a set-sized fragment (finite birthday tower) where the access grade does type-level work. The module name `SurrealBridge` may overclaim; `DayBoundedTropicalBridge` would be more precise. The composition with Echo types is a bridge scaffold — it imports the Echo grade structure but does not depend on the full echo-types library. +`BoundedEcho C measure budget y` keeps resource bounds separate from retention. +The concrete surreal adapter weakens a proved upper bound and preserves the +data; it no longer changes an unconstrained grade label. `daySurrealAccess` +remains a finite-day example, with no full Conway-surreal or physical-cost claim. -=== Proof transport has a no-smuggling guarantee +`tests/integration/CanonicalEcho.agda` imports the actual sibling sources and +proves representation round trips and lowering agreement. This optional gate +uses the standard library; the core continues to use builtins only. See +link:docs/continuity-foundations.adoc[] for assumptions and reproduction. -[quote, README.adoc] -____ -The no-smuggling property (proofNeedsChecker) states: every proof a holder possesses carries that holder's own checker and evidence. No checker-free View sender a Proof c → View receiver a Proof c is exported. -____ +=== Proof transport entails an explicit claim meaning How this is implemented:: -`link:src/EpistemicTypes/ProofTransport.agda[]` defines `View`, `transmit`, `verify`, and proves `proofNeedsChecker`, `publicIsPortable`, `designatedBindsHolder`, `opaqueNotCertifying`, `verifyReceiptIsGap`. `link:src/EpistemicTypes/ProofTransportExample.agda[]` works the K9-SVC/A2ML-style attestation flow (issuer K9SVC, receiver Alice, third party Bob). +`src/EpistemicTypes/ProofTransport.agda` takes `Meaning` and `Payload`. +`CertificateCheck` provides an executable check plus acceptance soundness. +`asProofUnder` requires the check to return true. `proofSound` derives the +exact holder/artefact/claim meaning, and `proofCannotSupportFalse` excludes +proof status for a refuted meaning. Public portability requires a supplied +implication between the holders' meanings. Caveat:: -This formalises the *typing* of attestation, not the cryptographic implementation. `transmit` moves bytes; `verify` calls a checker. The no-smuggling property is a structural consequence of the `View` typing discipline, not a cryptographic hardness assumption. The A2ML/K9 rendering in `.machine_readable/proof-transport/` is an engineering shadow, not a proof. +The former token-only model did not justify semantic soundness. +`proofNeedsChecker` alone was only a structural statement. The new Boolean +examples and deliberate rejection controls test both acceptance and false +claims. The theorem remains relative to the specified meaning and checker +proof; it does not establish cryptography or physical facts. See +link:docs/proof-transport.adoc[]. == Dogfooded Across The Account @@ -82,7 +99,7 @@ This formalises the *typing* of attestation, not the cryptographic implementatio | Standpoint-indexed modality | Core `E κ A` interface -| link:https://github.com/hyperpolymath/echo-types[echo-types] (as `Echo r A`) +| link:https://github.com/hyperpolymath/echo-types[echo-types] (distinct residue formalism) | Proof transport / no-smuggling | `ProofTransport.agda` @@ -112,12 +129,12 @@ This formalises the *typing* of attestation, not the cryptographic implementatio [CAUTION] ==== -**Access laws are assumed, not derived.** `EpistemicTypes.Access` takes preorder and transport laws as fields. This is honest (arbitrary standpoints don't determine them) but means the prototype lacks concrete derived models validating these laws from first principles. +**Access laws are assumed, not derived.** `EpistemicTypes.Access` takes preorder and transport laws as fields. This is honest (arbitrary standpoints don't determine them) and the laws must be supplied for each instance; the repository includes small concrete instances. ==== [CAUTION] ==== -**Echo-type bridge is a scaffold.** The composition `E κ (Echo r A)` imports grade structure but does not depend on the full echo-types library. Deep integration (e.g., shared comonadic structure) is deferred. +**Combined semantics remain open.** The residue correspondence is checked, but a combined Firmboot calculus, external-store correspondence, scheduler bounds, and runtime refinement are not established. ==== == Evidence Index @@ -136,11 +153,11 @@ This formalises the *typing* of attestation, not the cryptographic implementatio | Preorder accessibility + transport | `src/EpistemicTypes/SurrealBridge.agda` -| Tropical-graded access loss + GradedSurrealModality + daySurrealAccess +| Resource-bound weakening + GradedSurrealModality + finite daySurrealAccess | `src/EpistemicTypes/ProofTransport.agda` -| View / transmit / verify + no-smuggling + opacity laws +| View / transmit / verify + semantic soundness + opacity laws | `src/EpistemicTypes/ProofTransportExample.agda` -| K9-SVC/A2ML-style attestation worked example +| Sound Boolean verification, false-claim rejection, and holder-boundary counterexample |=== diff --git a/Justfile b/Justfile index 746589d..ac8c924 100644 --- a/Justfile +++ b/Justfile @@ -1,8 +1,16 @@ -check: - agda --no-libraries -i src src/EpistemicTypes/All.agda +check: check-proofs check-rejections -# build / test / validate all reduce to the single proof check: the library's -# correctness IS that All.agda type-checks under --safe --without-K. +check-proofs: + bash tests/check-proofs.sh + +check-rejections: + bash tests/check-rejections.sh + +# Optional integration gate: actual echo-types checkout and stdlib source. +check-canonical echo_root stdlib_src: + agda --no-libraries --safe --without-K --double-check --ignore-interfaces -W error -W noUnsupportedIndexedMatch -i src -i tests/integration -i '{{echo_root}}/proofs/agda' -i '{{stdlib_src}}' tests/integration/CanonicalEcho.agda + +# Build/test/validate include positive proofs and semantic rejection controls. build: check test: check validate: check diff --git a/PROOF-STATUS.adoc b/PROOF-STATUS.adoc index cc293da..89837ee 100644 --- a/PROOF-STATUS.adoc +++ b/PROOF-STATUS.adoc @@ -8,7 +8,44 @@ Verification status of the epistemic-types Agda formalisation. The whole library self-contained (`--no-libraries`: it imports only `Agda.Builtin.*` / `Agda.Primitive`). This records a reproduced `agda` run, not a "looks fine" reading. -== Verified (this environment) +== Current continuity-foundations correction — 2026-09-07 + +`ReadView` now entails equality with the indexed store contents. Cached-read +freshness is tied to a particular store history; every write invalidates old +freshness, and synchronization reads current contents in the model. + +`Echo` now carries a specified residue certificate. Source compatibility, recovery, +and migration have explicit obligations. The collision theorem refutes every +migration requiring a distinction discarded by the retained pair. Resource +bounds require measure inequalities; arbitrary grade retagging is removed. + +The eleven-module core and eleven deliberate rejection fixtures pass with +Agda 2.6.4.3 under `--safe --without-K --no-libraries`, without warnings. +The additional canonical Echo integration proves both representation round +trips and agreement of lowering; its standard-library dependencies emit Cubical +compatibility warnings. See link:docs/continuity-foundations.adoc[] for commands, +scope, and remaining runtime and combined-language obligations. + +== Earlier semantic proof-transport correction — 2026-09-07 + +The token-only proof-status construction has been replaced. `proofSound` +derives an explicit `Meaning holder artifact claim` from every proof status. +The verifier supplies a Boolean check and a proof of acceptance soundness; +proof construction requires its successful-check equality. No global soundness +axiom is added. + +Reproduced with Agda 2.6.4.3: `just check` passes the full 10-module library +and four semantic rejection controls. Examples prove legitimate acceptance +and rejection of bad payloads, altered artefacts, false claims, opaque modes, +and missing checking resources. Holder-dependent transfer is explicitly +qualified. The older `proofNeedsChecker` theorem remains a weaker structural +projection; its former semantic interpretation was unsupported. + +At that stage ReadConsistency/store coherence and EchoBridge/index constraints +were still open; the later correction above addresses their model-level gaps. +External-store and runtime correspondence remain open. + +== Earlier reproduced baseline * Command: `agda --safe -i src src/EpistemicTypes/All.agda` → **exit 0**. * All **10/10** modules declare `{-# OPTIONS --safe #-}`; **zero `postulate`**, @@ -32,9 +69,9 @@ agda --safe -i src src/EpistemicTypes/All.agda * Status: **prototype (v0.1.0)** — a deliberately small, honest formalisation of standpoint-indexed modal / epistemic / echo-like type formers. -* `EchoBridge` and `SurrealBridge` are **local re-implementations** of the - `Echo`/`Grade` and surreal shapes (no dependency on the `echo-types` Agda - library or a surreal-number library); the relationship is at the design level. +* `EchoBridge` and `SurrealBridge` remain self-contained. The optional integration + test imports canonical Echo sources and proves a residue correspondence; no + full surreal-number library or combined-runtime verification is claimed. * The library is self-contained by design (`--no-libraries`); it does not depend on the standard library. diff --git a/README.adoc b/README.adoc index 1969c40..8622ad3 100644 --- a/README.adoc +++ b/README.adoc @@ -7,11 +7,11 @@ image:https://img.shields.io/badge/OpenSSF-BestPractices-green[link="https://www.bestpractices.dev/projects/XXXX"] -Constructive Agda prototype for standpoint-indexed epistemic modalities, separating knowledge, belief, and warrant, and formalising proof transport across trust boundaries with a no-smuggling guarantee. +Constructive Agda prototype for standpoint-indexed epistemic modalities, separating knowledge, belief, and warrant, with proof transport sound relative to an explicit claim meaning. == Overview -When an agent observes a fact, the type of their access matters. Knowledge is factive; belief is not. A warrant records evidence without assuming soundness. Proof transported across a boundary becomes a receipt until the receiver re-verifies it with their own checker. +When an agent observes a fact, the type of their access matters. Knowledge is factive; belief is not. A warrant records evidence without assuming soundness. Proof transported across a boundary becomes a receipt; a receiving proof requires a successful sound check of the receiver's claim meaning. Epistemic types provide a mechanised vocabulary for these distinctions. Given a type of standpoints `K` (agents, observers, evidence states), the modality `E : K → Set ℓ → Set ℓ` reads: `E κ A` is the type of `A` as epistemically available from standpoint `κ`. @@ -64,36 +64,62 @@ Standpoint access is modelled by a preorder `κ ≤κ κ'` (read: `κ'` is at le === The surreal bridge -`SurrealBridge` enriches the preorder: each access step carries a tropical grade measuring the information loss or refinement cost of the access: +`SurrealBridge` enriches the preorder with an instance-supplied access grade. +Its laws specify composition; they do not establish a physical cost or an +information-loss measure: magnitude-loss : x ≤♯ y → Grade loss-refl : magnitude-loss refl ≡ finite zero loss-trans : magnitude-loss (trans p q) ≡ gradePlus (magnitude-loss p) (magnitude-loss q) -This composes with echo types: transporting `E x (Echo r A)` along `p : x ≤♯ y` degrades the echo grade: +Its concrete Echo adapter relaxes a proved upper bound on a residue measure +along `p : x ≤♯ y`, while preserving the retained value: - GradedSurrealModality: E x (Echo r A) → E y (Echo (gradePlus r (magnitude-loss p)) A) + E x (BoundedEcho C measure r visible) + → E y (BoundedEcho C measure (gradePlus r (magnitude-loss p)) visible) The concrete `daySurrealAccess` instance models the finite birthday tower using `Nat` standpoints, where the grade is the number of refinement steps. This is a set-sized fragment, not the full Conway proper class of surreals. -== Proof transport across trust boundaries +== Store-coherent reads and certified residues + +`ReadConsistency` now models finite store histories. A `ReadView s` proves its +value equals `contents s`; a cached read records its source history and ancestry. +Writes make existing caches stale. `synchronize` reads current contents in the +model, while preserving evidence across a change requires an explicit proof. +The former version-only relabelling and free `Sync` witness have been removed. + +`Echo C y` carries a residue satisfying the relation specified by `Retention C`. +Source compatibility is explicit in `MatchesSource`; exact recovery and migration need +their respective round-trip and adequacy laws. A checked counterexample shows +that discarded distinctions cannot support a migration requiring those +distinctions. Resource grades are separate, measured upper bounds. -`ProofTransport` formalises the lifecycle of a proof crossing a boundary. An artefact is read three ways: +See link:docs/continuity-foundations.adoc[the breaking API correction and proof +boundaries]. An optional integration gate proves correspondence with the actual +sibling `EchoResidue.EchoR`; the core remains dependency-free. -* **Data** — von Neumann structure / bytes. -* **Proof** — Curry–Howard witness. -* **Receipt** — attestation of proofhood without the witness itself. +== Proof transport across trust boundaries -Transmission moves bytes, not proofhood: +`ProofTransport` is parameterised by agents, claim labels, artefacts, +`Meaning : Agent -> Artifact -> Claim -> Set`, and a certificate +`Payload : Artifact -> Claim -> Set`. The caller states the meaning being proved. - transmit : (b : Boundary) → View (from b) a Proof c → View (to b) a Receipt c +A `CertificateCheck` contains an executable Boolean check and a proof that +acceptance entails that exact meaning. Evidence carries a payload; possessing +it alone proves nothing. A proof constructor also requires +`runChecker checker evidence ≡ true`. -Proofhood is recovered only by the receiver's own verification: + proofSound : View holder a Proof c -> Meaning holder a c - verify : Checker holder m a c → Evidence m a c → View holder a Data c - → Either Gap (View holder a Proof c) +`verify` evaluates the checking function and returns `InvalidEvidence` on +rejection. `transmit` produces a receipt at the receiving holder. +`publicIsPortable` requires an explicit implication between the two holders' +meanings; it does not silently relabel holder-dependent truths. -The **no-smuggling property** (`proofNeedsChecker`) states: every proof a holder possesses carries that holder's own checker and evidence. No checker-free `View sender a Proof c → View receiver a Proof c` is exported. +The example checks Boolean artefacts and certificates, proves legitimate +acceptance, and refutes false claims. It does not claim that a physical action +occurred. The older token-only model lacked semantic soundness; the strengthened +interface is a breaking correction documented in link:docs/proof-transport.adoc[]. == What is standard and what is ours @@ -117,11 +143,11 @@ The **no-smuggling property** (`proofNeedsChecker`) states: every proof a holder | Standard | `EpistemicTypes.Access` -| Tropical-graded access loss on surreal-like standpoints -| **Novel composition** +| Resource-bound transport on surreal-like standpoints +| Project-specific composition; no novelty theorem | `EpistemicTypes.SurrealBridge` -| Proof transport with no-smuggling guarantee +| Proof transport with explicit semantic soundness | **Novel formalisation** | `EpistemicTypes.ProofTransport` |=== @@ -143,7 +169,7 @@ This is a prototype, not a complete epistemic logic. The following are **intenti [source,bash] ---- -just check +just check # positive proofs and expected rejection controls ---- Or directly: @@ -156,28 +182,9 @@ agda --no-libraries -i src src/EpistemicTypes/All.agda == Documentation * link:EXPLAINME.adoc[EXPLAINME] — claim-by-claim receipts and known gaps -* link:docs/roadmap.adoc[Roadmap] — projected models and structure additions -* link:Glossary.adoc[Glossary] — terminology reference +* link:docs/continuity-foundations.adoc[Continuity foundations] — store coherence, retained information, bounds, and next obligations +* link:docs/proof-transport.adoc[Proof transport] — semantic verification across boundaries == License -SPDX-License-Identifier: MPL-2.0 — see link:LICENSE[LICENSE]. verify : Checker holder m a c → Evidence m a c → View holder a Data c - → Either Gap (View holder a Proof c) - -The **no-smuggling property** (`proofNeedsChecker`) states: every proof a holder possesses carries that holder's own checker and evidence. No checker-free `View sender a Proof c → View receiver a Proof c` is exported. - -== What is standard and what is ours - -[cols="1,2,2", options="header"] -|=== -| Concept | Status | Home in this repo - -| Indexed endofunctor / modality -| Standard -| `EpistemicTypes.Base` - -| Knowledge (factivity) vs. Belief distinction -| Standard (modal logic S5 vs. KD45) -| `EpistemicTypes.Base` - -| Warrant types without assumed soundness +SPDX-License-Identifier: MPL-2.0 — see link:LICENSE[LICENSE]. diff --git a/coordination.k9 b/coordination.k9 index 8da9fc1..ccf63ef 100644 --- a/coordination.k9 +++ b/coordination.k9 @@ -68,7 +68,7 @@ protected_paths: - path: "src/EpistemicTypes/All.agda" role: "re-export aggregator; the check entry point" - path: ".machine_readable/" - role: "a2ml + Nickel/k9 machine-readable surface (6a2/, proof-transport/)" + role: "a2ml + Nickel/k9 machine-readable surface (descriptiles/, proof-transport/)" - path: "Justfile" role: "canonical build recipe" - path: "epistemic-types.agda-lib" @@ -80,7 +80,7 @@ invariants: statement: "The library typechecks: `just check` succeeds." command: "just check" expands_to: "agda --no-libraries -i src src/EpistemicTypes/All.agda" - tool: "Agda 2.8.0" + tool: "Agda 2.6.4.3" - id: "no-postulates" statement: "No postulates. Compiles under {-# OPTIONS --safe --without-K #-}; constructive throughout." - id: "no-stdlib" @@ -90,11 +90,10 @@ invariants: - id: "honesty-over-api" statement: "Favour mathematical honesty over a large API. The base E : K -> Set ℓ -> Set ℓ is a plain indexed endofunctor (map only) — not a monad/comonad; no generic return/reflect. Echo r A is kept distinct from E κ A." -# CI is intentionally absent (estate Actions billing wall; Scorecard known-broken -# estate-wide). Verification is local-only via `just check`. See AUDIT.adoc. +# CI and merge gates are explicitly authorized by the owner (2026-09-07). ci: - enabled: false - note: "No CI; not enabled (see AUDIT.adoc). Verification is local via `just check`." + enabled: true + note: "Proof and security CI are configured; just check remains the local core gate." # Real ecosystem siblings this repo coordinates with. ecosystem: diff --git a/docs/README.adoc b/docs/README.adoc index 6ea1e03..f0cae63 100644 --- a/docs/README.adoc +++ b/docs/README.adoc @@ -14,7 +14,7 @@ authority. |=== | Document | What it covers -| `readme.adoc` (repo root) +| `README.adoc` (repo root) | Project overview: the core form `E : K -> Set ℓ -> Set ℓ`, the module layout, and the `just check` build (`agda --no-libraries -i src src/EpistemicTypes/All.agda`). @@ -30,6 +30,12 @@ authority. public / designated / receipt distinctions. |=== +== Continuity foundations + +link:continuity-foundations.adoc[] documents store-coherent reads, certified +residues, source compatibility, migration sufficiency, resource bounds, and the +optional canonical Echo integration gate. + == Machine-readable specs The `.machine_readable/` tree mirrors the prose for a2ml / Nickel-k9 tooling. @@ -39,7 +45,7 @@ The Agda modules remain authoritative; these files restate them as data. |=== | Path | Role -| `.machine_readable/6a2/` +| `.machine_readable/descriptiles/` | Project-level notes for automated agents: `0-AI-MANIFEST.a2ml`, `STATE.a2ml`, and a short `README.adoc`. @@ -52,15 +58,15 @@ The Agda modules remain authoritative; these files restate them as data. == Source modules (authority) -The library lives in `src/EpistemicTypes/` and re-exports through `All.agda`: -`Base`, `Warrant`, `Access`, `EchoBridge`, `SurrealBridge`, `Examples`, -`ProofTransport`, and `ProofTransportExample`. It is constructive, compiles -under `{-# OPTIONS --safe --without-K #-}`, uses no postulates, and depends on -no Agda standard library — only `Agda.Builtin.*` / `Agda.Primitive` (Agda 2.8.0). +The core lives in `src/EpistemicTypes/`. `All.agda` checks `Base`, `Warrant`, +`Access`, `ReadConsistency`, `EchoBridge`, `SurrealBridge`, `ContinuityExamples`, +`Examples`, `ProofTransport`, and `ProofTransportExample`. Some imports are not +publicly re-exported to avoid helper-name collisions. Every core module uses +`--safe --without-K` and builtins only. Local checks use Agda 2.6.4.3. == Notes -* `EchoBridge` (min-plus graded loss/residue `Echo r A`) is kept deliberately - distinct from `E κ A`; it composes with the sibling `echo-types` formalism. -* Continuous integration is not enabled for this prototype; the build is the - single `just check` invocation. +* `Echo C y`, `BoundedEcho C measure budget y`, and `E κ A` have separate roles. +* `just check` runs the core proof graph and eleven semantic rejection fixtures. +* `just check-canonical` separately checks correspondence against actual sibling + Echo sources; it requires an explicit standard-library source path. diff --git a/docs/ci-safety.adoc b/docs/ci-safety.adoc new file mode 100644 index 0000000..ed51e87 --- /dev/null +++ b/docs/ci-safety.adoc @@ -0,0 +1,62 @@ += Proof and security gates +:revdate: 2026-09-07 + +Changes reach `main` through a pull request after the required checks pass. +The owner explicitly authorized maintaining these CI and merge safeguards on +2026-09-07; the former no-CI policy is superseded. + +== Proof checks + +`Proof core and rejection controls` checks every file under +`src/EpistemicTypes/`, including a file accidentally omitted from `All.agda`. +It uses Agda 2.6.4.3 with `--safe --without-K --double-check +--ignore-interfaces -W error --no-libraries`. It also runs all eleven enumerated +false-claim controls. The rejection runner requires Agda's type-error exit code +and the intended semantic diagnostic; import and environment failures do not pass. + +`Canonical Echo correspondence` imports the actual `echo-types` source pinned to +`46cd1a32d4dcf1020f01dd1aab41f816742da10e`. It checks both residue-conversion round +trips and agreement of lowering. Its standard library is Debian's Agda stdlib +2.1-4. Only `UnsupportedIndexedMatch`, the already-reviewed warning about Cubical +transport compatibility, is suppressed for this integration. Safe mode, +without-K, internal double checking and all other warnings-as-errors remain. +The claim is ordinary Agda correspondence, not Cubical computation compatibility. + +The Debian 13 container is pinned by digest; the Agda packages are pinned by +version and installed through authenticated Debian repositories. There are no +proof-interface caches in CI. Checkout does not persist its GitHub credential. +Core checking remains independent of the standard library and Echo checkout. + +== Security and merge enforcement + +The existing CodeQL workflow analyzes GitHub Actions, the applicable language for +this repository. It does not claim to analyze Agda semantics. The shared secret +scanner checks for credentials; shell/Rust-specific jobs are supplementary when +those files are present. The governance workflow checks the estate's conventions. +Reusable workflows and actions are pinned to immutable revisions. + +Required status checks are configured on GitHub separately from these workflow +files. The proof core, canonical correspondence and secret scan must succeed on +the reviewed change. Existing signed-commit, pull-request and CodeQL security +rules remain in force. Changes to checks or dependency pins require review like +changes to proof source; a skipped or missing proof job is not a successful proof. + +Checks run for PRs and pushes to main, with timeouts and cancellation of superseded +proof runs. They never use `pull_request_target` to execute contributor code. +These gates establish the declared formal and repository-security checks. They +do not certify a deployed runtime, the adequacy of every modeled proposition, +or physical continuity. + +== Reproduce + +[source,sh] +---- +just check +just check-canonical /path/to/reviewed/echo-types /path/to/writable/agda-stdlib/src +actionlint +gh actions-lock --no-fix +---- + +The explicit writable stdlib path lets Agda recheck source without trying to +write interfaces into a system-owned package directory. CI's container performs +the same source check in its isolated filesystem. diff --git a/docs/continuity-foundations.adoc b/docs/continuity-foundations.adoc new file mode 100644 index 0000000..4f6bad7 --- /dev/null +++ b/docs/continuity-foundations.adoc @@ -0,0 +1,174 @@ += Continuity foundations: store views and certified residues +:toc: + +== Scope and status + +This is the 2026-09-07 correction of two independent prototype gaps, following +the semantic proof-transport repair. The checked source is in +`ReadConsistency.agda`, `EchoBridge.agda`, `SurrealBridge.agda`, and +`ContinuityExamples.agda`. These are breaking research APIs. + +The local Agda model now binds read values to store states, residue certificates +to a specified relation, migrations to retained information, and resource bounds +to a supplied measure. It does not implement a Firmboot typechecker, a concurrent +store, a scheduler, a physical sensor, or an update runtime. + +== Reads: state first, version second + +The old `ReadView v A` contained only a value of type `A`. Its `readIncrease` +copied that value into any later version index; `Fresh v v` then held by +reflexivity. Nothing established that the value matched the later store. +`Sync old new` was freely constructible, so its recovery theorems did not prove +that an actual read happened or that a scheduler eventually performed one. +Those definitions and the purported mutable-read `versionAccessible` instance +have been removed. Numeric version order remains a valid preorder. + +The replacement is a pure inductive store history: + +[source,agda] +---- +data Store (A : Set) : Set where + initial : A -> Store A + write : Store A -> A -> Store A +---- + +`version` is the history length, and `contents` is the latest value. A +`ReadView s` carries a value and `value ≡ contents s`. Its public constructor +requires this equality; direct construction cannot bypass it. + +`CachedRead current` carries a source history, a proof that the source is an +ancestor of `current`, and a `ReadView source`. Its freshness means equality +of source and current histories, not just equality of their version numbers. +Two different branches may have the same version and different contents. + +* `advanceCache` preserves the cached sample while extending its historical + context after a write. +* `writeStalesCache` and `writeInvalidatesFreshness` apply to every such cache, + including a write that restores an earlier value. +* `synchronize s` computes a new view using `contents s`. + `syncReadsCurrent` establishes value agreement, and `syncRestoresFresh` + establishes that its source is the current history. +* `retainUnchanged` permits an old value to become a certified view of a later + state only with an ancestry witness and an explicit contents equality. +* `FactAt s P` means `P (contents s)`. `transportFact` needs a proof that the + specific fact survives the change. The pair example changes the second + component while preserving a fact about the first. + +These are properties of a finite pure model. The model stores the full history; +no bounded-memory implementation or proof-erasure claim is made. A connection +from this history to an authoritative external store, atomic snapshots, +version reuse, memory ordering, and scheduling remains an implementation proof +obligation. Synchronization correctness is not eventual synchronization. + +== Echo: certificates, source compatibility, and sufficient information + +The former `Echo r A` stored an arbitrary residue type and token, with no +relationship to `A` or `r`. `retagEcho` could silently change its grade. + +The replacement `Retention A B R` specifies: + +* `observe : A -> B`, the visible observation; +* `retain : A -> R`, the residue actually retained; +* `Cert : R -> B -> Set`, the interpretation of a residue certificate; +* `sound : (x : A) -> Cert (retain x) (observe x)`. + +`Echo C y` carries a residue and a proof of `Cert residue y`. `lower C x` +constructs it from the actual observation and retention functions. + +A certificate's meaning is still the caller's responsibility. A trivial `Cert` +is allowed and proves only a trivial proposition. In particular, an arbitrary +certified residue need not identify the original source. `MatchesSource C x e` +requires both the observation and residue to agree with those produced from +the candidate source `x`. `lowerMatchesSource` proves this for constructed +residues. Multiple candidates may match after loss: the checked +`ambiguousSource` example establishes exactly that. This is compatibility, +not a historical-origin or execution-provenance claim, and there is no general +source-extraction rule. + +`Recovery C` additionally requires a left-inverse law for the retained pair. +`Migration C target` instead requires: + +[source,agda] +---- +adequate : (x : A) -> + migrate (observe x) (retain x) ≡ target x +---- + +The target may need less than full recovery. The example retains the first of +two Booleans and proves adequate migration for the first. It refutes adequate +migration for the discarded second Boolean. The general +`collisionForbidsMigration` theorem proves that two identical retained pairs +with different required results rule out every migration with this interface. +`migrateMatching` establishes correctness for any compatible source. Full recovery +additionally gives `recoverMatching`; these laws prevent incompatible required +results from being recovered from an ambiguous retained pair. + +`EchoMap` requires a map of visible values, a map of residues, and a proof of +certificate preservation. It claims only that relation preservation; any +source-level migration or recovery claim needs its additional law. + +== Resource bounds are separate + +`BoundedEcho C measure budget y` packages an `Echo C y` with +`measure residue ≤G budget`. The natural-number-or-infinity grade is an upper +bound on a supplied measure, not an Echo retention index. Its meaning and units +come from that measure; it is not automatically elapsed time, energy, or bytes. + +`weakenBound` requires an order proof and preserves the retained data. A smaller +bound cannot be claimed without proving that it holds. The surreal adapter now +uses `r ≤G gradePlus r accessCost` to relax an existing bound. This does not +assert that data was lost or recovered during access. The legacy +`magnitude-loss` field name denotes an instance-supplied access grade; its +composition laws alone give no information-theoretic interpretation. + +`daySurrealAccess` remains a set-sized finite-day example, not a full +formalisation of Conway's surreals. General `GradedSurrealModality` transport +is an interface obligation; only its provided instance is constructed here. + +== Relationship to canonical Echo + +The core remains dependency-free. `tests/integration/CanonicalEcho.agda` +separately imports the actual sibling `Echo` and `EchoResidue` modules. It +proves both conversion round trips between this `Echo C y` and canonical +`EchoR R (Cert C) y`, and proves that `lower` agrees with canonical +`echo-to-residue` applied to `echo-intro`. + +This is a checked correspondence for the residue representation and lowering. +It is not a proof of a full graded comonad, all sibling bridges, or runtime +migration. The canonical retention axis remains distinct from resource grades. + +== Reproduction and deliberate rejection controls + +[source,sh] +---- +just check +agda --no-libraries --safe --without-K --ignore-interfaces -i src src/EpistemicTypes/All.agda +just check-canonical /path/to/echo-types /path/to/agda-stdlib/src +---- + +The core and examples have been checked with Agda 2.6.4.3. `just check` covers +all eleven source modules and eleven semantic rejection fixtures: the four +proof-transport controls plus `StaleSample`, `FakeFreshness`, `ForkedHistory`, +`ForgedResidue`, `MismatchedSource`, `UnderstatedBound`, and `InventedMigration`. +An unrelated import or tool failure fails the rejection gate. + +The optional canonical integration also checks successfully with the locally +available standard library 2.1. Its dependencies emit `UnsupportedIndexedMatch` +compatibility warnings about Cubical transports; this run establishes ordinary +`--without-K` checking, not Cubical computation compatibility. The core build +has no standard-library dependency and emits no warnings. + +== Next obligations + +Use these constructions in the detector's complete update contract: retained +cursor/history/event status, current-state admission, linear ownership, +preparation and cancellation effects, and a permitted service trace. Then +connect resource bounds to an independently specified scheduler and implement +an acceptance checker with a soundness proof. These remain separate work. + +== Continuous verification + +The core, deliberate rejection controls and pinned canonical Echo correspondence +are CI gates; see link:ci-safety.adoc[]. Only the documented Cubical transport +compatibility warning is suppressed for the integration. The core remains +warning-free with no standard-library dependency. diff --git a/docs/proof-transport.adoc b/docs/proof-transport.adoc index 29b8e4f..e1a4731 100644 --- a/docs/proof-transport.adoc +++ b/docs/proof-transport.adoc @@ -1,736 +1,130 @@ = Proof Transport Across Trust Boundaries -Jonathan D.A. Jewell (hyperpolymath) -v0.1.0, 2026-06-15: prototype -:toc: left -:toclevels: 3 -:sectnums: -:sectnumlevels: 3 -:icons: font -:source-highlighter: rouge +:revdate: 2026-09-07 +:toc: -This is the human-readership explainer for `EpistemicTypes.ProofTransport`, the -standpoint-indexed proof-transport module of the *epistemic-types* prototype. -The Agda source at `src/EpistemicTypes/ProofTransport.agda` is the authority; -this document explains what it says and why, in prose, with the load-bearing -signatures quoted verbatim. The worked scenario lives in -`src/EpistemicTypes/ProofTransportExample.agda`, and an engineering rendering of -the same model — for A2ML/K9 tooling — lives in -`.machine_readable/proof-transport/`. +The module `EpistemicTypes.ProofTransport` enforces semantic soundness relative +to an explicit interpretation of claims. Its former token-only encoding let a +caller manufacture `Proof` status for any claim label. The earlier +`proofNeedsChecker` theorem was structurally correct but did not establish that +the claim was true. That stronger interpretation is withdrawn. -Everything described here type-checks under `{-# OPTIONS --safe --without-K #-}`, -with no postulates and no standard library (`agda --no-libraries`). The whole -library is checked by `just check`. +== The meaning and trust boundary -== Motivation: one artefact, three readings - -A single object — call it the *artefact* — can be read in three quite different -ways. The friction this module is about comes entirely from the fact that these -three readings do not travel together. - -von Neumann (data/code):: The artefact is bytes. Code and data live in the same -store; a program is just data you can also run. Bytes cross any wall: you can -copy them, mail them, post them publicly. Nothing about the bytes asserts that -they are *true* or that they *prove* anything. In this module this reading is the -type `Artifact` together with the cheap statuses `Data` and `Code`. - -Curry–Howard (proof):: A *checked* artefact can be a proof of a proposition. A -program of type `A` is a proof of `A` — but only once something has actually -checked that it has that type. Proofhood is not a property of the bytes alone; -it is the bytes *plus a successful check*. In this module the proof reading is -the statuses `Proof` and `ProofUnder m`, and those statuses are reachable only by -running a `Checker` over `Evidence`. - -Epistemic status relative to a receiver:: The same bytes mean different things to -different parties. What the sender holds as a *proof*, a receiver who has not -re-checked anything holds only as *data*, or an unverified *claim*, or a bare -*receipt* of delivery. Proofhood is *standpoint-indexed*: it is always proofhood -*for somebody*. This is the contribution of epistemic-types, and it is the reason -this module exists rather than being a one-line "just send the proof object". - -The whole design follows from one observation: *transmission moves the von -Neumann reading but not the Curry–Howard reading.* You can put a proof object on -the wire, but proofhood does not ride along with it. The receiver gets bytes. To -get *proof*, the receiver must re-establish it locally. - -[NOTE] -==== -This is exactly the discipline of *proof-carrying code* (PCC), made -standpoint-relative. In PCC a producer ships code together with a certificate, -and the consumer re-runs a small local verifier to re-establish the safety -property on its own terms — it does not trust the producer's say-so. Here the -certificate is `Evidence` (it travels as data), and the consumer's local verifier -is its own `Checker` (which does not automatically travel). Proofhood is whatever -the consumer's own checker re-establishes. -==== - -== The conceptual mapping - -The four readings line up against the module's vocabulary as follows. This same -table appears, near-verbatim, in the a2ml spec's `mapping` block and the k9 -file's `mapping` field, so that an agent consuming the engineering rendering sees -the same correspondence a human reads here. - -[cols="1,3"] -|=== -| Reading | In the module - -| von Neumann -| `Artifact` plus the statuses `Data` / `Code`: a program or proof object can - cross the wall as bytes. - -| Curry–Howard -| The statuses `Proof` / `ProofUnder m`: a *checked* artefact can be a proof of a - proposition. - -| proof-carrying code -| `Evidence` is the certificate (it travels as data); the holder's own `Checker` - is the local verifier that re-establishes proofhood. - -| epistemic-types -| Proofhood is standpoint-indexed and must be *transported and upgraded* for the - receiver, never assumed to transfer automatically. -|=== - -== The core types - -The module is parameterised over three abstract carriers — there is no built-in -notion of who or what is involved: +The module takes five arguments: [source,agda] ---- -module EpistemicTypes.ProofTransport - (Agent : Set) -- who holds a standpoint / view - (Claim : Set) -- what is asserted - (Artifact : Set) -- the von Neumann object: bytes, code, certificate - where +Agent : Set +Claim : Set +Artifact : Set +Meaning : Agent -> Artifact -> Claim -> Set +Payload : Artifact -> Claim -> Set ---- -Because the library does not depend on a standard library, a tiny local prelude -defines `⊥`, `¬_`, `Either`, `Σ`, `_×_`, and `Maybe` in-module, mirroring the -local `⊥`/`¬` pattern already used in `EpistemicTypes.Examples`. +`Claim` is a label. `Meaning holder artifact claim` is the proposition a +proof status must actually entail. A consumer must specify this proposition +faithfully: choosing a trivial meaning proves only a trivial claim. -=== View: the standpoint-indexed judgement +`Payload` describes certificate data, without conferring truth. Public, +designated, issuer, and environment evidence all carry a payload. Their mode +tags are structural; they do not establish cryptographic identity or authority. +Any required authority belongs in `Meaning` and the sound verifier's premises. -`View` is the central judgement. `View holder artifact status claim` reads as -"the *holder* regards *artifact* at epistemic *status* with respect to *claim*." -The holder index is what makes proofhood standpoint-relative. +== Executable verification with a soundness obligation [source,agda] ---- -data View (holder : Agent) : Artifact -> Status -> Claim -> Set where - asData : {a : Artifact} {c : Claim} -> View holder a Data c - asCode : {a : Artifact} {c : Claim} -> View holder a Code c - asClaimed : {a : Artifact} {c : Claim} -> View holder a Claimed c - asReceipt : {a : Artifact} {c : Claim} -> View holder a Receipt c - asProofUnder : - {a : Artifact} {m : Mode} {c : Claim} -> - Certifying m -> Checker holder m a c -> Evidence m a c -> - View holder a (ProofUnder m) c - forgetMode : - {a : Artifact} {m : Mode} {c : Claim} -> - View holder a (ProofUnder m) c -> View holder a Proof c ----- - -The asymmetry between the constructors is the entire honesty discipline: - -* The *cheap* statuses — `Data`, `Code`, `Claimed`, `Receipt` — are freely - introducible. Anybody can hold bytes, hold a claim, or hold a receipt; these - cost nothing and assert nothing about the claim. -* The *proof* statuses are not free. The only way to reach `ProofUnder m` is - `asProofUnder`, and it demands three things at once: a witness `Certifying m` - that the mode actually certifies, a `Checker holder m a c` that *this holder* - possesses, and matching `Evidence m a c`. The only way to reach `Proof` is - `forgetMode`, which simply forgets which mode a `ProofUnder` was checked in. - -So `Proof` is never a bare assertion. Every inhabitant of `View holder a Proof c` -is, by construction, a `forgetMode` of an `asProofUnder` that carried the -holder's own checker and evidence. That structural fact is what the no-smuggling -theorem later reads back off (see <>). - -=== Status: the epistemic ladder - -`Status` enumerates how an artefact stands relative to a holder and a claim. The -first four are cheap; the last two are earned. - -[source,agda] ----- -data Status : Set where - Data : Status -- von Neumann bytes; asserts nothing - Code : Status -- executable bytes; still just data to a receiver - Claimed : Status -- a claim is asserted, but unverified - Receipt : Status -- an acknowledgement; not proof of the claim - Proof : Status -- a checked proof of the claim (mode forgotten) - ProofUnder : Mode -> Status -- a checked proof under a specific mode/standpoint ----- - -The distinction between `Receipt` and `Proof` is the crux of the whole module. -A receipt acknowledges that bytes arrived; it says nothing about the truth of the -claim. `Code` is worth a separate mention: executable bytes are *still just data -to a receiver* — being able to run something is not the same as having checked -that it proves something. - -=== Mode: how an attestation is checked - -`Mode` records the verification regime under which an attestation can be checked. - -[source,agda] ----- -data Mode : Set where - Public : Mode -- publicly checkable; transferable - Designated : Agent -> Mode -- "Designated Agent": bound to one party - IssuerMediated : Mode -- needs trust in the issuer - EnvironmentMediated : Mode -- needs a runtime / environment context - OpaqueReceipt : Mode -- only acknowledges receipt; never certifies ----- - -Two modes carry the headline behaviours. `Public` attestations are portable: a -public check held by one agent is reconstructible by any other. `Designated d` -attestations are bound to a single party `d`: the checker for a designation is -pinned to that party and to no one else. `OpaqueReceipt` is the odd one out — it -acknowledges receipt and *never* certifies the underlying claim. - -A companion predicate `Certifying` records exactly which modes may yield a proof. -Crucially, `OpaqueReceipt` is *absent* from it: - -[source,agda] ----- -data Certifying : Mode -> Set where - certPublic : Certifying Public - certDesignated : {d : Agent} -> Certifying (Designated d) - certIssuer : Certifying IssuerMediated - certEnv : Certifying EnvironmentMediated ----- - -=== Gap: why an upgrade fails - -When an attempt to reach `Proof` does not succeed, the failure is named by a -`Gap` rather than being a silent dead end. - -[source,agda] ----- -data Gap : Set where - TrivialGap : Gap -- nothing else to do, but a checker is still required - DesignatedGap : Gap -- the designation does not match this holder - EnvironmentGap : Gap -- environment / context absent - IssuerTrustGap : Gap -- issuer not trusted by this holder - OpaqueGap : Gap -- receipt-only; the underlying claim is not certified - MissingChecker : Gap -- the holder lacks the checking capability - MissingEvidence : Gap -- the holder lacks the certificate / evidence - MissingContext : Gap -- the holder lacks the ambient context ----- - -[IMPORTANT] -==== -The `Gap` type is *vocabulary*, and most of it is reserved for future -refinement. The research core today actually constructs only three of these -gaps: `verify` emits `OpaqueGap` for the receipt-only case, and `tryUpgrade` -emits `MissingChecker` / `MissingEvidence` for the missing-resource cases. The -remaining gaps — and the per-mode `gap_on_fail` mapping in the k9 file — are -names for behaviour a later refinement may implement, not behaviour the core -emits yet. The k9 file records this honestly as `law.gaps_realized_today`. -==== - -=== Checker and Evidence: capability versus certificate - -This is the distinction that makes the whole thing work, so it is worth stating -plainly: *evidence travels; capability does not.* - -`Evidence` is the certificate payload. It is plain data — von Neumann bytes — and -it crosses any boundary freely. Possessing evidence is *not* the same as -possessing proof. - -[source,agda] ----- -data Evidence : Mode -> Artifact -> Claim -> Set where - publicEv : {a : Artifact} {c : Claim} -> Evidence Public a c - designatedEv : {a : Artifact} {c : Claim} (d : Agent) -> Evidence (Designated d) a c - issuerEv : {a : Artifact} {c : Claim} -> Evidence IssuerMediated a c - envEv : {a : Artifact} {c : Claim} -> Evidence EnvironmentMediated a c - receiptEv : {a : Artifact} {c : Claim} -> Evidence OpaqueReceipt a c ----- - -`Checker holder m a c` is a *holder's capability* to verify, in mode `m`, that -artefact `a` certifies claim `c`. Capabilities — not certificates — are the part -that does not automatically cross a trust boundary. The indexing on `holder` is -where the standpoint lives. - -[source,agda] ----- -data Checker (holder : Agent) : Mode -> Artifact -> Claim -> Set where - publicCheck : {a : Artifact} {c : Claim} -> Checker holder Public a c - designatedCheck : {a : Artifact} {c : Claim} -> Checker holder (Designated holder) a c - issuerCheck : {a : Artifact} {c : Claim} -> Checker holder IssuerMediated a c - envCheck : {a : Artifact} {c : Claim} -> Checker holder EnvironmentMediated a c - receiptCheck : {a : Artifact} {c : Claim} -> Checker holder OpaqueReceipt a c ----- - -Two constructors deserve close reading: - -* `publicCheck` is agent-agnostic — *any* holder can introduce it. This is why - public verification is portable. -* `designatedCheck` produces a `Checker holder (Designated holder) a c` — note - that the designated party in its mode is forced to be `holder` itself. There is - *deliberately no* constructor that gives one agent a checker for another - agent's designation. This single design choice is what gives designated - attestations their deniability, and it is read back off by the theorem - `designatedBindsHolder`. - -=== Boundary: a directed trust wall - -A `Boundary` is simply a directed edge from a sender to a receiver: - -[source,agda] ----- -record Boundary : Set where - constructor _⇒_ +record CertificateCheck (holder : Agent) (a : Artifact) (c : Claim) : Set where + constructor certificateCheck field - from : Agent - to : Agent ----- - -So `Alice ⇒ Bob` is the boundary across which something flows from Alice to Bob. - -== The two operations - -The whole behavioural surface is two operations that pull in opposite -directions: one conservative (transport never adds proofhood) and one -constructive (local checking is the only thing that does). - -=== transmit: bytes cross, proofhood does not - -`transmit` is the conservative half. A sender's *proof* arrives at the receiver -only as a *receipt*: - -[source,agda] ----- -transmit : - {a : Artifact} {c : Claim} -> - (b : Boundary) -> - View (from b) a Proof c -> - View (to b) a Receipt c -transmit b _ = asReceipt ----- - -The implementation discards its proof argument and returns `asReceipt`. That is -not laziness — it is the point. Transport of a proof object yields, on the far -side, an *acknowledgement of delivery* and nothing stronger. The bytes crossed -the wall; the proofhood did not. - -=== verify: local checking is the only upgrade - -`verify` is the constructive half. Given the holder's *own* checker and matching -evidence, it upgrades a `Data` view to a `Proof` view — or returns a `Gap`: - -[source,agda] ----- -verify : - {holder : Agent} {a : Artifact} {m : Mode} {c : Claim} -> - Checker holder m a c -> - Evidence m a c -> - View holder a Data c -> - Either Gap (View holder a Proof c) -verify publicCheck ev _ = right (forgetMode (asProofUnder certPublic publicCheck ev)) -verify designatedCheck ev _ = right (forgetMode (asProofUnder certDesignated designatedCheck ev)) -verify issuerCheck ev _ = right (forgetMode (asProofUnder certIssuer issuerCheck ev)) -verify envCheck ev _ = right (forgetMode (asProofUnder certEnv envCheck ev)) -verify receiptCheck _ _ = left OpaqueGap ----- - -Each certifying checker constructs an honest `asProofUnder` — carrying the -certifying witness, the checker, and the evidence — then forgets the mode. The -`receiptCheck` case has no certifying witness available (`OpaqueReceipt` is not -`Certifying`), so it can only return `left OpaqueGap`. - -=== checkableTransportUpgrades: the central positive theorem - -The two halves are combined in the central theorem. It takes the full apparatus -of a real transport — the sender already had a proof, it crossed a boundary, and -the receiver holds the bytes — but the upgrade is justified *only* by the -receiver's own checker and evidence: - -[source,agda] ----- -checkableTransportUpgrades : - {sender receiver : Agent} {a : Artifact} {m : Mode} {c : Claim} -> - View sender a Proof c -> -- the sender already had a proof ... - Boundary -> -- ... it crossed a boundary ... - View receiver a Data c -> -- ... and the receiver holds the bytes, - Checker receiver m a c -> -- but proofhood is recovered only via the - Evidence m a c -> -- receiver's own checker and evidence. - Either Gap (View receiver a Proof c) -checkableTransportUpgrades _ _ dv ck ev = verify ck ev dv ----- - -The sender's proof and the boundary are bound to `_` — they are *present but -deliberately unused*. The body is just `verify ck ev dv`. The message of the type -signature is therefore precise: even when a genuine proof really did cross a real -boundary, the upgrade on the far side is earned entirely by the receiver's local -checker and evidence. Transmission contributes nothing to proofhood. - -== The three regimes - -The three headline modes give three distinct transport regimes. Each is captured -by a small theorem. - -=== Public: portable - -A public certificate plus a public checker upgrades data to proof, and public -checking is *not* bound to any one receiver — a public checker held by `r` is -reconstructible by any other agent `q`: - -[source,agda] ----- -publicTransfer : - {receiver : Agent} {a : Artifact} {c : Claim} -> - Checker receiver Public a c -> - Evidence Public a c -> - View receiver a Data c -> - Either Gap (View receiver a Proof c) -publicTransfer = verify - -publicIsPortable : - {r q : Agent} {a : Artifact} {c : Claim} -> - Checker r Public a c -> Checker q Public a c -publicIsPortable publicCheck = publicCheck ----- - -`publicIsPortable` is the formal content of "public means anyone can check it". - -=== Designated: receiver-bound and deniable - -The designated receiver can verify a designated attestation addressed to it -(`designatedTransfer`). But a designated checker *pins the designation to its own -holder*: - -[source,agda] ----- -designatedBindsHolder : - {holder d : Agent} {a : Artifact} {c : Claim} -> - Checker holder (Designated d) a c -> d ≡ holder -designatedBindsHolder designatedCheck = refl ----- - -Reading this: if you have a checker for `Designated d`, then `d` *is* you. No -third party can ever hold the checker for someone else's designation. This is the -deniability of a designated-verifier attestation, established *by construction* — -not by an assumption, but because there is no constructor that could provide -otherwise. - -=== Receipt-only: never certifies - -The opaque-receipt regime never certifies the underlying claim, for anyone. Two -facts pin this down: - -[source,agda] ----- -opaqueNotCertifying : ¬ Certifying OpaqueReceipt -opaqueNotCertifying () - -verifyReceiptIsGap : - {holder : Agent} {a : Artifact} {c : Claim} -> - (ev : Evidence OpaqueReceipt a c) -> - (v : View holder a Data c) -> - verify {holder} receiptCheck ev v ≡ left OpaqueGap -verifyReceiptIsGap ev v = refl + check : Payload a c -> Bool + sound : (p : Payload a c) -> check p ≡ true -> Meaning holder a c ---- -`opaqueNotCertifying` says there is no certifying witness for `OpaqueReceipt` at -all (proved by an absurd pattern — the type is empty). `verifyReceiptIsGap` says -that running `verify` with a receipt checker computes, definitionally, to -`left OpaqueGap` — it can never produce a proof. +A checker may reject every payload: completeness is not assumed. It may accept +only when its soundness proof can establish the meaning. An always-accepting +checker for a false meaning cannot satisfy this interface under the stated +safe Agda discipline. -== The resource-gathering layer +`runChecker` evaluates the chosen check on the evidence payload. +`asProofUnder` requires a certifying mode, the checker, evidence, and a proof +that this computation equals `true`. Direct use of the exported constructor +therefore has the same semantic obligation as `verify`. -Before you can even run a check you must actually *possess* the capability and -the certificate. `tryUpgrade` is the discovery layer that sits above `verify` and -names the missing-resource gaps: +The primary guarantee is: [source,agda] ---- -tryUpgrade : - {holder : Agent} {a : Artifact} {m : Mode} {c : Claim} -> - Maybe (Checker holder m a c) -> - Maybe (Evidence m a c) -> - View holder a Data c -> - Either Gap (View holder a Proof c) -tryUpgrade nothing _ _ = left MissingChecker -tryUpgrade (just _) nothing _ = left MissingEvidence -tryUpgrade (just ck) (just ev) v = verify ck ev v ----- - -This is where `MissingChecker` and `MissingEvidence` — the other two -realised-today gaps — come from. - -[#honesty] -== The honesty property: no smuggling - -The whole module is built so that nobody can sneak a proof across a boundary -without re-earning it. The structural statement of this is `proofNeedsChecker`: - -[source,agda] ----- -proofNeedsChecker : +proofSound : {holder : Agent} {a : Artifact} {c : Claim} -> - View holder a Proof c -> - Σ Mode (λ m -> Certifying m × Checker holder m a c × Evidence m a c) -proofNeedsChecker (forgetMode (asProofUnder cert ck ev)) = _ , cert , ck , ev ----- - -Read it as a guarantee about *any* proof a holder claims to possess. Given any -`View holder a Proof c`, this function extracts the mode, the certifying witness, -*the holder's own* checker, and the evidence that must have backed it. The single -pattern `forgetMode (asProofUnder cert ck ev)` is exhaustive precisely because -`View`'s constructors leave no other route to `Proof`. - -The corollary is the no-smuggling property the module is named for: there is *no -exported function* of type - -[source,agda] ----- -View sender a Proof c -> View receiver a Proof c ----- - -Such a function would have to fabricate the *receiver's* checker and evidence out -of nothing, and `View` provides no constructor that lets it. Combined with -`transmit` — whose only output for a crossing proof is `asReceipt` — this means -the only honest path from a sender's proof to a receiver's proof runs through the -receiver doing its own `verify`. That is the entire ethic of the module, and it -is enforced by Agda's coverage and totality checking, not by convention. - -To summarise the honesty discipline: - -* *Conservative transport.* `transmit` yields only `Receipt`; no - `View sender a Proof c -> View receiver a Proof c` is exported. -* *No smuggling.* Every `View holder a Proof c` carries that holder's own mode, - certifying witness, checker, and evidence (`proofNeedsChecker`). -* *Constructive.* Compiles under `--safe --without-K`; no postulates; no standard - library. - -== Worked example: K9-SVC, Alice, and Bob - -`EpistemicTypes.ProofTransportExample` instantiates the core at concrete -carriers and walks the scenario end to end. The cast: - -[cols="1,2"] -|=== -| Role | Value - -| issuer | `K9SVC` -| receiver | `Alice` -| third party | `Bob` -| claim | `ActionWasPerformed` -| artifact | `AttestationBlob` -|=== - -[source,agda] ----- -data Agent : Set where - K9SVC : Agent - Alice : Agent - Bob : Agent - -data Claim : Set where ActionWasPerformed : Claim -data Artifact : Set where AttestationBlob : Artifact - -open import EpistemicTypes.ProofTransport Agent Claim Artifact ----- - -=== Case 1: the blob is raw data for Alice - -Before Alice checks anything, the attestation blob is just bytes to her: - -[source,agda] ----- -aliceRaw : View Alice AttestationBlob Data ActionWasPerformed -aliceRaw = asData ----- - -No claim is certified. This is the von Neumann reading and nothing more. - -=== Case 2: Alice upgrades with her designated checker and evidence - -K9SVC issued the attestation *designated to Alice*. Alice therefore holds the -matching designated checker and evidence, and upgrades the blob to a genuine -proof of `ActionWasPerformed`: - -[source,agda] ----- -aliceChecker : Checker Alice (Designated Alice) AttestationBlob ActionWasPerformed -aliceChecker = designatedCheck - -aliceEvidence : Evidence (Designated Alice) AttestationBlob ActionWasPerformed -aliceEvidence = designatedEv Alice - -aliceUpgrade : Either Gap (View Alice AttestationBlob Proof ActionWasPerformed) -aliceUpgrade = designatedTransfer aliceChecker aliceEvidence aliceRaw ----- - -And the upgrade demonstrably *succeeds* — it computes to `right aliceProof`, a -fact the example pins down with a `refl` proof: - -[source,agda] ----- -aliceUpgradeSucceeds : aliceUpgrade ≡ right aliceProof -aliceUpgradeSucceeds = refl ----- - -=== Case 3: Bob across the boundary - -This is where the three regimes show their teeth. Bob sits on the far side of the -`Alice ⇒ Bob` boundary. - -==== Case 3a: Bob gets a receipt, not a proof - -When Alice's proof crosses to Bob, it degrades to a receipt. The bytes crossed; -the proofhood did not: - -[source,agda] ----- -aliceToBob : Boundary -aliceToBob = Alice ⇒ Bob - -bobReceipt : View Bob AttestationBlob Receipt ActionWasPerformed -bobReceipt = transmit aliceToBob aliceProof ----- - -==== Case 3b: Bob cannot manufacture the designated proof - -Bob cannot conjure Alice's designated proof, because the designated capability is -bound to Alice and `Alice ≢ Bob`. The type -`Checker Bob (Designated Alice) AttestationBlob ActionWasPerformed` is *empty* — -and the example proves it so, using `designatedBindsHolder`: - -[source,agda] ----- -Alice≢Bob : ¬ (Alice ≡ Bob) -Alice≢Bob () - -bobHasNoDesignatedChecker : - ¬ Checker Bob (Designated Alice) AttestationBlob ActionWasPerformed -bobHasNoDesignatedChecker ck = Alice≢Bob (designatedBindsHolder ck) ----- - -If Bob *had* such a checker, `designatedBindsHolder` would force `Alice ≡ Bob`, -which `Alice≢Bob` refutes. This is the deniability of the designated attestation, -realised concretely: a third party simply cannot hold the verification -capability. Whatever Bob shows around, he cannot turn it into a proof addressed -to him. - -==== Case 3c: but a public attestation is portable to Bob - -If, instead, the attestation had been *public*, Bob would upgrade like anyone -else, because public checking is portable from Alice to Bob: - -[source,agda] ----- -bobPublicChecker : Checker Bob Public AttestationBlob ActionWasPerformed -bobPublicChecker = publicIsPortable {Alice} {Bob} publicCheck - -bobPublicUpgrade : - Evidence Public AttestationBlob ActionWasPerformed -> - Either Gap (View Bob AttestationBlob Proof ActionWasPerformed) -bobPublicUpgrade ev = publicTransfer bobPublicChecker ev asData ----- - -The contrast between 3b and 3c is the whole point of the public/designated split: -the same shape of operation either is or is not available to a third party, -entirely according to the mode the issuer chose. - -==== A receipt-only attestation upgrades for nobody - -Finally, a receipt-only attestation never reaches proof, for Bob or anyone: - -[source,agda] ----- -bobReceiptStuck : - (ev : Evidence OpaqueReceipt AttestationBlob ActionWasPerformed) -> - verify receiptCheck ev bobBlob ≡ left OpaqueGap -bobReceiptStuck ev = verifyReceiptIsGap ev bobBlob ----- - -== The a2ml / k9 engineering rendering - -The same model has an *engineering* counterpart under -`.machine_readable/proof-transport/`, intended for A2ML/K9 tooling. The Agda -module is the authority; these files mirror it as data agents can read and -validate. - -[cols="1,3"] -|=== -| File | Role - -| `ProofTransport.a2ml` -| A2ML spec: the entities, statuses, modes, gaps, the judgement, the operations, - the theorems, the honesty discipline, the conceptual mapping, and the K9-SVC - scenario — written for agents to consume. - -| `proof-transport.k9.ncl` -| A K9 contractile at the `'Kennel` leash (pure data, no eval): the same model as - a Nickel datum that K9 tooling can typecheck and export - (`nickel typecheck` / `nickel export`). -|=== - -The correspondence is one-to-one with the Agda surface: - -[cols="1,1"] -|=== -| Research (Agda) | Engineering (a2ml / k9) - -| `View`, `Status` | `statuses` -| `Mode` | `modes` -| `Gap` | `gaps` -| `transmit` | `law.transmit_yields = "Receipt"` -| `verify` / `checkableTransportUpgrades` | `law.upgrade_requires` -| `publicIsPortable` | `modes.Public.portable = true` -| `designatedBindsHolder` | `modes.Designated.receiver_bound = true` -| `opaqueNotCertifying` | `modes.OpaqueReceipt.certifies = false` -| `proofNeedsChecker` | `law.no_free_proof_transfer = true` -| `ProofTransportExample` | `scenario` (K9SVC / Alice / Bob) -|=== - -[NOTE] -==== -The k9 file carries a per-mode `gap_on_fail` field, and the a2ml/k9 vocabulary -lists all eight gaps. These are *reserved* failure mappings. As noted in -<>, the research core currently constructs only `OpaqueGap` (via -`verify`) and `MissingChecker` / `MissingEvidence` (via `tryUpgrade`); the k9 -file records this faithfully in `law.gaps_realized_today`. The rest is vocabulary -for a future refinement, not behaviour the core implements today. The engineering -rendering is deliberately not allowed to over-claim relative to the Agda. -==== - -== Scope: what this is and is not - -This is a small, compositional core — a deliberately honest scaffold, not a full -proof-carrying-code system. Cryptography, the full A2ML format, and the real -K9-SVC service are *not* modelled; `K9SVC`, `Alice`, `Bob`, and `AttestationBlob` -are abstract carriers chosen to make the standpoint structure legible. Likely -future directions, kept out of the current core on purpose, include concrete -checkers, issuer-trust contexts, and a graded bridge to `Echo` (via -`EpistemicTypes.EchoBridge`) for *partial* proofs — proofs that arrive with a -measured residue of loss rather than wholesale. - -What the module does claim, it claims exactly: proofhood is standpoint-indexed, -transmission moves bytes and not proofhood, and the only honest way to a -receiver's proof is the receiver's own check. - -== Where to look next - -* `src/EpistemicTypes/ProofTransport.agda` — the authoritative module. -* `src/EpistemicTypes/ProofTransportExample.agda` — the worked K9-SVC scenario. -* `readme.adoc` — the repository overview, including the proof-transport section. -* `.machine_readable/proof-transport/README.adoc` — the engineering rendering's - own guide, with the same correspondence table. -* `EpistemicTypes.EchoBridge` and the sibling *echo-types* repository — the - min-plus graded loss/residue formalism this module would compose with for - partial proofs. - -Type-check everything with: - -[source,console] ----- -just check ----- - -which runs `agda --no-libraries -i src src/EpistemicTypes/All.agda` under Agda -2.8.0. + View holder a Proof c -> Meaning holder a c +---- + +Its construction extracts the acceptance equality and invokes the checker's +soundness proof. `proofCannotSupportFalse` derives the impossibility of a +proof status for a refuted meaning. `proofHasSuccessfulCheck` extracts the +checker, evidence, and successful-check witness. `proofNeedsChecker` retains +the weaker structural projection for callers that need it. + +== Transfer and failure + +* `transmit` produces a receiver-side `Receipt`. +* `verify` returns a proof on successful verification and `InvalidEvidence` + when a certifying checker returns false. +* Opaque receipt mode always returns `OpaqueGap`. +* `tryUpgrade` additionally reports `MissingChecker` or `MissingEvidence`. +* Other `Gap` constructors remain reserved vocabulary; they are not automatic + runtime checks of issuer trust or environmental availability. + +The boundary supplied to `checkableTransportUpgrades` now determines its sender +and receiver indices. The sender's proof is not used to invent the receiver's +meaning; the receiver's check must establish it. + +A public checking algorithm can be reused at another holder only when the +caller supplies `Meaning r a c -> Meaning q a c`. For holder-independent +meanings this implication can be the identity function. Arbitrary +holder-dependent meanings do not admit it. The checker still runs on the +payload after such transport. + +The designated mode pins the designated party to the holder. This is a type +index property, not a proof of cryptographic deniability, unforgeable identity, +or a physical access-control mechanism. + +== Checked examples and regression controls + +`ProofTransportExample` supplies a concrete Boolean certificate checker. +`ArtifactIsTrue` means the artefact equals `true`; `ImpossibleClaim` has an +empty meaning. The examples establish: + +* successful designated, public, issuer, and environment checks; +* rejection of invalid payloads, altered artefacts, and impossible claims; +* opaque-receipt and missing-resource rejection; +* impossibility of arbitrary proof-status fabrication; +* impossibility of silently moving a holder-dependent proof to another holder. + +These are proofs about an actual Boolean checking function in the model, +not certificates that an external physical action occurred. + +`just check` checks the whole library and four files that must be rejected: +`LyingVerifier`, `ForgedAcceptance`, `ReplayedArtifact`, and +`ReplayedHolder`. The rejection runner requires the intended type-mismatch +diagnostic; a missing import or broken tool does not count as a pass. + +== Migration and remaining scope + +This is a breaking prototype API correction. Module instantiations must supply +`Meaning` and `Payload`; certifying checker constructors take a +`CertificateCheck`; evidence constructors take a payload; `asProofUnder` +takes the successful-check equality; public portability takes an explicit +semantic implication. The in-repository example has been updated. + +The result is conditional on the supplied meaning, the checker's soundness +proof, and Agda's trusted implementation. There is no postulated semantic +soundness axiom in this module. A consumer may not silently replace the +meaning, attach a proof to different artefacts, or infer physical correctness +without a separate model-to-implementation argument. + +The subsequent continuity-foundations repair connects `ReadConsistency` to a +finite store model and replaces unconstrained Echo indices with certified +relations and measured bounds. See link:continuity-foundations.adoc[]. External +store, concurrent runtime, and physical correspondence remain separate. diff --git a/docs/what-epistemic-is.adoc b/docs/what-epistemic-is.adoc index cb56015..c8f6725 100644 --- a/docs/what-epistemic-is.adoc +++ b/docs/what-epistemic-is.adoc @@ -58,11 +58,11 @@ determine them. Neumann bytes, a Curry–Howard proof, an epistemic status relative to a holder — via `View holder artifact status claim`. `transmit` moves *bytes, not proofhood* (a sender's `Proof` arrives only as a `Receipt`); `verify` recovers -proofhood *only* with the *receiver's own* `Checker` and `Evidence`; and -`proofNeedsChecker` is the structural *no-smuggling* property: every -`View holder a Proof c` decomposes into that holder's own certifying mode, -checker, and evidence, so no checker-free -`View sender … Proof → View receiver … Proof` exists. All of the above +proofhood through a successful sound check of an explicit +`Meaning holder artifact claim`. `proofSound` derives that meaning; +`proofNeedsChecker` remains a weaker structural projection. Public transport +requires a proved implication between the holders' meanings. The earlier +token-only encoding did not establish semantic truth. All of the above type-checks under `--safe --without-K` with zero postulates, per `AFFIRMATION.adoc`. @@ -149,7 +149,7 @@ checkable artefacts* recorded as ground truth in `AFFIRMATION.adoc`: for `⊥`; * `ProofTransport.proofNeedsChecker` (no-smuggling), with `designatedBindsHolder`, `opaqueNotCertifying`, and `verifyReceiptIsGap` giving - the public-portable / designated-bound / receipt-never-certifies trichotomy. + the explicitly qualified public portability / designated-bound / receipt-never-certifies distinction. These results are consumed downstream: the proof-transport / warrant-gap model is used by *snifs* (deniable, non-forging attestation) and is named as the @@ -183,13 +183,13 @@ To keep boundaries un-eroded: `SoundWarrant.sound`) is a *separate, assumed* interface; the default `Warrant`/`Belief` carry no truth axiom. A reader who treats a warrant as a proof of its claim has crossed exactly the line this repo draws. -* the *epistemic* modality `E` *is NOT the echo* (loss/residue) modality. They - *compose* — `E κ (Echo r A)` is meaningful — but do *not collapse*: - `EchoBridge` is a deliberate scaffold that proves *no graded-loss theorems of - its own* (per `AFFIRMATION.adoc`), and the prototype keeps `Echo r A` and - `E κ A` distinct on purpose. +* the epistemic modality, Echo retention, and resource bounds remain separate. + `E κ (Echo C y)` describes availability of a certified residue; + `BoundedEcho C measure budget y` adds a measure inequality. The optional + canonical integration proves residue representation and lowering agreement. + No full graded-comonad or physical-loss theorem follows from this bridge. * epistemic-types *is NOT a verified external system*. The green typecheck - establishes an *idealised core calculus*; it does not establish that any real + checks the formalised types and propositions; it does not establish that any real attestation protocol, CRDT read path, or proof-carrying-code pipeline *refines* it. There is no production implementation in this repo. * the `SurrealBridge` *is NOT* the full Conway proper class of surreals — only diff --git a/explainme.adoc b/explainme.adoc index 94d6e36..dfb9c7e 100644 --- a/explainme.adoc +++ b/explainme.adoc @@ -35,50 +35,57 @@ for `A` at `κ`. `Epi κ A` packages a warrant and a token. This still does no prove `A`. A sound warrant is a separate record with an explicit soundness function. -== Echo distinction +== Reads and retained information -Echo-types track loss, residue, or irrecoverability grades. Epistemic types -track standpoint-relative access, belief, knowledge, or warrant. The bridge -`E κ (Echo r A)` says that a standpoint has access to a lossy/residual echo of -`A`; it is not the same as directly having `E κ A`. +A `ReadView s` proves that its value matches the contents of the store history +`s`. Cached reads retain their source and ancestry. A write makes them stale; +a model read obtains current data. Facts about unchanged aspects can survive a +write through an explicit proof. + +`Echo C y` holds a residue certified relative to the chosen retention contract. +`MatchesSource` checks compatibility with a candidate source; information loss +can leave multiple candidates. Exact recovery and migration require additional +laws. The example retains one Boolean from a pair: it supports migration for +that Boolean, but cannot support migration for the discarded Boolean. + +The composition `E κ (Echo C y)` expresses epistemic access to that certified +residue. Standpoint access, retained information, and resource quantities remain +separate dimensions. == Surreal bridge -The surreal bridge uses an abstract set-sized carrier with an order and a -grade-valued access loss. The loss is used by `GradedSurrealModality`: +`BoundedEcho C measure budget y` adds a proved upper bound on a residue measure. +The concrete surreal adapter preserves data while relaxing that bound according +to an instance-supplied access grade. The legacy `magnitude-loss` name does not +establish measured information loss or physical elapsed time. ----- -E x (Echo r A) -> E y (Echo (gradePlus r (magnitude-loss p)) A) ----- +The bridge keeps the existing factive/non-factive separation results. Its +`daySurrealAccess` is a set-sized finite-day example, not all Conway surreals. +The optional canonical integration proves correspondence with the actual +`EchoResidue.EchoR`. See link:docs/continuity-foundations.adoc[]. -for `p : x ≤♯ y`. This is the point where surreal-like magnitude does work in -the type: moving across access accumulates a tropical loss grade. +== Proof transport -The bridge still proves the same separation results: factive knowledge needs -`reflect`, belief has no generic reflection, and warrant tokens do not expose -their claims without separate soundness. +`ProofTransport` is parameterised by agents, claim labels, artefacts, +`Meaning : Agent -> Artifact -> Claim -> Set`, and a certificate +`Payload : Artifact -> Claim -> Set`. The caller states the meaning being proved. -The bridge is not a formalization of the full class of Conway surreals. That -would require a universe-indexed or class-like treatment, not a single ordinary -Agda `Set`. The included `daySurrealAccess` instance is a finite birthday -tower: the grade is the number of birthday/refinement steps. +A `CertificateCheck` contains an executable Boolean check and a proof that +acceptance entails that exact meaning. Evidence carries a payload; possessing +it alone proves nothing. A proof constructor also requires +`runChecker checker evidence ≡ true`. -== Proof transport + proofSound : View holder a Proof c -> Meaning holder a c + +`verify` evaluates the checking function and returns `InvalidEvidence` on +rejection. `transmit` produces a receipt at the receiving holder. +`publicIsPortable` requires an explicit implication between the two holders' +meanings; it does not silently relabel holder-dependent truths. -One artefact can be read three ways at once: as von Neumann data/code, as a -Curry–Howard proof object, and as an epistemic status relative to a receiver. -`EpistemicTypes.ProofTransport` keeps these apart. - -The honesty point mirrors the rest of the library: a receiver does not get -`Proof claim` for free. `transmit` carries a sender's proof across a trust -boundary as a mere `Receipt`; the receiver re-establishes proofhood only by -running its own `Checker` over `Evidence` (`verify`). Public verification is -portable to anyone; a designated checker is pinned to its holder, so a third -party cannot reconstruct it; a receipt-only attestation never certifies the -underlying claim. This is the proof-carrying-code pattern made -standpoint-relative: the certificate is data and travels, but the verification -standpoint must be re-supplied by the receiver. An engineering rendering for -A2ML/K9 tooling lives under `.machine_readable/proof-transport/`. +The example checks Boolean artefacts and certificates, proves legitimate +acceptance, and refutes false claims. It does not claim that a physical action +occurred. The older token-only model lacked semantic soundness; the strengthened +interface is a breaking correction documented in link:docs/proof-transport.adoc[]. == Roadmap diff --git a/src/EpistemicTypes/All.agda b/src/EpistemicTypes/All.agda index 61064ed..6280350 100644 --- a/src/EpistemicTypes/All.agda +++ b/src/EpistemicTypes/All.agda @@ -11,6 +11,7 @@ open import EpistemicTypes.EchoBridge public -- which would clash with Examples' identically-named helpers if both were -- re-exported. The module is still part of the build via this import. import EpistemicTypes.ReadConsistency +import EpistemicTypes.ContinuityExamples open import EpistemicTypes.SurrealBridge public open import EpistemicTypes.Examples public open import EpistemicTypes.ProofTransportExample public diff --git a/src/EpistemicTypes/ContinuityExamples.agda b/src/EpistemicTypes/ContinuityExamples.agda new file mode 100644 index 0000000..40ddd01 --- /dev/null +++ b/src/EpistemicTypes/ContinuityExamples.agda @@ -0,0 +1,188 @@ +{-# OPTIONS --safe --without-K #-} + +module EpistemicTypes.ContinuityExamples where + +open import Agda.Builtin.Bool using (Bool; true; false) +open import Agda.Builtin.Equality using (_≡_; refl) +open import Agda.Builtin.Nat using (zero; suc) +open import Agda.Builtin.Sigma using (Σ; _,_; fst; snd) +open import Agda.Builtin.Unit using (⊤; tt) +import EpistemicTypes.ReadConsistency as Read +import EpistemicTypes.EchoBridge as Echo +import EpistemicTypes.SurrealBridge as Surreal + +module Reads where + open Read + + before : Store Bool + before = initial false + + after : Store Bool + after = write before true + + anotherWrite : Store Bool + anotherWrite = write after false + + old : CachedRead before + old = synchronize before + + historical : CachedRead after + historical = advanceCache true old + + oldSamplePreserved : cachedValue historical ≡ false + oldSamplePreserved = refl + + oldSampleNotFresh : ¬ (Fresh historical) + oldSampleNotFresh = writeInvalidatesFreshness true old + + refreshActuallyChangesValue : cachedValue (synchronize after) ≡ true + refreshActuallyChangesValue = syncReadsCurrent after + + refreshAfterTwoWrites : Fresh (synchronize anotherWrite) + refreshAfterTwoWrites = syncRestoresFresh anotherWrite + + historicalAgain : CachedRead anotherWrite + historicalAgain = advanceCache false historical + + valueReturnedButSnapshotDidNot : cachedValue historicalAgain ≡ contents anotherWrite + valueReturnedButSnapshotDidNot = refl + + stillHistoricalAfterValueReturns : ¬ (Fresh historicalAgain) + stillHistoricalAfterValueReturns = writeInvalidatesFreshness false historical + + falseIsNotTrue : false ≡ true -> ⊥ + falseIsNotTrue () + + cannotKeepFalseAsCurrent : (rv : ReadView after) -> value rv ≡ false -> ⊥ + cannotKeepFalseAsCurrent (readView .false eq) refl = falseIsNotTrue eq + + -- Version equality alone does not identify a store or its contents. + otherBranch : Store Bool + otherBranch = write before false + + sameVersion : version after ≡ version otherBranch + sameVersion = refl + + differentCurrentValues : contents otherBranch ≡ contents after -> ⊥ + differentCurrentValues = falseIsNotTrue + + -- The sample is still historical after a value-preserving write, but an + -- explicit value equality allows it to become a certified current view. + sameValue : Store Bool + sameValue = write before false + + retainedValue : ReadView sameValue + retainedValue = retainUnchanged (earlier here) refl (readCurrent before) + + retainedValueIsFalse : value retainedValue ≡ false + retainedValueIsFalse = refl + + -- A fact about one component can survive a change to another component. + Pair : Set + Pair = Σ Bool (λ _ -> Bool) + + pairBefore : Store Pair + pairBefore = initial (true , false) + + pairAfter : Store Pair + pairAfter = write pairBefore (true , true) + + FirstIsTrue : Pair -> Set + FirstIsTrue pair = fst pair ≡ true + + unaffectedFact : FactAt pairAfter FirstIsTrue + unaffectedFact = transportFact {s = pairBefore} {t = pairAfter} + {P = FirstIsTrue} (λ p -> p) refl + + -- There is no value-preserving version-only transport for arbitrary writes. + noUniversalValueRetag : + ((s : Store Bool) (a : Bool) (rv : ReadView s) -> + Σ (ReadView (write s a)) (λ next -> value next ≡ value rv)) -> ⊥ + noUniversalValueRetag retag with retag before true (readCurrent before) + ... | next , unchanged = cannotKeepFalseAsCurrent next unchanged + +module Residues where + open Echo + + -- Identity observation and retention give valid and invalid certificates + -- for the same contract: the residue must equal the indexed visible value. + identityRetention : Retention Bool Bool Bool + Retention.observe identityRetention b = b + Retention.retain identityRetention b = b + Retention.Cert identityRetention r y = r ≡ y + Retention.sound identityRetention b = refl + + identityTrue : Echo identityRetention true + identityTrue = lower identityRetention true + + identityRecovery : Recovery identityRetention + Recovery.recover identityRecovery _ r = r + Recovery.roundtrip identityRecovery b = refl + + trueRoundtrip : Recovery.recover identityRecovery true + (Echo.residue identityTrue) ≡ true + trueRoundtrip = recoverLower identityRecovery true + + -- Forget the second Boolean while retaining exactly the first. The target + -- needs only the first, so its migration is adequate despite lost data. + Pair : Set + Pair = Σ Bool (λ _ -> Bool) + + firstRetention : Retention Pair ⊤ Bool + Retention.observe firstRetention _ = tt + Retention.retain firstRetention pair = fst pair + Retention.Cert firstRetention _ _ = ⊤ + Retention.sound firstRetention _ = tt + + -- Compatibility does not identify the original source after loss: this + -- echo was lowered from (true,false) and also matches (true,true). + ambiguousSource : MatchesSource firstRetention (true , true) + (lower firstRetention (true , false)) + ambiguousSource = matchesSource refl refl + + firstMigration : Migration firstRetention fst + Migration.migrate firstMigration _ r = r + Migration.adequate firstMigration pair = refl + + migrateFirst : Migration.migrate firstMigration tt + (Echo.residue (lower firstRetention (true , false))) ≡ true + migrateFirst = migrateMatching firstMigration (true , false) + (lower firstRetention (true , false)) (lowerMatchesSource firstRetention (true , false)) + + falseIsNotTrue : false ≡ true -> Impossible + falseIsNotTrue () + + -- Both source states have exactly the same visible value and residue. + -- Consequently NO implementation can migrate the discarded second bit. + cannotMigrateSecond : Migration firstRetention snd -> Impossible + cannotMigrateSecond = collisionForbidsMigration firstRetention snd + (true , false) (true , true) refl refl falseIsNotTrue + + constantCost : Bool -> Grade + constantCost _ = finite (suc zero) + + boundedTrue : BoundedEcho identityRetention constantCost (finite (suc zero)) true + boundedTrue = bounded identityTrue (finite≤ (suc≤ zero≤)) + + relaxed : BoundedEcho identityRetention constantCost (finite (suc (suc zero))) true + relaxed = weakenBound (finite≤ (suc≤ zero≤)) boundedTrue + + boundRelaxationPreservesData : Echo.residue (BoundedEcho.retained relaxed) ≡ true + boundRelaxationPreservesData = refl + + oneDoesNotFitZero : finite (suc zero) ≤G finite zero -> Impossible + oneDoesNotFitZero (finite≤ ()) + + noUnderstatedBound : BoundedEcho identityRetention constantCost (finite zero) true -> Impossible + noUnderstatedBound e = oneDoesNotFitZero (BoundedEcho.within e) + + -- Concrete use of the repaired surreal adapter: day access relaxes a proved + -- bound from one to three, and the certified data remains true. + dayTransport : BoundedEcho identityRetention constantCost + (finite (suc (suc (suc zero)))) true + dayTransport = Surreal.GradedSurrealModality.transportWithLoss + (Surreal.surrealEchoKnowledge Surreal.daySurrealAccess) + (Surreal.z≤n {n = suc (suc zero)}) (finite (suc zero)) boundedTrue + + dayTransportPreservesData : Echo.residue (BoundedEcho.retained dayTransport) ≡ true + dayTransportPreservesData = refl diff --git a/src/EpistemicTypes/EchoBridge.agda b/src/EpistemicTypes/EchoBridge.agda index 257bea8..ec3e3e1 100644 --- a/src/EpistemicTypes/EchoBridge.agda +++ b/src/EpistemicTypes/EchoBridge.agda @@ -2,14 +2,125 @@ module EpistemicTypes.EchoBridge where -open import Agda.Primitive using (lzero; lsuc) +open import Agda.Primitive using (lzero) +open import Agda.Builtin.Equality using (_≡_; refl) open import Agda.Builtin.Nat using (Nat; zero; suc; _+_) - open import EpistemicTypes.Base --- This module is only a bridge scaffold. --- Echo grades are min-plus-like loss/residue grades, while epistemic indices --- are standpoints. They compose, but they are not the same modality. +-- The certification shape follows canonical EchoResidue.EchoR. This small +-- interface uses builtins only; cross-repository correspondence is checked +-- separately. Cert is supplied by the consumer, so its intended meaning must +-- be reviewed. No recovery or information-loss bound follows from its name. +record Retention (Source Visible Residue : Set) : Set₁ where + field + observe : Source -> Visible + retain : Source -> Residue + Cert : Residue -> Visible -> Set + sound : (x : Source) -> Cert (retain x) (observe x) + +record Echo {A B R : Set} (C : Retention A B R) (y : B) : Set where + constructor echo + field + residue : R + certified : Retention.Cert C residue y + +lower : {A B R : Set} (C : Retention A B R) (x : A) -> + Echo C (Retention.observe C x) +lower C x = echo (Retention.retain C x) (Retention.sound C x) + +-- A candidate source must match both the observation and residue. This is +-- compatibility, not proof of historical origin: multiple sources can match +-- after information loss. Actual execution provenance needs another model. +record MatchesSource {A B R : Set} (C : Retention A B R) (x : A) + {y : B} (e : Echo C y) : Set where + constructor matchesSource + field + observationMatches : Retention.observe C x ≡ y + residueMatches : Retention.retain C x ≡ Echo.residue e + +lowerMatchesSource : {A B R : Set} (C : Retention A B R) (x : A) -> MatchesSource C x (lower C x) +lowerMatchesSource C x = matchesSource refl refl + +-- Recovering a source requires a left-inverse law for the ACTUAL observation +-- and residue functions. A certificate alone need not supply this capability. +record Recovery {A B R : Set} (C : Retention A B R) : Set where + field + recover : B -> R -> A + roundtrip : (x : A) -> recover (Retention.observe C x) (Retention.retain C x) ≡ x + +recoverLower : {A B R : Set} {C : Retention A B R} (rec : Recovery C) (x : A) -> + Recovery.recover rec (Retention.observe C x) (Echo.residue (lower C x)) ≡ x +recoverLower rec x = Recovery.roundtrip rec x + +recoverMatching : {A B R : Set} {C : Retention A B R} (rec : Recovery C) + (x : A) {y : B} (e : Echo C y) -> MatchesSource C x e -> + Recovery.recover rec y (Echo.residue e) ≡ x +recoverMatching rec x e (matchesSource refl refl) = Recovery.roundtrip rec x + +-- A migration can need less information than full source recovery. Its +-- implementation must factor the specified target behaviour through the +-- actual retained pair. This is the load-bearing sufficiency obligation. +record Migration {A B R T : Set} (C : Retention A B R) (target : A -> T) : Set where + field + migrate : B -> R -> T + adequate : (x : A) -> migrate (Retention.observe C x) (Retention.retain C x) ≡ target x + +migrateLower : {A B R T : Set} {C : Retention A B R} {target : A -> T} -> + (m : Migration C target) (x : A) -> + Migration.migrate m (Retention.observe C x) (Echo.residue (lower C x)) ≡ target x +migrateLower m x = Migration.adequate m x + +migrateMatching : {A B R T : Set} {C : Retention A B R} {target : A -> T} + (m : Migration C target) (x : A) {y : B} (e : Echo C y) -> MatchesSource C x e -> + Migration.migrate m y (Echo.residue e) ≡ target x +migrateMatching m x e (matchesSource refl refl) = Migration.adequate m x + +data Impossible : Set where + +private + sym : {A : Set} {x y : A} -> x ≡ y -> y ≡ x + sym refl = refl + + trans : {A : Set} {x y z : A} -> x ≡ y -> y ≡ z -> x ≡ z + trans refl q = q + + cong₂ : {A B T : Set} (f : A -> B -> T) {a a' : A} {b b' : B} -> + a ≡ a' -> b ≡ b' -> f a b ≡ f a' b' + cong₂ f refl refl = refl + +-- Equal retained observations cannot support differing required results. +-- This rules out ALL migrations with this signature, not just one candidate. +collisionForbidsMigration : {A B R T : Set} (C : Retention A B R) + (target : A -> T) (x x' : A) -> + Retention.observe C x ≡ Retention.observe C x' -> + Retention.retain C x ≡ Retention.retain C x' -> + (target x ≡ target x' -> Impossible) -> Migration C target -> Impossible +collisionForbidsMigration C target x x' sameVisible sameResidue distinct m = + distinct (trans (sym (Migration.adequate m x)) + (trans (cong₂ (Migration.migrate m) sameVisible sameResidue) + (Migration.adequate m x'))) + +-- Changing the observation/residue contract requires certificate transport. +-- This proves preservation of Cert, not an unstated source-recovery law. +record EchoMap {A B R A' B' R' : Set} + (C : Retention A B R) (D : Retention A' B' R') : Set where + field + mapVisible : B -> B' + mapResidue : R -> R' + preserves : {r : R} {y : B} -> Retention.Cert C r y -> + Retention.Cert D (mapResidue r) (mapVisible y) + +mapEcho : {A B R A' B' R' : Set} + {C : Retention A B R} {D : Retention A' B' R'} -> + (m : EchoMap C D) {y : B} -> Echo C y -> Echo D (EchoMap.mapVisible m y) +mapEcho m (echo r cert) = echo (EchoMap.mapResidue m r) (EchoMap.preserves m cert) + +EpistemicEcho : {K A B R : Set} -> Modality K lzero -> + K -> (C : Retention A B R) -> B -> Set +EpistemicEcho M κ C y = Modality.E M κ (Echo C y) + +-- Resource bounds are a separate axis. These are upper bounds on a supplied +-- residue measure; they are not Echo retention indices or physical timings. data Grade : Set where finite : Nat -> Grade infinity : Grade @@ -19,35 +130,59 @@ minNat zero n = zero minNat (suc m) zero = zero minNat (suc m) (suc n) = suc (minNat m n) --- Tropical "addition": choose the smaller grade. gradeMin : Grade -> Grade -> Grade gradeMin (finite m) (finite n) = finite (minNat m n) gradeMin (finite m) infinity = finite m gradeMin infinity (finite n) = finite n gradeMin infinity infinity = infinity --- Tropical "multiplication": compose costs by ordinary addition. gradePlus : Grade -> Grade -> Grade gradePlus (finite m) (finite n) = finite (m + n) gradePlus (finite m) infinity = infinity gradePlus infinity (finite n) = infinity gradePlus infinity infinity = infinity --- Echo is represented abstractly here. A value of Echo r A contains a --- residue token, not an exposed value of A. -record Echo (r : Grade) (A : Set) : Set₁ where - constructor echo +data _≤ℕ_ : Nat -> Nat -> Set where + zero≤ : {n : Nat} -> zero ≤ℕ n + suc≤ : {m n : Nat} -> m ≤ℕ n -> suc m ≤ℕ suc n + +≤ℕ-trans : {a b c : Nat} -> a ≤ℕ b -> b ≤ℕ c -> a ≤ℕ c +≤ℕ-trans zero≤ _ = zero≤ +≤ℕ-trans (suc≤ p) (suc≤ q) = suc≤ (≤ℕ-trans p q) + +≤ℕ-plus : (a b : Nat) -> a ≤ℕ (a + b) +≤ℕ-plus zero b = zero≤ +≤ℕ-plus (suc a) b = suc≤ (≤ℕ-plus a b) + +data _≤G_ : Grade -> Grade -> Set where + finite≤ : {m n : Nat} -> m ≤ℕ n -> finite m ≤G finite n + top≤ : {g : Grade} -> g ≤G infinity + +≤G-trans : {a b c : Grade} -> a ≤G b -> b ≤G c -> a ≤G c +≤G-trans (finite≤ p) (finite≤ q) = finite≤ (≤ℕ-trans p q) +≤G-trans p top≤ = top≤ + +≤G-plus : (a b : Grade) -> a ≤G gradePlus a b +≤G-plus (finite a) (finite b) = finite≤ (≤ℕ-plus a b) +≤G-plus (finite _) infinity = top≤ +≤G-plus infinity (finite _) = top≤ +≤G-plus infinity infinity = top≤ + +record BoundedEcho {A B R : Set} (C : Retention A B R) + (measure : R -> Grade) (budget : Grade) (y : B) : Set where + constructor bounded field - Residue : Set - residue : Residue - --- E κ (Echo r A): standpoint κ has epistemic access to an echo of A at --- irrecoverability grade r. -EpistemicEcho : - {K : Set} -> - Modality K (lsuc lzero) -> - K -> - Grade -> - Set -> - Set₁ -EpistemicEcho M κ r A = Modality.E M κ (Echo r A) + retained : Echo C y + within : measure (Echo.residue retained) ≤G budget + +weakenBound : {A B R : Set} {C : Retention A B R} {measure : R -> Grade} + {r r' : Grade} {y : B} -> r ≤G r' -> + BoundedEcho C measure r y -> BoundedEcho C measure r' y +weakenBound p (bounded e bound) = bounded e (≤G-trans bound p) + +weakenPreservesResidue : {A B R : Set} {C : Retention A B R} + {measure : R -> Grade} {r r' : Grade} {y : B} -> + (p : r ≤G r') (e : BoundedEcho C measure r y) -> + Echo.residue (BoundedEcho.retained (weakenBound p e)) ≡ + Echo.residue (BoundedEcho.retained e) +weakenPreservesResidue p e = refl diff --git a/src/EpistemicTypes/ProofTransport.agda b/src/EpistemicTypes/ProofTransport.agda index 566bf82..1fc2173 100644 --- a/src/EpistemicTypes/ProofTransport.agda +++ b/src/EpistemicTypes/ProofTransport.agda @@ -1,62 +1,28 @@ {-# OPTIONS --safe --without-K #-} ------------------------------------------------------------------------- --- Standpoint-indexed proof transport across trust boundaries. --- --- This module distinguishes three readings of one artefact: --- --- 1. von Neumann : the artefact is data/code — bytes that can cross --- any wall. Here this is `Artifact`, and the cheap --- statuses `Data` / `Code`. --- 2. Curry–Howard : a *checked* artefact can be a proof of a --- proposition. Here `Proof` / `ProofUnder m` are the --- statuses reached only by running a `Checker` over --- `Evidence` (a `verify`). --- 3. proof-carrying : code-plus-certificate can be re-checked by the --- code (PCC) consumer. Here `Evidence` is the certificate (it --- travels as data), and the consumer's `Checker` is --- the local verifier that re-establishes proofhood. --- --- The epistemic-types contribution is that *proofhood is standpoint-indexed*. --- A sender may hold an artefact as `View sender artifact Proof claim`, while --- the receiver initially holds the same bytes only as `Data`, `Claimed`, or --- `Receipt`. Transmission moves bytes, not proofhood: `transmit` downgrades a --- sender's proof to a receiver's `Receipt`. Proofhood is *recovered* on the --- receiver's side only when the receiver has an appropriate verification --- capability (`Checker`) and certificate (`Evidence`). --- --- The honesty discipline of this repository (see EpistemicTypes.Base) is kept: --- the only constructor of `View` that reaches a proof status demands a --- certifying mode, a checker, and evidence. No checker-free transport --- function `View sender a Proof c -> View receiver a Proof c` is exported. --- See `proofNeedsChecker` for the structural statement of this. ------------------------------------------------------------------------- - +-- Proof statuses carry a successful check and entail a caller-supplied meaning. +-- Soundness is relative to Meaning and the verifier's explicit soundness proof. +-- This module does not establish cryptography, physical facts, or runtime timing. module EpistemicTypes.ProofTransport - (Agent : Set) -- who holds a standpoint / view - (Claim : Set) -- what is asserted - (Artifact : Set) -- the von Neumann object: bytes, code, certificate + (Agent : Set) + (Claim : Set) + (Artifact : Set) + (Meaning : Agent -> Artifact -> Claim -> Set) + (Payload : Artifact -> Claim -> Set) where open import Agda.Primitive using (Level; _⊔_) open import Agda.Builtin.Equality using (_≡_; refl) - ------------------------------------------------------------------------- --- Tiny prelude. This library does not depend on a standard library --- (`agda --no-libraries`), so the few structural types are defined locally, --- mirroring the local ⊥/¬ pattern in EpistemicTypes.Examples. ------------------------------------------------------------------------- +open import Agda.Builtin.Bool using (Bool; true; false) data ⊥ : Set where - ¬_ : {ℓ : Level} -> Set ℓ -> Set ℓ ¬ A = A -> ⊥ infixr 4 _,_ infixr 2 _×_ - data Either {ℓ ℓ' : Level} (A : Set ℓ) (B : Set ℓ') : Set (ℓ ⊔ ℓ') where - left : A -> Either A B + left : A -> Either A B right : B -> Either A B record Σ {ℓ ℓ' : Level} (A : Set ℓ) (B : A -> Set ℓ') : Set (ℓ ⊔ ℓ') where @@ -70,250 +36,196 @@ A × B = Σ A (λ _ -> B) data Maybe {ℓ : Level} (A : Set ℓ) : Set ℓ where nothing : Maybe A - just : A -> Maybe A - ------------------------------------------------------------------------- --- Verification / attestation modes. ------------------------------------------------------------------------- + just : A -> Maybe A data Mode : Set where - Public : Mode -- publicly checkable; transferable - Designated : Agent -> Mode -- "Designated Agent": bound to one party - IssuerMediated : Mode -- needs trust in the issuer - EnvironmentMediated : Mode -- needs a runtime / environment context - OpaqueReceipt : Mode -- only acknowledges receipt; never certifies - ------------------------------------------------------------------------- --- Epistemic status of an artefact, relative to a holder, w.r.t. a claim. ------------------------------------------------------------------------- + Public : Mode + Designated : Agent -> Mode + IssuerMediated EnvironmentMediated OpaqueReceipt : Mode data Status : Set where - Data : Status -- von Neumann bytes; asserts nothing - Code : Status -- executable bytes; still just data to a receiver - Claimed : Status -- a claim is asserted, but unverified - Receipt : Status -- an acknowledgement; not proof of the claim - Proof : Status -- a checked proof of the claim (mode forgotten) - ProofUnder : Mode -> Status -- a checked proof under a specific mode/standpoint - ------------------------------------------------------------------------- --- Gaps: reasons an upgrade to Proof fails. ------------------------------------------------------------------------- + Data Code Claimed Receipt Proof : Status + ProofUnder : Mode -> Status data Gap : Set where - TrivialGap : Gap -- nothing else to do, but a checker is still required - DesignatedGap : Gap -- the designation does not match this holder - EnvironmentGap : Gap -- environment / context absent - IssuerTrustGap : Gap -- issuer not trusted by this holder - OpaqueGap : Gap -- receipt-only; the underlying claim is not certified - MissingChecker : Gap -- the holder lacks the checking capability - MissingEvidence : Gap -- the holder lacks the certificate / evidence - MissingContext : Gap -- the holder lacks the ambient context - ------------------------------------------------------------------------- --- A Checker is a holder's *capability* to verify, in a given mode, that an --- artefact certifies a claim. Capabilities — not certificates — are the part --- that does not automatically cross a trust boundary. ------------------------------------------------------------------------- + TrivialGap DesignatedGap EnvironmentGap IssuerTrustGap OpaqueGap : Gap + MissingChecker MissingEvidence MissingContext InvalidEvidence : Gap + +-- Evidence carries a payload, but the payload's existence never proves Meaning. +data Evidence : Mode -> Artifact -> Claim -> Set where + publicEv : {a : Artifact} {c : Claim} -> Payload a c -> Evidence Public a c + designatedEv : {a : Artifact} {c : Claim} (d : Agent) -> + Payload a c -> Evidence (Designated d) a c + issuerEv : {a : Artifact} {c : Claim} -> Payload a c -> Evidence IssuerMediated a c + envEv : {a : Artifact} {c : Claim} -> Payload a c -> Evidence EnvironmentMediated a c + receiptEv : {a : Artifact} {c : Claim} -> Payload a c -> Evidence OpaqueReceipt a c + +evidencePayload : {m : Mode} {a : Artifact} {c : Claim} -> Evidence m a c -> Payload a c +evidencePayload (publicEv p) = p +evidencePayload (designatedEv _ p) = p +evidencePayload (issuerEv p) = p +evidencePayload (envEv p) = p +evidencePayload (receiptEv p) = p + +-- A real checking function plus a proof that acceptance entails the exact claim +-- for this holder and artifact. Completeness is deliberately not required. +record CertificateCheck (holder : Agent) (a : Artifact) (c : Claim) : Set where + constructor certificateCheck + field + check : Payload a c -> Bool + sound : (p : Payload a c) -> check p ≡ true -> Meaning holder a c data Checker (holder : Agent) : Mode -> Artifact -> Claim -> Set where - -- Public verification is agent-agnostic: any holder can run it. - publicCheck : {a : Artifact} {c : Claim} -> Checker holder Public a c - -- Designated verification binds the designated party to the holder itself. - -- There is deliberately NO constructor designated to another agent. - designatedCheck : {a : Artifact} {c : Claim} -> Checker holder (Designated holder) a c - -- Issuer-mediated and environment-mediated capabilities for the holder. - issuerCheck : {a : Artifact} {c : Claim} -> Checker holder IssuerMediated a c - envCheck : {a : Artifact} {c : Claim} -> Checker holder EnvironmentMediated a c - -- An opaque receipt is the capability only to acknowledge receipt — never to - -- certify the underlying claim. (Note: `Certifying OpaqueReceipt` is empty.) - receiptCheck : {a : Artifact} {c : Claim} -> Checker holder OpaqueReceipt a c - --- Which modes actually *certify* a claim, i.e. may yield `Proof`. --- `OpaqueReceipt` is deliberately excluded — see `opaqueNotCertifying`. + publicCheck : {a : Artifact} {c : Claim} -> + CertificateCheck holder a c -> Checker holder Public a c + designatedCheck : {a : Artifact} {c : Claim} -> + CertificateCheck holder a c -> Checker holder (Designated holder) a c + issuerCheck : {a : Artifact} {c : Claim} -> + CertificateCheck holder a c -> Checker holder IssuerMediated a c + envCheck : {a : Artifact} {c : Claim} -> + CertificateCheck holder a c -> Checker holder EnvironmentMediated a c + receiptCheck : {a : Artifact} {c : Claim} -> Checker holder OpaqueReceipt a c + data Certifying : Mode -> Set where - certPublic : Certifying Public + certPublic : Certifying Public certDesignated : {d : Agent} -> Certifying (Designated d) - certIssuer : Certifying IssuerMediated - certEnv : Certifying EnvironmentMediated + certIssuer : Certifying IssuerMediated + certEnv : Certifying EnvironmentMediated --- Evidence is the certificate payload. It is plain data and may cross the --- boundary freely (von Neumann). Possessing evidence is not possessing proof; --- proof additionally requires the holder's own certifying `Checker`. -data Evidence : Mode -> Artifact -> Claim -> Set where - publicEv : {a : Artifact} {c : Claim} -> Evidence Public a c - designatedEv : {a : Artifact} {c : Claim} (d : Agent) -> Evidence (Designated d) a c - issuerEv : {a : Artifact} {c : Claim} -> Evidence IssuerMediated a c - envEv : {a : Artifact} {c : Claim} -> Evidence EnvironmentMediated a c - receiptEv : {a : Artifact} {c : Claim} -> Evidence OpaqueReceipt a c - ------------------------------------------------------------------------- --- The standpoint-indexed judgement. --- --- View holder artifact status claim --- "the holder regards `artifact` at epistemic `status` w.r.t. `claim`." --- --- The cheap statuses (Data/Code/Claimed/Receipt) are freely introducible. --- A proof status is NOT: the only route to `ProofUnder m` is `asProofUnder`, --- which demands `Certifying m`, a `Checker`, and `Evidence`; and `Proof` --- is reached only by forgetting the mode of a `ProofUnder`. ------------------------------------------------------------------------- +runChecker : + {holder : Agent} {a : Artifact} {m : Mode} {c : Claim} -> + Checker holder m a c -> Evidence m a c -> Bool +runChecker (publicCheck v) ev = CertificateCheck.check v (evidencePayload ev) +runChecker (designatedCheck v) ev = CertificateCheck.check v (evidencePayload ev) +runChecker (issuerCheck v) ev = CertificateCheck.check v (evidencePayload ev) +runChecker (envCheck v) ev = CertificateCheck.check v (evidencePayload ev) +runChecker receiptCheck _ = false + +checkerSound : + {holder : Agent} {a : Artifact} {m : Mode} {c : Claim} -> + Certifying m -> (ck : Checker holder m a c) -> (ev : Evidence m a c) -> + runChecker ck ev ≡ true -> Meaning holder a c +checkerSound certPublic (publicCheck v) ev ok = CertificateCheck.sound v (evidencePayload ev) ok +checkerSound certDesignated (designatedCheck v) ev ok = CertificateCheck.sound v (evidencePayload ev) ok +checkerSound certIssuer (issuerCheck v) ev ok = CertificateCheck.sound v (evidencePayload ev) ok +checkerSound certEnv (envCheck v) ev ok = CertificateCheck.sound v (evidencePayload ev) ok data View (holder : Agent) : Artifact -> Status -> Claim -> Set where - asData : {a : Artifact} {c : Claim} -> View holder a Data c - asCode : {a : Artifact} {c : Claim} -> View holder a Code c + asData : {a : Artifact} {c : Claim} -> View holder a Data c + asCode : {a : Artifact} {c : Claim} -> View holder a Code c asClaimed : {a : Artifact} {c : Claim} -> View holder a Claimed c asReceipt : {a : Artifact} {c : Claim} -> View holder a Receipt c asProofUnder : {a : Artifact} {m : Mode} {c : Claim} -> - Certifying m -> Checker holder m a c -> Evidence m a c -> - View holder a (ProofUnder m) c + Certifying m -> (ck : Checker holder m a c) -> (ev : Evidence m a c) -> + runChecker ck ev ≡ true -> View holder a (ProofUnder m) c forgetMode : {a : Artifact} {m : Mode} {c : Claim} -> View holder a (ProofUnder m) c -> View holder a Proof c ------------------------------------------------------------------------- --- A trust boundary, directed from a sender to a receiver. ------------------------------------------------------------------------- +-- The semantic guarantee holds even for clients using the constructors directly. +proofSound : + {holder : Agent} {a : Artifact} {c : Claim} -> + View holder a Proof c -> Meaning holder a c +proofSound (forgetMode (asProofUnder cert ck ev ok)) = checkerSound cert ck ev ok -infix 4 _⇒_ +proofCannotSupportFalse : + {holder : Agent} {a : Artifact} {c : Claim} -> + ¬ Meaning holder a c -> ¬ View holder a Proof c +proofCannotSupportFalse notMeaning proof = notMeaning (proofSound proof) +infix 4 _⇒_ record Boundary : Set where constructor _⇒_ field - from : Agent - to : Agent + from to : Agent open Boundary public --- Transmission across a boundary. A sender's *proof* arrives at the receiver --- only as a *receipt*: the bytes cross the wall, the proofhood does not. --- This is the conservative half of the story — transport alone never upgrades. transmit : - {a : Artifact} {c : Claim} -> - (b : Boundary) -> - View (from b) a Proof c -> - View (to b) a Receipt c + {a : Artifact} {c : Claim} -> (b : Boundary) -> + View (from b) a Proof c -> View (to b) a Receipt c transmit b _ = asReceipt ------------------------------------------------------------------------- --- verify: with a matching checker and evidence, upgrade Data to Proof. --- The opaque-receipt capability yields a Gap, never a proof of the claim. ------------------------------------------------------------------------- +verifyCertifying : + {holder : Agent} {a : Artifact} {m : Mode} {c : Claim} -> + Certifying m -> (ck : Checker holder m a c) -> Evidence m a c -> + Either Gap (View holder a Proof c) +verifyCertifying cert ck ev with runChecker ck ev in accepted +... | true = right (forgetMode (asProofUnder cert ck ev accepted)) +... | false = left InvalidEvidence verify : {holder : Agent} {a : Artifact} {m : Mode} {c : Claim} -> - Checker holder m a c -> - Evidence m a c -> - View holder a Data c -> + Checker holder m a c -> Evidence m a c -> View holder a Data c -> Either Gap (View holder a Proof c) -verify publicCheck ev _ = right (forgetMode (asProofUnder certPublic publicCheck ev)) -verify designatedCheck ev _ = right (forgetMode (asProofUnder certDesignated designatedCheck ev)) -verify issuerCheck ev _ = right (forgetMode (asProofUnder certIssuer issuerCheck ev)) -verify envCheck ev _ = right (forgetMode (asProofUnder certEnv envCheck ev)) -verify receiptCheck _ _ = left OpaqueGap - ------------------------------------------------------------------------- --- The central positive theorem. --- --- A receiver holding the artefact as Data, *and* a checker and evidence, can --- upgrade to Proof. The sender's proof and the boundary are present but --- deliberately unused (`_`): transmission alone does not justify the upgrade — --- only the receiver's own checker and evidence do. ------------------------------------------------------------------------- +verify (publicCheck v) ev _ = verifyCertifying certPublic (publicCheck v) ev +verify (designatedCheck v) ev _ = verifyCertifying certDesignated (designatedCheck v) ev +verify (issuerCheck v) ev _ = verifyCertifying certIssuer (issuerCheck v) ev +verify (envCheck v) ev _ = verifyCertifying certEnv (envCheck v) ev +verify receiptCheck _ _ = left OpaqueGap +-- This returns a checked result, not a promise that arbitrary evidence succeeds. checkableTransportUpgrades : - {sender receiver : Agent} {a : Artifact} {m : Mode} {c : Claim} -> - View sender a Proof c -> -- the sender already had a proof ... - Boundary -> -- ... it crossed a boundary ... - View receiver a Data c -> -- ... and the receiver holds the bytes, - Checker receiver m a c -> -- but proofhood is recovered only via the - Evidence m a c -> -- receiver's own checker and evidence. - Either Gap (View receiver a Proof c) -checkableTransportUpgrades _ _ dv ck ev = verify ck ev dv - ------------------------------------------------------------------------- --- Public (transferable) attestation. ------------------------------------------------------------------------- + {a : Artifact} {m : Mode} {c : Claim} -> + (b : Boundary) -> View (from b) a Proof c -> View (to b) a Data c -> + Checker (to b) m a c -> Evidence m a c -> + Either Gap (View (to b) a Proof c) +checkableTransportUpgrades b _ dv ck ev = verify ck ev dv --- A public certificate plus a public checker upgrades data to proof. publicTransfer : {receiver : Agent} {a : Artifact} {c : Claim} -> - Checker receiver Public a c -> - Evidence Public a c -> - View receiver a Data c -> - Either Gap (View receiver a Proof c) + Checker receiver Public a c -> Evidence Public a c -> + View receiver a Data c -> Either Gap (View receiver a Proof c) publicTransfer = verify --- Public verification is not bound to one designated receiver: a public --- checker held by `r` is reconstructible by any other agent `q`. +-- Holder-dependent meanings cannot be silently transported. A caller supplies +-- the semantic implication, while the executable payload check is preserved. publicIsPortable : {r q : Agent} {a : Artifact} {c : Claim} -> + (Meaning r a c -> Meaning q a c) -> Checker r Public a c -> Checker q Public a c -publicIsPortable publicCheck = publicCheck - ------------------------------------------------------------------------- --- Designated (deniable) attestation. ------------------------------------------------------------------------- +publicIsPortable transport (publicCheck v) = publicCheck + (certificateCheck (CertificateCheck.check v) + (λ p ok -> transport (CertificateCheck.sound v p ok))) --- The designated receiver can verify a designated attestation addressed to it. designatedTransfer : {receiver : Agent} {a : Artifact} {c : Claim} -> Checker receiver (Designated receiver) a c -> - Evidence (Designated receiver) a c -> - View receiver a Data c -> + Evidence (Designated receiver) a c -> View receiver a Data c -> Either Gap (View receiver a Proof c) designatedTransfer = verify --- But a designated checker pins the designated party to its own holder. Thus --- no third party can hold the checker for someone else's designation: that --- gives the deniability of a designated-verifier attestation by construction. --- (See EpistemicTypes.ProofTransportExample for the concrete Bob case.) designatedBindsHolder : {holder d : Agent} {a : Artifact} {c : Claim} -> Checker holder (Designated d) a c -> d ≡ holder -designatedBindsHolder designatedCheck = refl - ------------------------------------------------------------------------- --- Receipt-only (opaque) attestation never certifies the underlying claim. ------------------------------------------------------------------------- +designatedBindsHolder (designatedCheck _) = refl opaqueNotCertifying : ¬ Certifying OpaqueReceipt opaqueNotCertifying () verifyReceiptIsGap : {holder : Agent} {a : Artifact} {c : Claim} -> - (ev : Evidence OpaqueReceipt a c) -> - (v : View holder a Data c) -> + (ev : Evidence OpaqueReceipt a c) -> (v : View holder a Data c) -> verify {holder} receiptCheck ev v ≡ left OpaqueGap verifyReceiptIsGap ev v = refl ------------------------------------------------------------------------- --- A resource-gathering entry point that names the missing-resource gaps. --- This is the partial / discovery layer above `verify`: before you can run a --- check you must actually possess the capability and the certificate. ------------------------------------------------------------------------- - tryUpgrade : {holder : Agent} {a : Artifact} {m : Mode} {c : Claim} -> - Maybe (Checker holder m a c) -> - Maybe (Evidence m a c) -> - View holder a Data c -> - Either Gap (View holder a Proof c) -tryUpgrade nothing _ _ = left MissingChecker -tryUpgrade (just _) nothing _ = left MissingEvidence + Maybe (Checker holder m a c) -> Maybe (Evidence m a c) -> + View holder a Data c -> Either Gap (View holder a Proof c) +tryUpgrade nothing _ _ = left MissingChecker +tryUpgrade (just _) nothing _ = left MissingEvidence tryUpgrade (just ck) (just ev) v = verify ck ev v ------------------------------------------------------------------------- --- No smuggling. --- --- Every proof a holder possesses is backed by *that holder's* own certifying --- mode, checker, and evidence. Equivalently: a `View holder a Proof c` can --- never be obtained witness-free, so in particular there is no exported --- View sender a Proof c -> View receiver a Proof c --- (such a function would have to fabricate the receiver's checker+evidence). ------------------------------------------------------------------------- - proofNeedsChecker : {holder : Agent} {a : Artifact} {c : Claim} -> View holder a Proof c -> Σ Mode (λ m -> Certifying m × Checker holder m a c × Evidence m a c) -proofNeedsChecker (forgetMode (asProofUnder cert ck ev)) = _ , cert , ck , ev +proofNeedsChecker (forgetMode (asProofUnder cert ck ev ok)) = _ , cert , ck , ev + +proofHasSuccessfulCheck : + {holder : Agent} {a : Artifact} {c : Claim} -> + View holder a Proof c -> + Σ Mode (λ m -> Σ (Checker holder m a c) + (λ ck -> Σ (Evidence m a c) (λ ev -> runChecker ck ev ≡ true))) +proofHasSuccessfulCheck (forgetMode (asProofUnder cert ck ev ok)) = _ , ck , ev , ok diff --git a/src/EpistemicTypes/ProofTransportExample.agda b/src/EpistemicTypes/ProofTransportExample.agda index cd5f692..728af25 100644 --- a/src/EpistemicTypes/ProofTransportExample.agda +++ b/src/EpistemicTypes/ProofTransportExample.agda @@ -1,114 +1,186 @@ {-# OPTIONS --safe --without-K #-} ------------------------------------------------------------------------- --- A K9-SVC / A2ML-style attestation, modelled with proof transport. --- --- issuer K9SVC --- receiver Alice --- third party Bob --- claim ActionWasPerformed --- artifact AttestationBlob --- --- Three cases are exhibited: --- (1) the blob is raw Data for Alice; --- (2) Alice upgrades it to Proof with her designated checker + evidence; --- (3) Bob, across the boundary, holds only a Receipt — and *cannot* hold the --- designated capability that was issued to Alice — UNLESS the attestation --- is public, which is portable to any agent. ------------------------------------------------------------------------- - +-- Executable Boolean certificate checks, semantic soundness, and countercases. +-- ArtifactIsTrue means a Boolean equality, not that a physical action occurred. module EpistemicTypes.ProofTransportExample where +open import Agda.Builtin.Bool using (Bool; true; false) open import Agda.Builtin.Equality using (_≡_; refl) data Agent : Set where - K9SVC : Agent - Alice : Agent - Bob : Agent + K9SVC Alice Bob : Agent data Claim : Set where - ActionWasPerformed : Claim + ArtifactIsTrue ImpossibleClaim : Claim + +Artifact : Set +Artifact = Bool + +data NoMeaning : Set where + +Meaning : Agent -> Artifact -> Claim -> Set +Meaning _ a ArtifactIsTrue = a ≡ true +Meaning _ _ ImpossibleClaim = NoMeaning -data Artifact : Set where - AttestationBlob : Artifact +Payload : Artifact -> Claim -> Set +Payload _ _ = Bool --- Instantiate the proof-transport core at these concrete carriers. -open import EpistemicTypes.ProofTransport Agent Claim Artifact +open import EpistemicTypes.ProofTransport Agent Claim Artifact Meaning Payload ----------------------------------------------------------------------- --- Case 1: the attestation blob is just data for Alice. ----------------------------------------------------------------------- +checkPayload : (a : Artifact) -> (c : Claim) -> Payload a c -> Bool +checkPayload true ArtifactIsTrue p = p +checkPayload false ArtifactIsTrue _ = false +checkPayload _ ImpossibleClaim _ = false -aliceRaw : View Alice AttestationBlob Data ActionWasPerformed +checkPayloadSound : + (holder : Agent) (a : Artifact) (c : Claim) (p : Payload a c) -> + checkPayload a c p ≡ true -> Meaning holder a c +checkPayloadSound _ true ArtifactIsTrue true _ = refl +checkPayloadSound _ true ArtifactIsTrue false () +checkPayloadSound _ false ArtifactIsTrue p () +checkPayloadSound _ true ImpossibleClaim p () +checkPayloadSound _ false ImpossibleClaim p () + +verifier : (holder : Agent) (a : Artifact) (c : Claim) -> CertificateCheck holder a c +verifier holder a c = certificateCheck (checkPayload a c) (checkPayloadSound holder a c) + +aliceRaw : View Alice true Data ArtifactIsTrue aliceRaw = asData ----------------------------------------------------------------------- --- Case 2: Alice has the designated checker and the matching evidence, so she --- upgrades the blob to a proof of ActionWasPerformed. ----------------------------------------------------------------------- +aliceChecker : Checker Alice (Designated Alice) true ArtifactIsTrue +aliceChecker = designatedCheck (verifier Alice true ArtifactIsTrue) -aliceChecker : Checker Alice (Designated Alice) AttestationBlob ActionWasPerformed -aliceChecker = designatedCheck +aliceEvidence : Evidence (Designated Alice) true ArtifactIsTrue +aliceEvidence = designatedEv Alice true -aliceEvidence : Evidence (Designated Alice) AttestationBlob ActionWasPerformed -aliceEvidence = designatedEv Alice +aliceProof : View Alice true Proof ArtifactIsTrue +aliceProof = forgetMode (asProofUnder certDesignated aliceChecker aliceEvidence refl) -aliceUpgrade : Either Gap (View Alice AttestationBlob Proof ActionWasPerformed) +aliceUpgrade : Either Gap (View Alice true Proof ArtifactIsTrue) aliceUpgrade = designatedTransfer aliceChecker aliceEvidence aliceRaw -aliceProof : View Alice AttestationBlob Proof ActionWasPerformed -aliceProof = forgetMode (asProofUnder certDesignated aliceChecker aliceEvidence) - --- The upgrade really does succeed (it computes to `right aliceProof`). aliceUpgradeSucceeds : aliceUpgrade ≡ right aliceProof aliceUpgradeSucceeds = refl ----------------------------------------------------------------------- --- Case 3a: across the Alice ⇒ Bob boundary, Bob's view of the proof degrades --- to a mere receipt. The bytes crossed; the proofhood did not. ----------------------------------------------------------------------- +aliceProofHasMeaning : Meaning Alice true ArtifactIsTrue +aliceProofHasMeaning = proofSound aliceProof aliceToBob : Boundary aliceToBob = Alice ⇒ Bob -bobReceipt : View Bob AttestationBlob Receipt ActionWasPerformed +bobReceipt : View Bob true Receipt ArtifactIsTrue bobReceipt = transmit aliceToBob aliceProof ----------------------------------------------------------------------- --- Case 3b: Bob cannot manufacture the *designated* proof. The designated --- capability is bound to Alice, and Alice ≢ Bob, so the type --- Checker Bob (Designated Alice) AttestationBlob ActionWasPerformed --- is uninhabited. This is the deniability of a designated attestation. ----------------------------------------------------------------------- - Alice≢Bob : ¬ (Alice ≡ Bob) Alice≢Bob () -bobHasNoDesignatedChecker : - ¬ Checker Bob (Designated Alice) AttestationBlob ActionWasPerformed +bobHasNoDesignatedChecker : ¬ Checker Bob (Designated Alice) true ArtifactIsTrue bobHasNoDesignatedChecker ck = Alice≢Bob (designatedBindsHolder ck) ----------------------------------------------------------------------- --- Case 3c: but if the attestation is *public*, Bob upgrades like anyone else, --- because public checking is portable from Alice to Bob. ----------------------------------------------------------------------- - -bobPublicChecker : Checker Bob Public AttestationBlob ActionWasPerformed -bobPublicChecker = publicIsPortable {Alice} {Bob} publicCheck - -bobPublicUpgrade : - Evidence Public AttestationBlob ActionWasPerformed -> - Either Gap (View Bob AttestationBlob Proof ActionWasPerformed) -bobPublicUpgrade ev = publicTransfer bobPublicChecker ev asData - ----------------------------------------------------------------------- --- A receipt-only attestation never upgrades to proof of the claim, for anyone. ----------------------------------------------------------------------- - -bobBlob : View Bob AttestationBlob Data ActionWasPerformed -bobBlob = asData - -bobReceiptStuck : - (ev : Evidence OpaqueReceipt AttestationBlob ActionWasPerformed) -> - verify receiptCheck ev bobBlob ≡ left OpaqueGap -bobReceiptStuck ev = verifyReceiptIsGap ev bobBlob +-- This concrete meaning is holder-independent, so the required implication is id. +bobPublicChecker : Checker Bob Public true ArtifactIsTrue +bobPublicChecker = publicIsPortable {r = Alice} {q = Bob} (λ p -> p) + (publicCheck (verifier Alice true ArtifactIsTrue)) + +bobPublicProof : View Bob true Proof ArtifactIsTrue +bobPublicProof = forgetMode + (asProofUnder certPublic bobPublicChecker (publicEv true) refl) + +bobPublicUpgradeSucceeds : + publicTransfer bobPublicChecker (publicEv true) asData ≡ right bobPublicProof +bobPublicUpgradeSucceeds = refl + +-- Negative data cases are successful proofs ABOUT actual rejection computations. +badPayloadRejected : + publicTransfer bobPublicChecker (publicEv false) asData ≡ left InvalidEvidence +badPayloadRejected = refl + +tamperedArtifactRejected : + verify (publicCheck (verifier Bob false ArtifactIsTrue)) + (publicEv true) asData ≡ left InvalidEvidence +tamperedArtifactRejected = refl + +falseClaimRejected : + verify (publicCheck (verifier Bob true ImpossibleClaim)) + (publicEv true) asData ≡ left InvalidEvidence +falseClaimRejected = refl + +falseClaimHasNoProof : ¬ View Bob true Proof ImpossibleClaim +falseClaimHasNoProof = proofCannotSupportFalse (λ ()) + +-- Any attempted generic fabrication function is refuted by the false instance. +noArbitraryProofStatuses : + ¬ ((c : Claim) -> View Bob true Proof c) +noArbitraryProofStatuses manufacture = falseClaimHasNoProof (manufacture ImpossibleClaim) + +receiptModeRejected : + verify {holder = Bob} {a = true} {c = ArtifactIsTrue} + receiptCheck (receiptEv true) asData ≡ left OpaqueGap +receiptModeRejected = refl + +missingCheckerRejected : + tryUpgrade {holder = Bob} {a = true} {m = Public} {c = ArtifactIsTrue} + nothing (just (publicEv true)) asData ≡ left MissingChecker +missingCheckerRejected = refl + +missingEvidenceRejected : + tryUpgrade (just bobPublicChecker) nothing asData ≡ left MissingEvidence +missingEvidenceRejected = refl + +-- Issuer/environment modes use the SAME semantic soundness obligation. +issuerProof : View Alice true Proof ArtifactIsTrue +issuerProof = forgetMode (asProofUnder certIssuer + (issuerCheck (verifier Alice true ArtifactIsTrue)) (issuerEv true) refl) + +issuerAccepts : + verify (issuerCheck (verifier Alice true ArtifactIsTrue)) (issuerEv true) asData + ≡ right issuerProof +issuerAccepts = refl + +issuerRejectsFalse : + verify (issuerCheck (verifier Alice true ImpossibleClaim)) (issuerEv true) asData + ≡ left InvalidEvidence +issuerRejectsFalse = refl + +environmentProof : View Alice true Proof ArtifactIsTrue +environmentProof = forgetMode (asProofUnder certEnv + (envCheck (verifier Alice true ArtifactIsTrue)) (envEv true) refl) + +environmentAccepts : + verify (envCheck (verifier Alice true ArtifactIsTrue)) (envEv true) asData + ≡ right environmentProof +environmentAccepts = refl + +environmentRejectsFalse : + verify (envCheck (verifier Alice true ImpossibleClaim)) (envEv true) asData + ≡ left InvalidEvidence +environmentRejectsFalse = refl + +designatedRejectsFalse : + verify (designatedCheck (verifier Alice true ImpossibleClaim)) + (designatedEv Alice true) asData ≡ left InvalidEvidence +designatedRejectsFalse = refl + +-- A holder-sensitive interpretation demonstrates why portability needs a proof. +-- Alice knows her own identity; that fact cannot be relabelled as Bob = Alice. +module HolderBoundary where + LocalMeaning : Agent -> Artifact -> Claim -> Set + LocalMeaning holder _ _ = holder ≡ Alice + + import EpistemicTypes.ProofTransport as Core + module Local = Core Agent Claim Artifact LocalMeaning Payload + + aliceCheck : Local.CertificateCheck Alice true ArtifactIsTrue + aliceCheck = Local.certificateCheck (λ _ -> true) (λ _ _ -> refl) + + aliceLocalProof : Local.View Alice true Local.Proof ArtifactIsTrue + aliceLocalProof = Local.forgetMode (Local.asProofUnder Local.certPublic + (Local.publicCheck aliceCheck) (Local.publicEv true) refl) + + noBobProof : Local.¬ Local.View Bob true Local.Proof ArtifactIsTrue + noBobProof = Local.proofCannotSupportFalse (λ ()) + + noSilentHolderTransport : + Local.¬ (Local.View Alice true Local.Proof ArtifactIsTrue -> + Local.View Bob true Local.Proof ArtifactIsTrue) + noSilentHolderTransport move = noBobProof (move aliceLocalProof) diff --git a/src/EpistemicTypes/ReadConsistency.agda b/src/EpistemicTypes/ReadConsistency.agda index 57a4322..0b72914 100644 --- a/src/EpistemicTypes/ReadConsistency.agda +++ b/src/EpistemicTypes/ReadConsistency.agda @@ -1,243 +1,173 @@ {-# OPTIONS --safe --without-K #-} ------------------------------------------------------------------------- --- Version-monotone read-consistency RECOVERY LIVENESS, as a concrete --- instance over the canonical epistemic framework. --- --- This module is the Agda upstream draft of typed-wasm's Idris --- TypedWasm.ABI.Epistemic (Level 12, shared-memory read consistency). --- The Idris file proves there is no permanently-stuck stale state: a --- single re-sync always recovers freshness, and freshness propagates --- across any number of intervening writes via one re-sync. Here those --- same liveness theorems are re-derived over Nat versions, and the --- model is wired to the canonical EpistemicTypes.Access Preorder / --- AccessibleModality so that "versions-as-standpoints" is an actual --- instance of the standpoint-indexed accessible modality, not a --- parallel ad-hoc theory. --- --- Standpoints are versions (a Version = Nat). v ≤κ v' reads "v' is at --- least as informed/advanced as v" — i.e. v' is a later (or equal) --- version, and knowledge at v can be transported to v'. This matches --- the canonical Access reading exactly: transport flows from the less --- informed standpoint to the more informed one. --- --- Estate boundary note (cf. Epistemic.idr header): the Idris file flags --- this as a possibly-DIFFERENT problem from the canonical standpoint --- modality. This module is the affirmative answer to the OPEN DESIGN --- QUESTION it poses: versions DO instantiate the canonical --- AccessibleModality (Version-as-standpoint, ≤ on Nat as access), and --- the read-consistency liveness theorems are theorems ABOUT that --- instance. ------------------------------------------------------------------------- - module EpistemicTypes.ReadConsistency where -open import Agda.Primitive using (Level; lzero; lsuc) +open import Agda.Primitive using (Level; lzero) open import Agda.Builtin.Equality using (_≡_; refl) open import Agda.Builtin.Nat using (Nat; zero; suc) +open import EpistemicTypes.Access using (Preorder) -open import EpistemicTypes.Base -open import EpistemicTypes.Access - ------------------------------------------------------------------------- --- Versions, ordering, and the empty type ------------------------------------------------------------------------- +-- A pure, finite store-history model. A write extends a particular history; +-- its version is derived from that history, not supplied by the caller. +-- This is not a shared-memory implementation or a scheduler-liveness proof. +data Store (A : Set) : Set where + initial : A -> Store A + write : Store A -> A -> Store A --- A version is just a Nat. Each write increments it (modelled by suc). Version : Set Version = Nat +version : {A : Set} -> Store A -> Version +version (initial _) = zero +version (write s _) = suc (version s) + +contents : {A : Set} -> Store A -> A +contents (initial a) = a +contents (write _ a) = a + data ⊥ : Set where ¬_ : {ℓ : Level} -> Set ℓ -> Set ℓ ¬ A = A -> ⊥ --- Less-than-or-equal on versions. This is the accessibility relation: --- v ≤ v' means v' is the same or a later version. +cong : {A B : Set} {x y : A} -> (f : A -> B) -> x ≡ y -> f x ≡ f y +cong f refl = refl + +trans : {A : Set} {x y z : A} -> x ≡ y -> y ≡ z -> x ≡ z +trans refl q = q + +subst : {A : Set} (P : A -> Set) {x y : A} -> x ≡ y -> P x -> P y +subst P refl px = px + data _≤_ : Version -> Version -> Set where z≤n : {n : Version} -> zero ≤ n s≤s : {m n : Version} -> m ≤ n -> suc m ≤ suc n --- Strict less-than: v < v' ≜ suc v ≤ v'. Used for "a write has happened". -_<_ : Version -> Version -> Set -m < n = suc m ≤ n - ≤-refl : {n : Version} -> n ≤ n -≤-refl {zero} = z≤n +≤-refl {zero} = z≤n ≤-refl {suc n} = s≤s ≤-refl ≤-trans : {l m n : Version} -> l ≤ m -> m ≤ n -> l ≤ n -≤-trans z≤n _ = z≤n -≤-trans (s≤s p) (s≤s q) = s≤s (≤-trans p q) +≤-trans z≤n _ = z≤n +≤-trans (s≤s p) (s≤s q) = s≤s (≤-trans p q) --- < is irreflexive: v < v is uninhabited. Mirrors Idris ltIrreflexive. -<-irrefl : {n : Version} -> ¬ (n < n) -<-irrefl {suc n} (s≤s p) = <-irrefl p +≤-step : {m n : Version} -> m ≤ n -> m ≤ suc n +≤-step z≤n = z≤n +≤-step (s≤s p) = s≤s (≤-step p) --- A strict-less witness is itself a (weak) ≤ witness. -<⇒≤ : {m n : Version} -> m < n -> m ≤ n -<⇒≤ {zero} _ = z≤n -<⇒≤ {suc m} (s≤s p) = s≤s (<⇒≤ p) +_<_ : Version -> Version -> Set +m < n = suc m ≤ n ------------------------------------------------------------------------- --- The canonical Preorder instance: versions ordered by ≤ ------------------------------------------------------------------------- +<-irrefl : {n : Version} -> ¬ (n < n) +<-irrefl {suc n} (s≤s p) = <-irrefl p --- Versions-as-standpoints: the access relation of the canonical --- EpistemicTypes.Access.Preorder, instantiated at K = Version with ≤. +-- Numeric order is a preorder, but does not itself refresh data or evidence. versionPreorder : Preorder {rℓ = lzero} Version -Preorder._≤κ_ versionPreorder = _≤_ -Preorder.refl≤ versionPreorder = ≤-refl +Preorder._≤κ_ versionPreorder = _≤_ +Preorder.refl≤ versionPreorder = ≤-refl Preorder.trans≤ versionPreorder = ≤-trans ------------------------------------------------------------------------- --- Freshness / staleness predicates over versions ------------------------------------------------------------------------- - --- A module's knowledge at knownVersion is FRESH relative to a field's --- currentVersion iff it has caught up: knownVersion ≡ currentVersion. --- (The Idris Fresh additionally pins a FieldVersion record to ground --- truth; that pin is an Idris-side soundness device for the global --- store and is orthogonal to the liveness story re-proved here.) --- --- Defined AS the propositional equality of the two version indices, --- rather than as a fresh data type with a green-slime reflexive index. --- Under --without-K, matching a `Fresh v v` self-reflexive index would --- be rejected (UnificationStuck); routing through _≡_ keeps every proof --- below K-free while preserving the named predicate Fresh. -Fresh : (knownVersion currentVersion : Version) -> Set -Fresh knownVersion currentVersion = knownVersion ≡ currentVersion - --- Canonical freshness constructor: a view that has caught up. -mkFresh : {v : Version} -> Fresh v v -mkFresh = refl - --- Knowledge is STALE iff the field has advanced past what is known: --- knownVersion < currentVersion. -data Stale : (knownVersion currentVersion : Version) -> Set where - mkStale : {v v' : Version} -> v < v' -> Stale v v' - --- A SYNC event carries a module from oldVersion up to newVersion; after --- it, the module knows newVersion. Modelled as the post-sync witness --- (oldVersion is recorded only to mirror the Idris index shape). -data Sync : (oldVersion newVersion : Version) -> Set where - sync : {old new : Version} -> Sync old new - ------------------------------------------------------------------------- --- Projectors / non-interference (mirrors the Idris lemmas) ------------------------------------------------------------------------- - -freshImpliesEqual : {v v' : Version} -> Fresh v v' -> v ≡ v' -freshImpliesEqual eq = eq - -staleImpliesLT : {v v' : Version} -> Stale v v' -> v < v' -staleImpliesLT (mkStale lt) = lt - --- Fresh and Stale are mutually exclusive at the same indices. -freshNotStale : {v v' : Version} -> Fresh v v' -> Stale v v' -> ⊥ -freshNotStale refl (mkStale lt) = <-irrefl lt - ------------------------------------------------------------------------- --- Core recovery-liveness theorems ------------------------------------------------------------------------- - --- A sync restores freshness at the synced-to version. (Idris --- syncRestoresFresh.) -syncRestoresFresh : {old new : Version} -> Sync old new -> Fresh new new -syncRestoresFresh sync = mkFresh - --- Concurrent-write staleness: a fresh view goes stale once the global --- current version advances strictly past it. (Idris --- concurrentWriteStales.) -concurrentWriteStales : - {v v' : Version} -> Fresh v v -> v < v' -> Stale v v' -concurrentWriteStales _ lt = mkStale lt - --- Re-synchronisation after a concurrent write restores freshness: --- a stale view plus a sync to the current version yields a fresh view. --- This is the no-permanently-stuck-state guarantee. (Idris --- resyncRecoversFresh.) -resyncRecoversFresh : - {v cur : Version} -> Stale v cur -> Sync v cur -> Fresh cur cur -resyncRecoversFresh _ s = syncRestoresFresh s - --- FLAGSHIP liveness: freshness propagates under any number of --- intervening writes via a SINGLE re-sync. Starting fresh at v, after --- the current version advances to cur (by however many writes, captured --- as v < cur), one sync recovers freshness at cur. (Idris --- freshnessPropagatesUnderWrites.) -freshnessPropagatesUnderWrites : - {v cur : Version} -> Fresh v v -> v < cur -> Sync v cur -> Fresh cur cur -freshnessPropagatesUnderWrites _ _ s = syncRestoresFresh s - --- Chained syncs end fresh: any two-step sync sequence terminates fresh --- at the final version. (Idris syncChainEndsFresh.) -syncChainEndsFresh : - {v1 v2 v3 : Version} -> Sync v1 v2 -> Sync v2 v3 -> Fresh v3 v3 -syncChainEndsFresh _ s2 = syncRestoresFresh s2 - ------------------------------------------------------------------------- --- Wiring to the canonical AccessibleModality ------------------------------------------------------------------------- - --- A fresh epistemic view at standpoint (version) v of a value of type A. --- The view is indexed by the *current* version v; holding ReadView v A --- means "I have A and my knowledge is fresh at v". Freshness is --- intrinsic to the index — a view living at version v is by definition --- caught up to v — so it is recovered as the lemma `viewIsFresh` below --- rather than stored as a field. Keeping the record to a single value --- field is what makes the canonical increase-refl / increase-trans laws --- hold *definitionally* under --without-K (no UIP on a stored proof). -record ReadView (v : Version) (A : Set) : Set where +-- An ancestor must belong to this particular history. Equal version numbers +-- on unrelated branches are insufficient. +data _⊑_ {A : Set} : Store A -> Store A -> Set where + here : {s : Store A} -> s ⊑ s + earlier : {s t : Store A} {a : A} -> s ⊑ t -> s ⊑ write t a + +ancestorVersions : {A : Set} {s t : Store A} -> s ⊑ t -> version s ≤ version t +ancestorVersions here = ≤-refl +ancestorVersions (earlier p) = ≤-step (ancestorVersions p) + +-- Every constructor, including direct client construction, must establish +-- that the observed value matches the indexed store state. +record ReadView {A : Set} (s : Store A) : Set where constructor readView field - value : A - -open ReadView - --- A view at version v is fresh at v, by construction. This recovers the --- "fresh field" as a theorem, tying the modal layer back to the Fresh --- predicate of the liveness theorems above. -viewIsFresh : {v : Version} {A : Set} -> ReadView v A -> Fresh v v -viewIsFresh _ = mkFresh - --- The bare modality: E v A = ReadView v A. map acts on the carried --- value; freshness is preserved automatically since it is intrinsic. -readModality : Modality Version lzero -Modality.E readModality v A = ReadView v A -Modality.map readModality f rv = readView (f (value rv)) - --- Monotone transport along version access: given v ≤ v' (v' is a later --- version) and a view fresh at v, we can RE-SYNC it to a view fresh at --- v'. This is exactly the canonical `increase`, and it is the modal --- packaging of `freshnessPropagatesUnderWrites`: advancing the --- standpoint never destroys the value; a single (implicit) sync --- re-establishes freshness at the newer version. -readIncrease : - {v v' : Version} {A : Set} -> v ≤ v' -> ReadView v A -> ReadView v' A -readIncrease _ rv = readView (value rv) - --- Transport at refl≤ is the identity (holds definitionally — the record --- has a single value field with η). -readIncrease-refl : - {v : Version} {A : Set} (rv : ReadView v A) -> - readIncrease (≤-refl {v}) rv ≡ rv -readIncrease-refl _ = refl - --- Transport composes (definitionally). -readIncrease-trans : - {v0 v1 v2 : Version} {A : Set} - (p : v0 ≤ v1) (q : v1 ≤ v2) (rv : ReadView v0 A) -> - readIncrease q (readIncrease p rv) ≡ readIncrease (≤-trans p q) rv -readIncrease-trans _ _ _ = refl - --- The full canonical AccessibleModality instance: versions-as- --- standpoints, ≤ as access, ReadView as the modality, and re-sync as --- monotone transport. This is the concrete hookup the Idris header's --- OPEN DESIGN QUESTION asked for. -versionAccessible : AccessibleModality Version lzero -AccessibleModality.modality versionAccessible = readModality -AccessibleModality.access versionAccessible = versionPreorder -AccessibleModality.increase versionAccessible = readIncrease -AccessibleModality.increase-refl versionAccessible = readIncrease-refl -AccessibleModality.increase-trans versionAccessible = readIncrease-trans + value : A + matches : value ≡ contents s + +open ReadView public + +readCurrent : {A : Set} (s : Store A) -> ReadView s +readCurrent s = readView (contents s) refl + +-- A cached read records its source and its relation to the current history. +record CachedRead {A : Set} (current : Store A) : Set where + constructor cached + field + source : Store A + ancestor : source ⊑ current + view : ReadView source + +open CachedRead public + +cachedValue : {A : Set} {s : Store A} -> CachedRead s -> A +cachedValue c = value (view c) + +Fresh : {A : Set} {s : Store A} -> CachedRead s -> Set +Fresh {s = s} c = source c ≡ s + +Stale : {A : Set} {s : Store A} -> CachedRead s -> Set +Stale {s = s} c = version (source c) < version s + +freshImpliesValue : {A : Set} {s : Store A} (c : CachedRead s) -> + Fresh c -> cachedValue c ≡ contents s +freshImpliesValue (cached _ _ rv) refl = matches rv + +freshNotStale : {A : Set} {s : Store A} {c : CachedRead s} -> + Fresh c -> Stale c -> ⊥ +freshNotStale refl st = <-irrefl st + +-- This operation actually obtains contents s in the model. Its existence +-- says nothing about whether an external scheduler performs the read. +synchronize : {A : Set} (s : Store A) -> CachedRead s +synchronize s = cached s here (readCurrent s) + +syncRestoresFresh : {A : Set} (s : Store A) -> Fresh (synchronize s) +syncRestoresFresh s = refl + +syncReadsCurrent : {A : Set} (s : Store A) -> + cachedValue (synchronize s) ≡ contents s +syncReadsCurrent s = refl + +-- Writes do not rewrite cached data. They extend its historical context. +advanceCache : {A : Set} {s : Store A} (a : A) -> + CachedRead s -> CachedRead (write s a) +advanceCache a (cached origin p rv) = cached origin (earlier p) rv + +advancePreservesSample : {A : Set} {s : Store A} (a : A) (c : CachedRead s) -> + cachedValue (advanceCache a c) ≡ cachedValue c +advancePreservesSample a c = refl + +writeStalesCache : {A : Set} {s : Store A} (a : A) (c : CachedRead s) -> + Stale (advanceCache a c) +writeStalesCache a c = s≤s (ancestorVersions (ancestor c)) + +writeInvalidatesFreshness : {A : Set} {s : Store A} (a : A) (c : CachedRead s) -> + ¬ (Fresh (advanceCache a c)) +writeInvalidatesFreshness a c fresh = + freshNotStale {c = advanceCache a c} fresh (writeStalesCache a c) + +-- Keeping an old value as a view of a later state requires a real equality. +retainUnchanged : {A : Set} {s t : Store A} -> s ⊑ t -> + contents s ≡ contents t -> ReadView s -> ReadView t +retainUnchanged _ stable (readView a eq) = readView a (trans eq stable) + +-- Evidence about a particular snapshot remains meaningful as historical +-- evidence. Moving it to a new snapshot requires an explicit implication. +FactAt : {A : Set} -> Store A -> (A -> Set) -> Set +FactAt s P = P (contents s) + +factFromView : {A : Set} {s : Store A} (P : A -> Set) (rv : ReadView s) -> + P (value rv) -> FactAt s P +factFromView P rv p = subst P (matches rv) p + +transportFact : {A : Set} {s t : Store A} {P : A -> Set} -> + (P (contents s) -> P (contents t)) -> FactAt s P -> FactAt t P +transportFact preserves p = preserves p + +stableFact : {A : Set} {s t : Store A} (P : A -> Set) -> + contents s ≡ contents t -> FactAt s P -> FactAt t P +stableFact P eq p = subst P eq p + +-- A version-only readIncrease / versionAccessible for mutable contents is +-- deliberately absent: an old value need not equal the later store value. diff --git a/src/EpistemicTypes/SurrealBridge.agda b/src/EpistemicTypes/SurrealBridge.agda index 170b0ca..66fb4fd 100644 --- a/src/EpistemicTypes/SurrealBridge.agda +++ b/src/EpistemicTypes/SurrealBridge.agda @@ -8,7 +8,8 @@ open import Agda.Builtin.Nat using (Nat; zero; suc; _+_) open import EpistemicTypes.Access open import EpistemicTypes.Base -open import EpistemicTypes.EchoBridge using (Echo; Grade; echo; finite; gradePlus) +open import EpistemicTypes.EchoBridge using + (Retention; BoundedEcho; Grade; finite; gradePlus; weakenBound; ≤G-plus) open import EpistemicTypes.Warrant data Empty : Set where @@ -31,8 +32,8 @@ sym refl = refl -- This is still not the full Conway proper class of all surreal numbers. -- It is a small interface for a day-bounded fragment or chosen carrier of -- surreal-like standpoints. Unlike a mere preorder, it must attach a --- tropical grade to each access proof. That grade is the formal place where --- "how much epistemic access is lost/refined between standpoints" lives. +-- resource grade to each access proof. Its interpretation is supplied by the +-- instance; the laws alone do not measure actual information loss or time. record SurrealAccess {sℓ oℓ : Level} : Set (lsuc (sℓ ⊔ oℓ)) where infix 4 _≤♯_ field @@ -76,32 +77,27 @@ Preorder._≤κ_ (surrealPreorder S) = SurrealAccess._≤♯_ S Preorder.refl≤ (surrealPreorder S) = SurrealAccess.refl♯ S Preorder.trans≤ (surrealPreorder S) = SurrealAccess.trans♯ S --- Echo retagging preserves the residue while changing the declared loss grade. --- This is not a recovery of A; it only records that the same residue is now --- seen after an additional access loss. -retagEcho : {r r' : Grade} {A : Set} -> Echo r A -> Echo r' A -retagEcho (echo Residue residue) = echo Residue residue - --- A modality whose transport across surreal access accumulates access loss --- into the Echo grade. This is where the surreal magnitude actually does --- work in the type. +-- Transport weakens a proved resource upper bound. It does not change the +-- retention contract or claim that information has been lost or recovered. +-- Arbitrary retagEcho is removed: reducing a budget needs a fresh bound. record GradedSurrealModality {sℓ oℓ : Level} (S : SurrealAccess {sℓ = sℓ} {oℓ = oℓ}) : Set (sℓ ⊔ oℓ ⊔ lsuc (lsuc lzero)) where open SurrealAccess S field - modality : Modality Carrier (lsuc lzero) + modality : Modality Carrier lzero open Modality modality public field transportWithLoss : - {x y : Carrier} {A : Set} -> + {x y : Carrier} {A B R : Set} -> + {C : Retention A B R} {measure : R -> Grade} {visible : B} -> (p : x ≤♯ y) -> (r : Grade) -> - E x (Echo r A) -> - E y (Echo (gradePlus r (magnitude-loss p)) A) + E x (BoundedEcho C measure r visible) -> + E y (BoundedEcho C measure (gradePlus r (magnitude-loss p)) visible) -- Factive knowledge over surreal standpoints is still explicit and separate. surrealKnowledge : @@ -127,8 +123,8 @@ AccessibleModality.increase (surrealKnowledgeAccess S) p a = a AccessibleModality.increase-refl (surrealKnowledgeAccess S) a = refl AccessibleModality.increase-trans (surrealKnowledgeAccess S) p q a = refl --- Identity-on-objects epistemic access to echoes: the value is still only an --- echo, and crossing access p changes the grade by magnitude-loss p. +-- Identity-on-objects access: the retained value is unchanged. The existing +-- measure proof justifies the larger budget through the grade order. surrealEchoKnowledge : {sℓ oℓ : Level} -> (S : SurrealAccess {sℓ = sℓ} {oℓ = oℓ}) -> @@ -139,7 +135,7 @@ GradedSurrealModality.modality (surrealEchoKnowledge S) = ; map = λ f a -> f a } GradedSurrealModality.transportWithLoss (surrealEchoKnowledge S) p r e = - retagEcho e + weakenBound (≤G-plus r (SurrealAccess.magnitude-loss S p)) e -- Belief over surreal standpoints remains non-factive. data SurrealBelief {sℓ : Level} {K : Set sℓ} diff --git a/tests/check-proofs.sh b/tests/check-proofs.sh new file mode 100644 index 0000000..bc5f41d --- /dev/null +++ b/tests/check-proofs.sh @@ -0,0 +1,13 @@ +#!/usr/bin/env bash +set -euo pipefail +cd -- "$(dirname -- "${BASH_SOURCE[0]}")/.." + +# Check each source module, including any new module omitted from All.agda. +shopt -s nullglob +modules=(src/EpistemicTypes/*.agda) +[[ ${#modules[@]} -gt 0 ]] || { echo 'FAIL: no proof modules'; exit 1; } +for module in "${modules[@]}"; do + agda --no-libraries --safe --without-K --double-check --ignore-interfaces \ + -W error -i src "$module" +done +printf 'PASS: %s source modules checked under the required proof discipline\n' "${#modules[@]}" diff --git a/tests/check-rejections.sh b/tests/check-rejections.sh new file mode 100644 index 0000000..8960106 --- /dev/null +++ b/tests/check-rejections.sh @@ -0,0 +1,36 @@ +#!/usr/bin/env bash +set -euo pipefail +cd -- "$(dirname -- "${BASH_SOURCE[0]}")/.." + +# Each fixture must reach its intended type error. Missing tools/imports or +# unrelated parse failures must fail this gate rather than count as rejection. +fixtures=(LyingVerifier ForgedAcceptance ReplayedArtifact ReplayedHolder \ + StaleSample FakeFreshness ForkedHistory ForgedResidue MismatchedSource \ + UnderstatedBound InventedMigration) +expected_files=$(printf 'tests/reject/%s.agda\n' "${fixtures[@]}" | sort) +actual_files=$(rg --files tests/reject -g '*.agda' | sort) +[[ "$actual_files" == "$expected_files" ]] || { echo 'FAIL: rejection manifest differs from files'; exit 1; } +for fixture in "${fixtures[@]}"; do + status=0 + diagnostic=$(agda --no-libraries --safe --without-K --double-check -W error \ + -i src -i tests/reject "tests/reject/$fixture.agda" 2>&1) || status=$? + if [[ "$status" -eq 0 ]]; then + printf 'FAIL: %s unexpectedly type-checked\n' "$fixture" + exit 1 + fi + case "$fixture" in + LyingVerifier|ForgedAcceptance) expected='false != .*true' ;; + ReplayedArtifact) expected='true != .*false' ;; + ReplayedHolder) expected='Alice != .*Bob' ;; + StaleSample|ForkedHistory|ForgedResidue|MismatchedSource) expected='false != .*true' ;; + FakeFreshness) expected='initial .*false !=' ;; + UnderstatedBound) expected='1 != 0' ;; + InventedMigration) expected='true != .*false' ;; + esac + if [[ "$status" -ne 42 ]] || ! rg -q "$expected" <<< "$diagnostic" || \ + ! rg -q 'when checking' <<< "$diagnostic"; then + printf 'FAIL: %s failed for an unexpected reason\n%s\n' "$fixture" "$diagnostic" + exit 1 + fi + printf 'PASS: %s rejected for the expected type mismatch\n' "$fixture" +done diff --git a/tests/integration/CanonicalEcho.agda b/tests/integration/CanonicalEcho.agda new file mode 100644 index 0000000..665d10c --- /dev/null +++ b/tests/integration/CanonicalEcho.agda @@ -0,0 +1,34 @@ +{-# OPTIONS --safe --without-K #-} + +module CanonicalEcho where + +open import Agda.Builtin.Equality using (_≡_; refl) +open import Agda.Builtin.Sigma using (_,_) +import Echo as Core +import EchoResidue as Canonical +open import EpistemicTypes.EchoBridge + +-- This file imports the actual sibling sources, not a copied approximation. +-- Keep it separate from the dependency-free core build. +toCanonical : {A B R : Set} {C : Retention A B R} {y : B} -> + Echo C y -> Canonical.EchoR R (Retention.Cert C) y +toCanonical (echo r p) = r , p + +fromCanonical : {A B R : Set} {C : Retention A B R} {y : B} -> + Canonical.EchoR R (Retention.Cert C) y -> Echo C y +fromCanonical (r , p) = echo r p + +fromTo : {A B R : Set} {C : Retention A B R} {y : B} (e : Echo C y) -> + fromCanonical {C = C} (toCanonical e) ≡ e +fromTo (echo r p) = refl + +toFrom : {A B R : Set} {C : Retention A B R} {y : B} + (e : Canonical.EchoR R (Retention.Cert C) y) -> + toCanonical (fromCanonical {C = C} e) ≡ e +toFrom (r , p) = refl + +lowerAgreesWithCanonical : {A B R : Set} (C : Retention A B R) (x : A) -> + toCanonical (lower C x) ≡ Canonical.echo-to-residue + (Retention.observe C) (Retention.retain C) (Retention.Cert C) (Retention.sound C) + (Core.echo-intro (Retention.observe C) x) +lowerAgreesWithCanonical C x = refl diff --git a/tests/reject/FakeFreshness.agda b/tests/reject/FakeFreshness.agda new file mode 100644 index 0000000..3206ff2 --- /dev/null +++ b/tests/reject/FakeFreshness.agda @@ -0,0 +1,8 @@ +{-# OPTIONS --safe --without-K #-} +module FakeFreshness where +open import Agda.Builtin.Equality +open import EpistemicTypes.ReadConsistency +import EpistemicTypes.ContinuityExamples as Examples +open Examples.Reads using (historical) +forged : Fresh historical +forged = refl diff --git a/tests/reject/ForgedAcceptance.agda b/tests/reject/ForgedAcceptance.agda new file mode 100644 index 0000000..f24f9e0 --- /dev/null +++ b/tests/reject/ForgedAcceptance.agda @@ -0,0 +1,10 @@ +{-# OPTIONS --safe --without-K #-} +module ForgedAcceptance where +open import Agda.Builtin.Bool using (true; false) +open import Agda.Builtin.Equality using (refl) +open import EpistemicTypes.ProofTransportExample using (Agent; Claim; Artifact; Meaning; Payload; Bob; ArtifactIsTrue; bobPublicChecker) +open import EpistemicTypes.ProofTransport Agent Claim Artifact Meaning Payload + +-- The public constructor cannot bypass a sound check rejecting this payload. +forge : View Bob true Proof ArtifactIsTrue +forge = forgetMode (asProofUnder certPublic bobPublicChecker (publicEv false) refl) diff --git a/tests/reject/ForgedResidue.agda b/tests/reject/ForgedResidue.agda new file mode 100644 index 0000000..b5612cf --- /dev/null +++ b/tests/reject/ForgedResidue.agda @@ -0,0 +1,9 @@ +{-# OPTIONS --safe --without-K #-} +module ForgedResidue where +open import Agda.Builtin.Bool +open import Agda.Builtin.Equality +open import EpistemicTypes.EchoBridge +import EpistemicTypes.ContinuityExamples as Examples +open Examples.Residues using (identityRetention) +forged : Echo identityRetention true +forged = echo false refl diff --git a/tests/reject/ForkedHistory.agda b/tests/reject/ForkedHistory.agda new file mode 100644 index 0000000..a713ea5 --- /dev/null +++ b/tests/reject/ForkedHistory.agda @@ -0,0 +1,7 @@ +{-# OPTIONS --safe --without-K #-} +module ForkedHistory where +open import EpistemicTypes.ReadConsistency +import EpistemicTypes.ContinuityExamples as Examples +open Examples.Reads using (after; otherBranch) +forged : CachedRead after +forged = cached otherBranch here (readCurrent otherBranch) diff --git a/tests/reject/InventedMigration.agda b/tests/reject/InventedMigration.agda new file mode 100644 index 0000000..18b9cf8 --- /dev/null +++ b/tests/reject/InventedMigration.agda @@ -0,0 +1,14 @@ +{-# OPTIONS --safe --without-K #-} +module InventedMigration where +open import Agda.Builtin.Bool +open import Agda.Builtin.Equality +open import Agda.Builtin.Sigma +open import EpistemicTypes.EchoBridge +import EpistemicTypes.ContinuityExamples as Examples +open Examples.Residues using (firstRetention) +forged : Migration firstRetention snd +Migration.migrate forged _ residue = residue +Migration.adequate forged (true , false) = refl +Migration.adequate forged (true , true) = refl +Migration.adequate forged (false , false) = refl +Migration.adequate forged (false , true) = refl diff --git a/tests/reject/LyingVerifier.agda b/tests/reject/LyingVerifier.agda new file mode 100644 index 0000000..6dc42d1 --- /dev/null +++ b/tests/reject/LyingVerifier.agda @@ -0,0 +1,10 @@ +{-# OPTIONS --safe --without-K #-} +module LyingVerifier where +open import Agda.Builtin.Bool using (true; false) +open import Agda.Builtin.Equality using (refl) +open import EpistemicTypes.ProofTransportExample using (Agent; Claim; Artifact; Meaning; Payload; Alice; ArtifactIsTrue) +open import EpistemicTypes.ProofTransport Agent Claim Artifact Meaning Payload + +-- An always-accepting checker cannot supply soundness for a false artifact. +lie : CertificateCheck Alice false ArtifactIsTrue +lie = certificateCheck (λ _ -> true) (λ _ _ -> refl) diff --git a/tests/reject/MismatchedSource.agda b/tests/reject/MismatchedSource.agda new file mode 100644 index 0000000..e6b9efe --- /dev/null +++ b/tests/reject/MismatchedSource.agda @@ -0,0 +1,9 @@ +{-# OPTIONS --safe --without-K #-} +module MismatchedSource where +open import Agda.Builtin.Bool +open import Agda.Builtin.Equality +open import EpistemicTypes.EchoBridge +import EpistemicTypes.ContinuityExamples as Examples +open Examples.Residues using (identityRetention; identityTrue) +forged : MatchesSource identityRetention false identityTrue +forged = matchesSource refl refl diff --git a/tests/reject/ReplayedArtifact.agda b/tests/reject/ReplayedArtifact.agda new file mode 100644 index 0000000..cbbe7c0 --- /dev/null +++ b/tests/reject/ReplayedArtifact.agda @@ -0,0 +1,9 @@ +{-# OPTIONS --safe --without-K #-} +module ReplayedArtifact where +open import Agda.Builtin.Bool using (false) +open import EpistemicTypes.ProofTransportExample using (Agent; Claim; Artifact; Meaning; Payload; Alice; ArtifactIsTrue; aliceProof) +open import EpistemicTypes.ProofTransport Agent Claim Artifact Meaning Payload + +-- A proof bound to the original artifact cannot be reused for an altered one. +replay : View Alice false Proof ArtifactIsTrue +replay = aliceProof diff --git a/tests/reject/ReplayedHolder.agda b/tests/reject/ReplayedHolder.agda new file mode 100644 index 0000000..e299817 --- /dev/null +++ b/tests/reject/ReplayedHolder.agda @@ -0,0 +1,9 @@ +{-# OPTIONS --safe --without-K #-} +module ReplayedHolder where +open import Agda.Builtin.Bool using (true) +open import EpistemicTypes.ProofTransportExample using (Bob; ArtifactIsTrue; module HolderBoundary) +open HolderBoundary using (module Local; aliceLocalProof) + +-- Holder-sensitive evidence cannot silently acquire a different holder. +replay : Local.View Bob true Local.Proof ArtifactIsTrue +replay = aliceLocalProof diff --git a/tests/reject/StaleSample.agda b/tests/reject/StaleSample.agda new file mode 100644 index 0000000..6213460 --- /dev/null +++ b/tests/reject/StaleSample.agda @@ -0,0 +1,9 @@ +{-# OPTIONS --safe --without-K #-} +module StaleSample where +open import Agda.Builtin.Bool +open import Agda.Builtin.Equality +open import EpistemicTypes.ReadConsistency +import EpistemicTypes.ContinuityExamples as Examples +open Examples.Reads using (after) +forged : ReadView after +forged = readView false refl diff --git a/tests/reject/UnderstatedBound.agda b/tests/reject/UnderstatedBound.agda new file mode 100644 index 0000000..f3f940a --- /dev/null +++ b/tests/reject/UnderstatedBound.agda @@ -0,0 +1,9 @@ +{-# OPTIONS --safe --without-K #-} +module UnderstatedBound where +open import Agda.Builtin.Bool +open import Agda.Builtin.Nat +open import EpistemicTypes.EchoBridge +import EpistemicTypes.ContinuityExamples as Examples +open Examples.Residues using (identityRetention; constantCost; boundedTrue) +forged : BoundedEcho identityRetention constantCost (finite zero) true +forged = boundedTrue From d31ce7db8af093771c0465214ea205ba89a18894 Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Mon, 7 Sep 2026 02:27:32 +0100 Subject: [PATCH 2/3] fix(ci): use UTF-8 and lock-aware governance checks --- .github/workflows/actions.lock | 4 ++-- .github/workflows/{proofs.yml => agda.yml} | 7 +++++++ .github/workflows/governance.yml | 2 +- 3 files changed, 10 insertions(+), 3 deletions(-) rename .github/workflows/{proofs.yml => agda.yml} (91%) diff --git a/.github/workflows/actions.lock b/.github/workflows/actions.lock index c4148f8..2f7fccb 100644 --- a/.github/workflows/actions.lock +++ b/.github/workflows/actions.lock @@ -3,11 +3,11 @@ # Docs: https://gh.io/actions-lockfile version: 'v0.0.2' workflows: + '.github/workflows/agda.yml': + - 'actions/checkout@v6.0.3' '.github/workflows/codeql.yml': - 'actions/checkout@v6.0.3' - 'github/codeql-action@v4.36.2' - '.github/workflows/proofs.yml': - - 'actions/checkout@v6.0.3' '.github/workflows/push-email-notify.yml': - 'hyperpolymath/smtp-notify-action@v0.2.0' dependencies: diff --git a/.github/workflows/proofs.yml b/.github/workflows/agda.yml similarity index 91% rename from .github/workflows/proofs.yml rename to .github/workflows/agda.yml index 400fff7..7e924e7 100644 --- a/.github/workflows/proofs.yml +++ b/.github/workflows/agda.yml @@ -1,4 +1,7 @@ # This workflow is managed by gh actions-lock. +# SPDX-License-Identifier: MPL-2.0 +# SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell +# This workflow is managed by gh actions-lock. name: Proof Safety @@ -12,6 +15,10 @@ on: permissions: contents: read +env: + LANG: C.UTF-8 + LC_ALL: C.UTF-8 + concurrency: group: ${{ github.workflow }}-${{ github.ref }} cancel-in-progress: true diff --git a/.github/workflows/governance.yml b/.github/workflows/governance.yml index 7ce96ba..e4c0d2c 100644 --- a/.github/workflows/governance.yml +++ b/.github/workflows/governance.yml @@ -14,4 +14,4 @@ permissions: jobs: governance: - uses: hyperpolymath/standards/.github/workflows/governance-reusable.yml@81dbf2dd854b1444fd6236fa2352474383b2c2b9 + uses: hyperpolymath/standards/.github/workflows/governance-reusable.yml@a26cc7479b14cdf70433919bfc228625f1c5c6f2 From a3d1f17122e270e59ff1b5494cf8c1472de56c32 Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Mon, 7 Sep 2026 02:35:38 +0100 Subject: [PATCH 3/3] fix(metadata): encode conditional transport and align verification contracts --- .github/workflows/governance.yml | 1 + .../descriptiles/0-AI-MANIFEST.a2ml | 8 +++--- .machine_readable/descriptiles/AGENTIC.a2ml | 6 ++--- .machine_readable/descriptiles/META.a2ml | 8 +++--- .machine_readable/descriptiles/NEUROSYM.a2ml | 6 ++--- .../proof-transport/ProofTransport.a2ml | 6 +++++ .../proof-transport/proof-transport.k9.ncl | 13 ++++----- 0-AI-MANIFEST.a2ml | 27 ++++++++++--------- CONTRIBUTING.adoc | 7 +++-- EXPLAINME.adoc | 2 +- coordination.k9 | 6 ++--- docs/README.adoc | 2 +- docs/what-epistemic-is.adoc | 10 +++---- tests/check-rejections.sh | 2 +- 14 files changed, 57 insertions(+), 47 deletions(-) diff --git a/.github/workflows/governance.yml b/.github/workflows/governance.yml index e4c0d2c..6336e02 100644 --- a/.github/workflows/governance.yml +++ b/.github/workflows/governance.yml @@ -10,6 +10,7 @@ on: workflow_dispatch: permissions: + actions: read contents: read jobs: diff --git a/.machine_readable/descriptiles/0-AI-MANIFEST.a2ml b/.machine_readable/descriptiles/0-AI-MANIFEST.a2ml index 49e6832..68c00e5 100644 --- a/.machine_readable/descriptiles/0-AI-MANIFEST.a2ml +++ b/.machine_readable/descriptiles/0-AI-MANIFEST.a2ml @@ -22,20 +22,20 @@ mathematical_honesty = "Do not postulate laws silently. No Agda postulates; laws factivity = "Separate factive knowledge from non-factive belief." warrants = "Use explicit warrant objects where possible." scope = "Keep modules small and type-check frequently; keep to a single-tool Agda library checked by 'just check'." -echo_distinction = "Echo-types are min-plus-graded loss/residue modalities; epistemic types are standpoint/warrant/access modalities." +echo_distinction = "Echo values have explicit retention certificates; resource bounds are separate; epistemic types are standpoint/warrant/access modalities." no_collapse = "Do not collapse Echo C y and E κ A. Their composition is meaningful, but they are not the same modality." [typecheck] -command = "agda --no-libraries -i src src/EpistemicTypes/All.agda" +command = "bash tests/check-proofs.sh && bash tests/check-rejections.sh" just-target = "just check" agda-version = "2.6.4.3" [canonical-locations] # The descriptiles directory is authoritative for this repo's machine-readable metadata. # Present in this directory (right-sized for a small formal-methods prototype): -present = [ "0-AI-MANIFEST.a2ml", "STATE.a2ml", "README.adoc" ] +present = ["0-AI-MANIFEST.a2ml", "AGENTIC.a2ml", "ECOSYSTEM.a2ml", "META.a2ml", "NEUROSYM.a2ml", "PLAYBOOK.a2ml", "README.adoc", "STATE.a2ml"] [invariants] single-source-of-truth = "This directory is authoritative; no duplicate metadata in the root directory." no-stale-metadata = true -ci = "Not enabled (see AUDIT.adoc)." +ci = "Proof and security workflows configured; see docs/ci-safety.adoc." diff --git a/.machine_readable/descriptiles/AGENTIC.a2ml b/.machine_readable/descriptiles/AGENTIC.a2ml index d8725ee..857991a 100644 --- a/.machine_readable/descriptiles/AGENTIC.a2ml +++ b/.machine_readable/descriptiles/AGENTIC.a2ml @@ -11,7 +11,7 @@ last-updated = "2026-06-15" [agent-permissions] can-edit-source = true # Agda modules under src/EpistemicTypes/ -can-edit-docs = true # readme.adoc, explainme.adoc, AsciiDoc docs +can-edit-docs = true # README.adoc, explainme.adoc, AsciiDoc docs can-edit-machine-readable = true # .machine_readable/ (descriptiles, proof-transport) can-edit-build = true # Justfile, epistemic-types.agda-lib, .gitignore can-create-files = true @@ -41,7 +41,7 @@ can-add-spdx-headers = false # repo is intentionally SPDX-free; keep it consist # - Never edit LICENSE or add SPDX-License-Identifier / copyright headers. # Licensing (classified MPL-2.0 as the owner's sole repo) is owner-manual only. # - Never commit secrets or credentials. -# - Keep docs in AsciiDoc; do not rename or duplicate readme.adoc / explainme.adoc. +# - Keep docs in AsciiDoc; do not rename or duplicate README.adoc / explainme.adoc. # - Maintain the owner-authorized proof and security CI gates; never bypass failing checks. [maintenance-integrity] @@ -55,7 +55,7 @@ release-claim-requires-hard-pass = true [verification] # The single source of truth for "does it hold". command = "just check" -underlying = "agda --no-libraries -i src src/EpistemicTypes/All.agda" +underlying = "bash tests/check-proofs.sh && bash tests/check-rejections.sh" agda-version = "2.6.4.3" entrypoint = "src/EpistemicTypes/All.agda" expected = "type-checks clean, no postulates, no warnings" diff --git a/.machine_readable/descriptiles/META.a2ml b/.machine_readable/descriptiles/META.a2ml index 39835a8..4591f3d 100644 --- a/.machine_readable/descriptiles/META.a2ml +++ b/.machine_readable/descriptiles/META.a2ml @@ -22,7 +22,7 @@ adrs = [ { id = "ADR-002", title = "Separate FactiveModality from BeliefModality; no generic reflect/return", status = "accepted", date = "2026-06-15" }, { id = "ADR-003", title = "Compile under --safe --without-K", status = "accepted", date = "2026-06-15" }, { id = "ADR-004", title = "No Agda standard library; build with agda --no-libraries", status = "accepted", date = "2026-06-15" }, - { id = "ADR-005", title = "Keep Echo grades distinct from epistemic standpoints", status = "accepted", date = "2026-06-15" }, + { id = "ADR-005", title = "Keep certified residues and resource bounds distinct from epistemic standpoints", status = "accepted", date = "2026-06-15" }, { id = "ADR-006", title = "ProofTransport: no smuggling by construction", status = "accepted", date = "2026-06-15" } ] @@ -55,10 +55,10 @@ decision = "Build with `agda --no-libraries`, using only `Agda.Builtin.*` and `A consequence = "The project is self-contained and reproducible with just an Agda binary, at the cost of re-deriving small primitives in-tree." [architecture-decisions.ADR-005] -title = "Keep Echo grades distinct from epistemic standpoints" +title = "Keep certified residues and resource bounds distinct from epistemic standpoints" status = "accepted" -context = "`EchoBridge` provides a min-plus-graded loss/residue modality `Echo C y`. It is tempting to identify the grade `r` with an epistemic standpoint `κ`, collapsing two different ideas." -decision = "`Echo C y` (graded loss/residue) and `E κ A` (standpoint-indexed epistemic availability) are kept as separate type formers. Their composition is meaningful and intended, but they are never the same modality." +context = "Echo C y packages a residue certified by Retention.Cert. Measured resource bounds are separate; the epistemic index κ denotes a standpoint." +decision = "Preserve the distinction between certified Echo residues, measured bounds, and E κ A. Compose them only with explicit laws." consequence = "The echo bridge can be extended without dragging in a full graded comonad, and standpoint reasoning stays independent of loss accounting." [architecture-decisions.ADR-006] diff --git a/.machine_readable/descriptiles/NEUROSYM.a2ml b/.machine_readable/descriptiles/NEUROSYM.a2ml index 1296e08..b3de403 100644 --- a/.machine_readable/descriptiles/NEUROSYM.a2ml +++ b/.machine_readable/descriptiles/NEUROSYM.a2ml @@ -12,7 +12,7 @@ last-updated = "2026-06-15" author = "Jonathan D.A. Jewell (hyperpolymath) " [hypatia-config] -scan-enabled = true +scan-enabled = false scan-depth = "standard" # quick | standard | deep report-format = "logtalk" scan-paths = [ "src/EpistemicTypes" ] @@ -47,9 +47,9 @@ safe-flags = "--safe --without-K" # Neural pattern detection is not configured for this prototype. # A formal Agda library is better served by the deterministic symbolic rules # above and by the type-checker than by learned pattern matching. -enabled = true +enabled = false [ci] # CI checks core proofs, semantic rejections, pinned Echo correspondence and workflow/secret security. # See AUDIT.adoc. Verification is local via `just check`. -enabled = true +enabled = false diff --git a/.machine_readable/proof-transport/ProofTransport.a2ml b/.machine_readable/proof-transport/ProofTransport.a2ml index ec099bc..df51159 100644 --- a/.machine_readable/proof-transport/ProofTransport.a2ml +++ b/.machine_readable/proof-transport/ProofTransport.a2ml @@ -26,6 +26,12 @@ verify = "Evaluates the check; successful verification yields Proof, false yield opaque = "OpaqueReceipt always yields OpaqueGap." tryUpgrade = "Additionally emits MissingChecker or MissingEvidence." +[transport] +transmit = "Moves sender proof data to a receiver-side Receipt; it does not establish the receiver's Meaning." +checkableTransportUpgrades = "The boundary fixes sender/receiver indices; successful sound verification establishes the receiver's Meaning." +publicTransfer = "Transfers the public checker and evidence using an explicit Meaning r a c -> Meaning q a c implication." +designatedTransfer = "A designated checker can be used only at its indexed holder; designation is not cryptographic authentication." + [statuses] values = ["Data", "Code", "Claimed", "Receipt", "Proof", "ProofUnder"] diff --git a/.machine_readable/proof-transport/proof-transport.k9.ncl b/.machine_readable/proof-transport/proof-transport.k9.ncl index a273c4a..efcdd51 100644 --- a/.machine_readable/proof-transport/proof-transport.k9.ncl +++ b/.machine_readable/proof-transport/proof-transport.k9.ncl @@ -13,6 +13,7 @@ let Leash = [| 'Kennel, 'Yard, 'Hunt |] in let Mode = [| 'Public, 'Designated, 'IssuerMediated, 'EnvironmentMediated, 'OpaqueReceipt |] in +let Portability = [| 'RequiresHolderMeaningImplication, 'NoGenericTransfer |] in let Gap = [| 'TrivialGap, 'DesignatedGap, 'EnvironmentGap, 'IssuerTrustGap, 'OpaqueGap, 'MissingChecker, 'MissingEvidence, 'MissingContext, 'InvalidEvidence @@ -21,7 +22,7 @@ let Gap = [| # Per-mode transport semantics. let ModeRule = { certifies | Bool, # can a matching checker + evidence yield Proof? - portable | Bool, # supported ONLY with an explicit meaning implication + portability | Portability, # conditional support is an explicit schema value receiver_bound | Bool, # is the checker pinned to one designated holder? gap_on_fail | Gap, # RESERVED: the gap a future refinement would report # for this mode. The core does NOT yet emit these per @@ -59,23 +60,23 @@ let ModeRule = { # Verification / attestation modes and how each transports. modes = { Public | ModeRule = { - certifies = true, portable = true, receiver_bound = false, + certifies = true, portability = 'RequiresHolderMeaningImplication, receiver_bound = false, gap_on_fail = 'MissingEvidence, }, Designated | ModeRule = { - certifies = true, portable = false, receiver_bound = true, + certifies = true, portability = 'NoGenericTransfer, receiver_bound = true, gap_on_fail = 'DesignatedGap, }, IssuerMediated | ModeRule = { - certifies = true, portable = false, receiver_bound = false, + certifies = true, portability = 'NoGenericTransfer, receiver_bound = false, gap_on_fail = 'IssuerTrustGap, }, EnvironmentMediated | ModeRule = { - certifies = true, portable = false, receiver_bound = false, + certifies = true, portability = 'NoGenericTransfer, receiver_bound = false, gap_on_fail = 'EnvironmentGap, }, OpaqueReceipt | ModeRule = { - certifies = false, portable = false, receiver_bound = false, + certifies = false, portability = 'NoGenericTransfer, receiver_bound = false, gap_on_fail = 'OpaqueGap, }, }, diff --git a/0-AI-MANIFEST.a2ml b/0-AI-MANIFEST.a2ml index ed84a53..a6ed4f8 100644 --- a/0-AI-MANIFEST.a2ml +++ b/0-AI-MANIFEST.a2ml @@ -27,7 +27,7 @@ proof-transport-contractile = ".machine_readable/proof-transport/proof-transport proof-transport-readme = ".machine_readable/proof-transport/README.adoc" [docs] -readme = "readme.adoc" +readme = "README.adoc" explainme = "explainme.adoc" audit = "AUDIT.adoc" format = "AsciiDoc (.adoc) is the default; existing lowercase doc filenames are canonical and are not renamed." @@ -36,31 +36,34 @@ format = "AsciiDoc (.adoc) is the default; existing lowercase doc filenames are scm-files-location = ".machine_readable/ ONLY — a2ml and scm/Nickel/k9 files never live at repo root" license = "MPL-2.0" build = "just check" -build-expansion = "safe Agda All.agda check plus tests/check-rejections.sh" +build-expansion = "bash tests/check-proofs.sh && bash tests/check-rejections.sh" agda-options = "{-# OPTIONS --safe --without-K #-} ; no postulates; no Agda standard library (only Agda.Builtin.* / Agda.Primitive)" -agda-version = "2.8.0" -echo-distinction = "Do not collapse Echo r A and E κ A. Echo-types are min-plus-graded loss/residue; epistemic types are standpoint/warrant/access modalities. Their composition is meaningful; they are not the same modality." -ci = "none — no GitHub Actions, no badges (see AUDIT.adoc)" +agda-version = "2.6.4.3" +echo-distinction = "Do not collapse Echo C y and E κ A. Echo retains certified residues; epistemic types are standpoint/warrant/access modalities. Their composition is meaningful; they are not the same modality." +ci = "Proof and security workflows configured; required merge checks are described in docs/ci-safety.adoc" [source] root = "src/EpistemicTypes/" aggregator = "src/EpistemicTypes/All.agda" modules = [ - "EpistemicTypes.Base", - "EpistemicTypes.Warrant", "EpistemicTypes.Access", + "EpistemicTypes.All", + "EpistemicTypes.Base", + "EpistemicTypes.ContinuityExamples", "EpistemicTypes.EchoBridge", - "EpistemicTypes.SurrealBridge", "EpistemicTypes.Examples", "EpistemicTypes.ProofTransport", "EpistemicTypes.ProofTransportExample", + "EpistemicTypes.ReadConsistency", + "EpistemicTypes.SurrealBridge", + "EpistemicTypes.Warrant", ] [source.descriptions] Base = "Modality / LawfulModality / FactiveModality / BeliefModality / ReturnModality. The base E is a plain indexed endofunctor (map only)." Warrant = "Warrant / Epi / SoundWarrant — explicit warrant objects." Access = "Preorder plus AccessibleModality transport ('increase') across the access preorder." -EchoBridge = "Min-plus graded loss/residue 'Echo r A', kept distinct from E κ A." +EchoBridge = "Certified Echo C y residues, explicit migration/recovery and separately measured resource bounds." SurrealBridge = "SurrealAccess carrier plus GradedSurrealModality plus daySurrealAccess finite-birthday tower." Examples = "Worked instances of the abstract interfaces." ProofTransport = "Standpoint-indexed proof transport across trust boundaries." @@ -87,8 +90,8 @@ step-2 = "Read .machine_readable/descriptiles/STATE.a2ml for current project sta step-3 = "Read .machine_readable/descriptiles/META.a2ml for architecture and design decisions." step-4 = "Read .machine_readable/descriptiles/ECOSYSTEM.a2ml for ecosystem position and sibling repos." step-5 = "Read .machine_readable/descriptiles/AGENTIC.a2ml, NEUROSYM.a2ml, and PLAYBOOK.a2ml for agent guidance." -step-6 = "Read readme.adoc and explainme.adoc for the human-facing overview." -step-7 = "Run 'just check' to type-check src/EpistemicTypes/All.agda before and after changes." +step-6 = "Read README.adoc and explainme.adoc for the human-facing overview." +step-7 = "Run 'just check' to check every source module and semantic rejection fixture before and after changes." [policy] rules = [ @@ -97,7 +100,7 @@ rules = [ "Keep modules small and type-check frequently with 'just check'.", "Keep a2ml / Nickel / k9 files under .machine_readable/ only.", "License and SPDX changes are owner-manual; do not add LICENSE files or SPDX headers.", - "Do not add CI, containers, or badges; this is a single-tool Agda library.", + "Maintain owner-authorized proof and security CI; do not bypass failing checks.", ] [ecosystem] diff --git a/CONTRIBUTING.adoc b/CONTRIBUTING.adoc index d7b0a4c..cdf52c4 100644 --- a/CONTRIBUTING.adoc +++ b/CONTRIBUTING.adoc @@ -143,15 +143,14 @@ machine-readable description in step. * *AsciiDoc (`.adoc`) is the default* for documentation. Update the relevant `.adoc` file alongside any behavioural or interface change. -* Existing docs keep their current lowercase names: `readme.adoc` and +* Existing docs keep their current names: `README.adoc` and `explainme.adoc`. Do *not* rename or duplicate them. * Machine-readable descriptions live under `.machine++_++readable/` (a2ml {plus} Nickel/k9). a2ml files use the canonical TOML-like dialect: `++[++section++]++` headers, `key = "value"`, arrays `++[++ "a", "b" ++]++`, inline tables `++{++ k = "v", j = "w" }`. -* Only these files may be Markdown (GitHub community-health -special-casing): `CONTRIBUTING.adoc`, `CODE++_++OF++_++CONDUCT.md`, -`SECURITY.md`, `CHANGELOG.adoc`. Everything else is `.adoc`. +* Root contribution, conduct, security and changelog documents use AsciiDoc. + Preserve their existing `.adoc` filenames. ''''' diff --git a/EXPLAINME.adoc b/EXPLAINME.adoc index 62041ec..c016218 100644 --- a/EXPLAINME.adoc +++ b/EXPLAINME.adoc @@ -153,7 +153,7 @@ link:docs/proof-transport.adoc[]. | Preorder accessibility + transport | `src/EpistemicTypes/SurrealBridge.agda` -| Resource-bound weakening + GradedSurrealModality + finite daySurrealAccess +| BoundedEcho resource-bound weakening, with GradedSurrealModality as an explicit interface and finite daySurrealAccess | `src/EpistemicTypes/ProofTransport.agda` | View / transmit / verify + semantic soundness + opacity laws diff --git a/coordination.k9 b/coordination.k9 index ccf63ef..2be88c6 100644 --- a/coordination.k9 +++ b/coordination.k9 @@ -79,7 +79,7 @@ invariants: - id: "build-green" statement: "The library typechecks: `just check` succeeds." command: "just check" - expands_to: "agda --no-libraries -i src src/EpistemicTypes/All.agda" + expands_to: "bash tests/check-proofs.sh && bash tests/check-rejections.sh" tool: "Agda 2.6.4.3" - id: "no-postulates" statement: "No postulates. Compiles under {-# OPTIONS --safe --without-K #-}; constructive throughout." @@ -107,7 +107,7 @@ ecosystem: - name: "a2ml + k9" relationship: "Machine-readable + contractile tooling; ProofTransport's engineering target (.machine_readable/proof-transport/)." -# Docs keep their existing lowercase names; do not rename or duplicate. +# Docs keep their existing names; do not rename or duplicate. docs: - - "readme.adoc" + - "README.adoc" - "explainme.adoc" diff --git a/docs/README.adoc b/docs/README.adoc index f0cae63..9d6f89a 100644 --- a/docs/README.adoc +++ b/docs/README.adoc @@ -16,7 +16,7 @@ authority. | `README.adoc` (repo root) | Project overview: the core form `E : K -> Set ℓ -> Set ℓ`, the module layout, - and the `just check` build (`agda --no-libraries -i src src/EpistemicTypes/All.agda`). + and the `just check` build (`just check`). | `explainme.adoc` (repo root) | Gentler, narrative explanation of the ideas — why `E κ A` is a plain indexed diff --git a/docs/what-epistemic-is.adoc b/docs/what-epistemic-is.adoc index c8f6725..7bd7c76 100644 --- a/docs/what-epistemic-is.adoc +++ b/docs/what-epistemic-is.adoc @@ -26,7 +26,7 @@ accessibility contexts, warrant regimes). The reading of `E κ A` is that `A` is *epistemically available from standpoint `κ`*: known, believed, observed, warranted, inferable, or assertable under that standpoint. This is the operative definition as the code actually uses it, and it is the form named in -`readme.adoc` and verified green in `AFFIRMATION.adoc`. +`README.adoc` and verified green in `AFFIRMATION.adoc`. The library's defining move is to *separate the interfaces* rather than ship one omnibus modality (`src/EpistemicTypes/Base.agda`): @@ -71,7 +71,7 @@ type-checks under `--safe --without-K` with zero postulates, per Honesty first, because it is load-bearing: unlike the sibling repos echo-types (which is provably the fibre / a graded-loss modality) and tropical-resource-typing (provably a dioid), epistemic-types' *deep* mathematical identity is -*deliberately unsettled*. The repository's own `readme.adoc` lists "concrete +*deliberately unsettled*. The repository's own `README.adoc` lists "concrete Kripke-style and evidence-state models" (roadmap #2) and the monadic/comonadic *variance* question (roadmap #7) as *intentionally unformalized*, and `AFFIRMATION.adoc` confirms the Kripke semantics is absent, @@ -134,7 +134,7 @@ What is *ours* is the *modelling and assembly*: the specific Agda *interface-separation* (`Modality` / `LawfulModality` / `FactiveModality` / `BeliefModality` / `ReturnModality`; `Warrant` versus `SoundWarrant`), and the *standpoint-indexed proof-transport* calculus that makes proofhood holder-relative -and proves the no-smuggling property. The usefulness is *demonstrated by concrete, +and proves semantic soundness relative to Meaning through `proofSound`. The usefulness is *demonstrated by concrete, checkable artefacts* recorded as ground truth in `AFFIRMATION.adoc`: * the whole library type-checks *cold and green* under `--safe --without-K` @@ -147,7 +147,7 @@ checkable artefacts* recorded as ground truth in `AFFIRMATION.adoc`: `no-polymorphic-epi-reflection` *refute* a generic `(A : Set) -> Belief rough A -> A` (resp. `Epi`) by exhibiting a belief/warrant for `⊥`; -* `ProofTransport.proofNeedsChecker` (no-smuggling), with +* `ProofTransport.proofNeedsChecker` (structural projection; `proofSound` is the semantic guarantee), with `designatedBindsHolder`, `opaqueNotCertifying`, and `verifyReceiptIsGap` giving the explicitly qualified public portability / designated-bound / receipt-never-certifies distinction. @@ -176,7 +176,7 @@ EI-2.) To keep boundaries un-eroded: * epistemic-types *is NOT a complete epistemic logic or a Kripke semantics* — by - its own statement (`readme.adoc` "What remains intentionally unformalized"; + its own statement (`README.adoc` "What remains intentionally unformalized"; `AFFIRMATION.adoc` "Prototype scope"). It formalises honesty-preserving *interfaces* and real *separation theorems*, not a worlds-and-valuation model. * epistemic-types *is NOT factive by default*. Factivity (`reflect`, diff --git a/tests/check-rejections.sh b/tests/check-rejections.sh index 8960106..cc65009 100644 --- a/tests/check-rejections.sh +++ b/tests/check-rejections.sh @@ -12,7 +12,7 @@ actual_files=$(rg --files tests/reject -g '*.agda' | sort) [[ "$actual_files" == "$expected_files" ]] || { echo 'FAIL: rejection manifest differs from files'; exit 1; } for fixture in "${fixtures[@]}"; do status=0 - diagnostic=$(agda --no-libraries --safe --without-K --double-check -W error \ + diagnostic=$(agda --no-libraries --safe --without-K --double-check --ignore-interfaces -W error \ -i src -i tests/reject "tests/reject/$fixture.agda" 2>&1) || status=$? if [[ "$status" -eq 0 ]]; then printf 'FAIL: %s unexpectedly type-checked\n' "$fixture"