CIP-0140? | Ouroboros Peras - Faster Settlement

CIP-0PRS/.gitignore

@@ -0,0 +1 @@
+*.agdai

CIP-0PRS/iog-prelude/Prelude/Allable.agda

@@ -0,0 +1,45 @@
+module Prelude.Allable where
+
+open import Prelude.Init
+open import Prelude.LiteralSequences
+open import Prelude.DecEq
+
+record Allable (F : Type ℓ → Type ℓ) : Type (lsuc ℓ) where
+  field All : ∀ {A} → (A → Type) → F A → Type ℓ
+
+  ∀∈-syntax   = All
+  ∀∈-syntax′  = All
+  ¬∀∈-syntax  = λ {A} P → ¬_ ∘ All {A} P
+  ¬∀∈-syntax′ = ¬∀∈-syntax
+  infix 2 ∀∈-syntax ∀∈-syntax′ ¬∀∈-syntax ¬∀∈-syntax′
+  syntax ∀∈-syntax   P         xs = ∀[∈     xs ] P
+  syntax ∀∈-syntax′  (λ x → P) xs = ∀[  x ∈ xs ] P
+  syntax ¬∀∈-syntax  P         xs = ¬∀[∈    xs ] P
+  syntax ¬∀∈-syntax′ (λ x → P) xs = ¬∀[ x ∈ xs ] P
+
+open Allable ⦃...⦄ public
+
+instance
+  Allable-List : Allable {ℓ} List
+  Allable-List .All = L.All.All
+
+  Allable-Vec : ∀ {n} → Allable {ℓ} (flip Vec n)
+  Allable-Vec .All P = V.All.All P
+
+  Allable-Maybe : Allable {ℓ} Maybe
+  Allable-Maybe .All = M.All.All
+
+private
+  open import Prelude.Decidable
+
+  _ : ∀[ x ∈ List ℕ ∋ [ 1 ⨾ 2 ⨾ 3 ] ] (x > 0)
+  _ = auto
+
+  _ : ∀[ x ∈ just 42 ] (x > 0)
+  _ = auto
+
+  _ : ∀[ x ∈ nothing ] (x > 0)
+  _ = auto
+
+  _ : ¬∀[ x ∈ just 0 ] (x > 0)
+  _ = auto

CIP-0PRS/iog-prelude/Prelude/Anyable.agda

@@ -0,0 +1,41 @@
+module Prelude.Anyable where
+
+open import Prelude.Init
+open import Prelude.LiteralSequences
+
+record Anyable (F : Type ℓ → Type ℓ) : Type (lsuc ℓ) where
+  field Any : ∀ {A} → (A → Type) → F A → Type ℓ
+
+  ∃∈-syntax  = Any
+  ∃∈-syntax′ = Any
+  ∄∈-syntax  = λ {A} P → ¬_ ∘ Any {A} P
+  ∄∈-syntax′ = ∄∈-syntax
+  infix 2 ∃∈-syntax ∃∈-syntax′ ∄∈-syntax ∄∈-syntax′
+  syntax ∃∈-syntax  P         xs = ∃[∈    xs ] P
+  syntax ∃∈-syntax′ (λ x → P) xs = ∃[ x ∈ xs ] P
+  syntax ∄∈-syntax  P         xs = ∄[∈    xs ] P
+  syntax ∄∈-syntax′ (λ x → P) xs = ∄[ x ∈ xs ] P
+
+open Anyable ⦃...⦄ public
+
+instance
+  Anyable-List : Anyable {ℓ} List
+  Anyable-List .Any = L.Any.Any
+
+  Anyable-Vec : ∀ {n} → Anyable {ℓ} (flip Vec n)
+  Anyable-Vec .Any P = V.Any.Any P
+
+  Anyable-Maybe : Anyable {ℓ} Maybe
+  Anyable-Maybe .Any = M.Any.Any
+
+private
+  open import Prelude.Decidable
+
+  _ : ∃[ x ∈ List ℕ ∋ [ 1 ⨾  2 ⨾ 3 ] ] (x > 0)
+  _ = auto
+
+  _ : ∃[ x ∈ just 42 ] (x > 0)
+  _ = auto
+
+  _ : ∄[ x ∈ nothing ] (x > 0)
+  _ = auto

CIP-0PRS/iog-prelude/Prelude/AssocList.agda

