LH runs forever on my code when totality checking is on

[michaelborkowski]

While attempting to mechanize a proof of type soundness and termination for a simply typed lambda calculus, I found that the module would pass as Safe when --no-totality is enabled, but LH will run forever (getting stuck during the "Working" phase) when --no-totality is turned off.

There's only one major proof here, called main_lemma. There's a 5-way case split on the typing derivation:

{-@ main_lemma :: e:Expr -> t:Type -> env:Env -> g:Ctx 
                -> ProofOf(HasType g e t) -> ProofOf(WBEnv env g)
                -> (Value, (BStep, WBValue))<{\v pfs ->
                      (propOf (fst pfs) == BStep env e v) && (propOf (snd pfs) == WBValue v t)}> @-} 
main_lemma :: Expr -> Type -> Env -> Ctx -> HasType -> WBEnv
                -> (Value, (BStep, WBValue))
main_lemma e t env g (TNum _g n)    _       = (VNum n, (ENum env n, WBVNum n))
main_lemma e t env g (TVar _g x _t) p_env_g = ...
main_lemma e t env g (TAdd _g e1 p_e1_Int e2 p_e2_Int) p_env_g = ...
main_lemma e t env g (TAbs _g x t1 e' t2 p_e2_t2) p_env_g = ...
main_lemma e t env g (TApp _g e1 t2 _t p_e1_t2t e2 p_e2_t2) p_env_g = ...

I also tried moving the type derivation up to be the first argument to main_lemma, but that didn't help either.

Other info:

With --no-totality the running time for Liquid Haskell went from relative fast to very slow (at least 5 mins) when I added in the last case to main_lemma

The rest of the code is here: https://github.com/michaelborkowski/liquidmeta/blob/master/STLC.hs

[ranjitjhala]

Thanks Michael, can you put it in a separate file/gist so it’s frozen? From the name it looks like this one may change over time?

On Fri, Jan 24, 2020 at 11:59 AM Michael Borkowski notifications@github.com wrote:

While attempting to mechanize a proof of type soundness and termination for a simply typed lambda calculus, I found that the module would pass as Safe when --no-totality is enabled, but LH will run forever (getting stuck during the "Working" phase) when --no-totality is turned off.

There's only one major proof here, called main_lemma. There's a 5-way case split on the typing derivation:

{-@ main_lemma :: e:Expr -> t:Type -> env:Env -> g:Ctx -> ProofOf(HasType g e t) -> ProofOf(WBEnv env g) -> (Value, (BStep, WBValue))<{\v pfs -> (propOf (fst pfs) == BStep env e v) && (propOf (snd pfs) == WBValue v t)}> @-} main_lemma :: Expr -> Type -> Env -> Ctx -> HasType -> WBEnv -> (Value, (BStep, WBValue)) main_lemma e t env g (TNum g n) = (VNum n, (ENum env n, WBVNum n)) main_lemma e t env g (TVar _g x _t) p_env_g = ... main_lemma e t env g (TAdd _g e1 p_e1_Int e2 p_e2_Int) p_env_g = ... main_lemma e t env g (TAbs _g x t1 e' t2 p_e2_t2) p_env_g = ... main_lemma e t env g (TApp _g e1 t2 _t p_e1_t2t e2 p_e2_t2) p_env_g = ...

I also tried moving the type derivation up to be the first argument to main_lemma, but that didn't help either.

Other info:

With --no-totality the running time for Liquid Haskell went from relative fast to very slow (at least 5 mins) when I added in the last case to main_lemma

The rest of the code is here: https://github.com/michaelborkowski/liquidmeta/blob/master/STLC.hs

— 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/1591?email_source=notifications&email_token=AAMS4OC2UO3YALRPMKX7GNTQ7NB7DA5CNFSM4KLLJTWKYY3PNVWWK3TUL52HS4DFUVEXG43VMWVGG33NNVSW45C7NFSM4IITP2EA, or unsubscribe https://github.com/notifications/unsubscribe-auth/AAMS4OBWQRYTMT5C64OOW7LQ7NB7DANCNFSM4KLLJTWA .

[nikivazou]

Thanks!

1. Have you set the --max-case-expand=INT flag?
2. Can you split your proof to modules where the main_lemma is the only function defined in the module? It would be easier for us to understand what triggers the leak then.

[michaelborkowski]

I've tried different values of --max-case-expand= but it didn't seem to have an effect.

Here's the module-ized version: https://github.com/michaelborkowski/liquidmeta/blob/master/snapshots/STLC_20200125/Lemma.hs

(the extra assignment statements are the workaround to issue 1394 )

[nikivazou]

@michaelborkowski I took a look at this, and with the totality check you are actually putting MANY things for LH to prove. So, it is expected to be so slow.

When you have totality check on, for, say data AOrB = A | B, if you write

... 
   where B = foo 5 

you ask LH to prove that foo 5 always returns B. In your code, you do such a thing on all the recursive calls of main_lemma.

My suggestion is to rewrite your proof as

{-@ main_lemma :: e:Expr -> t:Type -> env:Env -> g:Ctx -> ProofOf(HasType g e t) -> ProofOf(WBEnv env g) -> (Value, (BStep, WBValue))<{\v pfs -> (propOf (fst pfs) == BStep env e v) && (propOf (snd pfs) == WBValue v t)}> @-} main_lemma :: Expr -> Type -> Env -> Ctx -> HasType -> WBEnv -> (Value, (BStep, WBValue)) main_lemma e t env g (TNum g n) = lemmaTNum .... main_lemma e t env g (TVar _g x _t) p_env_g = lemmaTVar ... main_lemma e t env g (TAdd _g e1 p_e1_Int e2 p_e2_Int) p_env_g = lemmaTAdd ... main_lemma e t env g (TAbs _g x t1 e' t2 p_e2_t2) p_env_g = lemmaTAbs ... main_lemma e t env g (TApp _g e1 t2 _t p_e1_t2t e2 p_e2_t2) p_env_g = lemmaTApp ...

where you will define `lemmaT...` as top level functions. 
This will speed up checking. Makes sense? 

BTW, it is quite unclear to me why this function terminates, do you know?

[facundominguez]

The verification takes more than a minute to complete (didn't wait to see if it would finish) and GBs of memory in the latest LH. I had to disable the positivity check as otherwise LH complains of some data declarations. I didn't enable termination checking.