Skip to content

DSAIL Language Guide

DSAIL is Jaxon's domain-specific language (DSL) for expressing policy constraints, logical constructs, and other rules that compile to SMT solver inputs. DSAIL is designed to validate compliance with policy requirements by checking for satisfiability (SAT) or unsatisfiability (UNSAT). Each assert statement will be tested independently to see if it holds under possible assignments of variables.

Overview

DSAIL programs consist of:

  • Version An optional version tag version 1.0;. Omitting this version tag will use the newest interpreter.
  • Variable Declarations (boolean, real, integer, symbol).
  • Optional Assignments for default, constant, or initial values.
  • Assertions (logical constraints, arithmetic, and policy rules to satisfy).
  • Optional Function Definitions to encapsulate repeated logic or more complex expressions.
  • Optional Quantifiers (forAll, exists) to express universal or existential constraints.

When compiled, the resulting formula is passed to an SMT solver to check if the constraints are SAT (i.e., they can be satisfied) or UNSAT (they cannot all be satisfied). Each assert statement can be assessed individually. Unbound variables - those not assigned using a let, not provided a value by inference-time questions, or otherwise constrained - will be assigned any value that can satisfy the global set of constraints. Pragmatically, this means that assertions "default" to being satisfied if any possible value for the unbound variables can make it so.

Basic Syntax

  • Statements end with a semicolon (;) unless enclosed in braces (e.g., the assert block).
  • Block statements are in curly braces ({ ... }).
  • Identifiers are alphanumeric and underscores (_).

Example:

version 1.0;
declare x as boolean;
let x = true;

assert myAssertion {
  x
};

Data Types

DSAIL supports the following core types:

  • boolean Represents truth values (true or false).

  • integer Represents integer values (e.g., 0, 42, -3).

  • real Represents real (floating) values (e.g., 3.14, -0.5).

  • symbol Represents fixed values (e.g., "purple"). Used primarily for enumerating collections of values that don't logically map to the above data types.

Collections

DSAIL also includes collections for grouping data:

Arrays

An array in DSAIL is declared with typed keys and typed values, much like an ordered dictionary or map. Each key must be unique, and each entry is accessible by its key.

declare myPrices as array[integer] of real;
  • Key type: In the example above, integer is the type for the array’s indices.
  • Value type: real is the type for the values.

Access is typically done within expressions or assertions by referencing myPrices[key].

Arrays may be used in quantifiers (forAll, exists) by iterating over known keys.

Example Usage

declare myPrices as array[integer] of real;

// Possibly assign a specific index:
let myPrices[0] = 10.99;
let myPrices[1] = 20.50;

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

Sets

A set in DSAIL contains a collection of typed elements without repetition. Typically used in quantifiers, membership checks, or cardinality constraints.

declare tenantIDs as set of integer;
  • Element type: integer in the above example.
  • Membership is tested through expressions like x in tenantIDs.
  • Used with forAll(x in tenantIDs, ...) or exists(x in tenantIDs, ...).

Example Usage

declare tenantIDs as set of integer;

assert hasTenants {
  // e.g., the set is not empty
  Exists(x in tenantIDs)
};

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

Both arrays and sets allow more advanced constraints (e.g., checking membership, ordering, or cardinalities) depending on the solver features. By default, they offer a straightforward means to group data for quantifier-based rules.

Declarations

Use declare to introduce a new variable and specify its type. The variable is initially unbound (unknown) unless given a default with let.

declare myBool as boolean;
declare myNumber as real;
declare mySymbol as symbol;

Purpose

  • Establishes a typed variable for later usage in assertions or assignments.
  • An unbound variable can unify to any value of its declared type.

Assignment

Use let to assign a value to a previously declared variable. This can be done any time after declare. If omitted, the solver may leave it as unknown, which can still satisfy certain constraints depending on the logic.

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

Purpose

  • Fixes a variable to a specific value.
  • Overwrites any previous assignment if repeated.

Assertions

Use assert <name> { <formula> } to express a logical formula that must hold for SAT. Each assertion can be viewed independently to check compliance with a specific policy rule.

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

