Updated Pure definition in the metatheory

plutus-metatheory/plutus-metatheory.cabal

@@ -86,7 +86,7 @@ library
     Untyped
 
   -- WARNING: Order is important! MAlonzo modules must be listed last.
-  -- But cabal-fmt reorders modules alphabetically, so we use two 
+  -- But cabal-fmt reorders modules alphabetically, so we use two
   -- exposed-modules subsets to work around that. See Setup.hs
   exposed-modules:
     MAlonzo.Code.Agda.Builtin.Bool
@@ -188,6 +188,7 @@ library
     MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Properties
     MAlonzo.Code.Data.List.Relation.Unary.All
     MAlonzo.Code.Data.List.Relation.Unary.All.Properties
+    MAlonzo.Code.Data.List.Relation.Unary.All.Properties.Core
     MAlonzo.Code.Data.List.Relation.Unary.AllPairs.Core
     MAlonzo.Code.Data.List.Relation.Unary.Any
     MAlonzo.Code.Data.List.Relation.Unary.Any.Properties
@@ -346,14 +347,14 @@ library
     MAlonzo.Code.Untyped
     MAlonzo.Code.Untyped.CEK
     MAlonzo.Code.Untyped.CEKWithCost
+    MAlonzo.Code.Untyped.Purity
     MAlonzo.Code.Untyped.RenamingSubstitution
     MAlonzo.Code.Utils
     MAlonzo.Code.Utils.Decidable
     MAlonzo.Code.Utils.List
     MAlonzo.Code.Utils.Reflection
     MAlonzo.Code.VerifiedCompilation
     MAlonzo.Code.VerifiedCompilation.Equality
-    MAlonzo.Code.VerifiedCompilation.Purity
     MAlonzo.Code.VerifiedCompilation.UCaseOfCase
     MAlonzo.Code.VerifiedCompilation.UCaseReduce
     MAlonzo.Code.VerifiedCompilation.UCSE
@@ -451,6 +452,7 @@ library
     MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Properties
     MAlonzo.Code.Data.List.Relation.Unary.All
     MAlonzo.Code.Data.List.Relation.Unary.All.Properties
+    MAlonzo.Code.Data.List.Relation.Unary.All.Properties.Core
     MAlonzo.Code.Data.List.Relation.Unary.AllPairs.Core
     MAlonzo.Code.Data.List.Relation.Unary.Any
     MAlonzo.Code.Data.List.Relation.Unary.Any.Properties
@@ -638,7 +640,7 @@ library
     MAlonzo.Code.Utils.Reflection
     MAlonzo.RTE
     MAlonzo.RTE.Float
-    MAlonzo.Code.VerifiedCompilation.Purity
+    MAlonzo.Code.Untyped.Purity
     MAlonzo.Code.VerifiedCompilation.UCSE
     MAlonzo.Code.VerifiedCompilation.UFloatDelay
 

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

