Certifier: add the decision procedure for caseReduce into the certifier (#6939)

Author: ana-pantilie

plutus-metatheory/plutus-metatheory.cabal

@@ -355,9 +355,11 @@ library
     MAlonzo.Code.VerifiedCompilation.Equality
     MAlonzo.Code.VerifiedCompilation.Purity
     MAlonzo.Code.VerifiedCompilation.UCaseOfCase
+    MAlonzo.Code.VerifiedCompilation.UCaseReduce
     MAlonzo.Code.VerifiedCompilation.UCSE
     MAlonzo.Code.VerifiedCompilation.UFloatDelay
     MAlonzo.Code.VerifiedCompilation.UForceDelay
+    MAlonzo.Code.VerifiedCompilation.UInline
     MAlonzo.Code.VerifiedCompilation.UntypedTranslation
     MAlonzo.Code.VerifiedCompilation.UntypedViews
     MAlonzo.RTE
@@ -370,11 +372,13 @@ library
     MAlonzo.Code.Agda.Builtin.Float
     MAlonzo.Code.Agda.Builtin.Int
     MAlonzo.Code.Agda.Builtin.IO
+    MAlonzo.Code.VerifiedCompilation.UInline
     MAlonzo.Code.Agda.Builtin.List
     MAlonzo.Code.Agda.Builtin.Maybe
     MAlonzo.Code.Agda.Builtin.Nat
     MAlonzo.Code.Agda.Builtin.Reflection
     MAlonzo.Code.Agda.Builtin.Sigma
+    MAlonzo.Code.VerifiedCompilation.UCaseReduce
     MAlonzo.Code.Agda.Builtin.Strict
     MAlonzo.Code.Agda.Builtin.String
     MAlonzo.Code.Agda.Builtin.Unit

plutus-metatheory/src/VerifiedCompilation.lagda.md

@@ -27,39 +27,33 @@ containing the generated proof object, a.k.a. the _certificate_. The certificate
 it into Agda and checking that it is correctly typed.
 
 ```
-{-# OPTIONS --allow-unsolved-metas #-}
 module VerifiedCompilation where
 ```
 
 ## Imports
 
 ```
-import Data.Bool.Base using (Bool; true; false; T; _∧_; _∨_; not)
-open import Data.Nat using (ℕ; zero; suc)
 open import Relation.Nullary using (Dec; yes; no; ¬_)
 
-import Relation.Nullary using (_×-dec_)
-import Relation.Binary using (Decidable)
 open import Untyped
 open import Utils as U using (Maybe;nothing;just;Either;inj₁;inj₂;List;[];_∷_;_×_;_,_)
 open import RawU using (Untyped)
-open import Data.String using (String;_++_)
+open import Data.String using (String)
 open import Agda.Builtin.IO using (IO)
-open import Agda.Builtin.Unit using (⊤;tt)
-import IO.Primitive.Core as IO using (return;_>>=_)
+open import Agda.Builtin.Unit using (⊤)
 import VerifiedCompilation.UCaseOfCase as UCC
 import VerifiedCompilation.UForceDelay as UFD
 import VerifiedCompilation.UFloatDelay as UFlD
 import VerifiedCompilation.UCSE as UCSE
+import VerifiedCompilation.UInline as UInline
+import VerifiedCompilation.UCaseReduce as UCR
 open import Data.Empty using (⊥)
-open import Scoped using (ScopeError;deBError)
 open import VerifiedCompilation.Equality using (DecEq)
-import Relation.Binary as Binary using (Decidable)
-open import VerifiedCompilation.UntypedTranslation using (Translation; Relation; translation?)
-import Relation.Binary as Binary using (Decidable)
+open import VerifiedCompilation.UntypedTranslation using (Relation)
 import Relation.Unary as Unary using (Decidable)
 import Agda.Builtin.Int
 import Relation.Nary as Nary using (Decidable)
+import IO.Primitive.Core as IO
 ```
 
 ## Compiler optimisation traces
@@ -96,8 +90,10 @@ data Transformation : SimplifierTag → Relation where
   isFD : {X : Set}{{_ : DecEq X}} → {ast ast' : X ⊢} → UFD.ForceDelay ast ast' → Transformation forceDelayT ast ast'
   isFlD : {X : Set}{{_ : DecEq X}} → {ast ast' : X ⊢} → UFlD.FloatDelay ast ast' → Transformation floatDelayT ast ast'
   isCSE : {X : Set}{{_ : DecEq X}} → {ast ast' : X ⊢} → UCSE.UntypedCSE ast ast' → Transformation cseT ast ast'
+  -- TODO: the decision procedure for Inline is broken, so we leave it as "not implemented"
+  -- isUInline : {X : Set}{{_ : DecEq X}} → {ast ast' : X ⊢} → UInline.UInline ast ast' → Transformation inlineT ast ast'
   inlineNotImplemented : {X : Set}{{_ : DecEq X}} → {ast ast' : X ⊢} → Transformation inlineT ast ast'
-  caseReduceNotImplemented : {X : Set}{{_ : DecEq X}} → {ast ast' : X ⊢} → Transformation caseReduceT ast ast'
+  isCaseReduce : {X : Set}{{_ : DecEq X}} → {ast ast' : X ⊢} → UCR.UCaseReduce ast ast' → Transformation caseReduceT ast ast'
 
 data Trace : { X : Set } {{_ : DecEq X}} → List (SimplifierTag × (X ⊢) × (X ⊢)) → Set₁ where
   empty : {X : Set}{{_ : DecEq X}} → Trace {X} []
@@ -120,8 +116,14 @@ isTransformation? tag ast ast' | forceDelayT with UFD.isForceDelay? ast ast'
 isTransformation? tag ast ast' | caseOfCaseT with UCC.isCaseOfCase? ast ast'
 ... | no ¬p = no λ { (isCoC x) → ¬p x }
 ... | yes p = yes (isCoC p)
-isTransformation? tag ast ast' | caseReduceT = yes caseReduceNotImplemented
+-- isTransformation? tag ast ast' | caseReduceT = yes caseReduceNotImplemented
+isTransformation? tag ast ast' | caseReduceT with UCR.isCaseReduce? ast ast'
+... | no ¬p = no λ { (isCaseReduce x) → ¬p x }
+... | yes p = yes (isCaseReduce p)
 isTransformation? tag ast ast' | inlineT = yes inlineNotImplemented
+-- isTransformation? tag ast ast' | inlineT with UInline.isInline? ast ast'
+-- ... | no ¬p = no λ { (isUInline x) → ¬p x }
+-- ... | yes p = yes (isUInline p)
 isTransformation? tag ast ast' | cseT with UCSE.isUntypedCSE? ast ast'
 ... | no ¬p = no λ { (isCSE x) → ¬p x }
 ... | yes p = yes (isCSE p)

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

@@ -66,6 +66,8 @@ isCR? ast ast' with (isCase? (isConstr? allTerms?) allTerms?) ast
 
 isCaseReduce? = translation? isCR?
 
+UCaseReduce = Translation CaseReduce
+
 ```
 ## An Example:
 

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

@@ -13,7 +13,7 @@ module VerifiedCompilation.UInline where
 ```
 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; convert; reflexive)
+open import VerifiedCompilation.UntypedTranslation using (Translation; TransMatch; translation?; Relation; convert; reflexive)
 import Relation.Binary as Binary using (Decidable)
 open import Untyped.RenamingSubstitution using (_[_])
 open import Agda.Builtin.Maybe using (Maybe; just; nothing)
@@ -43,7 +43,7 @@ _ : pureInline {⊥} (ƛ (` nothing) · error) error
 _ = inline (tr reflexive)
 
 _ : {X : Set} {a b : X} {{_ : DecEq X}} → pureInline (((ƛ (ƛ ((` (just nothing)) · (` nothing)))) · (` a)) · (` b)) ((` a) · (` b))
-_ = tr (Translation.app (Translation.istranslation (inline (tr reflexive))) reflexive) ⨾ inline (tr reflexive)
+_ = tr (Translation.match (TransMatch.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.
@@ -76,7 +76,7 @@ _ = 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.app (Translation.istranslation (var (last-sub reflexive))) reflexive
+_ = Translation.match (TransMatch.app (Translation.istranslation (var (last-sub reflexive))) reflexive)
 ```
 # Inline implies pureInline
 ```
@@ -108,4 +108,7 @@ isIl? ((e , v₁) , v) .(ƛ x) ast' | no ¬app | yes (islambda (isterm x)) with
 
 isInline? = translation? (isIl? □)
 
+UInline : {X : Set} {{_ : DecEq X}} → (ast : X ⊢) → (ast' : X ⊢) → Set₁
+UInline = Translation (Inline □)
+
 ```