From 4a4a962de1e93af1ca94fd867a6b1d097ecdeca5 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Javier=20D=C3=ADaz?= <javier.diaz@iohk.io>
Date: Thu, 21 Nov 2024 12:13:27 +0000
Subject: [PATCH] Generate Haskell code for TickNonce

---
 docs/agda-spec/src/Foreign/Convertible.agda   |  82 ++++
 .../src/Foreign/Convertible/Deriving.agda     | 172 +++++++++
 .../src/Foreign/Convertible/DerivingTest.agda |  86 +++++
 docs/agda-spec/src/Foreign/HaskellTypes.agda  |  52 +++
 .../src/Foreign/HaskellTypes/Deriving.agda    | 362 ++++++++++++++++++
 docs/agda-spec/src/Makefile                   |  37 +-
 .../src/Spec/Foreign/ExternalFunctions.agda   |  15 +
 .../src/Spec/Foreign/HSConsensus.agda         |   4 +
 .../Spec/Foreign/HSConsensus/BaseTypes.agda   |  25 ++
 .../src/Spec/Foreign/HSConsensus/Core.agda    |  53 +++
 .../Spec/Foreign/HSConsensus/TickNonce.agda   |  19 +
 docs/agda-spec/src/Spec/Foreign/HSTypes.agda  |  42 ++
 docs/agda-spec/src/Spec/hs-src/Lib.hs         |  11 +
 docs/agda-spec/src/Spec/hs-src/cabal.project  |   2 +
 .../cardano-consensus-executable-spec.cabal   |  57 +++
 docs/agda-spec/src/Spec/hs-src/test/Spec.hs   |   1 +
 .../src/Spec/hs-src/test/TickNonceSpec.hs     |  30 ++
 docs/agda-spec/src/Tactic/Substitute.agda     |  47 +++
 ...ger.agda-lib => formal-consensus.agda-lib} |   4 +-
 19 files changed, 1096 insertions(+), 5 deletions(-)
 create mode 100644 docs/agda-spec/src/Foreign/Convertible.agda
 create mode 100644 docs/agda-spec/src/Foreign/Convertible/Deriving.agda
 create mode 100644 docs/agda-spec/src/Foreign/Convertible/DerivingTest.agda
 create mode 100644 docs/agda-spec/src/Foreign/HaskellTypes.agda
 create mode 100644 docs/agda-spec/src/Foreign/HaskellTypes/Deriving.agda
 create mode 100644 docs/agda-spec/src/Spec/Foreign/ExternalFunctions.agda
 create mode 100644 docs/agda-spec/src/Spec/Foreign/HSConsensus.agda
 create mode 100644 docs/agda-spec/src/Spec/Foreign/HSConsensus/BaseTypes.agda
 create mode 100644 docs/agda-spec/src/Spec/Foreign/HSConsensus/Core.agda
 create mode 100644 docs/agda-spec/src/Spec/Foreign/HSConsensus/TickNonce.agda
 create mode 100644 docs/agda-spec/src/Spec/Foreign/HSTypes.agda
 create mode 100644 docs/agda-spec/src/Spec/hs-src/Lib.hs
 create mode 100644 docs/agda-spec/src/Spec/hs-src/cabal.project
 create mode 100644 docs/agda-spec/src/Spec/hs-src/cardano-consensus-executable-spec.cabal
 create mode 100644 docs/agda-spec/src/Spec/hs-src/test/Spec.hs
 create mode 100644 docs/agda-spec/src/Spec/hs-src/test/TickNonceSpec.hs
 create mode 100644 docs/agda-spec/src/Tactic/Substitute.agda
 rename docs/agda-spec/src/{formal-ledger.agda-lib => formal-consensus.agda-lib} (69%)

