Translation relation and decision procedure for the Float-Delay (#6482)

* WIP

* WIP

* WIP

* WIP

* WIP

* WIP - Most of the nFD->FD proof is done but I am now wondering if the application rules need the force in them...

* Some progress on the FD->pureFD proof... Not completely sure it is going in a good direction...

* Made the parameters to istranslation implicit, since they are encoded in the relation anyway

* WIP

* WIP

* WIP - with crazy variable binding issues

* Add 'forall DecEq' to 'Relation'

* Roman's additions.

* Workign Float-Delay translation relation and decision procedure.

* Missed a definition

* Now uses Purity, althought that is 'stub code' at the moment.

* Now with added Purity...

* Remove 'Terminating' from 'translation?'

---------

Co-authored-by: effectfully <[email protected]>

plutus-metatheory/src/VerifiedCompilation/Purity.lagda.md

@@ -0,0 +1,25 @@
+---
+title: VerifiedCompilation.Purity
+layout: page
+---
+
+# Definitions of Purity for Terms
+```
+module VerifiedCompilation.Purity where
+
+```
+## Imports
+
+```
+open import Untyped using (_⊢; case; builtin; _·_; force; `; ƛ; delay; con; constr; error)
+open import Relation.Nullary using (Dec; yes; no; ¬_)
+
+```
+## Untyped Purity
+```
+data UPure (X : Set) : (X ⊢) → Set where
+  FIXME : (t : X ⊢) → UPure X t
+
+isUPure? : {X : Set} → (t : X ⊢) → Dec (UPure X t)
+isUPure? t = yes (FIXME t)
+```

plutus-metatheory/src/VerifiedCompilation/UCaseOfCase.lagda.md

@@ -34,13 +34,13 @@ open import Data.List using (List; _∷_; [])
 ## Translation Relation
 
 This compiler stage only applies to the very specific case where an `IfThenElse` builtin exists in a `case` expression.
-It moves the `IfThenElse` outside and creates two `case` expressions with each of the possible lists of cases. 
+It moves the `IfThenElse` outside and creates two `case` expressions with each of the possible lists of cases.
 
 This will just be an instance of the `Translation` relation once we define the "before" and "after" patterns.
 
 ```
 data CoC : Relation where
-  isCoC : {X : Set} → (b : X ⊢) (tn fn : ℕ)  (tt tt' ft ft' alts alts' : List (X ⊢)) →
+  isCoC : {X : Set} {{_ : DecEq X}} → (b : X ⊢) (tn fn : ℕ)  (tt tt' ft ft' alts alts' : List (X ⊢)) →
              Pointwise (Translation CoC) alts alts' →
              Pointwise (Translation CoC) tt tt' →
              Pointwise (Translation CoC) ft ft' →
@@ -76,7 +76,7 @@ isCoCCase? t  | no ¬CoCCase = no λ { (isCoCCase b tn fn alts tt ft) → ¬CoCC
                                                                                    (isconstr tn (allterms alts)))
                                                                                   (isconstr fn (allterms tt)))
                                                                                  (allterms ft)) }
-                                                                                 
+
 data CoCForce {X : Set} :  (X ⊢) → Set where
   isCoCForce : (b : (X ⊢)) (tn fn : ℕ) (tt' ft' alts' : List (X ⊢)) → CoCForce (force ((((force (builtin ifThenElse)) · b) · (delay (case (constr tn tt') alts'))) · (delay (case (constr fn ft') alts'))))
 isCoCForce? : {X : Set} {{ _ : DecEq X }} → Unary.Decidable (CoCForce {X})
