spec: distinguish resolution design and executable fragment #74
There are no files selected for viewing
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,130 @@ | ||
| # 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/deed-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/deed-ecosystem@main': | ||
| ref: 'main' | ||
| commit: 'sha1-f7a40a4d5cc82b2e73f861119baa6818d77a448d' | ||
| owner_id: 6759885 | ||
| repo_id: 1275649586 | ||
| '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 |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,38 @@ | ||
| # 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: | ||
| name: KRL fragment conformance | ||
| 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: 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@v2.7.0 | ||
|
Check failure on line 34 in .github/workflows/fragment-conformance.yml
|
||
| with: | ||
| version: '1.12.6' | ||
| - name: Check fragment syntax, execution and explicit refusal | ||
| run: julia --startup-file=no tests/conformance/retrieval_fragment.jl deps/quandledb | ||
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -1,144 +1,99 @@ | ||
| // SPDX-License-Identifier: CC-BY-SA-4.0 | ||
| // SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk> | ||
| [[assumptions-registry--krl]] | ||
| == Assumptions Registry — KRL | ||
|
|
||
| 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]. | ||
|
|
||
| Every load-bearing *unproven* assumption used in this repo, with an | ||
| ID, classification, and the obligation it supports. | ||
|
|
||
| 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. | ||
|
|
||
| ''''' | ||
|
|
||
| [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{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 | ||
|
|
||
| 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. | ||
|
|
||
| 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.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 | ||
|
|
||
| [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 | | ||
| |DESIGN → MATH (rare) |the design happens to encode a known theorem | | ||
| |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. | ||
|
|
||
| ''''' | ||
|
|
||
| === Changelog | ||
|
|
||
| [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 | ||
| |=== |
Oops, something went wrong.
Oops, something went wrong.
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Uh oh!
There was an error while loading. Please reload this page.