From 1cd62990eb1225ac30caf2740d58f4fa5effda62 Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Mon, 7 Sep 2026 02:45:43 +0100 Subject: [PATCH 1/4] spec: separate resolution design and tested retrieval fragment --- .github/workflows/actions.lock | 136 +++++++ .github/workflows/boj-build.yml | 3 +- .github/workflows/codeql.yml | 7 +- .github/workflows/dependabot-automerge.yml | 3 +- .github/workflows/dogfood-gate.yml | 17 +- .github/workflows/e2e.yml | 13 +- .github/workflows/fragment-conformance.yml | 37 ++ .github/workflows/governance.yml | 1 + .github/workflows/hypatia-scan.yml | 1 + .github/workflows/instant-sync.yml | 3 +- .github/workflows/label-triage.yml | 1 + .github/workflows/labels.yml | 1 + .github/workflows/mirror.yml | 1 + .github/workflows/openssf-compliance.yml | 3 +- .github/workflows/pages.yml | 9 +- .github/workflows/push-email-notify.yml | 3 +- .github/workflows/release.yml | 11 +- .github/workflows/rhodibot.yml | 3 +- .github/workflows/rust-ci.yml | 1 + .github/workflows/scorecard.yml | 1 + .github/workflows/secret-scanner.yml | 1 + .github/workflows/static-analysis-gate.yml | 23 +- ASSUMPTIONS.adoc | 169 ++++----- PROOF-NARRATIVE.adoc | 336 +++--------------- PROOF-NEEDS.adoc | 105 ++---- READINESS.adoc | 168 +++++---- README.adoc | 204 +++++------ .../0002-query-language-deferred.adoc | 119 ++----- docs/developer/ABI-FFI-README.adoc | 4 +- docs/krl_map.html | 21 +- spec/SURFACES.adoc | 40 +++ spec/grammar.ebnf | 8 +- tests/conformance/retrieval_fragment.jl | 24 ++ tests/smoke/grammar_smoke.sh | 7 +- 34 files changed, 660 insertions(+), 824 deletions(-) create mode 100644 .github/workflows/actions.lock create mode 100644 .github/workflows/fragment-conformance.yml create mode 100644 spec/SURFACES.adoc create mode 100644 tests/conformance/retrieval_fragment.jl diff --git a/.github/workflows/actions.lock b/.github/workflows/actions.lock new file mode 100644 index 0000000..7f029cb --- /dev/null +++ b/.github/workflows/actions.lock @@ -0,0 +1,136 @@ +# 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/boj-build.yml': + - 'actions/checkout@v6.0.2' + '.github/workflows/codeql.yml': + - 'actions/checkout@v6.0.2' + - 'github/codeql-action@v4.34.0' + '.github/workflows/dependabot-automerge.yml': + - 'dependabot/fetch-metadata@v2.2.0' + '.github/workflows/dogfood-gate.yml': + - 'actions/checkout@v4.3.1' + - 'hyperpolymath/a2ml-ecosystem@main' + - 'hyperpolymath/k9-ecosystem@main' + '.github/workflows/e2e.yml': + - 'actions/checkout@v6.0.2' + - 'goto-bus-stop/setup-zig@v2.2.1' + '.github/workflows/fragment-conformance.yml': + - 'actions/checkout@v7.0.0' + - 'julia-actions/setup-julia@v2.7.0' + '.github/workflows/instant-sync.yml': + - 'peter-evans/repository-dispatch@v4.0.1' + '.github/workflows/openssf-compliance.yml': + - 'actions/checkout@v4.3.1' + '.github/workflows/pages.yml': + - 'actions/checkout@v6.0.2' + - 'actions/deploy-pages@v4.0.5' + - 'actions/upload-pages-artifact@v3.0.1' + '.github/workflows/push-email-notify.yml': + - 'hyperpolymath/smtp-notify-action@v0.2.0' + '.github/workflows/release.yml': + - 'actions/checkout@v6.0.2' + - 'actions/upload-artifact@v4.6.2' + - 'softprops/action-gh-release@v2.5.0' + '.github/workflows/rhodibot.yml': + - 'actions/checkout@v4.3.1' + '.github/workflows/static-analysis-gate.yml': + - 'actions/checkout@v6.0.2' + - 'actions/download-artifact@v4.1.8' + - 'actions/upload-artifact@v4.6.2' + - 'erlef/setup-beam@v1.20.4' +dependencies: + 'actions/checkout@v4.3.1': + ref: 'v4.3.1' + commit: 'sha1-34e114876b0b11c390a56381ad16ebd13914f8d5' + owner_id: 44036562 + repo_id: 197814629 + 'actions/checkout@v6.0.2': + ref: 'v6.0.2' + commit: 'sha1-de0fac2e4500dabe0009e67214ff5f5447ce83dd' + owner_id: 44036562 + repo_id: 197814629 + 'actions/checkout@v7.0.0': + ref: 'v7.0.0' + commit: 'sha1-9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0' + owner_id: 44036562 + repo_id: 197814629 + 'actions/deploy-pages@v4.0.5': + ref: 'v4.0.5' + commit: 'sha1-d6db90164ac5ed86f2b6aed7e0febac5b3c0c03e' + owner_id: 44036562 + repo_id: 438112499 + 'actions/download-artifact@v4.1.8': + ref: 'v4.1.8' + commit: 'sha1-fa0a91b85d4f404e444e00e005971372dc801d16' + owner_id: 44036562 + repo_id: 192626254 + 'actions/upload-artifact@v4': + ref: 'v4' + commit: 'sha1-ea165f8d65b6e75b540449e92b4886f43607fa02' + owner_id: 44036562 + repo_id: 192625955 + 'actions/upload-artifact@v4.6.2': + ref: 'v4.6.2' + commit: 'sha1-ea165f8d65b6e75b540449e92b4886f43607fa02' + owner_id: 44036562 + repo_id: 192625955 + 'actions/upload-pages-artifact@v3.0.1': + ref: 'v3.0.1' + commit: 'sha1-56afc609e74202658d3ffba0e8f6dda462b719fa' + owner_id: 44036562 + repo_id: 496012378 + uses: + - 'actions/upload-artifact@v4' + 'dependabot/fetch-metadata@v2.2.0': + ref: 'v2.2.0' + commit: 'sha1-dbb049abf0d677abbd7f7eee0375145b417fdd34' + owner_id: 27347476 + repo_id: 371068214 + 'erlef/setup-beam@v1.20.4': + ref: 'v1.20.4' + commit: 'sha1-e6d7c94229049569db56a7ad5a540c051a010af9' + owner_id: 47606891 + repo_id: 331103973 + 'github/codeql-action@v4.34.0': + ref: 'v4.34.0' + commit: 'sha1-c6f931105cb2c34c8f901cc885ba1e2e259cf745' + owner_id: 9919 + repo_id: 259445878 + 'goto-bus-stop/setup-zig@v2.2.1': + ref: 'v2.2.1' + commit: 'sha1-abea47f85e598557f500fa1fd2ab7464fcb39406' + owner_id: 1006268 + repo_id: 212984112 + 'hyperpolymath/a2ml-ecosystem@main': + ref: 'main' + commit: 'sha1-b6ce942d54b3528f7d7a30d63f57617005fc0d6a' + owner_id: 6759885 + repo_id: 1275649586 + 'hyperpolymath/k9-ecosystem@main': + ref: 'main' + commit: 'sha1-347ee5d6a1b77831de56fe8da21a473724e4cac2' + owner_id: 6759885 + repo_id: 1275650185 + 'hyperpolymath/smtp-notify-action@v0.2.0': + ref: 'v0.2.0' + commit: 'sha1-ede1191ef6ff3ac02c4f4d9efdf837ee517e11d7' + owner_id: 6759885 + repo_id: 1352485172 + 'julia-actions/setup-julia@v2.7.0': + ref: 'v2.7.0' + commit: 'sha1-4c0cb0fce8556fdb04a90347310e5db8b1f98fb9' + owner_id: 53965732 + repo_id: 202020219 + 'peter-evans/repository-dispatch@v4.0.1': + ref: 'v4.0.1' + commit: 'sha1-28959ce8df70de7be546dd1250a005dd32156697' + owner_id: 18365890 + repo_id: 220359305 + 'softprops/action-gh-release@v2.5.0': + ref: 'v2.5.0' + commit: 'sha1-a06a81a03ee405af7f2048a818ed3f03bbf83c7b' + owner_id: 2242 + repo_id: 204253808 diff --git a/.github/workflows/boj-build.yml b/.github/workflows/boj-build.yml index a81237c..1277be3 100644 --- a/.github/workflows/boj-build.yml +++ b/.github/workflows/boj-build.yml @@ -1,3 +1,4 @@ +# This workflow is managed by gh actions-lock. # SPDX-License-Identifier: MPL-2.0 # # OPTIONAL: BoJ Server Build Trigger @@ -23,7 +24,7 @@ jobs: # no-op behaviour. steps: - name: Checkout - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2 + uses: actions/checkout@v6.0.2 - name: Trigger BoJ Server (Casket/ssg-mcp) env: BOJ_URL: ${{ secrets.BOJ_SERVER_URL || vars.BOJ_SERVER_URL }} diff --git a/.github/workflows/codeql.yml b/.github/workflows/codeql.yml index c21d00e..4215dab 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 name: CodeQL Security Analysis on: @@ -31,13 +32,13 @@ jobs: build-mode: none steps: - name: Checkout - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2 + uses: actions/checkout@v6.0.2 - name: Initialize CodeQL - uses: github/codeql-action/init@c6f931105cb2c34c8f901cc885ba1e2e259cf745 # v3 + uses: github/codeql-action/init@v4.34.0 with: languages: ${{ matrix.language }} build-mode: ${{ matrix.build-mode }} - name: Perform CodeQL Analysis - uses: github/codeql-action/analyze@c6f931105cb2c34c8f901cc885ba1e2e259cf745 # v3 + uses: github/codeql-action/analyze@v4.34.0 with: category: "/language:${{ matrix.language }}" diff --git a/.github/workflows/dependabot-automerge.yml b/.github/workflows/dependabot-automerge.yml index bce3810..403756d 100644 --- a/.github/workflows/dependabot-automerge.yml +++ b/.github/workflows/dependabot-automerge.yml @@ -1,3 +1,4 @@ +# This workflow is managed by gh actions-lock. # SPDX-License-Identifier: MPL-2.0 # # dependabot-automerge.yml — enable GitHub's native auto-merge on @@ -51,7 +52,7 @@ jobs: steps: - name: Fetch Dependabot metadata id: meta - uses: dependabot/fetch-metadata@dbb049abf0d677abbd7f7eee0375145b417fdd34 # v2.2.0 + uses: dependabot/fetch-metadata@v2.2.0 with: github-token: ${{ secrets.GITHUB_TOKEN }} # --- Policy gate ------------------------------------------------------- diff --git a/.github/workflows/dogfood-gate.yml b/.github/workflows/dogfood-gate.yml index 7d21f25..59d5df9 100644 --- a/.github/workflows/dogfood-gate.yml +++ b/.github/workflows/dogfood-gate.yml @@ -1,3 +1,4 @@ +# This workflow is managed by gh actions-lock. # SPDX-License-Identifier: MPL-2.0 # Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) # @@ -26,7 +27,7 @@ jobs: steps: - name: Checkout repository - uses: actions/checkout@34e114876b0b11c390a56381ad16ebd13914f8d5 # v4 + uses: actions/checkout@v4.3.1 - name: Check for A2ML files id: detect @@ -43,7 +44,7 @@ jobs: # which taught the validator the colon/brace-block identity form # (`id: "..."`), so docs/governance/TSDM.a2ml failed against the old # pin despite being valid. Bumped to current main. - uses: hyperpolymath/a2ml-ecosystem/validate-action@aa4b836bd969df2bc58128cb8e3d20bbc88d5e79 # main + uses: hyperpolymath/a2ml-ecosystem/validate-action@main with: path: '.' strict: 'false' @@ -75,7 +76,7 @@ jobs: steps: - name: Checkout repository - uses: actions/checkout@34e114876b0b11c390a56381ad16ebd13914f8d5 # v4 + uses: actions/checkout@v4.3.1 - name: Check for K9 files id: detect @@ -92,7 +93,7 @@ jobs: - name: Validate K9 contracts if: steps.detect.outputs.k9_count > 0 - uses: hyperpolymath/k9-ecosystem/validate-action@89f3c2702f4f650a92aa7411502f38da06abd562 # main + uses: hyperpolymath/k9-ecosystem/validate-action@main with: path: '.' strict: 'false' @@ -125,7 +126,7 @@ jobs: steps: - name: Checkout repository - uses: actions/checkout@34e114876b0b11c390a56381ad16ebd13914f8d5 # v4 + uses: actions/checkout@v4.3.1 - name: Scan for invisible characters id: lint @@ -190,7 +191,7 @@ jobs: steps: - name: Checkout repository - uses: actions/checkout@34e114876b0b11c390a56381ad16ebd13914f8d5 # v4 + uses: actions/checkout@v4.3.1 - name: Check for Groove manifest id: groove @@ -249,7 +250,7 @@ jobs: steps: - name: Checkout repository - uses: actions/checkout@34e114876b0b11c390a56381ad16ebd13914f8d5 # v4 + uses: actions/checkout@v4.3.1 - name: Check and validate eclexiaiser manifest id: eclex @@ -324,7 +325,7 @@ jobs: steps: - name: Checkout repository - uses: actions/checkout@34e114876b0b11c390a56381ad16ebd13914f8d5 # v4 + uses: actions/checkout@v4.3.1 - name: Generate dogfooding scorecard run: | diff --git a/.github/workflows/e2e.yml b/.github/workflows/e2e.yml index a71d3ca..738bbf6 100644 --- a/.github/workflows/e2e.yml +++ b/.github/workflows/e2e.yml @@ -1,3 +1,4 @@ +# This workflow is managed by gh actions-lock. # SPDX-License-Identifier: MPL-2.0 # Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) # @@ -43,9 +44,9 @@ jobs: timeout-minutes: 15 steps: - name: Checkout - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2 + uses: actions/checkout@v6.0.2 - name: Set up Zig - uses: goto-bus-stop/setup-zig@abea47f85e598557f500fa1fd2ab7464fcb39406 # v2.2.1 + uses: goto-bus-stop/setup-zig@v2.2.1 with: version: ${{ env.ZIG_VERSION }} - name: Run E2E suite @@ -57,7 +58,7 @@ jobs: timeout-minutes: 10 steps: - name: Checkout - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2 + uses: actions/checkout@v6.0.2 - name: Run aspect tests run: bash tests/aspect_tests.sh @@ -67,7 +68,7 @@ jobs: timeout-minutes: 10 steps: - name: Checkout - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2 + uses: actions/checkout@v6.0.2 - name: Run grammar smoke suite run: bash tests/smoke/grammar_smoke.sh @@ -77,9 +78,9 @@ jobs: timeout-minutes: 15 steps: - name: Checkout - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2 + uses: actions/checkout@v6.0.2 - name: Set up Zig - uses: goto-bus-stop/setup-zig@abea47f85e598557f500fa1fd2ab7464fcb39406 # v2.2.1 + uses: goto-bus-stop/setup-zig@v2.2.1 with: version: ${{ env.ZIG_VERSION }} - name: zig build test diff --git a/.github/workflows/fragment-conformance.yml b/.github/workflows/fragment-conformance.yml new file mode 100644 index 0000000..e629ecf --- /dev/null +++ b/.github/workflows/fragment-conformance.yml @@ -0,0 +1,37 @@ +# This workflow is managed by gh actions-lock. +# SPDX-License-Identifier: MPL-2.0 +name: KRL fragment conformance +on: + pull_request: + push: + branches: [main, master] + workflow_dispatch: +permissions: + contents: read +concurrency: + group: ${{ github.workflow }}-${{ github.ref }} + cancel-in-progress: true +jobs: + fragment: + runs-on: ubuntu-latest + timeout-minutes: 15 + steps: + - name: Checkout specification + uses: actions/checkout@v7.0.0 + with: + persist-credentials: false + - name: Checkout pinned QuandleDB implementation + uses: actions/checkout@v7.0.0 + with: + repository: hyperpolymath/quandledb + ref: 4a00d5cacafd721aee1993bec23c164db425a70d + path: deps/quandledb + persist-credentials: false + - name: Record implementation revision + run: git -C deps/quandledb rev-parse HEAD + - name: Install Julia + uses: julia-actions/setup-julia@v2.7.0 + with: + version: '1.12.6' + - name: Check fragment acceptance and rejection + run: julia --startup-file=no tests/conformance/retrieval_fragment.jl deps/quandledb 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/hypatia-scan.yml b/.github/workflows/hypatia-scan.yml index 31c33e5..93ac840 100644 --- a/.github/workflows/hypatia-scan.yml +++ b/.github/workflows/hypatia-scan.yml @@ -1,3 +1,4 @@ +# This workflow is managed by gh actions-lock. # SPDX-License-Identifier: MPL-2.0 name: Hypatia Security Scan diff --git a/.github/workflows/instant-sync.yml b/.github/workflows/instant-sync.yml index 0994325..766c0a5 100644 --- a/.github/workflows/instant-sync.yml +++ b/.github/workflows/instant-sync.yml @@ -1,3 +1,4 @@ +# This workflow is managed by gh actions-lock. # SPDX-License-Identifier: MPL-2.0 # Instant Forge Sync - Triggers propagation to all forges on push/release name: Instant Sync @@ -14,7 +15,7 @@ jobs: timeout-minutes: 15 steps: - name: Trigger Propagation - uses: peter-evans/repository-dispatch@28959ce8df70de7be546dd1250a005dd32156697 # v3 + uses: peter-evans/repository-dispatch@v4.0.1 with: token: ${{ secrets.FARM_DISPATCH_TOKEN }} repository: hyperpolymath/.git-private-farm 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/mirror.yml b/.github/workflows/mirror.yml index 6bd847d..77f087a 100644 --- a/.github/workflows/mirror.yml +++ b/.github/workflows/mirror.yml @@ -1,3 +1,4 @@ +# This workflow is managed by gh actions-lock. # SPDX-License-Identifier: MPL-2.0 name: Mirror to Git Forges on: diff --git a/.github/workflows/openssf-compliance.yml b/.github/workflows/openssf-compliance.yml index abb7c1e..ac995a4 100644 --- a/.github/workflows/openssf-compliance.yml +++ b/.github/workflows/openssf-compliance.yml @@ -1,3 +1,4 @@ +# This workflow is managed by gh actions-lock. # SPDX-License-Identifier: MPL-2.0 # OpenSSF Best Practices compliance gate — blocks PRs and pushes that lack # required files or still contain unfilled placeholder tokens. @@ -17,7 +18,7 @@ jobs: permissions: contents: read steps: - - uses: actions/checkout@34e114876b0b11c390a56381ad16ebd13914f8d5 # v4 + - uses: actions/checkout@v4.3.1 with: persist-credentials: false - name: Check SECURITY.md exists and has substance diff --git a/.github/workflows/pages.yml b/.github/workflows/pages.yml index 825a763..6924017 100755 --- a/.github/workflows/pages.yml +++ b/.github/workflows/pages.yml @@ -1,3 +1,4 @@ +# This workflow is managed by gh actions-lock. # SPDX-License-Identifier: MPL-2.0 # Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) name: GitHub Pages (Ddraig SSG) @@ -26,9 +27,9 @@ jobs: image: ghcr.io/stefan-hoeck/idris2-pack@sha256:f0758996a931fb35d9ecb1de273c4d59dabe2a09b433afc7e357f65a08b7e1ff steps: - name: Checkout Site - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2 + uses: actions/checkout@v6.0.2 - name: Checkout Ddraig SSG - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2 + uses: actions/checkout@v6.0.2 with: repository: hyperpolymath/ddraig-ssg path: .ddraig-ssg @@ -45,7 +46,7 @@ jobs: fi ./.ddraig-ssg/build/exec/ddraig build src _site https://hyperpolymath.github.io/${GITHUB_REPOSITORY#*/} - name: Upload artifact - uses: actions/upload-pages-artifact@56afc609e74202658d3ffba0e8f6dda462b719fa # v3 + uses: actions/upload-pages-artifact@v3.0.1 with: path: '_site' deploy: @@ -62,4 +63,4 @@ jobs: steps: - name: Deploy to GitHub Pages id: deployment - uses: actions/deploy-pages@d6db90164ac5ed86f2b6aed7e0febac5b3c0c03e # v4 + uses: actions/deploy-pages@v4.0.5 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/release.yml b/.github/workflows/release.yml index 0b50929..4eb83d2 100644 --- a/.github/workflows/release.yml +++ b/.github/workflows/release.yml @@ -1,3 +1,4 @@ +# This workflow is managed by gh actions-lock. # SPDX-License-Identifier: MPL-2.0 # Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) # @@ -19,7 +20,7 @@ jobs: permissions: contents: read steps: - - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2 + - uses: actions/checkout@v6.0.2 - name: Detect project type and build id: build run: | @@ -80,7 +81,7 @@ jobs: changelog: ${{ steps.cliff.outputs.content }} version: ${{ steps.version.outputs.version }} steps: - - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2 + - uses: actions/checkout@v6.0.2 with: fetch-depth: 0 - name: Extract version from tag @@ -105,7 +106,7 @@ jobs: run: | git cliff --output CHANGELOG.md - name: Upload updated CHANGELOG.md - uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02 # v4.6.2 + uses: actions/upload-artifact@v4.6.2 with: name: changelog path: CHANGELOG.md @@ -118,14 +119,14 @@ jobs: permissions: contents: write steps: - - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2 + - uses: actions/checkout@v6.0.2 # TODO: Download build artifacts if uploading to the release # - uses: actions/download-artifact@v4 # with: # name: release-artifacts # path: artifacts/ - name: Create GitHub Release - uses: softprops/action-gh-release@a06a81a03ee405af7f2048a818ed3f03bbf83c7b # v2 + uses: softprops/action-gh-release@v2.5.0 with: body: ${{ needs.changelog.outputs.changelog }} draft: false diff --git a/.github/workflows/rhodibot.yml b/.github/workflows/rhodibot.yml index d020405..cf1034b 100644 --- a/.github/workflows/rhodibot.yml +++ b/.github/workflows/rhodibot.yml @@ -1,3 +1,4 @@ +# This workflow is managed by gh actions-lock. # SPDX-License-Identifier: MPL-2.0 # rhodibot.yml — Automated RSR compliance enforcement # @@ -27,7 +28,7 @@ jobs: timeout-minutes: 15 steps: - name: Checkout - uses: actions/checkout@34e114876b0b11c390a56381ad16ebd13914f8d5 # v4 + uses: actions/checkout@v4.3.1 with: fetch-depth: 1 - name: Rhodibot — Scan and Fix diff --git a/.github/workflows/rust-ci.yml b/.github/workflows/rust-ci.yml index bd1387d..aa8b3cd 100644 --- a/.github/workflows/rust-ci.yml +++ b/.github/workflows/rust-ci.yml @@ -1,3 +1,4 @@ +# This workflow is managed by gh actions-lock. # SPDX-License-Identifier: MPL-2.0 # Rust CI — thin wrapper calling the shared estate reusable in # hyperpolymath/standards. Configure once, propagate everywhere. diff --git a/.github/workflows/scorecard.yml b/.github/workflows/scorecard.yml index 11d9b2a..cd8c045 100644 --- a/.github/workflows/scorecard.yml +++ b/.github/workflows/scorecard.yml @@ -1,3 +1,4 @@ +# This workflow is managed by gh actions-lock. # SPDX-License-Identifier: MPL-2.0 name: OSSF Scorecard diff --git a/.github/workflows/secret-scanner.yml b/.github/workflows/secret-scanner.yml index 0012a87..a56f599 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 name: Secret Scanner on: diff --git a/.github/workflows/static-analysis-gate.yml b/.github/workflows/static-analysis-gate.yml index 7ebf65c..d4c9f9f 100644 --- a/.github/workflows/static-analysis-gate.yml +++ b/.github/workflows/static-analysis-gate.yml @@ -1,3 +1,4 @@ +# This workflow is managed by gh actions-lock. # SPDX-License-Identifier: MPL-2.0 # Static Analysis Gate — Required by branch protection rules. # Runs panic-attack and hypatia, deposits findings for gitbot-fleet learning. @@ -19,7 +20,7 @@ jobs: timeout-minutes: 15 steps: - name: Checkout repository - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2 + uses: actions/checkout@v6.0.2 with: fetch-depth: 0 - name: Install panic-attack (if available) @@ -116,7 +117,7 @@ jobs: echo "" >> "$GITHUB_STEP_SUMMARY" echo "Skipped: panic-attack not available in this environment." >> "$GITHUB_STEP_SUMMARY" - name: Upload panic-attack findings - uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02 # v4 + uses: actions/upload-artifact@v4.6.2 with: name: panic-attack-findings path: panic-attack-findings.json @@ -135,13 +136,13 @@ jobs: timeout-minutes: 15 steps: - name: Checkout repository - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2 + uses: actions/checkout@v6.0.2 with: fetch-depth: 0 - name: Setup Elixir for Hypatia scanner id: beam continue-on-error: true - uses: erlef/setup-beam@e6d7c94229049569db56a7ad5a540c051a010af9 # v1.18.2 + uses: erlef/setup-beam@v1.20.4 with: elixir-version: '1.19.4' otp-version: '28.3' @@ -242,7 +243,7 @@ jobs: echo "" >> "$GITHUB_STEP_SUMMARY" echo "Skipped: Hypatia scanner not available in this environment." >> "$GITHUB_STEP_SUMMARY" - name: Upload hypatia findings - uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02 # v4 + uses: actions/upload-artifact@v4.6.2 with: name: hypatia-findings path: hypatia-findings.json @@ -261,7 +262,7 @@ jobs: timeout-minutes: 15 steps: - name: Checkout repository - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2 + uses: actions/checkout@v6.0.2 with: fetch-depth: 0 - name: Install panic-attack (if available) @@ -323,7 +324,7 @@ jobs: echo "" >> "$GITHUB_STEP_SUMMARY" echo "Skipped: panic-attack not available in this environment." >> "$GITHUB_STEP_SUMMARY" - name: Upload bridge report - uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02 # v4 + uses: actions/upload-artifact@v4.6.2 with: name: bridge-report path: bridge-report.json @@ -345,17 +346,17 @@ jobs: if: always() steps: - name: Download panic-attack findings - uses: actions/download-artifact@fa0a91b85d4f404e444e00e005971372dc801d16 # v4 + uses: actions/download-artifact@v4.1.8 with: name: panic-attack-findings path: findings/ - name: Download hypatia findings - uses: actions/download-artifact@fa0a91b85d4f404e444e00e005971372dc801d16 # v4 + uses: actions/download-artifact@v4.1.8 with: name: hypatia-findings path: findings/ - name: Download bridge report - uses: actions/download-artifact@fa0a91b85d4f404e444e00e005971372dc801d16 # v4 + uses: actions/download-artifact@v4.1.8 with: name: bridge-report path: findings/ @@ -415,7 +416,7 @@ jobs: echo "medium=$MEDIUM" >> "$GITHUB_OUTPUT" echo "low=$LOW" >> "$GITHUB_OUTPUT" - name: Upload unified findings (fleet scanner picks these up) - uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02 # v4 + uses: actions/upload-artifact@v4.6.2 with: name: unified-findings path: findings/unified-findings.json diff --git a/ASSUMPTIONS.adoc b/ASSUMPTIONS.adoc index b1106ec..61f03b6 100644 --- a/ASSUMPTIONS.adoc +++ b/ASSUMPTIONS.adoc @@ -1,144 +1,99 @@ +// SPDX-License-Identifier: CC-BY-SA-4.0 +// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell +[[assumptions-registry--krl]] == Assumptions Registry — KRL -Every load-bearing *unproven* assumption used in this repo, with an ID, -classification, and the obligation it supports. +The corrected link:PROOF-NARRATIVE.adoc[proof narrative] defines current obligation +scope. Unanchored and void rows below are retained as historical design records; +they do not reinstate an adapter, a Tangle compilation target, or a guarantee +from matching index fingerprints. See link:spec/SURFACES.adoc[surface contracts]. -Classifications: - *MATH* — true by an external mathematical theorem -(cite it) - *DESIGN* — true by construction in our code (must remain -true; flag if you change the named code) - *EMPIRICAL* — believed from -testing; not formally verified - *CRYPTO* — standard -cryptographic-primitive assumption +Every load-bearing *unproven* assumption used in this repo, with an +ID, classification, and the obligation it supports. -Cross-references use `+[[A-KR-N.M]]+` syntax, resolved here. +Classifications: + +* *MATH* — true by an external mathematical theorem (cite it) +* *DESIGN* — true by construction in our code (must remain true; flag if you change the named code) +* *EMPIRICAL* — believed from testing; not formally verified +* *CRYPTO* — standard cryptographic-primitive assumption + +Cross-references use `++[[++A-KR-N.M++]]++` syntax, resolved here. ''''' -[width="100%",cols="10%,12%,14%,19%,17%,28%",options="header",] +[cols=",,,,,",options="header",] |=== |ID |Class |Status |Statement |Cited by |Where it lives -|A-KR-1.1 |DESIGN |*UNANCHORED* |Every `+KRLExpr+` AST variant has a -matching arm in the lowering pass |KR-1 |was -`+KRLAdapter.jl/src/parser/lower.jl+` — gone; no lowering pass exists -anywhere - -|A-KR-1.2 |DESIGN |*UNANCHORED* |The AST module defines the only AST -shapes the parser produces |KR-1 |was -`+KRLAdapter.jl/src/parser/ast.jl+` — gone. -`+quandledb/server/krl/Ast.jl+` exists but encodes a _different_ -language (see below) - -|A-KR-2.1 |DESIGN |*UNANCHORED* |Generator arity is fixed: -`+sigma i / sigma_inv i : in=i+1, out=i+1+`; `+cup i : in=0, out=2+`; -`+cap i : in=2, out=0+` |KR-2 |`+spec/grammar.ebnf+` only. No -implementation defines these generators — `+sigma+`, `+cup+` and `+cap+` -appear 0 times in `+quandledb/server/krl/+` - -|A-KR-2.2 |MATH |holds |`+arity_in(a \| b) = arity_in(a) + arity_in(b)+` -and same for output (monoidal-category tensor) |KR-2 |Standard -categorical tangle definition - -|A-KR-3.1 |MATH |holds |Reidemeister’s theorem: R1+R2+R3 generate -isotopy equivalence on tangle diagrams |KR-3 |Reidemeister 1927; -Kauffman _Knots and Physics_ ch. 1 - -|A-KR-3.2 |DESIGN |*UNANCHORED* |`+r1_simplify+` / `+r2_simplify+` / -`+r3_simplify+` implement those moves faithfully |KR-3 |was -`+KRLAdapter.jl/src/operations.jl+` — gone. No Reidemeister -simplification exists in `+quandledb/server/krl/+` - -|A-KR-4.1 |DESIGN |*UNANCHORED* |The pretty-printer’s bracketing is -unambiguous: `+;+` only inside parens; tensor `+\|+` has lower -precedence than compose `+;+` inside parens |KR-4 |No pretty-printer -exists in any current implementation - -|A-KR-6.1 |DESIGN |*VOID* |Two independent parsers both target -`+spec/grammar.ebnf+` v0.1.0 |KR-6 |Only one parser now exists -(`+quandledb/server/krl/Parser.jl+`), and it targets -`+quandledb/spec/grammar.ebnf+`, not this one - -|A-KR-6.2 |DESIGN |*VOID* |Both implementations share the same `+Token+` -enumeration |KR-6 |Only one lexer now exists -(`+quandledb/server/krl/Lexer.jl+`); there is nothing to share with - -|A-KR-8.1 |MATH (partial) |holds |Fundamental-quandle functor is -faithful on prime alternating knots; partial in general |KR-8 |Joyce -1982; for partial cases see Eisermann _The number of knot group -representations_ - -|A-KR-8.2 |MATH |holds |Two non-isomorphic quandles have distinct -canonical presentations (true by definition of "`canonical`") |KR-8 -|Standard algebraic-presentation result +|A-KR-1.1 |DESIGN |*UNANCHORED* |Every `KRLExpr` AST variant has a matching arm in the lowering pass |KR-1 |was `KRLAdapter.jl/src/parser/lower.jl` — gone; no lowering pass exists anywhere +|A-KR-1.2 |DESIGN |*UNANCHORED* |The AST module defines the only AST shapes the parser produces |KR-1 |was `KRLAdapter.jl/src/parser/ast.jl` — gone. `quandledb/server/krl/Ast.jl` exists but encodes a _different_ language (see below) +|A-KR-2.1 |DESIGN |*UNANCHORED* |Generator arity is fixed: `sigma i / sigma++_++inv i : in=i{plus}1, out=i{plus}1`; `cup i : in=0, out=2`; `cap i : in=2, out=0` |KR-2 |`spec/grammar.ebnf` only. No implementation defines these generators — `sigma`, `cup` and `cap` appear 0 times in `quandledb/server/krl/` +|A-KR-2.2 |MATH |holds |`arity++_++in(a {vbar} b) = arity++_++in(a) {plus} arity++_++in(b)` and same for output (monoidal-category tensor) |KR-2 |Standard categorical tangle definition +|A-KR-3.1 |MATH |holds |Reidemeister's theorem: R1{plus}R2{plus}R3 generate isotopy equivalence on tangle diagrams |KR-3 |Reidemeister 1927; Kauffman _Knots and Physics_ ch. 1 +|A-KR-3.2 |DESIGN |*UNANCHORED* |`r1++_++simplify` / `r2++_++simplify` / `r3++_++simplify` implement those moves faithfully |KR-3 |was `KRLAdapter.jl/src/operations.jl` — gone. No Reidemeister simplification exists in `quandledb/server/krl/` +|A-KR-4.1 |DESIGN |*UNANCHORED* |The pretty-printer's bracketing is unambiguous: `;` only inside parens; tensor `{vbar}` has lower precedence than compose `;` inside parens |KR-4 |No pretty-printer exists in any current implementation +|A-KR-6.1 |DESIGN |*VOID* |Two independent parsers both target `spec/grammar.ebnf` v0.1.0 |KR-6 |Only one parser now exists (`quandledb/server/krl/Parser.jl`), and it targets `quandledb/spec/grammar.ebnf`, not this one +|A-KR-6.2 |DESIGN |*VOID* |Both implementations share the same `Token` enumeration |KR-6 |Only one lexer now exists (`quandledb/server/krl/Lexer.jl`); there is nothing to share with +|A-KR-8.1 |MATH (partial) |holds |Fundamental-quandle functor is faithful on prime alternating knots; partial in general |KR-8 |Joyce 1982; for partial cases see Eisermann _The number of knot group representations_ +|A-KR-8.2 |MATH |holds |Two non-isomorphic quandles have distinct canonical presentations (true by definition of "canonical") |KR-8 |Standard algebraic-presentation result |=== -=== On the UNANCHORED and VOID rows +==== On the UNANCHORED and VOID rows -A DESIGN assumption is defined above as _"`true by construction in our -code (must remain true; flag if you change the named code)`"_. Seven -rows named code in `+KRLAdapter.jl+`, which no longer exists, so there -is no construction left to be true by. They are recorded here rather -than deleted, because the statements are still the design intent — but -none of them is currently checkable, and none may be cited as -discharged. +A DESIGN assumption is defined above as _"true by construction in our code +(must remain true; flag if you change the named code)"_. Seven rows named code +in `KRLAdapter.jl`, which no longer exists, so there is no construction left to +be true by. They are recorded here rather than deleted, because the statements +are still the design intent — but none of them is currently checkable, and none +may be cited as discharged. -*UNANCHORED* means the statement stands as intent but names no live -code. *VOID* means the statement presupposes two implementations, and -only one exists. +*UNANCHORED* means the statement stands as intent but names no live code. +*VOID* means the statement presupposes two implementations, and only one +exists. -Re-anchoring is blocked on the specification itself. -`+spec/grammar.ebnf+` (here) and `+quandledb/spec/grammar.ebnf+` are -disjoint on core vocabulary: the braid generators these assumptions -describe appear only in the former, and only the latter is implemented. -Until the two are reconciled and a conformance suite exists, these rows -cannot be re-anchored to anything. See `+READINESS.md+`. +Re-anchoring is blocked on the specification itself. `spec/grammar.ebnf` (here) +and `quandledb/spec/grammar.ebnf` are disjoint on core vocabulary: the braid +generators these assumptions describe appear only in the former, and only the +latter is implemented. Until the two are reconciled and a conformance suite +exists, these rows cannot be re-anchored to anything. See `READINESS.adoc`. ''''' === How to use this file -* *Reading code.* When you see a function whose correctness depends on -something not enforced by the local types — _that’s an assumption_. Find -or add the entry here and reference it by ID. -* *Writing a proof.* Every proof obligation in PROOF-NARRATIVE.md names -its assumptions by ID. Before discharging the proof, audit the -assumptions. -* *Modifying load-bearing code.* Each DESIGN assumption names a file. If -you edit that file, re-validate the assumption (or update the obligation -if you changed the design intentionally). - +* *Reading code.* When you see a function whose correctness depends +on something not enforced by the local types — _that's an +assumption_. Find or add the entry here and reference it by ID. +* *Writing a proof.* Every proof obligation in +PROOF-NARRATIVE.adoc names its assumptions by +ID. Before discharging the proof, audit the assumptions. +* *Modifying load-bearing code.* Each DESIGN assumption names a +file. If you edit that file, re-validate the assumption (or update +the obligation if you changed the design intentionally). + +[[promoting--demoting-assumptions]] === Promoting / demoting assumptions -[width="100%",cols="30%,25%,45%",options="header",] +[cols=",,",options="header",] |=== |From |To |Trigger |EMPIRICAL → MATH |discharge with a citation | - |EMPIRICAL → DESIGN |refactor to make it a structural invariant | - -|MATH → (delete) |obligation it supports has been re-cast not to need it -| - +|MATH → (delete) |obligation it supports has been re-cast not to need it | |DESIGN → MATH (rare) |the design happens to encode a known theorem | - -|any → CRYPTO |only for cryptographic primitives (BLAKE3, SHA-256, etc.) -| +|any → CRYPTO |only for cryptographic primitives (BLAKE3, SHA-256, etc.) | |=== -When you change a row, leave a one-line note at the bottom of this file -with the date and reason. +When you change a row, leave a one-line note at the bottom of this +file with the date and reason. ''''' === Changelog -[width="100%",cols="32%,42%,26%",options="header",] +[cols=",,",options="header",] |=== |Date |Change |By |2026-06-01 |Initial registry, scoped to KRL surface obligations |Audit - -|2026-07-21 |Added Status column. Marked A-KR-1.1, 1.2, 2.1, 3.2 and 4.1 -UNANCHORED and A-KR-6.1, 6.2 VOID: all seven named code in -`+KRLAdapter.jl+`, which no longer exists. Verified that no replacement -exists — `+sigma+`, `+cup+`, `+cap+`, `+r1_simplify+` and any -pretty-printer appear 0 times in `+quandledb/server/krl/+`. The four -MATH rows are unaffected. |Audit +|2026-07-21 |Added Status column. Marked A-KR-1.1, 1.2, 2.1, 3.2 and 4.1 UNANCHORED and A-KR-6.1, 6.2 VOID: all seven named code in `KRLAdapter.jl`, which no longer exists. Verified that no replacement exists — `sigma`, `cup`, `cap`, `r1++_++simplify` and any pretty-printer appear 0 times in `quandledb/server/krl/`. The four MATH rows are unaffected. |Audit |=== diff --git a/PROOF-NARRATIVE.adoc b/PROOF-NARRATIVE.adoc index d194055..2c1576f 100644 --- a/PROOF-NARRATIVE.adoc +++ b/PROOF-NARRATIVE.adoc @@ -1,305 +1,57 @@ -== Proof Narrative — KRL +// SPDX-License-Identifier: CC-BY-SA-4.0 +// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell +== KRL proof narrative -This file is the *single coherent story* of what KRL proves, what it -assumes, and what it has left to prove. It is the document a reader -should open first when asking _"`is this language sound, and how do I -know?`"_. +KRL expresses construction, transformation, resolution and retrieval for QuandleDB. +This repository owns its specification. The running fragment is implemented by +`quandledb/server/krl/`: source → Julia AST → evaluator → data/semantic providers. +link:spec/SURFACES.adoc[Surface contracts] separate that fragment from the construction +and resolution draft. No theorem about the whole KRL language is established by +fragment tests. -For the per-obligation status checklist, see PROOF-NEEDS.md. For the -registry of every load-bearing unproven assumption, see ASSUMPTIONS.md. +Skein.jl is an independent Julia library for knot storage/indexing and invariants. +KnotTheory.jl is an independent mathematical toolkit. QuandleDB uses these libraries, +but their purpose is broader than implementing KRL operations. Tangle is a separate +Turing-complete language for knot mathematics. KRL has no Tangle compilation target +and inherits no Tangle proof result. -''''' +=== Evidence that runs -=== 1. Position in the stack +`tests/conformance/retrieval++_++fragment.jl` tests source acceptance, AST structure, +malformed-input rejection and rejection of the unimplemented construction draft. +It runs against an explicitly supplied QuandleDB checkout. The evaluator's +`resolution++_++boundary++_++test.jl` supplies deliberately colliding index buckets: +heuristic candidates are returned with a warning, while requests for stronger +assurance fail. It also checks that filtering to zero rows stays empty. -KRL is the *surface language* of a four-layer federated stack. It is -_not_ a standalone implementation; the canonical implementations live in -sibling repos: +These are executable regression controls. They do not prove grammar equivalence, +termination for arbitrary source, isotopy invariance or completeness of resolution. -.... -┌─────────────────────────────────────────────────────────┐ -│ KRL surface language (this repo) │ -│ • spec/grammar.ebnf (v0.1.0) │ -│ • Idris2 ABI types (src/interface/Abi/) │ -│ • Zig FFI scaffold (src/interface/ffi/) │ -│ • examples (examples/) │ -└─────────────────┬───────────────────────────────────────┘ - │ implements - ▼ -┌─────────────────────────────────────────────────────────┐ -│ KRLAdapter.jl — canonical parser / lower │ -│ quandledb/server/krl/ — server-side query parser │ -└─────────────────┬───────────────────────────────────────┘ - │ lowers to - ▼ -┌─────────────────────────────────────────────────────────┐ -│ TangleIR — canonical interchange object │ -└─────────────────┬───────────────────────────────────────┘ - │ semantics on - ▼ -┌─────────────────────────────────────────────────────────┐ -│ Tangle (hyperpolymath/tangle) — proven core │ -│ Progress · Preservation · Determinism · Type Safety │ -└─────────────────┬───────────────────────────────────────┘ - │ persisted+queried via - ▼ -┌─────────────────────────────────────────────────────────┐ -│ Skein.jl + QuandleDB — storage + semantic index │ -└─────────────────────────────────────────────────────────┘ -.... +=== Obligations and corrections -Consequence: *this repo’s proof obligations are spec-level, not -implementation-level*. We owe a precise definition of what a KRL program -_is_, plus refinement-style obligations against the two parser -implementations. +Historical obligation IDs are retained below to explain their disposition; references +in older assumption/checklist files must be read against this corrected boundary. -=== 2. Proven now - -[cols=",,,",options="header",] +[cols=",,",options="header",] |=== -|ID |Statement |Form |Where -|— |_none yet at the KRL surface level_ |— |— +|ID |Current obligation |Status +|KR-1 |Accepted syntax must either execute with defined semantics or report a specific unsupported operation. |Fragment tested; total lowering to Tangle was a mistaken claim and is withdrawn. +|KR-2 |Construct/compose must check port arity and preserve it. |Design obligation; no KRL construction checker claimed. +|KR-3 |Each implemented transformation must preserve its stated equivalence relation. |Requires evidence for the actual rewrite implementation; no inherited theorem. +|KR-4 |Parse/print round-trip for each supported surface. |Open; acceptance fixtures alone do not establish it. +|KR-5 |ABI/FFI declarations must agree with and reach real implementations. |ABI compilation alone does not discharge this. +|KR-6 |Fragment grammar and actual parser must agree. |An executable corpus now exists; full conformance remains open. The former two-parser comparison against a nonexistent adapter is withdrawn. +|KR-7 |Generator indices and arities must be valid. |Draft/example lexical checks only; no runtime construction guarantee. +|KR-8 |A successful equivalence resolution must carry evidence sufficient for its declared claim and scope. |Index candidates are labelled heuristic; stronger requests are refused until a witness checker is implemented. |=== -The Idris2 / Lean / Coq files previously sitting under -`+verification/proofs/+` were rsr-template-repo boilerplate (generic -`+Bounded+`, `+ApiResult+`, typed-arithmetic `+TypeSafety+`). They -asserted nothing about KRL. They have been deleted in the same PR as -this narrative to avoid the "`looks proven, isn’t`" failure mode. Their -content is recoverable from the PR description if anyone wants the -template back. - -*The actually-proven results that the KRL stack benefits from live in -`+hyperpolymath/tangle/proofs/Tangle.lean+`* (16 theorems and lemmas -including Progress, Preservation, Determinism, and Type Safety for the -core Tangle calculus that KRL lowers into). See the tangle repo’s -`+PROOF-NARRATIVE.md+` for details. Until KRL has its own surface -proofs, the soundness story rests on (a) the Tangle core proofs and (b) -the _unproven_ claim that KRL faithfully lowers into that core. That -claim is `+KR-1+` and `+KR-2+` below. - -=== 3. Obligations (the narrative arc) - -The arc from "`KRL text`" to "`trusted query result`": - -.... -KRL source text - │ [KR-7] parser rejects ill-typed concrete syntax - ▼ -KRLProgram AST - │ [KR-1] lowering is total on parseable programs - │ [KR-2] lowering preserves port arity - ▼ -TangleIR - │ [hyperpolymath/tangle: T-Progress, T-Preservation, T-Determinism] - ▼ -Tangle value - │ [KR-3] simplify is semantics-preserving - │ [KR-8] equivalent? is sound w.r.t. fundamental-quandle iso - ▼ -Query result -.... - -Each obligation in detail: - -==== KR-1 — Lowering is total on parseable programs - -*Claim.* For every `+KRLProgram p+` produced by `+parse_krl+`, the -function `+lower(p)+` returns a `+TangleIR+` (never raises -`+KRLLowerError+`). - -*Why valuable.* A `+KRLLowerError+` at runtime means the parser accepted -a program that the lowering rejected — a soundness regression that the -lexer/parser/AST should have prevented. Closing this proves -parser-and-lowering agree on the language. - -*Status.* Unproven. Currently `+KRLLowerError+` is raised from -`+KRLAdapter.jl/src/parser/lower.jl+` on (a) unbound identifiers and (b) -un-matched AST variants. Case (a) is correct (it’s a real user error); -case (b) is the soundness gap. - -*Assumptions (load-bearing for this claim).* - [[A-KR-1.1]] Every -`+KRLExpr+` AST variant has a matching arm in `+lower.jl+`. - -[[A-KR-1.2]] The AST defined in `+KRLAdapter.jl/src/parser/ast.jl+` is -the _only_ AST shape the parser can produce. - -*How to discharge.* Add an exhaustiveness check to the lowering function -(compile-time in Julia is weak; consider a property-based test -enumerating every constructor as a stop-gap, with Idris2 as the target -prover for the long term). - -==== KR-2 — Lowering preserves port arity - -*Claim.* If `+p : KRLProgram+` lowers to `+ir : TangleIR+`, then for -every sub-expression `+(compose a b)+` in `+p+`, the number of output -ports of `+lower(a)+` equals the number of input ports of `+lower(b)+`. - -*Why valuable.* Composition is the central operation. Without this, you -can write KRL that lowers to ill-formed TangleIR — e.g. composing a -2-strand braid with a 3-strand tangle — and the error surfaces -downstream as garbled invariant computation, not as a clear "`your -program is wrong`" message. - -*Status.* Unproven, and the typechecker that would enforce this at parse -time is *not yet implemented* (acknowledged in `+READINESS.md+` under -"`Path to C`"). - -*Assumptions.* - [[A-KR-2.1]] Generators have known fixed arity: -`+sigma i : in=i, out=i+1+` (and same arity in/out), -`+cup i : in=0, out=2+`, `+cap i : in=2, out=0+`. - [[A-KR-2.2]] -Tensor and compose distribute over arity in the obvious way: -`+arity_in(a | b) = arity_in(a) + arity_in(b)+`. - -*How to discharge.* Implement port-arity checking in the typechecker; -prove the typechecker sound against this property. - -==== KR-3 — `+simplify+` is semantics-preserving - -*Claim.* For every `+e : KRLExpr+` and its simplified form -`+e' = simplify(e)+`, the lowered TangleIR objects `+lower(e)+` and -`+lower(e')+` represent the same tangle up to isotopy. - -*Why valuable.* This is the _retrieval guarantee_: queries against the -simplified form must return the same answer as queries against the -original. Without it, simplification is a performance trick that can -change semantics. - -*Status.* Unproven; `+simplify+` is partially implemented in -KRLAdapter.jl (R2 detection works inside a single sigma sequence but not -across `+compose+` boundaries — see `+READINESS.md+`). - -*Assumptions.* - [[A-KR-3.1]] R1, R2, R3 are the complete set of local -moves needed to relate isotopic tangles (Reidemeister’s theorem; -mathematically established). - [[A-KR-3.2]] `+r1_simplify+`, -`+r2_simplify+`, `+r3_simplify+` (when implemented; R3 is currently a -gap — see `+quandledb/PROOF-NARRATIVE.md+` QD-2) faithfully implement -those moves. - -*How to discharge.* Prove each rewrite preserves the fundamental quandle -presentation (which encodes isotopy). - -==== KR-4 — Pretty-print/parse round-trip - -*Claim.* For every `+e : KRLExpr+` produced by `+parse_krl+`, -`+parse_krl(pretty(e)) = e+`. - -*Why valuable.* A free fuzz oracle. Catches a whole class of "`lossy -IR`" bugs at the parse boundary. Also the foundation of the -`+reconstruct_source+` claim in `+README.adoc+`. - -*Status.* Unproven; `+pretty+` exists in KRLAdapter.jl but no round-trip -test. - -*Assumptions.* - [[A-KR-4.1]] The pretty-printer’s choice of bracketing -is unambiguous w.r.t. the grammar (e.g. `+;+` only inside parens at the -expression level — see `+READINESS.md+`). - -*How to discharge.* Add a property test in `+KRLAdapter.jl/test/+` that -round-trips every well-formed program from `+examples/+`. - -==== KR-5 — Idris2/Zig ABI primitives are load-bearing - -*Claim.* `+SafePtr+`, `+Handle+`, `+Bounded+`, `+NonEmpty+` (currently -in `+src/interface/Abi/+` and `+verification/proofs/idris2/+`) must -either be *referenced by the actual Zig FFI surface* or be deleted. - -*Why valuable.* Right now they’re floating. They were rsr-template -content; they have non-trivial dependent-type structure but no consumer. - -*Status.* Decision pending. Recommended decision: keep `+SafePtr+` and -`+Handle+`, wire them through the FFI; delete `+Bounded+` and -`+NonEmpty+` as unused. - -==== KR-6 — Two-parser equivalence - -*Claim.* For every input string `+s+`, `+KRLAdapter.jl::parse_krl(s)+` -and `+quandledb/server/krl/Parser.jl::parse_any(s)+` either both succeed -with equal ASTs or both fail. - -*Why valuable.* The two implementations exist by design — one for -end-user code, one for query-time parsing — but if they accept different -languages, the server can run queries the user can’t write, and vice -versa. - -*Status.* Unproven; no differential test exists. - -*Assumptions.* - [[A-KR-6.1]] Both implementations target the same EBNF -grammar (`+spec/grammar.ebnf+` v0.1.0). - [[A-KR-6.2]] Both -implementations have the same notion of "`valid identifier`", "`valid -integer literal`", "`valid string literal`". - -*How to discharge.* Build a differential fuzz harness that feeds random -strings to both and asserts result equivalence. Easy single PR. - -==== KR-7 — Generator-index validity - -*Claim.* `+sigma N+`, `+sigma_inv N+`, `+cup N+`, `+cap N+` are accepted -iff `+N ≥ 1+`. - -*Why valuable.* Small but catches a real class of off-by-one bugs; also -a parser-level invariant that should be asserted explicitly. - -*Status.* Currently encoded in the existing parser-error case ("`zero -index`" rejected). Not asserted as a property test. - -==== KR-8 — `+equivalent?+` is sound w.r.t. quandle isomorphism - -*Claim.* If `+equivalent?(a, b)+` returns `+true+`, then the fundamental -quandles of `+a+` and `+b+` are isomorphic. - -*Why valuable.* This is the central claim of the retrieval layer. False -positives mean the database lies; without this, `+equivalent?+` is -heuristic, not semantic. - -*Status.* Unproven; implementation in QuandleDB. Soundness rests on -[[A-KR-8.1]] and the fingerprint determinism claim -`+quandledb/PROOF-NARRATIVE.md+` QD-4. - -*Assumptions.* - [[A-KR-8.1]] Fundamental-quandle functor is _faithful_ -on isotopy classes (true for prime alternating knots; partial in general -— this needs to be a stated and bounded assumption). - [[A-KR-8.2]] -Fingerprint collisions are mathematically impossible for non-isomorphic -quandles (this is a property of the canonicalisation, not the hash). - -*How to discharge.* Either: - Restrict the claim to the -prime-alternating subset (where the functor is provably faithful), or - -State the obligation as "`equivalence is sound modulo the -fundamental-quandle relation`", which is weaker but provable. - -=== 4. The "`stupid proof`" exclusions - -For completeness, things we deliberately do *not* prove: - -* _"``+KRLProgram+` is a record with these fields`"_ — enforced by the -Julia type system; no proof needed. -* _"``+parse_krl+` returns a `+KRLProgram+``"_ — Julia type assertion. -* _"`Compose is associative when types agree`"_ — implied by list-append -associativity. -* _"`BLAKE3 is collision-resistant`"_ — out of scope; cryptographic -primitive assumption inherited from QuandleDB. - -If you find yourself drafting a proof in one of these categories, delete -the draft. - -=== 5. How to add a new obligation - -[arabic] -. Add an entry to PROOF-NEEDS.md with an ID (`+KR-N+`), category, -prover, priority, effort estimate. -. Add the narrative entry here: statement, _why valuable_, status, -*assumptions*, how to discharge. The assumptions block is non-optional. -. For each new assumption, add an entry to ASSUMPTIONS.md with an ID -(`+A-KR-N.M+`) and a note on whether it is _mathematical_ (true by -external theorem), _design_ (true by our construction), or _empirical_ -(believed, not verified). +=== Resolution is more than a lookup -=== 6. References +Equal invariant values can nominate candidates. Equality of selected invariants, +a matching fingerprint or membership in an index bucket is not by itself an isotopy +witness. The declared assurance threshold is a demand on the implementation, never +evidence supplied by the requester. Missing index data means unresolved, not unequal. -* Architecture: README.adoc, section "`Architecture position`". -* Companion narratives: -** `+hyperpolymath/tangle/PROOF-NARRATIVE.md+` — semantic core proofs -** `+hyperpolymath/quandledb/PROOF-NARRATIVE.md+` — quandle / DB proofs -* Implementations: -** `+KRLAdapter.jl+` — canonical parser, AST, lower -** `+quandledb/server/krl/+` — server-side query parser -* Spec: spec/grammar.ebnf, spec/grammar-overview.md. +The next substantive proof work belongs at the implemented parser, transformation +and witness boundaries. A future unified grammar must settle the conflicting use +of `++|++` before claiming execution across all four operation families. diff --git a/PROOF-NEEDS.adoc b/PROOF-NEEDS.adoc index 2367ee2..cf6402a 100644 --- a/PROOF-NEEDS.adoc +++ b/PROOF-NEEDS.adoc @@ -1,76 +1,53 @@ +// SPDX-License-Identifier: CC-BY-SA-4.0 +// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell +[[proof-requirements--krl]] == Proof Requirements — KRL ____ -The single coherent story is PROOF-NARRATIVE.md. The assumption registry -is ASSUMPTIONS.md. This file is the *per-obligation checklist* with -status, prover, priority. +The single coherent story is PROOF-NARRATIVE.adoc. +The assumption registry is ASSUMPTIONS.adoc. +This file is the *per-obligation checklist* with status, prover, priority. ____ === Proof Tier -*Tier:* T2 — High. KRL is the surface language of a federated stack -whose correctness claims (semantic-equivalence queries, -isotopy-respecting retrieval) rest on KRL→TangleIR lowering being -trustworthy. The semantic core (TangleIR/Tangle) is already partially -proven; KRL’s job is to guarantee faithful lowering. +*Tier:* T2 — High. +KRL's assurance must come from its actual parser, transformation implementations +and resolution witnesses. QuandleDB implements the current fragment. Tangle is +a separate language and supplies no inherited KRL proof guarantee. === Proof categories -[width="100%",cols="24%,36%,40%",options="header",] +[cols=",,",options="header",] |=== |Code |Meaning |Applies? |*TP* |Typing proofs (port-arity, lowering totality) |Yes - |*INV* |Invariant proofs (round-trip, grammar refinement) |Yes - |*SEC* |Security proofs |No - |*CONC* |Concurrency proofs |No - |*ALG* |Algorithm proofs (simplification correctness) |Yes - -|*ABI* |ABI/FFI proofs (Zig FFI boundary, Idris2 layout) |Yes (low -priority) - +|*ABI* |ABI/FFI proofs (Zig FFI boundary, Idris2 layout) |Yes (low priority) |*DOM* |Domain proofs (quandle equivalence soundness) |Yes |=== === Obligations -[width="100%",cols="9%,18%,17%,13%,17%,13%,13%",options="header",] +[cols=",,,,,,",options="header",] |=== -|# |Statement |Category |Prover |Priority |Effort |Status -|KR-1 |`+lower+` is total on parseable programs |TP |Idris2 + Julia -property test |P1 |1d |NOT STARTED - -|KR-2 |`+lower+` preserves port arity |TP |Idris2 + typechecker impl |P1 -|3d |NOT STARTED (typechecker not implemented) - -|KR-3 |`+simplify+` is semantics-preserving (KR-3a: R1; KR-3b: R2; -KR-3c: R3) |ALG |Lean4 or property test against quandle iso |P1 |5d -|PARTIAL (R2 across compose() is gap) - -|KR-4 |Pretty/parse round-trip: `+parse(pretty(e)) = e+` |INV |Julia -property test (cheap) |P1 |4h |NOT STARTED - -|KR-5 |Idris2 `+SafePtr+` / `+Handle+` are load-bearing in the Zig FFI -surface |ABI |Decision + wiring |P3 |2h |DECISION PENDING - -|KR-6 |`+KRLAdapter.jl::parse_krl+` ≡ -`+quandledb/server/krl::parse_any+` on the v0.1.0 grammar |INV -|Differential property test |P1 |4h |NOT STARTED - -|KR-7 |`+sigma N+`, `+cup N+`, etc. accepted iff `+N ≥ 1+` |INV |Grammar -smoke test extension |P2 |1h |PARTIAL (error path exists, not -property-tested) - -|KR-8 |`+equivalent?+` is sound w.r.t. fundamental-quandle isomorphism -|DOM |Lean4 (factored through QuandleDB’s QD-3) |P1 |5d |NOT STARTED +|++#++ |Statement |Category |Prover |Priority |Effort |Status +|KR-1 |Accepted fragment operations execute with defined semantics or explicit refusal |TP |Idris2 {plus} Julia property test |P1 |1d |NOT STARTED +|KR-2 |Construction/composition preserve checked port arity |TP |Idris2 {plus} typechecker impl |P1 |3d |NOT STARTED (typechecker not implemented) +|KR-3 |`simplify` is semantics-preserving (KR-3a: R1; KR-3b: R2; KR-3c: R3) |ALG |Lean4 or property test against quandle iso |P1 |5d |OPEN (no KRL transformation implementation claimed) +|KR-4 |Pretty/parse round-trip: `parse(pretty(e)) = e` |INV |Julia property test (cheap) |P1 |4h |NOT STARTED +|KR-5 |Idris2 `SafePtr` / `Handle` are load-bearing in the Zig FFI surface |ABI |Decision {plus} wiring |P3 |2h |DECISION PENDING +|KR-6 |Declared fragment agrees with `quandledb/server/krl/Parser.jl` |INV |Acceptance/rejection corpus |P1 |— |PARTIAL (11 checks; full conformance open) +|KR-7 |`sigma N`, `cup N`, etc. accepted iff `N ≥ 1` |INV |Grammar smoke test extension |P2 |1h |DRAFT (example lexical checks only) +|KR-8 |`equivalent?` is sound w.r.t. fundamental-quandle isomorphism |DOM |Lean4 (factored through QuandleDB's QD-3) |P1 |5d |NOT STARTED |=== -For full statements, _why valuable_, and the assumptions each obligation -rests on, see PROOF-NARRATIVE.md. For the assumptions themselves, see -ASSUMPTIONS.md. +For full statements, _why valuable_, and the assumptions each +obligation rests on, see PROOF-NARRATIVE.adoc. +For the assumptions themselves, see ASSUMPTIONS.adoc. === Dangerous patterns (BANNED) @@ -79,17 +56,17 @@ CI rejects any PR introducing any of these: [cols=",,",options="header",] |=== |Pattern |Language |Meaning -|`+believe_me+` |Idris2 |Unsafe cast -|`+assert_total+` |Idris2 |Skip totality check -|`+postulate+` |Idris2 / Agda |Unproven axiom -|`+sorry+` |Lean4 |Incomplete proof -|`+Admitted+` |Coq |Incomplete proof -|`+unsafeCoerce+` |Haskell |Unsafe cast -|`+Obj.magic+` |OCaml / ReScript |Unsafe cast -|`+unsafe+` (unaudited) |Rust |Unsafe block without safety comment +|`believe++_++me` |Idris2 |Unsafe cast +|`assert++_++total` |Idris2 |Skip totality check +|`postulate` |Idris2 / Agda |Unproven axiom +|`sorry` |Lean4 |Incomplete proof +|`Admitted` |Coq |Incomplete proof +|`unsafeCoerce` |Haskell |Unsafe cast +|`Obj.magic` |OCaml / ReScript |Unsafe cast +|`unsafe` (unaudited) |Rust |Unsafe block without safety comment |=== -Enforced by `+panic-attack assail --proofs-only+`. +Enforced by `panic-attack assail --proofs-only`. === Where proofs go @@ -97,16 +74,12 @@ Enforced by `+panic-attack assail --proofs-only+`. verification/proofs/ ├── idris2/ — ABI / type-level invariants (KR-1, KR-2, KR-5) ├── lean4/ — Semantic claims (KR-3, KR-8) -└── julia/ — Property tests against KRLAdapter.jl (KR-4, KR-6, KR-7) +└── julia/ — Property tests against the declared QuandleDB fragment (KR-4, KR-6, KR-7) .... -(The previous `+coq/+` directory has been removed; obligations have been -re-allocated to Lean4 where the Tangle metatheory lives.) - === References -* Companion narratives: `+hyperpolymath/tangle/PROOF-NARRATIVE.md+` -(semantic core), `+hyperpolymath/quandledb/PROOF-NARRATIVE.md+` (quandle -/ DB). -* Implementations under proof: `+KRLAdapter.jl+`, -`+quandledb/server/krl/+`. +* link:PROOF-NARRATIVE.adoc[Current narrative and obligation dispositions]. +* link:spec/SURFACES.adoc[Surface contracts]. +* `hyperpolymath/quandledb/PROOF-NARRATIVE.md` — database semantic obligations. +* Implementation under test: `quandledb/server/krl/`. diff --git a/READINESS.adoc b/READINESS.adoc index 8afbd23..2fbc1e3 100644 --- a/READINESS.adoc +++ b/READINESS.adoc @@ -1,144 +1,138 @@ +// SPDX-License-Identifier: CC-BY-SA-4.0 +// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell +[[component-readiness--krl]] == Component Readiness — KRL -*Standard:* -https://github.com/hyperpolymath/standards/tree/main/component-readiness-grades[CRG -v2.0 STRICT] *Current Grade:* E *Assessed:* 2026-07-21 (demoted D → E) +Update 2026-09-07: an executable retrieval-fragment conformance corpus now passes +11 checks against the local QuandleDB parser. The construction/resolution draft +remains unimplemented. See link:spec/SURFACES.adoc[surface contracts] and the corrected +link:PROOF-NARRATIVE.adoc[proof narrative]. The assessment below is dated history; +this update does not assign a new whole-language readiness grade. + +*Standard:* https://github.com/hyperpolymath/standards/tree/main/component-readiness-grades[CRG v2.0 STRICT] +*Current Grade:* E +*Assessed:* 2026-07-21 (demoted D → E) *Assessor:* Jonathan D.A. Jewell ''''' +[[why-the-grade-moved-d--e]] === Why the grade moved D → E -The previous assessment (2026-04-12) recorded Grade D on the strength of -a parser, AST, recursive-descent implementation and a 57-test matrix, -all of which lived in `+KRLAdapter.jl+`. *That repository no longer -exists* — it was discarded, deliberately and not recoverably. +The previous assessment (2026-04-12) recorded Grade D on the strength of a +parser, AST, recursive-descent implementation and a 57-test matrix, all of +which lived in `KRLAdapter.jl`. *That repository no longer exists* — it was +discarded, deliberately and not recoverably. -None of the D evidence can be checked. Under the CRG demotion table, -`+D → E+` applies when _"`the scope narrows so far that the component -barely does anything`"_, which is precisely what happened: with the -adapter gone, nothing in this repository can parse or execute a KRL -program. +None of the D evidence can be checked. Under the CRG demotion table, `D → E` +applies when _"the scope narrows so far that the component barely does +anything"_, which is precisely what happened: with the adapter gone, nothing in +this repository can parse or execute a KRL program. -This is a correction to the record, not a regression in the work. The -grade was restated rather than left standing on evidence nobody can -inspect. +This is a correction to the record, not a regression in the work. The grade was +restated rather than left standing on evidence nobody can inspect. ''''' === Grade rationale (evidence for E) -Grade E criterion: _"`Does something slight … there is a kernel of value -… at least one successful test case demonstrating the kernel of -functionality, and documentation of known failures and limitations.`"_ +Grade E criterion: _"Does something slight … there is a kernel of value … at +least one successful test case demonstrating the kernel of functionality, and +documentation of known failures and limitations."_ -Every item below was executed on 2026-07-21, not inferred from -documentation. +Every item below was executed on 2026-07-21, not inferred from documentation. ==== Evidence -[width="100%",cols="34%,33%,33%",options="header",] +[cols=",,",options="header",] |=== |Artefact |Check |Result -|`+spec/grammar.ebnf+` |114-line EBNF, v0.1.0 |present - -|`+examples/*.krl+` |4 example programs |present - -|`+tests/smoke/grammar_smoke.sh+` |lexical conformance of examples to -the grammar |20 checks, all pass - -|`+src/interface/ffi/+` |`+zig build test+` |3/3 pass - -|`+src/interface/ffi/+` |`+zig build+` |produces `+libkrl.a+` - -|`+src/interface/Abi/+` |`+%foreign+` declarations |4, all covered by 11 -Zig exports - -|`+tests/aspect_tests.sh+` |SPDX, banned constructs, ABI/FFI -correspondence |4/4 pass - -|`+tests/e2e.sh+` |full local pipeline |4/4 pass, negative-controlled +|`spec/grammar.ebnf` |114-line EBNF, v0.1.0 |present +|`examples/++*++.krl` |4 example programs |present +|`tests/smoke/grammar++_++smoke.sh` |lexical conformance of examples to the grammar |20 checks, all pass +|`src/interface/ffi/` |`zig build test` |3/3 pass +|`src/interface/ffi/` |`zig build` |produces `libkrl.a` +|`src/interface/Abi/` |`%foreign` declarations |4, all covered by 11 Zig exports +|`tests/aspect++_++tests.sh` |SPDX, banned constructs, ABI/FFI correspondence |4/4 pass +|`tests/e2e.sh` |full local pipeline |4/4 pass, negative-controlled |=== -The kernel of value is the specification plus a set of examples that -provably conform to it at the lexical level, over a C ABI that compiles -and is tested. +The kernel of value is the specification plus a set of examples that provably +conform to it at the lexical level, over a C ABI that compiles and is tested. ==== Known failures and limitations -* *No parser, and therefore no execution.* Nothing in this repository -can read a `+.krl+` program and produce a result. `+grammar_smoke.sh+` -is lexical only and says so in its own header. -* *The specification is contested.* `+spec/grammar.ebnf+` here and -`+quandledb/spec/grammar.ebnf+` both claim to be KRL v0.1.0 and are -disjoint on core vocabulary; `+|+` is bound to opposite meanings in the -two. See README. +* *No parser, and therefore no execution.* Nothing in this repository can +read a `.krl` program and produce a result. `grammar++_++smoke.sh` is lexical +only and says so in its own header. +* *The specification is contested.* `spec/grammar.ebnf` here and +`quandledb/spec/grammar.ebnf` both claim to be KRL v0.1.0 and are disjoint on +core vocabulary; `++|++` is bound to opposite meanings in the two. See README. * *No conformance suite.* There is no executable artefact that an -implementation can be tested against, so "`conforms to the KRL spec`" is -not currently a checkable claim. -* *Proof obligations are unmet.* `+PROOF-STATUS.md+` records 0 of 8 -obligations proven, 2 partial. -* *`+rust-ci.yml+` gates nothing* — it calls the shared Rust reusable, -but this repository contains no `+Cargo.toml+`. +implementation can be tested against, so "conforms to the KRL spec" is not +currently a checkable claim. +* *Proof obligations are unmet.* `PROOF-STATUS.adoc` records 0 of 8 obligations +proven, 2 partial. +* *`rust-ci.yml` gates nothing* — it calls the shared Rust reusable, but this +repository contains no `Cargo.toml`. ''''' === Rework needed to reach D -Grade D requires a matrix of tested scenarios and at least one test per -claimed capability. Concretely: +Grade D requires a matrix of tested scenarios and at least one test per claimed +capability. Concretely: [arabic] -. *Reconcile the two grammars* into one normative specification, -resolving the `+|+` collision. -. *Write an executable conformance suite* — programs plus expected -results — so that spec conformance becomes testable rather than -asserted. -. *Run that suite against `+quandledb/server/krl/+`*, the actual -implementation (3,035 lines of Julia plus 1,732 lines of tests). One -passing test per claimed capability is the D bar. - -Until at least (1) and (2) exist, this repository specifies a language -nobody can be shown to implement. +. *Reconcile the two grammars* into one normative specification, resolving +the `++|++` collision. +. *Write an executable conformance suite* — programs plus expected results — +so that spec conformance becomes testable rather than asserted. +. *Run that suite against `quandledb/server/krl/`*, the actual +implementation (3,035 lines of Julia plus 1,732 lines of tests). One passing +test per claimed capability is the D bar. + +Until at least (1) and (2) exist, this repository specifies a language nobody +can be shown to implement. ''''' === Iteration history +[[iteration-0--x-2026-04-05]] ==== Iteration 0 — X (2026-04-05) -Templated from `+rsr-template-repo+`. Zero KRL-specific content. +Templated from `rsr-template-repo`. Zero KRL-specific content. +[[iteration-1--promoted-to-e-2026-04-05]] ==== Iteration 1 — promoted to E (2026-04-05) -* `+spec/grammar.ebnf+` (v0.1.0 EBNF) and `+spec/grammar-overview.md+` -* 4 `+examples/+` programs -* `+tests/smoke/grammar_smoke.sh+` (16 lexical assertions) +* `spec/grammar.ebnf` (v0.1.0 EBNF) and `spec/grammar-overview.adoc` +* 4 `examples/` programs +* `tests/smoke/grammar++_++smoke.sh` (16 lexical assertions) +[[iteration-2--promoted-to-d-2026-04-12--evidence-since-lost]] ==== Iteration 2 — promoted to D (2026-04-12) — *evidence since lost* -Decision "`Option B — Julia in `+KRLAdapter.jl+``"; lexer, AST, -recursive-descent parser and lowering implemented there, with 57 -dedicated parser tests. The repository holding all of it has since been -discarded, so none of this is verifiable. Retained here as history, not -as evidence. +Decision "Option B — Julia in `KRLAdapter.jl`"; lexer, AST, recursive-descent +parser and lowering implemented there, with 57 dedicated parser tests. The +repository holding all of it has since been discarded, so none of this is +verifiable. Retained here as history, not as evidence. +[[iteration-3--demoted-to-e-2026-07-21]] ==== Iteration 3 — demoted to E (2026-07-21) -* Grade restated against what is actually present and runnable in this -tree. -* Zig FFI shim repaired: it had never compiled (`+opaque+` type with -fields). -* Three vacuous or false gates repaired (`+aspect_tests.sh+`, -`+e2e.sh+`). -* False `+TangleIR+` lowering claims and dead `+KRLAdapter.jl+` -references removed from the README. +* Grade restated against what is actually present and runnable in this tree. +* Zig FFI shim repaired: it had never compiled (`opaque` type with fields). +* Three vacuous or false gates repaired (`aspect++_++tests.sh`, `e2e.sh`). +* False `TangleIR` lowering claims and dead `KRLAdapter.jl` references removed +from the README. === Review cycle Reassess when a conformance suite exists and has been run against -`+quandledb/server/krl/+`. +`quandledb/server/krl/`. ''''' -Run `+just crg-badge+` to generate the shields.io badge for the README. +Run `just crg-badge` to generate the shields.io badge for the README. diff --git a/README.adoc b/README.adoc index 57bf83d..1b8a852 100644 --- a/README.adoc +++ b/README.adoc @@ -1,167 +1,141 @@ +// SPDX-License-Identifier: CC-BY-SA-4.0 +// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell +[[krl--knot-resolution-language]] == KRL — Knot Resolution Language -https://www.bestpractices.dev/en/projects/new?repo_url=https://github.com/hyperpolymath/krl[image:https://img.shields.io/badge/OpenSSF-Best_Practices-green?logo=opensourcesecurity[OpenSSF -Best Practices]] +https://www.bestpractices.dev/en/projects/new?repo_url=https://github.com/hyperpolymath/krl[image:https://img.shields.io/badge/OpenSSF-Best_Practices-green?logo=opensourcesecurity[OpenSSF Best Practices]] -KRL (pronounced "`curl`") is the resolution language for -https://github.com/hyperpolymath/quandledb[QuandleDB]. This repository -holds its *normative specification*; the implementation lives in -QuandleDB. +KRL (pronounced "curl") is the resolution language for +https://github.com/hyperpolymath/quandledb[QuandleDB]. This repository holds +its *normative specification*; the implementation lives in QuandleDB. === What it is -QuandleDB is a *knot database* — a database whose stored objects are -knots and tangles, and whose identity relation is equivalence under -ambient isotopy rather than byte equality. KRL is the language you use -to work with it. +QuandleDB is a *knot database* — a database whose stored objects are knots and +tangles, and whose intended identity relation is equivalence under ambient isotopy rather +than byte equality. KRL is the language you use to work with it. -The point of a dedicated language is that the interesting questions -about a knot database are hard ones — is this the same knot, what class -does it fall in, what witnesses the answer — and you should be able to -ask them directly rather than assembling them out of general-purpose -data access. Record retrieval is one operation _within_ KRL, because -without it you could not get at anything; it is not what KRL is for. +The point of a dedicated language is that the interesting questions about a knot +database are hard ones — is this the same knot, what class does it fall in, what +witnesses the answer — and you should be able to ask them directly rather than +assembling them out of general-purpose data access. Record retrieval is one +operation _within_ KRL, because without it you could not get at anything; it is +not what KRL is for. -The name reflects the central operation. In knot theory, _resolution_ is -how crossings are resolved in the skein relation — the algebraic heart -of invariant computation. KRL generalises the word to every interaction -with the system: resolving structure, resolving equivalence, resolving -queries. +The name reflects the central operation. In knot theory, _resolution_ is how +crossings are resolved in the skein relation — the algebraic heart of invariant +computation. KRL generalises the word to every interaction with the system: +resolving structure, resolving equivalence, retrieving relevant evidence. === Where KRL sits -Three separate projects, developed for different purposes: +Related projects, developed for different purposes: -[width="100%",cols="50%,50%",options="header",] +[cols=",",options="header",] |=== |Project |What it is -|https://github.com/hyperpolymath/quandledb[*QuandleDB*] |The knot -database. Stores presentations, invariants, fingerprints, equivalence -classes and witnesses. - -|*KRL* (this repository) |QuandleDB’s resolution language. Specified -here, implemented in `+quandledb/server/krl/+`. - -|https://github.com/hyperpolymath/tangle[*Tangle*] |A separate, general -language for knot mathematics — topological, algebraic, geometric and -logical. Turing-complete; not a backend for KRL. +|https://github.com/hyperpolymath/quandledb[*QuandleDB*] |The knot database. Stores presentations, invariants, fingerprints, equivalence classes and witnesses. +|*KRL* (this repository) |QuandleDB's resolution language. Specified here, implemented in `quandledb/server/krl/`. +|https://github.com/hyperpolymath/Skein.jl[*Skein.jl*] |Independent Julia library for knot storage, indexing and invariant computation; used by QuandleDB. +|https://github.com/hyperpolymath/KnotTheory.jl[*KnotTheory.jl*] |Independent Julia mathematical toolkit for diagrams, braids, invariants and transformations. +|https://github.com/hyperpolymath/tangle[*Tangle*] |A separate, general language for knot mathematics — topological, algebraic, geometric and logical. Turing-complete; not a backend for KRL. |=== -KRL and QuandleDB were designed together and are deliberately close. -Tangle is a different project with a different remit that happens to -share the subject matter. The two are related by domain, not by -architecture: *KRL does not compile to, lower into, or depend on -Tangle.* - -____ -[!IMPORTANT] Earlier revisions of this README described a -`+KRL → TangleIR → Tangle+` compilation pipeline and named -`+KRLAdapter.jl+` as the canonical implementation. Neither is true. -`+TangleIR+` does not appear anywhere in the KRL implementation, and -`+KRLAdapter.jl+` no longer exists. Those claims have been removed -rather than restated. -____ +KRL and QuandleDB were designed together and are deliberately close. Tangle is a +different project with a different remit that happens to share the subject +matter. The two are related by domain, not by architecture: *KRL does not +compile to, lower into, or depend on Tangle.* + +[IMPORTANT] +==== +Earlier revisions of this README described a `KRL → TangleIR → Tangle` +compilation pipeline and named `KRLAdapter.jl` as the canonical +implementation. Neither is true. `TangleIR` does not appear anywhere in the +KRL implementation, and `KRLAdapter.jl` no longer exists. Those claims have +been removed rather than restated. +==== === The four operations -KRL has four operation families. The four-verb shape is deliberate: it -stops "`querying`" from becoming the whole identity of the language. +KRL has four operation families. The four-verb shape is deliberate: it stops +"querying" from becoming the whole identity of the language. -[width="100%",cols="34%,33%,33%",options="header",] +[cols=",,",options="header",] |=== |Operation |Knot concept |What it does -|*construct* |Tangles, ports, composition, tensor |create or declare -presentations, structures, claims, datasets - -|*transform* |PD code, Reidemeister moves |rewrite, normalise, compose, -concatenate, permute, mutate - -|*resolve* |Isotopy, quandle, equivalence class |decide, disambiguate, -or evaluate equivalence and identity questions - -|*retrieve* |Invariants, witnesses, stored resolutions |inspect, fetch, -project, explain, or return stored or computed results +|*construct* |Tangles, ports, composition, tensor |create or declare presentations, structures, claims, datasets +|*transform* |PD code, Reidemeister moves |rewrite, normalise, compose, concatenate, permute, mutate +|*resolve* |Isotopy, quandle, equivalence class |decide, disambiguate, or evaluate equivalence and identity questions +|*retrieve* |Invariants, witnesses, stored resolutions |inspect, fetch, project, explain, or return stored or computed results |=== -____ -[!NOTE] *Retrieve is not arbitrary database querying.* It recovers +[NOTE] +==== +*Retrieve is not arbitrary database querying.* It recovers resolution-relevant artefacts: presentations, invariants, witnesses, equivalence classes, prior resolutions, explanations and provenance. -Generic data access — arbitrary filters, dashboards, reporting, -analytics, index tuning — is an engine-layer affordance, deliberately -not elevated to a KRL operation. A separate query language is -*deferred*, not absent; see -`+docs/decisions/0002-query-language-deferred.adoc+`. -____ +Generic data access — arbitrary filters, dashboards, reporting, analytics, +index tuning — is an engine-layer affordance, deliberately not elevated to a +KRL operation. No additional public language is precommitted; see +link:docs/decisions/0002-query-language-deferred.adoc[the retrieval boundary decision]. +==== === What this repository holds -* The grammar specification (`+spec/grammar.ebnf+`). -* Idris2 ABI declarations (`+src/interface/Abi/+`). -* A Zig FFI shim over the C ABI (`+src/interface/ffi/+`). -* Example programs (`+examples/*.krl+`). -* The proof narrative (`+PROOF-NARRATIVE.md+`) and obligations registry. +* The grammar specification (`spec/grammar.ebnf`). +* Idris2 ABI declarations (`src/interface/Abi/`). +* A Zig FFI shim over the C ABI (`src/interface/ffi/`). +* Example programs (`examples/++*++.krl`). +* The proof narrative (`PROOF-NARRATIVE.adoc`) and obligations registry. It does *not* hold a parser or evaluator. Those are in -`+quandledb/server/krl/+` — 3,035 lines of Julia (lexer, parser, AST, -evaluator, SQL front end) with 1,732 lines of tests. +`quandledb/server/krl/`: a Julia lexer, parser, AST and evaluator, with a +separate compatibility frontend. These implement a fragment; they do not yet +execute all four operation families. + +For a high-level proof progress summary, see PROOF-PROGRESS.adoc. === Status Assessed against what is in this tree, not against absent work. -[width="100%",cols="50%,50%",options="header",] +[cols=",",options="header",] |=== |Component |State -|Grammar specification |Drafted (`+spec/grammar.ebnf+`, 114 lines) - -|Examples |Four `+.krl+` programs, lexically checked against the grammar -by `+tests/smoke/grammar_smoke.sh+` (20 checks) - -|Idris2 ABI |Declared — 4 `+%foreign+` declarations - -|Zig FFI |Compiles; 3/3 unit tests pass; `+zig build+` produces -`+libkrl.a+` - +|Grammar specification |Drafted (`spec/grammar.ebnf`, 114 lines) +|Examples |Four `.krl` programs, lexically checked against the grammar by `tests/smoke/grammar++_++smoke.sh` (20 checks) +|Idris2 ABI |Declared — 4 `%foreign` declarations +|Zig FFI |Compiles; 3/3 unit tests pass; `zig build` produces `libkrl.a` |Parser / evaluator |Not in this repository (see above) - -|Conformance suite |Not yet written — planned, see below +|Conformance suite |Executable retrieval-fragment acceptance/rejection corpus in `tests/conformance/retrieval++_++fragment.jl`; see `spec/SURFACES.adoc` |=== There is no parser here, so nothing in this repository can execute a KRL -program. `+tests/smoke/grammar_smoke.sh+` performs lexical-level -checking only and says so. +program. `tests/smoke/grammar++_++smoke.sh` performs lexical-level checking only and +says so. -=== Known divergence +=== Surface contracts -Two documents currently call themselves the KRL grammar, and they do not -agree: +spec/SURFACES.adoc distinguishes the construction/resolution +*draft* from QuandleDB's executable retrieval/candidate *fragment*. In the +former, `++|++` is tensor composition; in the latter it separates stages. These are +separately scoped contracts, not interchangeable grammars. -[width="100%",cols="34%,33%,33%",options="header",] -|=== -| |`+krl/spec/grammar.ebnf+` |`+quandledb/spec/grammar.ebnf+` -|Size |114 lines |402 lines - -|Construction |`+sigma+`, `+sigma_inv+`, `+cup+`, `+cap+` |none +Run the fragment's acceptance/rejection corpus against a concrete implementation: -|Retrieval |`+find … where …+` |`+from … \| filter \| sort \| …+` -pipeline - -|Implemented |no |yes -|=== +[source,sh] +---- +julia --startup-file=no tests/conformance/retrieval_fragment.jl /path/to/quandledb +---- -They are disjoint on core vocabulary, and `+|+` is bound to *opposite -meanings* in the two — tensor product here, pipeline separator there. -Reconciling them, and giving this repository an executable conformance -suite so that "`the spec`" becomes a thing an implementation can be -tested against, is the next body of work. It is not done, and this -README does not claim otherwise. +The evaluator's resolution-boundary tests additionally reject demands for exact, +sufficient or necessary assurance from an index bucket. Heuristic candidates +remain available with an explicit warning. Full resolution syntax and witness +checking are still implementation obligations. === Related -* https://github.com/hyperpolymath/quandledb[QuandleDB] — the knot -database -* https://github.com/hyperpolymath/tangle[Tangle] — general -knot-mathematics language (separate project) +* https://github.com/hyperpolymath/quandledb[QuandleDB] — the knot database +* https://github.com/hyperpolymath/tangle[Tangle] — general knot-mathematics language (separate project) * link:docs/krl_map.html[KRL architecture map (HTML)] diff --git a/docs/decisions/0002-query-language-deferred.adoc b/docs/decisions/0002-query-language-deferred.adoc index 53b994b..edef7be 100644 --- a/docs/decisions/0002-query-language-deferred.adoc +++ b/docs/decisions/0002-query-language-deferred.adoc @@ -1,96 +1,25 @@ // SPDX-License-Identifier: CC-BY-SA-4.0 -// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) -= Architecture Decision Record: 0002-query-language-deferred - - - -# 2. Query language deferred — querying stays a mode of KRL - -Date: 2026-06-18 - -## Status - -Accepted - -## Context - -KRL is a *resolution language*, not a query language. Its identity is the four -operations — *construct*, *transform*, *resolve*, *retrieve* — and the four-verb -shape is deliberate: it stops "querying" from becoming the whole identity of the -language. - -A recurring pressure works against this: - -- Databases are *expected* to ship a query language; its apparent absence reads as - "toy" to evaluators arriving with SQL / Cypher / AQL muscle memory. -- The *retrieve* operation, by name, can drag readers back toward "query language". -- There is a genuine future need for non-resolution data operations: dashboards, - arbitrary filters, administrative analytics, bulk reporting, exploratory search, - index tuning. - -But the two failure modes are asymmetric: - -- *No query language* is a **messaging** problem — cheap, reversible, fixable with - documentation. -- *A premature, weak query language* is a **reputation** problem — it invites direct - comparison with mature query languages on their own turf, where a young project - loses, and first impressions in developer tooling are durable. A bounced evaluator - is hard to win back. - -Query *access* already exists at the engine/API layer (Skein.jl composable -predicates over SQLite; QuandleDB's filtered HTTP endpoints). What is declined here -is a *first-class, branded query language* that competes as a paradigm. Those are -different things. - -There is also a strategic-identity dimension. A capability framed as "a query -sublanguage" is absorbable as a feature ("the next AQL add-in module"); a *named -category* — resolution as a paradigm for equivalence / identity determination — is -not. Keeping KRL a language rather than a query mode is therefore also how the work -retains a distinct, attributable identity, especially if the broader bet (resolution -as a general primitive for determining equivalent acts and things, including for AI) -pays off. - -## Decision - -1. Querying remains a *mode of KRL* — the *retrieve* operation — not a first-class - sibling language. No separate query language is built now. - -2. *Retrieve* is defined narrowly. It recovers **resolution-relevant artefacts**: - presentations, invariants, witnesses, equivalence classes, prior resolutions, - explanations, and provenance. It is **not** arbitrary database querying. - -3. Generic data access (arbitrary filters, dashboards, reporting, analytics, - exploratory search, index tuning) is an *engine-layer* affordance (Skein.jl / - SQLite; QuandleDB endpoints), deliberately not elevated to a KRL operation. - -4. A separate query language is *deferred, not rejected*. It becomes warranted only - when sustained non-resolution database operations accumulate — the trigger list: - dashboards, arbitrary filters, administrative analytics, bulk reporting, - exploratory search, index tuning. - -5. *Pre-committed shape.* If/when that query language is built, it will be a - *KRL-family projection / reporting dialect that compiles to the same TangleIR and - engine* — one semantic core with a reporting surface — not an independent rival - paradigm. This makes it structurally impossible for the future query language to - be a "me-too" graph/relational language. - -## Consequences - -### Positive - -- KRL leads from strength (resolution — where it has no competitor) rather than - fighting established query languages on their turf. -- The distinctive, attributable identity ("knot resolution", a named paradigm) is - preserved against commoditisation. -- No premature surface to poison first impressions. - -### Negative - -- Evaluators expecting a headline query language must be pointed at the engine-layer - access path and the *retrieve* clause; the absence must be *explained*, not shipped - around. - -### Neutral - -- The decision is revisited when the trigger conditions accrue; this ADR is then - superseded by the ADR that specifies the deferred dialect. +// Copyright (c) 2026 Jonathan D.A. Jewell += Decision 0002: resolution and retrieval + +Revised 2026-09-07. Accepted. The filename is retained for existing links. + +KRL is a resolution language with construct, transform, resolve and retrieve +operations. Retrieve recovers presentations, invariants, candidate matches, +witnesses, prior resolutions and their explanations/provenance. It supports the +resolution task without defining the language's entire purpose. + +Generic selection, filtering, reporting and administration may remain engine or +API operations. No additional branded language or compilation architecture is +precommitted. A future proposal must establish an unmet user task and a precise +semantic contract before adding another public surface. + +Skein.jl and KnotTheory.jl are independent Julia libraries. QuandleDB may use +those libraries without redefining their purpose. Tangle is a separate +Turing-complete language for knot mathematics. Shared subject matter implies no +compilation dependency and transfers no proof guarantee to KRL. + +The implemented retrieval/candidate fragment and the construction/resolution +draft are separately scoped in `../../spec/SURFACES.adoc`. A successful retrieval +must state the assurance actually established. Index membership alone cannot +satisfy a demand for a checked equivalence witness. diff --git a/docs/developer/ABI-FFI-README.adoc b/docs/developer/ABI-FFI-README.adoc index e24ba5d..e851327 100644 --- a/docs/developer/ABI-FFI-README.adoc +++ b/docs/developer/ABI-FFI-README.adoc @@ -342,8 +342,8 @@ zig build test-integration -- Runtime checks main : IO () main = do - verifyLayoutsCorrect - verifyAlignmentsCorrect + verifyLayouorrect + verifyAlignmenorrect putStrLn "ABI verification passed" ``` diff --git a/docs/krl_map.html b/docs/krl_map.html index a8c96bb..3a55ab6 100644 --- a/docs/krl_map.html +++ b/docs/krl_map.html @@ -59,11 +59,11 @@

