Metatheory: use Fin instead of nested Maybe for representing variables (#7486)

Metatheory: simplify variable representation by using Fin instead of nested Maybe

Author: basetunnel

plutus-metatheory/README.md

@@ -80,7 +80,7 @@ $ cabal test plutus-metatheory
 To build the documentation as a static site:
 
 ```
-$ agda --html --html-highlight=auto --html-dir=html src/index.lagda.md
+$ agda-with-stdlib --html --html-highlight=auto --html-dir=html src/index.lagda.md
 $ jekyll build -s html -d html/_site
 ```
 

plutus-metatheory/src/Algorithmic/Erasure.lagda.md

@@ -3,14 +3,12 @@ title: Algorithmic.Erasure
 layout: page
 ---
 ```
-{-# OPTIONS --injective-type-constructors #-}
-
 module Algorithmic.Erasure where
 ```
 
 ```
 open import Agda.Primitive using (lzero)
-open import Data.Nat using (ℕ)
+open import Data.Nat using (ℕ;suc;zero)
 open import Function using (_∘_;id)
 open import Data.Nat using (_+_)
 open import Data.Nat.Properties using (+-cancelˡ-≡)
@@ -55,20 +53,20 @@ open import Algorithmic.Soundness using (embCtx;embVar;emb;emb-ConstrArgs;lema-m
 ```
 
 ```
-len⋆ : Ctx⋆ → Set
-len⋆ ∅        = ⊥
-len⋆ (Γ ,⋆ K) = Maybe (len⋆ Γ)
+len⋆ : Ctx⋆ → ℕ
+len⋆ ∅        = 0
+len⋆ (Γ ,⋆ K) = suc (len⋆ Γ)
 
-len : ∀{Φ} → Ctx Φ → Set
-len ∅ = ⊥
+len : ∀{Φ} → Ctx Φ → ℕ
+len ∅ = 0
 len (Γ ,⋆ K) = len Γ
-len (Γ , A)  = Maybe (len Γ)
+len (Γ , A)  = suc (len Γ)
 ```
 
 ```
-eraseVar : ∀{Φ Γ}{A : Φ ⊢Nf⋆ *} → Γ ∋ A → len Γ
-eraseVar Z     = nothing
-eraseVar (S α) = just (eraseVar α)
+eraseVar : ∀{Φ Γ}{A : Φ ⊢Nf⋆ *} → Γ ∋ A → Fin (len Γ)
+eraseVar Z     = zero
+eraseVar (S α) = suc (eraseVar α)
 eraseVar (T α) = eraseVar α
 
 eraseTC : (A : ∅ ⊢Nf⋆ Kind.♯) → ⟦ A ⟧ → TmCon
@@ -114,47 +112,45 @@ I need to pattern match on the term constructors
 lenLemma : ∀ {Φ}(Γ : D.Ctx Φ) → len (nfCtx Γ) ≡ D.len Γ
 lenLemma D.∅        = refl
 lenLemma (Γ D.,⋆ J) = lenLemma Γ
-lenLemma (Γ D., A)  = cong Maybe (lenLemma Γ)
+lenLemma (Γ D., A)  = cong suc (lenLemma Γ)
 
 lenLemma⋆ : ∀ Φ → D.len⋆ Φ ≡ len⋆ Φ
 lenLemma⋆ ∅       = refl
-lenLemma⋆ (Φ ,⋆ K) = cong Maybe (lenLemma⋆ Φ)
+lenLemma⋆ (Φ ,⋆ K) = cong suc (lenLemma⋆ Φ)
 
 -- these lemmas for each clause of eraseVar and erase below could be
 -- avoided by using with but it would involve doing with on a long
 -- string of arguments, both contexts, equality proof above, and
 -- before and after versions of all arguments and all recursive calls
 
--- these lemmas (as stated and proved) require injectivity of type
--- constructors
-lemzero : ∀{X X'}(p : Maybe {lzero} X ≡ Maybe X') → nothing ≡ subst id p nothing
+lemzero : ∀{X X' : ℕ} (p : suc X ≡ suc X') → zero ≡ subst Fin p zero
 lemzero refl = refl
 
-lemsuc : ∀{X X'}(p : Maybe {lzero} X ≡ Maybe X')(q : X ≡ X')(x : X) →
-  just (subst id q x) ≡ subst id p (just x)
+lemsuc : ∀{X X' : ℕ} (p : suc X ≡ suc X') (q : X ≡ X') (x : Fin X) →
+  suc (subst Fin q x) ≡ subst Fin p (suc x)
 lemsuc refl refl x = refl
 
 lem≡Ctx : ∀{Φ}{Γ Γ' : Ctx Φ} → Γ ≡ Γ' → len Γ ≡ len Γ'
 lem≡Ctx refl = refl
 
 lem-conv∋ : ∀{Φ Γ Γ'}{A A' : Φ ⊢Nf⋆ *}(p : Γ ≡ Γ')(q : A ≡ A')(x : Γ A.∋ A)
-  →  subst id (lem≡Ctx p) (eraseVar x) ≡ eraseVar (conv∋ p q x)
+  →  subst Fin (lem≡Ctx p) (eraseVar x) ≡ eraseVar (conv∋ p q x)
 lem-conv∋ refl refl x = refl
 
 sameVar : ∀{Φ Γ}{A : Φ ⊢⋆ *}(x : Γ D.∋ A)
-  → D.eraseVar x ≡ subst id (lenLemma Γ) (eraseVar (nfTyVar x))
-sameVar {Γ = Γ D., _} D.Z     = lemzero (cong Maybe (lenLemma Γ))
+  → D.eraseVar x ≡ subst Fin (lenLemma Γ) (eraseVar (nfTyVar x))
+sameVar {Γ = Γ D., _} D.Z     = lemzero (cong suc (lenLemma Γ))
 sameVar {Γ = Γ D., _} (D.S x) = trans
-  (cong just (sameVar x))
-  (lemsuc (cong Maybe (lenLemma Γ)) (lenLemma Γ) (eraseVar (nfTyVar x)))
+  (cong suc (sameVar x))
+  (lemsuc (cong suc (lenLemma Γ)) (lenLemma Γ) (eraseVar (nfTyVar x)))
 sameVar {Γ = Γ D.,⋆ _} (D.T {A = A} x) = trans
   (sameVar x)
-  (cong (subst id (lenLemma Γ)) (lem-conv∋ refl (ren-nf S A) (T (nfTyVar x))))
+  (cong (subst Fin (lenLemma Γ)) (lem-conv∋ refl (ren-nf S A) (T (nfTyVar x))))
 
-lemVar : ∀{X X'}(p : X ≡ X')(x : X) →  ` (subst id p x) ≡ subst _⊢ p (` x)
+lemVar : ∀{X X'}(p : X ≡ X')(x : Fin X) →  ` (subst Fin p x) ≡ subst _⊢ p (` x)
 lemVar refl x = refl
 
-lemƛ : ∀{X X'}(p : X ≡ X')(q : Maybe X ≡ Maybe X')(t : Maybe X ⊢)
+lemƛ : ∀{X X'}(p : X ≡ X')(q : suc X ≡ suc X')(t : suc X ⊢)
   → ƛ (subst _⊢ q t) ≡ subst _⊢ p (ƛ t)
 lemƛ refl refl t = refl
 
@@ -235,7 +231,7 @@ same {Γ = Γ}(D.` x) =
   trans (cong ` (sameVar x)) (lemVar (lenLemma Γ) (eraseVar (nfTyVar x)))
 same {Γ = Γ} (D.ƛ t) = trans
   (cong ƛ (same t))
-  (lemƛ (lenLemma Γ) (cong Maybe (lenLemma Γ)) (erase (nfType t)))
+  (lemƛ (lenLemma Γ) (cong suc (lenLemma Γ)) (erase (nfType t)))
 same {Γ = Γ} (t D.· u) = trans
   (cong₂ _·_ (same t) (same u))
   (lem· (lenLemma Γ) (erase (nfType t)) (erase (nfType u)))
@@ -274,21 +270,21 @@ same {Γ = Γ} (D.case t cases) rewrite lemCase (erase (nfType t)) (erase-Cases
 same'Len : ∀ {Φ}(Γ : A.Ctx Φ) → D.len (embCtx Γ) ≡ len Γ
 same'Len ∅          = refl
 same'Len (Γ ,⋆ J)   = same'Len Γ
-same'Len (Γ , A)    = cong Maybe (same'Len Γ)
+same'Len (Γ , A)    = cong suc (same'Len Γ)
 
 lem-Dconv∋ : ∀{Φ Γ Γ'}{A A' : Φ ⊢⋆ *}(p : Γ ≡ Γ')(q : A ≡ A')(x : Γ D.∋ A)
-  → subst id (cong D.len p) (D.eraseVar x)  ≡ D.eraseVar (D.conv∋ p q x)
+  → subst Fin (cong D.len p) (D.eraseVar x)  ≡ D.eraseVar (D.conv∋ p q x)
 lem-Dconv∋ refl refl x = refl
 
 same'Var : ∀{Φ Γ}{A : Φ ⊢Nf⋆ *}(x : Γ A.∋ A)
-  →  eraseVar x ≡ subst id (same'Len Γ) (D.eraseVar (embVar x))
-same'Var {Γ = Γ , _} Z     = lemzero (cong Maybe (same'Len Γ))
+  →  eraseVar x ≡ subst Fin (same'Len Γ) (D.eraseVar (embVar x))
+same'Var {Γ = Γ , _} Z     = lemzero (cong suc (same'Len Γ))
 same'Var {Γ = Γ , _} (S x) = trans
-  (cong just (same'Var x))
-  (lemsuc (cong Maybe (same'Len Γ)) (same'Len Γ) (D.eraseVar (embVar x)))
+  (cong suc (same'Var x))
+  (lemsuc (cong suc (same'Len Γ)) (same'Len Γ) (D.eraseVar (embVar x)))
 same'Var {Γ = Γ ,⋆ _} (T {A = A} x) = trans
   (same'Var x)
-  (cong (subst id (same'Len Γ)) (lem-Dconv∋ refl (sym (ren-embNf S A))
+  (cong (subst Fin (same'Len Γ)) (lem-Dconv∋ refl (sym (ren-embNf S A))
         (D.T (embVar x))))
 
 same'TC : ∀ {Φ} {Γ : Ctx Φ} A (tcn : ⟦ A ⟧) →
@@ -326,7 +322,7 @@ same' {Γ = Γ} (` x) =
   trans (cong ` (same'Var x)) (lemVar (same'Len Γ) (D.eraseVar (embVar x)))
 same' {Γ = Γ} (ƛ t) = trans
   (cong ƛ (same' t))
-  (lemƛ (same'Len Γ) (cong Maybe (same'Len Γ)) (D.erase (emb t)))
+  (lemƛ (same'Len Γ) (cong suc (same'Len Γ)) (D.erase (emb t)))
 same' {Γ = Γ} (t · u) = trans
   (cong₂ _·_ (same' t) (same' u))
   (lem· (same'Len Γ) (D.erase (emb t)) (D.erase (emb u)))

plutus-metatheory/src/Algorithmic/Erasure/RenamingSubstitution.lagda.md

@@ -10,7 +10,8 @@ module Algorithmic.Erasure.RenamingSubstitution where
 open import Relation.Binary.PropositionalEquality using (_≡_;refl;sym;trans;subst;cong;cong₂)
 open import Function using (id;_∘_)
 open import Data.Vec using (Vec;_∷_;lookup)
-open import Data.Fin using (Fin;toℕ)
+open import Data.Fin using (Fin;toℕ;suc;zero)
+open import Data.Nat using (ℕ;suc;zero)
 
 open import Utils using (Kind;*;Maybe;nothing;just)
 open import Utils.List using (List;[];_∷_)
@@ -38,15 +39,15 @@ open import Builtin.Constant.Type using (TyCon)
 ```
 
 ```
-backVar⋆ : ∀{Φ}(Γ : Ctx Φ) → len Γ → Φ ⊢Nf⋆ *
+backVar⋆ : ∀{Φ}(Γ : Ctx Φ) → Fin (len Γ) → Φ ⊢Nf⋆ *
 backVar⋆ (Γ ,⋆ J) x        = weakenNf (backVar⋆ Γ x)
-backVar⋆ (Γ , A)  nothing  = A
-backVar⋆ (Γ , A)  (just x) = backVar⋆ Γ x
+backVar⋆ (Γ , A)  zero  = A
+backVar⋆ (Γ , A)  (suc x) = backVar⋆ Γ x
 
-backVar : ∀{Φ}(Γ : Ctx Φ)(x : len Γ) → Γ ∋ (backVar⋆ Γ x)
+backVar : ∀{Φ}(Γ : Ctx Φ)(x : Fin (len Γ)) → Γ ∋ (backVar⋆ Γ x)
 backVar (Γ ,⋆ J) x       = T (backVar Γ x)
-backVar (Γ , A) nothing  = Z
-backVar (Γ , A) (just x) = S (backVar Γ x)
+backVar (Γ , A) zero  = Z
+backVar (Γ , A) (suc x) = S (backVar Γ x)
 
 backVar⋆-eraseVar : ∀{Φ}{Γ : Ctx Φ}{A : Φ ⊢Nf⋆ *}(x : Γ ∋ A) →
   backVar⋆ Γ (eraseVar x) ≡ A
@@ -85,11 +86,11 @@ backVar-eraseVar (S x) = trans
   (cong S (backVar-eraseVar x))
 backVar-eraseVar (T x) = trans (subst-T (backVar⋆-eraseVar x) (cong weakenNf (backVar⋆-eraseVar x)) (backVar _ (eraseVar x))) (cong T (backVar-eraseVar x))
 
-eraseVar-backVar : ∀{Φ}(Γ : Ctx Φ)(x : len Γ) → eraseVar (backVar Γ x) ≡ x
+eraseVar-backVar : ∀{Φ}(Γ : Ctx Φ)(x : Fin (len Γ)) → eraseVar (backVar Γ x) ≡ x
 eraseVar-backVar ∅       ()
 eraseVar-backVar (Γ ,⋆ J) x        = eraseVar-backVar Γ x
-eraseVar-backVar (Γ , A)  nothing  = refl
-eraseVar-backVar (Γ , A)  (just x) = cong just (eraseVar-backVar Γ x)
+eraseVar-backVar (Γ , A)  zero  = refl
+eraseVar-backVar (Γ , A)  (suc x) = cong suc (eraseVar-backVar Γ x)
 
 --
 
@@ -98,10 +99,10 @@ erase-Ren : ∀{Φ Ψ}{Γ : Ctx Φ}{Δ : Ctx Ψ}(ρ⋆ : ⋆.Ren Φ Ψ)
 erase-Ren ρ⋆ ρ i = eraseVar (ρ (backVar _ i))
 
 ext-erase : ∀{Φ Ψ}{Γ : Ctx Φ}{Δ : Ctx Ψ}(ρ⋆ : ⋆.Ren Φ Ψ)
-  → (ρ : A.Ren ρ⋆ Γ Δ){A : Φ ⊢Nf⋆ *}(α : len (Γ , A))
+  → (ρ : A.Ren ρ⋆ Γ Δ){A : Φ ⊢Nf⋆ *}(α : Fin (len (Γ , A)))
   → erase-Ren ρ⋆ (A.ext ρ⋆ ρ {B = A}) α ≡ U.lift (erase-Ren ρ⋆ ρ) α
-ext-erase ρ⋆ ρ nothing  = refl
-ext-erase ρ⋆ ρ (just α) = refl
+ext-erase ρ⋆ ρ zero  = refl
+ext-erase ρ⋆ ρ (suc α) = refl
 
 conv∋-erase : ∀{Φ}{Γ : Ctx Φ}{A A' : Φ ⊢Nf⋆ *}
   → (p : A ≡ A')
@@ -116,7 +117,7 @@ conv⊢-erase : ∀{Φ}{Γ : Ctx Φ}{A A' : Φ ⊢Nf⋆ *}
 conv⊢-erase refl t = refl
 
 ext⋆-erase : ∀{Φ Ψ K}{Γ : Ctx Φ}{Δ : Ctx Ψ}(ρ⋆ : ⋆.Ren Φ Ψ)
-  → (ρ : A.Ren ρ⋆ Γ Δ)(α : len Γ)
+  → (ρ : A.Ren ρ⋆ Γ Δ)(α : Fin (len Γ))
   → erase-Ren (⋆.ext ρ⋆ {K = K}) (A.ext⋆ ρ⋆ ρ) α ≡ erase-Ren ρ⋆ ρ α
 ext⋆-erase {Γ = Γ} ρ⋆ ρ α = conv∋-erase
   (trans (sym (renNf-comp (backVar⋆ Γ α))) (renNf-comp (backVar⋆ Γ α)))
@@ -202,23 +203,23 @@ cong-erase-sub σ⋆ σ refl x .x refl = refl
 
 exts-erase : ∀ {Φ Ψ}{Γ Δ}(σ⋆ : SubNf Φ Ψ)(σ : A.Sub σ⋆ Γ Δ)
   → {B : Φ ⊢Nf⋆ *}
-  → (α : Maybe (len Γ))
+  → (α : Fin (suc (len Γ)))
   → erase-Sub σ⋆ (A.exts σ⋆ σ {B}) α ≡ U.lifts (erase-Sub σ⋆ σ) α
-exts-erase σ⋆ σ nothing = refl
-exts-erase {Γ = Γ}{Δ} σ⋆ σ {B} (just α) = trans
+exts-erase σ⋆ σ zero = refl
+exts-erase {Γ = Γ}{Δ} σ⋆ σ {B} (suc α) = trans
   (conv⊢-erase
     (renNf-id (subNf σ⋆ (backVar⋆ Γ α)))
     (A.ren id (conv∋ refl (sym (renNf-id _)) ∘ S) (σ (backVar Γ α))))
     (trans (ren-erase id (conv∋ refl (sym (renNf-id _)) ∘ S) (σ (backVar Γ α)))
            (U.ren-cong (λ β → trans
              (conv∋-erase (sym (renNf-id _)) (S (backVar Δ β)))
-             (cong just (eraseVar-backVar Δ β)))
+             (cong suc (eraseVar-backVar Δ β)))
              (erase (σ (backVar Γ α)))))
 
 exts⋆-erase : ∀ {Φ Ψ}{Γ Δ}(σ⋆ : SubNf Φ Ψ)(σ : A.Sub σ⋆ Γ Δ)
   → {B : Φ ⊢Nf⋆ *}
   → ∀{K}
-  → (α : len Γ)
+  → (α : Fin (len Γ))
   →  erase-Sub (extsNf σ⋆ {K}) (A.exts⋆ σ⋆ σ) α ≡ erase-Sub σ⋆ σ α
 exts⋆-erase {Γ = Γ}{Δ} σ⋆ σ {B} α = trans
   (conv⊢-erase
@@ -315,8 +316,8 @@ lem[] : ∀{Φ}{Γ : Ctx Φ}{A B : Φ ⊢Nf⋆ *}(N : Γ , A ⊢ B)(W : Γ ⊢ A
 lem[] {Γ = Γ}{A = A}{B} N W = trans
   (trans
     (U.sub-cong
-      (λ{ nothing    → sym (conv⊢-erase (sym (subNf-id A)) W)
-        ; (just α) → trans
+      (λ{ zero    → sym (conv⊢-erase (sym (subNf-id A)) W)
+        ; (suc α) → trans
                (cong ` (sym (eraseVar-backVar Γ α)))
                (sym (conv⊢-erase (sym (subNf-id (backVar⋆ Γ α))) (` (backVar Γ α))))})
       (erase N))

plutus-metatheory/src/Declarative/Erasure.lagda.md

@@ -10,8 +10,8 @@ module Declarative.Erasure where
 ## Imports
 
 ```
-open import Data.Nat using (ℕ)
-open import Data.Fin using (toℕ)
+open import Data.Nat using (ℕ;suc;zero)
+open import Data.Fin using (Fin;suc;zero;toℕ)
 open import Data.Empty using (⊥)
 open import Data.Vec using (Vec)
 open import Data.Unit using (tt)
@@ -39,23 +39,23 @@ open import Algorithmic using (ty≅sty₁)
 ```
 
 ```
-len : ∀{Φ} → Ctx Φ → Set
-len ∅        = ⊥
+len : ∀{Φ} → Ctx Φ → ℕ
+len ∅        = 0
 len (Γ ,⋆ K) = len Γ
-len (Γ , A)  = Maybe (len Γ)
+len (Γ , A)  = suc (len Γ)
 
-lenI : ∀{Φ} → Ctx Φ → Set
-lenI ∅        = ⊥
-lenI (Γ ,⋆ K) = Maybe (lenI Γ)
-lenI (Γ , A)  = Maybe (lenI Γ)
+lenI : ∀{Φ} → Ctx Φ → ℕ
+lenI ∅        = 0
+lenI (Γ ,⋆ K) = suc (lenI Γ)
+lenI (Γ , A)  = suc (lenI Γ)
 
-len⋆ : Ctx⋆ → Set
-len⋆ ∅        = ⊥
-len⋆ (Γ ,⋆ K) = Maybe (len⋆ Γ)
+len⋆ : Ctx⋆ → ℕ
+len⋆ ∅        = 0
+len⋆ (Γ ,⋆ K) = suc (len⋆ Γ)
 
-eraseVar : ∀{Φ Γ}{A : Φ ⊢⋆ *} → Γ ∋ A → len Γ
-eraseVar Z     = nothing
-eraseVar (S α) = just (eraseVar α)
+eraseVar : ∀{Φ Γ}{A : Φ ⊢⋆ *} → Γ ∋ A → Fin (len Γ)
+eraseVar Z     = zero
+eraseVar (S α) = suc (eraseVar α)
 eraseVar (T α) = eraseVar α
 
 eraseTC : (A : ∅ ⊢⋆ ♯) → ⟦ A ⟧d → TmCon
@@ -94,15 +94,15 @@ erase (error A)       = error
 erase (constr e Tss p cs) = constr (toℕ e) (erase-ConstrArgs cs)
 erase (case t cases)  = case (erase t) (erase-Cases cases)
 
-backVar⋆ : ∀{Φ}(Γ : Ctx Φ) → len Γ → Φ ⊢⋆ *
+backVar⋆ : ∀{Φ}(Γ : Ctx Φ) → Fin (len Γ) → Φ ⊢⋆ *
 backVar⋆ (Γ ,⋆ J) x       = T.weaken (backVar⋆ Γ x)
-backVar⋆ (Γ , A) nothing  = A
-backVar⋆ (Γ , A) (just x) = backVar⋆ Γ x
+backVar⋆ (Γ , A) zero  = A
+backVar⋆ (Γ , A) (suc x) = backVar⋆ Γ x
 
-backVar : ∀{Φ}(Γ : Ctx Φ)(x : len Γ) → Γ ∋ (backVar⋆ Γ x)
+backVar : ∀{Φ}(Γ : Ctx Φ)(x : Fin (len Γ)) → Γ ∋ (backVar⋆ Γ x)
 backVar (Γ ,⋆ J) x        = T (backVar Γ x)
-backVar (Γ , A)  nothing  = Z
-backVar (Γ , A)  (just x) = S (backVar Γ x)
+backVar (Γ , A)  zero  = Z
+backVar (Γ , A)  (suc x) = S (backVar Γ x)
 
 erase-Sub σ⋆ σ i = erase (σ (backVar _ i))
 ```

plutus-metatheory/src/Evaluator/Program.lagda.md

@@ -126,7 +126,7 @@ parsePLC namedprog = do
   -- ^ FIXME: this should have an interface that guarantees that the
   -- shifter is run
 
-parseUPLC : ProgramNU → Either ERROR (⊥ U.⊢)
+parseUPLC : ProgramNU → Either ERROR (0 U.⊢)
 parseUPLC namedprog = do
   prog ← withE (ERROR.scopeError ∘ freeVariableError) $ deBruijnifyU namedprog
   withE scopeError $ U.scopeCheckU0 (convPU prog)
@@ -177,7 +177,7 @@ showUPLCResult (□ V) = return $ prettyPrintUTm (U.extricateU0 (U.discharge V))
 showUPLCResult ◆     = inj₁ (runtimeError userError)
 showUPLCResult _     = inj₁ (runtimeError gasError)
 
-executeUPLCwithMP : ∀{A} → RawCostModel → (CostModel → MachineParameters A) → (A → String) → ⊥ U.⊢ → Either ERROR String
+executeUPLCwithMP : ∀{A} → RawCostModel → (CostModel → MachineParameters A) → (A → String) → 0 U.⊢ → Either ERROR String
 executeUPLCwithMP (cekMachineCosts , rawmodel) mkMP report t with createMap rawmodel
 ... | just model = do
     let machineparam = mkMP (cekMachineCosts , model)
@@ -187,7 +187,7 @@ executeUPLCwithMP (cekMachineCosts , rawmodel) mkMP report t with createMap rawm
     return (r ++ report exBudget)
 ... | nothing = inj₁ (jsonError "while processing parameters.")
 
-executeUPLC : BudgetMode RawCostModel → ⊥ U.⊢ → Either ERROR String
+executeUPLC : BudgetMode RawCostModel → 0 U.⊢ → Either ERROR String
 executeUPLC Silent t = (withE runtimeError $ U.stepper maxsteps (ε ; [] ▻ t)) >>= showUPLCResult
 executeUPLC (Counting rcm) t = executeUPLCwithMP rcm machineParameters countingReport t
 executeUPLC (Tallying rcm) t = executeUPLCwithMP rcm tallyingMachineParameters tallyingReport t

plutus-metatheory/src/MAlonzo/Code/Algorithmic.hs

@@ -48,10 +48,10 @@ data T_'9839'Kinded_40
   = C_'9839'_42 | C_K'9839'_48 T_'9839'Kinded_40
 -- Algorithmic.lemma♯Kinded
 d_lemma'9839'Kinded_58 ::
-  MAlonzo.Code.Utils.T_Kind_652 ->
-  MAlonzo.Code.Utils.T_Kind_652 ->
-  MAlonzo.Code.Utils.T_Kind_652 ->
-  MAlonzo.Code.Utils.T_Kind_652 ->
+  MAlonzo.Code.Utils.T_Kind_682 ->
+  MAlonzo.Code.Utils.T_Kind_682 ->
+  MAlonzo.Code.Utils.T_Kind_682 ->
+  MAlonzo.Code.Utils.T_Kind_682 ->
   T_'9839'Kinded_40 ->
   MAlonzo.Code.Type.BetaNormal.T__'8866'Ne'8902'__6 ->
   MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20
@@ -154,11 +154,11 @@ data T__'8866'__178
     C__'183'__196 MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4
                   T__'8866'__178 T__'8866'__178 |
     C_Λ_202 T__'8866'__178 |
-    C__'183''8902'_'47'__212 MAlonzo.Code.Utils.T_Kind_652
+    C__'183''8902'_'47'__212 MAlonzo.Code.Utils.T_Kind_682
                              MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4 T__'8866'__178
                              MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4 |
     C_wrap_220 T__'8866'__178 |
-    C_unwrap_230 MAlonzo.Code.Utils.T_Kind_652
+    C_unwrap_230 MAlonzo.Code.Utils.T_Kind_682
                  MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4
                  MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4 T__'8866'__178 |
     C_constr_240 MAlonzo.Code.Data.Fin.Base.T_Fin_10