rio monad smt2 file explosion

I've been doing some tests with the refined monad from the bounded refinement types paper (icfp15), in combination with some behavioral types, and while it generally works well, I ran into some cases where the smt2 file gets to absurd sizes (and thus, it takes a lot of time to prove). I think this is probably a bug, but I'm not sure.

The following is an example showing this, although it may be a bit contrived. I'm trying to reduce it a bit more, but I think it may be enough for someone with more knowledge than me to figure out what's happening.

I know it doesn't happen without the branching behavior, so the problem is probably selectLeft, but I don't see anything special about it.

{-@ LIQUID "--no-pattern-inline" @-}

module Lib where

import Prelude
import Control.Applicative

newtype Rec
  = MkRec (Branch (A Int Rec) End)

{-@ data A a s = A s @-}
data A a s = A s
data End      = End ()

type Branch c1 c2 = A (Either c1 c2) ()

{-@ f :: Rec -> RIO <{\w -> lastVal w = 0}> () @-}
f :: Rec -> RIO ()
f (MkRec s) = do 
    s <- selectLeft s
    MkRec s <- doA 100 s
    -- smt2 file size: 331 kb
    s <- selectLeft s
    MkRec s <- doA 100 s
    -- smt2 file size: 797 kb
    s <- selectLeft s
    MkRec s <- doA 300 s
    -- smt2 file size: 5 mb 
    s <- selectLeft s
    MkRec s <- doA 400 s
    -- smt2 file size: 43 mb
    s <- selectLeft s
    MkRec s <- doA 500 s
    -- smt2 file size: 385mb
    s <- selectRight s
    end s

{-@ assume doA :: Typestate s => v1:Int -> A Int s -> RIO<{\w -> lastVal w < v1}, {\w1 b w2 -> lastVal w2 = v1}> s @-}
doA :: Typestate s => Int -> A Int s -> RIO s
doA i (A s) = return s

{-@ end :: End -> RIO <{\x -> true}, {\w1 b w2 -> Pure w1 w2}> () @-}
end :: End -> RIO ()
end (End s) = return ()

{-@ assume selectLeft :: Typestate s => Branch s_1 s_2 -> RIO<{\w1 -> true}, {\w1 v w2 -> Pure w1 w2 }> s_1 @-}
selectLeft :: (Typestate s_1) => Branch s_1 s_2 -> RIO s_1
selectLeft (A _) = return $ newS

{-@ assume selectRight :: Typestate s => Branch s_1 s_2 -> RIO<{\w1 -> true}, {\w1 v w2 -> Pure w1 w2}> s_2 @-}
selectRight :: (Typestate s_2) => Branch s_1 s_2 -> RIO s_2
selectRight (A _) = return $ newS

-- recursive constructors
--
class Typestate s where
  newS :: s

instance Typestate s => Typestate (A a s) where
  newS = A newS

instance Typestate End where
  newS = End ()

instance Typestate () where
  newS = ()

instance Typestate Rec
  where
    newS = MkRec $ newS 

{-@ data RIO a <p :: World -> Bool, q :: World -> a -> World -> Bool>
      = RIO (runState :: (x:World<p> -> (a, World)<\w -> {v:World<q x w> | true}>))
  @-}
data RIO a  = RIO {runState :: World -> (a, World)}

{-@ runState :: forall <p :: World -> Bool, q :: World -> a -> World -> Bool>.
                RIO <p, q> a -> xyy:World<p> -> (a, World)<\w -> {v:World<q xyy w> | true}> @-}

{-@ measure lastVal :: World -> Int @-}
{-@ predicate Pure W1 W2 = W1 = W2 @-}
data World = W

{-@ assume emptyWorld :: {w:World | lastVal w = 0} @-}
emptyWorld :: World
emptyWorld = W

instance Functor RIO where
  fmap = undefined

instance Applicative RIO where
  pure  = undefined
  (<*>) = undefined

