Verification¶

Unlike Logica, which lets the database raise errors at execution time, Synalog embeds a formal verifier that catches issues at compile time before any SQL is generated, and before anything touches a database.

This matters most for AI agents: it prevents producing programs that parse correctly but fail at execution time, a common failure mode when generating SQL directly.

Checks¶

Unsafe SqlExpr¶

SqlExpr("...", {...}) injects a raw SQL string straight into the compiled query: unparsed, untyped, unverified and rarely portable across engines, defeating the guarantees Synalog exists to provide. It is reserved for the built-in library (which uses it for ArgMin/ArgMax/regex/...); user programs that call it are rejected, by the compiler as well as the verifier, so compiling without verifying is safe too:

errors, warnings = synalog.check('''
  TenMinutesAgo(timestamp:) :-
    Now(timestamp: now),
    timestamp == SqlExpr("{t} - INTERVAL 10 MINUTE", {t: now});
''')
# errors: ["Unsafe SqlExpr in rule 'TenMinutesAgo': raw SQL bypasses verification and portability"]

The safe alternative is to express the logic in Synalog. For date/time math, stay on the string→int pipeline (Substr → ToInt64 → ToString); see temporal data.

Unsafe Cast type¶

Cast(expr, "TYPE") and TryCast(expr, "TYPE") paste TYPE into the query as CAST(expr AS TYPE), unquoted. A type name is accepted only when it is a string literal of type characters (letters, digits, _, spaces and balanced (), <>, ,) — TEXT, DECIMAL(38, 2), ARRAY<INT64>. Anything else (Cast(1, "TEXT) AS x; DROP TABLE t; --"), or a non-literal like Cast(1, Upper("text"))) is refused, by the compiler as well as the verifier. The accepted grammar is proved (see Proved algorithms) to hold no character that could end the CAST(...) or start anything after it.

Ordering¶

A file whose front matter names a predicate (name: TopCustomers) is about that predicate: it is what runs, and its results are read page by page. Without @OrderBy, rows come back in whatever order the engine picks, so the same page differs between runs. The named predicate must be ordered; the file's helpers need not be, and a program without front matter is not checked.

errors, warnings = synalog.check('''---
name: TopCustomers
---
Spent(customer_id:, spent:) :- customer_id in Range(3), spent == 1;
TopCustomers(customer_id:) :- Spent(customer_id:);
''')
# errors: ['Missing @OrderBy for 'TopCustomers', the predicate this file is about: ... add @OrderBy(TopCustomers, "column"); before its rules']

Text never becomes SQL¶

A program's text reaches SQL only as values or as checked names, so no string can add a statement or change one:

• every string (a fact, a pattern for Like or search, a Format) is a literal in the engine's own escapes; on Databricks and BigQuery, whose literals take backslash escapes, a quote of the value is written \u0022, so a literal holds no quote but its own two, and whatever splits a script into statements finds its end;
• on PostgreSQL, a string with a backslash is an E'...' literal, read the same whatever standard_conforming_strings says;
• names (predicates, columns, fields) are identifiers, quoted when they are keywords; @OrderBy takes columns, @Limit a number, @Dataset a schema name of letters, digits, _ and -: anything else is refused;
• Cast(expr, "TYPE") pastes TYPE into the query unquoted; only a plain type name (TEXT, DECIMAL(38, 2), ARRAY<INT64>) is accepted, nothing that could end the cast or add a statement;
• SqlExpr, raw SQL, is refused in a program, and so is a table name that is not one: a table the program reads is a dotted path of names, or one in backticks whose parts may hold any letter, spaces and -'&#@+%:() (`my-project.sales.Ventes (2024)`), each part quoted for the engine — never what could end the quoting (", a backtick, \), make a path or a URL (/, *, ?) or name a variable ($); on Databricks, where Spark reads format.path as a file (text.secret), a two-part name whose first part is a file format (text, csv, json, parquet, ...) is refused: such a table is named with its catalog;
• ${...} in a string is text, also on Databricks, whose Spark substitutes ${var} in a statement's text before parsing it (${env:HOME}): there a dollar in a string is written \u0024, and a name holds none; a flag is read with FlagValue("name"), which gives its value as a string;
• a program reaches no file, process or service: there is no ReadFile, WriteFile or Intelligence, no @AttachDatabase, no copy_to_file, and a table name opens none: once the files given to execute are loaded, its DuckDB session reads no file, installs no extension and takes no Python variable for a table (secret.csv, "secret"."parquet"), which DuckDB otherwise does (tests/cli/test_file_access.py);
• a grounded table lives in Synalog's dataset, also when @Ground names it: a program cannot drop or replace a table elsewhere.

