diff --git a/plutus-metatheory/changelog.d/20240502_122129_ramsay.taylor_verified_compilation.rst b/plutus-metatheory/changelog.d/20240502_122129_ramsay.taylor_verified_compilation.rst new file mode 100644 index 00000000000..68b4e0b4981 --- /dev/null +++ b/plutus-metatheory/changelog.d/20240502_122129_ramsay.taylor_verified_compilation.rst @@ -0,0 +1,3 @@ +# Added + +Initial Translation Relation for the Untyped Case of Case simplification phase diff --git a/plutus-metatheory/src/Untyped.lagda.md b/plutus-metatheory/src/Untyped.lagda.md index da55cc9094b..53a5dc2d037 100644 --- a/plutus-metatheory/src/Untyped.lagda.md +++ b/plutus-metatheory/src/Untyped.lagda.md @@ -40,6 +40,12 @@ open Untyped ## Well-scoped Syntax +This defines the syntax for UPLC and requires that it be "well scoped", which +is that only variables in the context are used. The context uses de Bruijn naming, +so the variables are numbered. This numbering is provided by an inductively defined +natural number, which uses the Maybe type (so: `Nothing` = zero, `Just Just Nothing` = 2) +to allow direct translation to Haskell. + ``` data _⊢ (X : Set) : Set where ` : X → X ⊢ diff --git a/plutus-metatheory/src/Utils.lagda.md b/plutus-metatheory/src/Utils.lagda.md index 94216fbff09..7571f4ff958 100644 --- a/plutus-metatheory/src/Utils.lagda.md +++ b/plutus-metatheory/src/Utils.lagda.md @@ -175,6 +175,10 @@ postulate ByteString : Set {-# FOREIGN GHC import qualified Data.ByteString as BS #-} {-# COMPILE GHC ByteString = type BS.ByteString #-} +postulate + eqByteString : ByteString → ByteString → Bool +{-# COMPILE GHC eqByteString = (==) #-} + ``` ## Record Types ``` @@ -246,13 +250,25 @@ postulate Bls12-381-G1-Element : Set {-# FOREIGN GHC import qualified PlutusCore.Crypto.BLS12_381.G1 as G1 #-} {-# COMPILE GHC Bls12-381-G1-Element = type G1.Element #-} +postulate + eqBls12-381-G1-Element : Bls12-381-G1-Element → Bls12-381-G1-Element → Bool +{-# COMPILE GHC eqBls12-381-G1-Element = (==) #-} + postulate Bls12-381-G2-Element : Set {-# FOREIGN GHC import qualified PlutusCore.Crypto.BLS12_381.G2 as G2 #-} {-# COMPILE GHC Bls12-381-G2-Element = type G2.Element #-} +postulate + eqBls12-381-G2-Element : Bls12-381-G2-Element → Bls12-381-G2-Element → Bool +{-# COMPILE GHC eqBls12-381-G2-Element = (==) #-} + postulate Bls12-381-MlResult : Set {-# FOREIGN GHC import qualified PlutusCore.Crypto.BLS12_381.Pairing as Pairing #-} {-# COMPILE GHC Bls12-381-MlResult = type Pairing.MlResult #-} + +postulate + eqBls12-381-MlResult : Bls12-381-MlResult → Bls12-381-MlResult → Bool +{-# COMPILE GHC eqBls12-381-MlResult = (==) #-} ``` ## Kinds diff --git a/plutus-metatheory/src/VerifiedCompilation/Equality.lagda.md b/plutus-metatheory/src/VerifiedCompilation/Equality.lagda.md new file mode 100644 index 00000000000..5f10dde4afb --- /dev/null +++ b/plutus-metatheory/src/VerifiedCompilation/Equality.lagda.md @@ -0,0 +1,334 @@ +--- +title: VerifiedCompilation.Equality +layout: page +--- +# Verified Compilation Equality +``` +module VerifiedCompilation.Equality where +``` + +## Decidable Equivalence + +There are various points in the Translation definitions where we need to compare terms +for equality. It is almost always the case that an unchanged term is a valid translation; in +many of the translations there are parts that must remain untouched. + +``` +import Relation.Binary.PropositionalEquality as Eq +open Eq using (_≡_; refl; isEquivalence; cong) +open import Data.Nat using (ℕ) +open import Data.Empty using (⊥) +open import RawU using (TmCon; tmCon; decTag; TyTag; ⟦_⟧tag; decTagCon; tmCon2TagCon) +open import Relation.Binary.Definitions using (DecidableEquality) +open import Builtin.Constant.AtomicType using (AtomicTyCon; decAtomicTyCon; ⟦_⟧at) +open import Agda.Builtin.Bool using (true; false) +open import Data.List using (List; []; _∷_) +open import Data.List.Relation.Binary.Pointwise.Base using (Pointwise) +open import Data.List.Relation.Binary.Pointwise using (Pointwise-≡⇒≡; ≡⇒Pointwise-≡) +open import Data.List.Properties using (≡-dec) +open import Relation.Binary.Core using (REL) +open import Level using (Level) +open import Builtin using (Builtin; decBuiltin) +open import Builtin.Signature using (_⊢♯) +import Data.Nat.Properties using (_≟_) +open import Data.Integer using (ℤ) +import Data.Integer.Properties using (_≟_) +import Data.String.Properties using (_≟_) +import Data.Bool.Properties using (_≟_) +import Data.Unit.Properties using (_≟_) +open import Untyped using (_⊢; `; ƛ; case; constr; _·_; force; delay; con; builtin; error) +import Relation.Unary as Unary using (Decidable) +import Relation.Binary.Definitions as Binary using (Decidable) +open import Relation.Nullary using (Dec; yes; no; ¬_) +open import Data.Product using (_,_) +open import Relation.Nullary.Product using (_×-dec_) +open import Utils as U using (Maybe; nothing; just; Either) +import Data.List.Properties as LP using (≡-dec) +open import Builtin.Constant.AtomicType using (decAtomicTyCon) +open import Agda.Builtin.TrustMe using (primTrustMe) +open import Agda.Builtin.String using (String; primStringEquality) +``` +Instances of `DecEq` will provide a Decidable Equality procedure for their type. + +``` +record DecEq (A : Set) : Set where + field _≟_ : DecidableEquality A +open DecEq {{...}} public +``` +Several of the decision procedures depend on other `DecEq` instances, so it is useful +to give them types and bind them to instance declarations first and then use them in the +implementations further down. + +``` +decEq-TmCon : DecidableEquality TmCon + +decEq-TyTag : DecidableEquality TyTag + +decEq-⟦_⟧tag : ( t : TyTag ) → DecidableEquality ⟦ t ⟧tag +``` +# Pointwise Decisions + +We often need to show that one list of AST elements is a valid translation +of another list of AST elements by showing the `n`th element of one is a translation of the +`n`th element of the other, pointwise. + +``` +decPointwise : {l₁ l₂ : Level} { A B : Set l₁ } { _~_ : A → B → Set l₂} → Binary.Decidable _~_ → Binary.Decidable (Pointwise _~_) +decPointwise dec [] [] = yes Pointwise.[] +decPointwise dec [] (x ∷ ys) = no (λ ()) +decPointwise dec (x ∷ xs) [] = no (λ ()) +decPointwise dec (x ∷ xs) (y ∷ ys) with dec x y | decPointwise dec xs ys +... | yes p | yes q = yes (p Pointwise.∷ q) +... | yes _ | no ¬q = no λ where (_ Pointwise.∷ xs~ys) → ¬q xs~ys +... | no ¬p | _ = no λ where (x∼y Pointwise.∷ _) → ¬p x∼y +``` + +## Decidable Equality Instances + +Creating Instance declarations for various Decidable Equality functions to be used +when creating translation decision procedures. + +``` +decEq-⊢ : ∀{X} {{_ : DecEq X}} → DecidableEquality (X ⊢) + +instance + DecEq-Maybe : ∀{A} {{_ : DecEq A}} → DecEq (Maybe A) + DecEq-Maybe ._≟_ = M.≡-dec _≟_ + where import Data.Maybe.Properties as M + + EmptyEq : DecEq ⊥ + EmptyEq = record { _≟_ = λ () } + + DecAtomicTyCon : DecEq AtomicTyCon + DecAtomicTyCon ._≟_ = decAtomicTyCon + + DecEq-TmCon : DecEq TmCon + DecEq-TmCon ._≟_ = decEq-TmCon + + DecEq-⊢ : ∀{X} {{_ : DecEq X}} → DecEq (X ⊢) + DecEq-⊢ ._≟_ = decEq-⊢ + + DecEq-List-⊢ : ∀{X} {{_ : DecEq X}} → DecEq (List (X ⊢)) + DecEq-List-⊢ ._≟_ = LP.≡-dec decEq-⊢ + + DecEq-Builtin : DecEq Builtin + DecEq-Builtin ._≟_ = decBuiltin + + DecEq-ℕ : DecEq ℕ + DecEq-ℕ ._≟_ = Data.Nat.Properties._≟_ + + DecEq-ℤ : DecEq ℤ + DecEq-ℤ ._≟_ = Data.Integer.Properties._≟_ + + DecEq-TyTag : DecEq TyTag + DecEq-TyTag ._≟_ = decEq-TyTag + +``` +The `TmCon` type inserts constants into Terms, so it is built from the +type tag and semantics equality decision procedures. + +Type Tags (`TyTag`) are just a list of constructors to represent each +of the builtin types, or they are a structure built on top of those using +`list` or `pair`. +``` +decEq-TyTag (_⊢♯.atomic x) (_⊢♯.atomic x₁) with (decAtomicTyCon x x₁) +... | yes refl = yes refl +... | no ¬x=x₁ = no λ { refl → ¬x=x₁ refl } +decEq-TyTag (_⊢♯.atomic x) (_⊢♯.list t') = no (λ ()) +decEq-TyTag (_⊢♯.atomic x) (_⊢♯.pair t' t'') = no (λ ()) +decEq-TyTag (_⊢♯.list t) (_⊢♯.atomic x) = no (λ ()) +decEq-TyTag (_⊢♯.list t) (_⊢♯.list t') with t ≟ t' +... | yes refl = yes refl +... | no ¬p = no λ { refl → ¬p refl } +decEq-TyTag (_⊢♯.list t) (_⊢♯.pair t' t'') = no (λ ()) +decEq-TyTag (_⊢♯.pair t t₁) (_⊢♯.atomic x) = no (λ ()) +decEq-TyTag (_⊢♯.pair t t₁) (_⊢♯.list t') = no (λ ()) +decEq-TyTag (_⊢♯.pair t t₁) (_⊢♯.pair t' t'') with (t ≟ t') ×-dec (t₁ ≟ t'') +... | yes (refl , refl) = yes refl +... | no ¬pq = no λ { refl → ¬pq (refl , refl) } + +``` +The equality of the semantics of constants will depend on the equality of +the underlying types, so this can leverage the standard library decision +procedures. + +``` +record HsEq (A : Set) : Set where + field + hsEq : A → A → Agda.Builtin.Bool.Bool + +open HsEq {{...}} public + +postulate + magicNeg : ∀ {A : Set} {a b : A} → ¬ a ≡ b + +magicBoolDec : {A : Set} → {a b : A} → Agda.Builtin.Bool.Bool → Dec (a ≡ b) +magicBoolDec true = yes primTrustMe +magicBoolDec false = no magicNeg + +builtinEq : {A : Set} {{_ : HsEq A}} → Binary.Decidable {A = A} _≡_ +builtinEq x y = magicBoolDec (hsEq x y) + +instance + HsEqBytestring : HsEq U.ByteString + HsEqBytestring = record { hsEq = U.eqByteString } + HsEqBlsG1 : HsEq U.Bls12-381-G1-Element + HsEqBlsG1 = record { hsEq = U.eqBls12-381-G1-Element } + HsEqBlsG2 : HsEq U.Bls12-381-G2-Element + HsEqBlsG2 = record { hsEq = U.eqBls12-381-G2-Element } + HsEqBlsMlResult : HsEq U.Bls12-381-MlResult + HsEqBlsMlResult = record { hsEq = U.eqBls12-381-MlResult } + +decEq-⟦ _⊢♯.atomic AtomicTyCon.aInteger ⟧tag = Data.Integer.Properties._≟_ +decEq-⟦ _⊢♯.atomic AtomicTyCon.aBytestring ⟧tag = builtinEq +decEq-⟦ _⊢♯.atomic AtomicTyCon.aString ⟧tag = Data.String.Properties._≟_ +decEq-⟦ _⊢♯.atomic AtomicTyCon.aUnit ⟧tag = Data.Unit.Properties._≟_ +decEq-⟦ _⊢♯.atomic AtomicTyCon.aBool ⟧tag = Data.Bool.Properties._≟_ +decEq-⟦ _⊢♯.atomic AtomicTyCon.aData ⟧tag v v₁ = magicBoolDec (U.eqDATA v v₁) +decEq-⟦ _⊢♯.atomic AtomicTyCon.aBls12-381-g1-element ⟧tag = builtinEq +decEq-⟦ _⊢♯.atomic AtomicTyCon.aBls12-381-g2-element ⟧tag = builtinEq +decEq-⟦ _⊢♯.atomic AtomicTyCon.aBls12-381-mlresult ⟧tag = builtinEq +decEq-⟦ _⊢♯.list t ⟧tag U.[] U.[] = yes refl +decEq-⟦ _⊢♯.list t ⟧tag U.[] (x U.∷ v₁) = no λ () +decEq-⟦ _⊢♯.list t ⟧tag (x U.∷ v) U.[] = no (λ ()) +decEq-⟦ _⊢♯.list t ⟧tag (x U.∷ v) (x₁ U.∷ v₁) with decEq-⟦ t ⟧tag x x₁ +... | no ¬x=x₁ = no λ { refl → ¬x=x₁ refl } +... | yes refl with decEq-⟦ _⊢♯.list t ⟧tag v v₁ +... | yes refl = yes refl +... | no ¬v=v₁ = no λ { refl → ¬v=v₁ refl } +decEq-⟦ _⊢♯.pair t t₁ ⟧tag (proj₁ U., proj₂) (proj₃ U., proj₄) with (decEq-⟦ t ⟧tag proj₁ proj₃) ×-dec (decEq-⟦ t₁ ⟧tag proj₂ proj₄) +... | yes ( refl , refl ) = yes refl +... | no ¬pq = no λ { refl → ¬pq (refl , refl) } +decEq-TmCon (tmCon t x) (tmCon t₁ x₁) with t ≟ t₁ +... | no ¬t=t₁ = no λ { refl → ¬t=t₁ refl } +... | yes refl with decEq-⟦ t ⟧tag x x₁ +... | yes refl = yes refl +... | no ¬x=x₁ = no λ { refl → ¬x=x₁ refl } + +``` +The Decidable Equality of terms needs to use the other instances, so we can present +that now. +``` +-- This terminating declaration shouldn't be needed? +-- It is the mutual recursion with list equality that requires it. +{-# TERMINATING #-} +decEq-⊢ (` x) (` x₁) with x ≟ x₁ +... | yes refl = yes refl +... | no ¬p = no λ { refl → ¬p refl } +decEq-⊢ (` x) (ƛ t₁) = no (λ ()) +decEq-⊢ (` x) (t₁ · t₂) = no (λ ()) +decEq-⊢ (` x) (force t₁) = no (λ ()) +decEq-⊢ (` x) (delay t₁) = no (λ ()) +decEq-⊢ (` x) (con x₁) = no (λ ()) +decEq-⊢ (` x) (constr i xs) = no (λ ()) +decEq-⊢ (` x) (case t₁ ts) = no (λ ()) +decEq-⊢ (` x) (builtin b) = no (λ ()) +decEq-⊢ (` x) error = no (λ ()) +decEq-⊢ (ƛ t) (` x) = no (λ ()) +decEq-⊢ (ƛ t) (ƛ t₁) with t ≟ t₁ +... | yes p = yes (cong ƛ p) +... | no ¬p = no λ { refl → ¬p refl } +decEq-⊢ (ƛ t) (t₁ · t₂) = no (λ ()) +decEq-⊢ (ƛ t) (force t₁) = no (λ ()) +decEq-⊢ (ƛ t) (delay t₁) = no (λ ()) +decEq-⊢ (ƛ t) (con x) = no (λ ()) +decEq-⊢ (ƛ t) (constr i xs) = no (λ ()) +decEq-⊢ (ƛ t) (case t₁ ts) = no (λ ()) +decEq-⊢ (ƛ t) (builtin b) = no (λ ()) +decEq-⊢ (ƛ t) error = no (λ ()) +decEq-⊢ (t · t₂) (` x) = no (λ ()) +decEq-⊢ (t · t₂) (ƛ t₁) = no (λ ()) +decEq-⊢ (t · t₂) (t₁ · t₃) with (t ≟ t₁) ×-dec (t₂ ≟ t₃) +... | yes ( refl , refl ) = yes refl +... | no ¬p = no λ { refl → ¬p (refl , refl) } +decEq-⊢ (t · t₂) (force t₁) = no (λ ()) +decEq-⊢ (t · t₂) (delay t₁) = no (λ ()) +decEq-⊢ (t · t₂) (con x) = no (λ ()) +decEq-⊢ (t · t₂) (constr i xs) = no (λ ()) +decEq-⊢ (t · t₂) (case t₁ ts) = no (λ ()) +decEq-⊢ (t · t₂) (builtin b) = no (λ ()) +decEq-⊢ (t · t₂) error = no (λ ()) +decEq-⊢ (force t) (` x) = no (λ ()) +decEq-⊢ (force t) (ƛ t₁) = no (λ ()) +decEq-⊢ (force t) (t₁ · t₂) = no (λ ()) +decEq-⊢ (force t) (force t₁) with t ≟ t₁ +... | yes refl = yes refl +... | no ¬p = no λ { refl → ¬p refl } +decEq-⊢ (force t) (delay t₁) = no (λ ()) +decEq-⊢ (force t) (con x) = no (λ ()) +decEq-⊢ (force t) (constr i xs) = no (λ ()) +decEq-⊢ (force t) (case t₁ ts) = no (λ ()) +decEq-⊢ (force t) (builtin b) = no (λ ()) +decEq-⊢ (force t) error = no (λ ()) +decEq-⊢ (delay t) (` x) = no (λ ()) +decEq-⊢ (delay t) (ƛ t₁) = no (λ ()) +decEq-⊢ (delay t) (t₁ · t₂) = no (λ ()) +decEq-⊢ (delay t) (force t₁) = no (λ ()) +decEq-⊢ (delay t) (delay t₁) with t ≟ t₁ +... | yes refl = yes refl +... | no ¬p = no λ { refl → ¬p refl } +decEq-⊢ (delay t) (con x) = no (λ ()) +decEq-⊢ (delay t) (constr i xs) = no (λ ()) +decEq-⊢ (delay t) (case t₁ ts) = no (λ ()) +decEq-⊢ (delay t) (builtin b) = no (λ ()) +decEq-⊢ (delay t) error = no (λ ()) +decEq-⊢ (con x) (` x₁) = no (λ ()) +decEq-⊢ (con x) (ƛ t₁) = no (λ ()) +decEq-⊢ (con x) (t₁ · t₂) = no (λ ()) +decEq-⊢ (con x) (force t₁) = no (λ ()) +decEq-⊢ (con x) (delay t₁) = no (λ ()) +decEq-⊢ (con x) (con x₁) with x ≟ x₁ +... | yes refl = yes refl +... | no ¬p = no λ { refl → ¬p refl } +decEq-⊢ (con x) (constr i xs) = no (λ ()) +decEq-⊢ (con x) (case t₁ ts) = no (λ ()) +decEq-⊢ (con x) (builtin b) = no (λ ()) +decEq-⊢ (con x) error = no (λ ()) +decEq-⊢ (constr i xs) (` x) = no (λ ()) +decEq-⊢ (constr i xs) (ƛ t₁) = no (λ ()) +decEq-⊢ (constr i xs) (t₁ · t₂) = no (λ ()) +decEq-⊢ (constr i xs) (force t₁) = no (λ ()) +decEq-⊢ (constr i xs) (delay t₁) = no (λ ()) +decEq-⊢ (constr i xs) (con x) = no (λ ()) +decEq-⊢ (constr i xs) (constr i₁ xs₁) with (i ≟ i₁) ×-dec (xs ≟ xs₁) +... | yes (refl , refl) = yes refl +... | no ¬pq = no λ { refl → ¬pq (refl , refl) } +decEq-⊢ (constr i xs) (case t₁ ts) = no (λ ()) +decEq-⊢ (constr i xs) (builtin b) = no (λ ()) +decEq-⊢ (constr i xs) error = no (λ ()) +decEq-⊢ (case t ts) (` x) = no (λ ()) +decEq-⊢ (case t ts) (ƛ t₁) = no (λ ()) +decEq-⊢ (case t ts) (t₁ · t₂) = no (λ ()) +decEq-⊢ (case t ts) (force t₁) = no (λ ()) +decEq-⊢ (case t ts) (delay t₁) = no (λ ()) +decEq-⊢ (case t ts) (con x) = no (λ ()) +decEq-⊢ (case t ts) (constr i xs) = no (λ ()) +decEq-⊢ (case t ts) (case t₁ ts₁) with (decEq-⊢ t t₁) ×-dec (ts ≟ ts₁) +... | yes (refl , refl) = yes refl +... | no ¬pq = no λ { refl → ¬pq (refl , refl) } +decEq-⊢ (case t ts) (builtin b) = no (λ ()) +decEq-⊢ (case t ts) error = no (λ ()) +decEq-⊢ (builtin b) (` x) = no (λ ()) +decEq-⊢ (builtin b) (ƛ t₁) = no (λ ()) +decEq-⊢ (builtin b) (t₁ · t₂) = no (λ ()) +decEq-⊢ (builtin b) (force t₁) = no (λ ()) +decEq-⊢ (builtin b) (delay t₁) = no (λ ()) +decEq-⊢ (builtin b) (con x) = no (λ ()) +decEq-⊢ (builtin b) (constr i xs) = no (λ ()) +decEq-⊢ (builtin b) (case t₁ ts) = no (λ ()) +decEq-⊢ (builtin b) (builtin b₁) with b ≟ b₁ +... | yes refl = yes refl +... | no ¬p = no λ { refl → ¬p refl } +decEq-⊢ (builtin b) error = no (λ ()) +decEq-⊢ error (` x) = no (λ ()) +decEq-⊢ error (ƛ t₁) = no (λ ()) +decEq-⊢ error (t₁ · t₂) = no (λ ()) +decEq-⊢ error (force t₁) = no (λ ()) +decEq-⊢ error (delay t₁) = no (λ ()) +decEq-⊢ error (con x) = no (λ ()) +decEq-⊢ error (constr i xs) = no (λ ()) +decEq-⊢ error (case t₁ ts) = no (λ ()) +decEq-⊢ error (builtin b) = no (λ ()) +decEq-⊢ error error = yes refl + +``` diff --git a/plutus-metatheory/src/VerifiedCompilation/UCaseOfCase.lagda.md b/plutus-metatheory/src/VerifiedCompilation/UCaseOfCase.lagda.md new file mode 100644 index 00000000000..5b857251aba --- /dev/null +++ b/plutus-metatheory/src/VerifiedCompilation/UCaseOfCase.lagda.md @@ -0,0 +1,135 @@ +--- +title: VerifiedCompilation.UCaseOfCas +layout: page +--- +# Untyped Case of Case Translation Phase + +``` +module VerifiedCompilation.UCaseOfCase where + +``` +## Imports + +``` +open import VerifiedCompilation.Equality using (DecEq; _≟_; decPointwise) +open import VerifiedCompilation.UntypedViews using (Pred; isCase?; isApp?; isForce?; isBuiltin?; isConstr?; isDelay?; isTerm?; allTerms?; iscase; isapp; isforce; isbuiltin; isconstr; isterm; allterms; isdelay) +open import VerifiedCompilation.UntypedTranslation using (Translation; translation?; Relation) + +import Relation.Binary as Binary using (Decidable) +import Relation.Unary as Unary using (Decidable) +open import Untyped using (_⊢; case; builtin; _·_; force; `; ƛ; delay; con; constr; error) +open import Untyped.CEK using (BApp; fullyAppliedBuiltin; BUILTIN; stepper; State; Stack) +open import Evaluator.Base using (maxsteps) +open import Builtin using (Builtin; ifThenElse) +open import Data.Product using (_×_; proj₁; proj₂; _,_) +open import Relation.Nullary using (Dec; yes; no; ¬_) +open import Data.Nat using (ℕ) +import Relation.Binary.PropositionalEquality as Eq +open Eq using (_≡_; refl; isEquivalence; cong) +open import Data.List.Relation.Binary.Pointwise.Base using (Pointwise) +open import Relation.Nullary.Product using (_×-dec_) +open import Data.Product using (_,_) +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. + +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 ⊢)) → + Pointwise (Translation CoC) alts alts' → + Pointwise (Translation CoC) tt tt' → + Pointwise (Translation CoC) ft ft' → + CoC + (case ((((force (builtin ifThenElse)) · b) · (constr tn tt)) · (constr fn ft)) alts) + (force ((((force (builtin ifThenElse)) · b) · (delay (case (constr tn tt') alts'))) · (delay (case (constr fn ft') alts')))) + +UntypedCaseOfCase : {X : Set} {{_ : DecEq X}} → (ast : X ⊢) → (ast' : X ⊢) → Set₁ +UntypedCaseOfCase = Translation CoC + +``` +## Decision Procedure + +Since this compiler phase is just a syntax re-arrangement in a very particular situation, we can +match on that situation in the before and after ASTs and apply the translation rule for this, or +expect anything else to be unaltered. + +This translation matches on exactly one, very specific pattern. Using parameterised Views we can +detect that case. We create two "views" for the two patterns - we will tie together the variables in the +later function `isCoC?`. +``` + +data CoCCase {X : Set} : (X ⊢) → Set where + isCoCCase : (b : X ⊢) (tn fn : ℕ) (tt ft alts : List (X ⊢)) → CoCCase (case ((((force (builtin ifThenElse)) · b) · (constr tn tt)) · (constr fn ft)) alts) +isCoCCase? : {X : Set} → Unary.Decidable (CoCCase {X}) +isCoCCase? t with (isCase? (isApp? (isApp? (isApp? (isForce? (isBuiltin?)) isTerm?) (isConstr? (allTerms?))) (isConstr? (allTerms?))) (allTerms?)) t +... | yes (iscase (isapp (isapp (isapp (isforce (isbuiltin ite)) (isterm b)) (isconstr tn (allterms tt))) (isconstr fn (allterms ft))) (allterms alts)) with ite ≟ ifThenElse +... | yes refl = yes (isCoCCase b tn fn tt ft alts) +... | no ¬≡b = no λ { (isCoCCase .b .tn .fn .tt .ft .alts) → ¬≡b refl } +isCoCCase? t | no ¬CoCCase = no λ { (isCoCCase b tn fn alts tt ft) → ¬CoCCase (iscase + (isapp + (isapp (isapp (isforce (isbuiltin ifThenElse)) (isterm b)) + (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}) +isCoCForce? t with (isForce? (isApp? (isApp? (isApp? (isForce? isBuiltin?) isTerm?) (isDelay? (isCase? (isConstr? allTerms?) allTerms?))) (isDelay? (isCase? (isConstr? allTerms?) allTerms?)))) t +... | no ¬CoCForce = no λ { (isCoCForce b tn fn tt' ft' alts') → ¬CoCForce + (isforce + (isapp + (isapp (isapp (isforce (isbuiltin ifThenElse)) (isterm b)) + (isdelay (iscase (isconstr tn (allterms tt')) (allterms alts')))) + (isdelay (iscase (isconstr fn (allterms ft')) (allterms alts')))))} +... | yes (isforce (isapp (isapp (isapp (isforce (isbuiltin ite)) (isterm b)) (isdelay (iscase (isconstr tn (allterms tt')) (allterms alts'))) ) (isdelay (iscase (isconstr fn (allterms ft')) (allterms alts''))))) with ite ≟ ifThenElse ×-dec alts' ≟ alts'' +... | yes (refl , refl) = yes (isCoCForce b tn fn tt' ft' alts') +... | no ¬p = no λ { (isCoCForce .b .tn .fn .tt' .ft' .alts') → ¬p (refl , refl) } + +``` +We can now create the final decision procedure. Because the translation can be applied recursively we need +the individual pattern decision `isCoC?` and the overall translation decision `isUntypedCaseOfCase?` to be mutually +recursive, so the `isUntypedCaseOfCase?` type declaration comes first, with the implementation later. + +``` +isUntypedCaseOfCase? : {X : Set} {{_ : DecEq X}} → Binary.Decidable (Translation CoC {X}) + +{-# TERMINATING #-} +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') } +... | 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? +``` + +## Semantic Equivalence + +We can show that this translation never alters the semantics of the statement. This is shown +in terms of the CEK machine evaluation. Since it is a simple re-arrangement of the syntax, it +isn't a refinement argument - the state before and after the operation is the same type, and is +unaltered buy the syntax re-arrangement. + +This does rely on the encoding of the semantics of `IfThenElse` in the CEK module, since we +need to show that the effective list of cases is the same as it would have been without the re-arrangement. + +The `stepper` function uses the CEK machine to evaluate a term. Here we call it with a very +large gas budget and begin in an empty context (which assumes the term is closed). + +``` +-- TODO: Several approaches are possible. +--semantic_equivalence : ∀ {X set} {ast ast' : ⊥ ⊢} + -- → ⊥ ⊢̂ ast ⊳̂ ast' + -- + -- → (stepper maxsteps (Stack.ϵ ; [] ▻ ast)) ≡ (stepper maxsteps (Stack.ε ; [] ▻ ast')) + +-- ∀ {s : ℕ} → stepper s ast ≡ ⇔ ∃ { s' : ℕ } [ stepper s' ast' ≡ ] +``` diff --git a/plutus-metatheory/src/VerifiedCompilation/UForceDelay.lagda.md b/plutus-metatheory/src/VerifiedCompilation/UForceDelay.lagda.md new file mode 100644 index 00000000000..c98902f096e --- /dev/null +++ b/plutus-metatheory/src/VerifiedCompilation/UForceDelay.lagda.md @@ -0,0 +1,113 @@ +--- +title: VerifiedCompilation.UForceDelay +layout: page +--- + +# Force-Delay Translation Phase +``` +module VerifiedCompilation.UForceDelay 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 Data.Nat using (ℕ; zero; suc) +open import Untyped.RenamingSubstitution using (weaken) +``` +## Translation Relation + +The Force-Delay translation removes the redundant application of the `force` operator to the `delay` operator. + +The simplest case of this is where there is a direct application `force (delay t)` that simply cancels out. However, +the translation also applies to nested or repeated applications, e.g. `force (force (delay (delay t)))`. + +Additionally, the translation applies where there is a Lambda abstraction paired with an application, so +`force (ƛ (delay t) · t₂)` for example. There can be multiple abstractions and applications, so long as they +cancel out precisely. + +`pureFD` is a mathematical expression of the relation. `FD` is more amenable to building a decision procedure. +Ultimately they should be equivalent. + +``` +data pureFD : Relation where + forcedelay : {X : Set} → (x x' : X ⊢) → Translation pureFD x x' → pureFD (force (delay x)) x' + pushfd : {X : Set} → (x : Maybe X ⊢) → (y : X ⊢) + → pureFD (force ((ƛ x) · y)) ((ƛ (force x)) · y) + transfd : {X : Set} → (x x'' x' : X ⊢) → Translation pureFD x x'' → Translation pureFD x'' x' → pureFD x x' + appfd : {X : Set} → (x : Maybe X ⊢) → (y : X ⊢) → pureFD ((ƛ x) · y) (ƛ (x · (weaken y))) + appfd⁻¹ : {X : Set} → (x : Maybe X ⊢) → (y : X ⊢) → pureFD (ƛ (x · (weaken y))) ((ƛ x) · y) + +data FD : ℕ → ℕ → Relation where + forcefd : (n nₐ : ℕ) → {X : Set} → (x x' : X ⊢) → FD (suc n) nₐ x x' → FD n nₐ (force x) x' + delayfd : (n nₐ : ℕ) → {X : Set} → (x x' : X ⊢) → FD n nₐ x x' → FD (suc n) nₐ (delay x) x' + lastdelay : (n nₐ : ℕ) → {X : Set} → (x x' : X ⊢) → Translation (FD zero zero) x x' → FD (suc zero) zero (delay x) x' + multiappliedfd : (n nₐ : ℕ) → {X : Set} → (x y x' y' : X ⊢) + → Translation (FD zero zero) y y' + → FD n (suc nₐ) (force x) x' + → FD n nₐ (force (x · y)) (x' · y') + multiabstractfd : (n nₐ : ℕ) → {X : Set} → (x x' : Maybe X ⊢) + → FD n nₐ (force x) x' + → FD n (suc nₐ) (force (ƛ x)) (ƛ x') + +ForceDelay : {X : Set} {{_ : DecEq X}} → (ast : X ⊢) → (ast' : X ⊢) → Set₁ +ForceDelay = Translation (FD zero zero) +``` +## Decision Procedure + + +``` +isForceDelay? : {X : Set} {{_ : DecEq X}} → Binary.Decidable (Translation (FD zero zero) {X}) + +{-# TERMINATING #-} +isFD? : {X : Set} {{_ : DecEq X}} → (n nₐ : ℕ) → Binary.Decidable (FD n nₐ {X}) + +isFD? n nₐ ast ast' with isForce? isTerm? ast + +-- If it doesn't start with force then it isn't going to match this translation, unless we have some delays left +isFD? zero nₐ ast ast' | no ¬force = no λ { (forcefd .zero .nₐ x .ast' xx) → ¬force (isforce (isterm x)) ; (multiappliedfd .zero .nₐ x y x' y' x₁ xx) → ¬force (isforce (isterm (x · y))) ; (multiabstractfd .zero nₐ x x' xx) → ¬force (isforce (isterm (ƛ x))) } +isFD? (suc n) nₐ ast ast' | no ¬force with (isDelay? isTerm? ast) +... | no ¬delay = no λ { (forcefd .(suc n) .nₐ x .ast' xx) → ¬force (isforce (isterm x)) ; (delayfd .n .nₐ x .ast' xx) → ¬delay (isdelay (isterm x)) ; (lastdelay n nₐ x .ast' x₁) → ¬delay (isdelay (isterm x)) ; (multiappliedfd .(suc n) .nₐ x y x' y' x₁ xx) → ¬force (isforce (isterm (x · y))) ; (multiabstractfd .(suc n) nₐ x x' xx) → ¬force (isforce (isterm (ƛ x))) } +... | yes (isdelay (isterm t)) with (isForceDelay? t ast') ×-dec (n ≟ zero) ×-dec (nₐ ≟ zero) +... | yes (p , refl , refl) = yes (lastdelay zero zero t ast' p) +... | no ¬zero with isFD? n nₐ t ast' +... | no ¬p = no λ { (delayfd .n .nₐ .t .ast' xxx) → ¬p xxx ; (lastdelay n nₐ .t .ast' x) → ¬zero (x , refl , refl)} +... | yes p = yes (delayfd n nₐ t ast' p) + +-- If there is an application we can increment the application counter +isFD? n nₐ ast ast' | yes (isforce (isterm t)) with (isApp? isTerm? isTerm?) t +isFD? n nₐ ast ast' | yes (isforce (isterm t)) | yes (isapp (isterm t₁) (isterm t₂)) with (isApp? isTerm? isTerm?) ast' +isFD? n nₐ ast ast' | yes (isforce (isterm t)) | yes (isapp (isterm t₁) (isterm t₂)) | no ¬isApp = no λ { (multiappliedfd .n .nₐ .t₁ .t₂ x' y' x xx) → ¬isApp (isapp (isterm x') (isterm y')) } +isFD? n nₐ ast ast' | yes (isforce (isterm t)) | yes (isapp (isterm t₁) (isterm t₂)) | yes (isapp (isterm t₁') (isterm t₂')) with (isFD? n (suc nₐ) (force t₁) t₁') ×-dec (isForceDelay? t₂ t₂') +... | yes (pfd , pfd2) = yes (multiappliedfd n nₐ t₁ t₂ t₁' t₂' pfd2 pfd) +... | no ¬FD = no λ { (multiappliedfd .n .nₐ .t₁ .t₂ .t₁' .t₂' x xx) → ¬FD (xx , x) } + +-- If there is a lambda we can decrement the application counter unless we have reached zero +isFD? n nₐ ast ast' | yes (isforce (isterm t)) | no ¬isApp with (isLambda? isTerm? t) +isFD? n (suc nₐ ) ast ast' | yes (isforce (isterm t)) | no ¬isApp | yes (islambda (isterm t₂)) with (isLambda? isTerm?) ast' +... | no ¬ƛ = no λ { (multiabstractfd .n .nₐ .t₂ x' xx) → ¬ƛ (islambda (isterm x')) } +... | yes (islambda (isterm t₂')) with (isFD? n nₐ (force t₂) t₂') +... | yes p = yes (multiabstractfd n nₐ t₂ t₂' p) +... | no ¬p = no λ { (multiabstractfd .n .nₐ .t₂ .t₂' xx) → ¬p xx } +-- If we have zero in the application counter then we can't descend further +isFD? n zero ast ast' | yes (isforce (isterm t)) | no ¬isApp | yes (islambda (isterm t₂)) = no λ { (forcefd .n .zero .(ƛ t₂) .ast' ()) } + +-- If we have matched none of the patterns then we need to consider nesting. +isFD? n nₐ ast ast' | yes (isforce (isterm t)) | no ¬isApp | no ¬ƛ with isFD? (suc n) nₐ t ast' +... | yes p = yes (forcefd n nₐ t ast' p) +... | no ¬p = no λ { (forcefd .n .nₐ .t .ast' xx) → ¬p xx ; (multiappliedfd .n .nₐ x y x' y' x₁ xx) → ¬isApp (isapp (isterm x) (isterm y)) ; (multiabstractfd .n nₐ x x' xx) → ¬ƛ (islambda (isterm x)) } + +isForceDelay? = translation? (isFD? zero zero) + +``` diff --git a/plutus-metatheory/src/VerifiedCompilation/UntypedTranslation.lagda.md b/plutus-metatheory/src/VerifiedCompilation/UntypedTranslation.lagda.md new file mode 100644 index 00000000000..4c1c1f604e9 --- /dev/null +++ b/plutus-metatheory/src/VerifiedCompilation/UntypedTranslation.lagda.md @@ -0,0 +1,193 @@ +--- +title: VerifiedCompilation.UntypedTranslation +layout: page +--- +# Generic Translation Relations for Untyped Plutus Core + +``` +module VerifiedCompilation.UntypedTranslation where + +open import Untyped using (_⊢; `; ƛ; case; constr; _·_; force; delay; con; builtin; error) +import Relation.Unary as Unary using (Decidable) +import Relation.Binary as Binary using (Decidable) +open import Relation.Nullary.Product using (_×-dec_) +open import Data.Product using (_,_) +open import Relation.Nullary using (Dec; yes; no; ¬_) +open import VerifiedCompilation.UntypedViews using (Pred; ListPred) +open import Utils as U using (Maybe) +open import RawU using (TmCon; tmCon; decTag; TyTag; ⟦_⟧tag; decTagCon; tmCon2TagCon) +open import Data.List using (List; [_]) +open import Data.Nat using (ℕ) +open import Data.List.Relation.Binary.Pointwise.Base using (Pointwise) +open import Builtin using (Builtin) +import Relation.Binary.PropositionalEquality as Eq +open Eq using (_≡_; refl) +open import VerifiedCompilation.Equality using (DecEq; _≟_; decPointwise) +``` +The generic type of a Translation is that it matches one (or more) patterns on the left to one +(or more) patterns on the right. If there are decision procedures to identify those patterns, +we can build a decision procedure to apply them recursivley down the AST structure. + +``` +Relation = { X : Set } → (X ⊢) → (X ⊢) → Set₁ + +data Translation (R : Relation) : { X : Set } → (X ⊢) → (X ⊢) → Set₁ where + istranslation : { X : Set } → (ast ast' : X ⊢) → R ast ast' → Translation R ast ast' + var : { X : Set } → {x : X} → Translation R (` x) (` x) -- We assume we won't want to translate variables individually? + ƛ : { X : Set } → {x x' : Maybe X ⊢} + → Translation R x x' + ---------------------- + → Translation R (ƛ x) (ƛ x') + app : { X : Set } → {f t f' t' : X ⊢} → + Translation R f f' → + Translation R t t' → + Translation R (f · t) (f' · t') + force : { X : Set } → {t t' : X ⊢} → + Translation R t t' → + Translation R (force t) (force t') + delay : { X : Set } → {t t' : X ⊢} → + Translation R t t' → + Translation R (delay t) (delay t') + con : { X : Set } → {tc : TmCon} → Translation R {X} (con tc) (con tc) + constr : { X : Set } → {xs xs' : List (X ⊢)} { n : ℕ } + → Pointwise (Translation R) xs xs' + ------------------------ + → Translation R (constr n xs) (constr n xs') + case : { X : Set } → {p p' : X ⊢} {alts alts' : List (X ⊢)} + → Pointwise (Translation R) alts alts' -- recursive translation for the other case patterns + → Translation R p p' + ------------------------ + → Translation R (case p alts) (case p' alts') + builtin : { X : Set } → {b : Builtin} → Translation R {X} (builtin b) (builtin b) + error : { X : Set } → Translation R {X} error error +``` +For the decision procedure we have the rather dissapointing 110 lines to demonstrate to Agda that, +having determine that we aren't in the translation pattern, we are in fact, still not in the translation pattern +for each pair of term types. +``` +-- Yes, I know, but for now... +{-# TERMINATING #-} +translation? : {X' : Set} {{ _ : DecEq X'}} → {R : Relation} → ({ X : Set } {{ _ : DecEq X}} → Binary.Decidable (R {X})) → Binary.Decidable (Translation R {X'}) +translation? isR? ast ast' with (isR? ast ast') +... | yes p = yes (istranslation ast ast' p) +translation? isR? (` x) ast' | no ¬p with (` x) ≟ ast' +... | yes refl = yes var +... | no ¬x=x = no λ { + (istranslation _ _ xx) → ¬p (xx); + var → ¬x=x refl + } +translation? isR? (ƛ ast) (ƛ ast') | no ¬p with translation? isR? ast ast' +... | yes p = yes (ƛ p) +... | no ¬pp = no (λ { (istranslation .(ƛ ast) .(ƛ ast') x) → ¬p x ; (ƛ xxx) → ¬pp xxx}) +translation? isR? (ƛ ast) (` x) | no ¬p = no λ { (istranslation _ _ x₁) → ¬p x₁ } +translation? isR? (ƛ ast) (ast'' · ast''') | no ¬p = no λ { (istranslation _ _ x₁) → ¬p x₁ } +translation? isR? (ƛ ast) (force ast'') | no ¬p = no λ { (istranslation _ _ x₁) → ¬p x₁ } +translation? isR? (ƛ ast) (delay ast'') | no ¬p = no λ { (istranslation _ _ x₁) → ¬p x₁ } +translation? isR? (ƛ ast) (con x) | no ¬p = no λ { (istranslation _ _ x₁) → ¬p x₁ } +translation? isR? (ƛ ast) (constr i xs) | no ¬p = no λ { (istranslation _ _ x₁) → ¬p x₁ } +translation? isR? (ƛ ast) (case ast'' ts) | no ¬p = no λ { (istranslation _ _ x₁) → ¬p x₁ } +translation? isR? (ƛ ast) (builtin b) | no ¬p = no λ { (istranslation _ _ x₁) → ¬p x₁ } +translation? isR? (ƛ ast) error | no ¬p = no λ { (istranslation _ _ x₁) → ¬p x₁ } + +translation? isR? (ast · ast₁) (` x) | no ¬p = no λ { (istranslation _ _ x₁) → ¬p x₁ } +translation? isR? (ast · ast₁) (ƛ ast') | no ¬p = no λ { (istranslation _ _ x₁) → ¬p x₁ } +translation? isR? (ast · ast₁) (ast' · ast'') | no ¬p with (translation? isR? ast ast') ×-dec (translation? isR? ast₁ ast'') +... | yes (p , q) = yes (app p q) +... | no ¬ppqq = no λ { (istranslation _ _ x) → ¬p x ; (app ppp ppp₁) → ¬ppqq (ppp , ppp₁)} +translation? isR? (ast · ast₁) (force ast') | no ¬p = no λ { (istranslation _ _ x₁) → ¬p x₁ } +translation? isR? (ast · ast₁) (delay ast') | no ¬p = no λ { (istranslation _ _ x₁) → ¬p x₁ } +translation? isR? (ast · ast₁) (con x) | no ¬p = no λ { (istranslation _ _ x₁) → ¬p x₁ } +translation? isR? (ast · ast₁) (constr i xs) | no ¬p = no λ { (istranslation _ _ x₁) → ¬p x₁ } +translation? isR? (ast · ast₁) (case ast' ts) | no ¬p = no λ { (istranslation _ _ x₁) → ¬p x₁ } +translation? isR? (ast · ast₁) (builtin b) | no ¬p = no λ { (istranslation _ _ x₁) → ¬p x₁ } +translation? isR? (ast · ast₁) error | no ¬p = no λ { (istranslation _ _ x₁) → ¬p x₁ } + +translation? isR? (force ast) (` x) | no ¬p = no λ { (istranslation _ _ x₁) → ¬p x₁ } +translation? isR? (force ast) (ƛ ast') | no ¬p = no λ { (istranslation _ _ x₁) → ¬p x₁ } +translation? isR? (force ast) (ast' · ast'') | no ¬p = no λ { (istranslation _ _ x₁) → ¬p x₁ } +translation? isR? (force ast) (force ast') | no ¬p with translation? isR? ast ast' +... | yes p = yes (force p) +... | no ¬pp = no λ { (istranslation .(force ast) .(force ast') x) → ¬p x ; (force xxx) → ¬pp xxx } +translation? isR? (force ast) (delay ast') | no ¬p = no λ { (istranslation _ _ x₁) → ¬p x₁ } +translation? isR? (force ast) (con x) | no ¬p = no λ { (istranslation _ _ x₁) → ¬p x₁ } +translation? isR? (force ast) (constr i xs) | no ¬p = no λ { (istranslation _ _ x₁) → ¬p x₁ } +translation? isR? (force ast) (case ast' ts) | no ¬p = no λ { (istranslation _ _ x₁) → ¬p x₁ } +translation? isR? (force ast) (builtin b) | no ¬p = no λ { (istranslation _ _ x₁) → ¬p x₁ } +translation? isR? (force ast) error | no ¬p = no λ { (istranslation _ _ x₁) → ¬p x₁ } + +translation? isR? (delay ast) (` x) | no ¬p = no λ { (istranslation _ _ x₁) → ¬p x₁ } +translation? isR? (delay ast) (ƛ ast') | no ¬p = no λ { (istranslation _ _ x₁) → ¬p x₁ } +translation? isR? (delay ast) (ast' · ast'') | no ¬p = no λ { (istranslation _ _ x₁) → ¬p x₁ } +translation? isR? (delay ast) (force ast') | no ¬p = no λ { (istranslation _ _ x₁) → ¬p x₁ } +translation? isR? (delay ast) (delay ast') | no ¬p with translation? isR? ast ast' +... | yes p = yes (delay p) +... | no ¬pp = no λ { (istranslation .(delay ast) .(delay ast') x) → ¬p x ; (delay xxx) → ¬pp xxx } +translation? isR? (delay ast) (con x) | no ¬p = no λ { (istranslation _ _ x₁) → ¬p x₁ } +translation? isR? (delay ast) (constr i xs) | no ¬p = no λ { (istranslation _ _ x₁) → ¬p x₁ } +translation? isR? (delay ast) (case ast' ts) | no ¬p = no λ { (istranslation _ _ x₁) → ¬p x₁ } +translation? isR? (delay ast) (builtin b) | no ¬p = no λ { (istranslation _ _ x₁) → ¬p x₁ } +translation? isR? (delay ast) error | no ¬p = no λ { (istranslation _ _ x₁) → ¬p x₁ } + +translation? isR? (con x) (` x₁) | no ¬p = no λ { (istranslation _ _ x₁) → ¬p x₁ } +translation? isR? (con x) (ƛ ast') | no ¬p = no λ { (istranslation _ _ x₁) → ¬p x₁ } +translation? isR? (con x) (ast' · ast'') | no ¬p = no λ { (istranslation _ _ x₁) → ¬p x₁ } +translation? isR? (con x) (force ast') | no ¬p = no λ { (istranslation _ _ x₁) → ¬p x₁ } +translation? isR? (con x) (delay ast') | no ¬p = no λ { (istranslation _ _ x₁) → ¬p x₁ } +translation? isR? (con x) (con x₁) | no ¬p with x ≟ x₁ +... | yes refl = yes con +... | no ¬x≟x₁ = no λ { (istranslation .(con x) .(con x₁) xx) → ¬p xx ; con → ¬x≟x₁ refl } +translation? isR? (con x) (constr i xs) | no ¬p = no λ { (istranslation _ _ x₁) → ¬p x₁ } +translation? isR? (con x) (case ast' ts) | no ¬p = no λ { (istranslation _ _ x₁) → ¬p x₁ } +translation? isR? (con x) (builtin b) | no ¬p = no λ { (istranslation _ _ x₁) → ¬p x₁ } +translation? isR? (con x) error | no ¬p = no λ { (istranslation _ _ x₁) → ¬p x₁ } + +translation? isR? (constr i xs) (` x) | no ¬p = no λ { (istranslation _ _ x₁) → ¬p x₁ } +translation? isR? (constr i xs) (ƛ ast') | no ¬p = no λ { (istranslation _ _ x₁) → ¬p x₁ } +translation? isR? (constr i xs) (ast' · ast'') | no ¬p = no λ { (istranslation _ _ x₁) → ¬p x₁ } +translation? isR? (constr i xs) (force ast') | no ¬p = no λ { (istranslation _ _ x₁) → ¬p x₁ } +translation? isR? (constr i xs) (delay ast') | no ¬p = no λ { (istranslation _ _ x₁) → ¬p x₁ } +translation? isR? (constr i xs) (con x) | no ¬p = no λ { (istranslation _ _ x₁) → ¬p x₁ } +translation? isR? (constr i xs) (constr i₁ xs₁) | no ¬p with (i ≟ i₁) ×-dec (decPointwise (translation? isR?) xs xs₁) +... | yes (refl , pxs) = yes (constr pxs) +... | no ¬ixs = no λ { (istranslation _ _ x) → ¬p x ; (constr x) → ¬ixs (refl , x) } +translation? isR? (constr i xs) (case ast' ts) | no ¬p = no λ { (istranslation _ _ x₁) → ¬p x₁ } +translation? isR? (constr i xs) (builtin b) | no ¬p = no λ { (istranslation _ _ x₁) → ¬p x₁ } +translation? isR? (constr i xs) error | no ¬p = no λ { (istranslation _ _ x₁) → ¬p x₁ } + +translation? isR? (case ast ts) (` x) | no ¬p = no λ { (istranslation _ _ x₁) → ¬p x₁ } +translation? isR? (case ast ts) (ƛ ast') | no ¬p = no λ { (istranslation _ _ x₁) → ¬p x₁ } +translation? isR? (case ast ts) (ast' · ast'') | no ¬p = no λ { (istranslation _ _ x₁) → ¬p x₁ } +translation? isR? (case ast ts) (force ast') | no ¬p = no λ { (istranslation _ _ x₁) → ¬p x₁ } +translation? isR? (case ast ts) (delay ast') | no ¬p = no λ { (istranslation _ _ x₁) → ¬p x₁ } +translation? isR? (case ast ts) (con x) | no ¬p = no λ { (istranslation _ _ x₁) → ¬p x₁ } +translation? isR? (case ast ts) (constr i xs) | no ¬p = no λ { (istranslation _ _ x₁) → ¬p x₁ } +translation? isR? (case ast ts) (case ast' ts₁) | no ¬p with (translation? isR? ast ast') ×-dec (decPointwise (translation? isR?) ts ts₁) +... | yes ( pa , pts ) = yes (case pts pa) +... | no ¬papts = no λ { (istranslation _ _ x) → ¬p x ; (case x xxx) → ¬papts (xxx , x) } +translation? isR? (case ast ts) (builtin b) | no ¬p = no λ { (istranslation _ _ x₁) → ¬p x₁ } +translation? isR? (case ast ts) error | no ¬p = no λ { (istranslation _ _ x₁) → ¬p x₁ } + +translation? isR? (builtin b) (` x) | no ¬p = no λ { (istranslation _ _ x₁) → ¬p x₁ } +translation? isR? (builtin b) (ƛ ast') | no ¬p = no λ { (istranslation _ _ x₁) → ¬p x₁ } +translation? isR? (builtin b) (ast' · ast'') | no ¬p = no λ { (istranslation _ _ x₁) → ¬p x₁ } +translation? isR? (builtin b) (force ast') | no ¬p = no λ { (istranslation _ _ x₁) → ¬p x₁ } +translation? isR? (builtin b) (delay ast') | no ¬p = no λ { (istranslation _ _ x₁) → ¬p x₁ } +translation? isR? (builtin b) (con x) | no ¬p = no λ { (istranslation _ _ x₁) → ¬p x₁ } +translation? isR? (builtin b) (constr i xs) | no ¬p = no λ { (istranslation _ _ x₁) → ¬p x₁ } +translation? isR? (builtin b) (case ast' ts) | no ¬p = no λ { (istranslation _ _ x₁) → ¬p x₁ } +translation? isR? (builtin b) (builtin b₁) | no ¬p with b ≟ b₁ +... | yes refl = yes builtin +... | no ¬b=b₁ = no λ { (istranslation _ _ x) → ¬p x ; builtin → ¬b=b₁ refl } +translation? isR? (builtin b) error | no ¬p = no λ { (istranslation _ _ x₁) → ¬p x₁ } + +translation? isR? error (` x) | no ¬p = no λ { (istranslation _ _ x₁) → ¬p x₁ } +translation? isR? error (ƛ ast') | no ¬p = no λ { (istranslation _ _ x₁) → ¬p x₁ } +translation? isR? error (ast' · ast'') | no ¬p = no λ { (istranslation _ _ x₁) → ¬p x₁ } +translation? isR? error (force ast') | no ¬p = no λ { (istranslation _ _ x₁) → ¬p x₁ } +translation? isR? error (delay ast') | no ¬p = no λ { (istranslation _ _ x₁) → ¬p x₁ } +translation? isR? error (con x) | no ¬p = no λ { (istranslation _ _ x₁) → ¬p x₁ } +translation? isR? error (constr i xs) | no ¬p = no λ { (istranslation _ _ x₁) → ¬p x₁ } +translation? isR? error (case ast' ts) | no ¬p = no λ { (istranslation _ _ x₁) → ¬p x₁ } +translation? isR? error (builtin b) | no ¬p = no λ { (istranslation _ _ x₁) → ¬p x₁ } +translation? isR? error error | no ¬p = yes error +``` diff --git a/plutus-metatheory/src/VerifiedCompilation/UntypedViews.lagda.md b/plutus-metatheory/src/VerifiedCompilation/UntypedViews.lagda.md new file mode 100644 index 00000000000..6b80c4fc9e5 --- /dev/null +++ b/plutus-metatheory/src/VerifiedCompilation/UntypedViews.lagda.md @@ -0,0 +1,215 @@ +--- +title: VerifiedCompilation.UntypedViews +layout: page +--- +# Predicates and View Types for Untyped Terms +``` +module VerifiedCompilation.UntypedViews where + +open import Untyped using (_⊢; `; ƛ; case; constr; _·_; force; delay; con; builtin; error) +open import Relation.Unary as Unary using (Decidable) +open import Relation.Nullary using (Dec; yes; no; ¬_) +open import Utils as U using (Maybe; nothing; just; Either) +open import Relation.Nullary.Product using (_×-dec_) +open import Data.Product using (_,_) +open import RawU using (TmCon) +open import Builtin using (Builtin) +open import VerifiedCompilation.Equality using (decEq-⊢) +open import Data.List using (List; [_]) +open import Data.Nat using (ℕ) +open import Function using (_∋_) + +``` +## Pattern Views for Terms + +Because many of the translations only run on a very specific AST pattern, we need a +[View](https://www.cambridge.org/core/journals/journal-of-functional-programming/article/view-from-the-left/F8A44CAC27CCA178AF69DD84BC585A2D) +to recognise that pattern and extract the variables. + +Following suggestions from Philip Wadler: creating Views for each Term type and then +allowing them to accept arbitrary sub-views should make this reusable. We can create +patterns using nested calls to these views, and decide them with nested calls to the +decision procedures. +``` + +Pred : Set₁ +Pred = {X : Set} → (X ⊢) → Set + +ListPred : Set₁ +ListPred = {X : Set} → List (X ⊢) → Set + +data isVar { X : Set } : (X ⊢) → Set where + isvar : (v : X) → isVar (` v) +isVar? : {X : Set} → Decidable (isVar {X}) +isVar? (` x) = yes (isvar x) +isVar? (ƛ x) = no λ () +isVar? (x · x₁) = no (λ ()) +isVar? (force x) = no (λ ()) +isVar? (delay x) = no (λ ()) +isVar? (con x) = no (λ ()) +isVar? (constr i xs) = no (λ ()) +isVar? (case x ts) = no (λ ()) +isVar? (builtin b) = no (λ ()) +isVar? error = no (λ ()) + +data isLambda (P : Pred) { X : Set } : (X ⊢) → Set where + islambda : {t : ((Maybe X) ⊢)} → P t → isLambda P (ƛ t) +isLambda? : {X : Set} {P : Pred} → ({X : Set} → Decidable (P {X})) → Decidable (isLambda P {X}) +isLambda? isP? (` x) = no λ () +isLambda? isP? (ƛ t) with isP? t +... | no ¬p = no λ { (islambda x) → ¬p x} +... | yes p = yes (islambda p) +isLambda? isP? (t _⊢.· t₁) = no (λ ()) +isLambda? isP? (_⊢.force t) = no (λ ()) +isLambda? isP? (_⊢.delay t) = no (λ ()) +isLambda? isP? (_⊢.con x) = no (λ ()) +isLambda? isP? (constr i xs) = no (λ ()) +isLambda? isP? (case t ts) = no (λ ()) +isLambda? isP? (_⊢.builtin b) = no (λ ()) +isLambda? isP? _⊢.error = no (λ ()) + +data isApp (P Q : Pred) {X : Set} : (X ⊢) → Set where + isapp : {l r : (X ⊢)} → P l → Q r → isApp P Q (l · r) +isApp? : {X : Set} → {P Q : Pred} → ({X : Set} → Decidable (P {X})) → ({X : Set} → Decidable (Q {X})) → Decidable (isApp P Q {X}) +isApp? isP? isQ? (` x) = no (λ ()) +isApp? isP? isQ? (ƛ t) = no (λ ()) +isApp? isP? isQ? (t · t₁) with (isP? t) ×-dec (isQ? t₁) +... | no ¬p = no λ { (isapp x x₁) → ¬p (x , x₁)} +... | yes (p , q) = yes (isapp p q) +isApp? isP? isQ? (force t) = no (λ ()) +isApp? isP? isQ? (delay t) = no (λ ()) +isApp? isP? isQ? (con x) = no (λ ()) +isApp? isP? isQ? (constr i xs) = no (λ ()) +isApp? isP? isQ? (case t ts) = no (λ ()) +isApp? isP? isQ? (builtin b) = no (λ ()) +isApp? isP? isQ? error = no (λ ()) + +data isForce (P : Pred) {X : Set} : (X ⊢) → Set where + isforce : {t : (X ⊢)} → P t → isForce P (force t) +isForce? : {X : Set} → {P : Pred} → ({X : Set} → Decidable (P {X})) → Decidable (isForce P {X}) +isForce? isP? (` x) = no (λ ()) +isForce? isP? (ƛ t) = no (λ ()) +isForce? isP? (t · t₁) = no (λ ()) +isForce? isP? (force t) with isP? t +... | no ¬p = no λ { (isforce x) → ¬p x} +... | yes p = yes (isforce p) +isForce? isP? (delay t) = no (λ ()) +isForce? isP? (con x) = no (λ ()) +isForce? isP? (constr i xs) = no (λ ()) +isForce? isP? (case t ts) = no (λ ()) +isForce? isP? (builtin b) = no (λ ()) +isForce? isP? error = no (λ ()) + + +data isDelay (P : Pred) {X : Set} : (X ⊢) → Set where + isdelay : {t : (X ⊢)} → P t → isDelay P (delay t) +isDelay? : {X : Set} → {P : Pred} → ({X : Set} → Decidable (P {X})) → Decidable (isDelay P {X}) +isDelay? isP? (` x) = no (λ ()) +isDelay? isP? (ƛ t) = no (λ ()) +isDelay? isP? (t · t₁) = no (λ ()) +isDelay? isP? (force t) = no (λ ()) +isDelay? isP? (delay t) with isP? t +... | yes p = yes (isdelay p) +... | no ¬p = no λ { (isdelay x) → ¬p x } +isDelay? isP? (con x) = no (λ ()) +isDelay? isP? (constr i xs) = no (λ ()) +isDelay? isP? (case t ts) = no (λ ()) +isDelay? isP? (builtin b) = no (λ ()) +isDelay? isP? error = no (λ ()) + +data isCon {X : Set} : (X ⊢) → Set where + iscon : (t : TmCon) → isCon {X} (con t) +isCon? : {X : Set} → Decidable (isCon {X}) +isCon? (` x) = no (λ ()) +isCon? (ƛ t) = no (λ ()) +isCon? (t · t₁) = no (λ ()) +isCon? (force t) = no (λ ()) +isCon? (delay t) = no (λ ()) +isCon? (con c) = yes (iscon c) +isCon? (constr i xs) = no (λ ()) +isCon? (case t ts) = no (λ ()) +isCon? (builtin b) = no (λ ()) +isCon? error = no (λ ()) + +data isConstr (Qs : ListPred) {X : Set} : (X ⊢) → Set where + isconstr : (i : ℕ) → {xs : List (X ⊢)} → Qs xs → isConstr Qs (constr i xs) +isConstr? : {X : Set} → {Qs : ListPred} → ({X : Set} → Decidable (Qs {X})) → Decidable (isConstr Qs {X}) +isConstr? isQs? (` x) = no (λ()) +isConstr? isQs? (ƛ t) = no (λ()) +isConstr? isQs? (t · t₁) = no (λ()) +isConstr? isQs? (force t) = no (λ()) +isConstr? isQs? (delay t) = no (λ()) +isConstr? isQs? (con x) = no (λ()) +isConstr? isQs? (constr i xs) with isQs? xs +... | no ¬q = no λ { (isconstr i₁ q) → ¬q q } +... | yes q = yes (isconstr i q) +isConstr? isQs? (case t ts) = no (λ()) +isConstr? isQs? (builtin b) = no (λ()) +isConstr? isQs? error = no (λ()) + +data isCase (P : Pred) (Qs : ListPred) { X : Set } : (X ⊢) → Set where + iscase : {t : (X ⊢)} → {ts : List (X ⊢)} → P t → Qs ts → isCase P Qs (case t ts) +isCase? : {X : Set} → {P : Pred} → {Qs : ListPred} → ({X : Set} → Decidable (P {X})) → ({X : Set} → Decidable (Qs {X})) → Decidable (isCase P Qs {X}) +isCase? isP? isQs? (` x) = no (λ ()) +isCase? isP? isQs? (ƛ t) = no (λ ()) +isCase? isP? isQs? (t · t₁) = no (λ ()) +isCase? isP? isQs? (force t) = no (λ ()) +isCase? isP? isQs? (delay t) = no (λ ()) +isCase? isP? isQs? (con x) = no (λ ()) +isCase? isP? isQs? (constr i xs) = no (λ ()) +isCase? isP? isQs? (case t ts) with (isP? t) ×-dec (isQs? ts) +... | no ¬pqs = no λ { (iscase p qs) → ¬pqs (p , qs)} +... | yes (p , qs) = yes (iscase p qs) +isCase? isP? isQs? (builtin b) = no (λ ()) +isCase? isP? isQs? error = no (λ ()) + +data isBuiltin {X : Set} : (X ⊢) → Set where + isbuiltin : (b : Builtin) → isBuiltin {X} (builtin b) +isBuiltin? : {X : Set} → Decidable (isBuiltin {X}) +isBuiltin? (` x) = no (λ ()) +isBuiltin? (ƛ t) = no (λ ()) +isBuiltin? (t · t₁) = no (λ ()) +isBuiltin? (force t) = no (λ ()) +isBuiltin? (delay t) = no (λ ()) +isBuiltin? (con x) = no (λ ()) +isBuiltin? (constr i xs) = no (λ ()) +isBuiltin? (case t ts) = no (λ ()) +isBuiltin? (builtin b) = yes (isbuiltin b) +isBuiltin? error = no (λ ()) + +data isError {X : Set} : (X ⊢) → Set where + iserror : isError {X} error +isError? : {X : Set} → Decidable (isError {X}) +isError? (` x) = no (λ ()) +isError? (ƛ t) = no (λ ()) +isError? (t · t₁) = no (λ ()) +isError? (force t) = no (λ ()) +isError? (delay t) = no (λ ()) +isError? (con x) = no (λ ()) +isError? (constr i xs) = no (λ ()) +isError? (case t ts) = no (λ ()) +isError? (builtin b) = no (λ ()) +isError? error = yes iserror +``` +Some basic views that will match any Term, to be used for "wildcard" parts of the pattern. +``` +data isTerm { X : Set } : (X ⊢) → Set where + isterm : (t : X ⊢) → isTerm t +isTerm? : {X : Set} → Decidable (isTerm {X}) +isTerm? t = yes (isterm t) + +data allTerms { X : Set } : List (X ⊢) → Set where + allterms : (ts : List (X ⊢)) → allTerms ts +allTerms? : {X : Set} → Decidable (allTerms {X}) +allTerms? ts = yes (allterms ts) +``` +## An Example +``` +data TestPat {X : Set} : (X ⊢) → Set where + tp : (t : X ⊢) (ts ts₂ : List (X ⊢)) → TestPat {X} (case (case t ts) ts₂) +isTestPat? : {X : Set} → Decidable (TestPat {X}) +isTestPat? v with isCase? (isCase? isTerm? allTerms?) allTerms? v +... | yes (iscase (iscase (isterm t) (allterms ts)) (allterms ts₁)) = yes (tp t ts ts₁) +... | no ¬tp = no λ { (tp t ts ts₂) → ¬tp (iscase (iscase (isterm t) (allterms ts)) (allterms ts₂)) } + +```