Skip to content

Commit

Permalink
Remove ADRs from user documentation (IntersectMBO#6401)
Browse files Browse the repository at this point in the history
  • Loading branch information
zliu41 authored Aug 10, 2024
1 parent ffe8f15 commit de3150e
Show file tree
Hide file tree
Showing 6 changed files with 57 additions and 86 deletions.
9 changes: 2 additions & 7 deletions doc/docusaurus/docs/adr/adr-index.md → doc/adr/README.md
Original file line number Diff line number Diff line change
@@ -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:
Expand All @@ -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.

10 changes: 3 additions & 7 deletions doc/docusaurus/docs/adr/adr1.md → doc/adr/adr1.md
Original file line number Diff line number Diff line change
@@ -1,7 +1,3 @@
---
sidebar_position: 10
---

# ADR 1: Record architectural decisions

Date: 2022-06-08
Expand All @@ -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.

Expand All @@ -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.
Expand Down Expand Up @@ -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
Expand Down
48 changes: 22 additions & 26 deletions doc/docusaurus/docs/adr/adr2.md → doc/adr/adr2.md
Original file line number Diff line number Diff line change
@@ -1,7 +1,3 @@
---
sidebar_position: 15
---

# ADR 2: Steppable CEK machine

Date: 2022-10
Expand All @@ -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
Expand All @@ -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)
```

Expand All @@ -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
Expand All @@ -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.

Expand Down Expand Up @@ -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`.
Expand All @@ -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:
Expand Down Expand Up @@ -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.
Expand All @@ -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)
Expand Down
58 changes: 27 additions & 31 deletions doc/docusaurus/docs/adr/adr3.md → doc/adr/adr3.md
Original file line number Diff line number Diff line change
@@ -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

Expand All @@ -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.
Expand All @@ -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
Expand All @@ -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
Expand All @@ -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
Expand All @@ -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
Expand All @@ -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.
10 changes: 3 additions & 7 deletions doc/docusaurus/docs/adr/adr4.md → doc/adr/adr4.md
Original file line number Diff line number Diff line change
@@ -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

Expand All @@ -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:
Expand Down Expand Up @@ -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.
Expand Down
8 changes: 0 additions & 8 deletions doc/docusaurus/docs/adr/_category_.json

This file was deleted.

0 comments on commit de3150e

Please sign in to comment.