Skip to content

Commit

Permalink
working on defining decidability for timelock scripts
Browse files Browse the repository at this point in the history
  • Loading branch information
@Ali-Hill
Ali-Hill committed Oct 3, 2023
1 parent 65ed31d commit 4843267
Show file tree
Hide file tree
Showing 3 changed files with 103 additions and 13 deletions.
79 changes: 68 additions & 11 deletions src/Ledger/Script.lagda
View file
Original file line number Diff line number Diff line change
Expand Up @@ -98,7 +98,8 @@ data Timelock : Set where
RequireTimeExpire : Slot → Timelock
\end{code}
\begin{code}[hide]
module _ ⦃ _ : DecEq Slot ⦄ (_≤_ : Slot → Slot → Set) (_≤ᵇ_ : Slot → Slot → Bool) where

module _ ⦃ _ : DecEq Slot ⦄ (_≤_ : Slot → Slot → Set) (_≤ᵇ_ : Slot → Slot → Bool)(_≤ˢ?_ : (s s₁ : Slot) → Dec (s ≤ s₁)) where
private variable s : Timelock
ss ss' : List Timelock
k : ℕ
Expand All @@ -112,28 +113,31 @@ module _ ⦃ _ : DecEq Slot ⦄ (_≤_ : Slot → Slot → Set) (_≤ᵇ_ : Slot
→ evalTimelock (RequireAllOf ss)
evalAny : Any evalTimelock ss
→ evalTimelock (RequireAnyOf ss)
-- evalMOf : ss' S.⊆ ss → All evalTimelock ss'
-- → evalTimelock (RequireMOf (length ss') ss)
evalMOf : ss' S.⊆ ss → All evalTimelock ss'
→ evalTimelock (RequireMOf (length ss') ss)
evalSig : x ∈ khs
→ evalTimelock (RequireSig x)
evalTSt : I .proj₁ ≡ just l → a ≤ l
→ evalTimelock (RequireTimeStart a)
evalTEx : I .proj₂ ≡ just r → r ≤ a
→ evalTimelock (RequireTimeStart a)
-- → evalTimelock (RequireTimeStart a) -- This is also wrong
→ evalTimelock (RequireTimeExpire a)
\end{code}
\caption{Timelock scripts and their evaluation}
\label{fig:defs:timelock}
\end{figure*}

\begin{code}[hide]
module _ (khs : ℙ KeyHash) where
evalTimelockᵇ : (Maybe Slot × Maybe Slot) → Timelock → Bool
{- evalTimelockᵇ : (Maybe Slot × Maybe Slot) → Timelock → Bool
evalTimelockᵇ I (RequireAllOf []) = true
evalTimelockᵇ I (RequireAllOf (x ∷ xs)) =
evalTimelockᵇ I x ∧ evalTimelockᵇ I (RequireAllOf xs)
evalTimelockᵇ I (RequireAnyOf []) = false
evalTimelockᵇ I (RequireAnyOf (x ∷ xs)) =
evalTimelockᵇ I x ∨ evalTimelockᵇ I (RequireAllOf xs)
evalTimelockᵇ I x ∨ evalTimelockᵇ I (RequireAllOf xs) -- Is this not a mistake
evalTimelockᵇ I (RequireMOf zero _) = true
evalTimelockᵇ I (RequireMOf (suc _) []) = false
evalTimelockᵇ I (RequireMOf (suc m) (x ∷ xs)) = if evalTimelockᵇ I x
Expand All @@ -143,16 +147,69 @@ module _ ⦃ _ : DecEq Slot ⦄ (_≤_ : Slot → Slot → Set) (_≤ᵇ_ : Slot
evalTimelockᵇ (just l , _) (RequireTimeStart x) = x ≤ᵇ l
evalTimelockᵇ (nothing , _) (RequireTimeStart x) = false
evalTimelockᵇ (_ , just r ) (RequireTimeExpire x) = r ≤ᵇ x
evalTimelockᵇ (_ , nothing) (RequireTimeExpire x) = false
evalTimelockᵇ (_ , nothing) (RequireTimeExpire x) = false -}

unquoteDecl DecEq-Timelock = derive-DecEq ((quote Timelock , DecEq-Timelock) ∷ [])
\end{code}

\begin{code}
open P1ScriptStructure

-- P1ScriptStructure-TL : Hashable Timelock ScriptHash → P1ScriptStructure
-- P1ScriptStructure-TL h .P1Script = Timelock
-- P1ScriptStructure-TL h .validP1Script = evalTimelock
-- P1ScriptStructure-TL h .validP1Script? = {!!}
-- P1ScriptStructure-TL h .Hashable-P1Script = h
-- P1ScriptStructure-TL h .DecEq-P1Script = DecEq-Timelock
-- evalMOf : ss' S.⊆ ss → All evalTimelock ss'
-- → evalTimelock (RequireMOf (length ss') ss)
--

open import Data.Nat.Properties using (_≤?_)

{-
data Sublist : REL (List A) (List B) (a ⊔ b ⊔ r) where
[] : Sublist [] []
_∷ʳ_ : ∀ {xs ys} → ∀ y → Sublist xs ys → Sublist xs (y ∷ ys)
_∷_ : ∀ {x xs y ys} → R x y → Sublist xs ys → Sublist (x ∷ xs) (y ∷ ys)


evalMOf : ss' S.⊆ ss → All evalTimelock ss'
→ evalTimelock (RequireMOf (length ss') ss)

RequireMOf : ℕ → List Timelock → Timelock

-}



evalTimelock? : (khs : ℙ KeyHash) (I : Maybe Slot × Maybe Slot)(s : Timelock) → Dec (evalTimelock khs I s)
evalTimelock? khs I (RequireAllOf []) = yes (evalAll [])
evalTimelock? khs I (RequireAllOf (x ∷ xs)) with evalTimelock? khs I x | evalTimelock? khs I (RequireAllOf xs)
... | no ¬p | yes p = no (λ { (evalAll (px ∷ x)) → ¬p px})
... | no ¬p | no ¬p₁ = no (λ { (evalAll (px ∷ x)) → ¬p px})
... | yes p | no ¬p₁ = no (λ { (evalAll (px ∷ x)) → ¬p₁ (evalAll x)})
... | yes p | yes (evalAll x₁) = yes (evalAll (p ∷ x₁))
evalTimelock? khs I (RequireAnyOf []) = no λ { (evalAny ())}
evalTimelock? khs I (RequireAnyOf (x ∷ xs)) with evalTimelock? khs I x | evalTimelock? khs I (RequireAnyOf xs)
... | no ¬p | yes (evalAny x₁) = yes (evalAny (there x₁))
... | no ¬p | no ¬p₁ = no (λ { (evalAny (here px)) → ¬p px ; (evalAny (there x)) → ¬p₁ (evalAny x)})
... | yes p | no ¬p₁ = yes (evalAny (here p))
... | yes p | yes p₁ = yes (evalAny (here p))
evalTimelock? khs I (RequireMOf zero x₁) = yes (evalMOf {!!} [])
evalTimelock? khs I (RequireMOf (suc x) []) = no λ {x₁ → {!!}}
evalTimelock? khs I (RequireMOf (suc x) (x₁ ∷ x₂)) = {!!}
evalTimelock? khs I (RequireSig x) with x ∈? khs
... | no ¬p = no λ { (evalSig x) → ¬p x}
... | yes p = yes (evalSig p)
evalTimelock? khs (just l , snd) (RequireTimeStart x) with x ≤ˢ? l
... | no ¬p = no (λ { (evalTSt refl x₁) → ¬p x₁})
... | yes p = yes (evalTSt refl p)
evalTimelock? khs (nothing , snd) (RequireTimeStart x) = no λ { (evalTSt () x₁)}
evalTimelock? khs (fst , just r) (RequireTimeExpire x) with r ≤ˢ? x
... | no ¬p = no (λ { (evalTEx refl x₁) → ¬p x₁})
... | yes p = yes (evalTEx refl p)
evalTimelock? khs (fst , nothing) (RequireTimeExpire x) = no (λ { (evalTEx () x₁)})

P1ScriptStructure-TL : Hashable Timelock ScriptHash → P1ScriptStructure
P1ScriptStructure-TL h .P1Script = Timelock
P1ScriptStructure-TL h .validP1Script = evalTimelock
P1ScriptStructure-TL h .validP1Script? = evalTimelock?
P1ScriptStructure-TL h .Hashable-P1Script = h
P1ScriptStructure-TL h .DecEq-P1Script = DecEq-Timelock

\end{code}
36 changes: 34 additions & 2 deletions src/Ledger/ScriptValidation.agda
View file
Original file line number Diff line number Diff line change
Expand Up @@ -191,12 +191,44 @@ open Tx
⟦_⟧,_,_,_ : P2Script → CostModel → ExUnits → List Data → Bool
⟦ s ⟧, cm , eu , d = runPLCScript cm s eu d

evalScripts : {{DecEq Slot}} → Tx → List (Script × List Data × ExUnits × CostModel) → IsValid

{-
RequireAllOf : List Timelock → Timelock
RequireAnyOf : List Timelock → Timelock
RequireMOf : ℕ → List Timelock → Timelock
RequireSig : KeyHash → Timelock
RequireTimeStart : Slot → Timelock
RequireTimeExpire : Slot → Timelock
-}

P1ScriptStructure-TL : Hashable Timelock ScriptHash → P1ScriptStructure
P1ScriptStructure-TL h = {!!}

helpMe : P1ScriptStructure → Timelock
helpMe record { P1Script = P1Script ;
validP1Script = vs ;
validP1Script? = validP1Script? ;
Hashable-P1Script = Hashable-P1Script ;
DecEq-P1Script = DecEq-P1Script } = RequireAllOf
({!!} ∷
{!vs!} ∷
{!!} )

record P1ScriptStructure' : Set₁ where
field validP1Script' : ℙ KeyHash × Maybe Slot × Maybe Slot × P1Script → Set

helpMe' : P1ScriptStructure' → Timelock
helpMe' record { validP1Script' = vs } = {!vs!}


evalScripts : {{DecEq Slot}} → Tx → List (Script × List Data × ExUnits × CostModel) → Bool
evalScripts x [] = true
evalScripts x ((inj₁ x₁ , d , eu , cm) ∷ Γ) = evalTimelockᵇ _<ˢ_ (λ x₂ x₃ → isYes (x₂ ≤ˢ? x₃))
(reqSigHash (body x))
(txvldt (body x))
{!x₁!}
{!!}
∧ evalScripts x Γ
evalScripts x ((inj₂ y , d , eu , cm) ∷ Γ) = ⟦ y ⟧, cm , eu , d ∧ evalScripts x Γ

test : Timelock
test = {!!}
1 change: 1 addition & 0 deletions src/Ledger/Utxow.lagda
View file
Original file line number Diff line number Diff line change
Expand Up @@ -72,6 +72,7 @@ data _⊢_⇀⦇_,UTXOW⦈_ where
in
∀[ (vk , σ) ∈ vkSigs ˢ ] isSigned vk (txidBytes txid) σ
→ ∀[ s ∈ scriptsP1 ] validP1Script witsKeyHashes txvldt s
-- ∀[ s ∈ scriptsP1 ] (evalTimelockᵇ witsKeyHashes txvldt ≡ true)
→ witsVKeyNeeded ppolicy utxo txb ⊆ witsKeyHashes
→ scriptsNeeded ppolicy utxo txb ≡ᵉ witsScriptHashes
→ txADhash ≡ M.map hash txAD
Expand Down

0 comments on commit 4843267

Please sign in to comment.