Introducing Cosette – a SQL solver for checking semantic equivalences of queries

Re:Introducing Cosette – a SQL solver for checking semantic ... by lukaseder on Thursday July 20, 2017 @04:45AM (#14810905)

Nice idea, but it breaks quite quickly (still). Tried to see if Cosette can prove equivalence of these two queries:

    /* define schema s1, 
       here s1 can contain any number of attributes, 
       but it has to at least contain integer attributes 
       x and y */
    schema s1(x:int, ya:int, ??);
    
    schema s2(yb:int, ??);        -- define schema s2
    
    table a(s1);            -- define table a using schema s1
    table b(s2);            -- define table b using schema s1
    
    query q1                -- define query q1 on tables a and b
    `select distinct x.x as ax from a x, b y
     where x.ya = y.yb`;
    
    query q2                -- define query q2 likewise
    `select x.x as ax from a x, a y, b z 
     where x.x = y.x and x.ya = z.yb
     union select 1 as ax from a x where 1 = 0`;
    
    verify q1 q2;           -- does q1 equal to q2?

Got a syntax error:

    Syntax Error. 
    ERROR: (line 19, column 8):
    unexpected "s"
    expecting "--" or "/*"

There are many other bugs up to the point where this is not really usable.

[ Parent | on HN ]

Re:Introducing Cosette – a SQL solver for checking semantic ... by LaPrometheus on Thursday July 20, 2017 @12:21PM (#14813808)

Thanks for trying out. The parser error report is not great now. The real error actually, it should be "union all" rather than "union".

I changed your query:

/* define schema s1, here s1 can contain any number of attributes, but it has to at least contain integer attributes x and y */ schema s1(x:int, ya:int, ??);

    schema s2(yb:int, ??);        -- define schema s2
    
    table a(s1);            -- define table a using schema s1
    table b(s2);            -- define table b using schema s1
    
    query q1                -- define query q1 on tables a and b
    `select distinct x.x as ax 
    from a x, b y
     where x.ya = y.yb`;
    
    query q2                -- define query q2 likewise
    `(select x.x as ax 
     from a x, a y, b z 
     where x.x = y.x and x.ya = z.yb)
     union all (select 1 as ax from a x where 1 = 0)`;
    
    verify q1 q2;           -- does q1 equal to q2?

The Rosette execution indeed returns a counterexample (since they are not equal). There is an error in Coq code generation part, we are fixing that now.

[ Parent | on HN ]

Re:Introducing Cosette – a SQL solver for checking semantic ... by lukaseder on Friday July 21, 2017 @04:40AM (#14818996)

Yes, I understood later on that you're not supporting union yet. Would have been nice, though, there are quite some caveats when trying to transform distinct / union into one another... :)

Btw, another parser error happened when I indented the code, e.g. pasting the indented code from Hackernews here into your tool. The parser then complains about \r or something like that.

[ Parent | on HN ]

Re:Introducing Cosette – a SQL solver for checking semantic ... by LaPrometheus on Tuesday July 25, 2017 @01:49AM (#14845401)

Please try again now :)

[ Parent | on HN ]