Method, language and evidence boundaries

DCL/1 v1.0 is a deliberately small contract language with strict keyword checking. It does not claim JSON Schema compatibility.

Exact supported language

The envelope accepts dialect, schema and optional semantics only. dialect is dcl/1. The root is a non-null object. Every schema node requires type: object, array, string, number, integer, boolean, null, or exactly [type,"null"]. Nullable is explicit; nullable is not a supported keyword.

Type	Allowed keywords besides type
object	properties, required, additionalProperties (boolean only)
array	items (required), minItems, maxItems
string	enum (scalar), minLength, maxLength
number / integer	enum (scalar), minimum, maximum (inclusive)
boolean / null	enum (scalar)

Object properties default to {}; required defaults to []; additionalProperties defaults to true. Required names must be declared. Array items is one schema for every item. String length counts Unicode code points. Enums contain distinct type-valid scalars. Wrong-type keywords, contradictory bounds, unknown keywords and empty enums are errors. $schema, $ref, format, pattern, anyOf, oneOf, allOf and arbitrary business expressions are unsupported. Use JSON Pointer (RFC 6901) paths for nested diagnostics; ~ and / become ~0 and ~1. Numbers use finite IEEE-754 doubles; integer values must be safe integers. Decimal arithmetic is not exact.

Structural inclusion: which direction?

For each reader, ask whether every structurally valid producer value also satisfies that reader. We compare old → reader and new → reader, then separately new → old and old → new. A recursive sufficient proof checks type containment (integer ⊆ number), required guarantees, property constraints, extra fields, scalar enums, inclusive numeric bounds, string lengths and array item/length containment. A producer enum is checked exhaustively. No text diff is used as proof.

“Proven inclusion” is a sound sufficient proof within DCL/1. If that proof fails, a bounded constructive search tries concrete producer-valid objects, enum members and boundary values. A witness is returned only after validating producer acceptance and consumer rejection. Otherwise the result is “Not proven”, never a claim of incompatibility. Search is incomplete: a directed branch search allows 2,000 local candidate checks, followed by bounded fallback sampling (at most 200 candidates at each node). Each constructed witness is capped at 1,000 value nodes; the proof is conservative, so some compatible contracts remain unproved. Witnesses cover structure only. Structural proof does not prove actual producer behavior.

Semantic declarations

semantics maps declared object-property JSON Pointers to rules. Arrays cannot be addressed by semantic paths in v1. Missing declarations are unknown; field names never imply units. Consumer-declared paths determine semantic comparison scope. Missing producer declarations require review. Matching declarations are promises, not runtime verification.

{"/event_time":{"kind":"timestamp","unit":"s","timezone":"UTC","after":"2020-01-01T00:00:00Z","before":"2030-01-01T00:00:00Z"},"/amount":{"kind":"money","unit":"USD-cent"},"/event_id":{"kind":"identifier","format":"decimal-string"}}

Timestamp unit is s or ms with integer schema and UTC, or rfc3339 with string schema and UTC / explicit-offset. UTC strings require Z; explicit-offset accepts Z or a numeric offset. Timestamp strings require full date, time, seconds and timezone, with 0–3 fractional digits; leap seconds are unsupported. Calendar validity is checked. Optional inclusive after/before UTC timestamps establish the declared window. Without a window, a numeric value alone cannot reveal whether a unit is wrong. No units are guessed.

Money units are USD-cent, USD-dollar, EUR-cent, EUR-euro. Cents require safe integers; whole-currency values are finite numbers. Values cannot prove a currency or scale, so changed units require declaration review. Identifier decimal-string requires digits only. No number-to-string coercion occurs. Optional absent/null values skip semantic checks; use required and type for presence/nullability. No undeclared business rule is inferred.

Replay and exported evidence

The same parsed row is checked against both structural schemas, both semantic declarations and all consumers. Row status: pass both, new failure, fixed or still failing. Within each row, introduced/resolved/unchanged errors match by JSON Pointer + code across structure and semantics. These counts can reveal changed errors even if a row still fails. A malformed line is a parse error, excluded from both validations. Empty input never means zero errors.

The browser executes these algorithms on each run. The four cases are synthetic authored inputs, not a production benchmark. There are no hidden saved measurements masquerading as checks. Reports include input contracts and names, but omit raw sample event values; generated witnesses can contain schema enum values. CSV uses quoted cells plus apostrophe guards for formula-like prefixes including whitespace. Keep guards during spreadsheet import.

What remains outside scope