instance Monad RIO where
{-@ instance Monad RIO where
      >>= :: forall < p  :: World -> Bool 
                    , p2 :: a -> World -> Bool
                    , r  :: a -> Bool
                    , q1 :: World -> a -> World -> Bool
                    , q2 :: a -> World -> b -> World -> Bool
                    , q  :: World -> b -> World -> Bool>.
           {x::a<r>, w::World<p>|- World<q1 w x> <: World<p2 x>}
           {w::World<p>, x::a<r>, w1:: World<q1 w x>, w2::{v:World<p2 x> | v == w1}, y::b|- World<q2 x w2 y> <: World<q w y>}
           {x::a, w::World<p>, w2::World<q1 w x>|- {v:a | v = x} <: a<r>}
           RIO <p, q1> a
        -> (x:a<r> -> RIO <{v:World<p2 x> | true}, \w1 y -> {v:World<q2 x w1 y> | true}> b)
        -> RIO <p, q> b ;
      >>  :: forall < p   :: World -> Bool
                    , p2  :: World -> Bool
                    , q1 :: World -> a -> World -> Bool
                    , q2 :: World -> b -> World -> Bool
                    , q :: World -> b -> World -> Bool>.
            {x::a, w::World<p>|- World<q1 w x> <: World<p2>}
            {w::World<p>, w2::World<p2>, y::a, w3:: {v:World<q1 w y> | v == w2}, x::b |- World<q2 w2 x> <: World<q w x>}
            RIO <p, q1> a
         -> RIO <p2, q2> b
         -> RIO <p, q> b  ;
      return :: forall <p :: World -> Bool>.
                x:a -> RIO <p, \w0 y -> {w1:World | w0 == w1 && y == x}> a
  @-}
  (RIO g) >>= f = RIO $ \x -> case g x of {(y, s) -> (runState (f y)) s}
  (RIO g) >>  f = RIO $ \x -> case g x of {(y, s) -> (runState f    ) s}
  return w      = RIO $ \x -> (w, x)

Also, just in case, I'm using the following versions, although I did try with a few variations.

#stack.yaml
packages:
  - .

extra-deps:
  - Diff-0.3.4
  - git: https://github.com/ucsd-progsys/liquidhaskell
    commit: 154c5006a51e182d214e38e59b35e22de7d70df7 
    subdirs:
      - .
      - liquid-base
      - liquid-ghc-prim
      - liquid-containers
      - liquid-prelude
  - git: https://github.com/ucsd-progsys/liquid-fixpoint
    commit: b91e279b8dd3a4716372692d2126ffcb90f5e5a3 
  - git: https://github.com/zgrannan/rest
    commit: 1cadb23edfbc393245ae964315b07f5c8581ea9f
  - hashable-1.3.0.0@sha256:d60cad00223d46172020c136e68acef0481a47d0302b2e74b1805b4f3a446a9b,5389

resolver: nightly-2022-03-10
compiler: ghc-8.10.7

allow-newer: true

Wow, I have sometimes seen this but hasn’t been easy to reproduce. Thanks very much for posting this so we can get to the bottom of the problem!

On Sat, Apr 2, 2022 at 7:38 PM Enzo Cioppettini @.***> wrote:

I've been doing some tests with the refined monad from the bounded refinement types paper (icfp15), in combination with some behavioral types, and while it generally works well, I ran into some cases where the smt2 file gets to absurd sizes (and thus, it takes a lot of time to prove). I think this is probably a bug, but I'm not sure.

The following is an example showing this, although it may be a bit contrived. I'm trying to reduce it a bit more, but I think it may be enough for someone with more knowledge than me to figure out what's happening.

I know it doesn't happen without the branching behavior, so the problem is probably selectLeft, but I don't see anything special about it.

{-@ LIQUID "--no-pattern-inline" @-}

module Lib where

