Unfold-unfolded definitions when the extentionality flag is active #704

AlecsFerra · 2024-09-10T15:25:51Z

When trying to prove pretty trivial statements PLE gives up because is not unfolding enough the definitions or lambdas: see the following examples:

{-@ LIQUID "--reflection"                @-}
{-@ LIQUID "--ple"                       @-}
{-@ LIQUID "--full"                      @-}
{-@ LIQUID "--extensionality"            @-}
{-@ LIQUID "--dump-opaque-reflections"   @-}
{-@ LIQUID "--ple-with-undecided-guards" @-}

module Example where

{-@ reflect f @-}
f :: Int -> Int
f x = 13

{-@ reflect g @-}
g :: Int -> Int -> Int
g x y = f y

{-@ reflect k @-}
k :: Int -> Int -> Int
k x y = 13


{-@ complexProof :: { f = (\x:Int -> 13) } @-}
complexProof :: ()
complexProof = ()

{-@ complexProof' :: { g = k } @-}
complexProof' :: ()
complexProof' = ()

AlecsFerra · 2024-09-10T15:26:24Z

I have ran all the tests in the liquid-haskell repo and they are passing

facundominguez · 2024-09-10T15:39:29Z

👋 Hello @AlecsFerra. The following works for me.

{-@ LIQUID "--ple"                       @-}

module Example where

{-@ reflect f @-}
f :: Int -> Int
f x = 13

{-@ reflect g @-}
g :: Int -> Int -> Int
g x y = f y

{-@ reflect k @-}
k :: Int -> Int -> Int
k x y = 13


{-@ complexProof' :: x:Int -> y:Int -> { g x y = k x y } @-}
complexProof' :: Int -> Int -> ()
complexProof' _ _ = ()

Enabling --extensionality seems to break it, though.

I don't know how to deal with the lambda in the first lemma. But my intuition is that functions like f need to be applied to actual arguments before they can be unfolded.

AlecsFerra · 2024-09-10T15:46:18Z

The thing is that the extensionality flag is adding some "fake" variables that prevent the unfoldings

AlecsFerra · 2024-09-10T15:47:06Z

So it should pass without adding the extra arguments to the proof

facundominguez

Thanks for the PR.

I need some help understanding the problem, I think. My comment below contains my first questions.

Also, before merging, looks like some new tests are going to be needed here and in liquidhaskell.

facundominguez · 2024-09-10T15:54:37Z

src/Language/Fixpoint/Solver/PLE.hs

@@ -458,6 +460,8 @@ data EvalEnv = EvalEnv
                                    -- an expression
  , evSMTCache :: M.HashMap Expr Bool -- ^ Whether an expression is valid or its negation
  , evFuel     :: FuelCount
+  , unfoldedDefinitions :: S.HashSet Symbol -- ^ Functions that we have already unfolded


Thinking about documentation:

unfoldedDefinitions seems to be used to inhibit unfolding of some saturated function application, for instance length xs. However, it would also inhibit unfolding of length ys. Is this necessary?

Also, the scope in which a function is inhibited from unfolding needs to be made explicit. It seems to be inhibited only when scanning for more applications to unfold, in the result of the first unfolding (eval γ ctx et e3' below). Why?

Technically we could keep in the unfolded set of also arguments of the call (Symbol, [Expr]) but I'm worried that it could be tricked to end in an infinite loop somehow since the termination checking happens after this code is ran

I don't understand your second comment sorry

but I'm worried that it could be tricked to end in an infinite loop somehow

How would PLE enter an infinite loop if unfoldedDefinitions isn't introduced at all?

I don't understand your second comment sorry

This ties to the motivation of unfoldedDefinitions which isn't clear to me yet. Symbols aren't kept in unfoldedDefinitions forever, they are removed with unsetUnfolded. And I'm asking how did you choose when to call unsetUnfolded.

For the proofs I wanted to wait for some comments about the PR (both on the implementation and on the idea) hence why is marked as a draft,

I hadn't noticed this PR was marked as a draft. Collecting feedback sounds good.

Take as an example

{-@ LIQUID "--reflection" @-} {-@ LIQUID "--ple" @-} {-@ LIQUID "--full" @-} {-@ LIQUID "--extensionality" @-} {-@ LIQUID "--ple-with-undecided-guards" @-} module Example where {-@ reflect f @-} f :: Int -> Int f n = if n > 0 then f n + n else 0 {-@ reflect g @-} g :: Int -> Int -> Int g x y = f 3 {-@ complexProof :: { g = (\x:Int -> (\y:Int -> 3)) } @-} complexProof :: () complexProof = ()

Even tough LH is able to infer that f is non terminating, LH will try to look for some other errors so when trying to prove complexProof will start with the unfolding of g so it will try to unfold f 3 so it will try to unfold then then branch of the body of f and so on till we finish the space for the call stack.

You can try it by your self by commenting away L807.

Cool thing :) we have infinite loops only in non terminating programs we dont have infinite loops in programs that are safe

{-@ LIQUID "--reflection" @-} {-@ LIQUID "--ple" @-} {-@ LIQUID "--full" @-} {-@ LIQUID "--extensionality" @-} {-@ LIQUID "--ple-with-undecided-guards" @-} module Example where {-@ reflect f @-} f :: Int -> Int f n = if n > 0 then f (n - 1) + n else 0 {-@ reflect g @-} g :: Int -> Int -> Int g x y = f 3 {-@ complexProof :: { g = (\x:Int -> (\y:Int -> 6)) } @-} complexProof :: () complexProof = ()

For example this passes even without keeping track of the unfolded definitions

If its the case then I guess we can perform the same modification in the case I added at line 868, removing the recursive call call and modifying the return

we can perform the same modification in the case I added at line 868

The return in that case looks correct to me.

Yeah but I'm calling eval inside that case maybe it isn't needed if PLE decides by looking at what is returned it it wants to unfold again

Btw regarding making PLE diverge i think its our job to make LH terminate anyway, also before I added the infinite loop check, some test in the liquidhaskell repo was entering in the same infinite loop

Happy to discuss that further, but I don't think it affects the contribution in this PR. I'd propose to open a separate issue or PR for that sake.

AlecsFerra · 2024-09-10T18:01:30Z

The problem is the following:

morally

{-@ complexProof' :: x:Int -> y:Int -> { g x y = k x y } @-}
complexProof' :: Int -> Int -> ()
complexProof' _ _ = ()

and

{-@ complexProof' :: { g = k } @-}
complexProof' :: ()
complexProof' = ()

Have two different statements. we would like to LH to prove by itself the second statement as it's a common class of proofs that we have to do when performing higher order reasoning in LH.

As part of a project I'm proving the correctness of compiling terms of the lambda calculus to the SKI combinators:

See: https://gist.github.com/AlecsFerra/9d48ae08f63d8192b2267d0e378f8c09
You can see the file Try3.hs using the old PLE and Whole.hs using the new PLE
the proofs are much simpler (Try3.hs has the proof of only some of the statements, instead Whole.hs has a proof of all the statements)

AlecsFerra · 2024-09-10T18:03:38Z

For the proofs I wanted to wait for some comments about the PR (both on the implementation and on the idea) hence why is marked as a draft, I've already discussed about this with @nikivazou

AlecsFerra · 2024-09-10T18:21:51Z

Also forgot to mention this code works even if we drop the check for the extensionality flag, I've already tested running the tests in the main liquidhaskell repo, is just making the typechecker slower

nikivazou · 2024-09-11T06:20:00Z

Great! Let's not merge yet then, and keep it as draft until we come up with more tests.

hlint also complains :)

The tests on LH should not be slower if the extra unfoldings happen only when the extensionality flag is on, correct?

AlecsFerra · 2024-09-11T08:24:10Z

After the discussion with @facundominguez yesterday the fact that PLE wasn't unfolding recursively was a bug in PLE, so I decided to deleted my code that was dealing with function application and implement the fix that was suggested in the comments above.
That solutions leads PLE in an infinite loop in some cases (I personally believe that we should stop PLE like I was doing in my first commit).
Then I dont know if it still makes sense to hide this feature behind the extensionality flag, I'll run the benchmarks this afternoon.

I left the code that handles lambdas untouched and behind the extensionality flag.

AlecsFerra · 2024-09-11T08:37:33Z

Let me know if i should squash the commits

AlecsFerra · 2024-09-11T08:52:29Z

Regarding tests I think that we can reuse all the snippets in the discussion + the whole SKI compilation file for the liquid haskell main repo.

For the liquid fixpoint repo first I have to study the file format

AlecsFerra · 2024-09-11T09:52:03Z

Benchmarks:

AlecsFerra · 2024-09-11T10:05:35Z

I modified the case for the lambda application to make it behave the same as normal function application, I don't know if we have to handle the undecided guards thing

facundominguez

The code is looking good to me.

src/Language/Fixpoint/Solver/PLE.hs

facundominguez · 2024-09-11T11:08:46Z

I don't know if we have to handle the undecided guards thing

Edited this answer after posting, see next comment.

facundominguez · 2024-09-11T11:35:23Z

hm, evPendingUnfoldings does rather delay adding new equalities that may not be insightful. In length ys, most of the time it is not helpful to add an equality

length ys = if null ys then 0 else length ys + 1

unless the null ys condition can be decided.

For lambda expressions

(\xs -> if null xs then e0 else e1) ys

I think the question is: does it help most of the time to add an equality

(\xs -> if null xs then e0 else e1) ys = if null ys then e0 else e1

when the condition null ys cannot be decided? If it does help, then leave the code as is. If it doesn't, then imitate the non-lambda case.

AlecsFerra · 2024-09-11T14:55:08Z

No It helps as that equality is encoding "eta-equivalence" that before my PR it wasn't provable in LH

AlecsFerra · 2024-09-11T14:56:21Z

How do I get the .fq files? I can't find them in the .liquid directory.
I want them so that I can add the examples as tests in liquid-fixpoint

facundominguez · 2024-09-11T15:28:26Z

How do I get the .fq files?

{-@ LIQUID "--save" @-}

AlecsFerra · 2024-09-12T09:11:29Z

Let me know if those tests are enough

Feat: unfold-unfolded definitions when the extentionality flag is active

0c51b40

AlecsFerra marked this pull request as draft September 10, 2024 15:26

facundominguez reviewed Sep 10, 2024

View reviewed changes

Alessio Ferrarini and others added 2 commits September 11, 2024 10:26

Fixup (unfold-unfold) do not recurse inside evalApp

7f4b1f6

Chore: hlint

0ead02b

AlecsFerra changed the title ~~Unfolded-unfolded definitions when the extentionality flag is active~~ Unfold-unfolded definitions when the extentionality flag is active Sep 11, 2024

AlecsFerra added 2 commits September 11, 2024 12:02

Fixup: remove recusive call inside lambda application

f44f2d1

Chore: hlint

65eca14

facundominguez reviewed Sep 11, 2024

View reviewed changes

src/Language/Fixpoint/Solver/PLE.hs Outdated Show resolved Hide resolved

src/Language/Fixpoint/Solver/PLE.hs Outdated Show resolved Hide resolved

src/Language/Fixpoint/Solver/PLE.hs Outdated Show resolved Hide resolved

Chore: inlined isExtensionalityOn

fdea2c0

AlecsFerra marked this pull request as ready for review September 11, 2024 12:23

tests: add tests for ucsd-progsys#704

3d9aded

nikivazou approved these changes Sep 12, 2024

View reviewed changes

nikivazou merged commit 9765308 into ucsd-progsys:develop Sep 12, 2024
1 check passed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Unfold-unfolded definitions when the extentionality flag is active #704

Unfold-unfolded definitions when the extentionality flag is active #704

AlecsFerra commented Sep 10, 2024

AlecsFerra commented Sep 10, 2024

facundominguez commented Sep 10, 2024

AlecsFerra commented Sep 10, 2024

AlecsFerra commented Sep 10, 2024

facundominguez left a comment •

edited

Loading

facundominguez Sep 10, 2024 •

edited

Loading

AlecsFerra Sep 10, 2024

facundominguez Sep 10, 2024

AlecsFerra Sep 10, 2024

AlecsFerra Sep 10, 2024 •

edited

Loading

AlecsFerra Sep 10, 2024

facundominguez Sep 10, 2024

AlecsFerra Sep 10, 2024

AlecsFerra Sep 10, 2024

facundominguez Sep 11, 2024

AlecsFerra commented Sep 10, 2024 •

edited

Loading

AlecsFerra commented Sep 10, 2024

AlecsFerra commented Sep 10, 2024

nikivazou commented Sep 11, 2024

AlecsFerra commented Sep 11, 2024

AlecsFerra commented Sep 11, 2024

AlecsFerra commented Sep 11, 2024

AlecsFerra commented Sep 11, 2024

AlecsFerra commented Sep 11, 2024

facundominguez left a comment

facundominguez commented Sep 11, 2024 •

edited

Loading

facundominguez commented Sep 11, 2024 •

edited

Loading

AlecsFerra commented Sep 11, 2024

AlecsFerra commented Sep 11, 2024

facundominguez commented Sep 11, 2024

AlecsFerra commented Sep 12, 2024

Unfold-unfolded definitions when the extentionality flag is active #704

Unfold-unfolded definitions when the extentionality flag is active #704

Conversation

AlecsFerra commented Sep 10, 2024

AlecsFerra commented Sep 10, 2024

facundominguez commented Sep 10, 2024

AlecsFerra commented Sep 10, 2024

AlecsFerra commented Sep 10, 2024

facundominguez left a comment • edited Loading

Choose a reason for hiding this comment

facundominguez Sep 10, 2024 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

AlecsFerra Sep 10, 2024 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

AlecsFerra commented Sep 10, 2024 • edited Loading

AlecsFerra commented Sep 10, 2024

AlecsFerra commented Sep 10, 2024

nikivazou commented Sep 11, 2024

AlecsFerra commented Sep 11, 2024

AlecsFerra commented Sep 11, 2024

AlecsFerra commented Sep 11, 2024

AlecsFerra commented Sep 11, 2024

AlecsFerra commented Sep 11, 2024

facundominguez left a comment

Choose a reason for hiding this comment

facundominguez commented Sep 11, 2024 • edited Loading

facundominguez commented Sep 11, 2024 • edited Loading

AlecsFerra commented Sep 11, 2024

AlecsFerra commented Sep 11, 2024

facundominguez commented Sep 11, 2024

AlecsFerra commented Sep 12, 2024

facundominguez left a comment •

edited

Loading

facundominguez Sep 10, 2024 •

edited

Loading

AlecsFerra Sep 10, 2024 •

edited

Loading

AlecsFerra commented Sep 10, 2024 •

edited

Loading

facundominguez commented Sep 11, 2024 •

edited

Loading

facundominguez commented Sep 11, 2024 •

edited

Loading