# CatDB formal semantic core roadmap ## Purpose and claim boundary This roadmap defines the smallest semantic core needed to test CatDB's central research claim: typed, composable, versioned schema mappings can carry integration meaning independently of where data is stored or executed. The roadmap is a research contract with a bounded accepted implementation cut. Rust and Haskell semantic prototypes, selected Lean invariants, and a 43-case cross-language fixture suite exist through accepted Slice 5. Later formalization and query targets remain future work. A computational release does not silently close a theorem obligation listed below. This work does not claim that CatDB eliminates ETL, schema-migration cost, physical data movement, query-planning uncertainty, or distributed-systems tradeoffs. It also does not treat agreement among three programs as a proof. ## Evidence and status vocabulary The program-wide claim labels and the operational statuses answer different questions: | Operational status | Meaning in this roadmap | Permitted claim label | | --- | --- | --- | | `PROVED` | A mathematical argument has been written, checked against its assumptions, and independently reviewed. | `proved` | | `CONDITIONAL` | The statement follows only under the listed assumptions, or depends on an unverified semantic model. | `supported by prior literature`, `engineering hypothesis`, or `open conjecture`, as stated | | `COMPUTATIONAL` | Executable examples or property tests support the bounded tested domain. | `experimentally supported` | | `OBSTRUCTED` | A named counterexample, missing definition, or undecidable/intractable obligation blocks the target. | `open conjecture` or a rejected/narrowed claim | | `OPEN` | The artifact or evidence does not yet exist. | `engineering hypothesis`, `open conjecture`, or `speculative` | `machine-checked` is used only for a statement accepted by the Lean 4 kernel from the pinned project environment. A passing Rust or Haskell test is `COMPUTATIONAL`, not `PROVED` or `machine-checked`. ## Semantic profile v1 The first profile is deliberately finite and explicit. - A **schema** is a finite presentation with stable identifiers for entities, generating arrows, scalar attributes, and equations between typed paths. - A **path** has a declared start entity and an ordered list of generating arrows. The empty list is the identity path. - An **equation** relates two well-typed paths with the same start and end. - A **mapping** assigns every source entity to a target entity, every source arrow to a target path, and every source attribute to a typed target attribute expression. It is valid only if those assignments preserve source equations. - An **instance** is a finite interpretation: a finite carrier for each entity, a total function for every arrow, and a total typed value assignment for every attribute. Profile v1 requires `required: true` on every attribute; null, missing values, and partial attribute functions are deferred. Instance equations must hold pointwise. - A **migration** is an operation induced by a validated mapping. Profile v1 requires executable `delta`. Bounded finite `sigma` is a later target. General `pi`, general Kan extensions, chase procedures, and external typeside functions are explicitly unsupported until their assumptions and cost model are fixed. - **Information loss** in v1 is a conservative, syntactic report about named witnesses such as object identification, arrow collapse, and attribute omission. Absence of a reported witness is not a proof of semantic invertibility. - A **schema diff** compares stable identifiers and typed definitions. It does not infer a rename from similar names; absent identity metadata, a rename is reported as remove plus add. The initial scalar profile is `string`, `integer`, `boolean`, `decimal`, `date`, and `uuid`. Integers are limited to the signed 64-bit range in every language. Decimal values use canonical decimal strings and reject all negative-zero spellings. Dates use ISO `YYYY-MM-DD` strings. UUIDs use lowercase canonical RFC-variant spelling and versions 1 through 8; Nil, Max, non-RFC variants, uppercase forms, and unversioned UUID-shaped strings are outside profile v1. These restrictions keep fixture comparison independent of host numeric, UUID, and time libraries. Every fixture carries an `assumptions` array. The field is mandatory so an omitted assumption cannot be confused with a reviewed empty set; the array may be empty when the operation has no fixture-specific assumptions beyond profile v1. ## Language and authority boundaries ### Rust production IR Rust owns the production representation, parser boundary, diagnostics, catalog integration, deterministic normalization, physical-plan boundary, and benchmarkable behavior. Validated wrapper types should prevent planners from receiving unresolved schemas, ill-typed paths, invalid mappings, or invalid instances. Rust is authoritative for what the shipping CatDB compiler accepts and emits. Its tests establish production conformance to the fixture contract. They do not prove general categorical laws, query equivalence on arbitrary backends, or correctness of connector execution. The production IR should remain language-neutral at serialization boundaries. It must not encode Rust enum layout, map iteration order, pointer identity, or database-driver objects in shared fixtures. ### Haskell reference semantics Haskell owns the small executable reference model for finite schemas, well-typed paths, mappings, finite instances, `delta`, and the selected structural analyses. It should favor clarity and total functions over production optimization. QuickCheck/Hedgehog generators must construct both valid values and single-fault invalid values. Exhaustive enumeration may supplement property tests for bounded universes. Haskell evidence is the oracle for intended finite semantics only after disagreements are resolved against the written definitions; it is not automatically authoritative merely because it is Haskell. Haskell must not absorb connector transport, distributed execution, storage transactions, or production catalog behavior. ### Lean 4 kernel-checked invariants Lean receives the smallest mathematical definitions that justify durable laws: typed paths, identity and composition, lawful mappings, mapping composition, finite instances, and selected migration/query laws. The Lean model must state all finiteness, decidable-equality, totality, quotient, and typeside assumptions explicitly. Lean is authoritative only for theorem statements compiled by its kernel. Extraction, code generation, examples, `native_decide`, and agreement with fixtures are useful evidence but are not substitutes for checking the exact theorem. No connector behavior, SQL optimizer behavior, database transaction, cost estimate, floating-point operation, or network execution is in the Lean scope unless separately modeled. ### Shared boundary All three implementations consume fixtures conforming to `fixtures/schema-v1.schema.json`. Arrays with semantic ordering remain ordered; set-like arrays use the canonical sort rules in `fixtures/README.md`. Implementations compare the normalized result or the exact diagnostic code, phase, and location. Free-form exception messages are never the acceptance surface. ## Canonical operations Let a well-typed path in schema \(S\) be written \(p : A \rightsquigarrow B\). The empty path at \(A\) is \(\mathrm{id}_A\). If \(p : A \rightsquigarrow B\) and \(q : B \rightsquigarrow C\), then the serialized composition is the arrows of `p` followed by the arrows of `q`: \[ q \circ p : A \rightsquigarrow C. \] A mapping \(F : S \to T\) assigns objects and generating arrows and extends to paths: \[ F(\mathrm{id}_A)=\mathrm{id}_{F(A)}, \qquad F(q\circ p)=F(q)\circ F(p). \] It is lawful only when each source equation \(p=q\) maps to an equation \(F(p)=F(q)\) derivable in the target presentation. Profile v1 must distinguish syntactic equality from equality justified by declared equations. Any rewriting algorithm must document whether it is complete for its restricted equational fragment. Categorical laws use extensional equality, not artifact-ID equality. Two mappings are extensionally equal when their source and target schema IDs and canonical object, arrow, and attribute assignments agree, ignoring only the mapping artifact ID. Two instances are extensionally equal when their schema ID, carriers, arrow functions, and attribute functions agree, ignoring only the instance artifact ID. Schema IDs remain part of the typing context. Migration results compare their output instances extensionally; generated artifact IDs and discharged-obligation lists are acceptance metadata. Golden fixtures still compare complete normalized JSON, and their input supplies the exact output mapping or instance ID. For an instance \(I\) on \(S\), each arrow \(f:A\to B\) is interpreted as a total function \(I(f):I(A)\to I(B)\). A declared path equation \(p=q\) holds when \(I(p)(x)=I(q)(x)\) for every \(x\in I(A)\). For \(F:S\to T\), the first executable migration is pullback: \[ \Delta_F(J)(A)=J(F(A)) \] with arrows and attributes interpreted along their mapped target paths and expressions. This definition assumes \(F\) is lawful and \(J\) is a valid finite \(T\)-instance. ## Invariant ledger Every row states assumptions, the production obligation, executable reference evidence, any justified Lean target, and the honest initial status. | ID | Invariant and assumptions | Rust test obligation | Haskell evidence | Lean target | Initial status | | --- | --- | --- | --- | --- | --- | | `SCH-01` | Schema identifiers are unique; every arrow/attribute endpoint resolves. Assumes finite input and exact identifier equality. | Golden accept/reject tests for duplicate and unresolved identifiers with stable diagnostic codes and JSON pointers. | Generator plus property that validation accepts exactly referentially closed bounded schemas. | None initially; this is representation validation rather than a categorical law. | `OPEN` — engineering hypothesis | | `SCALAR-01` | Profile-v1 integers are signed 64-bit; decimals reject every negative-zero lexical form; UUIDs are lowercase RFC-variant versions 1–8; all attributes are required and total. Assumes JSON numbers are decoded without loss before range checking and dates receive a separate calendar-validity check. | Boundary and one-past-boundary integer fixtures; decimal lexical probes; UUID version/variant/case probes; reject `required: false` and missing attribute assignments. | Generators constrained to the same domain plus single-fault out-of-range, negative-zero, UUID, and missing-value cases. | Use bounded integers or a range predicate only where scalar values enter later semantic theorems; no standalone categorical theorem is justified. | `OPEN` — representation contract | | `PATH-01` | Path typing is deterministic. Assumes a referentially closed schema and a declared start entity. | Fixture tests for empty, valid multi-arrow, unknown-arrow, and source-mismatch paths. | `typePath` property: one result endpoint or one typed error; compare against independent fold. | Define indexed or predicate-based typed paths and prove endpoint uniqueness. | `OPEN` — theorem target not yet encoded | | `PATH-02` | `id_A` is well typed from `A` to `A`. Assumes `A` belongs to the schema. | Empty-arrow fixture normalizes without inserting a synthetic arrow. | Unit property over generated entities. | Prove left and right identity for typed path composition. | `OPEN` — theorem target | | `PATH-03` | Composition is defined iff the first endpoint equals the second start; the result concatenates arrows in traversal order. | Positive and negative composition fixtures, including diagnostic location. | Property comparing composition with list append plus endpoint checking. | Prove typing preservation of composition. | `OPEN` — theorem target | | `PATH-04` | Path composition is associative where all endpoints align. | Triple-composition property over production IR plus normalized fixture equality. | QuickCheck over three composable generated paths. | Prove associativity, not by fixture enumeration. | `OPEN` — theorem target | | `EQ-01` | Both sides of a schema equation have the same start and end. Assumes each side is otherwise well typed. | Reject mismatched endpoints before theorem reasoning. | Generate typed and single-endpoint-fault equations. | Represent only parallel paths in the well-formed equation type. | `OPEN` | | `EQ-02` | A finite instance satisfies each schema equation pointwise. Assumes total arrow interpretations and decidable generator equality. | Evaluate every declared equation over every source carrier element and report the first canonical counterexample. | Exhaustive finite evaluation; mutate one assignment to obtain a counterexample when possible. | Define finite instances and prove the validator sound and complete for pointwise equation satisfaction. | `OPEN` — bounded theorem target | | `MAP-01` | A mapping is total on source entities, arrows, and attributes; each image is well typed with the required endpoints and scalar type. | Accept complete fixtures; reject missing, duplicate, or ill-typed assignments with stable codes. | Total validator plus generators that delete or corrupt exactly one assignment. | Define `LawfulMapping` as data plus typing and preservation proofs. | `OPEN` | | `MAP-02` | A lawful mapping preserves every declared source equation. Assumes the target equality decision procedure is sound for its declared fragment. | Fixture cases for syntactic preservation, declared-equation preservation, and unproved preservation. | Evaluate bounded target instances as counterexample search; separately test the chosen rewrite procedure. | Prove preservation from the `LawfulMapping` witness. Completeness of the target prover is a separate, optional theorem. | `OPEN`; general decision procedure is `OBSTRUCTED` until a fragment is chosen | | `MAP-03` | The identity mapping sends each entity, arrow, and attribute to itself and is lawful. | Construct and compare the exact canonical identity-mapping fixture. | Property over generated valid schemas. | Prove identity mapping lawfulness and identity action on paths. | `OPEN` — theorem target | | `MAP-04` | For lawful `F:S→T` and `G:T→U`, composition is total and lawful; arrow images are obtained by path substitution. | Composition fixtures cover success, schema mismatch, empty paths, and equation-bearing schemas. | Property comparing direct path substitution with sequential interpretation. | Prove lawfulness of composition. | `OPEN` — theorem target | | `MAP-05` | Mapping composition is associative and identity mappings are units under the extensional equality defined above. Assumes all mappings are lawful and share the stated schema IDs; artifact IDs are ignored. | Property tests on bounded normalized production IR after erasing only `mapping.id`; no reliance on hash-map order. Golden fixtures separately preserve caller-supplied IDs. | QuickCheck over chains of lawful generated mappings using the same extensional comparator. | Prove category laws for schemas and lawful mappings, whose equality excludes serialization IDs. | `OPEN` — theorem target | | `INS-01` | Every schema entity has one finite carrier; each arrow is a total function into its target carrier; every profile-v1 attribute is required, total, and typed. Assumes signed-64-bit integers and the scalar/UUID restrictions above. | Fixtures for missing carrier, duplicate generator, non-total function, out-of-carrier target, missing attribute value, wrong scalar tag, and integer overflow. | Independent finite validator and single-fault generators constrained to the same scalar domain. | Prove that accepted finite interpretations define a functor on the generated path category, conditional on equation satisfaction. | `OPEN` | | `MIG-01` | `delta` produces a valid source instance from a lawful `F:S→T` and valid finite target instance `J`. | Golden migration fixtures compare the complete normalized output instance; invalid preconditions are errors, not partial results. | Executable `delta`; property that output validation succeeds. | Prove output validity under the stated assumptions. | `OPEN` — first migration target | | `MIG-02` | `delta` respects identity and reverses mapping composition under extensional instance equality: `Δ_id J ≈ J` and `Δ_(G∘F) J ≈ Δ_F(Δ_G J)`. Assumes lawful mappings, valid total instances, and canonical generator/value equality; output artifact IDs and obligation lists are ignored. | Production properties erase only output `instance.id` and compare the remaining normalized instance; golden fixtures still check the prescribed ID exactly. | QuickCheck plus exhaustive small-instance comparison with the same extensional comparator. | Prove both laws for the finite model without serialization IDs in the semantic objects. | `OPEN` — theorem target | | `MIG-03` | Bounded `sigma` is a finite left pushforward with a documented quotient/canonicalization procedure. Assumes finite carriers and a decidable, terminating equality fragment. | Until implemented, fixtures must return `unsupported/SIGMA_NOT_IN_PROFILE`; later golden quotient cases must be added. | Prototype only after canonical representative semantics are fixed. | State and prove the `Σ_F ⊣ Δ_F` fragment only after quotient definitions are accepted. | `OBSTRUCTED` — definitions and complexity boundary not fixed | | `MIG-04` | General `pi` or right Kan migration is outside profile v1. | Return `unsupported/PI_NOT_IN_PROFILE`, never silently approximate. | No executable obligation in v1. | No v1 theorem target. | `OBSTRUCTED` — explicitly unsupported | | `LOSS-01` | Each `lossy` result has one or more concrete syntactic witnesses and may also contain inconclusive findings; concrete witnesses take precedence. `lossless_under_checked_criteria` has no findings. `unknown` has one or more findings and every one is inconclusive. Assumes only the selected checks, stable semantic-reference encoding, and not semantic invertibility. | Golden fixtures for object identification, arrow collapse, attribute omission, no detected witness, inconclusive analysis, and a mixed concrete-plus-inconclusive result; reject inconsistent classification/finding pairs and use the total finding order. | Recompute each witness independently; property that every finding references existing definitions and classification matches the finding set, including mixed-result precedence. | Optionally prove detector soundness for each syntactic criterion. Do not prove completeness or invertibility. | `OPEN`; “no finding” remains `CONDITIONAL` | | `DIFF-01` | Stable-ID schema diff is deterministic and complete for supported declaration-level changes. Assumes unique stable IDs, canonical orientation-independent equation subjects, the fixed kind rank, RFC 8785 snapshot keys, and no rename inference. | Golden add/remove/retype/equation-change fixtures; repeated runs and input permutation yield identical normalized changes under the total four-component sort key. | Reference set-difference implementation and permutation property using the same subject and ordering definitions. | None initially; an executable finite algorithm is sufficient. | `OPEN` — computational target | | `DIFF-02` | Applying a supported diff to its exact base yields the normalized target. Assumes no conflicting edit and all change kinds have defined application semantics. | Round-trip property plus rejection of wrong-base application. | Reference `diff`/`apply` round trip on generated schemas. | Optional finite theorem after the change algebra is stable. | `OPEN` | | `QRY-01` | Typed path navigation may be reassociated without changing finite-instance denotation. Assumes pure total arrows. | Compare original and reassociated logical IR before physical lowering. | Evaluate both forms on generated valid finite instances. | Derive from path associativity and instance functoriality. | `OPEN` — selected rewrite target | | `QRY-02` | Mapping-path inlining preserves denotation. Assumes a lawful mapping and the finite categorical query fragment. | Fixture-derived differential tests between staged and inlined logical plans. | Evaluate both plans through the reference model. | Prove for the defined path-selection fragment. | `OPEN`; query syntax not yet fixed | | `QRY-03` | Filter fusion and projection pushdown are allowed only for pure, total expressions under one specified boolean/null and bag/set semantics. | Backend-independent IR tests plus backend differential tests; disable rewrite when capability/semantics differ. | Small-model enumeration after expression semantics are defined. | No theorem until nulls, errors, volatility, and multiplicity are modeled. | `OBSTRUCTED` — semantic choices not fixed | | `QRY-04` | Inner-join reassociation is considered only with explicit predicates and a fixed multiplicity/null model; outer joins are excluded. | Differential test against native execution per supported backend before enabling. | Finite relation enumeration after the relational fragment is defined. | Later theorem target for the exact algebra only. | `OBSTRUCTED` — not a profile-v1 law | ## Fixture program `fixtures/schema-v1.schema.json` supports exactly these initial categories: 1. `schema_parsing` 2. `path_typing` 3. `path_composition` 4. `identity_mapping` 5. `mapping_composition` 6. `migration_validation` 7. `information_loss_detection` 8. `schema_diff` Every fixture contains one input and one deterministic expected outcome: `ok`, `error`, or `unsupported`. `error` means the operation is in profile but the input is rejected. `unsupported` means the fixture deliberately requests a feature outside the implementation profile. Outcomes are not interchangeable: non-migration categories admit only applicable `ok`/`error` outcomes; `delta` admits only `ok`/applicable `error`; `sigma` admits only `unsupported/SIGMA_NOT_IN_PROFILE`; and `pi` admits only `unsupported/PI_NOT_IN_PROFILE`. Diagnostic code/phase pairs and their category subsets are schema-enforced. A runner must not convert an error or unsupported case into a skipped test. The contract intentionally excludes query-rewrite fixtures from schema v1. The query IR and its null, error, and multiplicity semantics are not yet fixed. Selected rewrites remain roadmap targets and require a versioned schema change before cross-language acceptance fixtures are added. ## Work packages and gates ### F0 — freeze definitions and diagnostics Deliverables: - review the profile-v1 definitions and composition order; - freeze identifier, scalar, canonical-order, and diagnostic rules; - create at least one `ok`, one `error`, and where applicable one `unsupported` fixture for every category; - validate every fixture against the JSON Schema. Gate: an independent reviewer can compute each expected result by hand and no fixture relies on a free-form error message. Status: `COMPUTATIONAL`; accepted by Slice 0 for the frozen fixture contract. ### F1 — Rust representation and validators Deliverables: - parse and structurally validate every shared envelope, including finite instance inputs and schema-diff result values, without discarding duplicate evidence; - implement semantic schema, path, equation, and mapping validation; - implement deterministic normalization and diagnostic locations, including canonical serialization of instance and schema-diff envelopes; - pass parsing, path, identity, and mapping-composition semantic fixtures, plus structural round-trip/golden-serialization tests for instance and schema-diff envelopes. Gate: production tests pass twice with randomized construction/insertion order and byte-identical normalized JSON output. The F1 report marks instance and schema-diff operation cases `structural-only`; it may not count pointwise instance validity, `delta`, diff computation, or diff application as a semantic pass. Status: `COMPUTATIONAL`; accepted by Slice 1 for its declared finite subset. ### F2 — Haskell reference model Deliverables: - implement total finite reference functions for the F1 semantic subset and independent structural decoding/encoding for every profile-v1 envelope; - add valid and single-fault generators; - compare reference output with every shared fixture admitted by the F1 capability set; - record seeds and minimized counterexamples for every failure. Gate: Rust/Haskell disagreements are resolved by changing the written definition or the incorrect implementation, never by special-casing a fixture. F4 and F5 extend this reference model with finite-instance/`delta` semantics and semantic loss/diff operations rather than treating their F2 envelope round trips as those later results. Status: `COMPUTATIONAL`; accepted by Slice 2 for its declared finite subset. ### F3 — Lean path and mapping kernel Deliverables: - encode typed paths, identity, composition, equations, and lawful mappings; - prove `PATH-02` through `PATH-04` and `MAP-03` through `MAP-05`; - publish a coverage table mapping theorem names to invariant IDs and exact assumptions. Gate: the pinned `lake` build is accepted by Lean 4 with no `sorry`, `admit`, or unreviewed axioms in the trusted core. Status: `machine-checked` only for the exact Slice 3 coverage table and axiom report; all omitted invariants remain `OPEN`. ### F4 — finite instances and `delta` Deliverables: - extend the F1/F2 envelope support with semantic finite-instance validation in Rust and Haskell: carrier completeness, total arrow/attribute functions, scalar typing, target-carrier membership, and pointwise equation satisfaction; - implement `delta` and full-output migration fixtures; - prove the finite-model statements `EQ-02`, `MIG-01`, and `MIG-02` where the accepted definitions justify them. Gate: shared fixtures pass in Rust and Haskell, Lean theorem coverage is reported statement by statement, and no result is generalized to physical database execution. Status: `COMPUTATIONAL` for the accepted Slice 4 Rust/Haskell finite boundary. The additional Lean statements named above remain `OPEN`. ### F5 — conservative loss and diff analysis Deliverables: - implement only the named information-loss witnesses; - extend F1's schema-diff envelope/serialization support with semantic stable-ID diff computation and supported diff application; - add permutation, round-trip, and counterexample tests; - document false negatives and unsupported change kinds. Gate: semantic diff generation and application pass golden, permutation, and wrong-base/round-trip properties; `lossless_under_checked_criteria` is never rendered as “lossless”; and a rename is never inferred without explicit identity metadata. Status: `COMPUTATIONAL` for the accepted Slice 5 conservative loss/diff boundary; no general invertibility or completeness theorem is claimed. ### F6 — selected query rewrites Deliverables: - freeze a typed finite query IR and denotation; - select the exact rewrite subset from `QRY-01` through `QRY-04`; - version the fixture schema if new fixture categories are needed; - implement the independent Haskell evaluator `CatDB.Query.Finite` and executable `catdb-query-ref` without Rust, SQLite, SQL parsing, FFI, or replay of fixture expectations; - exhaust a fixed type-indexed scalar domain for type-correct models up to two entities, two records per entity, two scans, and query depth three; supplement this with independently seeded Hedgehog generators up to three entities, three records per entity, three scans, and query depth four; and persist every minimized generated counterexample with its seed and profile version; - add backend differential tests separately from semantic proofs. Gate: every enabled rewrite names its assumptions, reference evaluator, counterexample strategy, Lean theorem if any, and backend exclusion list. The pre-backend gate runs: ```bash cabal build catdb-query-ref --ghc-options="-Wall -Werror" cabal test catdb-semantics:query-profile-v1 cabal test catdb-semantics:query-small-model cabal run catdb-query-ref -- --manifest fixtures/query-profile-v1-manifest.json --emit haskell/generated/query-profile-v1-results.json python scripts/compare-query-reference.py fixtures/query-profile-v1-manifest.json haskell/generated/query-profile-v1-results.json ``` It exits only when the evaluator agrees with all admitted golden fixtures and all found generated counterexamples are minimized and retained. Backend differential tests remain a later, separate obligation. Status: `DEFERRED FUTURE WORK`; research-only query and provenance profile candidates exist, but no evaluator, fixture corpus, or rewrite result is claimed. ## Cross-language acceptance and disagreement policy A fixture passes an implementation only when: 1. the fixture validates against the shared JSON Schema; 2. the implementation supports the requested category and feature profile; 3. the normalized `ok` result is structurally equal to `expected.result`, or the exact expected diagnostic/unsupported envelope is returned; 4. every set-like result array obeys the canonical sort rule; 5. the runner records implementation revision, fixture schema version, and fixture identifier. When Rust, Haskell, Lean, or a hand-worked expectation disagree, work stops on that invariant. The resolution record must identify whether the defect was in the prose definition, fixture, production code, reference model, or theorem statement. Majority agreement is not a resolution rule. Lean fixtures are examples connected to definitions, not a requirement that Lean parse the production JSON directly. A small audited translation may construct Lean values from fixtures, but theorem coverage must still cite the general theorem rather than an example evaluation. ## Explicit nonclaims and deferred work - A lawful logical mapping does not guarantee an economical or available physical migration. - Finite-instance validation does not validate a warehouse snapshot under concurrent mutation. - `delta` laws do not establish `sigma`, `pi`, or general Kan-extension correctness. - Syntactic information-loss checks are not a decision procedure for invertibility, equivalence, recoverability, or business meaning. - Schema diffs do not by themselves define safe online migrations. - Logical query equivalence does not prove identical SQL error behavior, floating-point behavior, collation, time-zone behavior, query cost, or transactional behavior across backends. - Shared fixture agreement does not prove compiler correctness. - CQL is a prior-art reference and possible compatibility target; this roadmap does not assert behavioral parity with the current CQL implementation. ## Completion criterion for the formal semantic core milestone The milestone is complete only when the fixture corpus exists, all fixtures validate, Rust and Haskell independently pass the agreed profile, Lean checks the explicitly selected general theorems, coverage and assumptions are published, and every unresolved or unsupported invariant remains visibly labeled. Until then, this document is a roadmap with `OPEN` and `OBSTRUCTED` targets, not evidence that CatDB's semantic core has been implemented or proved.