DSAIL Language

DSAIL is Jaxon's domain-specific language for expressing policy constraints as formal logic. DSAIL code compiles to SMT solver inputs, enabling mathematically provable compliance checking rather than probabilistic LLM-based assessment. Where an LLM might say "this probably complies," a DSAIL assertion either holds or it does not.

Each ruleset rule contains DSAIL code that declares variables, defines constraints through assertions, and compiles to formulas that an SMT solver evaluates. The solver determines whether each assertion is satisfiable (the constraint holds) or unsatisfiable (the constraint is violated). This satisfiability check maps to a boolean outcome for each assertion, giving a precise, per-rule compliance verdict for every input document tested.

How DSAIL Works

DSAIL bridges the gap between natural language policies and formal verification. Here is how it fits into the ruleset workflow:

1. A policy rule is expressed in natural language — for example, "The proposed rent must not exceed 110% of local market average"
2. DSAIL code formalizes that rule — declaring variables like landlordStatedProposedRent and localMarketAverageRent, then asserting the constraint landlordStatedProposedRent <= (localMarketAverageRent * 1.1 "")
3. Questions are generated for each variable — at run time, an LLM reads the document and answers questions like "What is the proposed rent?"
4. Answers become variable assignments — the LLM's answers are bound to the declared variables
5. The solver evaluates the assertion — given the variable values, is the constraint satisfied?

This approach separates two concerns: the LLM handles data extraction (answering straightforward factual questions about document content), while the SMT solver handles logical reasoning (determining whether the extracted facts satisfy the formal constraint). The result is more reliable than asking an LLM to reason about compliance directly.

For Compliance Teams

While it is a good idea to audit DSAIL logic to ensure that it aligns with policy expectations, it is not necessary to write DSAIL code manually. The platform can generate DSAIL from natural language rules using the ruleset creation wizard. Understanding what DSAIL does — encoding policy rules as provable logic — is more important than knowing the syntax. The language reference below is primarily for technical users who want to write or customize rules directly.

One thing, or several?

Read this before writing any rule. It is the single decision that most often separates a rule that means what you think from one that quietly does not, and it cannot be recovered from later — the rest of the rule is built on top of it.

The rule of thumb

A declared claim holds one answer for the whole document. declare interest_rate as numeric; means the interest rate — one value, for this document.

When a document describes several separate things of the same kind, name the kind. declare Loan as entity; says "there are some number of these, discovered per document", and claims bound to it with of Loan are extracted once per loan.

There is no third mode. Multiplicity comes from an entity declaration and from nothing else — the platform never decides on its own that a claim turned out to be about several things.

Why it matters: the same document, two rulesets

Take a document that says, in full:

Bob is happy. Jane is unhappy.

Written as a document property, the ruleset says there is one answer to "is the subject happy?":

declare happy as boolean;
assert everyone_happy { happy };

There are two subjects and one slot to put them in. Whatever the extractor returns — Bob's answer, Jane's answer, or an unresolved conflict between them — the rule cannot express "both of them", so its verdict is not about the document you meant. Nothing errors. That is what makes this the expensive mistake.

Written with an entity, the ruleset says there are people, and each has an answer:

declare Person as entity;
declare happy as boolean of Person;

assert everyone_happy { ForAll(p in Person, happy[p]) };
assert someone_happy  { Exists(p in Person, happy[p]) };

Now the two rules disagree, which is the point — they are asking different questions, and the document answers them differently:

Rule	Verdict	Why
everyone_happy	NO	Jane is a counterexample. One is enough to refute every.
someone_happy	YES	Bob is a witness. One is enough to satisfy some.

A single boolean claim cannot produce that pair of answers, because there is only one answer to produce.

Which one do I want?

Ask what the sentence is about:

The document...	Write	Example
states one fact about itself	a plain claim	the contract's governing law, the filing date, the total
describes several things of one kind, and the rule is about each of them	an entity	every loan in a portfolio, each named party, each line item
repeats one fact several times	a plain claim	a rate restated in the summary and the schedule — same fact, one answer

The middle row is the one people miss. "The document mentions three loans" is not three answers to one question; it is one answer to each of three loans' questions, which is exactly what an entity scope is.

Not sure yet?

Start with plain claims. Adding an entity later is a ruleset edit, and the entity section below walks through it. The reverse — a rule that has been reporting confident verdicts about the wrong subject — is the case you cannot detect from the results.

Language Reference

DSAIL programs consist of:

• Variable declarations — Typed variables (boolean/Bool subtypes, numeric, enum).
• Assignments — Default, constant, or initial values for variables.
• Assertions — Named logical constraints that the solver evaluates.
• Functions — Reusable logic encapsulated as named functions.
• Quantifiers — Universal (ForAll) and existential (Exists) constraints over collections.

Basic Syntax

• Statements end with a semicolon (;) unless enclosed in braces.
• Block statements use curly braces ({ ... }).
• Identifiers are alphanumeric with underscores (_).

declare x as boolean;
let x = true;

assert myAssertion {
  x
};

Naming a registry claim

A claim from the shared corpus registry is named with an @ sigil and its catalog id — @namespace.name — in its declaration and at every reference. There are three kinds of name a rule can introduce, and one rule can show all three:

// Retention policy §4.2 -- personal data must not be kept beyond the stated limit.
declare @data.personal_data as boolean;         // a governed registry claim
declare retention_days as numeric;              // this rule's own claim
declare local retention_limit as numeric;       // an intermediate -- generates no question

let retention_limit = 730 "days";

assert retention_within_limit [pessimistic] {
  Or(Not(@data.personal_data), retention_days <= retention_limit)
};

Form	What it names	Question generated?
@namespace.name	A registry claim. Its gloss, type and question are defined once in the corpus and every rule that names it inherits them.	Yes — the registry's own question, identical for every rule that names it
A bare identifier	This rule's own claim. No other rule can name it.	Yes — a question generated for this rule
declare local <name>	An intermediate: a named constant, or a value a let fully determines.	No — declare local never becomes a question or a claim

Why the sigil exists. Without it you cannot tell the first two apart. A registry claim id and a rule-local name are both lowercase words joined by punctuation, so data_personal_data in a rule could be a governed term forty rules depend on, or something this rule's author invented five minutes ago. The sigil puts the difference in the source, and the editor colours it as well.

The sigil is the only way to name a registry claim. A bare identifier is always local to the rule it appears in, so @fh.steering_language and a rule-local that happens to be spelled fh_steering_language are two different claims and always read as two different claims — there is no silent capture in either direction. Any number of dotted segments is allowed (@clas.portion.level), and the sigil is what keeps a claim name from being confused with a dotted type such as Bool.Tri.

declare local @ns.name is rejected: local means private to this rule, which is the opposite of registry-backed. The compiler says so in as many words, and names both ways out — drop the local, or drop the sigil.

Existing rulesets keep working, unchanged

Every rule written before the sigil existed uses bare identifiers, and bare identifiers still mean exactly what they always meant: claims local to their rule. Nothing needs rewriting, nothing is upgraded behind your back, and a ruleset that names no registry claim behaves identically to how it always did. Adopting the shared vocabulary is a deliberate edit, one rule at a time — see Promoting a local claim.

One claim, one answer