diff --git a/docs/agda-spec/src/Foreign/Convertible.agda b/docs/agda-spec/src/Foreign/Convertible.agda
new file mode 100644
index 0000000000..3cc064528d
--- /dev/null
+++ b/docs/agda-spec/src/Foreign/Convertible.agda
@@ -0,0 +1,82 @@
+module Foreign.Convertible where
+
+open import Ledger.Prelude
+open import Foreign.HaskellTypes
+
+record Convertible (A B : Type) : Type where
+  field to   : A → B
+        from : B → A
+open Convertible ⦃...⦄ public
+
+HsConvertible : (A : Set) → ⦃ HasHsType A ⦄ → Set
+HsConvertible A = Convertible A (HsType A)
+
+Convertible-Refl : ∀ {A} → Convertible A A
+Convertible-Refl = λ where .to → id; .from → id
+
+Convertible₁ : (Type → Type) → (Type → Type) → Type₁
+Convertible₁ T U = ∀ {A B} → ⦃ Convertible A B ⦄ → Convertible (T A) (U B)
+
+Convertible₂ : (Type → Type → Type) → (Type → Type → Type) → Type₁
+Convertible₂ T U = ∀ {A B} → ⦃ Convertible A B ⦄ → Convertible₁ (T A) (U B)
+
+Functor⇒Convertible : ∀ {F : Type↑} → ⦃ Functor F ⦄ → Convertible₁ F F
+Functor⇒Convertible = λ where
+  .to   → map to
+  .from → map from
+
+Bifunctor⇒Convertible : ∀ {F} → ⦃ Bifunctor F ⦄ → Convertible₂ F F
+Bifunctor⇒Convertible = λ where
+  .to   → bimap to to
+  .from → bimap from from
+
+_⨾_ : ∀ {A B C} → Convertible A B → Convertible B C → Convertible A C
+(c ⨾ c') .to   = c' .to   ∘ c  .to
+(c ⨾ c') .from = c  .from ∘ c' .from
+
+-- ** instances
+
+open import Foreign.Haskell
+open import Foreign.Haskell.Coerce using (coerce)
+
+instance
+  Convertible-Maybe : Convertible₁ Maybe Maybe
+  Convertible-Maybe = Functor⇒Convertible
+
+  Convertible-× : Convertible₂ _×_ _×_
+  Convertible-× = Bifunctor⇒Convertible
+
+  Convertible-Pair : Convertible₂ _×_ Pair
+  Convertible-Pair = λ where
+    .to   → coerce ∘ bimap to to
+    .from → bimap from from ∘ coerce
+
+  Convertible-⊎ : Convertible₂ _⊎_ _⊎_
+  Convertible-⊎ = Bifunctor⇒Convertible
+
+  Convertible-Either : Convertible₂ _⊎_ Either
+  Convertible-Either = λ where
+    .to   → coerce ∘ bimap to to
+    .from → bimap from from ∘ coerce
+
+  Convertible-FinSet : Convertible₁ ℙ_ List
+  Convertible-FinSet = λ where
+    .to   → map to   ∘ setToList
+    .from → fromList ∘ map from
+
+  Convertible-Map : ∀ {K K' V V'} → ⦃ DecEq K ⦄
+    → ⦃ Convertible K K' ⦄ → ⦃ Convertible V V' ⦄
+    → Convertible (K ⇀ V) (List $ Pair K' V')
+  Convertible-Map = λ where
+    .to   → to        ∘ proj₁
+    .from → fromListᵐ ∘ map from
+
+  Convertible-List : Convertible₁ List List
+  Convertible-List = λ where
+    .to   → map to
+    .from → map from
+
+  Convertible-Fun : ∀ {A A' B B'} → ⦃ Convertible A A' ⦄ → ⦃ Convertible B B' ⦄ → Convertible (A → B) (A' → B')
+  Convertible-Fun = λ where
+    .to   → λ f → to   ∘ f ∘ from
+    .from → λ f → from ∘ f ∘ to
diff --git a/docs/agda-spec/src/Foreign/Convertible/Deriving.agda b/docs/agda-spec/src/Foreign/Convertible/Deriving.agda
new file mode 100644
index 0000000000..dc85fc206c
--- /dev/null
+++ b/docs/agda-spec/src/Foreign/Convertible/Deriving.agda
@@ -0,0 +1,172 @@
+module Foreign.Convertible.Deriving where
+
+open import Level
+open import MetaPrelude
+open import Meta
+
+import Data.List as L
+import Data.List.NonEmpty as NE
+import Data.String as S
+import Data.Product as P
+
+open import Relation.Nullary
+open import Relation.Nullary.Decidable
+
+open import Reflection.Tactic
+open import Reflection.AST.Term
+open import Reflection.AST.DeBruijn
+import Reflection.TCM as R
+open import Reflection.Utils
+open import Reflection.Utils.TCI
+import Function.Identity.Effectful as Identity
+
+open import Class.DecEq
+open import Class.DecEq
+open import Class.Functor
+open import Class.Monad
+open import Class.MonadTC.Instances
+open import Class.Traversable
+open import Class.Show
+open import Class.MonadReader
+
+open import Tactic.Substitute
+open import Foreign.Convertible
+open import Foreign.HaskellTypes
+open import Foreign.HaskellTypes.Deriving
+
+private instance
+  _ = Functor-M {TC}
+
+-- TODO: move to agda-stdlib-meta
+liftTC : ∀ {a} {A : Set a} → R.TC A → TC A
+liftTC m _ = m
+
+private
+
+  open MonadReader ⦃...⦄
+
+  variable
+    A B C : Set
+
+  TyViewTel = List (Abs (Arg Type))
+
+  substTel : Subst TyViewTel
+  substTel x s [] = []
+  substTel x s (abs z t ∷ tel) = abs z (substArg x s t) ∷ (substTel (ℕ.suc x) s tel)
+    -- Note: `abs` is abused in TyViewTel and doesn't actually scope over the `t`
+
+  -- Substitute leading level parameters with lzero
+  smashLevels : TyViewTel → ℕ × TyViewTel
+  smashLevels (abs s (arg i (def (quote Level) [])) ∷ tel) =
+    P.map ℕ.suc (substTel 0 (quote 0ℓ ∙)) $ smashLevels tel
+  smashLevels tel = (0 , tel)
+
+  tyViewToTel : TyViewTel → Telescope
+  tyViewToTel = L.map λ where (abs s a) → s , a
+
+  hideTyView : Abs (Arg A) → Abs (Arg A)
+  hideTyView (abs s (arg (arg-info _ m) x)) = abs s (arg (arg-info hidden m) x)
+
+  -- The type of a Convertible instance. For parameterised types adds the appropriate instance
+  -- arguments and instantiates level arguments to lzero. For instance,
+  -- instanceType _⊎_ Hs.Either = {A B : Set} {a b : Set} → ⦃ Convertible A a ⦄ → ⦃ Convertible B b ⦄
+  --                              Convertible (A ⊎ B) (Hs.Either a b)
+  instanceType : (agdaName hsName : Name) → TC TypeView
+  instanceType agdaName hsName = do
+    aLvls , agdaParams ← smashLevels <$> getParamsAndIndices agdaName
+    hLvls , hsParams   ← smashLevels <$> getParamsAndIndices hsName
+    true ← return (length agdaParams == length hsParams)
+      where false → liftTC $ R.typeErrorFmt "%q and %q have different number of parameters" agdaName hsName
+    let n = length agdaParams
+        l₀ = quote 0ℓ ∙
+    agdaTy ← applyWithVisibility agdaName $ L.replicate aLvls l₀ ++ L.map ♯ (take n (downFrom (n + n)))
+    hsTy   ← applyWithVisibility hsName   $ L.replicate hLvls l₀ ++ L.map ♯ (downFrom n)
+    let instHead = weaken n $ quote Convertible ∙⟦ agdaTy ∣ hsTy ⟧
+        tel      = L.map hideTyView (agdaParams ++ hsParams) ++
+                   L.replicate n (abs "_" (iArg (quote Convertible ∙⟦ ♯ (n + n ∸ 1) ∣ ♯ (n ∸ 1) ⟧)))
+    return $ tel , instHead
+
+  -- Compute one clause of the Convertible instance. For instance,
+  -- conversionClause Convertible.to to ((c₁ , _) , (c₂ , _)) generates
+  -- .to (c₁ x₁ .. xn) = c₂ (to x₁) .. (to xn)
+  -- where the xi are the visible constructor arguments.
+  conversionClause : Name → Name → (Name × Type) × (Name × Type) → TC Clause
+  conversionClause prjP prjE ((fromC , fromTy) , (toC , toTy)) = do
+    let isVis   = λ { (abs _ (arg (arg-info visible _) _)) → true; _ → false }
+        fromTel = L.filterᵇ isVis (proj₁ (viewTy fromTy))
+        toTel   = L.filterᵇ isVis (proj₁ (viewTy toTy))
+        n       = length fromTel
+        mkCon  c mkArg = Term.con c    $ L.map (vArg ∘ mkArg ∘ ♯)  (downFrom n)
+        mkConP c mkArg = Pattern.con c $ L.map (vArg ∘ mkArg ∘ `_) (downFrom n)
+    true ← return (n == length toTel)
+      where false → liftTC $ R.typeErrorFmt "%q and %q have different number of arguments" fromC toC
+    return $ clause (tyViewToTel $ L.map (λ where (abs x (arg i _)) → abs x (arg i unknown)) fromTel)
+                    (vArg (proj prjP) ∷ vArg (mkConP fromC id) ∷ [])
+                    (mkCon toC (prjE ∙⟦_⟧))
+
+  -- Compute the clauses of a convertible instance.
+  instanceClauses : (agdaName hsName : Name) → TC (List Clause)
+  instanceClauses agdaName hsName = do
+    agdaCons ← getConstrs agdaName
+    hsCons   ← getConstrs hsName
+    agdaPars ← length <$> getParamsAndIndices agdaName
+    hsPars   ← length <$> getParamsAndIndices hsName
+    true ← return (length agdaCons == length hsCons)
+      where false → liftTC $ R.typeErrorFmt "%q and %q have different number of constructors" agdaName hsName
+    toClauses   ← mapM (conversionClause (quote Convertible.to)   (quote to)  ) (L.zip agdaCons hsCons)
+    fromClauses ← mapM (conversionClause (quote Convertible.from) (quote from)) (L.zip hsCons agdaCons)
+    return $ toClauses ++ fromClauses
+
+  absurdClause : Name → Clause
+  absurdClause prj = absurd-clause (("x" , vArg unknown) ∷ []) (vArg (proj prj) ∷ vArg (absurd 0) ∷ [])
+
+  -- Compute conversion clauses for the current goal and wrap them in a pattern lambda.
+  patternLambda : TC Term
+  patternLambda = do
+    quote Convertible ∙⟦ `A ∣ `B ⟧ ← reduce =<< goalTy
+      where t → liftTC $ R.typeErrorFmt "Expected Convertible A B, got %t" t
+    agdaCons ← getConstrsForType `A
+    hsCons   ← getConstrsForType `B
+    toClauses   ← mapM (conversionClause (quote Convertible.to)   (quote to)  ) (L.zip agdaCons hsCons)
+    fromClauses ← mapM (conversionClause (quote Convertible.from) (quote from)) (L.zip hsCons agdaCons)
+    case toClauses ++ fromClauses of λ where
+      []  → return $ pat-lam (absurdClause (quote Convertible.to) ∷ absurdClause (quote Convertible.from) ∷ []) []
+      cls → return $ pat-lam cls []
+
+doPatternLambda : Term → R.TC Term
+doPatternLambda hole = patternLambda =<< initTCEnvWithGoal hole
+
+-- Deriving a Convertible instance. Usage
+--   unquoteDecl iName = deriveConvertible iName (quote AgdaTy) (quote HsTy)
+deriveConvertible : Name → Name → Name → R.TC ⊤
+deriveConvertible instName agdaName hsName = initUnquoteWithGoal ⦃ defaultTCOptions ⦄ (agda-sort (lit 0)) do
+  agdaDef ← getDefinition agdaName
+  hsDef   ← getDefinition hsName
+  -- instName ← freshName $ "Convertible" S.++ show hsName
+  instTel , instTy ← instanceType agdaName hsName
+  inst    ← declareDef (iArg instName) (tyView (instTel , instTy))
+  clauses ← instanceClauses agdaName hsName
+  defineFun instName clauses
+  return _
+
+-- Macros providing an alternative interface. Usage
+--   iName : ConvertibleType AgdaTy HsTy
+--   iName = autoConvertible
+-- or
+--   iName = autoConvert AgdaTy
+macro
+  ConvertibleType : Name → Name → Tactic
+  ConvertibleType agdaName hsName = initTac ⦃ defaultTCOptions ⦄ $
+    unifyWithGoal ∘ tyView =<< instanceType agdaName hsName
+
+  autoConvertible : Tactic
+  autoConvertible = initTac ⦃ defaultTCOptions ⦄ $
+    unifyWithGoal =<< patternLambda
+
+  autoConvert : Name → Tactic
+  autoConvert d hole = do
+    hsTyMeta ← R.newMeta `Set
+    R.checkType hole $ quote Convertible ∙⟦ d ∙ ∣ hsTyMeta ⟧
+    hsTy ← solveHsType (d ∙)
+    R.unify hsTyMeta hsTy
+    R.unify hole =<< doPatternLambda hole
diff --git a/docs/agda-spec/src/Foreign/Convertible/DerivingTest.agda b/docs/agda-spec/src/Foreign/Convertible/DerivingTest.agda
new file mode 100644
index 0000000000..43f1ecc23d
--- /dev/null
+++ b/docs/agda-spec/src/Foreign/Convertible/DerivingTest.agda
@@ -0,0 +1,86 @@
+
+module Foreign.Convertible.DerivingTest where
+
+open import Level
+open import MetaPrelude
+open import Meta
+
+import Data.List as L
+import Data.List.NonEmpty as NE
+import Data.String as S
+import Data.Product as P
+
+open import Relation.Nullary
+open import Relation.Nullary.Decidable
+
+open import Reflection.Tactic
+open import Reflection.AST.Term
+open import Reflection.AST.DeBruijn
+import Reflection.TCM as R
+open import Reflection.Utils
+open import Reflection.Utils.TCI
+import Function.Identity.Effectful as Identity
+
+open import Class.DecEq
+open import Class.DecEq
+open import Class.Functor
+open import Class.Monad
+open import Class.MonadTC.Instances
+open import Class.Traversable
+open import Class.Show
+open import Class.MonadReader
+
+open import Foreign.Convertible
+open import Foreign.Convertible.Deriving
+
+-- Tests
+
+open import Data.Maybe.Base
+open import Data.Sum.Base
+
+data HsMaybe (a : Set) : Set where
+  just    : (x : a) → HsMaybe a
+  nothing : HsMaybe a
+
+data HsEither (a b : Set) : Set where
+  left : a → HsEither a b
+  right : b → HsEither a b
+
+-- We should be able to generate this
+ConvertibleMaybe : ∀ {a a'} → ⦃ Convertible a a' ⦄ → Convertible (Maybe a) (HsMaybe a')
+ConvertibleMaybe .to (just x)   = just (to x)
+ConvertibleMaybe .to nothing    = nothing
+ConvertibleMaybe .from (just x) = just (from x)
+ConvertibleMaybe .from nothing  = nothing
+
+-- With deriveConvertible
+unquoteDecl iConvertMaybe  = deriveConvertible iConvertMaybe (quote Maybe) (quote HsMaybe)
+
+-- or with ConvertibleType and autoConvertible
+instance
+  iConvertEither : ConvertibleType _⊎_ HsEither
+  iConvertEither = autoConvertible
+
+instance
+  ConvertibleNat = Convertible-Refl {ℕ}
+
+test : ℕ ⊎ Maybe ℕ → HsEither ℕ (HsMaybe ℕ)
+test = to
+
+_ : test (inj₂ (just 5)) ≡ right (just 5)
+_ = refl
+
+-- There was a problem due to Agda#7182 with record types in parameterised modules.
+
+module Param (A : Set) where
+  record AgdaThing : Set where
+    field theThing : A
+
+record HsThing : Set where
+  field theThing : ℕ
+
+open Param ℕ
+unquoteDecl iConvertThing = deriveConvertible iConvertThing (quote AgdaThing) (quote HsThing)
+
+convThing : Convertible AgdaThing HsThing
+convThing = autoConvertible
diff --git a/docs/agda-spec/src/Foreign/HaskellTypes.agda b/docs/agda-spec/src/Foreign/HaskellTypes.agda
new file mode 100644
index 0000000000..04ce72a1cf
--- /dev/null
+++ b/docs/agda-spec/src/Foreign/HaskellTypes.agda
@@ -0,0 +1,52 @@
+
+module Foreign.HaskellTypes where
+
+open import Level using (Level)
+open import Data.Bool.Base using (Bool)
+open import Data.Nat.Base using (ℕ)
+open import Data.String.Base using (String)
+open import Data.List.Base using (List)
+open import Data.Maybe.Base using (Maybe)
+open import Data.Sum.Base using (_⊎_)
+open import Data.Product.Base using (_×_)
+open import Data.Unit using (⊤)
+
+open import Foreign.Haskell.Pair using (Pair)
+open import Foreign.Haskell.Either using (Either)
+
+private variable
+  l : Level
+  A B : Set l
+
+record HasHsType (A : Set l) : Set₁ where
+  field
+    HsType : Set
+
+HsType : (A : Set l) → ⦃ HasHsType A ⦄ → Set
+HsType _ ⦃ i ⦄ = i .HasHsType.HsType
+
+MkHsType : (A : Set l) (Hs : Set) → HasHsType A
+MkHsType A Hs .HasHsType.HsType = Hs
+
+instance
+
+  iHsTy-ℕ      = MkHsType ℕ ℕ
+  iHsTy-Bool   = MkHsType Bool Bool
+  iHsTy-⊤      = MkHsType ⊤ ⊤
+  iHsTy-String = MkHsType String String
+
+  -- Could make a macro for these kind of congruence instances.
+  iHsTy-List : ⦃ HasHsType A ⦄ → HasHsType (List A)
+  iHsTy-List {A = A} .HasHsType.HsType = List (HsType A)
+
+  iHsTy-Maybe : ⦃ HasHsType A ⦄ → HasHsType (Maybe A)
+  iHsTy-Maybe {A = A} .HasHsType.HsType = Maybe (HsType A)
+
+  iHsTy-Fun : ⦃ HasHsType A ⦄ → ⦃ HasHsType B ⦄ → HasHsType (A → B)
+  iHsTy-Fun {A = A} {B = B} .HasHsType.HsType = HsType A → HsType B
+
+  iHsTy-Sum : ⦃ HasHsType A ⦄ → ⦃ HasHsType B ⦄ → HasHsType (A ⊎ B)
+  iHsTy-Sum {A = A} {B = B} .HasHsType.HsType = Either (HsType A) (HsType B)
+
+  iHsTy-Pair : ⦃ HasHsType A ⦄ → ⦃ HasHsType B ⦄ → HasHsType (A × B)
+  iHsTy-Pair {A = A} {B = B} .HasHsType.HsType = Pair (HsType A) (HsType B)
diff --git a/docs/agda-spec/src/Foreign/HaskellTypes/Deriving.agda b/docs/agda-spec/src/Foreign/HaskellTypes/Deriving.agda
new file mode 100644
index 0000000000..2911f971db
--- /dev/null
+++ b/docs/agda-spec/src/Foreign/HaskellTypes/Deriving.agda
@@ -0,0 +1,362 @@
+
+module Foreign.HaskellTypes.Deriving where
+
+open import Meta hiding (TC; Monad-TC; MonadError-TC)
+
+open import Level using (Level; 0ℓ)
+open import Agda.Builtin.Reflection using (declareData; defineData; pragmaForeign; pragmaCompile;
+                                           solveInstanceConstraints)
+open import Reflection as R hiding (showName; _>>=_; _>>_)
+open import Reflection.AST hiding (showName)
+open import Reflection.AST.DeBruijn
+open import Data.Maybe using (Maybe; nothing; just; fromMaybe; maybe′; _<∣>_)
+open import Data.Unit using (⊤; tt)
+open import Data.Integer.Base using (ℤ)
+open import Data.Sum using (_⊎_; inj₁; inj₂)
+open import Data.String using (String) renaming (_++_ to _&_)
+open import Data.Product hiding (map; zip; zipWith)
+import Data.String as String
+open import Data.Bool
+open import Data.Nat
+open import Data.List hiding (lookup; fromMaybe)
+open import Data.Char using (toUpper; toLower)
+open import Foreign.Haskell
+open import Function
+open import Text.Printf
+
+open import Class.DecEq
+open import Class.Functor
+open import Class.Monad
+open import Class.MonadError
+open import Class.MonadReader
+open import Class.Show
+open import Class.Show.Instances
+open import Class.MonadTC using (TCEnv; dontReduce; defaultTCOptions)
+open import Tactic.Derive.Show using (showName)
+
+open import Reflection.Utils
+open import Reflection.Utils.TCI
+open import Foreign.HaskellTypes
+open import Foreign.Haskell.Pair using (Pair)
+
+{-
+Need to generate:
+  - a data type that can be compiled to a Haskell data type
+  - the corresponding Haskell type (in a FOREIGN pragma)
+  - the COMPILE pragma binding them together
+-}
+
+private variable
+  l : Level
+  A B : Set l
+
+-- TODO: somewhere else
+`Set = agda-sort (Sort.set (quote 0ℓ ∙))
+
+-- * Controlling the names of the generated types
+
+record NameEnv : Set where
+  field
+    customNames : List (Name × String)
+    tName       : Name → Maybe String
+    cName       : Name → Maybe String
+    fName       : Name → Maybe String
+
+private
+  mapHead : (A → A) → List A → List A
+  mapHead f []       = []
+  mapHead f (x ∷ xs) = f x ∷ xs
+
+capitalize : String → String
+capitalize = String.fromList ∘ mapHead toUpper ∘ String.toList
+
+uncapitalize : String → String
+uncapitalize = String.fromList ∘ mapHead toLower ∘ String.toList
+
+private
+  lookup : ⦃ DecEq A ⦄ → A → List (A × B) → Maybe B
+  lookup x xs = proj₂ <$> findᵇ ((x ==_) ∘ proj₁) xs
+
+  lookupEnv : (NameEnv → Name → Maybe String) → NameEnv → Name → Maybe String
+  lookupEnv fn env x = lookup x (NameEnv.customNames env) <∣> fn env x
+
+  lookupTypeName  = lookupEnv NameEnv.tName
+  lookupConName   = lookupEnv NameEnv.cName
+  lookupFieldName = lookupEnv NameEnv.fName
+
+  emptyEnv : NameEnv
+  emptyEnv = record{ customNames = []
+                   ; tName = const nothing
+                   ; cName = const nothing
+                   ; fName = const nothing }
+
+  customName : Name → String → NameEnv
+  customName x s = record emptyEnv { customNames = (x , s) ∷ [] }
+
+onTypes : (String → String) → NameEnv
+onTypes f = record emptyEnv { tName = just ∘ f ∘ showName }
+
+onConstructors : (String → String) → NameEnv
+onConstructors f = record emptyEnv { cName = just ∘ f ∘ showName }
+
+withName : String → NameEnv
+withName t = onTypes (const t)
+
+-- Only use for single constructor types obviously
+withConstructor : String → NameEnv
+withConstructor c = onConstructors (const c)
+
+onFields : (String → String) → NameEnv
+onFields f = record emptyEnv { fName = just ∘ f ∘ showName }
+
+fieldPrefix : String → NameEnv
+fieldPrefix pre = onFields $ (pre String.++_) ∘ capitalize
+
+infixr 5 _•_
+_•_ : NameEnv → NameEnv → NameEnv
+env • env₁ = record
+  { customNames = env.customNames ++ env₁.customNames
+  ; tName       = λ x → env.tName x <∣> env₁.tName x
+  ; cName       = λ x → env.cName x <∣> env₁.cName x
+  ; fName       = λ x → env.fName x <∣> env₁.fName x
+  }
+  where
+    module env  = NameEnv env
+    module env₁ = NameEnv env₁
+
+
+-- * The inner workings
+
+solveHsType : Term → TC Term
+solveHsType tm = do
+  hsTy ← checkType (quote HsType ∙⟦ tm ⟧) `Set
+  solveInstanceConstraints
+  normalise hsTy >>= λ where
+    (def (quote HsType) _) → typeErrorFmt "Failed to solve HsType %t" tm
+    hsTy                   → return hsTy
+
+private
+  debug = debugPrintFmt "tactic.hs-types"
+
+  _‼_ : List A → ℕ → Maybe A
+  []       ‼ i     = nothing
+  (x ∷ xs) ‼ zero  = just x
+  (x ∷ xs) ‼ suc i = xs ‼ i
+
+  specialHsTypes : List (Name × String)
+  specialHsTypes = (quote ⊤      , "()")
+                 ∷ (quote ℕ      , "Integer")
+                 ∷ (quote ℤ      , "Integer")
+                 ∷ (quote Bool   , "Bool")
+                 ∷ (quote List   , "[]")
+                 ∷ (quote Pair   , "(,)")
+                 ∷ (quote Maybe  , "Maybe")
+                 ∷ (quote Either , "Either")
+                 ∷ (quote String , "Data.Text.Text")
+                 ∷ []
+
+  hsTypeName : NameEnv → Name → String
+  hsTypeName env d = fromMaybe (capitalize $ showName d) (lookupTypeName env d)
+
+  freshHsTypeName : NameEnv → Name → TC Name
+  freshHsTypeName env d = freshName (hsTypeName env d)
+
+  hsConName : NameEnv → Name → String
+  hsConName env c = fromMaybe (capitalize $ showName c) (lookupConName env c)
+
+  hsFieldName : NameEnv → Name → String
+  hsFieldName env f = fromMaybe (uncapitalize $ showName f) (lookupFieldName env f)
+
+  freshHsConName : NameEnv → Name → Name → TC Name
+  freshHsConName env tyName c =
+    if showName c == "constructor"
+    then freshName (hsConName env tyName) -- Unnamed record constructor: use type name
+    else freshName (hsConName env c)
+
+  isThis : Name → Term → Bool
+  isThis f (def g _) = f == g
+  isThis _ _ = false
+
+  computeHsType : Name → Name → Term → TC Term
+  computeHsType aThis hThis tm with isThis aThis tm
+  ... | true = pure (hThis ∙)
+  computeHsType aThis hThis (Π[ x ∶ arg (arg-info visible _) a ] b) | false = do
+    dom ← computeHsType aThis hThis a
+    rng ← extendContext x (vArg a) $ computeHsType aThis hThis b
+    pure (vΠ[ x ∶ dom ] rng)
+  computeHsType aThis hThis (Π[ x ∶ a ] b) | false = do
+    ty ← extendContext x a $ computeHsType aThis hThis b
+    just ty′ ← pure (strengthen ty)
+      where nothing → extendContext x a $ typeErrorFmt "%s free in computed HsType %t" x ty
+    pure ty′
+  -- Hack to get recursive occurrences under lists to work
+  computeHsType aThis hThis (def (quote List) (_ ∷ vArg a ∷ [])) | false = do
+    ty ← computeHsType aThis hThis a
+    pure (quote List ∙⟦ ty ⟧)
+  computeHsType _ _ tm | false = do
+    debug 10 "solving HsType %t" tm
+    ty ← solveHsType tm
+    debug 10 "HsType %t = %t" tm ty
+    pure ty
+
+  makeHsCon : NameEnv → Name → Name → Name → TC (Name × Agda.Builtin.Reflection.Quantity × Type)
+  makeHsCon env agdaName hsName c = do
+    debug 10 "Making constructor %q : %q" c agdaName
+    def agdaName' _ ← normalise (def agdaName [])
+      where _ → typeErrorFmt "Failed to compute source type for %q" agdaName
+    hsC  ← freshHsConName env hsName c
+    cTy  ← getType c
+    debug 10 "cTy = %t" cTy
+    hsTy ← computeHsType agdaName' hsName cTy
+    debug 10 "hsTy = %t" hsTy
+    pure (hsC , quantity-ω , hsTy)
+
+  makeHsData : NameEnv → Name → ℕ → List Name → TC Name
+  makeHsData env agdaName nPars constrs = do
+    hsName ← freshHsTypeName env agdaName
+    declareData hsName 0 `Set
+    hsCons ← mapM (makeHsCon env agdaName hsName) constrs
+    defineData hsName hsCons
+    pure hsName
+
+  makeHsType : NameEnv → Name → TC Name
+  makeHsType env d = getDefinition d >>= λ where
+      (data-type pars cs) → makeHsData env d pars cs
+      (record-type c fs)  → makeHsData env d 0 (c ∷ [])
+      _                   → typeErrorFmt "%q is not a data or record type" d
+
+  joinStrings : String → List String → String
+  joinStrings sep ss = foldr _&_ "" $ intersperse sep ss
+
+  compilePragma : Name → List Name → String
+  compilePragma d cs = printf "= data %s (%s)" (showName d) (joinStrings " | " (map showName cs))
+
+  renderHsTypeName : Name → String
+  renderHsTypeName d = fromMaybe ("MAlonzo.Code." String.++ R.showName d) (lookup d specialHsTypes)
+
+  renderHsType : Term → String
+  renderHsArgs : List (Arg Term) → List String
+
+  renderHsType (def (quote List) (_ ∷ vArg a ∷ [])) = printf "[%s]" (renderHsType a)
+  renderHsType (def (quote Pair) (_ ∷ _ ∷ vArg a ∷ vArg b ∷ [])) = printf "(%s, %s)" (renderHsType a) (renderHsType b)
+  renderHsType (def d []) = renderHsTypeName d
+  renderHsType (def d vs) = printf "(%s %s)" (renderHsTypeName d) (joinStrings " " (renderHsArgs vs))
+  renderHsType t = printf "(TODO: renderHsType %s)" (show t)
+
+  renderHsArgs [] = []
+  renderHsArgs (vArg a ∷ as) = renderHsType a ∷ renderHsArgs as
+  renderHsArgs (_ ∷ as) = renderHsArgs as
+
+  foreignPragma : Name → List Name → TC String
+  foreignPragma d cs = do
+    cons ← forM cs λ c → do
+            tel , _ ← viewTy <$> getType c
+            let args = map unAbs tel
+            pure $ printf "%s %s" (showName c) (joinStrings " " $ renderHsArgs args)
+    pure $ printf "data %s = %s\n  deriving (Show, Eq, Generic)"
+                  (showName d) (joinStrings " | " cons)
+
+  -- Record types
+  foreignPragmaRec : NameEnv → Name → List Name → List Name → TC String
+  foreignPragmaRec _ d [] _ = typeErrorFmt "impossible: %q is a record type with no constructors" d
+  foreignPragmaRec env d (c ∷ _) fs = do
+    tel , _ ← viewTy <$> withNormalisation true (getType c)
+    let fNames = map (hsFieldName env) fs
+    let args = map unAbs tel
+        renderField f ty = printf "%s :: %s" f (renderHsType $ unArg ty)
+        con = printf "%s {%s}" (showName c) (joinStrings ", " $ zipWith renderField fNames args)
+    pure $ printf "data %s = %s\n  deriving (Show, Eq, Generic)"
+                  (showName d) con
+
+  hsImports : String
+  hsImports = "import GHC.Generics (Generic)"
+
+  -- Take the name of a simple data type and generate the COMPILE and
+  -- FOREIGN pragmas to bind to Haskell.
+  bindHsType : NameEnv → Name → Name → TC ⊤
+  bindHsType env agdaName hsName = getDefinition hsName >>= λ where
+    (data-type pars cs) → do
+      pragmaForeign "GHC" hsImports
+      pragmaCompile "GHC" hsName $ compilePragma hsName cs
+      getDefinition agdaName >>= λ where
+        (data-type _ _)    → pragmaForeign "GHC" =<< foreignPragma hsName cs
+        (record-type _ fs) → pragmaForeign "GHC" =<< foreignPragmaRec env hsName cs (map unArg fs)
+        _ → typeErrorFmt "%q is not a data or record type" agdaName
+    _ → typeErrorFmt "%q is not a data type (impossible)" hsName
+
+  computeProjections : ℕ → Name → TC (List Term)
+  computeProjections npars c = do
+    argTys , _ ← viewTy <$> getType c
+    let is  = downFrom (length argTys)
+        tel = map (λ where (abs x ty) → x , ty) argTys
+        lhs = vArg (con c (map (λ where (i , abs x (arg info _)) → arg info (var i))
+                               (drop npars (zip is argTys)))) ∷ []
+    return $ map (λ i → pat-lam (clause tel lhs (var i []) ∷ []) []) (drop npars is)
+
+  makeTypeAlias : Name → NameEnv → Term → TC ⊤
+  makeTypeAlias agdaName env hole = do
+    hsTy ← solveHsType (def agdaName [])
+    pragmaForeign "GHC" $ printf "type %s = %s" (hsTypeName env agdaName) (renderHsType hsTy)
+    unify hole (quote return ∙⟦ con (quote tt) [] ⟧)
+
+-- * Exported macros
+
+doAutoHsType : NameEnv → Name → Term → TC Term
+doAutoHsType env d hole = do
+  checkType hole (quote HasHsType ∙⟦ d ∙ ⟧)
+  hs ← makeHsType env d
+  debug 50 "  HsType %q = %q" d hs
+  bindHsType env d hs
+  unify hole (`λ⟦ proj (quote HasHsType.HsType) ⇒ hs ∙ ⟧)
+  pure (hs ∙)
+
+macro
+  autoHsType : Name → Term → TC ⊤
+  autoHsType d hole = _ <$ doAutoHsType emptyEnv d hole
+
+  infix 0 autoHsType_⊣_
+  autoHsType_⊣_ : Name → NameEnv → Term → TC ⊤
+  autoHsType_⊣_ d env hole = _ <$ doAutoHsType env d hole
+
+  infix 9 _↦_
+  _↦_ : Name → String → Term → TC ⊤
+  x ↦ s = unify (quote customName ∙⟦ lit (name x) ∣ lit (string s) ⟧)
+
+  -- Generate a Haskell type synonym for the HsType of the given type
+  -- Usage `unquoteDecl = do hsTypeSynonym Foo; hsTypeSynonym Bar`
+  hsTypeAlias : Name → Term → TC ⊤
+  hsTypeAlias agdaName = makeTypeAlias agdaName emptyEnv
+
+  -- The only NameEnv that's useful here is `withName`.
+  hsTypeAlias_⊣_ : Name → NameEnv → Term → TC ⊤
+  hsTypeAlias agdaName ⊣ env = makeTypeAlias agdaName env
+
+  -- * Macros for constructing and deconstructing generated types
+
+  hsCon : Term → ℕ → Term → TC ⊤
+  hsCon agdaTy i hole = do
+    hsTy@(def hsName _) ← solveHsType agdaTy
+      where _ → typeErrorFmt "Failed to compute HsType of %t" agdaTy
+    cs ← getDefinition hsName >>= λ where
+      (data-type _ cs)  → return cs
+      _ → typeErrorFmt "Expected HsType %t to be a data type, but got %t" agdaTy hsTy
+    c ← maybe′ return  (typeErrorFmt "%q has only %u constructors" hsName (length cs)) (cs ‼ i)
+    unify hole (con c [])
+
+  hsProj : Term → ℕ → Term → TC ⊤
+  hsProj agdaTy i hole = do
+    hsTy@(def hsName _) ← solveHsType agdaTy
+      where _ → typeErrorFmt "Failed to compute HsType of %t" agdaTy
+    prjs ← getDefinition hsName >>= λ where
+      (data-type npars (c ∷ [])) → computeProjections npars c
+      _ → typeErrorFmt "Expected HsType %t to be a single constructor data type, but got %t" agdaTy hsTy
+    prj ← maybe′ return (typeErrorFmt "%q has only %u fields" hsName (length prjs)) (prjs ‼ i)
+    target ← newMeta `Set
+    checkType hole (pi (vArg hsTy) (abs "_" target))
+    unify hole prj
+
+  hsTyName : Term → Term → TC ⊤
+  hsTyName agdaTy hole = do
+    hsTy@(def hsName _) ← solveHsType agdaTy
+      where _ → typeErrorFmt "Failed to compute HsType of %t" agdaTy
+    unify hole (lit (name hsName))
diff --git a/docs/agda-spec/src/Makefile b/docs/agda-spec/src/Makefile
index 2de9935429..d2fe72f313 100644
--- a/docs/agda-spec/src/Makefile
+++ b/docs/agda-spec/src/Makefile
@@ -1,3 +1,4 @@
+# Constants
 PDF_NAME=consensus-spec
 AGDA?=agda
 AGDA_RUN=$(AGDA) --transliterate
@@ -9,14 +10,18 @@ PRE=$(addprefix $(LATEX_DIR)/,\
 PDF_DIR=$(OUT_DIR)/pdfs
 LIB_NAME=Ledger
 INTERFACE_LIB_NAME=InterfaceLibrary
+HS_DIR=$(OUT_DIR)/haskell
+MALONZO_DIR=MAlonzo/Code
+CABAL_TEST=cabal run test
 
 # Agda -> LaTeX -> PDF
 latexFiles=$(patsubst %.lagda, $(LATEX_DIR)/%.tex,\
              $(shell find . -name '*.lagda' | sed 's|\.\/||g'))
 $(latexFiles): $(LATEX_DIR)/%.tex: %.lagda
 	@echo "Compiling $<"
-	$(AGDA_RUN) --latex --latex-dir=$(LATEX_DIR) $< # --only-scope-checking
-define latexToPdf =
+	$(AGDA_RUN) --latex --latex-dir=$(LATEX_DIR) $<
+
+define latexToPdf
     @echo "Generating $@"
     $(eval PDF=$(notdir $@))
     mkdir -p $(dir $@)
@@ -27,8 +32,34 @@ endef
 $(PDF_DIR)/$(PDF_NAME).pdf: $(LATEX_DIR)/Spec/PDF.tex $(latexFiles) $(PRE)
 	$(latexToPdf)
 
+# Agda -> Haskell
+define agdaToHs
+    @echo "Generating $@"
+    $(eval CABAL_FILE=$(1).cabal)
+    $(eval HS_DIST=$(HS_DIR)/Spec)
+    mkdir -p $(HS_DIST)
+    cp -r Spec/hs-src/* $(HS_DIST)/
+    cp Spec/hs-src/$(CABAL_FILE) $(HS_DIST)/
+    $(AGDA_RUN) -c --ghc-dont-call-ghc --compile-dir $(HS_DIST) $<
+    find $(HS_DIST)/MAlonzo -name "*.hs" -print\
+      | sed "s#^$(HS_DIST)/#        #;s#\.hs##;s#/#.#g"\
+      >> $(HS_DIST)/$(CABAL_FILE)
+endef
+HS_CONSENSUS=$(HS_DIR)/Consensus/$(MALONZO_DIR)/Spec/Foreign/HSConsensus.hs
+$(HS_CONSENSUS): Spec/Foreign/HSConsensus.agda
+	$(call agdaToHs,cardano-consensus-executable-spec)
+
 # User commands
-.PHONY: default clean docs
+.PHONY: default clean docs hs hsTest
+
+consensus.hs: $(HS_CONSENSUS)
+
+hs: consensus.hs
+
+consensus.hsTest: $(HS_CONSENSUS)
+	cd $(HS_DIR)/Spec && $(CABAL_TEST)
+
+hsTest: consensus.hsTest
 
 docs: $(PDF_DIR)/$(PDF_NAME).pdf
 
diff --git a/docs/agda-spec/src/Spec/Foreign/ExternalFunctions.agda b/docs/agda-spec/src/Spec/Foreign/ExternalFunctions.agda
new file mode 100644
index 0000000000..542d2ee5c9
--- /dev/null
+++ b/docs/agda-spec/src/Spec/Foreign/ExternalFunctions.agda
@@ -0,0 +1,15 @@
+module Spec.Foreign.ExternalFunctions where -- TODO: Complete
+
+open import Ledger.Prelude
+open import Foreign.HaskellTypes.Deriving
+
+record ExternalFunctions : Set where
+  field extDummy : ℕ → Bool
+{-# FOREIGN GHC
+  data ExternalFunctions = MkExternalFunctions { extDummy :: Integer -> Bool }
+#-}
+{-# COMPILE GHC ExternalFunctions = data ExternalFunctions (MkExternalFunctions) #-}
+
+dummyExternalFunctions : ExternalFunctions
+dummyExternalFunctions = record { extDummy = λ x → true }
+{-# COMPILE GHC dummyExternalFunctions as dummyExternalFunctions #-}
diff --git a/docs/agda-spec/src/Spec/Foreign/HSConsensus.agda b/docs/agda-spec/src/Spec/Foreign/HSConsensus.agda
new file mode 100644
index 0000000000..add652d055
--- /dev/null
+++ b/docs/agda-spec/src/Spec/Foreign/HSConsensus.agda
@@ -0,0 +1,4 @@
+module Spec.Foreign.HSConsensus where
+
+open import Spec.Foreign.HSConsensus.TickNonce public
+
diff --git a/docs/agda-spec/src/Spec/Foreign/HSConsensus/BaseTypes.agda b/docs/agda-spec/src/Spec/Foreign/HSConsensus/BaseTypes.agda
new file mode 100644
index 0000000000..f47c6b36f4
--- /dev/null
+++ b/docs/agda-spec/src/Spec/Foreign/HSConsensus/BaseTypes.agda
@@ -0,0 +1,25 @@
+module Spec.Foreign.HSConsensus.BaseTypes where
+
+open import Spec.Foreign.ExternalFunctions
+open import Spec.Foreign.HSConsensus.Core public
+import Spec.Foreign.HSTypes as F
+
+instance -- TODO: Complete
+  iConvNat    = Convertible-Refl {ℕ}
+  iConvString = Convertible-Refl {String}
+  iConvBool   = Convertible-Refl {Bool}
+
+instance -- TODO: Complete
+
+  -- * ComputationResult
+
+  HsTy-ComputationResult : ∀ {l} {Err} {A : Type l}
+                           → ⦃ HasHsType Err ⦄ → ⦃ HasHsType A ⦄
+                           → HasHsType (ComputationResult Err A)
+  HsTy-ComputationResult {Err = Err} {A} = MkHsType _ (F.ComputationResult (HsType Err) (HsType A))
+
+  Conv-ComputationResult : ConvertibleType ComputationResult F.ComputationResult
+  Conv-ComputationResult = autoConvertible
+
+open ExternalStructures dummyExternalFunctions -- TODO: Complete
+  public
diff --git a/docs/agda-spec/src/Spec/Foreign/HSConsensus/Core.agda b/docs/agda-spec/src/Spec/Foreign/HSConsensus/Core.agda
new file mode 100644
index 0000000000..2032d57c9b
--- /dev/null
+++ b/docs/agda-spec/src/Spec/Foreign/HSConsensus/Core.agda
@@ -0,0 +1,53 @@
+{-# OPTIONS --allow-unsolved-metas #-} -- TODO: Remove when structs are fully implemented
+
+open import Spec.Foreign.ExternalFunctions
+
+module Spec.Foreign.HSConsensus.Core where
+
+open import Ledger.Prelude hiding (ε) renaming (fromList to fromListˢ) public
+open Computational public
+
+open import Foreign.Convertible           public
+open import Foreign.Convertible.Deriving  public
+open import Foreign.HaskellTypes          public
+open import Foreign.HaskellTypes.Deriving public
+
+open import Ledger.Crypto
+open import Ledger.Types.Epoch
+
+module _ {A : Type} ⦃ _ : DecEq A ⦄ ⦃ _ : Show A ⦄ where instance
+  ∀Hashable : Hashable A A
+  ∀Hashable = λ where .hash → id
+
+  ∀isHashableSet : isHashableSet A
+  ∀isHashableSet = mkIsHashableSet A
+
+instance
+  Hashable-⊤ : Hashable ⊤ ℕ
+  Hashable-⊤ = λ where .hash tt → 0
+
+module Implementation where
+
+  -- TODO: Complete
+
+module ExternalStructures (externalFunctions : ExternalFunctions) where
+  HSGlobalConstants = GlobalConstants ∋ record {Implementation}
+  instance
+    HSEpochStructure = EpochStructure ∋ ℕEpochStructure HSGlobalConstants
+
+    -- TODO: Complete
+    HSCrypto : Crypto
+    HSCrypto = record {}
+
+    open import Spec.BaseTypes HSCrypto
+
+    -- TODO: Complete
+    HSNonces : Nonces
+    HSNonces = record
+      { Nonce = ℕ
+      ; _⋆_ = _+_
+      }
+
+    open EpochStructure HSEpochStructure public
+    open Crypto HSCrypto public
+    open Nonces HSNonces public
diff --git a/docs/agda-spec/src/Spec/Foreign/HSConsensus/TickNonce.agda b/docs/agda-spec/src/Spec/Foreign/HSConsensus/TickNonce.agda
new file mode 100644
index 0000000000..03b349283b
--- /dev/null
+++ b/docs/agda-spec/src/Spec/Foreign/HSConsensus/TickNonce.agda
@@ -0,0 +1,19 @@
+module Spec.Foreign.HSConsensus.TickNonce where
+
+open import Spec.Foreign.HSConsensus.BaseTypes
+open import Spec.TickNonce it it it
+
+open import Spec.TickNonce.Properties it it it using (Computational-TICKN)
+
+instance
+
+  HsTy-TickNonceEnv = autoHsType TickNonceEnv ⊣ withConstructor "MkTickNonceEnv"
+  Conv-TickNonceEnv = autoConvert TickNonceEnv
+
+  HsTy-TickNonceState = autoHsType TickNonceState ⊣ withConstructor "MkTickNonceState"
+  Conv-TickNonceState = autoConvert TickNonceState
+
+tickn-step : HsType (TickNonceEnv → TickNonceState → Bool → ComputationResult String TickNonceState)
+tickn-step = to (compute Computational-TICKN)
+
+{-# COMPILE GHC tickn-step as ticknStep #-}
diff --git a/docs/agda-spec/src/Spec/Foreign/HSTypes.agda b/docs/agda-spec/src/Spec/Foreign/HSTypes.agda
new file mode 100644
index 0000000000..b4990a88b3
--- /dev/null
+++ b/docs/agda-spec/src/Spec/Foreign/HSTypes.agda
@@ -0,0 +1,42 @@
+module Spec.Foreign.HSTypes where
+
+{-# FOREIGN GHC
+  {-# LANGUAGE DeriveGeneric #-}
+  {-# LANGUAGE DeriveFunctor #-}
+#-}
+
+open import Prelude
+
+open import Foreign.Haskell
+open import Foreign.Haskell.Coerce
+open import Foreign.Haskell.Either
+open import Data.Rational.Base
+
+{-# FOREIGN GHC
+  import GHC.Generics (Generic)
+  import Data.Void (Void)
+  import Prelude hiding (Rational)
+  import GHC.Real (Ratio(..))
+#-}
+
+-- * ComputationResult
+
+data ComputationResult E A : Type where
+  Success : A → ComputationResult E A
+  Failure : E → ComputationResult E A
+
+{-# FOREIGN GHC
+  data ComputationResult e a = Success a | Failure e
+    deriving (Functor, Eq, Show, Generic)
+
+  instance Applicative (ComputationResult e) where
+    pure = Success
+    (Success f) <*> x = f <$> x
+    (Failure e) <*> _ = Failure e
+
+  instance Monad (ComputationResult e) where
+    return = pure
+    (Success a) >>= m = m a
+    (Failure e) >>= _ = Failure e
+#-}
+{-# COMPILE GHC ComputationResult = data ComputationResult (Success | Failure) #-}
diff --git a/docs/agda-spec/src/Spec/hs-src/Lib.hs b/docs/agda-spec/src/Spec/hs-src/Lib.hs
new file mode 100644
index 0000000000..5097326e53
--- /dev/null
+++ b/docs/agda-spec/src/Spec/hs-src/Lib.hs
@@ -0,0 +1,11 @@
+module Lib
+  ( module X
+  , module Lib
+  ) where
+
+import MAlonzo.Code.Spec.Foreign.HSTypes               as X
+  (ComputationResult(..)) -- TODO: Complete
+import MAlonzo.Code.Spec.Foreign.HSConsensus.TickNonce as X
+  (TickNonceEnv(..), TickNonceState(..), ticknStep)
+import MAlonzo.Code.Spec.Foreign.ExternalFunctions     as X
+  (ExternalFunctions(..), dummyExternalFunctions)
diff --git a/docs/agda-spec/src/Spec/hs-src/cabal.project b/docs/agda-spec/src/Spec/hs-src/cabal.project
new file mode 100644
index 0000000000..dfb30afe59
--- /dev/null
+++ b/docs/agda-spec/src/Spec/hs-src/cabal.project
@@ -0,0 +1,2 @@
+-- TODO: Remove this file when code is properly integrated to the existing setup
+packages: .
diff --git a/docs/agda-spec/src/Spec/hs-src/cardano-consensus-executable-spec.cabal b/docs/agda-spec/src/Spec/hs-src/cardano-consensus-executable-spec.cabal
new file mode 100644
index 0000000000..ddba40b272
--- /dev/null
+++ b/docs/agda-spec/src/Spec/hs-src/cardano-consensus-executable-spec.cabal
@@ -0,0 +1,57 @@
+cabal-version:      3.12
+name:               cardano-consensus-executable-spec
+version:            0.1.0.0
+synopsis:
+
+-- A longer description of the package.
+-- description:
+homepage:
+
+-- A URL where users can report bugs.
+-- bug-reports:
+license:            NONE
+author:             Javier Díaz
+maintainer:         javier.diaz@iohk.io
+
+-- A copyright notice.
+-- copyright:
+-- category:
+
+common globalOptions
+    default-language: Haskell2010
+    build-depends: base
+    default-extensions:
+        PolyKinds EmptyDataDecls EmptyCase ExistentialQuantification
+        ScopedTypeVariables NoMonomorphismRestriction RankNTypes
+        PatternSynonyms DeriveGeneric
+    ghc-options:
+        -Wno-overlapping-patterns
+
+test-suite test
+    import: globalOptions
+    hs-source-dirs: test
+    main-is: Spec.hs
+    other-modules:
+        TickNonceSpec
+    build-depends:
+        cardano-consensus-executable-spec,
+        hspec,
+        HUnit,
+        text
+    build-tool-depends: hspec-discover:hspec-discover
+    type: exitcode-stdio-1.0
+    ghc-options:
+        -Wall
+        -threaded -rtsopts -with-rtsopts=-N
+        -fno-warn-type-defaults
+
+library
+    import: globalOptions
+    hs-source-dirs: .
+    exposed-modules:
+        Lib
+    build-depends:
+        text,
+        ieee
+-- This will be generated automatically when building with nix
+    other-modules:
diff --git a/docs/agda-spec/src/Spec/hs-src/test/Spec.hs b/docs/agda-spec/src/Spec/hs-src/test/Spec.hs
new file mode 100644
index 0000000000..a824f8c30c
--- /dev/null
+++ b/docs/agda-spec/src/Spec/hs-src/test/Spec.hs
@@ -0,0 +1 @@
+{-# OPTIONS_GHC -F -pgmF hspec-discover #-}
diff --git a/docs/agda-spec/src/Spec/hs-src/test/TickNonceSpec.hs b/docs/agda-spec/src/Spec/hs-src/test/TickNonceSpec.hs
new file mode 100644
index 0000000000..c13f7566b3
--- /dev/null
+++ b/docs/agda-spec/src/Spec/hs-src/test/TickNonceSpec.hs
@@ -0,0 +1,30 @@
+{-# LANGUAGE StandaloneDeriving #-}
+{-# OPTIONS -Wno-orphans #-}
+module TickNonceSpec (spec) where
+
+import Data.Text
+
+import Test.Hspec ( Spec, describe, it )
+import Test.HUnit ( (@?=) )
+
+import Lib
+
+initEnv :: TickNonceEnv
+initEnv = MkTickNonceEnv { ηc = 2, ηph = 5 }
+
+initState :: TickNonceState
+initState = MkTickNonceState { η₀ = 3, ηh = 4 }
+
+testTickNonceStepFalse :: ComputationResult Text TickNonceState
+testTickNonceStepFalse = ticknStep initEnv initState False
+
+testTickNonceStepTrue :: ComputationResult Text TickNonceState
+testTickNonceStepTrue = ticknStep initEnv initState True
+
+spec :: Spec
+spec = do
+  describe "ticknStep" $ do
+    it "ticknStep results in the expected state with signal False" $
+      testTickNonceStepFalse @?= Success (MkTickNonceState { η₀ = 3, ηh = 4 })
+    it "ticknStep results in the expected state with signal True" $
+      testTickNonceStepTrue @?= Success (MkTickNonceState { η₀ = 6, ηh = 5 })
diff --git a/docs/agda-spec/src/Tactic/Substitute.agda b/docs/agda-spec/src/Tactic/Substitute.agda
new file mode 100644
index 0000000000..f54efdd92d
--- /dev/null
+++ b/docs/agda-spec/src/Tactic/Substitute.agda
@@ -0,0 +1,47 @@
+
+module Tactic.Substitute where
+
+open import MetaPrelude
+open import Meta
+
+-- There aren't any nice substitution functions (that I can find) in the standard library or
+-- stdlib-meta. This one is cheating and only works for closed terms at either never gets
+-- applied, or where we can safely throw away the arguments (e.g. `unknown`).
+
+Subst : Set → Set
+Subst A = ℕ → Term → A → A
+
+substTerm : Subst Term
+substArgs : Subst (Args Term)
+substArg  : Subst (Arg Term)
+substAbs  : Subst (Abs Term)
+substSort : Subst Sort
+
+substTerm x s (var y args) =
+  case compare x y of λ where
+    (less _ _)    → var (y ∸ 1) (substArgs x s args)
+    (equal _)     → s  -- cheating and dropping the args!
+    (greater _ _) → var y (substArgs x s args)
+substTerm x s (con c args) = con c (substArgs x s args)
+substTerm x s (def f args) = def f (substArgs x s args)
+substTerm x s (lam v t) = lam v (substAbs x s t)
+substTerm x s (pat-lam cs args₁) = unknown  -- ignoring for now
+substTerm x s (pi a b) = pi (substArg x s a) (substAbs x s b)
+substTerm x s (agda-sort s₁) = agda-sort (substSort x s s₁)
+substTerm x s (lit l) = lit l
+substTerm x s (meta m args) = meta m (substArgs x s args)
+substTerm x s unknown = unknown
+
+substArgs x s [] = []
+substArgs x s (a ∷ as) = substArg x s a ∷ substArgs x s as
+
+substArg x s (arg i t) = arg i (substTerm x s t)
+
+substAbs x s (abs z t) = abs z (substTerm (ℕ.suc x) s t)
+
+substSort x s (set t) = set (substTerm x s t)
+substSort x s (lit n) = lit n
+substSort x s (prop t) = prop (substTerm x s t)
+substSort x s (propLit n) = propLit n
+substSort x s (inf n) = inf n
+substSort x s unknown = unknown
diff --git a/docs/agda-spec/src/formal-ledger.agda-lib b/docs/agda-spec/src/formal-consensus.agda-lib
similarity index 69%
rename from docs/agda-spec/src/formal-ledger.agda-lib
rename to docs/agda-spec/src/formal-consensus.agda-lib
index 0176be2b09..2ec75a2da4 100644
--- a/docs/agda-spec/src/formal-ledger.agda-lib
+++ b/docs/agda-spec/src/formal-consensus.agda-lib
@@ -1,6 +1,6 @@
-name: formal-ledger
+name: formal-consensus
 depend:
   standard-library
   standard-library-classes
   standard-library-meta
-include: .
\ No newline at end of file
+include: .