diff --git a/plutus-metatheory/src/VerifiedCompilation.lagda.md b/plutus-metatheory/src/VerifiedCompilation.lagda.md index 839f4c02c97..3796dea4635 100644 --- a/plutus-metatheory/src/VerifiedCompilation.lagda.md +++ b/plutus-metatheory/src/VerifiedCompilation.lagda.md @@ -4,7 +4,7 @@ layout: page --- # Verified Compilation -## Introduction +## Introduction The verified compilation project is a formalization of the Untyped Plutus Core compiler optimisation transformations in Agda. The goal is to generate a formal proof that the optimisation component of the compiler has transformed the input program correctly @@ -19,7 +19,7 @@ the original and the optimised program. This is planned future work. The project is divided into several Agda modules, each of which is based on an optimisation stage of the compiler. They each contain the respective Agda formalisation of the program transformation and a decision procedure which takes -two programs as input and decides whether the transformation is applicable. +two programs as input and decides whether the transformation is applicable. This module is at the top of the project hierarchy and contains the main decision procedure which verifies the entire optimisation process. The final certification function receives a list of intermediate program ASTs produced by the compiler and outputs a file @@ -62,7 +62,7 @@ import Relation.Unary as Unary using (Decidable) A `Trace` represents a sequence of optimisation transformations applied to a program. It is a list of pairs of ASTs, where each pair represents the before and after of a transformation application. The `IsTransformation` type is a sum type that represents the possible transformations which are implemented in their -respective modules. Adding a new transformation requires extending this type. +respective modules. Adding a new transformation requires extending this type. The `isTrace?` decision procedure is at the core of the certification process. It produces the proof that the given list of ASTs are in relation with one another according to the transformations implemented in the project. It is @@ -76,26 +76,26 @@ element of the next pair in the list. This might not be necessary if we decide t which produces a `Trace` always produces a correct one, although it might be useful to make this explicit in the type. **TODO**: The compiler should provide information on which transformation was applied at each step in the trace. -`IsTransformation?` is currently quadratic in the number of transformations, which is not ideal. +`IsTransformation?` is currently quadratic in the number of transformations, which is not ideal. ``` -data Trace (R : Relation) : { X : Set } → List ((X ⊢) × (X ⊢)) → Set₁ where - empty : {X : Set} → Trace R {X} [] - cons : {X : Set} {x x' : X ⊢} {xs : List ((X ⊢) × (X ⊢))} → R x x' → Trace R {X} xs → Trace R {X} ((x , x') ∷ xs) +data Trace (R : Relation) : { X : Set } {{_ : DecEq X}} → List ((X ⊢) × (X ⊢)) → Set₁ where + empty : {X : Set}{{_ : DecEq X}} → Trace R {X} [] + cons : {X : Set}{{_ : DecEq X}} {x x' : X ⊢} {xs : List ((X ⊢) × (X ⊢))} → R x x' → Trace R {X} xs → Trace R {X} ((x , x') ∷ xs) data IsTransformation : Relation where - isCoC : {X : Set} → (ast ast' : X ⊢) → UCC.CoC ast ast' → IsTransformation ast ast' - isFD : {X : Set} → (ast ast' : X ⊢) → UFD.FD zero zero ast ast' → IsTransformation ast ast' + isCoC : {X : Set}{{_ : DecEq X}} → (ast ast' : X ⊢) → UCC.CoC ast ast' → IsTransformation ast ast' + isFD : {X : Set}{{_ : DecEq X}} → (ast ast' : X ⊢) → UFD.FD zero zero ast ast' → IsTransformation ast ast' -isTrace? : {X : Set} {R : Relation} → Binary.Decidable (R {X}) → Unary.Decidable (Trace R {X}) +isTrace? : {X : Set} {{_ : DecEq X}} {R : Relation} → Binary.Decidable (R {X}) → Unary.Decidable (Trace R {X}) isTrace? {X} {R} isR? [] = yes empty isTrace? {X} {R} isR? ((x₁ , x₂) ∷ xs) with isTrace? {X} {R} isR? xs ... | no ¬p = no λ {(cons a as) → ¬p as} ... | yes p with isR? x₁ x₂ ... | no ¬p = no λ {(cons x x₁) → ¬p x} ... | yes p₁ = yes (cons p₁ p) - + isTransformation? : {X : Set} {{_ : DecEq X}} → Binary.Decidable (IsTransformation {X}) isTransformation? ast₁ ast₂ with UCC.isCoC? ast₁ ast₂ ... | scrt with UFD.isFD? zero zero ast₁ ast₂ @@ -114,8 +114,8 @@ The proof objects are converted to a textual representation which can be written **TODO**: Finish the implementation. A textual representation is not usually ideal, but it is a good starting point. ``` -showTranslation : {X : Set} {ast ast' : X ⊢} → Translation IsTransformation ast ast' → String -showTranslation (Translation.istranslation _ _ x) = "istranslation TODO" +showTranslation : {X : Set} {{_ : DecEq X}} {ast ast' : X ⊢} → Translation IsTransformation ast ast' → String +showTranslation (Translation.istranslation x) = "istranslation TODO" showTranslation Translation.var = "var" showTranslation (Translation.ƛ t) = "(ƛ " ++ showTranslation t ++ ")" showTranslation (Translation.app t t₁) = "(app " ++ showTranslation t ++ " " ++ showTranslation t₁ ++ ")" @@ -127,12 +127,12 @@ showTranslation (Translation.case x t) = "(case TODO " ++ showTranslation t ++ " showTranslation Translation.builtin = "builtin" showTranslation Translation.error = "error" -showTrace : {X : Set} {xs : List ((X ⊢) × (X ⊢))} → Trace (Translation IsTransformation) xs → String +showTrace : {X : Set} {{_ : DecEq X}} {xs : List ((X ⊢) × (X ⊢))} → Trace (Translation IsTransformation) xs → String showTrace empty = "empty" showTrace (cons x bla) = "(cons " ++ showTranslation x ++ showTrace bla ++ ")" -serializeTraceProof : {X : Set} {xs : List ((X ⊢) × (X ⊢))} → Dec (Trace (Translation IsTransformation) xs) → String -serializeTraceProof (no ¬p) = "no" +serializeTraceProof : {X : Set} {{_ : DecEq X}} {xs : List ((X ⊢) × (X ⊢))} → Dec (Trace (Translation IsTransformation) xs) → String +serializeTraceProof (no ¬p) = "no" serializeTraceProof (yes p) = "yes " ++ showTrace p ``` @@ -140,7 +140,7 @@ serializeTraceProof (yes p) = "yes " ++ showTrace p ## The certification function The `runCertifier` function is the top-level function which can be called by the compiler through the foreign function interface. -It represents the "impure top layer" which receives the list of ASTs produced by the compiler and writes the certificate +It represents the "impure top layer" which receives the list of ASTs produced by the compiler and writes the certificate generated by the `certifier` function to disk. Again, the `certifier` is generic for testing purposes but it is instantiated with the top-level decision procedures by the `runCertifier` function. @@ -167,7 +167,7 @@ buildPairs [] = [] buildPairs (x ∷ []) = (x , x) ∷ [] buildPairs (x₁ ∷ (x₂ ∷ xs)) = (x₁ , x₂) ∷ buildPairs (x₂ ∷ xs) -traverseEitherList : {A B E : Set} → (A → Either E B) → List A → Either E (List B) +traverseEitherList : {A B E : Set} → (A → Either E B) → List A → Either E (List B) traverseEitherList _ [] = inj₂ [] traverseEitherList f (x ∷ xs) with f x ... | inj₁ err = inj₁ err @@ -176,13 +176,13 @@ traverseEitherList f (x ∷ xs) with f x ... | inj₂ resList = inj₂ (x' ∷ resList) certifier - : {X : Set} + : {X : Set} {{_ : DecEq X}} → List Untyped → Unary.Decidable (Trace (Translation IsTransformation) {Maybe X}) → Either ScopeError String certifier {X} rawInput isRTrace? with traverseEitherList toWellScoped rawInput ... | inj₁ err = inj₁ err -... | inj₂ rawTrace = +... | inj₂ rawTrace = let inputTrace = buildPairs rawTrace in inj₂ (serializeTraceProof (isRTrace? inputTrace)) diff --git a/plutus-metatheory/src/VerifiedCompilation/UCSE.lagda.md b/plutus-metatheory/src/VerifiedCompilation/UCSE.lagda.md new file mode 100644 index 00000000000..d1b559cc2c4 --- /dev/null +++ b/plutus-metatheory/src/VerifiedCompilation/UCSE.lagda.md @@ -0,0 +1,65 @@ +--- +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 (_[_]) +open import VerifiedCompilation.Purity using (UPure; isUPure?) +``` +## 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} {{ _ : DecEq X}} {x' : Maybe X ⊢} {x e : X ⊢} + → UPure X e + → Translation UCSE x (x' [ e ]) + → UCSE x ((ƛ x') · e) + +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 up x) → ¬match (isapp (islambda (isterm _)) (isterm _)) } +... | yes (isapp (islambda (isterm x')) (isterm e)) with (isUntypedCSE? ast (x' [ e ])) ×-dec (isUPure? e) +... | no ¬p = no λ { (cse up x) → ¬p (x , up) } +... | yes (p , upure) = yes (cse upure p) + +isUntypedCSE? = translation? isUCSE? +``` diff --git a/plutus-metatheory/src/VerifiedCompilation/UForceDelay.lagda.md b/plutus-metatheory/src/VerifiedCompilation/UForceDelay.lagda.md index 2f800fc86a9..b5566e3d54f 100644 --- a/plutus-metatheory/src/VerifiedCompilation/UForceDelay.lagda.md +++ b/plutus-metatheory/src/VerifiedCompilation/UForceDelay.lagda.md @@ -256,49 +256,49 @@ FD→pureFD {x = x} {x' = x'} (ffd (afd .zero (ffd .zero args x₁))) = FD→pur ``` -{- + isForceDelay? : {X : Set} {{_ : DecEq X}} → Binary.Decidable (Translation (FD zero zero) {X}) {-# TERMINATING #-} -isFD? : {X : Set} {{_ : DecEq X}} → (n args : ℕ) → Binary.Decidable (FD n args {X}) +isFD? : {X : Set} {{_ : DecEq X}} → (n nₐ : ℕ) → Binary.Decidable (FD {X} n nₐ) isFD? n args 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 args ast ast' | no ¬force = no λ { (forcefd .zero .args xx) → ¬force (isforce (isterm _)) ; (multiappliedfd .zero .args x xx) → ¬force (isforce (isterm (_ · _))) ; (multiabstractfd .zero args xx) → ¬force (isforce (isterm (ƛ _))) } -isFD? (suc n) args ast ast' | no ¬force with (isDelay? isTerm? ast) -... | no ¬delay = no λ { (forcefd .(suc n) .args xx) → ¬force (isforce (isterm _)) ; (delayfd .n .args xx) → ¬delay (isdelay (isterm _)) ; (lastdelay n args x) → ¬delay (isdelay (isterm _)) ; (multiappliedfd .(suc n) .args x xx) → ¬force (isforce (isterm (_ · _))) ; (multiabstractfd .(suc n) args xx) → ¬force (isforce (isterm (ƛ _)))} -... | yes (isdelay (isterm t)) with (isForceDelay? t ast') ×-dec (n ≟ zero) ×-dec (args ≟ zero) +isFD? zero nₐ ast ast' | no ¬force = no λ { (forcefd .zero .nₐ xx) → ¬force (isforce (isterm _)) ; (multiappliedfd .zero .nₐ x xx) → ¬force (isforce (isterm (_ · _))) ; (multiabstractfd .zero nₐ xx) → ¬force (isforce (isterm (ƛ _))) } +isFD? (suc n) nₐ ast ast' | no ¬force with (isDelay? isTerm? ast) +... | no ¬delay = no λ { (forcefd .(suc n) .nₐ xx) → ¬force (isforce (isterm _)) ; (delayfd .n .nₐ xx) → ¬delay (isdelay (isterm _)) ; (lastdelay n nₐ x) → ¬delay (isdelay (isterm _)) ; (multiappliedfd .(suc n) .nₐ x xx) → ¬force (isforce (isterm (_ · _))) ; (multiabstractfd .(suc n) nₐ xx) → ¬force (isforce (isterm (ƛ _)))} +... | yes (isdelay (isterm t)) with (isForceDelay? t ast') ×-dec (n ≟ zero) ×-dec (nₐ ≟ zero) ... | yes (p , refl , refl) = yes (lastdelay zero zero p) -... | no ¬zero with isFD? n args t ast' -... | no ¬p = no λ { (delayfd .n .args xx) → ¬p xx ; (lastdelay n args x) → ¬zero (x , refl , refl)} -... | yes p = yes (delayfd n args p) +... | no ¬zero with isFD? n nₐ t ast' +... | no ¬p = no λ { (delayfd .n .nₐ xx) → ¬p xx ; (lastdelay n nₐ x) → ¬zero (x , refl , refl)} +... | yes p = yes (delayfd n nₐ p) -- If there is an application we can increment the application counter -isFD? n args ast ast' | yes (isforce (isterm t)) with (isApp? isTerm? isTerm?) t -isFD? n args ast ast' | yes (isforce (isterm t)) | yes (isapp (isterm t₁) (isterm t₂)) with (isApp? isTerm? isTerm?) ast' -isFD? n args ast ast' | yes (isforce (isterm t)) | yes (isapp (isterm t₁) (isterm t₂)) | no ¬isApp = no λ { (multiappliedfd .n .args x xx) → ¬isApp (isapp (isterm _) (isterm _)) } -isFD? n args ast ast' | yes (isforce (isterm t)) | yes (isapp (isterm t₁) (isterm t₂)) | yes (isapp (isterm t₁') (isterm t₂')) with (isFD? n (suc args) (force t₁) t₁') ×-dec (isForceDelay? t₂ t₂') -... | yes (pfd , pfd2) = yes (multiappliedfd n args pfd2 pfd) -... | no ¬FD = no λ { (multiappliedfd .n .args x xx) → ¬FD (xx , x) } +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ₐ x xx) → ¬isApp (isapp (isterm _) (isterm _)) } +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ₐ pfd2 pfd) +... | no ¬FD = no λ { (multiappliedfd .n .nₐ x xx) → ¬FD (xx , x) } -- If there is a lambda we can decrement the application counter unless we have reached zero -isFD? n args ast ast' | yes (isforce (isterm t)) | no ¬isApp with (isLambda? isTerm? t) -isFD? n (suc args ) ast ast' | yes (isforce (isterm t)) | no ¬isApp | yes (islambda (isterm t₂)) with (isLambda? isTerm?) ast' -... | no ¬ƛ = no λ { (multiabstractfd .n .args xx) → ¬ƛ (islambda (isterm _)) } -... | yes (islambda (isterm t₂')) with (isFD? n args (force t₂) t₂') -... | yes p = yes (multiabstractfd n args p) -... | no ¬p = no λ { (multiabstractfd .n .args xx) → ¬p xx } +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ₐ xx) → ¬ƛ (islambda (isterm _)) } +... | yes (islambda (isterm t₂')) with (isFD? n nₐ (force t₂) t₂') +... | yes p = yes (multiabstractfd n nₐ p) +... | no ¬p = no λ { (multiabstractfd .n .nₐ 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 ()) } -- If we have matched none of the patterns then we need to consider nesting. -isFD? n args ast ast' | yes (isforce (isterm t)) | no ¬isApp | no ¬ƛ with isFD? (suc n) args t ast' -... | yes p = yes (forcefd n args p) -... | no ¬p = no λ { (forcefd .n .args xx) → ¬p xx ; (multiappliedfd .n .args x xx) → ¬isApp (isapp (isterm _) (isterm _)) ; (multiabstractfd .n args xx) → ¬ƛ (islambda (isterm _)) } +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ₐ p) +... | no ¬p = no λ { (forcefd .n .nₐ xx) → ¬p xx ; (multiappliedfd .n .nₐ x xx) → ¬isApp (isapp (isterm _) (isterm _)) ; (multiabstractfd .n nₐ xx) → ¬ƛ (islambda (isterm _)) } isForceDelay? = translation? (isFD? zero zero) --} + ```