The sigil is not only a spelling. It is a commitment with a visible consequence: because @namespace.name means the same claim in every rule that writes it, a run asks it once per subject — one question, one answer — and records that answer against every rule that reads it.

You see this in a finished run. Open it, expand a document on the Evaluation tab, and every rule shows its own Claims table: the claim's name, the question that was asked of the document, and the extracted value. Fourteen rules that name @sys.operating_frequency all list that claim, and they all show the same value, because there was one observation behind them. Declared as fourteen rule-local claims instead, the same fourteen rules ask fourteen separate questions and are free to come back with fourteen different frequencies — with nothing on the screen to tell you they disagreed, because each rule looks internally consistent.

That contrast is the decision you are making when you write the declaration. Take a rule that needs one governed fact and one fact of its own:

declare @sys.operating_frequency as numeric;   // the registry's claim
declare freq_band_mentioned as boolean;        // this rule's own claim

Repeat that pair across fourteen rules of one ruleset and the run asks:

Written as	Questions asked	What a rule can see
@sys.operating_frequency	one, shared	the one answer, identical in all fourteen rules
freq_band_mentioned	fourteen, one per rule	fourteen answers, free to differ

Fifteen questions for that ruleset rather than twenty-eight.

The wording is the registry's, not the rule's. When a rule declares a registry claim, the platform does not invent an extraction question for it — it adopts the canonical question the claim carries in the corpus, so the same sentence is put to the document wherever the claim is used. And because the claim is asked once, editing that question by hand in one rule's claim editor does not buy that rule a question of its own: one wording reaches the model for all of them. A claim's canonical wording belongs in the Vocabulary Workbench, where it is defined, not in one rule that happens to share it.

Fewer questions is a practical reason to prefer a registry claim. Every question is a separate model call, so a ruleset whose shared facts are registry claims makes fewer calls and finishes sooner — and the fewer times a fact is independently judged, the fewer chances there are for two judgements of it to diverge. Metered usage is deliberately not reduced: it counts the verification each rule's verdict rests on, so it is the same whether a claim is shared or duplicated. What sharing saves is model calls and wall-clock time.

Nothing about the result changes shape. The claim still appears under every rule that reads it, with its value and, where the run captured one, its supporting excerpt. A grail likewise trains one head per registry claim rather than one per rule, so the proposition is learned once.

Three things are deliberately not folded together, because they are not one claim:

• Bare identifiers. Two rules' retention_days are two claims that merely look alike, and each keeps its own question and its own answer.
• The same claim asked of two different documents. In a multi-slot ruleset, a claim bound to contract in one rule and to amendment in another is two questions — there are two documents, so there are two answers.
• Entity-scoped claims. A claim declared of <Entity> answers by enumerating a population per quantified scope, so there is no single value to share. See Multiple Answers.

If a rule pins its reference to a specific corpus version while another rule reads the same name unpinned or at a different version, those are different claims too, and each is asked separately — the two versions may word the claim differently, and nothing silently resolves one to the other.

Data Types

DSAIL supports the following types:

Boolean

Truth values (True or False). Bare boolean is shorthand for Bool.Monotone. Boolean subtypes control how repeated measurements of the same claim combine when a document is streamed in chunks — see Boolean subtypes.

Numeric

A (value, unit) tuple — every numeric carries a unit. Literals write the unit as a quoted string immediately after the value (e.g. 5.0 "m/s"), using the empty string "" for unitless quantities. Conversion happens inside the rule at comparison time — see Units.

Enum

A fixed set of string values. Declare the allowed values as an ordered array [...] or an unordered set {...} — see Enums.

Units

A numeric value is a (value, unit) tuple — there is no bare integer or real. Numeric literals carry their unit as a quoted string, attached to the value rather than the declaration:

declare speed as numeric;
assert limit { speed <= 5.0 "m/s" };

Extraction is verbatim. The value pulled from a document — and shown to you as the claim — is the raw number and unit exactly as found in the text (e.g. 1.2 g), with no alteration or conversion. Unit conversion happens inside the rule, at the moment of comparison: when a claim of 1.2 g meets the rule literal 500 "mg", the registry converts the claim to the rule's unit (1200 mg) and the comparison decides the verdict. Conversion never mutates the extracted claim.

Conversion uses a per-project unit-converter library merged over the platform's built-in standard libraries:

• Counts & Ratios — the unitless numerics (see Counts and ratios below). Counts: items, units, x, each, pcs, #, and the count multipliers dozen, pair, thousand, million, billion. Ratios: % (with pct, percentage point/pp), basis points, ppm/ppb, per mille ‰, and the named base ratio. The two are separate dimensions and never cross-convert.
• SI & metric — SI base and derived units with metric prefixes, plus SI-accepted units (litre, tonne, hour, degree). Percent and basis points live in Counts & Ratios, not here. Its time units are the fixed ones (nanoseconds through weeks): a day is 24 hours and a week is 7 days by definition.
• Calendar durations — months and years, as the ranges they actually are. See Calendar durations below.
• US customary & imperial — inches through acres, °F, mph, psi, with converters into the SI bases.
• Digital information — bytes and bits with decimal (KB, MB, GB) and binary (KiB, MiB, GiB) prefixes, plus data rates (bit/s through Tbit/s, bps aliases, and byte-per-second forms). Sizes and rates are separate dimensions and never cross-convert.
• Currencies — alias groups for the major world currencies (codes, symbols, spellings). Deliberately no exchange-rate converters — rates are not constants; a project whose policy fixes a rate can add its own converter.

Each library is a per-project toggle on the Unit Library page: new projects start with all of them active, and the page lists every active library's contents. Deactivate one and its units stop resolving for that project's rules, and its names become free for project redefinition — so a project that needs its own mph deactivates US customary & imperial and defines the units it does want, without giving up metres, percentages or currencies in the process. (Prefer a distinct project-specific name where you can: redefining a built-in name is rejected while its library is active, because the built-in edge would silently win.) The selection is saved in the versioned library document, so runs record exactly which libraries they evaluated under. If a claim's unit cannot be resolved to the rule's unit — including a unitless number compared against a dimensioned literal — that comparison is Unknown (a dimensional mismatch is not silently compared in the wrong unit). When a run hits such a mismatch, the assertion carries a warning naming the missing conversion, with an Add converter action that opens the project's Unit Library and asks whether the gap is an alias (same unit written differently) or a converter (different units) — then pre-fills the entry for you to finish and save.

The Unit Library page

Units in the project menu opens that project's Unit Library. Most projects never need it: all built-in standards start active, and a project that measures things in ordinary units already resolves them. You come here to turn a standard off, or to teach the project a unit it doesn't know.

The page has three parts:

Built-in standards. One row per standard listed above, each with an Active/Off checkbox and a count of what it contains. Expand a row to read its aliases (m = meters) and converters (km → m ×1000); built-in contents are read-only. Turning a standard off stops its units resolving in this project's rules and frees those names for redefinition.

Project alias groups. Names for the same unit, comma-separated — USD, $, dollar, dollars. Anything in one group is treated as one unit.

Project converters. A from-unit, a to-unit, a multiplication factor, and an optional offset. The factor may be a range written 28..31 for units that genuinely vary, the way the Calendar durations standard handles months; a range factor and an offset can't be combined.

