Gargamelle technical contract

This document specifies the intended public semantics of Gargamelle 0.1.0. “Must” denotes a requirement, not a claim that the implementation has been formally proved. Verification results and implementation history are separate.

1. Model and scope

A Definition(a) consists conceptually of a structural acceptance relation and a conversion from accepted JSON inputs to values of type a. Public definitions are opaque and constructible only through library operations. The definition is authoritative: schema emission and decoding are derived interpretations of it. There is no independent schema/decoder override or arbitrary predicate escape hatch.

The supported target is Gleam compiled to JavaScript. Schemas use JSON Schema Draft 2020-12 and declare that dialect at the root. The contract applies to the vocabulary generated by the public constructors, not arbitrary imported schemas.

Let J be finite JSON trees represented after JavaScript JSON parsing: null, booleans, strings, finite IEEE-754 binary64 numbers, arrays and objects with string keys. Values containing undefined, functions, bigint, NaN, infinities, cyclic references, accessors or arbitrary host objects are outside J. Public Value is opaque; parse admits JSON text into this domain.

Parsing follows JSON.parse semantics, including rounding numeric literals, underflow and retaining the last occurrence of a duplicate object key. Numeric overflow to a nonfinite value is an admission error. The contract concerns the resulting parsed value, not arbitrary-precision decimal text. Escaped lone surrogates follow JavaScript string semantics.

2. Acceptance equivalence and value correctness

For every well-formed, finalized definition S and x in J, assuming sufficient runtime resources and pure, total conversion callbacks:

Valid202012(emit_json(S), x)
    ⇔ validate(S, x) = Ok(Nil)
    ⇔ ∃v. decode(S, x) = Ok(v)

Valid202012 denotes the dialect’s validation semantics without coercion, default insertion or property removal. Every comparison must use the same parsed input value. A validator’s optional lint restrictions are not additional acceptance rules.

For accepted input, the returned v must also satisfy S’s decoded-value contract below. Acceptance agreement alone is insufficient. For invalid in-domain input, validation and decoding must return structural data errors. They must not treat callback exceptions or runtime exhaustion as rejection.

validate and emission must not execute conversion callbacks. decode must validate the complete input before conversion. Construction must not probe constructors or maps with fabricated values. Recursive builders receive typed reference definitions, not invented decoded outputs. Neither validation nor conversion performed by the library mutates the admitted input.

Mappings are trusted application functions. They cannot add structural rejection rules. Exceptions, nontermination and side effects in user functions are outside the guarantee. Application checks such as cross-record identity, external references and business invariants belong in a separate semantic validation stage.

3. Constructor semantics

The identifiers below describe semantic operations; public API spellings are listed in the generated API reference. All composition must preserve section 2.

4. Primitive and constraint rules

Safe integers use inclusive bounds within ±9007199254740991. These limits must appear in the emitted schema. Parsed 1.0 is integral; integer comparisons treat negative zero and zero equivalently. Finite numbers decode to Float and preserve the admitted binary64 value, including signed zero. Number constraints use finite inclusive/exclusive endpoints. Repetition intersects intervals; equal endpoints with either side exclusive and inverted intervals fail construction. A valid real interval need not contain a representable binary64 value.

String values are preserved without trimming, case conversion or normalization. Lengths count Unicode code points, not UTF-16 units or grapheme clusters. Patterns use ECMAScript Unicode (u) regular expressions with search semantics and no implicit anchoring or additional flags. Invalid expressions fail construction. Distinct repeated patterns are conjoined; identical patterns are deduplicated in first-declaration order. Regex execution bounds are not guaranteed.

Integer bounds and size bounds are inclusive. Size limits are nonnegative safe integers. None denotes an unbounded endpoint. Repetition intersects bounds; invalid bounds and application to unsupported underlying definitions fail construction. Bounds/patterns should be applied before naming or union composition; wrappers are not a promise that every constraint supports every composition.