tests/programs/injection holds the attempts this is checked against, on every engine. The quoting of strings and identifiers is also proved (see Proved algorithms): for any text, the engine's lexer reads it back exactly and ends the literal at its closing quote.

Contradictions¶

A rule whose conditions contradict each other gives no row, which is almost always a reversed comparison or a wrong constant. The verifier reads the comparisons a rule always applies (<, <=, >, >=, ==, != between variables and constants) and warns when they can never all hold: a cycle through a strict comparison, two different constants made equal, or two values both forced equal and required to differ. A rule with a disjunction is reported only when every branch contradicts itself. Comparisons involving arithmetic or a function are left out, so a warning is always right, though some contradictions go unreported.

errors, warnings = synalog.check('''V(x:) :- x in [1, 7, 12];
C(x:) :- V(x:), x > 10, x < 5;''')
# warnings: ['Contradictory conditions: x > 10, x < 5 can never all hold, so the rule gives no row: C(x:) :- V(x:), x > 10, x < 5']

Front matter¶

Front matter is how a file says what it is: name is the predicate it is about — the one that runs — and description what that predicate's rows are, the words someone searches for to find it. A file that opens front matter must give both, as text: a missing, blank or non-text name or description is refused. The name must also be a predicate the file defines (a parse error otherwise) and orders (see Ordering). A program without front matter is not checked.

errors, warnings = synalog.check('''---
name: TopCustomers
---
@OrderBy(TopCustomers, "customer_id");
TopCustomers(customer_id:) :- customer_id in Range(3);
''')
# errors: ["The front matter has no description for 'TopCustomers': say what its rows are — in the words someone would search for (description: ...)"]

Proved algorithms¶

The algorithms behind the stratification and recursion checks, the compiler's choice of how to unfold a mutual recursion, the order a compiled program's tables run in, the contradiction warning, pagination, quoting and the Cast type-name check are written in Verus: each algorithm carries a specification that Verus proves it meets, for every input:

The type inference's intersection of two types runs too often to convert its types for a proved version: Verus proves a reference intersection the greatest common refinement of two types (it refines both, every type refining both refines it, and when there is none no type refines both), and a test checks the type inference agrees with it on 20,000 random pairs of types (cargo test --test type_intersection).

The proofs live in the verified/ crate and run with the test suite (cargo test --test verus_proofs).

Assertions¶

@Assert states what a predicate must satisfy, in first-order logic, and Synalog checks it against the data by searching for counterexamples:

@Assert(Ancestor, transitive: "∀ x y z, Ancestor x y → Ancestor y z → Ancestor x z");

The verifier rejects an assertion that does not parse, applies a predicate to the wrong number of arguments, or is stated twice, and warns about one that cannot be checked against a database. Inside a connected project, check() also runs the assertions and reports each violated one as an error. See Assertions.

Usage¶

Verification runs through check():

import synalog

bad_source = """
Test(x:, y:) :- Numbers(x:);
"""

errors, warnings = synalog.check(bad_source)
for e in errors:
    print(e)
# Unbound variable 'y' in head of rule: Test(x:, y:) :- Numbers(x:)

check() returns the errors and the warnings as two lists. No error means the program is structurally valid and safe to compile; warnings do not make it invalid.

Complete example¶

An intentionally invalid program (an unbound head variable, an unbounded self-recursion and a reserved predicate name), and everything the verifier reports for it:

# expect-errors
# This program is intentionally invalid: the verifier catches every issue
# at compile time, before any SQL is generated.
@Engine("duckdb");

Numbers(x: 1);
Numbers(x: 2);

# 'y' appears in the head but is never bound in the body.
Test(x:, y:) :- Numbers(x:);

# Unbounded recursion: no @Recursive annotation.
Loop(x:) :- Loop(x:);

# 'Num' is a built-in library predicate and cannot be redefined.
Num(n: 1);

$ synalog.check('verification.l')
5 error(s) found:
  - Unbound variable 'y' in head of rule: Test(x:, y:) :- Numbers(x:)
  - Recursive predicate 'Loop' has no base case
  - Trivial infinite loop: 'Loop' calls itself with same arguments
  - Recursive predicate 'Loop' missing @Recursive annotation
  - Reserved predicate name 'Num': it is a built-in library predicate and cannot be redefined