diff --git a/plutus-metatheory/src/Algorithmic.lagda b/plutus-metatheory/src/Algorithmic.lagda index f57451d27a8..06f9fece106 100644 --- a/plutus-metatheory/src/Algorithmic.lagda +++ b/plutus-metatheory/src/Algorithmic.lagda @@ -91,85 +91,85 @@ A term is indexed over by its context and type. A term is a variable, an abstraction, an application, a type abstraction, or a type application. \begin{code} -ISIG : Builtin → Σ Ctx⋆ λ Φ → Ctx Φ × Φ ⊢Nf⋆ * -ISIG ifThenElse = _ ,, ∅ ,⋆ * , con bool , ne (` Z) , ne (` Z) ,, ne (` Z) -ISIG addInteger = ∅ ,, ∅ , con integer , con integer ,, con integer -ISIG subtractInteger = ∅ ,, ∅ , con integer , con integer ,, con integer -ISIG multiplyInteger = ∅ ,, ∅ , con integer , con integer ,, con integer -ISIG divideInteger = ∅ ,, ∅ , con integer , con integer ,, con integer -ISIG quotientInteger = ∅ ,, ∅ , con integer , con integer ,, con integer -ISIG remainderInteger = ∅ ,, ∅ , con integer , con integer ,, con integer -ISIG modInteger = ∅ ,, ∅ , con integer , con integer ,, con integer -ISIG lessThanInteger = ∅ ,, ∅ , con integer , con integer ,, con bool -ISIG lessThanEqualsInteger = ∅ ,, ∅ , con integer , con integer ,, con bool -ISIG equalsInteger = ∅ ,, ∅ , con integer , con integer ,, con bool -ISIG appendByteString = ∅ ,, ∅ , con bytestring , con bytestring ,, con bytestring -ISIG lessThanByteString = ∅ ,, ∅ , con bytestring , con bytestring ,, con bool -ISIG lessThanEqualsByteString = ∅ ,, ∅ , con bytestring , con bytestring ,, con bool -ISIG sha2-256 = ∅ ,, ∅ , con bytestring ,, con bytestring -ISIG sha3-256 = ∅ ,, ∅ , con bytestring ,, con bytestring -ISIG verifySignature = ∅ ,, ∅ , con bytestring , con bytestring , con bytestring ,, con bool -ISIG equalsByteString = ∅ ,, ∅ , con bytestring , con bytestring ,, con bool -ISIG appendString = ∅ ,, ∅ , con string , con string ,, con string -ISIG trace = _ ,, ∅ ,⋆ * , con string , ne (` Z) ,, ne (` Z) -ISIG equalsString = ∅ ,, ∅ , con string , con string ,, con bool -ISIG encodeUtf8 = ∅ ,, ∅ , con string ,, con bytestring -ISIG decodeUtf8 = ∅ ,, ∅ , con bytestring ,, con string -ISIG fstPair = +sig : Builtin → Σ Ctx⋆ λ Φ → Ctx Φ × Φ ⊢Nf⋆ * +sig ifThenElse = _ ,, ∅ ,⋆ * , con bool , ne (` Z) , ne (` Z) ,, ne (` Z) +sig addInteger = _ ,, ∅ , con integer , con integer ,, con integer +sig subtractInteger = _ ,, ∅ , con integer , con integer ,, con integer +sig multiplyInteger = _ ,, ∅ , con integer , con integer ,, con integer +sig divideInteger = _ ,, ∅ , con integer , con integer ,, con integer +sig quotientInteger = _ ,, ∅ , con integer , con integer ,, con integer +sig remainderInteger = _ ,, ∅ , con integer , con integer ,, con integer +sig modInteger = _ ,, ∅ , con integer , con integer ,, con integer +sig lessThanInteger = _ ,, ∅ , con integer , con integer ,, con bool +sig lessThanEqualsInteger = _ ,, ∅ , con integer , con integer ,, con bool +sig equalsInteger = _ ,, ∅ , con integer , con integer ,, con bool +sig appendByteString = _ ,, ∅ , con bytestring , con bytestring ,, con bytestring +sig lessThanByteString = _ ,, ∅ , con bytestring , con bytestring ,, con bool +sig lessThanEqualsByteString = _ ,, ∅ , con bytestring , con bytestring ,, con bool +sig sha2-256 = _ ,, ∅ , con bytestring ,, con bytestring +sig sha3-256 = _ ,, ∅ , con bytestring ,, con bytestring +sig verifySignature = _ ,, ∅ , con bytestring , con bytestring , con bytestring ,, con bool +sig equalsByteString = _ ,, ∅ , con bytestring , con bytestring ,, con bool +sig appendString = _ ,, ∅ , con string , con string ,, con string +sig trace = _ ,, ∅ ,⋆ * , con string , ne (` Z) ,, ne (` Z) +sig equalsString = _ ,, ∅ , con string , con string ,, con bool +sig encodeUtf8 = _ ,, ∅ , con string ,, con bytestring +sig decodeUtf8 = _ ,, ∅ , con bytestring ,, con string +sig fstPair = _ ,, ∅ ,⋆ * ,⋆ * , con (pair (ne (` (S Z))) (ne (` Z))) ,, ne (` (S Z)) -ISIG sndPair = +sig sndPair = _ ,, ∅ ,⋆ * ,⋆ * , con (pair (ne (` (S Z))) (ne (` Z))) ,, ne (` Z) -ISIG nullList = _ ,, ∅ ,⋆ * , con (list (ne (` Z))) ,, con bool -ISIG headList = _ ,, ∅ ,⋆ * , con (list (ne (` Z))) ,, ne (` Z) -ISIG tailList = _ ,, ∅ ,⋆ * , con (list (ne (` Z))) ,, con (list (ne (` Z))) -ISIG chooseList = +sig nullList = _ ,, ∅ ,⋆ * , con (list (ne (` Z))) ,, con bool +sig headList = _ ,, ∅ ,⋆ * , con (list (ne (` Z))) ,, ne (` Z) +sig tailList = _ ,, ∅ ,⋆ * , con (list (ne (` Z))) ,, con (list (ne (` Z))) +sig chooseList = _ ,, ∅ ,⋆ * ,⋆ * , ne (` (S Z)) , ne (` (S Z)) , con (list (ne (` Z))) ,, ne (` (S Z)) -ISIG constrData = _ ,, ∅ , con integer , con (list (con Data)) ,, con Data -ISIG mapData = _ ,, ∅ , con (pair (con Data) (con Data)) ,, con Data -ISIG listData = _ ,, ∅ , con (list (con Data)) ,, con Data -ISIG iData = _ ,, ∅ , con integer ,, con Data -ISIG bData = _ ,, ∅ , con bytestring ,, con Data -ISIG unConstrData = +sig constrData = _ ,, ∅ , con integer , con (list (con Data)) ,, con Data +sig mapData = _ ,, ∅ , con (pair (con Data) (con Data)) ,, con Data +sig listData = _ ,, ∅ , con (list (con Data)) ,, con Data +sig iData = _ ,, ∅ , con integer ,, con Data +sig bData = _ ,, ∅ , con bytestring ,, con Data +sig unConstrData = _ ,, ∅ , con Data ,, con (pair (con integer) (con (list (con Data)))) -ISIG unMapData = _ ,, ∅ , con Data ,, con (pair (con Data) (con Data)) -ISIG unListData = _ ,, ∅ , con Data ,, con (list (con Data)) -ISIG unIData = _ ,, ∅ , con Data ,, con integer -ISIG unBData = _ ,, ∅ , con Data ,, con bytestring -ISIG equalsData = _ ,, ∅ , con Data , con Data ,, con bool -ISIG chooseData = +sig unMapData = _ ,, ∅ , con Data ,, con (pair (con Data) (con Data)) +sig unListData = _ ,, ∅ , con Data ,, con (list (con Data)) +sig unIData = _ ,, ∅ , con Data ,, con integer +sig unBData = _ ,, ∅ , con Data ,, con bytestring +sig equalsData = _ ,, ∅ , con Data , con Data ,, con bool +sig chooseData = _ ,, ∅ ,⋆ * , ne (` Z) , ne (` Z) , ne (` Z) , ne (` Z) , ne (` Z) , con Data ,, ne (` Z) -ISIG chooseUnit = _ ,, ∅ ,⋆ * , ne (` Z) , con unit ,, ne (` Z) -ISIG mkPairData = +sig chooseUnit = _ ,, ∅ ,⋆ * , ne (` Z) , con unit ,, ne (` Z) +sig mkPairData = _ ,, ∅ , con Data , con Data ,, con (pair (con Data) (con Data)) -ISIG mkNilData = _ ,, ∅ , con unit ,, con (list (con Data)) -ISIG mkNilPairData = _ ,, ∅ , con unit ,, con (list (con (pair (con Data) (con Data)))) -ISIG mkCons = +sig mkNilData = _ ,, ∅ , con unit ,, con (list (con Data)) +sig mkNilPairData = _ ,, ∅ , con unit ,, con (list (con (pair (con Data) (con Data)))) +sig mkCons = _ ,, ∅ , con Data , con (list (con Data)) ,, con (list (con Data)) -ISIG consByteString = _ ,, ∅ , con integer , con bytestring ,, con bytestring -ISIG sliceByteString = +sig consByteString = _ ,, ∅ , con integer , con bytestring ,, con bytestring +sig sliceByteString = _ ,, ∅ , con integer , con integer , con bytestring ,, con bytestring -ISIG lengthOfByteString = _ ,, ∅ , con bytestring ,, con integer -ISIG indexByteString = _ ,, ∅ , con bytestring , con integer ,, con integer -ISIG blake2b-256 = _ ,, ∅ , con bytestring ,, con bytestring +sig lengthOfByteString = _ ,, ∅ , con bytestring ,, con integer +sig indexByteString = _ ,, ∅ , con bytestring , con integer ,, con integer +sig blake2b-256 = _ ,, ∅ , con bytestring ,, con bytestring -isig2type : (Φ : Ctx⋆) → Ctx Φ → Φ ⊢Nf⋆ * → ∅ ⊢Nf⋆ * -isig2type .∅ ∅ C = C -isig2type (Φ ,⋆ J) (Γ ,⋆ J) C = isig2type Φ Γ (Π C) -isig2type Φ (Γ , A) C = isig2type Φ Γ (A ⇒ C) +sig2type : (Φ : Ctx⋆) → Ctx Φ → Φ ⊢Nf⋆ * → ∅ ⊢Nf⋆ * +sig2type .∅ ∅ C = C +sig2type (Φ ,⋆ J) (Γ ,⋆ J) C = sig2type Φ Γ (Π C) +sig2type Φ (Γ , A) C = sig2type Φ Γ (A ⇒ C) -itype : ∀{Φ} → Builtin → Φ ⊢Nf⋆ * -itype b = let Φ ,, Γ ,, C = ISIG b in subNf (λ()) (isig2type Φ Γ C) +btype : ∀{Φ} → Builtin → Φ ⊢Nf⋆ * +btype b = let Φ ,, Γ ,, C = sig b in subNf (λ()) (sig2type Φ Γ C) -postulate itype-ren : ∀{Φ Ψ} b (ρ : ⋆.Ren Φ Ψ) → itype b ≡ renNf ρ (itype b) -postulate itype-sub : ∀{Φ Ψ} b (ρ : SubNf Φ Ψ) → itype b ≡ subNf ρ (itype b) +postulate btype-ren : ∀{Φ Ψ} b (ρ : ⋆.Ren Φ Ψ) → btype b ≡ renNf ρ (btype b) +postulate btype-sub : ∀{Φ Ψ} b (ρ : SubNf Φ Ψ) → btype b ≡ subNf ρ (btype b) infixl 7 _·⋆_ @@ -221,7 +221,7 @@ data _⊢_ {Φ} (Γ : Ctx Φ) : Φ ⊢Nf⋆ * → Set where ------------------- → Γ ⊢ con tcn - ibuiltin : (b : Builtin) → Γ ⊢ itype b + builtin : (b : Builtin) → Γ ⊢ btype b error : (A : Φ ⊢Nf⋆ *) → Γ ⊢ A \end{code} @@ -265,5 +265,5 @@ ctx2bwdarity (Γ ,⋆ J) = ctx2bwdarity Γ :< Type ctx2bwdarity (Γ , A) = ctx2bwdarity Γ :< Term arity : Builtin → Arity -arity b = ctx2bwdarity (proj₁ (proj₂ (ISIG b))) <>> [] +arity b = ctx2bwdarity (proj₁ (proj₂ (sig b))) <>> [] \end{code} diff --git a/plutus-metatheory/src/Algorithmic/CC.lagda.md b/plutus-metatheory/src/Algorithmic/CC.lagda.md index e083241a940..274f1cf7318 100644 --- a/plutus-metatheory/src/Algorithmic/CC.lagda.md +++ b/plutus-metatheory/src/Algorithmic/CC.lagda.md @@ -188,7 +188,7 @@ stepT (E ▻ (M ·⋆ A)) = extEC E (-·⋆ A) ▻ M stepT (E ▻ wrap A B M) = extEC E wrap- ▻ M stepT (E ▻ unwrap M) = extEC E unwrap- ▻ M stepT (E ▻ con c) = E ◅ V-con c -stepT (E ▻ ibuiltin b) = E ◅ ival b +stepT (E ▻ builtin b) = E ◅ ival b stepT (E ▻ error A) = ◆ A stepT (E ◅ V) = stepV V (dissect E) stepT (□ V) = □ V @@ -1045,8 +1045,8 @@ thm1b (wrap A B M) M' E p N V (step* refl q) = thm1b (unwrap M) M' E p N V (step* refl q) = thm1b M _ (extEC E unwrap-) (trans p (sym (extEC-[]ᴱ E unwrap- M))) N V q thm1b (con c) M' E p N V (step* refl q) = thm1bV (con c) (V-con c) M' E p N V q -thm1b (ibuiltin b) M' E p N V (step* refl q) = - thm1bV (ibuiltin b) (ival b) M' E p N V q +thm1b (builtin b) M' E p N V (step* refl q) = + thm1bV (builtin b) (ival b) M' E p N V q thm1b (error _) M' E p N V (step* refl q) = ⊥-elim (diamond2box N V q) thm1bV M W M' E p N V (step* x q) with dissect E | inspect dissect E diff --git a/plutus-metatheory/src/Algorithmic/CEKV.lagda.md b/plutus-metatheory/src/Algorithmic/CEKV.lagda.md index 73351c2602f..b1638261a8c 100644 --- a/plutus-metatheory/src/Algorithmic/CEKV.lagda.md +++ b/plutus-metatheory/src/Algorithmic/CEKV.lagda.md @@ -71,7 +71,7 @@ data Value : (A : ∅ ⊢Nf⋆ *) → Set where → Value (Π B) data BAPP b where - base : BAPP b (start (arity b)) (itype b) + base : BAPP b (start (arity b)) (btype b) app : ∀{A B}{az as} → (p : az <>> (Term ∷ as) ∈ arity b) → BAPP b p (A ⇒ B) @@ -125,7 +125,7 @@ dischargeBody⋆ {A = A} M ρ = conv⊢ (sub (extsNf (ne ∘ `)) (exts⋆ (ne ∘ `) (env2ren ρ)) M) dischargeB : ∀{b A}{az}{as}{p : az <>> as ∈ arity b} → BAPP b p A → ∅ ⊢ A -dischargeB {b = b} base = ibuiltin b +dischargeB {b = b} base = builtin b dischargeB (app p bt vu) = dischargeB bt · discharge vu dischargeB (app⋆ p bt refl) = dischargeB bt ·⋆ _ @@ -816,7 +816,7 @@ data State (T : ∅ ⊢Nf⋆ *) : Set where -ival : ∀ b → Value (itype b) +ival : ∀ b → Value (btype b) ival addInteger = V-I⇒ addInteger _ base ival subtractInteger = V-I⇒ subtractInteger _ base ival multiplyInteger = V-I⇒ multiplyInteger _ base @@ -878,7 +878,7 @@ step (s ; ρ ▻ (L ·⋆ A)) = (s , -·⋆ A) ; ρ ▻ L step (s ; ρ ▻ wrap A B L) = (s , wrap-) ; ρ ▻ L step (s ; ρ ▻ unwrap L) = (s , unwrap-) ; ρ ▻ L step (s ; ρ ▻ con c) = s ◅ V-con c -step (s ; ρ ▻ ibuiltin b) = s ◅ ival b +step (s ; ρ ▻ builtin b) = s ◅ ival b step (s ; ρ ▻ error A) = ◆ A step (ε ◅ V) = □ V step ((s , -· M ρ') ◅ V) = (s , V ·-) ; ρ' ▻ M @@ -973,7 +973,7 @@ cek2ckClos (L ·⋆ A) ρ = cek2ckClos L ρ ·⋆ A cek2ckClos (wrap A B L) ρ = wrap A B (cek2ckClos L ρ) cek2ckClos (unwrap L) ρ = unwrap (cek2ckClos L ρ) cek2ckClos (con c) ρ = con c -cek2ckClos (ibuiltin b) ρ = ibuiltin b +cek2ckClos (builtin b) ρ = builtin b cek2ckClos (error _) ρ = error _ cek2ckFrame : ∀{A B} → Frame A B → Red.Frame A B @@ -1046,7 +1046,7 @@ thm65a (s ; ρ ▻ (L ·⋆ A)) s' (step* refl q) = CK.step* refl (thm65a _ s' thm65a (s ; ρ ▻ wrap A B L) s' (step* refl q) = CK.step* refl (thm65a _ s' q) thm65a (s ; ρ ▻ unwrap L) s' (step* refl q) = CK.step* refl (thm65a _ s' q) thm65a (s ; ρ ▻ con c) s' (step* refl q) = CK.step* refl (thm65a _ s' q) -thm65a (s ; ρ ▻ ibuiltin b) s' (step* refl q) = CK.step* (ival-lem b) (thm65a _ s' q) +thm65a (s ; ρ ▻ builtin b) s' (step* refl q) = CK.step* (ival-lem b) (thm65a _ s' q) thm65a (s ; ρ ▻ error _) s' (step* refl q) = CK.step* refl (thm65a _ s' q) thm65a (ε ◅ V) s' (step* refl q) = CK.step* refl (thm65a _ s' q) thm65a ((s , -· L ρ) ◅ V) s' (step* refl q) = CK.step* refl (thm65a _ s' q) @@ -1104,7 +1104,7 @@ postulate cek2ckClos-unwraplem : ∀{K}{A}{B : ∅ ⊢Nf⋆ K}{L : ∅ ⊢ μ A postulate cek2ckClos-conlem : ∀{tc : TyCon ∅}(c : TermCon (con tc)){Γ}{M' : Γ ⊢ con tc}{ρ : Env Γ} → con c ≡ cek2ckClos M' ρ → M' ≡ con c ⊎ ∃ λ x → M' ≡ ` x × V-con c ≡ lookup x ρ -postulate cek2ckClos-ibuiltinlem : ∀{b}{Γ}{M' : Γ ⊢ itype b}{ρ : Env Γ} → ibuiltin b ≡ cek2ckClos M' ρ → (M' ≡ ibuiltin b × ∃ λ p → substEq Red.Value p (Red.ival b) ≡ cek2ckVal (ival b)) ⊎ ∃ λ x → M' ≡ ` x × ∃ λ (p : ibuiltin b ≡ discharge (lookup x ρ)) → substEq Red.Value p (Red.ival b) ≡ cek2ckVal (lookup x ρ) +postulate cek2ckClos-ibuiltinlem : ∀{b}{Γ}{M' : Γ ⊢ btype b}{ρ : Env Γ} → builtin b ≡ cek2ckClos M' ρ → (M' ≡ builtin b × ∃ λ p → substEq Red.Value p (Red.ival b) ≡ cek2ckVal (ival b)) ⊎ ∃ λ x → M' ≡ ` x × ∃ λ (p : builtin b ≡ discharge (lookup x ρ)) → substEq Red.Value p (Red.ival b) ≡ cek2ckVal (lookup x ρ) cek2ckStack-εlem : ∀{A}(s : Stack A A) → CK.ε ≡ cek2ckStack s → s ≡ ε cek2ckStack-εlem ε p = refl @@ -1196,11 +1196,11 @@ thm65b {M = con c}{s = s}{M' = M'}{ρ = ρ}{s' = s'} p q (CK.step* refl r) ... | inj₁ refl = _ ,, step* refl r' ,, x1 ,, x2 ... | inj₂ (var ,, refl ,, y2) = _ ,, step* (cong (s' ◅_) (sym y2)) r' ,, x1 ,, x2 -thm65b {M = ibuiltin b} {s = s}{M' = N}{ρ = ρ}{s' = s'} p q (CK.step* refl r) +thm65b {M = builtin b} {s = s}{M' = N}{ρ = ρ}{s' = s'} p q (CK.step* refl r) with cek2ckClos-ibuiltinlem {M' = N}{ρ = ρ} p -thm65b {M = ibuiltin b} {s = s}{M' = N}{ρ = ρ}{s' = s'} p q (CK.step* refl r) | inj₂ (x ,, refl ,, y2 ,, y3) with thm65bV y2 y3 q r +thm65b {M = builtin b} {s = s}{M' = N}{ρ = ρ}{s' = s'} p q (CK.step* refl r) | inj₂ (x ,, refl ,, y2 ,, y3) with thm65bV y2 y3 q r ... | V' ,, r' ,, y1 ,, y2 = V' ,, step* refl r' ,, y1 ,, y2 -thm65b {M = ibuiltin b} {s = s}{M' = N}{ρ = ρ}{s' = s'} p q (CK.step* refl r) | inj₁ (refl ,, x1 ,, x2) +thm65b {M = builtin b} {s = s}{M' = N}{ρ = ρ}{s' = s'} p q (CK.step* refl r) | inj₁ (refl ,, x1 ,, x2) with thm65bV x1 x2 q r ... | V' ,, r' ,, y1 ,, y2 = V' ,, step* refl r' ,, y1 ,, y2 diff --git a/plutus-metatheory/src/Algorithmic/CK.lagda.md b/plutus-metatheory/src/Algorithmic/CK.lagda.md index f24d11133cd..32fa79315a1 100644 --- a/plutus-metatheory/src/Algorithmic/CK.lagda.md +++ b/plutus-metatheory/src/Algorithmic/CK.lagda.md @@ -82,7 +82,7 @@ step ((s , (V-ƛ t ·-)) ◅ V) = s ▻ (t [ discharge V ]) step ((s , (-·⋆ A)) ◅ V-Λ t) = s ▻ (t [ A ]⋆) step ((s , wrap-) ◅ V) = s ◅ (V-wrap V) step ((s , unwrap-) ◅ V-wrap V) = s ▻ deval V -step (s ▻ ibuiltin b) = s ◅ ival b +step (s ▻ builtin b) = s ◅ ival b step ((s , (V-I⇒ b {as' = []} p bt ·-)) ◅ vu) = s ▻ BUILTIN' b (bubble p) (app p bt vu) step ((s , (V-I⇒ b {as' = _ ∷ as'} p bt ·-)) ◅ vu) = @@ -168,7 +168,7 @@ thm64 (E CC.▻ unwrap M) E' (CC.step* refl p) = step* (cong (λ E → E ▻ M) (lemmaH E unwrap-)) (thm64 _ E' p) thm64 (E CC.▻ con M) E' (CC.step* refl p) = step* refl (thm64 _ E' p) -thm64 (E CC.▻ ibuiltin b) E' (CC.step* refl p) = +thm64 (E CC.▻ builtin b) E' (CC.step* refl p) = step* refl (thm64 _ E' p) thm64 (E CC.▻ error _) E' (CC.step* refl p) = step* refl (thm64 _ E' p) thm64 (E CC.◅ V) E' (CC.step* refl p) with CC.dissect E | inspect CC.dissect E @@ -197,7 +197,7 @@ thm64b (s ▻ (M ·⋆ A)) s' (step* refl p) = CC.step* refl (thm64b _ s' p) thm64b (s ▻ wrap A B M) s' (step* refl p) = CC.step* refl (thm64b _ s' p) thm64b (s ▻ unwrap M) s' (step* refl p) = CC.step* refl (thm64b _ s' p) thm64b (s ▻ con c) s' (step* refl p) = CC.step* refl (thm64b _ s' p) -thm64b (s ▻ ibuiltin b) s' (step* refl p) = CC.step* refl (thm64b _ s' p) +thm64b (s ▻ builtin b) s' (step* refl p) = CC.step* refl (thm64b _ s' p) thm64b (s ▻ error _) s' (step* refl p) = CC.step* refl (thm64b _ s' p) thm64b (ε ◅ V) s' (step* refl p) = CC.step* refl (thm64b _ s' p) thm64b ((s , (-· M)) ◅ V) s' (step* refl p) = CC.step* @@ -235,7 +235,7 @@ thm64b (□ x₁) s' (step* refl p) = CC.step* refl (thm64b _ s' p) thm64b (◆ A) s' (step* refl p) = CC.step* refl (thm64b _ s' p) test : State (con unit) -test = ε ▻ (ƛ (con unit) · (ibuiltin iData · con (integer (+ 0)))) +test = ε ▻ (ƛ (con unit) · (builtin iData · con (integer (+ 0)))) postulate lemV : ∀{A B}(M : ∅ ⊢ B)(V : Value M)(E : Stack A B) → (E ▻ M) -→s (E ◅ V) diff --git a/plutus-metatheory/src/Algorithmic/Completeness.lagda b/plutus-metatheory/src/Algorithmic/Completeness.lagda index ed983802b35..e3a57282965 100644 --- a/plutus-metatheory/src/Algorithmic/Completeness.lagda +++ b/plutus-metatheory/src/Algorithmic/Completeness.lagda @@ -112,7 +112,7 @@ nfList : ∀{Δ} → List (Δ ⊢⋆ *) → List (Δ ⊢Nf⋆ *) nfList [] = [] nfList (A ∷ As) = nf A ∷ nfList As -postulate itype-lem : ∀ {Φ} b → Norm.itype {Φ} b ≡ nf (Syn.itype b) +postulate btype-lem : ∀ {Φ} b → Norm.btype {Φ} b ≡ nf (Syn.btype b) nfType : ∀{Φ Γ} → {A : Φ ⊢⋆ *} @@ -137,7 +137,7 @@ nfType (Syn.unwrap {A = A}{B = B} t) = Norm.conv⊢ (Norm.unwrap (nfType t)) nfType (Syn.conv p t) = Norm.conv⊢ refl (completeness p) (nfType t) nfType (Syn.con t) = Norm.con (nfTypeTC t) -nfType (Syn.ibuiltin b) = Norm.conv⊢ refl (itype-lem b) (Norm.ibuiltin b) +nfType (Syn.builtin b) = Norm.conv⊢ refl (btype-lem b) (Norm.builtin b) nfType (Syn.error A) = Norm.error (nf A) completenessT : ∀{Φ Γ}{A : Φ ⊢⋆ *} → Γ Syn.⊢ A diff --git a/plutus-metatheory/src/Algorithmic/Erasure.lagda b/plutus-metatheory/src/Algorithmic/Erasure.lagda index 41ea2885c86..d62828e2e07 100644 --- a/plutus-metatheory/src/Algorithmic/Erasure.lagda +++ b/plutus-metatheory/src/Algorithmic/Erasure.lagda @@ -67,7 +67,7 @@ erase (_·⋆_ t A) = force (erase t) erase (wrap A B t) = erase t erase (unwrap t) = erase t erase {Γ = Γ} (con t) = con (eraseTC {Γ = Γ} t) -erase (ibuiltin b) = builtin b +erase (builtin b) = builtin b erase (error A) = error \end{code} @@ -269,9 +269,9 @@ same {Γ = Γ} (D.con tcn) = trans (cong con (sameTC {Γ = Γ} tcn)) (lemcon' (lenLemma Γ) (eraseTC {Γ = nfCtx Γ} (nfTypeTC tcn))) -same {Γ = Γ} (D.ibuiltin b) = trans +same {Γ = Γ} (D.builtin b) = trans (lembuiltin b (lenLemma Γ)) (cong (subst _⊢ (lenLemma Γ)) - (lem-erase refl (itype-lem b) (ibuiltin b))) + (lem-erase refl (btype-lem b) (builtin b))) same {Γ = Γ} (D.error A) = lemerror (lenLemma Γ) open import Algorithmic.Soundness @@ -326,6 +326,6 @@ same' {Γ = Γ} (unwrap t) = same' t same' {Γ = Γ} (con x) = trans (cong con (same'TC {Γ = Γ} x)) (lemcon' (same'Len Γ) (D.eraseTC {Γ = embCtx Γ}(embTC x))) -same' {Γ = Γ} (ibuiltin b) = lembuiltin b (same'Len Γ) +same' {Γ = Γ} (builtin b) = lembuiltin b (same'Len Γ) same' {Γ = Γ} (error A) = lemerror (same'Len Γ) \end{code} diff --git a/plutus-metatheory/src/Algorithmic/Erasure/Reduction.lagda b/plutus-metatheory/src/Algorithmic/Erasure/Reduction.lagda index 671bfd521ef..52f71a26bba 100644 --- a/plutus-metatheory/src/Algorithmic/Erasure/Reduction.lagda +++ b/plutus-metatheory/src/Algorithmic/Erasure/Reduction.lagda @@ -48,7 +48,7 @@ erase≤C' (A.skip⋆ p) = U.skipType (erase≤C' p) erase≤C' (A.skip p) = U.skipTerm (erase≤C' p) -- there could be a simpler version of this without p and q... -erase-arity-lem : ∀ b {Φ}{Γ}(p : proj₁ (ISIG b) ≡ Φ)(q : subst Ctx p (proj₁ (proj₂ (ISIG b))) ≡ Γ) → eraseCtx Γ ≡ U.arity b +erase-arity-lem : ∀ b {Φ}{Γ}(p : proj₁ (sig b) ≡ Φ)(q : subst Ctx p (proj₁ (proj₂ (sig b))) ≡ Γ) → eraseCtx Γ ≡ U.arity b erase-arity-lem addInteger refl refl = refl erase-arity-lem subtractInteger refl refl = refl erase-arity-lem multiplyInteger refl refl = refl @@ -142,9 +142,9 @@ erase-decIf (no ¬p) t f = refl -- typed semantics would give the same answer. Here we just -- exhaustively pattern match on the builtin and its typed args to get -- it to compute. -erase-BUILTIN : ∀ b (σ : SubNf (proj₁ (ISIG b)) ∅)(vs : A.ITel b (proj₁ (proj₂ (ISIG b))) σ) → +erase-BUILTIN : ∀ b (σ : SubNf (proj₁ (sig b)) ∅)(vs : A.ITel b (proj₁ (proj₂ (sig b))) σ) → proj₁ - (U.IBUILTIN' b (erase-arity-lem b refl refl) (eraseITel b (proj₁ (proj₂ (ISIG b))) σ vs)) + (U.IBUILTIN' b (erase-arity-lem b refl refl) (eraseITel b (proj₁ (proj₂ (sig b))) σ vs)) ≡ erase (proj₁ (A.IBUILTIN b σ vs)) erase-BUILTIN addInteger σ ((tt ,, _ ,, A.V-con (integer i)) ,, _ ,, A.V-con (integer i')) = refl erase-BUILTIN subtractInteger σ ((tt ,, _ ,, A.V-con (integer i)) ,, _ ,, A.V-con (integer i')) = refl @@ -223,7 +223,7 @@ erase-BUILTIN indexByteString σ ((tt ,, _ ,, A.V-con (bytestring b)) ,, _ ,, A. ... | yes _ = refl erase-BUILTIN blake2b-256 σ (tt ,, _ ,, A.V-con (bytestring b)) = refl -erase-BUILTIN' : ∀ b {Φ'}{Γ' : Ctx Φ'}(p : proj₁ (ISIG b) ≡ Φ')(q : subst Ctx p (proj₁ (proj₂ (ISIG b))) ≡ Γ')(σ : SubNf Φ' ∅)(vs : A.ITel b Γ' σ){C' : Φ' ⊢Nf⋆ *}(r : subst (_⊢Nf⋆ *) p (proj₂ (proj₂ (ISIG b))) ≡ C') → +erase-BUILTIN' : ∀ b {Φ'}{Γ' : Ctx Φ'}(p : proj₁ (sig b) ≡ Φ')(q : subst Ctx p (proj₁ (proj₂ (sig b))) ≡ Γ')(σ : SubNf Φ' ∅)(vs : A.ITel b Γ' σ){C' : Φ' ⊢Nf⋆ *}(r : subst (_⊢Nf⋆ *) p (proj₂ (proj₂ (sig b))) ≡ C') → proj₁ (U.IBUILTIN' b (erase-arity-lem b p q) (eraseITel b Γ' σ vs)) diff --git a/plutus-metatheory/src/Algorithmic/Erasure/RenamingSubstitution.lagda b/plutus-metatheory/src/Algorithmic/Erasure/RenamingSubstitution.lagda index 6362a9aaf5f..f240eacdfc4 100644 --- a/plutus-metatheory/src/Algorithmic/Erasure/RenamingSubstitution.lagda +++ b/plutus-metatheory/src/Algorithmic/Erasure/RenamingSubstitution.lagda @@ -158,8 +158,8 @@ ren-erase ρ⋆ ρ (unwrap {A = A}{B = B} t) = trans (conv⊢-erase (sym (ren-nf-μ ρ⋆ A B)) (unwrap (A.ren ρ⋆ ρ t))) (ren-erase ρ⋆ ρ t) ren-erase ρ⋆ ρ (con c) = cong con (renTermCon-erase ρ⋆ ρ c) -ren-erase ρ⋆ ρ (ibuiltin b) = - sym (lem-erase refl (itype-ren b ρ⋆) (ibuiltin b)) +ren-erase ρ⋆ ρ (builtin b) = + sym (lem-erase refl (btype-ren b ρ⋆) (builtin b)) ren-erase ρ⋆ ρ (error A) = refl -- @@ -240,8 +240,8 @@ sub-erase σ⋆ σ (unwrap {A = A}{B} t) = trans (conv⊢-erase (sym (sub-nf-μ σ⋆ A B)) (unwrap (A.sub σ⋆ σ t))) (sub-erase σ⋆ σ t) sub-erase σ⋆ σ (con c) = cong con (subTermCon-erase σ⋆ σ c) -sub-erase σ⋆ σ (ibuiltin b) = - sym (lem-erase refl (itype-sub b σ⋆) (ibuiltin b)) +sub-erase σ⋆ σ (builtin b) = + sym (lem-erase refl (btype-sub b σ⋆) (builtin b)) sub-erase σ⋆ σ (error A) = refl lem[]⋆ : ∀{Φ}{Γ : Ctx Φ}{K}{B : Φ ,⋆ K ⊢Nf⋆ *}(N : Γ ,⋆ K ⊢ B)(A : Φ ⊢Nf⋆ K) diff --git a/plutus-metatheory/src/Algorithmic/Reduction.lagda b/plutus-metatheory/src/Algorithmic/Reduction.lagda index 3b25ef58ef7..47ad5bebad9 100644 --- a/plutus-metatheory/src/Algorithmic/Reduction.lagda +++ b/plutus-metatheory/src/Algorithmic/Reduction.lagda @@ -126,7 +126,7 @@ data Value : {A : ∅ ⊢Nf⋆ *} → ∅ ⊢ A → Set where -- but is it helpful to have it on the top level? V-I⇒ : ∀(b : Builtin){Φ Φ'}{Γ : Ctx Φ}{Δ : Ctx Φ'}{A : Φ' ⊢Nf⋆ *}{C : Φ ⊢Nf⋆ *} - → let Ψ ,, Γ' ,, C' = ISIG b in + → let Ψ ,, Γ' ,, C' = sig b in (p : Ψ ≡ Φ) → (q : substEq Ctx p Γ' ≡ Γ) → (r : substEq (_⊢Nf⋆ *) p C' ≡ C) @@ -137,7 +137,7 @@ data Value : {A : ∅ ⊢Nf⋆ *} → ∅ ⊢ A → Set where → Value t V-IΠ : ∀(b : Builtin){Φ Φ'}{Γ : Ctx Φ}{Δ : Ctx Φ'}{K}{C : Φ ⊢Nf⋆ *} - → let Ψ ,, Γ' ,, C' = ISIG b in + → let Ψ ,, Γ' ,, C' = sig b in (p : Ψ ≡ Φ) → (q : substEq Ctx p Γ' ≡ Γ) → (r : substEq (_⊢Nf⋆ *) p C' ≡ C) @@ -176,7 +176,7 @@ convVal refl v = v \begin{code} IBUILTIN : (b : Builtin) - → let Φ ,, Γ ,, C = ISIG b in + → let Φ ,, Γ ,, C = sig b in (σ : SubNf Φ ∅) → (tel : ITel b Γ σ) ----------------------------- @@ -251,7 +251,7 @@ IBUILTIN unBData σ (tt ,, _ ,, V-con (Data (bDATA b))) = IBUILTIN b σ t = _ ,, inj₂ E-error IBUILTIN' : (b : Builtin) - → let Φ ,, Γ ,, C = ISIG b in + → let Φ ,, Γ ,, C = sig b in ∀{Φ'}{Γ' : Ctx Φ'} → (p : Φ ≡ Φ') → (q : substEq Ctx p Γ ≡ Γ') @@ -337,7 +337,7 @@ data _—→_ : {A : ∅ ⊢Nf⋆ *} → (∅ ⊢ A) → (∅ ⊢ A) → Set whe β-sbuiltin : (b : Builtin) - → let Φ ,, Γ ,, C = ISIG b in + → let Φ ,, Γ ,, C = sig b in ∀{Φ'}{Γ' : Ctx Φ'}{A : Φ' ⊢Nf⋆ *} → (σ : SubNf Φ' ∅) → (p : Φ ≡ Φ') @@ -353,7 +353,7 @@ data _—→_ : {A : ∅ ⊢Nf⋆ *} → (∅ ⊢ A) → (∅ ⊢ A) → Set whe β-sbuiltin⋆ : (b : Builtin) - → let Φ ,, Γ ,, C = ISIG b in + → let Φ ,, Γ ,, C = sig b in ∀{Φ'}{Γ' : Ctx Φ'}{K}{A : ∅ ⊢Nf⋆ K} → (σ : SubNf Φ' ∅) → (p : Φ ≡ Φ' ,⋆ K) @@ -427,58 +427,58 @@ progress-· (error E-error) q = step E-·₁ convValue : ∀{A A'}{t : ∅ ⊢ A}(p : A ≡ A') → Value (conv⊢ refl p t) → Value t convValue refl v = v -ival : ∀ b → Value (ibuiltin b) -ival addInteger = V-I⇒ addInteger refl refl refl (λ()) (skip base) tt (ibuiltin addInteger) -ival subtractInteger = V-I⇒ subtractInteger refl refl refl (λ()) (skip base) tt (ibuiltin subtractInteger) -ival multiplyInteger = V-I⇒ multiplyInteger refl refl refl (λ()) (skip base) tt (ibuiltin multiplyInteger) -ival divideInteger = V-I⇒ divideInteger refl refl refl (λ()) (skip base) tt (ibuiltin divideInteger) -ival quotientInteger = V-I⇒ quotientInteger refl refl refl (λ()) (skip base) tt (ibuiltin quotientInteger) -ival remainderInteger = V-I⇒ remainderInteger refl refl refl (λ()) (skip base) tt (ibuiltin remainderInteger) -ival modInteger = V-I⇒ modInteger refl refl refl (λ()) (skip base) tt (ibuiltin modInteger) -ival lessThanInteger = V-I⇒ lessThanInteger refl refl refl (λ()) (skip base) tt (ibuiltin lessThanInteger) -ival lessThanEqualsInteger = V-I⇒ lessThanEqualsInteger refl refl refl (λ()) (≤Cto≤C' (skip base)) tt (ibuiltin lessThanEqualsInteger) -ival equalsInteger = V-I⇒ equalsInteger refl refl refl (λ()) (skip base) tt (ibuiltin equalsInteger) -ival lessThanByteString = V-I⇒ lessThanByteString refl refl refl (λ()) (skip base) tt (ibuiltin lessThanByteString) -ival lessThanEqualsByteString = V-I⇒ lessThanEqualsByteString refl refl refl (λ()) (≤Cto≤C' (skip base)) tt (ibuiltin lessThanEqualsByteString) -ival sha2-256 = V-I⇒ sha2-256 refl refl refl (λ()) base tt (ibuiltin sha2-256) -ival sha3-256 = V-I⇒ sha3-256 refl refl refl (λ()) base tt (ibuiltin sha3-256) -ival verifySignature = V-I⇒ verifySignature refl refl refl (λ()) (skip (skip base)) tt (ibuiltin verifySignature) -ival equalsByteString = V-I⇒ equalsByteString refl refl refl (λ()) (skip base) tt (ibuiltin equalsByteString) -ival appendByteString = V-I⇒ appendByteString refl refl refl (λ()) (skip base) tt (ibuiltin appendByteString) -ival appendString = V-I⇒ appendString refl refl refl (λ()) (skip base) tt (ibuiltin appendString) -ival ifThenElse = V-IΠ ifThenElse refl refl refl (λ()) (skip (skip (skip base))) tt (ibuiltin ifThenElse) -ival trace = V-IΠ trace refl refl refl (λ()) (skip (skip base)) tt (ibuiltin trace) -ival equalsString = V-I⇒ equalsString refl refl refl (λ()) (skip base) tt (ibuiltin equalsString) -ival encodeUtf8 = V-I⇒ encodeUtf8 refl refl refl (λ()) base tt (ibuiltin encodeUtf8) -ival decodeUtf8 = V-I⇒ decodeUtf8 refl refl refl (λ()) base tt (ibuiltin decodeUtf8) -ival fstPair = V-IΠ fstPair refl refl refl (λ()) (skip⋆ (skip base)) tt (ibuiltin fstPair) -ival sndPair = V-IΠ sndPair refl refl refl (λ()) (skip⋆ (skip base)) tt (ibuiltin sndPair) -ival nullList = V-IΠ nullList refl refl refl (λ()) (skip base) tt (ibuiltin nullList) -ival headList = V-IΠ headList refl refl refl (λ()) (skip base) tt (ibuiltin headList) -ival tailList = V-IΠ tailList refl refl refl (λ()) (skip base) tt (ibuiltin tailList) -ival chooseList = V-IΠ chooseList refl refl refl (λ()) (skip⋆ (skip (skip (skip base)))) tt (ibuiltin chooseList) -ival constrData = V-I⇒ constrData refl refl refl (λ()) (skip base) tt (ibuiltin constrData) -ival mapData = V-I⇒ mapData refl refl refl (λ()) base tt (ibuiltin mapData) -ival listData = V-I⇒ listData refl refl refl (λ()) base tt (ibuiltin listData) -ival iData = V-I⇒ iData refl refl refl (λ()) base tt (ibuiltin iData) -ival bData = V-I⇒ bData refl refl refl (λ()) base tt (ibuiltin bData) -ival unConstrData = V-I⇒ unConstrData refl refl refl (λ()) base tt (ibuiltin unConstrData) -ival unMapData = V-I⇒ unMapData refl refl refl (λ()) base tt (ibuiltin unMapData) -ival unListData = V-I⇒ unListData refl refl refl (λ()) base tt (ibuiltin unListData) -ival unIData = V-I⇒ unIData refl refl refl (λ()) base tt (ibuiltin unIData) -ival unBData = V-I⇒ unBData refl refl refl (λ()) base tt (ibuiltin unBData) -ival equalsData = V-I⇒ equalsData refl refl refl (λ()) (skip base) tt (ibuiltin equalsData) -ival chooseData = V-IΠ chooseData refl refl refl (λ()) (skip (skip (skip (skip (skip (skip base)))))) tt (ibuiltin chooseData) -ival chooseUnit = V-IΠ chooseUnit refl refl refl (λ()) (skip (skip base)) tt (ibuiltin chooseUnit) -ival mkPairData = V-I⇒ mkPairData refl refl refl (λ()) (skip base) tt (ibuiltin mkPairData) -ival mkNilData = V-I⇒ mkNilData refl refl refl (λ()) base tt (ibuiltin mkNilData) -ival mkNilPairData = V-I⇒ mkNilPairData refl refl refl (λ()) base tt (ibuiltin mkNilPairData) -ival mkCons = V-I⇒ mkCons refl refl refl (λ()) (skip base) tt (ibuiltin mkCons) -ival consByteString = V-I⇒ consByteString refl refl refl (λ()) (skip base) tt (ibuiltin consByteString) -ival sliceByteString = V-I⇒ sliceByteString refl refl refl (λ()) (skip (skip base)) tt (ibuiltin sliceByteString) -ival lengthOfByteString = V-I⇒ lengthOfByteString refl refl refl (λ()) base tt (ibuiltin lengthOfByteString) -ival indexByteString = V-I⇒ indexByteString refl refl refl (λ()) (skip base) tt (ibuiltin indexByteString) -ival blake2b-256 = V-I⇒ blake2b-256 refl refl refl (λ()) base tt (ibuiltin blake2b-256) +ival : ∀ b → Value (builtin b) +ival addInteger = V-I⇒ addInteger refl refl refl (λ()) (skip base) tt (builtin addInteger) +ival subtractInteger = V-I⇒ subtractInteger refl refl refl (λ()) (skip base) tt (builtin subtractInteger) +ival multiplyInteger = V-I⇒ multiplyInteger refl refl refl (λ()) (skip base) tt (builtin multiplyInteger) +ival divideInteger = V-I⇒ divideInteger refl refl refl (λ()) (skip base) tt (builtin divideInteger) +ival quotientInteger = V-I⇒ quotientInteger refl refl refl (λ()) (skip base) tt (builtin quotientInteger) +ival remainderInteger = V-I⇒ remainderInteger refl refl refl (λ()) (skip base) tt (builtin remainderInteger) +ival modInteger = V-I⇒ modInteger refl refl refl (λ()) (skip base) tt (builtin modInteger) +ival lessThanInteger = V-I⇒ lessThanInteger refl refl refl (λ()) (skip base) tt (builtin lessThanInteger) +ival lessThanEqualsInteger = V-I⇒ lessThanEqualsInteger refl refl refl (λ()) (≤Cto≤C' (skip base)) tt (builtin lessThanEqualsInteger) +ival equalsInteger = V-I⇒ equalsInteger refl refl refl (λ()) (skip base) tt (builtin equalsInteger) +ival lessThanByteString = V-I⇒ lessThanByteString refl refl refl (λ()) (skip base) tt (builtin lessThanByteString) +ival lessThanEqualsByteString = V-I⇒ lessThanEqualsByteString refl refl refl (λ()) (≤Cto≤C' (skip base)) tt (builtin lessThanEqualsByteString) +ival sha2-256 = V-I⇒ sha2-256 refl refl refl (λ()) base tt (builtin sha2-256) +ival sha3-256 = V-I⇒ sha3-256 refl refl refl (λ()) base tt (builtin sha3-256) +ival verifySignature = V-I⇒ verifySignature refl refl refl (λ()) (skip (skip base)) tt (builtin verifySignature) +ival equalsByteString = V-I⇒ equalsByteString refl refl refl (λ()) (skip base) tt (builtin equalsByteString) +ival appendByteString = V-I⇒ appendByteString refl refl refl (λ()) (skip base) tt (builtin appendByteString) +ival appendString = V-I⇒ appendString refl refl refl (λ()) (skip base) tt (builtin appendString) +ival ifThenElse = V-IΠ ifThenElse refl refl refl (λ()) (skip (skip (skip base))) tt (builtin ifThenElse) +ival trace = V-IΠ trace refl refl refl (λ()) (skip (skip base)) tt (builtin trace) +ival equalsString = V-I⇒ equalsString refl refl refl (λ()) (skip base) tt (builtin equalsString) +ival encodeUtf8 = V-I⇒ encodeUtf8 refl refl refl (λ()) base tt (builtin encodeUtf8) +ival decodeUtf8 = V-I⇒ decodeUtf8 refl refl refl (λ()) base tt (builtin decodeUtf8) +ival fstPair = V-IΠ fstPair refl refl refl (λ()) (skip⋆ (skip base)) tt (builtin fstPair) +ival sndPair = V-IΠ sndPair refl refl refl (λ()) (skip⋆ (skip base)) tt (builtin sndPair) +ival nullList = V-IΠ nullList refl refl refl (λ()) (skip base) tt (builtin nullList) +ival headList = V-IΠ headList refl refl refl (λ()) (skip base) tt (builtin headList) +ival tailList = V-IΠ tailList refl refl refl (λ()) (skip base) tt (builtin tailList) +ival chooseList = V-IΠ chooseList refl refl refl (λ()) (skip⋆ (skip (skip (skip base)))) tt (builtin chooseList) +ival constrData = V-I⇒ constrData refl refl refl (λ()) (skip base) tt (builtin constrData) +ival mapData = V-I⇒ mapData refl refl refl (λ()) base tt (builtin mapData) +ival listData = V-I⇒ listData refl refl refl (λ()) base tt (builtin listData) +ival iData = V-I⇒ iData refl refl refl (λ()) base tt (builtin iData) +ival bData = V-I⇒ bData refl refl refl (λ()) base tt (builtin bData) +ival unConstrData = V-I⇒ unConstrData refl refl refl (λ()) base tt (builtin unConstrData) +ival unMapData = V-I⇒ unMapData refl refl refl (λ()) base tt (builtin unMapData) +ival unListData = V-I⇒ unListData refl refl refl (λ()) base tt (builtin unListData) +ival unIData = V-I⇒ unIData refl refl refl (λ()) base tt (builtin unIData) +ival unBData = V-I⇒ unBData refl refl refl (λ()) base tt (builtin unBData) +ival equalsData = V-I⇒ equalsData refl refl refl (λ()) (skip base) tt (builtin equalsData) +ival chooseData = V-IΠ chooseData refl refl refl (λ()) (skip (skip (skip (skip (skip (skip base)))))) tt (builtin chooseData) +ival chooseUnit = V-IΠ chooseUnit refl refl refl (λ()) (skip (skip base)) tt (builtin chooseUnit) +ival mkPairData = V-I⇒ mkPairData refl refl refl (λ()) (skip base) tt (builtin mkPairData) +ival mkNilData = V-I⇒ mkNilData refl refl refl (λ()) base tt (builtin mkNilData) +ival mkNilPairData = V-I⇒ mkNilPairData refl refl refl (λ()) base tt (builtin mkNilPairData) +ival mkCons = V-I⇒ mkCons refl refl refl (λ()) (skip base) tt (builtin mkCons) +ival consByteString = V-I⇒ consByteString refl refl refl (λ()) (skip base) tt (builtin consByteString) +ival sliceByteString = V-I⇒ sliceByteString refl refl refl (λ()) (skip (skip base)) tt (builtin sliceByteString) +ival lengthOfByteString = V-I⇒ lengthOfByteString refl refl refl (λ()) base tt (builtin lengthOfByteString) +ival indexByteString = V-I⇒ indexByteString refl refl refl (λ()) (skip base) tt (builtin indexByteString) +ival blake2b-256 = V-I⇒ blake2b-256 refl refl refl (λ()) base tt (builtin blake2b-256) progress-·⋆ : ∀{K B}{t : ∅ ⊢ Π B} → Progress t → (A : ∅ ⊢Nf⋆ K) → Progress (t ·⋆ A) @@ -513,7 +513,7 @@ progress (M ·⋆ A) = progress-·⋆ (progress M) A progress (wrap A B M) = progress-wrap (progress M) progress (unwrap M) = progress-unwrap (progress M) progress (con c) = done (V-con c) -progress (ibuiltin b) = done (ival b) +progress (builtin b) = done (ival b) progress (error A) = error E-error open import Data.Nat diff --git a/plutus-metatheory/src/Algorithmic/ReductionEC.lagda.md b/plutus-metatheory/src/Algorithmic/ReductionEC.lagda.md index 67117a0acdd..cadd5066c42 100644 --- a/plutus-metatheory/src/Algorithmic/ReductionEC.lagda.md +++ b/plutus-metatheory/src/Algorithmic/ReductionEC.lagda.md @@ -151,7 +151,7 @@ data Value : {A : ∅ ⊢Nf⋆ *} → ∅ ⊢ A → Set data BApp (b : Builtin) : ∀{az}{as} → az <>> as ∈ arity b → ∀{A} → ∅ ⊢ A → Set where - base : BApp b (start (arity b)) (ibuiltin b) + base : BApp b (start (arity b)) (builtin b) step : ∀{A B}{az as} → (p : az <>> (Term ∷ as) ∈ arity b) → {t : ∅ ⊢ A ⇒ B} → BApp b p t @@ -258,7 +258,7 @@ VALUE2Value (V-IΠ b p refl x) = V-IΠ b p x data BAPP (b : Builtin) : ∀{az}{as} → az <>> as ∈ arity b → ∀{A} → ∅ ⊢ A → Set where - base : BAPP b (start (arity b)) (ibuiltin b) + base : BAPP b (start (arity b)) (builtin b) step : ∀{A B}{az as} → (p : az <>> (Term ∷ as) ∈ arity b) → {t : ∅ ⊢ A ⇒ B} → BAPP b p t @@ -634,7 +634,7 @@ lemma∷1 as .as (start .as) = refl -- HINT: pattern matching on p rather than the next arg (q) generates -- fewer cases -bappTermLem : ∀ b {A}{az as}(M : ∅ ⊢ A)(p : az <>> (Term ∷ as) ∈ arity b) +bappTermLem : ∀ b {A}{az as}(M : ∅ ⊢ A)(p : az <>> Term ∷ as ∈ arity b) → BAPP b p M → ∃ λ A' → ∃ λ A'' → A ≡ A' ⇒ A'' bappTermLem addInteger _ (start _) base = _ ,, _ ,, refl bappTermLem addInteger {as = as} _ (bubble {as = az} p) q @@ -879,7 +879,7 @@ bappTermLem mkCons _ (bubble (start _)) (step _ base _) bappTermLem appendByteString _ _ base = _ ,, _ ,, refl bappTermLem appendByteString {as = as} (M · M') .(bubble p) (step {az = az} p q x) with <>>-cancel-both az (([] :< Term) :< Term) as p -bappTermLem appendByteString {as = .[]} (.(ibuiltin appendByteString) · M') (bubble (start .(Term ∷ Term ∷ []))) (step {az = _} (start .(Term ∷ Term ∷ [])) base x) +bappTermLem appendByteString {as = .[]} (.(builtin appendByteString) · M') (bubble (start .(Term ∷ Term ∷ []))) (step {az = _} (start .(Term ∷ Term ∷ [])) base x) | refl ,, refl = _ ,, _ ,, refl bappTermLem appendByteString {as = as} M .(bubble p) (step⋆ {az = az} p q q₁ x) with <>>-cancel-both' az (([] :< Type) :< Term) (([] :< Term) :< Term) as p refl @@ -1107,7 +1107,7 @@ V-I b {a = Term} p q with bappTermLem b _ p (BApp2BAPP q) V-I b {a = Type} p q with bappTypeLem b _ p (BApp2BAPP q) ... | _ ,, _ ,, refl = V-IΠ b p q -ival : ∀ b → Value (ibuiltin b) +ival : ∀ b → Value (builtin b) -- ival b = V-I b (start _) base -- ^ not possible as we could have a builtin with no args @@ -1201,7 +1201,7 @@ progress (unwrap M) with progress M ... | done (V-wrap V) = step (ruleEC [] (β-wrap V) refl refl) ... | error E-error = step (ruleErr (unwrap []) refl) progress (con c) = done (V-con c) -progress (ibuiltin b) = done (ival b) +progress (builtin b) = done (ival b) progress (error A) = error E-error _↓ : ∀{A} → ∅ ⊢ A → Set @@ -1248,7 +1248,7 @@ lemma51 (unwrap M) with lemma51 M ... | inj₂ (B ,, E ,, L ,, p ,, p') = inj₂ (B ,, unwrap E ,, L ,, p ,, cong unwrap p') lemma51 (con c) = inj₁ (V-con c) -lemma51 (ibuiltin b) = inj₁ (ival b) +lemma51 (builtin b) = inj₁ (ival b) lemma51 (error _) = inj₂ (_ ,, ([] ,, (error _ ,, (inj₂ E-error) ,, refl))) progress' : {A : ∅ ⊢Nf⋆ *} → (M : ∅ ⊢ A) → Progress M @@ -1267,7 +1267,7 @@ uniqueVal : ∀{A}(M : ∅ ⊢ A)(v v' : Value M) → v ≡ v' uniqueBApp : ∀{A b as az} → (p : az <>> as ∈ arity b)(M : ∅ ⊢ A)(v v' : BApp b p M) → v ≡ v' -uniqueBApp .(start (arity b)) (ibuiltin b) base base = refl +uniqueBApp .(start (arity b)) (builtin b) base base = refl uniqueBApp .(bubble p) (M ·⋆ A) (step⋆ p v) (step⋆ .p v') with uniqueBApp p M v v' ... | refl = refl @@ -1278,7 +1278,7 @@ uniqueBApp .(bubble p) (M · M') (step p v w) (step .p v' w') uniqueBApp' : ∀{A b b' as as' az az'}(M : ∅ ⊢ A)(p : az <>> as ∈ arity b)(p' : az' <>> as' ∈ arity b')(v : BApp b p M)(v' : BApp b' p' M) → ∃ λ (r : b ≡ b') → ∃ λ (r' : az ≡ az') → ∃ λ (r'' : as ≡ as') → p ≡ subst<>>∈ p' r r' r'' -uniqueBApp' (ibuiltin b) .(start (arity b)) .(start (arity b)) base base = +uniqueBApp' (builtin b) .(start (arity b)) .(start (arity b)) base base = refl ,, refl ,, refl ,, refl uniqueBApp' (M · M') .(bubble p) .(bubble p₁) (step p q x) (step p₁ q' x₁) with uniqueBApp' M p p₁ q q' @@ -1709,7 +1709,7 @@ rlemma51! (unwrap M) with rlemma51! M λ E p q → let X ,, Y ,, Y' = Uunwrap2 VM refl E (≡-to-≅ p) q in X ,, ≅-to-≡ Y ,, ≅-to-≡ Y' rlemma51! (con c) = done (V-con c) -rlemma51! (ibuiltin b) = done (ival b) +rlemma51! (builtin b) = done (ival b) rlemma51! (error _) = step (valerr E-error) [] diff --git a/plutus-metatheory/src/Algorithmic/RenamingSubstitution.lagda b/plutus-metatheory/src/Algorithmic/RenamingSubstitution.lagda index 18a5ed2e4b6..ee1dfa6bdf8 100644 --- a/plutus-metatheory/src/Algorithmic/RenamingSubstitution.lagda +++ b/plutus-metatheory/src/Algorithmic/RenamingSubstitution.lagda @@ -92,7 +92,7 @@ ren ρ⋆ ρ (unwrap {A = A}{B} M) = conv⊢ (sym (ren-nf-μ ρ⋆ A B)) (unwrap (ren ρ⋆ ρ M)) ren ρ⋆ ρ (con c) = con (renTermCon ρ⋆ c) -ren ρ⋆ ρ (ibuiltin b) = conv⊢ refl (itype-ren b ρ⋆) (ibuiltin b) +ren ρ⋆ ρ (builtin b) = conv⊢ refl (btype-ren b ρ⋆) (builtin b) ren ρ⋆ ρ (error A) = error (renNf ρ⋆ A) \end{code} @@ -181,7 +181,7 @@ sub σ⋆ σ (unwrap {A = A}{B} M) = conv⊢ (sym (sub-nf-μ σ⋆ A B)) (unwrap (sub σ⋆ σ M)) sub σ⋆ σ (con c) = con (subTermCon σ⋆ c) -sub σ⋆ σ (ibuiltin b) = conv⊢ refl (itype-sub b σ⋆) (ibuiltin b) +sub σ⋆ σ (builtin b) = conv⊢ refl (btype-sub b σ⋆) (builtin b) sub σ⋆ σ (error A) = error (subNf σ⋆ A) \end{code} diff --git a/plutus-metatheory/src/Algorithmic/Soundness.lagda b/plutus-metatheory/src/Algorithmic/Soundness.lagda index be2cb57cd31..b3ce6795b97 100644 --- a/plutus-metatheory/src/Algorithmic/Soundness.lagda +++ b/plutus-metatheory/src/Algorithmic/Soundness.lagda @@ -139,7 +139,7 @@ lemsub A A' σ p = trans≡β ((≡2β (sym (cong embNf (sub-eval A' idCR (embNf ∘ σ)))))))) (sym≡β (soundness (sub (embNf ∘ σ) A'))) -postulate itype-lem≡β : ∀{Φ} b → Dec.itype {Φ} b ≡β embNf (Alg.itype b) +postulate btype-lem≡β : ∀{Φ} b → Dec.btype {Φ} b ≡β embNf (Alg.btype b) emb : ∀{Φ Γ}{A : Φ ⊢Nf⋆ *} → Γ Alg.⊢ A → embCtx Γ Dec.⊢ embNf A emb (Alg.` α) = Dec.` (embVar α) @@ -155,7 +155,7 @@ emb (Alg.wrap A B t) = Dec.wrap emb (Alg.unwrap {A = A}{B} t) = Dec.conv (soundness-μ refl A B) (Dec.unwrap (emb t)) emb (Alg.con {tcn = tcn} t ) = Dec.con (embTC t) -emb (Alg.ibuiltin b) = Dec.conv (itype-lem≡β b) (Dec.ibuiltin b) +emb (Alg.builtin b) = Dec.conv (btype-lem≡β b) (Dec.builtin b) emb (Alg.error A) = Dec.error (embNf A) soundnessT : ∀{Φ Γ}{A : Φ ⊢Nf⋆ *} → Γ Alg.⊢ A → embCtx Γ Dec.⊢ embNf A diff --git a/plutus-metatheory/src/Check.lagda.md b/plutus-metatheory/src/Check.lagda.md index cd14953679c..86d069e6d8a 100644 --- a/plutus-metatheory/src/Check.lagda.md +++ b/plutus-metatheory/src/Check.lagda.md @@ -387,7 +387,7 @@ inferType {Φ} Γ (con c) = do inferType Γ (error A) = do A ← isStar (inferKind _ A) return (A ,, error A) -inferType Γ (ibuiltin b) = inj₂ (itype b ,, ibuiltin b) +inferType Γ (builtin b) = inj₂ (btype b ,, builtin b) inferType Γ (wrap A B L) = do K ,, A ← isPat (inferKind _ A) B ← checkKind _ B K diff --git a/plutus-metatheory/src/Declarative.lagda.md b/plutus-metatheory/src/Declarative.lagda.md index dd08835ba0a..63c5351f1d9 100644 --- a/plutus-metatheory/src/Declarative.lagda.md +++ b/plutus-metatheory/src/Declarative.lagda.md @@ -95,29 +95,29 @@ Let `x`, `y` range over variables. Computing a signature for a builtin. Ideally this should be done generically: ``` -ISIG : Builtin → Σ Ctx⋆ λ Φ → Ctx Φ × Φ ⊢⋆ * -ISIG ifThenElse = ∅ ,⋆ * ,, ∅ ,⋆ * , con bool , ` Z , ` Z ,, ` Z -ISIG addInteger = ∅ ,, ∅ , con integer , con integer ,, con integer -ISIG subtractInteger = ∅ ,, ∅ , con integer , con integer ,, con integer -ISIG multiplyInteger = ∅ ,, ∅ , con integer , con integer ,, con integer -ISIG divideInteger = ∅ ,, ∅ , con integer , con integer ,, con integer -ISIG quotientInteger = ∅ ,, ∅ , con integer , con integer ,, con integer -ISIG remainderInteger = ∅ ,, ∅ , con integer , con integer ,, con integer -ISIG modInteger = ∅ ,, ∅ , con integer , con integer ,, con integer -ISIG lessThanInteger = ∅ ,, ∅ , con integer , con integer ,, con bool -ISIG lessThanEqualsInteger = ∅ ,, ∅ , con integer , con integer ,, con bool -ISIG equalsInteger = ∅ ,, ∅ , con integer , con integer ,, con bool -ISIG appendByteString = ∅ ,, ∅ , con bytestring , con bytestring ,, con bytestring -ISIG lessThanByteString = ∅ ,, ∅ , con bytestring , con bytestring ,, con bool -ISIG lessThanEqualsByteString = +sig : Builtin → Σ Ctx⋆ λ Φ → Ctx Φ × Φ ⊢⋆ * +sig ifThenElse = ∅ ,⋆ * ,, ∅ ,⋆ * , con bool , ` Z , ` Z ,, ` Z +sig addInteger = ∅ ,, ∅ , con integer , con integer ,, con integer +sig subtractInteger = ∅ ,, ∅ , con integer , con integer ,, con integer +sig multiplyInteger = ∅ ,, ∅ , con integer , con integer ,, con integer +sig divideInteger = ∅ ,, ∅ , con integer , con integer ,, con integer +sig quotientInteger = ∅ ,, ∅ , con integer , con integer ,, con integer +sig remainderInteger = ∅ ,, ∅ , con integer , con integer ,, con integer +sig modInteger = ∅ ,, ∅ , con integer , con integer ,, con integer +sig lessThanInteger = ∅ ,, ∅ , con integer , con integer ,, con bool +sig lessThanEqualsInteger = ∅ ,, ∅ , con integer , con integer ,, con bool +sig equalsInteger = ∅ ,, ∅ , con integer , con integer ,, con bool +sig appendByteString = ∅ ,, ∅ , con bytestring , con bytestring ,, con bytestring +sig lessThanByteString = ∅ ,, ∅ , con bytestring , con bytestring ,, con bool +sig lessThanEqualsByteString = ∅ ,, ∅ , con bytestring , con bytestring ,, con bool -ISIG sha2-256 = ∅ ,, ∅ , con bytestring ,, con bytestring -ISIG sha3-256 = ∅ ,, ∅ , con bytestring ,, con bytestring -ISIG verifySignature = ∅ ,, ∅ , con bytestring , con bytestring , con bytestring ,, con bool -ISIG equalsByteString = ∅ ,, ∅ , con bytestring , con bytestring ,, con bool -ISIG appendString = ∅ ,, ∅ , con string , con string ,, con string -ISIG trace = ∅ ,, ∅ , con string ,, con unit -ISIG _ = ∅ ,, ∅ ,, con unit -- TODO: add support for remaining builtins +sig sha2-256 = ∅ ,, ∅ , con bytestring ,, con bytestring +sig sha3-256 = ∅ ,, ∅ , con bytestring ,, con bytestring +sig verifySignature = ∅ ,, ∅ , con bytestring , con bytestring , con bytestring ,, con bool +sig equalsByteString = ∅ ,, ∅ , con bytestring , con bytestring ,, con bool +sig appendString = ∅ ,, ∅ , con string , con string ,, con string +sig trace = ∅ ,, ∅ , con string ,, con unit +sig _ = ∅ ,, ∅ ,, con unit -- TODO: add support for remaining builtins ``` Converting a signature to a totally unsaturated type: @@ -132,15 +132,15 @@ isig2type Φ (Γ , A) C = isig2type Φ Γ (A ⇒ C) Compute the type for a builtin: ``` -itype : Builtin → Φ ⊢⋆ * -itype b = let Φ ,, Γ ,, C = ISIG b in sub (λ()) (isig2type Φ Γ C) +btype : Builtin → Φ ⊢⋆ * +btype b = let Φ ,, Γ ,, C = sig b in sub (λ()) (isig2type Φ Γ C) ``` Two lemmas concerning renaming and substituting types of builtins: ``` -postulate itype-ren : ∀ b (ρ : Ren Φ Ψ) → itype b ≡ ren ρ (itype b) -postulate itype-sub : ∀ b (ρ : Sub Φ Ψ) → itype b ≡ sub ρ (itype b) +postulate btype-ren : ∀ b (ρ : Ren Φ Ψ) → btype b ≡ ren ρ (btype b) +postulate btype-sub : ∀ b (ρ : Sub Φ Ψ) → btype b ≡ sub ρ (btype b) ``` ## Terms @@ -195,9 +195,9 @@ data _⊢_ (Γ : Ctx Φ) : Φ ⊢⋆ * → Set where --------------- → Γ ⊢ con c - ibuiltin : (b : Builtin) - -------------- - → Γ ⊢ itype b + builtin : (b : Builtin) + -------------- + → Γ ⊢ btype b error : (A : Φ ⊢⋆ *) ------------ diff --git a/plutus-metatheory/src/Declarative/Erasure.lagda.md b/plutus-metatheory/src/Declarative/Erasure.lagda.md index 59c1badfe0e..b4f1e62c9ea 100644 --- a/plutus-metatheory/src/Declarative/Erasure.lagda.md +++ b/plutus-metatheory/src/Declarative/Erasure.lagda.md @@ -69,17 +69,17 @@ erase : ∀{Φ Γ}{A : Φ ⊢⋆ *} → Γ ⊢ A → len Γ ⊢ erase-Sub : ∀{Φ Ψ}{Γ : Ctx Φ}{Δ : Ctx Ψ}(σ⋆ : T.Sub Φ Ψ) → D.Sub Γ Δ σ⋆ → U.Sub (len Γ) (len Δ) -erase (` α) = ` (eraseVar α) -erase (ƛ t) = ƛ (erase t) -erase (t · u) = erase t · erase u -erase (Λ t) = delay (erase t) -erase (t ·⋆ A) = force (erase t) -erase (wrap A B t) = erase t -erase (unwrap t) = erase t -erase (conv p t) = erase t -erase {Γ = Γ} (con t) = con (eraseTC {Γ = Γ} t) -erase (ibuiltin b) = builtin b -erase (error A) = error +erase (` α) = ` (eraseVar α) +erase (ƛ t) = ƛ (erase t) +erase (t · u) = erase t · erase u +erase (Λ t) = delay (erase t) +erase (t ·⋆ A) = force (erase t) +erase (wrap A B t) = erase t +erase (unwrap t) = erase t +erase (conv p t) = erase t +erase {Γ = Γ} (con t) = con (eraseTC {Γ = Γ} t) +erase (builtin b) = builtin b +erase (error A) = error backVar⋆ : ∀{Φ}(Γ : Ctx Φ) → Fin (len Γ) → Φ ⊢⋆ * backVar⋆ (Γ ,⋆ J) x = T.weaken (backVar⋆ Γ x) diff --git a/plutus-metatheory/src/Declarative/Examples.lagda.md b/plutus-metatheory/src/Declarative/Examples.lagda.md index 44a0ea6940b..7e6fe3d3fc2 100644 --- a/plutus-metatheory/src/Declarative/Examples.lagda.md +++ b/plutus-metatheory/src/Declarative/Examples.lagda.md @@ -44,7 +44,7 @@ module Builtins where con2 = con (integer (pos 2)) builtin2plus2 : ∅ ⊢ con integer - builtin2plus2 = ibuiltin addInteger · con2 · con2 + builtin2plus2 = builtin addInteger · con2 · con2 builtininc2 : ∅ ⊢ con integer builtininc2 = inc · con2 diff --git a/plutus-metatheory/src/Declarative/Examples/StdLib/ChurchNat.lagda b/plutus-metatheory/src/Declarative/Examples/StdLib/ChurchNat.lagda index ed33f09cffc..1d47c3d74fa 100644 --- a/plutus-metatheory/src/Declarative/Examples/StdLib/ChurchNat.lagda +++ b/plutus-metatheory/src/Declarative/Examples/StdLib/ChurchNat.lagda @@ -40,7 +40,7 @@ con1 : ∀{Φ}{Γ : Ctx Φ} → Γ ⊢ con integer con1 = con (integer (ℤ.pos 1)) inc : ∀{Φ}{Γ : Ctx Φ} → Γ ⊢ con integer ⇒ con integer -inc = ƛ (ibuiltin addInteger · con1 · ` Z) +inc = ƛ (builtin addInteger · con1 · ` Z) Nat2Int : ∅ ⊢ N ⇒ con integer Nat2Int = ƛ (Iter diff --git a/plutus-metatheory/src/Declarative/RenamingSubstitution.lagda.md b/plutus-metatheory/src/Declarative/RenamingSubstitution.lagda.md index de1bb8548bd..47a7ba773db 100644 --- a/plutus-metatheory/src/Declarative/RenamingSubstitution.lagda.md +++ b/plutus-metatheory/src/Declarative/RenamingSubstitution.lagda.md @@ -99,7 +99,7 @@ ren _ ρ (wrap A B L) = wrap _ _ (conv⊢ refl (⋆.ren-μ _ A B) (ren _ ρ L)) ren _ ρ (unwrap L) = conv⊢ refl (sym (⋆.ren-μ _ _ _)) (unwrap (ren _ ρ L)) ren _ ρ (conv p L) = conv (ren≡β _ p) (ren _ ρ L) ren ρ⋆ ρ (con cn) = con (renTermCon ρ⋆ cn) -ren ρ⋆ _ (ibuiltin b) = conv⊢ refl (itype-ren b ρ⋆) (ibuiltin b) +ren ρ⋆ _ (builtin b) = conv⊢ refl (btype-ren b ρ⋆) (builtin b) ren _ _ (error A) = error (⋆.ren _ A) ``` @@ -193,7 +193,7 @@ sub _ σ (unwrap L) = conv⊢ refl (sym (⋆.sub-μ _ (muPat L) (muArg L))) (unwrap (sub _ σ L)) sub _ σ (conv p L) = conv (sub≡β _ p) (sub _ σ L) sub σ⋆ _ (con cn) = con (subTermCon σ⋆ cn) -sub _ _ (ibuiltin b) = conv⊢ refl (itype-sub b _) (ibuiltin b) +sub _ _ (builtin b) = conv⊢ refl (btype-sub b _) (builtin b) sub _ _ (error A) = error (⋆.sub _ A) ``` diff --git a/plutus-metatheory/src/Scoped.lagda b/plutus-metatheory/src/Scoped.lagda index cd674e16710..b22d68179a0 100644 --- a/plutus-metatheory/src/Scoped.lagda +++ b/plutus-metatheory/src/Scoped.lagda @@ -25,72 +25,6 @@ open import Utils \end{code} \begin{code} -arity : Builtin → ℕ -arity addInteger = 2 -arity subtractInteger = 2 -arity multiplyInteger = 2 -arity divideInteger = 2 -arity quotientInteger = 2 -arity remainderInteger = 2 -arity modInteger = 2 -arity lessThanInteger = 2 -arity lessThanEqualsInteger = 2 -arity equalsInteger = 2 -arity appendByteString = 2 -arity lessThanByteString = 2 -arity lessThanEqualsByteString = 2 -arity sha2-256 = 1 -arity sha3-256 = 1 -arity verifySignature = 3 -arity equalsByteString = 2 -arity ifThenElse = 3 -arity appendString = 2 -arity trace = 2 -arity equalsString = 2 -arity encodeUtf8 = 1 -arity decodeUtf8 = 1 -arity fstPair = 1 -arity sndPair = 1 -arity nullList = 1 -arity headList = 1 -arity tailList = 1 -arity chooseList = 3 -arity constrData = 2 -arity mapData = 1 -arity listData = 1 -arity iData = 1 -arity bData = 1 -arity unConstrData = 1 -arity unMapData = 1 -arity unListData = 1 -arity unIData = 1 -arity unBData = 1 -arity equalsData = 2 -arity chooseData = 6 -arity chooseUnit = 2 -arity mkPairData = 2 -arity mkNilData = 1 -arity mkNilPairData = 1 -arity mkCons = 2 -arity consByteString = 2 -arity sliceByteString = 3 -arity lengthOfByteString = 1 -arity indexByteString = 2 -arity blake2b-256 = 1 - - -arity⋆ : Builtin → ℕ -arity⋆ ifThenElse = 1 -arity⋆ fstPair = 2 -arity⋆ sndPair = 2 -arity⋆ nullList = 1 -arity⋆ headList = 1 -arity⋆ tailList = 1 -arity⋆ chooseList = 2 -arity⋆ chooseData = 1 -arity⋆ chooseUnit = 1 -arity⋆ trace = 1 -arity⋆ _ = 0 open import Type data ScopedTy (n : ℕ) : Set @@ -253,7 +187,7 @@ data ScopedTm {n}(w : Weirdℕ n) : Set where _·_ : ScopedTm w → ScopedTm w → ScopedTm w con : TermCon → ScopedTm w error : ScopedTy n → ScopedTm w - ibuiltin : (b : Builtin) → ScopedTm w + builtin : (b : Builtin) → ScopedTm w wrap : ScopedTy n → ScopedTy n → ScopedTm w → ScopedTm w unwrap : ScopedTm w → ScopedTm w @@ -341,7 +275,7 @@ scopeCheckTm (t · u) = do u ← scopeCheckTm u return (t · u) scopeCheckTm (con c) = return (con c) -scopeCheckTm (builtin b) = return (ibuiltin b) +scopeCheckTm (builtin b) = return (builtin b) scopeCheckTm (error A) = fmap error (scopeCheckTy A) scopeCheckTm (wrap A B t) = do A ← scopeCheckTy A @@ -390,7 +324,7 @@ extricateScope (ƛ A t) = ƛ (extricateScopeTy A) (extricateScope t) extricateScope (t · u) = extricateScope t · extricateScope u extricateScope (con c) = con c extricateScope (error A) = error (extricateScopeTy A) -extricateScope (ibuiltin bn) = builtin bn +extricateScope (builtin bn) = builtin bn extricateScope (wrap pat arg t) = wrap (extricateScopeTy pat) (extricateScopeTy arg) (extricateScope t) extricateScope (unwrap t) = unwrap (extricateScope t) @@ -427,7 +361,7 @@ ugly (Λ _ t) = "(Λ " ++ ugly t ++ ")" ugly (t ·⋆ A) = "( " ++ ugly t ++ " ·⋆ " ++ "TYPE" ++ ")" ugly (con c) = "(con " -- ++ uglyTermCon c ++ ")" -ugly (ibuiltin b) = "builtin " ++ uglyBuiltin b +ugly (builtin b) = "builtin " ++ uglyBuiltin b {- "(builtin " ++ uglyBuiltin b ++ " " ++ diff --git a/plutus-metatheory/src/Scoped/Erasure.lagda b/plutus-metatheory/src/Scoped/Erasure.lagda index 76e4854d222..6d9e0493287 100644 --- a/plutus-metatheory/src/Scoped/Erasure.lagda +++ b/plutus-metatheory/src/Scoped/Erasure.lagda @@ -54,5 +54,5 @@ eraseTm (con c) = con c eraseTm (error A) = error eraseTm (wrap pat arg t) = eraseTm t eraseTm (unwrap t) = eraseTm t -eraseTm (ibuiltin b) = error -- builtin b (≤″⇒≤‴ (≤⇒≤″ z≤n)) [] +eraseTm (builtin b) = error -- builtin b (≤″⇒≤‴ (≤⇒≤″ z≤n)) [] \end{code} diff --git a/plutus-metatheory/src/Scoped/Extrication.lagda b/plutus-metatheory/src/Scoped/Extrication.lagda index 854bc3588d2..9c36f134d29 100644 --- a/plutus-metatheory/src/Scoped/Extrication.lagda +++ b/plutus-metatheory/src/Scoped/Extrication.lagda @@ -86,9 +86,6 @@ extricateC (bool b) = bool b extricateC unit = unit extricateC (Data d) = Data d -open import Data.Product as P -open import Function hiding (_∋_) - extricateSub : ∀ {Γ Δ} → (∀ {J} → Δ ∋⋆ J → Γ ⊢Nf⋆ J) → Scoped.Tel⋆ (len⋆ Γ) (len⋆ Δ) extricateSub {Δ = ∅} σ = [] @@ -97,117 +94,6 @@ extricateSub {Γ}{Δ ,⋆ K} σ = (+-comm (len⋆ Δ) 1) (extricateSub {Δ = Δ} (σ ∘ S) ++ Data.Vec.[ extricateNf⋆ (σ Z) ]) -open import Data.List - -lemma⋆ : ∀ b → len⋆ (proj₁ (ISIG b)) ≡ arity⋆ b -lemma⋆ addInteger = refl -lemma⋆ subtractInteger = refl -lemma⋆ multiplyInteger = refl -lemma⋆ divideInteger = refl -lemma⋆ quotientInteger = refl -lemma⋆ remainderInteger = refl -lemma⋆ modInteger = refl -lemma⋆ lessThanInteger = refl -lemma⋆ lessThanEqualsInteger = refl -lemma⋆ equalsInteger = refl -lemma⋆ appendByteString = refl -lemma⋆ lessThanByteString = refl -lemma⋆ lessThanEqualsByteString = refl -lemma⋆ sha2-256 = refl -lemma⋆ sha3-256 = refl -lemma⋆ verifySignature = refl -lemma⋆ equalsByteString = refl -lemma⋆ ifThenElse = refl -lemma⋆ appendString = refl -lemma⋆ trace = refl -lemma⋆ equalsString = refl -lemma⋆ encodeUtf8 = refl -lemma⋆ decodeUtf8 = refl -lemma⋆ fstPair = refl -lemma⋆ sndPair = refl -lemma⋆ nullList = refl -lemma⋆ headList = refl -lemma⋆ tailList = refl -lemma⋆ chooseList = refl -lemma⋆ constrData = refl -lemma⋆ mapData = refl -lemma⋆ listData = refl -lemma⋆ iData = refl -lemma⋆ bData = refl -lemma⋆ unConstrData = refl -lemma⋆ unMapData = refl -lemma⋆ unListData = refl -lemma⋆ unIData = refl -lemma⋆ unBData = refl -lemma⋆ equalsData = refl -lemma⋆ chooseData = refl -lemma⋆ chooseUnit = refl -lemma⋆ mkPairData = refl -lemma⋆ mkNilData = refl -lemma⋆ mkNilPairData = refl -lemma⋆ mkCons = refl -lemma⋆ consByteString = refl -lemma⋆ sliceByteString = refl -lemma⋆ lengthOfByteString = refl -lemma⋆ indexByteString = refl -lemma⋆ blake2b-256 = refl - -lemma : ∀ b → wtoℕTm (len (proj₁ (proj₂ (ISIG b)))) ≡ Scoped.arity b -lemma addInteger = refl -lemma subtractInteger = refl -lemma multiplyInteger = refl -lemma divideInteger = refl -lemma quotientInteger = refl -lemma remainderInteger = refl -lemma modInteger = refl -lemma lessThanInteger = refl -lemma lessThanEqualsInteger = refl -lemma equalsInteger = refl -lemma appendByteString = refl -lemma lessThanByteString = refl -lemma lessThanEqualsByteString = refl -lemma sha2-256 = refl -lemma sha3-256 = refl -lemma verifySignature = refl -lemma equalsByteString = refl -lemma ifThenElse = refl -lemma appendString = refl -lemma trace = refl -lemma equalsString = refl -lemma encodeUtf8 = refl -lemma decodeUtf8 = refl -lemma fstPair = refl -lemma sndPair = refl -lemma nullList = refl -lemma headList = refl -lemma tailList = refl -lemma chooseList = refl -lemma constrData = refl -lemma mapData = refl -lemma listData = refl -lemma iData = refl -lemma bData = refl -lemma unConstrData = refl -lemma unMapData = refl -lemma unListData = refl -lemma unIData = refl -lemma unBData = refl -lemma equalsData = refl -lemma chooseData = refl -lemma chooseUnit = refl -lemma mkPairData = refl -lemma mkNilData = refl -lemma mkNilPairData = refl -lemma mkCons = refl -lemma consByteString = refl -lemma sliceByteString = refl -lemma lengthOfByteString = refl -lemma indexByteString = refl -lemma blake2b-256 = refl - -≡2≤‴ : ∀{m n} → m ≡ n → m ≤‴ n -≡2≤‴ refl = ≤‴-refl - extricate : ∀{Φ Γ}{A : Φ ⊢Nf⋆ *} → Γ ⊢ A → ScopedTm (len Γ) extricate (` x) = ` (extricateVar x) extricate {Φ}{Γ} (ƛ {A = A} t) = ƛ (extricateNf⋆ A) (extricate t) @@ -218,6 +104,6 @@ extricate {Φ}{Γ} (wrap pat arg t) = wrap (extricateNf⋆ pat) (extricateNf⋆ (extricate t) extricate (unwrap t) = unwrap (extricate t) extricate (con c) = con (extricateC c) -extricate (ibuiltin b) = ibuiltin b +extricate (builtin b) = builtin b extricate {Φ}{Γ} (error A) = error (extricateNf⋆ A) \end{code} diff --git a/plutus-metatheory/src/Scoped/RenamingSubstitution.lagda b/plutus-metatheory/src/Scoped/RenamingSubstitution.lagda index 598e414cd85..aa86a1360e0 100644 --- a/plutus-metatheory/src/Scoped/RenamingSubstitution.lagda +++ b/plutus-metatheory/src/Scoped/RenamingSubstitution.lagda @@ -68,7 +68,7 @@ ren ρ⋆ ρ (ƛ A t) = ƛ (ren⋆ ρ⋆ A) (ren ρ⋆ (lift ρ) t) ren ρ⋆ ρ (t · u) = ren ρ⋆ ρ t · ren ρ⋆ ρ u ren ρ⋆ ρ (con c) = con c ren ρ⋆ ρ (error A) = error (ren⋆ ρ⋆ A) -ren ρ⋆ ρ (ibuiltin b) = ibuiltin b +ren ρ⋆ ρ (builtin b) = builtin b ren ρ⋆ ρ (wrap A B t) = wrap (ren⋆ ρ⋆ A) (ren⋆ ρ⋆ B) (ren ρ⋆ ρ t) ren ρ⋆ ρ (unwrap t) = unwrap (ren ρ⋆ ρ t) @@ -130,7 +130,7 @@ sub σ⋆ σ (ƛ A t) = ƛ (sub⋆ σ⋆ A) (sub σ⋆ (slift σ) t) sub σ⋆ σ (t · u) = sub σ⋆ σ t · sub σ⋆ σ u sub σ⋆ σ (con c) = con c sub σ⋆ σ (error A) = error (sub⋆ σ⋆ A) -sub σ⋆ σ (ibuiltin b) = ibuiltin b +sub σ⋆ σ (builtin b) = builtin b sub σ⋆ σ (wrap A B t) = wrap (sub⋆ σ⋆ A) (sub⋆ σ⋆ B) (sub σ⋆ σ t) sub σ⋆ σ (unwrap t) = unwrap (sub σ⋆ σ t)