Enums are nonempty, contain distinct strings and perform no coercion. Constants use type-sensitive equality. Integer constants must lie in the safe range.

unique_items applies to a direct homogeneous array definition and compares the original JSON items structurally, before mapping. Object key order is irrelevant and both numeric zero signs are equivalent. Decoded list order is unchanged.

5. Records, presence and tagged variants

Fields are static declarations keyed by wire name. A curried constructor consumes actual decoded field values. Duplicate wire names fail construction. A record explicitly chooses Closed (reject extras) or Open (accept extras and project them away from output). Empty records still require objects. Dictionaries retain all keys and decode their values to a Gleam list of key/value pairs; key order has no semantic meaning. Keys including __proto__, constructor, toString, empty strings and Unicode must be handled as data.

Presence is independent of nullability. For child output a:

Defaults are admitted JSON values validated during construction without invoking converters. On absence, conversion decodes that default normally. Present invalid values never fall back to defaults. The schema’s default remains an annotation; no input or external-validator mutation is permitted.

Nullable uses an outer-first null check: null produces None, otherwise the child result is wrapped in Some. Nested nullable values may leave some output values unreachable. Null bypasses an inner one-of, even if multiple inner branches accept null. Non-null child errors retain their paths.

A tagged union owns a required string discriminator with distinct tags. Branches come from record builders; arbitrary wrapped definitions are not branches. The discriminator must not be redeclared. Variant annotations and maps are explicit. The selected branch constructs its ordinary payload; the tag is not injected as an extra output field. Empty variant sets and duplicate tags fail construction. Missing, invalid or unknown tags are diagnosed before branch fields.

6. Structural auxiliary constraints

Auxiliary definitions contribute only their structural acceptance relations; their conversion callbacks must never execute. Base output and type are retained. Checks inspect the original admitted input before defaults, projection or maps.

property_names constrains every present own object key as a JSON string and conjoins repeated constraints. It accepts supported record/dictionary bodies. Keys are not renamed. An empty object satisfies the key constraint vacuously. A String-output mapping can retain a non-string structural contract; that may reject every actual key while still accepting the empty object.

contains counts array positions satisfying a matching definition, including duplicate positions, and enforces nonnegative inclusive minimum/optional maximum counts. It supports homogeneous arrays and exact tuples. Repeated requirements are conjoined. Minimum zero with no maximum adds no acceptance restriction. It neither removes unmatched elements nor alters conversion.

if_then requires the consequence only when the condition accepts. if_then_else requires the consequence on condition acceptance and the alternative otherwise. Condition rejection is branch selection, not a data error. Operational failure must not select the alternative. Repeated conditionals are conjoined.

exclude requires the base to accept and every forbidden definition to reject. A matching forbidden definition produces a data error at the current path. Operational failure is not evidence of forbidden rejection. Repetition intersects constraints without replacing previous exclusions.

7. Names and recursion

Names start with an ASCII letter and otherwise contain only ASCII letters, digits, underscores or hyphens. Named definitions preserve acceptance and output while emitting finite local $defs/$ref graphs. Distinct bodies with conflicting names, including transitive conflicts, must not produce an ambiguous schema.

Self recursion and mutually recursive pairs use typed placeholders and retain the declared output types; the pair’s types may differ. Every cycle must descend into a strict input subvalue through an array item, tuple position, dictionary value or record field. Names, references, nullable, union, annotations and same-input constraints do not supply descent. Same-input cycles fail construction, including syntactically reachable cycles in otherwise unreachable branches. The guard is conservative; it is not a satisfiability proof.

References cannot be validated, decoded, emitted or used to validate defaults before finalization. Rejected graph finalization invalidates its bound references. Unfinished or conflicting composed graphs fail operationally at public validation or emission boundaries. Traversal of finalized schemas must terminate through identity tracking; shared completed branches must not be repeatedly expanded by the recursion guard. Emission must remain finite even for recursive definitions.