@@ -103,12 +103,12 @@ isUntypedCaseOfCase? : {X : Set} {{_ : DecEq X}} → Binary.Decidable (Translati
 isCoC? : {X : Set} {{_ : DecEq X}} → Binary.Decidable (CoC {X})
 isCoC? ast ast' with (isCoCCase? ast) ×-dec (isCoCForce? ast')
 ... | no ¬cf = no λ { (isCoC b tn fn tt tt' ft ft' alts alts' x x₁ x₂) → ¬cf
-                                                                          (isCoCCase b tn fn tt ft alts , isCoCForce b tn fn tt' ft' alts') }
+      (isCoCCase b tn fn tt ft alts , isCoCForce b tn fn tt' ft' alts') }
 ... | yes (isCoCCase b tn fn tt ft alts , isCoCForce b₁ tn₁ fn₁ tt' ft' alts') with (b ≟ b₁) ×-dec (tn ≟ tn₁) ×-dec (fn ≟ fn₁) ×-dec (decPointwise isUntypedCaseOfCase? tt tt') ×-dec (decPointwise isUntypedCaseOfCase? ft ft') ×-dec (decPointwise isUntypedCaseOfCase? alts alts')
 ... | yes (refl , refl , refl , ttpw , ftpw , altpw) = yes (isCoC b tn fn tt tt' ft ft' alts alts' altpw ttpw ftpw)
 ... | no ¬p = no λ { (isCoC .b .tn .fn .tt .tt' .ft .ft' .alts .alts' x x₁ x₂) → ¬p (refl , refl , refl , x₁ , x₂ , x) }
 
-isUntypedCaseOfCase? {X} = translation? {X} isCoC? 
+isUntypedCaseOfCase? {X} = translation? {X} isCoC?
 ```
 
 ## Semantic Equivalence
@@ -125,11 +125,11 @@ The `stepper` function uses the CEK machine to evaluate a term. Here we call it
 large gas budget and begin in an empty context (which assumes the term is closed).
 
 ```
--- TODO: Several approaches are possible. 
+-- TODO: Several approaches are possible.
 --semantic_equivalence : ∀ {X set} {ast ast' : ⊥ ⊢}
  --                    → ⊥ ⊢̂ ast ⊳̂ ast'
- -- <Some stuff about whether one runs out of gas -- as long as neither runs out of gas, _then_ they are equivilent> 
+ -- <Some stuff about whether one runs out of gas -- as long as neither runs out of gas, _then_ they are equivilent>
  --                    → (stepper maxsteps  (Stack.ϵ ; [] ▻ ast)) ≡ (stepper maxsteps (Stack.ε ; [] ▻ ast'))
 
--- ∀ {s : ℕ} → stepper s ast ≡ <valid terminate state> ⇔ ∃ { s' : ℕ } [ stepper s' ast' ≡ <same valid terminate state> ] 
+-- ∀ {s : ℕ} → stepper s ast ≡ <valid terminate state> ⇔ ∃ { s' : ℕ } [ stepper s' ast' ≡ <same valid terminate state> ]
 ```

plutus-metatheory/src/VerifiedCompilation/UFloatDelay.lagda.md

@@ -0,0 +1,157 @@
+---
+title: VerifiedCompilation.UFloatDelay
+layout: page
+---
+
+# Float-Delay Translation Phase
+```
+module VerifiedCompilation.UFloatDelay where
+
+```
+## Imports
+
+```
+open import VerifiedCompilation.Equality using (DecEq; _≟_;decPointwise)
+open import VerifiedCompilation.UntypedViews using (Pred; isCase?; isApp?; isLambda?; isForce?; isBuiltin?; isConstr?; isDelay?; isTerm?; isVar?; allTerms?; iscase; isapp; islambda; isforce; isbuiltin; isconstr; isterm; allterms; isdelay; isvar)
+open import VerifiedCompilation.UntypedTranslation using (Translation; translation?; Relation; convert; reflexive)
+open import Relation.Nullary.Product using (_×-dec_)
+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 Function using (case_of_)
+open import Agda.Builtin.Maybe using (Maybe; just; nothing)
+open import Data.List using (map; all)
+open import Relation.Nullary using (Dec; yes; no; ¬_)
+import Relation.Binary as Binary using (Decidable)
+open import Data.Product using (_,_)
+open import Data.Nat using (ℕ)
+open import Data.List using (List)
+open import Builtin using (Builtin)
+open import RawU using (TmCon)
+open import VerifiedCompilation.Purity using (UPure; isUPure?)
+open import Data.List.Relation.Unary.All using (All; all?)
+
+variable
+  X : Set
+  x x' y y' : X ⊢
+```
+## Translation Relation
+
+This translation "floats" delays in applied terms into the abstraction, without inlining the whole term.
+This is separate from inlining because the added `delay` may make it seem like a substantial increase in code
+size, and so dissuade the inliner from executing. However, it may be that the laziness inside the resulting term
+is more computationally efficient.
+
+This translation will only preserve semantics if the instances of the bound variable are under a `force` and if the applied term is "Pure".
+
+This requires a function to check all the bound variables are under `force`. The `AllForced` type
+is defined in terms of the de Brujin index of the bound variable, since this will be incremented under
+further lambdas.
+```
+
+data AllForced (X : Set){{ _ : DecEq X}} : X → (X ⊢) → Set where
+  var : (v : X) → {v' : X} → v' ≢ v → AllForced X v (` v')
+  forced : (v : X) → AllForced X v (force (` v))
+  force : (v : X) → AllForced X v x' → AllForced X v (force x')
+  delay : (v : X) → AllForced X v x' → AllForced X v (delay x')
+  ƛ : (v : X) → {t : (Maybe X) ⊢}
+      → AllForced (Maybe X) (just v) t
+      → AllForced X v (ƛ t)
+  app : (v : X)
+      → AllForced X v x
+      → AllForced X v y
+      → AllForced X v (x · y)
+  error : {v : X} → AllForced X v error
+  builtin : {v : X} → {b : Builtin} → AllForced X v (builtin b)
+  con : {v : X} → {c : TmCon} → AllForced X v (con c)
+  case : (v : X) → {t : X ⊢} {ts : List (X ⊢)}
+      → AllForced X v t
+      → All (AllForced X v) ts
+      → AllForced X v (case t ts)
+  constr : (v : X) → {i : ℕ} {xs : List (X ⊢)}
+      → All (AllForced X v) xs
+      → AllForced X v (constr i xs)
+
+{-# TERMINATING #-}
+isAllForced? : {{ _ : DecEq X}} → (v : X) → (t : X ⊢) → Dec (AllForced X v t)
+isAllForced? v t with isForce? isTerm? t
+... | yes (isforce (isterm t)) with isVar? t
+...           | no ¬var with isAllForced? v t
+...                       | yes allForced = yes (force v allForced)
+...                       | no ¬allForced = no λ { (forced .v) → ¬var (isvar v) ; (force .v p) → ¬allForced p }
+isAllForced? v t | yes (isforce (isterm _)) | yes (isvar v₁) with v₁ ≟ v
+...                       | yes refl = yes (forced v)
+...                       | no v₁≢v = yes (force v (var v v₁≢v))
+isAllForced? v (` x) | no ¬force with x ≟ v
+... | yes refl = no λ { (var .v x≢v) → x≢v refl}
+... | no x≢v = yes (var v x≢v)
+isAllForced? {X} v (ƛ t) | no ¬force with isAllForced? {Maybe X} (just v) t
+... | yes p = yes (ƛ v p)
+... | no ¬p = no λ { (ƛ .v p) → ¬p p}
+isAllForced? v (t₁ · t₂) | no ¬force with (isAllForced? v t₁) ×-dec (isAllForced? v t₂)
+... | yes (pt₁ , pt₂) = yes (app v pt₁ pt₂)
+... | no ¬p = no λ { (app .v x₁ x₂) → ¬p (x₁ , x₂)}
+isAllForced? v (force t) | no ¬force = no λ { (forced .v) → ¬force (isforce (isterm t)) ; (force .v x) → ¬force (isforce (isterm t)) }
+isAllForced? v (delay t) | no ¬force with isAllForced? v t
+... | yes p = yes (delay v p)
+... | no ¬p = no λ { (delay .v pp) → ¬p pp}
+isAllForced? v (con x) | no ¬force = yes con
+isAllForced? v (constr i xs) | no ¬force with all? (isAllForced? v) xs
+... | yes p = yes (constr v p)
+... | no ¬p = no λ { (constr .v p) → ¬p p }
+isAllForced? v (case t ts) | no ¬force with (isAllForced? v t) ×-dec (all? (isAllForced? v) ts)
+... | yes (p₁ , p₂) = yes (case v p₁ p₂)
+... | no ¬p = no λ { (case .v p₁ p₂) → ¬p ((p₁ , p₂)) }
+isAllForced? v (builtin b) | no ¬force = yes builtin
+isAllForced? v error | no ¬force = yes error
+```
+The `delay` needs to be added to all bound variables.
+```
+{-# TERMINATING #-}
+subs-delay : {X : Set}{{de : DecEq X}} → (v : Maybe X) → (Maybe X ⊢) → (Maybe X ⊢)
+subs-delay v (` x) with v ≟ x
+... | yes refl = (delay (` x))
+... | no _ = (` x)
+subs-delay v (ƛ t) = ƛ (subs-delay (just v) t) -- The de Brujin index has to be incremented
+subs-delay v (t · t₁) = (subs-delay v t) · (subs-delay v t₁)
+subs-delay v (force t) = force (subs-delay v t) -- This doesn't immediately apply Force-Delay
+subs-delay v (delay t) = delay (subs-delay v t)
+subs-delay v (con x) = con x
+subs-delay v (constr i xs) = constr i (map (subs-delay v) xs)
+subs-delay v (case t ts) = case (subs-delay v t) (map (subs-delay v) ts)
+subs-delay v (builtin b) = builtin b
+subs-delay v error = error
+
+```
+The translation relation is then fairly striaghtforward.
+
+```
+data FlD {X : Set} {{de : DecEq X}} : (X ⊢) → (X ⊢) → Set₁ where
+  floatdelay : {y y' : X ⊢} {x x' : (Maybe X) ⊢}
+          → Translation FlD (subs-delay nothing x) x'
+          → Translation FlD y y'
+          → UPure X y'
+          → FlD (ƛ x · (delay y)) (ƛ x' · y')
+
+FloatDelay : {X : Set} {{_ : DecEq X}} → (ast : X ⊢) → (ast' : X ⊢) → Set₁
+FloatDelay = Translation FlD
+
+```
+## Decision Procedure
+```
+
+isFloatDelay? : {X : Set} {{de : DecEq X}} → Binary.Decidable (FloatDelay {X})
+
+{-# TERMINATING #-}
+isFlD? : {X : Set} {{de : DecEq X}} → Binary.Decidable (FlD {X})
+isFlD? ast ast' with (isApp? (isLambda? isTerm?) (isDelay? isTerm?)) ast
+... | no ¬match = no λ { (floatdelay x x₁ x₂) → ¬match ((isapp (islambda (isterm _)) (isdelay (isterm _)))) }
+... | yes (isapp (islambda (isterm t₁)) (isdelay (isterm t₂))) with (isApp? (isLambda? isTerm?) isTerm?) ast'
+... | no ¬match = no λ { (floatdelay x x₁ x₂) → ¬match ((isapp (islambda (isterm _)) (isterm _))) }
+... | yes (isapp (islambda (isterm t₁')) (isterm t₂')) with (isFloatDelay? (subs-delay nothing t₁) t₁') ×-dec (isFloatDelay? t₂ t₂') ×-dec (isUPure? t₂')
+... | no ¬p = no λ { (floatdelay x₁ x₂ x₃) → ¬p ((x₁ , x₂ , x₃))}
+... | yes (p₁ , p₂ , pure) = yes (floatdelay p₁ p₂ pure)
+isFloatDelay? = translation? isFlD?
+
+```