Unsoundly Proving 1 = 2 and false

[rachel960122]

I was playing with the infinite list data structure described in the ICFP '14 paper (section 5.2) in order to explore how Liquid Haskell handles non-termination. I've got the following definition for infinite list (based on the original definition from the paper):

{-@ data L [length] a <p :: L a -> Bool> = N | C { x :: a, xs :: L<p> a <<p>> } @-}
data L a = N | C a (L a)

{-@ type Stream a = {xs: L <{\v -> not (emp v)}> a | not (emp xs) } @-}

{-@ measure length @-}
{-@ length :: L a -> Nat @-}
length :: L a -> Int
length N = 0
length (C _ xs) = 1 + length xs

{-@ reflect emp @-}
emp :: L a -> Bool
emp N         = True
emp (C x xs)  = False

Then @goldfirere and I wrote the following proof, which was successfully verified:

-- Proof that Stream is infinite
{-@ thmStreamInf :: xs:Stream a -> { 1 == 2 } @-}
thmStreamInf :: L a -> Proof
thmStreamInf N = error "never happens"
thmStreamInf (C x xs) = thmStreamInf xs *** QED

Consequently, we could use thmStreamInf to prove {1 == 2}, for example:

{-@ silly :: { 1 == 2 } @-}
silly = thmStreamInf (repeat 3)

{-@ lazy repeat @-}
{-@ repeat :: a -> Stream a @-}
repeat x = C x (repeat x)

Now we could prove something that's simply false, for example:

{-@ abs :: Int -> Nat @-}
abs :: Int -> Int
abs x = x

where the definition of abs does not always return a Nat.

Any thoughts on why this might have happened? In particular, what are the exact reasons why thmStreamInf was verified?

[ranjitjhala]

Thanks @rachel960122 and @goldfirere

Yes, lazy is an unsafe escape hatch for locally disabling the termination checker and here's a simplified variant of your code that is still accepted by LH.

{-@ diverge :: Int -> {false} @-}
{-@ lazy diverge @-}
diverge :: Int -> Int
diverge n = diverge n

{-@ one_eq_two :: { 1 == 2 } @-}
one_eq_two = diverge 0

@niki I think either @goldfirere or @nomeata (or both!) suggested we should try to make a list of known sources of unsoundness like the above, the negative datatype and so on. Do you know if we have one? Else can start?

Thanks!

[The solution for the above is to use the strata thing, so any value computed from lazy value is also marked lazy; and to then tell users that a real proof should not be marked lazy ... ]

[nikivazou]

There exists an issue on how to break the termination checker. Other than that, there is no list of unsoundness. But, to be sound you need to have the termination checker on. Are there more sources of unsoundness other than divergence?

[ranjitjhala]

Maybe we can just generalize the other issue to be "known unsoundness" ?

…

On Fri, Jun 22, 2018 at 1:33 PM Niki Vazou ***@***.***> wrote: There exists an issue on how to break the termination checker. Other than that, there is no list of unsoundness. But, to be sound you need to have the termination checker on. Are there more sources of unsoundness other than divergence? — You are receiving this because you commented. Reply to this email directly, view it on GitHub <#1339 (comment)>, or mute the thread <https://github.com/notifications/unsubscribe-auth/ABkuOJRfrA6sv3HN6UhWV10YYmfSZLXoks5t_VR3gaJpZM4UzKVF> .

[jprider63]

I have a feature request related to this: Provide a flag to give a warning whenever a function is potentially unsound (when assume is used, when a function is marked lazy, when a proof uses undefined, etc).

[nikivazou]

That is a good point!

Following Safe Haskell we can have a SAFE flag that checks you have not used undefined or any of the unsound flags (e.g., no-termination, lazy, no-totality). Or we can go the other way and allow these unsafe flags only when you also enable the UNSOUND flag.

[goldfirere]

So it sounds like the ideas from the "Refinement Types for Haskell" paper around stratification is unimplemented. Is that right? We were working from Sec. 5.2 of that paper which introduces lazy but does not declare that doing so is unsafe. Have I missed something?

[nikivazou]

The stratification is deprecated. (There was an implementation back then, but since it was not actually used for other than this paper's benchmarks, it did not survive all the refactoring.)

As described in this paper, to soundly reason about lazy expressions (e.g., expressions that do not provably terminate assuming CBV) you need strata, which does not exist in the current LH branch.

[nikivazou]

@goldfirere also, I have a claim that, you can use all these strata to do strictness analysis.
Let me know if you want to discuss it!

[goldfirere]

It's a shame LH no longer supports infinite structures, but I suppose there hasn't been a demand from your users. And, I'm not surprised that the strata and strictness are closely linked -- it would seem you essentially have to do strictness analysis to calculate the strata.

As @ranjitjhala suggested above, perhaps this is really a documentation bug. If we know that lazy means "I promise this terminates" rather than "I want to write a non-terminating function", then the result is unsurprising.

[ranjitjhala]

@nikivazou do you mean that instead of lazy one should use the strata mechanism for code like repeat ?

[buggymcbugfix]

@nikivazou I think your suggestion to have an UNSOUND (or maybe --prove-bottom?) flag would make a lot of sense. This would make explicit that you are potentially proving nonsense.