|
| 1 | +// SPDX-License-Identifier: CC-BY-SA-4.0 |
| 2 | +// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk> |
| 3 | += AFFIRMATION — tangle, as of 2026-06-19 |
| 4 | +:toc: macro |
| 5 | +:toclevels: 2 |
| 6 | + |
| 7 | +_the No-Bullshit file: what we affirm was true and checkable at this moment_ |
| 8 | + |
| 9 | +[NOTE] |
| 10 | +==== |
| 11 | +*Genre.* An *affirmation* is a solemn declaration of the truth of a statement, |
| 12 | +made by someone who _declines to swear an oath_ — our truth-as-best-believed at |
| 13 | +a stamped instant, binding on our honesty, not a claim of infallibility. It is |
| 14 | +not the README and not the EXPLAINME: |
| 15 | +
|
| 16 | +[cols="1,3,2",options="header"] |
| 17 | +|=== |
| 18 | +| File | Answers | Tense |
| 19 | +| `README.adoc` | _Where is this going, and why?_ — Tangle's purpose and steering | future / aspirational |
| 20 | +| `EXPLAINME.adoc` | _How is it built, and what's the evidence?_ | descriptive / mechanism |
| 21 | +| *`AFFIRMATION.adoc`* (this file) | _What can we honestly affirm was *true and checkable* at a stamped moment?_ | a frozen instant, falsifiable |
| 22 | +|=== |
| 23 | +
|
| 24 | +Every repo in the estate carries one, per the 2026-06-19 estate rule. |
| 25 | +==== |
| 26 | + |
| 27 | +toc::[] |
| 28 | + |
| 29 | +== What this is, and how it is designed to work |
| 30 | + |
| 31 | +*What it is.* A short, dated, jointly-signed snapshot of what we can _honestly |
| 32 | +and verifiably_ claim about the tangle repo at one exact commit. |
| 33 | + |
| 34 | +*How it is designed to work.* |
| 35 | + |
| 36 | +. *Ground truth, not memory.* Every gate result below was produced by _running |
| 37 | + the check this session_. *Material caveat (read it):* `just` is absent, so RSR/ |
| 38 | + contractile checks were run *as bash*; and *none of tangle's build/test/proof |
| 39 | + toolchains were runnable this session* — `cargo build --offline` could not |
| 40 | + resolve dependencies (no vendored crates / no network), and OCaml `dune` + Lean |
| 41 | + are not installed. See <<Outstanding / not-run>>. |
| 42 | +. *A frozen anchor.* The file names the exact commit SHA, branch, and toolchain |
| 43 | + (see <<Verifiable anchor>>). |
| 44 | +. *A real signature.* Authoritatively landed by the maintainer's *signed git |
| 45 | + commit*. The AI engineering party *cannot* GPG-sign and does not claim to. |
| 46 | + |
| 47 | +*We are fallible.* Best honest belief, not a proof of its own correctness. |
| 48 | + |
| 49 | +== The epistemic contract |
| 50 | + |
| 51 | +This document records our *best joint belief* at the timestamp below. *No |
| 52 | +intentional overclaim:* where a check passed we say "PASS"; where the toolchain |
| 53 | +was *absent* we say "not run", never "passed". |
| 54 | + |
| 55 | +*Standing invitation to refute.* Reproduce <<reproduce>> at the stamped commit |
| 56 | +and tell us where the discrepancy is. |
| 57 | + |
| 58 | +== Verifiable anchor |
| 59 | + |
| 60 | +[cols="1,3"] |
| 61 | +|=== |
| 62 | +| *Repo* | `hyperpolymath/tangle` — Tangle / KRL topological programming language: the proven type-safe small-step core + canonical TangleIR |
| 63 | +| *Branch* | `claude/practical-newton-9eFe2` (feature branch; *not* anchored to `main`) |
| 64 | +| *Commit (HEAD)* | `102499dbacb005bb5adc46736c8798fa1d365a82` |
| 65 | +| *Permalink* | https://github.com/hyperpolymath/tangle/tree/102499dbacb005bb5adc46736c8798fa1d365a82 |
| 66 | +| *Verified* | 2026-06-19 (checks run this session; precise UTC second not captured — date, not claimed instant) |
| 67 | +| *Working-tree delta* | Clean — `git status --porcelain` shows only this untracked `AFFIRMATION.adoc`. (The README stack-diagram edit placing VerisimCore is *maintainer-confirmed* and is committed in the parent commit `102499d`.) |
| 68 | +| *Toolchain (present)* | `git`, `Agda 2.6.3`, `rustc`, `cargo`. *Absent this session:* `just`, `deno`, `julia`, `lean`, OCaml `dune`. |
| 69 | +| *Run method* | RSR/contractile gate bodies as bash. `cargo build --offline` *attempted* (dep-resolution failure — not a code verdict). OCaml + Lean *not run* (absent). |
| 70 | +| *HEAD commit signature* | *Not signed by the AI party.* Authoritative signature is the maintainer's signed commit that lands this file. |
| 71 | +|=== |
| 72 | + |
| 73 | +== Stack placement: VerisimCore (maintainer-confirmed 2026-06-19) [[verisimcore]] |
| 74 | + |
| 75 | +The architecture ladder in `README.adoc` was updated and *confirmed correct by |
| 76 | +the maintainer* on 2026-06-19. The canonical stack now reads: |
| 77 | + |
| 78 | +[literal] |
| 79 | +KRL (surface language) |
| 80 | + ↓ |
| 81 | +TangleIR (canonical representation) |
| 82 | + ↓ |
| 83 | +VerisimCore (categorical abstraction) |
| 84 | + ↓ |
| 85 | +Skein / QuandleDB (storage and equivalence) |
| 86 | + |
| 87 | +This *resolves the previously-parked VerisimCore-placement question* — VerisimCore |
| 88 | +sits between TangleIR and the storage/equivalence layer as the categorical |
| 89 | +abstraction. The edit is committed in the parent commit `102499d` (not |
| 90 | +uncommitted). It simplifies the diagram's labels; the finer estate framings (e.g. |
| 91 | +"KRL is not merely a query language", "Skein is the engine") continue to live in |
| 92 | +krl's and Skein.jl's own docs and affirmations. |
| 93 | + |
| 94 | +== Companion documents and repo metadata (cross-check) |
| 95 | + |
| 96 | +* *`README.adoc`* — title `= Tangle / KRL — Topological Programming Language` |
| 97 | + (real). Now carries the maintainer-confirmed VerisimCore stack (committed, |
| 98 | + parent `102499d`). |
| 99 | +* *`EXPLAINME.adoc`* — present, real: `= EXPLAINME: Tangle`. |
| 100 | +* *`0-AI-MANIFEST.a2ml`* — present. |
| 101 | +* *Template residue* — *5 files* still contain `{{PLACEHOLDER}}` tokens and *8 |
| 102 | + files* reference the `rsr-template-repo` lineage. The `Justfile` itself is |
| 103 | + clean of the template name. Partial instantiation debt — noted, not hidden. |
| 104 | +* *GitHub repo description / topics* — *not fetched this session* (no `gh`). |
| 105 | + |
| 106 | +== The honest state (one breath) |
| 107 | + |
| 108 | +tangle is the *most rigorous repo in the estate so far*: a serious multi-language |
| 109 | +implementation — an OCaml compiler core (`compiler/{bin,lib,test}` + |
| 110 | +`dune-project`), Rust crates (`src/rust` with a committed `Cargo.lock`, |
| 111 | +`compiler/tangle-lsp`, `compiler/tangle-wasm`), Lean-4 type-safety proofs |
| 112 | +(`proofs/Tangle.lean`, `proofs/TG3Differential.lean`, `lean-toolchain`), grammars, |
| 113 | +and five dialects. It self-grades READINESS *C* and documents *real* formal |
| 114 | +verification, and its stack placement (incl. VerisimCore) is maintainer-confirmed. |
| 115 | +The honest gaps: some template residue remains, and — crucially — *none of its |
| 116 | +build/test/proof toolchains were runnable this session*, so what follows confirms |
| 117 | +*structure and the repo's own proof ledger*, not a fresh green build. |
| 118 | + |
| 119 | +== What is solid (and how we checked) |
| 120 | + |
| 121 | +* *MUST/TRUST-style checks — PASS.* Run as bash: LICENSE present; no banned |
| 122 | + `Dockerfile`/`Makefile`; SPDX headers on a sampled 120 `.rs` files (0 |
| 123 | + unheadered); LICENSE carries an SPDX/MPL identifier; no `.env` / |
| 124 | + `credentials.json` committed. |
| 125 | +* *Real, substantial, multi-language content.* OCaml compiler (`compiler/lib`, |
| 126 | + `compiler/bin`, `compiler/test`, `dune-project`); 18 Rust source files with a |
| 127 | + pinned `Cargo.lock`; LSP + WASM Rust crates; grammars (`src/tangle.ebnf`, |
| 128 | + `src/tangle-jtv.ebnf`, `spec/grammar.ebnf`); Lean proofs; five dialects |
| 129 | + (`braid-calculus`, `quantum-circuit`, `skein-algebra`, `string-diagram`, |
| 130 | + `virtual-knot`). |
| 131 | +* *Documented formal verification (the repo's ledger, reported as such).* |
| 132 | + `PROOF-NEEDS.md` records *TG-3 LANDED* at translation-validation level: *496 |
| 133 | + Lean kernel-checked obligations* in `TG3Differential.lean` (generated from |
| 134 | + `infer_expr`, `by decide`) + *1008 OCaml `--check` assertions* (`dune |
| 135 | + runtest`), reduced via TG-2 (`infer ≡ HasType`). We report this as tangle's |
| 136 | + *own documented status* — we did *not* re-run Lean/OCaml this session. |
| 137 | + |
| 138 | +== Known-incomplete but honestly fenced (loud, never silent) |
| 139 | + |
| 140 | +* *READINESS grade `C`.* `READINESS.md` self-assesses *Current Grade: C* — |
| 141 | + reported as-is. |
| 142 | +* *Template residue.* 5 `{{PLACEHOLDER}}` files + 8 `rsr-template-repo` |
| 143 | + references remain to be cleaned. |
| 144 | +* *Proof scope is honest in the repo's own words:* TG-3 refinement is OCaml→Lean |
| 145 | + *only* (not a universal Lean proof over all OCaml runs); `bool==bool` and the |
| 146 | + `close` boundary are catalogued divergences (D1/D2). We do not inflate it. |
| 147 | + |
| 148 | +== Outstanding / not-run (no spin) [[Outstanding / not-run]] |
| 149 | + |
| 150 | +* *No build/test/proof toolchain was runnable this session.* |
| 151 | + ** `cargo build --offline` *failed to resolve dependencies* (`serde`, … are not |
| 152 | + vendored and offline mode cannot fetch them). This is an *environment* |
| 153 | + limit, **not** a code verdict — `Cargo.lock` is present; a *networked* |
| 154 | + `cargo build`/`cargo test` in-environment is the authoritative check. |
| 155 | + ** OCaml `dune` and `lean` are *absent*, so the compiler test suite and the |
| 156 | + Lean proofs were *not executed*. We affirm the proof *files exist* and |
| 157 | + report the repo's *documented* TG-2/TG-3 status — we do *not* affirm, from |
| 158 | + this session, a fresh green proof/build. |
| 159 | + |
| 160 | +== Reproduce it yourself [[reproduce]] |
| 161 | + |
| 162 | +From the repo root, at the commit above: |
| 163 | + |
| 164 | +[source,bash] |
| 165 | +---- |
| 166 | +git rev-parse HEAD # expect 102499dbacb005bb5adc46736c8798fa1d365a82 |
| 167 | +git status --porcelain # expect only this untracked AFFIRMATION.adoc |
| 168 | +
|
| 169 | +# MUST / TRUST style (expect PASS): |
| 170 | +test -f LICENSE; test ! -f Dockerfile -a ! -f Makefile |
| 171 | +grep -q 'SPDX\|MPL' LICENSE; test ! -f .env |
| 172 | +
|
| 173 | +# Instantiation debt (expect residue): |
| 174 | +grep -rl '{{'{{'}}[A-Z_]*{{'}}'}}' --include='*.adoc' --include='*.md' . | grep -v PLACEHOLDERS # ~5 files |
| 175 | +grep -rl 'rsr-template-repo' . | grep -v '.git/' # ~8 files |
| 176 | +
|
| 177 | +# The honest gaps (NOT runnable without env/toolchain): |
| 178 | +# ( cd src/rust && cargo build ) # needs network or vendored deps |
| 179 | +# ( cd compiler && dune runtest ) # needs OCaml/dune |
| 180 | +# bash proofs/check-tg3-differential.sh # needs Lean |
| 181 | +---- |
| 182 | + |
| 183 | +== One-line characterisation (quote this) |
| 184 | + |
| 185 | +"Tangle is the proven type-safe small-step core + TangleIR of the KRL stack |
| 186 | +(KRL → TangleIR → VerisimCore → Skein/QuandleDB, maintainer-confirmed) — a |
| 187 | +serious multi-language implementation (OCaml compiler, Rust LSP/WASM with a |
| 188 | +pinned `Cargo.lock`, Lean-4 type-safety proofs, five dialects) that self-grades |
| 189 | +READINESS `C` and documents real formal verification (TG-3 translation-validation |
| 190 | +LANDED: 496 Lean obligations + 1008 OCaml assertions, per its own proof ledger). |
| 191 | +`MUST`/`TRUST` gates pass; honest debt: 5 placeholder files + 8 `rsr-template-repo` |
| 192 | +references remain, and *none* of its build/test/proof toolchains were runnable |
| 193 | +this session (cargo offline can't resolve deps; OCaml/dune + Lean absent) — so |
| 194 | +structure + the repo's proof records are confirmed, not a fresh green build. No |
| 195 | +intentional overclaim." |
| 196 | + |
| 197 | +== Key concern + cross-repo wiring |
| 198 | + |
| 199 | +tangle's *key concern* is *type-safe semantics + the canonical TangleIR* — the |
| 200 | +proven small-step core that KRL lowers into and that the categorical / |
| 201 | +storage / equivalence layers build on. Per the 2026-06-19 estate rule, each repo |
| 202 | +carries its own AFFIRMATION + scoped Must/Intend/Wish table; tangle's lives at |
| 203 | +`docs/identity-fabric/musts-intends-wishes.adoc`. Confirmed stack: *krl* (surface |
| 204 | +DSL) → *tangle* (TangleIR + type-safe core, this repo) → *VerisimCore* |
| 205 | +(categorical abstraction) → *Skein.jl* / *quandledb* (storage + equivalence). |
| 206 | +Adjacent: *echo-types* — structured-loss theory + the identity-fabric framing. |
| 207 | + |
| 208 | +== Joint attestation |
| 209 | + |
| 210 | +To the best of our joint belief at the timestamp above, every claim in this file |
| 211 | +is true and was checked as described — with no intentional overclaim and with the |
| 212 | +un-run toolchains stated rather than implied. |
| 213 | + |
| 214 | +* *Engineering party (AI):* ran the RSR/contractile checks recorded here as bash |
| 215 | + on 2026-06-19, attempted the offline cargo build, committed the |
| 216 | + maintainer-confirmed VerisimCore README edit, and stands behind this wording as |
| 217 | + a faithful report — including the toolchain-absent caveats and explicitly *not* |
| 218 | + having re-run the Lean/OCaml proofs. |
| 219 | +* *Owner / maintainer:* Jonathan D.A. Jewell — signs by committing this file with |
| 220 | + `-S`; the signed git commit over this content, at the SHA above, is the |
| 221 | + authoritative form. |
| 222 | +* *Signed-off-date:* (fill on signing) |
0 commit comments