Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

This seems 'too easy' but to certify things I don't think it needs to be more complex? #6513

Open
wants to merge 2 commits into
base: master
Choose a base branch
from
+63 −0
Open

This seems 'too easy' but to certify things I don't think it needs to be more complex? #6513

Changes from 1 commit
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
43e2545
This seems 'too easy' but to certify things I don't think it needs to…
ramsay-t Sep 24, 2024
9ad6f51
Er, I think this was the wrong way round
ramsay-t Sep 25, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
63 changes: 63 additions & 0 deletions plutus-metatheory/src/VerifiedCompilation/UCSE.lagda.md
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,63 @@
---
title: VerifiedCompilation.UCSE
layout: page
---

# Common Subexpression Elimination Translation Phase
```
module VerifiedCompilation.UCSE where

```
## Imports

```
open import VerifiedCompilation.Equality using (DecEq; _≟_; decPointwise)
open import VerifiedCompilation.UntypedViews using (Pred; isCase?; isApp?; isLambda?; isForce?; isBuiltin?; isConstr?; isDelay?; isTerm?; allTerms?; iscase; isapp; islambda; isforce; isbuiltin; isconstr; isterm; allterms; isdelay)
open import VerifiedCompilation.UntypedTranslation using (Translation; translation?; Relation)
open import Relation.Nullary.Product using (_×-dec_)
open import Data.Product using (_,_)
import Relation.Binary as Binary using (Decidable)
open import Relation.Nullary using (Dec; yes; no; ¬_)
open import Untyped using (_⊢; case; builtin; _·_; force; `; ƛ; delay; con; constr; error)
import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl)
open import Data.Empty using (⊥)
open import Agda.Builtin.Maybe using (Maybe; just; nothing)
open import Untyped.RenamingSubstitution using (_[_])
```
## Translation Relation

This module is required to certify that an application of CSE doesn't break the
semantics; we are explicitly not evaluating whether the particular choice of
sub-expression was a "good" choice.

As such, this Translation Relation primarily checks that substituting the expression
back in would yield the original expression.

```
data UCSE : Relation where
cse : {X : Set} {x : Maybe X ⊢} {x' e : X ⊢}
→ Translation UCSE (x [ e ]) x'
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I'm perhaps nitpicking, but this isn't sufficient in the general case. CSE promises to pull some common subexpressions out, but it doesn't promise to pull all of them out. I.e. x' may still start with the same lambda and e may be substituted partially in x.

→ UCSE ((ƛ x) · e) x'
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Well just like with float-delay, you gotta make sure that e is pure. If the implementation pulls out an effectful e, then this may be a bug in the implementation.

... but unfortunately, it may not be a bug, sometimes it is fine to move impure things around for as long as that doesn't change the semantics of the program (and then there's an entirely separate discussion on whether effect ordering is important or not). For example if you have a bunch of applied lambda and all but one are pure, then it doesn't really matter in which order to execute them, since you're still going to get the single effect that you're ought to get.

So I suggest to reflect what I just said. Require e to be pure and say that this isn't the most general correct CSE, but is sufficient for now. Perhaps also add a link to this discussion.


UntypedCSE : {X : Set} {{_ : DecEq X}} → (ast : X ⊢) → (ast' : X ⊢) → Set₁
UntypedCSE = Translation UCSE

```

## Decision Procedure

```

isUntypedCSE? : {X : Set} {{_ : DecEq X}} → Binary.Decidable (Translation UCSE {X})

{-# TERMINATING #-}
isUCSE? : {X : Set} {{_ : DecEq X}} → Binary.Decidable (UCSE {X})
isUCSE? ast ast' with (isApp? (isLambda? isTerm?) isTerm?) ast
... | no ¬match = no λ { (cse x) → ¬match (isapp (islambda (isterm _)) (isterm _)) }
... | yes (isapp (islambda (isterm x)) (isterm e)) with isUntypedCSE? (x [ e ]) ast'
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think the whole approach to certification is very suboptimal. I.e. this pass and the others (not sure if all of them). So what you do here is you check that the LHS has the right shape and then you proceed with substitution and recurse. Potentially just to figure out that you didn't need to do all this work, because the terms match exactly and there was no point in all these substitutions and non-deterministic digressing into CSE, float-delay and everything else at every lambda application node.

I guess this is a fine start, but I wouldn't be surprised if it eventually turns out that all the passes need to be rewritten, because they can't handle real-world terms fast enough.

... | no ¬p = no λ { (cse x) → ¬p x }
... | yes p = yes (cse p)

isUntypedCSE? = translation? isUCSE?
```
Loading