Stream: MetaCoq

Topic: Erasure evaluation relation is nondeterministic


view this post on Zulip Jakob Botsch Nielsen (Jun 29 2020 at 21:21):

The evaluation relation used in erasure is nondeterministic because eval_fix uses is_constructor_or_box while eval_fix_value uses just ~is_constructor:

Definition f := tFix [{| dname := nAnon; dbody := tLambda nAnon (tRel 0); rarg := 0 |}] 0.

Lemma eval1 Σ :
  Σ ⊢ tApp f tBox ▷ tApp f tBox.
Proof. change (tApp f tBox) with (mkApps f [tBox]). repeat constructor. Qed.

Lemma eval2 Σ :
  Σ ⊢ tApp f tBox ▷ tBox.
Proof.
  change (tApp f tBox) with (mkApps f [tBox]).
  eapply eval_fix; repeat constructor; try easy.
  eapply eval_beta; repeat constructor.
Qed.

I suppose eval_fix_value case should be using is_constructor_or_box like eval_fix, right?

view this post on Zulip Matthieu Sozeau (Jun 30 2020 at 08:29):

Hmm, I think you're right, can you please report an issue about this?

view this post on Zulip Matthieu Sozeau (Jun 30 2020 at 08:30):

We certainly should also uncomment the proof below that eval is deterministic :)

view this post on Zulip Jakob Botsch Nielsen (Jun 30 2020 at 08:31):

Sure. I can also see if I can fix it and submit a PR.
I don't think that proof is finished (PCUIC does not seem to have a proof of it either). I have a proof of it, but first using a slightly restated intermediate evaluation relation that I then show is equivalent (except for this particular part I was asking about), so it is a bit of code.

view this post on Zulip Matthieu Sozeau (Jun 30 2020 at 08:37):

It used to be proven until we changed something in fixpoint unfolding , maybe we were precisely hitting this problem (we would have anyway)

view this post on Zulip Jakob Botsch Nielsen (Jun 30 2020 at 09:42):

I changed the constructor of eval, but now the correctness proof of erasure broke because, in the case where a PCUIC fix is stuck with enough arguments, we only know that the structural argument is not a constructor, and we need to show that its erasure is not a constructor and not a box.
Ideally I guess we should show the case is impossible because the environment is axiom free, so the structural argument has to be a constructor (by canonicity). Is this true?

view this post on Zulip Matthieu Sozeau (Jun 30 2020 at 10:00):

If the PCUIC fix is stuck indeed we would have a closed value in an inductive type that is not a constructor and that is impossible.
Your reasoning is correct

view this post on Zulip Jakob Botsch Nielsen (Jun 30 2020 at 10:31):

Are there existing results about this in MetaCoq?

view this post on Zulip Matthieu Sozeau (Jun 30 2020 at 10:44):

There does not seem to be anything yet. It might be in one of Yannick Forster's branches. In principle it follows from SN, SR etc...

view this post on Zulip Matthieu Sozeau (Jun 30 2020 at 10:44):

@Yannick Forster (Gitter import) ?

view this post on Zulip Cyril Cohen (Jun 30 2020 at 14:23):

Matthieu Sozeau said:

Yannick Forster (Gitter import) ?

This account has not been claimed and was therefore archived.

view this post on Zulip Matthieu Sozeau (Jun 30 2020 at 14:27):

Cyril Cohen said:

Matthieu Sozeau said:

Yannick Forster (Gitter import) ?

This account has not been claimed and was therefore archived.

Ok, thanks!

view this post on Zulip Jakob Botsch Nielsen (Jun 30 2020 at 14:33):

I have another related issue which I think is also an issue in PCUIC big-step evaluation. As far as I can tell, there is no possible derivation for the execution of the following program:

Fixpoint f (a b : nat) {struct b} := b.
Definition prog := (fun x => f x) 0 0.

The problem is that the evaluation relations do not allow adding arguments to things that evaluate to stuck fixpoint, they only allow saying that the fully applied syntactic fixpoint will evaluate to something.

