Certifier for case-reduce

[basetunnel]

This adds

• A translation relation and decision procedure for case-reduce pass, see CaseReduce.lagda.md for documentation on how it is structured.
• Reusable definitions/properties for translation relations in Untyped.Relation.Binary.{Core,Properties,Structures}. This mimics the module structure of agda-stdlib
• Modular rules for building translation relations (Untyped.Relation.Binary.Modular), used by the equivalence relation of case-reduce, see the end of the module for an example how to build decidable relations.

[ana-pantilie]

This is really cool! My comments only regard structure/formatting/notation, so I can approve this now

[zliu41]

If I understand correctly this is a quite complex way of saying: "If M reduces to M' via case-reduce, pass, else fail".

As we discussed, this has the disadvantage of tight coupling with the compiler: for example, if the compiler is changed such that it stops reducing case-constr in certain cases, then the certifier would break. I thought we've discussed an approach that doesn't have such tight coupling?

[zliu41]

What's the point of having this relation, and why does it need to be symmetric or reflexive?

[basetunnel]

For the same reason why the force-delay paper has an equivalence: it is (more) obviously semantics preserving, and since the case-reduce pas in Agda is a re-implementation of the Haskell implementation, a mistake there could carry over to Agda. It also becomes easier to count the optimization sites using a relation vs a function.

[zliu41]

I'd agree with the value of _~_ if its definition is much simpler and much more obviously correct than CaseReduce, but their complexities seem similar.

Also, since CaseReduce performs the actual reduction that the compiler does, doesn't it already include compatibility closure, making the CompatTerm redundant?

[basetunnel]

I'd agree with the value of ~ if its definition is much simpler and much more obviously correct than CaseReduce, but their complexities seem similar.

You're right that their complexity doesn't differ much. Still I think it's useful to have a more general and declarative relation like _~_, since case-reduce is just a re-implementation of the compiler logic (potentially having the same bugs etc.)

[basetunnel]

Also, since CaseReduce performs the actual reduction that the compiler does, doesn't it already include compatibility closure, making the CompatTerm redundant?

CompatTerm is part of _~_, not CaseReduce, so I don't understand exactly what you're asking.

CompatTerm is not redundant in _~_ because it relates the parts of terms that are not changed by the pass.

[zliu41]

I find it confusing that the definition of CaseReduce mentions _~_. I thought they are supposed to be two completely separate relations, one is more of an actual reduction algorithm, and the other is a specification that is more obviously correct.

[basetunnel]

Good point, that's not necessary here. R just needs to be instantiated to resolve ambiguity for the type checker, it's not actually used.

[basetunnel]

Good point, that's not necessary here. R just needs to be instantiated to resolve ambiguity for the type checker, it's not actually used.

I was wrong. It's needed because I defined reduce to be sound wrt ~ by construction, i.e. it computes a Maybe pair of the reduced term and a proof of its soundness. The reduced term is completely independent of the proof, so reduceM does not depend on ~, it just additionally shows it is sound.

To make the connection clearer, we could also set it up like this:

red-unit : X ⊢ → Maybe (X ⊢)

red-unit-sound : (M M' : X ⊢) → red-unit M ≡ just M' → CaseUnit R M M'

But this has to be done for each reduction rule and resulted in more boilerplate code which disappears if you combine them.

[basetunnel]

I've updated the comments in the code with this explanation

[basetunnel]

If I understand correctly this is a quite complex way of saying: "If M reduces to M' via case-reduce, pass, else fail".

It also guarantees by construction that it is sound with respect to the inductive reduction rules.

As we discussed, this has the disadvantage of tight coupling with the compiler: for example, if the compiler is changed such that it stops reducing case-constr in certain cases, then the certifier would break. I thought we've discussed an approach that doesn't have such tight coupling?

Yes, I looked at two ways of doing that:

1. reduce both pre- and post-term:

_≈_ : Relation
M ≈ M' = case-reduce M ≡ case-reduce M'

This is equally easy to decide, and less coupled because it allows case-reduction rules to be applied selectively: the compiler is allowed to not touch some case-constant/case-constructor. However, it also accepts the reverse application of reduction rules, which we deemed outside of the spec of the pass (this relation is sound/complete with the ~ equivalence).

2. a decision procedure for

Fix (Reduction + CompatTerm + Transitivity)

This would also allow selective application of the reduction rules, but the decision procedure needs to do some reducing itself. Initially that made it hard to construct the proof of the relation, but with the sound-by-construction rules it may now not be that difficult anymore.

Anyway, I'm happy to look into 2 more, but I wanted to get working certifiers for all passes first before generalizing more.

[zliu41]

This seems overcomplicated for a simple pass like CaseReduce. I feel like some small changes on top of the original approach would be fine.

This approach with two relations - one easier to decide and the other more obviously correct - would be more useful for the inliner, since its current relation is quite complex and not obviously correct.