search

michaelbjames / partial-refinements

MIT License
0 stars 0 forks source link

Datatype instances not inductive to Z3 #2

Closed michaelbjames closed 3 years ago

michaelbjames commented 4 years ago

We cannot use instantiations of datatypes in our conjunction examples. For example, with the environment

data List a where
    Nil :: List a
    Cons :: x: a -> xs: List a -> List a

termination measure len :: List a -> {Int | _v >= 0} where
  Nil -> 0
  Cons x xs -> 1 + len xs

We cannot check

snoc :: xs: List Int -> x: Int -> {List Int |
    (((x == 0) && (xs == Nil)) ==> (_v == (Cons 0 Nil))) &&
    (((x == 0) && (xs == (Cons 1 Nil))) ==> (_v == (Cons 1 (Cons 0 Nil)))) &&
    (((x == 0) && (xs == (Cons 2 (Cons 1 Nil)))) ==> (_v == (Cons 2 (Cons 1 (Cons 0 Nil)))))
    }
snoc = \zs. \z.
    match zs with
        Nil -> Cons z Nil
        Cons y ys -> Cons y (snoc ys z)

We get the error:

test/intersection/myth/List-Snoc.sq:38: Error:
  Cannot find sufficiently strong refinements
  when checking Cons y (snoc ys z)
  ::
  {List Int|((z == 0 && zs == (Nil) ==> _v == (Cons 0 (Nil))) && (z == 0 && zs == (Cons 1 (Nil)) ==> _v == (Cons 1 ((Cons 0 (Nil)))))) && (z == 0 && zs == (Cons 2 ((Cons 1 (Nil)))) ==> _v == (Cons 2 ((Cons 1 ((Cons 0 (Nil)))))))}
  in
  \zs . \z . 
      match zs with
        Cons y ys -> Cons y (snoc ys z)

However if our datatype were data IntList where Nil :: IntList; Cons :: Int -> IntList -> IntList, this example would work.

We believe this comes from the way we encode polymorphic datatypes in Z3.

michaelbjames commented 4 years ago

Confusingly, the list-sum function is okay with types like this:

-- Checks, but does not synthesize
sum :: xs: List Int -> {Int |
        (xs == Nil) ==> (_v == 0) &&
        (xs == (Cons 1 Nil)) ==> (_v == 1) &&
        (xs == (Cons 4 (Cons 1 Nil))) ==> (_v == 5)}
sum = \xs.
    match xs with
        Nil -> 0
        Cons y ys -> y + sum ys

Edit: This example is missing parenthesis and so it 's trivially true. The extra parens ((a ==> b) && (c ==> d)), make this an unexceptional example. It fails like the rest.

michaelbjames commented 4 years ago

Here appears to be a minimal example:

data Nat a where
    Z :: Nat a
    S :: Nat a -> Nat a

termination measure len :: Nat a -> {Int | _v >= 0} where
    Z -> 0
    S xs -> 1 + len xs

toZero :: n:Nat Int -> {Int |
    ((n == Z) ==> (_v == 0)) &&
    ((n == S Z) ==> (_v == 0)) && -- Comment this out and it checks.
    True
    }
toZero = \n.
    match n with
        Z -> 0
        S xs -> toZero xs

You can make this succeed in two ways:

  1. Comment out the S Z example.
  2. Monomorphize the "Nat a" into just a Nat

It appears to spit out this core SMTLIB (commented out lines not needed to see a difference of behavior): 

(assert
    (not (=> (and (= nIntS (SIntSIntS xsIntS))
          ;    (>= (lenIntSIntS nIntS) 0)
          ;    (>= (lenIntSIntS xsIntS) 0)
              (or (not (= xsIntS ZIntS)) (= _vIntS 0))
              (or (not (= xsIntS (SIntSIntS ZIntS))) (= _vIntS 0))
              true
          ;    (= (lenIntSIntS (SIntSIntS xsIntS)) (+ 1 (lenIntSIntS xsIntS)))
          ;    (= (lenIntSIntS (SIntSIntS ZIntS)) (+ 1 (lenIntSIntS ZIntS)))
          ;    (= (lenIntSIntS ZIntS) 0)
          )
         (and (=> (= nIntS ZIntS) (= _vIntS 0))
              (=> (= nIntS (SIntSIntS ZIntS)) (= _vIntS 0))
              true))))

