Computation Threads

Steps:

1. Parses the computation state from its datum StepDatum.
2. /Optionally/ receives args from its redeemer to /guide/ the computation step.
3. Adv the computation by /the step/, producing a new comp state.
4. Suspends the comp by serializing the new comp state into a new datum

I drop this, and moved to something simpler.

Datum

Datum only holds who is computing.

structure ComputationThreads.Datum.StepDatum (α : Type) : Type

• fraud_prover : VKeyHash
• block_id : Tokens.Elem.TId
• data : α
• name : String

Definition of the ComputationState:

• A State
• No state, indicating the end of the computation
• Error state, not so sure about this state. Computation ending is not very concrete yet.

inductive ComputationThreads.Datum.ComputationState (α : Type) : Type

• State {α : Type} : α → ComputationState α
• Empty {α : Type} : ComputationState α
• Error {α : Type} : ComputationState α

structure ComputationThreads.Datum.Thread (α β : Type) : Type

• datum : StepDatum (ComputationState α)
• steps : List (α → β → ComputationState α)

@[reducible, inline]

abbrev ComputationThreads.Datum.ComputationThreads (α β : Type) : Type

Equations

• ComputationThreads.Datum.ComputationThreads α β = Tokens.State.Tokens (ComputationThreads.Datum.Thread α β)