Language Reference

This is the contract lookup for Verdict policy source (.vd) and shared textual query syntax. For explanations, start with Predicates, rules, and facts; for reported errors and warnings, use Policy Diagnostics.

• Predicates and statements
• Values and types
• Operators and binding
• Attribute access
• Profiles and negation
• Lexical forms
• Textual queries

Predicates

A predicate is identified by its name and number of terms (arity). Supported arities are one through three. member(user, organization) and member(user, role, organization) identify distinct predicates.

A concrete predicate states a fact. A predicate containing variables describes matches used by a rule or query. A predicate does not return a function result.

Statements and declarations

Rules

owner_read: allow(user: User, "read", document: Document) if
  is_owner(user, document);

The head precedes if; the body contains conditions after it. An optional label before the head identifies the rule in diagnostics and explain traces. Multiple rules for one predicate supply alternative derivations. Rule order does not determine precedence between grants.

Static policy facts

A bodyless statement with concrete values is a static policy fact:

is_owner(User:alice, Document:handbook);

A bodyless statement containing variables is invalid. Duplicate concrete policy facts are validation errors. Static facts are part of the published policy; changing application facts normally belong in the server’s fact store.

Rules derive conclusions during checks and queries. Those conclusions are not inserted as application facts into the fact store. Predicates, rules, and facts explains that distinction.

Fact type declarations

declare is_owner(User, Document);
declare has_attribute(user: User, "clearance", level: int);
declare metadata(Document, string, *);

A declare declaration documents expected inputs and helps tooling recognize declared predicate names and arities. Declarations are allowed at the root or inside a test scope; file-start ordering is conventional rather than syntactically required. A declaration does not assert data, enforce slot types on rule calls, constrain runtime fact writes, or prevent rules deriving the same predicate.

Each declaration has one to three slots:

Slot form	Meaning
User, Document	Expected identity type
int, string, boolean	Expected primitive type
primitive	Any primitive value
*, _	Any value
user: User, value: *, bare value	Optional documentation label with a constraint, or any value for a bare label
"clearance", 42, true, User:alice	A concrete expected value

A documentation label must be unique within its declaration. Repeating item in declare pair(item: Document, item: Document); is invalid; declaration labels do not correlate slots as rule variables do. Labels may qualify types or wildcards, not literal values.

Multiple declarations with the same name and arity document alternative shapes. Different arities still identify different predicates.

Inline test blocks

test "owners can read" {
  is_owner(User:alice, Document:handbook);
  assert allow(User:alice, "read", Document:handbook);
  assert not allow(User:bob, "read", Document:handbook);
}

Each test scope inherits root declarations and adds regular fact clauses, conditional rules, declarations, queries, assertions, and fact transitions. Local declarations are initialized before imperative statements execute. Open assertions support equals { ... } and contains { ... } comparisons over complete sets of ground predicates; not negates the comparison, and a trailing query ? is optional. Expected set literals must be ground. Tests execute in isolated runtime state; root queries, assertions, mutations, and sibling tests do not affect them. Test bodies are excluded from published clauses.

See Testing & Validating Policies for the workflow and the CLI test reference for runner options.

Fact transitions

Standalone programs and inline tests can change asserted facts in execution order:

test "replace an owner" {
  is_owner(User:alice, Document:handbook);
  commit {
    delete is_owner(User:alice, Document:handbook);
    is_owner(User:bob, Document:handbook);
  }
  assert is_owner(owner, Document:handbook) equals {
    is_owner(User:bob, Document:handbook)
  };
  delete is_owner(User:bob, Document:handbook);
  assert not is_owner(owner, Document:handbook);
}

A commit block contains only ground fact insertions and ground delete statements. Empty commits are valid. Each commit executes atomically, with all deletions before all insertions regardless of their source order. Inserting the same fact more than once is idempotent; deleting an absent fact succeeds. Deleting and inserting the same fact leaves it present.

A standalone delete is an atomic single-fact deletion. Deletion removes asserted facts, including initial bare facts, without changing rules that may still derive the predicate. Bare facts and rules initialize the scope before its imperative statements execute, even when declared later in the source.

Mutation arguments must be concrete values or identities. Variable and wildcard patterns, dynamic rules, declarations, queries, assertions, labels, tags, and nested blocks are not supported inside commits. commit(...) and delete(...) remain ordinary predicate calls.

Published policies reject root commit and delete statements. Inline test mutations are admitted and excluded from published clauses.

Read-only query blocks

Use query { ... } to evaluate temporary facts and rules against the enclosing program’s current state. A block can have a label, such as snapshot: query { ... }.

owns(User:alice, Document:handbook);
test "temporary context" {
  snapshot: query {
    current_user(User:alice);
    visible(document) if current_user(user) and owns(user, document);
    selected: visible(?document)?;
    assert visible(Document:handbook);
  }
  assert not current_user(User:alice);
}