Edits are staged until you press Save — including standard toggles, and including entries pre-filled by the Add converter action described above. Reload discards unsaved changes; the page warns you before navigating away with work in progress. For bulk edits, a raw-JSON mode exposes the whole library as text.

Calendar durations

A month is 28–31 days and a year is 365 or 366, so neither has a fixed size. The Calendar durations standard says so directly: it converts "months", "quarters" and "years" into days as a range rather than an average.

Unit	Days
"month"	28–31
"quarter"	90–92
"year"	365–366

The fixed time units — nanoseconds through weeks — are ordinary SI converters instead, because a day is 24 hours and a week is 7 days by definition. Only the units a calendar makes irregular live here, which is why the standard is named for the calendar: turning it off does not stop hours from converting.

declare span as numeric;              // extracted "2 years"
assert long_enough { span > 700 "d" };   // TRUE: 2 years is 730-732 days

A comparison is decided whenever the whole range decides it, and is Unknown only when the answer genuinely depends on which month or year was meant:

declare notice as numeric;            // extracted "365 days"
assert year_of_notice { notice >= 1 "y" };   // Unknown: 365 days might be short

That second verdict is the honest one — 365 days is a full year unless the year in question is a leap year. When a rule really means a date-anchored span, the run's warning says so rather than offering a converter that already exists.

Months, quarters and years still relate to each other exactly, so the everyday comparisons are unaffected: 36 "mo" == 3 "y" and 4 "qtr" == 1 "y" are both TRUE. Only their relationship to days is a range, because only that one is genuinely uncertain.

If your policy text defines a year — contracts often fix it at 365 days — add an ordinary converter for y → d in the project's Unit Library. A project converter takes precedence over a standard's, and the choice is recorded in the versioned library like any other edit. Turning the standard off instead leaves "months" and "years" as recognized units with no path to days, which surfaces as a normal missing-converter warning.

The Unit Library page edits alias groups and converters as a form (a converter is to = from × factor + offset, where the factor may be a range [low, high] for a unit whose size is not fixed; offset is only for affine scales like °C → K, and a ranged factor cannot carry one). A raw-JSON mode remains for bulk edits. Common spellings and symbols are accepted as built-in aliases — for example temperatures may be written degC/degF or with the degree glyphs °C/°F, all resolving to the same unit.

Spelled-out units are case-insensitive. 30 Days, 18 MONTHS and 2 Quarters resolve exactly as their lowercase forms do, because documents are routinely title-cased and the capitalization of a word carries no meaning. Symbols are not, because for them capitalization is the unit: mW is a milliwatt and MW a megawatt, Cal is a kilocalorie and cal a calorie. A miscased symbol is therefore left unresolved — surfacing as an ordinary unknown-unit warning — rather than being guessed at. Manage a project's converters and aliases through the unit-library API (/api/v1/projects/{id}/unit-library); the standard defaults are importable from /api/v1/unit-library/si-standard.

A PUT replaces the whole library, so it takes the library document (aliases, converters, standards) and rejects any other field with a 422 naming it — a misspelled converters is a library with no converters in it, and the symptom would otherwise land a run later as a claim that could not be converted. For convenience the GET response envelope ({project_id, library, version}) is accepted and unwrapped, so a read-modify-write client can feed a response straight back; the project_id and version it carries are ignored, because every write appends a new version regardless.

Counts and ratios

A number with no unit is a count, and its unit is the empty string (""). Every generic quantifier word is an alias of it, so 11, 11 "items" and 11 "units" are the same quantity and all compare cleanly against a 11 "" rule literal. The count multipliers convert into it — 2 "dozen" is 24, 3 "k" is 3000.

Counting words are deliberately generic only. A domain's classifier nouns — 3 "loans", 2 "cars" — are that project's vocabulary, not platform-wide names: declare them in the project's Unit Library (a loan alias group, and a loan → "" converter with factor 1 if you also want them to compare against bare counts). Naming the thing being counted is good practice; it makes a claim self-describing and keeps two different counts in one ruleset from being compared by accident.

Ratios are a different dimension from counts, and the separation is deliberate. A fraction of a whole is written in "%" — or in the named base "ratio", where 1.0 "ratio" is 100%. Percent, basis points, ppm, ppb and ‰ all convert among themselves and into "ratio", but none of them converts to or from "": a bare 0.8 in a document is a count of 0.8, not 80%, and silently reading it as a percentage would be wrong by 100×. So a rule that means a fraction should say so — ltv <= 0.8 "ratio" or ltv <= 80 "%" — and a claim extracted as a bare 0.8 against either of those surfaces Unknown with a missing-converter warning rather than a wrong verdict. A project whose documents genuinely write bare fractions can add the "" → ratio converter itself; that is a per-project decision because it is only correct if that project never counts anything.

Three notes on the ratio units:

• x stays a count multiplier, not a ratio. 3 "x" is 3, not 300% — if a ruleset mixes 3x with 300%, add a project converter to relate them.
• percentage point / pp is an alias of %: dimensionally they are the same unit, and whether a change is relative or absolute is part of what the rule asserts, not part of the unit.
• ppt deliberately does not ship — it means parts per thousand, parts per trillion, and percentage point depending on the field. Alias it in your project if your domain fixes the meaning.

The unit library is versioned: every save, import, or clear creates a new immutable version rather than editing in place, so changing the library never silently alters what past runs meant. Runs record the library version they were built against, and any historical version can be inspected via ?version=N or listed at /api/v1/projects/{id}/unit-library/versions. Clearing the library appends an empty version — earlier versions remain recoverable.

Enums

An enum is a fixed set of string values. Declare the allowed values to make the domain explicit, choosing ordered (array [...]) or unordered (set {...}):

// Ordered enum: comparisons (<, <=, >, >=) are allowed and follow declaration order.
declare severity as enum ["info", "warn", "error"];

assert escalate {
  // "error" > "warn" > "info"
  IF severity >= "warn" THEN True END
};

// Unordered enum: only == / != / membership are allowed.
declare contract_type as enum {"lease", "purchase"};

assert is_lease { contract_type == "lease" };

The operator table is what the language allows. Corpus verification refuses a rule that breaks it before any run, naming the claim and the domain; on the production evaluation path the same rule does not silently pass either — it reports UNKNOWN rather than a verdict. One shape is worse than UNKNOWN and is called out below.

What the ordered form grants that the unordered form does not. Both forms declare a closed domain, so both give the claim its identity: ==, != and set membership work on either, and an == against a value outside the declared domain is refused rather than compiled into a comparison that could never be true. The ordered form grants comparison as well. <, <=, > and >= are legal between an ordered enum and a quoted label from that enum's own domain, in either position, and they mean exactly what the declaration order says: the comparison expands to the equalities that order satisfies, so severity >= "warn" is Or(severity == "warn", severity == "error"). No ordinal encoding is exposed and a label's spelling never enters into it — the declared order is the whole definition.

Two shapes stay unsupported on both forms:

• An ordering operator on an unordered enum. The refusal says the domain declares no ordering, rather than reporting the operator as meaningless — the fix is to declare the domain with [...], and only the declaration knows whether that is right.
• Two enums compared against each other (severity > other_severity). A declared order orders that domain's own labels; it says nothing about how one domain's labels sit against another's. Compare each side against a label.

