Why not an unlifted kind like # for Proof? (undefined/error problems)

[rrnewton]

We found that when using liquid prover we can put an "undefined" for all our proofs.

Ideally, it would be nice to couple liquid Haskell to SafeHaskell for enforcing some (un)trusted code boundaries. I.e. it would be fine to have a "trustme" proof value for use in development, but it would be imported from an Unsafe module, and then we could ensure -XSafe files that also pass liquid really prove the things they claim to prove.

But if undefined or always serves as "trustme"... that's hard to rule out.

What if an existing unlifted type like Int# could serve as the Proof type alias?

@vikraman @vollmerm @RyanGlScott

[rrnewton]

Actually, unlifted types aren't a solution either. Error and undefined are poly-kinded, so GHC lets this through:

val :: () -> (# Int#, Int# #)
val () = undefined

If that were our Proof type we would still need to run it at runtime to find out if it has a non-bottom WHNF....

[nikivazou]

That is a very interesting point!

But yet even Coq has a todo tactic. I believe there are very few values that serve as "trust me" (error and undefined) which you can hide from import Predule hiding (undefined).

BTW, all proof files should have the totality flag on {-@ LIQUID "--totality" @-} otherwise it is again easy to construct bad proofs.

It would be sweet to soundly exclude undefined. Actually according to the theory in the Liquid Types for Haskell paper (http://goto.ucsd.edu/~nvazou/refinement_types_for_haskell.pdf) since undefined cannot be proven to converge, it should be trivially refined (ie. refined to true equivalently should not be refined to false). But the implementation does not exactly follow the theory of this paper. My only (weak) argument why we allow undefined to be instantiated to any refinement is that is convenient during development and that if one gets into using Liquid [Haskell/Prover] she will be more careful than using undefined. Again weak argument....

[rrnewton]

For cases where I don't trust the code (e.g. code/proof given to my server over the internet), it would be good to have some kind of compile-time distinction enforceable by the server, but it doesn't have to be -XSafe vs -XTrustworthy. It could also be a flag to liquid. Like liquid --strict or something to disallow holes.

Is there a way in a .spec file to give undefined a "bad" refinement type of some kind that would stop people from being able to use it in a proof?

Or perhaps such a strict mode could simply check for a blacklist of things (error, undefined, etc) in every expression of type Proof? Would that plus totality checking do the trick?

[ranjitjhala]

​Either of these two methods:

Is there a way in a .spec file to give undefined a "bad" refinement type of some kind that would stop people from being able to use it in a proof?

​and ​

Or perhaps such a strict mode could simply check for a blacklist of things (error, undefined, etc) in every expression of type Proof? Would that plus totality checking do the trick?

​should work.

@nikivazou would adding something like this to Prelude.spec

lazy undefined :: {v:a | False} ensure that:

(1) it is not added to the environment (thereby polluting it with FALSE) (2) it ​is treated as the above type during checking, thereby rejecting any uses?

—

You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub https://github.com/ucsd-progsys/liquidhaskell/issues/815#issuecomment-239593813, or mute the thread https://github.com/notifications/unsubscribe-auth/ABkuONM7YsFuSS6H4-eqUiI6NH0Trwgyks5qfR16gaJpZM4JjXQa .

[nikivazou]

@ranjitjhala the only semantics of lazy in the implementation are that we do not check termination. So, I cannot see a way to enforce your suggestions.

The easiest way I see right now is to make sure that every proof file includes

import Prelude hiding (error, undefined, ..)
{-@ LIQUID "--totality" @-}

and in the near future create a flag --LSafe than enforces the above.

[rrnewton]

Do error and undefined cause any problems in non-Proof expressions? I.e. is it sufficient to syntactically check that these exact bindings are not used within the proof expressions or must they not be imported at all for an entire module? Erk, with polymorphism, can liquid distinguish which expressions are proof expressions?

Enforcement at the module layer seems tricky because of reexports from other places. If checking at the variable reference sites it may be easier to conclude if the symbol is really "error", peering through reexports. (I don't know - @RyanGlScott?) But, either way, blacklisting seems challenging. How do we stop other modules from creating new wrappers around or aliases to these blacklisted values and us importing them?

module Naughty(naughty) where
naughty x = error x

@ranjitjhala Is there a check that {v:a | False} does not get added to the environment? (I thought that type would just let us prove anything?)

[gridaphobe]

Checking that false doesn't get into the environment is tricky because we actually want it in local environments, when we need to show a contradiction. Take head for example.

{-@ head :: {v:[a] | len v > 0} -> a @-}
head xs = case xs of
  []  -> error "empty"
  x:_ -> x

We effectively want to prove that the [] branch is unreachable. We do this by combining the top-level refinement xs :: {v:[a] | len v > 0} with the branch-condition xs = [], where [] :: {v:[a] | len v = 0}. When you conjoin the two refinements you get xs :: {v:[a] | len v > 0 && len v = 0} which implies xs :: {v:[a] | false}. This is what lets us prove that the call to error is safe, because it can't actually happen!

That's only for local environments though, if false gets into the global environment, then we're in quite a bit of trouble, so a global check would be good. I believe we already accomplish this though, by checking whether false occurs in the solution to the k-vars.

---

I'm actually a bit curious about how undefined is causing problems. We don't actually give undefined a type, so even if you use it, it should have the type

undefined :: {v:a | true}

because we default all exports to a true type unless an explicit signature is given.

So undefined shouldn't actually be very useful in proving things at the LH level. Do you have an example we can look at? Or perhaps there's something else I'm missing?

[ranjitjhala]

@gridaphobe, the trouble is in the a which gets instantiated with anything, and since the a is unconstrained, it can be inferred as false.

e.g. you can prove:

undefined :: forall a. a

bogus :: {v:Int | v = 22}
bogus = undefined @ Int

Note that in the above the "false" refines the Int to which the undefined is instantiated.

@rrnewton: one super easy fix (?) could be the one Eric suggests, namely in --strict mode (with --totality and --termination) additionally promote the "WARNING" that we currently report when you have

unconstrained-refinements-solved-to-false

(as in bogus above) to "ERROR" that reject the program? @gridaphobe -- this would not break the path-sensitive stuff either.

@nikivazou: any thoughts?

On Mon, Aug 15, 2016 at 5:36 PM, Eric Seidel notifications@github.com wrote:

Checking that false doesn't get into the environment is tricky because we actually want it in local environments, when we need to show a contradiction. Take head for example.

{-@ head :: {v:[a] | len v > 0} -> a @-}head xs = case xs of [] -> error "empty" x:_ -> x

We effectively want to prove that the [] branch is unreachable. We do this by combining the top-level refinement xs :: {v:[a] | len v > 0} with the branch-condition xs = [], where [] :: {v:[a] | len v = 0}. When you conjoin the two refinements you get xs :: {v:[a] | len v > 0 && len v = 0} which implies xs :: {v:[a] | false}. This is what lets us prove that the call to error is safe, because it can't actually happen!

That's only for local environments though, if false gets into the global environment, then we're in quite a bit of trouble, so a global check would be good. I believe we already accomplish this though, by checking whether

false occurs in the solution to the k-vars.

I'm actually a bit curious about how undefined is causing problems. We don't actually give undefined a type, so even if you use it, it should have the type

undefined :: {v:a | true}

because we default all exports to a true type unless an explicit signature is given.

So undefined shouldn't actually be very useful in proving things at the LH level. Do you have an example we can look at? Or perhaps there's something else I'm missing?

— You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub https://github.com/ucsd-progsys/liquidhaskell/issues/815#issuecomment-239970423, or mute the thread https://github.com/notifications/unsubscribe-auth/ABkuOHgL3NJ_ClUOiodNy4TFN-exuAKrks5qgQYHgaJpZM4JjXQa .

[nikivazou]

@ranjitjhala it seems to me that this strategy will break the path-sensitive stuff, since unconstraint refinements in the cases are solved to false to prove dead code.

[ranjitjhala]

@nikivazou -- no the "dead code" proofs are not from unconstrained kvars but from proper contradictions. Thus I don't think this approach will break those proofs.

Btw this reminds me: the old fixpoint had an option --true-unconstrained perhaps we can add it to the new fixpoint and see what happens? (It may already be implemented...)

[nikivazou]

These contradictions may appear while solving k vars. But I agree that in most cases it will be proper contradictions. We shall try it and see if anything breaks

On Aug 17, 2016 4:22 AM, "Ranjit Jhala" notifications@github.com wrote:

@nikivazou https://github.com/nikivazou -- no the "dead code" proofs are not from unconstrained kvars but from proper contradictions. Thus I don't think this approach will break those proofs.

Btw this reminds me: the old fixpoint had an option --true-unconstrained perhaps we can add it to the new fixpoint and see what happens? (It may already be implemented...)

— You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub https://github.com/ucsd-progsys/liquidhaskell/issues/815#issuecomment-240288007, or mute the thread https://github.com/notifications/unsubscribe-auth/AArotU2pxmbulOkLfDPkuh_L_-2Ah_XGks5qgmJlgaJpZM4JjXQa .