Soundness argument¶

This page argues, in a form a reader can check, why an accept is never wrong: if valgebra reports a value valid, the value really is in the schema's set. It is a written argument backed by adversarial tests, not a machine-checked proof; the honest limits say exactly what is taken on trust.

The claim¶

Write ⟦S⟧ for the set of Python values a schema S denotes (its denotation). valgebra rests on three soundness statements:

Membership is exact. For every schema S and value x, the walk accepts x if and only if x ∈ ⟦S⟧. The "only if" half is soundness of acceptance — the property downstream code relies on; the "if" half is completeness of the check.
Construction preserves meaning. The normal form a constructor builds denotes the set the spelling names: ⟦union(A, B)⟧ = ⟦A⟧ ∪ ⟦B⟧ however the members are flattened, absorbed, ordered or folded on the way in. The deprecated simplify method preserves meaning for the same reason, since every fold it applies is a law of the same algebra.
Decisions are sound. If is_subtype_of(A, B) is True then ⟦A⟧ ⊆ ⟦B⟧; if is_empty(S) is True then ⟦S⟧ = ∅. The converses are not claimed — the decision is deliberately conservative.

There is no separate specification the implementation could disagree with: the denotation is the meaning, so soundness is the statement that the Rust walk computes x ∈ ⟦S⟧. The argument is therefore a node-by-node check that the walk's accept condition is, line for line, the membership condition of ⟦S⟧.

Why membership is exact: structural induction¶

The walk recurses on the structure of S. Take as induction hypothesis that the walk is exact on every strict sub-schema; then check each node. The denotation and the walk's accept condition coincide at every one:

S                accepts x  ⟺  x ∈ ⟦S⟧, by:
---------------  -----------------------------------------------------------
Anything         always                         (⟦Anything⟧ = all values;
                                                 `Any` is this node, spelled)
Nothing          never                          (⟦Nothing⟧ = ∅)
Bool/Int/...     isinstance(x, T)               (the scalar region)
Literal(c)       type(x) is type(c) and x == c  (typed singleton)
Union(A_i)       some A_i accepts x             (∃: set union)
Intersection     every A_i accepts x            (∀: set intersection)
Complement(A)    A does not accept x            (¬: set complement)
Refine(B, c_j)   B accepts x and every c_j      (base ∩ constraints)
Seq(kind, r)     x is a kind whose elements     (regular language over
                 match the regex r                element denotations)
Coll{kind, A}    every element accepts A         (homogeneous container)
KeyedMap(f, d)   fields present-and-match, and   (named fields ∩ keyed
                 every other key matches a       default clauses)
                 default clause
Instance(C)      isinstance(x, C)               (class extension)
AttrRecord(f)    every required field's          (attribute record; no
                 attribute is present on x       carrier, so a dataclass is
                 and matches                     `Instance(C) ∧ AttrRecord`)

Any admits every value, exactly as the top does, and it is the top: one node, one denotation, with the spelling kept for repr alone (see Any is the top, spelled). The row above covers both.

For the Boolean nodes the equivalence is the definition of the set operation, so the step is immediate given the hypothesis on the children. For the structural nodes (Seq, Coll, KeyedMap) the walk evaluates the children exactly by hypothesis and combines them by the same connective the denotation uses. The scalar and Instance leaves reduce to isinstance, which is Python's own membership test for those sets, and Literal adds the same-type guard that keeps Literal[1], Literal[True], and Literal[1.0] distinct.

Recursion terminates and stays exact¶

A recursive schema is guarded: every back-edge sits under a structural constructor. Membership unfolds the definition against the value in hand, and because the value is a finite Python object each unfolding asks about a strictly smaller value — so the set is defined by well-founded recursion on the value rather than chosen among fixpoints, and the guard is what makes that recursion well founded. Two further guards keep the unfolding finite in the walk:

an object-identity guard rejects a value that contains itself (recursion_loop) rather than looping, and
a depth bound rejects a value nested past the limit (recursion_limit) rather than overflowing the stack (see resource limits).