Where each is caught. Corpus verification refuses both outright, before a run. On the production evaluation path an ordering it cannot give meaning to — on a boolean, on an unordered enum, against a label outside the domain, or arithmetic on an enum — yields no verdict for that assertion: it reports UNKNOWN. Two enum claims are the exception, and the reason not to write the shape: they are compared as text rather than by either declaration, so the assertion returns a confident verdict that is not the declared order — over ["LOW", "MED", "HIGH"], sev > sev2 answers true for MED > HIGH. Compare each side against a label and the question does not arise.

A label the declared domain does not contain is refused too, by the name of the domain it is not in: the literal is resolved against the domain before any comparison is built, so a typo in a label reads as a typo rather than as a rule that is quietly never true. Corpus verification refuses it under every operator; on the production path it is refused outright under == and !=, and reported as UNKNOWN under an ordering.

One declaration, one meaning: the SMT engine on the evaluation path and the corpus's own solver expand an ordered-enum comparison against a label into the same disjunction over the same declared order, and the grail compiler enforces the same operator table when a ruleset is compiled.

A registry claim keeps the registry's type and wording

Referencing a registry claim requires declaring it, so declare @sys.band as boolean; is normal and necessary. What is refused is declaring it with a type, boolean subtype or enum domain that differs from the one the registry holds — that is not a reference, it is a second claim wearing the same name.

The @ sigil means one thing: this is the registry's claim, on the registry's terms. Type, subtype and domain are all part of what the claim means, so they belong to the registry the way units and range do. A subtype in particular decides how repeated measurements of a claim combine, and one claim has one answer — two rules resolving the same claim's conflicts differently would give it two.

The extraction question is the registry's for the same reason, and it is not editable from a ruleset. The claim editor shows it, marked as coming from the shared vocabulary, and the field is read-only; a rule stores no copy of it. That is what makes rewording a claim in the corpus reach every rule that references it at once, with no stale copies left behind to ask the same claim two different ways. To change how a registry claim is asked, edit it in Corpus → Vocabulary; the next run of every referencing ruleset asks the new wording.

Declaration	Result
declare @sys.band as boolean; where the registry holds boolean	Allowed — this is how you reference it.
declare @sys.band as Bool.Tri;	Refused. Overrides the registry's subtype.
declare @sys.freq as boolean; where the registry holds numeric	Refused. Type mismatch.
declare @clas.level as enum;	Allowed — a bare enum takes the registry's domain.
declare @clas.level as enum ["TS","S","C","U"]; where the registry holds U,C,S,TS	Refused. For an ordered claim the declaration order is the scale, so restating it silently reorders the levels.
Editing the question on @sys.band in the ruleset editor	Not offered — the field is read-only and shows the registry's wording.

There is deliberately no override syntax. If you want different semantics you want a different claim, so give it a different name:

declare band_mentioned_tri as Bool.Tri;   // a local claim, yours to define

If the variant needs to be shared across rules rather than living inside one, promote it into the registry as its own claim — so it gets a name, a gloss and vetting like everything else, rather than appearing as a per-rule surprise.

Why the editor catches this and the compiler cannot

The DSAIL compiler has no registry access — the registry is group-scoped and the compiler is pure — so a contradicting declaration compiles cleanly. The check therefore runs where the registry is readable, when the rule is saved: the save is refused with the conflict named, and readiness reports it for rules that predate the check or arrived by import. It is never left to surface at inference time.

What a claim asks decides whether silence is an answer

A boolean claim is one of two things, and which it is decides what an unanswered document means. A rule's author has to know which of the two readings their claims have, because it changes what the rules must expect — and, where the wording alone does not make it obvious, has to say which they meant.

A claim about the text. "Does the portion state the operating frequency band?" — the context is the entire subject of the question, so it is always answerable. If the portion states a band the answer is True; if it does not, the answer is False. Silence is the answer. Presence questions are recognised by what they ask of the text: whether it states, names, mentions, identifies, discloses, reveals, specifies or contains something.

A claim about the world. "The subject drank alcohol on the job." — a document's silence settles nothing about the world. True if the document states it, False only if the document states something incompatible with it, and Unknown if the document does not address it. Absence of evidence is not evidence of absence.

The claim asks	Silence yields	Because
Does this text contain X?	False	The text is the whole subject; not containing X is a fact about it
Does X hold in the world?	Unknown	The text is evidence about the world, and it is silent

Settling it, rather than leaving it to be read

A claim can declare which of the two it is, and a claim that does is judged that way on every call. Registry claims carry the declaration in the corpus — What silence means, beside the canonical question in the claim editor — and a rule-local claim carries it on itself. Leaving it undeclared is fine and is what every claim written before this field does: the judge reads the intent from the wording, which is stable for a question that lands squarely on one side.

Declare it when the wording does not land squarely. A question can ask something of the text and something about the world in one sentence, usually because the concept genuinely has two halves:

"Does this message represent that a dwelling is not available for inspection, rental, or sale when the thread indicates it is in fact available?"

Everything up to when asks what the message says; in fact asks what is so. Both halves are real — the statute this claim encodes has a falsity element — but the judge has to pick one reading to answer under, and it picks per call. The same silent document then answers False on some runs and Unknown on others, and under the safe mark that moves the verdict without moving the document.

Two ways out, and they are not exclusive:

• Declare the reading. The question keeps its wording and every run reads it the same way.
• Reword so both halves ask the record. In adjudication the artefact under review is the record, so "…where the record also shows that the same dwelling is available" keeps the second half of the element and asks it of something the judge can actually read.

The platform will not guess for you. It does say when it cannot tell: a claim whose wording carries signals of both readings is badged Silence unsettled in the vocabulary registry, and a ruleset that reads one reports ambiguous_silence_reading in readiness, naming the words that caused it. Declaring a reading clears both.

A claim that gates a rule is chosen by which way it fails

The advice above is about meaning: which reading the claim is. There is a second question, and for one kind of claim it is the deciding one.

A claim that appears in a conjunction inside a floor — And(@ns.content, @ns.authorship) — is a claim a False answer can switch the whole floor off with. And the two readings cannot fail the same way: text answers False on silence, world answers Unknown. Under the safe mark those go in opposite directions:

The answer	What the floor does	What the mark records
True	applies	the raised level
False	satisfied vacuously	the lower level, unknown_driven false — nothing says the answer was a guess
Unknown	may apply, so the worst case is taken	the raised level, unknown_driven true, and the claim is named

So on an input the text cannot settle, text produces a silently lower mark and world produces a flagged higher one. Neither is stable there — a question the text cannot answer will waver whichever reading it carries — and stability is the wrong thing to choose on. Pick the reading whose failure you can see.

That is not an argument for world everywhere. A presence claim in an adjudication corpus is genuinely about the record, and most claims are not inside a floor's conjunction at all: for them silence is the answer and text is both truer and quieter. Ask which claims a False could switch a rule off with, and give those the reading that has to admit it does not know.

Finding them

A claim inside a floor's And(...) is the shape to look for. The corpus surfaces do not flag it for you today — it is a property of how your rules are written, not of the claim — so it is worth a pass over the floors when a verdict comes back lower than a reader expects and the claim it turned on is one the document only implies.

A numeric claim has no reading to declare, and cannot be given one in its question

