Metatheory: add quantifications to formalization of builtin signatures

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

@@ -25,9 +25,10 @@ open import Type.Equality using (_≡β_;≡2β)
 open _≡β_
 open import Type.RenamingSubstitution using (weaken;ren;_[_];sub-cons;Sub;sub;sub∅;sub-cong)
 open import Builtin using (signature)
-open import Builtin.Signature using (Sig;sig;_⊢♯;_/_⊢⋆;mkCtx⋆)
-open _/_⊢⋆
+open import Builtin.Signature using (Sig;sig;_⊢♯;_⊢⋆;mkCtx⋆)
+open _⊢⋆
 open import Builtin.Constant.Type
+open import Data.Sum using (_⊎_;inj₁;inj₂)
 
 import Declarative as Syn
 import Algorithmic as Norm
@@ -146,11 +147,11 @@ helper (_⊢♯.list x) = cong ne (cong (^ list ·_) (helper x))
 helper (_⊢♯.array x) = cong ne (cong (^ array ·_) (helper x))
 helper (_⊢♯.pair x y) = cong ne (cong₂ (λ x y → ^ pair · x · y) (helper x) (helper y))
 
-mkTy-lem : ∀ {n⋆ n♯}(t : n⋆ / n♯ ⊢⋆) → Norm.mkTy t ≡ nf (Syn.mkTy t)
-mkTy-lem (` x) = refl
-mkTy-lem (x ↑) = cong con (helper x)
+mkTy-lem : ∀ {n⋆ n♯}(t : n⋆ ⊢⋆ ⊎ n♯ ⊢♯) → Norm.mkTy t ≡ nf (Syn.mkTy t)
+mkTy-lem (inj₁ (` x)) = refl
+mkTy-lem (inj₂ x) = cong con (helper x)
 
-sig2type⇒-lem : ∀{n⋆ n♯}{algRes}{synRes} (args : List (n⋆ / n♯ ⊢⋆)) → (algRes ≡ nf synRes) →
+sig2type⇒-lem : ∀{n⋆ n♯}{algRes}{synRes} (args : List (n⋆ ⊢⋆ ⊎ n♯ ⊢♯)) → (algRes ≡ nf synRes) →
                           Norm.sig2type⇒ args algRes ≡ nf (Syn.sig2type⇒ args synRes)
 sig2type⇒-lem [] p = p
 sig2type⇒-lem (x ∷ args) p = sig2type⇒-lem args (cong₂ _⇒_ (mkTy-lem x) p)

plutus-metatheory/src/Builtin.lagda.md

@@ -36,11 +36,12 @@ open import Agda.Builtin.Int using (Int)
 open import Agda.Builtin.String using (String)
 open import Utils using (ByteString;Maybe;DATA;Bls12-381-G1-Element;Bls12-381-G2-Element;Bls12-381-MlResult;♯)
 import Utils as U
-open import Builtin.Signature using (Sig;sig;_⊢♯;_/_⊢⋆;Args)
+open import Builtin.Signature using (Sig;sig;_⊢♯;_⊢⋆;Args;_↑)
                  using (integer;string;bytestring;unit;bool;pdata;bls12-381-g1-element;bls12-381-g2-element;bls12-381-mlresult)
 open _⊢♯ renaming (pair to bpair; list to blist; array to barray)
-open _/_⊢⋆
+open _⊢⋆
 open import Builtin.Constant.AtomicType
