SQLite busy challenge

31/154 formalized, 2/154 termination proved
https://github.com/sivukhin/sqlite3-lean-proofs | Generated: 2026-01-25 19:41:59
SQL Query Formalized Termination Gas Bound PR
SELECT * FROM t yes yes 3 * n + 9 -
SELECT f1 FROM test1 yes yes 3 * n + 9 #1
SELECT f2 FROM test1 yes sorry - -
SELECT f2, f1 FROM test1 yes sorry - -
SELECT f1, f2 FROM test1 yes sorry - -
SELECT * FROM test1 yes sorry - -
SELECT *, * FROM test1 yes sorry - -
SELECT *, min(f1,f2), max(f1,f2) FROM test1 sorry sorry - -
SELECT 'one', *, 'two', * FROM test1 yes sorry - -
SELECT * FROM test1, test2 sorry sorry - -
SELECT *, 'hi' FROM test1, test2 sorry sorry - -
SELECT 'one', *, 'two', * FROM test1, test2 sorry sorry - -
SELECT test1.f1, test2.r1 FROM test1, test2 sorry sorry - -
SELECT test1.f1, test2.r1 FROM test2, test1 sorry sorry - -
SELECT * FROM test2, test1 sorry sorry - -
SELECT * FROM test1 AS a, test1 AS b yes sorry - -
SELECT max(test1.f1,test2.r1), min(test1.f2,test2.r2) sorry sorry - -
SELECT min(test1.f1,test2.r1), max(test1.f2,test2.r2) sorry sorry - -
SELECT * FROM t3; yes sorry - -
SELECT count(f1) FROM test1 yes sorry - -
SELECT Count() FROM test1 sorry sorry - -
SELECT COUNT(*) FROM test1 sorry sorry - -
SELECT COUNT(*)+1 FROM test1 sorry sorry - -
SELECT count(*),count(a),count(b) FROM t3 yes sorry - -
SELECT count(*),count(a),count(b) FROM t4 yes sorry - -
SELECT count(*),count(a),count(b) FROM t4 WHERE b=5 yes sorry - -
SELECT Min(f1) FROM test1 sorry sorry - -
SELECT MIN(f1,f2) FROM test1 sorry sorry - -
SELECT coalesce(min(a),'xyzzy') FROM t3 sorry sorry - -
SELECT min(coalesce(a,'xyzzy')) FROM t3 sorry sorry - -
SELECT min(b), min(b) FROM t4 sorry sorry - -
SELECT Max(f1) FROM test1 sorry sorry - -
SELECT max(f1,f2) FROM test1 sorry sorry - -
SELECT MAX(f1,f2)+1 FROM test1 sorry sorry - -
SELECT MAX(f1)+1 FROM test1 sorry sorry - -
SELECT coalesce(max(a),'xyzzy') FROM t3 sorry sorry - -
SELECT max(coalesce(a,'xyzzy')) FROM t3 sorry sorry - -
SELECT Sum(f1) FROM test1 yes sorry - -
SELECT SUM(f1)+1 FROM test1 sorry sorry - -
SELECT sum(a) FROM t3 yes sorry - -
SELECT SUM(min(f1,f2)) FROM test1 sorry sorry - -
SELECT f1 FROM test1 WHERE f1<11 sorry sorry - -
SELECT f1 FROM test1 WHERE f1<=11 sorry sorry - -
SELECT f1 FROM test1 WHERE f1=11 yes sorry - -
SELECT f1 FROM test1 WHERE f1>=11 sorry sorry - -
SELECT f1 FROM test1 WHERE f1>11 sorry sorry - -
SELECT f1 FROM test1 WHERE f1!=11 yes sorry - -
SELECT f1 FROM test1 WHERE min(f1,f2)!=11 sorry sorry - -
SELECT f1 FROM test1 WHERE max(f1,f2)!=11 sorry sorry - -
SELECT f1 FROM test1 ORDER BY f1 sorry sorry - -
SELECT f1 FROM test1 ORDER BY -f1 sorry sorry - -
SELECT f1 FROM test1 ORDER BY min(f1,f2) sorry sorry - -
SELECT f1 FROM test1 ORDER BY 8.4 sorry sorry - -
SELECT f1 FROM test1 ORDER BY '8.4' sorry sorry - -
SELECT * FROM t5 ORDER BY 1; sorry sorry - -
SELECT * FROM t5 ORDER BY 2; sorry sorry - -
SELECT * FROM t5 ORDER BY +2; sorry sorry - -
SELECT * FROM t5 ORDER BY 2, 1 DESC; sorry sorry - -
SELECT * FROM t5 ORDER BY 1 DESC, b; sorry sorry - -
SELECT * FROM t5 ORDER BY b DESC, 1; sorry sorry - -
SELECT max(f1) FROM test1 ORDER BY f2 sorry sorry - -
SELECT f1 FROM test1 ORDER BY f2 sorry sorry - -
SELECT f1 FROM test1 ORDER BY f2 sorry sorry - -
SELECT f1 as 'f1' FROM test1 ORDER BY f2 sorry sorry - -
SELECT * FROM test1 WHERE f1==11 yes sorry - -
SELECT DISTINCT * FROM test1 WHERE f1==11 sorry sorry - -
SELECT * FROM test1 WHERE f1==11 yes sorry - -
SELECT DISTINCT * FROM test1 WHERE f1==11 sorry sorry - -
SELECT f1 as xyzzy FROM test1 ORDER BY f2 sorry sorry - -
SELECT f1 as "xyzzy" FROM test1 ORDER BY f2 sorry sorry - -
SELECT f1 as 'xyzzy ' FROM test1 ORDER BY f2 sorry sorry - -
SELECT f1+F2 as xyzzy FROM test1 ORDER BY f2 sorry sorry - -
SELECT f1+F2 FROM test1 ORDER BY f2 sorry sorry - -
SELECT test1.f1+F2 FROM test1 ORDER BY f2 sorry sorry - -
SELECT test1.f1+F2 FROM test1 ORDER BY f2 sorry sorry - -
SELECT test1.f1+F2, t1 FROM test1, test2 sorry sorry - -
SELECT A.f1, t1 FROM test1 as A, test2 sorry sorry - -
SELECT A.f1, B.f1 FROM test1 as A, test1 as B sorry sorry - -
SELECT test1 . f1, test1 . f2 FROM test1 LIMIT 1 sorry sorry - -
SELECT test1 . f1, test1 . f2 FROM test1 LIMIT 1 sorry sorry - -
SELECT 123.45; sorry sorry - -
SELECT * FROM test1 a, test1 b LIMIT 1 sorry sorry - -
SELECT * FROM test1 a, (select 5, 6) LIMIT 1 sorry sorry - -
SELECT * FROM test1 a, (select 5 AS x, 6 AS y) AS b LIMIT 1 sorry sorry - -
SELECT a.f1, b.f2 FROM test1 a, test1 b LIMIT 1 sorry sorry - -
SELECT f1, t1 FROM test1, test2 LIMIT 1 sorry sorry - -
SELECT a.f1, b.f2 FROM test1 a, test1 b LIMIT 1 sorry sorry - -
SELECT f1, t1 FROM test1, test2 LIMIT 1 sorry sorry - -
SELECT a.f1, b.f1 FROM test1 a, test1 b LIMIT 1 sorry sorry - -
SELECT f1, t1 FROM test1, test2 LIMIT 1 sorry sorry - -
SELECT a.f1, b.f1 FROM test1 a, test1 b LIMIT 1 sorry sorry - -
SELECT f1, t1 FROM test1, test2 LIMIT 1 sorry sorry - -
SELECT f1 FROM test1 UNION SELECT f2 FROM test1 sorry sorry - -
SELECT a FROM t6 WHERE b IN sorry sorry - -
SELECT a FROM t6 WHERE b IN sorry sorry - -
SELECT a FROM t6 WHERE b IN sorry sorry - -
SELECT a FROM t6 WHERE b IN sorry sorry - -
SELECT f1 FROM test1 WHERE 4.3+2.4 OR 1 ORDER BY f1 sorry sorry - -
SELECT f1 FROM test1 WHERE ('x' || f1) BETWEEN 'x10' AND 'x20' sorry sorry - -
SELECT f1 FROM test1 WHERE 5-3==2 sorry sorry - -
SELECT min(1,2,3), -max(1,2,3) sorry sorry - -
SELECT * FROM test1 WHERE f1<0 sorry sorry - -
SELECT * FROM test1 WHERE f1<(select count(*) from test2) sorry sorry - -
SELECT * FROM test1 ORDER BY f1 sorry sorry - -
SELECT * FROM test1 WHERE f1<0 ORDER BY f1 sorry sorry - -
SELECT f1 AS x FROM test1 ORDER BY x sorry sorry - -
SELECT f1 AS x FROM test1 ORDER BY -x sorry sorry - -
SELECT f1-23 AS x FROM test1 ORDER BY abs(x) sorry sorry - -
SELECT f1-23 AS x FROM test1 ORDER BY -abs(x) sorry sorry - -
SELECT f1-22 AS x, f2-22 as y FROM test1 sorry sorry - -
SELECT f1-22 AS x, f2-22 as y FROM test1 WHERE x>0 AND y<50 sorry sorry - -
SELECT f1 COLLATE nocase AS x FROM test1 ORDER BY x sorry sorry - -
SELECT * FROM t3, t4; yes sorry - -
SELECT t3.*, t4.b FROM t3, t4; yes sorry - -
SELECT "t3".*, t4.b FROM t3, t4; yes sorry - -
SELECT x.*, y.b FROM t3 AS x, t4 AS y; yes sorry - -
SELECT t3.b, t4.* FROM t3, t4; yes sorry - -
SELECT x.b, y.* FROM t3 AS x, t4 AS y; yes sorry - -
SELECT t3.* FROM t3, (SELECT max(a), max(b) FROM t4) sorry sorry - -
SELECT t3.* FROM (SELECT max(a), max(b) FROM t4), t3 sorry sorry - -
SELECT * FROM t3, (SELECT max(a), max(b) FROM t4) AS 'tx' sorry sorry - -
SELECT y.*, t3.* FROM t3, (SELECT max(a), max(b) FROM t4) AS y sorry sorry - -
SELECT y.* FROM t3 as y, t4 as z yes sorry - -
SELECT 1+2+3 sorry sorry - -
SELECT 1,'hello',2 yes sorry - -
SELECT 1 AS 'a','hello' AS 'b',2 AS 'c' yes sorry - -
SELECT * FROM t3 UNION SELECT 3 AS 'a', 4 ORDER BY a; sorry sorry - -
SELECT 3, 4 UNION SELECT * FROM t3; sorry sorry - -
SELECT * FROM t3 WHERE a=(SELECT 1); sorry sorry - -
SELECT * FROM t3 WHERE a=(SELECT 2); sorry sorry - -
SELECT x FROM ( sorry sorry - -
SELECT z.x FROM ( sorry sorry - -
SELECT count( sorry sorry - -
SELECT name FROM sqlite_master WHERE type = 'table' yes sorry - -
SELECT * FROM sqlite_master WHERE rowid>10; sorry sorry - -
SELECT * FROM sqlite_master WHERE rowid=10; sorry sorry - -
SELECT * FROM sqlite_master WHERE rowid<10; sorry sorry - -
SELECT * FROM sqlite_master WHERE rowid<=10; sorry sorry - -
SELECT * FROM sqlite_master WHERE rowid>=10; sorry sorry - -
SELECT * FROM sqlite_master; yes sorry - -
SELECT 10 IN (SELECT rowid FROM sqlite_master); sorry sorry - -
SELECT 2 IN (SELECT a FROM t1) sorry sorry - -
SELECT 2 IN (SELECT a FROM t1) sorry sorry - -
SELECT * FROM t1,(SELECT * FROM t2 WHERE y=2 ORDER BY y,z); sorry sorry - -
SELECT * FROM t1,(SELECT * FROM t2 WHERE y=2 ORDER BY y,z LIMIT 4); sorry sorry - -
SELECT * FROM t1,(SELECT * FROM t2 WHERE y=2 sorry sorry - -
SELECT x FROM t2, t1 WHERE x BETWEEN c AND null OR x AND sorry sorry - -
SELECT x FROM t2, t1 WHERE x BETWEEN c AND (c+1) OR x AND sorry sorry - -
SELECT 1 FROM t1 WHERE ( sorry sorry - -
SELECT 1 FROM t1, t2 WHERE ( sorry sorry - -
SELECT*FROM"main"."t1" sorry sorry - -
SELECT * FROM t1 JOIN t1 USING(a,b) sorry sorry - -
SELECT ifnull(a, max((SELECT 123))), count(a) FROM t1 ; sorry sorry - -
SELECT a,(+a)b,(+a)b,(+a)b,NOT EXISTS(SELECT null FROM t2),CASE z WHEN 487 THEN 992 WHEN 391 THEN 203 WHEN 10 THEN '?k<D Q' END,'' FROM t1 LEFT JOIN v1a ON z=b; sorry sorry - -