A number the document does not give is Unknown, whatever the claim is about, and both numeric judge prompts say so. Writing "answer 0 if no wait is indicated" into the question does not change that — it puts a second instruction about the same case in front of the model, and which one wins is decided per call. Readiness reports this as numeric_silence_instruction. Let the claim answer Unknown and let the rule's completion policy decide what that means.

Which reading a claim has is a configuration-time fact, not a runtime one. Rewording a claim changes which reading it has, and so does declaring one — either way it is a different claim, which is one reason registry claims are versioned and immutable. Two consequences to author around:

• A rule that needs to know a fact is absent must read a claim about the text. Not(@sys.freq_band_mentioned) is satisfiable only if that claim can answer False, so phrasing it as a world claim makes the rule's antecedent unreachable on any real document.
• A rule that must not treat silence as a finding must read a claim about the world, and pair it with a completion policy that says what to do with the Unknown. A conduct claim phrased about the text answers False on a record that simply never raises the subject — which is usually right for adjudication, and is exactly wrong if you meant "we cannot rule this out".

In adjudication the artefact under review is the record, so text-shaped is right for both halves of a guideline — but for opposite reasons, and the second is easy to get backwards.

• A concern is raised by what the record alleges. A file that never raises alcohol establishes no alcohol concern, so a text-shaped claim answering False on silence is correct. Phrasing it as a world claim would put every clean file into an indeterminate bucket that a pessimistic policy then reads as a concern.
• A mitigating condition is established by what the record shows — treatment completed, abstinence maintained, time elapsed. The subject carries the burden, so a text-shaped mitigation claim answering False on silence is also correct: not shown is not mitigated. Do not author a mitigation claim as a world claim by analogy with the concern claims — silence would then read Unknown, and a completion policy that treats Unknown favourably makes silence mitigating.

What a text-shaped claim cannot tell you, and the instrument for it

A text-shaped claim collapses two different facts about a file: "this file does not allege X" and "this file investigated X and found none" both answer False. In adjudication that is the difference between a closed file and an incomplete investigation, and it is a difference a reviewer is accountable for.

The claim cannot carry it, and should not be reworded to try: the right instrument is a coverage obligation — a declared requirement that the record address the subject at all. The obligation states "the file must address alcohol"; the claim states what it says about it. Declare one for every subject a reviewer must confirm was actually examined, rather than inferring it from the presence or absence of an excerpt.

A hedged fact is still the fact; a withheld one is not

A presence claim asks whether the text gives the fact, not whether it uses the words. The two edges are worth knowing because they used to be decided by whichever reading the model reached first:

• "may operate somewhere in the vicinity of the Ku band, though this has not been confirmed by test" → True. A hedge lowers confidence in the fact; it does not remove the fact from the text.
• "operates in the [REDACTED] band", "Band: TBD", "will be specified in Annex B", "a northern latitude facility" → False. The category is named and the value is not given, which is the opposite case.

A document that recites a rule falls on the False side for the same reason: "Portions that state the operating band must be marked C" gives no band. This is the honest answer for one sentence, but it is not a general defence — a classification guide, a marking instruction or a training deck is full of example values, and the rules cannot tell such a document from a portion being marked. That is a scope question, not a claim question: tag those documents into their own scope profile so the marking rules are not in scope for them, rather than trying to phrase a claim that excludes them.

Why this matters most for marking

Under the safe mark an unanswered claim resolves to the worst case, so a presence claim that answers Unknown instead of False raises the mark. A document whose every paragraph is silent about the things a guide keys on would mark at the top of the scale — a paragraph about acceptance testing coming back SECRET. Phrase presence claims as questions about the text and they answer False, and the mark falls where the rules actually put it.

A False from an explicit denial quotes it ("No deployment site is named."); a False the judge reached because the context does not state the fact carries no excerpt. Read that as a hint, not a proof: "no excerpt" means nothing contradicting was quotable, which is not the same as the document being silent on the whole subject — a record can discuss a topic at length and still not state the particular fact a claim asks about. An Unknown that does carry an excerpt is the mirror case: the document said something the platform could not turn into a value.

A quote may never support the opposite of the answer beside it. If you see one that does, the answer is wrong, and there are three causes worth checking in this order:

1. The claim's wording — usually it asks about a narrower condition than the reader assumed ("reported for duty impaired" is not "became impaired on duty"). Fixing the claim fixes it permanently.
2. The claim's silence reading is unsettled — the wording asks something of the text and something about the world, so the judge picks one per call and the same document answers False on some runs and Unknown on others. The registry badges this as Silence unsettled and readiness reports ambiguous_silence_reading; the fix is to declare the reading, which needs no rewording.
3. The input is genuinely ambiguous — a hedged mention plus an explicit non-confirmation ("may operate somewhere in the vicinity of the Ku band, though this has not been confirmed by test") admits two defensible readings of the same question, and the answer can differ between runs on identical input even at temperature 0. Here the claim's wording is fine and re-phrasing it will not help. The contradicting quote is the tell that the answer was close, and a variance test is the instrument: it measures the instability instead of leaving you to count runs by hand.

Boolean subtypes

When a document is evaluated by streaming it in chunks, the same claim may be measured more than once. A boolean's subtype governs how those repeated measurements combine:

Subtype	Meaning
Bool.Tri	true / false / unknown; the last known measurement wins (Unknown never overwrites a known value).
Bool.Monotone	sticky: once True, a later False does not overwrite it. Bare boolean / Bool is Bool.Monotone.
Bool.Paraconsistent	conflicting True/False are recorded as a contradiction; the projected value becomes Unknown while the full both-state is preserved in attribution provenance.
Bool.Scoped	state resets per entity/section, so measurements do not bleed across scopes.

declare defaulted as Bool.Monotone;   // once defaulted, always defaulted
declare conflicting_clause as Bool.Paraconsistent;
declare early_signal as Bool.Tri;

A subtype only ever arbitrates repeated, disagreeing measurements of the same claim, so it is inert wherever a claim is measured once. That is narrower than it sounds, and worth knowing before you reach for one:

Path	Does a subtype bite?
Single-shot (batch) evaluation	No. The document is seen once, so there is one measurement and nothing to arbitrate. All subtypes behave identically.
Streaming attribution, default cumulative chunking	No. Each chunk is a growing prefix, so chunk 2 contains everything chunk 1 contained. A claim that resolved in chunk 1 has no reason to resolve differently later, so there is still one effective measurement.
Streaming attribution, windowed chunking	Yes. Sliding windows do not contain each other, so the same claim can be measured twice and disagree. You reach them two ways: ask for them with streaming_chunker_mode: "sliding", or let the chunker fall back to them for the tail of a document whose next cumulative prefix would exceed the model's context window. Flips carry attribution_mode: "windowed".
Multi-instance claims	Yes. One claim is answered per instance, and mentions folded by identity can disagree — which is what the subtype's bit-pair algebra resolves.

So on an ordinary document, batch and streaming give the same answers for every subtype, and that is expected rather than a sign that the declaration was ignored. To see a subtype do work you need repeated, disagreeing measurements — which means one of three things: a sliding-window run, an entity-scoped claim with conflicting mentions, or a document long enough to trip the windowed fallback.

That agreement is enforced rather than assumed. Both paths ask several claims in one call for speed, and a batched call answers a boolean Unknown more readily than a single-claim one does. Either path therefore re-asks such a claim on its own before accepting the answer, so a presence claim resolves the same way whichever path evaluated it. Re-asking cannot manufacture an answer: a claim about the world answers Unknown on both prompts and stays Unknown.