On the inhabitants — the finite values — the guarded unfolding accepts exactly the members, which is why a coinductive comparison at the greatest fixpoint never contradicts a membership answer (see recursion).

Why construction preserves meaning¶

Every fold a constructor applies is a law of the Boolean algebra of sets — flattening associative nodes, dropping identities and duplicates, absorbing a member that contains another, ordering the members, and folding X ∩ ¬X to ⊥ and X ∪ ¬X to ⊤ — each of which holds of the sets, so none can change ⟦S⟧. The form is held to this one invariant and to nothing stronger: it is a lattice normal form, not a decision, so membership relations are read off the decision procedures, never off the shape of a term.

Why the decisions are sound (and only sound)¶

is_subtype_of applies structural inclusion rules, each a valid set inclusion: A ⊆ B₁ ∪ … ∪ Bₙ when A ⊆ some Bᵢ, A₁ ∩ … ∩ Aₙ ⊆ B when some Aᵢ ⊆ B, the contrapositive between two complements (¬A ⊆ ¬B when B ⊆ A) and emptiness of the meet against one (A ⊆ ¬B when A ∩ B is empty), componentwise inclusion for the structural forms, and the coinductive rule for recursion (assume the goal on the current path — sound for inclusion at the greatest fixpoint). A leaf the rules cannot relate is handed to an oracle that returns False when it cannot prove the relation. Every rule preserves "the conclusion holds whenever the premises do", so a True is a proof.

is_empty is the primitive, not a derived relation: it decides the value regions, the complement and disjointness laws, and the refinement bounds directly, and the subtyping rules call into it — the lattice bounds ∅ ⊆ B and A ⊆ U are asked of emptiness, and A ⊆ ¬B reduces to A ∩ B being empty. So emptiness carries its own soundness and lends it upward, which is the direction to check the argument in. is_equivalent is mutual inclusion and inherits from subtyping.

The conservatism is the price: when a rule does not fire and the oracle declines, the answer is False — "not proven", not "disproven". This is why the decidability boundary maps where False is exact and where it is conservative, and why the docs say closed algebra, conservative decision.

How the argument is mechanized¶

The argument is checked, not just asserted. Four of the suite's layers bear on it directly; docs/dev/08-testing.md in the repository owns the full list, with what each layer is blind to beside it.

Denotation oracle. Each node's ⟦S⟧ is written as a reference predicate over a value generator, and the walk is property-tested to agree with it — this is the membership-exactness claim, checked on generated values.
Algebra laws. Every law construction relies on is property-tested against the membership relation, in Rust (proptest) and Python (Hypothesis).
External ground truth. The same schemas and values run through pydantic-core and jsonschema; a divergence is a bug or a documented intentional difference — an independent check that the reference predicates themselves are right, closing the single-author blind spot.
Coverage-guided fuzzing. libFuzzer drives the decision procedures over the whole IR, asserting the sound order laws (reflexivity, the lattice bounds, equivalence as mutual inclusion); the same invariants gate every merge.

These are partial mechanization — adversarial, independent, and coverage-guided — in place of a fully formal proof.

What this argument assumes¶

The soundness is relative to a small, explicit trust base:

isinstance and the PyO3 conversions report Python's own membership. A value crosses the boundary as itself, and what Python answers about it is read as a fact about the value rather than checked against a second reading.

A builtin kind is not read through isinstance, and __class__ is not in the trust base for one. isinstance consults a value's __class__, which a property can answer with any type at all, so an object declaring itself an int passes isinstance(value, int) while holding none of an integer's storage. A schema over a builtin kind reads the value's real type instead.

The sharper case is a genuine int subclass that declares itself a str. isinstance reads the real type first and the claim second, so Python admits that value to both kinds — which no value is, and which would put one value in a meet this library proves empty. Reading the real type gives one answer to each kind.