import Prelude import Control.Applicative newtype Rec = MkRec (Branch (A Int Rec) End) {-@ data A a s = A s @-}data A a s = A sdata End = End () type Branch c1 c2 = A (Either c1 c2) () {-@ f :: Rec -> RIO <{\w -> lastVal w = 0}> () @-}f :: Rec -> RIO () f (MkRec s) = do s <- selectLeft s MkRec s <- doA 100 s -- smt2 file size: 331 kb s <- selectLeft s MkRec s <- doA 100 s -- smt2 file size: 797 kb s <- selectLeft s MkRec s <- doA 300 s -- smt2 file size: 5 mb s <- selectLeft s MkRec s <- doA 400 s -- smt2 file size: 43 mb s <- selectLeft s MkRec s <- doA 500 s -- smt2 file size: 385mb s <- selectRight s end s {-@ assume doA :: Typestate s => v1:Int -> A Int s -> RIO<{\w -> lastVal w < v1}, {\w1 b w2 -> lastVal w2 = v1}> s @-}doA :: Typestate s => Int -> A Int s -> RIO s doA i (A s) = return s {-@ end :: End -> RIO <{\x -> true}, {\w1 b w2 -> Pure w1 w2}> () @-}end :: End -> RIO () end (End s) = return () {-@ assume selectLeft :: Typestate s => Branch s_1 s_2 -> RIO<{\w1 -> true}, {\w1 v w2 -> Pure w1 w2 }> s_1 @-}selectLeft :: (Typestate s_1) => Branch s_1 s_2 -> RIO s1 selectLeft (A ) = return $ newS {-@ assume selectRight :: Typestate s => Branch s_1 s_2 -> RIO<{\w1 -> true}, {\w1 v w2 -> Pure w1 w2}> s_2 @-}selectRight :: (Typestate s_2) => Branch s_1 s_2 -> RIO s2 selectRight (A ) = return $ newS -- recursive constructors--class Typestate s where newS :: s instance Typestate s => Typestate (A a s) where newS = A newS instance Typestate End where newS = End () instance Typestate () where newS = () instance Typestate Rec where newS = MkRec $ newS {-@ data RIO a Bool, q :: World -> a -> World -> Bool> = RIO (runState :: (x:World
-> (a, World)<\w -> {v:World | true}>)) @-}data RIO a = RIO {runState :: World -> (a, World)} {-@ runState :: forall Bool, q :: World -> a -> World -> Bool>. RIO <p, q> a -> xyy:World
-> (a, World)<\w -> {v:World | true}> @-} {-@ measure lastVal :: World -> Int @-}{-@ predicate Pure W1 W2 = W1 = W2 @-}data World = W {-@ assume emptyWorld :: {w:World | lastVal w = 0} @-}emptyWorld :: World emptyWorld = W instance Functor RIO where fmap = undefined instance Applicative RIO where pure = undefined (<*>) = undefined instance Monad RIO where{-@ instance Monad RIO where >>= :: forall Bool , p2 :: a -> World -> Bool , r :: a -> Bool , q1 :: World -> a -> World -> Bool , q2 :: a -> World -> b -> World -> Bool , q :: World -> b -> World -> Bool>. {x::a, w::World
|- World <: World} {w::World
, x::a, w1:: World, w2::{v:World | v == w1}, y::b|- World <: World} {x::a, w::World
, w2::World|- {v:a | v = x} <: a} RIO <p, q1> a -> (x:a -> RIO <{v:World | true}, \w1 y -> {v:World | true}> b) -> RIO <p, q> b ; >> :: forall Bool , p2 :: World -> Bool , q1 :: World -> a -> World -> Bool , q2 :: World -> b -> World -> Bool , q :: World -> b -> World -> Bool>. {x::a, w::World
|- World <: World} {w::World
, w2::World, y::a, w3:: {v:World | v == w2}, x::b |- World <: World} RIO <p, q1> a -> RIO <p2, q2> b -> RIO <p, q> b ; return :: forall Bool>. x:a -> RIO <p, \w0 y -> {w1:World | w0 == w1 && y == x}> a @-} (RIO g) >>= f = RIO $ \x -> case g x of {(y, s) -> (runState (f y)) s} (RIO g) >> f = RIO $ \x -> case g x of {(y, s) -> (runState f ) s} return w = RIO $ \x -> (w, x)

Also, just in case, I'm using the following versions, although I did try with a few variations.

stack.yamlpackages:

. extra-deps:

