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:

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.

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;
• 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 - (`my-project.sales.orders`), each part quoted for the engine;
• ${...} 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;
• 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.

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: ...)"]

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