80 lines
3.9 KiB
Markdown
80 lines
3.9 KiB
Markdown
# datalogkit — a stratified Datalog engine, differentially verified
|
|
|
|
Wizard: **null** · Lane: Codeforge (hard coding and agentic reasoning)
|
|
|
|
`datalog.py` is a dependency-free Datalog engine: hand-written parser, static
|
|
checks (arity, rule safety, stratification), Tarjan-SCC stratification, and
|
|
**semi-naive** bottom-up evaluation with stratified negation. No imports beyond
|
|
the standard library.
|
|
|
|
## Files
|
|
|
|
datalog.py the engine (module + JSON/text CLI)
|
|
test_datalog.py the verification suite — its exit code is the verdict
|
|
evidence_run.py reproduces every number in EVIDENCE.txt
|
|
examples/reach.dl CLI demo program
|
|
EVIDENCE.txt captured output of the above (measured, not claimed)
|
|
|
|
## Run it
|
|
|
|
python3 datalog.py examples/reach.dl --text --stats
|
|
python3 datalog.py examples/reach.dl -q unreachable # JSON, one predicate
|
|
python3 test_datalog.py # 0 = all checks pass
|
|
|
|
## Language
|
|
|
|
% comment
|
|
edge(a, b). % fact
|
|
path(X, Y) :- edge(X, Y). % rule
|
|
path(X, Y) :- edge(X, Z), path(Z, Y).
|
|
unreach(X) :- node(X), not reach(X). % '!' is accepted as 'not'
|
|
|
|
Terms: `?X` variable, `?_` anonymous (independent per occurrence), bare lowercase
|
|
atom, `"quoted"` string, integer. Head and negated-literal variables must be
|
|
bound by a positive body literal; a rule with no positive body literal is
|
|
rejected. Negation must be stratified — a negated literal may not sit inside a
|
|
recursive cycle.
|
|
|
|
## Verification (this is the point of the artifact)
|
|
|
|
`test_datalog.py` = 40 tests, 0 failures. The load-bearing part is
|
|
**differential testing against an independent oracle** written from scratch in
|
|
the test file: stratification via reflexive-transitive reachability closure plus
|
|
Kahn waves (the engine uses iterative Tarjan SCC), evaluation via
|
|
cartesian-product naive fixpoint (the engine uses delta-driven semi-naive).
|
|
The two share only the parser.
|
|
|
|
| check | result |
|
|
|---|---|
|
|
| unittest suite | 40 tests, 0 failures, 0 errors |
|
|
| random programs, engine vs oracle (seeds 20261024 / 20261025) | 600 programs, 61 of them unstratified — verdicts and 3234 predicate-relations identical, 0 mismatches |
|
|
| fresh-seed re-run (evidence_run.py, seed 999) | 400 programs, 43 unstratified, 2142 relations, 0 mismatches |
|
|
| semi-naive actually saves work (chain transitive closure, 12 nodes) | 858 vs 5687 body bindings enumerated — 6.6x; at n=20, 3990 vs 47291 — 11.9x |
|
|
| KATs | transitive closure, non-linear same-generation recursion, stratified negation, anonymous vars in negation, zero-arity, repeated variables, order independence |
|
|
|
|
Numbers above are read off `EVIDENCE.txt`, which `evidence_run.py` regenerates
|
|
in one run.
|
|
|
|
## Bug this suite actually caught
|
|
|
|
The first run of the differential test failed on 1 of 300 random programs:
|
|
the engine derived `p0(c, c)` where the oracle derived nothing. Root cause: the
|
|
join reorders positive body literals smallest-relation-first, so a literal like
|
|
`p1(X, X)` can be joined *first*; the unifier bound `X` from the first argument
|
|
into a private dict while checking the second argument against the *original*
|
|
environment, so a repeated variable inside a single literal did not constrain
|
|
both positions. Fixed in `_match` (bindings are now visible to later arguments
|
|
of the same literal); the same latent flaw was removed from the oracle, and the
|
|
exact failing program is now a regression KAT
|
|
(`test_repeated_variable_inside_one_literal`).
|
|
|
|
## Stated limits (not hidden)
|
|
|
|
* String constants compare as written — no unescaping, so two spellings of the
|
|
same escaped string are distinct terms.
|
|
* `-` is a token only as part of an integer literal; no arithmetic or builtins.
|
|
* No functors, no aggregation, no `$ref`-style imports.
|
|
* The engine reports `rounds`/`bindings`/`derived`/`rule_runs`; it is not tuned
|
|
for large relations (semi-naive delta is tracked per predicate, joins are
|
|
unindexed).
|