Where a schema names a user class, membership is isinstance by definition and a lying __class__ is honoured: overriding it is how a proxy is written, and a proxy every other consumer treats as a Target is one here too. - What a value answers is a function of the value. Membership asks a value questions through Python — isinstance, __eq__, a rich comparison, __len__, %, a predicate — and reads the answers as facts about it. A method that answers differently on two calls with the same argument is not describing a set, and the walk is built on the assumption that none does.

A & ~A does not rest on it. That law is a law about sets, so it is applied only where both sides are one: an atom running a predicate, or a class whose metaclass overrides __instancecheck__ or __subclasscheck__, is declined rather than folded. An abc.ABC is declined by the same test, because ABCMeta overrides both hooks -- which is how register changes the relation after a schema is built. A class whose metaclass leaves the hooks alone is a set, and the law still decides it.

A bound conjunction still rests on it. A contradiction between two bounds is decided by comparing the bounds, which holds only because a value ordered against one is ordered the same way against the other. Annotated[int, Gt(0), Lt(1)] is decided empty, and an int subclass whose comparisons answer True satisfies both -- a True no value supports. Deciding it soundly means reading the bounds over the exact builtin, which needs a schema to distinguish "exactly int" from "an int or a subclass"; that distinction is not expressible yet. The case is pinned as a known-unsound test rather than left unwritten. - A class whose metaclass leaves isinstance alone holds an object. A refutation about a class stands on a value of it, and nothing here can build one: reporting A not below B for two unrelated classes reads the difference as holding a value, and a class no value can instantiate is empty and below everything. The assumption licenses one object, on the line of objects with no builtin kind — a plain class against the complement of int stays undecided, because an integer that is an instance of it would need a class deriving from both. It moves no True: a proof is a proof, and the assumption is only ever read to believe a refutation. The decidability page states it with the rows it moves. - The JSON parser (jiter) agrees with json.loads where both accept. On a document both parsers build a value from, they build the same value, which is what makes the JSON path's denotation the object path's.

The grammar is the stricter of the two, and the difference is named. Two documents Python's module parses are refused here: a non-standard float token (NaN, Infinity, -Infinity) and an escape naming a lone surrogate. Each is reported as json_invalid before a schema sees it, so the JSON path admits a subset of what the object path does and never a different value (the JSON path states both with the queries that show them). - The crates contain no unsafe. Both crate roots carry #![forbid(unsafe_code)], which makes an unsafe block below one a compile error rather than a reviewer's job — so there is no memory-safety obligation here beyond the compiler's. - Predicate refinements are opaque. A Predicate constraint runs arbitrary Python; valgebra checks that it returned truthy, and the soundness of that leaf is the caller's. Regex constraints are matched natively and match the text of a str: a string carrying a lone surrogate has no such text and matches no pattern. The str kind holds one all the same — it is a string of one character — so a kind is never a subtype of a pattern over it, however much text that pattern matches, and "\ud800" is the value that says so. - A literal is a singleton where its constant's equality is Python's own. Literal[c] denotes {x | type(x) is type(c) and x == c}. For a builtin scalar that is one value; for a constant whose class defines __eq__ it is whatever that method admits, and for float("nan"), which is equal to nothing including itself, it is the empty set. - The values are the finite ones. A guarded fixpoint denotes the values built by finitely many unfoldings, which is what makes membership an induction on the value. A value that contains itself is not a large member: it is outside the model, which is why the identity guard reports recursion_loop rather than deciding. - The value holds still for the length of the call. Membership is a claim about the value the walk read, so a value that changes while it is being read has no membership answer. A change the walk can see — a container whose size moves, or a second reading that disagrees with the first — is reported as mutated_during_validation rather than answered (the error model); a change it cannot see, such as a field rewritten in place after the walk passed it, leaves an answer about the value as it was. - The suites check necessary properties, which is weaker than an oracle. A property-based or metamorphic check fails when the implementation is wrong; passing does not entail it is right, however many such properties are added. So the layers above raise the cost of a defect surviving without bounding it.

Within that base, an accept is a claim that x ∈ ⟦S⟧, justified node by node above and exercised by the layers named there — which is what "rock solid" can honestly mean before a machine-checked proof and outside review exist.