@@ -0,0 +1,146 @@
+---
+title: VerifiedCompilation.Purity
+layout: page
+---
+
+# Definitions of Purity for Terms
+```
+module Untyped.Purity where
+
+```
+## Imports
+
+```
+open import Untyped using (_⊢; case; builtin; _·_; force; `; ƛ; delay; con; constr; error)
+open import Relation.Nullary using (Dec; yes; no; ¬_; _×-dec_)
+open import Builtin using (Builtin; arity)
+open import Utils as U using (Maybe;nothing;just)
+open import RawU using (TmCon)
+open import Data.Product using (_,_; _×_)
+open import Data.Nat using (ℕ; zero; suc; _>_; _>?_)
+open import Data.List using (List; _∷_; [])
+open import Data.List.Relation.Unary.All using (All)
+open import Data.Maybe using (Maybe; just; nothing; from-just)
+open import Data.Maybe.Properties using (just-injective)
+open import Agda.Builtin.Equality using (_≡_; refl)
+open import Relation.Nullary.Negation using (contradiction)
+open import Relation.Binary.PropositionalEquality.Core using (trans; _≢_; subst; sym; cong)
+open import Data.Empty using (⊥)
+open import Function.Base using (case_of_)
+open import Untyped.CEK using (lookup?)
+open import VerifiedCompilation.UntypedViews using (isDelay?; isTerm?; isdelay; isterm)
+-- FIXME: This moves to Untyped.Reduction in a different PR...
+open import VerifiedCompilation.UCaseReduce using (iterApp)
+```
+## Untyped Purity
+
+The definition here is based on the (Haskell Implementation)[https://github.com/IntersectMBO/plutus/blob/master/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Purity.hs]. It is mostly uncontentious.
+```
+saturation : {X : Set} → X ⊢ → Maybe (ℕ × ℕ)
+saturation (builtin b) = just (((arity b), zero))
+saturation (t · _) with saturation t
+... | nothing = nothing
+... | just (arity , apps) = just (arity , suc apps)
+saturation (force t) with saturation t
+... | nothing = nothing
+... | just (arity , apps) = just (arity , suc apps)
+saturation _ = nothing
+
+sat-det : {X : Set} {arity args arity₁ args₁ : ℕ} {t t₁ : X ⊢}
+        → saturation t ≡ just (arity , args)
+        → saturation t₁ ≡ just (arity₁ , args₁)
+        → t ≡ t₁
+        → just (arity , args) ≡ just (arity₁ , args₁)
+sat-det sat-t sat-t₁ refl = trans (sym sat-t) sat-t₁
+
+data Pure {X : Set} : (X ⊢) → Set where
+    force : {t : X ⊢} → Pure t → Pure (force (delay t))
+
+    constr : {i : ℕ} {xs : List (X ⊢)} → All Pure xs → Pure (constr i xs)
+    -- case applied to constr would reduce, and possibly be pure.
+    case : {i : ℕ} {t : X ⊢}{vs ts : List (X ⊢)}
+           → lookup? i ts ≡ just t
+           → Pure (iterApp t vs)
+           → Pure (case (constr i vs) ts)
+    -- case applied to anything else is Unknown
+
+    builtin : {b : Builtin} → Pure (builtin b)
+
+    unsat-builtin : {t₁ t₂ : X ⊢} {arity args : ℕ}
+            → saturation t₁ ≡ just (arity , args)
+            → arity > (suc args)
+            → Pure t₂
+            → Pure (t₁ · t₂)
+
+    -- This is deliberately not able to cover all applications
+    -- ƛ (error) · t -- not pure
+    -- ƛ ƛ (error) · t · n -- not pure
+    -- ƛ ƛ ( (` nothing) · (` just nothing) ) · (ƛ error) · t -- not pure
+    -- Double application is considered impure (Unknown) by
+    -- the Haskell implementation at the moment.
+    app : {l : Maybe X ⊢} {r : X ⊢}
+            → Pure l
+            → Pure r
+            → Pure ((ƛ l) · r)
+
+    var : {v : X} → Pure (` v)
+    delay : {t : X ⊢} → Pure (delay t)
+    ƛ : {t : (Maybe X) ⊢} → Pure (ƛ t)
+    con : {c : TmCon} → Pure (con c)
+    -- errors are not pure ever.
+
+isPure? : {X : Set} → (t : X ⊢) → Dec (Pure t)
+
+allPure? : {X : Set} → (ts : List (X ⊢)) → Dec (All Pure ts)
+allPure? [] = yes All.[]
+allPure? (t ∷ ts) with (isPure? t) ×-dec (allPure? ts)
+... | yes (p , ps) = yes (p All.∷ ps)
+... | no ¬p = no λ { (px All.∷ x) → ¬p (px , x) }
+
+{-# TERMINATING #-}
+isPure? (` x) = yes var
+isPure? (ƛ t) = yes ƛ
+isPure? (l · r) with saturation l in sat-l
+isPure? (l · r) | just (arity , args) with arity >? (suc args)
+... | no ¬arity>args = no λ { (unsat-builtin sat-l₁ arity>args pr) → contradiction (subst (λ { (ar , ag) → ar > (suc ag) }) (just-injective (trans (sym sat-l₁) sat-l)) arity>args) ¬arity>args }
+... | yes arity<args with isPure? r
+...   | yes pr = yes (unsat-builtin sat-l arity<args pr)
+...   | no ¬pr = no λ { (unsat-builtin _ _ pr) → ¬pr pr ; (app _ pr) → ¬pr pr }
+isPure? (` x · r) | nothing = no λ { (unsat-builtin sat-l≡just _ _) → contradiction (trans (sym sat-l) sat-l≡just) (λ ()) }
+isPure? (ƛ l · r) | nothing with (isPure? l) ×-dec (isPure? r)
+... | yes (pl , pr) = yes (app pl pr)
+... | no ¬pl-pr = no λ { (app pl pr) → ¬pl-pr (pl , pr) }
+isPure? ((l · l₁) · r) | nothing = no λ { (unsat-builtin sat-l≡just _ _) → contradiction (trans (sym sat-l) sat-l≡just) (λ ()) }
+isPure? (force l · r) | nothing = no λ { (unsat-builtin sat-l≡just _ _) → contradiction (trans (sym sat-l) sat-l≡just) (λ ()) }
+isPure? (delay l · r) | nothing = no λ { (unsat-builtin sat-l≡just _ _) → contradiction (trans (sym sat-l) sat-l≡just) (λ ()) }
+isPure? (con x · r) | nothing = no λ { (unsat-builtin sat-l≡just _ _) → contradiction (trans (sym sat-l) sat-l≡just) (λ ()) }
+isPure? (constr i xs · r) | nothing = no λ { (unsat-builtin sat-l≡just _ _) → contradiction (trans (sym sat-l) sat-l≡just) (λ ()) }
+isPure? (case l ts · r) | nothing = no λ { (unsat-builtin sat-l≡just _ _) → contradiction (trans (sym sat-l) sat-l≡just) (λ ()) }
+isPure? (error · r) | nothing = no λ { (unsat-builtin sat-l≡just _ _) → contradiction (trans (sym sat-l) sat-l≡just) (λ ()) }
+isPure? (force t) with isDelay? (isTerm?) t
+... | no ¬delay = no λ { (force x) → ¬delay (isdelay (isterm _))}
+... | yes (isdelay (isterm tt)) with isPure? tt
+...    | yes p = yes (force p)
+...    | no ¬p = no λ { (force x) → ¬p x }
+isPure? (delay t) = yes delay
+isPure? (con x) = yes con
+isPure? (constr i xs) with allPure? xs
+... | yes pp = yes (constr pp)
+... | no ¬pp = no λ { (constr x) → ¬pp x }
+isPure? (case (` x) ts) = no (λ ())
+isPure? (case (ƛ t) ts) = no (λ ())
+isPure? (case (t · t₁) ts) = no (λ ())
+isPure? (case (force t) ts) = no (λ ())
+isPure? (case (delay t) ts) = no (λ ())
+isPure? (case (con x) ts) = no (λ ())
+isPure? (case (constr i vs) ts) with lookup? i ts in lookup-i
+... | nothing = no λ { (case lookup≡just pt·vs) → contradiction (trans (sym lookup-i) lookup≡just) λ () }
+... | just t with isPure? (iterApp t vs)
+...   | yes pt·vs = yes (case lookup-i pt·vs)
+...   | no ¬p = no λ { (case lookup≡just pt·vs) → contradiction (subst (λ x → Pure (iterApp x vs)) (just-injective (trans (sym lookup≡just) lookup-i)) pt·vs) ¬p }
+isPure? (case (case t ts₁) ts) = no (λ ())
+isPure? (case (builtin b) ts) = no (λ ())
+isPure? (case error ts) = no (λ ())
+isPure? (builtin b) = yes builtin
+isPure? error = no λ ()
+```

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

@@ -24,7 +24,7 @@ open Eq using (_≡_; refl)
 open import Data.Empty using (⊥)
 open import Agda.Builtin.Maybe using (Maybe; just; nothing)
 open import Untyped.RenamingSubstitution using (_[_])
-open import VerifiedCompilation.Purity using (UPure; isUPure?)
+open import Untyped.Purity using (Pure; isPure?)
 ```
 ## Translation Relation
 