A sliding-window run is the one of those three to reach for when you want to see the difference, because it needs no special document and no long one. Put a claim's assertion near the start of a document and its denial near the end, far enough apart that no single window holds both, and run with a window narrow enough to separate them:

{
  "streaming_attribution": true,
  "streaming_chunker_mode": "sliding",
  "streaming_chunker_window_size": 10,
  "streaming_chunker_overlap": 2
}

Four claims that differ only in subtype then answer the same question four different ways: Bool.Monotone keeps the first True, Bool.Tri and Bool.Scoped take the later False, and Bool.Paraconsistent reports Unknown with contradiction: true on the flip. The same document under the default cumulative chunker gives True on all four, because each prefix contains the last and nothing ever disagrees.

Collections

Collections — arrays and sets — hold author-supplied reference data: thresholds, allow-lists, code lists, and category tables that you, the rule author, know when you write the rule. Their members must be known at compile time, so a collection is never the place to gather values the document supplies. That is a deliberate, permanent split:

The value comes from…	Use	Example
You (the rule author) — known when the rule is written	a declare local set/array + let	an approved-vendor allow-list, a threshold table
The document — however many times it says it	a scalar claim + a multi-instance quantifier	every interest rate stated, each loan described

// author-supplied reference data — known at compile time
declare local certified as set of enum;
let certified = {"acme", "globex", "umbrella"};

// document-supplied multiplicity — discovered per document
declare mentionedVendor as enum;
assert all_certified { ForAll(v in mentionedVendor, IsMember(v, certified)) };

Name document-supplied claims in the singular

A plural name like mentionedVendors pulls you toward the collection form — but a claim you quantify over should be singular (mentionedVendor). The multiplicity comes from the answers the document supplies, not from the claim's type: the claim still declares one vendor, and the quantifier ranges over however many the document names.

Arrays are declared with typed keys and typed values, functioning as ordered maps. Each key must be unique.

declare myPrices as array[numeric] of numeric;

let myPrices[0] = 10.99 "";
let myPrices[1] = 20.50 "";

assert priceCheck {
  myPrices[0] < myPrices[1]
};

Sets hold an unordered, duplicate-free group of typed elements, used with quantifiers and membership checks. Like every collection, a set's members are let-bound reference data known at compile time — not values pulled from a document.

declare local tenantIDs as set of numeric;
let tenantIDs = {101 "", 102 "", 205 ""};

assert allPositiveIDs {
  ForAll(x in tenantIDs, x > 0 "")
};

Collection members must be known at compile time

The compiler requires every set and array to have a known, finite membership: declare the collection with declare local and bind its members with let statements (or a literal), as in the examples above. A set or array whose members would come from document extraction does not compile. To reason about a value that occurs multiple times in a document (e.g. several interest rates), use multi-instance quantification over a scalar claim instead.

Membership over extracted values. The canonical set policy — "every value found in the document must be on an approved list" — combines the two: quantify over the extracted claim, and test each value against a compile-time-known set with IsMember. The binder is the extracted value; the set is your let-bound constant:

declare approvedVendor as enum {"acme", "globex", "umbrella", "initech"};
declare local certified as set of enum;
let certified = {"acme", "globex", "umbrella"};

assert every_vendor_certified {
  ForAll(v in approvedVendor, IsMember(v, certified))
};

IsMember(binder, S) inside a quantifier is shorthand for Or(binder == s1, binder == s2, ...) over S's known members, so S must still be compile-time-known (a literal, a set operation, or a let-bound set) — a set whose members are themselves extracted is rejected.

Declarations

Use declare to introduce a typed variable. Undeclared variables cannot be used in assertions or assignments.

declare myBool as boolean;
declare myNumber as numeric;
declare myEnum as enum;

An unbound variable (one without an assignment) can unify to any value of its declared type. This is how DSAIL handles variables whose values come from LLM question-answering at run time.

Local Variables

Use declare local to create intermediate variables that are not turned into questions or claims. Local variables are typed and usable in expressions and assertions, but the platform will not ask about them or try to populate them at inference time.

declare local ageThreshold as numeric;
let ageThreshold = 18 "";

declare applicantAge as numeric;
assert ageRequirement [pessimistic] { applicantAge >= ageThreshold };

In this example, ageThreshold is a fixed constant used in the assertion — there is no reason to generate a question for it. applicantAge is a regular declaration, so the platform will generate a question asking for its value.

When to use declare local:

• The variable's value is fully determined by a let assignment
• The variable is an intermediate computation combining other variables
• The variable serves as a named constant and should not generate a claim

When to use regular declare:

• The variable's value comes from user input or document extraction
• The platform should generate a question for this variable

Assignments

Use let to assign a default value to a declared variable. If no assignment is provided, the solver treats the variable as unknown.

let myBool = true;
let myNumber = 42 "";
let myEnum = "Large";

Assertions

A rule contains one or more named assertions. Each assertion's result (TRUE, FALSE, or UNKNOWN) is reported individually, and the rule is read as compliant when all of its assertions hold — assertions are not implicitly AND-ed into a single value.

Define an assertion with assert <name> { <formula> }:

assert myRule {
  And(myBool, Not(false))
};

Assertion names are scoped to their rule, so the same name (e.g. ok) may be reused across different rules without collision; an unnamed assert is auto-named assertion_N. Assertion names appear in Runs results and are used as column headers in Datasets ground truth CSVs.

Completion Policies

When unbound variables (those not assigned a value by LLM answers or let statements) prevent the solver from reaching a definitive TRUE or FALSE, the assertion result is UNKNOWN. Completion policies control how an UNKNOWN assertion result is resolved:

neutral (default)

The assertion result remains UNKNOWN.

pessimistic

An UNKNOWN assertion result is treated as FALSE (violation).

optimistic

An UNKNOWN assertion result is treated as TRUE (passing).

Specify a completion policy per assertion using square brackets:

declare age as numeric;

// Default (neutral): UNKNOWN result stays UNKNOWN
assert AgeCheck {
  age >= 18 ""
};

// Pessimistic: UNKNOWN result becomes FALSE
assert SafetyCheck [pessimistic] {
  safety_score > 0.8 ""
};

// Optimistic: UNKNOWN result becomes TRUE
assert BestEffortCheck [optimistic] {
  optional_field != ""
};

Logical Operators

DSAIL provides standard logical operators:

Operator	Description
And(expr1, expr2, ...)	True if all expressions are true
Or(expr1, expr2, ...)	True if at least one expression is true
Not(expr)	Logical negation
Xor(expr1, expr2)	True if exactly one expression is true (exclusive or)
Implies(expr1, expr2)	Logical implication — true unless expr1 is true and expr2 is false
If(cond, then, else)	Returns then when condition is true, otherwise else. Both branches must be the same type

assert rule_with_logic {
  And(
    myBool,
    Or(Not(myBool), true)
  )
};

declare isInScope as boolean;
declare requiresFullReview as boolean;
declare requiresPartialReview as boolean;

assert reviewRequired {
  If(isInScope, requiresFullReview, requiresPartialReview)
};

Relational Operators