+open import Data.Sum using (_⊎_;inj₁;inj₂)
 
 open import Utils.Reflection using (defDec;defShow;defEnum;defListConstructors)
 ```
@@ -202,11 +203,11 @@ hence need to be embedded into `n⋆ / n♯ ⊢⋆` using the postfix constructo
     ∀A,a = (1 ,, 1)
 
     -- names for type variables of kind ⋆
-    A :  ∀{n⋆ n♯} → suc n⋆ / n♯ ⊢⋆
-    A = ` Z
+    A :  ∀{n⋆ n♯} → suc n⋆ ⊢⋆ ⊎ n♯ ⊢♯
+    A = inj₁ (` Z)
 
-    B :  ∀{n⋆ n♯} → suc (suc n⋆) / n♯ ⊢⋆
-    B = ` (S Z)
+    B :  ∀{n⋆ n♯} → suc (suc n⋆) ⊢⋆ ⊎ n♯ ⊢♯
+    B = inj₁ (` (S Z))
 
     -- names for type variables of kind ♯
     a : ∀{n♯} → suc n♯ ⊢♯
@@ -215,14 +216,14 @@ hence need to be embedded into `n⋆ / n♯ ⊢⋆` using the postfix constructo
     b : ∀{n♯} → suc (suc n♯) ⊢♯
     b = ` (S Z)
 
-    pair : ∀{n⋆ n♯} → n♯ ⊢♯ → n♯ ⊢♯ → n⋆ / n♯ ⊢⋆
-    pair a b = (bpair a b) ↑
+    pair : ∀{n⋆ n♯} → n♯ ⊢♯ → n♯ ⊢♯ → n⋆ ⊢⋆ ⊎ n♯ ⊢♯
+    pair a b = bpair a b ↑
 
-    list :  ∀{n⋆ n♯} → n♯ ⊢♯ → n⋆ / n♯ ⊢⋆
-    list a = (blist a) ↑
+    list :  ∀{n⋆ n♯} → n♯ ⊢♯ → n⋆ ⊢⋆ ⊎ n♯ ⊢♯
+    list a = blist a ↑
 
-    array :  ∀{n⋆ n♯} → n♯ ⊢♯ → n⋆ / n♯ ⊢⋆
-    array a = (barray a) ↑
+    array :  ∀{n⋆ n♯} → n♯ ⊢♯ → n⋆ ⊢⋆ ⊎ n♯ ⊢♯
+    array a = barray a ↑
 ```
 
 ### Operators for constructing signatures
@@ -245,10 +246,10 @@ sig n⋆ n♯ (t₃ ∷ t₂ ∷ t₁) tᵣ
     ArgSet = Σ (ℕ × ℕ) (λ { (n⋆ ,, n♯) → Args n⋆ n♯})
 
     ArgTy : ArgSet → Set
-    ArgTy ((n⋆ ,, n♯) ,, _) = n⋆ / n♯ ⊢⋆
+    ArgTy ((n⋆ ,, n♯) ,, _) = n⋆ ⊢⋆ ⊎ n♯ ⊢♯
 
     infix 12 _[_
-    _[_ : (nn : ℕ × ℕ)  → proj₁ nn / proj₂ nn ⊢⋆ → ArgSet
+    _[_ : (nn : ℕ × ℕ)  → proj₁ nn ⊢⋆ ⊎ proj₂ nn ⊢♯ → ArgSet
     _[_ (n⋆ ,, n♯) x = (n⋆ ,, n♯) ,, [ x ]
 
     infixl 10 _,_

plutus-metatheory/src/Builtin/Signature.lagda.md

@@ -32,6 +32,7 @@ open import Builtin.Constant.AtomicType using (AtomicTyCon;⟦_⟧at)
 open AtomicTyCon
 open import Builtin.Constant.Type using (TyCon)
 open TyCon
+open import Data.Sum using (_⊎_; inj₁; inj₂)
 ```
 
 ## Argument Types and Built-in Compatible Types
@@ -47,11 +48,17 @@ or type operators applied to built-in-compatible type.
 The type of built-in-compatible types (_⊢♯) is indexed by the number of
 distinct type variables of kind ♯.
 ```
+data ∀ₜ : ℕ → Set where
+  ∀̬ : ∀ {n}
+    → Fin n
+    --------
+    → ∀ₜ n
+
 -- Builtin compatible types of kind ♯
 data _⊢♯ : ℕ → Set where
   -- a type variable
-  ` : ∀ {n♯} →
-      Fin n♯
+  ` : ∀ {n♯}
+    → ∀ₜ n♯
       --------
     → n♯ ⊢♯
 
@@ -75,18 +82,15 @@ data _⊢♯ : ℕ → Set where
         -------
       → n♯ ⊢♯
 
--- argument types are either a variable of kind * or a builtin compatible type
-data _/_⊢⋆ : ℕ → ℕ → Set where
+data _⊢⋆ : ℕ → Set where
   -- a type variable of kind *
-  ` : ∀ {n⋆ n♯} →
-      Fin n⋆
+  ` : ∀ {n⋆}
+    → ∀ₜ n⋆
       --------
-    → n⋆ / n♯ ⊢⋆
-  -- a builtin compatible type
-  _↑ : ∀ {n⋆ n♯} →
-        n♯ ⊢♯
-       -------
-     → n⋆ / n♯ ⊢⋆
+    → n⋆ ⊢⋆
+
+_↑ : ∀{n⋆ n♯} → n♯ ⊢♯ → n⋆ ⊢⋆ ⊎ n♯ ⊢♯
+_↑ = inj₂
 
 pattern integer              = atomic aInteger
 pattern bytestring           = atomic aBytestring
@@ -106,7 +110,7 @@ of kind ♯ and kind *  that may appear.
 ```
 
 Args : ℕ → ℕ → Set
-Args n⋆ n♯ = List⁺ (n⋆ / n♯ ⊢⋆)
+Args n⋆ n♯ = List⁺ (∀ₜ n⋆ ⊎ ∀ₜ n♯ ⊎ n⋆ ⊢⋆ ⊎ n♯ ⊢♯) 
 
 ```
 
@@ -115,7 +119,7 @@ A Universe for return types.
 ```
 data _/_⊢r⋆ : ℕ → ℕ → Set where
   argtype : ∀ {n⋆ n♯} →
-      n⋆ / n♯ ⊢⋆
+      n⋆ ⊢⋆ ⊎ n♯ ⊢♯
       --------
     → n⋆ / n♯ ⊢r⋆
 
@@ -141,7 +145,7 @@ record Sig : Set where
      -- list of arguments
     args : Args fv⋆ fv♯
      -- type of result
-    result : fv⋆ / fv♯ ⊢⋆
+    result : fv⋆ ⊢⋆ ⊎ fv♯ ⊢♯
 
 open Sig
 
@@ -220,15 +224,21 @@ module FromSig (Ty : Ctx⋆ → Kind → Set)
 
 ```
     ⊢♯2TyNe♯ : ∀{n⋆ n♯} → n♯ ⊢♯ → TyNe (mkCtx⋆ n⋆ n♯) ♯
-    ⊢♯2TyNe♯ (` x) =  var (fin♯2∋⋆ x)
+    ⊢♯2TyNe♯ (` (∀̬ x)) =  var (fin♯2∋⋆ x)
     ⊢♯2TyNe♯ (atomic x) = ^ (atomic x)
     ⊢♯2TyNe♯ (list x)   = ^ list · ne (⊢♯2TyNe♯ x)
     ⊢♯2TyNe♯ (array x)   = ^ array · ne (⊢♯2TyNe♯ x)
     ⊢♯2TyNe♯ (pair x y) = ((^ pair) · ne (⊢♯2TyNe♯ x)) · ne (⊢♯2TyNe♯ y)
 
-    mkTy : ∀{n⋆ n♯} → n⋆ / n♯ ⊢⋆ → Ty (mkCtx⋆ n⋆ n♯) *
-    mkTy (` x) = ne (var (fin⋆2∋⋆ x))
-    mkTy (x ↑) = mkCon (ne (⊢♯2TyNe♯ x))
+    mkTy : ∀{n⋆ n♯} → ∀ₜ n⋆ ⊎ ∀ₜ n♯ ⊎ n⋆ ⊢⋆ ⊎ n♯ ⊢♯ → Ty (mkCtx⋆ n⋆ n♯) *
+    mkTy (inj₁ (∀̬ x)) = {!   !}
+    mkTy (inj₂ (inj₁ (∀̬ x))) = {!   !}
+    mkTy (inj₂ (inj₂ (inj₁ (` (∀̬ x))))) = ne (var (fin⋆2∋⋆ x))
+    mkTy (inj₂ (inj₂ (inj₂ x))) = mkCon (ne (⊢♯2TyNe♯ x))
+
+    mkResTy : ∀{n⋆ n♯} → n⋆ ⊢⋆ ⊎ n♯ ⊢♯ → Ty (mkCtx⋆ n⋆ n♯) *
+    mkResTy (inj₁ (` (∀̬ x))) = ne (var (fin⋆2∋⋆ x))
+    mkResTy (inj₂ x) = mkCon (ne (⊢♯2TyNe♯ x))
 ```
 
  `sig2type⇒` takes a list of arguments and a result type, and produces
@@ -239,7 +249,7 @@ module FromSig (Ty : Ctx⋆ → Kind → Set)
 
 ```
     sig2type⇒ : ∀{n⋆ n♯}
-              → List (n⋆ / n♯ ⊢⋆)
+              → List (∀ₜ n⋆ ⊎ ∀ₜ n♯ ⊎ n⋆ ⊢⋆ ⊎ n♯ ⊢♯)
               → Ty (mkCtx⋆ n⋆ n♯) * → Ty (mkCtx⋆ n⋆ n♯) *
     sig2type⇒ [] r = r
     sig2type⇒ (a ∷ as) r = sig2type⇒ as (mkTy a ⇒ r)
@@ -258,7 +268,7 @@ module FromSig (Ty : Ctx⋆ → Kind → Set)
 
 ```
     sig2type : Sig → Ty ∅ *
-    sig2type (sig fv⋆ fv♯ as res) = sig2typeΠ (sig2type⇒ (toList as) (mkTy res))
+    sig2type (sig fv⋆ fv♯ as res) = sig2typeΠ (sig2type⇒ (toList as) (mkResTy res))
 ```
 
 ### Types originating from a Signature
@@ -307,7 +317,7 @@ Every type obtained from a Signature σ using sig2type is a SigType.
              -- Additionally we could ask for the following condition to hold
              --  → (pn : n⋆ + n♯ ≡ tt)
                → {pt : tt ∔ 0 ≣ tt}
-               → (as : List (n⋆ / n♯ ⊢⋆))
+               → (as : List (∀ₜ n⋆ ⊎ ∀ₜ n♯ ⊎ n⋆ ⊢⋆ ⊎ n♯ ⊢♯))
                → ∀ {am at}(pa : length as ∔ am ≣ at)
                → {A : Ty (mkCtx⋆ n⋆ n♯) *} → (σA : SigTy pt pa A)
                → SigTy pt (start at) (sig2type⇒ as A)
@@ -327,7 +337,7 @@ Every type obtained from a Signature σ using sig2type is a SigType.
     -- From a signature obtain a signature type
     sig2SigTy : (σ : Sig) → SigTy (start (fv σ)) (start (args♯ σ)) (sig2type σ)
     sig2SigTy (sig n⋆ n♯ as r) =
-                sig2SigTyΠ refl (alldone (n⋆ + n♯)) (sig2SigTy⇒ (toList as) (alldone (length⁺ as)) (bresult (mkTy r)))
+                sig2SigTyΠ refl (alldone (n⋆ + n♯)) (sig2SigTy⇒ (toList as) (alldone (length⁺ as)) (bresult (mkResTy r)))
 
     -- extract the concrete type from a signature type.
     sigTy2type : ∀{Φ tm tn tt an am at}{A : Ty Φ *} → {pt : tn ∔ tm ≣ tt} → {pa : an ∔ am ≣ at} → SigTy pt pa A → Ty Φ *
@@ -348,5 +358,4 @@ Every type obtained from a Signature σ using sig2type is a SigType.
         → SigTy pt pa A
         → SigTy pt' pa' A'
     convSigTy {pt = pt} {pt'} {pa = pa} {pa'} refl sty rewrite unique∔ pt pt' | unique∔ pa pa' = sty
--- -}
 ```

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

@@ -100,7 +100,7 @@ d_sty2ty_84 v0
   = coe
       MAlonzo.Code.Type.BetaNormal.C_ne_20
       (coe
-         MAlonzo.Code.Builtin.Signature.du_'8866''9839'2TyNe'9839'_186
+         MAlonzo.Code.Builtin.Signature.du_'8866''9839'2TyNe'9839'_184
          (\ v1 v2 v3 -> coe MAlonzo.Code.Type.BetaNormal.C_ne_20 v3)
          (coe
             (\ v1 v2 v3 v4 -> coe MAlonzo.Code.Type.BetaNormal.C_'96'_8 v4))