@@ -38,7 +38,7 @@ back in would yield the original expression.
 ```
 data UCSE : Relation where
   cse : {X : Set} {{ _ : DecEq X}} {x' : Maybe X ⊢} {x e : X ⊢}
-    → UPure X e
+    → Pure e
     → Translation UCSE x (x' [ e ])
     → UCSE x ((ƛ x') · e)
 
@@ -57,7 +57,7 @@ isUntypedCSE? : {X : Set} {{_ : DecEq X}} → Binary.Decidable (Translation UCSE
 isUCSE? : {X : Set} {{_ : DecEq X}} → Binary.Decidable (UCSE {X})
 isUCSE? ast ast' with (isApp? (isLambda? isTerm?) isTerm?) ast'
 ... | no ¬match = no λ { (cse up x) → ¬match (isapp (islambda (isterm _)) (isterm _)) }
-... | yes (isapp (islambda (isterm x')) (isterm e)) with (isUntypedCSE? ast (x' [ e ])) ×-dec (isUPure? e)
+... | yes (isapp (islambda (isterm x')) (isterm e)) with (isUntypedCSE? ast (x' [ e ])) ×-dec (isPure? e)
 ... | no ¬p = no λ { (cse up x) → ¬p (x , up) }
 ... | yes (p , upure) = yes (cse upure p)
 

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

@@ -29,7 +29,7 @@ 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 Untyped.Purity using (Pure; isPure?)
 open import Data.List.Relation.Unary.All using (All; all?)
 
 variable
@@ -131,7 +131,7 @@ 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'
+          → Pure y'
           → FlD (ƛ x · (delay y)) (ƛ x' · y')
 
 FloatDelay : {X : Set} {{_ : DecEq X}} → (ast : X ⊢) → (ast' : X ⊢) → Set₁
@@ -149,7 +149,7 @@ 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₂')
+... | yes (isapp (islambda (isterm t₁')) (isterm t₂')) with (isFloatDelay? (subs-delay nothing t₁) t₁') ×-dec (isFloatDelay? t₂ t₂') ×-dec (isPure? t₂')
 ... | no ¬p = no λ { (floatdelay x₁ x₂ x₃) → ¬p ((x₁ , x₂ , x₃))}
 ... | yes (p₁ , p₂ , pure) = yes (floatdelay p₁ p₂ pure)
 isFloatDelay? = translation? isFlD?

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

@@ -41,10 +41,10 @@ data pureInline : Relation where
 
 _ : pureInline {⊥} (ƛ (` nothing) · error) error
 _ = inline (tr reflexive)
