From dad489d65427e4d04f0932d7318afb20746a0311 Mon Sep 17 00:00:00 2001 From: James Dabbs Date: Thu, 2 Jul 2026 17:17:34 -0700 Subject: [PATCH 1/3] feat(core): add derived-data artifact schemas and serialization Define the versioned artifact set (manifest, slim core, per-space derived shards, text) that compile will publish so consumers can load precomputed deductions instead of re-running the prover. Serialization is canonical - prover inputs and all output collections are sorted - so the same logical input yields byte-identical artifacts, which diffs and sha-keyed caching will rely on. See doc/artifacts.md for the format contract. --- doc/artifacts.md | 53 ++++++ packages/core/src/Artifacts.ts | 231 +++++++++++++++++++++++++++ packages/core/src/Logic/index.ts | 2 +- packages/core/src/index.ts | 3 + packages/core/test/Artifacts.test.ts | 153 ++++++++++++++++++ 5 files changed, 441 insertions(+), 1 deletion(-) create mode 100644 doc/artifacts.md create mode 100644 packages/core/src/Artifacts.ts create mode 100644 packages/core/test/Artifacts.test.ts diff --git a/doc/artifacts.md b/doc/artifacts.md new file mode 100644 index 00000000..1814f52f --- /dev/null +++ b/doc/artifacts.md @@ -0,0 +1,53 @@ +# Derived-data artifacts + +The compiler publishes a bundle's data as a versioned set of artifacts, so +that consumers (notably the viewer) can load precomputed deductions instead of +re-running the prover, and can load only the slices of data a page actually +needs. Schemas and serialization live in `packages/core/src/Artifacts.ts`. + +The legacy monolithic `bundle.json` continues to be published alongside these +artifacts and remains the stable public data API. Consumers without artifact +support (or reading a bundle predating them) fall back to it and derive traits +client-side. + +## Artifact set + +| Path | Contents | +| ------------------ | ------------------------------------------------------------ | +| `manifest.json` | Format version, data version (`ref`/`sha`), artifact paths | +| `core.json` | Deduction-minimal data: uids, names, aliases, theorem formulas, asserted trait values | +| `spaces/{id}.json` | Traits derivable for one space, with proofs | +| `text.json` | Descriptions and refs for all entities and asserted traits | + +Paths are relative to the manifest's location and are declared in the +manifest, so consumers should discover them from `manifest.json` rather than +hard-coding. `paths.spaces` is a template in which `{id}` stands for a space's +uid. + +Rationale for the split: descriptions and refs are ~85% of bundle bytes but +are only read on detail pages, while `core.json` alone supports lists, search, +and full client-side deduction. Derived traits with proofs are far too large +to ship whole (~8 MB raw) but shard to tens of KB per space. + +## Format versioning + +`manifest.json` carries a `format` number (`artifacts.FORMAT`). It is bumped +whenever the serialized shape of any artifact changes incompatibly; consumers +should check it before assuming they can read the other paths, and fall back +to `bundle.json` when it is unrecognized. + +## Determinism + +Serialization is canonical: the same logical input produces byte-identical +artifacts, regardless of source file enumeration order. Artifact diffs and +sha-keyed caching rely on this, and `test/Artifacts.test.ts` enforces it. + +Two mechanisms provide it: + +1. **Pinned prover inputs.** Proof content depends on the order theorems and + traits are fed to the prover, so `artifacts.implications` and + `artifacts.deduceSpace` sort both by uid. Derived artifacts must be + produced through these entry points. +2. **Canonical serialization.** Every collection in every artifact is sorted + (entities by uid, traits by space then property) and object keys are + emitted in schema order. diff --git a/packages/core/src/Artifacts.ts b/packages/core/src/Artifacts.ts new file mode 100644 index 00000000..3744e88a --- /dev/null +++ b/packages/core/src/Artifacts.ts @@ -0,0 +1,231 @@ +import { z } from 'zod' +import { Bundle, Version } from './Bundle.js' +import { formulaSchema } from './Formula.js' +import { Id } from './Id.js' +import { Derivations, ImplicationIndex, deduceTraits } from './Logic/index.js' +import { Result } from './Logic/Prover.js' +import { refSchema } from './Ref.js' +import { proofSchema } from './Trait.js' + +// The derived-data artifact set is the precomputed representation of a bundle +// that `compile` publishes and consumers (notably the viewer) can load without +// re-running the prover. See doc/artifacts.md for the format contract. + +// Bump when the serialized shape of any artifact changes incompatibly. +// Consumers should check this before assuming they can read the other paths. +export const FORMAT = 1 + +const versionSchema = z.object({ ref: z.string(), sha: z.string() }) + +export const manifestSchema = z.object({ + format: z.number().int().positive(), + version: versionSchema, + paths: z.object({ + core: z.string(), + text: z.string(), + // Template for per-space artifacts, with `{id}` standing in for the + // space's uid - e.g. `spaces/{id}.json` + spaces: z.string(), + }), +}) + +export type Manifest = z.infer + +// Everything needed to run deductions (and render lists and search): names, +// formulas and asserted trait values, but no descriptions or refs. +export const coreArtifactSchema = z.object({ + properties: z.array( + z.object({ + uid: z.string(), + name: z.string(), + aliases: z.array(z.string()), + counterexamples_id: z.number().optional().nullable(), + }), + ), + spaces: z.array( + z.object({ + uid: z.string(), + name: z.string(), + aliases: z.array(z.string()), + ambiguous_construction: z.boolean().optional(), + counterexamples_id: z.number().optional().nullable(), + }), + ), + theorems: z.array( + z.object({ + uid: z.string(), + when: formulaSchema(z.string()), + then: formulaSchema(z.string()), + converse: z.array(z.string()).optional().nullable(), + counterexamples_id: z.number().optional().nullable(), + }), + ), + traits: z.array( + z.object({ + space: z.string(), + property: z.string(), + value: z.boolean(), + }), + ), + version: versionSchema, +}) + +export type CoreArtifact = z.infer + +// The traits derivable for a single space from the asserted traits in the +// corresponding core artifact, with proofs +export const spaceArtifactSchema = z.object({ + space: z.string(), + traits: z.array( + z.object({ + property: z.string(), + value: z.boolean(), + proof: proofSchema(z.string()), + }), + ), + version: versionSchema, +}) + +export type SpaceArtifact = z.infer + +const entityTextSchema = z.object({ + uid: z.string(), + description: z.string(), + refs: z.array(refSchema), +}) + +// Descriptions and refs, which are only read on detail pages +export const textArtifactSchema = z.object({ + properties: z.array(entityTextSchema), + spaces: z.array(entityTextSchema), + theorems: z.array(entityTextSchema), + traits: z.array( + z.object({ + space: z.string(), + property: z.string(), + description: z.string(), + refs: z.array(refSchema), + }), + ), + version: versionSchema, +}) + +export type TextArtifact = z.infer + +export type Artifacts = { + manifest: Manifest + core: CoreArtifact + text: TextArtifact + spaces: Map +} + +// Prover inputs feed directly into derived proofs, so producing reproducible +// artifacts requires pinning theorem and trait iteration order (here, by uid). +export function implications(bundle: Bundle): ImplicationIndex { + return new ImplicationIndex( + sortByUid([...bundle.theorems.values()]).map(({ uid, when, then }) => ({ + id: uid, + when, + then, + })), + ) +} + +export function deduceSpace( + bundle: Bundle, + space: Id, + index: ImplicationIndex = implications(bundle), +): Result { + const asserted = [...bundle.traits.values()] + .filter(trait => trait.space === space) + .sort((a, b) => compare(a.property, b.property)) + + return deduceTraits( + index, + new Map(asserted.map(({ property, value }) => [property, value])), + ) +} + +export function serialize( + bundle: Bundle, + deductions: Map>, +): Artifacts { + return { + manifest: manifest(bundle.version), + core: coreArtifact(bundle), + text: textArtifact(bundle), + spaces: new Map( + [...deductions.entries()] + .sort(([a], [b]) => compare(a, b)) + .map(([space, derivations]) => [ + space, + spaceArtifact(bundle, space, derivations), + ]), + ), + } +} + +export function manifest(version: Version): Manifest { + return manifestSchema.parse({ + format: FORMAT, + version, + paths: { + core: 'core.json', + text: 'text.json', + spaces: 'spaces/{id}.json', + }, + }) +} + +// The zod parses below both validate the shapes and canonicalize the output: +// object schemas strip fields that don't belong in the artifact (description, +// refs) and emit keys in schema order, so serialization is deterministic even +// if input objects vary in field order. +export function coreArtifact(bundle: Bundle): CoreArtifact { + return coreArtifactSchema.parse({ + properties: sortByUid([...bundle.properties.values()]), + spaces: sortByUid([...bundle.spaces.values()]), + theorems: sortByUid([...bundle.theorems.values()]), + traits: sortTraits([...bundle.traits.values()]), + version: bundle.version, + }) +} + +export function spaceArtifact( + bundle: Bundle, + space: Id, + derivations: Derivations, +): SpaceArtifact { + return spaceArtifactSchema.parse({ + space, + traits: derivations.all().sort((a, b) => compare(a.property, b.property)), + version: bundle.version, + }) +} + +export function textArtifact(bundle: Bundle): TextArtifact { + return textArtifactSchema.parse({ + properties: sortByUid([...bundle.properties.values()]), + spaces: sortByUid([...bundle.spaces.values()]), + theorems: sortByUid([...bundle.theorems.values()]), + traits: sortTraits([...bundle.traits.values()]), + version: bundle.version, + }) +} + +// Plain codepoint comparison; localeCompare varies by environment +function compare(a: string, b: string): number { + return a < b ? -1 : a > b ? 1 : 0 +} + +function sortByUid(collection: T[]): T[] { + return collection.sort((a, b) => compare(a.uid, b.uid)) +} + +function sortTraits( + collection: T[], +): T[] { + return collection.sort( + (a, b) => compare(a.space, b.space) || compare(a.property, b.property), + ) +} diff --git a/packages/core/src/Logic/index.ts b/packages/core/src/Logic/index.ts index 88d2d015..1b7ac7d8 100644 --- a/packages/core/src/Logic/index.ts +++ b/packages/core/src/Logic/index.ts @@ -1,5 +1,5 @@ export { default as ImplicationIndex } from './ImplicationIndex.js' -export { Derivations } from './Derivations.js' +export { Derivations, type Derivation } from './Derivations.js' export { Contradiction, Proof } from './Prover.js' import { Formula, negate } from '../Formula.js' diff --git a/packages/core/src/index.ts b/packages/core/src/index.ts index bb346fae..ff248af8 100644 --- a/packages/core/src/index.ts +++ b/packages/core/src/index.ts @@ -9,6 +9,8 @@ export { type Formula, type And, type Atom, type Or } from './Formula.js' export { parser } from './Parser.js' export { type Property, PropertyPage } from './Property.js' export { + Derivations, + type Derivation, ImplicationIndex, deduceTraits, disproveFormula, @@ -21,6 +23,7 @@ export { type Trait } from './Trait.js' export { type Version } from './Bundle.js' export { parseDocument } from './Document.js' +export * as artifacts from './Artifacts.js' export * as bundle from './Bundle.js' export * as formula from './Formula.js' export * as Id from './Id.js' diff --git a/packages/core/test/Artifacts.test.ts b/packages/core/test/Artifacts.test.ts new file mode 100644 index 00000000..6eacf278 --- /dev/null +++ b/packages/core/test/Artifacts.test.ts @@ -0,0 +1,153 @@ +import { describe, expect, it } from 'vitest' +import * as artifacts from '../src/Artifacts' +import { Bundle, deserialize } from '../src/Bundle' +import { atom, or } from '../src/Formula' +import { Id } from '../src/Id' +import { Derivations } from '../src/Logic' +import { property, space, theorem, trait } from '../src/testUtils' + +const version = { ref: 'test', sha: 'HEAD' } + +const fixtures = { + properties: [ + property({ uid: 'P1' }), + property({ uid: 'P2' }), + property({ uid: 'P3' }), + property({ uid: 'P4' }), + ], + spaces: [space({ uid: 'S1' }), space({ uid: 'S2' })], + theorems: [ + theorem({ uid: 'T1', when: atom('P1'), then: atom('P2') }), + theorem({ uid: 'T2', when: atom('P2'), then: or(atom('P3'), atom('P4')) }), + ], + traits: [ + trait({ space: 'S1', property: 'P1', value: true }), + trait({ space: 'S1', property: 'P3', value: false }), + trait({ space: 'S2', property: 'P2', value: false }), + ], + version, +} + +function deduceAll(bundle: Bundle): Map> { + const index = artifacts.implications(bundle) + const deductions = new Map>() + + for (const space of bundle.spaces.values()) { + const result = artifacts.deduceSpace(bundle, space.uid, index) + if (result.kind !== 'derivations') { + throw new Error(`unexpected contradiction for space=${space.uid}`) + } + deductions.set(space.uid, result.derivations) + } + + return deductions +} + +function serializeAll(bundle: Bundle) { + const { manifest, core, text, spaces } = artifacts.serialize( + bundle, + deduceAll(bundle), + ) + return { manifest, core, text, spaces: [...spaces.entries()] } +} + +describe('serialize', () => { + const bundle = deserialize(fixtures) + + it('produces the expected manifest', () => { + expect(artifacts.serialize(bundle, deduceAll(bundle)).manifest).toEqual({ + format: artifacts.FORMAT, + version, + paths: { + core: 'core.json', + text: 'text.json', + spaces: 'spaces/{id}.json', + }, + }) + }) + + it('strips text from the core artifact', () => { + const { core } = artifacts.serialize(bundle, deduceAll(bundle)) + + expect(core.properties).toEqual([ + { uid: 'P1', name: 'P1', aliases: [], counterexamples_id: undefined }, + { uid: 'P2', name: 'P2', aliases: [], counterexamples_id: undefined }, + { uid: 'P3', name: 'P3', aliases: [], counterexamples_id: undefined }, + { uid: 'P4', name: 'P4', aliases: [], counterexamples_id: undefined }, + ]) + expect(core.traits).toEqual([ + { space: 'S1', property: 'P1', value: true }, + { space: 'S1', property: 'P3', value: false }, + { space: 'S2', property: 'P2', value: false }, + ]) + expect(core.theorems.map(t => t.uid)).toEqual(['T1', 'T2']) + }) + + it('keeps text in the text artifact', () => { + const { text } = artifacts.serialize(bundle, deduceAll(bundle)) + + expect(text.properties).toEqual([ + { uid: 'P1', description: 'P1', refs: [] }, + { uid: 'P2', description: 'P2', refs: [] }, + { uid: 'P3', description: 'P3', refs: [] }, + { uid: 'P4', description: 'P4', refs: [] }, + ]) + expect(text.traits).toEqual([ + { space: 'S1', property: 'P1', description: '', refs: [] }, + { space: 'S1', property: 'P3', description: '', refs: [] }, + { space: 'S2', property: 'P2', description: '', refs: [] }, + ]) + }) + + it('shards derived traits and proofs per space', () => { + const { spaces } = artifacts.serialize(bundle, deduceAll(bundle)) + + expect(spaces.get('S1')).toEqual({ + space: 'S1', + traits: [ + { + property: 'P2', + value: true, + proof: { theorems: ['T1'], properties: ['P1'] }, + }, + { + property: 'P4', + value: true, + proof: { theorems: ['T1', 'T2'], properties: ['P3', 'P1'] }, + }, + ], + version, + }) + expect(spaces.get('S2')).toEqual({ + space: 'S2', + traits: [ + { + property: 'P1', + value: false, + proof: { theorems: ['T1'], properties: ['P2'] }, + }, + ], + version, + }) + }) + + it('is deterministic regardless of input order', () => { + const shuffled = deserialize({ + ...fixtures, + properties: [...fixtures.properties].reverse(), + spaces: [...fixtures.spaces].reverse(), + theorems: [...fixtures.theorems].reverse(), + traits: [...fixtures.traits].reverse(), + }) + + expect(JSON.stringify(serializeAll(shuffled))).toEqual( + JSON.stringify(serializeAll(bundle)), + ) + }) + + it('is deterministic across repeated runs', () => { + expect(JSON.stringify(serializeAll(bundle))).toEqual( + JSON.stringify(serializeAll(bundle)), + ) + }) +}) From c86a3e367c9b02dd1537d529eb7aa47429773cad Mon Sep 17 00:00:00 2001 From: James Dabbs Date: Thu, 2 Jul 2026 17:20:47 -0700 Subject: [PATCH 2/3] refactor(compile): keep per-space derivations from bundle validation Bundle validation already deduces every space to check for contradictions, then discarded the result. Return the Derivations keyed by space uid instead (threading them through load), so a follow-up can emit them as derived-data artifacts. Deduction now runs through core's artifact entry points, which pin prover input order for reproducible proofs, and builds the implication index once instead of per space. --- packages/compile/src/load.ts | 13 ++++-- packages/compile/src/validations.test.ts | 26 ++++++----- packages/compile/src/validations.ts | 56 ++++++++---------------- 3 files changed, 41 insertions(+), 54 deletions(-) diff --git a/packages/compile/src/load.ts b/packages/compile/src/load.ts index 438a5c09..8a5abb6c 100644 --- a/packages/compile/src/load.ts +++ b/packages/compile/src/load.ts @@ -13,6 +13,7 @@ export default async function load( version?: Version, ): Promise<{ bundle?: B.Bundle + deductions?: Validations.Deductions errors?: Map }> { return validate({ @@ -51,7 +52,10 @@ export function validate({ return format(Validations.bundle(bundle)) } catch (e) { if (e instanceof ValidationError) { - return format({ value: bundle, errors: e.messages }) + return format({ + value: bundle && { bundle, deductions: new Map() }, + errors: e.messages, + }) } else { throw e } @@ -82,8 +86,9 @@ function checkAll( return result.value } -function format({ value, errors }: Validations.Result): { +function format({ value, errors }: Validations.Result): { bundle?: B.Bundle + deductions?: Validations.Deductions errors?: Map } { if (errors.length > 0) { @@ -95,8 +100,8 @@ function format({ value, errors }: Validations.Result): { grouped.get(path).push(message) }) - return { bundle: value, errors: grouped } + return { ...value, errors: grouped } } else { - return { bundle: value } + return { ...value } } } diff --git a/packages/compile/src/validations.test.ts b/packages/compile/src/validations.test.ts index 4d2e8c82..14632b07 100644 --- a/packages/compile/src/validations.test.ts +++ b/packages/compile/src/validations.test.ts @@ -127,8 +127,8 @@ describe('bundle', () => { ]) }) - it('adds deductions', () => { - const { value: b, errors } = bundle({ + it('returns the derivations for each space', () => { + const { value, errors } = bundle({ properties: [ F.property({ uid: 'P1' }), F.property({ uid: 'P2' }), @@ -157,15 +157,17 @@ describe('bundle', () => { expect(errors).toEqual([]) - // TODO - // const { value, proof } = b!.traits.get( - // traitId({ space: 'S1', property: 'P3' }), - // )! - - // expect(value).toEqual(true) - // expect(proof).toEqual({ - // properties: ['P1'], - // theorems: ['T1', 'T2'], - // }) + expect(value!.deductions.get('S1')!.all()).toEqual([ + { + property: 'P2', + value: true, + proof: { theorems: ['T1'], properties: ['P1'] }, + }, + { + property: 'P3', + value: true, + proof: { theorems: ['T1', 'T2'], properties: ['P1'] }, + }, + ]) }) }) diff --git a/packages/compile/src/validations.ts b/packages/compile/src/validations.ts index a21f77d8..d8a702ce 100644 --- a/packages/compile/src/validations.ts +++ b/packages/compile/src/validations.ts @@ -3,42 +3,21 @@ import yaml from 'yaml-front-matter' import { type Bundle, - ImplicationIndex, + type Derivations, type Property, - type Space, - deduceTraits, + artifacts, formula as Formula, schemas, } from '@pi-base/core' import type { File } from './fs.js' -// FIXME -type CheckResult = - | { kind: 'bundle'; bundle: Bundle } - | { - kind: 'contradiction' - contradiction: { theorems: unknown[]; properties: unknown[] } - } -function check(bundle: Bundle, space: Space): CheckResult { - const implications = new ImplicationIndex( - Array.from(bundle.theorems.values()).map(({ uid, when, then }) => ({ - id: uid, - when, - then, - })), - ) - const traits = new Map( - Array.from(bundle.traits.values()) - .filter(trait => trait.space === space.uid) - .map(trait => [trait.property, trait.value]), - ) - - const result = deduceTraits(implications, traits) - if (result.kind === 'contradiction') { - return result - } - return { kind: 'bundle', bundle } +// Traits derivable from each space's asserted traits, keyed by space uid +export type Deductions = Map> + +export type Deduced = { + bundle: Bundle + deductions: Deductions } export type Message = { @@ -282,7 +261,7 @@ export function trait(input: File) { }) } -export function bundle(bundle: Bundle): Result { +export function bundle(bundle: Bundle): Result { return validate('', error => { const duplicatePropertyNames = duplicated( Array.from(bundle.properties.values()).map(s => s.name), @@ -333,24 +312,25 @@ export function bundle(bundle: Bundle): Result { } }) - let result = bundle + const deductions: Deductions = new Map() + const implications = artifacts.implications(bundle) - for (const space of result.spaces.values()) { + for (const space of bundle.spaces.values()) { const key = paths.space(space.uid) - const checked = check(bundle, space) - switch (checked.kind) { - case 'bundle': - result = checked.bundle + const result = artifacts.deduceSpace(bundle, space.uid, implications) + switch (result.kind) { + case 'derivations': + deductions.set(space.uid, result.derivations) break case 'contradiction': error( - `properties=${checked.contradiction.properties} contradict theorems=${checked.contradiction.theorems}`, + `properties=${result.contradiction.properties} contradict theorems=${result.contradiction.theorems}`, key, ) break } } - return result + return { bundle, deductions } }) } From 57384119083d466f8e2bb2c971dc010a02df53ac Mon Sep 17 00:00:00 2001 From: James Dabbs Date: Thu, 2 Jul 2026 17:35:11 -0700 Subject: [PATCH 3/3] feat(compile): emit the derived-data artifact set alongside bundle.json Write manifest.json, core.json, text.json and per-space derived-trait shards (to an 'artifacts' directory by default) next to the unchanged bundle.json. Adds a viewer parity test - artifact deduction equals what the client prover derives on the same fixture - guarding the property that users can re-derive published results locally. Verified against the live data repo: 49,578 derived traits across 222 shards (max 44 KB), byte-identical across repeated runs. --- packages/compile/src/main.test.ts | 52 ++++++++++++- packages/compile/src/main.ts | 33 +++++++-- packages/core/src/Artifacts.ts | 5 ++ .../src/stores/deduction.parity.test.ts | 74 +++++++++++++++++++ 4 files changed, 157 insertions(+), 7 deletions(-) create mode 100644 packages/viewer/src/stores/deduction.parity.test.ts diff --git a/packages/compile/src/main.test.ts b/packages/compile/src/main.test.ts index fcbc4ce6..1562f3cc 100644 --- a/packages/compile/src/main.test.ts +++ b/packages/compile/src/main.test.ts @@ -1,6 +1,6 @@ import { beforeEach, afterAll, expect, it } from 'vitest' import { spawnSync } from 'node:child_process' -import { readFile, stat, unlink } from 'node:fs/promises' +import { readFile, rm, stat, unlink } from 'node:fs/promises' import { join } from 'node:path' const main = join(__dirname, '..', 'src', 'main.ts') @@ -38,6 +38,11 @@ async function cleanup() { if (await exists(out)) { await unlink(out) } + await rm(join(repo, 'valid', 'artifacts'), { recursive: true, force: true }) +} + +async function readJson(path: string) { + return JSON.parse((await readFile(path)).toString()) } beforeEach(cleanup) @@ -48,7 +53,7 @@ it('builds a bundle', async () => { expect(output).toContain(`::debug Compiling repo=${repo}/valid to out=`) expect(error).toBe(false) - const bundle = JSON.parse((await readFile(`${repo}/valid/${out}`)).toString()) + const bundle = await readJson(`${repo}/valid/${out}`) expect(bundle.properties.length).toEqual(3) expect(bundle.spaces.length).toEqual(2) @@ -56,6 +61,49 @@ it('builds a bundle', async () => { expect(bundle.traits.length).toEqual(3) }) +it('emits the derived-data artifact set', async () => { + const { error } = await run('valid') + expect(error).toBe(false) + + const dir = join(repo, 'valid', 'artifacts') + + const manifest = await readJson(join(dir, 'manifest.json')) + expect(manifest.format).toEqual(1) + expect(manifest.version.sha).toEqual( + 'c74d99cf46f6ed23e742f2617e9908294b4a608b', + ) + + const core = await readJson(join(dir, manifest.paths.core)) + expect(core.properties.length).toEqual(3) + expect(core.spaces.length).toEqual(2) + expect(core.theorems.length).toEqual(1) + expect(core.traits).toEqual([ + { space: 'S000001', property: 'P000016', value: true }, + { space: 'S000001', property: 'P000036', value: false }, + { space: 'S000002', property: 'P000036', value: false }, + ]) + + const text = await readJson(join(dir, manifest.paths.text)) + expect(text.properties.length).toEqual(3) + expect(text.properties.every((p: any) => p.description.length > 0)).toBe(true) + + const shard = await readJson( + join(dir, manifest.paths.spaces.replace('{id}', 'S000001')), + ) + expect(shard.traits).toEqual([ + { + property: 'P000019', + value: true, + proof: { theorems: ['T000001'], properties: ['P000016'] }, + }, + ]) + + const empty = await readJson( + join(dir, manifest.paths.spaces.replace('{id}', 'S000002')), + ) + expect(empty.traits).toEqual([]) +}) + it('writes error messages for invalid bundles', async () => { const { output, error } = await run('invalid') diff --git a/packages/compile/src/main.ts b/packages/compile/src/main.ts index 8d244192..c16cabb5 100644 --- a/packages/compile/src/main.ts +++ b/packages/compile/src/main.ts @@ -1,13 +1,18 @@ import * as fs from 'fs' +import * as path from 'path' import * as process from 'process' -import { bundle as B } from '@pi-base/core' +import { artifacts as A, bundle as B } from '@pi-base/core' import load from './load.js' -async function run(repo = '.', out = 'bundle.json'): Promise { - log(`Compiling repo=${repo} to out=${out}`, 'debug') +async function run( + repo = '.', + out = 'bundle.json', + artifactsOut = 'artifacts', +): Promise { + log(`Compiling repo=${repo} to out=${out} artifacts=${artifactsOut}`, 'debug') - const { bundle, errors } = await load(repo) + const { bundle, deductions, errors } = await load(repo) if (errors) { errors.forEach((messages, path) => { @@ -17,12 +22,30 @@ async function run(repo = '.', out = 'bundle.json'): Promise { }) } - if (errors || !bundle) { + if (errors || !bundle || !deductions) { log('Compilation finished with errors', 'error') process.exit(1) } fs.writeFileSync(`${repo}/${out}`, JSON.stringify(B.serialize(bundle))) + writeArtifacts(`${repo}/${artifactsOut}`, A.serialize(bundle, deductions)) +} + +function writeArtifacts(dir: string, artifacts: A.Artifacts): void { + const write = (relative: string, data: unknown) => { + const file = path.join(dir, relative) + fs.mkdirSync(path.dirname(file), { recursive: true }) + fs.writeFileSync(file, JSON.stringify(data)) + } + + const { manifest, core, text, spaces } = artifacts + + write('manifest.json', manifest) + write(manifest.paths.core, core) + write(manifest.paths.text, text) + spaces.forEach((artifact, space) => { + write(A.spacePath(manifest, space), artifact) + }) } type Level = 'debug' | 'info' | 'error' diff --git a/packages/core/src/Artifacts.ts b/packages/core/src/Artifacts.ts index 3744e88a..434e2158 100644 --- a/packages/core/src/Artifacts.ts +++ b/packages/core/src/Artifacts.ts @@ -177,6 +177,11 @@ export function manifest(version: Version): Manifest { }) } +// Resolve the manifest's per-space path template for a given space +export function spacePath(manifest: Manifest, space: Id): string { + return manifest.paths.spaces.replace('{id}', space) +} + // The zod parses below both validate the shapes and canonicalize the output: // object schemas strip fields that don't belong in the artifact (description, // refs) and emit keys in schema order, so serialization is deterministic even diff --git a/packages/viewer/src/stores/deduction.parity.test.ts b/packages/viewer/src/stores/deduction.parity.test.ts new file mode 100644 index 00000000..66cd73b9 --- /dev/null +++ b/packages/viewer/src/stores/deduction.parity.test.ts @@ -0,0 +1,74 @@ +import { readFileSync } from 'node:fs' +import { get, writable } from 'svelte/store' +import { describe, expect, it } from 'vitest' +import { artifacts, bundle as B } from '@pi-base/core' +import * as Gateway from '@/gateway' +import { Collection, Id, Theorems, Traits, type Trait } from '@/models' +import * as Deduction from './deduction' + +// Precomputed artifacts must match what the client prover derives on the same +// data: users check published results by re-deriving them locally, and +// alternative data sources without artifacts fall back to client deduction. +describe('artifact deduction parity', () => { + it('derives the same traits as the client prover', async () => { + const fixture = JSON.parse( + readFileSync( + new URL('../../cypress/fixtures/main.min.json', import.meta.url), + 'utf-8', + ), + ) + const bundle = B.deserialize(fixture) + + // Artifact-side: deduce each space through core's pinned-order entry points + const index = artifacts.implications(bundle) + const fromArtifacts = new Map() + for (const space of bundle.spaces.values()) { + const result = artifacts.deduceSpace(bundle, space.uid, index) + expect(result.kind).toEqual('derivations') + if (result.kind !== 'derivations') { + continue + } + for (const { property, value } of result.derivations.all()) { + fromArtifacts.set(`${Id.toInt(space.uid)}|${Id.toInt(property)}`, value) + } + } + + // Client-side: run the same bundle through the gateway transform and the + // eager full-database deduction pass + const synced = await Gateway.sync(unusedFetch, bundle)('host', 'branch') + const properties = Collection.byId(synced!.properties) + const spaces = writable(Collection.byId(synced!.spaces)) + const theorems = writable(Theorems.build(synced!.theorems, properties)) + const traits = writable( + Traits.build(synced!.traits, get(spaces), properties), + ) + + const derived: Trait[] = [] + const store = Deduction.create(undefined, spaces, traits, theorems, added => + derived.push(...added), + ) + await store.run() + + expect(get(store).contradiction).toBeUndefined() + + const fromClient = new Map( + derived.map(({ space, property, value }) => [ + `${space}|${property}`, + value, + ]), + ) + + const mismatched = [...fromArtifacts].filter( + ([key, value]) => fromClient.get(key) !== value, + ) + expect(mismatched).toEqual([]) + expect(fromClient.size).toEqual(fromArtifacts.size) + + // Guard against vacuously passing on an empty or trivial fixture + expect(fromArtifacts.size).toBeGreaterThan(100) + }) +}) + +const unusedFetch = async () => { + throw new Error('parity test should not fetch') +}