Operator	Meaning
==	Equality
!=	Inequality
<	Less than
>	Greater than
<=	Less than or equal
>=	Greater than or equal

== and != apply to every type. The four ordering operators apply to numerics and to ordered enums — the latter against a quoted label of the enum's own domain, read in declared order (see Enums) — and are a rejected anywhere else — on a boolean, on an unordered enum, or between two enum claims. Corpus verification refuses those before a run; what the production path does with them instead is in Enums.

assert numeric_check {
  myNumber <= 100 ""
};

assert equality_check {
  mySymbol == "Apple"
};

Comparisons are binary. Chained comparisons such as 0 < a < 10 are a compile error — write the conjunction explicitly:

assert range_check {
  And(0 "" < a, a < 10 "")
};

Relational operators bind more loosely than arithmetic, so x + 1 "" == 2 "" means (x + 1) == 2.

Arithmetic

DSAIL supports standard arithmetic on numeric types:

Operator	Description
+	Addition
-	Subtraction
*	Multiplication
/	Division (real division only)
%	Modulo (remainder after division)
- (unary)	Negation

All operations are strictly typed. Mixing incompatible types (e.g., a numeric and a boolean) is not allowed.

declare baseRent as numeric;
declare surcharge as numeric;
declare tax as numeric;
declare totalRent as numeric;

let baseRent = 1200.0 "";
let surcharge = 150.0 "";

let totalRent = (baseRent + surcharge) * tax;

assert rentWithinLimit {
  totalRent <= 1400.0 ""
};

Conditionals: IF and CASE

IF and CASE are conditional expressions that compile to boolean comparators (not assignments):

// IF cond THEN a [ELSE b] END
assert rate_cap {
  IF rate_type == "floating" THEN rate_cap <= 0.05 "" END
};

// CASE subject OF label: expr, ... [DEFAULT: expr] END
assert maturity_ok {
  CASE instrument_type OF
    "bond": maturity <= 10 "years",
    "loan": maturity <= 5 "years",
    DEFAULT: maturity <= 2 "years"
  END
};

These are distinct from the If(a, b, c) ternary, which selects a value.

Quantifiers

ForAll and Exists quantify over a set using an explicit x in set binding. They are ordinary boolean clauses — like And / Or / Not — written inside an assert:

declare local approvedVendors as set of enum;
let approvedVendors = {"acme", "globex", "initech"};

assert all_active { ForAll(x in approvedVendors, isActive(x)) };
assert any_active { Exists(x in approvedVendors, isActive(x)) };

Counting quantifiers count how many elements of a set satisfy a predicate:

declare local vendors as set of enum;
let vendors = {"a", "b", "c"};

assert at_least_two_active { AtLeast(2 "", v in vendors, isActive(v)) };
assert exactly_one_primary { ExactlyOne(v in vendors, isPrimary(v)) };
assert count_match { CountWhere(v in vendors, isActive(v)) == 2 "" };
// AtMost(n, x in set, P(x)) is also available.

Multiple Answers (multi-instance)

Always available

Multi-instance rules are part of the language, not a capability a deployment opts into: whether a ruleset is multi-instance is decided by whether its DSAIL declares an entity, and by nothing else. They evaluate everywhere ordinary rules do — ruleset test runs and batch runs.

This section is the detail behind One thing, or several?. The contract in one line: a plain claim is one answer per document, and several separate things of one kind need an entity.

Declaring an entity names a kind of thing. You never list the instances — how many the document describes, and which ones, is discovered when the document is read:

declare Loan as entity;               // there are N of these, discovered per document
declare amount as numeric of Loan;    // extracted once PER LOAN
declare is_secured as boolean of Loan;

assert cap { ForAll(l in Loan, amount[l] <= 950000 "USD") };

Repeated statements of the same answer about the same instance are de-duplicated; conflicting statements about the same instance surface as an ambiguous rule outcome rather than being silently resolved in favour of one of them.

This is the other half of the Collections split: a collection holds reference data you supply, while an entity scope ranges over whatever the document supplies. Keep each entity claim singular — the multiplicity lives in the instances, not in the claim's type.

Nothing is vacuously true

If a document yields no instances of a scope, its rules resolve Unknown — not "every loan complies". Extracting no loans is not evidence that the document describes none, and a clean verdict on a document nobody could read is the one answer worth less than no answer.

Legacy: quantifying over a plain claim

Older rulesets quantify directly over a claim — ForAll(r in interest_rate, r <= 5.0 "percent") — treating its answers as the population. This still evaluates, so existing rulesets keep working, but prefer an entity for new rules: of <Entity> is what ties an instance's claims to each other, which is the thing a bare claim quantifier can never express. A rule about loan amounts written this way cannot also ask whether that same loan was secured.

How the pieces fit

• declare <Name> as entity; names a kind of thing. You never list the instances — how many loans a document mentions, and which ones, is discovered at evaluation time. Instances are numbered and tracked automatically, the way array elements get positions.
• of <Entity> binds a claim to the kind. Claims without a binding stay document-scalar — both forms coexist in one ruleset, and a single rule may use both.
• Inside an entity quantifier the binder is a handle: reference the instance's claims through it (amount[l]). That is what lets one rule relate an instance's claims to each other — amount[l] and is_secured[l] are the same loan.

What you can write inside an entity scope

The whole language. An entity-quantified assertion is an ordinary DSAIL expression in which claims are read through the binder:

declare Loan as entity;
declare amount as numeric of Loan;
declare collateral as numeric of Loan;
declare status as enum ["performing", "watch", "default"] of Loan;
declare local reviewed_states as set of enum;
declare portfolio_signed_off as boolean;

let reviewed_states = {"performing", "watch"};

// Arithmetic on an entity claim
assert headroom { ForAll(l in Loan, amount[l] * 2 <= 5000000 "USD") };

// One instance's claims compared against each other
assert secured { ForAll(l in Loan, collateral[l] >= amount[l]) };

// Counting, and negation
assert few_defaults { CountWhere(l in Loan, status[l] == "default") <= 1 "" };
assert none_default { Not(Exists(l in Loan, status[l] == "default")) };

// Set membership against a collection you supplied
assert all_reviewed { ForAll(l in Loan, IsMember(status[l], reviewed_states)) };

// A document-scalar claim and an entity quantifier in the same rule
assert signed_off_and_capped {
    And(portfolio_signed_off,
        ForAll(l in Loan, amount[l] <= 950000 "USD"))
};

Quantifiers available over an entity scope: ForAll, Exists, AtLeast, AtMost, ExactlyOne, and CountWhere.

The one thing that does not apply to an entity scope is length(): the instance count is not known until the whole document has been read, so there is no set whose length you can take. Express cardinality with the counting quantifiers instead.

IsMember(claim[l], S) requires S to have compile-time-known membership — a let-bound local set, a set literal, or a Union/Intersect/Difference over those. A set that is itself extracted from the document has no known members to compare against. IsSubset is not extended to entity claims.

Worked example: loan portfolio caps

Suppose a credit memo reads (abridged):

"Loan L-101 was originated in March with a principal of $400,000. It is fully secured by collateral. … Loan L-207 carries a principal of $1,200,000 and is unsecured. …"

against this ruleset:

declare Loan as entity;
declare amount as numeric of Loan;
declare is_secured as boolean of Loan;
declare status as enum ["performing", "watch", "default"] of Loan;

