module RG where
import Data.IORef as R
{- Liquid Rely-Guarantee References / RG-Haskell
This is an embedding of a slightly simplified rely-guarantee reference system.
(See "Rely-Guarantee References for Refinement Types over Aliased Mutable Data,"
by Gordon, Ernst, and Grossman, PLDI'13. I promise to never use such a long paper
title ever again.)
The key idea in that paper is to augment each reference with a predicate refining
the referent and heap reachable from it, and binary relations describing permitted
local actions (the guarantee) and possible remote actions (the rely):
ref{T|P}[R,G]
The terminology comes from rely-guarantee reasoning, from the concurrent program
logic literature. As long as
each reference's guarantee relation is a subrelation of any alias's rely (plus some
subtle side conditions about nested references), any predicate P that is /stable/
with respect to a rely R on a given reference (forall x y, P x -> R x y -> P y)
is trivially preserved by any update through an alias that respects that alias's
guarantee relation.
Embedding into Liquid Haskell instead of Coq requires a few weakenings of the
original design, so we lose expressiveness but gain substantially from automation
and being a refinement of a language with real programs! The main simplifications are:
- TEMPORARILY, rely and guarantee are the same, until we get rolling. In general,
we must always have that the guarantee implies the rely, since Haskell wouldn't
respect the substructural restrictions. Leaving them the same makes weakening the
guarantee unsound, so we should fix this soon.
- Predicates and relations can refer only to the immediate referent for now.
- Folding (pushing a local restriction through to new references reached via
dereference) doesn't exist in this system, mostly because all predicates and
relations can restrict only one cell.
-}
{- We wrap IORefs in a new constructor to add ghost parameters for the predicate and
relation(s). It is a standard GHC optimization to eliminate the overhead since there is a single
constructor with one physical argument, so at runtime these will look the same as IORefs:
we won't pay time or space overhead. -}
{-@ data RGRef a Bool, r :: a -> a -> Bool>
= Wrap (rr :: R.IORef a

) @-}
data RGRef a = Wrap (R.IORef a)
{- A stability proof can be embedded into LH as a function of type:
x:a

-> y:a -> {v:a

| v = y}
This encodes the requirement that knowing P x and R x y is sufficient to deduce P y.
-}
-- Requires explicit type anno for LH type to refine the inferred Haskell type
{-@ stable_monocount :: x:{v:Int | v > 0 } -> y:{v:Int | x <= v } -> {v:Int | ((v = y) && (v > 0)) } @-}
stable_monocount :: Int -> Int -> Int
stable_monocount x y = y
-- Testing / debugging function
{-@ generic_accept_stable :: forall

Bool, r :: a -> a -> Bool >.
f:(x:a

-> y:a -> {v:a

| (v = y)}) ->
()
@-}
generic_accept_stable :: (a -> a -> a) -> ()
generic_accept_stable pf = ()
{-@ proves_reflexivity :: x:{v:Int | v > 0} -> y:{v:Int | v > 0} -> {v:Int | v > 0} @-}
proves_reflexivity :: Int -> Int -> Int
proves_reflexivity x y = x
test :: ()
test = generic_accept_stable proves_reflexivity
{-@ proves_nothing :: x:a -> y:a -> {v:a | (v = y)} @-}
proves_nothing :: a -> a -> a
proves_nothing x y = y --proves_nothing x y
{- TODO: e2 is a hack to sidestep the inference of false for r,
it forces r to be inhabited. -}
{-@ newRGRef :: forall

Bool, r :: a -> a -> Bool >.
e:a

->
e2:a ->
f:(x:a

-> y:a -> {v:a

| (v = y)}) ->
IO (RGRef

a) @-}
newRGRef :: a -> a -> (a -> a -> a) -> IO (RGRef a)
newRGRef e e2 stabilityPf = do {
r <- newIORef e;
return (Wrap r)
}
-- LH's assume statement seems to only affect spec files
{-@ readRGRef :: forall

Bool, r :: a -> a -> Bool >.
RGRef

a -> IO (a

) @-}
readRGRef (Wrap x) = readIORef x
-- TODO: full spec, fix pf type
writeRGRef :: RGRef a -> a -> (a -> a -> Bool) -> IO ()
writeRGRef (Wrap x) e pf = writeIORef x e
{- modifyRGRef :: forall

Bool, r :: a -> a -> Bool >.
r:(RGRef

a) ->
f:(x:a

-> a) ->
pf:(x:a

-> y:a -> {v:a

| (v = y)}) ->
IO () @-}
modifyRGRef :: RGRef a -> (a -> a) -> (a -> a -> a) -> IO ()
modifyRGRef (Wrap x) f pf = modifyIORef x (\ v -> pf v (f v))
--
--{- modifyRGRef' :: forall

Bool, r :: a -> a -> Bool >.
-- RGRef

a ->
-- f:(x:a

-> a) ->
-- IO () @-}
---- TODO: strictify, so we don't de-optimize modifyIORef' calls
--modifyRGRef' (Wrap x) f = modifyIORef x f
--
--
main = do {
r <- newRGRef 1 3 stable_monocount; -- SHOULD BE ref{Int|>0}[<=,<=]
-- Instead we get ref{Int|>0}[false,false] !
r2 <- newRGRef 2 9 proves_nothing; -- SHOULD BE ref{Int|>0}[havoc,havoc].
-- Instead we get ref{Int|>0}[false,false] !
--r3 <- newRGRef 3 10 proves_reflexivity; -- BAD, correctly rejected
return ()
}
-- What are the subtyping rules for data structure params that aren't
-- used within the structure?
{-@ unused_contra :: RGRef <{\x -> x > 0}, {\x y -> x <= y}> Int -> RGRef <{\x -> x > 0}, {\x y -> false}> Int @-}
unused_contra :: RGRef Int -> RGRef Int
unused_contra r = r
{-@ unused_covar :: RGRef <{\x -> x > 0}, {\x y -> false}> Int -> RGRef <{\x -> x > 0}, {\x y -> x <= y}> Int @-}
unused_covar :: RGRef Int -> RGRef Int
unused_covar r = r
-- It looks like there's simply no constraint!