KRL — Knot Resolution Language

-

each operation is grounded in topology, implemented by a dedicated repo, and exposed as syntax

+

Four operation families; syntax examples below are design sketches. See spec/SURFACES.adoc for what executes.

knot concepts
-
repository
+
design responsibility
KRL operation
language feature
@@ -74,8 +74,8 @@

KRL — Knot Resolution Language

ObjectInterfaceComposeTensor
-
Tangle PL
-
syntax layer
+
KRL / QuandleDB
+
construction design
Construct
@@ -94,8 +94,8 @@

KRL — Knot Resolution Language

StructureTransformation
-
KnotTheory.jl
-
engine
+
KRL / QuandleDB
+
transformation contract
Transform
@@ -134,8 +134,8 @@

KRL — Knot Resolution Language

Invariant
-
Skein.jl
-
persistence
+
KRL / QuandleDB
+
retrieval contract
Retrieve
@@ -148,8 +148,9 @@

KRL — Knot Resolution Language

-

"Query" = row 4 only  ·  "Resolution" spans rows 2–3, where knot topology is distinctive  ·  hence KRL, not KQL

-

Tags show Verisim octad grounding for each operation

+

Skein.jl and KnotTheory.jl are independent Julia libraries that QuandleDB uses. Their purposes are not individual KRL operations.