There is no implicit decoding depth cap, input-size cap or definition-size cap in acceptance. Stack exhaustion, timeouts and other resource failures remain operational failures. Linear or bounded runtime is not guaranteed for arbitrary compositions, overlapping branches or patterns.

8. Schema emission and canonical serialization

emit_json returns an opaque JSON value describing the definition; emit_text returns its canonical JSON string. Emission must not depend on conversion callbacks or process history. The schematic forms are:

Finite numbers emit type: number with minimum/maximum or exclusiveMinimum/exclusiveMaximum as appropriate. Unique arrays add uniqueItems: true. Named/reference targets are collected into root $defs and represented by local $ref without recursive expansion. No remote or dynamic references or implicit $id are introduced.

The root declares $schema: https://json-schema.org/draft/2020-12/schema. Metadata is added only by the corresponding constructors. Distinct repeated string patterns emit allOf pattern branches; repeated membership, property-name, conditional and exclusion constraints preserve conjunction. Zero/no-maximum membership may omit vacuous keywords. Annotations do not change acceptance and outermost repeated titles/descriptions win.

Required-field arrays are sorted by lexicographic UTF-16 code-unit order; enum, union and other semantically ordered arrays preserve declaration order. Canonical text recursively inserts object keys in that sorted order and uses compact JSON.stringify serialization without a trailing newline. JavaScript enumeration then places array-index keys first in numeric order. Thus properties named 2 and 10 serialize in numeric order, while the required array is ["10","2"]. Defaults obey the same canonicalization. All own keys must survive serialization without invoking inherited setters or changing prototypes.

For the same finalized definition, text emission must be byte-identical:

parse(emit_text(S)) = Ok(emit_json(S))  // JSON value equality
emit_text(S) = emit_text(S)            // byte equality on repeated emission

JSON object member order is not part of value equality. Serialization normalizes negative zero to zero. There is no typed encoder, arbitrary schema importer, surjectivity guarantee onto the output type or decode/encode inversion promise. Defaults, projection and maps can deliberately lose the original representation.

9. Errors and boundaries

Admission errors concern JSON syntax and nonfinite parsed values. Construction errors concern invalid definitions: duplicate fields/tags/enums, empty enums or unions, invalid bounds, constants, defaults, names, regexes or recursion graphs, and unsupported constraint/definition combinations. Some invalid combinations are excluded by static types. Data errors concern admitted values rejected by a well-formed definition. Operational failures are distinct from all three.

Data paths are JSON Pointers: root is the empty string, array indices are decimal, ~ becomes ~0 and / becomes ~1. Missing required fields point to the containing object and carry missing_key; undeclared keys point to that key. Errors have categories. Union errors carry zero-based branch failures for no match and matching indices for one-of ambiguity. Selected tagged-branch errors pass through; nullable non-null child errors preserve their paths. English wording and error enumeration order are not guarantees.

Core decoding and emission have no filesystem, network, application storage, UI or host-lifecycle dependencies. Runtime helpers may implement primitive JSON, regex, numeric and graph operations; they must not forge generic typed values.

10. Optional documentation

HTML documentation is presentation of the emitted vocabulary, not an independent validator. Text and attribute values must be escaped. Shared and recursive references are represented finitely with links. Presentation aliases do not change schema or decoding semantics.

Checked examples are admitted input values validated against the definition, without executing converters. All rejected example indices and validation errors are returned instead of rendering a successful example section. Accepted examples are displayed as escaped canonical input JSON, not as decoded outputs. An empty example list has the ordinary rendering behavior.

11. Excluded guarantees

The contract does not claim full JSON Schema dialect support, arbitrary schema import, remote/dynamic references, arbitrary heterogeneous recursion groups, general public intersection, pattern properties, schema-constrained extra record fields, format assertions, multipleOf, fractional/general JSON constants, encoders, migrations or reversible value conversion. Erlang and other runtime support are outside the 0.1.0 contract. Machine-checked correctness, resource bounds and arbitrary user-code safety are not promised.