-
+{-
 _ : {X : Set} {a b : X} {{_ : DecEq X}} → pureInline (((ƛ (ƛ ((` (just nothing)) · (` nothing)))) · (` a)) · (` b)) ((` a) · (` b))
-_ = tr (Translation.match (TransMatch.app (Translation.istranslation (inline (tr reflexive))) reflexive)) ⨾ inline (tr reflexive)
-
+_ = tr (Translation.app (Translation.istranslation (inline (tr reflexive))) reflexive) ⨾ inline (tr reflexive)
+-}
 ```
 However, this has several intermediate values that are very hard to determine for a decision procedure.
 
@@ -74,9 +74,10 @@ data Inline {X : Set} {{ _ : DecEq X}} : Env {X} → (X ⊢) → (X ⊢) → Set
 _ : {X : Set} {a b : X} {{_ : DecEq X}} → Inline □ (((ƛ (ƛ ((` (just nothing)) · (` nothing)))) · (` a)) · (` b)) ((` a) · (` b))
 _ = var (var (sub (last-sub reflexive)))
 
+{-
 _ : {X : Set} {a b : X} {{_ : DecEq X}} → Translation (Inline □) (((ƛ (ƛ ((` (just nothing)) · (` nothing)))) · (` a)) · (` b)) ((ƛ ((` (just a)) · (` nothing))) · (` b))
-
-_ = Translation.match (TransMatch.app (Translation.istranslation (var (last-sub reflexive))) reflexive)
+_ = Translation.app (Translation.istranslation (var (last-sub reflexive))) reflexive
+-}
 ```
 # Inline implies pureInline
 ```