The Corpus

The corpus is a governed vocabulary of claims, plus the axioms that connect that vocabulary across rules written by different people from different sources. It is what lets the platform reason about your rules together — finding contradictions between two policies, marking a document at the level the rules force, or answering "what would have to change for this to be allowed" — instead of one ruleset at a time.

The insight behind it is that the durable asset is not the rules. Transcribing a rule from a policy document is cheap. Deciding that the privacy regulation's "personal data" and the retention policy's "PII record" mean the same thing is not, and nothing can compute that for you. The corpus is where that alignment work is recorded, versioned and reviewed.

Where the Corpus Lives in the Product

Three screens sit on top of the corpus. Two are in the workspace sidebar; the third is inside a project.

Everything the corpus holds is scoped to your active group, the same way documents and rulesets are.

Claims

A claim is a typed proposition about the thing under review, together with the one canonical question that answers it. It is the corpus's unit of vocabulary.

A claim as the Registry tab shows it:

data.personal_data v3 · boolean · authoritative

Information relating to an identified or identifiable natural person.

Question: Does the record contain information relating to an identified or identifiable natural person?

Linked by 4 rules: gdpr.art5_storage_limitation, retention.pii_schedule, …

Two fields carry most of the weight:

The gloss is the anti-collision field. It states precisely what the claim denotes, so that when someone later proposes a claim that sounds the same, a reviewer can tell whether it is the same. Vague glosses are how two subtly different concepts end up sharing one symbol. The gloss is also the name the claim is displayed under everywhere — in a question sentence, in a witness, in a finding — so it is written to be read.

The question is the single question generated for this claim, wherever it is used. That indirection is the point: a rule references the claim and never restates the question, so every rule that links the claim inherits the same wording. A claim with no question is not extracted from a document at all, and the corpus distinguishes two reasons for that. When a rule or axiom determines the claim it is solved-for — deliberate, and what an ordered verdict claim is. When nothing determines it, the claim is incomplete: it can take no value from any route, so every verdict that reads it is UNKNOWN. The Registry tab renders the three states as three different sentences rather than leaving a blank or calling both of the questionless ones solved-for.

See Authoring a claim for how one is created and what to get right.

Naming a claim in a rule: the @ sigil

A rule names a registry claim by its catalog id under an @ sigil — @data.personal_data. A bare identifier is always local to the rule it appears in.

This is the one piece of syntax the corpus adds to DSAIL, and it exists because without it you cannot tell the 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 a name this rule's author invented five minutes ago. The sigil makes that difference visible in the source, and the product colours it differently as well: a registry claim renders in its own colour in the DSAIL editor and in the Ruleset Studio's claims list, where a rule-local stays plain.

Three kinds of name appear in a rule, and this one rule shows 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 -- no question is asked for it

let retention_limit = 730 "days";

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

Two consequences worth stating plainly:

• A bare name can never accidentally bind to the registry. Because the sigil is the only way to reach a registry claim, an author who writes data_personal_data gets a rule-local, and gets it visibly. There is no silent capture.
• 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, and nothing is upgraded behind your back. Adopting the shared vocabulary is a deliberate edit, one rule at a time, and the editor's Promote to vocabulary action is what makes it a small one.

Typed domains

Claim types are DSAIL's: boolean, numeric and enum. A claim also carries the constraints its domain needs, which the platform compiles into the background of every query:

An ordered claim — a numeric claim restricted to whole numbers, with a range and a set of level labels — is what makes verdict levels expressible. DSAIL's relational operators then apply natively, so a rule can say @clas.portion_level >= 2 and mean "at least SECRET".

Ordered enums

Ordered is not only a numeric property. An enum claim carries its allowed values as a list, and declaring it ordered says that list is in order — which is what a rule needs to compare it at all.

(Set membership — IsMember — is one of the constructs the corpus layer does not compile at all, on either form: it ranges over instance data a design-time layer does not have. It stays available in the production evaluation path.)