@@ -0,0 +1,59 @@
+-- Finite maps as association lists
+module Prelude.AssocList where
+
+open import Prelude.Init
+open import Prelude.DecEq
+open import Prelude.Decidable
+open import Prelude.Irrelevance
+open import Prelude.Default
+
+AssocList : Type → Type → Type
+AssocList K V = List (K × V)
+
+mapValues : ∀ {K V V′} → (V → V′) → AssocList K V → AssocList K V′
+mapValues f = map (map₂ f)
+
+module _ {K V : Type} where
+  _∈ᵐ_ _∉ᵐ_ : K → AssocList K V → Type
+  k ∈ᵐ m = AnyFirst ((k ≡_) ∘ proj₁) m
+  k ∉ᵐ m = ·¬ (k ∈ᵐ m)
+
+  ∈ᵐ-irrelevant : ∀ {k m} → Irrelevant (k ∈ᵐ m)
+  ∈ᵐ-irrelevant = AnyFirst-irrelevant λ where refl refl → refl
+
+  _∪_ : Op₂ (AssocList K V)
+  _∪_ = _++_
+
+  module _ ⦃ _ : DecEq K ⦄ where
+
+    _∈ᵐ?_ = ¿ _∈ᵐ_ ¿²
+    _∉ᵐ?_ = ¿ _∉ᵐ_ ¿²
+
+    _‼_ : ∀ {k : K} (m : AssocList K V) → k ∈ᵐ m → V
+    m ‼ p = L.First.satisfied p .proj₁ .proj₂
+
+    _⁉_ : AssocList K V → K → Maybe V
+    m ⁉ k with k ∈ᵐ? m
+    ... | yes p = just (m ‼ p)
+    ... | no  _ = nothing
+
+    module _ {k : K} {m : AssocList K V} where
+      _∷~_ : k ∈ᵐ m → (V → V) → AssocList K V
+      p ∷~ f = m [ L.First.index p ]∷= (k , f (m ‼ p))
+
+      _∷=_ : k ∈ᵐ m → V → AssocList K V
+      p ∷= v = p ∷~ const v
+
+    module _ ⦃ _ : Default V ⦄ where
+      modify : K → (V → V) → Op₁ (AssocList K V)
+      modify k f m = case k ∈ᵐ? m of λ where
+        (no _)  → (k , f def) ∷ m
+        (yes p) → p ∷= f (m ‼ p)
+
+      set : K → V → Op₁ (AssocList K V)
+      set k v = modify k (const v)
+
+      _‼d_ : AssocList K V → K → V
+      m ‼d k with m ⁉ k
+      ... | nothing = def
+      ... | just v  = v

CIP-0PRS/iog-prelude/Prelude/Bitmasks.agda

@@ -0,0 +1,21 @@
+module Prelude.Bitmasks where
+
+open import Prelude.Init
+open import Prelude.Lists
+open import Prelude.Default
+
+private variable A : Type
+
+Bitmask : List A → Type
+Bitmask xs = Vec Bool (length xs)
+
+select : (xs : List A) → Bitmask xs → List A
+select []       []       = []
+select (x ∷ xs) (b ∷ bs) = (if b then (x ∷_) else id) (select xs bs)
+
+switchOn switchOff : ∀ {xs : List A} → Index xs → Op₁ (Bitmask xs)
+switchOn  i bs = bs V.[ i ]≔ true
+switchOff i bs = bs V.[ i ]≔ false
+
+-- set default bits to 0
+instance Default-Bool = Default-Bool-✖

CIP-0PRS/iog-prelude/Prelude/Closures.agda

@@ -0,0 +1,22 @@
+open import Prelude.Init
+
+module Prelude.Closures {A : Type ℓ} (_—→_ : Rel A ℓ) where
+
+private variable x y z : A
+
+-- left-biased
+infix  3 _∎
+infixr 2 _—→⟨_⟩_ _—↠⟨_⟩_
+infix  1 begin_; pattern begin_ x = x
+infix -1 _—↠_
+
+data _—↠_ : Rel A ℓ where
+  _∎ : ∀ x → x —↠ x
+  _—→⟨_⟩_ : ∀ x → x —→ y → y —↠ z → x —↠ z
+
+—↠-trans : Transitive _—↠_
+—↠-trans (x ∎) xz = xz
+—↠-trans (_ —→⟨ r ⟩ xy) yz = _ —→⟨ r ⟩ —↠-trans xy yz
+
+_—↠⟨_⟩_ : ∀ x → x —↠ y → y —↠ z → x —↠ z
+_—↠⟨_⟩_ _ = —↠-trans

CIP-0PRS/iog-prelude/Prelude/DecEq.agda