+

Tangle is a separate Turing-complete language for knot mathematics. KRL does not compile into it or inherit its proofs.

+

The running fragment retrieves heuristic candidates. Full construction and checked equivalence resolution remain separate implementation obligations.

diff --git a/spec/SURFACES.adoc b/spec/SURFACES.adoc new file mode 100644 index 0000000..3fa2848 --- /dev/null +++ b/spec/SURFACES.adoc @@ -0,0 +1,40 @@ +// SPDX-License-Identifier: CC-BY-SA-4.0 +// Copyright (c) 2026 Jonathan D.A. Jewell += KRL surface contracts + +KRL's four operation families are construct, transform, resolve and retrieve. +The design and the currently executable fragment have distinct surface contracts. +They must not be concatenated into one grammar: their use of `|` is incompatible. + +[cols="1,2,2",options=header] +|=== +| Surface | Syntax authority | Execution status +| Construction/resolution draft +| `spec/grammar.ebnf` in this repository; `|` denotes tensor composition +| Design only. The QuandleDB parser does not execute these programs. +| Retrieval/candidate fragment +| `quandledb/spec/grammar.ebnf`, implemented in `quandledb/server/krl/`; + `|` separates stages +| A running Julia parser/evaluator. Parsing a resolution request does not imply + an implementation can supply the requested evidence. +|=== + +`tests/conformance/retrieval_fragment.jl` runs a cross-repository acceptance and +rejection corpus against a supplied QuandleDB checkout. It includes unsupported +construction syntax as an explicit rejection control. This is fragment +conformance, not proof of equivalence between an EBNF document and a parser. + +[source,console] +---- +julia --startup-file=no tests/conformance/retrieval_fragment.jl /path/to/quandledb +---- + +The evaluator's `resolution_boundary_test.jl` separately checks that an index +collision cannot be promoted to exact, sufficient or necessary assurance. +The current bucket provider supports heuristic candidates only. A `via` list +is parsed but is not checked by that provider; results say so. An absent target +means resolution is unavailable, not a proof of inequivalence. + +A future unified surface needs an explicit grammar decision, semantics for all +four operations, port/arity checking, and executable witness checking. No +separate reporting language or Tangle compilation dependency is precommitted. diff --git a/spec/grammar.ebnf b/spec/grammar.ebnf index 4021826..016ec38 100644 --- a/spec/grammar.ebnf +++ b/spec/grammar.ebnf @@ -2,6 +2,8 @@ (* KRL — Knot Resolution Language *) (* Grammar v0.1.0 (2026-04-05) — DRAFT *) (* Pronounced "curl" *) +(* CONSTRUCTION/RESOLUTION DRAFT ONLY; not the QuandleDB parser contract. *) +(* See spec/SURFACES.adoc for the separately executable retrieval fragment. *) (* =================================================================== *) (* Top-level program *) @@ -11,7 +13,7 @@ program = { statement } ; statement = binding | expression_stmt - | query ; + | retrieval ; binding = "let" , identifier , "=" , expression , ";" ; expression_stmt = expression , ";" ; @@ -52,10 +54,10 @@ cup_cap_gen = "cup" , integer (* cup on st | "cap" , integer ; (* cap on strands i, i+1 *) (* =================================================================== *) -(* Queries (RETRIEVE) *) +(* Retrieval (RETRIEVE) *) (* =================================================================== *) -query = "find" , "where" , filter_list , ";" ; +retrieval = "find" , "where" , filter_list , ";" ; filter_list = filter , { "and" , filter } ; diff --git a/tests/conformance/retrieval_fragment.jl b/tests/conformance/retrieval_fragment.jl new file mode 100644 index 0000000..d455858 --- /dev/null +++ b/tests/conformance/retrieval_fragment.jl @@ -0,0 +1,24 @@ +# SPDX-License-Identifier: MPL-2.0 +# Copyright (c) 2026 Jonathan D.A. Jewell +using Test +length(ARGS) == 1 || error("Usage: julia retrieval_fragment.jl /path/to/quandledb") +implementation = joinpath(abspath(ARGS[1]), "server", "krl", "KRL.jl") +isfile(implementation) || error("QuandleDB KRL implementation not found: $implementation") +include(implementation) +using .KRL + +@testset "KRL retrieval fragment contract" begin + q = parse_krl_query("from knots | filter crossing_number == 3 | return name") + @test q.source isa KRLSourceKnots + @test q.stages[1] isa KRLFilterStage + @test q.stages[2] isa KRLReturnStage + resolution = parse_krl_query("from knots | find_equivalent \"3_1\" confidence >= exact") + @test resolution.stages[1] isa KRLFindEquivStage + @test resolution.stages[1].min_confidence == ConfExact + # Syntax acceptance is distinct from the evaluator's assurance refusal. + for invalid in ["from knots | filter", "from knots | wobble 3", + "from knots | take x", "from (from knots", + "sigma 1;", "let k = close (sigma 1 | sigma 2);"] + @test_throws KRLParseError parse_krl(invalid) + end +end diff --git a/tests/smoke/grammar_smoke.sh b/tests/smoke/grammar_smoke.sh index cd52341..55cf7ba 100755 --- a/tests/smoke/grammar_smoke.sh +++ b/tests/smoke/grammar_smoke.sh @@ -119,10 +119,9 @@ for file in "${EXAMPLE_FILES[@]}"; do done # 4b. KR-7: generator indices must be POSITIVE (N >= 1). - # The canonical parser in KRLAdapter.jl raises a "zero index" error - # for `sigma 0`, `sigma_inv 0`, etc., and negative indices are - # outside the lexer's positive-Int recognition. The smoke test - # asserts that no committed example contains such a pattern. + # This is a draft/example constraint, not evidence of a running + # construction parser. The executable fragment is scoped separately + # in spec/SURFACES.adoc. # # See PROOF-NARRATIVE.md KR-7 and ASSUMPTIONS.md A-KR-2.1. # NB: grep returns 1 when nothing matches; under `set -e` we From 50378527dd45e565e95b1c986190525cb4e3ca05 Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Mon, 7 Sep 2026 03:43:02 +0100 Subject: [PATCH 2/4] fix(ci): enforce blocking scans and repair verification workflows --- .github/workflows/actions.lock | 6 --- .github/workflows/boj-build.yml | 2 +- .github/workflows/codeql.yml | 6 +-- .github/workflows/dependabot-automerge.yml | 2 +- .github/workflows/dogfood-gate.yml | 51 +++++++++++++++++----- .github/workflows/e2e.yml | 12 ++--- .github/workflows/fragment-conformance.yml | 7 +-- .github/workflows/governance.yml | 2 +- .github/workflows/hypatia-scan.yml | 5 ++- .github/workflows/instant-sync.yml | 2 +- .github/workflows/openssf-compliance.yml | 2 +- .github/workflows/pages.yml | 8 ++-- .github/workflows/push-email-notify.yml | 2 +- .github/workflows/release.yml | 12 ++--- .github/workflows/rhodibot.yml | 2 +- .github/workflows/secret-scanner.yml | 2 +- .github/workflows/static-analysis-gate.yml | 22 +++++----- 17 files changed, 85 insertions(+), 60 deletions(-) diff --git a/.github/workflows/actions.lock b/.github/workflows/actions.lock index 7f029cb..4f64f07 100644 --- a/.github/workflows/actions.lock +++ b/.github/workflows/actions.lock @@ -13,7 +13,6 @@ workflows: '.github/workflows/dogfood-gate.yml': - 'actions/checkout@v4.3.1' - 'hyperpolymath/a2ml-ecosystem@main' - - 'hyperpolymath/k9-ecosystem@main' '.github/workflows/e2e.yml': - 'actions/checkout@v6.0.2' - 'goto-bus-stop/setup-zig@v2.2.1' @@ -109,11 +108,6 @@ dependencies: commit: 'sha1-b6ce942d54b3528f7d7a30d63f57617005fc0d6a' owner_id: 6759885 repo_id: 1275649586 - 'hyperpolymath/k9-ecosystem@main': - ref: 'main' - commit: 'sha1-347ee5d6a1b77831de56fe8da21a473724e4cac2' - owner_id: 6759885 - repo_id: 1275650185 'hyperpolymath/smtp-notify-action@v0.2.0': ref: 'v0.2.0' commit: 'sha1-ede1191ef6ff3ac02c4f4d9efdf837ee517e11d7' diff --git a/.github/workflows/boj-build.yml b/.github/workflows/boj-build.yml index 1277be3..86419d8 100644 --- a/.github/workflows/boj-build.yml +++ b/.github/workflows/boj-build.yml @@ -24,7 +24,7 @@ jobs: # no-op behaviour. steps: - name: Checkout - uses: actions/checkout@v6.0.2 + uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2 - name: Trigger BoJ Server (Casket/ssg-mcp) env: BOJ_URL: ${{ secrets.BOJ_SERVER_URL || vars.BOJ_SERVER_URL }} diff --git a/.github/workflows/codeql.yml b/.github/workflows/codeql.yml index 4215dab..bff8072 100644 --- a/.github/workflows/codeql.yml +++ b/.github/workflows/codeql.yml @@ -32,13 +32,13 @@ jobs: build-mode: none steps: - name: Checkout - uses: actions/checkout@v6.0.2 + uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2 - name: Initialize CodeQL - uses: github/codeql-action/init@v4.34.0 + uses: github/codeql-action/init@c6f931105cb2c34c8f901cc885ba1e2e259cf745 # v4.34.0 with: languages: ${{ matrix.language }} build-mode: ${{ matrix.build-mode }} - name: Perform CodeQL Analysis - uses: github/codeql-action/analyze@v4.34.0 + uses: github/codeql-action/analyze@c6f931105cb2c34c8f901cc885ba1e2e259cf745 # v4.34.0 with: category: "/language:${{ matrix.language }}" diff --git a/.github/workflows/dependabot-automerge.yml b/.github/workflows/dependabot-automerge.yml index 403756d..b90bd1f 100644 --- a/.github/workflows/dependabot-automerge.yml +++ b/.github/workflows/dependabot-automerge.yml @@ -52,7 +52,7 @@ jobs: steps: - name: Fetch Dependabot metadata id: meta - uses: dependabot/fetch-metadata@v2.2.0 + uses: dependabot/fetch-metadata@dbb049abf0d677abbd7f7eee0375145b417fdd34 # v2.2.0 with: github-token: ${{ secrets.GITHUB_TOKEN }} # --- Policy gate ------------------------------------------------------- diff --git a/.github/workflows/dogfood-gate.yml b/.github/workflows/dogfood-gate.yml index 59d5df9..f0809dc 100644 --- a/.github/workflows/dogfood-gate.yml +++ b/.github/workflows/dogfood-gate.yml @@ -27,7 +27,7 @@ jobs: steps: - name: Checkout repository - uses: actions/checkout@v4.3.1 + uses: actions/checkout@34e114876b0b11c390a56381ad16ebd13914f8d5 # v4.3.1 - name: Check for A2ML files id: detect @@ -44,7 +44,7 @@ jobs: # which taught the validator the colon/brace-block identity form # (`id: "..."`), so docs/governance/TSDM.a2ml failed against the old # pin despite being valid. Bumped to current main. - uses: hyperpolymath/a2ml-ecosystem/validate-action@main + uses: hyperpolymath/a2ml-ecosystem/validate-action@b6ce942d54b3528f7d7a30d63f57617005fc0d6a # main with: path: '.' strict: 'false' @@ -76,7 +76,7 @@ jobs: steps: - name: Checkout repository - uses: actions/checkout@v4.3.1 + uses: actions/checkout@34e114876b0b11c390a56381ad16ebd13914f8d5 # v4.3.1 - name: Check for K9 files id: detect @@ -91,12 +91,40 @@ jobs: echo "::warning::Found $CONFIG_COUNT config files but no K9 contracts. Run k9iser to generate contracts." fi - - name: Validate K9 contracts + - name: Check out the canonical K9 validator if: steps.detect.outputs.k9_count > 0 - uses: hyperpolymath/k9-ecosystem/validate-action@main + uses: actions/checkout@34e114876b0b11c390a56381ad16ebd13914f8d5 # v4.3.1 with: - path: '.' - strict: 'false' + repository: hyperpolymath/k9-ecosystem + ref: 347ee5d6a1b77831de56fe8da21a473724e4cac2 + path: .ci-k9-validator + persist-credentials: false + sparse-checkout-cone-mode: false + sparse-checkout: | + /validate-action/action.yml + /validate-action/validate-k9.sh + + - name: Validate K9 contracts + if: steps.detect.outputs.k9_count > 0 + # Sparse checkout avoids unrelated dangling symlinks in the upstream + # action archive; execute the unchanged canonical validator. + env: + INPUT_PATH: '.' + INPUT_STRICT: 'false' + # Canonical action.yml defaults at the pinned validator revision. + INPUT_PATHS_IGNORE: | + vendor/ + vendored/ + verified-container-spec/ + .audittraining/ + integration/fixtures/ + test/fixtures/ + tests/fixtures/ + absolute-zero/ + coordination.k9 + session/custom-checks.k9 + self-validating/methodology-guard.k9.ncl + run: bash .ci-k9-validator/validate-action/validate-k9.sh - name: Write summary run: | @@ -126,7 +154,7 @@ jobs: steps: - name: Checkout repository - uses: actions/checkout@v4.3.1 + uses: actions/checkout@34e114876b0b11c390a56381ad16ebd13914f8d5 # v4.3.1 - name: Scan for invisible characters id: lint @@ -191,7 +219,7 @@ jobs: steps: - name: Checkout repository - uses: actions/checkout@v4.3.1 + uses: actions/checkout@34e114876b0b11c390a56381ad16ebd13914f8d5 # v4.3.1 - name: Check for Groove manifest id: groove @@ -250,7 +278,7 @@ jobs: steps: - name: Checkout repository - uses: actions/checkout@v4.3.1 + uses: actions/checkout@34e114876b0b11c390a56381ad16ebd13914f8d5 # v4.3.1 - name: Check and validate eclexiaiser manifest id: eclex @@ -325,7 +353,7 @@ jobs: steps: - name: Checkout repository - uses: actions/checkout@v4.3.1 + uses: actions/checkout@34e114876b0b11c390a56381ad16ebd13914f8d5 # v4.3.1 - name: Generate dogfooding scorecard run: | @@ -398,4 +426,3 @@ jobs: *Generated by the [Dogfood Gate](https://github.com/hyperpolymath/rsr-template-repo) workflow.* *Dogfooding is guinea pig fooding — we test our tools on ourselves.* EOF - diff --git a/.github/workflows/e2e.yml b/.github/workflows/e2e.yml index 738bbf6..b410235 100644 --- a/.github/workflows/e2e.yml +++ b/.github/workflows/e2e.yml @@ -44,9 +44,9 @@ jobs: timeout-minutes: 15 steps: - name: Checkout - uses: actions/checkout@v6.0.2 + uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2 - name: Set up Zig - uses: goto-bus-stop/setup-zig@v2.2.1 + uses: goto-bus-stop/setup-zig@abea47f85e598557f500fa1fd2ab7464fcb39406 # v2.2.1 with: version: ${{ env.ZIG_VERSION }} - name: Run E2E suite @@ -58,7 +58,7 @@ jobs: timeout-minutes: 10 steps: - name: Checkout - uses: actions/checkout@v6.0.2 + uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2 - name: Run aspect tests run: bash tests/aspect_tests.sh @@ -68,7 +68,7 @@ jobs: timeout-minutes: 10 steps: - name: Checkout - uses: actions/checkout@v6.0.2 + uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2 - name: Run grammar smoke suite run: bash tests/smoke/grammar_smoke.sh @@ -78,9 +78,9 @@ jobs: timeout-minutes: 15 steps: - name: Checkout - uses: actions/checkout@v6.0.2 + uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2 - name: Set up Zig - uses: goto-bus-stop/setup-zig@v2.2.1 + uses: goto-bus-stop/setup-zig@abea47f85e598557f500fa1fd2ab7464fcb39406 # v2.2.1 with: version: ${{ env.ZIG_VERSION }} - name: zig build test diff --git a/.github/workflows/fragment-conformance.yml b/.github/workflows/fragment-conformance.yml index e629ecf..cdddf17 100644 --- a/.github/workflows/fragment-conformance.yml +++ b/.github/workflows/fragment-conformance.yml @@ -13,15 +13,16 @@ concurrency: cancel-in-progress: true jobs: fragment: + name: KRL fragment conformance runs-on: ubuntu-latest timeout-minutes: 15 steps: - name: Checkout specification - uses: actions/checkout@v7.0.0 + uses: actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0 # v7.0.0 with: persist-credentials: false - name: Checkout pinned QuandleDB implementation - uses: actions/checkout@v7.0.0 + uses: actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0 # v7.0.0 with: repository: hyperpolymath/quandledb ref: 4a00d5cacafd721aee1993bec23c164db425a70d @@ -30,7 +31,7 @@ jobs: - name: Record implementation revision run: git -C deps/quandledb rev-parse HEAD - name: Install Julia - uses: julia-actions/setup-julia@v2.7.0 + uses: julia-actions/setup-julia@4c0cb0fce8556fdb04a90347310e5db8b1f98fb9 # v2.7.0 with: version: '1.12.6' - name: Check fragment acceptance and rejection diff --git a/.github/workflows/governance.yml b/.github/workflows/governance.yml index 7ce96ba..1d17b3e 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@fcb566cfb8a86cea2d3666bf65a4f177a49b1313 diff --git a/.github/workflows/hypatia-scan.yml b/.github/workflows/hypatia-scan.yml index 93ac840..e6f1a78 100644 --- a/.github/workflows/hypatia-scan.yml +++ b/.github/workflows/hypatia-scan.yml @@ -12,6 +12,7 @@ on: workflow_dispatch: permissions: + actions: read contents: read # The reusable declares security-events: write (it uploads SARIF). A called # workflow cannot escalate beyond the caller's grant, so `read` here makes the @@ -20,4 +21,6 @@ permissions: jobs: scan: - uses: hyperpolymath/standards/.github/workflows/hypatia-scan-reusable.yml@81dbf2dd854b1444fd6236fa2352474383b2c2b9 + uses: hyperpolymath/standards/.github/workflows/hypatia-scan-reusable.yml@fcb566cfb8a86cea2d3666bf65a4f177a49b1313 + with: + block-on-high: true diff --git a/.github/workflows/instant-sync.yml b/.github/workflows/instant-sync.yml index 766c0a5..3d43e2a 100644 --- a/.github/workflows/instant-sync.yml +++ b/.github/workflows/instant-sync.yml @@ -15,7 +15,7 @@ jobs: timeout-minutes: 15 steps: - name: Trigger Propagation - uses: peter-evans/repository-dispatch@v4.0.1 + uses: peter-evans/repository-dispatch@28959ce8df70de7be546dd1250a005dd32156697 # v4.0.1 with: token: ${{ secrets.FARM_DISPATCH_TOKEN }} repository: hyperpolymath/.git-private-farm diff --git a/.github/workflows/openssf-compliance.yml b/.github/workflows/openssf-compliance.yml index ac995a4..83393d0 100644 --- a/.github/workflows/openssf-compliance.yml +++ b/.github/workflows/openssf-compliance.yml @@ -18,7 +18,7 @@ jobs: permissions: contents: read steps: - - uses: actions/checkout@v4.3.1 + - uses: actions/checkout@34e114876b0b11c390a56381ad16ebd13914f8d5 # v4.3.1 with: persist-credentials: false - name: Check SECURITY.md exists and has substance diff --git a/.github/workflows/pages.yml b/.github/workflows/pages.yml index 6924017..a6bce16 100755 --- a/.github/workflows/pages.yml +++ b/.github/workflows/pages.yml @@ -27,9 +27,9 @@ jobs: image: ghcr.io/stefan-hoeck/idris2-pack@sha256:f0758996a931fb35d9ecb1de273c4d59dabe2a09b433afc7e357f65a08b7e1ff steps: - name: Checkout Site - uses: actions/checkout@v6.0.2 + uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2 - name: Checkout Ddraig SSG - uses: actions/checkout@v6.0.2 + uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2 with: repository: hyperpolymath/ddraig-ssg path: .ddraig-ssg @@ -46,7 +46,7 @@ jobs: fi ./.ddraig-ssg/build/exec/ddraig build src _site https://hyperpolymath.github.io/${GITHUB_REPOSITORY#*/} - name: Upload artifact - uses: actions/upload-pages-artifact@v3.0.1 + uses: actions/upload-pages-artifact@56afc609e74202658d3ffba0e8f6dda462b719fa # v3.0.1 with: path: '_site' deploy: @@ -63,4 +63,4 @@ jobs: steps: - name: Deploy to GitHub Pages id: deployment - uses: actions/deploy-pages@v4.0.5 + uses: actions/deploy-pages@d6db90164ac5ed86f2b6aed7e0febac5b3c0c03e # v4.0.5 diff --git a/.github/workflows/push-email-notify.yml b/.github/workflows/push-email-notify.yml index 676f498..621885f 100644 --- a/.github/workflows/push-email-notify.yml +++ b/.github/workflows/push-email-notify.yml @@ -40,7 +40,7 @@ jobs: timeout-minutes: 5 steps: - name: Send push notification email - uses: hyperpolymath/smtp-notify-action@v0.2.0 + uses: hyperpolymath/smtp-notify-action@ede1191ef6ff3ac02c4f4d9efdf837ee517e11d7 # v0.2.0 with: server_address: ${{ secrets.SMTP_HOST }} server_port: ${{ secrets.SMTP_PORT }} diff --git a/.github/workflows/release.yml b/.github/workflows/release.yml index 4eb83d2..a5cbab7 100644 --- a/.github/workflows/release.yml +++ b/.github/workflows/release.yml @@ -20,7 +20,7 @@ jobs: permissions: contents: read steps: - - uses: actions/checkout@v6.0.2 + - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2 - name: Detect project type and build id: build run: | @@ -67,7 +67,7 @@ jobs: exit 1 fi # TODO: Upload build artifacts if needed - # - uses: actions/upload-artifact@v4 + # - uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02 # v4 # with: # name: release-artifacts # path: target/release/ @@ -81,7 +81,7 @@ jobs: changelog: ${{ steps.cliff.outputs.content }} version: ${{ steps.version.outputs.version }} steps: - - uses: actions/checkout@v6.0.2 + - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2 with: fetch-depth: 0 - name: Extract version from tag @@ -106,7 +106,7 @@ jobs: run: | git cliff --output CHANGELOG.md - name: Upload updated CHANGELOG.md - uses: actions/upload-artifact@v4.6.2 + uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02 # v4.6.2 with: name: changelog path: CHANGELOG.md @@ -119,14 +119,14 @@ jobs: permissions: contents: write steps: - - uses: actions/checkout@v6.0.2 + - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2 # TODO: Download build artifacts if uploading to the release # - uses: actions/download-artifact@v4 # with: # name: release-artifacts # path: artifacts/ - name: Create GitHub Release - uses: softprops/action-gh-release@v2.5.0 + uses: softprops/action-gh-release@a06a81a03ee405af7f2048a818ed3f03bbf83c7b # v2.5.0 with: body: ${{ needs.changelog.outputs.changelog }} draft: false diff --git a/.github/workflows/rhodibot.yml b/.github/workflows/rhodibot.yml index cf1034b..be74c23 100644 --- a/.github/workflows/rhodibot.yml +++ b/.github/workflows/rhodibot.yml @@ -28,7 +28,7 @@ jobs: timeout-minutes: 15 steps: - name: Checkout - uses: actions/checkout@v4.3.1 + uses: actions/checkout@34e114876b0b11c390a56381ad16ebd13914f8d5 # v4.3.1 with: fetch-depth: 1 - name: Rhodibot — Scan and Fix diff --git a/.github/workflows/secret-scanner.yml b/.github/workflows/secret-scanner.yml index a56f599..f0084b4 100644 --- a/.github/workflows/secret-scanner.yml +++ b/.github/workflows/secret-scanner.yml @@ -15,5 +15,5 @@ jobs: scan: permissions: contents: read - uses: hyperpolymath/standards/.github/workflows/secret-scanner-reusable.yml@7fdc2705df74b4e352d2a1cde3e87a5923fdf329 + uses: hyperpolymath/standards/.github/workflows/secret-scanner-reusable.yml@fcb566cfb8a86cea2d3666bf65a4f177a49b1313 secrets: inherit diff --git a/.github/workflows/static-analysis-gate.yml b/.github/workflows/static-analysis-gate.yml index d4c9f9f..ee2d90f 100644 --- a/.github/workflows/static-analysis-gate.yml +++ b/.github/workflows/static-analysis-gate.yml @@ -20,7 +20,7 @@ jobs: timeout-minutes: 15 steps: - name: Checkout repository - uses: actions/checkout@v6.0.2 + uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2 with: fetch-depth: 0 - name: Install panic-attack (if available) @@ -117,7 +117,7 @@ jobs: echo "" >> "$GITHUB_STEP_SUMMARY" echo "Skipped: panic-attack not available in this environment." >> "$GITHUB_STEP_SUMMARY" - name: Upload panic-attack findings - uses: actions/upload-artifact@v4.6.2 + uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02 # v4.6.2 with: name: panic-attack-findings path: panic-attack-findings.json @@ -136,13 +136,13 @@ jobs: timeout-minutes: 15 steps: - name: Checkout repository - uses: actions/checkout@v6.0.2 + uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2 with: fetch-depth: 0 - name: Setup Elixir for Hypatia scanner id: beam continue-on-error: true - uses: erlef/setup-beam@v1.20.4 + uses: erlef/setup-beam@e6d7c94229049569db56a7ad5a540c051a010af9 # v1.20.4 with: elixir-version: '1.19.4' otp-version: '28.3' @@ -243,7 +243,7 @@ jobs: echo "" >> "$GITHUB_STEP_SUMMARY" echo "Skipped: Hypatia scanner not available in this environment." >> "$GITHUB_STEP_SUMMARY" - name: Upload hypatia findings - uses: actions/upload-artifact@v4.6.2 + uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02 # v4.6.2 with: name: hypatia-findings path: hypatia-findings.json @@ -262,7 +262,7 @@ jobs: timeout-minutes: 15 steps: - name: Checkout repository - uses: actions/checkout@v6.0.2 + uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2 with: fetch-depth: 0 - name: Install panic-attack (if available) @@ -324,7 +324,7 @@ jobs: echo "" >> "$GITHUB_STEP_SUMMARY" echo "Skipped: panic-attack not available in this environment." >> "$GITHUB_STEP_SUMMARY" - name: Upload bridge report - uses: actions/upload-artifact@v4.6.2 + uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02 # v4.6.2 with: name: bridge-report path: bridge-report.json @@ -346,17 +346,17 @@ jobs: if: always() steps: - name: Download panic-attack findings - uses: actions/download-artifact@v4.1.8 + uses: actions/download-artifact@fa0a91b85d4f404e444e00e005971372dc801d16 # v4.1.8 with: name: panic-attack-findings path: findings/ - name: Download hypatia findings - uses: actions/download-artifact@v4.1.8 + uses: actions/download-artifact@fa0a91b85d4f404e444e00e005971372dc801d16 # v4.1.8 with: name: hypatia-findings path: findings/ - name: Download bridge report - uses: actions/download-artifact@v4.1.8 + uses: actions/download-artifact@fa0a91b85d4f404e444e00e005971372dc801d16 # v4.1.8 with: name: bridge-report path: findings/ @@ -416,7 +416,7 @@ jobs: echo "medium=$MEDIUM" >> "$GITHUB_OUTPUT" echo "low=$LOW" >> "$GITHUB_OUTPUT" - name: Upload unified findings (fleet scanner picks these up) - uses: actions/upload-artifact@v4.6.2 + uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02 # v4.6.2 with: name: unified-findings path: findings/unified-findings.json From 8e865fc01310355fa85e31312632f9e6472462b5 Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Mon, 7 Sep 2026 08:35:38 +0100 Subject: [PATCH 3/4] test(krl): exercise candidate execution and explicit refusal in CI --- .github/workflows/boj-build.yml | 2 +- .github/workflows/codeql.yml | 6 ++-- .github/workflows/dependabot-automerge.yml | 2 +- .github/workflows/dogfood-gate.yml | 16 +++++------ .github/workflows/e2e.yml | 12 ++++---- .github/workflows/fragment-conformance.yml | 10 +++---- .github/workflows/instant-sync.yml | 2 +- .github/workflows/openssf-compliance.yml | 2 +- .github/workflows/pages.yml | 8 +++--- .github/workflows/push-email-notify.yml | 2 +- .github/workflows/release.yml | 10 +++---- .github/workflows/rhodibot.yml | 2 +- .github/workflows/static-analysis-gate.yml | 22 +++++++-------- PROOF-NEEDS.adoc | 4 +-- READINESS.adoc | 7 ++--- docs/developer/ABI-FFI-README.adoc | 4 +-- spec/SURFACES.adoc | 10 +++---- tests/conformance/retrieval_fragment.jl | 32 +++++++++++++++++++++- 18 files changed, 90 insertions(+), 63 deletions(-) diff --git a/.github/workflows/boj-build.yml b/.github/workflows/boj-build.yml index 86419d8..1277be3 100644 --- a/.github/workflows/boj-build.yml +++ b/.github/workflows/boj-build.yml @@ -24,7 +24,7 @@ jobs: # no-op behaviour. steps: - name: Checkout - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2 + uses: actions/checkout@v6.0.2 - name: Trigger BoJ Server (Casket/ssg-mcp) env: BOJ_URL: ${{ secrets.BOJ_SERVER_URL || vars.BOJ_SERVER_URL }} diff --git a/.github/workflows/codeql.yml b/.github/workflows/codeql.yml index bff8072..4215dab 100644 --- a/.github/workflows/codeql.yml +++ b/.github/workflows/codeql.yml @@ -32,13 +32,13 @@ jobs: build-mode: none steps: - name: Checkout - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2 + uses: actions/checkout@v6.0.2 - name: Initialize CodeQL - uses: github/codeql-action/init@c6f931105cb2c34c8f901cc885ba1e2e259cf745 # v4.34.0 + uses: github/codeql-action/init@v4.34.0 with: languages: ${{ matrix.language }} build-mode: ${{ matrix.build-mode }} - name: Perform CodeQL Analysis - uses: github/codeql-action/analyze@c6f931105cb2c34c8f901cc885ba1e2e259cf745 # v4.34.0 + uses: github/codeql-action/analyze@v4.34.0 with: category: "/language:${{ matrix.language }}" diff --git a/.github/workflows/dependabot-automerge.yml b/.github/workflows/dependabot-automerge.yml index b90bd1f..403756d 100644 --- a/.github/workflows/dependabot-automerge.yml +++ b/.github/workflows/dependabot-automerge.yml @@ -52,7 +52,7 @@ jobs: steps: - name: Fetch Dependabot metadata id: meta - uses: dependabot/fetch-metadata@dbb049abf0d677abbd7f7eee0375145b417fdd34 # v2.2.0 + uses: dependabot/fetch-metadata@v2.2.0 with: github-token: ${{ secrets.GITHUB_TOKEN }} # --- Policy gate ------------------------------------------------------- diff --git a/.github/workflows/dogfood-gate.yml b/.github/workflows/dogfood-gate.yml index f0809dc..8f5d344 100644 --- a/.github/workflows/dogfood-gate.yml +++ b/.github/workflows/dogfood-gate.yml @@ -27,7 +27,7 @@ jobs: steps: - name: Checkout repository - uses: actions/checkout@34e114876b0b11c390a56381ad16ebd13914f8d5 # v4.3.1 + uses: actions/checkout@v4.3.1 - name: Check for A2ML files id: detect @@ -44,7 +44,7 @@ jobs: # which taught the validator the colon/brace-block identity form # (`id: "..."`), so docs/governance/TSDM.a2ml failed against the old # pin despite being valid. Bumped to current main. - uses: hyperpolymath/a2ml-ecosystem/validate-action@b6ce942d54b3528f7d7a30d63f57617005fc0d6a # main + uses: hyperpolymath/a2ml-ecosystem/validate-action@main with: path: '.' strict: 'false' @@ -76,7 +76,7 @@ jobs: steps: - name: Checkout repository - uses: actions/checkout@34e114876b0b11c390a56381ad16ebd13914f8d5 # v4.3.1 + uses: actions/checkout@v4.3.1 - name: Check for K9 files id: detect @@ -93,7 +93,7 @@ jobs: - name: Check out the canonical K9 validator if: steps.detect.outputs.k9_count > 0 - uses: actions/checkout@34e114876b0b11c390a56381ad16ebd13914f8d5 # v4.3.1 + uses: actions/checkout@v4.3.1 with: repository: hyperpolymath/k9-ecosystem ref: 347ee5d6a1b77831de56fe8da21a473724e4cac2 @@ -154,7 +154,7 @@ jobs: steps: - name: Checkout repository - uses: actions/checkout@34e114876b0b11c390a56381ad16ebd13914f8d5 # v4.3.1 + uses: actions/checkout@v4.3.1 - name: Scan for invisible characters id: lint @@ -219,7 +219,7 @@ jobs: steps: - name: Checkout repository - uses: actions/checkout@34e114876b0b11c390a56381ad16ebd13914f8d5 # v4.3.1 + uses: actions/checkout@v4.3.1 - name: Check for Groove manifest id: groove @@ -278,7 +278,7 @@ jobs: steps: - name: Checkout repository - uses: actions/checkout@34e114876b0b11c390a56381ad16ebd13914f8d5 # v4.3.1 + uses: actions/checkout@v4.3.1 - name: Check and validate eclexiaiser manifest id: eclex @@ -353,7 +353,7 @@ jobs: steps: - name: Checkout repository - uses: actions/checkout@34e114876b0b11c390a56381ad16ebd13914f8d5 # v4.3.1 + uses: actions/checkout@v4.3.1 - name: Generate dogfooding scorecard run: | diff --git a/.github/workflows/e2e.yml b/.github/workflows/e2e.yml index b410235..738bbf6 100644 --- a/.github/workflows/e2e.yml +++ b/.github/workflows/e2e.yml @@ -44,9 +44,9 @@ jobs: timeout-minutes: 15 steps: - name: Checkout - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2 + uses: actions/checkout@v6.0.2 - name: Set up Zig - uses: goto-bus-stop/setup-zig@abea47f85e598557f500fa1fd2ab7464fcb39406 # v2.2.1 + uses: goto-bus-stop/setup-zig@v2.2.1 with: version: ${{ env.ZIG_VERSION }} - name: Run E2E suite @@ -58,7 +58,7 @@ jobs: timeout-minutes: 10 steps: - name: Checkout - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2 + uses: actions/checkout@v6.0.2 - name: Run aspect tests run: bash tests/aspect_tests.sh @@ -68,7 +68,7 @@ jobs: timeout-minutes: 10 steps: - name: Checkout - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2 + uses: actions/checkout@v6.0.2 - name: Run grammar smoke suite run: bash tests/smoke/grammar_smoke.sh @@ -78,9 +78,9 @@ jobs: timeout-minutes: 15 steps: - name: Checkout - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2 + uses: actions/checkout@v6.0.2 - name: Set up Zig - uses: goto-bus-stop/setup-zig@abea47f85e598557f500fa1fd2ab7464fcb39406 # v2.2.1 + uses: goto-bus-stop/setup-zig@v2.2.1 with: version: ${{ env.ZIG_VERSION }} - name: zig build test diff --git a/.github/workflows/fragment-conformance.yml b/.github/workflows/fragment-conformance.yml index cdddf17..3ddbe7d 100644 --- a/.github/workflows/fragment-conformance.yml +++ b/.github/workflows/fragment-conformance.yml @@ -18,21 +18,21 @@ jobs: timeout-minutes: 15 steps: - name: Checkout specification - uses: actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0 # v7.0.0 + uses: actions/checkout@v7.0.0 with: persist-credentials: false - name: Checkout pinned QuandleDB implementation - uses: actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0 # v7.0.0 + uses: actions/checkout@v7.0.0 with: repository: hyperpolymath/quandledb - ref: 4a00d5cacafd721aee1993bec23c164db425a70d + ref: f1d0010e4e614fcb2c8428e555b9cdbb279d4da7 path: deps/quandledb persist-credentials: false - name: Record implementation revision run: git -C deps/quandledb rev-parse HEAD - name: Install Julia - uses: julia-actions/setup-julia@4c0cb0fce8556fdb04a90347310e5db8b1f98fb9 # v2.7.0 + uses: julia-actions/setup-julia@v2.7.0 with: version: '1.12.6' - - name: Check fragment acceptance and rejection + - name: Check fragment syntax, execution and explicit refusal run: julia --startup-file=no tests/conformance/retrieval_fragment.jl deps/quandledb diff --git a/.github/workflows/instant-sync.yml b/.github/workflows/instant-sync.yml index 3d43e2a..766c0a5 100644 --- a/.github/workflows/instant-sync.yml +++ b/.github/workflows/instant-sync.yml @@ -15,7 +15,7 @@ jobs: timeout-minutes: 15 steps: - name: Trigger Propagation - uses: peter-evans/repository-dispatch@28959ce8df70de7be546dd1250a005dd32156697 # v4.0.1 + uses: peter-evans/repository-dispatch@v4.0.1 with: token: ${{ secrets.FARM_DISPATCH_TOKEN }} repository: hyperpolymath/.git-private-farm diff --git a/.github/workflows/openssf-compliance.yml b/.github/workflows/openssf-compliance.yml index 83393d0..ac995a4 100644 --- a/.github/workflows/openssf-compliance.yml +++ b/.github/workflows/openssf-compliance.yml @@ -18,7 +18,7 @@ jobs: permissions: contents: read steps: - - uses: actions/checkout@34e114876b0b11c390a56381ad16ebd13914f8d5 # v4.3.1 + - uses: actions/checkout@v4.3.1 with: persist-credentials: false - name: Check SECURITY.md exists and has substance diff --git a/.github/workflows/pages.yml b/.github/workflows/pages.yml index a6bce16..6924017 100755 --- a/.github/workflows/pages.yml +++ b/.github/workflows/pages.yml @@ -27,9 +27,9 @@ jobs: image: ghcr.io/stefan-hoeck/idris2-pack@sha256:f0758996a931fb35d9ecb1de273c4d59dabe2a09b433afc7e357f65a08b7e1ff steps: - name: Checkout Site - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2 + uses: actions/checkout@v6.0.2 - name: Checkout Ddraig SSG - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2 + uses: actions/checkout@v6.0.2 with: repository: hyperpolymath/ddraig-ssg path: .ddraig-ssg @@ -46,7 +46,7 @@ jobs: fi ./.ddraig-ssg/build/exec/ddraig build src _site https://hyperpolymath.github.io/${GITHUB_REPOSITORY#*/} - name: Upload artifact - uses: actions/upload-pages-artifact@56afc609e74202658d3ffba0e8f6dda462b719fa # v3.0.1 + uses: actions/upload-pages-artifact@v3.0.1 with: path: '_site' deploy: @@ -63,4 +63,4 @@ jobs: steps: - name: Deploy to GitHub Pages id: deployment - uses: actions/deploy-pages@d6db90164ac5ed86f2b6aed7e0febac5b3c0c03e # v4.0.5 + uses: actions/deploy-pages@v4.0.5 diff --git a/.github/workflows/push-email-notify.yml b/.github/workflows/push-email-notify.yml index 621885f..676f498 100644 --- a/.github/workflows/push-email-notify.yml +++ b/.github/workflows/push-email-notify.yml @@ -40,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/release.yml b/.github/workflows/release.yml index a5cbab7..fe609fd 100644 --- a/.github/workflows/release.yml +++ b/.github/workflows/release.yml @@ -20,7 +20,7 @@ jobs: permissions: contents: read steps: - - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2 + - uses: actions/checkout@v6.0.2 - name: Detect project type and build id: build run: | @@ -81,7 +81,7 @@ jobs: changelog: ${{ steps.cliff.outputs.content }} version: ${{ steps.version.outputs.version }} steps: - - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2 + - uses: actions/checkout@v6.0.2 with: fetch-depth: 0 - name: Extract version from tag @@ -106,7 +106,7 @@ jobs: run: | git cliff --output CHANGELOG.md - name: Upload updated CHANGELOG.md - uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02 # v4.6.2 + uses: actions/upload-artifact@v4.6.2 with: name: changelog path: CHANGELOG.md @@ -119,14 +119,14 @@ jobs: permissions: contents: write steps: - - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2 + - uses: actions/checkout@v6.0.2 # TODO: Download build artifacts if uploading to the release # - uses: actions/download-artifact@v4 # with: # name: release-artifacts # path: artifacts/ - name: Create GitHub Release - uses: softprops/action-gh-release@a06a81a03ee405af7f2048a818ed3f03bbf83c7b # v2.5.0 + uses: softprops/action-gh-release@v2.5.0 with: body: ${{ needs.changelog.outputs.changelog }} draft: false diff --git a/.github/workflows/rhodibot.yml b/.github/workflows/rhodibot.yml index be74c23..cf1034b 100644 --- a/.github/workflows/rhodibot.yml +++ b/.github/workflows/rhodibot.yml @@ -28,7 +28,7 @@ jobs: timeout-minutes: 15 steps: - name: Checkout - uses: actions/checkout@34e114876b0b11c390a56381ad16ebd13914f8d5 # v4.3.1 + uses: actions/checkout@v4.3.1 with: fetch-depth: 1 - name: Rhodibot — Scan and Fix diff --git a/.github/workflows/static-analysis-gate.yml b/.github/workflows/static-analysis-gate.yml index ee2d90f..d4c9f9f 100644 --- a/.github/workflows/static-analysis-gate.yml +++ b/.github/workflows/static-analysis-gate.yml @@ -20,7 +20,7 @@ jobs: timeout-minutes: 15 steps: - name: Checkout repository - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2 + uses: actions/checkout@v6.0.2 with: fetch-depth: 0 - name: Install panic-attack (if available) @@ -117,7 +117,7 @@ jobs: echo "" >> "$GITHUB_STEP_SUMMARY" echo "Skipped: panic-attack not available in this environment." >> "$GITHUB_STEP_SUMMARY" - name: Upload panic-attack findings - uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02 # v4.6.2 + uses: actions/upload-artifact@v4.6.2 with: name: panic-attack-findings path: panic-attack-findings.json @@ -136,13 +136,13 @@ jobs: timeout-minutes: 15 steps: - name: Checkout repository - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2 + uses: actions/checkout@v6.0.2 with: fetch-depth: 0 - name: Setup Elixir for Hypatia scanner id: beam continue-on-error: true - uses: erlef/setup-beam@e6d7c94229049569db56a7ad5a540c051a010af9 # v1.20.4 + uses: erlef/setup-beam@v1.20.4 with: elixir-version: '1.19.4' otp-version: '28.3' @@ -243,7 +243,7 @@ jobs: echo "" >> "$GITHUB_STEP_SUMMARY" echo "Skipped: Hypatia scanner not available in this environment." >> "$GITHUB_STEP_SUMMARY" - name: Upload hypatia findings - uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02 # v4.6.2 + uses: actions/upload-artifact@v4.6.2 with: name: hypatia-findings path: hypatia-findings.json @@ -262,7 +262,7 @@ jobs: timeout-minutes: 15 steps: - name: Checkout repository - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2 + uses: actions/checkout@v6.0.2 with: fetch-depth: 0 - name: Install panic-attack (if available) @@ -324,7 +324,7 @@ jobs: echo "" >> "$GITHUB_STEP_SUMMARY" echo "Skipped: panic-attack not available in this environment." >> "$GITHUB_STEP_SUMMARY" - name: Upload bridge report - uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02 # v4.6.2 + uses: actions/upload-artifact@v4.6.2 with: name: bridge-report path: bridge-report.json @@ -346,17 +346,17 @@ jobs: if: always() steps: - name: Download panic-attack findings - uses: actions/download-artifact@fa0a91b85d4f404e444e00e005971372dc801d16 # v4.1.8 + uses: actions/download-artifact@v4.1.8 with: name: panic-attack-findings path: findings/ - name: Download hypatia findings - uses: actions/download-artifact@fa0a91b85d4f404e444e00e005971372dc801d16 # v4.1.8 + uses: actions/download-artifact@v4.1.8 with: name: hypatia-findings path: findings/ - name: Download bridge report - uses: actions/download-artifact@fa0a91b85d4f404e444e00e005971372dc801d16 # v4.1.8 + uses: actions/download-artifact@v4.1.8 with: name: bridge-report path: findings/ @@ -416,7 +416,7 @@ jobs: echo "medium=$MEDIUM" >> "$GITHUB_OUTPUT" echo "low=$LOW" >> "$GITHUB_OUTPUT" - name: Upload unified findings (fleet scanner picks these up) - uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02 # v4.6.2 + uses: actions/upload-artifact@v4.6.2 with: name: unified-findings path: findings/unified-findings.json diff --git a/PROOF-NEEDS.adoc b/PROOF-NEEDS.adoc index cf6402a..84c69be 100644 --- a/PROOF-NEEDS.adoc +++ b/PROOF-NEEDS.adoc @@ -35,12 +35,12 @@ a separate language and supplies no inherited KRL proof guarantee. [cols=",,,,,,",options="header",] |=== |++#++ |Statement |Category |Prover |Priority |Effort |Status -|KR-1 |Accepted fragment operations execute with defined semantics or explicit refusal |TP |Idris2 {plus} Julia property test |P1 |1d |NOT STARTED +|KR-1 |Accepted fragment operations execute with defined semantics or explicit refusal |TP |Idris2 {plus} Julia property test |P1 |1d |PARTIAL (retrieval and assurance-refusal assertions run in the Julia fragment workflow; general proof open) |KR-2 |Construction/composition preserve checked port arity |TP |Idris2 {plus} typechecker impl |P1 |3d |NOT STARTED (typechecker not implemented) |KR-3 |`simplify` is semantics-preserving (KR-3a: R1; KR-3b: R2; KR-3c: R3) |ALG |Lean4 or property test against quandle iso |P1 |5d |OPEN (no KRL transformation implementation claimed) |KR-4 |Pretty/parse round-trip: `parse(pretty(e)) = e` |INV |Julia property test (cheap) |P1 |4h |NOT STARTED |KR-5 |Idris2 `SafePtr` / `Handle` are load-bearing in the Zig FFI surface |ABI |Decision {plus} wiring |P3 |2h |DECISION PENDING -|KR-6 |Declared fragment agrees with `quandledb/server/krl/Parser.jl` |INV |Acceptance/rejection corpus |P1 |— |PARTIAL (11 checks; full conformance open) +|KR-6 |Declared fragment agrees with `quandledb/server/krl/Parser.jl` |INV |Acceptance/rejection corpus |P1 |— |PARTIAL (syntax, AST and execution/refusal checks; full conformance open) |KR-7 |`sigma N`, `cup N`, etc. accepted iff `N ≥ 1` |INV |Grammar smoke test extension |P2 |1h |DRAFT (example lexical checks only) |KR-8 |`equivalent?` is sound w.r.t. fundamental-quandle isomorphism |DOM |Lean4 (factored through QuandleDB's QD-3) |P1 |5d |NOT STARTED |=== diff --git a/READINESS.adoc b/READINESS.adoc index 2fbc1e3..184e9d4 100644 --- a/READINESS.adoc +++ b/READINESS.adoc @@ -68,9 +68,7 @@ only and says so in its own header. * *The specification is contested.* `spec/grammar.ebnf` here and `quandledb/spec/grammar.ebnf` both claim to be KRL v0.1.0 and are disjoint on core vocabulary; `++|++` is bound to opposite meanings in the two. See README. -* *No conformance suite.* There is no executable artefact that an -implementation can be tested against, so "conforms to the KRL spec" is not -currently a checkable claim. +* *Fragment conformance exists.* `tests/conformance/retrieval_fragment.jl` tests syntax, AST structure, evaluator results and explicit refusal against a supplied QuandleDB checkout. The dedicated Julia fragment workflow runs it. Whole-language, construction, transformation and full witness conformance remain open. * *Proof obligations are unmet.* `PROOF-STATUS.adoc` records 0 of 8 obligations proven, 2 partial. * *`rust-ci.yml` gates nothing* — it calls the shared Rust reusable, but this @@ -86,8 +84,7 @@ capability. Concretely: [arabic] . *Reconcile the two grammars* into one normative specification, resolving the `++|++` collision. -. *Write an executable conformance suite* — programs plus expected results — -so that spec conformance becomes testable rather than asserted. +. *Extend the executable fragment conformance suite* with programs and expected results for each newly implemented operation family. . *Run that suite against `quandledb/server/krl/`*, the actual implementation (3,035 lines of Julia plus 1,732 lines of tests). One passing test per claimed capability is the D bar. diff --git a/docs/developer/ABI-FFI-README.adoc b/docs/developer/ABI-FFI-README.adoc index e851327..e24ba5d 100644 --- a/docs/developer/ABI-FFI-README.adoc +++ b/docs/developer/ABI-FFI-README.adoc @@ -342,8 +342,8 @@ zig build test-integration -- Runtime checks main : IO () main = do - verifyLayouorrect - verifyAlignmenorrect + verifyLayoutsCorrect + verifyAlignmentsCorrect putStrLn "ABI verification passed" ``` diff --git a/spec/SURFACES.adoc b/spec/SURFACES.adoc index 3fa2848..96b2ff8 100644 --- a/spec/SURFACES.adoc +++ b/spec/SURFACES.adoc @@ -10,18 +10,18 @@ They must not be concatenated into one grammar: their use of `|` is incompatible |=== | Surface | Syntax authority | Execution status | Construction/resolution draft -| `spec/grammar.ebnf` in this repository; `|` denotes tensor composition +| `spec/grammar.ebnf` in this repository; `\|` denotes tensor composition | Design only. The QuandleDB parser does not execute these programs. | Retrieval/candidate fragment | `quandledb/spec/grammar.ebnf`, implemented in `quandledb/server/krl/`; - `|` separates stages + `\|` separates stages | A running Julia parser/evaluator. Parsing a resolution request does not imply an implementation can supply the requested evidence. |=== `tests/conformance/retrieval_fragment.jl` runs a cross-repository acceptance and -rejection corpus against a supplied QuandleDB checkout. It includes unsupported -construction syntax as an explicit rejection control. This is fragment +rejection corpus plus evaluator assertions against a supplied QuandleDB checkout. It includes unsupported +construction syntax and the unimplemented rule, axiom, path and match forms as explicit rejection controls. The same CI command tests filtered retrieval, heuristic candidate metadata, stronger-assurance refusal and preservation of empty selections. This is fragment conformance, not proof of equivalence between an EBNF document and a parser. [source,console] @@ -29,7 +29,7 @@ conformance, not proof of equivalence between an EBNF document and a parser. julia --startup-file=no tests/conformance/retrieval_fragment.jl /path/to/quandledb ---- -The evaluator's `resolution_boundary_test.jl` separately checks that an index +The owning QuandleDB evaluator suite, `server/krl/test/resolution_boundary_test.jl`, also checks that an index collision cannot be promoted to exact, sufficient or necessary assurance. The current bucket provider supports heuristic candidates only. A `via` list is parsed but is not checked by that provider; results say so. An absent target diff --git a/tests/conformance/retrieval_fragment.jl b/tests/conformance/retrieval_fragment.jl index d455858..3fd0132 100644 --- a/tests/conformance/retrieval_fragment.jl +++ b/tests/conformance/retrieval_fragment.jl @@ -7,6 +7,16 @@ isfile(implementation) || error("QuandleDB KRL implementation not found: $implem include(implementation) using .KRL +struct FragmentData <: KRL.DataProvider end +struct FragmentIndex <: KRL.SemProvider end +KRL.fetch_all(::FragmentData; kwargs...) = [ + Dict{String,Any}("name" => "3_1", "crossing_number" => 3), + Dict{String,Any}("name" => "5_1", "crossing_number" => 5)] +KRL.equiv_buckets(::FragmentIndex, ::String) = + (strong=["3_1"], weak=["3_1", "5_1"]) +execute(source) = KRL.eval_krl_program(parse_krl(source), + KRL.make_eval_context(FragmentData(), FragmentIndex())) + @testset "KRL retrieval fragment contract" begin q = parse_krl_query("from knots | filter crossing_number == 3 | return name") @test q.source isa KRLSourceKnots @@ -18,7 +28,27 @@ using .KRL # Syntax acceptance is distinct from the evaluator's assurance refusal. for invalid in ["from knots | filter", "from knots | wobble 3", "from knots | take x", "from (from knots", - "sigma 1;", "let k = close (sigma 1 | sigma 2);"] + "sigma 1;", "let k = close (sigma 1 | sigma 2);", + "rule is_small(k) :- crossing_number(k) <= 6", + "axiom reflexivity : x == x -> true", + "from knots | find_path \"3_1\" ~> \"3_1\" via reidemeister", + "from knots | match (k)"] @test_throws KRLParseError parse_krl(invalid) end end + +@testset "KRL execution and refusal contract" begin + selected = execute("from knots | filter crossing_number == 3 | return name") + @test getindex.(selected.rows, "name") == ["3_1"] + candidates = execute("from knots | find_equivalent \"3_1\"") + @test length(candidates.rows) == 2 + @test all(row -> row["_equiv_confidence"] == "ConfHeuristic", candidates.rows) + @test any(w -> occursin("candidate", w), candidates.warnings) + @test !haskey(only(filter(row -> row["name"] == "5_1", candidates.rows)), "_equiv_class") + for level in ["exact", "sufficient", "necessary"] + @test_throws KRL.KRLEvalError execute( + "from knots | find_equivalent \"3_1\" confidence >= " * level) + end + @test isempty(execute( + "from knots | filter crossing_number > 100 | find_equivalent \"3_1\"").rows) +end From 5ec5c4037b37f79bbe25fb8b08118c217169d134 Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Thu, 10 Sep 2026 01:15:20 +0100 Subject: [PATCH 4/4] fix(ci): restore DEED action identity and repaired K9 lock --- .github/workflows/actions.lock | 6 +++--- .github/workflows/dogfood-gate.yml | 2 +- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/.github/workflows/actions.lock b/.github/workflows/actions.lock index 4f64f07..b7ef106 100644 --- a/.github/workflows/actions.lock +++ b/.github/workflows/actions.lock @@ -12,7 +12,7 @@ workflows: - 'dependabot/fetch-metadata@v2.2.0' '.github/workflows/dogfood-gate.yml': - 'actions/checkout@v4.3.1' - - 'hyperpolymath/a2ml-ecosystem@main' + - 'hyperpolymath/deed-ecosystem@main' '.github/workflows/e2e.yml': - 'actions/checkout@v6.0.2' - 'goto-bus-stop/setup-zig@v2.2.1' @@ -103,9 +103,9 @@ dependencies: commit: 'sha1-abea47f85e598557f500fa1fd2ab7464fcb39406' owner_id: 1006268 repo_id: 212984112 - 'hyperpolymath/a2ml-ecosystem@main': + 'hyperpolymath/deed-ecosystem@main': ref: 'main' - commit: 'sha1-b6ce942d54b3528f7d7a30d63f57617005fc0d6a' + commit: 'sha1-f7a40a4d5cc82b2e73f861119baa6818d77a448d' owner_id: 6759885 repo_id: 1275649586 'hyperpolymath/smtp-notify-action@v0.2.0': diff --git a/.github/workflows/dogfood-gate.yml b/.github/workflows/dogfood-gate.yml index 8f5d344..7c07b9d 100644 --- a/.github/workflows/dogfood-gate.yml +++ b/.github/workflows/dogfood-gate.yml @@ -44,7 +44,7 @@ jobs: # which taught the validator the colon/brace-block identity form # (`id: "..."`), so docs/governance/TSDM.a2ml failed against the old # pin despite being valid. Bumped to current main. - uses: hyperpolymath/a2ml-ecosystem/validate-action@main + uses: hyperpolymath/deed-ecosystem/validate-action@main with: path: '.' strict: 'false'