michaelbjames/partial-refinements

partial-refinements's Issues

Unbound variable in SMT

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

{-
Does not check. The first two will check on their own just fine. Together the first two do not check.

With the first two refinements:
Problem while checking the first branch.
On (Cons z Nil)
Cons z Nil :: {List a|len _v == len xs + 1}
snoc, z, zs zs == (Nil) |- {List A2|_v == (Cons z (Nil))} <: {List a|len _v == len xs + 1} ()
xs was not bound?? in the SMT

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

This program will work if the zs and z are renamed to xs and x. I get the sense something isn't being renamed.

Unable to instantiate

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

snoc ::
		(xs: List a -> x: a ->  {List a | len _v == (len xs + 1)}) ^
		(xs: {List a | _v == Nil} -> x: a ->  {List a | _v == (Cons x Nil)}) ^
		(xs: {List Int| _v == (Cons 2 Nil)} -> x: {Int | _v == 1} -> {List Int | _v == (Cons 2 (Cons 1 Nil))}) ^
		(xs: {List Int| _v == (Nil)} -> x: {Int | _v == 1} -> {List Int | _v == (Cons 1 Nil)})
snoc = \xs. \x.
	match xs with
		Nil -> Cons x Nil
		Cons y ys -> Cons y (snoc ys x)

Should the last refinement be necessary?

Cannot match shape 'Int' with shape 'b'

It seems that sometimes, when using intersections with mixed shapes, you can get an erroneous shape-mismatch error.

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

-- Does not check:
-- shape mismatch: b / Int.
-- b gets instantiated to different types.
foldl2 :: (f:(acc:b -> x:a -> b) -> base:b -> xs:List a -> b) ^
          (f:(acc:Int -> x:Int -> {Int | _v == acc - x}) ->  -- f does subtraction
            base:Int ->
            xs:List Int ->
            {Int | ((base == 3 && xs == (Cons 2 (Cons 1 Nil))) ==> (_v == 0)) &&
                   ((base == 1 && xs == (Cons 1 Nil))          ==> (_v == 0)) &&
                   ((base == 0 && xs == Nil)                   ==> (_v == 0))}) -- concrete, trace-complete examples
foldl2 = \f. \base. \xs.
  match xs with
    Nil -> base
    Cons y ys -> foldl2 f (f base y) ys

The error is:

test/intersection/higher-order/List-Foldl.sq:70: Error:
  Cannot match shape 'Int'
  with shape 'b'
  when checking foldl2 ::
  x4:_ -> x3:_ -> x2:_ -> b in
  \f . \base . \xs . 
        match xs with
          Cons y ys -> foldl2 ?? ?? ??

This inductive function spec should type check!
It's not clear if this is a special case of #2.

Datatype instances not inductive to Z3

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.

List-Compress, must break up spec

Consider this program specification:

compress ::
  -- The output is always shorter or equal to the input
  (xs: List Int -> {List Int | ((len _v < len xs) || (_v == xs)) && elems _v == elems xs}) ^

  -- If it's empty list, then it should produce nothing
  (xs: {List Int | len _v == 0} -> {List Int | _v == Nil}) ^

  -- A couple base cases
  (xs: {List Int | _v == (Cons 1 Nil) || _v == (Cons 1 (Cons 1 Nil))} -> {List Int | _v == (Cons 1 Nil)}) ^

  -- QUESTIONABLE
  (xs: {List Int | _v == Cons 2 (Cons 1 Nil) || _v == (Cons 3 (Cons 2 (Cons 1 Nil))) } -> {List Int | _v == xs})
compress = \xs .  -- defn Taken from synquid-verified PLDI16 solutions
  match xs with
    Nil -> Nil
    Cons x3 x4 ->
      match compress x4 with
        Nil -> Cons x3 Nil
        Cons x10 x11 ->
          if x3 == x10
            then compress x4
            else Cons x3 (Cons x10 x11)

It fails to check that compress satisfies the last refinement intersection with the error:

  Cannot find sufficiently strong refinements
  when checking
  x4 :: {PList Int <True>|(_v == (Cons 2 ((Cons 1 (Nil)))) || _v == (Cons 3 ((Cons 2 ((Cons 1 (Nil))))))) && (len _v >= 0 && len _v < len xs)}
  in
  \xs . 
    match xs with
      Cons x3 x4 -> 
        match compress x4 with

Confusingly, to me, this program checks if I change the last spec.
Instead of:
(xs: {List Int | _v == Cons 2 (Cons 1 Nil) || _v == (Cons 3 (Cons 2 (Cons 1 Nil))) } -> {List Int | _v == xs})
I break it in two, to:

  (xs: {List Int | _v == Cons 2 (Cons 1 Nil)} -> {List Int | _v == xs}) ^
  (xs: {List Int | _v == Cons 3 (Cons 2 (Cons 1 Nil))} -> {List Int | _v == xs})

The whole program and refinement passes.

I'm not sure why this is.

Intersection not sufficient; conjunction is.

The same spec expressed with an intersection cannot check code that checks with conjunction.

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

-- Not strong enough...
pairs :: ((a -> a -> a) -> xs:{List a | len _v > 1} -> {List a | (2 * len _v >= len xs) && (len _v < len xs)}) ^
         ((a -> a -> a) -> xs:{List a | len _v <= 1} -> {List a | _v == xs})
-- This is strong enough.
-- pairs :: (a -> a -> a) -> xs:List a -> {List a |
--       ((len xs > 1) ==> ((2 * len _v >= len xs) && len _v < len xs)) &&
--       ((len xs <= 1) ==> (_v == xs)) &&
--       True}
pairs = \f. \xs.
  match xs with
    Nil -> Nil
    Cons y ys ->
      match ys with
        Nil -> Cons y ys
        Cons z zs -> Cons (f y z) (pairs f zs)

The error is:

Cannot find sufficiently strong refinements
  when checking zs ::
  {List a|len _v <= 1 && (len _v >= 0 && len _v < len xs)}
  in
  \f . \xs . 
      match xs with
        Cons y ys -> 
          match ys with
            Cons z zs -> Cons (f y z) (pairs
                                         f zs)

Clashing argument names when parsing higher-order function types

foldl :: List Int -> Int -> (Int -> Int -> Int) -> Int
foldl = \xs. \base. \f.
  match xs with
    Nil -> base
    Cons y ys -> foldl ys (f base y) f

Typechecking the function above produces the following error:

synquid: Attempt to substitute variable arg1 bound in a function type

The parsed type of foldl is this: arg2:List Int -> arg1:Int -> arg0:(arg1:Int -> arg0:Int -> Int) -> Int

Clearly, there is a bug here -- arg1 and arg2 are bound twice.
The issue is in this function from the parser (Parser.hs line 227):

parseFunctionTypeMb = do
  argType <- parseUnrefTypeWithArgs <|> parseTypeAtom
  parseFunctionRest argType <|> return argType
  where
    parseFunctionRest argType = do
      reservedOp "->"
      returnType <- parseType
      return $ FunctionT ("arg" ++ show (arity returnType)) argType returnType

Argument names are generated according to the arity of the return type. Thus, a higher-order function type will end up reusing names if none are provided.

Possible solutions

• Add some kind of fresh name infrastructure to the parser (maybe kinda awkward)
• Fix everything at resolve time
  • Already has fresh name infrastructure
  • Feels kinda hacky
• ???

I haven't done anything about this yet, just adding names in the mean time.

Unable to check across inductive cases

This function will not check

list_last :: (xs:List Int -> Maybe Int) ^
  (xs:{List Int| len _v == 0} -> {Maybe Int | _v == Nothing}) ^
  (xs:{List Int | _v == ((Cons 2 (Cons 1 Nil)))} -> {Maybe Int | _v == Nothing}) ^

  -- This last refinement causes it to fail
  (xs:{List {Int | _v == 1} | len _v > 0} -> {Maybe Int | _v == Nothing})
  -- It does not fail with a concrete example
  -- (xs:{List Int | _v == Cons 1 Nil} -> {Maybe Int | _v == Just 1})
list_last = \xs .
  match xs with
    Nil -> Nothing
    Cons x3 x4 ->
      match x4 with
        Nil -> Nothing
        Cons x8 x9 -> list_last x4

It seems that while checking the recursive case, the system will not consider the other types in the intersection--It cannot figure out that the IH (_v == Cons 1 Nil) fits the recursive where {List {Int | _v == 1} | len _v > 0}

This bug prevents us from writing "hybrid" specs, ones that include a concrete example, along with an intersection.