(check-sat)
(get-model)

I couldn't get it to spit out the header but here's what I can surmise:

(set-option :smt.mbqi false)

; unsat, which is the result we want
;(declare-datatype NList ((ZIntS) (SIntSIntS (prev NList))))

; sat, which is what we get
(declare-sort NList 0)
(declare-fun ZIntS () NList)
(declare-fun SIntSIntS (NList) NList)

(declare-const _vIntS Int)
(declare-const nIntS NList)
(declare-const xsIntS NList)
michaelbjames commented 4 years ago

Similarly, we have a minimal example of the SMTLIB, taken and simplified from the snoc example above. The way datatypes are declared in Z3 affect whether it can check the model. Declare-fun will let Z3 come up with a function definition.

(set-option :smt.mbqi false)
; doesnt work
(declare-datatype LList ((Nil) (Cons (hd Int) (tl LList))))
; works
;(declare-sort LList 0) (declare-fun Nil () LList) (declare-fun Cons (Int LList) LList)
(declare-const xsDataS LList)
(declare-const _vDataS LList)
(declare-const yIntS Int)
(declare-const ysDataS LList)
(assert
 (not (=>
         (= xsDataS (Cons yIntS ysDataS))
         (=>
             (= xsDataS Nil)
             (= _vDataS (Cons 0 Nil))
         )
       )))
(check-sat)
(get-model)

The whole constraints from snoc are:

(set-option :smt.mbqi false)
(declare-fun NilIntS () Int)
(declare-fun ConsIntSIntSIntS (Int Int) Int)
(declare-fun lenIntSIntS (Int) Int)

(declare-const xIntS Int)
(declare-const xsIntS Int)
(declare-const _vIntS Int)
(declare-const x2IntS Int)
(declare-const x3IntS Int)
(declare-const x6IntS Int)
(declare-const x7IntS Int)
(declare-const yIntS Int)
(declare-const ysIntS Int)

(assert
  (not (=> (and (= _vIntS (ConsIntSIntSIntS yIntS x7IntS))
              (= xsIntS (ConsIntSIntSIntS yIntS ysIntS))
              (>= (lenIntSIntS x7IntS) 0)
              (>= (lenIntSIntS xsIntS) 0)
              (>= (lenIntSIntS ysIntS) 0)
              (or (not (= xIntS 0))
                  (not (= ysIntS NilIntS))
                  (= x7IntS (ConsIntSIntSIntS 0 NilIntS)))
              (or (not (= xIntS 0))
                  (not (= ysIntS (ConsIntSIntSIntS 1 NilIntS)))
                  (= x7IntS (ConsIntSIntSIntS 1 (ConsIntSIntSIntS 0 NilIntS))))
              (or (not (= xIntS 0))
                  (not (= ysIntS
                          (ConsIntSIntSIntS 2 (ConsIntSIntSIntS 1 NilIntS))))
                  (= x7IntS
                     (ConsIntSIntSIntS 2
                                       (ConsIntSIntSIntS 1
                                                         (ConsIntSIntSIntS 0
                                                                           NilIntS)))))
              (= (lenIntSIntS (ConsIntSIntSIntS 0 NilIntS))
                 (+ 1 (lenIntSIntS NilIntS)))
              (= (lenIntSIntS (ConsIntSIntSIntS 1 (ConsIntSIntSIntS 0 NilIntS)))
                 (+ 1 (lenIntSIntS (ConsIntSIntSIntS 0 NilIntS))))
              (= (lenIntSIntS (ConsIntSIntSIntS 1 NilIntS))
                 (+ 1 (lenIntSIntS NilIntS)))
              (= (lenIntSIntS (ConsIntSIntSIntS 2
                                                (ConsIntSIntSIntS 1
                                                                  (ConsIntSIntSIntS 0
                                                                                    NilIntS))))
                 (+ 1
                    (lenIntSIntS (ConsIntSIntSIntS 1
                                                   (ConsIntSIntSIntS 0 NilIntS)))))
              (= (lenIntSIntS (ConsIntSIntSIntS 2 (ConsIntSIntSIntS 1 NilIntS)))
                 (+ 1 (lenIntSIntS (ConsIntSIntSIntS 1 NilIntS))))
              (= (lenIntSIntS (ConsIntSIntSIntS yIntS x7IntS))
                 (+ 1 (lenIntSIntS x7IntS)))
              (= (lenIntSIntS (ConsIntSIntSIntS yIntS ysIntS))
                 (+ 1 (lenIntSIntS ysIntS)))
              (= (lenIntSIntS NilIntS) 0))
         (and (=> (and (= xIntS 0) (= xsIntS NilIntS))
                  (= _vIntS (ConsIntSIntSIntS 0 NilIntS)))
              (=> (and (= xIntS 0) (= xsIntS (ConsIntSIntSIntS 1 NilIntS)))
                  (= _vIntS (ConsIntSIntSIntS 1 (ConsIntSIntSIntS 0 NilIntS))))
              (=> (and (= xIntS 0)
                       (= xsIntS
                          (ConsIntSIntSIntS 2 (ConsIntSIntSIntS 1 NilIntS))))
                  (= _vIntS
                     (ConsIntSIntSIntS 2
                                       (ConsIntSIntSIntS 1
                                                         (ConsIntSIntSIntS 0
                                                                           NilIntS)))))))))