@@ -0,0 +1,33 @@
+module Prelude.DecEq where
+
+open import Prelude.Init
+
+record DecEq (A : Type) : Type where
+  field _≟_ : DecidableEquality A
+
+  _==_ : A → A → Bool
+  _==_ = ⌊_⌋ ∘₂ _≟_
+
+  ≟-refl : ∀ (x : A) → (x ≟ x) ≡ yes refl
+  ≟-refl x with refl , p ← dec-yes (x ≟ x) refl = p
+open DecEq ⦃...⦄ public
+
+private variable
+  n : ℕ
+  A : Type
+
+instance
+  DecEq-⊤ : DecEq ⊤
+  DecEq-⊤ ._≟_ _ _ = yes refl
+
+  DecEq-ℕ : DecEq ℕ
+  DecEq-ℕ = record {Nat}
+
+  DecEq-Fin : DecEq (Fin n)
+  DecEq-Fin = record {Fi}
+
+  DecEq-List : ⦃ DecEq A ⦄ → DecEq (List A)
+  DecEq-List ._≟_ = L.≡-dec _≟_
+
+  DecEq-Bin : DecEq Bitstring
+  DecEq-Bin = record {Bin}

CIP-0PRS/iog-prelude/Prelude/Decidable.agda

@@ -0,0 +1,92 @@
+module Prelude.Decidable where
+
+open import Prelude.Init
+
+record _⁇ (P : Type ℓ) : Type ℓ where
+  constructor ⁇_
+  field dec : Dec P
+
+  auto : ⦃ True dec ⦄ → P
+  auto ⦃ pr ⦄ = toWitness pr
+
+  contradict : ∀ {X : Type} {pr : False dec} → P → X
+  contradict {pr = pr} = ⊥-elim ∘ toWitnessFalse pr
+
+open _⁇ ⦃ ... ⦄ public
+
+¿_¿ : ∀ (X : Type ℓ) → ⦃ X ⁇ ⦄ → Dec X
+¿ _ ¿ = dec
+
+_⁇¹ : ∀ {A : Type ℓ} → (P : Pred A ℓ′) → Type (ℓ ⊔ₗ ℓ′)
+P ⁇¹ = ∀ {x} → P x ⁇
+
+dec¹ : ∀ {A : Type ℓ} {P : Pred A ℓ′} → ⦃ P ⁇¹ ⦄ → Decidable¹ P
+dec¹ _ = dec
+
+¿_¿¹ : ∀ {A : Type ℓ} (P : Pred A ℓ′) → ⦃ P ⁇¹ ⦄ → Decidable¹ P
+¿ _ ¿¹ = dec¹
+
+_⁇² : ∀ {A B : Type ℓ} → (P : REL A B ℓ′) → Type (ℓ ⊔ₗ ℓ′)
+_~_ ⁇² = ∀ {x y} → (x ~ y) ⁇
+
+dec² : ∀ {A B : Type ℓ} {_~_ : REL A B ℓ′} → ⦃ _~_ ⁇² ⦄ → Decidable² _~_
+dec² _ _ = dec
+
+¿_¿² : ∀ {A B : Type ℓ} (_~_ : REL A B ℓ′) → ⦃ _~_ ⁇² ⦄ → Decidable² _~_
+¿ _ ¿² = dec²
+
+infix -100 auto∶_
+auto∶_ : ∀ (X : Type ℓ) → ⦃ X ⁇ ⦄ → Type
+auto∶_ A = True ¿ A ¿
+
+dec-✓ : ∀ {P : Type ℓ}  ⦃ _ : P ⁇ ⦄ (p : P) → ∃ λ p′ → (¿ P ¿ ≡ yes p′)
+dec-✓ {P = P} p = dec-yes ¿ P ¿ p
+
+-- ** instances
+
+private variable A : Type ℓ; B : Type ℓ′
+instance
+  Dec-⊥ : ⊥ ⁇
+  Dec-⊥ .dec = no λ()
+
+  Dec-⊤ : ⊤ ⁇
+  Dec-⊤ .dec = yes tt
+
+  Dec-T : T ⁇¹
+  Dec-T {false} .dec = no λ ()
+  Dec-T {true}  .dec = yes tt
+
+module _ ⦃ _ : A ⁇ ⦄ ⦃ _ : B ⁇ ⦄ where instance
+  Dec-→ : (A → B) ⁇
+  Dec-→ .dec = dec →-dec dec
+    where open import Relation.Nullary
+
+  Dec-× : (A × B) ⁇
+  Dec-× .dec = dec ×-dec dec
+    where open import Relation.Nullary
+
+  Dec-⊎ : (A ⊎ B) ⁇
+  Dec-⊎ .dec = dec ⊎-dec dec
+    where open import Relation.Nullary
+
+instance
+  open import Prelude.DecEq
+  DecEq⇒Dec : ⦃ DecEq A ⦄ → _≡_ {A = A} ⁇²
+  DecEq⇒Dec .dec = _ ≟ _
+
+  open import Data.Nat using (_≤_; _≤?_)
+  Dec-≤ : _≤_ ⁇²
+  Dec-≤ .dec = _ ≤? _
+
+module _ {P : Pred A ℓ} ⦃ _ : P ⁇¹ ⦄ where instance
+  Dec-Any : L.Any.Any P ⁇¹
+  Dec-Any .dec = L.Any.any? dec¹ _
+
+  Dec-All : L.All.All P ⁇¹
+  Dec-All .dec = L.All.all? dec¹ _
+
+  Dec-MAny : M.Any.Any P ⁇¹
+  Dec-MAny .dec = M.Any.dec dec¹ _
+
+  Dec-MAll : M.All.All P ⁇¹
+  Dec-MAll .dec = M.All.dec dec¹ _