Both forms give the claim its identity — a closed set of symbols the corpus builds one sort for. The ordered form grants comparison as well, and the declared order is the whole of what it means: @risk.tier >= "warn" is compiled as Or(@risk.tier == "warn", @risk.tier == "error"), expanded from the order the claim was registered with. Nothing about the labels' spelling and no hidden ordinal enters into it, so re-registering the same labels in a different order is a different domain rather than the same claim read differently — which is why the alias picker treats the two orderings as two domains.

Two shapes are refused, in the same words the rule and axiom editors use for any other type fault. An ordering operator on an unordered enum is refused saying that domain declares no ordering — not that the operator is meaningless, because whether the order is right is something only the declaration knows. Two enum claims compared against each other are refused as well: a declared order orders its own domain's labels and says nothing about how one domain's labels sit against another's, so compare each side against a label. A label the domain does not contain is refused by the name of the domain it is not in, exactly as it is for ==.

An ordered enum is not a marking target. Floors, ceilings and minimize/maximize need a scale with a range to push a verdict along, so their target has to be an ordered numeric claim; an ordered enum is a comparable domain, not a verdict level.

Versions

Claims are versioned and immutable. Changing a claim's question, type or domain appends a new version rather than editing the old one, and every reference pins the version it was written against. The Registry tab's version history expands the full list, each version with its gloss, vetting state and author.

That pinning is what makes staleness detectable. A rule that links data.personal_data@3 while the registry has moved to @4 was written against a different question, and the platform flags it as needing review rather than silently upgrading it. Nothing resolves "latest" implicitly.

Axioms

Rules from different sources use different words for the same thing. An axiom is the constraint that says so.

Axioms are ordinary DSAIL. They are not a new object type or a separate reasoning mechanism — they are more DSAIL that gets combined into the program the solver sees, the same way a ruleset already combines its rules:

// Alias: two claims are the same proposition.
assert ax_personal_data_alias {
  @gdpr.personal_data == @data.personal_data
};

// Refinement: the first claim is strictly narrower, so it entails the second.
// Read from the other end, @data.personal_data subsumes @retention.pii_record.
assert ax_pii_implies_personal {
  Or(Not(@retention.pii_record), @data.personal_data)
};

What the corpus adds around that DSAIL is governance: an id, a shape (equivalence, subsumption, disjoint or refines), a scope, an owner, a vetting state, and a human-readable summary the explanation panels render.

An axiom may also connect a claim to an expression, which is how a source's prose maps onto a canonical measurement:

// "above 10 GHz" in one guide's language, against the canonical frequency claim
assert ax_alpha_freq_meaning {
  @scg_alpha.freq_above_10ghz == (@sys.operating_frequency > 10.0)
};

Authoring an axiom walks through the editor, its live type check, and the impact preview that tells you how far a save reaches.

How the three objects relate

A claim is vocabulary. A rule is a requirement written in that vocabulary. An axiom is a statement that two pieces of vocabulary line up. Rules never reference each other; they meet only through the claims they share, and axioms are what let rules from different sources share a claim at all.