(check-sat)
(get-model)
michaelbjames commented 4 years ago

So it seems like we should be using Z3's declare-datatype instead of declare-sort and declare-fun. In the latter, Z3 can produce SAT by cheekily assigning the functions the same definitions (for https://github.com/michaelbjames/partial-refinements/issues/2#issuecomment-697714774):

(model 
  ;; universe for NList:
  ;;   NList!val!1 NList!val!0 
  ;; -----------
  ;; definitions for universe elements:
  (declare-fun NList!val!1 () NList)
  (declare-fun NList!val!0 () NList)
  ;; cardinality constraint:
  (forall ((x NList)) (or (= x NList!val!1) (= x NList!val!0)))
  ;; -----------
  (define-fun nIntS () NList
    NList!val!1)
  (define-fun ZIntS () NList
    NList!val!1)
  (define-fun _vIntS () Int
    1)
  (define-fun xsIntS () NList
    NList!val!0)
  (define-fun SIntSIntS ((x!0 NList)) NList
    (ite (= x!0 NList!val!0) NList!val!1
    (ite (= x!0 NList!val!1) NList!val!1
      NList!val!1)))
)

See that SIntSIntS is semantically equivalent to ZIntS!

I'm not sure what the tradeoffs are for using declare-datatype over declare-fun. Okay so what are the tradeoffs for using declare-datatype or delcare-fun?

Using declare-datatype Well, according to two stackoverflow questions, you cannot define a polymorphic function over a parametric datatype (e.g., a measure for List a). Instead, we would need to redefine each measure for each type we wanted to use it on. That sound you hear is C++-style polymorphism lumbering over.

Using declare-fun We need to add some axioms such that the datatype functions are never equal. In this case we want an extra axiom: forall x. S x != Z. We need those axioms across all sort functions to prevent, say, TreeEmpty == ListNil.

We need to decide which is easier to implement.

michaelbjames commented 4 years ago

Attempting to use declare-fun

Setup: I'm trying this on the toZero function. I'm testing a solution on the smt to make it unsat.

Assert functions not equal We know that SIntSIntS is the same as a ZIntS, and we explicitly want them to be distinct. So, I added the following assert: (assert (forall ((sz NList)) (not (= (SIntSIntS sz) ZIntS))))

This did not work: Z3 is infinitely cheeky. Our new model is:

