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/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/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/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 } }) } diff --git a/packages/core/src/Artifacts.ts b/packages/core/src/Artifacts.ts new file mode 100644 index 00000000..434e2158 --- /dev/null +++ b/packages/core/src/Artifacts.ts @@ -0,0 +1,236 @@ +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', + }, + }) +} + +// 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 +// 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)), + ) + }) +}) 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') +}