graph TD
    subgraph Source A["Privacy regulation"]
      RA["`Rule
      gdpr.art5_storage_limitation`"]
      CA["`Claim
      @gdpr.personal_data`"]
      RA -->|names| CA
    end

    subgraph Source B["Retention policy"]
      RB["`Rule
      retention.pii_schedule`"]
      CB["`Claim
      @retention.pii_record`"]
      RB -->|names| CB
    end

    CC["`Canonical claim
    @data.personal_data`"]

    AX1["`Axiom · equivalence
    ax.gdpr_personal_alias`"]
    AX2["`Axiom · refines
    ax.pii_implies_personal`"]

    CA --- AX1
    AX1 --- CC
    CB --- AX2
    AX2 --- CC

Delete the two axioms and the picture falls into two disconnected halves: the rules still evaluate, but nothing can compare them, because as far as the solver is concerned they talk about unrelated symbols.

The Canonical Namespace

Do not force every source onto shared claims. Let a privacy regulation keep its gdpr.* claims and a retention policy keep its retention.* claims, and connect them upward to a canonical namespace — by convention data.* and its siblings — with axioms.

The canonical layer is not an empty import target. It owns claims, each with its own gloss and its own single question, for the concepts that recur across sources. That is what makes the arrangement scale: with a populated hub, each source-local claim connects up to one canonical claim (n connections); without one, every local claim has to be reconciled against every other (n²).

Two ways a local claim connects up:

Alias

The local claim is equivalent to the canonical one. The local claim carries no question of its own — the question is answered once, at the canonical claim, and every equivalent local claim inherits the value when the corpus solves. (Inheritance through an axiom is design time only; what a run shares is described in Answering it once below.)

Refinement

The local claim is strictly narrower. It keeps its own question and connects up with a refines axiom — the local claim entails the canonical one, Or(Not(local), canonical). The same fact stated from the canonical end is a subsumption, whose implication runs the other way; see the shapes.

The lift is selective. Only recurring concepts are canonicalized; a notion specific to one source stays local and never connects up.

Answering it once

"Answer it once, and every equivalent claim inherits the value" is the argument for a canonical namespace. In a ruleset that runs against real documents, it is also something you can watch happen.

Write @sys.operating_frequency in fourteen rules and the run asks for the operating frequency once. Open the run, expand a document on the Evaluation tab, and all fourteen rules list that claim in their own Claims table — all showing the same value, because there was one question and one answer behind them. Give each rule a claim of its own instead, spelled the same way in all fourteen, and you get fourteen questions and fourteen answers that are free to disagree, with nothing on the screen to say that they did: each rule looks internally consistent while the ruleset as a whole is not.

That is what the sigil buys, and it is why it is worth the governance overhead of registering a claim. It is also the whole of what the corpus does at run time — see One claim, one answer for the rule author's view, including the two other things that are deliberately not folded together and the effect on model calls.

Two boundaries are worth stating plainly, because both are cases where two references that look identical are correctly treated as two claims:

• A version pin is part of a claim's identity. Two rules naming the same claim are asking one question only when their version pins agree. Pin one rule's reference to @3 while another reads the claim unpinned or at @4 and they are two claims, asked separately — the two versions may word the claim differently, and nothing silently resolves one to the other. Unpinned is its own identity, not a wildcard.
• Entity-scoped claims are answered per instance, not unified. A claim declared of <Entity> — the multi-instance form — has no single value to share: its population is enumerated per quantified scope, per rule, and each instance carries its own answer. Sharing there would mean discarding instances, so it is not done.

What this looks like in a rule

Here is the same rule as above, rewritten as a faithful transcription of the privacy regulation rather than of the canonical vocabulary:

// GDPR Art. 5(1)(e), transcribed in the regulation's own vocabulary.
declare @gdpr.personal_data as boolean;         // the source's own registry claim
declare retention_days as numeric;              // this rule's own claim
declare local retention_limit as numeric;       // an intermediate

let retention_limit = 730 "days";

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

Nothing in this rule mentions @data.personal_data. The crosswalk is ax.gdpr_personal_alias, and it lives in the axiom catalog where a reviewer can find it.

Rules in the Corpus

A corpus rule is one DSAIL assertion with governance metadata around it: an id and version, the claims it links (pinned by version), a completion policy, an authority citation, a scope, its corpus ruleset membership, and a summary — a plain sentence like "Revealing waveform X is SECRET" that the explanation surfaces render instead of showing you an identifier.

Rules additionally declare a role with respect to an ordered claim:

A rule may link registry claims or declare standalone claims of its own. Standalone is the older default and stays supported — when a standalone claim is later found to coincide with a canonical one, it is connected by an equality axiom rather than rewritten, and the original rule is left untouched.

Ordered Verdicts: Floors, Ceilings and Mosaics

Some questions a pass/fail rule cannot answer: at what level does this have to be marked? Where a normal ruleset assertion returns TRUE, FALSE or UNKNOWN, an ordered verdict returns a level on a scale — and, just as importantly, the reason it landed there.

The mechanism is general. Classification levels are the case it was built around, but any ordered verdict works the same way: a risk tier, a review level, a retention class, a violation severity.

The ordered verdict claim

One claim restricted to whole numbers, with a declared range and a label for each level:

clas.portion_level v1 · numeric · ordered · Solved-for · authoritative

The classification level at which this portion must be marked.

Solved-for — no extraction question, and never handed to extraction: its value follows from the rules and axioms that determine it.

Levels: 0 = U, 1 = C, 2 = S, 3 = TS

The absent question is deliberate. This claim is never asked of the document — its value is determined by the rules. That is what makes an ordered verdict a solving problem rather than an extraction problem.

Each level can also carry a level gloss: one sentence saying what that level means. Wherever the product shows a level — a mark chip, a level dropdown — an ⓘ beside it serves that sentence, followed by the claim's own gloss. A level the registry does not gloss shows no ⓘ at all, because an empty hover target is worse than none.

Floors and ceilings

Rules bear on the ordered claim in two directions, and both are required.

A floor raises the level when its condition holds:

// Revealing waveform X is SECRET.
assert alpha_waveform_floor [pessimistic] {
  Or(Not(@scg_alpha.item_waveform_x), @clas.portion_level >= 2)
};

A ceiling caps the level when its condition holds:

// The existence of waveform X, standing alone, is UNCLASSIFIED.
assert bravo_waveform_alone_u {
  Or(
    Not(And(@scg_alpha.item_waveform_x,
            Not(@sys.freq_band_mentioned),
            Not(@ops.deploy_location_mentioned))),
    @clas.portion_level == 0
  )
};

Rules are registered with a role of floor or ceiling and the ordered claim they bound, so the platform knows which direction each one pushes. Those annotations are what make the level determined rather than merely bounded — and a rule that reads the ordered claim without declaring a role takes that away, leaving the conflict scan to answer unknown and name the rules whose annotation is missing.

The two roles are not symmetric in how they get there. The floors compile into the definition of the level: it is the highest level demanded by a floor whose condition holds, and the bottom of the scale when none holds. A ceiling is not part of that definition — it is checked against it. At the level the floors define, a ceiling is either satisfied and therefore slack, or violated, and then no level is reported at all. There is no arithmetic in which a ceiling trims a level the floors have proved: where every claim a floor reads is answered and the floor fires, a colliding ceiling produces a reported collision, never a quietly reduced number. What a ceiling can do is settle a level the floors have not proved, and then the level it settles on can be lower — see When a ceiling decides an unknown, below the safe mark, because the safe mark is the mechanism it works through.

Where a floor and a ceiling do collide, no level is reported at all. That is the honest answer: the rules in scope disagree, and no mark is defensible until someone resolves it. Corpus Health catches the collision before any document arrives; Analysis reports it for a document in front of you.

The safe mark

A subject's mark is the level the rules force, given what is known about it. But a document rarely answers every question, and the interesting decision is what to do about the ones it leaves open.

The default is the safe mark: unknowns are resolved to the worst case. A free claim can raise the mark but can never lower it. If a document mentions a frequency band but the actual frequency is unknown, the mark assumes the frequency could be one that triggers a floor.

This is the same fail-safe reasoning as DSAIL's pessimistic completion policy, applied to a level instead of a verdict, and it is the default for the same reason: a mark that is too high is a review burden, and a mark that is too low is a disclosure.

Two other policies are available when you are asking a different question:

neutral is the useful one when you want to know whether the unknowns move the level. If it returns a level rather than UNKNOWN, every resolution of the open questions that the slice can honour gives that same level. Read it as exactly that and no more: it ranges over the resolutions the rules admit, so where a ceiling has already excluded the resolution that would have moved the level, neutral answers with a level rather than UNKNOWN. It does not hide that from you — such an answer comes back flagged unknown-driven, naming the unanswered claims it rests on — but the warning arrives as a flag beside a level, not as a refusal to answer. See When a ceiling decides an unknown.

The mark chip on the Analysis tab shows the pessimistic reading. All three policies are reachable through the Corpus API.

When a ceiling decides an unknown

Put the two halves together — floors define the level, the safe mark maximises over what is still free — and one consequence follows that surprises everybody the first time. A ceiling can lower the level the corpus reports, by more than one step, against identical evidence. It is not a trimmed floor. It is the safe mark choosing among the completions that remain.

The safe mark is the highest level reachable under some completion of the free claims that satisfies every rule in the slice, ceilings included. A completion in which a floor and a ceiling collide is not a completion: it is excluded before the maximum is taken, and the level that floor would have demanded goes with it. So when the only completion that fires a floor is also the one that fires a ceiling contradicting it, that floor can never set the level, and the maximum falls to whatever survives.

In the SCG corpus of the portion-marking tutorial, on a portion stating neither the operating band nor a deployment site, with does this reveal waveform X? left unanswered:

Answering the open question resolves the apparent paradox in whichever direction is true. Yes, it reveals waveform X is the collision: Alpha demands S, Bravo demands U, and the subject comes back contradicted with both rules named — the outcome the ceiling was encoded to produce. No, it does not is U on its own merits. The U you get while the question is open is the solver telling you that the only readings of this subject both guides can honour are ones where waveform X is absent — a fact about your rules, not about the document.

Read a low mark here as a prompt to answer that claim, never as a cap to reason around. A run and a corpus answer both flag it: a mark decided by a claim the run left unanswered is reported unknown-driven whether or not the ceiling collapsed low and high onto a single level, and assumed_claims names the claims the rules settled rather than evidence did — which is the shortest route from a surprising level to the question worth answering.

Mosaics

A mosaic rule is guidance that a combination of facts is more sensitive than any of them alone:

// The frequency band and a deployment location together are SECRET.
assert mosaic_band_location [pessimistic] {
  Or(
    Not(And(@sys.freq_band_mentioned, @ops.deploy_location_mentioned)),
    @clas.portion_level >= 2
  )
};

Two things about mosaics are worth stating plainly.

Mosaics are authored, not derived. "Unclassified plus unclassified equals secret" is not a logical consequence of anything — it is new guidance. No amount of analysis will discover it. It comes from the guide, or from a reviewer, and it lives as a rule.

The corpus is what makes a cross-source mosaic expressible at all. The two members of the rule above come from different guides' vocabularies. Without the canonical claims and the axioms connecting them, they are unrelated symbols and the rule cannot be written.

A mosaic is also the clearest case for why the subject is usually the whole document. One passage mentions the band; another names a deployment site. Each is fine alone; the document is not.

Where floors and ceilings are read. Analysis solves the mark over a finished run's values, and a ruleset that names an ordered claim as its Mark target solves the same mark during the run and returns it as marked_* assert results. Both read the floors and ceilings of the corpus rulesets in scope, under the same prove-high, default-low objective and the same safe-mark completion. A run may also carry floors of its own: an assertion in the ruleset that bounds the target joins the same program, which is what lets a ruleset carry guidance nobody has promoted into the corpus yet.

Subjects and the aggregate pass

A subject is whatever a claim value is bound to. Two shapes exist:

One document as one subject. This is what Analysis does: it binds the claim values a run extracted for the document and asks about it. A run asks its questions of the whole document, so a mosaic whose members are in different passages fires here.

Portions, plus a synthetic aggregate. The Corpus API also accepts one context per portion, each with its own claim values, and can append a synthetic aggregate context whose claims are the union of every portion's. A claim any portion states is stated by the document, so a present value displaces an absent one, and each surviving value keeps a provenance whose span names the contributing portion. That is what lets a cross-portion mosaic fire for the document while every individual portion stays clean, and lets the resulting finding point back at the portions that produced it.

The per-portion form is available through the API. The Analysis tab uses the single-subject form.

Where a document's claim values come from. They are recorded from runs. When a completed run's results are first read, every answer it gave for a registry claim becomes a claim value on that document — at the claim version the rule referenced, with origin: extracted and provenance naming the document and the run. Rule-local answers are not recorded, because a bare identifier is a claim about one rule rather than a governed corpus claim; UNKNOWN answers are not recorded, because a free claim and a claim bound to nothing are the same fact; and entity-scoped claims are not recorded, because they are answered once per instance and a claim value is one value per subject. Values can also be asserted through the API — a human statement rather than an extraction — and the two are distinguished by origin wherever they are shown.

Scopes

A scope is a context tag such as jurisdiction:EU or program:rf. Rules and axioms may carry scope tags, and a query supplies the scope it is asking under.

A request that supplies no scope tags is asking under every context, not under none: every rule, axiom and precedence decision available to the group is in the slice. That is the reading to hold on to, because the alternative — treating "no tags" as "only untagged objects" — silently empties a scope-tagged corpus, and an empty slice is trivially consistent. A "no, these rules cannot contradict each other" is a proof quantified over every possible input, and it must never be a proof about nothing.

When a request does name tags, it is naming the contexts that are loaded. An untagged rule is in scope everywhere; a tagged rule is in scope when every tag it carries is one the request named. Axioms and recorded precedence decisions follow exactly the same test — admitting a context's rules while dropping the axioms that reconcile their vocabularies would report contradictions the alignment layer exists to resolve.

Whatever the scope, a narrowed slice is disclosed on the answer. If tags excluded a rule from the rulesets you named, or a ruleset you named contributed no rule at all, the answer says so rather than presenting a clean result as a proof about rules it never saw.

Scope is what makes conflict detection contextual. An axiom tagged jurisdiction:EU is left out of any query that names some other context, so a contradiction that exists only under EU alignment does not appear under a jurisdiction:US query. Consistency is a property of a particular combination of rules and axioms, not of "the corpus" in the abstract — which is why a corpus can be clean under one program and contradictory under another, and why Corpus Health always names the scopes it checked.

The unscoped query sits at the other end of that: it is the union of every context, so it can surface a collision between two contexts that never co-occur in practice. That over-reporting is the safe direction — a false alarm a reviewer can dispose of, rather than a false proof of safety — and narrowing it is what declared scope profiles and the Analysis tab's scope tags are for.

A scope profile is a named, declared combination — a scope tag set plus the rulesets in play — that verification runs against. Profiles are declared deliberately rather than enumerated automatically, because the set of all possible scope combinations is not something anyone wants a report on.

Slices and the Slice Hash

Every corpus query resolves a slice before it does anything else. The slice is the thing the question is actually asked of, and it is narrower than "the corpus" every time.

graph TB
    Q["`**A question**
    scope tags + rulesets`"]

    subgraph Catalog["Everything in the group"]
      R1["Rules"]
      A1["Axioms"]
      C1["Claims"]
    end

    Q --> S1
    R1 --> S1
    A1 --> S1
    S1["`**1 · Scope resolution**
    keep the rules and axioms
    whose tags this question supplies`"]
    S1 --> S2
    C1 --> S2
    S2["`**2 · Claim closure**
    collect every claim reached
    through those rules and axioms`"]
    S2 --> S3
    S3["`**3 · Combination**
    rules + axioms + claim domains
    + any supplied values → one program`"]
    S3 --> H["`**Slice hash**
    the identity of this configuration`"]
    S3 --> SOLVE["The solver"]

Two details in that picture matter in practice. Claim closure runs to a fixpoint with a depth cap — a runaway closure means an over-broad axiom, and is reported as one. And the hash is a stable digest over the sorted, version-pinned rule, axiom and claim references, the scope tags, and the active precedence decisions.

That hash is the identity of a corpus configuration. It appears in every result's disclosure, it keys verification reports so an unchanged corpus is not re-verified, and it is what makes a stale result detectable: if the hash no longer matches, the answer was computed against a corpus that no longer exists.

Where Claim Values Come From

Claims are bound to values per subject, and every value carries an origin:

A claim left unbound is free, and free claims are not a failure state — they are the mechanism behind what-if questions and the safe mark. The origin tag is load-bearing: any result computed with a hypothetical input is flagged advisory and can never be presented as a determination.

Related Concepts

• Analysis — the ten questions, the two modes, and how to read an answer
• Corpus Health — static verification of the corpus against itself
• Vocabulary Workbench — the registry, the merge queue, promotion, and authoring claims and axioms
• DSAIL Language — the language claims, axioms and rules are written in, including the @ sigil
• Rulesets — the production authoring surface the corpus sits beside
• Runs — the evaluation path, which produces the extracted values the corpus reasons over, and which returns the mark for a ruleset that names an ordered claim as its target
• Corpus API — the REST surface behind every screen on this page