Inside the braces

  • You can write logical formulas with And, Or, Not, Imply, etc.
  • If the formula is unsatisfiable, this particular assert fails.
    • Unsatisfiable means there is no possible value that unbound variables could be assigned such that a true value could be returned.

Naming

  • The <name> is an identifier to distinguish this assertion.
  • Helpful for referencing specific rule compliance in results.

Logical Operators

DSAIL provides the standard logical operators, treating them as functions/constraints akin to SMT-LIB or Z3:

  • And(expr1, expr2, ...) Returns true if and only if all expressions are true.

  • Or(expr1, expr2, ...) Returns true if at least one expression is true.

  • Not(expr) Returns the logical negation of expr.

  • Imply(expr1, expr2) Equivalent to (Not(expr1) Or (expr2)). Useful for expressing “if expr1 then expr2.”

  • Distinct(val1, val2, ...) Returns true if all arguments are pairwise different.

Examples

assert rule_with_logic {
  And(
    myBool,
    Or(Not(myBool), true),
    Imply(myBool, myNumber < 50)
  )
};

Relational Operators

Relational operators in DSAIL are typically used for numeric comparisons but also for equality checks on booleans, symbols, etc.

  • Equality: ==
  • Inequality: !=
  • Less than: <
  • Greater than: >
  • Less than or equal: <=
  • Greater than or equal: >=

These appear within assertions or function definitions, for example:

assert numeric_check {
  myNumber <= 100
};

assert equality_check {
  mySymbol == "Apple"
};

Arithmetic

DSAIL supports standard arithmetic operators that mirror those directly supported by SMT solvers like Z3. These can be used in assertions, function bodies, variable assignments, or any context involving numeric expressions.

The following arithmetic operations are available:

  • Addition: +
  • Subtraction: -
  • Multiplication: *
  • Division: / (real division only; integer division must be modeled explicitly).
  • Negation: unary -

All operations are strictly typed. Mixing incompatible types (e.g., int and boolean) is not allowed. Parenthesis for grouping are supported.

Example Usage

declare baseRent as real;
declare surcharge as real;
declare tax as real;
declare totalRent as real;

let baseRent = 1200.0;
let surcharge = 150.0;

let totalRent = (baseRent + surcharge) * tax;

assert rentWithinLimit {
  totalRent <= 1400.0 
};

Quantifiers

Quantifiers resemble those in SMT-LIB or first-order logic. They allow you to express constraints over a range or set of values (though domain usage is typically required for meaningful iteration).

  • forAll(variableName in domain, formula) States that formula must hold for every element in domain.

  • exists(variableName in domain, formula) States that there is at least one element in domain for which formula holds.

Example

declare myInt as integer;

domain intDomain = [1, 2, 3, 4]; // example domain definition

assert universal_rule {
  forAll(x in intDomain, x > 0)
};

assert existential_rule {
  exists(x in intDomain, x == 2)
};

Functions

DSAIL supports defining named functions that encapsulate custom or repeated logic. The general form:

function <name>(param1 as Type1, param2 as Type2, ...) as ReturnType {
  // Return a formula or expression
  // e.g., And(), Or(), arithmetic, etc.
};

Inside the function

You write a formula or expression that can include local references to the parameters. The function’s return type must match the expression type.

Usage Example

function isPositive(value as integer) as boolean {
  value > 0
};

assert checkPositivity {
  isPositive(myInt)
};

Example Program

Below is a more complete example illustrating various language features:

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

let localMarketAverageRent = 1000.0;

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

assert fact_rent_reasonableness {
  landlordStatedProposedRent <= (localMarketAverageRent * 1.1)
};
  • Variables declared for a compliance scenario.
  • A default value of 10000.0 set for localMarketAverageRent. Note that this value may be overridden at inference time by an external input.
  • An assertion checking that the landlord has not refused or advertised refusal of Section 8.
    • This assertion will be satisfied if landlordMentionedPreferNoSection8 and landlordMentionedAvertisingNoSection8 are both False or unbound, as assertions will seek the presence of a possible solution whenever unbound variables are involved. Intuitively, satsification is the default and programs should be "oriented" based on this intuition.
  • A rent reasonableness rule comparing the proposed rent to local average.