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

[ana-pantilie]

I find this notation confusing. I'm used to seeing X as representing any type (of type Set usually). Whereas, X : ℕ here, so it's actually just a number! x is also just a number, but wrapped by Fin.

Would the following notation be better?

Suggested change

	∀ {X} (x : Fin X)
	∀ {n} (nᶠ : Fin n)

or

Suggested change

	∀ {X} (x : Fin X)
	∀ {n} (n↑ : Fin n)

or whatever you think is better.

[basetunnel]

Agreed that X is awkward. It is a left-over from when the metatheory used nested maybe's for representing scope size. Right now this is consistent with all other uses in the codebase like X ⊢. We should change this project-wide.

[basetunnel]

I actually don't mind x personally, since it represents an (arbitrary) variable name in the ast, it just happens to be represented by a natural. But perhaps v is also good?

[ana-pantilie]

Both x and v are ok, although tying it to the n in some way is more helpful to me since it indicates we're using Debruijn

[basetunnel]

I've opened https://github.com/IntersectMBO/plutus-private/issues/2182, it's probably better to do that in a separate PR.

[ana-pantilie]

Why is this decision procedure defined here instead of where the Pointwise type is defined?

Actually, why are the decision procedures for all of the relations defined in this module? Would it be better to have a Untyped.Relation.Decidable module?

[basetunnel]

I've moved pointwise? now to Untyped.Binary.Core. The decision procedures are here because they are tied to the Modular approach, I'd rather have them contained here. We could move them to Untyped.Relation.Binary.Modular.Decidable perhaps, but I don't think it's too bad to keep it all in a single module for 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?

[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]

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.