more changes

IntersectMBO · May 10, 2024 · 2be9b59 · 2be9b59
1 parent 4012a39
commit 2be9b59
Show file tree

Hide file tree

Showing 4 changed files with 140 additions and 139 deletions.
diff --git a/plutus-metatheory/src/Builtin.lagda.md b/plutus-metatheory/src/Builtin.lagda.md
@@ -155,151 +155,151 @@ shorthands for types, such as `integer`, `bool`, etc are of type `n♯ ⊢♯`,
 hence need to be embedded into `n⋆ / n♯ ⊢⋆` using the postfix constructor `↑`.
 
 ```
- open import Data.Product using (_×_) renaming (_,_ to _,,_)
+open import Data.Product using (_×_) renaming (_,_ to _,,_)
 
- -- number of different type variables
- ∙ ∀a ∀b,a ∀A ∀A,a : ℕ × ℕ
- ∙ = (0 ,, 0)
- ∀a = (0 ,, 1)
- ∀b,a = (0 ,, 2)
- ∀A = (1 ,, 0)
- ∀A,a = (1 ,, 1)
+-- number of different type variables
+∙ ∀a ∀b,a ∀A ∀A,a : ℕ × ℕ
+∙ = (0 ,, 0)
+∀a = (0 ,, 1)
+∀b,a = (0 ,, 2)
+∀A = (1 ,, 0)
+∀A,a = (1 ,, 1)
 
- -- names for type variables of kind ⋆
- A : ∀{n⋆ n♯} → suc n⋆ / n♯ ⊢⋆
- A = ` Z
+-- names for type variables of kind ⋆
+A : ∀{n⋆ n♯} → suc n⋆ / n♯ ⊢⋆
+A = ` Z
 
- B : ∀{n⋆ n♯} → suc (suc n⋆) / n♯ ⊢⋆
- B = ` (S Z)
+B : ∀{n⋆ n♯} → suc (suc n⋆) / n♯ ⊢⋆
+B = ` (S Z)
 
- -- names for type variables of kind ♯
- a : ∀{n♯} → suc n♯ ⊢♯
- a = ` Z
+-- names for type variables of kind ♯
+a : ∀{n♯} → suc n♯ ⊢♯
+a = ` Z
 
- b : ∀{n♯} → suc (suc n♯) ⊢♯
- b = ` (S Z)
+b : ∀{n♯} → suc (suc n♯) ⊢♯
+b = ` (S Z)
 
- pair : ∀{n⋆ n♯} → n♯ ⊢♯ → n♯ ⊢♯ → n⋆ / n♯ ⊢⋆
- pair a b = (bpair a b) ↑
- 
- list : ∀{n⋆ n♯} → n♯ ⊢♯ → n⋆ / n♯ ⊢⋆
- list a = (blist a) ↑
- ```
+pair : ∀{n⋆ n♯} → n♯ ⊢♯ → n♯ ⊢♯ → n⋆ / n♯ ⊢⋆
+pair a b = (bpair a b) ↑
+
+list : ∀{n⋆ n♯} → n♯ ⊢♯ → n⋆ / n♯ ⊢⋆
+list a = (blist a) ↑
+```
 
- ###Operators for constructing signatures
+### Operators for constructing signatures
 
- The following operators are used to express signatures in a familiar way,
- but ultimately, they construct a Sig 
+The following operators are used to express signatures in a familiar way,
+but ultimately, they construct a Sig 
 
- An expression 
-   n⋆×n♯ [ t₁ , t₂ , t₃ ]⟶ tᵣ
- 
- is actually parsed as
-   (((n⋆×n♯ [ t₁) , t₂) , t₃) ]⟶ tᵣ
- 
- and constructs a signature
-
- sig n⋆ n♯ (t₃ ∷ t₂ ∷ t₁) tᵣ
-
- ```
- ArgSet : Set
- ArgSet = Σ (ℕ × ℕ) (λ { (n⋆ ,, n♯) → Args n⋆ n♯}) 
-
- ArgTy : ArgSet → Set
- ArgTy ((n⋆ ,, n♯) ,, _) = n⋆ / n♯ ⊢⋆ 
-
- infix 12 _[_
- _[_ : (nn : ℕ × ℕ) → proj₁ nn / proj₂ nn ⊢⋆ → ArgSet
- _[_ (n⋆ ,, n♯) x = (n⋆ ,, n♯) ,, [ x ] 
-
- infixl 10 _,_
- _,_ : (p : ArgSet) → ArgTy p → ArgSet
- _,_ ((n⋆ ,, n♯) ,, args) arg = (n⋆ ,, n♯) ,, arg ∷⁺ args
-
- infix 8 _]⟶_
- _]⟶_ : (p : ArgSet) → ArgTy p → Sig
- _]⟶_ ((n⋆ ,, n♯) ,, as) res = sig n⋆ n♯ as res
- ```
-
- The signature of each builtin
-
- ```
- signature : Builtin → Sig
- signature addInteger = ∙ [ integer ↑ , integer ↑ ]⟶ integer ↑ 
- signature subtractInteger = ∙ [ integer ↑ , integer ↑ ]⟶ integer ↑
- signature multiplyInteger = ∙ [ integer ↑ , integer ↑ ]⟶ integer ↑
- signature divideInteger = ∙ [ integer ↑ , integer ↑ ]⟶ integer ↑
- signature quotientInteger = ∙ [ integer ↑ , integer ↑ ]⟶ integer ↑
- signature remainderInteger = ∙ [ integer ↑ , integer ↑ ]⟶ integer ↑
- signature modInteger = ∙ [ integer ↑ , integer ↑ ]⟶ integer ↑
- signature equalsInteger = ∙ [ integer ↑ , integer ↑ ]⟶ bool ↑
- signature lessThanInteger = ∙ [ integer ↑ , integer ↑ ]⟶ bool ↑
- signature lessThanEqualsInteger = ∙ [ integer ↑ , integer ↑ ]⟶ bool ↑
- signature appendByteString = ∙ [ bytestring ↑ , bytestring ↑ ]⟶ bytestring ↑
- signature consByteString = ∙ [ integer ↑ , bytestring ↑ ]⟶ bytestring ↑
- signature sliceByteString = ∙ [ integer ↑ , integer ↑ , bytestring ↑ ]⟶ bytestring ↑
- signature lengthOfByteString = ∙ [ bytestring ↑ ]⟶ integer ↑
- signature indexByteString = ∙ [ bytestring ↑ , integer ↑ ]⟶ integer ↑
- signature equalsByteString = ∙ [ bytestring ↑ , bytestring ↑ ]⟶ bool ↑
- signature lessThanByteString = ∙ [ bytestring ↑ , bytestring ↑ ]⟶ bool ↑
- signature lessThanEqualsByteString = ∙ [ bytestring ↑ , bytestring ↑ ]⟶ bool ↑
- signature sha2-256 = ∙ [ bytestring ↑ ]⟶ bytestring ↑
- signature sha3-256 = ∙ [ bytestring ↑ ]⟶ bytestring ↑
- signature blake2b-224 = ∙ [ bytestring ↑ ]⟶ bytestring ↑
- signature blake2b-256 = ∙ [ bytestring ↑ ]⟶ bytestring ↑
- signature keccak-256 = ∙ [ bytestring ↑ ]⟶ bytestring ↑
- signature verifyEd25519Signature = ∙ [ bytestring ↑ , bytestring ↑ , bytestring ↑ ]⟶ bool ↑
- signature verifyEcdsaSecp256k1Signature = ∙ [ bytestring ↑ , bytestring ↑ , bytestring ↑ ]⟶ bool ↑
- signature verifySchnorrSecp256k1Signature = ∙ [ bytestring ↑ , bytestring ↑ , bytestring ↑ ]⟶ bool ↑
- signature appendString = ∙ [ string ↑ , string ↑ ]⟶ string ↑
- signature equalsString = ∙ [ string ↑ , string ↑ ]⟶ bool ↑
- signature encodeUtf8 = ∙ [ string ↑ ]⟶ bytestring ↑
- signature decodeUtf8 = ∙ [ bytestring ↑ ]⟶ string ↑
- signature ifThenElse = ∀A [ bool ↑ , A , A ]⟶ A
- signature chooseUnit = ∀A [ A , unit ↑ ]⟶ A
- signature trace = ∀A [ string ↑ , A ]⟶ A
- signature fstPair = ∀b,a [ pair b a ]⟶ b ↑
- signature sndPair = ∀b,a [ pair b a ]⟶ a ↑
- signature chooseList = ∀A,a [ list a , A , A ]⟶ A
- signature mkCons = ∀a [ a ↑ , list a ]⟶ list a
- signature headList = ∀a [ list a ]⟶ a ↑
- signature tailList = ∀a [ list a ]⟶ list a
- signature nullList = ∀a [ list a ]⟶ bool ↑
- signature chooseData = ∀A [ pdata ↑ , A , A , A , A , A ]⟶ A
- signature constrData = ∙ [ integer ↑ , list pdata ]⟶ pdata ↑
- signature mapData = ∙ [ list (bpair pdata pdata) ]⟶ pdata ↑
- signature listData = ∙ [ list pdata ]⟶ pdata ↑
- signature iData = ∙ [ integer ↑ ]⟶ pdata ↑
- signature bData = ∙ [ bytestring ↑ ]⟶ pdata ↑
- signature unConstrData = ∙ [ pdata ↑ ]⟶ pair integer (blist pdata)
- signature unMapData = ∙ [ pdata ↑ ]⟶ list (bpair pdata pdata)
- signature unListData = ∙ [ pdata ↑ ]⟶ list pdata 
- signature unIData = ∙ [ pdata ↑ ]⟶ integer ↑
- signature unBData = ∙ [ pdata ↑ ]⟶ bytestring ↑
- signature equalsData = ∙ [ pdata ↑ , pdata ↑ ]⟶ bool ↑
- signature serialiseData = ∙ [ pdata ↑ ]⟶ bytestring ↑
- signature mkPairData = ∙ [ pdata ↑ , pdata ↑ ]⟶ pair pdata pdata
- signature mkNilData = ∙ [ unit ↑ ]⟶ list pdata
- signature mkNilPairData = ∙ [ unit ↑ ]⟶ list (bpair pdata pdata)
- signature bls12-381-G1-add = ∙ [ bls12-381-g1-element ↑ , bls12-381-g1-element ↑ ]⟶ bls12-381-g1-element ↑
- signature bls12-381-G1-neg = ∙ [ bls12-381-g1-element ↑ ]⟶ bls12-381-g1-element ↑
- signature bls12-381-G1-scalarMul = ∙ [ integer ↑ , bls12-381-g1-element ↑ ]⟶ bls12-381-g1-element ↑
- signature bls12-381-G1-equal = ∙ [ bls12-381-g1-element ↑ , bls12-381-g1-element ↑ ]⟶ bool ↑
- signature bls12-381-G1-hashToGroup = ∙ [ bytestring ↑ , bytestring ↑ ]⟶ bls12-381-g1-element ↑
- signature bls12-381-G1-compress = ∙ [ bls12-381-g1-element ↑ ]⟶ bytestring ↑
- signature bls12-381-G1-uncompress = ∙ [ bytestring ↑ ]⟶ bls12-381-g1-element ↑
- signature bls12-381-G2-add = ∙ [ bls12-381-g2-element ↑ , bls12-381-g2-element ↑ ]⟶ bls12-381-g2-element ↑
- signature bls12-381-G2-neg = ∙ [ bls12-381-g2-element ↑ ]⟶ bls12-381-g2-element ↑
- signature bls12-381-G2-scalarMul = ∙ [ integer ↑ , bls12-381-g2-element ↑ ]⟶ bls12-381-g2-element ↑
- signature bls12-381-G2-equal = ∙ [ bls12-381-g2-element ↑ , bls12-381-g2-element ↑ ]⟶ bool ↑
- signature bls12-381-G2-hashToGroup = ∙ [ bytestring ↑ , bytestring ↑ ]⟶ bls12-381-g2-element ↑
- signature bls12-381-G2-compress = ∙ [ bls12-381-g2-element ↑ ]⟶ bytestring ↑
- signature bls12-381-G2-uncompress = ∙ [ bytestring ↑ ]⟶ bls12-381-g2-element ↑
- signature bls12-381-millerLoop = ∙ [ bls12-381-g1-element ↑ , bls12-381-g2-element ↑ ]⟶ bls12-381-mlresult ↑
- signature bls12-381-mulMlResult = ∙ [ bls12-381-mlresult ↑ , bls12-381-mlresult ↑ ]⟶ bls12-381-mlresult ↑
- signature bls12-381-finalVerify = ∙ [ bls12-381-mlresult ↑ , bls12-381-mlresult ↑ ]⟶ bool ↑
- signature byteStringToInteger = ∙ [ bool ↑ , bytestring ↑ ]⟶ integer ↑
- signature integerToByteString = ∙ [ bool ↑ , integer ↑ , integer ↑ ]⟶ bytestring ↑
+An expression 
+ n⋆×n♯ [ t₁ , t₂ , t₃ ]⟶ tᵣ
+
+is actually parsed as
+ (((n⋆×n♯ [ t₁) , t₂) , t₃) ]⟶ tᵣ
+
+and constructs a signature
+
+sig n⋆ n♯ (t₃ ∷ t₂ ∷ t₁) tᵣ
+
+```
+ArgSet : Set
+ArgSet = Σ (ℕ × ℕ) (λ { (n⋆ ,, n♯) → Args n⋆ n♯}) 
+
+ArgTy : ArgSet → Set
+ArgTy ((n⋆ ,, n♯) ,, _) = n⋆ / n♯ ⊢⋆ 
+
+infix 12 _[_
+_[_ : (nn : ℕ × ℕ) → proj₁ nn / proj₂ nn ⊢⋆ → ArgSet
+_[_ (n⋆ ,, n♯) x = (n⋆ ,, n♯) ,, [ x ] 
+
+infixl 10 _,_
+_,_ : (p : ArgSet) → ArgTy p → ArgSet
+_,_ ((n⋆ ,, n♯) ,, args) arg = (n⋆ ,, n♯) ,, arg ∷⁺ args
+
+infix 8 _]⟶_
+_]⟶_ : (p : ArgSet) → ArgTy p → Sig
+_]⟶_ ((n⋆ ,, n♯) ,, as) res = sig n⋆ n♯ as res
+```
+
+The signature of each builtin
+
+```
+signature : Builtin → Sig
+signature addInteger = ∙ [ integer ↑ , integer ↑ ]⟶ integer ↑ 
+signature subtractInteger = ∙ [ integer ↑ , integer ↑ ]⟶ integer ↑
+signature multiplyInteger = ∙ [ integer ↑ , integer ↑ ]⟶ integer ↑
+signature divideInteger = ∙ [ integer ↑ , integer ↑ ]⟶ integer ↑
+signature quotientInteger = ∙ [ integer ↑ , integer ↑ ]⟶ integer ↑
+signature remainderInteger = ∙ [ integer ↑ , integer ↑ ]⟶ integer ↑
+signature modInteger = ∙ [ integer ↑ , integer ↑ ]⟶ integer ↑
+signature equalsInteger = ∙ [ integer ↑ , integer ↑ ]⟶ bool ↑
+signature lessThanInteger = ∙ [ integer ↑ , integer ↑ ]⟶ bool ↑
+signature lessThanEqualsInteger = ∙ [ integer ↑ , integer ↑ ]⟶ bool ↑
+signature appendByteString = ∙ [ bytestring ↑ , bytestring ↑ ]⟶ bytestring ↑
+signature consByteString = ∙ [ integer ↑ , bytestring ↑ ]⟶ bytestring ↑
+signature sliceByteString = ∙ [ integer ↑ , integer ↑ , bytestring ↑ ]⟶ bytestring ↑
+signature lengthOfByteString = ∙ [ bytestring ↑ ]⟶ integer ↑
+signature indexByteString = ∙ [ bytestring ↑ , integer ↑ ]⟶ integer ↑
+signature equalsByteString = ∙ [ bytestring ↑ , bytestring ↑ ]⟶ bool ↑
+signature lessThanByteString = ∙ [ bytestring ↑ , bytestring ↑ ]⟶ bool ↑
+signature lessThanEqualsByteString = ∙ [ bytestring ↑ , bytestring ↑ ]⟶ bool ↑
+signature sha2-256 = ∙ [ bytestring ↑ ]⟶ bytestring ↑
+signature sha3-256 = ∙ [ bytestring ↑ ]⟶ bytestring ↑
+signature blake2b-224 = ∙ [ bytestring ↑ ]⟶ bytestring ↑
+signature blake2b-256 = ∙ [ bytestring ↑ ]⟶ bytestring ↑
+signature keccak-256 = ∙ [ bytestring ↑ ]⟶ bytestring ↑
+signature verifyEd25519Signature = ∙ [ bytestring ↑ , bytestring ↑ , bytestring ↑ ]⟶ bool ↑
+signature verifyEcdsaSecp256k1Signature = ∙ [ bytestring ↑ , bytestring ↑ , bytestring ↑ ]⟶ bool ↑
+signature verifySchnorrSecp256k1Signature = ∙ [ bytestring ↑ , bytestring ↑ , bytestring ↑ ]⟶ bool ↑
+signature appendString = ∙ [ string ↑ , string ↑ ]⟶ string ↑
+signature equalsString = ∙ [ string ↑ , string ↑ ]⟶ bool ↑
+signature encodeUtf8 = ∙ [ string ↑ ]⟶ bytestring ↑
+signature decodeUtf8 = ∙ [ bytestring ↑ ]⟶ string ↑
+signature ifThenElse = ∀A [ bool ↑ , A , A ]⟶ A
+signature chooseUnit = ∀A [ A , unit ↑ ]⟶ A
+signature trace = ∀A [ string ↑ , A ]⟶ A
+signature fstPair = ∀b,a [ pair b a ]⟶ b ↑
+signature sndPair = ∀b,a [ pair b a ]⟶ a ↑
+signature chooseList = ∀A,a [ list a , A , A ]⟶ A
+signature mkCons = ∀a [ a ↑ , list a ]⟶ list a
+signature headList = ∀a [ list a ]⟶ a ↑
+signature tailList = ∀a [ list a ]⟶ list a
+signature nullList = ∀a [ list a ]⟶ bool ↑
+signature chooseData = ∀A [ pdata ↑ , A , A , A , A , A ]⟶ A
+signature constrData = ∙ [ integer ↑ , list pdata ]⟶ pdata ↑
+signature mapData = ∙ [ list (bpair pdata pdata) ]⟶ pdata ↑
+signature listData = ∙ [ list pdata ]⟶ pdata ↑
+signature iData = ∙ [ integer ↑ ]⟶ pdata ↑
+signature bData = ∙ [ bytestring ↑ ]⟶ pdata ↑
+signature unConstrData = ∙ [ pdata ↑ ]⟶ pair integer (blist pdata)
+signature unMapData = ∙ [ pdata ↑ ]⟶ list (bpair pdata pdata)
+signature unListData = ∙ [ pdata ↑ ]⟶ list pdata 
+signature unIData = ∙ [ pdata ↑ ]⟶ integer ↑
+signature unBData = ∙ [ pdata ↑ ]⟶ bytestring ↑
+signature equalsData = ∙ [ pdata ↑ , pdata ↑ ]⟶ bool ↑
+signature serialiseData = ∙ [ pdata ↑ ]⟶ bytestring ↑
+signature mkPairData = ∙ [ pdata ↑ , pdata ↑ ]⟶ pair pdata pdata
+signature mkNilData = ∙ [ unit ↑ ]⟶ list pdata
+signature mkNilPairData = ∙ [ unit ↑ ]⟶ list (bpair pdata pdata)
+signature bls12-381-G1-add = ∙ [ bls12-381-g1-element ↑ , bls12-381-g1-element ↑ ]⟶ bls12-381-g1-element ↑
+signature bls12-381-G1-neg = ∙ [ bls12-381-g1-element ↑ ]⟶ bls12-381-g1-element ↑
+signature bls12-381-G1-scalarMul = ∙ [ integer ↑ , bls12-381-g1-element ↑ ]⟶ bls12-381-g1-element ↑
+signature bls12-381-G1-equal = ∙ [ bls12-381-g1-element ↑ , bls12-381-g1-element ↑ ]⟶ bool ↑
+signature bls12-381-G1-hashToGroup = ∙ [ bytestring ↑ , bytestring ↑ ]⟶ bls12-381-g1-element ↑
+signature bls12-381-G1-compress = ∙ [ bls12-381-g1-element ↑ ]⟶ bytestring ↑
+signature bls12-381-G1-uncompress = ∙ [ bytestring ↑ ]⟶ bls12-381-g1-element ↑
+signature bls12-381-G2-add = ∙ [ bls12-381-g2-element ↑ , bls12-381-g2-element ↑ ]⟶ bls12-381-g2-element ↑
+signature bls12-381-G2-neg = ∙ [ bls12-381-g2-element ↑ ]⟶ bls12-381-g2-element ↑
+signature bls12-381-G2-scalarMul = ∙ [ integer ↑ , bls12-381-g2-element ↑ ]⟶ bls12-381-g2-element ↑
+signature bls12-381-G2-equal = ∙ [ bls12-381-g2-element ↑ , bls12-381-g2-element ↑ ]⟶ bool ↑
+signature bls12-381-G2-hashToGroup = ∙ [ bytestring ↑ , bytestring ↑ ]⟶ bls12-381-g2-element ↑
+signature bls12-381-G2-compress = ∙ [ bls12-381-g2-element ↑ ]⟶ bytestring ↑
+signature bls12-381-G2-uncompress = ∙ [ bytestring ↑ ]⟶ bls12-381-g2-element ↑
+signature bls12-381-millerLoop = ∙ [ bls12-381-g1-element ↑ , bls12-381-g2-element ↑ ]⟶ bls12-381-mlresult ↑
+signature bls12-381-mulMlResult = ∙ [ bls12-381-mlresult ↑ , bls12-381-mlresult ↑ ]⟶ bls12-381-mlresult ↑
+signature bls12-381-finalVerify = ∙ [ bls12-381-mlresult ↑ , bls12-381-mlresult ↑ ]⟶ bool ↑
+signature byteStringToInteger = ∙ [ bool ↑ , bytestring ↑ ]⟶ integer ↑
+signature integerToByteString = ∙ [ bool ↑ , integer ↑ , integer ↑ ]⟶ bytestring ↑
 
 open SugaredSignature using (signature) public
 

diff --git a/plutus-metatheory/src/Cost.lagda.md b/plutus-metatheory/src/Cost.lagda.md
@@ -266,4 +266,4 @@ tallyingReport (mp , budget) =
  if 1e6 ≤ᵇ t then (printf "%f μs" (t ÷ 1e6)) else
  if 1e3 ≤ᵇ t then (printf "%f ns" (t ÷ 1e3)) else
  printf "%f ps" t
- ```
+```
diff --git a/plutus-metatheory/src/Utils.lagda.md b/plutus-metatheory/src/Utils.lagda.md
@@ -66,7 +66,8 @@ cong₃ f refl refl refl = refl
  (P : A → Set p) {x y} (p q : x ≡ y) z →
  subst P p z ≡ subst P q z
 ≡-subst-removable P refl refl z = refl 
- ```
+```
+
 ## Natural Sum Type
 
 The type `n ∔ n' ≡ m` takes two naturals `n` and `n'` such that they sum to m.

diff --git a/plutus-metatheory/src/Utils/List.lagda.md b/plutus-metatheory/src/Utils/List.lagda.md
@@ -320,7 +320,7 @@ proj-IIBwd b bs fs xs with bsplitI bs (b ∷ fs) xs
 
  Index for IIList zippers
 
- ```
+```
 data _≣I_<>>_ {A : Set}{B : A → Set}{tot}(itot : IList B tot) : 
  ∀{bs ts} 
  → IBwd B bs