assert cap          { ForAll(l in Loan, amount[l] <= 950000 "USD") };
assert any_secured  { Exists(l in Loan, is_secured[l]) };
assert few_defaults { AtMost(1 "", l in Loan, status[l] == "default") };

Evaluation discovers two Loan instances and extracts each claim per loan:

	amount	is_secured	status
Loan #1 (L-101)	400,000 USD	true	—
Loan #2 (L-207)	1,200,000 USD	false	—

• cap resolves NO — Loan #2 violates, and the verdict is attributed to the sentence stating the $1,200,000 principal. Note the counting subtlety: ForAll cannot resolve YES until the whole document has been read (a later page could still introduce a third loan), but one violation resolves NO immediately.
• any_secured resolves YES as soon as Loan #1's collateral sentence is seen — Exists can conclude early.
• few_defaults resolves YES at end-of-document: neither loan's status is "default", and no further loans can appear.

If the document had stated two different amounts for the same loan, that conflict is not silently resolved: the rule outcome is surfaced as ambiguous, with both statements attributed.

If a rule will also be compiled to a grail

Nothing above restricts how rules run. Every construct in this section evaluates on ruleset test runs and batch runs alike.

Advanced: identity keys

Instance identity is automatic — you never declare it. The one optional refinement is marking a claim as an identity key when your documents happen to carry a reliable per-instance identifier that the policy already extracts (in practice a numeric one, e.g. a loan number):

declare loan_number as numeric of Loan identity;

An identity key never carries two values for one instance, so conflicting values are treated as evidence that two distinct instances were conflated, and the platform separates them — which keeps counting rules (AtMost, ExactlyOne) honest. If no natural identifier exists in your documents, omit this entirely; never add a claim just to serve as an identity key.

Set Operations

IsMember / IsSubset test set membership and containment; Union, Intersect, and Difference build new sets at compile time (zero runtime cost). Set operations are accepted only in the container-argument position of IsMember and IsSubset — e.g. IsMember(x, Union(a, b)) — or nested inside another set operation. They are not general expressions: using one in any other position, such as length(Intersect(a, b)), is a syntax error.

Operator	Description
IsMember(elem, set)	True if the element is contained in the set
IsSubset(subset, set)	True if every element of the first set is also in the second
Union(a, b)	The set of elements in either a or b
Intersect(a, b)	The set of elements in both a and b
Difference(a, b)	The elements of a not in b

declare selectedVendor as enum;
declare local approvedVendors as set of enum;
let approvedVendors = {"initech", "hooli"};
declare local certifiedVendors as set of enum;
let certifiedVendors = {"acme", "globex"};

assert vendor_ok {
  IsMember(selectedVendor, Union(approvedVendors, certifiedVendors))
};

Both sets are declare local with let-bound members — set members must be known at compile time (see the Collections note); the extracted claim here is the scalar selectedVendor being tested for membership.

Functions

Functions take one or more arguments (each an expression) and require a body:

function withinTolerance(actual: numeric, target: numeric) returns boolean = {
  actual <= target + 1 ""
};

A function's return type must match the type of its body expression, parameters are scoped to the function, and recursion (direct or mutual) is rejected — DSAIL compiles to an acyclic graph.

Built-in Functions

Function	Description
length(collection)	Returns the number of elements in an array or set

declare local lineItems as array[numeric] of numeric;
let lineItems[0] = 12.50 "";
let lineItems[1] = 8.75 "";

assert hasLineItems {
  length(lineItems) > 0 ""
};

As with all collections, the array's entries must be let-bound — length counts the members of a collection that is fully known at compile time.

Complete Example

This example shows a compliance scenario checking Section 8 housing policy:

declare landlordMentionedPreferNoSection8 as boolean;
declare landlordMentionedAdvertisingNoSection8 as boolean;
declare landlordStatedProposedRent as numeric;
declare localMarketAverageRent as numeric;

let localMarketAverageRent = 1000.0 "";

assert fact_mandatory_acceptance [pessimistic] {
  Not(
    Or(
      landlordMentionedPreferNoSection8,
      landlordMentionedAdvertisingNoSection8
    )
  )
};

assert fact_rent_reasonableness [pessimistic] {
  landlordStatedProposedRent <= (localMarketAverageRent * 1.1 "")
};

In this example:

• Two boolean variables capture whether the landlord expressed refusal of Section 8
• A numeric variable captures the proposed rent, compared against 110% of market average
• Both assertions use [pessimistic] completion policy — if the LLM cannot determine whether the landlord refused Section 8, the assertion fails (safe default for compliance)
• The localMarketAverageRent default of 1000.0 can be overridden at run time by external input

The DSAIL Editor

The platform includes a built-in DSAIL editor within Ruleset Studio that provides syntax highlighting and error feedback while writing or modifying code.

The platform can also generate DSAIL code automatically from natural language rules using the ruleset creation wizard. Generated code can be reviewed and manually edited in the editor.

Working with registry claims in the editor

Registry claims are coloured differently from rule-local names, so the shared vocabulary is visible at a glance without reading the ids.

Typing @ in a declare offers the registry claims in scope. Suggestions are matched against both the claim id and its gloss — so a claim can be found by what it means, not only by what it is called — and each row shows the claim's type alongside a snippet of its gloss. Accepting one completes the whole declaration, including the registry's own type:

declare @fh.steering_language as boolean;

The same claims are offered where a name is referenced inside an assertion, and hovering one shows its gloss and its canonical extraction question. A claim the rule already declares is not offered a second time in a declare, only where it would be referenced.

Opening a registry claim in the claim editor shows that question in a read-only field labelled as the shared vocabulary's, alongside the name and type, which are read-only for the same reason. Context, options and input slot stay editable: those are how this rule uses the claim, not what the claim means.

Promoting a local claim into the vocabulary

A claim declared without the sigil is private to its rule: no other rule can name it, and two rules that declare the same local name are two unrelated claims that merely look alike. Promote to vocabulary, in the claim editor, registers such a claim in the shared registry and rewrites the rule — its declaration and every reference — to the @ form.

Promotion asks for the namespace and id (defaulted from the local name), a gloss, and a canonical question. The gloss and question are required: they are how another author recognises the claim and how every rule that adopts it gets the same answer. Once promoted, the question is the registry's — the rule that promoted it reads it like any other reference, and further rewording happens in Corpus → Vocabulary. The type is inferred from the declaration. A newly registered claim starts at vetting draft, because a claim minted from one rule has been reviewed by nobody.

If the id is already taken, the editor says so rather than minting a near-duplicate:

• Same type and domain — the existing claim is shown, and the rule can adopt it. Nothing is registered and the existing definition is unchanged; this rule simply starts naming it.
• Different type or domain — both definitions are shown and neither path is offered, because a rule declaring a type the registry disagrees with does not compile. Choose another id, or correct the declaration.

Promotion changes only the rule being edited. Other rules declaring the same local name are listed but left alone — each rule is validated and versioned on its own. Once the claim exists, promoting the same local in one of those rules offers the adopt path instead of registering a second claim.

Related Concepts

• Rulesets contain the rules where DSAIL code lives — each rule in a ruleset has its own DSAIL program
• Runs execute rulesets and show per-assertion results from DSAIL evaluation