Blocks inherit enclosing rules and the facts present after preceding commits and deletes. Local ground facts, arbitrary valid conditional rules, and advisory declarations initialize before local queries and assertions. Local additions disappear on exit. Commits, deletes, nested query blocks, and nested tests are rejected inside a query block. Empty blocks and a trailing block semicolon are supported. Published policies reject root query blocks and exclude test-local blocks from published clauses.

Explicit labels are unique within their immediate scope; child scopes may reuse parent labels. Runtime query results use dotted label paths, such as snapshot.selected. Each scope numbers its direct queries and query blocks from zero, including explicitly labeled and empty blocks. An explicit label replaces the numeric component; other statements do not consume positions. Unlabeled queries receive automatic labels. Results remain in one flat array, and each test starts its own namespace. Source labels use identifier syntax and cannot contain dots or consist only of digits. query(...) remains an ordinary predicate call, and query remains a valid label.

Terms, values, and types

Policy terms include primitive constants, typed identities, and variables. Supported rule-body positions also accept attribute access.

Constants

Type	Literal forms and limits
string	Double-quoted text: "read", "alice@example.com"
int	Signed 64-bit decimal integer, from -9223372036854775808 through 9223372036854775807
boolean	true or false

Floating-point literals are not supported. Use integer base units where the domain needs fractional quantities.

Strings decode \" as a double quote and \\ as a backslash. Sequences such as \n, \r, and \t are not decoded as newline, carriage return, or tab escapes. A raw newline in a quoted string is invalid.

Identities

An identity is TypeName:id, pairing an entity type with a string ID:

User:alice
Document:123
User:"alice@example.com"
Team:"backend-eng"

Both the entity type and ID participate in equality. User:alice differs from Organization:alice. Document:123 has string ID "123" and differs from both 123 and "123".

An ordinary unquoted ID consists of letters, digits, and underscores and must be accepted as one identifier or integer token. Quote IDs containing other punctuation, spaces, or reserved-word spellings that are not accepted in that position. A negative integer token can also supply an ID; it remains a string. Quoted IDs use the same escaping as strings.

Variables

Form	Accepted matches
actor	Any concrete identity or primitive value
user: User	Identities of type User
level: int	Integer values
role: string	String values
active: boolean	Boolean values

Qualifiers constrain matching; they do not convert values or establish application entity existence. Uppercase User:alice is a concrete identity, while lowercase user: User is a qualified variable.

A variable’s qualifiers must agree within a scope. Variables local to separate negated scopes need not share qualifiers. See Variables and matching for correlation and equality.

Expressions and operators

Logical operators and precedence

Precedence, highest first	Operator	Behavior
1	=, !=, <, <=, >, >=	Non-associative comparisons
2	not	Prefix negation, subject to the active profile
3	and	All conditions must be true with compatible shared values
4	or	Any alternative may establish the condition

Parentheses override grouping. a or b and c groups as a or (b and c). Combining conditions explains shared requirements and alternatives.

Equality, comparisons, and variable binding

Equality and binding

= unifies its operands. It can bind an unknown variable to a concrete value or connect variables. With bound operands, their types and values must match.

action = "read"
document_org = member_org
age = user.age

Types remain distinct: 1, "1", and true are unequal, as are an identity and any primitive constant.

Inequality and ordering

Operator	Binding and comparison contract
!=	Requires bound operands; true when their types or values differ
<, <=, >, >=	Require bound comparable operands; compare matching primitive types
Ordering differing primitive types	Evaluates to false
Ordering identities	Outside the supported comparison contract; can produce execution diagnostics

Comparable primitive types include integers, strings, and booleans. Inequality and ordering filter existing values; they do not generate bindings. Source validation does not reject every mixed-type ordering expression.

A concrete check supplies head-variable values. Other values can come from positive facts or equality. An open query needs a supported source of the values it returns: a head-only variable that accepts a concrete input does not enumerate an arbitrary domain.

Attribute access (variable.attribute)

Dot access reads has_attribute(variable, "attribute", value) facts. Each occurrence is independent, so repeated accesses can match different stored values. Bind once and reuse the variable when several conditions must test the same selected value. Missing data supplies no implicit default.

Form or location	Support
user.clearance >= document.required_clearance	Supported in a rule body
accepted_domain(user.email_domain)	Supported predicate term in a rule body
age = user.age	Supported binding in a rule body
User:alice.clearance	Unsupported receiver; use a bare variable
user.profile.email	Chained access is unsupported
Standalone if document.archived;	Invalid; compare explicitly with true or false
Rule heads, test facts/assertions, textual queries	Dot access is unsupported

The receiver is an unqualified variable, and the key after the dot is a lowercase-initial identifier. Dot access always uses has_attribute/3; another arity does not supply these values. It does not impose stored uniqueness. See Attribute access for the independent-lookup and bind-once examples.

