938 migrate validation module

src/Ledger/Conway/Specification/Script.agda → src/Ledger/Conway/Specification/Script.lagda.md

@@ -1,3 +1,9 @@
+---
+source_branch: master
+source_path: src/Ledger/Conway/Specification/Script.lagda.md
+---
+
+```agda
 {-# OPTIONS --safe #-}
 
 open import Ledger.Core.Specification.Crypto
@@ -10,3 +16,4 @@ module Ledger.Conway.Specification.Script
 
 open import Ledger.Conway.Specification.Script.Base cs es public
 open import Ledger.Conway.Specification.Script.Timelock cs es public
+```

src/Ledger/Conway/Specification/Script/Base.agda → src/Ledger/Conway/Specification/Script/Base.lagda.md

@@ -1,3 +1,9 @@
+---
+source_branch: master
+source_path: src/Ledger/Conway/Specification/Script/Base.lagda.md
+---
+
+```agda
 {-# OPTIONS --safe #-}
 
 open import Algebra.Morphism
@@ -82,7 +88,7 @@ record ScriptStructure : Type₁ where
 
   isP1Script? : ∀ {s} → isP1Script s ⁇
   isP1Script? {inj₁ x} .dec = yes tt
-  isP1Script? {inj₂ y} .dec = no λ () 
+  isP1Script? {inj₂ y} .dec = no λ ()
 
   isNativeScript : Script → Type
   isNativeScript = isP1Script
@@ -99,3 +105,4 @@ record ScriptStructure : Type₁ where
 
   toP2Script : Script → Maybe P2Script
   toP2Script = isInj₂
+```

src/Ledger/Conway/Specification/Script/Timelock.lagda → src/Ledger/Conway/Specification/Script/Timelock.lagda.md

@@ -1,11 +1,16 @@
-\section{Scripts}
-\label{sec:scripts}
-\modulenote{\ConwayModule{Script}}, in which we define \Timelock{} scripts.
+---
+source_branch: master
+source_path: src/Ledger/Conway/Specification/Script/Timelock.lagda.md
+---
 
-\Timelock{} scripts can verify the presence of keys and whether a transaction happens in a certain slot
-interval.  The scripts are executed as part of the regular witnessing.
+# Timelock Scripts {#sec:timelock-scripts}
 
-\begin{code}[hide]
+This section defines `Timelock`{.AgdaDatatype} scripts, which verify the presence of
+keys and whether a transaction happens in a certain slot interval.  The scripts
+are executed as part of the regular witnessing.
+
+<!--
+```agda
 {-# OPTIONS --safe #-}
 
 open import Algebra.Morphism
@@ -35,20 +40,23 @@ open import Data.List.Relation.Unary.All
 open import Data.List.Relation.Unary.Any
   using (Any; any?)
 open import stdlib.Data.List.Relation.Unary.MOf
+```
+-->
 
-\end{code}
+## The <span class="AgdaDatatype">Timelock</span> Type {#sec:the-timelock-type}
 
-\begin{figure*}[h]
-\begin{code}
+```agda
 data Timelock : Type where
   RequireAllOf       : List Timelock      → Timelock
   RequireAnyOf       : List Timelock      → Timelock
   RequireMOf         : ℕ → List Timelock  → Timelock
   RequireSig         : KeyHash            → Timelock
   RequireTimeStart   : Slot               → Timelock
   RequireTimeExpire  : Slot               → Timelock
-\end{code}
-\begin{code}[hide]
+```
+
+<!--
+```agda
 unquoteDecl DecEq-Timelock = derive-DecEq ((quote Timelock , DecEq-Timelock) ∷ [])
 
 private variable
@@ -60,30 +68,23 @@ private variable
 
 open import Data.List.Relation.Binary.Sublist.Propositional as S
 import Data.Maybe.Relation.Unary.Any as M
-\end{code}
-\begin{code}[hide]
-data
-\end{code}
-\begin{code}
-  evalTimelock (khs : ℙ KeyHash) (I : Maybe Slot × Maybe Slot) : Timelock → Type where
-  evalAll  : All (evalTimelock khs I) ss
-           → (evalTimelock khs I) (RequireAllOf ss)
-  evalAny  : Any (evalTimelock khs I) ss
-           → (evalTimelock khs I) (RequireAnyOf ss)
-  evalMOf  : MOf m (evalTimelock khs I) ss
-           → (evalTimelock khs I) (RequireMOf m ss)
-  evalSig  : x ∈ khs
-           → (evalTimelock khs I) (RequireSig x)
-  evalTSt  : M.Any (a ≤_) (I .proj₁)
-           → (evalTimelock khs I) (RequireTimeStart a)
-  evalTEx  : M.Any (_≤ a) (I .proj₂)
-           → (evalTimelock khs I) (RequireTimeExpire a)
-\end{code}
-\caption{Timelock scripts and their evaluation}
-\label{fig:defs:timelock}
-\end{figure*}
-
-\begin{code}[hide]
+```
+-->
+
+## The <span class="AgdaDatatype">evalTimelock</span> Type {#sec:the-evaltimelock-type}
+
+```agda
+data evalTimelock (khs : ℙ KeyHash) (I : Maybe Slot × Maybe Slot) : Timelock → Type where
+  evalAll : All (evalTimelock khs I) ss → (evalTimelock khs I) (RequireAllOf ss)
+  evalAny : Any (evalTimelock khs I) ss → (evalTimelock khs I) (RequireAnyOf ss)
+  evalMOf : MOf m (evalTimelock khs I) ss → (evalTimelock khs I) (RequireMOf m ss)
+  evalSig : x ∈ khs → (evalTimelock khs I) (RequireSig x)
+  evalTSt : M.Any (a ≤_) (I .proj₁) → (evalTimelock khs I) (RequireTimeStart a)
+  evalTEx : M.Any (_≤ a) (I .proj₂) → (evalTimelock khs I) (RequireTimeExpire a)
+```
+
+<!--
+```agda
 instance
   Dec-evalTimelock : evalTimelock ⁇³
   Dec-evalTimelock {khs} {I} {tl} .dec = go? tl
@@ -130,4 +131,5 @@ instance
         (RequireTimeStart a)  → mapDec evalTSt evalTSt˘ dec
         (RequireTimeExpire a) → mapDec evalTEx evalTEx˘ dec
         (RequireMOf m xs)     → mapDec evalMOf evalMOf˘ (MOf-go? m xs)
-\end{code}
+```
+-->

src/Ledger/Conway/Specification/Script/Validation.agda → src/Ledger/Conway/Specification/Script/Validation.lagda.md

@@ -1,3 +1,9 @@
+---
+source_branch: master
+source_path: src/Ledger/Conway/Specification/Script/Validation.lagda.md
+---
+
+```agda
 {-# OPTIONS --safe #-}
 
 open import Ledger.Conway.Specification.Transaction
@@ -124,3 +130,4 @@ opaque
 
 evalP2Scripts : List (P2Script × List Data × ExUnits × CostModel) → Bool
 evalP2Scripts = all (λ (s , d , eu , cm) → runPLCScript cm s eu d)
+```