Remove ADRs from user documentation

doc/docusaurus/docs/adr/adr-index.md → doc/adr/README.md

@@ -1,11 +1,7 @@
----
-sidebar_position: 5
----
-
 # Architectural decision records
 
-We document our architectural and design decisions for all of our components. 
-To do that, there is a practice called architectural decision records (ADR), that we can integrate into our workflow. 
+We document our architectural and design decisions for all of our components.
+To do that, there is a practice called architectural decision records (ADR), that we can integrate into our workflow.
 An ADR is a document that captures an important architectural decision made along with its context and consequences.
 
 The goals are:
@@ -22,4 +18,3 @@ The general process for creating an ADR is:
     `[<ADR_NUMBER\>-<TITLE>.md]` in the directory `[doc/adr]`
 3. Adding the ADR in the table of contents tree of the documentation
 4. Committing and pushing to the repository.
-

doc/docusaurus/docs/adr/adr1.md → doc/adr/adr1.md

@@ -1,7 +1,3 @@
----
-sidebar_position: 10
----
-
 # ADR 1: Record architectural decisions
 
 Date: 2022-06-08
@@ -16,7 +12,7 @@ Accepted
 
 ## Context
 
-We are in search for a means to document our architectural and design decisions for all of our components. 
+We are in search for a means to document our architectural and design decisions for all of our components.
 To do that, there is a practice called architectural decision records (ADR) that we can
 integrate into our workflow.
 