view this post on Zulip Matthieu Sozeau (Jun 30 2020 at 16:57):

Hmm, this looks like a completely legitimate program to me, you mean that the eval_fix rule is wrong then?

view this post on Zulip Jakob Botsch Nielsen (Jun 30 2020 at 17:31):

Indeed, it does not allow this program to compute to anything.
I think it would make sense to replace eval_fix and eval_fix_value by

| eval_fix_value f mfix idx args narg fn a av :
    Σ ⊢ f ▷ mkApps (tFix mfix idx) args ->
    Σ ⊢ a ▷ av ->
    cunfold_fix mfix idx = Some (narg, fn) ->
    (#|args| <> narg \/
     (#|args| = narg /\ ~is_ctor_or_box av)) ->
    Σ ⊢ tApp f a ▷ mkApps (tFix mfix idx) (args ++ [av])

| eval_fix f mfix idx args narg fn a av v :
    Σ ⊢ f ▷ mkApps (tFix mfix idx) args ->
    Σ ⊢ a ▷ av ->
    cunfold_fix mfix idx = Some (narg, fn) ->
    #|args| = narg ->
    is_ctor_or_box av ->
    Σ ⊢ mkApps fn (args ++ [av]) ▷ v ->
    Σ ⊢ tApp f a ▷ v

(And potentially make it #|args| < narg in eval_fix). As an added bonus, with this replacement it is _way_ easier to invert and proving it deterministic is easy.

view this post on Zulip Jakob Botsch Nielsen (Jun 30 2020 at 17:41):

Actually, scratch that part about #|args| < narg, I can see now that more arguments might be needed

view this post on Zulip Matthieu Sozeau (Jul 01 2020 at 12:55):

That looks right. I'm surprised we didn't see the problem before, but that might be explained because we only exercise the evaluation relations after erasure in CertiCoq, where we additionally assume there are no longer stuck fixpoints.

view this post on Zulip Jakob Botsch Nielsen (Jul 01 2020 at 18:22):

I'm working on doing this as we need it as well. I'm curious, is there a reason unfold_fix is used in some places in the evaluation relation? So far I have replaced all of them with cunfold_fix which seems more in line with how the other rules work (with csubst)

view this post on Zulip Matthieu Sozeau (Jul 02 2020 at 07:25):

Ok, cool. [unfold_fix] and [cunfold_fix] are interchangeable on closed terms, so yes that's more uniform this way.

view this post on Zulip Jakob Botsch Nielsen (Jul 02 2020 at 11:01):

Ok, thanks!

view this post on Zulip Matthieu Sozeau (Jul 02 2020 at 11:36):

I'll look into the lemma we need for erasure correctness.

view this post on Zulip Jakob Botsch Nielsen (Jul 02 2020 at 11:52):

Awesome!

view this post on Zulip Jakob Botsch Nielsen (Jul 02 2020 at 12:55):

I'm not totally sure what the new rules should look like for template Coq's relation due to the n-ary applications there. I guess it still needs to have mkApps at the conclusion there

view this post on Zulip Danil Annenkov (Jul 02 2020 at 20:49):

It seems like WcbvEval for template-coq (kernel) terms is gone now.

view this post on Zulip Jakob Botsch Nielsen (Jul 02 2020 at 20:50):

There is still this one: https://github.com/MetaCoq/metacoq/blob/coq-8.11/checker/theories/WcbvEval.v

view this post on Zulip Danil Annenkov (Jul 03 2020 at 08:10):

Yes, true. I've seen that one but wasn't sure if it uses the kernel AST, but it seems it does. BTW, mkApps there is a bit different, it flattens the application instead of building the nested applications: https://github.com/MetaCoq/metacoq/blob/6d1ab4c5ab77bed63259133e747be83a7e643d87/template-coq/theories/Ast.v#L57

view this post on Zulip Jakob Botsch Nielsen (Jul 03 2020 at 08:39):

Yeah, because of this I'm not totally sure what the rule needs to look like. Also I'm not sure if there should be a rule that allows non-canonical terms to compute to the same thing as their canonical counterparts

view this post on Zulip Matthieu Sozeau (Jul 03 2020 at 08:44):

Everything is proven assuming well-formed terms in checker/template-coq, so you can assume every tApp t u is well-formed (t cannot be an application)

view this post on Zulip Jakob Botsch Nielsen (Jul 03 2020 at 08:48):

Ok, that helps. Then it should have mkApps at the conclusion as well, I think.

view this post on Zulip Matthieu Sozeau (Jul 03 2020 at 08:49):

I guess it should ressemble the new relation, where you have eval_fix ... : eval f (mkApps (mkFix mfix idx) args') -> ... eval (mkApps f args) res.

view this post on Zulip Matthieu Sozeau (Jul 03 2020 at 08:49):

Yes, you're kind of forced to see the whole spine of arguments in this representation.

view this post on Zulip Jakob Botsch Nielsen (Jul 03 2020 at 11:09):

Hmm right, but the rules have to be generalized to n-ary args instead of just adding a single argument to the stuck fixpoint, right?

view this post on Zulip Jakob Botsch Nielsen (Jul 03 2020 at 11:17):

  | eval_fix f mfix idx fixargsv args argsv narg fn res :
      eval f (mkApps (tFix mfix idx) fixargsv) ->
      All2 eval args argsv ->
      unfold_fix mfix idx = Some (narg, fn) ->
      is_constructor narg (fixargsv ++ argsv) ->
      eval (mkApps fn (fixargsv ++ argsv)) res ->
      eval (mkApps f args) res

  | eval_fix_value f mfix idx fixargsv args argsv narg fn :
      eval f (mkApps (tFix mfix idx) fixargsv) ->
      All2 eval args argsv ->
      unfold_fix mfix idx = Some (narg, fn) ->
      ~~is_constructor narg (fixargsv ++ argsv) ->
      eval (mkApps f args) (mkApps (tFix mfix idx) (fixargsv ++ argsv))

Like this, I suppose. I think I will give up on proving this one deterministic :)

view this post on Zulip Matthieu Sozeau (Jul 03 2020 at 14:27):

I understand, dealing with mkApps is no fun ;) But yes this looks right.

view this post on Zulip Jakob Botsch Nielsen (Jul 03 2020 at 14:30):

I updated it and proved the old results about it in the PR. The only thing missing is the fix/fix_value cases for erases_correct. I looked at it for a bit but it didn't seem totally straightforward to adapt the old proof.

view this post on Zulip Matthieu Sozeau (Jul 03 2020 at 14:43):

Ok, I will look at those with Yannick Forster. It was on our agenda already to show that we can even weaken the requirement a bit more: no need to test if the recursive argument is a constructor or a box in erasure, as it should be statically known to be.

view this post on Zulip Matthieu Sozeau (Jul 03 2020 at 14:43):

I'll be on vacation next week though. Do you want this merged while incomplete or can it wait?

view this post on Zulip Jakob Botsch Nielsen (Jul 03 2020 at 14:45):

It can wait, we can use a fork, no problem.

view this post on Zulip Jakob Botsch Nielsen (Jul 07 2020 at 14:36):

I took another look and managed to prove the new cases, except for the impossible case where a fixpoint is stuck on a non-constructor.

view this post on Zulip Jakob Botsch Nielsen (Jul 20 2020 at 08:28):

@Matthieu Sozeau should I leave it as a draft until we have the remaining case?

view this post on Zulip Matthieu Sozeau (Jul 20 2020 at 09:30):

I think we can merge it with this left as a todo, so you can turn it into a PR. I’ll be doing POPL PC work for the coming weeks so I don’t know if I’ll get around to it soon, but Yannick might.


Last updated: Aug 11 2022 at 03:02 UTC