(model 
  ;; universe for NList:
  ;;   NList!val!1 NList!val!2 NList!val!0 
  ;; -----------
  ;; definitions for universe elements:
  (declare-fun NList!val!1 () NList)
  (declare-fun NList!val!2 () NList)
  (declare-fun NList!val!0 () NList)
  ;; cardinality constraint:
  (forall ((x NList)) (or (= x NList!val!1) (= x NList!val!2) (= x NList!val!0)))
  ;; -----------
  (define-fun nIntS () NList
    NList!val!1)
  (define-fun ZIntS () NList
    NList!val!2)
  (define-fun _vIntS () Int
    1)
  (define-fun xsIntS () NList
    NList!val!0)
  (define-fun SIntSIntS ((x!0 NList)) NList
    NList!val!1)
)

This assert wasn't it--or it's not the whole solution. We'll also need to say that the successor has no fixpoint: (assert (forall ((sz NList)) (not (= (SIntSIntS sz) sz)))) :

 (define-fun nIntS () NList
    NList!val!1)
  (define-fun ZIntS () NList
    NList!val!2)
  (define-fun _vIntS () Int
    1)
  (define-fun xsIntS () NList
    NList!val!0)
  (define-fun k!3 ((x!0 NList)) NList
    (ite (= x!0 NList!val!1) NList!val!1
    (ite (= x!0 NList!val!0) NList!val!0
      NList!val!2)))
  (define-fun SIntSIntS!4 ((x!0 NList)) NList
    (ite (= x!0 NList!val!1) NList!val!3
      NList!val!1))
  (define-fun SIntSIntS ((x!0 NList)) NList
    (SIntSIntS!4 (k!3 x!0)))

Alas, still satisfiable.

I'm sure there are more axioms we need, but I'm going to try the datatype approach now.

A New Wind

Inspired by Nikolaj's work, I instantiated the algebraic datatype laws for our constructors. We do not need the previous axiom. It's implied by the junk check.

; occurs check: no infinite datatypes
(assert (forall ((sz NList)) (not (= (SIntSIntS sz) sz))))

; no confusion: Two datatypes are equal iff they are constructed exactly the same way
(assert (forall ((n1 NList) (n2 NList)) (and
    (=>
        (= (SIntSIntS n1) (SIntSIntS n2))
        (= n1 n2))
    (=>  ; Congruence
        (= n1 n2)
        (= (SIntSIntS n1) (SIntSIntS n2)))
    )))

; junk check: all trees are generated from the constructors
(assert (forall ((n NList))
    (xor
        (exists ((m NList)) (= n (SIntSIntS m)))
        (= n ZIntS))))

Unsat Now to generalize this...

michaelbjames commented 4 years ago

I have generalized this strategy. Its latest attempt is in the datatype-as-function branch. The occurs check was straightforward. We only need the first part of the confusion check; the second direction is the congruence axiom in the theory of uninterpreted functions. The junk check requires a 1-of-n constraint, which requires polynomially many subconstraints. This gives some concern about the speed of such an additional check.

Currently, the branch still uses Int as the default sort, even for datatypes, which leads to the curious constraint that all Ints must be made from one of the available constructor functions. I have made bespoke SMT2 test files that use separate, uninterpreted sorts like LList for a List. Indeed this is not yet truly polymorphic, but my test file doesn't yet test that polymorphism.

This approach does allow us to prove toZero and snoc!

A looming problem Great, toZero works! list-rev-append still doesn't work. The minimal example, appears to fail being unable to show that Nil == append Nil Nil. This code does not prove SAT, instead, it's UNKOWN, which is interpreted as SAT. I reconstructed the SMT it sends to Z3 here. This hangs as expected. It continues to hang, even when I change from Int to List where appropriate.

The Occurs Check and Junk Check each terminate on their own, but not together. (Both come out to SAT) The Confusion Check will hang alone or with either other axiom.

It appears that the encoding is too slow for Z3. So:

  1. Is there a faster encoding? Or a way to use Z3's :pattern suggestions to chug this along faster?
  2. Should I backtrack and use datatypes (with C++-style instantiation)?
michaelbjames commented 3 years ago

I have this largely fixed in a9d74dac8dcd8125d3ab38fbce0a259def94dbef . There may be some lingering issues (see List-Inc in conjunctions) but I'm not sure if they're related.