Stream: MetaCoq

Topic: Erasure evaluation relation is nondeterministic

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?

Matthieu Sozeau (Jun 30 2020 at 08:29):

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

Matthieu Sozeau (Jun 30 2020 at 08:30):

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

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.

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)

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?

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

Jakob Botsch Nielsen (Jun 30 2020 at 10:31):

Are there existing results about this in MetaCoq?

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...

Matthieu Sozeau (Jun 30 2020 at 10:44):

@Yannick Forster (Gitter import) ?

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.

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!

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.

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?

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.

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

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.

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)

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.

Jakob Botsch Nielsen (Jul 02 2020 at 11:01):

Ok, thanks!

Matthieu Sozeau (Jul 02 2020 at 11:36):

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

Jakob Botsch Nielsen (Jul 02 2020 at 11:52):

Awesome!

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

Danil Annenkov (Jul 02 2020 at 20:49):

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

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

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

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

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)

Jakob Botsch Nielsen (Jul 03 2020 at 08:48):

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

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.

Matthieu Sozeau (Jul 03 2020 at 08:49):

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

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?

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 :)

Matthieu Sozeau (Jul 03 2020 at 14:27):

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

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.

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.

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?

Jakob Botsch Nielsen (Jul 03 2020 at 14:45):

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

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.

Jakob Botsch Nielsen (Jul 20 2020 at 08:28):

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

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: Jun 01 2023 at 13:01 UTC