Profiles, negation, and validity

Validation settings

File-wide directives use line comments:

// @verdict:validate profile=authorization negation=fact_only strict_arity=warn

Setting	Values	Authorization default	General default
profile	authorization, general	authorization	Selected explicitly
negation	fact_only, unrestricted	fact_only	unrestricted
strict_arity	warn, off	warn	off

For each setting, a corresponding host override takes precedence over a source directive, which takes precedence over the effective profile’s default. Each source key may appear only once across the file. Invalid or duplicate directives remain errors even when a host overrides their values.

strict_arity controls only the mixed-arity warning. The general profile does not disable all semantic checks or editor/CLI heuristic lints.

Terminal authorization predicates

Under authorization, authorize is reserved. allow and deny can appear in heads, declarations, and tests, but cannot be referenced in rule bodies. Extract shared conditions into an ordinary helper.

Verdict Server evaluates authorization checks by testing whether allow(actor, action, resource) holds and no matching deny(actor, action, resource) holds:

authorize(actor, action, resource) if
  allow(actor, action, resource) and
  not deny(actor, action, resource);

A matching deny/3 overrides all matching grants. If no deny matches, a matching allow grants access. When a policy defines no deny/3 rules, Verdict evaluates allow/3 directly. Raw predicate queries (query allow(...)) report grants independently without applying deny precedence.

Stored-only negation

Negation generally requires the absence of a matching fact or derivation. Under fact_only, each not must apply directly to a stored-fact predicate with no derivation rule for that name and arity:

allow(user: User, "edit", document: Document) if
  is_owner(user, document) and
  not is_archived(document);

Negated compounds, comparisons, and derived predicates are rejected in this mode. Concrete static policy facts do not count as derivation rules. Adjacent double negation is normalized before applying the restriction.

unrestricted permits broader negation, subject to semantic binding and execution constraints. Verdict Server fixes the authorization profile and selects its configured negation mode, defaulting to fact_only. A source profile=general directive does not bypass server intake. See server policy admission for VERDICT_POLICY_NEGATION.

Variable safety in negation and bodyless rules

Bodyless variables are errors. In rules with a body, head variables may receive values from a concrete check even if no positive body condition supplies them.

Source validation checks that comparisons inside a negated scope have binding sources. A positive predicate within that scope can establish a local value, but local values do not become outputs outside the negation. Passing source validation alone does not establish that an arbitrary fresh-local negation shape is supported by the runtime. Use values captured from the concrete check or positive surrounding conditions for portable server authorization rules.

Negation and missing facts explains missing data and explicit false. Policy Diagnostics lists errors and warnings; Testing & Validating Policies explains the CLI warning gate and verification workflow.

Lexical rules and conventions

Identifiers and casing

Construct	Accepted identifier form	Suggested style
Predicate, variable, rule label	[a-z][a-zA-Z0-9_]*	snake_case
Entity type	[A-Z][a-zA-Z0-9_]*, excluding reserved primitive spellings	PascalCase

Reserved words and rejected type spellings

if, and, or, not, true, and false are reserved keywords. fact, test, and assert have contextual roles for declarations, test blocks, and assertions.

Use canonical primitive type qualifiers:

Canonical type	Rejected alternatives
int	Int, Integer, integer, Number, number
string	String
boolean	Boolean, Bool, bool

Reserved primitive spellings cannot be repurposed as entity types. primitive is supported as a declaration constraint, rather than a rule-variable qualifier.

Comments and semicolons

Line comments begin with //. Trailing semicolons are optional; the policy parser accepts adjacent complete statements without them. The formatter adds semicolons.

When continuing a rule across lines, place if, and, and or at the end of the line they continue. Formatting is available through verdict fmt.

Shared textual query syntax

The language package’s textual query parser is shared by CLI queries and server textual search. It accepts one predicate with one to three terms and an optional trailing semicolon. It does not accept a rule body or attribute access.

Query term	Meaning
User:alice, "read", 42, true	Concrete identity or primitive constant
?document or document	Named variable matching any value
?document:Document or document:Document	Named variable constrained to an identity type
?n:int, ?s:string, ?b:boolean	Named variable constrained to a primitive type
* or _	Independent anonymous wildcard
*:Document or _:Document	Independent anonymous wildcard constrained to an identity type
*:int, _:string, *:boolean	Independent primitive-constrained wildcard
?value:*	Unconstrained named variable

Repeating a named variable, as in has_relation(?x, "parent", ?x), requires equal values in those positions. Anonymous wildcards match independently, including typed anonymous wildcards. Qualifiers narrow matches and do not convert values. Requesting an output still requires a supported value source in the evaluated policy.

The operation determines whether the expression filters stored facts or evaluates derived policy results. Transport schemas belong in the REST reference; shell quoting, alternate positional forms, flags, and output belong in the CLI reference. See Enforcing Decisions & Querying for application use.