Diff-0.3.4

git: https://github.com/ucsd-progsys/liquidhaskell https://urldefense.proofpoint.com/v2/url?u=https-3A__github.com_ucsd-2Dprogsys_liquidhaskell&d=DwQCaQ&c=-35OiAkTchMrZOngvJPOeA&r=r3JfTqNkpwIJ1InE9-ChC2ld7xwATxgUx5XHAdA0UnA&m=5ma5h_7WV9WwFsydv-99pV0XI2ySVpYa6FwPDgo_uiNC3HSEgJk_TBQOiROrLM9k&s=L1B_P78IVM-lXUxinP49u43aqq8Y21s7nwLeouOLhdM&e= commit: 154c5006a51e182d214e38e59b35e22de7d70df7 subdirs:

.

liquid-base

liquid-ghc-prim

liquid-containers

liquid-prelude

git: https://github.com/ucsd-progsys/liquid-fixpoint https://urldefense.proofpoint.com/v2/url?u=https-3A__github.com_ucsd-2Dprogsys_liquid-2Dfixpoint&d=DwQCaQ&c=-35OiAkTchMrZOngvJPOeA&r=r3JfTqNkpwIJ1InE9-ChC2ld7xwATxgUx5XHAdA0UnA&m=5ma5h_7WV9WwFsydv-99pV0XI2ySVpYa6FwPDgo_uiNC3HSEgJk_TBQOiROrLM9k&s=urI0dlbiLTcJ-YXH-SwzEfIV62KkQAjRh9wzeY9EPYc&e= commit: b91e279b8dd3a4716372692d2126ffcb90f5e5a3

git: https://github.com/zgrannan/rest https://urldefense.proofpoint.com/v2/url?u=https-3A__github.com_zgrannan_rest&d=DwQCaQ&c=-35OiAkTchMrZOngvJPOeA&r=r3JfTqNkpwIJ1InE9-ChC2ld7xwATxgUx5XHAdA0UnA&m=5ma5h_7WV9WwFsydv-99pV0XI2ySVpYa6FwPDgo_uiNC3HSEgJk_TBQOiROrLM9k&s=I_5Vba102tTWy_zAPALd_6u6XVCIogljcLgrYV5UHjg&e= commit: 1cadb23edfbc393245ae964315b07f5c8581ea9f

@.***:d60cad00223d46172020c136e68acef0481a47d0302b2e74b1805b4f3a446a9b,5389 resolver: nightly-2022-03-10compiler: ghc-8.10.7 allow-newer: true

— Reply to this email directly, view it on GitHub https://urldefense.proofpoint.com/v2/url?u=https-3A__github.com_ucsd-2Dprogsys_liquidhaskell_issues_1959&d=DwMCaQ&c=-35OiAkTchMrZOngvJPOeA&r=r3JfTqNkpwIJ1InE9-ChC2ld7xwATxgUx5XHAdA0UnA&m=5ma5h_7WV9WwFsydv-99pV0XI2ySVpYa6FwPDgo_uiNC3HSEgJk_TBQOiROrLM9k&s=e5QlUfCdJIEF16Ouv7lqgJVPfmhp1gFlSgzdxDt0sHc&e=, or unsubscribe https://urldefense.proofpoint.com/v2/url?u=https-3A__github.com_notifications_unsubscribe-2Dauth_AAMS4OANPROD3D5CV6XCFDTVDEAB5ANCNFSM5SMQNA3A&d=DwMCaQ&c=-35OiAkTchMrZOngvJPOeA&r=r3JfTqNkpwIJ1InE9-ChC2ld7xwATxgUx5XHAdA0UnA&m=5ma5h_7WV9WwFsydv-99pV0XI2ySVpYa6FwPDgo_uiNC3HSEgJk_TBQOiROrLM9k&s=mf7xnrHrHbXcPKuRsAMnrLd-NmyruRmanjP5c3DXBFI&e= . You are receiving this because you are subscribed to this thread.Message ID: @.***>

ucsd-progsys / liquidhaskell

rio monad smt2 file explosion #1959

stack.yamlpackages: