diff --git a/frontend/src/type-theory/dendrogram-receipts/bridgeIndex.ts b/frontend/src/type-theory/dendrogram-receipts/bridgeIndex.ts new file mode 100644 index 0000000..6cf56b2 --- /dev/null +++ b/frontend/src/type-theory/dendrogram-receipts/bridgeIndex.ts @@ -0,0 +1,214 @@ +// SPDX-License-Identifier: AGPL-3.0-only +// SPDX-FileCopyrightText: 2026 Joshua Benjamin Jewell; 2026 Jonathan D.A. Jewell (hyperpolymath) +// +// Pure functions: parse the two JSON payloads at the boundary, and decide which +// single receipt a click on an internal node should show. No DOM, no fetch — +// so the whole selection policy is unit-testable under `bun test`. + +import { + BRIDGE_INDEX_SCHEMA, EPI_STATUSES, GAPS, PROOF_STATUSES, RECEIPT_SCHEMA, TRANSPORT_MODES, + type BridgeIndex, type EpistemicDomain, type ProofStatus, type ProofTransportReceipt, type ReceiptStub, +} from './types' + +export class BridgeContractError extends Error { + override name = 'BridgeContractError' +} + +// ── boundary parsing (unknown → typed, or throw) ──────────────────────────── + +type Obj = Record +const isObj = (v: unknown): v is Obj => typeof v === 'object' && v !== null && !Array.isArray(v) +const str = (o: Obj, k: string, at: string): string => { + const v = o[k] + if (typeof v !== 'string') throw new BridgeContractError(`${at}.${k}: expected string`) + return v +} +const strArr = (o: Obj, k: string, at: string): string[] => { + const v = o[k] + if (!Array.isArray(v) || !v.every((x) => typeof x === 'string')) { + throw new BridgeContractError(`${at}.${k}: expected string[]`) + } + return v as string[] +} +const oneOf = (allowed: readonly T[], v: unknown, at: string): T => { + if (typeof v === 'string' && (allowed as readonly string[]).includes(v)) return v as T + throw new BridgeContractError(`${at}: ${JSON.stringify(v)} not in {${allowed.join(', ')}}`) +} +const record = (o: Obj, k: string, at: string): Obj => { + const v = o[k] + if (!isObj(v)) throw new BridgeContractError(`${at}.${k}: expected object`) + return v +} + +/** Receipt hrefs must stay relative (the preview/proxy rule, and no exfiltration). */ +function relativeHref(h: string, at: string): string { + if (/^[a-z][a-z0-9+.-]*:/i.test(h) || h.startsWith('//')) { + throw new BridgeContractError(`${at}: href must be relative, got ${h}`) + } + return h +} + +export function parseBridgeIndex(raw: unknown): BridgeIndex { + if (!isObj(raw)) throw new BridgeContractError('index: expected object') + if (raw['schema'] !== BRIDGE_INDEX_SCHEMA) { + throw new BridgeContractError(`index.schema: expected ${BRIDGE_INDEX_SCHEMA}`) + } + const tree = record(raw, 'tree', 'index') + const nodeCount = tree['node_count'] + if (typeof nodeCount !== 'number' || !Number.isInteger(nodeCount) || nodeCount < 0) { + throw new BridgeContractError('index.tree.node_count: expected non-negative integer') + } + + const receipts: Record = {} + for (const [id, r] of Object.entries(record(raw, 'receipts', 'index'))) { + const at = `receipts.${id}` + if (!isObj(r)) throw new BridgeContractError(`${at}: expected object`) + receipts[id] = { + id, + href: relativeHref(str(r, 'href', at), `${at}.href`), + claim: str(r, 'claim', at), + status: oneOf(PROOF_STATUSES, r['status'], `${at}.status`), + artifacts: strArr(r, 'artifacts', at), + } + } + + const domains: Record = {} + for (const [id, d] of Object.entries(record(raw, 'domains', 'index'))) { + const at = `domains.${id}` + if (!isObj(d)) throw new BridgeContractError(`${at}: expected object`) + if (d['kind'] !== 'epistemic_domain') throw new BridgeContractError(`${at}.kind: expected epistemic_domain`) + const receiptIds = strArr(d, 'receipt_ids', at) + for (const rid of receiptIds) { + if (!(rid in receipts)) throw new BridgeContractError(`${at}: dangling receipt ${rid}`) + } + domains[id] = { + kind: 'epistemic_domain', id, + label: str(d, 'label', at), + standpoint: str(d, 'standpoint', at), + epi_status: oneOf(EPI_STATUSES, d['epi_status'], `${at}.epi_status`), + receipt_ids: receiptIds, + } + } + + const nodes: BridgeIndex['nodes'] = {} + for (const [id, n] of Object.entries(record(raw, 'nodes', 'index'))) { + const at = `nodes.${id}` + if (!isObj(n)) throw new BridgeContractError(`${at}: expected object`) + const ds = strArr(n, 'domains', at) + for (const did of ds) { + if (!(did in domains)) throw new BridgeContractError(`${at}: dangling domain ${did}`) + } + nodes[id] = { label: str(n, 'label', at), rank: str(n, 'rank', at), domains: ds } + } + + return { + schema: BRIDGE_INDEX_SCHEMA, + tree: { newick_sha256: str(tree, 'newick_sha256', 'index.tree'), node_count: nodeCount }, + nodes, domains, receipts, + } +} + +export function parseReceipt(raw: unknown, expectedId: string): ProofTransportReceipt { + const at = `receipt(${expectedId})` + if (!isObj(raw)) throw new BridgeContractError(`${at}: expected object`) + if (raw['schema'] !== RECEIPT_SCHEMA) throw new BridgeContractError(`${at}.schema: expected ${RECEIPT_SCHEMA}`) + const id = str(raw, 'id', at) + // A receipt served under the wrong href is the "ReplayedArtifact" negative + // case from epistemic-types, surfaced at the JSON layer. + if (id !== expectedId) throw new BridgeContractError(`${at}: id mismatch (${id})`) + const status = oneOf(PROOF_STATUSES, raw['status'], `${at}.status`) + const agda = record(raw, 'agda', at) + const safe = agda['safe'] + if (typeof safe !== 'boolean') throw new BridgeContractError(`${at}.agda.safe: expected boolean`) + + const out: ProofTransportReceipt = { + schema: RECEIPT_SCHEMA, id, + holder: str(raw, 'holder', at), + artifact: str(raw, 'artifact', at), + claim: str(raw, 'claim', at), + meaning: str(raw, 'meaning', at), + status, + mode: oneOf(TRANSPORT_MODES, raw['mode'], `${at}.mode`), + agda: { + module: str(agda, 'module', `${at}.agda`), + theorem: str(agda, 'theorem', `${at}.agda`), + source: str(agda, 'source', `${at}.agda`), + checked_commit: str(agda, 'checked_commit', `${at}.agda`), + safe, + }, + } + const certified = status === 'Proof' || status === 'ProofUnder' + if (raw['gap'] !== undefined) { + if (certified) throw new BridgeContractError(`${at}: a ${status} cannot carry a gap`) + out.gap = oneOf(GAPS, raw['gap'], `${at}.gap`) + } + // Mirrors opaqueNotCertifying: OpaqueReceipt mode can never be Proof. + if (certified && out.mode === 'OpaqueReceipt') { + throw new BridgeContractError(`${at}: OpaqueReceipt mode cannot be ${status}`) + } + if (status === 'ProofUnder') out.under = strArr(raw, 'under', at) + if (isObj(raw['exacts'])) { + const e = raw['exacts'] + out.exacts = { + summary_ref: str(e, 'summary_ref', `${at}.exacts`), + policy_fingerprint: str(e, 'policy_fingerprint', `${at}.exacts`), + } + } + return out +} + +// ── selection policy ───────────────────────────────────────────────────────── + +/** Higher = shown first. Opinionated, and the only place the ordering lives. */ +const STATUS_RANK: Record = { + Proof: 5, ProofUnder: 4, Receipt: 3, Claimed: 2, Code: 1, Data: 0, +} + +export interface Selection { + nodeId: string + label: string + rank: string + domains: EpistemicDomain[] + /** The single receipt the panel renders, or null (nothing relevant). */ + chosen: ReceiptStub | null + /** How many further relevant receipts exist — shown as a count, not rendered. */ + alternatives: number +} + +/** + * Click → selection, O(domains × receipts-per-domain) with no tree walk. + * Returns null for ids not in the index (leaves, or a stale tree). + * + * Relevance: a receipt whose `artifacts` names this node beats a domain-wide + * one (empty `artifacts`); receipts about OTHER nodes are not relevant at all. + * Ties break on status strength, then id, so the result is deterministic. + */ +export function resolveSelection(index: BridgeIndex, nodeId: string): Selection | null { + const node = index.nodes[nodeId] + if (!node) return null + const domains: EpistemicDomain[] = [] + const seen = new Set() + const scored: { stub: ReceiptStub; specific: boolean }[] = [] + for (const did of node.domains) { + const d = index.domains[did] + if (!d) continue + domains.push(d) + for (const rid of d.receipt_ids) { + if (seen.has(rid)) continue + seen.add(rid) + const stub = index.receipts[rid] + if (!stub) continue + const specific = stub.artifacts.includes(nodeId) + if (specific || stub.artifacts.length === 0) scored.push({ stub, specific }) + } + } + scored.sort((a, b) => + Number(b.specific) - Number(a.specific) || + STATUS_RANK[b.stub.status] - STATUS_RANK[a.stub.status] || + (a.stub.id < b.stub.id ? -1 : a.stub.id > b.stub.id ? 1 : 0)) + return { + nodeId, label: node.label, rank: node.rank, domains, + chosen: scored[0]?.stub ?? null, + alternatives: Math.max(0, scored.length - 1), + } +} diff --git a/frontend/src/type-theory/dendrogram-receipts/controller.ts b/frontend/src/type-theory/dendrogram-receipts/controller.ts new file mode 100644 index 0000000..d212bff --- /dev/null +++ b/frontend/src/type-theory/dendrogram-receipts/controller.ts @@ -0,0 +1,144 @@ +// SPDX-License-Identifier: AGPL-3.0-only +// SPDX-FileCopyrightText: 2026 Joshua Benjamin Jewell; 2026 Jonathan D.A. Jewell (hyperpolymath) +// +// Click → bridge index → one receipt → panel, without choking the DOM. +// +// The five rules that keep it cheap (see DESIGN.md §"Not choking the DOM"): +// 1. ONE delegated listener on the tree root, never one per node. +// 2. The click handler does no layout reads and no fetch-waiting: it resolves +// the selection synchronously from the in-memory index (O(1) lookup). +// 3. Every new selection aborts the previous fetch; a generation counter +// discards any response that still races in. +// 4. Full receipts are fetched lazily and kept in a small LRU. +// 5. The panel is written at most once per animation frame, as a single +// replaceChildren() of a detached fragment built with textContent only. + +import { parseReceipt, resolveSelection, type Selection } from './bridgeIndex' +import type { BridgeIndex, DendrogramHost, ProofTransportReceipt } from './types' +import { renderPanel } from './renderPanel' + +export type PanelState = + | { kind: 'idle' } + | { kind: 'loading'; selection: Selection } + | { kind: 'empty'; selection: Selection } + | { kind: 'ready'; selection: Selection; receipt: ProofTransportReceipt } + | { kind: 'error'; selection: Selection; message: string } + +export class Lru { + private readonly m = new Map() + constructor(private readonly cap: number) {} + get(k: K): V | undefined { + const v = this.m.get(k) + if (v !== undefined) { this.m.delete(k); this.m.set(k, v) } + return v + } + set(k: K, v: V): void { + this.m.delete(k) + this.m.set(k, v) + if (this.m.size > this.cap) this.m.delete(this.m.keys().next().value as K) + } + get size(): number { return this.m.size } +} + +export interface ControllerDeps { + index: BridgeIndex + fetchJson: DendrogramHost['fetchJson'] + /** Receives every state; the DOM sink coalesces, tests just record. */ + onState: (s: PanelState) => void + cacheSize?: number +} + +/** DOM-free state machine. `select` is safe to call at pointer-event rate. */ +export function createReceiptController(deps: ControllerDeps) { + const cache = new Lru(deps.cacheSize ?? 32) + let generation = 0 + let inflight: AbortController | null = null + let current: string | null = null + + async function select(nodeId: string): Promise { + if (nodeId === current) return // re-click on the same node: no work + const selection = resolveSelection(deps.index, nodeId) + if (!selection) return // leaf / unknown id: keep the current panel + current = nodeId + const gen = ++generation + inflight?.abort() + inflight = null + + const stub = selection.chosen + if (!stub) { deps.onState({ kind: 'empty', selection }); return } + const hit = cache.get(stub.id) + if (hit) { deps.onState({ kind: 'ready', selection, receipt: hit }); return } + + deps.onState({ kind: 'loading', selection }) + const ac = new AbortController() + inflight = ac + try { + const receipt = parseReceipt(await deps.fetchJson(stub.href, ac.signal), stub.id) + cache.set(stub.id, receipt) // cache even if stale: the next click may want it + if (gen !== generation) return + deps.onState({ kind: 'ready', selection, receipt }) + } catch (e) { + if (gen !== generation || ac.signal.aborted) return + deps.onState({ kind: 'error', selection, message: e instanceof Error ? e.message : String(e) }) + } finally { + if (inflight === ac) inflight = null + } + } + + function dispose(): void { + generation++ + inflight?.abort() + inflight = null + } + + return { select, dispose, get cacheSize() { return cache.size } } +} + +/** + * Wire the controller to a real DOM. The renderer must mark internal nodes as + * … + * (Protoctist's NHX `ND=` id is the natural source of data-node-id.) + * Returns a disposer; call it when the tree is re-rendered or unmounted. + */ +export function attachDendrogram(host: DendrogramHost, index: BridgeIndex): () => void { + let pending: PanelState | null = null + let frame = 0 + let selected: Element | null = null + const flush = () => { + frame = 0 + if (pending) { host.panel.replaceChildren(renderPanel(pending, host.panel.ownerDocument)); pending = null } + } + const ctl = createReceiptController({ + index, + fetchJson: host.fetchJson, + onState: (s) => { pending = s; if (!frame) frame = requestAnimationFrame(flush) }, + }) + + const nodeFrom = (t: EventTarget | null): Element | null => + t instanceof Element ? t.closest('[data-node-kind="internal"][data-node-id]') : null + + const activate = (el: Element) => { + // Selection highlight is one attribute flip on two elements, not a re-render. + selected?.removeAttribute('aria-selected') + el.setAttribute('aria-selected', 'true') + selected = el + void ctl.select(el.getAttribute('data-node-id') ?? '') + } + const onClick = (ev: Event) => { const el = nodeFrom(ev.target); if (el) activate(el) } + const onKey = (ev: Event) => { + const k = (ev as KeyboardEvent).key + if (k !== 'Enter' && k !== ' ') return + const el = nodeFrom(ev.target) + if (el) { ev.preventDefault(); activate(el) } + } + + host.panel.setAttribute('aria-live', 'polite') + host.treeRoot.addEventListener('click', onClick) + host.treeRoot.addEventListener('keydown', onKey) + return () => { + host.treeRoot.removeEventListener('click', onClick) + host.treeRoot.removeEventListener('keydown', onKey) + if (frame) cancelAnimationFrame(frame) + ctl.dispose() + } +} diff --git a/frontend/src/type-theory/dendrogram-receipts/index.ts b/frontend/src/type-theory/dendrogram-receipts/index.ts new file mode 100644 index 0000000..eb2f76d --- /dev/null +++ b/frontend/src/type-theory/dendrogram-receipts/index.ts @@ -0,0 +1,7 @@ +// SPDX-License-Identifier: AGPL-3.0-only +// SPDX-FileCopyrightText: 2026 Joshua Benjamin Jewell; 2026 Jonathan D.A. Jewell (hyperpolymath) +// Public surface of the exploratory dendrogram-receipts extension. +export * from './types' +export { parseBridgeIndex, parseReceipt, resolveSelection, BridgeContractError, type Selection } from './bridgeIndex' +export { attachDendrogram, createReceiptController, type PanelState } from './controller' +export { renderPanel } from './renderPanel' diff --git a/frontend/src/type-theory/dendrogram-receipts/renderPanel.ts b/frontend/src/type-theory/dendrogram-receipts/renderPanel.ts new file mode 100644 index 0000000..94c9fb2 --- /dev/null +++ b/frontend/src/type-theory/dendrogram-receipts/renderPanel.ts @@ -0,0 +1,56 @@ +// SPDX-License-Identifier: AGPL-3.0-only +// SPDX-FileCopyrightText: 2026 Joshua Benjamin Jewell; 2026 Jonathan D.A. Jewell (hyperpolymath) +// +// Builds the right-hand panel as a detached DocumentFragment. textContent only +// — receipt strings come from JSON and are never parsed as HTML. + +import type { PanelState } from './controller' + +export function renderPanel(s: PanelState, doc: Document): DocumentFragment { + const frag = doc.createDocumentFragment() + const el = (tag: K, text?: string, cls?: string) => { + const e = doc.createElement(tag) + if (text !== undefined) e.textContent = text + if (cls) e.className = cls + return e + } + if (s.kind === 'idle') { frag.append(el('p', 'Select an internal node.', 'pt-hint')); return frag } + + const { selection } = s + frag.append(el('h3', `${selection.label} (${selection.rank})`)) + const domains = el('ul', undefined, 'pt-domains') + for (const d of selection.domains) { + const li = el('li', `${d.label} — ${d.epi_status} @ ${d.standpoint}`) + li.dataset['epi'] = d.epi_status + domains.append(li) + } + frag.append(domains) + + switch (s.kind) { + case 'loading': frag.append(el('p', `Loading ${selection.chosen?.claim ?? ''}…`, 'pt-hint')); break + case 'empty': frag.append(el('p', 'No ProofTransport receipt is relevant to this clade.', 'pt-hint')); break + case 'error': frag.append(el('p', `Receipt unavailable: ${s.message}`, 'pt-error')); break + case 'ready': { + const r = s.receipt + const card = el('article', undefined, 'pt-receipt') + card.dataset['status'] = r.status + const dl = el('dl') + const row = (k: string, v: string) => dl.append(el('dt', k), el('dd', v)) + row('Status', r.gap ? `${r.status} (${r.gap})` : r.status) + row('Claim', r.claim) + row('Meaning', r.meaning) + row('Holder → artefact', `${r.holder} → ${r.artifact}`) + row('Mode', r.mode) + if (r.under?.length) row('Under', r.under.join('; ')) + row('Agda', `${r.agda.module}.${r.agda.theorem}${r.agda.safe ? ' (--safe)' : ''}`) + row('Checked at', r.agda.checked_commit.slice(0, 12)) + if (r.exacts) row('Exacts', `${r.exacts.summary_ref} [${r.exacts.policy_fingerprint.slice(0, 12)}]`) + card.append(dl, el('p', 'Displayed, not re-verified in the browser.', 'pt-hint')) + frag.append(card) + if (selection.alternatives > 0) { + frag.append(el('p', `${selection.alternatives} further relevant receipt(s) not shown.`, 'pt-hint')) + } + } + } + return frag +} diff --git a/frontend/src/type-theory/dendrogram-receipts/types.ts b/frontend/src/type-theory/dendrogram-receipts/types.ts new file mode 100644 index 0000000..b414e05 --- /dev/null +++ b/frontend/src/type-theory/dendrogram-receipts/types.ts @@ -0,0 +1,131 @@ +// SPDX-License-Identifier: AGPL-3.0-only +// SPDX-FileCopyrightText: 2026 Joshua Benjamin Jewell; 2026 Jonathan D.A. Jewell (hyperpolymath) +// +// Minimal wire contract for the ITOL-style dendrogram → ProofTransport receipt +// panel. EXPLORATORY: lives in the type-theory work section, not wired into the +// app routes. Design notes: type-theory/dendrogram-receipts/DESIGN.md. +// +// Three payloads, fetched at three different times: +// +// 1. BridgeIndex — loaded ONCE with the tree. Small. Everything a click +// needs to decide *which* receipt to show, O(1). +// 2. ReceiptStub — inside the index. Enough to rank and label. +// 3. ProofTransportReceipt — fetched LAZILY, one per click, cached. +// +// Nothing here verifies anything. A `status: "Proof"` is a report that the Agda +// check named in `agda` succeeded at `agda.checked_commit`; the browser displays +// that report, it does not re-establish it (epistemic-types §scope: +// "runtime integration" is explicitly not established). + +/** Mirrors `[statuses]` in epistemic-types/.machine_readable/proof-transport/ProofTransport.a2ml. */ +export const PROOF_STATUSES = ['Data', 'Code', 'Claimed', 'Receipt', 'Proof', 'ProofUnder'] as const +export type ProofStatus = (typeof PROOF_STATUSES)[number] + +/** Mirrors `[modes]`. */ +export const TRANSPORT_MODES = ['Public', 'Designated', 'IssuerMediated', 'EnvironmentMediated', 'OpaqueReceipt'] as const +export type TransportMode = (typeof TRANSPORT_MODES)[number] + +/** Mirrors `[gaps]`. Only the `realized` subset is produced by the Agda verifier today. */ +export const GAPS = [ + 'TrivialGap', 'DesignatedGap', 'EnvironmentGap', 'IssuerTrustGap', 'OpaqueGap', + 'MissingChecker', 'MissingEvidence', 'MissingContext', 'InvalidEvidence', +] as const +export type Gap = (typeof GAPS)[number] + +/** + * The epi_status ladder shared by EpistemicTypes.jl / src/core/epistemic.jl / + * Evidence/Warrant.agda (:SansFibre → :Belief → :Warranted → :Factive). + */ +export const EPI_STATUSES = ['SansFibre', 'Belief', 'Warranted', 'Factive'] as const +export type EpiStatus = (typeof EPI_STATUSES)[number] + +// ── 1. Bridge index (one JSON document per rendered tree) ──────────────────── + +export const BRIDGE_INDEX_SCHEMA = 'metamanifold.bridge-index/v1' as const + +export interface BridgeIndex { + schema: typeof BRIDGE_INDEX_SCHEMA + /** Binds the index to one tree. A click on a tree whose hash differs is refused. */ + tree: { newick_sha256: string; node_count: number } + /** + * Internal tree node id → epistemic_domain ids already ROLLED UP over the + * clade (Protoctist.rollup_counts does the post-order pass server-side), so + * a click never walks descendants in the browser. Leaves may be omitted. + * Ids are the NHX `ND=` tag written by Protoctist.annotate_newick. + */ + nodes: Record + domains: Record + receipts: Record +} + +export interface BridgeNode { + /** Taxonomic label, e.g. "Apicomplexa" — the ProofTransport `Artifact`. */ + label: string + rank: string + domains: string[] +} + +export interface EpistemicDomain { + kind: 'epistemic_domain' + id: string + /** Human label, e.g. "exact-descriptive-summaries". */ + label: string + /** Standpoint κ (the holder / Agent the claims are indexed by). */ + standpoint: string + epi_status: EpiStatus + receipt_ids: string[] +} + +export interface ReceiptStub { + id: string + /** Relative URL of the full ProofTransportReceipt JSON. Never absolute. */ + href: string + claim: string + status: ProofStatus + /** Tree node ids this receipt's `artifact` is about. Empty = domain-wide. */ + artifacts: string[] +} + +// ── 3. Full receipt (fetched per click) ────────────────────────────────────── + +export const RECEIPT_SCHEMA = 'metamanifold.proof-transport-receipt/v1' as const + +export interface ProofTransportReceipt { + schema: typeof RECEIPT_SCHEMA + id: string + holder: string + artifact: string + claim: string + /** Human rendering of `Meaning holder artifact claim` — the proposition, not the label. */ + meaning: string + status: ProofStatus + mode: TransportMode + /** Present iff verification did not yield Proof/ProofUnder. */ + gap?: Gap + /** For ProofUnder: the named assumptions the proof is relative to. */ + under?: string[] + agda: { + module: string + theorem: string + source: string + checked_commit: string + safe: boolean + } + /** Optional link back to the exact numbers (ExactSummaries) the claim is about. */ + exacts?: { summary_ref: string; policy_fingerprint: string } +} + +// ── Host contract ──────────────────────────────────────────────────────────── + +/** + * The only three things the extension needs from its host (the JEG shell, or + * this repo's React app). Kept deliberately tiny so the extension is testable + * without a browser and portable across hosts. + */ +export interface DendrogramHost { + /** The element that contains the rendered tree (an or
). */ + treeRoot: Element + /** The right-hand panel. The controller owns its children exclusively. */ + panel: Element + fetchJson: (href: string, signal: AbortSignal) => Promise +} diff --git a/frontend/tests/unit/type-theory-dendrogram-receipts.test.ts b/frontend/tests/unit/type-theory-dendrogram-receipts.test.ts new file mode 100644 index 0000000..b3b8279 --- /dev/null +++ b/frontend/tests/unit/type-theory-dendrogram-receipts.test.ts @@ -0,0 +1,98 @@ +// SPDX-License-Identifier: AGPL-3.0-only +// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell +// type-theory section: dendrogram → bridge index → ProofTransport receipt. +// DOM-free: exercises the parser, the selection policy and the controller's +// abort / stale-response / cache behaviour against the checked-in examples. +import { test, expect } from 'bun:test' +import { readFileSync } from 'node:fs' +import { join } from 'node:path' +import { + BridgeContractError, parseBridgeIndex, parseReceipt, resolveSelection, +} from '../../src/type-theory/dendrogram-receipts/bridgeIndex' +import { createReceiptController, Lru, type PanelState } from '../../src/type-theory/dendrogram-receipts/controller' + +const EX = join(import.meta.dir, '../../../type-theory/dendrogram-receipts/examples') +const load = (p: string): unknown => JSON.parse(readFileSync(join(EX, p), 'utf8')) +const index = parseBridgeIndex(load('bridge-index.example.json')) + +test('every example receipt parses under its own id', () => { + for (const [id, stub] of Object.entries(index.receipts)) { + expect(parseReceipt(load(stub.href), id).id).toBe(id) + } +}) + +test('node-specific receipt beats a stronger-looking domain-wide one', () => { + const s = resolveSelection(index, 'n2')! + expect(s.domains.map((d) => d.id)).toEqual(['exacts']) + expect(s.chosen?.id).toBe('r-checked-sum-n2') + expect(s.alternatives).toBe(1) +}) + +test('without a specific receipt, status strength decides; other nodes\' receipts are excluded', () => { + const s = resolveSelection(index, 'n1')! + expect(s.chosen?.id).toBe('r-checked-sum-any') // ProofUnder > Receipt; n2-specific excluded + expect(s.alternatives).toBe(1) +}) + +test('leaves / unknown ids resolve to null (click is a no-op)', () => { + expect(resolveSelection(index, 'leaf-17')).toBeNull() +}) + +test('contract rejections', () => { + const bad = load('bridge-index.example.json') as { receipts: Record } + bad.receipts['r-checked-sum-n2']!.href = 'https://evil.example/r.json' + expect(() => parseBridgeIndex(bad)).toThrow(BridgeContractError) + + const r = load('receipts/r-epi-not-factive.json') as Record + expect(() => parseReceipt(r, 'someone-else')).toThrow(/id mismatch/) + expect(() => parseReceipt({ ...r, status: 'Proof' }, 'r-epi-not-factive')).toThrow(/gap/) + const { gap: _gap, ...noGap } = r + expect(() => parseReceipt({ ...noGap, status: 'Proof' }, 'r-epi-not-factive')).toThrow(/OpaqueReceipt/) +}) + +test('LRU evicts least-recently-used', () => { + const l = new Lru(2) + l.set('a', 1); l.set('b', 2); l.get('a'); l.set('c', 3) + expect(l.get('b')).toBeUndefined() + expect(l.get('a')).toBe(1) +}) + +test('controller: rapid clicks abort the old fetch and never render a stale receipt', async () => { + const states: PanelState[] = [] + const aborted: string[] = [] + const gates = new Map void>() + const ctl = createReceiptController({ + index, + onState: (s) => states.push(s), + fetchJson: (href, signal) => new Promise((res) => { + signal.addEventListener('abort', () => aborted.push(href)) + gates.set(href, () => res(load(href))) + }), + }) + const p1 = ctl.select('n2') + const p2 = ctl.select('n1') + gates.get('receipts/r-checked-sum-n2.json')!() // late response for the first click + gates.get('receipts/r-checked-sum-any.json')!() + await Promise.all([p1, p2]) + + expect(aborted).toEqual(['receipts/r-checked-sum-n2.json']) + const ready = states.filter((s) => s.kind === 'ready') + expect(ready.length).toBe(1) + expect(ready[0]!.kind === 'ready' && ready[0]!.receipt.id).toBe('r-checked-sum-any') + expect(ctl.cacheSize).toBe(2) // the stale one is still cached for next time + + // Returning to n2 is served from cache: no loading state, no fetch. + const before = states.length + await ctl.select('n2') + expect(states.slice(before).map((s) => s.kind)).toEqual(['ready']) +}) + +test('controller: re-clicking the same node does nothing', async () => { + let fetches = 0 + const ctl = createReceiptController({ + index, onState: () => {}, + fetchJson: async (href) => { fetches++; return load(href) }, + }) + await ctl.select('n2'); await ctl.select('n2') + expect(fetches).toBe(1) +}) diff --git a/type-theory/README.md b/type-theory/README.md new file mode 100644 index 0000000..1a09d00 --- /dev/null +++ b/type-theory/README.md @@ -0,0 +1,27 @@ + + + +# Type-theory work section (exploratory) + +A space for trying out ideas where the estate's type-theory work (echo-types, +epistemic-types, `proofs/agda/`) meets the MetaManifold UI. **Nothing here +is wired into the app routes, the server, or the release.** When something here +is ready, it moves into `src/`, `frontend/src/views/` or `proofs/` through a +normal PR. Until then, treat it as an example of what this work could be used +for, not a promise. + +Layout: + +| Path | What | +|---|---| +| `type-theory//DESIGN.md` | The argument, the contract, open questions | +| `type-theory//examples/` | JSON fixtures, used by the tests | +| `frontend/src/type-theory//` | TypeScript (checked by the normal `tsc` gate) | +| `frontend/tests/unit/type-theory-*.test.ts` | `bun test` coverage | + +Topics: + +- [`dendrogram-receipts/`](dendrogram-receipts/DESIGN.md): clicking an internal + node of an ITOL-style dendrogram looks up the bridge index, gets the + `epistemic_domain`s for that clade, and shows one Agda `ProofTransport` + receipt in the right-hand panel. diff --git a/type-theory/dendrogram-receipts/DESIGN.md b/type-theory/dendrogram-receipts/DESIGN.md new file mode 100644 index 0000000..b14401c --- /dev/null +++ b/type-theory/dendrogram-receipts/DESIGN.md @@ -0,0 +1,141 @@ + + + +# Dendrogram → bridge index → ProofTransport receipt + +Status: **exploratory**. The TypeScript and tests are real and pass. The Julia +producer (`export_bridge_index`) is only a proposal (§5). + +## 1. The question + +> When someone clicks an internal node in the ITOL-style dendrogram, look up +> the bridge index, get the `epistemic_domain` nodes, and show only the +> relevant Agda `ProofTransport` receipt in the right-hand panel, without +> choking the DOM. + +## 2. What already exists (so we don't invent it twice) + +| Piece | Where | What it gives us | +|---|---|---| +| Taxonomy tree, cumulative rollup, NHX Newick, iTOL bundle | `Protoctist.jl` `src/tree.jl`, `src/io.jl` (`build_taxonomy_tree`, `rollup_counts`, `annotate_newick`, `export_itol_bundle`) | Node ids and a linear post-order rollup, so domain membership can be computed server-side ahead of time | +| Receipts, `epi_status` ladder, standpoints | `EpistemicTypes.jl` (`make_receipt`, `verify_receipt`, `epi_status`) and this repo's `src/core/epistemic.jl` | The `EpiStatus` values and the standpoint (κ) | +| Proof-transport vocabulary | `epistemic-types/.machine_readable/proof-transport/ProofTransport.a2ml` | `statuses`, `modes`, `gaps`, the `Meaning`/`Payload` split | +| Echo fibres | `echo-types`, `EchoTypes.jl`, `proofs/agda/MetaManifold/Evidence/Echo.agda` | Why a clade's rows can be stored as (observed, witnesses) pairs | +| Exact numbers | `src/analysis/exact_summaries.jl`, `proofs/agda/MetaManifold/ExactCounts.agda` | The claims the example receipts are about (`checkedSumOf-is-exact`, …) | +| Clade tree in the UI | `src/analysis/clade_cumulus.jl`, `frontend/src/components/CladeCumulus.tsx` | The node shape the tree view will actually render | + +I searched every repo listed above for **`epistemic_domain`**, **"bridge index"** and **JEG**. +None of them appear. This design therefore **defines** the first two (§3). It +treats JEG only as "the host shell", reached through the three-member +`DendrogramHost` interface. If JEG already has its own extension API, only +that adapter has to change. + +## 3. The contract (minimal JSON) + +There are two documents, fetched at different times. + +**Bridge index** (`metamanifold.bridge-index/v1`): one per rendered tree, +loaded with the tree. It is flat maps only, so a click is a hash lookup: + +```jsonc +{ + "schema": "metamanifold.bridge-index/v1", + "tree": { "newick_sha256": "…", "node_count": 7 }, + "nodes": { "n2": { "label": "Apicomplexa", "rank": "Class", "domains": ["exacts"] } }, + "domains": { "exacts": { "kind": "epistemic_domain", "id": "exacts", "label": "…", + "standpoint": "…", "epi_status": "Factive", + "receipt_ids": ["r-checked-sum-n2", "r-checked-sum-any"] } }, + "receipts": { "r-checked-sum-n2": { "href": "receipts/r-checked-sum-n2.json", + "claim": "CladeTotalIsExact", "status": "Proof", + "artifacts": ["n2"] } } +} +``` + +- `nodes[id].domains` has **already been rolled up over the clade**. The + browser never walks descendants. +- Node ids are the NHX `ND=` tags from `annotate_newick`, emitted as + `data-node-id`. +- `href` must be relative. The parser rejects absolute URLs, which keeps the + preview-proxy rule and blocks exfiltration. + +**Receipt** (`metamanifold.proof-transport-receipt/v1`): one per receipt, +fetched lazily. It carries `holder`, `artifact`, `claim`, `meaning` (the +proposition itself, not just its label), `status`, `mode`, an optional `gap`, +`under` for `ProofUnder`, the `agda` coordinates (module, theorem, source, +`checked_commit`, `safe`), and an optional `exacts` back-link. Full types +are in `frontend/src/type-theory/dendrogram-receipts/types.ts`. Working +examples are in `examples/`. + +The parser enforces the a2ml invariants that can be checked at the JSON level: + +- A `Proof`/`ProofUnder` cannot carry a gap. +- `OpaqueReceipt` can never be `Proof` (`opaqueNotCertifying`). +- A receipt's `id` must match the href it was requested under. This is the + `ReplayedArtifact` negative case at the wire layer. + +These checks are **not** verification. The panel says so on every card. + +## 4. Choosing "the relevant receipt" + +This lives in `resolveSelection`, the only place the policy is defined: + +1. Collect receipts from every domain on the clicked node, with duplicates + removed. +2. A receipt is relevant if its `artifacts` names this node, or if it is + domain-wide (`artifacts: []`). Receipts about *other* nodes are dropped. +3. Sort: node-specific first, then by status strength + (`Proof > ProofUnder > Receipt > Claimed > Code > Data`), then by id. +4. Render the first one. For the rest, show only a count. + +## 5. Not choking the DOM + +`controller.ts` follows five rules: + +1. **One delegated listener** (`click` and `keydown`) on the tree root, found + through `closest('[data-node-kind="internal"][data-node-id]')`. There are + no per-node listeners, so 10k nodes cost the same as 10. +2. **The click handler resolves synchronously** from the in-memory index. It + does no layout reads and no await before choosing. +3. **Each new selection aborts the previous fetch** (`AbortController`), and a + generation counter drops any response that still arrives. A late response + is still cached, because the user often clicks back. +4. **LRU of full receipts** (default 32). Re-clicking the same node does + nothing. +5. **At most one panel write per animation frame.** The write is a single + `replaceChildren()` of a detached fragment built with `textContent` only, + so receipt strings are never parsed as HTML. Moving the selection + highlight flips one attribute on two elements. + +The controller logic (`createReceiptController`) has no DOM dependency, so +`bun test` covers aborts, stale responses and the cache without a browser. + +## 6. Julia producer (proposal: Protoctist.jl is the natural home) + +Protoctist.jl already builds the tree, does the post-order rollup and writes +the iTOL bundle. The smallest addition would be a function next to +`export_itol_bundle`: + +```julia +export_bridge_index(run::ProtistRun, domains, receipts, outdir) -> String +# nodes[ND] ← union of domain ids over the clade, in the same post-order +# pass as rollup_counts (linear, not quadratic) +# domains ← EpistemicTypes standpoint + epi_status per domain +# receipts ← stubs; the full receipt JSON is written from the Agda build +# (checked_commit = the commit `just check` passed on) +``` + +EchoTypes.jl stays test-only, as Protoctist's own design says. It is where a +property test belongs: "every receipt whose artifacts names node *v* is in +the index under *v* or one of *v*'s ancestors". + +## 7. Open questions + +- **JEG**: what is its extension API? Replace `DendrogramHost` with an + adapter to it. +- **`epistemic_domain`**: is it meant to be a domain of *claims* (as modelled + here: exacts, warrant, …) or a taxonomic domain? The shape works for both. + Only the labels change. +- Should multiple receipts be viewable (a pager), or is "one plus a count" + the right default? +- Where does the receipt JSON come from in CI: generated from Agda + `--safe` output in `proofs.yml`, or hand-curated per release? diff --git a/type-theory/dendrogram-receipts/examples/bridge-index.example.json b/type-theory/dendrogram-receipts/examples/bridge-index.example.json new file mode 100644 index 0000000..c261c74 --- /dev/null +++ b/type-theory/dendrogram-receipts/examples/bridge-index.example.json @@ -0,0 +1,25 @@ +{ + "schema": "metamanifold.bridge-index/v1", + "tree": { "newick_sha256": "EXAMPLE-not-a-real-hash", "node_count": 7 }, + "nodes": { + "n0": { "label": "Eukaryota", "rank": "Domain", "domains": ["exacts", "warrant"] }, + "n1": { "label": "Alveolata", "rank": "Phylum", "domains": ["exacts", "warrant"] }, + "n2": { "label": "Apicomplexa", "rank": "Class", "domains": ["exacts"] } + }, + "domains": { + "exacts": { "kind": "epistemic_domain", "id": "exacts", "label": "exact-descriptive-summaries", + "standpoint": "MetaManifold.ExactSummaries", "epi_status": "Factive", + "receipt_ids": ["r-checked-sum-n2", "r-checked-sum-any"] }, + "warrant": { "kind": "epistemic_domain", "id": "warrant", "label": "warrant-without-soundness", + "standpoint": "reviewer", "epi_status": "Warranted", + "receipt_ids": ["r-epi-not-factive"] } + }, + "receipts": { + "r-checked-sum-n2": { "href": "receipts/r-checked-sum-n2.json", "claim": "CladeTotalIsExact", + "status": "Proof", "artifacts": ["n2"] }, + "r-checked-sum-any": { "href": "receipts/r-checked-sum-any.json", "claim": "CheckedSumNeverRounds", + "status": "ProofUnder", "artifacts": [] }, + "r-epi-not-factive": { "href": "receipts/r-epi-not-factive.json", "claim": "WarrantIsNotTruth", + "status": "Receipt", "artifacts": [] } + } +} diff --git a/type-theory/dendrogram-receipts/examples/receipts/r-checked-sum-any.json b/type-theory/dendrogram-receipts/examples/receipts/r-checked-sum-any.json new file mode 100644 index 0000000..e092ab9 --- /dev/null +++ b/type-theory/dendrogram-receipts/examples/receipts/r-checked-sum-any.json @@ -0,0 +1,13 @@ +{ + "schema": "metamanifold.proof-transport-receipt/v1", + "id": "r-checked-sum-any", + "holder": "MetaManifold.ExactSummaries", + "artifact": "any clade", + "claim": "CheckedSumNeverRounds", + "meaning": "checkedAdd refuses exactly when the true sum does not fit the bound.", + "status": "ProofUnder", + "under": ["Julia BigInt addition agrees with Agda ℤ addition (not proved; see proofs/residue/exact-counts.residue)"], + "mode": "Public", + "agda": { "module": "MetaManifold.ExactCounts", "theorem": "checkedAdd-refuses-exactly-when-it-must", + "source": "proofs/agda/MetaManifold/ExactCounts.agda", "checked_commit": "e6726fa765aebf9289b114cefe9cd270a439403c", "safe": true } +} diff --git a/type-theory/dendrogram-receipts/examples/receipts/r-checked-sum-n2.json b/type-theory/dendrogram-receipts/examples/receipts/r-checked-sum-n2.json new file mode 100644 index 0000000..66903a7 --- /dev/null +++ b/type-theory/dendrogram-receipts/examples/receipts/r-checked-sum-n2.json @@ -0,0 +1,13 @@ +{ + "schema": "metamanifold.proof-transport-receipt/v1", + "id": "r-checked-sum-n2", + "holder": "MetaManifold.ExactSummaries", + "artifact": "Apicomplexa (n2): cumulative count over clade", + "claim": "CladeTotalIsExact", + "meaning": "The clade total is the exact integer sum of its member counts, or the sum is refused; it is never silently rounded.", + "status": "Proof", + "mode": "Public", + "agda": { "module": "MetaManifold.ExactCounts", "theorem": "checkedSumOf-is-exact", + "source": "proofs/agda/MetaManifold/ExactCounts.agda", "checked_commit": "e6726fa765aebf9289b114cefe9cd270a439403c", "safe": true }, + "exacts": { "summary_ref": "exact_summary/group/Apicomplexa", "policy_fingerprint": "EXAMPLE-fingerprint" } +} diff --git a/type-theory/dendrogram-receipts/examples/receipts/r-epi-not-factive.json b/type-theory/dendrogram-receipts/examples/receipts/r-epi-not-factive.json new file mode 100644 index 0000000..23df19d --- /dev/null +++ b/type-theory/dendrogram-receipts/examples/receipts/r-epi-not-factive.json @@ -0,0 +1,13 @@ +{ + "schema": "metamanifold.proof-transport-receipt/v1", + "id": "r-epi-not-factive", + "holder": "reviewer", + "artifact": "any warranted assignment", + "claim": "WarrantIsNotTruth", + "meaning": "Holding a warrant token for a taxon assignment does not by itself entail the assignment.", + "status": "Receipt", + "mode": "OpaqueReceipt", + "gap": "OpaqueGap", + "agda": { "module": "MetaManifold.Evidence.Warrant", "theorem": "epi-does-not-give", + "source": "proofs/agda/MetaManifold/Evidence/Warrant.agda", "checked_commit": "e6726fa765aebf9289b114cefe9cd270a439403c", "safe": true } +}