From 1f73baff35256f0c5d6de80e4701fdf7c8c8d8a0 Mon Sep 17 00:00:00 2001 From: mjaskelioff Date: Mon, 20 Mar 2023 10:32:37 -0300 Subject: [PATCH] PLT-1345 Simplify bappTermlem / bappTypelem (#5216) The type of BApp is changed, so that bappLemmas can be simplified away. --- plutus-metatheory/plutus-metatheory.cabal | 2 + plutus-metatheory/src/Algorithmic.lagda | 44 +- .../ReductionvsCC.lagda.md | 40 +- plutus-metatheory/src/Algorithmic/CC.lagda.md | 14 +- .../src/Algorithmic/CEK.lagda.md | 942 +++--------------- plutus-metatheory/src/Algorithmic/CK.lagda.md | 15 +- .../src/Algorithmic/Completeness.lagda | 1 + .../Erasure/RenamingSubstitution.lagda | 3 +- .../src/Algorithmic/Reduction.lagda | 48 +- .../src/Algorithmic/ReductionEC.lagda.md | 821 ++------------- .../ReductionEC/Determinism.lagda.md | 34 +- .../Algorithmic/ReductionEC/Progress.lagda.md | 23 +- .../Algorithmic/RenamingSubstitution.lagda | 3 +- .../src/Algorithmic/Signature.lagda.md | 134 +++ .../src/Algorithmic/Soundness.lagda | 1 + plutus-metatheory/src/Builtin.lagda.md | 40 +- .../src/Builtin/Signature.lagda.md | 157 ++- plutus-metatheory/src/Check.lagda.md | 3 +- .../src/Type/BetaNBE/Completeness.lagda | 14 +- .../src/Type/RenamingSubstitution.lagda.md | 10 +- plutus-metatheory/src/Untyped.lagda.md | 1 - plutus-metatheory/src/Untyped/CEK.lagda.md | 238 ++--- plutus-metatheory/src/Utils.lagda | 241 +---- plutus-metatheory/src/index.lagda.md | 13 +- 24 files changed, 802 insertions(+), 2040 deletions(-) create mode 100644 plutus-metatheory/src/Algorithmic/Signature.lagda.md diff --git a/plutus-metatheory/plutus-metatheory.cabal b/plutus-metatheory/plutus-metatheory.cabal index 17e3ec3f6cc..0daf9055ad1 100644 --- a/plutus-metatheory/plutus-metatheory.cabal +++ b/plutus-metatheory/plutus-metatheory.cabal @@ -113,6 +113,7 @@ library MAlonzo.Code.Algorithmic.ReductionEC MAlonzo.Code.Algorithmic.ReductionEC.Progress MAlonzo.Code.Algorithmic.RenamingSubstitution + MAlonzo.Code.Algorithmic.Signature MAlonzo.Code.Builtin MAlonzo.Code.Builtin.Constant.Term MAlonzo.Code.Builtin.Constant.Type @@ -299,6 +300,7 @@ library MAlonzo.Code.Algorithmic.ReductionEC MAlonzo.Code.Algorithmic.ReductionEC.Progress MAlonzo.Code.Algorithmic.RenamingSubstitution + MAlonzo.Code.Algorithmic.Signature MAlonzo.Code.Builtin MAlonzo.Code.Builtin.Constant.Term MAlonzo.Code.Builtin.Constant.Type diff --git a/plutus-metatheory/src/Algorithmic.lagda b/plutus-metatheory/src/Algorithmic.lagda index 17a71a41c67..4a11ea97200 100644 --- a/plutus-metatheory/src/Algorithmic.lagda +++ b/plutus-metatheory/src/Algorithmic.lagda @@ -5,9 +5,7 @@ module Algorithmic where ## Imports \begin{code} -open import Data.List using (List;[];replicate;_++_) open import Relation.Binary.PropositionalEquality using (_≡_;refl) -open import Data.List.NonEmpty using (length) open import Utils hiding (TermCon) open import Type using (Ctx⋆;∅;_,⋆_;_⊢⋆_;_∋⋆_;Z;S;Φ) @@ -17,19 +15,18 @@ open import Type.BetaNormal using (_⊢Nf⋆_;_⊢Ne⋆_;weakenNf;renNf;embNf) open _⊢Nf⋆_ open _⊢Ne⋆_ -import Type.RenamingSubstitution as ⋆ using (Ren) +import Type.RenamingSubstitution as ⋆ open import Type.BetaNBE using (nf) -open import Type.BetaNBE.RenamingSubstitution using (subNf;SubNf) renaming (_[_]Nf to _[_]) +open import Type.BetaNBE.RenamingSubstitution renaming (_[_]Nf to _[_]) -open import Builtin using (Builtin;signature) -open Builtin.Builtin -open import Builtin.Signature using (Sig;sig;nat2Ctx⋆;fin2∈⋆) +open import Builtin using (Builtin) open import Builtin.Constant.Term Ctx⋆ Kind * _⊢Nf⋆_ con using (TermCon) open import Builtin.Constant.Type Ctx⋆ (_⊢Nf⋆ *) using (TyCon) open TyCon -open Builtin.Signature.FromSig Ctx⋆ (_⊢Nf⋆ *) nat2Ctx⋆ (λ x → ne (` (fin2∈⋆ x))) con _⇒_ Π using (sig2type) +open import Algorithmic.Signature using (btype) + \end{code} ## Fixity declarations @@ -91,6 +88,7 @@ data _∋_ : (Γ : Ctx Φ) → Φ ⊢Nf⋆ * → Set where ------------------- → Γ ,⋆ K ∋ weakenNf A \end{code} + Let `x`, `y` range over variables. ## Terms @@ -100,12 +98,6 @@ an abstraction, an application, a type abstraction, or a type application. \begin{code} -btype : Builtin → Φ ⊢Nf⋆ * -btype b = subNf (λ()) (sig2type (signature b)) - -postulate btype-ren : ∀{Φ Ψ} b (ρ : ⋆.Ren Φ Ψ) → btype b ≡ renNf ρ (btype b) -postulate btype-sub : ∀{Φ Ψ} b (ρ : SubNf Φ Ψ) → btype b ≡ subNf ρ (btype b) - infixl 7 _·⋆_/_ data _⊢_ (Γ : Ctx Φ) : Φ ⊢Nf⋆ * → Set where @@ -188,26 +180,4 @@ conv⊢ : ∀ {Γ Γ'}{A A' : Φ ⊢Nf⋆ *} → Γ ⊢ A → Γ' ⊢ A' conv⊢ refl refl t = t - -Ctx2type : (Γ : Ctx Φ) → Φ ⊢Nf⋆ * → ∅ ⊢Nf⋆ * -Ctx2type ∅ C = C -Ctx2type (Γ ,⋆ J) C = Ctx2type Γ (Π C) -Ctx2type (Γ , x) C = Ctx2type Γ (x ⇒ C) - -data Arg : Set where - Term Type : Arg - -Arity = List Arg - -arity : Builtin → Arity -arity b with signature b -... | sig n ar _ = replicate n Type ++ replicate (length ar) Term - -\end{code} - -When signatures supported universal quantifiers to be interleaved with other -parameters it made sense for `Arity` to be defined as above. Now that we don't, -`Arity` should be rewritten to be two numbers (`n` and `length ar` above), representing -the number of quantifiers and the number of (term) parameters. -We keep `Arity` this way in order to make the current implementation works, -but it will be changed. \ No newline at end of file +\end{code} \ No newline at end of file diff --git a/plutus-metatheory/src/Algorithmic/BehaviouralEquivalence/ReductionvsCC.lagda.md b/plutus-metatheory/src/Algorithmic/BehaviouralEquivalence/ReductionvsCC.lagda.md index ff1c6c1ebeb..d03dd00bac1 100644 --- a/plutus-metatheory/src/Algorithmic/BehaviouralEquivalence/ReductionvsCC.lagda.md +++ b/plutus-metatheory/src/Algorithmic/BehaviouralEquivalence/ReductionvsCC.lagda.md @@ -645,17 +645,17 @@ unwindVE : ∀{A B C}(M : ∅ ⊢ A)(N : ∅ ⊢ B)(E : EC C B)(E' : EC B A) unwindVE A B E E' refl VM VN with dissect E' | inspect dissect E' ... | inj₁ refl | I[ eq ] rewrite dissect-inj₁ E' refl eq rewrite uniqueVal A VM VN = base ... | inj₂ (_ ,, E'' ,, (V-ƛ M ·-)) | I[ eq ] rewrite dissect-inj₂ E' E'' (V-ƛ M ·-) eq = ⊥-elim (lemVβ (lemVE _ E'' (subst Value (extEC-[]ᴱ E'' (V-ƛ M ·-) A) VN))) -unwindVE A .(E' [ A ]ᴱ) E E' refl VM VN | inj₂ (_ ,, E'' ,, (V-I⇒ b {as' = []} p x ·-)) | I[ eq ] rewrite dissect-inj₂ E' E'' (V-I⇒ b p x ·-) eq = ⊥-elim (valred (lemVE _ E'' (subst Value (extEC-[]ᴱ E'' (V-I⇒ b p x ·-) A) VN)) (β-sbuiltin b (deval (V-I⇒ b p x)) p x A VM)) +unwindVE A .(E' [ A ]ᴱ) E E' refl VM VN | inj₂ (_ ,, E'' ,, (V-I⇒ b {as' = []} p x ·-)) | I[ eq ] rewrite dissect-inj₂ E' E'' (V-I⇒ b p x ·-) eq = ⊥-elim (valred (lemVE _ E'' (subst Value (extEC-[]ᴱ E'' (V-I⇒ b p x ·-) A) VN)) (β-builtin b (deval (V-I⇒ b p x)) p x A VM)) unwindVE A .(E' [ A ]ᴱ) E E' refl VM VN | inj₂ (_ ,, E'' ,, (V-I⇒ b {as' = x₁ ∷ as'} p x ·-)) | I[ eq ] rewrite dissect-inj₂ E' E'' (V-I⇒ b p x ·-) eq = step* (trans (cong (λ E → stepV VM (dissect E)) (compEC'-extEC E E'' (V-I⇒ b p x ·-))) (cong (stepV VM) (dissect-lemma (compEC' E E'') (V-I⇒ b p x ·-)))) (unwindVE _ _ E E'' (extEC-[]ᴱ E'' (V-I⇒ b p x ·-) A) (V-I b (bubble p) (step p x VM)) VN) unwindVE .(Λ M) .(E' [ Λ M ]ᴱ) E E' refl (V-Λ M) VN | inj₂ (_ ,, E'' ,, -·⋆ C) | I[ eq ] rewrite dissect-inj₂ E' E'' (-·⋆ C) eq = ⊥-elim (lemVβ⋆ (lemVE _ E'' (subst Value (extEC-[]ᴱ E'' (-·⋆ C) (Λ M)) VN))) -unwindVE A .(E' [ A ]ᴱ) E E' refl (V-IΠ b {as' = []} p x) VN | inj₂ (_ ,, E'' ,, -·⋆ C) | I[ eq ] rewrite dissect-inj₂ E' E'' (-·⋆ C) eq = ⊥-elim (valred (lemVE _ E'' (subst Value (extEC-[]ᴱ E'' (-·⋆ C) A) VN)) (β-sbuiltin⋆ b A p x C refl)) +unwindVE A .(E' [ A ]ᴱ) E E' refl (V-IΠ b {as' = []} p x) VN | inj₂ (_ ,, E'' ,, -·⋆ C) | I[ eq ] rewrite dissect-inj₂ E' E'' (-·⋆ C) eq = ⊥-elim (valred (lemVE _ E'' (subst Value (extEC-[]ᴱ E'' (-·⋆ C) A) VN)) (β-builtin⋆ b A p x C refl)) unwindVE A .(E' [ A ]ᴱ) E E' refl (V-IΠ b {as' = a ∷ as'} p x) VN | inj₂ (_ ,, E'' ,, -·⋆ C) | I[ eq ] rewrite dissect-inj₂ E' E'' (-·⋆ C) eq = step* (trans (cong (λ E → stepV _ (dissect E)) (compEC'-extEC E E'' (-·⋆ C))) (cong (stepV (V-IΠ b p x)) (dissect-lemma (compEC' E E'') (-·⋆ C)))) (unwindVE _ _ E E'' (extEC-[]ᴱ E'' (-·⋆ C) A) (V-I b (bubble p) (step⋆ p x refl)) VN) ... | inj₂ (_ ,, E'' ,, wrap-) | I[ eq ] rewrite dissect-inj₂ E' E'' wrap- eq = step* (trans (cong (λ E → stepV VM (dissect E)) (compEC'-extEC E E'' wrap-)) (cong (stepV VM) (dissect-lemma (compEC' E E'') wrap-))) (unwindVE _ _ E E'' (extEC-[]ᴱ E'' wrap- A) (V-wrap VM) VN) unwindVE .(wrap _ _ _) .(E' [ wrap _ _ _ ]ᴱ) E E' refl (V-wrap VM) VN | inj₂ (_ ,, E'' ,, unwrap-) | I[ eq ] rewrite dissect-inj₂ E' E'' unwrap- eq = ⊥-elim (valred (lemVE _ E'' (subst Value (extEC-[]ᴱ E'' unwrap- (deval (V-wrap VM))) VN)) (β-wrap VM refl)) unwindVE .(ƛ M) .(E' [ ƛ M ]ᴱ) E E' refl (V-ƛ M) VN | inj₂ (_ ,, E'' ,, (-· M')) | I[ eq ] rewrite dissect-inj₂ E' E'' (-· M') eq = ⊥-elim (lemVβ (lemVE (ƛ M · M') E'' (subst Value (extEC-[]ᴱ E'' (-· M') (ƛ M)) VN))) -unwindVE A .(E' [ A ]ᴱ) E E' refl V@(V-I⇒ b {as' = []} p x) VN | inj₂ (_ ,, E'' ,, (-· M')) | I[ eq ] rewrite dissect-inj₂ E' E'' (-· M') eq = ⊥-elim (valred (lemVE _ E'' (subst Value (extEC-[]ᴱ E'' (-· M') A) VN)) (β-sbuiltin b A p x M' (lemVE _ (extEC E'' (V ·-)) (subst Value (trans (extEC-[]ᴱ E'' (-· M') A) (sym (extEC-[]ᴱ E'' (V ·-) M'))) VN)))) +unwindVE A .(E' [ A ]ᴱ) E E' refl V@(V-I⇒ b {as' = []} p x) VN | inj₂ (_ ,, E'' ,, (-· M')) | I[ eq ] rewrite dissect-inj₂ E' E'' (-· M') eq = ⊥-elim (valred (lemVE _ E'' (subst Value (extEC-[]ᴱ E'' (-· M') A) VN)) (β-builtin b A p x M' (lemVE _ (extEC E'' (V ·-)) (subst Value (trans (extEC-[]ᴱ E'' (-· M') A) (sym (extEC-[]ᴱ E'' (V ·-) M'))) VN)))) unwindVE A .(E' [ A ]ᴱ) E E' refl V@(V-I⇒ b {as' = a ∷ as'} p x) VN | inj₂ (_ ,, E'' ,, (-· M')) | I[ eq ] rewrite dissect-inj₂ E' E'' (-· M') eq = step* (trans (cong (λ E → stepV (V-I⇒ b p x) (dissect E)) (compEC'-extEC E E'' (-· M'))) (cong (stepV (V-I⇒ b p x)) (dissect-lemma (compEC' E E'') (-· M')))) (step** (lemV M' (lemVE M' (extEC E'' (V-I⇒ b p x ·-)) (subst Value (trans (extEC-[]ᴱ E'' (-· M') A) (sym (extEC-[]ᴱ E'' (V-I⇒ b p x ·-) M'))) VN)) (extEC (compEC' E E'') (V-I⇒ b p x ·-))) (step* (cong (stepV _) (dissect-lemma (compEC' E E'') (V-I⇒ b p x ·-))) ((unwindVE (A · M') _ E E'' (extEC-[]ᴱ E'' (-· M') A) (V-I b (bubble p) (step p x (lemVE M' (extEC E'' (V-I⇒ b p x ·-)) @@ -739,8 +739,8 @@ refocus E M V@(V-I⇒ b {as' = []} p₁ x) E₁ L r p | inj₂ (_ ,, E₂ ,, (- ... | done VEM = ⊥-elim (valredex (lemVE L E₁ (subst Value p VEM)) r) ... | step ¬VEM E₃ x₂ x₃ U rewrite dissect-inj₂ E E₂ (-· N) eq with U E₁ p r -... | refl ,, refl ,, refl with U E₂ (extEC-[]ᴱ E₂ (-· N) M) (β (β-sbuiltin b M p₁ x N VN)) -... | refl ,, refl ,, refl = locate E₂ (-· N) [] refl V (λ V → valred V (β-sbuiltin b M p₁ x N VN)) [] (sym (extEC-[]ᴱ E₂ (-· N) M)) +... | refl ,, refl ,, refl with U E₂ (extEC-[]ᴱ E₂ (-· N) M) (β (β-builtin b M p₁ x N VN)) +... | refl ,, refl ,, refl = locate E₂ (-· N) [] refl V (λ V → valred V (β-builtin b M p₁ x N VN)) [] (sym (extEC-[]ᴱ E₂ (-· N) M)) refocus E M (V-I⇒ b {as' = x₁ ∷ as'} p₁ x) E₁ L r p | inj₂ (_ ,, E₂ ,, (-· N)) | I[ eq ] | done VN rewrite dissect-inj₂ E E₂ (-· N) eq with refocus E₂ (M · N) (V-I b (bubble p₁) (step p₁ x VN)) E₁ L r (trans (sym (extEC-[]ᴱ E₂ (-· N) M)) p) ... | locate E₃ F E₄ x₂ x₃ x₄ E₅ x₅ = locate E₃ @@ -766,8 +766,8 @@ refocus E M VM E₁ L r p | inj₂ (_ ,, E₂ ,, (V@(V-I⇒ b {as' = []} p₁ x) ⊥-elim (valredex (lemVE L E₁ (subst Value p VEM)) r) ... | step ¬VEM E₃ x₁ x₂ U rewrite dissect-inj₂ E E₂ (V ·-) eq with U E₁ p r -... | refl ,, refl ,, refl with U E₂ (extEC-[]ᴱ E₂ (V ·-) M) (β (β-sbuiltin b _ p₁ x M VM)) -... | refl ,, refl ,, refl = locate E₂ (V ·-) [] refl VM (λ V → valred V (β-sbuiltin b _ p₁ x M VM)) [] (sym (extEC-[]ᴱ E₂ (V ·-) M)) +... | refl ,, refl ,, refl with U E₂ (extEC-[]ᴱ E₂ (V ·-) M) (β (β-builtin b _ p₁ x M VM)) +... | refl ,, refl ,, refl = locate E₂ (V ·-) [] refl VM (λ V → valred V (β-builtin b _ p₁ x M VM)) [] (sym (extEC-[]ᴱ E₂ (V ·-) M)) refocus E M VM E₁ L r p | inj₂ (_ ,, E₂ ,, _·- {t = t} (V@(V-I⇒ b {as' = _ ∷ as'} p₁ x))) | I[ eq ] rewrite dissect-inj₂ E E₂ (V ·-) eq with refocus E₂ (t · M) (V-I b (bubble p₁) (step p₁ x VM)) E₁ L r (trans (sym (extEC-[]ᴱ E₂ (V ·-) M)) p) ... | locate E₃ F E₄ x₂ x₃ x₄ E₅ x₅ = locate E₃ @@ -788,8 +788,8 @@ refocus E M V@(V-IΠ b {as' = []} p₁ x) E₁ L r p | inj₂ (_ ,, E₂ ,, -· ... | done VEM = ⊥-elim (valredex (lemVE L E₁ (subst Value p VEM)) r) ... | step ¬VEM E₃ x₂ x₃ U rewrite dissect-inj₂ E E₂ (-·⋆ A) eq with U E₁ p r -... | refl ,, refl ,, refl with U E₂ (extEC-[]ᴱ E₂ (-·⋆ A) M) (β (β-sbuiltin⋆ b M p₁ x A refl)) -... | refl ,, refl ,, refl = locate E₂ (-·⋆ A) [] refl V (λ V → valred V (β-sbuiltin⋆ b M p₁ x A refl)) [] (sym (extEC-[]ᴱ E₂ (-·⋆ A) M)) +... | refl ,, refl ,, refl with U E₂ (extEC-[]ᴱ E₂ (-·⋆ A) M) (β (β-builtin⋆ b M p₁ x A refl)) +... | refl ,, refl ,, refl = locate E₂ (-·⋆ A) [] refl V (λ V → valred V (β-builtin⋆ b M p₁ x A refl)) [] (sym (extEC-[]ᴱ E₂ (-·⋆ A) M)) refocus E M (V-IΠ b {as' = _ ∷ as'} p₁ x) E₁ L r p | inj₂ (_ ,, E₂ ,, -·⋆ A) | I[ eq ] rewrite dissect-inj₂ E E₂ (-·⋆ A) eq with refocus E₂ (M ·⋆ A / refl) (V-I b (bubble p₁) (step⋆ p₁ x refl)) E₁ L r (trans (sym (extEC-[]ᴱ E₂ (-·⋆ A) M)) p) ... | locate E₃ F E₄ x₂ x₃ x₄ E₅ x₅ = locate E₃ @@ -829,7 +829,7 @@ lem-→s⋆ E (β-wrap V refl) = step* (step** (lemV _ (V-wrap V) (extEC E unwrap-)) (step* (cong (stepV (V-wrap V)) (dissect-lemma E unwrap-)) base)) -lem-→s⋆ E (β-sbuiltin b t p bt u vu) with bappTermLem b t p bt +lem-→s⋆ E (β-builtin b t p bt u vu) with bappTermLem b t p bt ... | _ ,, _ ,, refl = step* refl (step** (lemV t (V-I⇒ b p bt) (extEC E (-· u))) @@ -837,7 +837,7 @@ lem-→s⋆ E (β-sbuiltin b t p bt u vu) with bappTermLem b t p bt (step** (lemV u vu (extEC E (V-I⇒ b p bt ·-))) (step* (cong (stepV vu) (dissect-lemma E (V-I⇒ b p bt ·-))) base)))) -lem-→s⋆ E (β-sbuiltin⋆ b t p bt A refl) with bappTypeLem b t p bt +lem-→s⋆ E (β-builtin⋆ b t p bt A refl) with bappTypeLem b t p bt ... | _ ,, _ ,, refl = step* refl (step** (lemV t (V-IΠ b p bt) (extEC E (-·⋆ A))) @@ -880,10 +880,10 @@ lemmaF' .(ƛ M) (-· N) E E' L _ (V-ƛ M) (β-ƛ _) ¬VFM x₁ | done VN | step (step* (cong (stepV VN) (dissect-lemma E (V-ƛ M ·-))) (subst (λ E' → (E ▻ (M [ N ])) -→s (E' ▻ (M [ N ]))) x base))) lemmaF' M (-· N) E E' L L' V@(V-I⇒ b {as' = []} p x) r ¬VFM x₁ | done VN with rlemma51! (extEC E (-· N) [ M ]ᴱ) -... | done VMN = ⊥-elim (valred (lemVE _ E (subst Value (extEC-[]ᴱ E (-· N) M) VMN)) (β-sbuiltin b M p x N VN)) -... | step ¬VMN E₁ x₃ x₄ U with U E (extEC-[]ᴱ E (-· N) M) (β (β-sbuiltin b M p x N VN)) +... | done VMN = ⊥-elim (valred (lemVE _ E (subst Value (extEC-[]ᴱ E (-· N) M) VMN)) (β-builtin b M p x N VN)) +... | step ¬VMN E₁ x₃ x₄ U with U E (extEC-[]ᴱ E (-· N) M) (β (β-builtin b M p x N VN)) ... | refl ,, refl ,, refl with U (compEC' E E') x₁ (β r) -lemmaF' M (-· N) E E' .(M · N) _ V@(V-I⇒ b {as' = []} p x) (β-sbuiltin b₁ .M p₁ bt .N vu) ¬VFM x₁ | done VN | step ¬VMN E x₃ x₄ U | refl ,, refl ,, refl | refl ,, q ,, refl with uniqueVal N VN vu | uniqueVal M V (V-I⇒ b₁ p₁ bt) +lemmaF' M (-· N) E E' .(M · N) _ V@(V-I⇒ b {as' = []} p x) (β-builtin b₁ .M p₁ bt .N vu) ¬VFM x₁ | done VN | step ¬VMN E x₃ x₄ U | refl ,, refl ,, refl | refl ,, q ,, refl with uniqueVal N VN vu | uniqueVal M V (V-I⇒ b₁ p₁ bt) ... | refl | refl = step* (cong (stepV V) (dissect-lemma E (-· N))) (step** (lemV N VN (extEC E (V ·-))) @@ -897,9 +897,9 @@ lemmaF' M (V-ƛ M₁ ·-) E E' L L' V x x₁ x₂ | step ¬VƛM₁M E₁ x₃ x ... | refl ,, refl ,, refl with U E (extEC-[]ᴱ E (V-ƛ M₁ ·-) M) (β (β-ƛ V)) lemmaF' M (V-ƛ M₁ ·-) E E' L L' V (β-ƛ _) x₁ x₂ | step ¬VƛM₁M E₁ x₃ x₄ U | refl ,, refl ,, refl | refl ,, q ,, refl = step* (cong (stepV V) (dissect-lemma E (V-ƛ M₁ ·-))) ((subst (λ E' → (E ▻ _) -→s (E' ▻ _)) (sym q) base)) lemmaF' M (V-I⇒ b {as' = x₇ ∷ as'} p x₃ ·-) E E' L L' V x x₁ x₂ | step ¬VNM E₁ x₄ x₅ x₆ = ⊥-elim (x₁ (V-I b (bubble p) (step p x₃ V))) -lemmaF' M (VN@(V-I⇒ b {as' = []} p x₃) ·-) E E' L L' V x x₁ x₂ | step ¬VNM E₁ x₄ x₅ U with U E (extEC-[]ᴱ E (VN ·-) M) (β (β-sbuiltin b _ p x₃ M V)) +lemmaF' M (VN@(V-I⇒ b {as' = []} p x₃) ·-) E E' L L' V x x₁ x₂ | step ¬VNM E₁ x₄ x₅ U with U E (extEC-[]ᴱ E (VN ·-) M) (β (β-builtin b _ p x₃ M V)) ... | refl ,, refl ,, refl with U (compEC' E E') x₂ (β x) -lemmaF' M (VN@(V-I⇒ b {as' = []} p x₃) ·-) E E' L L' V x x₁ x₂ | step ¬VNM E₁ x₄ x₅ U | refl ,, refl ,, refl | refl ,, q ,, refl rewrite determinism⋆ x (β-sbuiltin b _ p x₃ M V) = step* +lemmaF' M (VN@(V-I⇒ b {as' = []} p x₃) ·-) E E' L L' V x x₁ x₂ | step ¬VNM E₁ x₄ x₅ U | refl ,, refl ,, refl | refl ,, q ,, refl rewrite determinism⋆ x (β-builtin b _ p x₃ M V) = step* (cong (stepV V) (dissect-lemma E (VN ·-))) (subst (λ E' → (E ▻ _) -→s (E' ▻ _)) q base) lemmaF' M (-·⋆ A) E E' L L' V x x₁ x₂ with rlemma51! (extEC E (-·⋆ A) [ M ]ᴱ) @@ -909,8 +909,8 @@ lemmaF' .(Λ M) (-·⋆ A) E E' L L' (V-Λ M) x x₁ x₂ | step ¬VM·⋆A .(co lemmaF' .(Λ M) (-·⋆ A) E E' L L' (V-Λ M) x x₁ x₂ | step ¬VM·⋆A .(compEC' E E') x₃ x₄ U | refl ,, refl ,, refl | refl ,, q ,, refl rewrite determinism⋆ x (β-Λ refl) = step* (cong (stepV (V-Λ M)) (dissect-lemma E (-·⋆ A))) (subst (λ E' → (E ▻ _) -→s (E' ▻ _)) (sym q) base) -lemmaF' M (-·⋆ A) E E' L L' (V-IΠ b {as' = []} p x₅) x x₁ x₂ | step ¬VM·⋆A .(compEC' E E') x₃ x₄ U | refl ,, refl ,, refl with U E (extEC-[]ᴱ E (-·⋆ A) M) (β (β-sbuiltin⋆ b M p x₅ A refl)) -lemmaF' M (-·⋆ A) E E' L L' VM@(V-IΠ b {as' = []} p x₅) x x₁ x₂ | step ¬VM·⋆A .(compEC' E E') x₃ x₄ U | refl ,, refl ,, refl | refl ,, q ,, refl rewrite determinism⋆ x (β-sbuiltin⋆ b M p x₅ A refl) = step* +lemmaF' M (-·⋆ A) E E' L L' (V-IΠ b {as' = []} p x₅) x x₁ x₂ | step ¬VM·⋆A .(compEC' E E') x₃ x₄ U | refl ,, refl ,, refl with U E (extEC-[]ᴱ E (-·⋆ A) M) (β (β-builtin⋆ b M p x₅ A refl)) +lemmaF' M (-·⋆ A) E E' L L' VM@(V-IΠ b {as' = []} p x₅) x x₁ x₂ | step ¬VM·⋆A .(compEC' E E') x₃ x₄ U | refl ,, refl ,, refl | refl ,, q ,, refl rewrite determinism⋆ x (β-builtin⋆ b M p x₅ A refl) = step* (cong (stepV VM) (dissect-lemma E (-·⋆ A))) (subst (λ E' → (E ▻ _) -→s (E' ▻ _)) (sym q) base) lemmaF' M (-·⋆ A) E E' L L' (V-IΠ b {as' = x₆ ∷ as'} p x₅) x x₁ x₂ | step ¬VM·⋆A .(compEC' E E') x₃ x₄ U | refl ,, refl ,, refl = ⊥-elim (x₁ (V-I b (bubble p) (step⋆ p x₅ refl))) @@ -998,7 +998,7 @@ thm1bV M W M' E p N V (step* refl q) | inj₂ (_ ,, E' ,, (V-ƛ M₁ ·-)) | I[ (ruleEC E' (β-ƛ W) (trans p (extEC-[]ᴱ E' (V-ƛ M₁ ·-) M)) refl) (thm1b (M₁ [ M ]) _ E' refl N V q) thm1bV M W M' E p N V (step* refl q) | inj₂ (_ ,, E' ,, (VI@(V-I⇒ b {as' = []} p₁ x₁) ·-)) | I[ eq ] rewrite dissect-inj₂ E E' (VI ·-) eq = trans—↠ - (ruleEC E' (β-sbuiltin b _ p₁ x₁ M W) (trans p (extEC-[]ᴱ E' (VI ·-) M)) refl) + (ruleEC E' (β-builtin b _ p₁ x₁ M W) (trans p (extEC-[]ᴱ E' (VI ·-) M)) refl) (thm1b (BUILTIN' b (bubble p₁) (step p₁ x₁ W)) _ E' refl N V q) thm1bV M W M' E p N V (step* refl q) | inj₂ (_ ,, E' ,, (VI@(V-I⇒ b {as' = x₂ ∷ as'} p₁ x₁) ·-)) | I[ eq ] rewrite dissect-inj₂ E E' (VI ·-) eq = thm1bV (_ · M) @@ -1011,7 +1011,7 @@ thm1bV M W M' E p N V (step* refl q) | inj₂ (_ ,, E' ,, (VI@(V-I⇒ b {as' = x q thm1bV .(Λ M) (V-Λ M) M' E p N V (step* refl q) | inj₂ (_ ,, E' ,, -·⋆ A) | I[ eq ] rewrite dissect-inj₂ E E' (-·⋆ A) eq = trans—↠ (ruleEC E' (β-Λ refl) (trans p (extEC-[]ᴱ E' (-·⋆ A) (Λ M))) refl) (thm1b (M [ A ]⋆) _ E' refl N V q) thm1bV M (V-IΠ b {as' = []} p₁ x₁) M' E p N V (step* refl q) | inj₂ (_ ,, E' ,, -·⋆ A) | I[ eq ] rewrite dissect-inj₂ E E' (-·⋆ A) eq = trans—↠ - (ruleEC E' (β-sbuiltin⋆ b _ p₁ x₁ A refl) (trans p (extEC-[]ᴱ E' (-·⋆ A) M)) refl) + (ruleEC E' (β-builtin⋆ b _ p₁ x₁ A refl) (trans p (extEC-[]ᴱ E' (-·⋆ A) M)) refl) (thm1b (BUILTIN' b (bubble p₁) (step⋆ p₁ x₁ refl)) _ E' refl N V q) thm1bV M (V-IΠ b {as' = x₂ ∷ as'} p₁ x₁) M' E p N V (step* refl q) | inj₂ (_ ,, E' ,, -·⋆ A) | I[ eq ] rewrite dissect-inj₂ E E' (-·⋆ A) eq = thm1bV (M ·⋆ A / refl) diff --git a/plutus-metatheory/src/Algorithmic/CC.lagda.md b/plutus-metatheory/src/Algorithmic/CC.lagda.md index ae078e799ab..c170761e0c3 100644 --- a/plutus-metatheory/src/Algorithmic/CC.lagda.md +++ b/plutus-metatheory/src/Algorithmic/CC.lagda.md @@ -11,6 +11,7 @@ module Algorithmic.CC where ## Imports ``` +open import Data.Nat using (suc) open import Relation.Binary.PropositionalEquality using (_≡_;refl) open import Data.Sum using (_⊎_;inj₁;inj₂) open import Data.Product using (Σ;_×_;∃) @@ -84,16 +85,13 @@ stepV : ∀{A B }{M : ∅ ⊢ A}(V : Value M) stepV V (inj₁ refl) = □ V stepV V (inj₂ (_ ,, E ,, (-· N))) = extEC E (V ·-) ▻ N stepV V (inj₂ (_ ,, E ,, (V-ƛ M ·-))) = E ▻ (M [ deval V ]) -stepV V (inj₂ (_ ,, E ,, (V-I⇒ b {as' = []} p q ·-))) = - E ▻ BUILTIN' b (bubble p) (step p q V) -stepV V (inj₂ (_ ,, E ,, (V-I⇒ b {as' = a ∷ as'} p q ·-))) = - E ◅ V-I b (bubble p) (step p q V) +stepV V (inj₂ (_ ,, E ,, (V-I⇒ b {am = 0} q ·-))) = + E ▻ BUILTIN' b (step q V) +stepV V (inj₂ (_ ,, E ,, (V-I⇒ b {am = suc _} q ·-))) = + E ◅ V-I b (step q V) stepV V (inj₂ (_ ,, E ,, wrap-)) = E ◅ V-wrap V stepV (V-Λ M) (inj₂ (_ ,, E ,, -·⋆ A)) = E ▻ (M [ A ]⋆) -stepV (V-IΠ b {as' = []} p q) (inj₂ (_ ,, E ,, -·⋆ A)) = - E ▻ BUILTIN' b (bubble p) (step⋆ p q refl) -stepV (V-IΠ b {as' = a ∷ as'} p q) (inj₂ (_ ,, E ,, -·⋆ A)) = - E ◅ V-I b (bubble p) (step⋆ p q refl) +stepV (V-IΠ b q) (inj₂ (_ ,, E ,, -·⋆ A)) = E ◅ V-I b (step⋆ q refl refl) stepV (V-wrap V) (inj₂ (_ ,, E ,, unwrap-)) = E ▻ deval V -- E ◅ V stepT : ∀{A} → State A → State A diff --git a/plutus-metatheory/src/Algorithmic/CEK.lagda.md b/plutus-metatheory/src/Algorithmic/CEK.lagda.md index 3885df2eb33..02c4f5aee30 100644 --- a/plutus-metatheory/src/Algorithmic/CEK.lagda.md +++ b/plutus-metatheory/src/Algorithmic/CEK.lagda.md @@ -3,12 +3,11 @@ ``` module Algorithmic.CEK where ---open import Data.Empty using (⊥-elim) open import Data.Nat using (ℕ;zero;suc) +open import Data.Nat.Properties using (+-identityʳ) open import Agda.Builtin.String using (primStringFromList; primStringAppend; primStringEquality) open import Function using (_∘_) -open import Data.Product using (∃;proj₁;proj₂) -open import Data.List using ([];_∷_) +--open import Data.Product using (proj₁;proj₂) open import Relation.Binary.PropositionalEquality using (_≡_;refl;sym;cong;trans) renaming (subst to substEq) open import Data.Unit using (⊤;tt) @@ -26,7 +25,8 @@ open _⊢Nf⋆_ open _⊢Ne⋆_ open import Type.BetaNBE using (nf) open import Type.BetaNBE.RenamingSubstitution using (_[_]Nf;subNf-id;subNf-cong;extsNf) -open import Algorithmic using (Ctx;arity;_⊢_;Term;Type;btype;_∋_;conv⊢;builtin_/_) +open import Algorithmic using (Ctx;_⊢_;_∋_;conv⊢;builtin_/_) +open import Algorithmic.Signature using (btype;_[_]SigTy) open Ctx open _⊢_ open _∋_ @@ -40,11 +40,19 @@ open TyCon open import Builtin.Constant.Term Ctx⋆ Kind * _⊢Nf⋆_ con using (TermCon) open TermCon +open import Builtin.Signature using (Sig;sig;Args;_⊢♯;nat2Ctx⋆;fin2∈⋆;args♯) +open Sig + +open Builtin.Signature.FromSig Ctx⋆ (_⊢Nf⋆ *) nat2Ctx⋆ (λ x → ne (` (fin2∈⋆ x))) con _⇒_ Π + using (sig2type;♯2*;SigTy;sig2SigTy;saturatedSigTy;convSigTy) +open SigTy + data Env : Ctx ∅ → Set -data BApp (b : Builtin) : ∀{az}{as} - → az <>> as ∈ arity b - → (A : ∅ ⊢Nf⋆ *) → Set +data BApp (b : Builtin) : + ∀{tn tm tt} → {pt : tn ∔ tm ≣ tt} + → ∀{an am at} → {pa : an ∔ am ≣ at} + → (A : ∅ ⊢Nf⋆ *) → SigTy pt pa A → Set data Value : (A : ∅ ⊢Nf⋆ *) → Set where V-ƛ : ∀ {Γ}{A B : ∅ ⊢Nf⋆ *} @@ -67,29 +75,44 @@ data Value : (A : ∅ ⊢Nf⋆ *) → Set where → (cn : TermCon {∅} (con tcn)) → Value (con tcn) - V-I⇒ : ∀ b {A B as as'} - → (p : as <>> (Term ∷ as') ∈ arity b) - → BApp b p (A ⇒ B) + V-I⇒ : ∀ b {A B}{tn} + → {pt : tn ∔ 0 ≣ fv♯ (signature b)} + → ∀{an am}{pa : an ∔ (suc am) ≣ args♯ (signature b)} + → {σB : SigTy pt (bubble pa) B} + → BApp b (A ⇒ B) (A B⇒ σB) → Value (A ⇒ B) - V-IΠ : ∀ b {K}{B : ∅ ,⋆ K ⊢Nf⋆ *}{as as'} - → (p : as <>> (Type ∷ as') ∈ arity b) - → BApp b p (Π B) + V-IΠ : ∀ b {B : ∅ ,⋆ * ⊢Nf⋆ *} + → ∀{tn tm} {pt : tn ∔ (suc tm) ≣ fv♯ (signature b)} + → ∀{an am}{pa : an ∔ suc am ≣ args♯ (signature b)} + → {σB : SigTy (bubble pt) pa B} + → BApp b (Π B) (sucΠ σB) → Value (Π B) data BApp b where - base : BApp b (start (arity b)) (btype b) - app : ∀{A B}{az as} - → (p : az <>> (Term ∷ as) ∈ arity b) - → BApp b p (A ⇒ B) - → Value A → BApp b (bubble p) B - app⋆ : ∀{B C}{az as} - → (p : az <>> (Type ∷ as) ∈ arity b) - → BApp b p (Π B) - → {A : ∅ ⊢Nf⋆ K} + base : BApp b (sig2type (signature b)) (sig2SigTy (signature b)) + app : ∀{A B}{tn} + → {pt : tn ∔ 0 ≣ fv♯ (signature b)} + → ∀{an am}{pa : an ∔ suc am ≣ args♯ (signature b)} + → {σB : SigTy pt (bubble pa) B} + → BApp b (A ⇒ B) (A B⇒ σB) + → Value A + → BApp b B σB + app⋆ : ∀{B C} + → ∀{tn tm} {pt : tn ∔ (suc tm) ≣ fv♯ (signature b)} + → ∀{an am}{pa : an ∔ (suc am) ≣ args♯ (signature b)} + → {σB : SigTy (bubble pt) pa B} + → BApp b (Π B) (sucΠ σB) + → {A : ∅ ⊢Nf⋆ *} → (q : C ≡ B [ A ]Nf) - → BApp b (bubble p) C + → {σC : SigTy (bubble pt) pa C} + → (σq : σC ≡ convSigTy (sym q) (σB [ A ]SigTy)) + → BApp b C σC +``` + +## Environments +``` data Env where [] : Env ∅ _∷_ : ∀{Γ A} → Env Γ → Value A → Env (Γ , A) @@ -97,14 +120,11 @@ data Env where lookup : ∀{Γ A} → Γ ∋ A → Env Γ → Value A lookup Z (ρ ∷ v) = v lookup (S x) (ρ ∷ v) = lookup x ρ +``` -convValue : ∀{A A'}(p : A ≡ A') → Value A → Value A' -convValue refl v = v - -data Error : ∅ ⊢Nf⋆ * → Set where - -- an actual error term - E-error : (A : ∅ ⊢Nf⋆ *) → Error A +## Conversion of Values to Terms +``` discharge : ∀{A} → Value A → ∅ ⊢ A env2sub : ∀{Γ} → Env Γ → Sub (ne ∘ `) Γ ∅ @@ -129,728 +149,125 @@ dischargeBody⋆ {A = A} M ρ = conv⊢ (subNf-id A)) (sub (extsNf (ne ∘ `)) (exts⋆ (ne ∘ `) (env2sub ρ)) M) - - -dischargeB : ∀{b A}{az}{as}{p : az <>> as ∈ arity b} → BApp b p A → ∅ ⊢ A -dischargeB {b = b} base = builtin b / refl -dischargeB (app p bt vu) = dischargeB bt · discharge vu -dischargeB (app⋆ p bt refl) = dischargeB bt ·⋆ _ / refl +dischargeB : ∀(b : Builtin) + → ∀{tn tm} → {pt : tn ∔ tm ≣ fv♯ (signature b)} + → ∀{an am} → {pa : an ∔ am ≣ args♯ (signature b)} + → ∀{C} → {Cb : SigTy pt pa C} → (bp : BApp b C Cb) + → ∅ ⊢ C +dischargeB b base = builtin b / refl +dischargeB b (app bt x) = dischargeB b bt · discharge x +dischargeB b (app⋆ bt q _) = dischargeB b bt ·⋆ _ / q discharge (V-ƛ M ρ) = ƛ (dischargeBody M ρ) discharge (V-Λ M ρ) = Λ (dischargeBody⋆ M ρ) discharge (V-wrap V) = wrap _ _ (discharge V) discharge (V-con c) = con c -discharge (V-I⇒ b p bt) = dischargeB bt -discharge (V-IΠ b p bt) = dischargeB bt - -BUILTIN : ∀ b {A} → BApp b (saturated (arity b)) A → Either (∅ ⊢Nf⋆ *) (Value A) -BUILTIN addInteger (app _ (app _ base (V-con (integer i))) (V-con (integer i'))) = inj₂ (V-con (integer (i + i'))) -BUILTIN subtractInteger (app _ (app _ base (V-con (integer i))) (V-con (integer i'))) = inj₂ (V-con (integer (i - i'))) -BUILTIN multiplyInteger (app _ (app _ base (V-con (integer i))) (V-con (integer i'))) = inj₂ (V-con (integer (i ** i'))) -BUILTIN divideInteger (app _ (app _ base (V-con (integer i))) (V-con (integer i'))) = decIf +discharge (V-I⇒ b bt) = dischargeB b bt +discharge (V-IΠ b bt) = dischargeB b bt +``` + +## Builtin Semantics + +``` +BUILTIN : ∀ b {A} → {Ab : saturatedSigTy (signature b) A} → BApp b A Ab → Either (∅ ⊢Nf⋆ *) (Value A) +BUILTIN addInteger (app (app base (V-con (integer i))) (V-con (integer i'))) = inj₂ (V-con (integer (i + i'))) +BUILTIN subtractInteger (app (app base (V-con (integer i))) (V-con (integer i'))) = inj₂ (V-con (integer (i - i'))) +BUILTIN multiplyInteger (app (app base (V-con (integer i))) (V-con (integer i'))) = inj₂ (V-con (integer (i ** i'))) +BUILTIN divideInteger (app (app base (V-con (integer i))) (V-con (integer i'))) = decIf (i' ≟ ℤ.pos 0) (inj₁ (con integer)) (inj₂ (V-con (integer (div i i')))) -BUILTIN quotientInteger (app _ (app _ base (V-con (integer i))) (V-con (integer i'))) = decIf +BUILTIN quotientInteger (app (app base (V-con (integer i))) (V-con (integer i'))) = decIf (i' ≟ ℤ.pos 0) (inj₁ (con integer)) (inj₂ (V-con (integer (quot i i')))) -BUILTIN remainderInteger (app _ (app _ base (V-con (integer i))) (V-con (integer i'))) = decIf +BUILTIN remainderInteger (app (app base (V-con (integer i))) (V-con (integer i'))) = decIf (i' ≟ ℤ.pos 0) (inj₁ (con integer)) (inj₂ (V-con (integer (rem i i')))) -BUILTIN modInteger (app _ (app _ base (V-con (integer i))) (V-con (integer i'))) = decIf +BUILTIN modInteger (app (app base (V-con (integer i))) (V-con (integer i'))) = decIf (i' ≟ ℤ.pos 0) (inj₁ (con integer)) (inj₂ (V-con (integer (mod i i')))) -BUILTIN lessThanInteger (app _ (app _ base (V-con (integer i))) (V-con (integer i'))) = decIf (i > as ∈ arity b) - → ∀{A} - → BApp b p A - → BApp b p' A -convBApp b p p' q rewrite unique<>> p p' = q - -BUILTIN' : ∀ b {A}{az}(p : az <>> [] ∈ arity b) - → BApp b p A +BUILTIN _ {A = A} _ = inj₁ A + +BUILTIN' : ∀ b {A} + → ∀{tn} → {pt : tn ∔ 0 ≣ fv♯ (signature b)} + → ∀{an} → {pa : an ∔ 0 ≣ args♯ (signature b)} + → {σA : SigTy pt pa A} + → BApp b A σA → ∅ ⊢ A -BUILTIN' b {az = az} p q - with sym (trans (cong ([] <><_) (sym (<>>2<>>' _ _ _ p))) (lemma<>2 az [])) -... | refl with BUILTIN b (convBApp b p (saturated (arity b)) q) -... | inj₂ V = discharge V +BUILTIN' b {pt = pt} {pa = pa} bt with trans (sym (+-identityʳ _)) (∔2+ pt) | trans (sym (+-identityʳ _)) (∔2+ pa) +... | refl | refl with unique∔ pt (alldone (fv♯ (signature b))) | unique∔ pa (alldone (args♯ (signature b))) +... | refl | refl with BUILTIN b bt ... | inj₁ A = error _ +... | inj₂ V = discharge V +``` -bappTermLem : ∀ b {A}{az as}(p : az <>> (Term ∷ as) ∈ arity b) - → BApp b p A → ∃ λ A' → ∃ λ A'' → A ≡ A' ⇒ A'' -bappTermLem addInteger _ base = _ ,, _ ,, refl -bappTermLem addInteger {as = as} .(bubble p) (app {az = az} p q x) - with <>>-cancel-both az (([] :< Term) :< Term) as p -bappTermLem addInteger {as = .[]} (bubble (start .(Term ∷ Term ∷ []))) (app {az = _} (start .(Term ∷ Term ∷ [])) base x) - | refl ,, refl = _ ,, _ ,, refl -bappTermLem addInteger {as = as} .(bubble p) (app⋆ {az = az} p q q₁) - with <>>-cancel-both' az (([] :< Type) :< Term) (([] :< Term) :< Term) as p refl -... | refl ,, refl ,, () -bappTermLem subtractInteger _ base = _ ,, _ ,, refl -bappTermLem subtractInteger {as = as} .(bubble p) (app {az = az} p q x) - with <>>-cancel-both az (([] :< Term) :< Term) as p -bappTermLem subtractInteger {as = .[]} (bubble (start .(Term ∷ Term ∷ []))) (app {az = _} (start .(Term ∷ Term ∷ [])) base x) - | refl ,, refl = _ ,, _ ,, refl -bappTermLem subtractInteger {as = as} (bubble p) (app⋆ {az = az} p q q₁) - with <>>-cancel-both' az (([] :< Type) :< Term) (([] :< Term) :< Term) as p refl -... | refl ,, refl ,, () -bappTermLem multiplyInteger _ base = _ ,, _ ,, refl -bappTermLem multiplyInteger {as = as} .(bubble p) (app {az = az} p q x) - with <>>-cancel-both az (([] :< Term) :< Term) as p -bappTermLem multiplyInteger {as = .[]} (bubble (start .(Term ∷ Term ∷ []))) (app {az = _} (start .(Term ∷ Term ∷ [])) base x) - | refl ,, refl = _ ,, _ ,, refl -bappTermLem multiplyInteger {as = as} .(bubble p) (app⋆ {az = az} p q q₁) - with <>>-cancel-both' az (([] :< Type) :< Term) (([] :< Term) :< Term) as p refl -... | refl ,, refl ,, () -bappTermLem divideInteger _ base = _ ,, _ ,, refl -bappTermLem divideInteger {as = as} .(bubble p) (app {az = az} p q x) - with <>>-cancel-both az (([] :< Term) :< Term) as p -bappTermLem divideInteger {as = .[]} (bubble (start .(Term ∷ Term ∷ []))) (app {az = _} (start .(Term ∷ Term ∷ [])) base x) - | refl ,, refl = _ ,, _ ,, refl -bappTermLem divideInteger {as = as} .(bubble p) (app⋆ {az = az} p q q₁) - with <>>-cancel-both' az (([] :< Type) :< Term) (([] :< Term) :< Term) as p refl -... | refl ,, refl ,, () -bappTermLem quotientInteger _ base = _ ,, _ ,, refl -bappTermLem quotientInteger {as = as} .(bubble p) (app {az = az} p q x) - with <>>-cancel-both az (([] :< Term) :< Term) as p -bappTermLem quotientInteger {as = .[]} (bubble (start .(Term ∷ Term ∷ []))) (app {az = _} (start .(Term ∷ Term ∷ [])) base x) - | refl ,, refl = _ ,, _ ,, refl -bappTermLem quotientInteger {as = as} .(bubble p) (app⋆ {az = az} p q q₁) - with <>>-cancel-both' az (([] :< Type) :< Term) (([] :< Term) :< Term) as p refl -... | refl ,, refl ,, () -bappTermLem remainderInteger _ base = _ ,, _ ,, refl -bappTermLem remainderInteger {as = as} .(bubble p) (app {az = az} p q x) - with <>>-cancel-both az (([] :< Term) :< Term) as p -bappTermLem remainderInteger {as = .[]} (bubble (start .(Term ∷ Term ∷ []))) (app {az = _} (start .(Term ∷ Term ∷ [])) base x) - | refl ,, refl = _ ,, _ ,, refl -bappTermLem remainderInteger {as = as} .(bubble p) (app⋆ {az = az} p q q₁) - with <>>-cancel-both' az (([] :< Type) :< Term) (([] :< Term) :< Term) as p refl -... | refl ,, refl ,, () -bappTermLem modInteger _ base = _ ,, _ ,, refl -bappTermLem modInteger {as = as} .(bubble p) (app {az = az} p q x) - with <>>-cancel-both az (([] :< Term) :< Term) as p -bappTermLem modInteger {as = .[]} (bubble (start .(Term ∷ Term ∷ []))) (app {az = _} (start .(Term ∷ Term ∷ [])) base x) - | refl ,, refl = _ ,, _ ,, refl -bappTermLem modInteger {as = as} .(bubble p) (app⋆ {az = az} p q q₁) - with <>>-cancel-both' az (([] :< Type) :< Term) (([] :< Term) :< Term) as p refl -... | refl ,, refl ,, () -bappTermLem lessThanInteger _ base = _ ,, _ ,, refl -bappTermLem lessThanInteger {as = as} .(bubble p) (app {az = az} p q x) - with <>>-cancel-both az (([] :< Term) :< Term) as p -bappTermLem lessThanInteger {as = .[]} (bubble (start .(Term ∷ Term ∷ []))) (app {az = _} (start .(Term ∷ Term ∷ [])) base x) - | refl ,, refl = _ ,, _ ,, refl -bappTermLem lessThanInteger {as = as} .(bubble p) (app⋆ {az = az} p q q₁) - with <>>-cancel-both' az (([] :< Type) :< Term) (([] :< Term) :< Term) as p refl -... | refl ,, refl ,, () -bappTermLem lessThanEqualsInteger _ base = _ ,, _ ,, refl -bappTermLem lessThanEqualsInteger {as = as} .(bubble p) (app {az = az} p q x) - with <>>-cancel-both az (([] :< Term) :< Term) as p -bappTermLem lessThanEqualsInteger {as = .[]} (bubble (start .(Term ∷ Term ∷ []))) (app {az = _} (start .(Term ∷ Term ∷ [])) base x) - | refl ,, refl = _ ,, _ ,, refl -bappTermLem lessThanEqualsInteger {as = as} .(bubble p) (app⋆ {az = az} p q q₁) - with <>>-cancel-both' az (([] :< Type) :< Term) (([] :< Term) :< Term) as p refl -... | refl ,, refl ,, () -bappTermLem equalsInteger _ base = _ ,, _ ,, refl -bappTermLem equalsInteger {as = as} .(bubble p) (app {az = az} p q x) - with <>>-cancel-both az (([] :< Term) :< Term) as p -bappTermLem equalsInteger {as = .[]} (bubble (start .(Term ∷ Term ∷ []))) (app {az = _} (start .(Term ∷ Term ∷ [])) base x) - | refl ,, refl = _ ,, _ ,, refl -bappTermLem equalsInteger {as = as} .(bubble p) (app⋆ {az = az} p q q₁) - with <>>-cancel-both' az (([] :< Type) :< Term) (([] :< Term) :< Term) as p refl -... | refl ,, refl ,, () -bappTermLem appendByteString _ base = _ ,, _ ,, refl -bappTermLem appendByteString {as = as} .(bubble p) (app {az = az} p q x) - with <>>-cancel-both az (([] :< Term) :< Term) as p -bappTermLem appendByteString {as = .[]} (bubble (start .(Term ∷ Term ∷ []))) (app {az = _} (start .(Term ∷ Term ∷ [])) base x) - | refl ,, refl = _ ,, _ ,, refl -bappTermLem appendByteString {as = as} .(bubble p) (app⋆ {az = az} p q q₁) - with <>>-cancel-both' az (([] :< Type) :< Term) (([] :< Term) :< Term) as p refl -... | refl ,, refl ,, () -bappTermLem lessThanByteString _ base = _ ,, _ ,, refl -bappTermLem lessThanByteString {as = as} .(bubble p) (app {az = az} p q x) - with <>>-cancel-both az (([] :< Term) :< Term) as p -bappTermLem lessThanByteString {as = .[]} (bubble (start .(Term ∷ Term ∷ []))) (app {az = _} (start .(Term ∷ Term ∷ [])) base x) - | refl ,, refl = _ ,, _ ,, refl -bappTermLem lessThanByteString {as = as} .(bubble p) (app⋆ {az = az} p q q₁) - with <>>-cancel-both' az (([] :< Type) :< Term) (([] :< Term) :< Term) as p refl -... | refl ,, refl ,, () - -bappTermLem lessThanEqualsByteString _ base = _ ,, _ ,, refl -bappTermLem lessThanEqualsByteString {as = as} .(bubble p) (app {az = az} p q x) - with <>>-cancel-both az (([] :< Term) :< Term) as p -bappTermLem lessThanEqualsByteString {as = .[]} (bubble (start .(Term ∷ Term ∷ []))) (app {az = _} (start .(Term ∷ Term ∷ [])) base x) - | refl ,, refl = _ ,, _ ,, refl -bappTermLem lessThanEqualsByteString {as = as} .(bubble p) (app⋆ {az = az} p q q₁) - with <>>-cancel-both' az (([] :< Type) :< Term) (([] :< Term) :< Term) as p refl -... | refl ,, refl ,, () -bappTermLem sha2-256 {az = az} {as} p q with <>>-cancel-both az ([] :< Term) as p -bappTermLem sha2-256 {az = .[]} {.[]} .(start (Term ∷ [])) base | refl ,, refl = _ ,, _ ,, refl -bappTermLem sha3-256 {az = az} {as} p q with <>>-cancel-both az ([] :< Term) as p -bappTermLem sha3-256 {az = .[]} {.[]} .(start (Term ∷ [])) base | refl ,, refl = _ ,, _ ,, refl -bappTermLem verifyEd25519Signature .(start (Term ∷ Term ∷ Term ∷ [])) base = _ ,, _ ,, refl -bappTermLem verifyEd25519Signature .(bubble (start (Term ∷ Term ∷ Term ∷ []))) (app .(start (Term ∷ Term ∷ Term ∷ [])) base x) = _ ,, _ ,, refl -bappTermLem verifyEd25519Signature {as = as} .(bubble (bubble p)) (app .(bubble p) (app {az = az} p q x₁) x) with <>>-cancel-both az ((([] :< Term) :< Term) :< Term) as p -bappTermLem verifyEd25519Signature {as = .[]} (bubble (bubble .(start (Term ∷ Term ∷ Term ∷ [])))) (app .(bubble (start (Term ∷ Term ∷ Term ∷ []))) (app {az = _} .(start (Term ∷ Term ∷ Term ∷ [])) base x₁) x) | refl ,, refl = _ ,, _ ,, refl -bappTermLem verifyEd25519Signature {as = as} .(bubble (bubble p)) (app .(bubble p) (app⋆ {az = az} p q q₁₁) x) with <>>-cancel-both' az ((([] :< Type) :< Term) :< Term) ((([] :< Term) :< Term) :< Term) as p refl -... | refl ,, refl ,, () -bappTermLem verifyEd25519Signature {as = as} .(bubble (bubble p)) (app⋆ .(bubble p) (app {az = az} p q x₁) q₁) with <>>-cancel-both' az ((([] :< Term) :< Type) :< Term) ((([] :< Term) :< Term) :< Term) as p refl -... | refl ,, refl ,, () -bappTermLem verifyEd25519Signature {as = as} .(bubble (bubble p)) (app⋆ .(bubble p) (app⋆ {az = az} p q q₂) q₁) with <>>-cancel-both' az ((([] :< Type) :< Type) :< Term) ((([] :< Term) :< Term) :< Term) as p refl -... | refl ,, refl ,, () -bappTermLem verifyEcdsaSecp256k1Signature .(start (Term ∷ Term ∷ Term ∷ [])) base = _ ,, _ ,, refl -bappTermLem verifyEcdsaSecp256k1Signature .(bubble (start (Term ∷ Term ∷ Term ∷ []))) (app .(start (Term ∷ Term ∷ Term ∷ [])) base x) = _ ,, _ ,, refl -bappTermLem verifyEcdsaSecp256k1Signature {as = as} .(bubble (bubble p)) (app .(bubble p) (app {az = az} p q x₁) x) with <>>-cancel-both az ((([] :< Term) :< Term) :< Term) as p -bappTermLem verifyEcdsaSecp256k1Signature {as = .[]} (bubble (bubble .(start (Term ∷ Term ∷ Term ∷ [])))) (app .(bubble (start (Term ∷ Term ∷ Term ∷ []))) (app {az = _} .(start (Term ∷ Term ∷ Term ∷ [])) base x₁) x) | refl ,, refl = _ ,, _ ,, refl -bappTermLem verifyEcdsaSecp256k1Signature {as = as} .(bubble (bubble p)) (app .(bubble p) (app⋆ {az = az} p q q₁₁) x) with <>>-cancel-both' az ((([] :< Type) :< Term) :< Term) ((([] :< Term) :< Term) :< Term) as p refl -... | refl ,, refl ,, () -bappTermLem verifyEcdsaSecp256k1Signature {as = as} .(bubble (bubble p)) (app⋆ .(bubble p) (app {az = az} p q x₁) q₁) with <>>-cancel-both' az ((([] :< Term) :< Type) :< Term) ((([] :< Term) :< Term) :< Term) as p refl -... | refl ,, refl ,, () -bappTermLem verifyEcdsaSecp256k1Signature {as = as} .(bubble (bubble p)) (app⋆ .(bubble p) (app⋆ {az = az} p q q₂) q₁) with <>>-cancel-both' az ((([] :< Type) :< Type) :< Term) ((([] :< Term) :< Term) :< Term) as p refl -... | refl ,, refl ,, () -bappTermLem verifySchnorrSecp256k1Signature .(start (Term ∷ Term ∷ Term ∷ [])) base = _ ,, _ ,, refl -bappTermLem verifySchnorrSecp256k1Signature .(bubble (start (Term ∷ Term ∷ Term ∷ []))) (app .(start (Term ∷ Term ∷ Term ∷ [])) base x) = _ ,, _ ,, refl -bappTermLem verifySchnorrSecp256k1Signature {as = as} .(bubble (bubble p)) (app .(bubble p) (app {az = az} p q x₁) x) with <>>-cancel-both az ((([] :< Term) :< Term) :< Term) as p -bappTermLem verifySchnorrSecp256k1Signature {as = .[]} (bubble (bubble .(start (Term ∷ Term ∷ Term ∷ [])))) (app .(bubble (start (Term ∷ Term ∷ Term ∷ []))) (app {az = _} .(start (Term ∷ Term ∷ Term ∷ [])) base x₁) x) | refl ,, refl = _ ,, _ ,, refl -bappTermLem verifySchnorrSecp256k1Signature {as = as} .(bubble (bubble p)) (app .(bubble p) (app⋆ {az = az} p q q₁₁) x) with <>>-cancel-both' az ((([] :< Type) :< Term) :< Term) ((([] :< Term) :< Term) :< Term) as p refl -... | refl ,, refl ,, () -bappTermLem verifySchnorrSecp256k1Signature {as = as} .(bubble (bubble p)) (app⋆ .(bubble p) (app {az = az} p q x₁) q₁) with <>>-cancel-both' az ((([] :< Term) :< Type) :< Term) ((([] :< Term) :< Term) :< Term) as p refl -... | refl ,, refl ,, () -bappTermLem verifySchnorrSecp256k1Signature {as = as} .(bubble (bubble p)) (app⋆ .(bubble p) (app⋆ {az = az} p q q₂) q₁) with <>>-cancel-both' az ((([] :< Type) :< Type) :< Term) ((([] :< Term) :< Term) :< Term) as p refl -... | refl ,, refl ,, () -bappTermLem equalsByteString _ base = _ ,, _ ,, refl -bappTermLem equalsByteString {as = as} .(bubble p) (app {az = az} p q x) - with <>>-cancel-both az (([] :< Term) :< Term) as p -bappTermLem equalsByteString {as = .[]} (bubble (start .(Term ∷ Term ∷ []))) (app {az = _} (start .(Term ∷ Term ∷ [])) base x) - | refl ,, refl = _ ,, _ ,, refl -bappTermLem equalsByteString {as = as} .(bubble p) (app⋆ {az = az} p q q₁) - with <>>-cancel-both' az (([] :< Type) :< Term) (([] :< Term) :< Term) as p refl -... | refl ,, refl ,, () -bappTermLem ifThenElse {as = as} .(bubble (bubble (bubble p))) (app .(bubble (bubble p)) (app .(bubble p) (app {az = az} p q x₂) x₁) x) with <>>-cancel-both' az (((([] :< Term) :< Term) :< Term) :< Term) (((([] :< Type) :< Term) :< Term) :< Term) as p refl -... | refl ,, refl ,, () -bappTermLem ifThenElse {as = as} .(bubble (bubble (bubble p))) (app .(bubble (bubble p)) (app .(bubble p) (app⋆ {az = az} p q q₁) x₁) x) with <>>-cancel-both az (((([] :< Type) :< Term) :< Term) :< Term) as p -bappTermLem ifThenElse {as = .[]} (bubble (bubble (bubble .(start (Type ∷ Term ∷ Term ∷ Term ∷ []))))) (app .(bubble (bubble (start (Type ∷ Term ∷ Term ∷ Term ∷ [])))) (app .(bubble (start (Type ∷ Term ∷ Term ∷ Term ∷ []))) (app⋆ {az = _} .(start (Type ∷ Term ∷ Term ∷ Term ∷ [])) base refl) x₁) x) | refl ,, refl = _ ,, _ ,, refl -bappTermLem ifThenElse .(bubble (bubble (start (Type ∷ Term ∷ Term ∷ Term ∷ [])))) (app .(bubble (start (Type ∷ Term ∷ Term ∷ Term ∷ []))) (app⋆ (start .(Type ∷ Term ∷ Term ∷ Term ∷ [])) base refl) x) = _ ,, _ ,, refl -bappTermLem ifThenElse {as = as} .(bubble (bubble (bubble p))) (app .(bubble (bubble p)) (app⋆ (bubble {as = as₁} p) q q₁₁) x) with <>>-cancel-both' as₁ (((([] :< _) :< Type) :< Term) :< Term) (((([] :< Type) :< Term) :< Term) :< Term)as p refl -... | refl ,, refl ,, () -bappTermLem ifThenElse .(bubble (start (Type ∷ Term ∷ Term ∷ Term ∷ []))) (app⋆ .(start (Type ∷ Term ∷ Term ∷ Term ∷ [])) base refl) = _ ,, _ ,, refl -bappTermLem ifThenElse {as = as} .(bubble (bubble (bubble p))) (app⋆ .(bubble (bubble p)) (app .(bubble p) (app {az = az} p q x₂) x₁) q₁) with <>>-cancel-both' az (((([] :< Term) :< Term) :< Type) :< Term) (((([] :< Type) :< Term) :< Term) :< Term) as p refl -... | refl ,, refl ,, () -bappTermLem ifThenElse {as = as} .(bubble (bubble (bubble p))) (app⋆ .(bubble (bubble p)) (app .(bubble p) (app⋆ {az = az} p q q₂) x₁) q₁) with <>>-cancel-both' az (((([] :< Type) :< Term) :< Type) :< Term) (((([] :< Type) :< Term) :< Term) :< Term) as p refl -... | refl ,, refl ,, () -bappTermLem ifThenElse {as = as} .(bubble (bubble (bubble p))) (app⋆ .(bubble (bubble p)) (app⋆ .(bubble p) (app {az = az} p q x₂) q₂) q₁) with <>>-cancel-both' az (((([] :< Term) :< Type) :< Type) :< Term) (((([] :< Type) :< Term) :< Term) :< Term) as p refl -... | refl ,, refl ,, () -bappTermLem ifThenElse {as = as} .(bubble (bubble (bubble p))) (app⋆ .(bubble (bubble p)) (app⋆ .(bubble p) (app⋆ {az = az} p q q₃) q₂) q₁) with <>>-cancel-both' az (((([] :< Type) :< Type) :< Type) :< Term) (((([] :< Type) :< Term) :< Term) :< Term) as p refl -... | refl ,, refl ,, () -bappTermLem appendString _ base = _ ,, _ ,, refl -bappTermLem appendString {as = as} .(bubble p) (app {az = az} p q x) - with <>>-cancel-both az (([] :< Term) :< Term) as p -bappTermLem appendString {as = .[]} (bubble (start .(Term ∷ Term ∷ []))) (app {az = _} (start .(Term ∷ Term ∷ [])) base x) - | refl ,, refl = _ ,, _ ,, refl -bappTermLem appendString {as = as} .(bubble p) (app⋆ {az = az} p q q₁) - with <>>-cancel-both' az (([] :< Type) :< Term) (([] :< Term) :< Term) as p refl -... | refl ,, refl ,, () -bappTermLem trace (bubble (start _)) (app⋆ _ base refl) = _ ,, _ ,, refl -bappTermLem trace {as = as} (bubble (bubble {as = az} p)) q - with <>>-cancel-both' az _ ([] <>< arity trace) _ p refl -bappTermLem trace (bubble (bubble (start _))) (app _ (app⋆ _ base refl) v) | refl ,, refl ,, refl = _ ,, _ ,, refl -bappTermLem equalsString (start _) base = _ ,, _ ,, refl -bappTermLem equalsString {as = as} (bubble {as = az} p) q - with <>>-cancel-both' az _ (([] :< Term) :< Term) as p refl -bappTermLem equalsString (bubble (start _)) (app _ base _) - | refl ,, refl ,, refl = _ ,, _ ,, refl -bappTermLem encodeUtf8 {az = az} {as} p q - with <>>-cancel-both az ([] :< Term) as p -bappTermLem encodeUtf8 (start _) base | refl ,, refl = _ ,, _ ,, refl -bappTermLem decodeUtf8 {az = az} {as} p q - with <>>-cancel-both az ([] :< Term) as p -bappTermLem decodeUtf8 (start _) base | refl ,, refl = _ ,, _ ,, refl -bappTermLem fstPair (bubble (bubble {as = az} p)) q - with <>>-cancel-both' az _ ([] <>< arity fstPair) _ p refl -bappTermLem fstPair - (bubble (bubble (start _))) - (app⋆ _ (app⋆ _ base refl) refl) - | refl ,, refl ,, refl = _ ,, _ ,, refl -bappTermLem sndPair (bubble (bubble {as = az} p)) q - with <>>-cancel-both' az _ ([] <>< arity fstPair) _ p refl -bappTermLem sndPair - (bubble (bubble (start _))) - (app⋆ _ (app⋆ _ base refl) refl) - | refl ,, refl ,, refl = _ ,, _ ,, refl -bappTermLem nullList (bubble {as = az} p) q - with <>>-cancel-both' az _ ([] <>< arity nullList) _ p refl -bappTermLem nullList (bubble (start _)) (app⋆ _ base refl) - | refl ,, refl ,, refl = _ ,, _ ,, refl -bappTermLem headList (bubble {as = az} p) q - with <>>-cancel-both' az _ ([] <>< arity nullList) _ p refl -bappTermLem headList (bubble (start _)) (app⋆ _ base refl) - | refl ,, refl ,, refl = _ ,, _ ,, refl -bappTermLem tailList (bubble {as = az} p) q - with <>>-cancel-both' az _ ([] <>< arity nullList) _ p refl -bappTermLem tailList (bubble (start _)) (app⋆ _ base refl) - | refl ,, refl ,, refl = _ ,, _ ,, refl -bappTermLem chooseList - (bubble (bubble (start _))) - (app⋆ _ (app⋆ _ base refl) refl) - = _ ,, _ ,, refl -bappTermLem chooseList - (bubble (bubble (bubble (start _)))) - (app _ (app⋆ _ (app⋆ _ base refl) refl) x) - = _ ,, _ ,, refl -bappTermLem chooseList (bubble (bubble (bubble (bubble {as = az} p)))) q - with <>>-cancel-both' az _ ([] <>< arity chooseList) _ p refl -bappTermLem chooseList - (bubble (bubble (bubble (bubble (start _))))) - (app _ (app _ (app⋆ _ (app⋆ _ base refl) refl) _) _) - | refl ,, refl ,, refl = _ ,, _ ,, refl -bappTermLem constrData (start _) base = _ ,, _ ,, refl -bappTermLem constrData {as = as} (bubble {as = az} p) q - with <>>-cancel-both' az _ (([] :< Term) :< Term) as p refl -bappTermLem constrData (bubble (start _)) (app _ base _) - | refl ,, refl ,, refl = _ ,, _ ,, refl -bappTermLem mapData {az = az} {as} p q - with <>>-cancel-both az ([] :< Term) as p -bappTermLem mapData (start _) base | refl ,, refl = _ ,, _ ,, refl -bappTermLem listData {az = az} {as} p q - with <>>-cancel-both az ([] :< Term) as p -bappTermLem listData (start _) base | refl ,, refl = _ ,, _ ,, refl -bappTermLem iData {az = az} {as} p q - with <>>-cancel-both az ([] :< Term) as p -bappTermLem iData (start _) base | refl ,, refl = _ ,, _ ,, refl -bappTermLem bData {az = az} {as} p q - with <>>-cancel-both az ([] :< Term) as p -bappTermLem bData (start _) base | refl ,, refl = _ ,, _ ,, refl -bappTermLem unConstrData {az = az} {as} p q - with <>>-cancel-both az ([] :< Term) as p -bappTermLem unConstrData (start _) base | refl ,, refl = _ ,, _ ,, refl -bappTermLem unMapData {az = az} {as} p q - with <>>-cancel-both az ([] :< Term) as p -bappTermLem unMapData (start _) base | refl ,, refl = _ ,, _ ,, refl -bappTermLem unListData {az = az} {as} p q - with <>>-cancel-both az ([] :< Term) as p -bappTermLem unListData (start _) base | refl ,, refl = _ ,, _ ,, refl -bappTermLem unIData {az = az} {as} p q - with <>>-cancel-both az ([] :< Term) as p -bappTermLem unIData (start _) base | refl ,, refl = _ ,, _ ,, refl -bappTermLem unBData {az = az} {as} p q - with <>>-cancel-both az ([] :< Term) as p -bappTermLem unBData (start _) base | refl ,, refl = _ ,, _ ,, refl -bappTermLem equalsData (start _) base = _ ,, _ ,, refl -bappTermLem equalsData {as = as} (bubble {as = az} p) q - with <>>-cancel-both' az _ (([] :< Term) :< Term) as p refl -bappTermLem equalsData (bubble (start _)) (app _ base _) - | refl ,, refl ,, refl = _ ,, _ ,, refl -bappTermLem serialiseData {az = az} {as} p q - with <>>-cancel-both az ([] :< Term) as p -bappTermLem serialiseData (start _) base | refl ,, refl = _ ,, _ ,, refl -bappTermLem chooseData (bubble (start _)) (app⋆ _ base refl) = - _ ,, _ ,, refl -bappTermLem chooseData - (bubble (bubble (start _))) - (app _ (app⋆ _ base refl) _) - = _ ,, _ ,, refl -bappTermLem chooseData - (bubble (bubble (bubble (start _)))) - (app _ (app _ (app⋆ _ base refl) _) _) - = _ ,, _ ,, refl -bappTermLem chooseData - (bubble (bubble (bubble (bubble (start _))))) - (app _ (app _ (app _ (app⋆ _ base refl) _) _) _) - = _ ,, _ ,, refl -bappTermLem chooseData - (bubble (bubble (bubble (bubble (bubble (start _)))))) - (app _ (app _ (app _ (app _ (app⋆ _ base refl) _) _) _) _) - = _ ,, _ ,, refl -bappTermLem chooseData - (bubble (bubble (bubble (bubble (bubble (bubble {as = az} p)))))) q - with <>>-cancel-both' az _ ([] <>< arity chooseData) _ p refl -bappTermLem - chooseData - (bubble (bubble (bubble (bubble (bubble (bubble (start _))))))) - (app _ (app _ (app _ (app _ (app _ (app⋆ _ base refl)_)_)_)_)_) - | refl ,, refl ,, refl = _ ,, _ ,, refl -bappTermLem chooseUnit (bubble (start _)) (app⋆ _ base refl) = - _ ,, _ ,, refl -bappTermLem chooseUnit (bubble (bubble {as = az} p)) q - with <>>-cancel-both' az _ ((([] :< Type) :< Term) :< Term) _ p refl -bappTermLem chooseUnit - (bubble (bubble (start _))) - (app _ (app⋆ _ base refl) x) - | refl ,, refl ,, refl = _ ,, _ ,, refl -bappTermLem mkPairData (start _) base = _ ,, _ ,, refl -bappTermLem mkPairData {as = as} (bubble {as = az} p) q - with <>>-cancel-both' az _ (([] :< Term) :< Term) as p refl -bappTermLem mkPairData (bubble (start _)) (app _ base _) - | refl ,, refl ,, refl = _ ,, _ ,, refl -bappTermLem mkNilData {az = az} {as} p q - with <>>-cancel-both az ([] :< Term) as p -bappTermLem mkNilData (start _) base | refl ,, refl = _ ,, _ ,, refl -bappTermLem mkNilPairData {az = az} {as} p q - with <>>-cancel-both az ([] :< Term) as p -bappTermLem mkNilPairData (start _) base | refl ,, refl = _ ,, _ ,, refl -bappTermLem mkCons (bubble (start _)) (app⋆ _ base refl) = - _ ,, _ ,, refl -bappTermLem mkCons (bubble (bubble {as = az} p)) q - with <>>-cancel-both' az _ ((([] :< Type) :< Term) :< Term) _ p refl -bappTermLem mkCons - (bubble (bubble (start _))) - (app _ (app⋆ _ base refl) x) - | refl ,, refl ,, refl = _ ,, _ ,, refl -bappTermLem consByteString (start _) base = _ ,, _ ,, refl -bappTermLem consByteString {as = as} (bubble {as = az} p) q - with <>>-cancel-both' az _ (([] :< Term) :< Term) as p refl -bappTermLem consByteString (bubble (start _)) (app _ base _) - | refl ,, refl ,, refl = _ ,, _ ,, refl -bappTermLem sliceByteString (start _) base = _ ,, _ ,, refl -bappTermLem sliceByteString (bubble (start _)) (app (start _) base _) = - _ ,, _ ,, refl -bappTermLem sliceByteString {as = as} (bubble (bubble {as = az} p)) q - with <>>-cancel-both' az _ ((([] :< Term) :< Term) :< Term) as p refl -bappTermLem sliceByteString - (bubble (bubble (start _))) - (app _ (app _ base _) _) - | refl ,, refl ,, refl = _ ,, _ ,, refl -bappTermLem lengthOfByteString {az = az} {as} p q - with <>>-cancel-both az ([] :< Term) as p -bappTermLem lengthOfByteString (start _) base | refl ,, refl = _ ,, _ ,, refl -bappTermLem indexByteString (start _) base = _ ,, _ ,, refl -bappTermLem indexByteString {as = as} (bubble {as = az} p) q - with <>>-cancel-both' az _ (([] :< Term) :< Term) as p refl -bappTermLem indexByteString (bubble (start _)) (app _ base _) - | refl ,, refl ,, refl = _ ,, _ ,, refl -bappTermLem blake2b-256 {az = az} {as} p q - with <>>-cancel-both az ([] :< Term) as p -bappTermLem blake2b-256 (start _) base | refl ,, refl = _ ,, _ ,, refl - -bappTypeLem : ∀ b {A}{az as}(p : az <>> (Type ∷ as) ∈ arity b) - → BApp b p A → ∃ λ K → ∃ λ (B : ∅ ,⋆ K ⊢Nf⋆ *) → A ≡ Π B -bappTypeLem addInteger {as = as} .(bubble p) (app {az = az} p q x) - with <>>-cancel-both' az (([] :< Term) :< Type) (([] :< Term) :< Term) as p refl -... | refl ,, refl ,, () -bappTypeLem addInteger {as = as} .(bubble p) (app⋆ {az = az} p q q₁) - with <>>-cancel-both' az (([] :< Type) :< Type) (([] :< Term) :< Term) as p refl -... | refl ,, refl ,, () - -bappTypeLem subtractInteger {as = as} .(bubble p) (app {az = az} p q x) - with <>>-cancel-both' az (([] :< Term) :< Type) (([] :< Term) :< Term) as p refl -... | refl ,, refl ,, () -bappTypeLem subtractInteger {as = as} .(bubble p) (app⋆ {az = az} p q q₁) - with <>>-cancel-both' az (([] :< Type) :< Type) (([] :< Term) :< Term) as p refl -... | refl ,, refl ,, () - -bappTypeLem multiplyInteger {as = as} .(bubble p) (app {az = az} p q x) - with <>>-cancel-both' az (([] :< Term) :< Type) (([] :< Term) :< Term) as p refl -... | refl ,, refl ,, () -bappTypeLem multiplyInteger {as = as} .(bubble p) (app⋆ {az = az} p q q₁) - with <>>-cancel-both' az (([] :< Type) :< Type) (([] :< Term) :< Term) as p refl -... | refl ,, refl ,, () - -bappTypeLem divideInteger {as = as} .(bubble p) (app {az = az} p q x) - with <>>-cancel-both' az (([] :< Term) :< Type) (([] :< Term) :< Term) as p refl -... | refl ,, refl ,, () -bappTypeLem divideInteger {as = as} .(bubble p) (app⋆ {az = az} p q q₁) - with <>>-cancel-both' az (([] :< Type) :< Type) (([] :< Term) :< Term) as p refl -... | refl ,, refl ,, () - -bappTypeLem quotientInteger {as = as} .(bubble p) (app {az = az} p q x) - with <>>-cancel-both' az (([] :< Term) :< Type) (([] :< Term) :< Term) as p refl -... | refl ,, refl ,, () -bappTypeLem quotientInteger {as = as} .(bubble p) (app⋆ {az = az} p q q₁) - with <>>-cancel-both' az (([] :< Type) :< Type) (([] :< Term) :< Term) as p refl -... | refl ,, refl ,, () - -bappTypeLem remainderInteger {as = as} .(bubble p) (app {az = az} p q x) - with <>>-cancel-both' az (([] :< Term) :< Type) (([] :< Term) :< Term) as p refl -... | refl ,, refl ,, () -bappTypeLem remainderInteger {as = as} .(bubble p) (app⋆ {az = az} p q q₁) - with <>>-cancel-both' az (([] :< Type) :< Type) (([] :< Term) :< Term) as p refl -... | refl ,, refl ,, () -bappTypeLem modInteger {as = as} .(bubble p) (app {az = az} p q x) - with <>>-cancel-both' az (([] :< Term) :< Type) (([] :< Term) :< Term) as p refl -... | refl ,, refl ,, () -bappTypeLem modInteger {as = as} .(bubble p) (app⋆ {az = az} p q q₁) - with <>>-cancel-both' az (([] :< Type) :< Type) (([] :< Term) :< Term) as p refl -... | refl ,, refl ,, () -bappTypeLem lessThanInteger {as = as} .(bubble p) (app {az = az} p q x) - with <>>-cancel-both' az (([] :< Term) :< Type) (([] :< Term) :< Term) as p refl -... | refl ,, refl ,, () -bappTypeLem lessThanInteger {as = as} .(bubble p) (app⋆ {az = az} p q q₁) - with <>>-cancel-both' az (([] :< Type) :< Type) (([] :< Term) :< Term) as p refl -... | refl ,, refl ,, () -bappTypeLem lessThanEqualsInteger {as = as} .(bubble p) (app {az = az} p q x) - with <>>-cancel-both' az (([] :< Term) :< Type) (([] :< Term) :< Term) as p refl -... | refl ,, refl ,, () -bappTypeLem lessThanEqualsInteger {as = as} .(bubble p) (app⋆ {az = az} p q q₁) - with <>>-cancel-both' az (([] :< Type) :< Type) (([] :< Term) :< Term) as p refl -... | refl ,, refl ,, () -bappTypeLem equalsInteger {as = as} .(bubble p) (app {az = az} p q x) - with <>>-cancel-both' az (([] :< Term) :< Type) (([] :< Term) :< Term) as p refl -... | refl ,, refl ,, () -bappTypeLem equalsInteger {as = as} .(bubble p) (app⋆ {az = az} p q q₁) - with <>>-cancel-both' az (([] :< Type) :< Type) (([] :< Term) :< Term) as p refl -... | refl ,, refl ,, () -bappTypeLem appendByteString {as = as} .(bubble p) (app {az = az} p q x) - with <>>-cancel-both' az (([] :< Term) :< Type) (([] :< Term) :< Term) as p refl -... | refl ,, refl ,, () -bappTypeLem appendByteString {as = as} .(bubble p) (app⋆ {az = az} p q q₁) - with <>>-cancel-both' az (([] :< Type) :< Type) (([] :< Term) :< Term) as p refl -... | refl ,, refl ,, () -bappTypeLem lessThanByteString {as = as} .(bubble p) (app {az = az} p q x) - with <>>-cancel-both' az (([] :< Term) :< Type) (([] :< Term) :< Term) as p refl -... | refl ,, refl ,, () -bappTypeLem lessThanByteString {as = as} .(bubble p) (app⋆ {az = az} p q q₁) - with <>>-cancel-both' az (([] :< Type) :< Type) (([] :< Term) :< Term) as p refl -... | refl ,, refl ,, () -bappTypeLem lessThanEqualsByteString {as = as} .(bubble p) (app {az = az} p q x) - with <>>-cancel-both' az (([] :< Term) :< Type) (([] :< Term) :< Term) as p refl -... | refl ,, refl ,, () -bappTypeLem lessThanEqualsByteString {as = as} .(bubble p) (app⋆ {az = az} p q q₁) - with <>>-cancel-both' az (([] :< Type) :< Type) (([] :< Term) :< Term) as p refl -... | refl ,, refl ,, () -bappTypeLem sha2-256 {az = az} {as} p q - with <>>-cancel-both' az ([] :< Type) ([] :< Term) as p refl -... | refl ,, refl ,, () -bappTypeLem sha3-256 {az = az} {as} p q - with <>>-cancel-both' az ([] :< Type) ([] :< Term) as p refl -... | refl ,, refl ,, () -bappTypeLem verifyEd25519Signature {as = as} .(bubble (bubble p)) (app .(bubble p) (app {az = az} p q x) x') - with <>>-cancel-both' az ((([] :< Term) :< Term) :< Type) ((([] :< Term) :< Term) :< Term) as p refl -... | refl ,, refl ,, () -bappTypeLem verifyEd25519Signature {as = as} .(bubble (bubble p)) (app .(bubble p) (app⋆ {az = az} p q q₁₁) x) - with <>>-cancel-both' az ((([] :< Type) :< Term) :< Type) ((([] :< Term) :< Term) :< Term) as p refl -... | refl ,, refl ,, () -bappTypeLem verifyEd25519Signature {as = as} .(bubble (bubble p)) (app⋆ .(bubble p) (app {az = az} p q x₁) q₁) with <>>-cancel-both' az ((([] :< Term) :< Type) :< Type) ((([] :< Term) :< Term) :< Term) as p refl -... | refl ,, refl ,, () -bappTypeLem verifyEd25519Signature {as = as} .(bubble (bubble p)) (app⋆ .(bubble p) (app⋆ {az = az} p q q₂) q₁) with <>>-cancel-both' az ((([] :< Type) :< Type) :< Type) ((([] :< Term) :< Term) :< Term) as p refl -... | refl ,, refl ,, () -bappTypeLem verifyEcdsaSecp256k1Signature {as = as} .(bubble (bubble p)) (app .(bubble p) (app {az = az} p q x) x') - with <>>-cancel-both' az ((([] :< Term) :< Term) :< Type) ((([] :< Term) :< Term) :< Term) as p refl -... | refl ,, refl ,, () -bappTypeLem verifyEcdsaSecp256k1Signature {as = as} .(bubble (bubble p)) (app .(bubble p) (app⋆ {az = az} p q q₁₁) x) - with <>>-cancel-both' az ((([] :< Type) :< Term) :< Type) ((([] :< Term) :< Term) :< Term) as p refl -... | refl ,, refl ,, () -bappTypeLem verifyEcdsaSecp256k1Signature {as = as} .(bubble (bubble p)) (app⋆ .(bubble p) (app {az = az} p q x₁) q₁) with <>>-cancel-both' az ((([] :< Term) :< Type) :< Type) ((([] :< Term) :< Term) :< Term) as p refl -... | refl ,, refl ,, () -bappTypeLem verifyEcdsaSecp256k1Signature {as = as} .(bubble (bubble p)) (app⋆ .(bubble p) (app⋆ {az = az} p q q₂) q₁) with <>>-cancel-both' az ((([] :< Type) :< Type) :< Type) ((([] :< Term) :< Term) :< Term) as p refl -... | refl ,, refl ,, () -bappTypeLem verifySchnorrSecp256k1Signature {as = as} .(bubble (bubble p)) (app .(bubble p) (app {az = az} p q x) x') - with <>>-cancel-both' az ((([] :< Term) :< Term) :< Type) ((([] :< Term) :< Term) :< Term) as p refl -... | refl ,, refl ,, () -bappTypeLem verifySchnorrSecp256k1Signature {as = as} .(bubble (bubble p)) (app .(bubble p) (app⋆ {az = az} p q q₁₁) x) - with <>>-cancel-both' az ((([] :< Type) :< Term) :< Type) ((([] :< Term) :< Term) :< Term) as p refl -... | refl ,, refl ,, () -bappTypeLem verifySchnorrSecp256k1Signature {as = as} .(bubble (bubble p)) (app⋆ .(bubble p) (app {az = az} p q x₁) q₁) with <>>-cancel-both' az ((([] :< Term) :< Type) :< Type) ((([] :< Term) :< Term) :< Term) as p refl -... | refl ,, refl ,, () -bappTypeLem verifySchnorrSecp256k1Signature {as = as} .(bubble (bubble p)) (app⋆ .(bubble p) (app⋆ {az = az} p q q₂) q₁) with <>>-cancel-both' az ((([] :< Type) :< Type) :< Type) ((([] :< Term) :< Term) :< Term) as p refl -... | refl ,, refl ,, () -bappTypeLem equalsByteString {as = as} .(bubble p) (app {az = az} p q x) - with <>>-cancel-both' az (([] :< Term) :< Type) (([] :< Term) :< Term) as p refl -... | refl ,, refl ,, () -bappTypeLem equalsByteString {as = as} .(bubble p) (app⋆ {az = az} p q q₁) - with <>>-cancel-both' az (([] :< Type) :< Type) (([] :< Term) :< Term) as p refl -... | refl ,, refl ,, () -bappTypeLem ifThenElse .(start (Type ∷ Term ∷ Term ∷ Term ∷ [])) base = _ ,, _ ,, refl -bappTypeLem ifThenElse {as = as} .(bubble (bubble (bubble p))) (app .(bubble (bubble p)) (app .(bubble p) (app {az = az} p q x₂) x₁) x) - with <>>-cancel-both' az (((([] :< Term) :< Term) :< Term) :< Type) (((([] :< Type) :< Term) :< Term) :< Term) as p refl -... | refl ,, refl ,, () -bappTypeLem ifThenElse {as = as} .(bubble (bubble (bubble p))) (app .(bubble (bubble p)) (app .(bubble p) (app⋆ {az = az} p q q₁₂) x₁) x) with <>>-cancel-both' az (((([] :< Type) :< Term) :< Term) :< Type) (((([] :< Type) :< Term) :< Term) :< Term) as p refl -... | refl ,, refl ,, () -bappTypeLem ifThenElse {as = as} .(bubble (bubble (bubble p))) (app .(bubble (bubble p)) (app⋆ .(bubble p) (app {az = az} p q x₂) q₁₁) x) with <>>-cancel-both' az (((([] :< Term) :< Type) :< Term) :< Type) (((([] :< Type) :< Term) :< Term) :< Term) as p refl -... | refl ,, refl ,, () -bappTypeLem ifThenElse {as = as} .(bubble (bubble (bubble p))) (app .(bubble (bubble p)) (app⋆ .(bubble p) (app⋆ {az = az} p q q₂) q₁) x) with <>>-cancel-both' az (((([] :< Type) :< Type) :< Term) :< Type) (((([] :< Type) :< Term) :< Term) :< Term) as p refl -... | refl ,, refl ,, () -bappTypeLem ifThenElse {as = as} .(bubble (bubble (bubble p))) (app⋆ .(bubble (bubble p)) (app .(bubble p) (app {az = az} p q x₂) x₁) q₁) with <>>-cancel-both' az (((([] :< Term) :< Term) :< Type) :< Type) (((([] :< Type) :< Term) :< Term) :< Term) as p refl -... | refl ,, refl ,, () -bappTypeLem ifThenElse {as = as} .(bubble (bubble (bubble p))) (app⋆ .(bubble (bubble p)) (app .(bubble p) (app⋆ {az = az} p q q₂) x₁) q₁) with <>>-cancel-both' az (((([] :< Type) :< Term) :< Type) :< Type) (((([] :< Type) :< Term) :< Term) :< Term) as p refl -... | refl ,, refl ,, () -bappTypeLem ifThenElse {as = as} .(bubble (bubble (bubble p))) (app⋆ .(bubble (bubble p)) (app⋆ .(bubble p) (app {az = az} p q x₂) q₂) q₁) with <>>-cancel-both' az (((([] :< Term) :< Type) :< Type) :< Type) (((([] :< Type) :< Term) :< Term) :< Term) as p refl -... | refl ,, refl ,, () -bappTypeLem ifThenElse {as = as} .(bubble (bubble (bubble p))) (app⋆ .(bubble (bubble p)) (app⋆ .(bubble p) (app⋆ {az = az} p q q₃) q₂) q₁) with <>>-cancel-both' az (((([] :< Type) :< Type) :< Type) :< Type) (((([] :< Type) :< Term) :< Term) :< Term) as p refl -... | refl ,, refl ,, () -bappTypeLem appendString {as = as} .(bubble p) (app {az = az} p q x) - with <>>-cancel-both' az (([] :< Term) :< Type) (([] :< Term) :< Term) as p refl -... | refl ,, refl ,, () -bappTypeLem appendString {as = as} .(bubble p) (app⋆ {az = az} p q q₁) - with <>>-cancel-both' az (([] :< Type) :< Type) (([] :< Term) :< Term) as p refl -... | refl ,, refl ,, () -bappTypeLem trace (start _) base = _ ,, _ ,, refl -bappTypeLem trace {as = as} (bubble (bubble {as = az} p)) q - with <>>-cancel-both' az _ ([] <>< arity trace) _ p refl -... | refl ,, refl ,, () -bappTypeLem equalsString (bubble {as = az} p) _ - with <>>-cancel-both' az _ (([] :< Term) :< Term) _ p refl -... | refl ,, refl ,, () -bappTypeLem encodeUtf8 {az = az} p _ - with <>>-cancel-both' az _ ([] :< Term) _ p refl -... | refl ,, refl ,, () -bappTypeLem decodeUtf8 {az = az} p _ - with <>>-cancel-both' az _ ([] :< Term) _ p refl -... | refl ,, refl ,, () -bappTypeLem fstPair (start _) base = _ ,, _ ,, refl -bappTypeLem fstPair (bubble (start _)) (app⋆ _ base refl) = - _ ,, _ ,, refl -bappTypeLem fstPair (bubble (bubble {as = az} p)) _ - with <>>-cancel-both' az _ ((([] :< Type) :< Type) :< Term) _ p refl -... | refl ,, refl ,, () -bappTypeLem sndPair (start _) base = _ ,, _ ,, refl -bappTypeLem sndPair (bubble (start _)) (app⋆ _ base refl) = - _ ,, _ ,, refl -bappTypeLem sndPair (bubble (bubble {as = az} p)) _ - with <>>-cancel-both' az _ ((([] :< Type) :< Type) :< Term) _ p refl -... | refl ,, refl ,, () -bappTypeLem bData {az = az} p q - with <>>-cancel-both' az _ ([] :< Term) _ p refl -... | refl ,, refl ,, () -bappTypeLem unConstrData {az = az} p q - with <>>-cancel-both' az _ ([] :< Term) _ p refl -... | refl ,, refl ,, () -bappTypeLem unMapData {az = az} p q - with <>>-cancel-both' az _ ([] :< Term) _ p refl -... | refl ,, refl ,, () -bappTypeLem unListData {az = az} p q - with <>>-cancel-both' az _ ([] :< Term) _ p refl -... | refl ,, refl ,, () -bappTypeLem unIData {az = az} p q - with <>>-cancel-both' az _ ([] :< Term) _ p refl -... | refl ,, refl ,, () -bappTypeLem unBData {az = az} p q - with <>>-cancel-both' az _ ([] :< Term) _ p refl -... | refl ,, refl ,, () -bappTypeLem equalsData (bubble {as = az} p) _ - with <>>-cancel-both' az _ (([] :< Term) :< Term) _ p refl -... | refl ,, refl ,, () -bappTypeLem serialiseData {az = az} p q - with <>>-cancel-both' az _ ([] :< Term) _ p refl -... | refl ,, refl ,, () -bappTypeLem chooseData (start _) base = _ ,, _ ,, refl -bappTypeLem chooseData (bubble (bubble (bubble (bubble (bubble (bubble {as = az} p)))))) _ - with <>>-cancel-both' az _ ([] <>< arity chooseData) _ p refl -... | _ ,, _ ,, () -bappTypeLem chooseUnit (start _) base = _ ,, _ ,, refl -bappTypeLem chooseUnit (bubble (bubble {as = az} p)) _ - with <>>-cancel-both' az _ ([] <>< arity chooseUnit) _ p refl -... | _ ,, _ ,, () -bappTypeLem mkPairData (bubble {as = az} p) q - with <>>-cancel-both' az _ (([] :< Term) :< Term) _ p refl -... | refl ,, refl ,, () -bappTypeLem mkNilData {az = az} p q - with <>>-cancel-both' az _ ([] :< Term) _ p refl -... | refl ,, refl ,, () -bappTypeLem mkNilPairData {az = az} p q - with <>>-cancel-both' az _ ([] :< Term) _ p refl -... | refl ,, refl ,, () -bappTypeLem mkCons (start _) base = _ ,, _ ,, refl -bappTypeLem mkCons (bubble (bubble {as = az} p)) _ - with <>>-cancel-both' az _ ([] <>< arity chooseUnit) _ p refl -... | _ ,, _ ,, () -bappTypeLem nullList (start _) base = _ ,, _ ,, refl -bappTypeLem nullList (bubble {as = az} p) _ - with <>>-cancel-both' az _ (([] :< Type) :< Term) _ p refl -... | refl ,, refl ,, () -bappTypeLem headList (start _) base = _ ,, _ ,, refl -bappTypeLem headList (bubble {as = az} p) _ - with <>>-cancel-both' az _ (([] :< Type) :< Term) _ p refl -... | refl ,, refl ,, () -bappTypeLem tailList (start _) base = _ ,, _ ,, refl -bappTypeLem tailList (bubble {as = az} p) _ - with <>>-cancel-both' az _ (([] :< Type) :< Term) _ p refl -... | refl ,, refl ,, () -bappTypeLem chooseList (start _) base = _ ,, _ ,, refl -bappTypeLem chooseList (bubble (start _)) (app⋆ _ base refl) = - _ ,, _ ,, refl -bappTypeLem chooseList (bubble (bubble (bubble (bubble {as = az} p)))) _ - with <>>-cancel-both' az _ ([] <>< arity chooseList) _ p refl -... | _ ,, _ ,, () -bappTypeLem constrData (bubble {as = az} p) _ - with <>>-cancel-both' az _ (([] :< Term) :< Term) _ p refl -... | refl ,, refl ,, () -bappTypeLem mapData {az = az} p q - with <>>-cancel-both' az _ ([] :< Term) _ p refl -... | refl ,, refl ,, () -bappTypeLem listData {az = az} p q - with <>>-cancel-both' az _ ([] :< Term) _ p refl -... | refl ,, refl ,, () -bappTypeLem iData {az = az} p q - with <>>-cancel-both' az _ ([] :< Term) _ p refl -... | refl ,, refl ,, () -bappTypeLem consByteString (bubble {as = az} p) q - with <>>-cancel-both' az _ (([] :< Term) :< Term) _ p refl -... | refl ,, refl ,, () -bappTypeLem sliceByteString (bubble (bubble {as = az} p)) q - with <>>-cancel-both' az _ ((([] :< Term) :< Term) :< Term) _ p refl -... | refl ,, refl ,, () -bappTypeLem lengthOfByteString {az = az} p q - with <>>-cancel-both' az _ ([] :< Term) _ p refl -... | refl ,, refl ,, () -bappTypeLem indexByteString (bubble {as = az} p) q - with <>>-cancel-both' az _ (([] :< Term) :< Term) _ p refl -... | refl ,, refl ,, () -bappTypeLem blake2b-256 {az = az} p q - with <>>-cancel-both' az _ ([] :< Term) _ p refl -... | refl ,, refl ,, () - -V-I : ∀ b {A : ∅ ⊢Nf⋆ *}{a as as'} - → (p : as <>> a ∷ as' ∈ arity b) - → BApp b p A +``` +V-I : ∀ (b : Builtin) {A : ∅ ⊢Nf⋆ *} + → ∀{tn tm} {pt : tn ∔ tm ≣ fv♯ (signature b)} + → ∀{an am} {pa : an ∔ suc am ≣ args♯ (signature b)} + → {σA : SigTy pt pa A} + → BApp b A σA → Value A -V-I b {a = Term} p q with bappTermLem b p q -... | _ ,, _ ,, refl = V-I⇒ b p q -V-I b {a = Type} p q with bappTypeLem b p q -... | _ ,, _ ,, refl = V-IΠ b p q +V-I b {tm = zero} {σA = A B⇒ σA} bt = V-I⇒ b bt +V-I b {tm = suc tm} {σA = sucΠ σA} bt = V-IΠ b bt + +data Error : ∅ ⊢Nf⋆ * → Set where + -- an actual error term + E-error : (A : ∅ ⊢Nf⋆ *) → Error A data Frame : (T : ∅ ⊢Nf⋆ *) → (H : ∅ ⊢Nf⋆ *) → Set where -· : ∀{Γ}{A B : ∅ ⊢Nf⋆ *} → Γ ⊢ A → Env Γ → Frame B (A ⇒ B) @@ -876,91 +293,32 @@ data State (T : ∅ ⊢Nf⋆ *) : Set where □ : Value T → State T ◆ : ∅ ⊢Nf⋆ * → State T - - -ival : ∀ b → Value (btype b) -ival addInteger = V-I⇒ addInteger _ base -ival subtractInteger = V-I⇒ subtractInteger _ base -ival multiplyInteger = V-I⇒ multiplyInteger _ base -ival divideInteger = V-I⇒ divideInteger _ base -ival quotientInteger = V-I⇒ quotientInteger _ base -ival remainderInteger = V-I⇒ remainderInteger _ base -ival modInteger = V-I⇒ modInteger _ base -ival lessThanInteger = V-I⇒ lessThanInteger _ base -ival lessThanEqualsInteger = V-I⇒ lessThanEqualsInteger _ base -ival equalsInteger = V-I⇒ equalsInteger _ base -ival appendByteString = V-I⇒ appendByteString _ base -ival lessThanByteString = V-I⇒ lessThanByteString _ base -ival lessThanEqualsByteString = V-I⇒ lessThanEqualsByteString _ base -ival sha2-256 = V-I⇒ sha2-256 _ base -ival sha3-256 = V-I⇒ sha3-256 _ base -ival verifyEd25519Signature = V-I⇒ verifyEd25519Signature _ base -ival verifyEcdsaSecp256k1Signature = V-I⇒ verifyEcdsaSecp256k1Signature _ base -ival verifySchnorrSecp256k1Signature = V-I⇒ verifySchnorrSecp256k1Signature _ base -ival equalsByteString = V-I⇒ equalsByteString _ base -ival ifThenElse = V-IΠ ifThenElse _ base -ival appendString = V-I⇒ appendString _ base -ival trace = V-IΠ trace _ base -ival equalsString = V-I⇒ equalsString (start _) base -ival encodeUtf8 = V-I⇒ encodeUtf8 (start _) base -ival decodeUtf8 = V-I⇒ decodeUtf8 (start _) base -ival fstPair = V-IΠ fstPair (start _) base -ival sndPair = V-IΠ sndPair (start _) base -ival nullList = V-IΠ nullList (start _) base -ival headList = V-IΠ headList (start _) base -ival tailList = V-IΠ tailList (start _) base -ival chooseList = V-IΠ chooseList (start _) base -ival constrData = V-I⇒ constrData (start _) base -ival mapData = V-I⇒ mapData (start _) base -ival listData = V-I⇒ listData (start _) base -ival iData = V-I⇒ iData (start _) base -ival bData = V-I⇒ bData (start _) base -ival unConstrData = V-I⇒ unConstrData (start _) base -ival unMapData = V-I⇒ unMapData (start _) base -ival unListData = V-I⇒ unListData (start _) base -ival unIData = V-I⇒ unIData (start _) base -ival unBData = V-I⇒ unBData (start _) base -ival equalsData = V-I⇒ equalsData (start _) base -ival serialiseData = V-I⇒ serialiseData (start _) base -ival chooseData = V-IΠ chooseData (start _) base -ival chooseUnit = V-IΠ chooseUnit (start _) base -ival mkPairData = V-I⇒ mkPairData (start _) base -ival mkNilData = V-I⇒ mkNilData (start _) base -ival mkNilPairData = V-I⇒ mkNilPairData (start _) base -ival mkCons = V-IΠ mkCons (start _) base -ival consByteString = V-I⇒ consByteString (start _) base -ival sliceByteString = V-I⇒ sliceByteString (start _) base -ival lengthOfByteString = V-I⇒ lengthOfByteString (start _) base -ival indexByteString = V-I⇒ indexByteString (start _) base -ival blake2b-256 = V-I⇒ blake2b-256 (start _) base +ival : ∀(b : Builtin) → Value (btype b) +ival b = V-I b base step : ∀{T} → State T → State T -step (s ; ρ ▻ ` x) = s ◅ lookup x ρ -step (s ; ρ ▻ ƛ L) = s ◅ V-ƛ L ρ -step (s ; ρ ▻ (L · M)) = (s , -· M ρ) ; ρ ▻ L -step (s ; ρ ▻ Λ L) = s ◅ V-Λ L ρ -step (s ; ρ ▻ (L ·⋆ A / refl)) = (s , -·⋆ A) ; ρ ▻ L -step (s ; ρ ▻ wrap A B L) = (s , wrap-) ; ρ ▻ L -step (s ; ρ ▻ unwrap L refl) = (s , unwrap-) ; ρ ▻ L -step (s ; ρ ▻ con c) = s ◅ V-con c -step (s ; ρ ▻ (builtin b / refl)) = s ◅ ival b -step (s ; ρ ▻ error A) = ◆ A -step (ε ◅ V) = □ V -step ((s , -· M ρ') ◅ V) = (s , V ·-) ; ρ' ▻ M -step ((s , (V-ƛ M ρ ·-)) ◅ V) = s ; ρ ∷ V ▻ M -step ((s , -·⋆ A) ◅ V-Λ M ρ) = s ; ρ ▻ (M [ A ]⋆) -step ((s , wrap- {A = A}{B = B}) ◅ V) = s ◅ V-wrap V -step ((s , unwrap-) ◅ V-wrap V) = s ◅ V -step ((s , (V-I⇒ b {as' = []} p vs ·-)) ◅ V) = - s ; [] ▻ (BUILTIN' b (bubble p) (app p vs V)) -step ((s , (V-I⇒ b {as' = x₂ ∷ as'} p vs ·-)) ◅ V) = - s ◅ V-I b (bubble p) (app p vs V) -step ((s , -·⋆ A) ◅ V-IΠ b {as' = []} p vs) = - s ; [] ▻ BUILTIN' b (bubble p) (app⋆ p vs refl) -step ((s , -·⋆ A) ◅ V-IΠ b {as' = x₂ ∷ as'} p vs) = - s ◅ V-I b (bubble p) (app⋆ p vs refl) -step (□ V) = □ V -step (◆ A) = ◆ A +step (s ; ρ ▻ ` x) = s ◅ lookup x ρ +step (s ; ρ ▻ ƛ L) = s ◅ V-ƛ L ρ +step (s ; ρ ▻ (L · M)) = (s , -· M ρ) ; ρ ▻ L +step (s ; ρ ▻ Λ L) = s ◅ V-Λ L ρ +step (s ; ρ ▻ (L ·⋆ A / refl)) = (s , -·⋆ A) ; ρ ▻ L +step (s ; ρ ▻ wrap A B L) = (s , wrap-) ; ρ ▻ L +step (s ; ρ ▻ unwrap L refl) = (s , unwrap-) ; ρ ▻ L +step (s ; ρ ▻ con c) = s ◅ V-con c +step (s ; ρ ▻ (builtin b / refl)) = s ◅ ival b +step (s ; ρ ▻ error A) = ◆ A +step (ε ◅ V) = □ V +step ((s , -· M ρ') ◅ V) = (s , V ·-) ; ρ' ▻ M +step ((s , (V-ƛ M ρ ·-)) ◅ V) = s ; ρ ∷ V ▻ M +step ((s , (V-I⇒ b {am = 0} bapp ·-)) ◅ V) = s ; [] ▻ (BUILTIN' b (app bapp V)) +step ((s , (V-I⇒ b {am = suc _} bapp ·-)) ◅ V) = s ◅ V-I b (app bapp V) +step ((s , -·⋆ A) ◅ V-Λ M ρ) = s ; ρ ▻ (M [ A ]⋆) +step ((s , -·⋆ A) ◅ V-IΠ b bapp) = s ◅ V-I b (app⋆ bapp refl refl) +step ((s , wrap-) ◅ V) = s ◅ V-wrap V +step ((s , unwrap-) ◅ V-wrap V) = s ◅ V +step (□ V) = □ V +step (◆ A) = ◆ A + stepper : ℕ → ∀{T} → State T → Either RuntimeError (State T) stepper zero st = inj₁ gasError @@ -969,3 +327,5 @@ stepper (suc n) st | (s ; ρ ▻ M) = stepper n (s ; ρ ▻ M) stepper (suc n) st | (s ◅ V) = stepper n (s ◅ V) stepper (suc n) st | (□ V) = return (□ V) stepper (suc n) st | ◆ A = return (◆ A) +-- -} + \ No newline at end of file diff --git a/plutus-metatheory/src/Algorithmic/CK.lagda.md b/plutus-metatheory/src/Algorithmic/CK.lagda.md index c0aa7dd3e1d..f198c78fce5 100644 --- a/plutus-metatheory/src/Algorithmic/CK.lagda.md +++ b/plutus-metatheory/src/Algorithmic/CK.lagda.md @@ -8,10 +8,10 @@ module Algorithmic.CK where ``` open import Data.List as L using (List;[];_∷_) -open import Relation.Binary.PropositionalEquality using (_≡_;refl) +open import Relation.Binary.PropositionalEquality using (_≡_;refl;sym) open import Data.Nat using (ℕ;zero;suc) -open import Utils using (Kind;*;_⇒_;Either;inj₁;_<>>_∈_;bubble;RuntimeError;Monad) +open import Utils using (Kind;*;_⇒_;Either;inj₁;RuntimeError;Monad) open RuntimeError open Monad {{...}} @@ -85,14 +85,9 @@ 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 ▻ (builtin b / refl)) = 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) = - s ◅ V-I b (bubble p) (app p bt vu) -step ((s , -·⋆ A) ◅ V-IΠ b {as' = []} p bt) = - s ▻ BUILTIN' b (bubble p) (app⋆ p bt refl) -step ((s , -·⋆ A) ◅ V-IΠ b {as' = _ ∷ as'} p bt) = - s ◅ V-I b (bubble p) (app⋆ p bt refl) +step ((s , (V-I⇒ b {am = 0} bt ·-)) ◅ vu) = s ▻ BUILTIN' b (app bt vu) +step ((s , (V-I⇒ b {am = suc _} bt ·-)) ◅ vu) = s ◅ V-I b (app bt vu) +step ((s , -·⋆ A) ◅ V-IΠ b bt) = s ◅ V-I b (app⋆ bt refl refl) step (□ V) = □ V step (◆ A) = ◆ A diff --git a/plutus-metatheory/src/Algorithmic/Completeness.lagda b/plutus-metatheory/src/Algorithmic/Completeness.lagda index 0e0095649e9..431a464c7d4 100644 --- a/plutus-metatheory/src/Algorithmic/Completeness.lagda +++ b/plutus-metatheory/src/Algorithmic/Completeness.lagda @@ -18,6 +18,7 @@ open _≡β_ open import Type.RenamingSubstitution using (weaken;ren;_[_];sub-cons;Sub;sub) import Declarative as Syn import Algorithmic as Norm +import Algorithmic.Signature as Norm open import Type.BetaNormal using (embNf;weakenNf;ne;_⊢Nf⋆_;_⊢Ne⋆_) open _⊢Nf⋆_ open _⊢Ne⋆_ diff --git a/plutus-metatheory/src/Algorithmic/Erasure/RenamingSubstitution.lagda b/plutus-metatheory/src/Algorithmic/Erasure/RenamingSubstitution.lagda index a28a83afb84..59558a04a16 100644 --- a/plutus-metatheory/src/Algorithmic/Erasure/RenamingSubstitution.lagda +++ b/plutus-metatheory/src/Algorithmic/Erasure/RenamingSubstitution.lagda @@ -18,7 +18,8 @@ open import Type.BetaNormal.Equality using (renNf-id;renNf-comp) open import Type.BetaNBE.RenamingSubstitution using (ren[]Nf;ren-nf-μ;SubNf;subNf-id;subNf;weakenNf[];weakenNf-subNf) using (sub-nf-Π;sub[]Nf';sub-nf-μ;subNf-cons;extsNf) -open import Algorithmic as A using (Ctx;_∋_;conv∋;_⊢_;conv⊢;btype-ren;btype-sub) +open import Algorithmic as A using (Ctx;_∋_;conv∋;_⊢_;conv⊢) +open import Algorithmic.Signature using (btype-ren;btype-sub) open Ctx open _∋_ open _⊢_ diff --git a/plutus-metatheory/src/Algorithmic/Reduction.lagda b/plutus-metatheory/src/Algorithmic/Reduction.lagda index 8edbddaa797..72b252726d6 100644 --- a/plutus-metatheory/src/Algorithmic/Reduction.lagda +++ b/plutus-metatheory/src/Algorithmic/Reduction.lagda @@ -15,18 +15,18 @@ open import Data.Unit using (tt) open import Data.Maybe using (just;from-just) open import Data.String using (String) -open import Utils using (Kind;*;_⇒_;_<>>_∈_;bubble;K) +open import Utils using (Kind;*;_⇒_;_∔_≣_;bubble;K) open import Type using (Ctx⋆;∅;_,⋆_;Z;_⊢⋆_) open _⊢⋆_ import Type.RenamingSubstitution as T open import Algorithmic.RenamingSubstitution using (_[_];_[_]⋆) open import Type.BetaNBE using (nf) -open import Type.BetaNormal using (_⊢Nf⋆_;embNf;weakenNf) +open import Type.BetaNormal using (_⊢Nf⋆_;_⊢Ne⋆_;embNf;weakenNf) open _⊢Nf⋆_ +open _⊢Ne⋆_ -open import Builtin using (Builtin) -open import Algorithmic using (Ctx;_⊢_;Term;Type;arity) +open import Algorithmic using (Ctx;_⊢_) open _⊢_ open Ctx open import Algorithmic.ReductionEC using (Value;BApp;BUILTIN';_—→⋆_;EC;_[_]ᴱ;Error) @@ -35,6 +35,15 @@ open EC open _—→⋆_ open import Algorithmic.ReductionEC.Progress using (step;done;error) +open import Builtin using (Builtin;signature) +open import Builtin.Signature using (Sig;sig;Args;_⊢♯;nat2Ctx⋆;fin2∈⋆;args♯) +open Sig + +open Builtin.Signature.FromSig Ctx⋆ (_⊢Nf⋆ *) nat2Ctx⋆ (λ x → ne (` (fin2∈⋆ x))) con _⇒_ Π + using (sig2type;♯2*;SigTy;sig2SigTy;sigTy2type;saturatedSigTy;convSigTy) +open SigTy + + import Algorithmic.ReductionEC as E import Algorithmic.ReductionEC.Progress as EP import Algorithmic.ReductionEC.Determinism as ED @@ -93,27 +102,17 @@ data _—→V_ : {A : ∅ ⊢Nf⋆ *} → (∅ ⊢ A) → (∅ ⊢ A) → Set wh → M —→V M' → wrap A B M —→V wrap A B M' - β-sbuiltin : ∀{A B} + β-builtin : ∀{A B}{tn} (b : Builtin) → (t : ∅ ⊢ A ⇒ B) - → ∀{az} - → (p : az <>> (Term ∷ []) ∈ arity b) - → (bt : BApp b p t) -- one left + → {pt : tn ∔ 0 ≣ fv♯ (signature b)} + → ∀{an} → {pa : an ∔ 1 ≣ args♯ (signature b)} + → {σB : SigTy pt (bubble pa) B} + → (bt : BApp b (A B⇒ σB) t) -- one left → (u : ∅ ⊢ A) → (vu : Value u) ----------------------------- - → t · u —→V BUILTIN' b (bubble p) (BApp.step p bt vu) - - β-sbuiltin⋆ : ∀{B : ∅ ,⋆ K ⊢Nf⋆ *}{C} - (b : Builtin) - → (t : ∅ ⊢ Π B) - → ∀{az} - → (p : az <>> (Type ∷ []) ∈ arity b) - → (bt : BApp b p t) -- one left - → ∀ A - → (q : C ≡ _) - ----------------------------- - → t ·⋆ A / q —→V BUILTIN' b (bubble p) (BApp.step⋆ p bt q) + → t · u —→V BUILTIN' b (BApp.step bt vu) \end{code} \begin{code} @@ -174,8 +173,7 @@ lem—→⋆ : ∀{A}{M M' : ∅ ⊢ A} → M —→⋆ M' → M —→V M' lem—→⋆ (β-ƛ v) = β-ƛ v lem—→⋆ (β-Λ refl) = β-Λ lem—→⋆ (β-wrap v refl) = β-wrap v -lem—→⋆ (β-sbuiltin b t p bt u vu) = β-sbuiltin b t p bt u vu -lem—→⋆ (β-sbuiltin⋆ b t p bt A q) = β-sbuiltin⋆ b t p bt A q +lem—→⋆ (β-builtin b t bt u vu) = β-builtin b t bt u vu lemCS—→V : ∀{A} → ∀{B}{L L' : ∅ ⊢ B} @@ -228,10 +226,8 @@ lemSC—→V (ξ-unwrap p) with lemSC—→V p lemSC—→V (ξ-wrap p) with lemSC—→V p ... | B ,, E ,, L ,, L' ,, refl ,, refl ,, q = B ,, wrap E ,, L ,, L' ,, refl ,, refl ,, q -lemSC—→V (β-sbuiltin b t p bt u vu) = - _ ,, [] ,, _ ,, _ ,, refl ,, refl ,, E.β-sbuiltin b t p bt u vu -lemSC—→V (β-sbuiltin⋆ b t p bt A q) = - _ ,, [] ,, _ ,, _ ,, refl ,, refl ,, E.β-sbuiltin⋆ b t p bt A q +lemSC—→V (β-builtin b t bt u vu) = + _ ,, [] ,, _ ,, _ ,, refl ,, refl ,, E.β-builtin b t bt u vu lemSC—→E : ∀{A}{M : ∅ ⊢ A} → M —→E error A diff --git a/plutus-metatheory/src/Algorithmic/ReductionEC.lagda.md b/plutus-metatheory/src/Algorithmic/ReductionEC.lagda.md index bd0fcb0f590..226bbaaeec5 100644 --- a/plutus-metatheory/src/Algorithmic/ReductionEC.lagda.md +++ b/plutus-metatheory/src/Algorithmic/ReductionEC.lagda.md @@ -5,12 +5,14 @@ module Algorithmic.ReductionEC where ``` open import Agda.Builtin.String using (primStringAppend ; primStringEquality) +open import Data.Nat using (ℕ;zero;suc) +open import Data.Nat.Properties using (+-identityʳ) open import Data.Bool using (Bool;true;false) open import Data.Empty using (⊥;⊥-elim) open import Data.Integer using (_> as ∈ arity b - → ∀{A} → ∅ ⊢ A → Set where - base : ∀{C}(p : C ≡ btype b) → BApp b (start (arity b)) (builtin b / p) - step : ∀{A B}{az as} - → (p : az <>> (Term ∷ as) ∈ arity b) - → {t : ∅ ⊢ A ⇒ B} → BApp b p t - → {u : ∅ ⊢ A} → Value u → BApp b (bubble p) (t · u) - step⋆ : ∀{C B}{az as} - → (p : az <>> (Type ∷ as) ∈ arity b) - → {t : ∅ ⊢ Π B} → BApp b p t - → {A : ∅ ⊢Nf⋆ K} +data BApp (b : Builtin) : + ∀{tn tm tt} → {pt : tn ∔ tm ≣ tt} + → ∀{an am at} → {pa : an ∔ am ≣ at} + → ∀{A} → SigTy pt pa A → ∅ ⊢ A → Set where + base : BApp b (sig2SigTy (signature b)) (builtin b / refl ) + step : ∀{A B}{tn} + → {pt : tn ∔ 0 ≣ fv♯ (signature b)} + → ∀{an am}{pa : an ∔ suc am ≣ args♯ (signature b)} + → {σB : SigTy pt (bubble pa) B} + → {t : ∅ ⊢ A ⇒ B} → BApp b (A B⇒ σB) t + → {u : ∅ ⊢ A} → Value u → BApp b σB (t · u) + step⋆ : ∀{C B} + → ∀{tn tm} {pt : tn ∔ (suc tm) ≣ fv♯ (signature b)} + → ∀{an am}{pa : an ∔ (suc am) ≣ args♯ (signature b)} + → {σB : SigTy (bubble pt) pa B} + → {t : ∅ ⊢ Π B} → BApp b (sucΠ σB) t + → {A : ∅ ⊢Nf⋆ *} → (q : C ≡ B [ A ]Nf) - → BApp b (bubble p) (t ·⋆ A / q) + → {σC : SigTy (bubble pt) pa C} + → (σq : σC ≡ substEq (SigTy (bubble pt) pa) (sym q) (σB [ A ]SigTy)) + → BApp b σC (t ·⋆ A / q) data Value where V-ƛ : {A B : ∅ ⊢Nf⋆ *} @@ -82,125 +100,122 @@ data Value where → (cn : TermCon (con tcn)) → Value (con cn) - V-I⇒ : ∀ b {A B as as'} - → (p : as <>> (Term ∷ as') ∈ arity b) + V-I⇒ : ∀ b {A B}{tn} + → {pt : tn ∔ 0 ≣ fv♯ (signature b)} + → ∀{an am}{pa : an ∔ (suc am) ≣ args♯ (signature b)} + → {σB : SigTy pt (bubble pa) B} → {t : ∅ ⊢ A ⇒ B} - → BApp b p t + → BApp b (A B⇒ σB) t → Value t - V-IΠ : ∀ b {A : ∅ ,⋆ K ⊢Nf⋆ *}{as as'} - → (p : as <>> (Type ∷ as') ∈ arity b) + V-IΠ : ∀ b {A : ∅ ,⋆ * ⊢Nf⋆ *} + → ∀{tn tm} {pt : tn ∔ (suc tm) ≣ fv♯ (signature b)} + → ∀{an am}{pa : an ∔ suc am ≣ args♯ (signature b)} + → {σA : SigTy (bubble pt) pa A} → {t : ∅ ⊢ Π A} - → BApp b p t + → BApp b (sucΠ σA) t → Value t + deval : {A : ∅ ⊢Nf⋆ *}{u : ∅ ⊢ A} → Value u → ∅ ⊢ A deval {u = u} _ = u -{- -tval : {A : ∅ ⊢Nf⋆ *}{u : ∅ ⊢ A} → Value u → ∅ ⊢Nf⋆ * -tval {A = A} _ = A --} - -BUILTIN : ∀ b {A}{t : ∅ ⊢ A} → BApp b (saturated (arity b)) t → ∅ ⊢ A -BUILTIN addInteger (step _ (step _ (base refl) (V-con (integer i))) (V-con (integer j))) = con (integer (i Data.Integer.+ j)) -BUILTIN subtractInteger (step _ (step _ (base refl) (V-con (integer i))) (V-con (integer j))) = con (integer (i Data.Integer.- j)) -BUILTIN multiplyInteger (step _ (step _ (base refl) (V-con (integer i))) (V-con (integer j))) = con (integer (i Data.Integer.* j)) -BUILTIN divideInteger (step _ (step _ (base refl) (V-con (integer i))) (V-con (integer j))) +BUILTIN : ∀ b {A}{t : ∅ ⊢ A} {Ab : saturatedSigTy (signature b) A} → BApp b Ab t → ∅ ⊢ A +BUILTIN addInteger (step (step base (V-con (integer i))) (V-con (integer j))) = con (integer (i Data.Integer.+ j)) +BUILTIN subtractInteger (step (step base (V-con (integer i))) (V-con (integer j))) = con (integer (i Data.Integer.- j)) +BUILTIN multiplyInteger (step (step base (V-con (integer i))) (V-con (integer j))) = con (integer (i Data.Integer.* j)) +BUILTIN divideInteger (step (step base (V-con (integer i))) (V-con (integer j))) with j ≟ Data.Integer.ℤ.pos 0 ... | no ¬p = con (integer (div i j)) ... | yes p = error _ -BUILTIN quotientInteger (step _ (step _ (base refl) (V-con (integer i))) (V-con (integer j))) +BUILTIN quotientInteger (step (step base (V-con (integer i))) (V-con (integer j))) with j ≟ Data.Integer.ℤ.pos 0 ... | no ¬p = con (integer (quot i j)) ... | yes p = error _ -BUILTIN remainderInteger (step _ (step _ (base refl) (V-con (integer i))) (V-con (integer j))) +BUILTIN remainderInteger (step (step base (V-con (integer i))) (V-con (integer j))) with j ≟ Data.Integer.ℤ.pos 0 ... | no ¬p = con (integer (rem i j)) ... | yes p = error _ -BUILTIN modInteger (step _ (step _ (base refl) (V-con (integer i))) (V-con (integer j))) +BUILTIN modInteger (step (step base (V-con (integer i))) (V-con (integer j))) with j ≟ Data.Integer.ℤ.pos 0 ... | no ¬p = con (integer (mod i j)) ... | yes p = error _ -BUILTIN lessThanInteger (step _ (step _ (base refl) (V-con (integer i))) (V-con (integer j))) +BUILTIN lessThanInteger (step (step base (V-con (integer i))) (V-con (integer j))) with i > as ∈ arity b) - → ∀{A}(t : ∅ ⊢ A) - → BApp b p t - → BApp b p' t -convBApp b p p' t q rewrite unique<>> p p' = q - -BUILTIN' : ∀ b {A}{t : ∅ ⊢ A}{az}(p : az <>> [] ∈ arity b) - → BApp b p t +BUILTIN' : ∀ b {A}{t : ∅ ⊢ A} + → ∀{tn} → {pt : tn ∔ 0 ≣ fv♯ (signature b)} + → ∀{an} → {pa : an ∔ 0 ≣ args♯ (signature b)} + → {σA : SigTy pt pa A} + → BApp b σA t → ∅ ⊢ A -BUILTIN' b {t = t}{az = az} p q - with sym (trans (cong ([] <><_) (sym (<>>2<>>' _ _ _ p))) (lemma<>2 az [])) -... | refl = BUILTIN b (convBApp b p (saturated (arity b)) t q) +BUILTIN' b {pt = pt} {pa = pa} bt with trans (sym (+-identityʳ _)) (∔2+ pt) | trans (sym (+-identityʳ _)) (∔2+ pa) +... | refl | refl with unique∔ pt (alldone (fv♯ (signature b))) | unique∔ pa (alldone (args♯ (signature b))) +... | refl | refl = BUILTIN b bt ``` ``` @@ -209,26 +224,6 @@ data Error : ∀ {Φ Γ} {A : Φ ⊢Nf⋆ *} → Γ ⊢ A → Set where E-error : ∀{Φ Γ }{A : Φ ⊢Nf⋆ *} → Error {Γ = Γ} (error {Φ} A) ``` -{- -convVal : ∀ {A A' : ∅ ⊢Nf⋆ *}(q : A ≡ A') - → ∀{t : ∅ ⊢ A} → Value t → Value (conv⊢ refl q t) -convVal refl v = v - -convVal' : ∀ {A A' : ∅ ⊢Nf⋆ *}(q : A ≡ A') - → ∀{t : ∅ ⊢ A} → Value (conv⊢ refl q t) → Value t -convVal' refl v = v - - -convBApp1 : ∀ b {az as}{p : az <>> as ∈ arity b}{A A' : ∅ ⊢Nf⋆ *}(q : A ≡ A') - → ∀{t : ∅ ⊢ A} → BApp b p t → BApp b p (conv⊢ refl q t) -convBApp1 b refl v = v - -convBApp1' : ∀ b {az as}{p : az <>> as ∈ arity b}{A A' : ∅ ⊢Nf⋆ *}(q : A ≡ A') - → ∀{t : ∅ ⊢ A} → BApp b p (conv⊢ refl q t) → BApp b p t -convBApp1' b refl v = v --} - - ## Intrinsically Type Preserving Reduction ### Frames @@ -305,52 +300,17 @@ data _—→⋆_ : {A : ∅ ⊢Nf⋆ *} → (∅ ⊢ A) → (∅ ⊢ A) → Set → (p : C ≡ _) → unwrap (wrap A B M) p —→⋆ substEq (∅ ⊢_) (sym p) M - β-sbuiltin : ∀{A B} + β-builtin : ∀{A B}{tn} (b : Builtin) → (t : ∅ ⊢ A ⇒ B) - → ∀{az} - → (p : az <>> (Term ∷ []) ∈ arity b) - → (bt : BApp b p t) -- one left + → {pt : tn ∔ 0 ≣ fv♯ (signature b)} + → ∀{an} → {pa : an ∔ 1 ≣ args♯ (signature b)} + → {σB : SigTy pt (bubble pa) B} + → (bt : BApp b (A B⇒ σB) t) -- one left → (u : ∅ ⊢ A) → (vu : Value u) ----------------------------- - → t · u —→⋆ BUILTIN' b (bubble p) (BApp.step p bt vu) - - β-sbuiltin⋆ : ∀{B : ∅ ,⋆ K ⊢Nf⋆ *}{C} - (b : Builtin) - → (t : ∅ ⊢ Π B) - → ∀{az} - → (p : az <>> (Type ∷ []) ∈ arity b) - → (bt : BApp b p t) -- one left - → ∀ A - → (q : C ≡ _) - ----------------------------- - → t ·⋆ A / q —→⋆ BUILTIN' b (bubble p) (BApp.step⋆ p bt q) - - -{- --- does this need to be heterogeneous? -lemΛE : ∀{K}{B : ∅ ,⋆ K ⊢Nf⋆ *} - → ∀{L : ∅ ,⋆ K ⊢ B}{X}{L' : ∅ ⊢ X}{Y} - → Y ≡ Π B - → (E : EC Y X) - → Λ L ≅ E [ L' ]ᴱ - → E ≅ EC.[] {A = Y} × Λ L ≅ L' -lemΛE refl [] refl = refl ,, refl -lemΛE refl (E l· M) () -lemΛE refl (x₂ ·r E) () -lemΛE refl (E ·⋆ A / q) () -lemΛE refl (unwrap E / q) () - --- apparently not... -lemΛE' : ∀{K}{B : ∅ ,⋆ K ⊢Nf⋆ *} - → ∀{L : ∅ ,⋆ K ⊢ B}{X}{L' : ∅ ⊢ X} - → (E : EC (Π B) X) - → Λ L ≡ E [ L' ]ᴱ - → ∃ λ (p : X ≡ Π B) - → substEq (EC (Π B)) p E ≡ EC.[] × Λ L ≡ substEq (∅ ⊢_) p L' -lemΛE' [] refl = refl ,, refl ,, refl --} + → t · u —→⋆ BUILTIN' b (step bt vu) ``` @@ -394,593 +354,26 @@ data _—↠_ : {A : ∅ ⊢Nf⋆ *} → ∅ ⊢ A → ∅ ⊢ A → Set → M —↠ M'' ``` -## Some auxiliary proofs used by Progress and Determinism. - -``` --- these two proofs are defined by pattern matching on the builtin, --- they are very long and very ugly. They could probably be made --- shorter by giving cases for particular types/arities, and adding a --- lemma that knocks off a more general class of imposible _<>>_∈_ --- inhabitants. - --- 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) - → BApp b p M → ∃ λ A' → ∃ λ A'' → A ≡ A' ⇒ A'' -bappTermLem addInteger _ (start _) (base refl) = _ ,, _ ,, refl -bappTermLem addInteger {as = as} _ (bubble {as = az} p) q - with <>>-cancel-both' az _ ([] :< Term :< Term) as p refl -bappTermLem addInteger _ (bubble (start _)) (step _ (base refl) _) - | refl ,, refl ,, refl = _ ,, _ ,, refl -bappTermLem subtractInteger _ (start _) (base refl) = _ ,, _ ,, refl -bappTermLem subtractInteger {as = as} _ (bubble {as = az} p) q - with <>>-cancel-both' az _ (([] :< Term) :< Term) as p refl -bappTermLem subtractInteger _ (bubble (start _)) (step _ (base refl) _) - | refl ,, refl ,, refl = _ ,, _ ,, refl -bappTermLem multiplyInteger _ (start _) (base refl) = _ ,, _ ,, refl -bappTermLem multiplyInteger {as = as} _ (bubble {as = az} p) q - with <>>-cancel-both' az _ (([] :< Term) :< Term) as p refl -bappTermLem multiplyInteger _ (bubble (start _)) (step _ (base refl) _) - | refl ,, refl ,, refl = _ ,, _ ,, refl -bappTermLem divideInteger _ (start _) (base refl) = _ ,, _ ,, refl -bappTermLem divideInteger {as = as} _ (bubble {as = az} p) q - with <>>-cancel-both' az _ (([] :< Term) :< Term) as p refl -bappTermLem divideInteger _ (bubble (start _)) (step _ (base refl) _) - | refl ,, refl ,, refl = _ ,, _ ,, refl -bappTermLem quotientInteger _ (start _) (base refl) = _ ,, _ ,, refl -bappTermLem quotientInteger {as = as} _ (bubble {as = az} p) q - with <>>-cancel-both' az _ (([] :< Term) :< Term) as p refl -bappTermLem quotientInteger _ (bubble (start _)) (step _ (base refl) _) - | refl ,, refl ,, refl = _ ,, _ ,, refl -bappTermLem remainderInteger _ (start _) (base refl) = _ ,, _ ,, refl -bappTermLem remainderInteger {as = as} _ (bubble {as = az} p) q - with <>>-cancel-both' az _ (([] :< Term) :< Term) as p refl -bappTermLem remainderInteger _ (bubble (start _)) (step _ (base refl) _) - | refl ,, refl ,, refl = _ ,, _ ,, refl -bappTermLem modInteger _ (start _) (base refl) = _ ,, _ ,, refl -bappTermLem modInteger {as = as} _ (bubble {as = az} p) q - with <>>-cancel-both' az _ (([] :< Term) :< Term) as p refl -bappTermLem modInteger _ (bubble (start _)) (step _ (base refl) _) - | refl ,, refl ,, refl = _ ,, _ ,, refl -bappTermLem lessThanInteger _ (start _) (base refl) = _ ,, _ ,, refl -bappTermLem lessThanInteger {as = as} _ (bubble {as = az} p) q - with <>>-cancel-both' az _ (([] :< Term) :< Term) as p refl -bappTermLem lessThanInteger _ (bubble (start _)) (step _ (base refl) _) - | refl ,, refl ,, refl = _ ,, _ ,, refl -bappTermLem lessThanEqualsInteger _ (start _) (base refl) = _ ,, _ ,, refl -bappTermLem lessThanEqualsInteger {as = as} _ (bubble {as = az} p) q - with <>>-cancel-both' az _ (([] :< Term) :< Term) as p refl -bappTermLem lessThanEqualsInteger _ (bubble (start _)) (step _ (base refl) _) - | refl ,, refl ,, refl = _ ,, _ ,, refl -bappTermLem equalsInteger _ (start _) (base refl) = _ ,, _ ,, refl -bappTermLem equalsInteger {as = as} _ (bubble {as = az} p) q - with <>>-cancel-both' az _ (([] :< Term) :< Term) as p refl -bappTermLem equalsInteger _ (bubble (start _)) (step _ (base refl) _) - | refl ,, refl ,, refl = _ ,, _ ,, refl -bappTermLem lessThanByteString _ (start _) (base refl) = _ ,, _ ,, refl -bappTermLem lessThanByteString {as = as} _ (bubble {as = az} p) q - with <>>-cancel-both' az _ (([] :< Term) :< Term) as p refl -bappTermLem lessThanByteString _ (bubble (start _)) (step _ (base refl) _) - | refl ,, refl ,, refl = _ ,, _ ,, refl -bappTermLem sha2-256 {az = az} {as} M p q - with <>>-cancel-both az ([] :< Term) as p -bappTermLem sha2-256 _ (start _) (base refl) | refl ,, refl = _ ,, _ ,, refl -bappTermLem sha3-256 {az = az} {as} M p q - with <>>-cancel-both az ([] :< Term) as p -bappTermLem sha3-256 _ (start _) (base refl) | refl ,, refl = _ ,, _ ,, refl -bappTermLem verifyEd25519Signature _ (start _) (base refl) = _ ,, _ ,, refl -bappTermLem verifyEd25519Signature _ (bubble (start _)) (step (start _) (base refl) _) = - _ ,, _ ,, refl -bappTermLem verifyEd25519Signature {as = as} _ (bubble (bubble {as = az} p)) q - with <>>-cancel-both' az _ ((([] :< Term) :< Term) :< Term) as p refl -bappTermLem verifyEd25519Signature - _ - (bubble (bubble (start _))) - (step _ (step _ (base refl) _) _) - | refl ,, refl ,, refl = _ ,, _ ,, refl -bappTermLem verifyEcdsaSecp256k1Signature _ (start _) (base refl) = _ ,, _ ,, refl -bappTermLem verifyEcdsaSecp256k1Signature _ (bubble (start _)) (step (start _) (base refl) _) = - _ ,, _ ,, refl -bappTermLem verifyEcdsaSecp256k1Signature {as = as} _ (bubble (bubble {as = az} p)) q - with <>>-cancel-both' az _ ((([] :< Term) :< Term) :< Term) as p refl -bappTermLem verifyEcdsaSecp256k1Signature - _ - (bubble (bubble (start _))) - (step _ (step _ (base refl) _) _) - | refl ,, refl ,, refl = _ ,, _ ,, refl -bappTermLem verifySchnorrSecp256k1Signature _ (start _) (base refl) = _ ,, _ ,, refl -bappTermLem verifySchnorrSecp256k1Signature _ (bubble (start _)) (step (start _) (base refl) _) = - _ ,, _ ,, refl -bappTermLem verifySchnorrSecp256k1Signature {as = as} _ (bubble (bubble {as = az} p)) q - with <>>-cancel-both' az _ ((([] :< Term) :< Term) :< Term) as p refl -bappTermLem verifySchnorrSecp256k1Signature - _ - (bubble (bubble (start _))) - (step _ (step _ (base refl) _) _) - | refl ,, refl ,, refl = _ ,, _ ,, refl -bappTermLem equalsByteString _ (start _) (base refl) = _ ,, _ ,, refl -bappTermLem equalsByteString {as = as} _ (bubble {as = az} p) q - with <>>-cancel-both' az _ (([] :< Term) :< Term) as p refl -bappTermLem equalsByteString _ (bubble (start _)) (step _ (base refl) _) - | refl ,, refl ,, refl = _ ,, _ ,, refl -bappTermLem ifThenElse _ (bubble (start _)) (step⋆ (start _) (base refl) refl) = - _ ,, _ ,, refl -bappTermLem ifThenElse - _ - (bubble (bubble (start _))) - (step _ (step⋆ _ (base refl) refl) _) = _ ,, _ ,, refl -bappTermLem ifThenElse _ (bubble (bubble (bubble {as = az} p))) q - with <>>-cancel-both' az _ ([] <>< arity ifThenElse) _ p refl -bappTermLem ifThenElse - _ - (bubble (bubble (bubble (start _)))) - (step _ (step _ (step⋆ _ (base refl) refl) _) _) - | refl ,, refl ,, refl = _ ,, _ ,, refl -bappTermLem trace {as = .(Term ∷ [])} _ (bubble (start .(Type ∷ Term ∷ Term ∷ []))) (step⋆ .(start (Type ∷ Term ∷ Term ∷ [])) (base refl) refl) = _ ,, _ ,, refl -bappTermLem trace {as = as} _ (bubble (bubble {as = az} p)) q with <>>-cancel-both' az _ ([] <>< arity trace) _ p refl -bappTermLem trace {as = .[]} _ (bubble (bubble {as = _} (start .(Type ∷ Term ∷ Term ∷ [])))) (step .(bubble (start (Type ∷ Term ∷ Term ∷ []))) (step⋆ .(start (Type ∷ Term ∷ Term ∷ [])) (base refl) refl) x) | refl ,, refl ,, refl = _ ,, _ ,, refl -bappTermLem equalsString _ (start _) (base refl) = _ ,, _ ,, refl -bappTermLem equalsString {as = as} _ (bubble {as = az} p) q - with <>>-cancel-both' az _ (([] :< Term) :< Term) as p refl -bappTermLem equalsString _ (bubble (start _)) (step _ (base refl) _) - | refl ,, refl ,, refl = _ ,, _ ,, refl -bappTermLem encodeUtf8 {az = az} {as} M p q - with <>>-cancel-both az ([] :< Term) as p -bappTermLem encodeUtf8 _ (start _) (base refl) | refl ,, refl = _ ,, _ ,, refl -bappTermLem decodeUtf8 {az = az} {as} M p q - with <>>-cancel-both az ([] :< Term) as p -bappTermLem decodeUtf8 _ (start _) (base refl) | refl ,, refl = _ ,, _ ,, refl -bappTermLem fstPair _ (bubble (bubble {as = az} p)) q - with <>>-cancel-both' az _ ([] <>< arity fstPair) _ p refl -bappTermLem fstPair - _ - (bubble (bubble (start _))) - (step⋆ _ (step⋆ _ (base refl) refl) refl) - | refl ,, refl ,, refl = _ ,, _ ,, refl -bappTermLem sndPair _ (bubble (bubble {as = az} p)) q - with <>>-cancel-both' az _ ([] <>< arity fstPair) _ p refl -bappTermLem sndPair - _ - (bubble (bubble (start _))) - (step⋆ _ (step⋆ _ (base refl) refl) refl) - | refl ,, refl ,, refl = _ ,, _ ,, refl -bappTermLem nullList _ (bubble {as = az} p) q - with <>>-cancel-both' az _ ([] <>< arity nullList) _ p refl -bappTermLem nullList _ (bubble (start _)) (step⋆ _ (base refl) refl) - | refl ,, refl ,, refl = _ ,, _ ,, refl -bappTermLem headList _ (bubble {as = az} p) q - with <>>-cancel-both' az _ ([] <>< arity nullList) _ p refl -bappTermLem headList _ (bubble (start _)) (step⋆ _ (base refl) refl) - | refl ,, refl ,, refl = _ ,, _ ,, refl -bappTermLem tailList _ (bubble {as = az} p) q - with <>>-cancel-both' az _ ([] <>< arity nullList) _ p refl -bappTermLem tailList _ (bubble (start _)) (step⋆ _ (base refl) refl) - | refl ,, refl ,, refl = _ ,, _ ,, refl -bappTermLem chooseList - _ - (bubble (bubble (start _))) - (step⋆ _ (step⋆ _ (base refl) refl) refl) - = _ ,, _ ,, refl -bappTermLem chooseList - _ - (bubble (bubble (bubble (start _)))) - (step _ (step⋆ _ (step⋆ _ (base refl) refl) refl) x) - = _ ,, _ ,, refl -bappTermLem chooseList _ (bubble (bubble (bubble (bubble {as = az} p)))) q - with <>>-cancel-both' az _ ([] <>< arity chooseList) _ p refl -bappTermLem chooseList - _ - (bubble (bubble (bubble (bubble (start _))))) - (step _ (step _ (step⋆ _ (step⋆ _ (base refl) refl) refl) _) _) - | refl ,, refl ,, refl = _ ,, _ ,, refl -bappTermLem constrData _ (start _) (base refl) = _ ,, _ ,, refl -bappTermLem constrData {as = as} _ (bubble {as = az} p) q - with <>>-cancel-both' az _ (([] :< Term) :< Term) as p refl -bappTermLem constrData _ (bubble (start _)) (step _ (base refl) _) - | refl ,, refl ,, refl = _ ,, _ ,, refl -bappTermLem mapData {az = az} {as} M p q - with <>>-cancel-both az ([] :< Term) as p -bappTermLem mapData _ (start _) (base refl) | refl ,, refl = _ ,, _ ,, refl -bappTermLem listData {az = az} {as} M p q - with <>>-cancel-both az ([] :< Term) as p -bappTermLem listData _ (start _) (base refl) | refl ,, refl = _ ,, _ ,, refl -bappTermLem iData {az = az} {as} M p q - with <>>-cancel-both az ([] :< Term) as p -bappTermLem iData _ (start _) (base refl) | refl ,, refl = _ ,, _ ,, refl -bappTermLem bData {az = az} {as} M p q - with <>>-cancel-both az ([] :< Term) as p -bappTermLem bData _ (start _) (base refl) | refl ,, refl = _ ,, _ ,, refl -bappTermLem unConstrData {az = az} {as} M p q - with <>>-cancel-both az ([] :< Term) as p -bappTermLem unConstrData _ (start _) (base refl) | refl ,, refl = _ ,, _ ,, refl -bappTermLem unMapData {az = az} {as} M p q - with <>>-cancel-both az ([] :< Term) as p -bappTermLem unMapData _ (start _) (base refl) | refl ,, refl = _ ,, _ ,, refl -bappTermLem unListData {az = az} {as} M p q - with <>>-cancel-both az ([] :< Term) as p -bappTermLem unListData _ (start _) (base refl) | refl ,, refl = _ ,, _ ,, refl -bappTermLem unIData {az = az} {as} M p q - with <>>-cancel-both az ([] :< Term) as p -bappTermLem unIData _ (start _) (base refl) | refl ,, refl = _ ,, _ ,, refl -bappTermLem unBData {az = az} {as} M p q - with <>>-cancel-both az ([] :< Term) as p -bappTermLem unBData _ (start _) (base refl) | refl ,, refl = _ ,, _ ,, refl -bappTermLem equalsData _ (start _) (base refl) = _ ,, _ ,, refl -bappTermLem equalsData {as = as} _ (bubble {as = az} p) q - with <>>-cancel-both' az _ (([] :< Term) :< Term) as p refl -bappTermLem equalsData _ (bubble (start _)) (step _ (base refl) _) - | refl ,, refl ,, refl = _ ,, _ ,, refl -bappTermLem serialiseData {az = az} {as} M p q - with <>>-cancel-both az ([] :< Term) as p -bappTermLem serialiseData _ (start _) (base refl) | refl ,, refl = _ ,, _ ,, refl -bappTermLem chooseData _ (bubble (start _)) (step⋆ _ (base refl) refl) = - _ ,, _ ,, refl -bappTermLem chooseData - _ - (bubble (bubble (start _))) - (step _ (step⋆ _ (base refl) refl) _) - = _ ,, _ ,, refl -bappTermLem chooseData - _ - (bubble (bubble (bubble (start _)))) - (step _ (step _ (step⋆ _ (base refl) refl) _) _) - = _ ,, _ ,, refl -bappTermLem chooseData - _ - (bubble (bubble (bubble (bubble (start _))))) - (step _ (step _ (step _ (step⋆ _ (base refl) refl) _) _) _) - = _ ,, _ ,, refl -bappTermLem chooseData - _ - (bubble (bubble (bubble (bubble (bubble (start _)))))) - (step _ (step _ (step _ (step _ (step⋆ _ (base refl) refl) _) _) _) _) - = _ ,, _ ,, refl -bappTermLem chooseData - _ - (bubble (bubble (bubble (bubble (bubble (bubble {as = az} p)))))) q - with <>>-cancel-both' az _ ([] <>< arity chooseData) _ p refl -bappTermLem - chooseData - _ - (bubble (bubble (bubble (bubble (bubble (bubble (start _))))))) - (step _ (step _ (step _ (step _ (step _ (step⋆ _ (base refl) refl)_)_)_)_)_) - | refl ,, refl ,, refl = _ ,, _ ,, refl -bappTermLem chooseUnit _ (bubble (start _)) (step⋆ _ (base refl) refl) = - _ ,, _ ,, refl -bappTermLem chooseUnit _ (bubble (bubble {as = az} p)) q - with <>>-cancel-both' az _ ((([] :< Type) :< Term) :< Term) _ p refl -bappTermLem chooseUnit - _ - (bubble (bubble (start _))) - (step _ (step⋆ _ (base refl) refl) x) - | refl ,, refl ,, refl = _ ,, _ ,, refl -bappTermLem mkPairData _ (start _) (base refl) = _ ,, _ ,, refl -bappTermLem mkPairData {as = as} _ (bubble {as = az} p) q - with <>>-cancel-both' az _ (([] :< Term) :< Term) as p refl -bappTermLem mkPairData _ (bubble (start _)) (step _ (base refl) _) - | refl ,, refl ,, refl = _ ,, _ ,, refl -bappTermLem mkNilData {az = az} {as} M p q - with <>>-cancel-both az ([] :< Term) as p -bappTermLem mkNilData _ (start _) (base refl) | refl ,, refl = _ ,, _ ,, refl -bappTermLem mkNilPairData {az = az} {as} M p q - with <>>-cancel-both az ([] :< Term) as p -bappTermLem mkNilPairData _ (start _) (base refl) | refl ,, refl = _ ,, _ ,, refl -bappTermLem mkCons _ (bubble (start _)) (step⋆ _ (base refl) refl) = - _ ,, _ ,, refl -bappTermLem mkCons _ (bubble (bubble {as = az} p)) q - with <>>-cancel-both' az _ ((([] :< Type) :< Term) :< Term) _ p refl -bappTermLem mkCons - _ - (bubble (bubble (start _))) - (step _ (step⋆ _ (base refl) refl) x) - | refl ,, refl ,, refl = _ ,, _ ,, refl -bappTermLem appendByteString _ _ (base refl) = _ ,, _ ,, 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 = .[]} (.(builtin appendByteString / refl) · M') (bubble (start .(Term ∷ Term ∷ []))) (step {az = _} (start .(Term ∷ Term ∷ [])) (base refl) x) - | refl ,, refl = _ ,, _ ,, refl -bappTermLem appendByteString {as = as} M .(bubble p) (step⋆ {az = az} p q q₁) - with <>>-cancel-both' az (([] :< Type) :< Term) (([] :< Term) :< Term) as p refl -... | refl ,, refl ,, () -bappTermLem lessThanEqualsByteString _ (start _) (base refl) = _ ,, _ ,, refl -bappTermLem lessThanEqualsByteString {as = as} _ (bubble {as = az} p) q - with <>>-cancel-both' az _ (([] :< Term) :< Term) as p refl -bappTermLem lessThanEqualsByteString _ (bubble (start _)) (step _ (base refl) _) - | refl ,, refl ,, refl = _ ,, _ ,, refl -bappTermLem appendString _ (start _) (base refl) = _ ,, _ ,, refl -bappTermLem appendString {as = as} _ (bubble {as = az} p) q - with <>>-cancel-both' az _ (([] :< Term) :< Term) as p refl -bappTermLem appendString _ (bubble (start _)) (step _ (base refl) _) - | refl ,, refl ,, refl = _ ,, _ ,, refl -bappTermLem consByteString _ (start _) (base refl) = _ ,, _ ,, refl -bappTermLem consByteString {as = as} _ (bubble {as = az} p) q - with <>>-cancel-both' az _ (([] :< Term) :< Term) as p refl -bappTermLem consByteString _ (bubble (start _)) (step _ (base refl) _) - | refl ,, refl ,, refl = _ ,, _ ,, refl -bappTermLem sliceByteString _ (start _) (base refl) = _ ,, _ ,, refl -bappTermLem sliceByteString _ (bubble (start _)) (step (start _) (base refl) _) = - _ ,, _ ,, refl -bappTermLem sliceByteString {as = as} _ (bubble (bubble {as = az} p)) q - with <>>-cancel-both' az _ ((([] :< Term) :< Term) :< Term) as p refl -bappTermLem sliceByteString - _ - (bubble (bubble (start _))) - (step _ (step _ (base refl) _) _) - | refl ,, refl ,, refl = _ ,, _ ,, refl -bappTermLem lengthOfByteString {az = az} {as} M p q - with <>>-cancel-both az ([] :< Term) as p -bappTermLem lengthOfByteString _ (start _) (base refl) | refl ,, refl = _ ,, _ ,, refl -bappTermLem indexByteString _ (start _) (base refl) = _ ,, _ ,, refl -bappTermLem indexByteString {as = as} _ (bubble {as = az} p) q - with <>>-cancel-both' az _ (([] :< Term) :< Term) as p refl -bappTermLem indexByteString _ (bubble (start _)) (step _ (base refl) _) - | refl ,, refl ,, refl = _ ,, _ ,, refl -bappTermLem blake2b-256 {az = az} {as} M p q - with <>>-cancel-both az ([] :< Term) as p -bappTermLem blake2b-256 _ (start _) (base refl) | refl ,, refl = _ ,, _ ,, refl -``` - -``` -bappTypeLem : ∀ b {A}{az as}(M : ∅ ⊢ A)(p : az <>> (Type ∷ as) ∈ arity b) - → BApp b p M → ∃ λ K → ∃ λ (B : ∅ ,⋆ K ⊢Nf⋆ *) → A ≡ Π B -bappTypeLem addInteger _ (bubble {as = az} p) _ - with <>>-cancel-both' az _ (([] :< Term) :< Term) _ p refl -... | refl ,, refl ,, () -bappTypeLem subtractInteger _ (bubble {as = az} p) _ - with <>>-cancel-both' az _ (([] :< Term) :< Term) _ p refl -... | refl ,, refl ,, () -bappTypeLem multiplyInteger _ (bubble {as = az} p) _ - with <>>-cancel-both' az _ (([] :< Term) :< Term) _ p refl -... | refl ,, refl ,, () -bappTypeLem divideInteger _ (bubble {as = az} p) _ - with <>>-cancel-both' az _ (([] :< Term) :< Term) _ p refl -... | refl ,, refl ,, () -bappTypeLem quotientInteger _ (bubble {as = az} p) _ - with <>>-cancel-both' az _ (([] :< Term) :< Term) _ p refl -... | refl ,, refl ,, () -bappTypeLem remainderInteger _ (bubble {as = az} p) _ - with <>>-cancel-both' az _ (([] :< Term) :< Term) _ p refl -... | refl ,, refl ,, () -bappTypeLem modInteger _ (bubble {as = az} p) _ - with <>>-cancel-both' az _ (([] :< Term) :< Term) _ p refl -... | refl ,, refl ,, () -bappTypeLem lessThanInteger _ (bubble {as = az} p) _ - with <>>-cancel-both' az _ (([] :< Term) :< Term) _ p refl -... | refl ,, refl ,, () -bappTypeLem lessThanEqualsInteger _ (bubble {as = az} p) _ - with <>>-cancel-both' az _ (([] :< Term) :< Term) _ p refl -... | refl ,, refl ,, () -bappTypeLem equalsInteger _ (bubble {as = az} p) _ - with <>>-cancel-both' az _ (([] :< Term) :< Term) _ p refl -... | refl ,, refl ,, () -bappTypeLem lessThanByteString _ (bubble {as = az} p) _ - with <>>-cancel-both' az _ (([] :< Term) :< Term) _ p refl -... | refl ,, refl ,, () -bappTypeLem sha2-256 {az = az} _ p _ - with <>>-cancel-both' az _ ([] :< Term) _ p refl -... | refl ,, refl ,, () -bappTypeLem sha3-256 {az = az} _ p _ - with <>>-cancel-both' az _ ([] :< Term) _ p refl -... | refl ,, refl ,, () -bappTypeLem verifyEd25519Signature _ (bubble (bubble {as = az} p)) _ - with <>>-cancel-both' az _ ([] <>< arity verifyEd25519Signature) _ p refl -... | refl ,, refl ,, () -bappTypeLem verifyEcdsaSecp256k1Signature _ (bubble (bubble {as = az} p)) _ - with <>>-cancel-both' az _ ([] <>< arity verifyEcdsaSecp256k1Signature) _ p refl -... | refl ,, refl ,, () -bappTypeLem verifySchnorrSecp256k1Signature _ (bubble (bubble {as = az} p)) _ - with <>>-cancel-both' az _ ([] <>< arity verifySchnorrSecp256k1Signature) _ p refl -... | refl ,, refl ,, () -bappTypeLem equalsByteString _ (bubble {as = az} p) _ - with <>>-cancel-both' az _ (([] :< Term) :< Term) _ p refl -... | refl ,, refl ,, () -bappTypeLem ifThenElse _ (start _) (base refl) = _ ,, _ ,, refl -bappTypeLem ifThenElse _ (bubble (bubble (bubble {as = az} p))) _ - with <>>-cancel-both' az _ ([] <>< arity ifThenElse) _ p refl -... | _ ,, _ ,, () -bappTypeLem trace _ (start _) (base refl) = _ ,, _ ,, refl -bappTypeLem trace M (bubble (bubble {as = az} p)) q with <>>-cancel-both' az _ ([] <>< arity trace) _ p refl -... | _ ,, _ ,, () -bappTypeLem equalsString _ (bubble {as = az} p) _ - with <>>-cancel-both' az _ (([] :< Term) :< Term) _ p refl -... | refl ,, refl ,, () -bappTypeLem encodeUtf8 {az = az} _ p _ - with <>>-cancel-both' az _ ([] :< Term) _ p refl -... | refl ,, refl ,, () -bappTypeLem decodeUtf8 {az = az} _ p _ - with <>>-cancel-both' az _ ([] :< Term) _ p refl -... | refl ,, refl ,, () -bappTypeLem fstPair _ (start _) (base refl) = _ ,, _ ,, refl -bappTypeLem fstPair _ (bubble (start _)) (step⋆ _ (base refl) refl) = - _ ,, _ ,, refl -bappTypeLem fstPair _ (bubble (bubble {as = az} p)) _ - with <>>-cancel-both' az _ ((([] :< Type) :< Type) :< Term) _ p refl -... | refl ,, refl ,, () -bappTypeLem sndPair _ (start _) (base refl) = _ ,, _ ,, refl -bappTypeLem sndPair _ (bubble (start _)) (step⋆ _ (base refl) refl) = - _ ,, _ ,, refl -bappTypeLem sndPair _ (bubble (bubble {as = az} p)) _ - with <>>-cancel-both' az _ ((([] :< Type) :< Type) :< Term) _ p refl -... | refl ,, refl ,, () -bappTypeLem bData {az = az} _ p q - with <>>-cancel-both' az _ ([] :< Term) _ p refl -... | refl ,, refl ,, () -bappTypeLem unConstrData {az = az} _ p q - with <>>-cancel-both' az _ ([] :< Term) _ p refl -... | refl ,, refl ,, () -bappTypeLem unMapData {az = az} _ p q - with <>>-cancel-both' az _ ([] :< Term) _ p refl -... | refl ,, refl ,, () -bappTypeLem unListData {az = az} _ p q - with <>>-cancel-both' az _ ([] :< Term) _ p refl -... | refl ,, refl ,, () -bappTypeLem unIData {az = az} _ p q - with <>>-cancel-both' az _ ([] :< Term) _ p refl -... | refl ,, refl ,, () -bappTypeLem unBData {az = az} _ p q - with <>>-cancel-both' az _ ([] :< Term) _ p refl -... | refl ,, refl ,, () -bappTypeLem equalsData _ (bubble {as = az} p) _ - with <>>-cancel-both' az _ (([] :< Term) :< Term) _ p refl -... | refl ,, refl ,, () -bappTypeLem serialiseData {az = az} _ p q - with <>>-cancel-both' az _ ([] :< Term) _ p refl -... | refl ,, refl ,, () -bappTypeLem chooseData _ (start _) (base refl) = _ ,, _ ,, refl -bappTypeLem chooseData _ (bubble (bubble (bubble (bubble (bubble (bubble {as = az} p)))))) _ - with <>>-cancel-both' az _ ([] <>< arity chooseData) _ p refl -... | _ ,, _ ,, () -bappTypeLem chooseUnit _ (start _) (base refl) = _ ,, _ ,, refl -bappTypeLem chooseUnit _ (bubble (bubble {as = az} p)) _ - with <>>-cancel-both' az _ ([] <>< arity chooseUnit) _ p refl -... | _ ,, _ ,, () -bappTypeLem mkPairData _ (bubble {as = az} p) q - with <>>-cancel-both' az _ (([] :< Term) :< Term) _ p refl -... | refl ,, refl ,, () -bappTypeLem mkNilData {az = az} _ p q - with <>>-cancel-both' az _ ([] :< Term) _ p refl -... | refl ,, refl ,, () -bappTypeLem mkNilPairData {az = az} _ p q - with <>>-cancel-both' az _ ([] :< Term) _ p refl -... | refl ,, refl ,, () -bappTypeLem appendString {as = as} .(_ · _) .(bubble p) (step {az = az} p q x) - with <>>-cancel-both' az (([] :< Term) :< Type) (([] :< Term) :< Term) as p refl -... | refl ,, refl ,, () -bappTypeLem appendString {as = as} M .(bubble p) (step⋆ {az = az} p q q₁) - with <>>-cancel-both' az (([] :< Type) :< Type) (([] :< Term) :< Term) as p refl -... | refl ,, refl ,, () -bappTypeLem mkCons _ (start _) (base refl) = _ ,, _ ,, refl -bappTypeLem mkCons _ (bubble (bubble {as = az} p)) _ - with <>>-cancel-both' az _ ([] <>< arity mkCons) _ p refl -... | _ ,, _ ,, () -bappTypeLem nullList _ (start _) (base refl) = _ ,, _ ,, refl -bappTypeLem nullList _ (bubble {as = az} p) _ - with <>>-cancel-both' az _ (([] :< Type) :< Term) _ p refl -... | refl ,, refl ,, () -bappTypeLem headList _ (start _) (base refl) = _ ,, _ ,, refl -bappTypeLem headList _ (bubble {as = az} p) _ - with <>>-cancel-both' az _ (([] :< Type) :< Term) _ p refl -... | refl ,, refl ,, () -bappTypeLem tailList _ (start _) (base refl) = _ ,, _ ,, refl -bappTypeLem tailList _ (bubble {as = az} p) _ - with <>>-cancel-both' az _ (([] :< Type) :< Term) _ p refl -... | refl ,, refl ,, () -bappTypeLem chooseList _ (start _) (base refl) = _ ,, _ ,, refl -bappTypeLem chooseList _ (bubble (start _)) (step⋆ _ (base refl) refl) = - _ ,, _ ,, refl -bappTypeLem chooseList _ (bubble (bubble (bubble (bubble {as = az} p)))) _ - with <>>-cancel-both' az _ ([] <>< arity chooseList) _ p refl -... | _ ,, _ ,, () -bappTypeLem appendByteString _ (bubble {as = az} p) _ - with <>>-cancel-both' az _ (([] :< Term) :< Term) _ p refl -... | refl ,, refl ,, () -bappTypeLem constrData _ (bubble {as = az} p) _ - with <>>-cancel-both' az _ (([] :< Term) :< Term) _ p refl -... | refl ,, refl ,, () -bappTypeLem mapData {az = az} _ p q - with <>>-cancel-both' az _ ([] :< Term) _ p refl -... | refl ,, refl ,, () -bappTypeLem listData {az = az} _ p q - with <>>-cancel-both' az _ ([] :< Term) _ p refl -... | refl ,, refl ,, () -bappTypeLem iData {az = az} _ p q - with <>>-cancel-both' az _ ([] :< Term) _ p refl -... | refl ,, refl ,, () -bappTypeLem lessThanEqualsByteString _ (bubble {as = az} p) _ - with <>>-cancel-both' az _ (([] :< Term) :< Term) _ p refl -... | refl ,, refl ,, () -bappTypeLem consByteString _ (bubble {as = az} p) q - with <>>-cancel-both' az _ (([] :< Term) :< Term) _ p refl -... | refl ,, refl ,, () -bappTypeLem sliceByteString _ (bubble (bubble {as = az} p)) q - with <>>-cancel-both' az _ ((([] :< Term) :< Term) :< Term) _ p refl -... | refl ,, refl ,, () -bappTypeLem lengthOfByteString {az = az} _ p q - with <>>-cancel-both' az _ ([] :< Term) _ p refl -... | refl ,, refl ,, () -bappTypeLem indexByteString _ (bubble {as = az} p) q - with <>>-cancel-both' az _ (([] :< Term) :< Term) _ p refl -... | refl ,, refl ,, () -bappTypeLem blake2b-256 {az = az} _ p q - with <>>-cancel-both' az _ ([] :< Term) _ p refl -... | refl ,, refl ,, () -``` - A smart constructor that looks at the arity and then puts on the right constructor ``` -V-I : ∀ b {A : ∅ ⊢Nf⋆ *}{a as as'} - → (p : as <>> a ∷ as' ∈ arity b) +V-I : ∀ (b : Builtin) {A : ∅ ⊢Nf⋆ *} + → ∀{tn tm} {pt : tn ∔ tm ≣ fv♯ (signature b)} + → ∀{an am} {pa : an ∔ suc am ≣ args♯ (signature b)} + → {σA : SigTy pt pa A} → {t : ∅ ⊢ A} - → BApp b p t + → BApp b σA t → Value t -V-I b {a = Term} p q with bappTermLem b _ p q -... | _ ,, _ ,, refl = V-I⇒ b p q -V-I b {a = Type} p q with bappTypeLem b _ p q -... | _ ,, _ ,, refl = V-IΠ b p q +V-I b {tm = zero} {σA = A B⇒ σA} bt = V-I⇒ b bt +V-I b {tm = suc tm} {σA = sucΠ σA} bt = V-IΠ b bt ``` For each builtin, return the value corresponding to the completely unapplied builtin ``` ival : ∀ b → Value (builtin b / refl) +ival b = V-I b base +-- -} +``` --- ival b = V-I b (start _) (base refl) --- ^ not possible as we could have a builtin with no args - -ival addInteger = V-I⇒ addInteger (start _) (base refl) -ival subtractInteger = V-I⇒ subtractInteger (start _) (base refl) -ival multiplyInteger = V-I⇒ multiplyInteger (start _) (base refl) -ival divideInteger = V-I⇒ divideInteger (start _) (base refl) -ival quotientInteger = V-I⇒ quotientInteger (start _) (base refl) -ival remainderInteger = V-I⇒ remainderInteger (start _) (base refl) -ival modInteger = V-I⇒ modInteger (start _) (base refl) -ival lessThanInteger = V-I⇒ lessThanInteger (start _) (base refl) -ival lessThanEqualsInteger = V-I⇒ lessThanEqualsInteger (start _) (base refl) -ival lessThanByteString = V-I⇒ lessThanByteString (start _) (base refl) -ival sha2-256 = V-I⇒ sha2-256 (start _) (base refl) -ival sha3-256 = V-I⇒ sha3-256 (start _) (base refl) -ival verifyEd25519Signature = V-I⇒ verifyEd25519Signature (start _) (base refl) -ival verifyEcdsaSecp256k1Signature = V-I⇒ verifyEcdsaSecp256k1Signature (start _) (base refl) -ival verifySchnorrSecp256k1Signature = V-I⇒ verifySchnorrSecp256k1Signature (start _) (base refl) -ival equalsByteString = V-I⇒ equalsByteString (start _) (base refl) -ival ifThenElse = V-IΠ ifThenElse (start _) (base refl) -ival trace = V-IΠ trace (start _) (base refl) -ival equalsString = V-I _ (start _) (base refl) -ival encodeUtf8 = V-I _ (start _) (base refl) -ival decodeUtf8 = V-I _ (start _) (base refl) -ival fstPair = V-I _ (start _) (base refl) -ival sndPair = V-I _ (start _) (base refl) -ival nullList = V-I _ (start _) (base refl) -ival headList = V-I _ (start _) (base refl) -ival tailList = V-I _ (start _) (base refl) -ival chooseList = V-I _ (start _) (base refl) -ival constrData = V-I _ (start _) (base refl) -ival mapData = V-I _ (start _) (base refl) -ival listData = V-I _ (start _) (base refl) -ival iData = V-I _ (start _) (base refl) -ival bData = V-I _ (start _) (base refl) -ival unConstrData = V-I _ (start _) (base refl) -ival unMapData = V-I _ (start _) (base refl) -ival unListData = V-I _ (start _) (base refl) -ival unIData = V-I _ (start _) (base refl) -ival unBData = V-I _ (start _) (base refl) -ival equalsData = V-I _ (start _) (base refl) -ival serialiseData = V-I _ (start _) (base refl) -ival chooseData = V-I _ (start _) (base refl) -ival chooseUnit = V-I _ (start _) (base refl) -ival mkPairData = V-I _ (start _) (base refl) -ival mkNilData = V-I _ (start _) (base refl) -ival mkNilPairData = V-I _ (start _) (base refl) -ival mkCons = V-I _ (start _) (base refl) -ival equalsInteger = V-I⇒ equalsInteger (start _) (base refl) -ival appendByteString = V-I⇒ appendByteString (start _) (base refl) -ival appendString = V-I⇒ appendString (start _) (base refl) -ival lessThanEqualsByteString = V-I⇒ lessThanEqualsByteString (start _) (base refl) -ival consByteString = V-I⇒ consByteString (start _) (base refl) -ival sliceByteString = V-I⇒ sliceByteString (start _) (base refl) -ival lengthOfByteString = V-I⇒ lengthOfByteString (start _) (base refl) -ival indexByteString = V-I⇒ indexByteString (start _) (base refl) -ival blake2b-256 = V-I⇒ blake2b-256 (start _) (base refl) -``` \ No newline at end of file diff --git a/plutus-metatheory/src/Algorithmic/ReductionEC/Determinism.lagda.md b/plutus-metatheory/src/Algorithmic/ReductionEC/Determinism.lagda.md index 9636cc7c702..b59b02d0730 100644 --- a/plutus-metatheory/src/Algorithmic/ReductionEC/Determinism.lagda.md +++ b/plutus-metatheory/src/Algorithmic/ReductionEC/Determinism.lagda.md @@ -18,7 +18,7 @@ open import Utils hiding (TermCon) open import Type using (Ctx⋆;∅;_,⋆_;_⊢⋆_;_∋⋆_;Z) open _⊢⋆_ import Type.RenamingSubstitution as T -open import Algorithmic using (Ctx;_⊢_;arity;Term;Type;conv⊢) +open import Algorithmic using (Ctx;_⊢_;Arity;Term;Type;conv⊢) renaming (arity to sigarity) open Ctx open _⊢_ open import Algorithmic.RenamingSubstitution using (_[_];_[_]⋆) @@ -28,6 +28,10 @@ open import Type.BetaNBE.RenamingSubstitution using (_[_]Nf) open import Type.BetaNormal using (_⊢Nf⋆_;embNf;weakenNf) open _⊢Nf⋆_ open import Algorithmic.ReductionEC +open import Builtin using (Builtin;signature) + +arity : (b : Builtin) -> Arity +arity b = sigarity (signature b) ``` ``` @@ -192,16 +196,16 @@ valred (V-I⇒ b .(bubble p₁) (step⋆ p₁ () .p)) (β-Λ p) valred (V-IΠ b .(bubble p₁) (step⋆ p₁ () .p)) (β-Λ p) valred (V-I⇒ b p₁ ()) (β-wrap VN p) valred (V-IΠ b p₁ ()) (β-wrap VN p) -valred (V-I⇒ b₁ .(bubble p₁) (step p₁ x x₁)) (β-sbuiltin b t p bt u vu) +valred (V-I⇒ b₁ .(bubble p₁) (step p₁ x x₁)) (β-builtin b t p bt u vu) with uniqueBApp' t p₁ p x bt ... | refl ,, refl ,, () ,, refl -valred (V-IΠ b₁ .(bubble p₁) (step p₁ x x₁)) (β-sbuiltin b t p bt u vu) +valred (V-IΠ b₁ .(bubble p₁) (step p₁ x x₁)) (β-builtin b t p bt u vu) with uniqueBApp' t p₁ p x bt ... | refl ,, refl ,, () ,, refl -valred (V-I⇒ b₁ .(bubble p₁) (step⋆ p₁ x q)) (β-sbuiltin⋆ b t p bt A q) +valred (V-I⇒ b₁ .(bubble p₁) (step⋆ p₁ x q)) (β-builtin⋆ b t p bt A q) with uniqueBApp' t p₁ p x bt ... | refl ,, refl ,, () ,, refl -valred (V-IΠ b₁ .(bubble p₁) (step⋆ p₁ x q)) (β-sbuiltin⋆ b t p bt A r) +valred (V-IΠ b₁ .(bubble p₁) (step⋆ p₁ x q)) (β-builtin⋆ b t p bt A r) with uniqueBApp' t p₁ p x bt ... | refl ,, refl ,, () ,, refl @@ -239,9 +243,9 @@ determinism⋆ : ∀{A}{L N N' : ∅ ⊢ A} → L —→⋆ N → L —→⋆ N' determinism⋆ (β-ƛ _) (β-ƛ _) = refl determinism⋆ (β-Λ refl) (β-Λ refl) = refl determinism⋆ (β-wrap _ refl) (β-wrap _ refl) = refl -determinism⋆ (β-sbuiltin b t p bt u vu) (β-sbuiltin b' .t p' bt' .u vu') = +determinism⋆ (β-builtin b t p bt u vu) (β-builtin b' .t p' bt' .u vu') = BUILTIN-eq _ (bubble p) (bubble p') (step p bt vu) (step p' bt' vu') -determinism⋆ (β-sbuiltin⋆ b t p bt A refl) (β-sbuiltin⋆ b' .t p' bt' .A refl) = +determinism⋆ (β-builtin⋆ b t p bt A refl) (β-builtin⋆ b' .t p' bt' .A refl) = BUILTIN-eq _ (bubble p) (bubble p') (step⋆ p bt refl) (step⋆ p' bt' refl) data Redex {A : ∅ ⊢Nf⋆ *} : ∅ ⊢ A → Set where @@ -311,7 +315,7 @@ U·⋆2 : ∀{K}{C}{A : ∅ ⊢Nf⋆ K}{B : ∅ ,⋆ K ⊢Nf⋆ *}{M : ∅ ⊢ ≡ E' × substEq (_⊢_ ∅) p₁ L ≡ L') U·⋆2 ¬VM eq [] refl (β (β-Λ .eq)) U = ⊥-elim (¬VM (V-Λ _)) -U·⋆2 ¬VM eq [] refl (β (β-sbuiltin⋆ b _ p bt _ .eq)) U = +U·⋆2 ¬VM eq [] refl (β (β-builtin⋆ b _ p bt _ .eq)) U = ⊥-elim (¬VM (V-IΠ b p bt)) U·⋆2 ¬VM eq (E ·⋆ A / .eq) refl q U with U E refl q ... | refl ,, refl ,, refl = refl ,, refl ,, refl @@ -399,7 +403,7 @@ rlemma51! (M · N) with rlemma51! M p (cong (_· N) q) λ { [] refl (β (β-ƛ VN)) → ⊥-elim (¬VM (V-ƛ _)) - ; [] refl (β (β-sbuiltin b .M p bt .N vu)) → ⊥-elim (¬VM (V-I⇒ b p bt)) + ; [] refl (β (β-builtin b .M p bt .N vu)) → ⊥-elim (¬VM (V-I⇒ b p bt)) ; (E' l· N') refl r → let X ,, Y ,, Y' = U E' refl r in X ,, trans ( subst-l· E N X) (cong (_l· N) Y) ,, Y' ; (VM ·r E') refl r → ⊥-elim (¬VM VM) @@ -411,7 +415,7 @@ rlemma51! (M · N) with rlemma51! M p (cong (M ·_) q) λ { [] refl (β (β-ƛ VN)) → ⊥-elim (¬VN VN) - ; [] refl (β (β-sbuiltin b .M p bt .N VN)) → ⊥-elim (¬VN VN) + ; [] refl (β (β-builtin b .M p bt .N VN)) → ⊥-elim (¬VN VN) ; (E' l· N') refl q → ⊥-elim (valredex (lemVE _ _ VM) q) ; (VM' ·r E') refl q → let X ,, X'' ,, X''' = U E' refl q in X @@ -430,11 +434,11 @@ rlemma51! (.(ƛ M) · N) | done (V-ƛ M) | done VN = step ⊥-elim (valredex (lemVE _ E' (substEq Value Y (substƛVal X))) q) ; (VM' ·r E') refl q → ⊥-elim (valredex (lemVE _ E' VN) q)} rlemma51! (M · N) | done (V-I⇒ b {as' = []} p x) | done VN = step - (λ V → valred V (β-sbuiltin b M p x N VN)) + (λ V → valred V (β-builtin b M p x N VN)) [] - (β (β-sbuiltin b M p x N VN)) + (β (β-builtin b M p x N VN)) refl - λ { [] refl (β (β-sbuiltin b .M p bt .N vu)) → refl ,, refl ,, refl + λ { [] refl (β (β-builtin b .M p bt .N vu)) → refl ,, refl ,, refl ; (E' l· N') refl q → ⊥-elim (valredex (lemBE _ E' x) q) ; (VM' ·r E') refl q → ⊥-elim (valredex (lemVE _ E' VN) q)} rlemma51! (M · N) | done (V-I⇒ b {as' = a' ∷ as'} p x) | done VN = @@ -448,9 +452,9 @@ rlemma51! (M ·⋆ A / x) with rlemma51! M refl (U·⋆1 x) rlemma51! (M ·⋆ A / x) | done (V-IΠ b {as' = []} p q) = step - (λ V → valred V (β-sbuiltin⋆ b M p q A x)) + (λ V → valred V (β-builtin⋆ b M p q A x)) [] - (β (β-sbuiltin⋆ b M p q A x)) + (β (β-builtin⋆ b M p q A x)) refl λ E p' q' → U·⋆3 x E (V-IΠ b _ q) p' q' rlemma51! (M ·⋆ A / x) | done (V-IΠ b {as' = x₁ ∷ as'} p q) = diff --git a/plutus-metatheory/src/Algorithmic/ReductionEC/Progress.lagda.md b/plutus-metatheory/src/Algorithmic/ReductionEC/Progress.lagda.md index 063a7cf170e..a1a6f5af9f8 100644 --- a/plutus-metatheory/src/Algorithmic/ReductionEC/Progress.lagda.md +++ b/plutus-metatheory/src/Algorithmic/ReductionEC/Progress.lagda.md @@ -4,6 +4,7 @@ module Algorithmic.ReductionEC.Progress where ## Imports ``` +open import Data.Nat using (zero;suc) open import Data.List as List using (List; _∷_; []) open import Relation.Binary.PropositionalEquality using (_≡_;refl) @@ -57,20 +58,19 @@ progress (M · M') with progress M ... | error E-error = step (ruleErr (VM ·r []) refl) progress (.(ƛ M) · M') | done (V-ƛ M) | done VM' = step (ruleEC [] (β-ƛ VM') refl refl) -progress (M · M') | done (V-I⇒ b {as' = []} p q) | done VM' = - step (ruleEC [] (β-sbuiltin b M p q M' VM') refl refl) -progress (M · M') | done (V-I⇒ b {as' = a ∷ as'} p q) | done VM' = - done (V-I b (bubble p) (step p q VM')) +progress (M · M') | done (V-I⇒ b {am = 0} q) | done VM' = + step (ruleEC [] (β-builtin b M q M' VM') refl refl) +progress (M · M') | done (V-I⇒ b {am = suc _} q) | done VM' = + done (V-I b (step q VM')) progress (Λ M) = done (V-Λ M) progress (M ·⋆ A / refl) with progress M ... | error E-error = step (ruleErr ([] ·⋆ A / refl) refl) ... | step (ruleEC E p refl refl) = step (ruleEC (E ·⋆ A / refl) p refl refl) ... | step (ruleErr E refl) = step (ruleErr (E ·⋆ A / refl) refl) ... | done (V-Λ M') = step (ruleEC [] (β-Λ refl) refl refl) -progress (M ·⋆ A / r) | done (V-IΠ b {as' = []} p q) = - step (ruleEC [] (β-sbuiltin⋆ b M p q A refl) refl refl) -progress (M ·⋆ A / refl) | done (V-IΠ b {as' = a ∷ as'} p q) = - done (V-I b (bubble p) (step⋆ p q refl)) +progress (M ·⋆ A / refl) | done (V-IΠ b {tm = 0} q) = done (V-I b (step⋆ q refl refl)) +progress (M ·⋆ A / refl) | done (V-IΠ b {tm = suc _} q) = + done (V-I b (step⋆ q refl refl)) progress (wrap A B M) with progress M ... | done V = done (V-wrap V) ... | step (ruleEC E p refl refl) = step (ruleEC (wrap E) p refl refl) @@ -82,7 +82,7 @@ progress (unwrap M refl) with progress M ... | done (V-wrap V) = step (ruleEC [] (β-wrap V refl) refl refl) ... | error E-error = step (ruleErr (unwrap [] / refl) refl) progress (con c) = done (V-con c) -progress (builtin b / refl) = done (ival b) +progress (builtin b / refl ) = done (ival b) progress (error A) = error E-error {- These definitions seems unused @@ -107,7 +107,7 @@ lemma51 (M · M') with lemma51 M lemma51 (.(ƛ M) · M') | inj₁ (V-ƛ M) | inj₁ VM' = inj₂ (_ ,, [] ,, _ ,, inj₁ (_ ,, β-ƛ VM') ,, refl) lemma51 (M · M') | inj₁ (V-I⇒ b {as' = []} p x) | inj₁ VM' = - inj₂ (_ ,, [] ,, _ ,, inj₁ (_ ,, β-sbuiltin b M p x M' VM') ,, refl) + inj₂ (_ ,, [] ,, _ ,, inj₁ (_ ,, β-builtin b M p x M' VM') ,, refl) lemma51 (M · M') | inj₁ (V-I⇒ b {as' = a ∷ as'} p x) | inj₁ VM' = inj₁ (V-I b (bubble p) (step p x VM')) lemma51 (Λ M) = inj₁ (V-Λ M) @@ -117,7 +117,7 @@ lemma51 (M ·⋆ A / refl) with lemma51 M ... | inj₂ (B ,, E ,, L ,, p ,, q) = inj₂ (B ,, E ·⋆ A / refl ,, L ,, p ,, cong (_·⋆ A / refl) q) lemma51 (M ·⋆ A / refl) | inj₁ (V-IΠ b {as' = []} p x) = - inj₂ (_ ,, [] ,, _ ,, inj₁ (_ ,, β-sbuiltin⋆ b M p x A refl) ,, refl) + inj₂ (_ ,, [] ,, _ ,, inj₁ (_ ,, β-builtin⋆ b M p x A refl) ,, refl) lemma51 (M ·⋆ A / refl) | inj₁ (V-IΠ b {as' = a ∷ as} p x) = inj₁ (V-I b (bubble p) (step⋆ p x refl)) lemma51 (wrap A B M) with lemma51 M @@ -140,3 +140,4 @@ progress' M with lemma51 M ... | inj₂ (B ,, E ,, L ,, inj₂ E-error ,, refl) = step (ruleErr E refl) -} + \ No newline at end of file diff --git a/plutus-metatheory/src/Algorithmic/RenamingSubstitution.lagda b/plutus-metatheory/src/Algorithmic/RenamingSubstitution.lagda index 6092c596384..6d8db8d9651 100644 --- a/plutus-metatheory/src/Algorithmic/RenamingSubstitution.lagda +++ b/plutus-metatheory/src/Algorithmic/RenamingSubstitution.lagda @@ -16,7 +16,8 @@ open _⊢Nf⋆_ open _⊢Ne⋆_ open import Type.BetaNBE.RenamingSubstitution -open import Algorithmic using (Ctx;_∋_;conv∋;_⊢_;conv⊢;btype-ren;btype-sub) +open import Algorithmic using (Ctx;_∋_;conv∋;_⊢_;conv⊢) +open import Algorithmic.Signature using (btype-ren;btype-sub) open Ctx open _∋_ open _⊢_ diff --git a/plutus-metatheory/src/Algorithmic/Signature.lagda.md b/plutus-metatheory/src/Algorithmic/Signature.lagda.md new file mode 100644 index 00000000000..9d1f84b0232 --- /dev/null +++ b/plutus-metatheory/src/Algorithmic/Signature.lagda.md @@ -0,0 +1,134 @@ + +``` +module Algorithmic.Signature where +``` + +## Imports + +``` +open import Data.Nat using (suc) + +open import Relation.Binary.PropositionalEquality using (_≡_;refl;cong;sym;trans) +open Relation.Binary.PropositionalEquality.≡-Reasoning + +open import Function using (_∘_) + +open import Utils using (*;_∔_≣_) +open import Type using (Ctx⋆;∅;_,⋆_;_⊢⋆_;Φ) +open _⊢⋆_ + +open import Type.BetaNormal using (_⊢Nf⋆_;_⊢Ne⋆_;renNf;embNf) +open _⊢Nf⋆_ +open _⊢Ne⋆_ + +import Type.RenamingSubstitution as ⋆ +open import Type.BetaNBE.Completeness using (reifyCR;idext;exte-lem) +open import Type.BetaNBE.RenamingSubstitution + using (subNf;SubNf;renNf-subNf;subNf-cong;subNf-comp;subNf-cons;extsNf;subNf-lemma) + renaming (_[_]Nf to _[_]) +open import Type.BetaNBE.Stability using (stability) +open import Builtin using (Builtin;signature) +open import Builtin.Signature using (Sig;sig;nat2Ctx⋆;fin2∈⋆) +open import Type.BetaNBE using (nf;reify;eval;idEnv;exte) +open Builtin.Signature.FromSig Ctx⋆ (_⊢Nf⋆ *) nat2Ctx⋆ (λ x → ne (` (fin2∈⋆ x))) con _⇒_ Π + using (sig2type;SigTy;sigTy2type) +open SigTy + + +``` + +``` +btype' : Builtin → Φ ⊢Nf⋆ * +btype' b = subNf (λ()) (sig2type (signature b)) + +btype-∅ : ∀ {A : ∅ ⊢Nf⋆ *} → A ≡ subNf {∅} {∅} (λ()) {*} A +btype-∅ {A} = begin + A + ≡⟨ sym (stability A) ⟩ + nf (embNf A) + ≡⟨ cong nf (sym (⋆.sub-∅ (embNf A) (embNf ∘ λ()))) ⟩ + nf (⋆.sub (embNf ∘ λ()) (embNf A)) + ≡⟨ refl ⟩ + subNf (λ ()) A + ∎ + +-- A version of btype' where btype {∅} b = sig2type (signature b) holds definitionally +btype : Builtin → Φ ⊢Nf⋆ * +btype {∅} b = sig2type (signature b) +btype {Φ ,⋆ x} b = btype' b + +-- Both versions are the same +btype-btype' : ∀ {Φ} b → btype {Φ} b ≡ btype' {Φ} b +btype-btype' {∅} b = btype-∅ +btype-btype' {Φ ,⋆ x} b = refl + +btype'-ren : ∀{Φ Ψ} b (ρ : ⋆.Ren Φ Ψ) → btype' b ≡ renNf ρ (btype' b) +btype'-ren b ρ = begin + btype' b + ≡⟨ refl ⟩ + subNf (λ()) (sig2type (signature b)) + ≡⟨ subNf-cong {f = λ()} {renNf ρ ∘ λ ()} (λ ()) (sig2type (signature b)) ⟩ + subNf (renNf ρ ∘ λ ()) (sig2type (signature b)) + ≡⟨ renNf-subNf (λ()) ρ (sig2type (signature b)) ⟩ + renNf ρ (btype' b) + ∎ + +btype-ren : ∀{Φ Ψ} b (ρ : ⋆.Ren Φ Ψ) → btype b ≡ renNf ρ (btype b) +btype-ren b ρ = trans (btype-btype' b) (trans (btype'-ren b ρ) (cong (renNf ρ) (sym (btype-btype' b)))) + +btype'-sub : ∀{Φ Ψ} b (ρ : SubNf Φ Ψ) → btype' b ≡ subNf ρ (btype' b) +btype'-sub b ρ = begin + btype' b + ≡⟨ refl ⟩ + subNf (λ()) (sig2type (signature b)) + ≡⟨ subNf-cong {f = λ()} {subNf ρ ∘ λ ()} (λ ()) (sig2type (signature b)) ⟩ + subNf (subNf ρ ∘ (λ ())) (sig2type (signature b)) + ≡⟨ subNf-comp (λ()) ρ (sig2type (signature b)) ⟩ + subNf ρ (subNf (λ()) (sig2type (signature b))) + ≡⟨ refl ⟩ + subNf ρ (btype' b) + ∎ + +btype-sub : ∀{Φ Ψ} b (ρ : SubNf Φ Ψ) → btype b ≡ subNf ρ (btype b) +btype-sub b ρ = trans ((btype-btype' b)) (trans (btype'-sub b ρ) (cong (subNf ρ) (sym (btype-btype' b)))) +``` + +## Substitution in Signature types + +``` +subNf-Π : ∀{Φ Ψ J}(ρ : SubNf Φ Ψ)(B : Φ ,⋆ J ⊢Nf⋆ *) → subNf ρ (Π B) ≡ Π (subNf (extsNf ρ) B) +subNf-Π {Φ}{Ψ}{J} ρ B = begin + subNf ρ (Π B) + ≡⟨ refl ⟩ + Π (reify (eval (⋆.sub (⋆.exts (embNf ∘ ρ)) (embNf B)) (exte (idEnv _)))) + ≡⟨ cong nf (cong Π (subNf-lemma ρ (embNf B)) ) ⟩ + Π (reify (eval (⋆.sub (embNf ∘ extsNf ρ) (embNf B)) (exte (idEnv _)))) + ≡⟨ cong Π (reifyCR (idext exte-lem ((⋆.sub (embNf ∘ extsNf ρ) (embNf B))))) ⟩ + Π (reify (eval (⋆.sub (embNf ∘ extsNf ρ) (embNf B)) (idEnv _))) + ≡⟨ refl ⟩ -- nf def + Π (nf (⋆.sub (embNf ∘ extsNf ρ) (embNf B))) + ≡⟨ refl ⟩ + Π (subNf (extsNf ρ) B) + ∎ + +subSigTy : ∀ {n m} + → (σ : SubNf (nat2Ctx⋆ n) (nat2Ctx⋆ m)) + → ∀{tn tm tt} {pt : tn ∔ tm ≣ tt} + → ∀{am an at} {pa : an ∔ am ≣ at} + → {A : nat2Ctx⋆ n ⊢Nf⋆ *} → SigTy pt pa A + ------------------------- + → SigTy pt pa (subNf σ A) +subSigTy σ (bresult _) = bresult _ +subSigTy σ (A B⇒ bt) = (subNf σ A) B⇒ (subSigTy σ bt) +subSigTy σ (sucΠ bt) rewrite (subNf-Π σ (sigTy2type bt)) + = sucΠ (subSigTy (extsNf σ) bt) + +_[_]SigTy : ∀{n} + → ∀{tn tm tt} {pt : tn ∔ tm ≣ tt} + → ∀{am an at} {pa : an ∔ am ≣ at} + → {B : (nat2Ctx⋆ (suc n)) ⊢Nf⋆ *} + → SigTy pt pa B + → (A : (nat2Ctx⋆ n) ⊢Nf⋆ *) + → SigTy pt pa (B [ A ]) +_[_]SigTy bt A = subSigTy (subNf-cons (ne ∘ `) A) bt +``` \ No newline at end of file diff --git a/plutus-metatheory/src/Algorithmic/Soundness.lagda b/plutus-metatheory/src/Algorithmic/Soundness.lagda index d614c352fbd..832faab0bca 100644 --- a/plutus-metatheory/src/Algorithmic/Soundness.lagda +++ b/plutus-metatheory/src/Algorithmic/Soundness.lagda @@ -20,6 +20,7 @@ open _≡β_ import Declarative as Dec import Algorithmic as Alg +import Algorithmic.Signature as Alg open import Type.BetaNormal using (_⊢Nf⋆_;_⊢Ne⋆_;embNf;ren-embNf;weakenNf) open _⊢Nf⋆_ open _⊢Ne⋆_ diff --git a/plutus-metatheory/src/Builtin.lagda.md b/plutus-metatheory/src/Builtin.lagda.md index 00d6b0d6fd6..a7c2ca1de83 100644 --- a/plutus-metatheory/src/Builtin.lagda.md +++ b/plutus-metatheory/src/Builtin.lagda.md @@ -14,7 +14,8 @@ module Builtin where ``` open import Data.Nat using (ℕ;suc) open import Data.Fin using (Fin) renaming (zero to Z; suc to S) -open import Data.List.NonEmpty using (List⁺;_∷⁺_;[_]) +open import Data.List.NonEmpty using (List⁺;_∷⁺_;[_];reverse) +open import Data.Product using (Σ;proj₁) open import Data.Bool using (Bool) open import Agda.Builtin.Int using (Int) @@ -136,20 +137,35 @@ This is defined in its own module so that these definitions are not exported. b : ∀{n} → suc (suc n) ⊢♯ b = ` (S Z) + ``` + + ###Operators for constructing signatures + + The following operators are used to express signatures in a familiar way, + but ultimately, they construct a Sig + + An expression + n [ t₁ , t₂ , t₃ ]⟶ tᵣ + + is actually parsed as + (((n [ t₁) , t₂) , t₃) ]⟶ tᵣ + + and constructs a signature + + sig n (t₃ ∷ t₂ ∷ t₁) tᵣ - -- operators for constructing signatures - - _]⟶_ : ∀{n} → n ⊢♯ → n ⊢♯ → Args n × n ⊢♯ - _]⟶_ x y = [ x ] ,, y - - infix 10 _[_ - _[_ : (n : ℕ) → Args n × n ⊢♯ → Sig - _[_ n (as ,, r) = sig n as r + ``` + infix 12 _[_ + _[_ : (n : ℕ) → n ⊢♯ → Σ ℕ (λ n → Args n) + _[_ n x = n ,, [ x ] - infixr 11 _,_ + infixl 10 _,_ + _,_ : (p : Σ ℕ (λ n → Args n)) → proj₁ p ⊢♯ → Σ ℕ (λ n → Args n) + _,_ (n ,, args) arg = n ,, arg ∷⁺ args - _,_ : ∀{n} → n ⊢♯ → Args n × n ⊢♯ → Args n × n ⊢♯ - _,_ x (as ,, r) = x ∷⁺ as ,, r + infix 8 _]⟶_ + _]⟶_ : (p : Σ ℕ (λ n → Args n)) → proj₁ p ⊢♯ → Sig + _]⟶_ (n ,, as) res = sig n as res ``` The signature of each builtin diff --git a/plutus-metatheory/src/Builtin/Signature.lagda.md b/plutus-metatheory/src/Builtin/Signature.lagda.md index c845bf99989..1284708258f 100644 --- a/plutus-metatheory/src/Builtin/Signature.lagda.md +++ b/plutus-metatheory/src/Builtin/Signature.lagda.md @@ -17,11 +17,15 @@ except for the minimal rule of guaranteeing well-formedness. module Builtin.Signature where open import Data.Nat using (ℕ;zero;suc) -open import Data.Fin renaming (zero to Z; suc to S) -open import Data.List.NonEmpty using (List⁺;foldr) - -open import Utils using (*) -open import Type using (Ctx⋆;∅;_,⋆_;_⊢⋆_;_∋⋆_;Z;S;Φ) +open import Data.Nat.Properties using (+-identityʳ) +open import Data.Fin using (Fin) renaming (zero to Z; suc to S) +open import Data.List using (List;[];_∷_;length) +open import Data.List.NonEmpty using (List⁺;foldr;_∷_;toList;reverse) renaming (length to length⁺) +open import Data.Product using (Σ;proj₁;proj₂) renaming (_,_ to _,,_) +open import Relation.Binary.PropositionalEquality using (_≡_;refl;sym;cong;trans;subst) + +open import Utils using (*;_∔_≣_;start;bubble;alldone;unique∔) +open import Type using (Ctx⋆;_,⋆_;_⊢⋆_;_∋⋆_;Z;S;Φ) ``` ## Built-in compatible types @@ -81,6 +85,10 @@ record Sig : Set where -- type of result result : fv♯ ⊢♯ +open Sig + +args♯ : Sig → ℕ +args♯ σ = length⁺ (args σ) ``` ## Obtaining concrete types from signatures @@ -102,6 +110,8 @@ The following parameters should be instantiated: import Builtin.Constant.Type as T2 open T2.TyCon + + module FromSig (Ctx : Set) (Ty : Ctx → Set) (nat2Ctx : ℕ → Ctx) @@ -110,7 +120,7 @@ module FromSig (Ctx : Set) (_⇒_ : ∀{n} → Ty (nat2Ctx n) → Ty (nat2Ctx n) → Ty (nat2Ctx n)) (Π : ∀{n} → Ty (nat2Ctx (suc n)) → Ty (nat2Ctx n)) where - + -- convert a built-in-compatible type into a Ty type ♯2* : ∀{n} → n ⊢♯ → Ty (nat2Ctx n) ♯2* (` x) = fin2Ty x @@ -123,37 +133,138 @@ module FromSig (Ctx : Set) ♯2* (con (pair x y)) = mkTyCon (T2.pair (♯2* x) (♯2* y)) ♯2* (con pdata) = mkTyCon T2.pdata - {- `sig2type-aux` takes a list of arguments and a result type, and produces + -- The empty context + ∅ : Ctx + ∅ = nat2Ctx 0 +``` + + `sig2type⇒` takes a list of arguments and a result type, and produces a function that takes all arguments and returns the result type. - sig2type-aux [ b₁ , b₂ , ... ,bₙ ] tᵣ = t₁ ⇒ t₂ ⇒ ... ⇒ tₙ ⇒ tᵣ - where tᵢ = ♯2* bᵢ - -} - sig2type-aux : ∀{n} - → Args n + sig2type⇒ [ b₁ , b₂ , ... ,bₙ ] tᵣ = tₙ ⇒ ... ⇒ t₂ ⇒ t₁ ⇒ tᵣ + where tᵢ = ♯2* bᵢ + +``` + sig2type⇒ : ∀{n} + → List (n ⊢♯) → Ty (nat2Ctx n) → Ty (nat2Ctx n) - sig2type-aux xs = foldr (λ A xs res → (♯2* A) ⇒ (xs res)) (λ A res → ♯2* A ⇒ res) xs + sig2type⇒ [] r = r + sig2type⇒ (a ∷ as) r = sig2type⇒ as (♯2* a ⇒ r) + --foldr (λ A xs res → (♯2* A) ⇒ (xs res)) (λ A res → ♯2* A ⇒ res) xs +``` - -- take a type and close its type variables using Π - sig2type-aux2 : ∀{n} → Ty (nat2Ctx n) → Ty (nat2Ctx 0) - sig2type-aux2 {zero} t = t - sig2type-aux2 {suc n} t = sig2type-aux2 {n} (Π t) + `sig2typeΠ` adds as many Π as needed to close the type. - -- The main conversion function - sig2type : Sig → Ty (nat2Ctx 0) - sig2type (sig _ as res) = sig2type-aux2 (sig2type-aux as (♯2* res)) ``` + sig2typeΠ : ∀{n} → Ty (nat2Ctx n) → Ty (nat2Ctx 0) + sig2typeΠ {zero} t = t + sig2typeΠ {suc n} t = sig2typeΠ {n} (Π t) +``` + + The main conversion function from a signature into a concrete type + +``` + sig2type : Sig → Ty ∅ + sig2type (sig _ as res) = sig2typeΠ (sig2type⇒ (toList as) (♯2* res)) +``` + +### Types originating from a Signature + +The types produced by a signature have a particular form: possibly +some Π applications and then at least one function argument. + +We define a predicate for concrete types of that shape as a datatype +indexed by the concrete types + +``` + -- an : number of arguments to be added to the type + -- am : number of arguments expected + -- at : total number of arguments + -- tm : number of Π applied + -- tn : number of Π yet to be applied + -- tt: number of Π in the signature (fv♯) + data SigTy : ∀{tn tm tt} → tn ∔ tm ≣ tt + → ∀{an am at} → an ∔ am ≣ at + → ∀{n} → Ty (nat2Ctx n) → Set where + bresult : ∀{tt} → {pt : tt ∔ 0 ≣ tt} + → ∀{at} → {pa : at ∔ 0 ≣ at} + → ∀{n} (A : Ty (nat2Ctx n)) + → SigTy pt pa A + _B⇒_ : ∀{tn tt} → {pt : tn ∔ 0 ≣ tt } -- all Π yet to be applied + → ∀{an am at} → {pa : an ∔ suc am ≣ at} -- there is one more argument to add + → ∀{n} → (A : Ty (nat2Ctx n)) + → {B : Ty (nat2Ctx n)} + → SigTy pt (bubble pa) B + → SigTy pt pa (A ⇒ B) + sucΠ : ∀{tn tm tt} → {pt : tn ∔ suc tm ≣ tt} + → ∀{am an at} → {pa : an ∔ am ≣ at} + → ∀{n}{A : Ty (nat2Ctx (suc n))} + → SigTy (bubble pt) pa A + → SigTy pt pa (Π A) + +``` + + A `SigTy (0 ∔ tn ≣ tn) at A` is a type that expects the total number of + type arguments `tn` and the total number of term arguments `at`. + +## Conversion from a Signature to a SigType + +``` + sig2SigTy⇒ : ∀{tt : ℕ} → {pt : tt ∔ 0 ≣ tt} + → (as : List (tt ⊢♯)) + → ∀ {am at}(pa : length as ∔ am ≣ at) + → {A : Ty (nat2Ctx tt)} → (σA : SigTy pt pa A) + → SigTy pt (start at) (sig2type⇒ as A) + sig2SigTy⇒ [] (start _) bty = bty + sig2SigTy⇒ (a ∷ as) (bubble pa) bty = sig2SigTy⇒ as pa (♯2* a B⇒ bty) + + + sig2SigTyΠ : ∀{tn tm tt : ℕ} → (pt : tn ∔ tm ≣ tt) + → ∀ {at}{pa : 0 ∔ at ≣ at} + → ∀{A : Ty (nat2Ctx tn)} → SigTy pt pa A + → SigTy (start tt) pa (sig2typeΠ A) + sig2SigTyΠ (start _) bty = bty + sig2SigTyΠ (bubble pt) bty = sig2SigTyΠ pt (sucΠ bty) + + -- From a signature obtain a signature type + sig2SigTy : (σ : Sig) → SigTy (start (fv♯ σ)) (start (args♯ σ)) (sig2type σ) + sig2SigTy (sig n as r) = + sig2SigTyΠ (alldone n) (sig2SigTy⇒ (toList as) (alldone (length⁺ as)) (bresult (♯2* r))) + + -- extract the concrete type from a signature type. + sigTy2type : ∀{n tm tn tt an am at}{A : Ty (nat2Ctx n)} → {pt : tn ∔ tm ≣ tt} → {pa : an ∔ am ≣ at} → SigTy pt pa A → Ty (nat2Ctx n) + sigTy2type {A = A} _ = A + + saturatedSigTy : ∀ (σ : Sig) → (A : Ty ∅) → Set + saturatedSigTy σ A = SigTy (alldone (fv♯ σ)) (alldone (args♯ σ)) A +``` + +## Conversion of Signature types + +``` + convSigTy : + ∀{tn tm tt} → {pt pt' : tn ∔ tm ≣ tt} + → ∀{an am at} → {pa pa' : an ∔ am ≣ at} + → ∀{n}{A A' : Ty (nat2Ctx n)} + → A ≡ A' + → 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 +-- -} +``` + +## Auxiliary functions The parameter `Ctx` above is usually `Ctx⋆`. In this case, the parameters - `nat2Ctx` and `fin2Ty` con be instantiated with the help of the following + `nat2Ctx` and `fin2Ty` can be instantiated with the help of the following auxiliary functions. ``` nat2Ctx⋆ : ℕ → Ctx⋆ -nat2Ctx⋆ zero = ∅ +nat2Ctx⋆ zero = Ctx⋆.∅ nat2Ctx⋆ (suc n) = nat2Ctx⋆ n ,⋆ * fin2∈⋆ : ∀{n} → Fin n → (nat2Ctx⋆ n) ∋⋆ * fin2∈⋆ Z = Z fin2∈⋆ (S x) = S (fin2∈⋆ x) -``` \ No newline at end of file +``` \ No newline at end of file diff --git a/plutus-metatheory/src/Check.lagda.md b/plutus-metatheory/src/Check.lagda.md index a493ff29416..b1f469f253a 100644 --- a/plutus-metatheory/src/Check.lagda.md +++ b/plutus-metatheory/src/Check.lagda.md @@ -37,7 +37,8 @@ open _≡β_ open import Type.BetaNBE using (nf) open import Type.BetaNBE.Soundness using (soundness) -open import Algorithmic using (_⊢_;Ctx;_∋_;btype) +open import Algorithmic using (_⊢_;Ctx;_∋_) +open import Algorithmic.Signature using (btype) open _⊢_ open Ctx open _∋_ diff --git a/plutus-metatheory/src/Type/BetaNBE/Completeness.lagda b/plutus-metatheory/src/Type/BetaNBE/Completeness.lagda index e84364ad58f..84f8d2ab317 100644 --- a/plutus-metatheory/src/Type/BetaNBE/Completeness.lagda +++ b/plutus-metatheory/src/Type/BetaNBE/Completeness.lagda @@ -11,7 +11,7 @@ open import Relation.Binary.PropositionalEquality using (_≡_;refl;sym;trans;cong;cong₂) open import Utils using (*;_⇒_;J;K) -open import Type using (Ctx⋆;Φ;Ψ;Θ;_⊢⋆_;_∋⋆_;S;Z) +open import Type using (Ctx⋆;_,⋆_;Φ;Ψ;Θ;_⊢⋆_;_∋⋆_;S;Z) open _⊢⋆_ open import Type.Equality using (_≡β_;_≡βTyCon_) open _≡β_ @@ -20,7 +20,7 @@ open import Type.RenamingSubstitution using (Ren;ren;renTyCon;ext;Sub;sub;subTyC open import Type.BetaNormal using (_⊢Nf⋆_;_⊢Ne⋆_;renNf;renNe;renNfTyCon) open _⊢Nf⋆_ open _⊢Ne⋆_ -open import Type.BetaNBE using (Val;renVal;reflect;reify;Env;_,,⋆_;_·V_;eval;evalTyCon;idEnv;nf) +open import Type.BetaNBE using (Val;renVal;reflect;reify;Env;_,,⋆_;_·V_;eval;evalTyCon;idEnv;nf;exte) open import Type.BetaNormal.Equality using (renNe-cong;renNf-id;renNe-id;renNf-comp;renNe-comp) import Builtin.Constant.Type Ctx⋆ (_⊢⋆ *) as Syn import Builtin.Constant.Type Ctx⋆ (_⊢Nf⋆ *) as Nf @@ -569,7 +569,17 @@ idCR : (x : Φ ∋⋆ K) → CR K (idEnv Φ x) (idEnv Φ x) idCR x = reflectCR refl \end{code} +Finally, the completeness theorem. + \begin{code} completeness : {s t : Φ ⊢⋆ K} → s ≡β t → nf s ≡ nf t completeness p = reifyCR (fund idCR p) \end{code} + +A small lemma relating environments. + +\begin{code} +exte-lem : ∀{Ψ J} → EnvCR (exte (idEnv Ψ)) (idEnv (Ψ ,⋆ J)) +exte-lem Z = idCR Z +exte-lem (S x) = renVal-reflect S (` x) +\end{code} diff --git a/plutus-metatheory/src/Type/RenamingSubstitution.lagda.md b/plutus-metatheory/src/Type/RenamingSubstitution.lagda.md index 07da86ddd5e..56d86e907a4 100644 --- a/plutus-metatheory/src/Type/RenamingSubstitution.lagda.md +++ b/plutus-metatheory/src/Type/RenamingSubstitution.lagda.md @@ -16,7 +16,7 @@ open import Relation.Binary.PropositionalEquality renaming (subst to substEq) open import Utils using (*;J;K) -open import Type using (Ctx⋆;_,⋆_;Φ;Ψ;_⊢⋆_;_∋⋆_;S;Z) +open import Type using (Ctx⋆;_,⋆_;∅;Φ;Ψ;_⊢⋆_;_∋⋆_;S;Z) open _⊢⋆_ open import Builtin.Constant.Type Ctx⋆ (_⊢⋆ *) using (TyCon) open TyCon @@ -345,6 +345,8 @@ sub-id : (A : Φ ⊢⋆ J) ------------ → sub ` A ≡ A + + subTyCon-id : (c : TyCon Φ) ------------ → subTyCon ` c ≡ c @@ -558,3 +560,9 @@ sub-Π : ∀(A : Φ ⊢⋆ K)(B : Φ ,⋆ K ⊢⋆ J)(σ : Sub Φ Ψ) sub-Π A B σ = trans (sym (sub-comp B)) (trans (sub-cong (sub-sub-cons σ A) B) (sub-comp B)) ``` + +Substituting in the empty type context is the same as doing nothing. +``` +sub-∅ : (A : ∅ ⊢⋆ J) → (x : Sub ∅ ∅) → sub x A ≡ A +sub-∅ A x = trans (sub-cong (λ ()) A) (sub-id A) +``` \ No newline at end of file diff --git a/plutus-metatheory/src/Untyped.lagda.md b/plutus-metatheory/src/Untyped.lagda.md index dd8fe136445..9eeb6b5c2f6 100644 --- a/plutus-metatheory/src/Untyped.lagda.md +++ b/plutus-metatheory/src/Untyped.lagda.md @@ -23,7 +23,6 @@ open import Builtin using (Builtin;equals) open Builtin.Builtin open import Raw using (decBuiltin) -open import Algorithmic using (arity;Term;Type) open import Agda.Builtin.String using (primStringFromList; primStringAppend; primStringEquality) open import Data.Nat using (ℕ;suc;zero) diff --git a/plutus-metatheory/src/Untyped/CEK.lagda.md b/plutus-metatheory/src/Untyped/CEK.lagda.md index ececd29c65e..a424f28e69d 100644 --- a/plutus-metatheory/src/Untyped/CEK.lagda.md +++ b/plutus-metatheory/src/Untyped/CEK.lagda.md @@ -7,6 +7,8 @@ module Untyped.CEK where ## Imports ``` +open import Data.Nat using (ℕ;zero;suc) +open import Data.Nat.Properties using (+-identityʳ) open import Function using (case_of_;_$_) open import Data.Integer using (_> as ∈ arity b +data BApp (b : Builtin) : + ∀{tn tm tt} → (pt : tn ∔ tm ≣ tt) + → ∀{an am at} → (pa : an ∔ am ≣ at) → Set data Value where V-ƛ : ∀{X} → Env X → Maybe X ⊢ → Value V-con : TermCon → Value V-delay : ∀{X} → Env X → X ⊢ → Value - V-I⇒ : ∀ b {as as'} - → (p : as <>> (Term ∷ as') ∈ arity b) - → BApp b p + V-I⇒ : ∀ b {tn} + → {pt : tn ∔ 0 ≣ fv♯ (signature b)} + → ∀{an am}{pa : an ∔ (suc am) ≣ args♯ (signature b)} + → BApp b pt pa → Value - V-IΠ : ∀ b {as as'} - → (p : as <>> (Type ∷ as') ∈ arity b) - → BApp b p + V-IΠ : ∀ b + → ∀{tn tm}{pt : tn ∔ (suc tm) ≣ fv♯ (signature b)} + → ∀{an am}{pa : an ∔ suc am ≣ args♯ (signature b)} + → BApp b pt pa → Value data BApp b where - base : BApp b (start (arity b)) - app : ∀{az as} - → (p : az <>> (Term ∷ as) ∈ arity b) - → BApp b p + base : BApp b (start (fv♯ (signature b))) (start (args♯ (signature b))) + app : ∀{tn} + {pt : tn ∔ 0 ≣ fv♯ (signature b)} + → ∀{an am}{pa : an ∔ suc am ≣ args♯ (signature b)} + → BApp b pt pa → Value - → BApp b (bubble p) - app⋆ : ∀{az as} - → (p : az <>> (Type ∷ as) ∈ arity b) - → BApp b p - → BApp b (bubble p) + → BApp b pt (bubble pa) + app⋆ : + ∀{tn tm} {pt : tn ∔ (suc tm) ≣ fv♯ (signature b)} + → ∀{an am}{pa : an ∔ (suc am) ≣ args♯ (signature b)} + → BApp b pt pa + → BApp b (bubble pt) pa env2sub : ∀{Γ} → Env Γ → Sub Γ ⊥ discharge : Value → ⊥ ⊢ -dischargeB : ∀{b}{az}{as}{p : az <>> as ∈ arity b} → BApp b p → ⊥ ⊢ + +dischargeB : ∀{b} + → ∀{tn tm} → {pt : tn ∔ tm ≣ fv♯ (signature b)} + → ∀{an am} → {pa : an ∔ am ≣ args♯ (signature b)} + → BApp b pt pa → ⊥ ⊢ discharge (V-ƛ ρ t) = ƛ (sub (lifts (env2sub ρ)) t) discharge (V-con c) = con c discharge (V-delay ρ t) = delay (sub (env2sub ρ) t) -discharge (V-I⇒ b p vs) = dischargeB vs -discharge (V-IΠ b p vs) = dischargeB vs +discharge (V-I⇒ b vs) = dischargeB vs +discharge (V-IΠ b vs) = dischargeB vs dischargeB {b = b} base = builtin b -dischargeB (app p vs v) = dischargeB vs · discharge v -dischargeB (app⋆ p vs) = force (dischargeB vs) +dischargeB (app vs v) = dischargeB vs · discharge v +dischargeB (app⋆ vs) = force (dischargeB vs) env2sub (ρ ∷ v) nothing = discharge v env2sub (ρ ∷ v) (just x) = env2sub ρ x @@ -98,121 +110,122 @@ lookup : ∀{Γ} → Env Γ → Γ → Value lookup (ρ ∷ v) nothing = v lookup (ρ ∷ v) (just x) = lookup ρ x +V-I : ∀ b + → ∀{tn tm} {pt : tn ∔ tm ≣ fv♯ (signature b)} + → ∀{an am} {pa : an ∔ suc am ≣ args♯ (signature b)} + → BApp b pt pa + → Value +V-I b {tm = zero} bt = V-I⇒ b bt +V-I b {tm = suc tm} bt = V-IΠ b bt -V-I : ∀ b {a as as'} - → (p : as <>> a ∷ as' ∈ arity b) - → BApp b p - → Value -V-I b {a = Term} p vs = V-I⇒ b p vs -V-I b {a = Type} p vs = V-IΠ b p vs - -BUILTIN : ∀ b → BApp b (saturated (arity b)) → Either RuntimeError Value +BUILTIN : ∀ b → BApp b (alldone (fv♯ (signature b))) (alldone (args♯ (signature b))) → Either RuntimeError Value BUILTIN addInteger = λ - { (app _ (app _ base (V-con (integer i))) (V-con (integer i'))) -> inj₂ (V-con (integer (i + i'))) ; _ -> inj₁ userError + { (app (app base (V-con (integer i))) (V-con (integer i'))) -> inj₂ (V-con (integer (i + i'))) + ; _ -> inj₁ userError } BUILTIN subtractInteger = λ - { (app _ (app _ base (V-con (integer i))) (V-con (integer i'))) -> inj₂ (V-con (integer (i - i'))) + { (app (app base (V-con (integer i))) (V-con (integer i'))) -> inj₂ (V-con (integer (i - i'))) ; _ -> inj₁ userError } BUILTIN multiplyInteger = λ - { (app _ (app _ base (V-con (integer i))) (V-con (integer i'))) -> inj₂ (V-con (integer (i ** i'))) + { (app (app base (V-con (integer i))) (V-con (integer i'))) -> inj₂ (V-con (integer (i ** i'))) ; _ -> inj₁ userError } BUILTIN divideInteger = λ - { (app _ (app _ base (V-con (integer i))) (V-con (integer i'))) -> decIf + { (app (app base (V-con (integer i))) (V-con (integer i'))) -> decIf (i' ≟ ℤ.pos 0) (inj₁ userError) (inj₂ (V-con (integer (div i i')))) ; _ -> inj₁ userError } BUILTIN quotientInteger = λ - { (app _ (app _ base (V-con (integer i))) (V-con (integer i'))) -> decIf + { (app (app base (V-con (integer i))) (V-con (integer i'))) -> decIf (i' ≟ ℤ.pos 0) (inj₁ userError) (inj₂ (V-con (integer (quot i i')))) ; _ -> inj₁ userError } BUILTIN remainderInteger = λ - { (app _ (app _ base (V-con (integer i))) (V-con (integer i'))) -> decIf + { (app (app base (V-con (integer i))) (V-con (integer i'))) -> decIf (i' ≟ ℤ.pos 0) (inj₁ userError) (inj₂ (V-con (integer (rem i i')))) ; _ -> inj₁ userError } BUILTIN modInteger = λ - { (app _ (app _ base (V-con (integer i))) (V-con (integer i'))) -> decIf + { (app (app base (V-con (integer i))) (V-con (integer i'))) -> decIf (i' ≟ ℤ.pos 0) (inj₁ userError) (inj₂ (V-con (integer (mod i i')))) ; _ -> inj₁ userError } BUILTIN lessThanInteger = λ - { (app _ (app _ base (V-con (integer i))) (V-con (integer i'))) -> decIf (i decIf (i inj₁ userError } BUILTIN lessThanEqualsInteger = λ - { (app _ (app _ base (V-con (integer i))) (V-con (integer i'))) -> decIf (i ≤? i') (inj₂ (V-con (bool true))) (inj₂ (V-con (bool false))) + { (app (app base (V-con (integer i))) (V-con (integer i'))) -> decIf (i ≤? i') (inj₂ (V-con (bool true))) (inj₂ (V-con (bool false))) ; _ -> inj₁ userError } BUILTIN equalsInteger = λ - { (app _ (app _ base (V-con (integer i))) (V-con (integer i'))) -> decIf (i ≟ i') (inj₂ (V-con (bool true))) (inj₂ (V-con (bool false))) + { (app (app base (V-con (integer i))) (V-con (integer i'))) -> decIf (i ≟ i') (inj₂ (V-con (bool true))) (inj₂ (V-con (bool false))) ; _ -> inj₁ userError } BUILTIN appendByteString = λ - { (app _ (app _ base (V-con (bytestring b))) (V-con (bytestring b'))) -> inj₂ (V-con (bytestring (concat b b'))) + { (app (app base (V-con (bytestring b))) (V-con (bytestring b'))) -> inj₂ (V-con (bytestring (concat b b'))) ; _ -> inj₁ userError } BUILTIN lessThanByteString = λ - { (app _ (app _ base (V-con (bytestring b))) (V-con (bytestring b'))) -> inj₂ (V-con (bool (B< b b'))) + { (app (app base (V-con (bytestring b))) (V-con (bytestring b'))) -> inj₂ (V-con (bool (B< b b'))) ; _ -> inj₁ userError } BUILTIN lessThanEqualsByteString = λ - { (app _ (app _ base (V-con (bytestring b))) (V-con (bytestring b'))) -> inj₂ (V-con (bool (B<= b b'))) + { (app (app base (V-con (bytestring b))) (V-con (bytestring b'))) -> inj₂ (V-con (bool (B<= b b'))) ; _ -> inj₁ userError } BUILTIN sha2-256 = λ - { (app _ base (V-con (bytestring b))) -> inj₂ (V-con + { (app base (V-con (bytestring b))) -> inj₂ (V-con (bytestring (SHA2-256 b))) ; _ -> inj₁ userError } BUILTIN sha3-256 = λ - { (app _ base (V-con (bytestring b))) -> + { (app base (V-con (bytestring b))) -> inj₂ (V-con (bytestring (SHA3-256 b))) ; _ -> inj₁ userError } BUILTIN blake2b-256 = λ - { (app _ base (V-con (bytestring b))) -> + { (app base (V-con (bytestring b))) -> inj₂ (V-con (bytestring (BLAKE2B-256 b))) ; _ -> inj₁ userError } BUILTIN verifyEd25519Signature = λ - { (app _ (app _ (app _ base (V-con (bytestring k))) (V-con (bytestring d))) (V-con (bytestring c))) -> case verifyEd25519Sig k d c of λ + { (app (app (app base (V-con (bytestring k))) (V-con (bytestring d))) (V-con (bytestring c))) -> case verifyEd25519Sig k d c of λ { (just b) -> inj₂ (V-con (bool b)) ; nothing -> inj₁ userError } ; _ -> inj₁ userError } BUILTIN verifyEcdsaSecp256k1Signature = λ - { (app _ (app _ (app _ base (V-con (bytestring k))) (V-con (bytestring d))) (V-con (bytestring c))) -> case verifyEcdsaSecp256k1Sig k d c of λ + { (app (app (app base (V-con (bytestring k))) (V-con (bytestring d))) (V-con (bytestring c))) -> case verifyEcdsaSecp256k1Sig k d c of λ { (just b) -> inj₂ (V-con (bool b)) ; nothing -> inj₁ userError } ; _ -> inj₁ userError } BUILTIN verifySchnorrSecp256k1Signature = λ - { (app _ (app _ (app _ base (V-con (bytestring k))) (V-con (bytestring d))) (V-con (bytestring c))) -> case verifySchnorrSecp256k1Sig k d c of λ + { (app (app (app base (V-con (bytestring k))) (V-con (bytestring d))) (V-con (bytestring c))) -> case verifySchnorrSecp256k1Sig k d c of λ { (just b) -> inj₂ (V-con (bool b)) ; nothing -> inj₁ userError } ; _ -> inj₁ userError } BUILTIN encodeUtf8 = λ - { (app _ base (V-con (string s))) -> + { (app base (V-con (string s))) -> inj₂ (V-con (bytestring (ENCODEUTF8 s))) ; _ -> inj₁ userError } BUILTIN decodeUtf8 = λ - { (app _ base (V-con (bytestring b))) -> + { (app base (V-con (bytestring b))) -> case DECODEUTF8 b of λ { (just s) -> inj₂ (V-con (string s)) ; nothing -> inj₁ userError @@ -220,43 +233,43 @@ BUILTIN decodeUtf8 = λ ; _ -> inj₁ userError } BUILTIN equalsByteString = λ - { (app _ (app _ base (V-con (bytestring b))) (V-con (bytestring b'))) -> inj₂ (V-con (bool (equals b b'))) + { (app (app base (V-con (bytestring b))) (V-con (bytestring b'))) -> inj₂ (V-con (bool (equals b b'))) ; _ -> inj₁ userError } BUILTIN ifThenElse = λ - { (app _ (app _ (app _ (app⋆ _ base) (V-con (bool b))) vt) vf) -> inj₂ $ if b then vt else vf + { (app (app (app (app⋆ base) (V-con (bool b))) vt) vf) -> inj₂ $ if b then vt else vf ; _ -> inj₁ userError } BUILTIN appendString = λ - { (app _ (app _ base (V-con (string s))) (V-con (string s'))) -> inj₂ (V-con (string (primStringAppend s s'))) + { (app (app base (V-con (string s))) (V-con (string s'))) -> inj₂ (V-con (string (primStringAppend s s'))) ; _ -> inj₁ userError } BUILTIN trace = λ - { (app _ (app _ (app⋆ _ base) (V-con (string s))) v) -> inj₂ (TRACE s v) + { (app (app (app⋆ base) (V-con (string s))) v) -> inj₂ (TRACE s v) ; _ -> inj₁ userError } BUILTIN iData = λ - { (app _ base (V-con (integer i))) -> inj₂ (V-con (pdata (iDATA i))) + { (app base (V-con (integer i))) -> inj₂ (V-con (pdata (iDATA i))) ; _ -> inj₁ userError } BUILTIN bData = λ - { (app _ base (V-con (bytestring b))) -> inj₂ (V-con (pdata (bDATA b))) + { (app base (V-con (bytestring b))) -> inj₂ (V-con (pdata (bDATA b))) ; _ -> inj₁ userError } BUILTIN consByteString = λ - { (app _ (app _ base (V-con (integer i))) (V-con (bytestring b))) -> inj₂ (V-con (bytestring (cons i b))) + { (app (app base (V-con (integer i))) (V-con (bytestring b))) -> inj₂ (V-con (bytestring (cons i b))) ; _ -> inj₁ userError } BUILTIN sliceByteString = λ - { (app _ (app _ (app _ base (V-con (integer st))) (V-con (integer n))) (V-con (bytestring b))) -> inj₂ (V-con (bytestring (slice st n b))) + { (app (app (app base (V-con (integer st))) (V-con (integer n))) (V-con (bytestring b))) -> inj₂ (V-con (bytestring (slice st n b))) ; _ -> inj₁ userError } BUILTIN lengthOfByteString = λ - { (app _ base (V-con (bytestring b))) -> inj₂ (V-con (integer (length b))) + { (app base (V-con (bytestring b))) -> inj₂ (V-con (integer (length b))) ; _ -> inj₁ userError } BUILTIN indexByteString = λ - { (app _ (app _ base (V-con (bytestring b))) (V-con (integer i))) -> + { (app (app base (V-con (bytestring b))) (V-con (integer i))) -> case Data.Integer.ℤ.pos 0 ≤? i of λ { (no _) -> inj₁ userError ; (yes _) -> case i inj₁ userError } BUILTIN equalsString = λ - { (app _ (app _ base (V-con (string s))) (V-con (string s'))) -> inj₂ (V-con (bool (primStringEquality s s'))) + { (app (app base (V-con (string s))) (V-con (string s'))) -> inj₂ (V-con (bool (primStringEquality s s'))) ; _ -> inj₁ userError } BUILTIN unIData = λ - { (app _ base (V-con (pdata (iDATA i)))) -> inj₂ (V-con (integer i)) + { (app base (V-con (pdata (iDATA i)))) -> inj₂ (V-con (integer i)) ; _ -> inj₁ userError } BUILTIN unBData = λ - { (app _ base (V-con (pdata (bDATA b)))) -> inj₂ (V-con (bytestring b)) + { (app base (V-con (pdata (bDATA b)))) -> inj₂ (V-con (bytestring b)) ; _ -> inj₁ userError } BUILTIN serialiseData = λ - { (app _ base (V-con (pdata d))) -> inj₂ (V-con (bytestring (serialiseDATA d))) + { (app base (V-con (pdata d))) -> inj₂ (V-con (bytestring (serialiseDATA d))) ; _ -> inj₁ userError } BUILTIN chooseUnit = λ - { (app _ (app _ (app⋆ _ base) (V-con unit)) v) -> inj₂ v + { (app (app (app⋆ base) (V-con unit)) v) -> inj₂ v ; _ -> inj₁ userError } BUILTIN fstPair = λ @@ -341,75 +354,19 @@ BUILTIN mkNilPairData = λ { _ -> inj₁ userError } -convBApp : (b : Builtin) → ∀{az}{as}(p p' : az <>> as ∈ arity b) - → BApp b p - → BApp b p' -convBApp b p p' q rewrite unique<>> p p' = q - -BUILTIN' : ∀ b {az}(p : az <>> [] ∈ arity b) - → BApp b p +BUILTIN' : ∀ b + → ∀{tn} → {pt : tn ∔ 0 ≣ fv♯ (signature b)} + → ∀{an} → {pa : an ∔ 0 ≣ args♯ (signature b)} + → BApp b pt pa → ⊥ ⊢ -BUILTIN' b {az = az} p q - with sym (trans (cong ([] <><_) (sym (<>>2<>>' _ _ _ p))) (lemma<>2 az [])) -... | refl with BUILTIN b (convBApp b p (saturated (arity b)) q) -... | inj₁ e = error +BUILTIN' b {pt = pt} {pa = pa} bt with trans (sym (+-identityʳ _)) (∔2+ pt) | trans (sym (+-identityʳ _)) (∔2+ pa) +... | refl | refl with unique∔ pt (alldone (fv♯ (signature b))) | unique∔ pa (alldone (args♯ (signature b))) +... | refl | refl with BUILTIN b bt +... | inj₁ _ = error ... | inj₂ V = discharge V ival : Builtin → Value -ival addInteger = V-I⇒ addInteger _ base -ival subtractInteger = V-I⇒ subtractInteger _ base -ival multiplyInteger = V-I⇒ multiplyInteger _ base -ival divideInteger = V-I⇒ divideInteger _ base -ival quotientInteger = V-I⇒ quotientInteger _ base -ival remainderInteger = V-I⇒ remainderInteger _ base -ival modInteger = V-I⇒ modInteger _ base -ival lessThanInteger = V-I⇒ lessThanInteger _ base -ival lessThanEqualsInteger = V-I⇒ lessThanEqualsInteger _ base -ival equalsInteger = V-I⇒ equalsInteger _ base -ival appendByteString = V-I⇒ appendByteString _ base -ival lessThanByteString = V-I⇒ lessThanByteString _ base -ival lessThanEqualsByteString = V-I⇒ lessThanEqualsByteString _ base -ival sha2-256 = V-I⇒ sha2-256 _ base -ival sha3-256 = V-I⇒ sha3-256 _ base -ival verifyEd25519Signature = V-I⇒ verifyEd25519Signature _ base -ival verifyEcdsaSecp256k1Signature = V-I⇒ verifyEcdsaSecp256k1Signature _ base -ival verifySchnorrSecp256k1Signature = V-I⇒ verifySchnorrSecp256k1Signature _ base -ival equalsByteString = V-I⇒ equalsByteString _ base -ival ifThenElse = V-IΠ ifThenElse _ base -ival appendString = V-I⇒ appendString _ base -ival trace = V-IΠ trace _ base -ival equalsString = V-I⇒ equalsString (start _) base -ival encodeUtf8 = V-I⇒ encodeUtf8 (start _) base -ival decodeUtf8 = V-I⇒ decodeUtf8 (start _) base -ival fstPair = V-IΠ fstPair (start _) base -ival sndPair = V-IΠ sndPair (start _) base -ival nullList = V-IΠ nullList (start _) base -ival headList = V-IΠ headList (start _) base -ival tailList = V-IΠ tailList (start _) base -ival chooseList = V-IΠ chooseList (start _) base -ival constrData = V-I⇒ constrData (start _) base -ival mapData = V-I⇒ mapData (start _) base -ival listData = V-I⇒ listData (start _) base -ival iData = V-I⇒ iData (start _) base -ival bData = V-I⇒ bData (start _) base -ival unConstrData = V-I⇒ unConstrData (start _) base -ival unMapData = V-I⇒ unMapData (start _) base -ival unListData = V-I⇒ unListData (start _) base -ival unIData = V-I⇒ unIData (start _) base -ival unBData = V-I⇒ unBData (start _) base -ival equalsData = V-I⇒ equalsData (start _) base -ival serialiseData = V-I⇒ serialiseData (start _) base -ival chooseData = V-IΠ chooseData (start _) base -ival chooseUnit = V-IΠ chooseUnit (start _) base -ival mkPairData = V-I⇒ mkPairData (start _) base -ival mkNilData = V-I⇒ mkNilData (start _) base -ival mkNilPairData = V-I⇒ mkNilPairData (start _) base -ival mkCons = V-IΠ mkCons (start _) base -ival consByteString = V-I⇒ consByteString (start _) base -ival sliceByteString = V-I⇒ sliceByteString (start _) base -ival lengthOfByteString = V-I⇒ lengthOfByteString (start _) base -ival indexByteString = V-I⇒ indexByteString (start _) base -ival blake2b-256 = V-I⇒ blake2b-256 (start _) base +ival b = V-I b base step : State → State step (s ; ρ ▻ ` x) = s ◅ lookup ρ x @@ -423,21 +380,18 @@ step (s ; ρ ▻ error) = ◆ step (ε ◅ v) = □ v step ((s , -· ρ u) ◅ v) = (s , (v ·-)) ; ρ ▻ u step ((s , (V-ƛ ρ t ·-)) ◅ v) = s ; ρ ∷ v ▻ t -step ((s , (V-I⇒ b {as' = []} p vs ·-)) ◅ v) = - s ; [] ▻ BUILTIN' b (bubble p) (app p vs v) -step ((s , (V-I⇒ b {as' = a ∷ as'} p vs ·-)) ◅ v) = - s ◅ V-I b (bubble p) (app p vs v) +step ((s , (V-I⇒ b {am = 0} bapp ·-)) ◅ v) = + s ; [] ▻ BUILTIN' b (app bapp v) +step ((s , (V-I⇒ b {am = suc _} bapp ·-)) ◅ v) = + s ◅ V-I b (app bapp v) step ((s , (V-con _ ·-)) ◅ v) = ◆ -- constant in function position step ((s , (V-delay _ _ ·-)) ◅ v) = ◆ -- delay in function position -step ((s , (V-IΠ b p vs ·-)) ◅ v) = ◆ -- delayed builtin in function position -step ((s , force-) ◅ V-IΠ b {as' = []} p vs) = - s ; [] ▻ BUILTIN' b (bubble p) (app⋆ p vs) -step ((s , force-) ◅ V-IΠ b {as' = a ∷ as'} p vs) = - s ◅ V-I b (bubble p) (app⋆ p vs) +step ((s , (V-IΠ b bapp ·-)) ◅ v) = ◆ -- delayed builtin in function position +step ((s , force-) ◅ V-IΠ b bapp) = s ◅ V-I b (app⋆ bapp) step ((s , force-) ◅ V-delay ρ t) = step (s ; ρ ▻ t) step ((s , force-) ◅ V-ƛ _ _) = ◆ -- lambda in delay position step ((s , force-) ◅ V-con _) = ◆ -- constant in delay position -step ((s , force-) ◅ V-I⇒ b p vs) = ◆ -- function in delay position +step ((s , force-) ◅ V-I⇒ b bapp) = ◆ -- function in delay position step (□ v) = □ v step ◆ = ◆ diff --git a/plutus-metatheory/src/Utils.lagda b/plutus-metatheory/src/Utils.lagda index c86dc45dd70..ec347915530 100644 --- a/plutus-metatheory/src/Utils.lagda +++ b/plutus-metatheory/src/Utils.lagda @@ -8,10 +8,10 @@ open import Data.Nat using (ℕ;zero;suc;_≤‴_;_≤_;_+_) open _≤_ open _≤‴_ open import Data.Nat.Properties using (≤⇒≤″;≤″⇒≤;≤″⇒≤‴;≤‴⇒≤″;+-monoʳ-≤) - using (+-suc;m+1+n≢m;+-cancelˡ-≡;m≢1+n+m;m+1+n≢0;+-cancelʳ-≡;+-assoc;+-comm) + using (+-suc;m+1+n≢m;+-cancelˡ-≡;m≢1+n+m;m+1+n≢0;+-cancelʳ-≡;+-assoc;+-comm;+-identityʳ) open import Relation.Binary using (Decidable) import Data.Integer as I -open import Data.List using (List;[];_∷_) +open import Data.List using (List;[];_∷_;length) open import Data.Sum using (_⊎_;inj₁;inj₂) open import Relation.Nullary using (Dec;yes;no;¬_) open import Data.Empty using (⊥;⊥-elim) @@ -88,230 +88,33 @@ lem≤‴ (≤‴-step p) (≤‴-step q) = cong ≤‴-step (lem≤‴ p q) +-monoʳ-≤‴ : (n₁ : ℕ) {x y : ℕ} → x ≤‴ y → n₁ + x ≤‴ n₁ + y +-monoʳ-≤‴ n p = ≤″⇒≤‴ (≤⇒≤″ (+-monoʳ-≤ n (≤″⇒≤ (≤‴⇒≤″ p)))) +\end{code} -data Bwd (A : Set) : Set where - [] : Bwd A - _:<_ : Bwd A → A → Bwd A - -infixl 5 _:<_ - - -bwd-length : ∀{A} → Bwd A → ℕ -bwd-length [] = 0 -bwd-length (az :< a) = Data.Nat.suc (bwd-length az) - -_<>>_ : ∀{A} → Bwd A → List A → List A -[] <>> as = as -(az :< a) <>> as = az <>> (a ∷ as) - -_<><_ : ∀{A} → Bwd A → List A → Bwd A -az <>< [] = az -az <>< (a ∷ as) = (az :< a) <>< as - -_:>_∈_ : ∀{A} → Bwd A → List A → List A → Set where - start : ∀{A}(as : List A) → [] <>> as ∈ as - bubble : ∀{A}{a : A}{as : Bwd A}{as' as'' : List A} → as <>> (a ∷ as') ∈ as'' - → (as :< a) <>> as' ∈ as'' +unique∔ : ∀{n n' m : ℕ}(p p' : n ∔ n' ≣ m) → p ≡ p' +unique∔ (start _) (start _) = refl +unique∔ (bubble p) (bubble p') = cong bubble (unique∔ p p') -data _<><_∈_ : ∀{A} → Bwd A → List A → Bwd A → Set where - start : ∀{A}(as : Bwd A) → as <>< [] ∈ as - bubble : ∀{A}{a : A}{as as'' : Bwd A}{as' : List A} - → (as :< a) <>< as' ∈ as'' - → as <>< (a ∷ as') ∈ as'' -unique<>> : ∀{A}{az : Bwd A}{as as' : List A}(p p' : az <>> as ∈ as') → p ≡ p' -unique<>> (start _) (start _) = refl -unique<>> (bubble p) (bubble p') = cong bubble (unique<>> p p') ++2∔ : ∀(n m t : ℕ) → n + m ≡ t → n ∔ m ≣ t ++2∔ zero m .(zero + m) refl = start _ ++2∔ (suc n) m t p = bubble (+2∔ n (suc m) t (trans (+-suc n m) p)) -_<>>_∈'_ : ∀{A} → Bwd A → List A → List A → Set -xs <>> ys ∈' zs = xs <>> ys ≡ zs - - - -<>>-length : ∀{A}(az : Bwd A)(as : List A) - → Data.List.length (az <>> as) ≡ bwd-length az Data.Nat.+ Data.List.length as -<>>-length [] as = refl -<>>-length (az :< x) as = trans (<>>-length az (x ∷ as)) (+-suc _ _) - - - --- reasoning about the length inspired by similar proof about ++ in the stdlib -<>>-rcancel : ∀{A}(az : Bwd A)(as : List A) → az <>> [] ≡ az <>> as → as ≡ [] -<>>-rcancel [] as p = sym p -<>>-rcancel (az :< a) [] p = refl -<>>-rcancel (az :< a) (a' ∷ as) p = ⊥-elim - (m+1+n≢m 1 - (sym (+-cancelˡ-≡ (bwd-length az) - (trans (trans (sym (<>>-length az (a ∷ []))) - (cong Data.List.length p)) - (<>>-length az (a ∷ a' ∷ as)))))) - -<>>-lcancel : ∀{A}(az : Bwd A)(as : List A) → as ≡ az <>> as → az ≡ [] -<>>-lcancel [] as p = refl -<>>-lcancel (az :< a) as p = ⊥-elim - (m≢1+n+m (Data.List.length as) - (trans (trans (cong Data.List.length p) - (<>>-length az (a ∷ as))) - (+-suc (bwd-length az) (Data.List.length as)))) - - - -<>>-lcancel' : ∀{A}(az : Bwd A)(as as' : List A) - → as ≡ az <>> as' - → Data.List.length as ≡ Data.List.length as' - → (az ≡ []) × (as ≡ as') -<>>-lcancel' [] as as' p q = refl ,, p -<>>-lcancel' (az :< a) as as' p q = ⊥-elim - (m≢1+n+m (Data.List.length as') - (trans (trans (trans (sym q) (cong Data.List.length p)) - (<>>-length az (a ∷ as'))) - (+-suc (bwd-length az) (Data.List.length as')))) - -<>>2<>>' : ∀{A}(xs : Bwd A)(ys zs : List A) → xs <>> ys ∈ zs → xs <>> ys ∈' zs -<>>2<>>' [] ys .ys (start .ys) = refl -<>>2<>>' (xs :< x) ys zs (bubble p) = <>>2<>>' xs (x ∷ ys) zs p - -<>>'2<>> : ∀{A}(xs : Bwd A)(ys zs : List A) → xs <>> ys ∈' zs → xs <>> ys ∈ zs -<>>'2<>> [] ys .ys refl = start ys -<>>'2<>> (xs :< x) ys zs p = bubble (<>>'2<>> xs (x ∷ ys) zs p) - -_<><_∈'_ : ∀{A} → Bwd A → List A → Bwd A → Set -xs <>< ys ∈' zs = xs <>< ys ≡ zs - -<><2<><' : ∀{A}(xs : Bwd A)(ys : List A)(zs : Bwd A) - → xs <>< ys ∈ zs → xs <>< ys ∈' zs -<><2<><' xs [] .xs (start .xs) = refl -<><2<><' xs (y ∷ ys) zs (bubble p) = <><2<><' (xs :< y) ys zs p - -<><'2<>< : ∀{A}(xs : Bwd A)(ys : List A)(zs : Bwd A) - → xs <>< ys ∈' zs → xs <>< ys ∈ zs -<><'2<>< xs [] .xs refl = start xs -<><'2<>< xs (x ∷ ys) zs p = bubble (<><'2<>< (xs :< x) ys zs p) - -lemma<><[] : ∀{A}(xs : Bwd A) → (xs <>< []) ≡ xs -lemma<><[] xs = refl - -lemma[]<>> : ∀{A}(xs : List A) → ([] <>> xs) ≡ xs -lemma[]<>> xs = refl - --- convert a list to a backward list and back again - -lemma<>1 : ∀{A}(xs : Bwd A)(ys : List A) → (xs <>< ys) <>> [] ≡ xs <>> ys -lemma<>1 xs [] = refl -lemma<>1 xs (x ∷ ys) = lemma<>1 (xs :< x) ys - -lemma<>2 : ∀{A}(xs : Bwd A)(ys : List A) → ([] <>< (xs <>> ys)) ≡ xs <>< ys -lemma<>2 [] ys = refl -lemma<>2 (xs :< x) ys = lemma<>2 xs (x ∷ ys) - -saturated : ∀{A}(as : List A) → ([] <>< as) <>> [] ∈ as -saturated as = <>>'2<>> ([] <>< as) [] as (lemma<>1 [] as) - -lemma∷1 : ∀{A}(as as' : List A) → [] <>> as ∈ as' → as ≡ as' -lemma∷1 as .as (start .as) = refl - --- these properties are needed for bappTermLem -<>>-cancel-both : ∀{A}(az az' : Bwd A)(as : List A) - → az <>> (az' <>> as) ∈ (az' <>> []) - → az ≡ [] × as ≡ [] -<>>-cancel-both az az' [] p = - <>>-lcancel az (az' <>> []) (sym (<>>2<>>' az (az' <>> []) (az' <>> []) p)) - ,, - refl -<>>-cancel-both az az' (a ∷ as) p = ⊥-elim (m+1+n≢0 - _ - (+-cancelʳ-≡ - _ - 0 - (trans - (trans - (+-assoc (bwd-length az) (Data.List.length (a ∷ as)) (bwd-length az')) - (trans - (cong - (bwd-length az Data.Nat.+_) - (+-comm (Data.List.length (a ∷ as)) (bwd-length az'))) - (trans - (cong - (bwd-length az Data.Nat.+_) - (sym (<>>-length az' (a ∷ as)))) - (trans - (sym (<>>-length az (az' <>> (a ∷ as)))) - (trans - (cong - Data.List.length - (<>>2<>>' az (az' <>> (a ∷ as)) (az' <>> []) p)) - (<>>-length az' [])))))) - (+-comm (bwd-length az') 0)))) - -<>>-cancel-both' : ∀{A}(az az' az'' : Bwd A)(as : List A) - → az <>> (az' <>> as) ∈ (az'' <>> []) → bwd-length az' ≡ bwd-length az'' - → az ≡ [] × as ≡ [] × az' ≡ az'' -<>>-cancel-both' az az' az'' [] p q - with <>>-lcancel' az (az'' <>> []) (az' <>> []) (sym (<>>2<>>' _ _ _ p)) (trans (<>>-length az'' []) (trans (cong (Data.Nat._+ 0) (sym q)) (sym (<>>-length az' [])))) -... | refl ,, Y = refl ,, refl ,, sym (trans (trans (sym (lemma<>2 az'' [])) (cong ([] <><_) Y)) (lemma<>2 az' [])) -<>>-cancel-both' az az' az'' (a ∷ as) p q = ⊥-elim (m+1+n≢0 - _ - (+-cancelʳ-≡ - _ - 0 - (trans - (trans - (+-assoc (bwd-length az) (Data.List.length (a ∷ as)) (bwd-length az')) - (trans - (cong - (bwd-length az Data.Nat.+_) - (+-comm (Data.List.length (a ∷ as)) (bwd-length az'))) - (trans - (cong - (bwd-length az Data.Nat.+_) - (sym (<>>-length az' (a ∷ as)))) - (trans - (sym (<>>-length az (az' <>> (a ∷ as)))) - (trans - (cong - Data.List.length - (<>>2<>>' az (az' <>> (a ∷ as)) (az'' <>> []) p)) - (trans (<>>-length az'' []) (cong (Data.Nat._+ 0) (sym q)))))))) - (+-comm (bwd-length az') 0)))) - -_