Unsound: LH checks incorrect program with diverging value

[lbartl]

I read the Refinement Types For Haskell, ICFP 2014 paper and came up with a similar example that uses a diverging value:

{-@ lazy diverge @-}
{-@ diverge :: {v:a | false} @-}
diverge = diverge

{-@ false_precond :: {v:a | false} -> Int -> {v:Int | v > 0} @-}
false_precond :: a -> Int -> Int
false_precond _ y = y

explode :: Int -> Int
explode x = x `div` false_precond diverge 0

LH checks that program and marks it as SAFE, but it is incorrect:

> explode 1
*** Exception: divide by zero

The following may be related: The paper says that this test_collatz function cannot be verified (though it is correct):

{-@ lazy collatz @-}
{-@ collatz :: Pos -> {v: Int | v == 1} @-}
collatz :: Int -> Int
collatz 1 = 1
collatz n
  | even n    = collatz $ n `div` 2
  | otherwise = collatz $ 3*n + 1

test_collatz = let x = collatz 10 in 12 `div` x + 1

But LH checks it and marks it as SAFE.

[ranjitjhala]

Hi @hanswurst862 -- this is not a bug: the lazy annotation means "all bets are off" (kind of like unsafe blocks in rust). So yes, if you have a binder like that in scope then you will be able to "prove" all sorts of spurious things, as essentially, you have "assumed" a contradiction to begin with.

[lbartl]

@ranjitjhala Thanks for your answer.

I had a different understanding of lazy. According to the paper:

The lazy keyword deactivates termination checking, and marks the output as a Div type.

I had the understanding that this means that one should use lazy for non-terminating functions and LH will respect that and will not „prove“ „spurious things“ because it marks the output as a Div type (like explained in the paper).

If this is not the case (lazy = unsafe), then how should one safely annotate functions that do not terminate?

[ranjitjhala]

Ah yes, very good (let me reopen so we fix it). We jettisoned the Div stuff as it was super rare, complicated the code. Instead, its just simpler to eyeball in the rare cases that you use lazy that there are no (output) refinements.

So effectively right now with lazy the semantics are only:

(1) termination checking is disabled all bets are off

Now you have two choices: to be on the safe side you can

(2) make sure there are no output refinements on lazy term

or if you are confident that the code is in fact terminating and you need an escape hatch you can add the refinements too.

I suppose it may make sense to have a strict or safe mode which specifically checks (2).

[lbartl]

Ok, so basically the paper is old news?

I don't think (2) is sufficient. This code does not use output refinements on lazy terms, is incorrect and LH says it's safe:

{-@ lazy diverge @-}
diverge :: a
diverge = diverge

{-@ false_precond :: {v:a | false} -> Int -> {v:Int | v > 0} @-}
false_precond :: a -> Int -> Int
false_precond _ y = y

explode :: Int -> Int
explode x = x `div` false_precond diverge 0

[ranjitjhala]

Aha yes @nikivazou favorite polymorphic instantiation issue :-) (That introduces refinements at instantiation - that too must be stopped for lazy functions - at least in a “strict” or “safe” mode)

On Thu, Nov 11, 2021 at 7:29 AM Lukas Bartl @.***> wrote:

Ok, so basically the paper is old news?

I don't think (2) is sufficient. This code does not use output refinements on lazy terms, is incorrect and LH says it's safe:

{-@ lazy diverge @-}diverge :: a diverge = diverge {-@ false_precond :: {v:a | false} -> Int -> {v:Int | v > 0} @-}false_precond :: a -> Int -> Int falseprecond y = y explode :: Int -> Int explode x = x div false_precond diverge 0

— You are receiving this because you modified the open/close state.

Reply to this email directly, view it on GitHub https://urldefense.proofpoint.com/v2/url?u=https-3A__github.com_ucsd-2Dprogsys_liquidhaskell_issues_1903-23issuecomment-2D966395846&d=DwMCaQ&c=-35OiAkTchMrZOngvJPOeA&r=r3JfTqNkpwIJ1InE9-ChC2ld7xwATxgUx5XHAdA0UnA&m=ZQjrMotPZz04OnmxZeeiejhN_iCQRc0qNNBaSG-Ydn1TZQbKkDp1HHGOOcuG_t-D&s=8L19OgpmkylwewAMSf0ki-_MXFWP_MW0zwiyOu2mvTE&e=, or unsubscribe https://urldefense.proofpoint.com/v2/url?u=https-3A__github.com_notifications_unsubscribe-2Dauth_AAMS4OAURG3WCCKSTVAMQY3ULPOOXANCNFSM5H2LVJIA&d=DwMCaQ&c=-35OiAkTchMrZOngvJPOeA&r=r3JfTqNkpwIJ1InE9-ChC2ld7xwATxgUx5XHAdA0UnA&m=ZQjrMotPZz04OnmxZeeiejhN_iCQRc0qNNBaSG-Ydn1TZQbKkDp1HHGOOcuG_t-D&s=Z05l1F-KBFtwTAwmpcUxV8k6LkM996oHjx6wvxYpFuE&e= . Triage notifications on the go with GitHub Mobile for iOS https://urldefense.proofpoint.com/v2/url?u=https-3A__apps.apple.com_app_apple-2Dstore_id1477376905-3Fct-3Dnotification-2Demail-26mt-3D8-26pt-3D524675&d=DwMCaQ&c=-35OiAkTchMrZOngvJPOeA&r=r3JfTqNkpwIJ1InE9-ChC2ld7xwATxgUx5XHAdA0UnA&m=ZQjrMotPZz04OnmxZeeiejhN_iCQRc0qNNBaSG-Ydn1TZQbKkDp1HHGOOcuG_t-D&s=wmrml8LA0VqRPrQ1pl_6DxfwEEIorVrrkPZzU8cUi1A&e= or Android https://urldefense.proofpoint.com/v2/url?u=https-3A__play.google.com_store_apps_details-3Fid-3Dcom.github.android-26referrer-3Dutm-5Fcampaign-253Dnotification-2Demail-2526utm-5Fmedium-253Demail-2526utm-5Fsource-253Dgithub&d=DwMCaQ&c=-35OiAkTchMrZOngvJPOeA&r=r3JfTqNkpwIJ1InE9-ChC2ld7xwATxgUx5XHAdA0UnA&m=ZQjrMotPZz04OnmxZeeiejhN_iCQRc0qNNBaSG-Ydn1TZQbKkDp1HHGOOcuG_t-D&s=qhDSgzI3XDfEG3ncOFA9-E0ozP3KNBHkrVKV3M5QrN8&e=.

[nikivazou]

For me too, the lazy or no-termination annotations means potential unsoundness. In the ICFP'14 paper we have ways to address this (1) do not allow refinementments on potential diverging expressions and 2) via the label mechanism we propose) but the code that implemented these did not survive...

[yanhasu]

On the current demo, lazy seems to postulate finite return type ('Fin type') as well eventual reduction to WHNF ('Wnf type').

So I'm guessing that Wnf has been jettisoned as well as Div, and now Fin is all that's left?

[facundominguez]

I'm closing since the initial example seems to be clarified. Still, it is unclear to me if further action would be wanted. In that case, I suggest starting a new issue.