@@ -36,7 +32,7 @@ For each decision, it is important to consider the following factors:
 
 - We will use ADRs to document, propose, and discuss any important or significant architectural and design decisions.
 - The ADR format will follow the format described in the [Implications](#implications) section.
-- We will follow the convention of storing those ADRs as rST or Markdown formatted documents stored under the [docs/adr] directory, as exemplified in Nat Pryce's [adr-tools](https://github.com/npryce/adr-tools). 
+- We will follow the convention of storing those ADRs as rST or Markdown formatted documents stored under the [docs/adr] directory, as exemplified in Nat Pryce's [adr-tools](https://github.com/npryce/adr-tools).
 This does not imply that we will be using [adr-tools] itself, as we might diverge from the proposed structure.
 - We will keep rejected ADRs.
 - We will strive, if possible, to create an ADR as early as possible in relation to the actual implementation.
@@ -95,7 +91,7 @@ Explain alternatives with sufficient detail to judge their suitability; refer to
 
 ### Implications (or consequences)
 
-Describe the decision’s implications. For example, it may: 
+Describe the decision’s implications. For example, it may:
 
 * Introduce a need to make other decisions
 * Create new requirements

doc/docusaurus/docs/adr/adr2.md → doc/adr/adr2.md

@@ -1,7 +1,3 @@
----
-sidebar_position: 15
----
-
 # ADR 2: Steppable CEK machine
 
 Date: 2022-10
@@ -20,30 +16,30 @@ Proposed
 
 In order to have a minimal viable product of a debugger for Plutus, we need a CEK machine that will give us more information for debugging than our current one.
 
-In order to provide debugging information for each evaluation step, we need a steppable CEK machine. 
-Implementing the steppable CEK machine is a non-trivial task and involves some design decisions. 
-One decision to make is about whether we can share the code between the production and the debugging machine. 
-That is not the scope of this ADR. 
+In order to provide debugging information for each evaluation step, we need a steppable CEK machine.
+Implementing the steppable CEK machine is a non-trivial task and involves some design decisions.
+One decision to make is about whether we can share the code between the production and the debugging machine.
+That is not the scope of this ADR.
 See the next ADR for that.
 
-This ADR proposes a design for an implementation of a steppable CEK machine. 
-Of course, this doesn't mean that this is the final decision. 
-This means that the next step for us is to prototype the machine in this way - which we have reasons to believe will go well. 
+This ADR proposes a design for an implementation of a steppable CEK machine.
+Of course, this doesn't mean that this is the final decision.
+This means that the next step for us is to prototype the machine in this way - which we have reasons to believe will go well.
 We may adjust our proposed approach depending on how the prototyping goes.
 
 ## Decision
 
 This section describes the proposed implementation of the debugging machine.
 
-We first **abstract out the computation to "steps"** on our current machine. 
+We first **abstract out the computation to "steps"** on our current machine.
 We then **implement a coroutine system** to add the debugging functionalities.
 
 ### Abstracting out the computation to "steps"
 
 This abstraction has been implemented in [PR#4909](https://github.com/IntersectMBO/plutus/pull/4909/).
 
-The current machine inlined the steps. 
-We separate each steps into separate functions. 
+The current machine inlined the steps.
+We separate each steps into separate functions.
 They all return a `CekState`:
 
 ```haskell
@@ -55,7 +51,7 @@ data CekState uni fun =
     -- evaluation finished
     | Terminating (Term NamedDeBruijn uni fun ())
 
-data Closure uni fun = 
+data Closure uni fun =
   Closure (Term NamedDeBruijn uni fun ()) (CekValEnv uni fun)
 ```
 
@@ -71,7 +67,7 @@ computeCekStep
     -> CekM uni fun s (CekState uni fun)
 ```
 
-Similarly for the returning step (`returnCekStep`). 
+Similarly for the returning step (`returnCekStep`).
 Then we link up all the steps with `continue`, and the machine behaves very similar to our current one:
 
 ```haskell
@@ -90,8 +86,8 @@ continue (Terminating term) = pure term
 
 ### Coroutines in Haskell
 
-The next step is to add debugging capabilities between each step. 
-To do so, we implement it as a *coroutine system*. 
+The next step is to add debugging capabilities between each step.
+To do so, we implement it as a *coroutine system*.
 A detailed introduction to coroutines in Haskell can be found in [Coroutine Pipelines](https://themonadreader.files.wordpress.com/2011/10/issue19.pdf).
 This section gives a brief summary.
 
@@ -127,9 +123,9 @@ Multiple suspension functors and computations can be composed using [coproducts]
 
 The base monad `m` is the monad the machine computation runs in.
 The machine computation interprets each request into an `m` action.
-It is essentially a natural transformation from the suspension functor to `m`. 
-This `m` will replace our current monad `CekM`. 
-Although we can actually just use `CekM` in the steppable CEK machine when we add `IO` capabilities for debugging. 
+It is essentially a natural transformation from the suspension functor to `m`.
+This `m` will replace our current monad `CekM`.
+Although we can actually just use `CekM` in the steppable CEK machine when we add `IO` capabilities for debugging.
 This is because we can convert it to/from `IO` via `unsafeSTToIO` and `unsafeIOToST`.
 
 Suppose we define a type `SteppableCekM a` as our base monad `m`.
@@ -143,7 +139,7 @@ handle = \case
   InputF k     -> input >>= pure . k
 ```
 
-where `step state`, `log text` and `input` return `SteppableCekM` actions. 
+where `step state`, `log text` and `input` return `SteppableCekM` actions.
 `step` will likely correspond to `computeCekStep` and `returnCekStep` depending on the states.
 
 We can then use `handle` to construct a monad morphism, interpreting the user computation (a `FreeT` structure) into a `SteppableCekM` action:
@@ -195,9 +191,9 @@ enterDebug termToDebug = do
 
 ### Argument: coroutine system
 
-Why a coroutine system? 
-In short, structuring the code this way will ease our future work. 
-Some of the advantages are mentioned above already. 
+Why a coroutine system?
+In short, structuring the code this way will ease our future work.
+Some of the advantages are mentioned above already.
 Here is a summary:
 
 - The debugger is naturally a coroutine, where one routine is the user and the other is the CEK machine, and they take turns to suspend and pass data and control to each other in a debugging session. The literature has contributed a good way to design/implement a coroutine. It makes sense to implement a well studied design.
@@ -207,7 +203,7 @@ Here is a summary:
 
 ## Implications
 
-In summary, we proposed to implement the debugging machine as a coroutine system with 'steps'. 
+In summary, we proposed to implement the debugging machine as a coroutine system with 'steps'.
 This implies that:
 
 - We have to maintain the CEK machine (eg, we need to check its conformance)

doc/docusaurus/docs/adr/adr3.md → doc/adr/adr3.md

@@ -1,14 +1,10 @@
----
-sidebar_position: 20
----
-
 # ADR 3: Sharing code between the production and debugging CEK machine
 
 Date: 2022-10
 
 ## Authors
 
-[Marty Stumpf](mailto:marty.stumpf@iohk.io) 
+[Marty Stumpf](mailto:marty.stumpf@iohk.io)
 
 ## Status
 
@@ -18,14 +14,14 @@ Draft
 
 In order to have a minimal viable product of a debugger for Plutus, we need a CEK machine that will give us more information for debugging than our current one.
 
-One of the first decision we need to make is: should the debugging machine be a separate one? 
+One of the first decision we need to make is: should the debugging machine be a separate one?
 The debugging machine needs to satisfy these requirements:
 
 - We must not compromise the performance of the production machine, and
 - The debugging machine must behave the same as the production machine.
 
-There are tradeoffs between these two requirements. 
-If we have a separate machine, the performance of the production machine will be untouched. 
+There are tradeoffs between these two requirements.
+If we have a separate machine, the performance of the production machine will be untouched.
 But there is more scope for us to make mistakes with the new machine.
 
 However, if we share code between the two machines, the performance of the production machine may be compromised.
@@ -34,9 +30,9 @@ This ADR proposes an approach for the two machines to share code while not compr
 
 ## Decision: Polymorphic compute/return steps
 
-As long as the debugging machine has the same type, we can alter `computeCek`/`returnCek` to be polymorphic over a type-level `Bool` specifying if we’re in debug mode or not. 
-Then we demote it to the term level in the definition of `computeCek`/`returnCek` and branch on the `Bool` thus implementing different logic depending on whether we're in debug mode or not. 
-This promotion to the type level allows us to statically instantiate the `Bool` in an instance and thus make GHC compile the whole worker of the CEK machine twice: once in debug mode and once in production mode. 
+As long as the debugging machine has the same type, we can alter `computeCek`/`returnCek` to be polymorphic over a type-level `Bool` specifying if we’re in debug mode or not.
+Then we demote it to the term level in the definition of `computeCek`/`returnCek` and branch on the `Bool` thus implementing different logic depending on whether we're in debug mode or not.
+This promotion to the type level allows us to statically instantiate the `Bool` in an instance and thus make GHC compile the whole worker of the CEK machine twice: once in debug mode and once in production mode.
 Theoretically, GHC will take care to remove all the dead debug code when in production mode.
 
 ### Detailed description with code snippets
@@ -52,14 +48,14 @@ data CekState uni fun =
     -- evaluation finished
     | Terminating (Term NamedDeBruijn uni fun ())
 
-data Closure uni fun = 
+data Closure uni fun =
   Closure (Term NamedDeBruijn uni fun ()) (CekValEnv uni fun)
 ```
 
 We enter either modes via `enterComputeCek`, which takes an extra `Bool` than our current implementation, to indicate whether we are in debugging mode or not:
 
 ```haskell
-enterComputeCek 
+enterComputeCek
     :: forall uni fun s
     . (Ix fun, PrettyUni uni fun, GivenCekReqs uni fun s)
     => Bool
@@ -68,9 +64,9 @@ enterComputeCek
     -> CekM uni fun s (CekState uni fun)
 enterComputeCek debug ctx (Closure term env) =
     -- The initial step is always computing with zero budget, empty context and environment.
-    -- `computeCekStep` matches on the `term` and calls `computeCek` or `returnCek` depending on the clause. 
+    -- `computeCekStep` matches on the `term` and calls `computeCek` or `returnCek` depending on the clause.
     computeCekStep (toWordArray 0) NoFrame (Closure term Env.empty) where
-    
+
     computeCek
         :: WordArray -- for costing
         -> Context uni fun
@@ -80,37 +76,37 @@ enterComputeCek debug ctx (Closure term env) =
     {-# NOINLINE computeCek #-}  -- Making sure the `if` is only evaluated once.
 
     -- in debugging mode, immediately returns the current `CekState` and halts execution. Debugging mode details to be worked out.
-    computeCekDebug 
+    computeCekDebug
         :: WordArray
         -> Context uni fun
         -> Closure uni fun
-        -> CekM uni fun s (CekState uni fun) 
-    computeCekDebug budget ctx (Closure term env) = 
+        -> CekM uni fun s (CekState uni fun)
+    computeCekDebug budget ctx (Closure term env) =
         pure $ Computing budget ctx (Closure term env)
 
-    -- In production mode, `computeCekStep` matches on the term and calls `computeCek` or `returnCek` on a subterm. 
+    -- In production mode, `computeCekStep` matches on the term and calls `computeCek` or `returnCek` on a subterm.
     -- In production mode, `computeCek` calls the original `computeCekStep`, i.e. in production mode `computeCekStep` calls itself through the thin `computeCek` wrapper thus achieving recursion and replicating the old behavior of the CEK machine.
-    computeCekStep 
+    computeCekStep
         :: WordArray
         -> Context uni fun
         -> Closure uni fun
         -> CekM uni fun s (CekState uni fun) -- the return type is `CekState` instead of a term.
     computeCekStep unbudgetedSteps ctx (Closure (Force _ body) env) = do -- exactly like in current prod
         !unbudgetedSteps' <- stepAndMaybeSpend BForce unbudgetedSteps -- update costs
         computeCek unbudgetedSteps' (FrameForce ctx) (Closure body env) -- compute again with updated costs and ctx
-    <other_clauses> -- there's a lot of code in here! Some clauses call `returnCek`, some `computeCek`, achieving recursive calling similar to our current implementation. 
-    
+    <other_clauses> -- there's a lot of code in here! Some clauses call `returnCek`, some `computeCek`, achieving recursive calling similar to our current implementation.
+
     -- details of `forceEvaluate`, `applyEvaluate` etc to be worked out.
 
     -- similarly for the returning step
 
     returnCek = if debug then returnCekDebug else returnCekStep
     {-# NOINLINE returnCek #-}
-    
+
     returnCekDebug = ...
 
-    
-    returnCekStep 
+
+    returnCekStep
         :: forall uni fun s
         . (PrettyUni uni fun, GivenCekReqs uni fun s)
         => WordArray
@@ -123,16 +119,16 @@ enterComputeCek debug ctx (Closure term env) =
     <other_clauses>
 ```
 
-This trick lets us inline the "step" functions and call them recursively like before. 
-Because when we are not debugging, we are still using basically the same code as our current implementation, the performance should not be affected by much. 
+This trick lets us inline the "step" functions and call them recursively like before.
+Because when we are not debugging, we are still using basically the same code as our current implementation, the performance should not be affected by much.
 (Given that the machine is tail-recursive, the additional wrapping of the returned term in the `Terminating` constructor will affect performance in a negligible way.)
 
 ## Implications
 
-This is a draft of an idea. 
-There are further details to be worked out in a prototype. 
+This is a draft of an idea.
+There are further details to be worked out in a prototype.
 The implementor should use their own judgement.
 
-Whether we proceed with this approach or not depends on how the prototyping goes, and its benchmarking results. 
-If we find that the slow down is negligible enough, then we may proceed with this. 
+Whether we proceed with this approach or not depends on how the prototyping goes, and its benchmarking results.
+If we find that the slow down is negligible enough, then we may proceed with this.
 Otherwise, we proceed with a separate implementation for the debugging machine.

doc/docusaurus/docs/adr/adr4.md → doc/adr/adr4.md

@@ -1,14 +1,10 @@
----
-sidebar_position: 25
----
-
 # ADR 4: Deferred unlifting in Plutus Core
 
 Date: 2022-11
 
 ## Authors
 
-[Michael Peyton Jones](mailto:michael.peyton-jones@iohk.io) 
+[Michael Peyton Jones](mailto:michael.peyton-jones@iohk.io)
 
 ## Status
 
@@ -24,7 +20,7 @@ This is necessary in order to apply the denotation of the builtin being applied,
 However, unlifting can fail: we cannot unlift a _string_ constant into a Haskell integer.
 This failure is visible in program execution, since it terminates the program with an error.
 
-The original design of the builtin application machinery performed unlifting of an argument as soon as it was received. 
+The original design of the builtin application machinery performed unlifting of an argument as soon as it was received.
 This meant that unlifting failures would surface at that point, whereas most of the errors that relate to builtin evaluation can only occur once the builtin has all its arguments, since that's when we run the actual function.
 
 For example:
@@ -57,7 +53,7 @@ Consequently, we felt that it was safe to change the default unlifting behaviour
 
 However, in order to gain the full benefit of simplification, we would like to remove the existence of immediate unlifting entirely.
 If historical script evaluations on the chain still rely on immediate unlifting, then we must support it (and specify it) forever.
-However, once the default has changed, if the history of the chain still validates with _deferred_ unlifting, then we know that no historical script evaluations relied on that behaviour. 
+However, once the default has changed, if the history of the chain still validates with _deferred_ unlifting, then we know that no historical script evaluations relied on that behaviour.
 At that point we can _unconditionally_ enable deferred unlifting without worrying about not being able to validate the chain.
 
 In theory, there could be outputs locked with script hashes whose behaviour would (if they are ever spent) rely on inmmediate unlifting.