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!
{"ft_lang_label":"__label__en","ft_lang_prob":0.6981797,"math_prob":0.9482261,"size":9448,"snap":"2019-26-2019-30","text_gpt3_token_len":3074,"char_repetition_ratio":0.20298602,"word_repetition_ratio":0.8072585,"special_character_ratio":0.40707028,"punctuation_ratio":0.19602577,"nsfw_num_words":0,"has_unicode_error":false,"math_prob_llama3":0.9905271,"pos_list":[0],"im_url_duplicate_count":[null],"WARC_HEADER":"{\"WARC-Type\":\"response\",\"WARC-Date\":\"2019-07-23T03:53:11Z\",\"WARC-Record-ID\":\"<urn:uuid:9168eb18-1254-46d9-9442-953ac87e6441>\",\"Content-Length\":\"6396\",\"Content-Type\":\"application/http; msgtype=response\",\"WARC-Warcinfo-ID\":\"<urn:uuid:028dbb2f-38a9-4a96-923a-8a3052b08978>\",\"WARC-Concurrent-To\":\"<urn:uuid:50499370-1a92-45d2-9c85-2144147434ba>\",\"WARC-IP-Address\":\"151.101.248.68\",\"WARC-Target-URI\":\"http://hackage.haskell.org/package/liquidhaskell-0.8.0.1/src/tests/neg/RG.hs\",\"WARC-Payload-Digest\":\"sha1:F2YOMWP6XFXI5KGGXCCUCPST6VIBKH2E\",\"WARC-Block-Digest\":\"sha1:FRITDRVVA5PTWOOEBEZRRNPEYMMRH6NW\",\"WARC-Identified-Payload-Type\":\"text/x-haskell\",\"warc_filename\":\"/cc_download/warc_2019/CC-MAIN-2019-30/CC-MAIN-2019-30_segments_1563195528687.63_warc_CC-MAIN-20190723022935-20190723044935-00344.warc.gz\"}"}