CIP-0PRS/iog-prelude/Prelude/Default.agda

@@ -0,0 +1,27 @@
+module Prelude.Default where
+
+open import Prelude.Init
+
+-- Types that have a default value.
+record Default (A : Type) : Type where
+  field def : A
+open Default ⦃...⦄ public
+
+private variable A B : Type; n : ℕ
+
+instance
+  Default-⊤ : Default ⊤
+  Default-⊤ .def = tt
+
+  Default-× : ⦃ Default A ⦄ → ⦃ Default B ⦄ → Default (A × B)
+  Default-× .def = def , def
+
+  Default-List : Default (List A)
+  Default-List .def = []
+
+  Default-Vec : ⦃ Default A ⦄ → Default (Vec A n)
+  Default-Vec .def = V.replicate _ def
+
+Default-Bool-✖ Default-Bool-✓ : Default Bool
+Default-Bool-✖ .def = false
+Default-Bool-✓ .def = true

CIP-0PRS/iog-prelude/Prelude/FromNat.agda

@@ -0,0 +1,41 @@
+module Prelude.FromNat where
+
+open import Prelude.Init
+open import Prelude.LiteralSequences
+open import Prelude.Decidable
+
+-- ** dependent version
+record Fromℕ (A : Type) (Can : ℕ → Type) : Type where
+  field fromℕ : (n : ℕ) → ⦃ Can n ⦄ → A
+open Fromℕ ⦃...⦄ public
+{-# BUILTIN FROMNAT fromℕ #-}
+
+-- ** non-dependent version
+Fromℕ′ : Type → Type
+Fromℕ′ A = Fromℕ A (const ⊤)
+
+fromℕ′ : ∀ {A} → ⦃ Fromℕ′ A ⦄ → ℕ → A
+fromℕ′ n = fromℕ n
+
+record MkFromℕ′ (A : Type) : Type where
+  constructor fromℕ∶_
+  field fromℕ : ℕ → A
+
+mkFromℕ′ : ∀ {A} → MkFromℕ′ A → Fromℕ′ A
+mkFromℕ′ r .fromℕ n = r .MkFromℕ′.fromℕ n
+
+instance
+  Fromℕ-Nat   = Fromℕ′ ℕ          ∋ mkFromℕ′ (fromℕ∶ id)
+  Fromℕ-Bool  = Fromℕ′ Bool       ∋ mkFromℕ′ (fromℕ∶ λ where 0 → false; _ → true)
+  Fromℕ-Bin   = Fromℕ′ Bitstring  ∋ mkFromℕ′ (record {Bin})
+  Fromℕ-Float = Fromℕ′ Float      ∋ mkFromℕ′ (record {Fl})
+
+  Fromℕ-Fin : ∀ {n} → Fromℕ (Fin n) (λ m → True (¿ suc m ≤ n ¿))
+  Fromℕ-Fin {n} .fromℕ m ⦃ m≤n ⦄ = (Fi.# m) {n} {m≤n}
+
+_ = ℕ         ∋ 0
+_ = Bool      ∋ 0
+_ = Bitstring ∋ 0
+_ = Float     ∋ 0
+_ = Fin 1     ∋ 0
+_ = Fin 200   ∋ 1